diff --git a/new.exs b/new.exs
index 98a7773..fbdcfde 100644
--- a/new.exs
+++ b/new.exs
@@ -682,10 +682,9 @@ defmodule Tdd.Consistency.Engine do
       end)
 
     # Attempt to merge the new implications into the set of all assumptions.
-    case Enum.reduce(implications, {:ok, %{}}, fn {implied_var, implied_val},
-                                                   acc ->
-      reduce_implication({implied_var, implied_val}, all_assumptions, acc)
-    end) do
+    case Enum.reduce(implications, {:ok, %{}}, fn {implied_var, implied_val}, acc ->
+           reduce_implication({implied_var, implied_val}, all_assumptions, acc)
+         end) do
       {:error, :contradiction} ->
         # A direct contradiction was found during expansion.
         :error
@@ -792,7 +791,12 @@ defmodule Tdd.Consistency.Engine do
         end
       end)
 
-    case result, do: (:invalid -> :error; _ -> :ok)
+    case result,
+      do:
+        (
+          :invalid -> :error
+          _ -> :ok
+        )
   end
 
   # Helper to check if a new range is valid and continue/halt the reduction.
@@ -814,7 +818,9 @@ defmodule Tdd.Consistency.Engine do
           case Info.get_traits(var) do
             %{type: :list_recursive_ambient, ambient_constraint_spec: spec} ->
               Map.merge(acc, %{head: spec, tail: spec})
-            _ -> acc
+
+            _ ->
+              acc
           end
 
         _, acc ->
@@ -869,8 +875,11 @@ defmodule Tdd.Algo do
   def apply(op_name, op_lambda, u1_id, u2_id) do
     # Memoization wrapper
     cache_key = {:apply, op_name, Enum.sort([u1_id, u2_id])}
+
     case Store.get_op_cache(cache_key) do
-      {:ok, result_id} -> result_id
+      {:ok, result_id} ->
+        result_id
+
       :not_found ->
         result_id = do_apply(op_name, op_lambda, u1_id, u2_id)
         Store.put_op_cache(cache_key, result_id)
@@ -883,20 +892,60 @@ defmodule Tdd.Algo do
          {:ok, u2_details} <- Store.get_node(u2_id) do
       cond do
         (u1_details == :true_terminal or u1_details == :false_terminal) and
-        (u2_details == :true_terminal or u2_details == :false_terminal) ->
-          if op_lambda.(u1_details, u2_details) == :true_terminal, do: Store.true_node_id(), else: Store.false_node_id()
-        (u1_details == :true_terminal or u1_details == :false_terminal) ->
+            (u2_details == :true_terminal or u2_details == :false_terminal) ->
+          if op_lambda.(u1_details, u2_details) == :true_terminal,
+            do: Store.true_node_id(),
+            else: Store.false_node_id()
+
+        u1_details == :true_terminal or u1_details == :false_terminal ->
           {var2, y2, n2, d2} = u2_details
-          Store.find_or_create_node(var2, apply(op_name, op_lambda, u1_id, y2), apply(op_name, op_lambda, u1_id, n2), apply(op_name, op_lambda, u1_id, d2))
-        (u2_details == :true_terminal or u2_details == :false_terminal) ->
+
+          Store.find_or_create_node(
+            var2,
+            apply(op_name, op_lambda, u1_id, y2),
+            apply(op_name, op_lambda, u1_id, n2),
+            apply(op_name, op_lambda, u1_id, d2)
+          )
+
+        u2_details == :true_terminal or u2_details == :false_terminal ->
           {var1, y1, n1, d1} = u1_details
-          Store.find_or_create_node(var1, apply(op_name, op_lambda, y1, u2_id), apply(op_name, op_lambda, n1, u2_id), apply(op_name, op_lambda, d1, u2_id))
+
+          Store.find_or_create_node(
+            var1,
+            apply(op_name, op_lambda, y1, u2_id),
+            apply(op_name, op_lambda, n1, u2_id),
+            apply(op_name, op_lambda, d1, u2_id)
+          )
+
         true ->
-          {var1, y1, n1, d1} = u1_details; {var2, y2, n2, d2} = u2_details
+          {var1, y1, n1, d1} = u1_details
+          {var2, y2, n2, d2} = u2_details
           top_var = Enum.min([var1, var2])
-          res_y = apply(op_name, op_lambda, if(var1 == top_var, do: y1, else: u1_id), if(var2 == top_var, do: y2, else: u2_id))
-          res_n = apply(op_name, op_lambda, if(var1 == top_var, do: n1, else: u1_id), if(var2 == top_var, do: n2, else: u2_id))
-          res_d = apply(op_name, op_lambda, if(var1 == top_var, do: d1, else: u1_id), if(var2 == top_var, do: d2, else: u2_id))
+
+          res_y =
+            apply(
+              op_name,
+              op_lambda,
+              if(var1 == top_var, do: y1, else: u1_id),
+              if(var2 == top_var, do: y2, else: u2_id)
+            )
+
+          res_n =
+            apply(
+              op_name,
+              op_lambda,
+              if(var1 == top_var, do: n1, else: u1_id),
+              if(var2 == top_var, do: n2, else: u2_id)
+            )
+
+          res_d =
+            apply(
+              op_name,
+              op_lambda,
+              if(var1 == top_var, do: d1, else: u1_id),
+              if(var2 == top_var, do: d2, else: u2_id)
+            )
+
           Store.find_or_create_node(top_var, res_y, res_n, res_d)
       end
     end
@@ -906,15 +955,24 @@ defmodule Tdd.Algo do
   @spec negate(non_neg_integer) :: non_neg_integer
   def negate(tdd_id) do
     cache_key = {:negate, tdd_id}
+
     case Store.get_op_cache(cache_key) do
-      {:ok, result_id} -> result_id
+      {:ok, result_id} ->
+        result_id
+
       :not_found ->
         result_id =
           case Store.get_node(tdd_id) do
-            {:ok, :true_terminal} -> Store.false_node_id()
-            {:ok, :false_terminal} -> Store.true_node_id()
-            {:ok, {var, y, n, d}} -> Store.find_or_create_node(var, negate(y), negate(n), negate(d))
+            {:ok, :true_terminal} ->
+              Store.false_node_id()
+
+            {:ok, :false_terminal} ->
+              Store.true_node_id()
+
+            {:ok, {var, y, n, d}} ->
+              Store.find_or_create_node(var, negate(y), negate(n), negate(d))
           end
+
         Store.put_op_cache(cache_key, result_id)
         result_id
     end
@@ -926,8 +984,11 @@ defmodule Tdd.Algo do
     # Sort assumptions to ensure the cache key is canonical.
     sorted_assumptions = Enum.sort(assumptions)
     cache_key = {:simplify, tdd_id, sorted_assumptions}
+
     case Store.get_op_cache(cache_key) do
-      {:ok, result_id} -> result_id
+      {:ok, result_id} ->
+        result_id
+
       :not_found ->
         result_id = do_simplify(tdd_id, assumptions)
         Store.put_op_cache(cache_key, result_id)
@@ -942,16 +1003,25 @@ defmodule Tdd.Algo do
     else
       case Store.get_node(tdd_id) do
         # 2. Terminal nodes are already simple.
-        {:ok, :true_terminal} -> Store.true_node_id()
-        {:ok, :false_terminal} -> Store.false_node_id()
+        {:ok, :true_terminal} ->
+          Store.true_node_id()
+
+        {:ok, :false_terminal} ->
+          Store.false_node_id()
 
         # 3. Handle non-terminal nodes.
         {:ok, {var, y, n, d}} ->
           # 4. Check if the variable's value is already known or implied.
           case Map.get(assumptions, var) do
-            true -> simplify(y, assumptions)
-            false -> simplify(n, assumptions)
-            :dc -> simplify(d, assumptions)
+            true ->
+              simplify(y, assumptions)
+
+            false ->
+              simplify(n, assumptions)
+
+            :dc ->
+              simplify(d, assumptions)
+
             nil ->
               # The variable is not explicitly constrained. Check for implied constraints.
               # Note: For now, the Engine only performs flat checks.
@@ -959,9 +1029,15 @@ defmodule Tdd.Algo do
               implies_false = Engine.check(Map.put(assumptions, var, true)) == :contradiction
 
               cond do
-                implies_true and implies_false -> Store.false_node_id()
-                implies_true -> simplify(y, assumptions)
-                implies_false -> simplify(n, assumptions)
+                implies_true and implies_false ->
+                  Store.false_node_id()
+
+                implies_true ->
+                  simplify(y, assumptions)
+
+                implies_false ->
+                  simplify(n, assumptions)
+
                 true ->
                   # No constraint, so recursively simplify all branches.
                   s_y = simplify(y, Map.put(assumptions, var, true))
@@ -974,6 +1050,7 @@ defmodule Tdd.Algo do
     end
   end
 end
+
 defmodule Tdd.TypeReconstructor do
   @moduledoc """
   Reconstructs a high-level `TypeSpec` from a low-level assumption map.
@@ -1089,6 +1166,7 @@ defmodule Tdd.TypeReconstructor do
     TypeSpec.normalize({:intersect, specs})
   end
 end
+
 defmodule Tdd.Compiler do
   @moduledoc "Compiles a `TypeSpec` into a canonical TDD ID."
   alias Tdd.TypeSpec
@@ -1104,7 +1182,9 @@ defmodule Tdd.Compiler do
     cache_key = {:spec_to_id, normalized_spec}
 
     case Store.get_op_cache(cache_key) do
-      {:ok, id} -> id
+      {:ok, id} ->
+        id
+
       :not_found ->
         id = do_spec_to_id(normalized_spec)
         Store.put_op_cache(cache_key, id)
@@ -1117,46 +1197,121 @@ defmodule Tdd.Compiler do
     raw_id =
       case spec do
         # --- Base Types ---
-        :any -> Store.true_node_id()
-        :none -> Store.false_node_id()
-        :atom -> Store.find_or_create_node(Variable.v_is_atom(), Store.true_node_id(), Store.false_node_id(), Store.false_node_id())
-        :integer -> Store.find_or_create_node(Variable.v_is_integer(), Store.true_node_id(), Store.false_node_id(), Store.false_node_id())
+        :any ->
+          Store.true_node_id()
+
+        :none ->
+          Store.false_node_id()
+
+        :atom ->
+          Store.find_or_create_node(
+            Variable.v_is_atom(),
+            Store.true_node_id(),
+            Store.false_node_id(),
+            Store.false_node_id()
+          )
+
+        :integer ->
+          Store.find_or_create_node(
+            Variable.v_is_integer(),
+            Store.true_node_id(),
+            Store.false_node_id(),
+            Store.false_node_id()
+          )
+
         # Add :list, :tuple etc. here. They are simple structural TDDs.
-        :list -> Store.find_or_create_node(Variable.v_is_list(), Store.true_node_id(), Store.false_node_id(), Store.false_node_id())
+        :list ->
+          Store.find_or_create_node(
+            Variable.v_is_list(),
+            Store.true_node_id(),
+            Store.false_node_id(),
+            Store.false_node_id()
+          )
 
         # --- Literal Types ---
         {:literal, val} when is_atom(val) ->
-          eq_node = Store.find_or_create_node(Variable.v_atom_eq(val), Store.true_node_id(), Store.false_node_id(), Store.false_node_id())
-          Store.find_or_create_node(Variable.v_is_atom(), eq_node, Store.false_node_id(), Store.false_node_id())
+          eq_node =
+            Store.find_or_create_node(
+              Variable.v_atom_eq(val),
+              Store.true_node_id(),
+              Store.false_node_id(),
+              Store.false_node_id()
+            )
+
+          Store.find_or_create_node(
+            Variable.v_is_atom(),
+            eq_node,
+            Store.false_node_id(),
+            Store.false_node_id()
+          )
+
         {:literal, val} when is_integer(val) ->
-          eq_node = Store.find_or_create_node(Variable.v_int_eq(val), Store.true_node_id(), Store.false_node_id(), Store.false_node_id())
-          Store.find_or_create_node(Variable.v_is_integer(), eq_node, Store.false_node_id(), Store.false_node_id())
+          eq_node =
+            Store.find_or_create_node(
+              Variable.v_int_eq(val),
+              Store.true_node_id(),
+              Store.false_node_id(),
+              Store.false_node_id()
+            )
+
+          Store.find_or_create_node(
+            Variable.v_is_integer(),
+            eq_node,
+            Store.false_node_id(),
+            Store.false_node_id()
+          )
+
         {:literal, []} ->
-          empty_node = Store.find_or_create_node(Variable.v_list_is_empty(), Store.true_node_id(), Store.false_node_id(), Store.false_node_id())
-          Store.find_or_create_node(Variable.v_is_list(), empty_node, Store.false_node_id(), Store.false_node_id())
+          empty_node =
+            Store.find_or_create_node(
+              Variable.v_list_is_empty(),
+              Store.true_node_id(),
+              Store.false_node_id(),
+              Store.false_node_id()
+            )
+
+          Store.find_or_create_node(
+            Variable.v_is_list(),
+            empty_node,
+            Store.false_node_id(),
+            Store.false_node_id()
+          )
+
         # Add other literals as needed
 
         # --- Set-Theoretic Combinators ---
         {:union, specs} ->
           ids = Enum.map(specs, &spec_to_id/1)
+
           Enum.reduce(ids, Store.false_node_id(), fn id, acc ->
-            Algo.apply(:sum, fn
-              :true_terminal, _ -> :true_terminal
-              _, :true_terminal -> :true_terminal
-              :false_terminal, t2 -> t2
-              t1, :false_terminal -> t1
-            end, id, acc)
+            Algo.apply(
+              :sum,
+              fn
+                :true_terminal, _ -> :true_terminal
+                _, :true_terminal -> :true_terminal
+                :false_terminal, t2 -> t2
+                t1, :false_terminal -> t1
+              end,
+              id,
+              acc
+            )
           end)
 
         {:intersect, specs} ->
           ids = Enum.map(specs, &spec_to_id/1)
+
           Enum.reduce(ids, Store.true_node_id(), fn id, acc ->
-            Algo.apply(:intersect, fn
-              :false_terminal, _ -> :false_terminal
-              _, :false_terminal -> :false_terminal
-              :true_terminal, t2 -> t2
-              t1, :true_terminal -> t1
-            end, id, acc)
+            Algo.apply(
+              :intersect,
+              fn
+                :false_terminal, _ -> :false_terminal
+                _, :false_terminal -> :false_terminal
+                :true_terminal, t2 -> t2
+                t1, :true_terminal -> t1
+              end,
+              id,
+              acc
+            )
           end)
 
         {:negation, sub_spec} ->
@@ -1164,9 +1319,14 @@ defmodule Tdd.Compiler do
 
         # --- Recursive Types (STUBS for now) ---
         # These will be implemented in Step 3
-        {:list_of, _} -> raise "Tdd.Compiler: :list_of not yet implemented"
-        {:tuple, _} -> raise "Tdd.Compiler: {:tuple, [...]} not yet implemented"
-        {:cons, _, _} -> raise "Tdd.Compiler: :cons not yet implemented"
+        {:list_of, _} ->
+          raise "Tdd.Compiler: :list_of not yet implemented"
+
+        {:tuple, _} ->
+          raise "Tdd.Compiler: {:tuple, [...]} not yet implemented"
+
+        {:cons, _, _} ->
+          raise "Tdd.Compiler: :cons not yet implemented"
 
         # --- Default ---
         _ ->
@@ -1178,6 +1338,7 @@ defmodule Tdd.Compiler do
     Algo.simplify(raw_id)
   end
 end
+
 ####
 # xxx
 ####
@@ -2002,18 +2163,30 @@ defmodule TypeReconstructorTests do
     end
   end
 end
+
 defmodule CompilerAlgoTests do
   alias Tdd.Compiler
   alias Tdd.Store
+  alias Tdd.Algo
 
   # High-level helpers that mimic the final API
   defp is_subtype(spec1, spec2) do
     id1 = Compiler.spec_to_id(spec1)
     id2 = Compiler.spec_to_id(spec2)
-    # is_subtype(A, B) <=> (A & ~B) == none
-    neg_id2 = Tdd.Algo.negate(id2)
-    intersect_id = Tdd.Algo.apply(:intersect, &(&1 == :false_terminal or &2 == :false_terminal), id1, neg_id2)
-    final_id = Tdd.Algo.simplify(intersect_id)
+    # The subtyping check is: `A <: B` if and only if `A & ~B` is empty (`:none`).
+    neg_id2 = Algo.negate(id2)
+
+    op_intersect = fn
+      :false_terminal, _ -> :false_terminal
+      _, :false_terminal -> :false_terminal
+      t, :true_terminal -> t
+      :true_terminal, t -> t
+      # Default case for non-terminal nodes, though apply handles recursion
+      _t1, _t2 -> :non_terminal
+    end
+
+    intersect_id = Algo.apply(:intersect, op_intersect, id1, neg_id2)
+    final_id = Algo.simplify(intersect_id)
     final_id == Store.false_node_id()
   end
 
@@ -2021,11 +2194,16 @@ defmodule CompilerAlgoTests do
     Compiler.spec_to_id(spec1) == Compiler.spec_to_id(spec2)
   end
 
+  defp is_contradiction(spec) do
+    Compiler.spec_to_id(spec) == Store.false_node_id()
+  end
+
   defp test_subtype(name, expected, s1, s2), do: test(name, expected, is_subtype(s1, s2))
   defp test_equiv(name, expected, s1, s2), do: test(name, expected, are_equivalent(s1, s2))
-  defp test(name, exp, res) do 
+  defp test_contradiction(name, expected \\ true), do: &test(name, expected, is_contradiction(&1))
 
-    is_ok = exp==res
+  defp test(name, exp, res) do
+    is_ok = exp == res
     status = if is_ok, do: "[PASS]", else: "[FAIL]"
     IO.puts("#{status} #{name}")
 
@@ -2036,19 +2214,22 @@ defmodule CompilerAlgoTests do
     end
   end
 
-
   def run() do
     IO.puts("\n--- Running Compiler & Algo Integration Tests ---")
+    Process.put(:test_failures, [])
     # Setup
     Tdd.Store.init()
 
     # --- Section: Basic Compilation & Equivalence ---
+    IO.puts("\n--- Section: Basic Equivalences ---")
     test_equiv("atom & any == atom", true, {:intersect, [:atom, :any]}, :atom)
     test_equiv("atom | none == atom", true, {:union, [:atom, :none]}, :atom)
     test_equiv("atom & int == none", true, {:intersect, [:atom, :integer]}, :none)
     test_equiv("¬(¬atom) == atom", true, {:negation, {:negation, :atom}}, :atom)
+    test_equiv("atom | atom == atom", true, {:union, [:atom, :atom]}, :atom)
 
-    # --- Section: Subtyping Tests ---
+    # --- Section: Basic Subtyping ---
+    IO.puts("\n--- Section: Basic Subtyping ---")
     test_subtype(":foo <: atom", true, {:literal, :foo}, :atom)
     test_subtype("atom <: :foo", false, :atom, {:literal, :foo})
     test_subtype(":foo <: integer", false, {:literal, :foo}, :integer)
@@ -2056,26 +2237,136 @@ defmodule CompilerAlgoTests do
     test_subtype("none <: atom", true, :none, :atom)
     test_subtype("atom <: any", true, :atom, :any)
 
-    # --- Section: De Morgan's Law Check ---
-    # ¬(A | B) == (¬A & ¬B)
+    # --- Section: Integer Range Logic ---
+    IO.puts("\n--- Section: Integer Range Logic ---")
+    int_5_to_10 = {:integer_range, 5, 10}
+    int_7_to_8 = {:integer_range, 7, 8}
+    int_15_to_20 = {:integer_range, 15, 20}
+    int_0_to_100 = {:integer_range, 0, 100}
+
+    test_subtype("range(7..8) <: range(5..10)", true, int_7_to_8, int_5_to_10)
+    test_subtype("range(5..10) <: range(7..8)", false, int_5_to_10, int_7_to_8)
+    test_subtype("range(5..10) <: range(15..20)", false, int_5_to_10, int_15_to_20)
+
+    test_equiv(
+      "range(5..10) & range(7..8) == range(7..8)",
+      true,
+      {:intersect, [int_5_to_10, int_7_to_8]},
+      int_7_to_8
+    )
+
+    test_equiv(
+      "range(5..10) & range(0..100) == range(5..10)",
+      true,
+      {:intersect, [int_5_to_10, int_0_to_100]},
+      int_5_to_10
+    )
+
+    test_equiv(
+      "range(5..10) | range(7..8) == range(5..10)",
+      true,
+      {:union, [int_5_to_10, int_7_to_8]},
+      int_5_to_10
+    )
+
+    # --- Section: Contradictions & Simplifications ---
+    IO.puts("\n--- Section: Contradictions & Simplifications ---")
+
+    test_contradiction("atom & integer").({:intersect, [:atom, :integer]})
+
+    test_contradiction(":foo & :bar").({:intersect, [{:literal, :foo}, {:literal, :bar}]})
+
+    test_contradiction("atom & (int==5)").({:intersect, [:atom, {:literal, 5}]})
+
+    test_contradiction("range(5..10) & range(15..20)").({:intersect, [int_5_to_10, int_15_to_20]})
+
+    test_contradiction("integer & ¬integer").({:intersect, [:integer, {:negation, :integer}]})
+
+    # --- Section: Subtype Reduction in Normalization ---
+    IO.puts("\n--- Section: Subtype Reduction Logic ---")
+
+    test_equiv(
+      "(:foo | :bar | atom) simplifies to atom",
+      true,
+      {:union, [{:literal, :foo}, {:literal, :bar}, :atom]},
+      :atom
+    )
+
+    test_equiv(
+      "(range(5..10) | integer) simplifies to integer",
+      true,
+      {:union, [int_5_to_10, :integer]},
+      :integer
+    )
+
+    test_equiv(
+      "(:foo & atom) simplifies to :foo",
+      true,
+      {:intersect, [{:literal, :foo}, :atom]},
+      {:literal, :foo}
+    )
+
+    test_equiv(
+      "(range(5..10) & integer) simplifies to range(5..10)",
+      true,
+      {:intersect, [int_5_to_10, :integer]},
+      int_5_to_10
+    )
+
+    # --- Section: Logical Laws (Distribution and De Morgan's) ---
+    IO.puts("\n--- Section: Logical Laws ---")
+
+    # De Morgan's Law: ¬(A | B) == (¬A & ¬B)
     spec_not_a_or_b = {:negation, {:union, [:atom, :integer]}}
     spec_not_a_and_not_b = {:intersect, [{:negation, :atom}, {:negation, :integer}]}
-    test_equiv("De Morgan's Law holds", true, spec_not_a_or_b, spec_not_a_and_not_b)
+
+    test_equiv(
+      "De Morgan's (¬(A|B) == ¬A & ¬B) holds",
+      true,
+      spec_not_a_or_b,
+      spec_not_a_and_not_b
+    )
+
+    # De Morgan's Law: ¬(A & B) == (¬A | ¬B)
+    spec_not_a_and_b = {:negation, {:intersect, [{:literal, :foo}, int_5_to_10]}}
+    spec_not_a_or_not_b = {:union, [{:negation, {:literal, :foo}}, {:negation, int_5_to_10}]}
+
+    test_equiv(
+      "De Morgan's (¬(A&B) == ¬A | ¬B) holds",
+      true,
+      spec_not_a_and_b,
+      spec_not_a_or_not_b
+    )
+
+    # Distributive Law: A & (B | C) == (A & B) | (A & C)
+    spec_a = :integer
+    spec_b = {:integer_range, 0, 10}
+    spec_c = {:integer_range, 20, 30}
+    spec_dist_lhs = {:intersect, [spec_a, {:union, [spec_b, spec_c]}]}
+    spec_dist_rhs = {:union, [{:intersect, [spec_a, spec_b]}, {:intersect, [spec_a, spec_c]}]}
+
+    test_equiv(
+      "Distributive Law (A & (B|C)) holds",
+      true,
+      spec_dist_lhs,
+      spec_dist_rhs
+    )
 
     # --- Final Report ---
     failures = Process.get(:test_failures, [])
 
     if failures == [] do
-      IO.puts("\n✅ All CompilerAlgoTests  tests passed!")
+      IO.puts("\n✅ All Compiler & Algo Integration tests passed!")
     else
       IO.puts("\n❌ Found #{length(failures)} test failures.")
     end
   end
 end
+
 TypeSpecTests.run()
 TddStoreTests.run()
 TddVariableTests.run()
 # TddAlgoTests.run()
-# ConsistencyEngineTests.run()
-TypeReconstructorTests.run()
-CompilerAlgoTests.run()
+ConsistencyEngineTests.run()
+# TypeReconstructorTests.run()
+# CompilerAlgoTests.run()