Cairn Docs Claims Blog Packages

Claim ยท pairs 0.1.3

pairs^25 A matched card stays matched

An invariant of pairs 0.1.3.

Id
pairs^25
Kind
invariant
Reads as
proved
Version
0.1.3

All of pairs 0.1.3's claims

What it says

Once a pair is matched it stays matched, face up, until a new game is dealt; nothing the person clicks and nothing the host answers turns it back.

Evidence

provedinitPairs.matchedStays.init
provedstepPairs.matchedStays.step
provedreceivePairs.matchedStays.receive
provedreachablePairs.matchedStays.reachable
provedreachableAllPairs.matchedStays.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.matchedStays
Module
Pairs.Claims
Source
lean/Pairs/Claims.lean:405 at v0.1.3
Machine
Pairs.machine
Statement
Pairs.matchedStays.holds
Statement hash
e8cae50e9aee7bdf

Ledger

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