diff --git a/lib/til.ex b/lib/til.ex
index 23b50db..aa3ac5a 100644
--- a/lib/til.ex
+++ b/lib/til.ex
@@ -1435,10 +1435,12 @@ defmodule Tdd.Algo do
     cache_key = {:negate, tdd_id}
 
     case Store.get_op_cache(cache_key) do
+      # If the result is already cached (or in progress), return it.
       {:ok, result_id} ->
         result_id
 
       :not_found ->
+        # On cache miss, compute the negation.
         result_id =
           case Store.get_node(tdd_id) do
             {:ok, :true_terminal} ->
@@ -1447,17 +1449,44 @@ defmodule Tdd.Algo do
             {:ok, :false_terminal} ->
               Store.true_node_id()
 
+            # This is the main recursive case for an internal node.
             {:ok, {var, y, n, d}} ->
-              Store.find_or_create_node(var, negate(y), negate(n), negate(d))
+              # 1. Create a temporary placeholder and cache it immediately.
+              #    This acts as a co-inductive "hook". Any recursive call to negate
+              #    this same `tdd_id` will hit the cache and get this placeholder,
+              #    breaking the infinite recursion.
+              placeholder = Store.create_placeholder({:negation_of, tdd_id})
+              Store.put_op_cache(cache_key, placeholder)
 
-            # TODO: Handle placeholder nodes encountered during co-inductive simplification.
-            # A placeholder is treated as `any` for the check, so its negation is `none`.
+              # 2. Recursively negate the children.
+              neg_y = negate(y)
+              neg_n = negate(n)
+              neg_d = negate(d)
+
+              # 3. Build the main body of the negated TDD. If there was a cycle,
+              #    this structure will refer to the `placeholder` ID at its leaves.
+              body_id = Store.find_or_create_node(var, neg_y, neg_n, neg_d)
+
+              # 4. "Tie the knot": Replace any occurrences of the placeholder within the
+              #    newly created graph with the ID of the graph's root (`body_id`).
+              #    This correctly forms the cycle in the negated graph.
+              final_id = substitute(body_id, placeholder, body_id)
+
+              # 5. The canonical graph is now built. Update the cache with the
+              #    final, correct ID before returning.
+              Store.put_op_cache(cache_key, final_id)
+              final_id
+
+            # This case indicates a logical error. A fully compiled TDD passed to `negate`
+            # should not be a placeholder itself. This new implementation avoids the
+            # previous incorrect handling.
             {:ok, {:placeholder, _spec}} ->
-              IO.inspect("RETURNING FALSE FOR NEGATE PLACEHOLDER")
-              Store.false_node_id()
+              raise "Tdd.Algo.negate: Attempted to negate a raw placeholder node. This indicates a logic error in the calling algorithm."
+
+            {:error, reason} ->
+              raise "Tdd.Algo.negate: Failed to get node #{tdd_id}: #{reason}"
           end
 
-        Store.put_op_cache(cache_key, result_id)
         result_id
     end
   end
@@ -1779,108 +1808,109 @@ defmodule Tdd.Algo do
          # This is the coinductive context (a MapSet).
          context
        ) do
-    {var, y, n, d} = node_details
-    assumptions = Map.new(sorted_assumptions)
+    # --- BEGIN IMPROVEMENT ---
+    # Co-inductive check for the constraint ID itself. If we are being asked to
+    # reason about a constraint that is a placeholder (i.e., part of a cycle
+    # currently being built), we must avoid operating on it directly. The correct
+    # co-inductive assumption is that the check succeeds, so we proceed down
+    # the 'yes' path without performing invalid logic on the placeholder.
+    case Store.get_node(constraint_id) do
+      {:ok, {:placeholder, _}} ->
+        {_var, y, _n, _d} = node_details
 
-    # 1. Build the TDD for the sub-problem's effective type by intersecting all
-    #    its constraints from the current assumption set.
-    op_intersect = fn
-      :false_terminal, _ -> :false_terminal
-      _, :false_terminal -> :false_terminal
-      t, :true_terminal -> t
-      :true_terminal, t -> t
-    end
-
-    sub_problem_constraints =
-      Enum.filter(assumptions, fn {v, _} ->
-        (Tdd.Predicate.Info.get_traits(v) || %{})[:sub_key] == sub_key
-      end)
-
-    sub_problem_tdd_id =
-      Enum.reduce(sub_problem_constraints, Store.true_node_id(), fn {var, val}, acc_id ->
-        constraint_for_this_assumption = Engine.unwrap_var(var)
-
-        id_to_intersect =
-          if val, do: constraint_for_this_assumption, else: negate(constraint_for_this_assumption)
-
-        apply(:intersect, op_intersect, acc_id, id_to_intersect)
-      end)
-
-    # 2. Check for the three logical outcomes:
-    #    - Does the path imply the constraint is satisfied?
-    #    - Does the path imply the constraint is violated?
-    #    - Or are both outcomes still possible?
-
-    # Implies satisfied: `sub_problem_tdd_id <: constraint_id`
-    # This is equivalent to `(sub_problem_tdd_id & !constraint_id)` being empty.
-    neg_constraint_id = negate(constraint_id)
-
-    intersect_sub_with_neg_constraint =
-      apply(:intersect, op_intersect, sub_problem_tdd_id, neg_constraint_id)
-
-    implies_satisfied =
-      check_emptiness(intersect_sub_with_neg_constraint) == Store.false_node_id()
-
-    # Implies violated: `sub_problem_tdd_id` and `constraint_id` are disjoint.
-    # This is equivalent to `(sub_problem_tdd_id & constraint_id)` being empty.
-    intersect_sub_with_constraint =
-      apply(:intersect, op_intersect, sub_problem_tdd_id, constraint_id)
-
-    implies_violated = check_emptiness(intersect_sub_with_constraint) == Store.false_node_id()
-
-    # 3. Branch based on the logical outcome.
-    cond do
-      implies_satisfied and implies_violated ->
-        # The sub-problem itself must be empty/impossible under the current assumptions.
-        # This whole path is a contradiction.
-        Store.false_node_id()
-
-      implies_satisfied ->
-        # The constraint is guaranteed by the path. Follow the 'yes' branch.
-        # The assumptions already imply this, so no change to them is needed.
         case algo_type do
           :simplify -> do_simplify(y, sorted_assumptions, context)
           :check_emptiness -> do_check_emptiness(y, sorted_assumptions, context)
         end
 
-      implies_violated ->
-        # The constraint is impossible given the path. Follow the 'no' branch.
-        # We can add this new fact `{var, false}` to strengthen the assumptions.
-        new_assumptions = Map.put(assumptions, var, false) |> Enum.sort()
+      # If the constraint_id is a valid, fully-formed node, proceed with the original logic.
+      _ ->
+        # --- END IMPROVEMENT ---
+        {var, y, n, d} = node_details
+        assumptions = Map.new(sorted_assumptions)
 
-        case algo_type do
-          :simplify -> do_simplify(n, new_assumptions, context)
-          :check_emptiness -> do_check_emptiness(n, new_assumptions, context)
+        # 1. Build the TDD for the sub-problem's effective type by intersecting all
+        #    its constraints from the current assumption set.
+        op_intersect = fn
+          :false_terminal, _ -> :false_terminal
+          _, :false_terminal -> :false_terminal
+          t, :true_terminal -> t
+          :true_terminal, t -> t
         end
 
-      true ->
-        # Neither outcome is guaranteed. Both are possible.
-        # We must explore both branches and combine the results.
-        new_assumptions_for_no_branch = Map.put(assumptions, var, false) |> Enum.sort()
+        sub_problem_constraints =
+          Enum.filter(assumptions, fn {v, _} ->
+            (Tdd.Predicate.Info.get_traits(v) || %{})[:sub_key] == sub_key
+          end)
 
-        case algo_type do
-          :check_emptiness ->
-            # Is there ANY path to true? Explore both and take their union.
-            res_y = do_check_emptiness(y, sorted_assumptions, context)
-            res_n = do_check_emptiness(n, new_assumptions_for_no_branch, context)
+        sub_problem_tdd_id =
+          Enum.reduce(sub_problem_constraints, Store.true_node_id(), fn {var, val}, acc_id ->
+            constraint_for_this_assumption = Engine.unwrap_var(var)
 
-            # Define local terminal logic for union
-            op_union = fn
-              :true_terminal, _ -> :true_terminal
-              _, :true_terminal -> :true_terminal
-              t, :false_terminal -> t
-              :false_terminal, t -> t
+            id_to_intersect =
+              if val,
+                do: constraint_for_this_assumption,
+                else: negate(constraint_for_this_assumption)
+
+            apply(:intersect, op_intersect, acc_id, id_to_intersect)
+          end)
+
+        # 2. Check for the three logical outcomes...
+        neg_constraint_id = negate(constraint_id)
+
+        intersect_sub_with_neg_constraint =
+          apply(:intersect, op_intersect, sub_problem_tdd_id, neg_constraint_id)
+
+        implies_satisfied =
+          check_emptiness(intersect_sub_with_neg_constraint) == Store.false_node_id()
+
+        intersect_sub_with_constraint =
+          apply(:intersect, op_intersect, sub_problem_tdd_id, constraint_id)
+
+        implies_violated = check_emptiness(intersect_sub_with_constraint) == Store.false_node_id()
+
+        # 3. Branch based on the logical outcome.
+        cond do
+          implies_satisfied and implies_violated ->
+            Store.false_node_id()
+
+          implies_satisfied ->
+            case algo_type do
+              :simplify -> do_simplify(y, sorted_assumptions, context)
+              :check_emptiness -> do_check_emptiness(y, sorted_assumptions, context)
             end
 
-            apply(:sum, op_union, res_y, res_n)
+          implies_violated ->
+            new_assumptions = Map.put(assumptions, var, false) |> Enum.sort()
 
-          :simplify ->
-            # Simplify both sub-trees and rebuild the node, as we cannot simplify this node away.
-            res_y = do_simplify(y, sorted_assumptions, context)
-            res_n = do_simplify(n, new_assumptions_for_no_branch, context)
-            # 'dc' branch is independent of 'var'
-            res_d = do_simplify(d, sorted_assumptions, context)
-            Store.find_or_create_node(var, res_y, res_n, res_d)
+            case algo_type do
+              :simplify -> do_simplify(n, new_assumptions, context)
+              :check_emptiness -> do_check_emptiness(n, new_assumptions, context)
+            end
+
+          true ->
+            new_assumptions_for_no_branch = Map.put(assumptions, var, false) |> Enum.sort()
+
+            case algo_type do
+              :check_emptiness ->
+                res_y = do_check_emptiness(y, sorted_assumptions, context)
+                res_n = do_check_emptiness(n, new_assumptions_for_no_branch, context)
+
+                op_union = fn
+                  :true_terminal, _ -> :true_terminal
+                  _, :true_terminal -> :true_terminal
+                  t, :false_terminal -> t
+                  :false_terminal, t -> t
+                end
+
+                apply(:sum, op_union, res_y, res_n)
+
+              :simplify ->
+                res_y = do_simplify(y, sorted_assumptions, context)
+                res_n = do_simplify(n, new_assumptions_for_no_branch, context)
+                res_d = do_simplify(d, sorted_assumptions, context)
+                Store.find_or_create_node(var, res_y, res_n, res_d)
+            end
         end
     end
   end