Supporting results for pointwise provable equality.

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.TwoSided {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) (Γ Δ : List F) : Prop

The Two Sided construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.TwoSided 𝓢 Γ Δ = Γ ⊢[𝓢] PointwiseComposition.List.disj Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.weakening {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ₁ Γ₂ Δ₁ Δ₂ : List F} (h : TwoSided 𝓢 Γ₁ Δ₁) (HΓ : Γ₁ ⊆ Γ₂ := by classical simp) (HΔ : Δ₁ ⊆ Δ₂ := by simp) : TwoSided 𝓢 Γ₂ Δ₂

theorem PointwiseComposition.FFL.Entailment.TwoSided.remove_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓢 Γ Δ) : TwoSided 𝓢 (φ :: Γ) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.remove_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓢 Γ Δ) : TwoSided 𝓢 Γ (φ :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.rotate_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓢 Γ (Δ ++ [φ])) : TwoSided 𝓢 Γ (φ :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.rotate_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓢 (Γ ++ [φ]) Δ) : TwoSided 𝓢 (φ :: Γ) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.rotate_right_inv {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓢 Γ (φ :: Δ)) : TwoSided 𝓢 Γ (Δ ++ [φ])

theorem PointwiseComposition.FFL.Entailment.TwoSided.rotate_left_inv {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} (hφ : TwoSided 𝓢 (φ :: Γ) Δ) : TwoSided 𝓢 (Γ ++ [φ]) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.to_provable {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {φ : F} (h : TwoSided 𝓢 [] [φ]) : 𝓢 ⊢ φ

theorem PointwiseComposition.FFL.Entailment.TwoSided.add_hyp {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} {𝒯 : S} [𝒯 ≼ 𝓢] (hφ : 𝒯 ⊢ φ) (h : TwoSided 𝓢 (φ :: Γ) Δ) : TwoSided 𝓢 Γ Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.right_closed {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} (h : φ ∈ Γ) : TwoSided 𝓢 Γ (φ :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.left_closed {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} (h : φ ∈ Δ) : TwoSided 𝓢 (φ :: Γ) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.verum_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} : TwoSided 𝓢 Γ (⊤ :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.falsum_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} : TwoSided 𝓢 (⊥ :: Γ) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.falsum_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} (h : TwoSided 𝓢 Γ Δ) : TwoSided 𝓢 Γ (⊥ :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.verum_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} (h : TwoSided 𝓢 Γ Δ) : TwoSided 𝓢 (⊤ :: Γ) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.and_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ ψ : F} (hφ : TwoSided 𝓢 Γ (Δ ++ [φ])) (hψ : TwoSided 𝓢 Γ (Δ ++ [ψ])) : TwoSided 𝓢 Γ (φ ⋏ ψ :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.or_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ ψ : F} (hφ : TwoSided 𝓢 (Γ ++ [φ]) Δ) (hψ : TwoSided 𝓢 (Γ ++ [ψ]) Δ) : TwoSided 𝓢 (φ ⋎ ψ :: Γ) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.or_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ ψ : F} (h : TwoSided 𝓢 Γ (Δ ++ [φ, ψ])) : TwoSided 𝓢 Γ (φ ⋎ ψ :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.and_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ ψ : F} (h : TwoSided 𝓢 (Γ ++ [φ, ψ]) Δ) : TwoSided 𝓢 (φ ⋏ ψ :: Γ) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.neg_right_int {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} (h : TwoSided 𝓢 (Γ ++ [φ]) []) : TwoSided 𝓢 Γ (∼φ :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.neg_right_cl {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ Δ : List F} {φ : F} [Entailment.Cl 𝓢] (h : TwoSided 𝓢 (Γ ++ [φ]) Δ) : TwoSided 𝓢 Γ (∼φ :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.neg_left_int {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} (h : TwoSided 𝓢 (Γ ++ [∼φ]) (Δ ++ [φ])) : TwoSided 𝓢 (∼φ :: Γ) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.neg_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ : F} (h : TwoSided 𝓢 Γ (Δ ++ [φ])) : TwoSided 𝓢 (∼φ :: Γ) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.imply_left_int {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ ψ : F} (hφ : TwoSided 𝓢 (Γ ++ [φ ⇒ₗ ψ]) (Δ ++ [φ])) (hψ : TwoSided 𝓢 (Γ ++ [ψ]) Δ) : TwoSided 𝓢 ((φ ⇒ₗ ψ) :: Γ) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.imply_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ ψ : F} (hφ : TwoSided 𝓢 Γ (Δ ++ [φ])) (hψ : TwoSided 𝓢 (Γ ++ [ψ]) Δ) : TwoSided 𝓢 ((φ ⇒ₗ ψ) :: Γ) Δ

theorem PointwiseComposition.FFL.Entailment.TwoSided.imply_right_int {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ ψ : F} (h : TwoSided 𝓢 (Γ ++ [φ]) [ψ]) : TwoSided 𝓢 Γ ((φ ⇒ₗ ψ) :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.imply_right_cl {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ Δ : List F} {φ ψ : F} [Entailment.Cl 𝓢] (h : TwoSided 𝓢 (Γ ++ [φ]) (Δ ++ [ψ])) : TwoSided 𝓢 Γ ((φ ⇒ₗ ψ) :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.iff_right_cl {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ Δ : List F} {φ ψ : F} [Entailment.Cl 𝓢] (hr : TwoSided 𝓢 (Γ ++ [φ]) (Δ ++ [ψ])) (hl : TwoSided 𝓢 (Γ ++ [ψ]) (Δ ++ [φ])) : TwoSided 𝓢 Γ ((φ ⇔ₗ ψ) :: Δ)

theorem PointwiseComposition.FFL.Entailment.TwoSided.iff_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} {φ ψ : F} (hr : TwoSided 𝓢 Γ (Δ ++ [φ, ψ])) (hl : TwoSided 𝓢 (Γ ++ [φ, ψ]) Δ) : TwoSided 𝓢 ((φ ⇔ₗ ψ) :: Γ) Δ

structure PointwiseComposition.FFL.Entailment.Tableaux.Sequent (F : Type u_1) : Type u_1

Data and laws for Sequent in FFL.Entailment.Tableaux.

• antecedent : List F

  The antecedent construction in FFL.Entailment.Tableaux.Sequent.

• succedent : List F

  The succedent construction in FFL.Entailment.Tableaux.Sequent.

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.Tableaux (F : Type u_1) : Type u_1

The Tableaux construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.Tableaux F = List (PointwiseComposition.FFL.Entailment.Tableaux.Sequent F)

inductive PointwiseComposition.FFL.Entailment.Tableaux.Valid {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) : Tableaux F → Prop

Data and laws for Valid in FFL.Entailment.Tableaux.

• head {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ Δ : List F} {τ : List (Sequent F)} : TwoSided 𝓢 Γ Δ → Valid 𝓢 ({ antecedent := Γ, succedent := Δ } :: τ)
• tail {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {S✝ : Sequent F} {τ : Tableaux F} : Valid 𝓢 τ → Valid 𝓢 (S✝ :: τ)

@[simp]

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.not_nil {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} : ¬Valid 𝓢 []

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.of_mem {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ Δ : List F} {τ : Tableaux F} (H : TwoSided 𝓢 Γ Δ) (h : { antecedent := Γ, succedent := Δ } ∈ τ) : Valid 𝓢 τ

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.of_subset {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {σ τ : Tableaux F} (h : Valid 𝓢 σ) (ss : σ ⊆ τ := by simp) : Valid 𝓢 τ

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.of_single_uppercedent {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.of_double_uppercedent {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.remove {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} : Valid 𝓢 T → Valid 𝓢 ({ antecedent := Γ, succedent := Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.to_provable {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] (h : Valid 𝓢 [{ antecedent := [], succedent := [φ] }]) : 𝓢 ⊢ φ

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.right_closed {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [Entailment.Int 𝓢] (h : φ ∈ Γ) : Valid 𝓢 ({ antecedent := Γ, succedent := φ :: Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.left_closed {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [Entailment.Int 𝓢] (h : φ ∈ Δ) : Valid 𝓢 ({ antecedent := φ :: Γ, succedent := Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.remove_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ, succedent := Δ } :: T) → Valid 𝓢 ({ antecedent := Γ, succedent := φ :: Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.remove_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ, succedent := Δ } :: T) → Valid 𝓢 ({ antecedent := φ :: Γ, succedent := Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.rotate_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ, succedent := Δ ++ [φ] } :: T) → Valid 𝓢 ({ antecedent := Γ, succedent := φ :: Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.rotate_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ ++ [φ], succedent := Δ } :: T) → Valid 𝓢 ({ antecedent := φ :: Γ, succedent := Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.verum_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ, succedent := ⊤ :: Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.falsum_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := ⊥ :: Γ, succedent := Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.falsum_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ, succedent := Δ } :: T) → Valid 𝓢 ({ antecedent := Γ, succedent := ⊥ :: Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.verum_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ, succedent := Δ } :: T) → Valid 𝓢 ({ antecedent := ⊤ :: Γ, succedent := Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.and_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ, succedent := Δ ++ [φ] } :: T) → Valid 𝓢 ({ antecedent := Γ, succedent := Δ ++ [ψ] } :: T) → Valid 𝓢 ({ antecedent := Γ, succedent := φ ⋏ ψ :: Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.or_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ ++ [φ], succedent := Δ } :: T) → Valid 𝓢 ({ antecedent := Γ ++ [ψ], succedent := Δ } :: T) → Valid 𝓢 ({ antecedent := φ ⋎ ψ :: Γ, succedent := Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.or_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ, succedent := Δ ++ [φ, ψ] } :: T) → Valid 𝓢 ({ antecedent := Γ, succedent := φ ⋎ ψ :: Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.and_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ ++ [φ, ψ], succedent := Δ } :: T) → Valid 𝓢 ({ antecedent := φ ⋏ ψ :: Γ, succedent := Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.neg_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ ++ [φ], succedent := [] } :: { antecedent := Γ, succedent := Δ ++ [∼φ] } :: T) → Valid 𝓢 ({ antecedent := Γ, succedent := ∼φ :: Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.neg_right' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ ++ [φ], succedent := [] } :: { antecedent := Γ, succedent := Δ } :: T) → Valid 𝓢 ({ antecedent := Γ, succedent := ∼φ :: Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.neg_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ ++ [∼φ], succedent := Δ ++ [φ] } :: T) → Valid 𝓢 ({ antecedent := ∼φ :: Γ, succedent := Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.imply_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ ++ [φ], succedent := [ψ] } :: { antecedent := Γ, succedent := Δ ++ [φ ⇒ₗ ψ] } :: T) → Valid 𝓢 ({ antecedent := Γ, succedent := (φ ⇒ₗ ψ) :: Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.imply_right' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ ++ [φ], succedent := [ψ] } :: { antecedent := Γ, succedent := Δ } :: T) → Valid 𝓢 ({ antecedent := Γ, succedent := (φ ⇒ₗ ψ) :: Δ } :: T)

theorem PointwiseComposition.FFL.Entailment.Tableaux.Valid.imply_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {T : Tableaux F} {Γ Δ : List F} {φ ψ : F} [Entailment.Int 𝓢] : Valid 𝓢 ({ antecedent := Γ ++ [φ ⇒ₗ ψ], succedent := Δ ++ [φ] } :: T) → Valid 𝓢 ({ antecedent := Γ ++ [ψ], succedent := Δ } :: T) → Valid 𝓢 ({ antecedent := (φ ⇒ₗ ψ) :: Γ, succedent := Δ } :: T)