Documentation

LeanPool.PointwiseComposition.Foundation.Meta.ClProverTheorems

Supporting results for pointwise provable equality.

Proof automation based on the proof search on $\mathbf{LK}$ #

source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.to_provable {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (φ : F) (h : Entailment.TwoSided 𝓢 [] [φ]) :
𝓢 ⊢ φ
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.rotate_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (hφ : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ])) :
Entailment.TwoSided 𝓢 Γ (φ :: Δ)
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.rotate_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (hφ : Entailment.TwoSided 𝓢 (Γ ++ [φ]) Δ) :
Entailment.TwoSided 𝓢 (φ :: Γ) Δ
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.add_hyp {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (𝒯 : S) (s : 𝒯 ≼ 𝓢) (Γ Δ : List F) (φ : F) (hφ : 𝒯 ⊢ φ) (h : Entailment.TwoSided 𝓢 (φ :: Γ) Δ) :
Entailment.TwoSided 𝓢 Γ Δ
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.right_closed {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (h : φ ∈ Γ) :
Entailment.TwoSided 𝓢 Γ (φ :: Δ)
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.left_closed {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (h : φ ∈ Δ) :
Entailment.TwoSided 𝓢 (φ :: Γ) Δ
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.verum_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) :
Entailment.TwoSided 𝓢 Γ (⊤ :: Δ)
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.falsum_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) :
Entailment.TwoSided 𝓢 (⊥ :: Γ) Δ
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.falsum_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (h : Entailment.TwoSided 𝓢 Γ Δ) :
Entailment.TwoSided 𝓢 Γ (⊥ :: Δ)
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.verum_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (h : Entailment.TwoSided 𝓢 Γ Δ) :
Entailment.TwoSided 𝓢 (⊤ :: Γ) Δ
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.and_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (hφ : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ])) (hψ : Entailment.TwoSided 𝓢 Γ (Δ ++ [ψ])) :
Entailment.TwoSided 𝓢 Γ (φ ⋏ ψ :: Δ)
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.or_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (hφ : Entailment.TwoSided 𝓢 (Γ ++ [φ]) Δ) (hψ : Entailment.TwoSided 𝓢 (Γ ++ [ψ]) Δ) :
Entailment.TwoSided 𝓢 (φ ⋎ ψ :: Γ) Δ
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.or_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (h : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ, ψ])) :
Entailment.TwoSided 𝓢 Γ (φ ⋎ ψ :: Δ)
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.and_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (h : Entailment.TwoSided 𝓢 (Γ ++ [φ, ψ]) Δ) :
Entailment.TwoSided 𝓢 (φ ⋏ ψ :: Γ) Δ
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.neg_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (h : Entailment.TwoSided 𝓢 (Γ ++ [φ]) Δ) :
Entailment.TwoSided 𝓢 Γ (∼φ :: Δ)
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.neg_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ : F) (h : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ])) :
Entailment.TwoSided 𝓢 (∼φ :: Γ) Δ
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.imply_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (h : Entailment.TwoSided 𝓢 (Γ ++ [φ]) (Δ ++ [ψ])) :
Entailment.TwoSided 𝓢 Γ ((φ ⇒ₗ ψ) :: Δ)
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.imply_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (hφ : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ])) (hψ : Entailment.TwoSided 𝓢 (Γ ++ [ψ]) Δ) :
Entailment.TwoSided 𝓢 ((φ ⇒ₗ ψ) :: Γ) Δ
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.iff_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (hr : Entailment.TwoSided 𝓢 (Γ ++ [φ]) (Δ ++ [ψ])) (hl : Entailment.TwoSided 𝓢 (Γ ++ [ψ]) (Δ ++ [φ])) :
Entailment.TwoSided 𝓢 Γ ((φ ⇔ₗ ψ) :: Δ)
source
theorem PointwiseComposition.FFL.Meta.ClProver.Theorems.iff_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) [Entailment.Cl 𝓢] (Γ Δ : List F) (φ ψ : F) (hr : Entailment.TwoSided 𝓢 Γ (Δ ++ [φ, ψ])) (hl : Entailment.TwoSided 𝓢 (Γ ++ [φ, ψ]) Δ) :
Entailment.TwoSided 𝓢 ((φ ⇔ₗ ψ) :: Γ) Δ