Cairn Docs Claims Blog Packages

Claim ยท pairs 0.1.3

pairs^31 A mismatch

A flow of pairs 0.1.3, in Pairs window.

Id
pairs^31
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 different faces.

What you see

Both are face up, unmatched, until they turn back; 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#1 Turn a card

Evidence

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

Ledger

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