NF weak partition development: ClassBoundaryBiimpDev009.

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

Proof-translation construction identified upstream as biimpForward.

Equations

• NFChoice.DirectCertificate.ClassBoundaryBiimpDev009.biimpForward h hp = NFChoice.Fol.prf.impE p (NFChoice.Fol.andE1 (NFChoice.Fol.preformula.imp q p) h) hp

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

Proof-translation construction identified upstream as biimpBackward.

Equations

• NFChoice.DirectCertificate.ClassBoundaryBiimpDev009.biimpBackward h hq = NFChoice.Fol.prf.impE q (NFChoice.Fol.andE2 (NFChoice.Fol.preformula.imp p q) h) hq

noncomputable def NFChoice.DirectCertificate.ClassBoundaryBiimpDev009.biimpCongr {L : Fol.Language} {Γ : Set (Fol.formula L)} {p p' q q' : Fol.formula L} (hpEq : Fol.prf Γ (Fol.biimp p p')) (hqEq : Fol.prf Γ (Fol.biimp q q')) : Fol.prf Γ (Fol.biimp (Fol.biimp p q) (Fol.biimp p' q'))

Proof-translation construction identified upstream as biimpCongr.

Equations

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