Documentation

Foundation.Meta.TwoSided

source
@[reducible, inline]
abbrev LO.Entailment.TwoSided {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] (𝓱 : S) (Γ Δ : List F) :
Prop
Equations
Instances For
    source
    theorem LO.Entailment.TwoSided.weakening {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ₁ Γ₂ Δ₁ Δ₂ : List F} (h : TwoSided 𝓱 Γ₁ Δ₁) (HΓ : Γ₁ ⊆ Γ₂ := by simp) (HΔ : Δ₁ ⊆ Δ₂ := by simp) :
    TwoSided 𝓱 Γ₂ Δ₂
    source
    theorem LO.Entailment.TwoSided.remove_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓱 Γ Δ) :
    TwoSided 𝓱 (φ :: Γ) Δ
    source
    theorem LO.Entailment.TwoSided.remove_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓱 Γ Δ) :
    TwoSided 𝓱 Γ (φ :: Δ)
    source
    theorem LO.Entailment.TwoSided.rotate_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓱 Γ (Δ ++ [φ])) :
    TwoSided 𝓱 Γ (φ :: Δ)
    source
    theorem LO.Entailment.TwoSided.rotate_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓱 (Γ ++ [φ]) Δ) :
    TwoSided 𝓱 (φ :: Γ) Δ
    source
    theorem LO.Entailment.TwoSided.rotate_right_inv {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓱 Γ (φ :: Δ)) :
    TwoSided 𝓱 Γ (Δ ++ [φ])
    source
    theorem LO.Entailment.TwoSided.rotate_left_inv {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓱 (φ :: Γ) Δ) :
    TwoSided 𝓱 (Γ ++ [φ]) Δ
    source
    theorem LO.Entailment.TwoSided.to_provable {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {φ : F} (h : TwoSided 𝓱 [] [φ]) :
    𝓱 ⊱ φ
    source
    theorem LO.Entailment.TwoSided.add_hyp {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} {𝒯 : S} [𝒯 âȘŻ 𝓱] (hφ : 𝒯 ⊱ φ) (h : TwoSided 𝓱 (φ :: Γ) Δ) :
    TwoSided 𝓱 Γ Δ
    source
    theorem LO.Entailment.TwoSided.right_closed {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} (h : φ ∈ Γ) :
    TwoSided 𝓱 Γ (φ :: Δ)
    source
    theorem LO.Entailment.TwoSided.left_closed {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} (h : φ ∈ Δ) :
    TwoSided 𝓱 (φ :: Γ) Δ
    source
    theorem LO.Entailment.TwoSided.verum_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} :
    TwoSided 𝓱 Γ (⊀ :: Δ)
    source
    theorem LO.Entailment.TwoSided.falsum_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} :
    TwoSided 𝓱 (⊄ :: Γ) Δ
    source
    theorem LO.Entailment.TwoSided.falsum_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} (h : TwoSided 𝓱 Γ Δ) :
    TwoSided 𝓱 Γ (⊄ :: Δ)
    source
    theorem LO.Entailment.TwoSided.verum_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} (h : TwoSided 𝓱 Γ Δ) :
    TwoSided 𝓱 (⊀ :: Γ) Δ
    source
    theorem LO.Entailment.TwoSided.and_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ ψ : F} (hφ : TwoSided 𝓱 Γ (Δ ++ [φ])) (hψ : TwoSided 𝓱 Γ (Δ ++ [ψ])) :
    TwoSided 𝓱 Γ (φ ⋏ ψ :: Δ)
    source
    theorem LO.Entailment.TwoSided.or_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ ψ : F} (hφ : TwoSided 𝓱 (Γ ++ [φ]) Δ) (hψ : TwoSided 𝓱 (Γ ++ [ψ]) Δ) :
    TwoSided 𝓱 (φ ⋎ ψ :: Γ) Δ
    source
    theorem LO.Entailment.TwoSided.or_right {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ ψ : F} (h : TwoSided 𝓱 Γ (Δ ++ [φ, ψ])) :
    TwoSided 𝓱 Γ (φ ⋎ ψ :: Δ)
    source
    theorem LO.Entailment.TwoSided.and_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ ψ : F} (h : TwoSided 𝓱 (Γ ++ [φ, ψ]) Δ) :
    TwoSided 𝓱 (φ ⋏ ψ :: Γ) Δ
    source
    theorem LO.Entailment.TwoSided.neg_right_int {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} (h : TwoSided 𝓱 (Γ ++ [φ]) []) :
    TwoSided 𝓱 Γ (∌φ :: Δ)
    source
    theorem LO.Entailment.TwoSided.neg_right_cl {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} {Γ Δ : List F} {φ : F} [Entailment.Cl 𝓱] (h : TwoSided 𝓱 (Γ ++ [φ]) Δ) :
    TwoSided 𝓱 Γ (∌φ :: Δ)
    source
    theorem LO.Entailment.TwoSided.neg_left_int {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} (h : TwoSided 𝓱 (Γ ++ [∌φ]) (Δ ++ [φ])) :
    TwoSided 𝓱 (∌φ :: Γ) Δ
    source
    theorem LO.Entailment.TwoSided.neg_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ : F} (h : TwoSided 𝓱 Γ (Δ ++ [φ])) :
    TwoSided 𝓱 (∌φ :: Γ) Δ
    source
    theorem LO.Entailment.TwoSided.imply_left_int {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ ψ : F} (hφ : TwoSided 𝓱 (Γ ++ [φ ➝ ψ]) (Δ ++ [φ])) (hψ : TwoSided 𝓱 (Γ ++ [ψ]) Δ) :
    TwoSided 𝓱 ((φ ➝ ψ) :: Γ) Δ
    source
    theorem LO.Entailment.TwoSided.imply_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ ψ : F} (hφ : TwoSided 𝓱 Γ (Δ ++ [φ])) (hψ : TwoSided 𝓱 (Γ ++ [ψ]) Δ) :
    TwoSided 𝓱 ((φ ➝ ψ) :: Γ) Δ
    source
    theorem LO.Entailment.TwoSided.imply_right_int {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ ψ : F} (h : TwoSided 𝓱 (Γ ++ [φ]) [ψ]) :
    TwoSided 𝓱 Γ ((φ ➝ ψ) :: Δ)
    source
    theorem LO.Entailment.TwoSided.imply_right_cl {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} {Γ Δ : List F} {φ ψ : F} [Entailment.Cl 𝓱] (h : TwoSided 𝓱 (Γ ++ [φ]) (Δ ++ [ψ])) :
    TwoSided 𝓱 Γ ((φ ➝ ψ) :: Δ)
    source
    theorem LO.Entailment.TwoSided.iff_right_cl {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} {Γ Δ : List F} {φ ψ : F} [Entailment.Cl 𝓱] (hr : TwoSided 𝓱 (Γ ++ [φ]) (Δ ++ [ψ])) (hl : TwoSided 𝓱 (Γ ++ [ψ]) (Δ ++ [φ])) :
    TwoSided 𝓱 Γ ((φ â­€ ψ) :: Δ)
    source
    theorem LO.Entailment.TwoSided.iff_left {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓱 : S} [Entailment.Int 𝓱] {Γ Δ : List F} {φ ψ : F} (hr : TwoSided 𝓱 Γ (Δ ++ [φ, ψ])) (hl : TwoSided 𝓱 (Γ ++ [φ, ψ]) Δ) :
    TwoSided 𝓱 ((φ â­€ ψ) :: Γ) Δ
    source
    structure LO.Entailment.Tableaux.Sequent (F : Type u_1) :
    Type u_1
    Instances For
      source
      @[reducible, inline]
      abbrev LO.Entailment.Tableaux (F : Type u_1) :
      Type u_1
      Equations
      Instances For
        source
        inductive LO.Entailment.Tableaux.Valid {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] (𝓱 : S) :
        Tableaux F → Prop
        Instances For
          source
          @[simp]
          theorem LO.Entailment.Tableaux.Valid.not_nil {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} :
          ¬Valid 𝓱 []
          source
          theorem LO.Entailment.Tableaux.Valid.of_mem {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {Γ Δ : List F} {τ : Tableaux F} (H : TwoSided 𝓱 Γ Δ) (h : { antecedent := Γ, succedent := Δ } ∈ τ) :
          Valid 𝓱 τ
          source
          theorem LO.Entailment.Tableaux.Valid.of_subset {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {σ τ : Tableaux F} (h : Valid 𝓱 σ) (ss : σ ⊆ τ := by simp) :
          Valid 𝓱 τ
          source
          theorem LO.Entailment.Tableaux.Valid.of_single_uppercedent {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ Ξ Λ : List F} (H : TwoSided 𝓱 Γ Δ → TwoSided 𝓱 Ξ Λ) (h : Valid 𝓱 ({ antecedent := Γ, succedent := Δ } :: T)) :
          Valid 𝓱 ({ antecedent := Ξ, succedent := Λ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.of_double_uppercedent {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ₁ Γ₂ Δ₁ Δ₂ Ξ Λ : List F} (H : TwoSided 𝓱 Γ₁ Δ₁ → TwoSided 𝓱 Γ₂ Δ₂ → TwoSided 𝓱 Ξ Λ) (h₁ : Valid 𝓱 ({ antecedent := Γ₁, succedent := Δ₁ } :: T)) (h₂ : Valid 𝓱 ({ antecedent := Γ₂, succedent := Δ₂ } :: T)) :
          Valid 𝓱 ({ antecedent := Ξ, succedent := Λ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.remove {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} :
          Valid 𝓱 T → Valid 𝓱 ({ antecedent := Γ, succedent := Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.to_provable {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {φ : F} [DecidableEq F] [Entailment.Int 𝓱] (h : Valid 𝓱 [{ antecedent := [], succedent := [φ] }]) :
          𝓱 ⊱ φ
          source
          theorem LO.Entailment.Tableaux.Valid.right_closed {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [DecidableEq F] [Entailment.Int 𝓱] (h : φ ∈ Γ) :
          Valid 𝓱 ({ antecedent := Γ, succedent := φ :: Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.left_closed {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [DecidableEq F] [Entailment.Int 𝓱] (h : φ ∈ Δ) :
          Valid 𝓱 ({ antecedent := φ :: Γ, succedent := Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.remove_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ, succedent := Δ } :: T) → Valid 𝓱 ({ antecedent := Γ, succedent := φ :: Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.remove_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ, succedent := Δ } :: T) → Valid 𝓱 ({ antecedent := φ :: Γ, succedent := Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.rotate_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ, succedent := Δ ++ [φ] } :: T) → Valid 𝓱 ({ antecedent := Γ, succedent := φ :: Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.rotate_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ ++ [φ], succedent := Δ } :: T) → Valid 𝓱 ({ antecedent := φ :: Γ, succedent := Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.verum_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ, succedent := ⊀ :: Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.falsum_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := ⊄ :: Γ, succedent := Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.falsum_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ, succedent := Δ } :: T) → Valid 𝓱 ({ antecedent := Γ, succedent := ⊄ :: Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.verum_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ, succedent := Δ } :: T) → Valid 𝓱 ({ antecedent := ⊀ :: Γ, succedent := Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.and_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ, succedent := Δ ++ [φ] } :: T) → Valid 𝓱 ({ antecedent := Γ, succedent := Δ ++ [ψ] } :: T) → Valid 𝓱 ({ antecedent := Γ, succedent := φ ⋏ ψ :: Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.or_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ ++ [φ], succedent := Δ } :: T) → Valid 𝓱 ({ antecedent := Γ ++ [ψ], succedent := Δ } :: T) → Valid 𝓱 ({ antecedent := φ ⋎ ψ :: Γ, succedent := Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.or_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ, succedent := Δ ++ [φ, ψ] } :: T) → Valid 𝓱 ({ antecedent := Γ, succedent := φ ⋎ ψ :: Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.and_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ ++ [φ, ψ], succedent := Δ } :: T) → Valid 𝓱 ({ antecedent := φ ⋏ ψ :: Γ, succedent := Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.neg_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ ++ [φ], succedent := [] } :: { antecedent := Γ, succedent := Δ ++ [∌φ] } :: T) → Valid 𝓱 ({ antecedent := Γ, succedent := ∌φ :: Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.neg_right' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ ++ [φ], succedent := [] } :: { antecedent := Γ, succedent := Δ } :: T) → Valid 𝓱 ({ antecedent := Γ, succedent := ∌φ :: Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.neg_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ ++ [∌φ], succedent := Δ ++ [φ] } :: T) → Valid 𝓱 ({ antecedent := ∌φ :: Γ, succedent := Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.imply_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ ++ [φ], succedent := [ψ] } :: { antecedent := Γ, succedent := Δ ++ [φ ➝ ψ] } :: T) → Valid 𝓱 ({ antecedent := Γ, succedent := (φ ➝ ψ) :: Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.imply_right' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ ++ [φ], succedent := [ψ] } :: { antecedent := Γ, succedent := Δ } :: T) → Valid 𝓱 ({ antecedent := Γ, succedent := (φ ➝ ψ) :: Δ } :: T)
          source
          theorem LO.Entailment.Tableaux.Valid.imply_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓱 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [DecidableEq F] [Entailment.Int 𝓱] :
          Valid 𝓱 ({ antecedent := Γ ++ [φ ➝ ψ], succedent := Δ ++ [φ] } :: T) → Valid 𝓱 ({ antecedent := Γ ++ [ψ], succedent := Δ } :: T) → Valid 𝓱 ({ antecedent := (φ ➝ ψ) :: Γ, succedent := Δ } :: T)