Proof Path Theory · Lean source
MissingSupport.lean
Selected results recorded Coverage and evidence
Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (1)
negative_controls/MissingSupport.lean7 lines
Original source path
formal/negative_controls/MissingSupport.lean1 import ProofPath.Examples
2 open ProofPath ProofPath.Examples
3 -- The pairwise matching assignment is not a model of the whole AND-rule.
4 example : conjunctionField.Model (fun v => v ≠ 2) := by
5 change (∀ v : Fin 3, False → v ≠ 2) ∧
6 (∀ _ : Unit, True → (∀ v : Fin 3, v ≠ 2 → v ≠ 2) → (2 : Fin 3) ≠ 2)
7 decide
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: fa57e3db02b1fe433343889a8858e8dcf404b0f9800f1f08ee2db9eebe6d1925