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

modularInterpret_step

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)

  56theorem modularInterpret_step (k : ℕ) (n : ArithmeticFromLogic.LogicNat) :
  57    modularInterpret k (ArithmeticFromLogic.LogicNat.succ n)
  58      = cycStep k (modularInterpret k n) := by

proof body

Term-mode proof.

  59  apply Fin.ext
  60  change ArithmeticFromLogic.LogicNat.toNat (ArithmeticFromLogic.LogicNat.succ n) % modulus k =
  61    (ArithmeticFromLogic.LogicNat.toNat n % modulus k + 1) % modulus k
  62  rw [ArithmeticFromLogic.LogicNat.toNat_succ, Nat.succ_eq_add_one]
  63  have h := (Nat.add_mod (ArithmeticFromLogic.LogicNat.toNat n) 1 (modulus k)).symm
  64  simpa [Nat.mod_eq_of_lt (one_lt_modulus k)] using h
  65
  66/-- Finite cyclic Law-of-Logic realization with periodic interpretation. -/

used by (1)

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

depends on (14)

Lean names referenced from this declaration's body.