case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.127743
P : Type ?u.127746
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.127774
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hψ : IsQF φ✝
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (toPrenexImpRight φ φ✝)

case all
L : Language
L' : Language
M : Type w
N : Type ?u.127743
P : Type ?u.127746
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.127774
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih1 : ∀ {φ : BoundedFormula L α (n✝ + 1)}, IsQF φ → IsPrenex (toPrenexImpRight φ φ✝)
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (toPrenexImpRight φ (all φ✝))

case ex
L : Language
L' : Language
M : Type w
N : Type ?u.127743
P : Type ?u.127746
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.127774
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih2 : ∀ {φ : BoundedFormula L α (n✝ + 1)}, IsQF φ → IsPrenex (toPrenexImpRight φ φ✝)
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (toPrenexImpRight φ (BoundedFormula.ex φ✝))
L : Language
L' : Language
M : Type w
N : Type ?u.127743
P : Type ?u.127746
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.127774
n l : ℕ
φ✝ ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ : BoundedFormula L α n
hφ : IsQF φ
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImpRight φ ψ)
induction' hψ with _ _ hψ _ _ _ ih1 _ _ _ ih2
case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.127743
P : Type ?u.127746
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.127774
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hψ : IsQF φ✝
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (imp φ φ✝)
case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.127743
P : Type ?u.127746
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.127774
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hψ : IsQF φ✝
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (toPrenexImpRight φ φ✝)
rw [hψ.toPrenexImpRight]
no goals
case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.127743
P : Type ?u.127746
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.127774
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hψ : IsQF φ✝
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (imp φ φ✝)
exact (hφ.imp hψ).isPrenex
no goals
case all
L : Language
L' : Language
M : Type w
N : Type ?u.127743
P : Type ?u.127746
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.127774
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih1 : ∀ {φ : BoundedFormula L α (n✝ + 1)}, IsQF φ → IsPrenex (toPrenexImpRight φ φ✝)
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (toPrenexImpRight φ (all φ✝))
exact (ih1 hφ.liftAt).all
no goals
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.127743
P : Type ?u.127746
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.127774
n l : ℕ
φ✝² ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ✝¹ ψ : BoundedFormula L α n
hφ✝ : IsQF φ✝¹
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih2 : ∀ {φ : BoundedFormula L α (n✝ + 1)}, IsQF φ → IsPrenex (toPrenexImpRight φ φ✝)
φ : BoundedFormula L α n✝
hφ : IsQF φ
⊢ IsPrenex (toPrenexImpRight φ (BoundedFormula.ex φ✝))
exact (ih2 hφ.liftAt).ex