L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize (φ ⇔ ψ) v xs
⊢ BoundedFormula.Realize (φ ⇔ θ) v xs
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (φ ⇔ θ) v xs
have h1' := h1 M v xs
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize (φ ⇔ ψ) v xs
h2' : BoundedFormula.Realize (ψ ⇔ θ) v xs
⊢ BoundedFormula.Realize (φ ⇔ θ) v xs
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize (φ ⇔ ψ) v xs
⊢ BoundedFormula.Realize (φ ⇔ θ) v xs
have h2' := h2 M v xs
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize φ v xs ↔ BoundedFormula.Realize ψ v xs
h2' : BoundedFormula.Realize ψ v xs ↔ BoundedFormula.Realize θ v xs
⊢ BoundedFormula.Realize φ v xs ↔ BoundedFormula.Realize θ v xs
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize (φ ⇔ ψ) v xs
h2' : BoundedFormula.Realize (ψ ⇔ θ) v xs
⊢ BoundedFormula.Realize (φ ⇔ θ) v xs
rw [BoundedFormula.realize_iff] at *
no goals
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ θ : BoundedFormula L α n
h1 : SemanticallyEquivalent T φ ψ
h2 : SemanticallyEquivalent T ψ θ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
h1' : BoundedFormula.Realize φ v xs ↔ BoundedFormula.Realize ψ v xs
h2' : BoundedFormula.Realize ψ v xs ↔ BoundedFormula.Realize θ v xs
⊢ BoundedFormula.Realize φ v xs ↔ BoundedFormula.Realize θ v xs
exact ⟨h2'.1 ∘ h1'.1, h1'.2 ∘ h2'.2⟩