  30    simp [intCost, h, h']
  31
  32/-- Interpret `LogicNat` as nonnegative integers. -/
  33def intOrbitInterpret (n : LogicNat) : ℤ :=
  34  (LogicNat.toNat n : ℤ)
  35
  36/-- Ordered integer realization with unit step. -/
  37def orderRealization : LogicRealization where
  38  Carrier := ℤ
  39  Cost := Nat
  40  zeroCost := inferInstance
  41  compare := intCost
  42  zero := 0
  43  step := fun z => z + 1
  44  Orbit := LogicNat
  45  orbitZero := LogicNat.zero
  46  orbitStep := LogicNat.succ
  47  interpret := intOrbitInterpret
  48  interpret_zero := by simp [intOrbitInterpret]
  49  interpret_step := by
  50    intro n
  51    show ((LogicNat.toNat (LogicNat.succ n) : ℤ) = (LogicNat.toNat n : ℤ) + 1)
  52    rw [LogicNat.toNat_succ]
  53    norm_num
  54  orbit_no_confusion := by
  55    intro n h
  56    exact LogicNat.zero_ne_succ n h
  57  orbit_step_injective := LogicNat.succ_injective
  58  orbit_induction := by
  59    intro P h0 hs n
  60    exact LogicNat.induction (motive := P) h0 hs n
  61  orbitEquivLogicNat := Equiv.refl LogicNat
  62  orbitEquiv_zero := rfl
  63  orbitEquiv_step := by intro n; rfl

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.