LeanPool.FormalizationOfBoundedArithmetic.IOPEN

class IOPENModel (num : Type u_1) extends BASICModel num : Type (max u_1 u_2)

Models of BASIC arithmetic satisfying open induction.

• funMap {n : ℕ} : peano.Functions n → (Fin n → num) → num
• RelMap {n : ℕ} : peano.Relations n → (Fin n → num) → Prop
• B1 {x : num} : x + 1 ≠ 0
• B2 (x y : num) : x + 1 = y + 1 → x = y
• B3 (x : num) : x + 0 = x
• B4 {x y : num} : x + (y + 1) = x + y + 1
• B5 {x : num} : x * 0 = 0
• B6 {x y : num} : x * (y + 1) = x * y + x
• B7 {x y : num} : x ≤ y → y ≤ x → x = y
• B8 {x y : num} : x ≤ x + y
• open_induction {n : FvName} {a : Type} [IsEnum a] (phi : FirstOrder.Language.peano.BoundedFormula (Vars1 n ⊕ a) 0) : phi.IsOpen → num ⊨ mkInductionSentence phi

def IOPENModel.tacticSimpOpenInductionAt_ : Lean.ParserDescr

Reduce an open-induction hypothesis: clear its complexity side condition then unfold the induction sentence into base/step goals.

Equations

• One or more equations did not get rendered due to their size.

theorem IOPENModel.forall_swap_231 {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {p : α → β → γ → Prop} : (∀ (x : α) (y : β) (z : γ), p x y z) ↔ ∀ (z : γ) (x : α) (y : β), p x y z

theorem IOPENModel.add_assoc {M : Type u} [iopen : IOPENModel M] (x y z : M) : x + y + z = x + (y + z)

theorem IOPENModel.add_zero_comm {M : Type u} [iopen : IOPENModel M] (x : M) : x + 0 = 0 + x

theorem IOPENModel.zero_add {M : Type u} [iopen : IOPENModel M] (x : M) : 0 + x = x

theorem IOPENModel.add_one_comm {M : Type u} [iopen : IOPENModel M] (x : M) : x + 1 = 1 + x

theorem IOPENModel.add_comm {M : Type u} [iopen : IOPENModel M] (x y : M) : x + y = y + x

theorem IOPENModel.mul_add {M : Type u} [iopen : IOPENModel M] (x y z : M) : x * (y + z) = x * y + x * z

theorem IOPENModel.mul_one {M : Type u} [iopen : IOPENModel M] (x : M) : x * 1 = x

theorem IOPENModel.mul_assoc {M : Type u} [iopen : IOPENModel M] (x y z : M) : x * y * z = x * (y * z)

theorem IOPENModel.zero_mul {M : Type u} [iopen : IOPENModel M] (x : M) : 0 * x = 0

theorem IOPENModel.one_mul {M : Type u} [iopen : IOPENModel M] (x : M) : 1 * x = x

theorem IOPENModel.mul_add_1_left {M : Type u} [iopen : IOPENModel M] (x y : M) : (x + 1) * y = x * y + y

theorem IOPENModel.mul_comm {M : Type u} [iopen : IOPENModel M] (x y : M) : x * y = y * x

theorem IOPENModel.add_cancel_right.mp {M : Type u} [iopen : IOPENModel M] {x y z : M} : x + z = y + z → x = y

theorem IOPENModel.add_cancel_right {M : Type u} [iopen : IOPENModel M] {x y z : M} : x + z = y + z ↔ x = y

theorem IOPENModel.add_cancel_left {M : Type u} [iopen : IOPENModel M] {x y z : M} : z + x = z + y ↔ x = y

theorem IOPENModel.zero_le {M : Type u} [iopen : IOPENModel M] (x : M) : 0 ≤ x

theorem IOPENModel.le_zero_eq {M : Type u} [iopen : IOPENModel M] (x : M) : x ≤ 0 → x = 0

theorem IOPENModel.ne_succ {M : Type u} [iopen : IOPENModel M] (x : M) : x ≠ x + 1

theorem IOPENModel.add_mul {M : Type u} [iopen : IOPENModel M] (x y z : M) : (x + y) * z = x * z + y * z