Documentation

LeanPool.NFWeakPartition.NominalAtomicRecanonDev

NF weak partition development: NominalAtomicRecanonDev.

source
@[reducible, inline]
abbrev NFChoice.DirectNominalPrf.Nominal.AtomicRecanonDev.Theory :
Fol.SentTheory Foundation.LNF

Proof-translation construction identified upstream as Theory.

Equations
Instances For

    Atomic syntactic bridges for the two Metamath print ambiguities.

    source
    noncomputable def NFChoice.DirectNominalPrf.Nominal.AtomicRecanonDev.representsCvSelf (s : Fol.term Foundation.LNF) :
    Fol.prf Theory.fst (DirectCertificate.ClassBoundaryNormalizationDev005.represents s (DirectCertificate.ClassBoundaryNormalizationDev005.cvPred s))

    Proof-translation construction identified upstream as representsCvSelf.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem NFChoice.DirectNominalPrf.Nominal.AtomicRecanonDev.representsCvTemplateSubst (s t : Fol.term Foundation.LNF) :
      DirectCertificate.ClassBoundaryNormalizationDev005.represents (Fol.liftTerm1 s) (DirectCertificate.ClassBoundaryNormalizationDev005.cvPred &0) [t // 0]f = DirectCertificate.ClassBoundaryNormalizationDev005.represents s (DirectCertificate.ClassBoundaryNormalizationDev005.cvPred t)
      source
      noncomputable def NFChoice.DirectNominalPrf.Nominal.AtomicRecanonDev.eqToRepresentsCv (s t : Fol.term Foundation.LNF) :
      Fol.prf Theory.fst ((Fol.preformula.equal s t).imp (DirectCertificate.ClassBoundaryNormalizationDev005.represents s (DirectCertificate.ClassBoundaryNormalizationDev005.cvPred t)))

      Proof-translation construction identified upstream as eqToRepresentsCv.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def NFChoice.DirectNominalPrf.Nominal.AtomicRecanonDev.objEqClassEqBiimp (s t : Fol.term Foundation.LNF) :
        Fol.prf Theory.fst (Fol.biimp (Fol.preformula.equal s t) (DirectCertificate.ClassBoundaryCoreDev006.classEq (DirectCertificate.ClassBoundaryNormalizationDev005.cvPred s) (DirectCertificate.ClassBoundaryNormalizationDev005.cvPred t)))

        Proof-translation construction identified upstream as objEqClassEqBiimp.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NFChoice.DirectNominalPrf.Nominal.AtomicRecanonDev.objMemClassMemBiimp (s t : Fol.term Foundation.LNF) :
          Fol.prf Theory.fst (Fol.biimp (DirectCertificate.ClassBoundaryNormalizationDev005.mem s t) (DirectCertificate.ClassBoundaryCoreDev006.classMem (DirectCertificate.ClassBoundaryNormalizationDev005.cvPred s) (DirectCertificate.ClassBoundaryNormalizationDev005.cvPred t)))

          Proof-translation construction identified upstream as objMemClassMemBiimp.

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