NF weak partition development: ClassBoundaryRawHandlersDev010.

@[reducible, inline]

abbrev NFChoice.DirectCertificate.ClassBoundaryRawHandlersDev010.Theory : Fol.SentTheory Foundation.LNF

Proof-translation construction identified upstream as Theory.

Equations

• NFChoice.DirectCertificate.ClassBoundaryRawHandlersDev010.Theory = NFChoice.Foundation.ExactLiteralTrial.LiteralHailperinNF

noncomputable def NFChoice.DirectCertificate.ClassBoundaryRawHandlersDev010.biimpSymm {L : Fol.Language} {Γ : Set (Fol.formula L)} {p q : Fol.formula L} (h : Fol.prf Γ (Fol.biimp p q)) : Fol.prf Γ (Fol.biimp q p)

Proof-translation construction identified upstream as biimpSymm.

Equations

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

noncomputable def NFChoice.DirectCertificate.ClassBoundaryRawHandlersDev010.andCongrRight {L : Fol.Language} {Γ : Set (Fol.formula L)} (p : Fol.formula L) {q r : Fol.formula L} (hqr : Fol.prf Γ (Fol.biimp q r)) : Fol.prf Γ (Fol.biimp (Fol.and' p q) (Fol.and' p r))

Proof-translation construction identified upstream as andCongrRight.

Equations

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

noncomputable def NFChoice.DirectCertificate.ClassBoundaryRawHandlersDev010.allCongr {L : Fol.Language} {Γ : Set (Fol.formula L)} {p q : Fol.formula L} (hpq : Fol.prf (Fol.liftFormula1 '' Γ) (Fol.biimp p q)) : Fol.prf Γ (Fol.biimp (Fol.preformula.all p) (Fol.preformula.all q))

Proof-translation construction identified upstream as allCongr.

Equations

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

noncomputable def NFChoice.DirectCertificate.ClassBoundaryRawHandlersDev010.exCongr {L : Fol.Language} {Γ : Set (Fol.formula L)} {p q : Fol.formula L} (hpq : Fol.prf (Fol.liftFormula1 '' Γ) (Fol.biimp p q)) : Fol.prf Γ (Fol.biimp (Fol.ex' p) (Fol.ex' q))

Proof-translation construction identified upstream as exCongr.

Equations

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

def NFChoice.DirectCertificate.ClassBoundaryRawHandlersDev010.liftedClassMem (P : Fol.formula Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as liftedClassMem.

Equations

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

theorem NFChoice.DirectCertificate.ClassBoundaryRawHandlersDev010.liftedApplyCancel (P : Fol.formula Foundation.LNF) : ClassBoundaryNormalizationDev005.applyPred (P ↑f' 1 # 1) &0 = P

noncomputable def NFChoice.DirectCertificate.ClassBoundaryRawHandlersDev010.rawDfCleq (P Q : Fol.formula Foundation.LNF) : Fol.prf Theory.fst (Fol.biimp (ClassBoundaryCoreDev006.classEq P Q) (Fol.preformula.all (Fol.biimp (liftedClassMem P) (liftedClassMem Q))))

Proof-translation construction identified upstream as rawDfCleq.

Equations

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

def NFChoice.DirectCertificate.ClassBoundaryRawHandlersDev010.liftedClassMemBody (P Q : Fol.formula Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as liftedClassMemBody.

Equations

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

noncomputable def NFChoice.DirectCertificate.ClassBoundaryRawHandlersDev010.rawDfClel (P Q : Fol.formula Foundation.LNF) : Fol.prf Theory.fst (Fol.biimp (ClassBoundaryCoreDev006.classMem P Q) (Fol.ex' (liftedClassMemBody P Q)))

Proof-translation construction identified upstream as rawDfClel.

Equations

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