defmodule Tdd do
  # --- Existing code from your previous version ---
  # (init_tdd_system, get_state, update_state, make_node, get_node_details,
  #  variable definitions, basic type constructors, apply, sum, print_tdd)
  # Ensure your `apply/4` function is the corrected version from the MatchError fix.
  @moduledoc """
  Ternary decision diagram for set-theoretic types.
  """

  # --- Terminal Node IDs ---
  @false_node_id 0
  @true_node_id 1

  defguard is_terminal_id(id) when id == @false_node_id or id == @true_node_id

  def init_tdd_system do
    Process.put(:nodes, %{})

    Process.put(:node_by_id, %{@false_node_id => :false_terminal, @true_node_id => :true_terminal})

    Process.put(:next_id, 2)
    Process.put(:op_cache, %{})
    IO.puts("TDD system initialized.")
  end

  defp get_state do
    %{
      nodes: Process.get(:nodes, %{}),
      node_by_id:
        Process.get(:node_by_id, %{
          @false_node_id => :false_terminal,
          @true_node_id => :true_terminal
        }),
      next_id: Process.get(:next_id, 2),
      op_cache: Process.get(:op_cache, %{})
    }
  end

  defp update_state(changes) do
    current_state = get_state()
    new_state = Map.merge(current_state, changes)
    Process.put(:nodes, new_state.nodes)
    Process.put(:node_by_id, new_state.node_by_id)
    Process.put(:next_id, new_state.next_id)
    Process.put(:op_cache, new_state.op_cache)
  end

  # --- Raw Node Creation (Structural) ---
  # This is the original make_node, focused on structural uniqueness and basic reduction rule.
  defp make_node_raw(variable, yes_id, no_id, dc_id) do
    # Basic reduction: if all children are identical, this node is redundant.
    if yes_id == no_id && yes_id == dc_id do
      yes_id
    else
      state = get_state()
      node_tuple = {variable, yes_id, no_id, dc_id}

      if Map.has_key?(state.nodes, node_tuple) do
        # Node already exists (structural sharing)
        state.nodes[node_tuple]
      else
        # Create new node
        new_id = state.next_id

        update_state(%{
          nodes: Map.put(state.nodes, node_tuple, new_id),
          node_by_id: Map.put(state.node_by_id, new_id, node_tuple),
          next_id: new_id + 1
        })

        new_id
      end
    end
  end

  # --- Public Node Creation (Currently same as raw, apply will handle context) ---
  # The `apply` algorithm inherently creates the necessary structure.
  # Semantic simplification is applied *after* `apply` completes.
  def make_node(variable, yes_id, no_id, dc_id) do
    make_node_raw(variable, yes_id, no_id, dc_id)
  end

  # --- Semantic Constraint Checking ---
  # assumptions_map is {variable_id => value (true, false, :dc)}
  defp check_assumptions_consistency(assumptions_map) do
    # Check 1: Primary type mutual exclusivity
    primary_true_predicates =
      Enum.reduce(assumptions_map, MapSet.new(), fn
        {{0, predicate_name}, true}, acc_set -> MapSet.put(acc_set, predicate_name)
        _otherwise, acc_set -> acc_set
      end)

    if MapSet.size(primary_true_predicates) > 1 do
      # IO.inspect(assumptions_map, label: "Contradiction: Primary Types")
      :contradiction
    else
      # Check 2: Specific atom value conflicts, e.g. {1, :value, :foo} == true AND {1, :value, :bar} == true
      atom_value_trues =
        Enum.reduce(assumptions_map, MapSet.new(), fn
          {{1, :value, atom_val}, true}, acc_set -> MapSet.put(acc_set, atom_val)
          _otherwise, acc_set -> acc_set
        end)

      if MapSet.size(atom_value_trues) > 1 do
        # IO.inspect(assumptions_map, label: "Contradiction: Atom Values")
        :contradiction
      else
        # Check 3: Tuple size conflicts, e.g. {4, :size, 2} == true AND {4, :size, 3} == true
        tuple_size_trues =
          Enum.reduce(assumptions_map, MapSet.new(), fn
            {{4, :size, size_val}, true}, acc_set -> MapSet.put(acc_set, size_val)
            _otherwise, acc_set -> acc_set
          end)

        if MapSet.size(tuple_size_trues) > 1 do
          # IO.inspect(assumptions_map, label: "Contradiction: Tuple Sizes")
          :contradiction
        else
          # Add more checks as new variable types are introduced
          :consistent
        end
      end
    end
  end

  # --- Semantic Simplification (Memoized) ---
  defp simplify_with_constraints(tdd_id, assumptions_map) do
    state = get_state()
    sorted_assumptions_list = Enum.sort_by(assumptions_map, fn {var, _val} -> var end)
    cache_key = {:simplify_constr, tdd_id, sorted_assumptions_list}

    # Order of checks is critical:
    # 1. Is the current set of assumptions inherently contradictory? If so, this path is dead.
    # 2. Is the TDD itself terminal? (Assumptions are consistent at this point)
    if check_assumptions_consistency(assumptions_map) == :contradiction do
      # IO.inspect({tdd_id, assumptions_map}, label: "SimplifyContradiction (Early Exit)")
      # No need to cache here if it's based purely on assumptions,
      # but if tdd_id was involved, caching the result for {tdd_id, assumptions} is good.
      # Let's cache it for safety, as tdd_id is part of cache_key.
      update_state(%{op_cache: Map.put(state.op_cache, cache_key, @false_node_id)})
      @false_node_id
    else
      # 3. Cache lookup
      if is_terminal_id(tdd_id) do
        # IO.inspect({tdd_id, assumptions_map}, label: "SimplifyTerminal")
        # Terminals are not affected by further assumptions if not contradictory
        tdd_id
      else
        if Map.has_key?(state.op_cache, cache_key) do
          # IO.inspect({tdd_id, assumptions_map}, label: "SimplifyFromCache")
          state.op_cache[cache_key]
        else
          # 4. Not contradictory, not terminal, not in cache: Process the node
          {var, y, n, d} = get_node_details(tdd_id)
          # IO.inspect({tdd_id, assumptions_map, var}, label: "SimplifyProcessingNode")
          result_id =
            case Map.get(assumptions_map, var) do
              true ->
                simplify_with_constraints(y, assumptions_map)

              false ->
                simplify_with_constraints(n, assumptions_map)

              :dc ->
                simplify_with_constraints(d, assumptions_map)

              nil ->
                simplified_y = simplify_with_constraints(y, Map.put(assumptions_map, var, true))
                simplified_n = simplify_with_constraints(n, Map.put(assumptions_map, var, false))
                simplified_d = simplify_with_constraints(d, Map.put(assumptions_map, var, :dc))
                make_node_raw(var, simplified_y, simplified_n, simplified_d)
            end

          # IO.inspect({tdd_id, assumptions_map, result_id}, label: "SimplifyExitComputed")
          update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
          result_id
        end
      end
    end

    # End of nested cond/if
  end

  # --- Public Node Creation (Used by Type Constructors) ---
  # Type constructors will create a raw TDD and then simplify it.
  defp make_node_for_constructors(variable, yes_id, no_id, dc_id) do
    raw_id = make_node_raw(variable, yes_id, no_id, dc_id)
    # Simplify with no initial assumptions
    simplify_with_constraints(raw_id, %{})
  end

  def get_node_details(id) when is_terminal_id(id) do
    if id == @true_node_id, do: :true_terminal, else: :false_terminal
  end

  def get_node_details(id) do
    state = get_state()
    state.node_by_id[id]
  end

  @v_is_atom {0, :is_atom}
  @v_is_tuple {0, :is_tuple}

  def v_atom_eq(atom_val), do: {1, :value, atom_val}
  def v_tuple_size_eq(size), do: {4, :size, size}
  def v_tuple_elem_pred(index, nested_pred_id), do: {4, :element, index, nested_pred_id}

  def type_any, do: @true_node_id
  def type_none, do: @false_node_id

  def type_atom do
    # Raw structure: if is_atom then True, else False, dc False
    # This structure is already semantically simple.
    make_node_for_constructors(@v_is_atom, @true_node_id, @false_node_id, @false_node_id)
  end

  def type_atom_literal(atom_val) do
    var_eq = v_atom_eq(atom_val)
    atom_val_node = make_node_raw(var_eq, @true_node_id, @false_node_id, @false_node_id)
    raw_node = make_node_raw(@v_is_atom, atom_val_node, @false_node_id, @false_node_id)
    simplify_with_constraints(raw_node, %{})
  end

  def type_tuple do
    make_node_for_constructors(@v_is_tuple, @true_node_id, @false_node_id, @false_node_id)
  end

  def type_empty_tuple do
    var_size_0 = v_tuple_size_eq(0)
    tuple_size_node = make_node_raw(var_size_0, @true_node_id, @false_node_id, @false_node_id)
    raw_node = make_node_raw(@v_is_tuple, tuple_size_node, @false_node_id, @false_node_id)
    simplify_with_constraints(raw_node, %{})
  end

  def type_tuple_sized_any(size) do
    var_size = v_tuple_size_eq(size)
    tuple_size_node = make_node_raw(var_size, @true_node_id, @false_node_id, @false_node_id)
    raw_node = make_node_raw(@v_is_tuple, tuple_size_node, @false_node_id, @false_node_id)
    simplify_with_constraints(raw_node, %{})
  end

  # --- The APPLY Algorithm (Core Logic, uses make_node_raw) ---
  # This function computes the raw structural result. Semantic simplification is applied by the caller.
  defp apply_raw(op_name, op_lambda, u1_id, u2_id) do
    state = get_state()
    # apply_raw cache key
    cache_key = {op_name, Enum.sort([u1_id, u2_id])}

    cond do
      Map.has_key?(state.op_cache, cache_key) ->
        state.op_cache[cache_key]

      is_terminal_id(u1_id) && is_terminal_id(u2_id) ->
        res_terminal_symbol = op_lambda.(get_node_details(u1_id), get_node_details(u2_id))
        if res_terminal_symbol == :true_terminal, do: @true_node_id, else: @false_node_id

      true ->
        u1_details = get_node_details(u1_id)
        u2_details = get_node_details(u2_id)

        result_id =
          cond do
            u1_details == :true_terminal or u1_details == :false_terminal ->
              {var2, y2, n2, d2} = u2_details
              res_y = apply_raw(op_name, op_lambda, u1_id, y2)
              res_n = apply_raw(op_name, op_lambda, u1_id, n2)
              res_d = apply_raw(op_name, op_lambda, u1_id, d2)
              make_node_raw(var2, res_y, res_n, res_d)

            u2_details == :true_terminal or u2_details == :false_terminal ->
              {var1, y1, n1, d1} = u1_details
              res_y = apply_raw(op_name, op_lambda, y1, u2_id)
              res_n = apply_raw(op_name, op_lambda, n1, u2_id)
              res_d = apply_raw(op_name, op_lambda, d1, u2_id)
              make_node_raw(var1, res_y, res_n, res_d)

            true ->
              {var1, y1, n1, d1} = u1_details
              {var2, y2, n2, d2} = u2_details
              # Elixir tuple comparison
              top_var = Enum.min([var1, var2])

              res_y =
                apply_raw(
                  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_raw(
                  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_raw(
                  op_name,
                  op_lambda,
                  if(var1 == top_var, do: d1, else: u1_id),
                  if(var2 == top_var, do: d2, else: u2_id)
                )

              make_node_raw(top_var, res_y, res_n, res_d)
          end

        update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
        result_id
    end
  end

  # --- Public Set Operations (API) ---
  def sum(tdd1_id, tdd2_id) do
    op_lambda_sum = fn
      :true_terminal, _ -> :true_terminal
      _, :true_terminal -> :true_terminal
      :false_terminal, t2_val -> t2_val
      t1_val, :false_terminal -> t1_val
    end

    raw_result_id = apply_raw(:sum, op_lambda_sum, tdd1_id, tdd2_id)
    simplify_with_constraints(raw_result_id, %{})
  end

  def intersect(tdd1_id, tdd2_id) do
    op_lambda_intersect = fn
      :false_terminal, _ -> :false_terminal
      _, :false_terminal -> :false_terminal
      :true_terminal, t2_val -> t2_val
      t1_val, :true_terminal -> t1_val
    end

    raw_result_id = apply_raw(:intersect, op_lambda_intersect, tdd1_id, tdd2_id)
    simplify_with_constraints(raw_result_id, %{})
  end

  def negate(tdd_id) do
    # Negation also needs semantic simplification wrapper if it can create complex structures,
    # but typically negation is structurally simple enough that raw ops are fine if children are simplified.
    # However, to be safe and ensure canonical form for ¬(A & B) vs ¬A | ¬B.
    raw_negated_id = negate_raw(tdd_id)
    simplify_with_constraints(raw_negated_id, %{})
  end

  # Renamed original negate
  defp negate_raw(tdd_id) do
    state = get_state()
    cache_key = {:negate_raw, tdd_id}

    cond do
      tdd_id == @true_node_id ->
        @false_node_id

      tdd_id == @false_node_id ->
        @true_node_id

      Map.has_key?(state.op_cache, cache_key) ->
        state.op_cache[cache_key]

      true ->
        {var, y, n, d} = get_node_details(tdd_id)
        # Negate children recursively using the public `negate` which includes simplification
        # Public negate to ensure children are simplified
        res_y = negate(y)
        res_n = negate(n)
        res_d = negate(d)
        result_id = make_node_raw(var, res_y, res_n, res_d)
        update_state(%{op_cache: Map.put(state.op_cache, cache_key, result_id)})
        result_id
    end
  end

  # --- Subtyping (API) ---
  def is_subtype(sub_type_id, super_type_id) do
    cond do
      sub_type_id == super_type_id ->
        true

      # none is subtype of anything
      sub_type_id == @false_node_id ->
        true

      # anything is subtype of any
      super_type_id == @true_node_id ->
        true

      true ->
        # A <: B  <=>  A ∩ (¬B) == ∅
        # All operations (intersect, negate) now produce semantically simplified results.
        negated_super = negate(super_type_id)
        intersection_result = intersect(sub_type_id, negated_super)
        # Check against canonical false
        intersection_result == @false_node_id
    end
  end

  def print_tdd(id, indent \\ 0) do
    prefix = String.duplicate("  ", indent)
    details = get_node_details(id)
    IO.puts("#{prefix}ID #{id}: #{inspect(details)}")

    case details do
      {_var, y, n, d} ->
        IO.puts("#{prefix}  Yes ->")
        print_tdd(y, indent + 1)
        IO.puts("#{prefix}  No  ->")
        print_tdd(n, indent + 1)
        IO.puts("#{prefix}  DC  ->")
        print_tdd(d, indent + 1)

      :true_terminal ->
        :ok

      :false_terminal ->
        :ok

      nil ->
        IO.puts("#{prefix} Error: Unknown ID #{id}")
    end
  end
end

# --- Example Usage ---
Tdd.init_tdd_system()

# Basic Types
tdd_foo = Tdd.type_atom_literal(:foo)
tdd_bar = Tdd.type_atom_literal(:bar)
tdd_atom = Tdd.type_atom()
tdd_empty_tuple = Tdd.type_empty_tuple()
tdd_any = Tdd.type_any()
tdd_none = Tdd.type_none()

test = fn name, expected, result ->
  current_failures = Process.get(:test_failures, [])

  if expected != result do
    Process.put(:test_failures, [name | current_failures])
  end

  status = if expected == result, do: "PASSED", else: "FAILED"
  IO.puts("#{name} (Expected: #{expected}) -> Result: #{result} - #{status}")
end

# Basic Types
tdd_foo = Tdd.type_atom_literal(:foo)
tdd_bar = Tdd.type_atom_literal(:bar)
tdd_baz = Tdd.type_atom_literal(:baz)
tdd_atom = Tdd.type_atom()
tdd_empty_tuple = Tdd.type_empty_tuple()
tdd_tuple = Tdd.type_tuple()
# Tuple of size 2, e.g. {any, any}
tdd_tuple_s2 = Tdd.type_tuple_sized_any(2)
tdd_any = Tdd.type_any()
tdd_none = Tdd.type_none()

test_all = fn ->
  IO.puts("\n--- TDD for :foo ---")
  Tdd.print_tdd(tdd_foo)

  IO.puts("\n--- TDD for not :foo ---")
  Tdd.print_tdd(Tdd.negate(tdd_foo))

  IO.puts("\n--- TDD for atom ---")
  Tdd.print_tdd(tdd_atom)

  IO.puts("\n--- TDD for not atom ---")
  # Expected: make_node(@v_is_atom, @false_node_id, @true_node_id, @true_node_id)
  # This represents "anything that is not an atom". The DC branch becomes true because if
  # "is_atom" test is irrelevant for "not atom", it means it's part of "not atom".
  Tdd.print_tdd(Tdd.negate(tdd_atom))

  IO.puts("\n--- TDD for :foo and :bar (should be none) ---")
  tdd_foo_and_bar = Tdd.intersect(tdd_foo, tdd_bar)
  # Expected ID 0: :false_terminal
  Tdd.print_tdd(tdd_foo_and_bar)

  IO.puts("\n--- TDD for :foo and atom (should be :foo) ---")
  tdd_foo_and_atom = Tdd.intersect(tdd_foo, tdd_atom)
  # Expected to be structurally identical to tdd_foo
  Tdd.print_tdd(tdd_foo_and_atom)
  IO.puts("\n--- Basic Subtyping Tests ---")
  test.(":foo <: atom", true, Tdd.is_subtype(tdd_foo, tdd_atom))
  test.("atom <: :foo", false, Tdd.is_subtype(tdd_atom, tdd_foo))
  test.(":foo <: :bar", false, Tdd.is_subtype(tdd_foo, tdd_bar))
  test.(":foo <: :foo", true, Tdd.is_subtype(tdd_foo, tdd_foo))
  test.("{} <: tuple", true, Tdd.is_subtype(tdd_empty_tuple, tdd_tuple))
  test.("tuple <: {}", false, Tdd.is_subtype(tdd_tuple, tdd_empty_tuple))
  test.(":foo <: {}", false, Tdd.is_subtype(tdd_foo, tdd_empty_tuple))
  test.("tuple_size_2 <: tuple", true, Tdd.is_subtype(tdd_tuple_s2, tdd_tuple))
  test.("tuple <: tuple_size_2", false, Tdd.is_subtype(tdd_tuple, tdd_tuple_s2))
  test.("tuple_size_2 <: {}", false, Tdd.is_subtype(tdd_tuple_s2, tdd_empty_tuple))

  IO.puts("\n--- Any/None Subtyping Tests ---")
  test.("any <: :foo", false, Tdd.is_subtype(tdd_any, tdd_foo))
  test.(":foo <: any", true, Tdd.is_subtype(tdd_foo, tdd_any))
  test.("none <: :foo", true, Tdd.is_subtype(tdd_none, tdd_foo))
  test.(":foo <: none", false, Tdd.is_subtype(tdd_foo, tdd_none))
  test.("none <: any", true, Tdd.is_subtype(tdd_none, tdd_any))
  test.("any <: none", false, Tdd.is_subtype(tdd_any, tdd_none))
  test.("any <: any", true, Tdd.is_subtype(tdd_any, tdd_any))
  test.("none <: none", true, Tdd.is_subtype(tdd_none, tdd_none))

  IO.puts("\n--- Union related Subtyping ---")
  tdd_foo_or_bar = Tdd.sum(tdd_foo, tdd_bar)
  tdd_foo_or_bar_or_baz = Tdd.sum(tdd_foo_or_bar, tdd_baz)

  test.(":foo <: (:foo | :bar)", true, Tdd.is_subtype(tdd_foo, tdd_foo_or_bar))
  test.(":baz <: (:foo | :bar)", false, Tdd.is_subtype(tdd_baz, tdd_foo_or_bar))
  test.("(:foo | :bar) <: atom", true, Tdd.is_subtype(tdd_foo_or_bar, tdd_atom))
  test.("atom <: (:foo | :bar)", false, Tdd.is_subtype(tdd_atom, tdd_foo_or_bar))

  test.(
    "(:foo | :bar) <: (:foo | :bar | :baz)",
    true,
    Tdd.is_subtype(tdd_foo_or_bar, tdd_foo_or_bar_or_baz)
  )

  test.(
    "(:foo | :bar | :baz) <: (:foo | :bar)",
    false,
    Tdd.is_subtype(tdd_foo_or_bar_or_baz, tdd_foo_or_bar)
  )

  # Test against a non-member of the union
  test.("(:foo | :bar) <: :baz", false, Tdd.is_subtype(tdd_foo_or_bar, tdd_baz))

  IO.puts("\n--- Intersection related Subtyping ---")
  # Should be equivalent to tdd_foo
  tdd_atom_and_foo = Tdd.intersect(tdd_atom, tdd_foo)
  # Should be tdd_none
  tdd_atom_and_tuple = Tdd.intersect(tdd_atom, tdd_tuple)

  test.("(atom & :foo) <: :foo", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_foo))
  test.(":foo <: (atom & :foo)", true, Tdd.is_subtype(tdd_foo, tdd_atom_and_foo))
  test.("(atom & tuple) <: none", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_none))
  test.("none <: (atom & tuple)", true, Tdd.is_subtype(tdd_none, tdd_atom_and_tuple))
  test.("(atom & :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_and_foo, tdd_bar))
  # An intersection is a subtype of its components
  test.("(atom & :foo) <: atom", true, Tdd.is_subtype(tdd_atom_and_foo, tdd_atom))
  # (none <: atom)
  test.("(atom & tuple) <: atom", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_atom))
  # (none <: tuple)
  test.("(atom & tuple) <: tuple", true, Tdd.is_subtype(tdd_atom_and_tuple, tdd_tuple))

  IO.puts("\n--- Negation related Subtyping (Contrapositives) ---")
  # Reminder: ¬A <: ¬B  is equivalent to B <: A (contrapositive)

  # Test 1: ¬atom <: ¬:foo  (Equivalent to :foo <: atom, which is true)
  test.("¬atom <: ¬:foo", true, Tdd.is_subtype(Tdd.negate(tdd_atom), Tdd.negate(tdd_foo)))

  # Test 2: ¬:foo <: ¬atom  (Equivalent to atom <: :foo, which is false)
  test.("¬:foo <: ¬atom", false, Tdd.is_subtype(Tdd.negate(tdd_foo), Tdd.negate(tdd_atom)))

  # Double negation
  test.("¬(¬:foo) <: :foo", true, Tdd.is_subtype(Tdd.negate(Tdd.negate(tdd_foo)), tdd_foo))
  test.(":foo <: ¬(¬:foo)", true, Tdd.is_subtype(tdd_foo, Tdd.negate(Tdd.negate(tdd_foo))))

  # Disjoint types
  test.("atom <: ¬tuple", true, Tdd.is_subtype(tdd_atom, Tdd.negate(tdd_tuple)))
  test.("tuple <: ¬atom", true, Tdd.is_subtype(tdd_tuple, Tdd.negate(tdd_atom)))
  test.(":foo <: ¬{}", true, Tdd.is_subtype(tdd_foo, Tdd.negate(tdd_empty_tuple)))

  IO.puts("\n--- Mixed Types & Complex Subtyping ---")
  tdd_atom_or_tuple = Tdd.sum(tdd_atom, tdd_tuple)
  tdd_foo_or_empty_tuple = Tdd.sum(tdd_foo, tdd_empty_tuple)

  test.(
    "(:foo | {}) <: (atom | tuple)",
    true,
    Tdd.is_subtype(tdd_foo_or_empty_tuple, tdd_atom_or_tuple)
  )

  test.(
    "(atom | tuple) <: (:foo | {})",
    false,
    Tdd.is_subtype(tdd_atom_or_tuple, tdd_foo_or_empty_tuple)
  )

  test.(":foo <: (atom | tuple)", true, Tdd.is_subtype(tdd_foo, tdd_atom_or_tuple))
  test.("{} <: (atom | tuple)", true, Tdd.is_subtype(tdd_empty_tuple, tdd_atom_or_tuple))

  # De Morgan's Law illustration (A | B = ¬(¬A & ¬B))
  # (:foo | :bar) <: ¬(¬:foo & ¬:bar)
  tdd_not_foo_and_not_bar = Tdd.intersect(Tdd.negate(tdd_foo), Tdd.negate(tdd_bar))

  test.(
    "(:foo | :bar) <: ¬(¬:foo & ¬:bar)",
    true,
    Tdd.is_subtype(tdd_foo_or_bar, Tdd.negate(tdd_not_foo_and_not_bar))
  )

  test.(
    "¬(¬:foo & ¬:bar) <: (:foo | :bar)",
    true,
    Tdd.is_subtype(Tdd.negate(tdd_not_foo_and_not_bar), tdd_foo_or_bar)
  )

  # Type difference: atom - :foo  (represented as atom & ¬:foo)
  tdd_atom_minus_foo = Tdd.intersect(tdd_atom, Tdd.negate(tdd_foo))
  test.("(atom - :foo) <: atom", true, Tdd.is_subtype(tdd_atom_minus_foo, tdd_atom))
  test.("(atom - :foo) <: :foo", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_foo))
  # True if :bar is in (atom - :foo)
  test.("(atom - :foo) <: :bar", false, Tdd.is_subtype(tdd_atom_minus_foo, tdd_bar))
  test.(":bar <: (atom - :foo)", true, Tdd.is_subtype(tdd_bar, tdd_atom_minus_foo))

  # (atom - :foo) | :foo should be atom
  tdd_recombined_atom = Tdd.sum(tdd_atom_minus_foo, tdd_foo)
  test.("((atom - :foo) | :foo) <: atom", true, Tdd.is_subtype(tdd_recombined_atom, tdd_atom))
  test.("atom <: ((atom - :foo) | :foo)", true, Tdd.is_subtype(tdd_atom, tdd_recombined_atom))

  # (atom | {}) & (tuple | :foo) must be (:foo | {})
  # Represents `atom() | {}`
  tdd_atom_or_empty = Tdd.sum(tdd_atom, tdd_empty_tuple)
  # Represents `tuple() | :foo`
  tdd_tuple_or_foo = Tdd.sum(tdd_tuple, tdd_foo)
  intersected_complex = Tdd.intersect(tdd_atom_or_empty, tdd_tuple_or_foo)
  # Expected result for intersected_complex is tdd_foo_or_empty_tuple

  test.(
    "(atom | {}) & (tuple | :foo) <: (:foo | {})",
    true,
    Tdd.is_subtype(intersected_complex, tdd_foo_or_empty_tuple)
  )

  test.(
    "(:foo | {}) <: (atom | {}) & (tuple | :foo)",
    true,
    Tdd.is_subtype(tdd_foo_or_empty_tuple, intersected_complex)
  )

  # {} | tuple_size_2 should be a subtype of tuple
  tdd_empty_or_s2 = Tdd.sum(tdd_empty_tuple, tdd_tuple_s2)
  test.("({} | tuple_size_2) <: tuple", true, Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple))

  test.(
    "({} | tuple_size_2) <: ({} | tuple_size_2)",
    true,
    Tdd.is_subtype(tdd_empty_or_s2, tdd_empty_or_s2)
  )

  test.(
    "({} | tuple_size_2) <: tuple_size_2",
    false,
    Tdd.is_subtype(tdd_empty_or_s2, tdd_tuple_s2)
  )

  IO.puts("\n--- TDD structure for (atom - :foo) ---")
  Tdd.print_tdd(tdd_atom_minus_foo)
  IO.puts("\n--- TDD structure for ((atom - :foo) | :foo) which should be 'atom' ---")
  Tdd.print_tdd(tdd_recombined_atom)
  IO.puts("\n--- TDD structure for 'atom' for comparison ---")
  Tdd.print_tdd(tdd_atom)

  IO.inspect(Process.get(:test_failures, []))
end

test_all.()