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

stepAt_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)

1020theorem stepAt_oneBitDiff {d : Nat} [AtomicTick (AccountRS d)] (sideAt : Nat → Side) (t : Nat) (L : LedgerState d) :
1021    OneBitDiff (parity d L) (parity d (stepAt (d := d) sideAt t L)) :=

proof body

Term-mode proof.

1022  postingStep_oneBitDiff (stepAt_isPostingStep (d := d) sideAt t L)
1023
1024/-! ## A per-tick posting schedule induces an adjacent walk in parity space -/
1025
1026/-- A per-tick posting instruction: (account index, side). -/

depends on (22)

Lean names referenced from this declaration's body.