Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C078C001Block021

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C078C001Part070.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078WppRefl0136 (x y g : SemanticCore.Var) :
Nominal.TReflOn [(nb078AlphaDummy285, nb078AlphaDummy286 g), (nb078AlphaDummy283, nb078AlphaDummy284 g), (nb078AlphaDummy001, g), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)] Compiler.CompactSourceSyntax.synCid.fv

Checked nominal proof certificate identified upstream as nb078_wpp_refl_0136.

Equations
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0041 (x y g : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb078AlphaDummy301, nb078AlphaDummy302 g), (nb078AlphaDummy299, nb078AlphaDummy300 g), (nb078AlphaDummy288, nb078AlphaDummy291 g), (nb078AlphaDummy287, nb078AlphaDummy290 g), (nb078AlphaDummy293, nb078AlphaDummy294 g), (nb078AlphaDummy001, g), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy301) (SemanticCore.Class.cab nb078AlphaDummy295 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy296 (SemanticCore.Class.cv nb078AlphaDummy287) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy295) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy296)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy301) (SemanticCore.Class.cab nb078AlphaDummy295 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy296 (SemanticCore.Class.cv nb078AlphaDummy287) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy295) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy296)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy302 g)) (SemanticCore.Class.cab (nb078AlphaDummy297 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy298 g) (SemanticCore.Class.cv (nb078AlphaDummy290 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy297 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy302 g)) (SemanticCore.Class.cab (nb078AlphaDummy297 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy298 g) (SemanticCore.Class.cv (nb078AlphaDummy290 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy297 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))))))).neg)

    Checked nominal proof certificate identified upstream as nb078_split_alpha_0041.

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

      Certificates from NAR4C078C001Part071.

      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0042 (x y g : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb078AlphaDummy296, nb078AlphaDummy298 g), (nb078AlphaDummy295, nb078AlphaDummy297 g), (nb078AlphaDummy325, nb078AlphaDummy326 g), (nb078AlphaDummy299, nb078AlphaDummy300 g), (nb078AlphaDummy288, nb078AlphaDummy291 g), (nb078AlphaDummy287, nb078AlphaDummy290 g), (nb078AlphaDummy293, nb078AlphaDummy294 g), (nb078AlphaDummy001, g), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy296) (SemanticCore.Class.cv nb078AlphaDummy288)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy295) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy296)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy298 g)) (SemanticCore.Class.cv (nb078AlphaDummy291 g))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy297 g)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy298 g))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

      Checked nominal proof certificate identified upstream as nb078_split_alpha_0042.

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

        Certificates from NAR4C078C001Part072.

        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb078SplitAlpha0043 (x y g : SemanticCore.Var) :
        Nominal.TAlphaWff [(nb078AlphaDummy337, nb078AlphaDummy338 g), (nb078AlphaDummy335, nb078AlphaDummy336 g), (nb078AlphaDummy289, nb078AlphaDummy292 g), (nb078AlphaDummy288, nb078AlphaDummy291 g), (nb078AlphaDummy287, nb078AlphaDummy290 g), (nb078AlphaDummy293, nb078AlphaDummy294 g), (nb078AlphaDummy001, g), (nb078AlphaDummy004, y), (nb078AlphaDummy003, x)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy337) (SemanticCore.Class.cab nb078AlphaDummy331 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy332 (SemanticCore.Class.cv nb078AlphaDummy287) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy331) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb078AlphaDummy337) (SemanticCore.Class.cab nb078AlphaDummy331 (Compiler.CompactSourceSyntax.synWrex nb078AlphaDummy332 (SemanticCore.Class.cv nb078AlphaDummy287) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb078AlphaDummy331) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb078AlphaDummy332)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy338 g)) (SemanticCore.Class.cab (nb078AlphaDummy333 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy334 g) (SemanticCore.Class.cv (nb078AlphaDummy290 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy333 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb078AlphaDummy338 g)) (SemanticCore.Class.cab (nb078AlphaDummy333 g) (Compiler.CompactSourceSyntax.synWrex (nb078AlphaDummy334 g) (SemanticCore.Class.cv (nb078AlphaDummy290 g)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb078AlphaDummy333 g)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb078AlphaDummy334 g))))))).neg)

        Checked nominal proof certificate identified upstream as nb078_split_alpha_0043.

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