Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C078C001Block045

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C078C001Part135.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078WppRefl0372 (x y h : SemanticCore.Var) :
Nominal.TReflOn [(nb078AlphaDummy765, nb078AlphaDummy766 h), (nb078AlphaDummy763, nb078AlphaDummy764 h), (nb078AlphaDummy002, h), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)] Compiler.CompactSourceSyntax.synCid.fv

Checked nominal proof certificate identified upstream as nb078_wpp_refl_0372.

Equations
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0113 (x y h : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb078AlphaDummy781, nb078AlphaDummy782 h), (nb078AlphaDummy779, nb078AlphaDummy780 h), (nb078AlphaDummy768, nb078AlphaDummy771 h), (nb078AlphaDummy767, nb078AlphaDummy770 h), (nb078AlphaDummy773, nb078AlphaDummy774 h), (nb078AlphaDummy002, h), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy781) (SemanticCore.Class.cab nb078AlphaDummy775 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy776 (SemanticCore.Class.cv nb078AlphaDummy767) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy775) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy781) (SemanticCore.Class.cab nb078AlphaDummy775 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy776 (SemanticCore.Class.cv nb078AlphaDummy767) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy775) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy782 h)) (SemanticCore.Class.cab (nb078AlphaDummy777 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy778 h) (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy777 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy782 h)) (SemanticCore.Class.cab (nb078AlphaDummy777 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy778 h) (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy777 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))))))).neg)

    Checked nominal proof certificate identified upstream as nb078_split_alpha_0113.

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

      Certificates from NAR4C078C001Part136.

      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0114 (x y h : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb078AlphaDummy776, nb078AlphaDummy778 h), (nb078AlphaDummy775, nb078AlphaDummy777 h), (nb078AlphaDummy805, nb078AlphaDummy806 h), (nb078AlphaDummy779, nb078AlphaDummy780 h), (nb078AlphaDummy768, nb078AlphaDummy771 h), (nb078AlphaDummy767, nb078AlphaDummy770 h), (nb078AlphaDummy773, nb078AlphaDummy774 h), (nb078AlphaDummy002, h), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy776) (SemanticCore.Class.cv nb078AlphaDummy768)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy775) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy776)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy778 h)) (SemanticCore.Class.cv (nb078AlphaDummy771 h))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy777 h)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy778 h))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

      Checked nominal proof certificate identified upstream as nb078_split_alpha_0114.

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

        Certificates from NAR4C078C001Part137.

        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0115 (x y h : SemanticCore.Var) :
        Nominal.TAlphaWff [(nb078AlphaDummy817, nb078AlphaDummy818 h), (nb078AlphaDummy815, nb078AlphaDummy816 h), (nb078AlphaDummy769, nb078AlphaDummy772 h), (nb078AlphaDummy768, nb078AlphaDummy771 h), (nb078AlphaDummy767, nb078AlphaDummy770 h), (nb078AlphaDummy773, nb078AlphaDummy774 h), (nb078AlphaDummy002, h), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy817) (SemanticCore.Class.cab nb078AlphaDummy811 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy812 (SemanticCore.Class.cv nb078AlphaDummy767) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy811) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy817) (SemanticCore.Class.cab nb078AlphaDummy811 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy812 (SemanticCore.Class.cv nb078AlphaDummy767) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy811) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy812)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy818 h)) (SemanticCore.Class.cab (nb078AlphaDummy813 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy814 h) (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy813 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy818 h)) (SemanticCore.Class.cab (nb078AlphaDummy813 h) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy814 h) (SemanticCore.Class.cv (nb078AlphaDummy770 h)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy813 h)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy814 h))))))).neg)

        Checked nominal proof certificate identified upstream as nb078_split_alpha_0115.

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