93@[simp] lemma phiVec_post_credit {d : Nat} (L : LedgerState d) (k : Fin d) (i : Fin d) : 94 phiVec (d := d) (post L k Side.credit) i =
proof body
Tactic-mode proof.
95 (if i = k then phiVec (d := d) L i - 1 else phiVec (d := d) L i) := by 96 by_cases hik : i = k 97 · subst hik 98 simp [post, phiVec, Recognition.phi] 99 ring_nf 100 · simp [post, phiVec, Recognition.phi, hik] 101 102/-! ## Bridge: a post induces a coord-atomic step on `phi` -/ 103
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.