Cairn Docs Claims Blog Packages

Claim ยท pairs 0.1.3

pairs^32 Win a game

A flow of pairs 0.1.3, in Pairs window.

Id
pairs^32
Kind
flow
Reads as
proved
Place
Pairs window ^1
Version
0.1.3

All of pairs 0.1.3's claims

What you do

Turn the cards of each face in turn, a pair at a time.

What you see

Every card is matched and the game is won, in eight moves.

Steps

The witness its liveness proof follows, from the app's first state.

  1. press on ^2#8 Turn a card
  2. press on ^2#11 Turn a card
  3. press on ^2#1 Turn a card
  4. press on ^2#14 Turn a card
  5. press on ^2#7 Turn a card
  6. press on ^2#12 Turn a card
  7. press on ^2#5 Turn a card
  8. press on ^2#10 Turn a card
  9. press on ^2#3 Turn a card
  10. press on ^2#6 Turn a card
  11. press on ^2#4 Turn a card
  12. press on ^2#15 Turn a card
  13. press on ^2#2 Turn a card
  14. press on ^2#9 Turn a card
  15. press on ^2 Turn a card
  16. press on ^2#13 Turn a card

Evidence

provedlivePairs.winGame.live
provedreachesPairs.winGame.reaches
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).
seenNot shown yet: a screenshot of the app shows it. A CI step will publish it (#95).

Where it's defined

Declaration
Pairs.winGame
Module
Pairs.Claims
Source
lean/Pairs/Claims.lean:481 at v0.1.3
Machine
Pairs.machine
Statement
Pairs.winGame.goal Pairs.winGame.witness
Statement hash
5b05f6a60dad4698

Ledger

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