Documentation

LeanPool.NFWeakPartition.Certificates.NAR4C068C001Block010

Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part037.

source
noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0089 (x y f : SemanticCore.Var) :
Nominal.TAlphaWff [(nb068AlphaDummy351, nb068AlphaDummy354 f), (nb068AlphaDummy350, nb068AlphaDummy353 f), (nb068AlphaDummy349, nb068AlphaDummy352 f), (nb068AlphaDummy347, nb068AlphaDummy348 f), (nb068AlphaDummy343, nb068AlphaDummy345 f), (nb068AlphaDummy344, nb068AlphaDummy346 f), (nb068AlphaDummy336, nb068AlphaDummy338 f), (nb068AlphaDummy335, nb068AlphaDummy337 f), (nb068AlphaDummy341, nb068AlphaDummy342 f), (nb068AlphaDummy339, nb068AlphaDummy340 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy350) (SemanticCore.Class.cv nb068AlphaDummy351)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy349) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy350) (SemanticCore.Class.cv nb068AlphaDummy351))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy353 f)) (SemanticCore.Class.cv (nb068AlphaDummy354 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy352 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy353 f)) (SemanticCore.Class.cv (nb068AlphaDummy354 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0089.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0090 (x y f : SemanticCore.Var) :
    Nominal.TAlphaWff [(nb068AlphaDummy343, nb068AlphaDummy345 f), (nb068AlphaDummy344, nb068AlphaDummy346 f), (nb068AlphaDummy336, nb068AlphaDummy338 f), (nb068AlphaDummy335, nb068AlphaDummy337 f), (nb068AlphaDummy341, nb068AlphaDummy342 f), (nb068AlphaDummy339, nb068AlphaDummy340 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy343) (SemanticCore.Class.cv nb068AlphaDummy336)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy344) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy343) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy343) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy343)))).neg (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy345 f)) (SemanticCore.Class.cv (nb068AlphaDummy338 f))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy346 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy345 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy345 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy345 f))))).neg

    Checked nominal proof certificate identified upstream as nb068_split_alpha_0090.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0091 (x y f : SemanticCore.Var) :
      Nominal.TAlphaWff [(nb068AlphaDummy351, nb068AlphaDummy354 f), (nb068AlphaDummy350, nb068AlphaDummy353 f), (nb068AlphaDummy349, nb068AlphaDummy352 f), (nb068AlphaDummy347, nb068AlphaDummy348 f), (nb068AlphaDummy343, nb068AlphaDummy345 f), (nb068AlphaDummy344, nb068AlphaDummy346 f), (nb068AlphaDummy369, nb068AlphaDummy370 f), (nb068AlphaDummy367, nb068AlphaDummy368 f), (nb068AlphaDummy336, nb068AlphaDummy338 f), (nb068AlphaDummy335, nb068AlphaDummy337 f), (nb068AlphaDummy365, nb068AlphaDummy366 f), (nb068AlphaDummy339, nb068AlphaDummy340 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy350) (SemanticCore.Class.cv nb068AlphaDummy351)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy349) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy350) (SemanticCore.Class.cv nb068AlphaDummy351))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy353 f)) (SemanticCore.Class.cv (nb068AlphaDummy354 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy352 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy353 f)) (SemanticCore.Class.cv (nb068AlphaDummy354 f)))).neg)

      Checked nominal proof certificate identified upstream as nb068_split_alpha_0091.

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

        Certificates from NAR4C068C001Part038.

        source
        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0092 (x y f : SemanticCore.Var) :
        Nominal.TAlphaWff [(nb068AlphaDummy343, nb068AlphaDummy345 f), (nb068AlphaDummy344, nb068AlphaDummy346 f), (nb068AlphaDummy369, nb068AlphaDummy370 f), (nb068AlphaDummy367, nb068AlphaDummy368 f), (nb068AlphaDummy336, nb068AlphaDummy338 f), (nb068AlphaDummy335, nb068AlphaDummy337 f), (nb068AlphaDummy365, nb068AlphaDummy366 f), (nb068AlphaDummy339, nb068AlphaDummy340 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy343) (SemanticCore.Class.cv nb068AlphaDummy336)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy344) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy343) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy343) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy343))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy345 f)) (SemanticCore.Class.cv (nb068AlphaDummy338 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy346 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy345 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy345 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy345 f)))).neg)

        Checked nominal proof certificate identified upstream as nb068_split_alpha_0092.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0093 (x y f : SemanticCore.Var) :
          Nominal.TAlphaWff [(nb068AlphaDummy365, nb068AlphaDummy366 f), (nb068AlphaDummy339, nb068AlphaDummy340 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy365) (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy328) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy365) (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy328) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy366 f)) (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy366 f)) (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

          Checked nominal proof certificate identified upstream as nb068_split_alpha_0093.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0094 (x y f : SemanticCore.Var) :
            Nominal.TAlphaWff [(nb068AlphaDummy387, nb068AlphaDummy390 f), (nb068AlphaDummy386, nb068AlphaDummy389 f), (nb068AlphaDummy385, nb068AlphaDummy388 f), (nb068AlphaDummy383, nb068AlphaDummy384 f), (nb068AlphaDummy379, nb068AlphaDummy381 f), (nb068AlphaDummy380, nb068AlphaDummy382 f), (nb068AlphaDummy372, nb068AlphaDummy374 f), (nb068AlphaDummy371, nb068AlphaDummy373 f), (nb068AlphaDummy377, nb068AlphaDummy378 f), (nb068AlphaDummy375, nb068AlphaDummy376 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy386) (SemanticCore.Class.cv nb068AlphaDummy387)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy385) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy386) (SemanticCore.Class.cv nb068AlphaDummy387))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy389 f)) (SemanticCore.Class.cv (nb068AlphaDummy390 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy388 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy389 f)) (SemanticCore.Class.cv (nb068AlphaDummy390 f)))).neg)

            Checked nominal proof certificate identified upstream as nb068_split_alpha_0094.

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

              Certificates from NAR4C068C001Part039.

              source
              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0095 (x y f : SemanticCore.Var) :
              Nominal.TAlphaWff [(nb068AlphaDummy379, nb068AlphaDummy381 f), (nb068AlphaDummy380, nb068AlphaDummy382 f), (nb068AlphaDummy372, nb068AlphaDummy374 f), (nb068AlphaDummy371, nb068AlphaDummy373 f), (nb068AlphaDummy377, nb068AlphaDummy378 f), (nb068AlphaDummy375, nb068AlphaDummy376 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy379) (SemanticCore.Class.cv nb068AlphaDummy372)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy380) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy379) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy379) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy379))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy381 f)) (SemanticCore.Class.cv (nb068AlphaDummy374 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy382 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy381 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy381 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy381 f)))).neg)

              Checked nominal proof certificate identified upstream as nb068_split_alpha_0095.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0096 (x y f : SemanticCore.Var) :
                Nominal.TAlphaWff [(nb068AlphaDummy387, nb068AlphaDummy390 f), (nb068AlphaDummy386, nb068AlphaDummy389 f), (nb068AlphaDummy385, nb068AlphaDummy388 f), (nb068AlphaDummy383, nb068AlphaDummy384 f), (nb068AlphaDummy379, nb068AlphaDummy381 f), (nb068AlphaDummy380, nb068AlphaDummy382 f), (nb068AlphaDummy405, nb068AlphaDummy406 f), (nb068AlphaDummy403, nb068AlphaDummy404 f), (nb068AlphaDummy372, nb068AlphaDummy374 f), (nb068AlphaDummy371, nb068AlphaDummy373 f), (nb068AlphaDummy401, nb068AlphaDummy402 f), (nb068AlphaDummy375, nb068AlphaDummy376 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy386) (SemanticCore.Class.cv nb068AlphaDummy387)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy385) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy386) (SemanticCore.Class.cv nb068AlphaDummy387))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy389 f)) (SemanticCore.Class.cv (nb068AlphaDummy390 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy388 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy389 f)) (SemanticCore.Class.cv (nb068AlphaDummy390 f)))).neg)

                Checked nominal proof certificate identified upstream as nb068_split_alpha_0096.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0097 (x y f : SemanticCore.Var) :
                  Nominal.TAlphaWff [(nb068AlphaDummy379, nb068AlphaDummy381 f), (nb068AlphaDummy380, nb068AlphaDummy382 f), (nb068AlphaDummy405, nb068AlphaDummy406 f), (nb068AlphaDummy403, nb068AlphaDummy404 f), (nb068AlphaDummy372, nb068AlphaDummy374 f), (nb068AlphaDummy371, nb068AlphaDummy373 f), (nb068AlphaDummy401, nb068AlphaDummy402 f), (nb068AlphaDummy375, nb068AlphaDummy376 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy379) (SemanticCore.Class.cv nb068AlphaDummy372)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy380) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy379) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy379) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy379))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy381 f)) (SemanticCore.Class.cv (nb068AlphaDummy374 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy382 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy381 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy381 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy381 f)))).neg)

                  Checked nominal proof certificate identified upstream as nb068_split_alpha_0097.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0098 (x y f : SemanticCore.Var) :
                    Nominal.TAlphaWff [(nb068AlphaDummy401, nb068AlphaDummy402 f), (nb068AlphaDummy375, nb068AlphaDummy376 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy401) (SemanticCore.Class.cab nb068AlphaDummy371 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy372 (SemanticCore.Class.cv nb068AlphaDummy329) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy371) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy401) (SemanticCore.Class.cab nb068AlphaDummy371 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy372 (SemanticCore.Class.cv nb068AlphaDummy329) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy371) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy402 f)) (SemanticCore.Class.cab (nb068AlphaDummy373 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy374 f) (SemanticCore.Class.cv (nb068AlphaDummy332 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy373 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy402 f)) (SemanticCore.Class.cab (nb068AlphaDummy373 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy374 f) (SemanticCore.Class.cv (nb068AlphaDummy332 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy373 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                    Checked nominal proof certificate identified upstream as nb068_split_alpha_0098.

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

                      Certificates from NAR4C068C001Part040.

                      source
                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0099 (x y f : SemanticCore.Var) :
                      Nominal.TAlphaWff [(nb068AlphaDummy429, nb068AlphaDummy432 f), (nb068AlphaDummy428, nb068AlphaDummy431 f), (nb068AlphaDummy427, nb068AlphaDummy430 f), (nb068AlphaDummy425, nb068AlphaDummy426 f), (nb068AlphaDummy421, nb068AlphaDummy423 f), (nb068AlphaDummy422, nb068AlphaDummy424 f), (nb068AlphaDummy414, nb068AlphaDummy416 f), (nb068AlphaDummy413, nb068AlphaDummy415 f), (nb068AlphaDummy419, nb068AlphaDummy420 f), (nb068AlphaDummy417, nb068AlphaDummy418 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy428) (SemanticCore.Class.cv nb068AlphaDummy429)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy427) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy428) (SemanticCore.Class.cv nb068AlphaDummy429))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy431 f)) (SemanticCore.Class.cv (nb068AlphaDummy432 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy430 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy431 f)) (SemanticCore.Class.cv (nb068AlphaDummy432 f)))).neg)

                      Checked nominal proof certificate identified upstream as nb068_split_alpha_0099.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0100 (x y f : SemanticCore.Var) :
                        Nominal.TAlphaWff [(nb068AlphaDummy421, nb068AlphaDummy423 f), (nb068AlphaDummy422, nb068AlphaDummy424 f), (nb068AlphaDummy414, nb068AlphaDummy416 f), (nb068AlphaDummy413, nb068AlphaDummy415 f), (nb068AlphaDummy419, nb068AlphaDummy420 f), (nb068AlphaDummy417, nb068AlphaDummy418 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy422) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy421) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy421) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy421))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy424 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy423 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy423 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy423 f))))

                        Checked nominal proof certificate identified upstream as nb068_split_alpha_0100.

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

                          Certificates from NAR4C068C001Part041.

                          source
                          noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0101 (x y f : SemanticCore.Var) :
                          Nominal.TAlphaWff [(nb068AlphaDummy429, nb068AlphaDummy432 f), (nb068AlphaDummy428, nb068AlphaDummy431 f), (nb068AlphaDummy427, nb068AlphaDummy430 f), (nb068AlphaDummy425, nb068AlphaDummy426 f), (nb068AlphaDummy421, nb068AlphaDummy423 f), (nb068AlphaDummy422, nb068AlphaDummy424 f), (nb068AlphaDummy447, nb068AlphaDummy448 f), (nb068AlphaDummy445, nb068AlphaDummy446 f), (nb068AlphaDummy414, nb068AlphaDummy416 f), (nb068AlphaDummy413, nb068AlphaDummy415 f), (nb068AlphaDummy443, nb068AlphaDummy444 f), (nb068AlphaDummy417, nb068AlphaDummy418 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy428) (SemanticCore.Class.cv nb068AlphaDummy429)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy427) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy428) (SemanticCore.Class.cv nb068AlphaDummy429))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy431 f)) (SemanticCore.Class.cv (nb068AlphaDummy432 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy430 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy431 f)) (SemanticCore.Class.cv (nb068AlphaDummy432 f)))).neg)

                          Checked nominal proof certificate identified upstream as nb068_split_alpha_0101.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0102 (x y f : SemanticCore.Var) :
                            Nominal.TAlphaWff [(nb068AlphaDummy425, nb068AlphaDummy426 f), (nb068AlphaDummy421, nb068AlphaDummy423 f), (nb068AlphaDummy422, nb068AlphaDummy424 f), (nb068AlphaDummy447, nb068AlphaDummy448 f), (nb068AlphaDummy445, nb068AlphaDummy446 f), (nb068AlphaDummy414, nb068AlphaDummy416 f), (nb068AlphaDummy413, nb068AlphaDummy415 f), (nb068AlphaDummy443, nb068AlphaDummy444 f), (nb068AlphaDummy417, nb068AlphaDummy418 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy425) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy421) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy421) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy425) (SemanticCore.Class.cv nb068AlphaDummy421)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy421) Compiler.CompactSourceSyntax.synCnnc).neg)) ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy426 f)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy423 f)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy423 f)) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy426 f)) (SemanticCore.Class.cv (nb068AlphaDummy423 f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy423 f)) Compiler.CompactSourceSyntax.synCnnc).neg))

                            Checked nominal proof certificate identified upstream as nb068_split_alpha_0102.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0103 (x y f : SemanticCore.Var) :
                              Nominal.TAlphaWff [(nb068AlphaDummy443, nb068AlphaDummy444 f), (nb068AlphaDummy417, nb068AlphaDummy418 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy443) (SemanticCore.Class.cab nb068AlphaDummy413 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy414 (SemanticCore.Class.cv nb068AlphaDummy408) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy413) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy443) (SemanticCore.Class.cab nb068AlphaDummy413 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy414 (SemanticCore.Class.cv nb068AlphaDummy408) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy413) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy444 f)) (SemanticCore.Class.cab (nb068AlphaDummy415 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy416 f) (SemanticCore.Class.cv (nb068AlphaDummy410 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy415 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy444 f)) (SemanticCore.Class.cab (nb068AlphaDummy415 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy416 f) (SemanticCore.Class.cv (nb068AlphaDummy410 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy415 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

                              Checked nominal proof certificate identified upstream as nb068_split_alpha_0103.

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

                                Certificates from NAR4C068C001Part042.

                                source
                                noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0104 (x y f : SemanticCore.Var) :
                                Nominal.TAlphaWff [(nb068AlphaDummy465, nb068AlphaDummy468 f), (nb068AlphaDummy464, nb068AlphaDummy467 f), (nb068AlphaDummy463, nb068AlphaDummy466 f), (nb068AlphaDummy461, nb068AlphaDummy462 f), (nb068AlphaDummy457, nb068AlphaDummy459 f), (nb068AlphaDummy458, nb068AlphaDummy460 f), (nb068AlphaDummy450, nb068AlphaDummy452 f), (nb068AlphaDummy449, nb068AlphaDummy451 f), (nb068AlphaDummy455, nb068AlphaDummy456 f), (nb068AlphaDummy453, nb068AlphaDummy454 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy464) (SemanticCore.Class.cv nb068AlphaDummy465)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy463) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy464) (SemanticCore.Class.cv nb068AlphaDummy465))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy467 f)) (SemanticCore.Class.cv (nb068AlphaDummy468 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy466 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy467 f)) (SemanticCore.Class.cv (nb068AlphaDummy468 f)))).neg)

                                Checked nominal proof certificate identified upstream as nb068_split_alpha_0104.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0105 (x y f : SemanticCore.Var) :
                                  Nominal.TAlphaWff [(nb068AlphaDummy457, nb068AlphaDummy459 f), (nb068AlphaDummy458, nb068AlphaDummy460 f), (nb068AlphaDummy450, nb068AlphaDummy452 f), (nb068AlphaDummy449, nb068AlphaDummy451 f), (nb068AlphaDummy455, nb068AlphaDummy456 f), (nb068AlphaDummy453, nb068AlphaDummy454 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy458) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy457) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy457) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy457))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy460 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy459 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy459 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy459 f))))

                                  Checked nominal proof certificate identified upstream as nb068_split_alpha_0105.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0106 (x y f : SemanticCore.Var) :
                                    Nominal.TAlphaWff [(nb068AlphaDummy465, nb068AlphaDummy468 f), (nb068AlphaDummy464, nb068AlphaDummy467 f), (nb068AlphaDummy463, nb068AlphaDummy466 f), (nb068AlphaDummy461, nb068AlphaDummy462 f), (nb068AlphaDummy457, nb068AlphaDummy459 f), (nb068AlphaDummy458, nb068AlphaDummy460 f), (nb068AlphaDummy483, nb068AlphaDummy484 f), (nb068AlphaDummy481, nb068AlphaDummy482 f), (nb068AlphaDummy450, nb068AlphaDummy452 f), (nb068AlphaDummy449, nb068AlphaDummy451 f), (nb068AlphaDummy479, nb068AlphaDummy480 f), (nb068AlphaDummy453, nb068AlphaDummy454 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy464) (SemanticCore.Class.cv nb068AlphaDummy465)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy463) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy464) (SemanticCore.Class.cv nb068AlphaDummy465))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy467 f)) (SemanticCore.Class.cv (nb068AlphaDummy468 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy466 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy467 f)) (SemanticCore.Class.cv (nb068AlphaDummy468 f)))).neg)

                                    Checked nominal proof certificate identified upstream as nb068_split_alpha_0106.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0107 (x y f : SemanticCore.Var) :
                                      Nominal.TAlphaWff [(nb068AlphaDummy461, nb068AlphaDummy462 f), (nb068AlphaDummy457, nb068AlphaDummy459 f), (nb068AlphaDummy458, nb068AlphaDummy460 f), (nb068AlphaDummy483, nb068AlphaDummy484 f), (nb068AlphaDummy481, nb068AlphaDummy482 f), (nb068AlphaDummy450, nb068AlphaDummy452 f), (nb068AlphaDummy449, nb068AlphaDummy451 f), (nb068AlphaDummy479, nb068AlphaDummy480 f), (nb068AlphaDummy453, nb068AlphaDummy454 f), (nb068AlphaDummy408, nb068AlphaDummy410 f), (nb068AlphaDummy407, nb068AlphaDummy409 f), (nb068AlphaDummy411, nb068AlphaDummy412 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy325, nb068AlphaDummy326 f), (nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy461) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy457) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy457) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy461) (SemanticCore.Class.cv nb068AlphaDummy457)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy457) Compiler.CompactSourceSyntax.synCnnc).neg)) ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy462 f)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy459 f)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy459 f)) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy462 f)) (SemanticCore.Class.cv (nb068AlphaDummy459 f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy459 f)) Compiler.CompactSourceSyntax.synCnnc).neg))

                                      Checked nominal proof certificate identified upstream as nb068_split_alpha_0107.

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