diff --git a/test/til_test.exs b/test/til_test.exs
index cb4a9cc..bc64346 100644
--- a/test/til_test.exs
+++ b/test/til_test.exs
@@ -8,6 +8,7 @@ defmodule TddSystemTest do
   alias Tdd.Compiler
   alias Tdd.Consistency.Engine
   alias Tdd.Algo
+  alias Tdd.Debug
 
   # Helper to mimic the old test structure and provide better failure messages
   # for spec comparisons.
@@ -165,7 +166,7 @@ defmodule TddSystemTest do
       assert_spec_normalized({:negation, :integer}, {:negation, :integer})
     end
 
-    @doc "Tests that an odd number of negations simplifies to a single negation."
+    @doc "Tests that an odd integer of negations simplifies to a single negation."
     test "¬(¬(¬atom)) simplifies to ¬atom" do
       assert_spec_normalized({:negation, :atom}, {:negation, {:negation, {:negation, :atom}}})
     end
@@ -433,4 +434,173 @@ defmodule TddSystemTest do
       refute_subtype({:negation, {:list_of, :integer}}, :none)
     end
   end
+
+  describe "Logical Equivalences: De Morgan's Laws & Distributivity" do
+    @doc "Tests ¬(A ∪ B) <=> (¬A ∩ ¬B)"
+    test "De Morgan's Law for negated unions" do
+      # ¬(atom | integer)
+      spec1 = {:negation, {:union, [:atom, :integer]}}
+      # ¬atom & ¬integer
+      spec2 = {:intersect, [{:negation, :atom}, {:negation, :integer}]}
+      assert_equivalent_specs(spec1, spec2)
+    end
+
+    @doc "Tests ¬(A ∩ B) <=> (¬A ∪ ¬B)"
+    test "De Morgan's Law for negated intersections" do
+      # ¬(integer & atom)
+      spec1 = {:negation, {:intersect, [:integer, :atom]}}
+      # ¬integer | ¬atom
+      spec2 = {:union, [{:negation, :integer}, {:negation, :atom}]}
+      assert_equivalent_specs(spec1, spec2)
+    end
+
+    @doc "Tests A ∩ (B ∪ C) <=> (A ∩ B) ∪ (A ∩ C)"
+    test "Distributive Law: intersection over union" do
+      # We'll use types where some intersections are meaningful and others are :none
+      # `integer` is a supertype of `integer` and `tuple`
+      # `(integer | tuple) & (atom | integer)`
+      spec1 =
+        {:intersect, [{:union, [:integer, :tuple]}, {:union, [:atom, :integer]}]}
+
+      # Should be equivalent to:
+      # (integer & atom) | (integer & integer) | (tuple & atom) | (tuple & integer)
+      # which simplifies to:
+      # :none | :integer | :none | :none
+      # which is just :integer
+      Debug.print_tdd_graph(Compiler.spec_to_id(spec1))
+      assert_equivalent_specs(spec1, :integer)
+    end
+
+    @doc "Tests A | (B & C) versus (A | B) & (A | C) -- they are NOT always equivalent"
+    test "subtyping with distributivity" do
+      # Let's test `A | (B & C) <: (A | B) & (A | C)`
+      spec_left = {:union, [:atom, {:intersect, [:integer, :positive_integer]}]}
+
+      spec_right =
+        {:intersect, [{:union, [:atom, :integer]}, {:union, [:atom, :positive_integer]}]}
+
+      # `spec_left` normalizes to `atom | positive_integer`
+      # `spec_right` normalizes to `(atom | integer) & (atom | positive_integer)`
+      # Since `atom | positive_integer` is a subtype of `atom | integer`, the intersection on the right
+      # simplifies to `atom | positive_integer`. Therefore, they are equivalent in this case.
+      assert_equivalent_specs(spec_left, spec_right)
+
+      # However, let's create a case where it's only a subtype relationship
+      # `integer | (atom & pid)` should be `integer | :none` which is `integer`.
+      # `(integer | atom) & (integer | pid)` is a much larger type.
+      # simplifies to :integer
+      spec_sub = {:union, [:integer, {:intersect, [:atom, :pid]}]}
+      spec_super = {:intersect, [{:union, [:integer, :atom]}, {:union, [:integer, :pid]}]}
+      assert_subtype(spec_sub, spec_super)
+      refute_subtype(spec_super, spec_sub)
+    end
+  end
+
+  # ---
+  # Advanced Negation and Contradiction Tests
+  # ---
+  describe "Tdd.Compiler: Advanced Negation and Contradiction" do
+    @doc "Tests that a type and its negation correctly partition the universal set (:any)."
+    test "A | ¬A <=> :any" do
+      spec = {:union, [:integer, {:negation, :integer}]}
+      assert_equivalent_specs(spec, :any)
+    end
+
+    @doc "Tests that a subtype relationship holds against a negated supertype"
+    test "subtyping with negation: integer <: ¬atom" do
+      # An integer is never an atom, so it should be a subtype of "not atom".
+      assert_subtype(:integer, {:negation, :atom})
+      # The reverse is not true: `not atom` includes lists, integers, etc.
+      refute_subtype({:negation, :atom}, :integer)
+    end
+
+    @doc "A complex type that should resolve to :none"
+    test "complex contradiction involving subtype logic" do
+      # This is `(integer and not a integer)`. Since all integers are integers, this is impossible.
+      spec = {:intersect, [:integer, {:negation, :integer}]}
+      assert_equivalent_specs(spec, :none)
+    end
+
+    @doc "The type 'list of integers that are also atoms' should be impossible"
+    test "contradiction inside a recursive type structure" do
+      # list_of(integer & atom) is list_of(:none).
+      # A list of :none can only be the empty list, as no element can ever exist.
+      spec = {:list_of, {:intersect, [:integer, :atom]}}
+      assert_equivalent_specs(spec, {:literal, []})
+    end
+  end
+
+  # ---
+  # Complex Recursive (μ) and Polymorphic (Λ, Apply) Tests
+  # These tests probe the interaction between recursion, polymorphism, and subtyping.
+  # ---
+  describe "Tdd.Compiler: Interplay of μ, Λ, and Subtyping" do
+    @doc "Tests subtyping between structurally similar, but not identical, recursive types."
+    test "subtyping of structural recursive types: list_of(1|2) <: list_of(integer)" do
+      list_of_1_or_2 = {:list_of, {:union, [{:literal, 1}, {:literal, 2}]}}
+      list_of_integer = {:list_of, :integer}
+
+      assert_subtype(list_of_1_or_2, list_of_integer)
+      refute_subtype(list_of_integer, list_of_1_or_2)
+    end
+
+    @doc "Tests a non-sensical recursion that should simplify away"
+    test "μ-types that should normalize to a non-recursive form" do
+      # A type defined as "itself or an integer" should be equivalent to just "integer",
+      # because any finite instance of it must eventually terminate with an integer.
+      spec = {:mu, :X, {:union, [{:type_var, :X}, :integer]}}
+      assert_equivalent_specs(spec, :integer)
+
+      # A type defined as "a cons of an atom and itself, or none" should be equivalent to `list_of(atom)`.
+      # This tests if our manual mu-calculus definition matches the syntactic sugar.
+      manual_list_of_atom = {:mu, :L, {:union, [{:literal, []}, {:cons, :atom, {:type_var, :L}}]}}
+      sugar_list_of_atom = {:list_of, :atom}
+      assert_equivalent_specs(manual_list_of_atom, sugar_list_of_atom)
+    end
+
+    @doc "Tests polymorphism with multiple type parameters."
+    test "lambda with multiple parameters: (Λ(A,B). {A,B})(int, atom)" do
+      # λ(A, B). {A, B}
+      map_constructor = {:type_lambda, [:A, :B], {:tuple, [{:type_var, :A}, {:type_var, :B}]}}
+      # Apply it to integer and atom
+      applied_spec = {:type_apply, map_constructor, [:integer, :atom]}
+      # The result should be the concrete type {integer, atom}
+      expected_spec = {:tuple, [:integer, :atom]}
+
+      assert_equivalent_specs(applied_spec, expected_spec)
+    end
+
+    @doc "Tests that applying a lambda to a complex recursive type works correctly"
+    test "applying a polymorphic list constructor to a tree type" do
+      # First, define our tree type from a previous test
+      leaf_node = {:literal, :empty_tree}
+
+      tree_spec =
+        {:mu, :Tree,
+         {:union,
+          [
+            leaf_node,
+            {:tuple, [:atom, {:type_var, :Tree}, {:type_var, :Tree}]}
+          ]}}
+
+      # Now, apply the generic list lambda to this tree_spec
+      gen_list_lambda = {:type_lambda, [:T], {:list_of, {:type_var, :T}}}
+      list_of_trees = {:type_apply, gen_list_lambda, [tree_spec]}
+
+      # Check if a concrete instance is a subtype of this new complex type
+      tree_instance_1 = {:tuple, [{:literal, :a}, leaf_node, leaf_node]}
+      tree_instance_2 = {:tuple, [{:literal, :b}, leaf_node, leaf_node]}
+      list_of_trees_instance = {:cons, tree_instance_1, {:cons, tree_instance_2, {:literal, []}}}
+
+      assert_subtype(list_of_trees_instance, list_of_trees)
+    end
+
+    @doc "An 'ill-formed' recursive type that should evaluate to :none"
+    test "μ-types that are self-contradictory should be :none" do
+      # A type defined as `μX. cons(integer, X)`. This describes an infinite list
+      # of integers with no base case (`[]`). No finite value can ever satisfy this type.
+      infinite_list = {:mu, :X, {:cons, :integer, {:type_var, :X}}}
+      assert_equivalent_specs(infinite_list, :none)
+    end
+  end
 end