Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part055.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0158 (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), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy457) (SemanticCore.Class.cv nb068AlphaDummy450)).imp (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))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy459 f)) (SemanticCore.Class.cv (nb068AlphaDummy452 f))).imp (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)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0158.

Equations

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

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

Equations

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

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0161 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(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), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy479) (SemanticCore.Class.cab nb068AlphaDummy449 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy450 (SemanticCore.Class.cv nb068AlphaDummy407) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy449) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy479) (SemanticCore.Class.cab nb068AlphaDummy449 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy450 (SemanticCore.Class.cv nb068AlphaDummy407) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy449) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy480 f)) (SemanticCore.Class.cab (nb068AlphaDummy451 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy452 f) (SemanticCore.Class.cv (nb068AlphaDummy409 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy451 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy480 f)) (SemanticCore.Class.cab (nb068AlphaDummy451 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy452 f) (SemanticCore.Class.cv (nb068AlphaDummy409 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy451 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0161.

Equations

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

Certificates from NAR4C068C001Part056.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0162 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy147, nb068AlphaDummy150 f), (nb068AlphaDummy146, nb068AlphaDummy149 f), (nb068AlphaDummy145, nb068AlphaDummy148 f), (nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy137, nb068AlphaDummy138 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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 nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy145) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy148 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0162.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0163 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy137, nb068AlphaDummy138 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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 nb068AlphaDummy140) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy139))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy142 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy141 f))))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0163.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0164 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy147, nb068AlphaDummy150 f), (nb068AlphaDummy146, nb068AlphaDummy149 f), (nb068AlphaDummy145, nb068AlphaDummy148 f), (nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy165, nb068AlphaDummy166 f), (nb068AlphaDummy163, nb068AlphaDummy164 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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 nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy145) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy148 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0164.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0165 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy165, nb068AlphaDummy166 f), (nb068AlphaDummy163, nb068AlphaDummy164 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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)] ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy143) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy143) (SemanticCore.Class.cv nb068AlphaDummy139)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc).neg)) ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy144 f)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy144 f)) (SemanticCore.Class.cv (nb068AlphaDummy141 f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synCnnc).neg))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0165.

Equations

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

Certificates from NAR4C068C001Part057.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0166 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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 nb068AlphaDummy161) (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy161) (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy162 f)) (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy162 f)) (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0166.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0167 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy183, nb068AlphaDummy186 f), (nb068AlphaDummy182, nb068AlphaDummy185 f), (nb068AlphaDummy181, nb068AlphaDummy184 f), (nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy173, nb068AlphaDummy174 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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 nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy181) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy184 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0167.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0168 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy173, nb068AlphaDummy174 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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 nb068AlphaDummy176) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy175))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy178 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy177 f))))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0168.

Equations

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

Certificates from NAR4C068C001Part058.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0169 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy183, nb068AlphaDummy186 f), (nb068AlphaDummy182, nb068AlphaDummy185 f), (nb068AlphaDummy181, nb068AlphaDummy184 f), (nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy201, nb068AlphaDummy202 f), (nb068AlphaDummy199, nb068AlphaDummy200 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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 nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy181) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy184 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0169.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0170 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy201, nb068AlphaDummy202 f), (nb068AlphaDummy199, nb068AlphaDummy200 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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)] ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy179) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy179) (SemanticCore.Class.cv nb068AlphaDummy175)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc).neg)) ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy180 f)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy180 f)) (SemanticCore.Class.cv (nb068AlphaDummy177 f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synCnnc).neg))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0170.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0171 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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)] (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy168) (SemanticCore.Class.cv nb068AlphaDummy125)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy167) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy168)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))).neg (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy170 f)) (SemanticCore.Class.cv (nb068AlphaDummy127 f))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy169 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy170 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))).neg

Checked nominal proof certificate identified upstream as nb068_split_alpha_0171.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0172 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Class.cv nb068AlphaDummy125)) (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Class.cv (nb068AlphaDummy127 f))) (SemanticCore.Class.cv f))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0172.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0173 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 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.all nb068AlphaDummy126 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy129) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb068AlphaDummy125) (SemanticCore.Class.cv nb068AlphaDummy126))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Class.cv nb068AlphaDummy000) (SemanticCore.Class.cv nb068AlphaDummy125))).neg) (SemanticCore.Wff.all (nb068AlphaDummy128 f) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy130 f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb068AlphaDummy127 f)) (SemanticCore.Class.cv (nb068AlphaDummy128 f)))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb068AlphaDummy127 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0173.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0174 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(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 nb068AlphaDummy411) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb068AlphaDummy407) (SemanticCore.Class.cv nb068AlphaDummy408))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb068AlphaDummy408) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000)) (SemanticCore.Class.cv nb068AlphaDummy407)).neg) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy412 f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb068AlphaDummy409 f)) (SemanticCore.Class.cv (nb068AlphaDummy410 f)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb068AlphaDummy410 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb068AlphaDummy409 f))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0174.

Equations

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