L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
h' : ∀ {m : ℕ} {φ : BoundedFormula L α m}, IsPrenex φ → P φ
⊢ P φ

case h'
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
⊢ ∀ {m : ℕ} {φ : BoundedFormula L α m}, IsPrenex φ → P φ
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
⊢ P φ
suffices h' : ∀ {m} {φ : L.BoundedFormula α m}, φ.IsPrenex → P φ
case h'
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
hφ : IsPrenex φ
⊢ P φ
case h'
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
⊢ ∀ {m : ℕ} {φ : BoundedFormula L α m}, IsPrenex φ → P φ
intro m φ hφ
case h'.of_isQF
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
⊢ P φ✝

case h'.all
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
hφ : P φ✝
⊢ P (∀'φ✝)

case h'.ex
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
hφ : P φ✝
⊢ P (∃'φ✝)
case h'
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
hφ : IsPrenex φ
⊢ P φ
induction' hφ with _ _ hφ _ _ _ hφ _ _ _ hφ
no goals
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
h' : ∀ {m : ℕ} {φ : BoundedFormula L α m}, IsPrenex φ → P φ
⊢ P φ
exact (hse φ.semanticallyEquivalent_toPrenex).2 (h' φ.toPrenex_isPrenex)
no goals
case h'.of_isQF
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
⊢ P φ✝
exact hqf hφ
no goals
case h'.all
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
hφ : P φ✝
⊢ P (∀'φ✝)
exact hall hφ
no goals
case h'.ex
L : Language
T : Theory L
α : Type w
n : ℕ
P : {m : ℕ} → BoundedFormula L α m → Prop
φ✝¹ : BoundedFormula L α n
hqf : ∀ {m : ℕ} {ψ : BoundedFormula L α m}, IsQF ψ → P ψ
hall : ∀ {m : ℕ} {ψ : BoundedFormula L α (m + 1)}, P ψ → P (∀'ψ)
hex : ∀ {m : ℕ} {φ : BoundedFormula L α (m + 1)}, P φ → P (∃'φ)
hse : ∀ {m : ℕ} {φ₁ φ₂ : BoundedFormula L α m}, Theory.SemanticallyEquivalent ∅ φ₁ φ₂ → (P φ₁ ↔ P φ₂)
m : ℕ
φ : BoundedFormula L α m
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
hφ : P φ✝
⊢ P (∃'φ✝)
exact hex hφ