toPrenexImp — Mathlib

English

Realize equivalence for toPrenexImpRight is preserved by simp lemmas.

Русский

Согласование реализации между toPrenexImpRight и имплицитной формой сохраняется под упрощениями.

LaTeX

$$$(φ.toPrenexImpRight ψ).Realize v xs \leftrightarrow (φ.imp ψ).Realize v xs$$$

Lean4

theorem toPrenexImp : ∀ {φ ψ : L.BoundedFormula α n}, φ.IsQF → φ.toPrenexImp ψ = φ.toPrenexImpRight ψ
  | _, _, IsQF.falsum => rfl
  | _, _, IsQF.of_isAtomic (IsAtomic.equal _ _) => rfl
  | _, _, IsQF.of_isAtomic (IsAtomic.rel _ _) => rfl
  | _, _, IsQF.imp IsQF.falsum _ => rfl
  | _, _, IsQF.imp (IsQF.of_isAtomic (IsAtomic.equal _ _)) _ => rfl
  | _, _, IsQF.imp (IsQF.of_isAtomic (IsAtomic.rel _ _)) _ => rfl
  | _, _, IsQF.imp (IsQF.imp _ _) _ => rfl

Похожие утверждения