Cairn Docs Claims Blog Packages

Claim ยท pairs 0.1.3

pairs^30 Find a pair

A flow of pairs 0.1.3, in Pairs window.

Id
pairs^30
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 two cards with the same face.

What you see

Both stay face up, matched; the move counter says 1.

Steps

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

  1. press on ^2 Turn a card
  2. press on ^2#13 Turn a card

Evidence

provedlivePairs.findPair.live
provedreachesPairs.findPair.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.findPair
Module
Pairs.Claims
Source
lean/Pairs/Claims.lean:468 at v0.1.3
Machine
Pairs.machine
Statement
Pairs.findPair.goal Pairs.findPair.witness
Statement hash
e5ca39049ca3621c

Ledger

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