Lax Lean Archive

Version history

Submission versions

  1. lax-783278current version

    Arc Kayles is PSPACE-complete

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceOpen version
  2. lax-689614viewing

    Arc Kayles is PSPACE-complete

    Created Lean v4.33.0mathlib db584cd6d46c92f209a44c0f1c829460d327499d
    GitHub sourceShown on this page

Proof of `Passing and assigning either truth value`

groundedproofs/Lax689614Proofs/Passes.lean · lax-689614

What this proof establishes

no assumptions

thm✓Lax689614.Passes

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Strategy stealing shows that moving first cannot hurt True, and assigning an additional variable to True cannot hurt True. Induction on unassigned variables plus the pass supply eliminates passes and assignments benefiting the opponent.