Proof of `Correctness and complexity of the reduction` (3rd statement)
groundedproofs/Lax689614Proofs/TrueSimulation.lean · lax-689614
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Simulate True's CNF strategy until the formula is satisfied, then consume the remaining regular moves. The last phase uses paired replies on a protected biclique with surviving literal witnesses for every clause.