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

reverseTick_involutive

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)

 143theorem reverseTick_involutive (p : Phase) : reverseTick (reverseTick p) = p := by

proof body

Tactic-mode proof.

 144  simp only [reverseTick]
 145  ext
 146  -- p.val < 8, so (7 - p.val) < 8, so (7 - p.val) % 8 = 7 - p.val
 147  -- Then (7 - (7 - p.val)) = p.val
 148  have hp := p.isLt
 149  have h1 : 7 - p.val < 8 := by omega
 150  have h2 : (7 - p.val) % 8 = 7 - p.val := Nat.mod_eq_of_lt h1
 151  simp only [h2]
 152  have h3 : 7 - (7 - p.val) = p.val := by omega
 153  simp only [h3, Nat.mod_eq_of_lt hp]
 154
 155/-- **THEOREM (CPT is Involution)**: Applying CPT twice returns the original. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.