Supporting results for pointwise provable equality.

@[reducible, inline]

abbrev PointwiseComposition.FFL.Axioms.NegEquiv {F : Type u_1} [LogicalConnective F] (φ : F) [LogicalNeutral F] : F

The Neg Equiv construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.NegEquiv φ = ∼φ ⇔ₗ (φ ⇒ₗ ⊥)

@[reducible, inline]

abbrev PointwiseComposition.FFL.Axioms.Verum {F : Type u_1} [LogicalNeutral F] : F

The Verum construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.Verum = ⊤

@[reducible, inline]

abbrev PointwiseComposition.FFL.Axioms.ImplyK {F : Type u_1} [LogicalConnective F] (φ ψ : F) : F

The Imply K construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.ImplyK φ ψ = φ ⇒ₗ ψ ⇒ₗ φ

@[reducible, inline]

abbrev PointwiseComposition.FFL.Axioms.ImplyS {F : Type u_1} [LogicalConnective F] (φ ψ χ : F) : F

The Imply S construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.ImplyS φ ψ χ = (φ ⇒ₗ ψ ⇒ₗ χ) ⇒ₗ (φ ⇒ₗ ψ) ⇒ₗ φ ⇒ₗ χ

@[reducible, inline]

abbrev PointwiseComposition.FFL.Axioms.AndElim₁ {F : Type u_1} [LogicalConnective F] (φ ψ : F) : F

The And Elim₁ construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.AndElim₁ φ ψ = φ ⋏ ψ ⇒ₗ φ

@[reducible, inline]

abbrev PointwiseComposition.FFL.Axioms.AndElim₂ {F : Type u_1} [LogicalConnective F] (φ ψ : F) : F

The And Elim₂ construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.AndElim₂ φ ψ = φ ⋏ ψ ⇒ₗ ψ

@[reducible, inline]

abbrev PointwiseComposition.FFL.Axioms.AndInst {F : Type u_1} [LogicalConnective F] (φ ψ : F) : F

The And Inst construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.AndInst φ ψ = φ ⇒ₗ ψ ⇒ₗ φ ⋏ ψ

@[reducible, inline]

abbrev PointwiseComposition.FFL.Axioms.OrInst₁ {F : Type u_1} [LogicalConnective F] (φ ψ : F) : F

The Or Inst₁ construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.OrInst₁ φ ψ = φ ⇒ₗ φ ⋎ ψ

@[reducible, inline]

abbrev PointwiseComposition.FFL.Axioms.OrInst₂ {F : Type u_1} [LogicalConnective F] (φ ψ : F) : F

The Or Inst₂ construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.OrInst₂ φ ψ = ψ ⇒ₗ φ ⋎ ψ

@[reducible, inline]

abbrev PointwiseComposition.FFL.Axioms.OrElim {F : Type u_1} [LogicalConnective F] (φ ψ χ : F) : F

The Or Elim construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.OrElim φ ψ χ = (φ ⇒ₗ χ) ⇒ₗ (ψ ⇒ₗ χ) ⇒ₗ φ ⋎ ψ ⇒ₗ χ

class PointwiseComposition.FFL.Entailment.ModusPonens {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Type (max u_2 u_3)

A proof system closed under modus ponens.

• mdpProof {φ ψ : F} : 𝓢 ⊢! φ ⇒ₗ ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ

  The mdp! construction in FFL.Entailment.ModusPonens.

def PointwiseComposition.FFL.Entailment.mdpProof {S : Type u_1} {F : Type u_2} {inst✝ : LogicalConnective F} {inst✝¹ : Entailment S F} {𝓢 : S} [self : ModusPonens 𝓢] {φ ψ : F} : 𝓢 ⊢! φ ⇒ₗ ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ

Alias of PointwiseComposition.FFL.Entailment.ModusPonens.mdpProof.

---

The mdp! construction in FFL.Entailment.ModusPonens.

Equations

• @PointwiseComposition.FFL.Entailment.mdpProof = @PointwiseComposition.FFL.Entailment.ModusPonens.mdpProof

def PointwiseComposition.FFL.Entailment.«term_⨀_» : Lean.TrailingParserDescr

The «term ⨀ » construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.mdp {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] : 𝓢 ⊢ φ ⇒ₗ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ

def PointwiseComposition.FFL.Entailment.«term_⨀__1» : Lean.TrailingParserDescr

The «term ⨀ 1» construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.«term_⨀!_» : Lean.TrailingParserDescr

The «term ⨀! » construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

class PointwiseComposition.FFL.Entailment.NegationEquiv {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] [LogicalNeutral F] (𝓢 : S) : Type (max u_2 u_3)

Negation ∼φ is equivalent to φ ⇒ₗ ⊥ on system.

This is weaker asssumption than "introducing ∼φ as an abbreviation of φ ⇒ₗ ⊥" (NegAbbrev).

• negEquivProof {φ : F} : 𝓢 ⊢! Axioms.NegEquiv φ

  The neg Equiv! construction in FFL.Entailment.

@[simp]

theorem PointwiseComposition.FFL.Entailment.neg_equiv {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [LogicalNeutral F] [NegationEquiv 𝓢] : 𝓢 ⊢ ∼φ ⇔ₗ (φ ⇒ₗ ⊥)

class PointwiseComposition.FFL.Entailment.HasAxiomVerum {S : Type u_1} {F : Type u_2} [Entailment S F] [LogicalNeutral F] (𝓢 : S) : Type u_3

Proofs of the truth constant in the given proof system.

• verumProof : 𝓢 ⊢! Axioms.Verum

  The verum! construction in FFL.Entailment.HasAxiomVerum.

def PointwiseComposition.FFL.Entailment.verumProof {S : Type u_1} {F : Type u_2} [Entailment S F] {𝓢 : S} [LogicalNeutral F] [HasAxiomVerum 𝓢] : 𝓢 ⊢! ⊤

The verum! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.verumProof = PointwiseComposition.FFL.Entailment.HasAxiomVerum.verumProof

@[simp]

theorem PointwiseComposition.FFL.Entailment.verum {S : Type u_1} {F : Type u_2} [Entailment S F] {𝓢 : S} [LogicalNeutral F] [HasAxiomVerum 𝓢] : 𝓢 ⊢ ⊤

class PointwiseComposition.FFL.Entailment.HasAxiomImplyK {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Type (max u_2 u_3)

Proofs of the implication-K axiom in the given proof system.

• implyKProof {φ ψ : F} : 𝓢 ⊢! Axioms.ImplyK φ ψ

  The imply K! construction in FFL.Entailment.

@[simp]

theorem PointwiseComposition.FFL.Entailment.implyK {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomImplyK 𝓢] : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.CProofOfConseqProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] (h : 𝓢 ⊢! φ) : 𝓢 ⊢! ψ ⇒ₗ φ

The C! of conseq! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CProofOfConseqProof h = PointwiseComposition.FFL.Entailment.implyKProof⨀!h

def PointwiseComposition.FFL.Entailment.dhypProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] (h : 𝓢 ⊢! φ) : 𝓢 ⊢! ψ ⇒ₗ φ

Alias of PointwiseComposition.FFL.Entailment.CProofOfConseqProof.

---

The C! of conseq! construction in FFL.Entailment.

Equations

• @PointwiseComposition.FFL.Entailment.dhypProof = @PointwiseComposition.FFL.Entailment.CProofOfConseqProof

theorem PointwiseComposition.FFL.Entailment.C_of_conseq {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] (d : 𝓢 ⊢ φ) : 𝓢 ⊢ ψ ⇒ₗ φ

theorem PointwiseComposition.FFL.Entailment.dhyp {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] (d : 𝓢 ⊢ φ) : 𝓢 ⊢ ψ ⇒ₗ φ

Alias of PointwiseComposition.FFL.Entailment.C_of_conseq.

class PointwiseComposition.FFL.Entailment.HasAxiomImplyS {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Type (max u_2 u_3)

Proofs of the implication-S axiom in the given proof system.

• implySProof {φ ψ χ : F} : 𝓢 ⊢! Axioms.ImplyS φ ψ χ

  The imply S! construction in FFL.Entailment.

@[simp]

theorem PointwiseComposition.FFL.Entailment.implyS {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomImplyS 𝓢] : 𝓢 ⊢ (φ ⇒ₗ ψ ⇒ₗ χ) ⇒ₗ (φ ⇒ₗ ψ) ⇒ₗ φ ⇒ₗ χ

class PointwiseComposition.FFL.Entailment.HasAxiomAndElim {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Type (max u_2 u_3)

Proofs of the two conjunction-elimination axioms.

• and₁Proof {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₁ φ ψ

  The and₁! construction in FFL.Entailment.

• and₂Proof {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₂ φ ψ

  The and₂! construction in FFL.Entailment.

@[simp]

theorem PointwiseComposition.FFL.Entailment.and₁ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⋏ ψ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.KProofLeft {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! φ

The K! left construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.KProofLeft d = PointwiseComposition.FFL.Entailment.and₁Proof⨀!d

theorem PointwiseComposition.FFL.Entailment.K_left {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ φ

@[simp]

theorem PointwiseComposition.FFL.Entailment.and₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⋏ ψ ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.KProofRight {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! ψ

The K! right construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.KProofRight d = PointwiseComposition.FFL.Entailment.and₂Proof⨀!d

theorem PointwiseComposition.FFL.Entailment.K_right {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ ψ

class PointwiseComposition.FFL.Entailment.HasAxiomAndInst {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Type (max u_2 u_3)

Proofs of the conjunction-introduction axiom.

• and₃Proof {φ ψ : F} : 𝓢 ⊢! Axioms.AndInst φ ψ

  The and₃! construction in FFL.Entailment.

@[simp]

theorem PointwiseComposition.FFL.Entailment.and₃ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomAndInst 𝓢] : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ φ ⋏ ψ

def PointwiseComposition.FFL.Entailment.KProofIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] (d₁ : 𝓢 ⊢! φ) (d₂ : 𝓢 ⊢! ψ) : 𝓢 ⊢! φ ⋏ ψ

The K! intro construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.KProofIntro d₁ d₂ = PointwiseComposition.FFL.Entailment.and₃Proof⨀!d₁⨀!d₂

theorem PointwiseComposition.FFL.Entailment.K_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] (d₁ : 𝓢 ⊢ φ) (d₂ : 𝓢 ⊢ ψ) : 𝓢 ⊢ φ ⋏ ψ

class PointwiseComposition.FFL.Entailment.HasAxiomOrInst {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Type (max u_2 u_3)

Data and laws for Has Axiom Or Inst in FFL.Entailment.

• or₁Proof {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₁ φ ψ

  The or₁! construction in FFL.Entailment.

• or₂Proof {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₂ φ ψ

  The or₂! construction in FFL.Entailment.

@[simp]

theorem PointwiseComposition.FFL.Entailment.or₁ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] : 𝓢 ⊢ φ ⇒ₗ φ ⋎ ψ

def PointwiseComposition.FFL.Entailment.AProofIntroLeft {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢! φ) : 𝓢 ⊢! φ ⋎ ψ

The A! intro left construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.AProofIntroLeft d = PointwiseComposition.FFL.Entailment.or₁Proof⨀!d

theorem PointwiseComposition.FFL.Entailment.A_intro_left {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢ φ) : 𝓢 ⊢ φ ⋎ ψ

@[simp]

theorem PointwiseComposition.FFL.Entailment.or₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] : 𝓢 ⊢ ψ ⇒ₗ φ ⋎ ψ

def PointwiseComposition.FFL.Entailment.AProofIntroRight {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢! ψ) : 𝓢 ⊢! φ ⋎ ψ

The A! intro right construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.AProofIntroRight d = PointwiseComposition.FFL.Entailment.or₂Proof⨀!d

theorem PointwiseComposition.FFL.Entailment.A_intro_right {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢ ψ) : 𝓢 ⊢ φ ⋎ ψ

class PointwiseComposition.FFL.Entailment.HasAxiomOrElim {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Type (max u_2 u_3)

Data and laws for Has Axiom Or Elim in FFL.Entailment.

• or₃Proof {φ ψ χ : F} : 𝓢 ⊢! Axioms.OrElim φ ψ χ

  The or₃! construction in FFL.Entailment.

@[simp]

theorem PointwiseComposition.FFL.Entailment.or₃ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] : 𝓢 ⊢ (φ ⇒ₗ χ) ⇒ₗ (ψ ⇒ₗ χ) ⇒ₗ φ ⋎ ψ ⇒ₗ χ

def PointwiseComposition.FFL.Entailment.leftAProofIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢! φ ⇒ₗ χ) (d₂ : 𝓢 ⊢! ψ ⇒ₗ χ) : 𝓢 ⊢! φ ⋎ ψ ⇒ₗ χ

The left A! intro construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.leftAProofIntro d₁ d₂ = PointwiseComposition.FFL.Entailment.or₃Proof⨀!d₁⨀!d₂

def PointwiseComposition.FFL.Entailment.CAProofOfCProofOfCProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢! φ ⇒ₗ χ) (d₂ : 𝓢 ⊢! ψ ⇒ₗ χ) : 𝓢 ⊢! φ ⋎ ψ ⇒ₗ χ

Alias of PointwiseComposition.FFL.Entailment.leftAProofIntro.

---

The left A! intro construction in FFL.Entailment.

Equations

• @PointwiseComposition.FFL.Entailment.CAProofOfCProofOfCProof = @PointwiseComposition.FFL.Entailment.leftAProofIntro

theorem PointwiseComposition.FFL.Entailment.left_A_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢ φ ⇒ₗ χ) (d₂ : 𝓢 ⊢ ψ ⇒ₗ χ) : 𝓢 ⊢ φ ⋎ ψ ⇒ₗ χ

theorem PointwiseComposition.FFL.Entailment.CA_of_C_of_C {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢ φ ⇒ₗ χ) (d₂ : 𝓢 ⊢ ψ ⇒ₗ χ) : 𝓢 ⊢ φ ⋎ ψ ⇒ₗ χ

Alias of PointwiseComposition.FFL.Entailment.left_A_intro.

def PointwiseComposition.FFL.Entailment.ofCProofOfCProofOfAProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢! φ ⇒ₗ χ) (d₂ : 𝓢 ⊢! ψ ⇒ₗ χ) (d₃ : 𝓢 ⊢! φ ⋎ ψ) : 𝓢 ⊢! χ

The of C! of C! of A! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.ofCProofOfCProofOfAProof d₁ d₂ d₃ = PointwiseComposition.FFL.Entailment.or₃Proof⨀!d₁⨀!d₂⨀!d₃

def PointwiseComposition.FFL.Entailment.AProofCases {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢! φ ⇒ₗ χ) (d₂ : 𝓢 ⊢! ψ ⇒ₗ χ) (d₃ : 𝓢 ⊢! φ ⋎ ψ) : 𝓢 ⊢! χ

Alias of PointwiseComposition.FFL.Entailment.ofCProofOfCProofOfAProof.

---

The of C! of C! of A! construction in FFL.Entailment.

Equations

• @PointwiseComposition.FFL.Entailment.AProofCases = @PointwiseComposition.FFL.Entailment.ofCProofOfCProofOfAProof

theorem PointwiseComposition.FFL.Entailment.of_C_of_C_of_A {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢ φ ⇒ₗ χ) (d₂ : 𝓢 ⊢ ψ ⇒ₗ χ) (d₃ : 𝓢 ⊢ φ ⋎ ψ) : 𝓢 ⊢ χ

theorem PointwiseComposition.FFL.Entailment.A_cases {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢ φ ⇒ₗ χ) (d₂ : 𝓢 ⊢ ψ ⇒ₗ χ) (d₃ : 𝓢 ⊢ φ ⋎ ψ) : 𝓢 ⊢ χ

Alias of PointwiseComposition.FFL.Entailment.of_C_of_C_of_A.

class PointwiseComposition.FFL.Entailment.Minimal {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] [LogicalNeutral F] (𝓢 : S) extends PointwiseComposition.FFL.Entailment.ModusPonens 𝓢, PointwiseComposition.FFL.Entailment.NegationEquiv 𝓢, PointwiseComposition.FFL.Entailment.HasAxiomVerum 𝓢, PointwiseComposition.FFL.Entailment.HasAxiomImplyK 𝓢, PointwiseComposition.FFL.Entailment.HasAxiomImplyS 𝓢, PointwiseComposition.FFL.Entailment.HasAxiomAndElim 𝓢, PointwiseComposition.FFL.Entailment.HasAxiomAndInst 𝓢, PointwiseComposition.FFL.Entailment.HasAxiomOrInst 𝓢, PointwiseComposition.FFL.Entailment.HasAxiomOrElim 𝓢 : Type (max u_2 u_3)

Data and laws for Minimal in FFL.Entailment.

• mdpProof {φ ψ : F} : 𝓢 ⊢! φ ⇒ₗ ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ
• negEquivProof {φ : F} : 𝓢 ⊢! Axioms.NegEquiv φ
• verumProof : 𝓢 ⊢! Axioms.Verum
• implyKProof {φ ψ : F} : 𝓢 ⊢! Axioms.ImplyK φ ψ
• implySProof {φ ψ χ : F} : 𝓢 ⊢! Axioms.ImplyS φ ψ χ
• and₁Proof {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₁ φ ψ
• and₂Proof {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₂ φ ψ
• and₃Proof {φ ψ : F} : 𝓢 ⊢! Axioms.AndInst φ ψ
• or₁Proof {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₁ φ ψ
• or₂Proof {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₂ φ ψ
• or₃Proof {φ ψ χ : F} : 𝓢 ⊢! Axioms.OrElim φ ψ χ

def PointwiseComposition.FFL.Entailment.COProofOfNProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [LogicalNeutral F] [HasAxiomAndElim 𝓢] [NegationEquiv 𝓢] : 𝓢 ⊢! ∼φ → 𝓢 ⊢! φ ⇒ₗ ⊥

The CO! of N! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.COProofOfNProof h = PointwiseComposition.FFL.Entailment.KProofLeft PointwiseComposition.FFL.Entailment.negEquivProof⨀!h

def PointwiseComposition.FFL.Entailment.NProofOfCOProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [LogicalNeutral F] [HasAxiomAndElim 𝓢] [NegationEquiv 𝓢] : 𝓢 ⊢! φ ⇒ₗ ⊥ → 𝓢 ⊢! ∼φ

The N! of CO! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.NProofOfCOProof h = PointwiseComposition.FFL.Entailment.KProofRight PointwiseComposition.FFL.Entailment.negEquivProof⨀!h

theorem PointwiseComposition.FFL.Entailment.N_iff_CO {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [LogicalNeutral F] [HasAxiomAndElim 𝓢] [NegationEquiv 𝓢] : 𝓢 ⊢ ∼φ ↔ 𝓢 ⊢ φ ⇒ₗ ⊥

def PointwiseComposition.FFL.Entailment.EProofIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] (b₁ : 𝓢 ⊢! φ ⇒ₗ ψ) (b₂ : 𝓢 ⊢! ψ ⇒ₗ φ) : 𝓢 ⊢! φ ⇔ₗ ψ

The E! intro construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.EProofIntro b₁ b₂ = PointwiseComposition.FFL.Entailment.KProofIntro b₁ b₂

theorem PointwiseComposition.FFL.Entailment.E_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] (h₁ : 𝓢 ⊢ φ ⇒ₗ ψ) (h₂ : 𝓢 ⊢ ψ ⇒ₗ φ) : 𝓢 ⊢ φ ⇔ₗ ψ

theorem PointwiseComposition.FFL.Entailment.K_intro_iff {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⋏ ψ ↔ 𝓢 ⊢ φ ∧ 𝓢 ⊢ ψ

theorem PointwiseComposition.FFL.Entailment.E_intro_iff {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⇔ₗ ψ ↔ 𝓢 ⊢ φ ⇒ₗ ψ ∧ 𝓢 ⊢ ψ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.CProofOfEProofMp {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndElim 𝓢] (h : 𝓢 ⊢! φ ⇔ₗ ψ) : 𝓢 ⊢! φ ⇒ₗ ψ

The C! of E! mp construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CProofOfEProofMp h = PointwiseComposition.FFL.Entailment.KProofLeft h

theorem PointwiseComposition.FFL.Entailment.C_of_E_mp {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⇔ₗ ψ → 𝓢 ⊢ φ ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.CProofOfEProofMpr {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndElim 𝓢] (h : 𝓢 ⊢! φ ⇔ₗ ψ) : 𝓢 ⊢! ψ ⇒ₗ φ

The C! of E! mpr construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CProofOfEProofMpr h = PointwiseComposition.FFL.Entailment.KProofRight h

theorem PointwiseComposition.FFL.Entailment.C_of_E_mpr {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⇔ₗ ψ → 𝓢 ⊢ ψ ⇒ₗ φ

theorem PointwiseComposition.FFL.Entailment.iff_of_E {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndElim 𝓢] (h : 𝓢 ⊢ φ ⇔ₗ ψ) : 𝓢 ⊢ φ ↔ 𝓢 ⊢ ψ

def PointwiseComposition.FFL.Entailment.CProofId {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] {φ : F} : 𝓢 ⊢! φ ⇒ₗ φ

The C! id construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CProofId = PointwiseComposition.FFL.Entailment.implySProof⨀!PointwiseComposition.FFL.Entailment.implyKProof⨀!PointwiseComposition.FFL.Entailment.implyKProof

@[simp]

theorem PointwiseComposition.FFL.Entailment.C_id {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.EProofId {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] {φ : F} : 𝓢 ⊢! φ ⇔ₗ φ

The E! id construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.EProofId = PointwiseComposition.FFL.Entailment.KProofIntro PointwiseComposition.FFL.Entailment.CProofId PointwiseComposition.FFL.Entailment.CProofId

@[simp]

theorem PointwiseComposition.FFL.Entailment.E_id {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [HasAxiomAndInst 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ ⇔ₗ φ

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.instNegationEquivOfNegAbbrevOfHasAxiomImplyKOfHasAxiomImplySOfHasAxiomAndInst {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] [LogicalNeutral F] [NegAbbrev F] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] [HasAxiomAndInst 𝓢] : NegationEquiv 𝓢

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.NOProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] [LogicalNeutral F] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] [NegationEquiv 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢! ∼⊥

The NO! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.NOProof = PointwiseComposition.FFL.Entailment.NProofOfCOProof PointwiseComposition.FFL.Entailment.CProofId

@[simp]

theorem PointwiseComposition.FFL.Entailment.NO {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] [LogicalNeutral F] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] [NegationEquiv 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢ ∼⊥

def PointwiseComposition.FFL.Entailment.mdp₁Proof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyS 𝓢] (bqr : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ) (bq : 𝓢 ⊢! φ ⇒ₗ ψ) : 𝓢 ⊢! φ ⇒ₗ χ

The mdp₁! construction in FFL.Entailment.

Equations

• bqr⨀₁bq = PointwiseComposition.FFL.Entailment.implySProof⨀!bqr⨀!bq

theorem PointwiseComposition.FFL.Entailment.mdp₁ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyS 𝓢] (hqr : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ) (hq : 𝓢 ⊢ φ ⇒ₗ ψ) : 𝓢 ⊢ φ ⇒ₗ χ

def PointwiseComposition.FFL.Entailment.«term_⨀₁_» : Lean.TrailingParserDescr

The «term ⨀₁ » construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.«term_⨀₁__1» : Lean.TrailingParserDescr

The «term ⨀₁ 1» construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.mdp₂Proof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (bqr : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s) (bq : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ) : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ s

The mdp₂! construction in FFL.Entailment.

Equations

• bqr⨀₂bq = PointwiseComposition.FFL.Entailment.CProofOfConseqProof PointwiseComposition.FFL.Entailment.implySProof⨀₁bqr⨀₁bq

theorem PointwiseComposition.FFL.Entailment.mdp₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hqr : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s) (hq : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ) : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ s

def PointwiseComposition.FFL.Entailment.«term_⨀₂_» : Lean.TrailingParserDescr

The «term ⨀₂ » construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.«term_⨀₂__1» : Lean.TrailingParserDescr

The «term ⨀₂ 1» construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.mdp₃Proof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s t : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (bqr : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s ⇒ₗ t) (bq : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s) : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ t

The mdp₃! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.mdp₃ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s t : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hqr : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s ⇒ₗ t) (hq : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s) : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ t

def PointwiseComposition.FFL.Entailment.«term_⨀₃_» : Lean.TrailingParserDescr

The «term ⨀₃ » construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.«term_⨀₃__1» : Lean.TrailingParserDescr

The «term ⨀₃ 1» construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.mdp₄Proof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s t u : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (bqr : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s ⇒ₗ t ⇒ₗ u) (bq : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s ⇒ₗ t) : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s ⇒ₗ u

The mdp₄! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.mdp₄ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s t u : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hqr : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s ⇒ₗ t ⇒ₗ u) (hq : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s ⇒ₗ t) : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ s ⇒ₗ u

def PointwiseComposition.FFL.Entailment.«term_⨀₄_» : Lean.TrailingParserDescr

The «term ⨀₄ » construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.«term_⨀₄__1» : Lean.TrailingParserDescr

The «term ⨀₄ 1» construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.CProofTrans {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (bpq : 𝓢 ⊢! φ ⇒ₗ ψ) (bqr : 𝓢 ⊢! ψ ⇒ₗ χ) : 𝓢 ⊢! φ ⇒ₗ χ

The C! trans construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CProofTrans bpq bqr = PointwiseComposition.FFL.Entailment.implySProof⨀!PointwiseComposition.FFL.Entailment.CProofOfConseqProof bqr⨀!bpq

theorem PointwiseComposition.FFL.Entailment.C_trans {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hpq : 𝓢 ⊢ φ ⇒ₗ ψ) (hqr : 𝓢 ⊢ ψ ⇒ₗ χ) : 𝓢 ⊢ φ ⇒ₗ χ

def PointwiseComposition.FFL.Entailment.CProofReplace {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {ψ₁ φ₁ φ₂ ψ₂ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h₁ : 𝓢 ⊢! ψ₁ ⇒ₗ φ₁) (h₂ : 𝓢 ⊢! φ₂ ⇒ₗ ψ₂) : 𝓢 ⊢! φ₁ ⇒ₗ φ₂ → 𝓢 ⊢! ψ₁ ⇒ₗ ψ₂

The C! replace construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CProofReplace h₁ h₂ h = PointwiseComposition.FFL.Entailment.CProofTrans h₁ (PointwiseComposition.FFL.Entailment.CProofTrans h h₂)

theorem PointwiseComposition.FFL.Entailment.C_replace {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {ψ₁ φ₁ φ₂ ψ₂ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h₁ : 𝓢 ⊢ ψ₁ ⇒ₗ φ₁) (h₂ : 𝓢 ⊢ φ₂ ⇒ₗ ψ₂) : 𝓢 ⊢ φ₁ ⇒ₗ φ₂ → 𝓢 ⊢ ψ₁ ⇒ₗ ψ₂

def PointwiseComposition.FFL.Entailment.EProofReplace {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ₁ ψ₁ φ₂ ψ₂ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h₁ : 𝓢 ⊢! φ₁ ⇔ₗ ψ₁) (h₂ : 𝓢 ⊢! φ₂ ⇔ₗ ψ₂) (h₃ : 𝓢 ⊢! φ₁ ⇔ₗ φ₂) : 𝓢 ⊢! ψ₁ ⇔ₗ ψ₂

The E! replace construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.E_replace {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ₁ ψ₁ φ₂ ψ₂ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ₁ ⇔ₗ ψ₁ → 𝓢 ⊢ φ₂ ⇔ₗ ψ₂ → 𝓢 ⊢ φ₁ ⇔ₗ φ₂ → 𝓢 ⊢ ψ₁ ⇔ₗ ψ₂

def PointwiseComposition.FFL.Entailment.EProofTrans {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h₁ : 𝓢 ⊢! φ ⇔ₗ ψ) (h₂ : 𝓢 ⊢! ψ ⇔ₗ χ) : 𝓢 ⊢! φ ⇔ₗ χ

The E! trans construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.E_trans {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h₁ : 𝓢 ⊢ φ ⇔ₗ ψ) (h₂ : 𝓢 ⊢ ψ ⇔ₗ χ) : 𝓢 ⊢ φ ⇔ₗ χ

def PointwiseComposition.FFL.Entailment.CCCCProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ φ

The CCCC! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CCCCProof = PointwiseComposition.FFL.Entailment.CProofTrans PointwiseComposition.FFL.Entailment.implyKProof PointwiseComposition.FFL.Entailment.implyKProof

theorem PointwiseComposition.FFL.Entailment.CCCC {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.CKProofOfCProofOfCProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (bq : 𝓢 ⊢! φ ⇒ₗ ψ) (br : 𝓢 ⊢! φ ⇒ₗ χ) : 𝓢 ⊢! φ ⇒ₗ ψ ⋏ χ

The CK! of C! of C! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CKProofOfCProofOfCProof bq br = PointwiseComposition.FFL.Entailment.CProofOfConseqProof PointwiseComposition.FFL.Entailment.and₃Proof⨀₁bq⨀₁br

theorem PointwiseComposition.FFL.Entailment.CK_of_C_of_C {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hq : 𝓢 ⊢ φ ⇒ₗ ψ) (hr : 𝓢 ⊢ φ ⇒ₗ χ) : 𝓢 ⊢ φ ⇒ₗ ψ ⋏ χ

def PointwiseComposition.FFL.Entailment.CKKProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢! φ ⋏ ψ ⇒ₗ ψ ⋏ φ

The CKK! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.CKK {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ ⋏ ψ ⇒ₗ ψ ⋏ φ

def PointwiseComposition.FFL.Entailment.KProofSymm {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! ψ ⋏ φ

The K! symm construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.KProofSymm h = PointwiseComposition.FFL.Entailment.CKKProof⨀!h

theorem PointwiseComposition.FFL.Entailment.K_symm {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ ψ ⋏ φ

def PointwiseComposition.FFL.Entailment.CEEProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢! φ ⇔ₗ ψ ⇒ₗ ψ ⇔ₗ φ

The CEE! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CEEProof = PointwiseComposition.FFL.Entailment.CKKProof

@[simp]

theorem PointwiseComposition.FFL.Entailment.CEE {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ ⇔ₗ ψ ⇒ₗ ψ ⇔ₗ φ

def PointwiseComposition.FFL.Entailment.EProofSymm {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h : 𝓢 ⊢! φ ⇔ₗ ψ) : 𝓢 ⊢! ψ ⇔ₗ φ

The E! symm construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.EProofSymm h = PointwiseComposition.FFL.Entailment.CEEProof⨀!h

theorem PointwiseComposition.FFL.Entailment.E_symm {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h : 𝓢 ⊢ φ ⇔ₗ ψ) : 𝓢 ⊢ ψ ⇔ₗ φ

def PointwiseComposition.FFL.Entailment.ECKCCProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢! (φ ⋏ ψ ⇒ₗ χ) ⇔ₗ (φ ⇒ₗ ψ ⇒ₗ χ)

The ECKCC! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.ECKCC {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ (φ ⋏ ψ ⇒ₗ χ) ⇔ₗ (φ ⇒ₗ ψ ⇒ₗ χ)

def PointwiseComposition.FFL.Entailment.CCProofOfCKProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (d : 𝓢 ⊢! φ ⋏ ψ ⇒ₗ χ) : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ

The CC! of CK! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CCProofOfCKProof d = PointwiseComposition.FFL.Entailment.KProofLeft PointwiseComposition.FFL.Entailment.ECKCCProof⨀!d

def PointwiseComposition.FFL.Entailment.CKProofOfCCProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (d : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ) : 𝓢 ⊢! φ ⋏ ψ ⇒ₗ χ

The CK! of CC! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CKProofOfCCProof d = PointwiseComposition.FFL.Entailment.KProofRight PointwiseComposition.FFL.Entailment.ECKCCProof⨀!d

theorem PointwiseComposition.FFL.Entailment.CK_iff_CC {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ ⋏ ψ ⇒ₗ χ ↔ 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ

def PointwiseComposition.FFL.Entailment.CVProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [LogicalNeutral F] [HasAxiomVerum 𝓢] [HasAxiomImplyK 𝓢] : 𝓢 ⊢! φ ⇒ₗ ⊤

The CV! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CVProof = PointwiseComposition.FFL.Entailment.CProofOfConseqProof PointwiseComposition.FFL.Entailment.verumProof

@[simp]

theorem PointwiseComposition.FFL.Entailment.CV {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [LogicalNeutral F] [HasAxiomImplyK 𝓢] [HasAxiomVerum 𝓢] : 𝓢 ⊢ φ ⇒ₗ ⊤

theorem PointwiseComposition.FFL.Entailment.unprovable_C_trans {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hpq : 𝓢 ⊢ φ ⇒ₗ ψ) : 𝓢 ⊬ φ ⇒ₗ χ → 𝓢 ⊬ ψ ⇒ₗ χ

theorem PointwiseComposition.FFL.Entailment.uniff_of_E {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndElim 𝓢] (H : 𝓢 ⊢ φ ⇔ₗ ψ) : 𝓢 ⊬ φ ↔ 𝓢 ⊬ ψ

def PointwiseComposition.FFL.Entailment.conj₂NthProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (n : ℕ) (hn : n < Γ.length) : 𝓢 ⊢! ⋀Γ ⇒ₗ Γ[n]

The conj₂Nth! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Entailment.conj₂NthProof [] x x_1 = ⋯.elim
• PointwiseComposition.FFL.Entailment.conj₂NthProof [ψ] 0 x_3 = PointwiseComposition.FFL.Entailment.CProofId
• PointwiseComposition.FFL.Entailment.conj₂NthProof (φ :: ψ :: Γ) 0 x_3 = PointwiseComposition.FFL.Entailment.and₁Proof

theorem PointwiseComposition.FFL.Entailment.conj₂_nth {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (n : ℕ) (hn : n < Γ.length) : 𝓢 ⊢ ⋀Γ ⇒ₗ Γ[n]

def PointwiseComposition.FFL.Entailment.leftConjProofIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : List F} {φ : F} (h : φ ∈ Γ) : 𝓢 ⊢! List.conj Γ ⇒ₗ φ

The left Conj! intro construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Entailment.leftConjProofIntro h_2 = ⋯.elim

theorem PointwiseComposition.FFL.Entailment.left_Conj_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} (h : φ ∈ Γ) : 𝓢 ⊢ List.conj Γ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.ConjProofIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (b : (φ : F) → φ ∈ Γ → 𝓢 ⊢! φ) : 𝓢 ⊢! List.conj Γ

The Conj! intro construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Entailment.ConjProofIntro [] b_2 = PointwiseComposition.FFL.Entailment.verumProof

theorem PointwiseComposition.FFL.Entailment.Conj_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ : List F} (b : ∀ φ ∈ Γ, 𝓢 ⊢ φ) : 𝓢 ⊢ List.conj Γ

def PointwiseComposition.FFL.Entailment.rightConjProofIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : F) (Γ : List F) (b : (ψ : F) → ψ ∈ Γ → 𝓢 ⊢! φ ⇒ₗ ψ) : 𝓢 ⊢! φ ⇒ₗ List.conj Γ

The right Conj! intro construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Entailment.rightConjProofIntro φ [] b_2 = PointwiseComposition.FFL.Entailment.CProofOfConseqProof PointwiseComposition.FFL.Entailment.verumProof

theorem PointwiseComposition.FFL.Entailment.right_Conj_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : F) (Γ : List F) (b : ∀ ψ ∈ Γ, 𝓢 ⊢ φ ⇒ₗ ψ) : 𝓢 ⊢ φ ⇒ₗ List.conj Γ

def PointwiseComposition.FFL.Entailment.CConjConjProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} [DecidableEq F] (h : Δ ⊆ Γ) : 𝓢 ⊢! List.conj Γ ⇒ₗ List.conj Δ

The CConj Conj! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.leftConj₂ProofIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : List F} {φ : F} (h : φ ∈ Γ) : 𝓢 ⊢! ⋀Γ ⇒ₗ φ

The left Conj₂! intro construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.leftConj₂ProofIntro h = PointwiseComposition.FFL.Entailment.cast (PointwiseComposition.FFL.Entailment.conj₂NthProof Γ (List.idxOf φ Γ) ⋯) ⋯

theorem PointwiseComposition.FFL.Entailment.left_Conj₂_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} (h : φ ∈ Γ) : 𝓢 ⊢ ⋀Γ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.Conj₂ProofIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (b : (φ : F) → φ ∈ Γ → 𝓢 ⊢! φ) : 𝓢 ⊢! ⋀Γ

The Conj₂! intro construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Entailment.Conj₂ProofIntro [] b_2 = PointwiseComposition.FFL.Entailment.verumProof
• PointwiseComposition.FFL.Entailment.Conj₂ProofIntro [ψ] b_2 = b_2 (⋀[ψ]) ⋯

theorem PointwiseComposition.FFL.Entailment.Conj₂_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ : List F} (b : ∀ φ ∈ Γ, 𝓢 ⊢ φ) : 𝓢 ⊢ ⋀Γ

def PointwiseComposition.FFL.Entailment.rightConj₂ProofIntro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : F) (Γ : List F) (b : (ψ : F) → ψ ∈ Γ → 𝓢 ⊢! φ ⇒ₗ ψ) : 𝓢 ⊢! φ ⇒ₗ ⋀Γ

The right Conj₂! intro construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Entailment.rightConj₂ProofIntro φ [] b_2 = PointwiseComposition.FFL.Entailment.CProofOfConseqProof PointwiseComposition.FFL.Entailment.verumProof
• PointwiseComposition.FFL.Entailment.rightConj₂ProofIntro φ [ψ] b_2 = b_2 (⋀[ψ]) ⋯

theorem PointwiseComposition.FFL.Entailment.right_Conj₂_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : F) (Γ : List F) (b : ∀ ψ ∈ Γ, 𝓢 ⊢ φ ⇒ₗ ψ) : 𝓢 ⊢ φ ⇒ₗ ⋀Γ

def PointwiseComposition.FFL.Entailment.CConj₂Conj₂Proof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : List F} (h : Δ ⊆ Γ) : 𝓢 ⊢! ⋀Γ ⇒ₗ ⋀Δ

The CConj₂Conj₂! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.CConj₂Conj₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} (h : Δ ⊆ Γ) : 𝓢 ⊢ ⋀Γ ⇒ₗ ⋀Δ

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.Minimal.ofEquiv {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {G : Type u_3} {T : Type u_4} [Entailment T G] [LogicalConnective G] [LogicalNeutral G] (𝓢 : S) [Entailment.Minimal 𝓢] (𝓣 : T) (f : G →ˡᶜ F) (e : (φ : G) → 𝓢 ⊢! f φ ≃ 𝓣 ⊢! φ) : Entailment.Minimal 𝓣

The of Equiv construction in FFL.Entailment.Minimal.

Equations

• One or more equations did not get rendered due to their size.

structure PointwiseComposition.FFL.Entailment.FiniteContext {S : Sort u_1} (F : Type u_2) (𝓢 : S) : Type u_2

Data and laws for Finite Context in FFL.Entailment.

• ctx : List F

  The ctx construction in FFL.Entailment.FiniteContext.

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instCoeList {F : Type u_1} {S : Sort u_2} {𝓢 : S} : Coe (List F) (FiniteContext F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.instCoeList = { coe := PointwiseComposition.FFL.Entailment.FiniteContext.mk }

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.FiniteContext.conj {F : Type u_1} {S : Sort u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] (Γ : FiniteContext F 𝓢) : F

The conj construction in FFL.Entailment.FiniteContext.

Equations

• Γ.conj = ⋀Γ.ctx

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.FiniteContext.disj {F : Type u_1} {S : Sort u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] (Γ : FiniteContext F 𝓢) : F

The disj construction in FFL.Entailment.FiniteContext.

Equations

• Γ.disj = ⋁Γ.ctx

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instEmptyCollection {F : Type u_1} {S : Sort u_2} {𝓢 : S} : EmptyCollection (FiniteContext F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.instEmptyCollection = { emptyCollection := { ctx := [] } }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instMembership {F : Type u_1} {S : Sort u_2} {𝓢 : S} : Membership F (FiniteContext F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.instMembership = { mem := fun (Γ : PointwiseComposition.FFL.Entailment.FiniteContext F 𝓢) (x : F) => x ∈ Γ.ctx }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instHasSubset {F : Type u_1} {S : Sort u_2} {𝓢 : S} : HasSubset (FiniteContext F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.instHasSubset = { Subset := fun (x1 x2 : PointwiseComposition.FFL.Entailment.FiniteContext F 𝓢) => x1.ctx ⊆ x2.ctx }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instAdjoin {F : Type u_1} {S : Sort u_2} {𝓢 : S} : Adjoin F (FiniteContext F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.instAdjoin = { adjoin := fun (x1 : F) (x2 : PointwiseComposition.FFL.Entailment.FiniteContext F 𝓢) => { ctx := x1 :: x2.ctx } }

theorem PointwiseComposition.FFL.Entailment.FiniteContext.mem_def {F : Type u_2} {S : Sort u_1} {𝓢 : S} {φ : F} {Γ : FiniteContext F 𝓢} : φ ∈ Γ ↔ φ ∈ Γ.ctx

@[simp]

theorem PointwiseComposition.FFL.Entailment.FiniteContext.coe_subset_coe_iff {F : Type u_1} {S : Sort u_2} {𝓢 : S} {Γ Δ : List F} : { ctx := Γ } ⊆ { ctx := Δ } ↔ Γ ⊆ Δ

@[simp]

theorem PointwiseComposition.FFL.Entailment.FiniteContext.mem_coe_iff {F : Type u_1} {S : Sort u_2} {𝓢 : S} {φ : F} {Γ : List F} : φ ∈ { ctx := Γ } ↔ φ ∈ Γ

theorem PointwiseComposition.FFL.Entailment.FiniteContext.not_mem_empty {F : Type u_1} {S : Sort u_2} {𝓢 : S} (φ : F) : φ ∉ ∅

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instAdjunctiveSet {F : Type u_1} {S : Sort u_2} {𝓢 : S} : AdjunctiveSet F (FiniteContext F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.inst {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] (𝓢 : S) : Entailment (FiniteContext F 𝓢) F

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.inst 𝓢 = { Prf := fun (x1 : PointwiseComposition.FFL.Entailment.FiniteContext F 𝓢) (x2 : F) => 𝓢 ⊢! x1.conj ⇒ₗ x2 }

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.FiniteContext.Prf {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] (𝓢 : S) (Γ : List F) (φ : F) : Type u_3

The Prf construction in FFL.Entailment.FiniteContext.

Equations

• (Γ ⊢[𝓢]! φ) = ({ ctx := Γ } ⊢! φ)

@[reducible, inline]

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

The Provable construction in FFL.Entailment.FiniteContext.

Equations

• (Γ ⊢[𝓢] φ) = ({ ctx := Γ } ⊢ φ)

@[reducible, inline]

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

The Unprovable construction in FFL.Entailment.FiniteContext.

Equations

• (Γ ⊬[𝓢] φ) = ({ ctx := Γ } ⊬ φ)

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.FiniteContext.PrfSet {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] (𝓢 : S) (Γ : List F) (s : Set F) : Type (max u_3 u_1)

The Prf Set construction in FFL.Entailment.FiniteContext.

Equations

• (Γ ⊢[𝓢]!* s) = ({ ctx := Γ } ⊢!* s)

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.FiniteContext.ProvableSet {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] (𝓢 : S) (Γ : List F) (s : Set F) : Prop

The Provable Set construction in FFL.Entailment.FiniteContext.

Equations

• (Γ ⊢[𝓢]* s) = ({ ctx := Γ } ⊢* s)

def PointwiseComposition.FFL.Entailment.FiniteContext.«term_⊢[_]!_» : Lean.TrailingParserDescr

The «term ⊢[ ]! » construction in FFL.Entailment.FiniteContext.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.FiniteContext.«term_⊢[_]_» : Lean.TrailingParserDescr

The «term ⊢[ ] » construction in FFL.Entailment.FiniteContext.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.FiniteContext.«term_⊬[_]_» : Lean.TrailingParserDescr

The «term ⊬[ ] » construction in FFL.Entailment.FiniteContext.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.FiniteContext.«term_⊢[_]!*_» : Lean.TrailingParserDescr

The «term ⊢[ ]!* » construction in FFL.Entailment.FiniteContext.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.FiniteContext.«term_⊢[_]*_» : Lean.TrailingParserDescr

The «term ⊢[ ]* » construction in FFL.Entailment.FiniteContext.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.FiniteContext.entailment_def {F : Type u_2} {S : Type u_1} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] (Γ : FiniteContext F 𝓢) (φ : F) : (Γ ⊢! φ) = (𝓢 ⊢! Γ.conj ⇒ₗ φ)

def PointwiseComposition.FFL.Entailment.FiniteContext.ofDefProof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} {φ : F} (b : 𝓢 ⊢! ⋀Γ ⇒ₗ φ) : Γ ⊢[𝓢]! φ

The of Def! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.ofDefProof b = b

def PointwiseComposition.FFL.Entailment.FiniteContext.toDefProof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} {φ : F} (b : Γ ⊢[𝓢]! φ) : 𝓢 ⊢! ⋀Γ ⇒ₗ φ

The to Def! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.toDefProof b = b

theorem PointwiseComposition.FFL.Entailment.FiniteContext.toₛ {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} {φ : F} (b : Γ ⊢[𝓢] φ) : 𝓢 ⊢ ⋀Γ ⇒ₗ φ

theorem PointwiseComposition.FFL.Entailment.FiniteContext.provable_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} {φ : F} : Γ ⊢[𝓢] φ ↔ 𝓢 ⊢ ⋀Γ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.FiniteContext.castProof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ' : List F} {φ' : F} {Γ : List F} {φ : F} (d : Γ ⊢[𝓢]! φ) (eΓ : Γ = Γ') (eφ : φ = φ') : Γ' ⊢[𝓢]! φ'

The cast! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.castProof d eΓ eφ = eΓ ▸ eφ ▸ d

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instAxiomatizedOfDecidableEq {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] [DecidableEq F] : Axiomatized (FiniteContext F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instCompact {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] : Compact (FiniteContext F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.FiniteContext.nthAxmProof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {Γ : List F} (n : ℕ) (h : n < Γ.length := by simp) : Γ ⊢[𝓢]! Γ[n]

The nth Axm! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.nthAxmProof n h = PointwiseComposition.FFL.Entailment.conj₂NthProof Γ n h

theorem PointwiseComposition.FFL.Entailment.FiniteContext.nth_axm {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {Γ : List F} (n : ℕ) (h : n < Γ.length := by simp) : Γ ⊢[𝓢] Γ[n]

def PointwiseComposition.FFL.Entailment.FiniteContext.byAxmProof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] [DecidableEq F] {φ : F} (h : φ ∈ Γ := by simp) : Γ ⊢[𝓢]! φ

The by Axm! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.byAxmProof h = PointwiseComposition.FFL.Entailment.Axiomatized.prfAxm ⋯

theorem PointwiseComposition.FFL.Entailment.FiniteContext.by_axm {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] {φ : F} (h : φ ∈ Γ := by classical simp) : Γ ⊢[𝓢] φ

def PointwiseComposition.FFL.Entailment.FiniteContext.weakeningProof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ Δ : List F} [Entailment.Minimal 𝓢] [DecidableEq F] (h : Γ ⊆ Δ) {φ : F} : Γ ⊢[𝓢]! φ → Δ ⊢[𝓢]! φ

The weakening! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.weakeningProof h = PointwiseComposition.FFL.Entailment.Axiomatized.weakening ⋯

theorem PointwiseComposition.FFL.Entailment.FiniteContext.weakening {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ Δ : List F} [Entailment.Minimal 𝓢] (h : Γ ⊆ Δ) {φ : F} : Γ ⊢[𝓢] φ → Δ ⊢[𝓢] φ

def PointwiseComposition.FFL.Entailment.FiniteContext.ofProof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] {φ : F} (b : 𝓢 ⊢! φ) : Γ ⊢[𝓢]! φ

The of! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.ofProof b = PointwiseComposition.FFL.Entailment.CProofOfConseqProof b

def PointwiseComposition.FFL.Entailment.FiniteContext.emptyPrfProof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {φ : F} : [] ⊢[𝓢]! φ → 𝓢 ⊢! φ

The empty Prf! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.emptyPrfProof b = b⨀!PointwiseComposition.FFL.Entailment.verumProof

theorem PointwiseComposition.FFL.Entailment.FiniteContext.provable_iff_provable {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ φ ↔ [] ⊢[𝓢] φ

theorem PointwiseComposition.FFL.Entailment.FiniteContext.of' {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢ φ) : Γ ⊢[𝓢] φ

def PointwiseComposition.FFL.Entailment.FiniteContext.idProof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {φ : F} : [φ] ⊢[𝓢]! φ

The id! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.idProof = PointwiseComposition.FFL.Entailment.FiniteContext.nthAxmProof 0 ⋯

@[simp]

theorem PointwiseComposition.FFL.Entailment.FiniteContext.id {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {φ : F} : [φ] ⊢[𝓢] φ

def PointwiseComposition.FFL.Entailment.FiniteContext.byAxm₀Proof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] {φ : F} : (φ :: Γ) ⊢[𝓢]! φ

The by Axm₀! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.byAxm₀Proof = PointwiseComposition.FFL.Entailment.FiniteContext.nthAxmProof 0 ⋯

theorem PointwiseComposition.FFL.Entailment.FiniteContext.by_axm₀ {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] {φ : F} : (φ :: Γ) ⊢[𝓢] φ

def PointwiseComposition.FFL.Entailment.FiniteContext.byAxm₁Proof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ : F} : (φ :: ψ :: Γ) ⊢[𝓢]! ψ

The by Axm₁! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.byAxm₁Proof = PointwiseComposition.FFL.Entailment.FiniteContext.nthAxmProof 1 ⋯

theorem PointwiseComposition.FFL.Entailment.FiniteContext.by_axm₁ {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ : F} : (φ :: ψ :: Γ) ⊢[𝓢] ψ

def PointwiseComposition.FFL.Entailment.FiniteContext.byAxm₂Proof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ χ : F} : (φ :: ψ :: χ :: Γ) ⊢[𝓢]! χ

The by Axm₂! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.byAxm₂Proof = PointwiseComposition.FFL.Entailment.FiniteContext.nthAxmProof 2 ⋯

theorem PointwiseComposition.FFL.Entailment.FiniteContext.by_axm₂ {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ χ : F} : (φ :: ψ :: χ :: Γ) ⊢[𝓢] χ

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instModusPonens {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : ModusPonens Γ

Equations

• Γ.instModusPonens = { mdpProof := fun {φ ψ : F} => PointwiseComposition.FFL.Entailment.mdp₁Proof }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instHasAxiomVerum {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomVerum Γ

Equations

• Γ.instHasAxiomVerum = { verumProof := PointwiseComposition.FFL.Entailment.FiniteContext.ofProof PointwiseComposition.FFL.Entailment.verumProof }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instHasAxiomImplyK {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomImplyK Γ

Equations

• Γ.instHasAxiomImplyK = { implyKProof := fun {φ ψ : F} => PointwiseComposition.FFL.Entailment.FiniteContext.ofProof PointwiseComposition.FFL.Entailment.implyKProof }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instHasAxiomImplyS {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomImplyS Γ

Equations

• Γ.instHasAxiomImplyS = { implySProof := fun {φ ψ χ : F} => PointwiseComposition.FFL.Entailment.FiniteContext.ofProof PointwiseComposition.FFL.Entailment.implySProof }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instHasAxiomAndElim {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomAndElim Γ

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instHasAxiomAndInst {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomAndInst Γ

Equations

• Γ.instHasAxiomAndInst = { and₃Proof := fun {φ ψ : F} => PointwiseComposition.FFL.Entailment.FiniteContext.ofProof PointwiseComposition.FFL.Entailment.and₃Proof }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instHasAxiomOrInst {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomOrInst Γ

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instHasAxiomOrElim {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : HasAxiomOrElim Γ

Equations

• Γ.instHasAxiomOrElim = { or₃Proof := fun {φ ψ χ : F} => PointwiseComposition.FFL.Entailment.FiniteContext.ofProof PointwiseComposition.FFL.Entailment.or₃Proof }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instNegationEquiv {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : NegationEquiv Γ

Equations

• Γ.instNegationEquiv = { negEquivProof := fun {φ : F} => PointwiseComposition.FFL.Entailment.FiniteContext.ofProof PointwiseComposition.FFL.Entailment.negEquivProof }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instMinimal {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] (Γ : FiniteContext F 𝓢) : Entailment.Minimal Γ

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.FiniteContext.mdp'Proof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ Δ : List F} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (bΓ : Γ ⊢[𝓢]! φ ⇒ₗ ψ) (bΔ : Δ ⊢[𝓢]! φ) : (Γ ++ Δ) ⊢[𝓢]! ψ

The mdp'! construction in FFL.Entailment.FiniteContext.

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.mdp'Proof bΓ bΔ = PointwiseComposition.FFL.Entailment.wk ⋯ bΓ⨀!PointwiseComposition.FFL.Entailment.wk ⋯ bΔ

def PointwiseComposition.FFL.Entailment.FiniteContext.deductProof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} : (φ :: Γ) ⊢[𝓢]! ψ → Γ ⊢[𝓢]! φ ⇒ₗ ψ

The deduct! construction in FFL.Entailment.FiniteContext.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.FiniteContext.deduct {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ : F} (h : (φ :: Γ) ⊢[𝓢] ψ) : Γ ⊢[𝓢] φ ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.FiniteContext.deductInvProof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} : Γ ⊢[𝓢]! φ ⇒ₗ ψ → (φ :: Γ) ⊢[𝓢]! ψ

The deduct Inv! construction in FFL.Entailment.FiniteContext.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.FiniteContext.deductInv {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ : F} (h : Γ ⊢[𝓢] φ ⇒ₗ ψ) : (φ :: Γ) ⊢[𝓢] ψ

theorem PointwiseComposition.FFL.Entailment.FiniteContext.deduct_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} : Γ ⊢[𝓢] φ ⇒ₗ ψ ↔ (φ :: Γ) ⊢[𝓢] ψ

def PointwiseComposition.FFL.Entailment.FiniteContext.deduct'Proof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {φ ψ : F} : [φ] ⊢[𝓢]! ψ → 𝓢 ⊢! φ ⇒ₗ ψ

The deduct'! construction in FFL.Entailment.FiniteContext.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.FiniteContext.deduct' {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {φ ψ : F} (h : [φ] ⊢[𝓢] ψ) : 𝓢 ⊢ φ ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.FiniteContext.deductInv'Proof {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! φ ⇒ₗ ψ → [φ] ⊢[𝓢]! ψ

The deduct Inv'! construction in FFL.Entailment.FiniteContext.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.FiniteContext.deductInv' {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ ⇒ₗ ψ) : [φ] ⊢[𝓢] ψ

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.deduction {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] : Deduction (FiniteContext F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instStrongCut {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [LogicalNeutral F] [Entailment.Minimal 𝓢] : StrongCut (FiniteContext F 𝓢) (FiniteContext F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

structure PointwiseComposition.FFL.Entailment.Context (F : Type u_1) {S : Sort u_2} (𝓢 : S) : Type u_1

Data and laws for Context in FFL.Entailment.

• ctx : Set F

  The ctx construction in FFL.Entailment.Context.

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.instCoeSet {S : Sort u_1} {F : Type u_2} {𝓢 : S} : Coe (Set F) (Context F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.Context.instCoeSet = { coe := PointwiseComposition.FFL.Entailment.Context.mk }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.instEmptyCollection {S : Sort u_1} {F : Type u_2} {𝓢 : S} : EmptyCollection (Context F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.Context.instEmptyCollection = { emptyCollection := { ctx := ∅ } }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.instMembership {S : Sort u_1} {F : Type u_2} {𝓢 : S} : Membership F (Context F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.Context.instMembership = { mem := fun (Γ : PointwiseComposition.FFL.Entailment.Context F 𝓢) (x : F) => x ∈ Γ.ctx }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.instHasSubset {S : Sort u_1} {F : Type u_2} {𝓢 : S} : HasSubset (Context F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.Context.instHasSubset = { Subset := fun (x1 x2 : PointwiseComposition.FFL.Entailment.Context F 𝓢) => x1.ctx ⊆ x2.ctx }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.instAdjoin {S : Sort u_1} {F : Type u_2} {𝓢 : S} : Adjoin F (Context F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.Context.instAdjoin = { adjoin := fun (x1 : F) (x2 : PointwiseComposition.FFL.Entailment.Context F 𝓢) => { ctx := insert x1 x2.ctx } }

theorem PointwiseComposition.FFL.Entailment.Context.mem_def {S : Sort u_2} {F : Type u_1} {𝓢 : S} {φ : F} {Γ : Context F 𝓢} : φ ∈ Γ ↔ φ ∈ Γ.ctx

@[simp]

theorem PointwiseComposition.FFL.Entailment.Context.coe_subset_coe_iff {S : Sort u_2} {F : Type u_1} {𝓢 : S} {Γ Δ : Set F} : { ctx := Γ } ⊆ { ctx := Δ } ↔ Γ ⊆ Δ

@[simp]

theorem PointwiseComposition.FFL.Entailment.Context.mem_coe_iff {S : Sort u_2} {F : Type u_1} {𝓢 : S} {φ : F} {Γ : Set F} : φ ∈ { ctx := Γ } ↔ φ ∈ Γ

theorem PointwiseComposition.FFL.Entailment.Context.not_mem_empty {S : Sort u_2} {F : Type u_1} {𝓢 : S} (φ : F) : φ ∉ ∅

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.instAdjunctiveSet {S : Sort u_1} {F : Type u_2} {𝓢 : S} : AdjunctiveSet F (Context F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

structure PointwiseComposition.FFL.Entailment.Context.Proof {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] (Γ : Context F 𝓢) (φ : F) : Type (max u_2 u_3)

Data and laws for Proof in FFL.Entailment.Context.

• ctx : List F

  The ctx construction in FFL.Entailment.Context.Proof.

• subset (ψ : F) : ψ ∈ self.ctx → ψ ∈ Γ
• prf : self.ctx ⊢[𝓢]! φ

  The prf construction in FFL.Entailment.Context.Proof.

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.inst {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] (𝓢 : S) : Entailment (Context F 𝓢) F

Equations

• PointwiseComposition.FFL.Entailment.Context.inst 𝓢 = { Prf := PointwiseComposition.FFL.Entailment.Context.Proof }

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.Context.Prf {S : Type u_1} {F : Type u_2} (𝓢 : S) [LogicalConnective F] [LogicalNeutral F] [Entailment S F] (Γ : Set F) (φ : F) : Type (max u_2 u_3)

The Prf construction in FFL.Entailment.Context.

Equations

• (Γ *⊢[𝓢]! φ) = ({ ctx := Γ } ⊢! φ)

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.Context.Provable {S : Type u_1} {F : Type u_2} (𝓢 : S) [LogicalConnective F] [LogicalNeutral F] [Entailment S F] (Γ : Set F) (φ : F) : Prop

The Provable construction in FFL.Entailment.Context.

Equations

• (Γ *⊢[𝓢] φ) = ({ ctx := Γ } ⊢ φ)

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.Context.Unprovable {S : Type u_1} {F : Type u_2} (𝓢 : S) [LogicalConnective F] [LogicalNeutral F] [Entailment S F] (Γ : Set F) (φ : F) : Prop

The Unprovable construction in FFL.Entailment.Context.

Equations

• (Γ *⊬[𝓢] φ) = ({ ctx := Γ } ⊬ φ)

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.Context.PrfSet {S : Type u_1} {F : Type u_2} (𝓢 : S) [LogicalConnective F] [LogicalNeutral F] [Entailment S F] (Γ s : Set F) : Type (max u_2 u_3)

The Prf Set construction in FFL.Entailment.Context.

Equations

• (Γ *⊢[𝓢]!* s) = ({ ctx := Γ } ⊢!* s)

@[reducible, inline]

abbrev PointwiseComposition.FFL.Entailment.Context.ProvableSet {S : Type u_1} {F : Type u_2} (𝓢 : S) [LogicalConnective F] [LogicalNeutral F] [Entailment S F] (Γ s : Set F) : Prop

The Provable Set construction in FFL.Entailment.Context.

Equations

• (Γ *⊢[𝓢]* s) = ({ ctx := Γ } ⊢* s)

def PointwiseComposition.FFL.Entailment.Context.«term_*⊢[_]!_» : Lean.TrailingParserDescr

The «term *⊢[ ]! » construction in FFL.Entailment.Context.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.Context.«term_*⊢[_]_» : Lean.TrailingParserDescr

The «term *⊢[ ] » construction in FFL.Entailment.Context.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.Context.«term_*⊬[_]_» : Lean.TrailingParserDescr

The «term *⊬[ ] » construction in FFL.Entailment.Context.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.Context.«term_*⊢[_]!*_» : Lean.TrailingParserDescr

The «term ⊢[ ]! » construction in FFL.Entailment.Context.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.Context.«term_*⊢[_]*_» : Lean.TrailingParserDescr

The «term ⊢[ ] » construction in FFL.Entailment.Context.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.Context.provable_iff {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {Γ : Set F} {φ : F} : Γ *⊢[𝓢] φ ↔ ∃ (Δ : List F), (∀ ψ ∈ Δ, ψ ∈ Γ) ∧ Δ ⊢[𝓢] φ

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.instAxiomatizedOfDecidableEq {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] [DecidableEq F] : Axiomatized (Context F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.Context.byAxmProof {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : Set F} {φ : F} (h : φ ∈ Γ) : Γ *⊢[𝓢]! φ

The by Axm! construction in FFL.Entailment.Context.

Equations

• PointwiseComposition.FFL.Entailment.Context.byAxmProof h = PointwiseComposition.FFL.Entailment.Axiomatized.prfAxm ⋯

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.instCompact {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] : Compact (Context F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.Context.deductProof {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] [DecidableEq F] {φ ψ : F} {Γ : Set F} : insert φ Γ *⊢[𝓢]! ψ → Γ *⊢[𝓢]! φ ⇒ₗ ψ

The deduct! construction in FFL.Entailment.Context.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.Context.deduct {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} {Γ : Set F} {ψ : F} (h : insert φ Γ *⊢[𝓢] ψ) : Γ *⊢[𝓢] φ ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.Context.deductInvProof {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : Set F} : Γ *⊢[𝓢]! φ ⇒ₗ ψ → insert φ Γ *⊢[𝓢]! ψ

The deduct Inv! construction in FFL.Entailment.Context.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.Context.deductInv {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {Γ : Set F} {φ ψ : F} (h : Γ *⊢[𝓢] φ ⇒ₗ ψ) : insert φ Γ *⊢[𝓢] ψ

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.deduction {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] [DecidableEq F] : Deduction (Context F 𝓢)

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.Context.weakeningProof {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {Γ Δ : Set F} [DecidableEq F] (h : Γ ⊆ Δ) {φ : F} : Γ *⊢[𝓢]! φ → Δ *⊢[𝓢]! φ

The weakening! construction in FFL.Entailment.Context.

Equations

• PointwiseComposition.FFL.Entailment.Context.weakeningProof h = PointwiseComposition.FFL.Entailment.Axiomatized.weakening ⋯

theorem PointwiseComposition.FFL.Entailment.Context.weakening {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {Γ Δ : Set F} (h : Γ ⊆ Δ) {φ : F} : Γ *⊢[𝓢] φ → Δ *⊢[𝓢] φ

def PointwiseComposition.FFL.Entailment.Context.ofProof {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {Γ : Set F} {φ : F} (b : 𝓢 ⊢! φ) : Γ *⊢[𝓢]! φ

The of! construction in FFL.Entailment.Context.

Equations

• PointwiseComposition.FFL.Entailment.Context.ofProof b = { ctx := [], subset := ⋯, prf := PointwiseComposition.FFL.Entailment.FiniteContext.ofProof b }

theorem PointwiseComposition.FFL.Entailment.Context.of {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} {Γ : Set F} (b : 𝓢 ⊢ φ) : Γ *⊢[𝓢] φ

def PointwiseComposition.FFL.Entailment.Context.mdpProof {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] {Γ : Set F} (bpq : Γ *⊢[𝓢]! φ ⇒ₗ ψ) (bp : Γ *⊢[𝓢]! φ) : Γ *⊢[𝓢]! ψ

The mdp! construction in FFL.Entailment.Context.

Equations

• PointwiseComposition.FFL.Entailment.Context.mdpProof bpq bp = { ctx := bpq.ctx ++ bp.ctx, subset := ⋯, prf := PointwiseComposition.FFL.Entailment.FiniteContext.mdp'Proof bpq.prf bp.prf }

theorem PointwiseComposition.FFL.Entailment.Context.by_axm {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {Γ : Set F} {φ : F} (h : φ ∈ Γ) : Γ *⊢[𝓢] φ

def PointwiseComposition.FFL.Entailment.Context.emptyPrfProof {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} : ∅ *⊢[𝓢]! φ → 𝓢 ⊢! φ

The empty Prf! construction in FFL.Entailment.Context.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.Context.emptyPrf {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} : ∅ *⊢[𝓢] φ → 𝓢 ⊢ φ

theorem PointwiseComposition.FFL.Entailment.Context.provable_iff_provable {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ φ ↔ ∅ *⊢[𝓢] φ

theorem PointwiseComposition.FFL.Entailment.Context.iff_provable_context_provable_finiteContext_toList {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} {Δ : Finset F} : ↑Δ *⊢[𝓢] φ ↔ Δ.toList ⊢[𝓢] φ

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.minimal {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] [DecidableEq F] (Γ : Context F 𝓢) : Entailment.Minimal Γ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.CVNO {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] : 𝓢 ⊢ ⊤ ⇒ₗ ∼⊥

def PointwiseComposition.FFL.Entailment.innerMDPProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! φ ⋏ (φ ⇒ₗ ψ) ⇒ₗ ψ

The inner MDP! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.inner_mdp {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ φ ⋏ (φ ⇒ₗ ψ) ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.botOfMemEitherProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} [DecidableEq F] (h₁ : φ ∈ Γ) (h₂ : ∼φ ∈ Γ) : Γ ⊢[𝓢]! ⊥

The bot of mem either! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.bot_of_mem_either {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} (h₁ : φ ∈ Γ) (h₂ : ∼φ ∈ Γ) : Γ ⊢[𝓢] ⊥

def PointwiseComposition.FFL.Entailment.negMDPProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (hnp : 𝓢 ⊢! ∼φ) (hn : 𝓢 ⊢! φ) : 𝓢 ⊢! ⊥

The neg MDP! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.negMDPProof hnp hn = PointwiseComposition.FFL.Entailment.COProofOfNProof hnp⨀!hn

theorem PointwiseComposition.FFL.Entailment.neg_mdp {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (hnp : 𝓢 ⊢ ∼φ) (hn : 𝓢 ⊢ φ) : 𝓢 ⊢ ⊥

def PointwiseComposition.FFL.Entailment.rightAProofIntroLeft {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ⇒ₗ χ) : 𝓢 ⊢! φ ⇒ₗ χ ⋎ ψ

The right A! intro left construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.right_A_intro_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ⇒ₗ χ) : 𝓢 ⊢ φ ⇒ₗ χ ⋎ ψ

def PointwiseComposition.FFL.Entailment.rightAProofIntroRight {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ ⇒ₗ χ) : 𝓢 ⊢! ψ ⇒ₗ φ ⋎ χ

The right A! intro right construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.right_A_intro_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ ⇒ₗ χ) : 𝓢 ⊢ ψ ⇒ₗ φ ⋎ χ

def PointwiseComposition.FFL.Entailment.rightKProofIntro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (hq : 𝓢 ⊢! φ ⇒ₗ ψ) (hr : 𝓢 ⊢! φ ⇒ₗ χ) : 𝓢 ⊢! φ ⇒ₗ ψ ⋏ χ

The right K! intro construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.right_K_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hq : 𝓢 ⊢ φ ⇒ₗ ψ) (hr : 𝓢 ⊢ φ ⇒ₗ χ) : 𝓢 ⊢ φ ⇒ₗ ψ ⋏ χ

theorem PointwiseComposition.FFL.Entailment.left_K_symm {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢ φ ⋏ ψ ⇒ₗ χ) : 𝓢 ⊢ ψ ⋏ φ ⇒ₗ χ

theorem PointwiseComposition.FFL.Entailment.left_K_intro_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ⇒ₗ χ) : 𝓢 ⊢ ψ ⋏ φ ⇒ₗ χ

theorem PointwiseComposition.FFL.Entailment.left_K_intro_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ⇒ₗ χ) : 𝓢 ⊢ φ ⋏ ψ ⇒ₗ χ

theorem PointwiseComposition.FFL.Entailment.cut {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ c : F} (d₁ : 𝓢 ⊢ φ₁ ⋏ c ⇒ₗ ψ₁) (d₂ : 𝓢 ⊢ φ₂ ⇒ₗ c ⋎ ψ₂) : 𝓢 ⊢ φ₁ ⋏ φ₂ ⇒ₗ ψ₁ ⋎ ψ₂

def PointwiseComposition.FFL.Entailment.CAAProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! φ ⋎ ψ ⇒ₗ ψ ⋎ φ

The CAA! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.CAA {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ φ ⋎ ψ ⇒ₗ ψ ⋎ φ

def PointwiseComposition.FFL.Entailment.AProofSymm {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (h : 𝓢 ⊢! φ ⋎ ψ) : 𝓢 ⊢! ψ ⋎ φ

The A! symm construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.AProofSymm h = PointwiseComposition.FFL.Entailment.CAAProof⨀!h

theorem PointwiseComposition.FFL.Entailment.A_symm {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ ⋎ ψ) : 𝓢 ⊢ ψ ⋎ φ

theorem PointwiseComposition.FFL.Entailment.A_assoc {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢ φ ⋎ ψ ⋎ χ ↔ 𝓢 ⊢ (φ ⋎ ψ) ⋎ χ

theorem PointwiseComposition.FFL.Entailment.K_assoc {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢ (φ ⋏ ψ) ⋏ χ ⇔ₗ φ ⋏ ψ ⋏ χ

theorem PointwiseComposition.FFL.Entailment.K_assoc_mp {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ (φ ⋏ ψ) ⋏ χ) : 𝓢 ⊢ φ ⋏ ψ ⋏ χ

theorem PointwiseComposition.FFL.Entailment.K_assoc_mpr {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ⋏ ψ ⋏ χ) : 𝓢 ⊢ (φ ⋏ ψ) ⋏ χ

def PointwiseComposition.FFL.Entailment.KProofReplaceLeft {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢! φ ⋏ ψ) (h : 𝓢 ⊢! φ ⇒ₗ χ) : 𝓢 ⊢! χ ⋏ ψ

The K! replace left construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.K_replace_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢ φ ⋏ ψ) (h : 𝓢 ⊢ φ ⇒ₗ χ) : 𝓢 ⊢ χ ⋏ ψ

def PointwiseComposition.FFL.Entailment.CKKProofOfCProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ⇒ₗ χ) : 𝓢 ⊢! φ ⋏ ψ ⇒ₗ χ ⋏ ψ

The CKK! of C! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.CKK_of_C {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ⇒ₗ χ) : 𝓢 ⊢ φ ⋏ ψ ⇒ₗ χ ⋏ ψ

def PointwiseComposition.FFL.Entailment.KProofReplaceRight {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢! φ ⋏ ψ) (h : 𝓢 ⊢! ψ ⇒ₗ χ) : 𝓢 ⊢! φ ⋏ χ

The K! replace right construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.K_replace_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢ φ ⋏ ψ) (h : 𝓢 ⊢ ψ ⇒ₗ χ) : 𝓢 ⊢ φ ⋏ χ

def PointwiseComposition.FFL.Entailment.CKKProofOfCProof' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ ⇒ₗ χ) : 𝓢 ⊢! φ ⋏ ψ ⇒ₗ φ ⋏ χ

The CKK! of C!' construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.CKK_of_C' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ ⇒ₗ χ) : 𝓢 ⊢ φ ⋏ ψ ⇒ₗ φ ⋏ χ

def PointwiseComposition.FFL.Entailment.KProofReplace {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ ξ : F} (hc : 𝓢 ⊢! φ ⋏ ψ) (h₁ : 𝓢 ⊢! φ ⇒ₗ χ) (h₂ : 𝓢 ⊢! ψ ⇒ₗ ξ) : 𝓢 ⊢! χ ⋏ ξ

The K! replace construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.KProofReplace hc h₁ h₂ = PointwiseComposition.FFL.Entailment.KProofReplaceRight (PointwiseComposition.FFL.Entailment.KProofReplaceLeft hc h₁) h₂

theorem PointwiseComposition.FFL.Entailment.K_replace {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ ξ : F} (hc : 𝓢 ⊢ φ ⋏ ψ) (h₁ : 𝓢 ⊢ φ ⇒ₗ χ) (h₂ : 𝓢 ⊢ ψ ⇒ₗ ξ) : 𝓢 ⊢ χ ⋏ ξ

def PointwiseComposition.FFL.Entailment.CKKProofOfCProofOfCProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ ξ : F} (h₁ : 𝓢 ⊢! φ ⇒ₗ χ) (h₂ : 𝓢 ⊢! ψ ⇒ₗ ξ) : 𝓢 ⊢! φ ⋏ ψ ⇒ₗ χ ⋏ ξ

The CKK! of C! of C! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.CKK_of_C_of_C {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ ξ : F} (h₁ : 𝓢 ⊢ φ ⇒ₗ χ) (h₂ : 𝓢 ⊢ ψ ⇒ₗ ξ) : 𝓢 ⊢ φ ⋏ ψ ⇒ₗ χ ⋏ ξ

def PointwiseComposition.FFL.Entailment.AProofReplaceLeft {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢! φ ⋎ ψ) (hp : 𝓢 ⊢! φ ⇒ₗ χ) : 𝓢 ⊢! χ ⋎ ψ

The A! replace left construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.A_replace_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢ φ ⋎ ψ) (hp : 𝓢 ⊢ φ ⇒ₗ χ) : 𝓢 ⊢ χ ⋎ ψ

def PointwiseComposition.FFL.Entailment.CAAProofOfCProofLeft {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hp : 𝓢 ⊢! φ ⇒ₗ χ) : 𝓢 ⊢! φ ⋎ ψ ⇒ₗ χ ⋎ ψ

The CAA! of C! left construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.CAA_of_C_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hp : 𝓢 ⊢ φ ⇒ₗ χ) : 𝓢 ⊢ φ ⋎ ψ ⇒ₗ χ ⋎ ψ

def PointwiseComposition.FFL.Entailment.AProofReplaceRight {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢! φ ⋎ ψ) (hq : 𝓢 ⊢! ψ ⇒ₗ χ) : 𝓢 ⊢! φ ⋎ χ

The A! replace right construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.A_replace_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢ φ ⋎ ψ) (hq : 𝓢 ⊢ ψ ⇒ₗ χ) : 𝓢 ⊢ φ ⋎ χ

def PointwiseComposition.FFL.Entailment.CAAProofOfCProofRight {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hq : 𝓢 ⊢! ψ ⇒ₗ χ) : 𝓢 ⊢! φ ⋎ ψ ⇒ₗ φ ⋎ χ

The CAA! of C! right construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.CAA_of_C_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hq : 𝓢 ⊢ ψ ⇒ₗ χ) : 𝓢 ⊢ φ ⋎ ψ ⇒ₗ φ ⋎ χ

def PointwiseComposition.FFL.Entailment.AProofReplace {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (h : 𝓢 ⊢! φ₁ ⋎ ψ₁) (hp : 𝓢 ⊢! φ₁ ⇒ₗ φ₂) (hq : 𝓢 ⊢! ψ₁ ⇒ₗ ψ₂) : 𝓢 ⊢! φ₂ ⋎ ψ₂

The A! replace construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.AProofReplace h hp hq = PointwiseComposition.FFL.Entailment.AProofReplaceRight (PointwiseComposition.FFL.Entailment.AProofReplaceLeft h hp) hq

theorem PointwiseComposition.FFL.Entailment.A_replace {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (h : 𝓢 ⊢ φ₁ ⋎ ψ₁) (hp : 𝓢 ⊢ φ₁ ⇒ₗ φ₂) (hq : 𝓢 ⊢ ψ₁ ⇒ₗ ψ₂) : 𝓢 ⊢ φ₂ ⋎ ψ₂

def PointwiseComposition.FFL.Entailment.CAAProofOfCProofOfCProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ ⇒ₗ φ₂) (hq : 𝓢 ⊢! ψ₁ ⇒ₗ ψ₂) : 𝓢 ⊢! φ₁ ⋎ ψ₁ ⇒ₗ φ₂ ⋎ ψ₂

The CAA! of C! of C! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.CAA_of_C_of_C {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ ⇒ₗ φ₂) (hq : 𝓢 ⊢ ψ₁ ⇒ₗ ψ₂) : 𝓢 ⊢ φ₁ ⋎ ψ₁ ⇒ₗ φ₂ ⋎ ψ₂

def PointwiseComposition.FFL.Entailment.EAAProofOfEProofOfEProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ ⇔ₗ φ₂) (hq : 𝓢 ⊢! ψ₁ ⇔ₗ ψ₂) : 𝓢 ⊢! φ₁ ⋎ ψ₁ ⇔ₗ φ₂ ⋎ ψ₂

The EAA! of E! of E! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.EAA_of_E_of_E {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ ⇔ₗ φ₂) (hq : 𝓢 ⊢ ψ₁ ⇔ₗ ψ₂) : 𝓢 ⊢ φ₁ ⋎ ψ₁ ⇔ₗ φ₂ ⋎ ψ₂

theorem PointwiseComposition.FFL.Entailment.EAAAA {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢ φ ⋎ ψ ⋎ χ ⇔ₗ (φ ⋎ ψ) ⋎ χ

theorem PointwiseComposition.FFL.Entailment.EAA_of_E_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢ ψ ⇔ₗ χ) : 𝓢 ⊢ φ ⋎ ψ ⇔ₗ φ ⋎ χ

theorem PointwiseComposition.FFL.Entailment.EAA_of_E_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢ φ ⇔ₗ χ) : 𝓢 ⊢ φ ⋎ ψ ⇔ₗ χ ⋎ ψ

def PointwiseComposition.FFL.Entailment.EKKProofOfEProofOfEProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ ⇔ₗ φ₂) (hq : 𝓢 ⊢! ψ₁ ⇔ₗ ψ₂) : 𝓢 ⊢! φ₁ ⋏ ψ₁ ⇔ₗ φ₂ ⋏ ψ₂

The EKK! of E! of E! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.EKK_of_E_of_E {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ ⇔ₗ φ₂) (hq : 𝓢 ⊢ ψ₁ ⇔ₗ ψ₂) : 𝓢 ⊢ φ₁ ⋏ ψ₁ ⇔ₗ φ₂ ⋏ ψ₂

def PointwiseComposition.FFL.Entailment.ECCProofOfEProofOfEProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ ⇔ₗ φ₂) (hq : 𝓢 ⊢! ψ₁ ⇔ₗ ψ₂) : 𝓢 ⊢! (φ₁ ⇒ₗ ψ₁) ⇔ₗ (φ₂ ⇒ₗ ψ₂)

The ECC! of E! of E! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.ECC_of_E_of_E {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ ⇔ₗ φ₂) (hq : 𝓢 ⊢ ψ₁ ⇔ₗ ψ₂) : 𝓢 ⊢ (φ₁ ⇒ₗ ψ₁) ⇔ₗ (φ₂ ⇒ₗ ψ₂)

theorem PointwiseComposition.FFL.Entailment.C_iff_C_of_E_of_E {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ ⇔ₗ φ₂) (hq : 𝓢 ⊢ ψ₁ ⇔ₗ ψ₂) : 𝓢 ⊢ φ₁ ⇒ₗ ψ₁ ↔ 𝓢 ⊢ φ₂ ⇒ₗ ψ₂

def PointwiseComposition.FFL.Entailment.dniProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢! φ ⇒ₗ ∼∼φ

The dni! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.dni {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ φ ⇒ₗ ∼∼φ

def PointwiseComposition.FFL.Entailment.dni'Proof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (b : 𝓢 ⊢! φ) : 𝓢 ⊢! ∼∼φ

The dni'! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.dni'Proof b = PointwiseComposition.FFL.Entailment.dniProof⨀!b

theorem PointwiseComposition.FFL.Entailment.dni' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (b : 𝓢 ⊢ φ) : 𝓢 ⊢ ∼∼φ

def PointwiseComposition.FFL.Entailment.ANNNNProofOfAProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (d : 𝓢 ⊢! φ ⋎ ψ) : 𝓢 ⊢! ∼∼φ ⋎ ∼∼ψ

The ANNNN! of A! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.ANNNN_of_A {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (d : 𝓢 ⊢ φ ⋎ ψ) : 𝓢 ⊢ ∼∼φ ⋎ ∼∼ψ

def PointwiseComposition.FFL.Entailment.KNNNNProofOfKProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (d : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! ∼∼φ ⋏ ∼∼ψ

The KNNNN! of K! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.KNNNN_of_K {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (d : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ ∼∼φ ⋏ ∼∼ψ

def PointwiseComposition.FFL.Entailment.CNNOOProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] : 𝓢 ⊢! ∼∼⊥ ⇒ₗ ⊥

The CNNOO! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.FFL.Entailment.ENNOOProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] : 𝓢 ⊢! ∼∼⊥ ⇔ₗ ⊥

The ENNOO! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.ENNOOProof = PointwiseComposition.FFL.Entailment.KProofIntro PointwiseComposition.FFL.Entailment.CNNOOProof PointwiseComposition.FFL.Entailment.dniProof

def PointwiseComposition.FFL.Entailment.CCCNNProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! (φ ⇒ₗ ψ) ⇒ₗ ∼ψ ⇒ₗ ∼φ

The CCCNN! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.CCCNN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ (φ ⇒ₗ ψ) ⇒ₗ ∼ψ ⇒ₗ ∼φ

@[deprecated PointwiseComposition.FFL.Entailment.CCCNNProof "use `CCCNN!`" (since := "2026-07-20")]

def PointwiseComposition.FFL.Entailment.contra₀Proof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! (φ ⇒ₗ ψ) ⇒ₗ ∼ψ ⇒ₗ ∼φ

Alias of PointwiseComposition.FFL.Entailment.CCCNNProof.

---

The CCCNN! construction in FFL.Entailment.

Equations

• @PointwiseComposition.FFL.Entailment.contra₀Proof = @PointwiseComposition.FFL.Entailment.CCCNNProof

@[deprecated PointwiseComposition.FFL.Entailment.CCCNN "use `CCCNN`" (since := "2026-07-20")]

theorem PointwiseComposition.FFL.Entailment.contra₀ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ (φ ⇒ₗ ψ) ⇒ₗ ∼ψ ⇒ₗ ∼φ

Alias of PointwiseComposition.FFL.Entailment.CCCNN.

def PointwiseComposition.FFL.Entailment.contraProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (b : 𝓢 ⊢! φ ⇒ₗ ψ) : 𝓢 ⊢! ∼ψ ⇒ₗ ∼φ

The contra! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.contraProof b = PointwiseComposition.FFL.Entailment.CCCNNProof⨀!b

theorem PointwiseComposition.FFL.Entailment.contra {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (b : 𝓢 ⊢ φ ⇒ₗ ψ) : 𝓢 ⊢ ∼ψ ⇒ₗ ∼φ

@[deprecated PointwiseComposition.FFL.Entailment.contraProof "use `contra!`" (since := "2026-07-20")]

def PointwiseComposition.FFL.Entailment.contra₀'Proof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (b : 𝓢 ⊢! φ ⇒ₗ ψ) : 𝓢 ⊢! ∼ψ ⇒ₗ ∼φ

Alias of PointwiseComposition.FFL.Entailment.contraProof.

---

The contra! construction in FFL.Entailment.

Equations

• @PointwiseComposition.FFL.Entailment.contra₀'Proof = @PointwiseComposition.FFL.Entailment.contraProof

@[deprecated PointwiseComposition.FFL.Entailment.contra "use `contra`" (since := "2026-07-20")]

theorem PointwiseComposition.FFL.Entailment.contra₀' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (b : 𝓢 ⊢ φ ⇒ₗ ψ) : 𝓢 ⊢ ∼ψ ⇒ₗ ∼φ

Alias of PointwiseComposition.FFL.Entailment.contra.

def PointwiseComposition.FFL.Entailment.CNNNNProofOfCProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (b : 𝓢 ⊢! φ ⇒ₗ ψ) : 𝓢 ⊢! ∼∼φ ⇒ₗ ∼∼ψ

The CNNNN! of C! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CNNNNProofOfCProof b = PointwiseComposition.FFL.Entailment.contraProof (PointwiseComposition.FFL.Entailment.contraProof b)

theorem PointwiseComposition.FFL.Entailment.CNNNN_of_C {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (b : 𝓢 ⊢ φ ⇒ₗ ψ) : 𝓢 ⊢ ∼∼φ ⇒ₗ ∼∼ψ

def PointwiseComposition.FFL.Entailment.CCCNNNNProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! (φ ⇒ₗ ψ) ⇒ₗ ∼∼φ ⇒ₗ ∼∼ψ

The CCCNNNN! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.CCCNNNN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ (φ ⇒ₗ ψ) ⇒ₗ ∼∼φ ⇒ₗ ∼∼ψ

def PointwiseComposition.FFL.Entailment.CNProofOfCNProofRight {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (b : 𝓢 ⊢! φ ⇒ₗ ∼ψ) : 𝓢 ⊢! ψ ⇒ₗ ∼φ

The CN! of CN! right construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.CN_of_CN_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (b : 𝓢 ⊢ φ ⇒ₗ ∼ψ) : 𝓢 ⊢ ψ ⇒ₗ ∼φ

def PointwiseComposition.FFL.Entailment.CCNCNProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! (φ ⇒ₗ ∼ψ) ⇒ₗ ψ ⇒ₗ ∼φ

The CCNCN! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.CCNCN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ (φ ⇒ₗ ∼ψ) ⇒ₗ ψ ⇒ₗ ∼φ

def PointwiseComposition.FFL.Entailment.ENNProofOfEProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (b : 𝓢 ⊢! φ ⇔ₗ ψ) : 𝓢 ⊢! ∼φ ⇔ₗ ∼ψ

The ENN! of E! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.ENN_of_E {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (b : 𝓢 ⊢ φ ⇔ₗ ψ) : 𝓢 ⊢ ∼φ ⇔ₗ ∼ψ

def PointwiseComposition.FFL.Entailment.ENNCCOOProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢! ∼∼φ ⇔ₗ ((φ ⇒ₗ ⊥) ⇒ₗ ⊥)

The ENNCCOO! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.ENNCCOO {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ ∼∼φ ⇔ₗ ((φ ⇒ₗ ⊥) ⇒ₗ ⊥)

def PointwiseComposition.FFL.Entailment.tneProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢! ∼∼∼φ ⇒ₗ ∼φ

The tne! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.tneProof = PointwiseComposition.FFL.Entailment.contraProof PointwiseComposition.FFL.Entailment.dniProof

@[simp]

theorem PointwiseComposition.FFL.Entailment.tne {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ ∼∼∼φ ⇒ₗ ∼φ

def PointwiseComposition.FFL.Entailment.tne'Proof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (b : 𝓢 ⊢! ∼∼∼φ) : 𝓢 ⊢! ∼φ

The tne'! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.tne'Proof b = PointwiseComposition.FFL.Entailment.tneProof⨀!b

theorem PointwiseComposition.FFL.Entailment.tne' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (b : 𝓢 ⊢ ∼∼∼φ) : 𝓢 ⊢ ∼φ

def PointwiseComposition.FFL.Entailment.tneIffProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢! ∼∼∼φ ⇔ₗ ∼φ

The tne Iff! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.tneIffProof = PointwiseComposition.FFL.Entailment.KProofIntro PointwiseComposition.FFL.Entailment.tneProof PointwiseComposition.FFL.Entailment.dniProof

def PointwiseComposition.FFL.Entailment.CCCProofOfCProofLeft {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ ⇒ₗ φ) : 𝓢 ⊢! (φ ⇒ₗ χ) ⇒ₗ ψ ⇒ₗ χ

The CCC! of C! left construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.CCC_of_C_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ ⇒ₗ φ) : 𝓢 ⊢ (φ ⇒ₗ χ) ⇒ₗ ψ ⇒ₗ χ

@[deprecated PointwiseComposition.FFL.Entailment.CCCProofOfCProofLeft "use `CCC!OfC!Left`" (since := "2026-07-20")]

def PointwiseComposition.FFL.Entailment.revDhypImp'Proof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ ⇒ₗ φ) : 𝓢 ⊢! (φ ⇒ₗ χ) ⇒ₗ ψ ⇒ₗ χ

Alias of PointwiseComposition.FFL.Entailment.CCCProofOfCProofLeft.

---

The CCC! of C! left construction in FFL.Entailment.

Equations

• @PointwiseComposition.FFL.Entailment.revDhypImp'Proof = @PointwiseComposition.FFL.Entailment.CCCProofOfCProofLeft

@[deprecated PointwiseComposition.FFL.Entailment.CCC_of_C_left "use `CCC_of_C_left`" (since := "2026-07-20")]

theorem PointwiseComposition.FFL.Entailment.rev_dhyp_imp' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ ⇒ₗ φ) : 𝓢 ⊢ (φ ⇒ₗ χ) ⇒ₗ ψ ⇒ₗ χ

Alias of PointwiseComposition.FFL.Entailment.CCC_of_C_left.

theorem PointwiseComposition.FFL.Entailment.C_iff_C_of_iff_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ⇔ₗ ψ) : 𝓢 ⊢ φ ⇒ₗ χ ↔ 𝓢 ⊢ ψ ⇒ₗ χ

theorem PointwiseComposition.FFL.Entailment.C_iff_C_of_iff_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ⇔ₗ ψ) : 𝓢 ⊢ χ ⇒ₗ φ ↔ 𝓢 ⊢ χ ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.CProofSwap {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (h : 𝓢 ⊢! φ ⇒ₗ ψ ⇒ₗ χ) : 𝓢 ⊢! ψ ⇒ₗ φ ⇒ₗ χ

The C! swap construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.C_swap {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ⇒ₗ ψ ⇒ₗ χ) : 𝓢 ⊢ ψ ⇒ₗ φ ⇒ₗ χ

def PointwiseComposition.FFL.Entailment.CCCCCProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] : 𝓢 ⊢! (φ ⇒ₗ ψ ⇒ₗ χ) ⇒ₗ ψ ⇒ₗ φ ⇒ₗ χ

The CCCCC! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.CCCCC {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢ (φ ⇒ₗ ψ ⇒ₗ χ) ⇒ₗ ψ ⇒ₗ φ ⇒ₗ χ

def PointwiseComposition.FFL.Entailment.CProofOfCCProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (h : 𝓢 ⊢! φ ⇒ₗ φ ⇒ₗ ψ) : 𝓢 ⊢! φ ⇒ₗ ψ

The C! of CC! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.C_of_CC {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ ⇒ₗ φ ⇒ₗ ψ) : 𝓢 ⊢ φ ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.CCCProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! φ ⇒ₗ (φ ⇒ₗ ψ) ⇒ₗ ψ

The CCC! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CCCProof = PointwiseComposition.FFL.Entailment.CProofSwap PointwiseComposition.FFL.Entailment.CProofId

theorem PointwiseComposition.FFL.Entailment.CCC {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ φ ⇒ₗ (φ ⇒ₗ ψ) ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.CCCProofOfCProofRight {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ ⇒ₗ ψ) : 𝓢 ⊢! (χ ⇒ₗ φ) ⇒ₗ χ ⇒ₗ ψ

The CCC! of C! right construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CCCProofOfCProofRight h = PointwiseComposition.FFL.Entailment.implySProof⨀!PointwiseComposition.FFL.Entailment.CProofOfConseqProof h

theorem PointwiseComposition.FFL.Entailment.CCC_of_C_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ⇒ₗ ψ) : 𝓢 ⊢ (χ ⇒ₗ φ) ⇒ₗ χ ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.CNNCCNNNNProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! ∼∼(φ ⇒ₗ ψ) ⇒ₗ ∼∼φ ⇒ₗ ∼∼ψ

The CNNCCNNNN! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.CNNCCNNNN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ ∼∼(φ ⇒ₗ ψ) ⇒ₗ ∼∼φ ⇒ₗ ∼∼ψ

def PointwiseComposition.FFL.Entailment.CNNNNProofOfNNCProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (b : 𝓢 ⊢! ∼∼(φ ⇒ₗ ψ)) : 𝓢 ⊢! ∼∼φ ⇒ₗ ∼∼ψ

The CNNNN! of NNC! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.CNNNNProofOfNNCProof b = PointwiseComposition.FFL.Entailment.CNNCCNNNNProof⨀!b

theorem PointwiseComposition.FFL.Entailment.CNNNN_of_NNC {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (b : 𝓢 ⊢ ∼∼(φ ⇒ₗ ψ)) : 𝓢 ⊢ ∼∼φ ⇒ₗ ∼∼ψ

def PointwiseComposition.FFL.Entailment.OProofIntroOfKNProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢! φ ⋏ ∼φ) : 𝓢 ⊢! ⊥

The O! intro of KN! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.O_intro_of_KN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢ φ ⋏ ∼φ) : 𝓢 ⊢ ⊥

theorem PointwiseComposition.FFL.Entailment.lac' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢ φ ⋏ ∼φ) : 𝓢 ⊢ ⊥

Law of contradiction

def PointwiseComposition.FFL.Entailment.CKNOProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢! φ ⋏ ∼φ ⇒ₗ ⊥

The CKNO! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.CKNO {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ φ ⋏ ∼φ ⇒ₗ ⊥

theorem PointwiseComposition.FFL.Entailment.lac {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ φ ⋏ ∼φ ⇒ₗ ⊥

Law of contradiction

def PointwiseComposition.FFL.Entailment.CANNNKProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! ∼φ ⋎ ∼ψ ⇒ₗ ∼(φ ⋏ ψ)

The CANNNK! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.CANNNK {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ ∼φ ⋎ ∼ψ ⇒ₗ ∼(φ ⋏ ψ)

def PointwiseComposition.FFL.Entailment.NKProofOfANNProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (d : 𝓢 ⊢! ∼φ ⋎ ∼ψ) : 𝓢 ⊢! ∼(φ ⋏ ψ)

The NK! of ANN! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.NKProofOfANNProof d = PointwiseComposition.FFL.Entailment.CANNNKProof⨀!d

theorem PointwiseComposition.FFL.Entailment.NK_of_ANN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (d : 𝓢 ⊢ ∼φ ⋎ ∼ψ) : 𝓢 ⊢ ∼(φ ⋏ ψ)

def PointwiseComposition.FFL.Entailment.CKNNNAProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! ∼φ ⋏ ∼ψ ⇒ₗ ∼(φ ⋎ ψ)

The CKNNNA! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.CKNNNA {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ ∼φ ⋏ ∼ψ ⇒ₗ ∼(φ ⋎ ψ)

def PointwiseComposition.FFL.Entailment.NAProofOfKNNProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (d : 𝓢 ⊢! ∼φ ⋏ ∼ψ) : 𝓢 ⊢! ∼(φ ⋎ ψ)

The NA! of KNN! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.NAProofOfKNNProof d = PointwiseComposition.FFL.Entailment.CKNNNAProof⨀!d

theorem PointwiseComposition.FFL.Entailment.NA_of_KNN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (d : 𝓢 ⊢ ∼φ ⋏ ∼ψ) : 𝓢 ⊢ ∼(φ ⋎ ψ)

def PointwiseComposition.FFL.Entailment.CNAKNNProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! ∼(φ ⋎ ψ) ⇒ₗ ∼φ ⋏ ∼ψ

The CNAKNN! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PointwiseComposition.FFL.Entailment.CNAKNN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ ∼(φ ⋎ ψ) ⇒ₗ ∼φ ⋏ ∼ψ

def PointwiseComposition.FFL.Entailment.KNNProofOfNAProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (b : 𝓢 ⊢! ∼(φ ⋎ ψ)) : 𝓢 ⊢! ∼φ ⋏ ∼ψ

The KNN! of NA! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.KNNProofOfNAProof b = PointwiseComposition.FFL.Entailment.CNAKNNProof⨀!b

theorem PointwiseComposition.FFL.Entailment.KNN_of_NA {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (b : 𝓢 ⊢ ∼(φ ⋎ ψ)) : 𝓢 ⊢ ∼φ ⋏ ∼ψ

def PointwiseComposition.FFL.Entailment.EConj₂ConjProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) : 𝓢 ⊢! ⋀Γ ⇔ₗ List.conj Γ

The EConj₂Conj! construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Entailment.EConj₂ConjProof [] = PointwiseComposition.FFL.Entailment.EProofId

@[simp]

theorem PointwiseComposition.FFL.Entailment.EConj₂Conj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ : List F} : 𝓢 ⊢ ⋀Γ ⇔ₗ List.conj Γ

theorem PointwiseComposition.FFL.Entailment.CConj_iff_CConj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} : 𝓢 ⊢ List.conj Γ ⇒ₗ φ ↔ 𝓢 ⊢ ⋀Γ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.rightConj'ProofIntro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_4} [DecidableEq F] (φ : F) (l : List ι) (ψ : ι → F) (b : (i : ι) → i ∈ l → 𝓢 ⊢! φ ⇒ₗ ψ i) : 𝓢 ⊢! φ ⇒ₗ (fun (x : ι → F) => List.conj' x l) ψ

! note: It may be easier to handle define List.conj based on List.conj' (?)

Equations

• One or more equations did not get rendered due to their size.

theorem PointwiseComposition.FFL.Entailment.right_Conj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} (φ : F) (l : List ι) (ψ : ι → F) (b : ∀ i ∈ l, 𝓢 ⊢ φ ⇒ₗ ψ i) : 𝓢 ⊢ φ ⇒ₗ (fun (x : ι → F) => List.conj' x l) ψ

def PointwiseComposition.FFL.Entailment.leftConj'ProofIntro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_4} {i : ι} [DecidableEq F] {l : List ι} (h : i ∈ l) (φ : ι → F) : 𝓢 ⊢! (fun (x : ι → F) => List.conj' x l) φ ⇒ₗ φ i

The left Conj'! intro construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.leftConj'ProofIntro h φ = PointwiseComposition.FFL.Entailment.leftConj₂ProofIntro ⋯

theorem PointwiseComposition.FFL.Entailment.left_Conj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} {i : ι} {l : List ι} (h : i ∈ l) (φ : ι → F) : 𝓢 ⊢ (fun (x : ι → F) => List.conj' x l) φ ⇒ₗ φ i

theorem PointwiseComposition.FFL.Entailment.right_Fconj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : F) (s : Finset F) (b : ∀ ψ ∈ s, 𝓢 ⊢ φ ⇒ₗ ψ) : 𝓢 ⊢ φ ⇒ₗ Finset.conj s

theorem PointwiseComposition.FFL.Entailment.left_Fconj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {s : Finset F} (h : φ ∈ s) : 𝓢 ⊢ Finset.conj s ⇒ₗ φ

theorem PointwiseComposition.FFL.Entailment.right_Fconj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} (φ : F) (s : Finset ι) (ψ : ι → F) (b : ∀ i ∈ s, 𝓢 ⊢ φ ⇒ₗ ψ i) : 𝓢 ⊢ φ ⇒ₗ ⋀ (i : ι) ∈ s, ψ i

theorem PointwiseComposition.FFL.Entailment.left_Fconj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} {s : Finset ι} (φ : ι → F) {i : ι} (hi : i ∈ s) : 𝓢 ⊢ (⋀ (i : ι) ∈ s, φ i) ⇒ₗ φ i

theorem PointwiseComposition.FFL.Entailment.right_Uconj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} [Fintype ι] (φ : F) (ψ : ι → F) (b : ∀ (i : ι), 𝓢 ⊢ φ ⇒ₗ ψ i) : 𝓢 ⊢ φ ⇒ₗ ⋀ (i : ι), ψ i

theorem PointwiseComposition.FFL.Entailment.left_Uconj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} [Fintype ι] (φ : ι → F) (i : ι) : 𝓢 ⊢ (⋀ (i : ι), φ i) ⇒ₗ φ i

theorem PointwiseComposition.FFL.Entailment.Conj₂_iff_forall_provable {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ : List F} : 𝓢 ⊢ ⋀Γ ↔ ∀ φ ∈ Γ, 𝓢 ⊢ φ

theorem PointwiseComposition.FFL.Entailment.CConj₂Conj₂_of_subset {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} (h : ∀ φ ∈ Γ, φ ∈ Δ) : 𝓢 ⊢ ⋀Δ ⇒ₗ ⋀Γ

theorem PointwiseComposition.FFL.Entailment.CConj₂Conj₂_of_provable {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} (h : ∀ φ ∈ Γ, Δ ⊢[𝓢] φ) : 𝓢 ⊢ ⋀Δ ⇒ₗ ⋀Γ

theorem PointwiseComposition.FFL.Entailment.CConj₂_of_forall_provable {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} (h : ∀ φ ∈ Γ, Δ ⊢[𝓢] φ) : Δ ⊢[𝓢] ⋀Γ

theorem PointwiseComposition.FFL.Entailment.CConj₂_of_unique {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} (he : ∀ g ∈ Γ, g = φ) : 𝓢 ⊢ φ ⇒ₗ ⋀Γ

theorem PointwiseComposition.FFL.Entailment.C_of_CConj₂_of_unique {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} (he : ∀ g ∈ Γ, g = φ) (hd : 𝓢 ⊢ ⋀Γ ⇒ₗ ψ) : 𝓢 ⊢ φ ⇒ₗ ψ

theorem PointwiseComposition.FFL.Entailment.CConj₂_iff_CKConj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} : 𝓢 ⊢ ⋀(φ :: Γ) ⇒ₗ ψ ↔ 𝓢 ⊢ φ ⋏ ⋀Γ ⇒ₗ ψ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CConj₂AppendKConj₂Conj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} : 𝓢 ⊢ ⋀(Γ ++ Δ) ⇒ₗ ⋀Γ ⋏ ⋀Δ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CKConj₂RemoveConj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} [DecidableEq F] : 𝓢 ⊢ ⋀(fun (x : F) => List.remove x Γ) φ ⋏ φ ⇒ₗ ⋀Γ

theorem PointwiseComposition.FFL.Entailment.CKConj₂Remove_of_CConj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} [DecidableEq F] (b : 𝓢 ⊢ ⋀Γ ⇒ₗ ψ) : 𝓢 ⊢ ⋀(fun (x : F) => List.remove x Γ) φ ⋏ φ ⇒ₗ ψ

theorem PointwiseComposition.FFL.Entailment.Conj₂Append_iff_KConj₂Conj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} : 𝓢 ⊢ ⋀(Γ ++ Δ) ↔ 𝓢 ⊢ ⋀Γ ⋏ ⋀Δ

@[simp]

theorem PointwiseComposition.FFL.Entailment.EConj₂AppendKConj₂Conj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} : 𝓢 ⊢ ⋀(Γ ++ Δ) ⇔ₗ ⋀Γ ⋏ ⋀Δ

theorem PointwiseComposition.FFL.Entailment.CConj₂Append_iff_CKConj₂Conj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ Δ : List F} : 𝓢 ⊢ ⋀(Γ ++ Δ) ⇒ₗ φ ↔ 𝓢 ⊢ ⋀Γ ⋏ ⋀Δ ⇒ₗ φ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CConj₂FConj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ : Finset F} : 𝓢 ⊢ ⋀Γ.toList ⇒ₗ Finset.conj Γ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CConj₂FConj_list {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : List F} : 𝓢 ⊢ ⋀Γ ⇒ₗ Finset.conj Γ.toFinset

@[simp]

theorem PointwiseComposition.FFL.Entailment.CFConjConj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ : Finset F} : 𝓢 ⊢ Finset.conj Γ ⇒ₗ ⋀Γ.toList

@[simp]

theorem PointwiseComposition.FFL.Entailment.CFConjConj₂_list {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : List F} : 𝓢 ⊢ Finset.conj Γ.toFinset ⇒ₗ ⋀Γ

theorem PointwiseComposition.FFL.Entailment.FConj_DT {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : Finset F} : 𝓢 ⊢ Finset.conj Γ ⇒ₗ φ ↔ ↑Γ *⊢[𝓢] φ

theorem PointwiseComposition.FFL.Entailment.FConj_iff_forall_provable {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : Finset F} : 𝓢 ⊢ Finset.conj Γ ↔ ∀ φ ∈ Γ, 𝓢 ⊢ φ

theorem PointwiseComposition.FFL.Entailment.FConj_of_FConj_of_subset {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : Finset F} (h : Δ ⊆ Γ) (hΓ : 𝓢 ⊢ Finset.conj Γ) : 𝓢 ⊢ Finset.conj Δ

theorem PointwiseComposition.FFL.Entailment.CFConjFConj_of_subset {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : Finset F} (h : Δ ⊆ Γ) : 𝓢 ⊢ Finset.conj Γ ⇒ₗ Finset.conj Δ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CFconjUnionKFconj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : Finset F} : 𝓢 ⊢ Finset.conj (Γ ∪ Δ) ⇒ₗ Finset.conj Γ ⋏ Finset.conj Δ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CinsertFConjKFConj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {Γ : Finset F} : 𝓢 ⊢ Finset.conj (insert φ Γ) ⇒ₗ φ ⋏ Finset.conj Γ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CKFconjFconjUnion {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : Finset F} : 𝓢 ⊢ Finset.conj Γ ⋏ Finset.conj Δ ⇒ₗ Finset.conj (Γ ∪ Δ)

@[simp]

theorem PointwiseComposition.FFL.Entailment.CKFConjinsertFConj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {Γ : Finset F} : 𝓢 ⊢ φ ⋏ Finset.conj Γ ⇒ₗ Finset.conj (insert φ Γ)

theorem PointwiseComposition.FFL.Entailment.FConj_DT' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {Γ Δ : Finset F} : ↑Γ *⊢[𝓢] Finset.conj Δ ⇒ₗ φ ↔ ↑(Γ ∪ Δ) *⊢[𝓢] φ

theorem PointwiseComposition.FFL.Entailment.CFconjFconj_of_provable {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : Finset F} (h : ∀ φ ∈ Γ, ↑Δ *⊢[𝓢] φ) : 𝓢 ⊢ Finset.conj Δ ⇒ₗ Finset.conj Γ

def PointwiseComposition.FFL.Entailment.rightDisjProofIntro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (Γ : List F) (h : φ ∈ Γ) : 𝓢 ⊢! φ ⇒ₗ List.disj Γ

The right Disj! intro construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Entailment.rightDisjProofIntro [] h_2 = ⋯.elim

theorem PointwiseComposition.FFL.Entailment.right_Disj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (Γ : List F) (h : φ ∈ Γ) : 𝓢 ⊢ φ ⇒ₗ List.disj Γ

def PointwiseComposition.FFL.Entailment.rightDisjProofIntro' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (Γ : List F) (h : φ ∈ Γ) (hψ : 𝓢 ⊢! ψ ⇒ₗ φ) : 𝓢 ⊢! ψ ⇒ₗ List.disj Γ

The right Disj! intro' construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.rightDisjProofIntro' Γ h hψ = PointwiseComposition.FFL.Entailment.CProofTrans hψ (PointwiseComposition.FFL.Entailment.rightDisjProofIntro Γ h)

theorem PointwiseComposition.FFL.Entailment.right_Disj_intro' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (Γ : List F) (h : φ ∈ Γ) (hψ : 𝓢 ⊢ ψ ⇒ₗ φ) : 𝓢 ⊢ ψ ⇒ₗ List.disj Γ

def PointwiseComposition.FFL.Entailment.rightDisj₂ProofIntro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (Γ : List F) (h : φ ∈ Γ) : 𝓢 ⊢! φ ⇒ₗ ⋁Γ

The right Disj₂! intro construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Entailment.rightDisj₂ProofIntro [] h_2 = ⋯.elim
• PointwiseComposition.FFL.Entailment.rightDisj₂ProofIntro [ψ] h_2 = ⋯ ▸ PointwiseComposition.FFL.Entailment.CProofId

theorem PointwiseComposition.FFL.Entailment.right_Disj₂_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (Γ : List F) (h : φ ∈ Γ) : 𝓢 ⊢ φ ⇒ₗ ⋁Γ

def PointwiseComposition.FFL.Entailment.rightDisj'ProofIntro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_4} {i : ι} [DecidableEq F] (φ : ι → F) (l : List ι) (h : i ∈ l) : 𝓢 ⊢! φ i ⇒ₗ (fun (x : ι → F) => List.disj' x l) φ

The right Disj'! intro construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.rightDisj'ProofIntro φ l h = PointwiseComposition.FFL.Entailment.rightDisj₂ProofIntro (List.map φ l) ⋯

theorem PointwiseComposition.FFL.Entailment.right_Disj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} {i : ι} (φ : ι → F) (l : List ι) (h : i ∈ l) : 𝓢 ⊢ φ i ⇒ₗ (fun (x : ι → F) => List.disj' x l) φ

theorem PointwiseComposition.FFL.Entailment.right_Fdisj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (s : Finset F) (h : φ ∈ s) : 𝓢 ⊢ φ ⇒ₗ Finset.disj s

theorem PointwiseComposition.FFL.Entailment.right_Fdisj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} (s : Finset ι) (φ : ι → F) {i : ι} (hi : i ∈ s) : 𝓢 ⊢ φ i ⇒ₗ ⋁ (j : ι) ∈ s, φ j

theorem PointwiseComposition.FFL.Entailment.right_Udisj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} {i : ι} [Fintype ι] (φ : ι → F) : 𝓢 ⊢ φ i ⇒ₗ ⋁ (j : ι), φ j

theorem PointwiseComposition.FFL.Entailment.CFConjFDisj_of_K_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ Δ : Finset F} [DecidableEq F] (hp : φ ∈ Γ) (hpq : ψ ∈ Γ) (hψ : φ ⋏ ψ ∈ Δ) : 𝓢 ⊢ Finset.conj Γ ⇒ₗ Finset.disj Δ

theorem PointwiseComposition.FFL.Entailment.CFConjFDisj_of_innerMDP {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ Δ : Finset F} [DecidableEq F] (hp : φ ∈ Γ) (hpq : φ ⇒ₗ ψ ∈ Γ) (hψ : ψ ∈ Δ) : 𝓢 ⊢ Finset.conj Γ ⇒ₗ Finset.disj Δ

theorem PointwiseComposition.FFL.Entailment.iff_FiniteContext_Context {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {Γ : List F} : Γ ⊢[𝓢] φ ↔ ↑Γ.toFinset *⊢[𝓢] φ

theorem PointwiseComposition.FFL.Entailment.FConj'_iff_forall_provable {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {α : Type u_3} {s : Finset α} {ι : α → F} : (𝓢 ⊢ ⋀ (i : α) ∈ s, ι i) ↔ ∀ i ∈ s, 𝓢 ⊢ ι i

theorem PointwiseComposition.FFL.Entailment.Context.provable_iff_finset {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ : Set F} {φ : F} : Γ *⊢[𝓢] φ ↔ ∃ (Δ : Finset F), ↑Δ ⊆ Γ ∧ ↑Δ *⊢[𝓢] φ

theorem PointwiseComposition.FFL.Entailment.Context.bot_of_mem_neg {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : Set F} (h₁ : φ ∈ Γ) (h₂ : ∼φ ∈ Γ) : Γ *⊢[𝓢] ⊥