Theorem: LO.FirstOrder.Arith.Model.hierarchy_polynomial_induction
Proof state before:
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ P x
Tactic:
induction x using order_induction_h
Proof state after:
case Γ
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
⊢ Polarity

case m
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
⊢ ℕ

case hP
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ DefinablePred ?m.1056264 (?Γ.coe, ?m) fun x => P x

case ind
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x✝ : M
a✝ : ∀ y < x✝, P y
⊢ P x✝

case inst
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ ?m.1056264.ORing

case inst
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ Structure ?m.1056264 M

case inst
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ Structure.ORing ?m.1056264 M

case inst
M : Type u_1
inst✝¹¹ : Zero M
inst✝¹⁰ : One M
inst✝⁹ : Add M
inst✝⁸ : Mul M
inst✝⁷ : LT M
inst✝⁶ : M ⊧ₘ* 𝐏𝐀⁻
inst✝⁵ : M ⊧ₘ* 𝐈open
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
zero : P 0
even : ∀ x > 0, P x → P (2 * x)
odd : ∀ (x : M), P x → P (2 * x + 1)
x : M
⊢ M ⊧ₘ* Theory.indScheme ?m.1056264 (Hierarchy ?Γ ?m)