Cairn Docs Claims Blog Packages

Claim ยท pairs 0.1.3

pairs^23 The game can always be won

An invariant of pairs 0.1.3.

Id
pairs^23
Kind
invariant
Reads as
proved
Version
0.1.3

All of pairs 0.1.3's claims

What it says

From every state the app reaches, some sequence of cards to turn wins the game: the cards of every face not yet matched, a pair at a time (Game.solve).

Evidence

provedinitPairs.canWin.init
provedstepPairs.canWin.step
provedreceivePairs.canWin.receive
provedreachablePairs.canWin.reachable
provedreachableAllPairs.canWin.reachableAll
fuzzedNot shown yet: the claim-driven fuzzer held it in every random sequence (docs/fuzz.md). A CI step will publish it (#95).
testedNot shown yet: the running app matched the model at every step that exercised it (docs/conformance.md). A CI step will publish it (#95).

Where it's defined

Declaration
Pairs.canWin
Module
Pairs.Claims
Source
lean/Pairs/Claims.lean:360 at v0.1.3
Machine
Pairs.machine
Statement
Pairs.canWin.holds
Statement hash
457e3c8a6a950d13

Ledger

pairs^23 is active in this version's claims.lock, statement 457e3c8a6a950d13. An id never moves or changes meaning.