pith. machine review for the scientific record. sign in
theorem proved term proof

legalAtomicTick_oneBitDiff

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 994theorem legalAtomicTick_oneBitDiff {d : Nat} {L L' : LedgerState d}
 995    (h : LegalAtomicTick (d := d) L L') :

proof body

Term-mode proof.

 996    OneBitDiff (parity d L) (parity d L') :=
 997  postingStep_oneBitDiff (legalAtomicTick_implies_PostingStep (d := d) h)
 998
 999/-! ## Workstream B tightening: RS AtomicTick ⇒ PostingStep (legality predicate) -/
1000
1001/-- Choose the unique posted account at tick `t` from an RS `AtomicTick` instance. -/

depends on (19)

Lean names referenced from this declaration's body.