Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part051.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0141 (x y f : SemanticCore.Var) : Nominal.TAlphaClass [(nb068AlphaDummy323, nb068AlphaDummy324 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Class.cab nb068AlphaDummy325 (Compiler.CompactSourceSyntax.synWnan (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy325) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy325) Compiler.CompactSourceSyntax.synCid))) (SemanticCore.Class.cab (nb068AlphaDummy326 f) (Compiler.CompactSourceSyntax.synWnan (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy326 f)) (Compiler.CompactSourceSyntax.synCcom (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy326 f)) Compiler.CompactSourceSyntax.synCid)))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0141.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0142 (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), (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_0142.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0143 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy336, nb068AlphaDummy338 f), (nb068AlphaDummy335, nb068AlphaDummy337 f), (nb068AlphaDummy341, nb068AlphaDummy342 f), (nb068AlphaDummy339, nb068AlphaDummy340 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0143.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0144 (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), (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_0144.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0145 (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), (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_0145.

Equations

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

Certificates from NAR4C068C001Part052.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0146 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy365, nb068AlphaDummy366 f), (nb068AlphaDummy339, nb068AlphaDummy340 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 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_0146.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0147 (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), (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_0147.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0148 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy372, nb068AlphaDummy374 f), (nb068AlphaDummy371, nb068AlphaDummy373 f), (nb068AlphaDummy377, nb068AlphaDummy378 f), (nb068AlphaDummy375, nb068AlphaDummy376 f), (nb068AlphaDummy329, nb068AlphaDummy332 f), (nb068AlphaDummy328, nb068AlphaDummy331 f), (nb068AlphaDummy327, nb068AlphaDummy330 f), (nb068AlphaDummy333, nb068AlphaDummy334 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy371) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy373 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0148.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0149 (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), (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_0149.

Equations

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

Certificates from NAR4C068C001Part053.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0150 (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), (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_0150.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0151 (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), (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_0151.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0152 (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), (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_0152.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0153 (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), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy421) (SemanticCore.Class.cv nb068AlphaDummy414)).imp (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))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy423 f)) (SemanticCore.Class.cv (nb068AlphaDummy416 f))).imp (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)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0153.

Equations

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

Certificates from NAR4C068C001Part054.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0154 (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), (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_0154.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0155 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(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), (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_0155.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0156 (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), (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_0156.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0157 (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), (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_0157.

Equations

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