Nominal proof certificates grouped in dependency order.

Certificates from NAR4C067C001Part026.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0057 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy213, nb067AlphaDummy215 f), (nb067AlphaDummy214, nb067AlphaDummy216 f), (nb067AlphaDummy239, nb067AlphaDummy240 f), (nb067AlphaDummy237, nb067AlphaDummy238 f), (nb067AlphaDummy206, nb067AlphaDummy208 f), (nb067AlphaDummy205, nb067AlphaDummy207 f), (nb067AlphaDummy235, nb067AlphaDummy236 f), (nb067AlphaDummy209, nb067AlphaDummy210 f), (nb067AlphaDummy164, nb067AlphaDummy166 f), (nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy214) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy213) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy213) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy213))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy216 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy215 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy215 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy215 f))))

Checked nominal proof certificate identified upstream as nb067_split_alpha_0057.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0058 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy235, nb067AlphaDummy236 f), (nb067AlphaDummy209, nb067AlphaDummy210 f), (nb067AlphaDummy164, nb067AlphaDummy166 f), (nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy235) (SemanticCore.Class.cab nb067AlphaDummy205 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy206 (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy205) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy235) (SemanticCore.Class.cab nb067AlphaDummy205 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy206 (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy205) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy206)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy236 f)) (SemanticCore.Class.cab (nb067AlphaDummy207 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy208 f) (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy207 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy236 f)) (SemanticCore.Class.cab (nb067AlphaDummy207 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy208 f) (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy207 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy208 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0058.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0059 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy164, nb067AlphaDummy166 f), (nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy167) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Class.cv nb067AlphaDummy164))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy163)).neg) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Class.cv (nb067AlphaDummy166 f)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb067AlphaDummy165 f))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0059.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0060 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy257, nb067AlphaDummy260 f), (nb067AlphaDummy256, nb067AlphaDummy259 f), (nb067AlphaDummy255, nb067AlphaDummy258 f), (nb067AlphaDummy253, nb067AlphaDummy254 f), (nb067AlphaDummy249, nb067AlphaDummy251 f), (nb067AlphaDummy250, nb067AlphaDummy252 f), (nb067AlphaDummy242, nb067AlphaDummy244 f), (nb067AlphaDummy241, nb067AlphaDummy243 f), (nb067AlphaDummy247, nb067AlphaDummy248 f), (nb067AlphaDummy245, nb067AlphaDummy246 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb067AlphaDummy256) (SemanticCore.Class.cv nb067AlphaDummy257)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy255) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy256) (SemanticCore.Class.cv nb067AlphaDummy257))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy259 f)) (SemanticCore.Class.cv (nb067AlphaDummy260 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy258 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy259 f)) (SemanticCore.Class.cv (nb067AlphaDummy260 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0060.

Equations

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

Certificates from NAR4C067C001Part027.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0061 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy249, nb067AlphaDummy251 f), (nb067AlphaDummy250, nb067AlphaDummy252 f), (nb067AlphaDummy242, nb067AlphaDummy244 f), (nb067AlphaDummy241, nb067AlphaDummy243 f), (nb067AlphaDummy247, nb067AlphaDummy248 f), (nb067AlphaDummy245, nb067AlphaDummy246 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy249) (SemanticCore.Class.cv nb067AlphaDummy242)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy250) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy249) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy249) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy249)))).neg (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy251 f)) (SemanticCore.Class.cv (nb067AlphaDummy244 f))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy252 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy251 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy251 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy251 f))))).neg

Checked nominal proof certificate identified upstream as nb067_split_alpha_0061.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0062 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy257, nb067AlphaDummy260 f), (nb067AlphaDummy256, nb067AlphaDummy259 f), (nb067AlphaDummy255, nb067AlphaDummy258 f), (nb067AlphaDummy253, nb067AlphaDummy254 f), (nb067AlphaDummy249, nb067AlphaDummy251 f), (nb067AlphaDummy250, nb067AlphaDummy252 f), (nb067AlphaDummy275, nb067AlphaDummy276 f), (nb067AlphaDummy273, nb067AlphaDummy274 f), (nb067AlphaDummy242, nb067AlphaDummy244 f), (nb067AlphaDummy241, nb067AlphaDummy243 f), (nb067AlphaDummy271, nb067AlphaDummy272 f), (nb067AlphaDummy245, nb067AlphaDummy246 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb067AlphaDummy256) (SemanticCore.Class.cv nb067AlphaDummy257)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy255) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy256) (SemanticCore.Class.cv nb067AlphaDummy257))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy259 f)) (SemanticCore.Class.cv (nb067AlphaDummy260 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy258 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy259 f)) (SemanticCore.Class.cv (nb067AlphaDummy260 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0062.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0063 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy249, nb067AlphaDummy251 f), (nb067AlphaDummy250, nb067AlphaDummy252 f), (nb067AlphaDummy275, nb067AlphaDummy276 f), (nb067AlphaDummy273, nb067AlphaDummy274 f), (nb067AlphaDummy242, nb067AlphaDummy244 f), (nb067AlphaDummy241, nb067AlphaDummy243 f), (nb067AlphaDummy271, nb067AlphaDummy272 f), (nb067AlphaDummy245, nb067AlphaDummy246 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy249) (SemanticCore.Class.cv nb067AlphaDummy242)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy250) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy249) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy249) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy249))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy251 f)) (SemanticCore.Class.cv (nb067AlphaDummy244 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy252 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy251 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy251 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy251 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0063.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0064 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy271, nb067AlphaDummy272 f), (nb067AlphaDummy245, nb067AlphaDummy246 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy271) (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy271) (SemanticCore.Class.cab nb067AlphaDummy241 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy242 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy241) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy242)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy272 f)) (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy272 f)) (SemanticCore.Class.cab (nb067AlphaDummy243 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy244 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy243 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy244 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0064.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0065 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy083) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy085)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy084)).neg) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy086 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb067AlphaDummy088 f))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb067AlphaDummy087 f))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0065.

Equations

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

Certificates from NAR4C067C001Part028.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0066 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy297, nb067AlphaDummy300 f), (nb067AlphaDummy296, nb067AlphaDummy299 f), (nb067AlphaDummy295, nb067AlphaDummy298 f), (nb067AlphaDummy293, nb067AlphaDummy294 f), (nb067AlphaDummy289, nb067AlphaDummy291 f), (nb067AlphaDummy290, nb067AlphaDummy292 f), (nb067AlphaDummy282, nb067AlphaDummy284 f), (nb067AlphaDummy281, nb067AlphaDummy283 f), (nb067AlphaDummy287, nb067AlphaDummy288 f), (nb067AlphaDummy285, nb067AlphaDummy286 f), (nb067AlphaDummy278, nb067AlphaDummy280 f), (nb067AlphaDummy277, nb067AlphaDummy279 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb067AlphaDummy296) (SemanticCore.Class.cv nb067AlphaDummy297)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy295) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy296) (SemanticCore.Class.cv nb067AlphaDummy297))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy299 f)) (SemanticCore.Class.cv (nb067AlphaDummy300 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy298 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy299 f)) (SemanticCore.Class.cv (nb067AlphaDummy300 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0066.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0067 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy282, nb067AlphaDummy284 f), (nb067AlphaDummy281, nb067AlphaDummy283 f), (nb067AlphaDummy287, nb067AlphaDummy288 f), (nb067AlphaDummy285, nb067AlphaDummy286 f), (nb067AlphaDummy278, nb067AlphaDummy280 f), (nb067AlphaDummy277, nb067AlphaDummy279 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy281) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy283 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f))))

Checked nominal proof certificate identified upstream as nb067_split_alpha_0067.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0068 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy297, nb067AlphaDummy300 f), (nb067AlphaDummy296, nb067AlphaDummy299 f), (nb067AlphaDummy295, nb067AlphaDummy298 f), (nb067AlphaDummy293, nb067AlphaDummy294 f), (nb067AlphaDummy289, nb067AlphaDummy291 f), (nb067AlphaDummy290, nb067AlphaDummy292 f), (nb067AlphaDummy315, nb067AlphaDummy316 f), (nb067AlphaDummy313, nb067AlphaDummy314 f), (nb067AlphaDummy282, nb067AlphaDummy284 f), (nb067AlphaDummy281, nb067AlphaDummy283 f), (nb067AlphaDummy311, nb067AlphaDummy312 f), (nb067AlphaDummy285, nb067AlphaDummy286 f), (nb067AlphaDummy278, nb067AlphaDummy280 f), (nb067AlphaDummy277, nb067AlphaDummy279 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb067AlphaDummy296) (SemanticCore.Class.cv nb067AlphaDummy297)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy295) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy296) (SemanticCore.Class.cv nb067AlphaDummy297))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy299 f)) (SemanticCore.Class.cv (nb067AlphaDummy300 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy298 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy299 f)) (SemanticCore.Class.cv (nb067AlphaDummy300 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0068.

Equations

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

Certificates from NAR4C067C001Part029.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0069 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy289, nb067AlphaDummy291 f), (nb067AlphaDummy290, nb067AlphaDummy292 f), (nb067AlphaDummy315, nb067AlphaDummy316 f), (nb067AlphaDummy313, nb067AlphaDummy314 f), (nb067AlphaDummy282, nb067AlphaDummy284 f), (nb067AlphaDummy281, nb067AlphaDummy283 f), (nb067AlphaDummy311, nb067AlphaDummy312 f), (nb067AlphaDummy285, nb067AlphaDummy286 f), (nb067AlphaDummy278, nb067AlphaDummy280 f), (nb067AlphaDummy277, nb067AlphaDummy279 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy289) (SemanticCore.Class.cv nb067AlphaDummy282)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy290) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy289) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy289) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy289))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy291 f)) (SemanticCore.Class.cv (nb067AlphaDummy284 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy292 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy291 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy291 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy291 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0069.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0070 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy311, nb067AlphaDummy312 f), (nb067AlphaDummy285, nb067AlphaDummy286 f), (nb067AlphaDummy278, nb067AlphaDummy280 f), (nb067AlphaDummy277, nb067AlphaDummy279 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy311) (SemanticCore.Class.cab nb067AlphaDummy281 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy282 (SemanticCore.Class.cv nb067AlphaDummy277) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy281) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy311) (SemanticCore.Class.cab nb067AlphaDummy281 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy282 (SemanticCore.Class.cv nb067AlphaDummy277) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy281) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy312 f)) (SemanticCore.Class.cab (nb067AlphaDummy283 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy284 f) (SemanticCore.Class.cv (nb067AlphaDummy279 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy283 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy312 f)) (SemanticCore.Class.cab (nb067AlphaDummy283 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy284 f) (SemanticCore.Class.cv (nb067AlphaDummy279 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy283 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0070.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0071 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy185, nb067AlphaDummy188 f), (nb067AlphaDummy184, nb067AlphaDummy187 f), (nb067AlphaDummy183, nb067AlphaDummy186 f), (nb067AlphaDummy181, nb067AlphaDummy182 f), (nb067AlphaDummy177, nb067AlphaDummy179 f), (nb067AlphaDummy178, nb067AlphaDummy180 f), (nb067AlphaDummy170, nb067AlphaDummy172 f), (nb067AlphaDummy169, nb067AlphaDummy171 f), (nb067AlphaDummy175, nb067AlphaDummy176 f), (nb067AlphaDummy173, nb067AlphaDummy174 f), (nb067AlphaDummy164, nb067AlphaDummy166 f), (nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy278, nb067AlphaDummy280 f), (nb067AlphaDummy277, nb067AlphaDummy279 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb067AlphaDummy184) (SemanticCore.Class.cv nb067AlphaDummy185)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy183) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy184) (SemanticCore.Class.cv nb067AlphaDummy185))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy187 f)) (SemanticCore.Class.cv (nb067AlphaDummy188 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy186 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy187 f)) (SemanticCore.Class.cv (nb067AlphaDummy188 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0071.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0072 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy177, nb067AlphaDummy179 f), (nb067AlphaDummy178, nb067AlphaDummy180 f), (nb067AlphaDummy170, nb067AlphaDummy172 f), (nb067AlphaDummy169, nb067AlphaDummy171 f), (nb067AlphaDummy175, nb067AlphaDummy176 f), (nb067AlphaDummy173, nb067AlphaDummy174 f), (nb067AlphaDummy164, nb067AlphaDummy166 f), (nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy278, nb067AlphaDummy280 f), (nb067AlphaDummy277, nb067AlphaDummy279 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy177) (SemanticCore.Class.cv nb067AlphaDummy170)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy178) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy177) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy177) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy177))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy179 f)) (SemanticCore.Class.cv (nb067AlphaDummy172 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy180 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy179 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy179 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy179 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0072.

Equations

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

Certificates from NAR4C067C001Part030.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0073 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy185, nb067AlphaDummy188 f), (nb067AlphaDummy184, nb067AlphaDummy187 f), (nb067AlphaDummy183, nb067AlphaDummy186 f), (nb067AlphaDummy181, nb067AlphaDummy182 f), (nb067AlphaDummy177, nb067AlphaDummy179 f), (nb067AlphaDummy178, nb067AlphaDummy180 f), (nb067AlphaDummy203, nb067AlphaDummy204 f), (nb067AlphaDummy201, nb067AlphaDummy202 f), (nb067AlphaDummy170, nb067AlphaDummy172 f), (nb067AlphaDummy169, nb067AlphaDummy171 f), (nb067AlphaDummy199, nb067AlphaDummy200 f), (nb067AlphaDummy173, nb067AlphaDummy174 f), (nb067AlphaDummy164, nb067AlphaDummy166 f), (nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy278, nb067AlphaDummy280 f), (nb067AlphaDummy277, nb067AlphaDummy279 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb067AlphaDummy184) (SemanticCore.Class.cv nb067AlphaDummy185)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy183) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy184) (SemanticCore.Class.cv nb067AlphaDummy185))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy187 f)) (SemanticCore.Class.cv (nb067AlphaDummy188 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy186 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy187 f)) (SemanticCore.Class.cv (nb067AlphaDummy188 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0073.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0074 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy177, nb067AlphaDummy179 f), (nb067AlphaDummy178, nb067AlphaDummy180 f), (nb067AlphaDummy203, nb067AlphaDummy204 f), (nb067AlphaDummy201, nb067AlphaDummy202 f), (nb067AlphaDummy170, nb067AlphaDummy172 f), (nb067AlphaDummy169, nb067AlphaDummy171 f), (nb067AlphaDummy199, nb067AlphaDummy200 f), (nb067AlphaDummy173, nb067AlphaDummy174 f), (nb067AlphaDummy164, nb067AlphaDummy166 f), (nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy278, nb067AlphaDummy280 f), (nb067AlphaDummy277, nb067AlphaDummy279 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy177) (SemanticCore.Class.cv nb067AlphaDummy170)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy178) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy177) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy177) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy177))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy179 f)) (SemanticCore.Class.cv (nb067AlphaDummy172 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy180 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy179 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy179 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy179 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0074.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0075 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy199, nb067AlphaDummy200 f), (nb067AlphaDummy173, nb067AlphaDummy174 f), (nb067AlphaDummy164, nb067AlphaDummy166 f), (nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy278, nb067AlphaDummy280 f), (nb067AlphaDummy277, nb067AlphaDummy279 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy199) (SemanticCore.Class.cab nb067AlphaDummy169 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy170 (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy169) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy199) (SemanticCore.Class.cab nb067AlphaDummy169 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy170 (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy169) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy170)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy200 f)) (SemanticCore.Class.cab (nb067AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy172 f) (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy200 f)) (SemanticCore.Class.cab (nb067AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy172 f) (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy172 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0075.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0076 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy221, nb067AlphaDummy224 f), (nb067AlphaDummy220, nb067AlphaDummy223 f), (nb067AlphaDummy219, nb067AlphaDummy222 f), (nb067AlphaDummy217, nb067AlphaDummy218 f), (nb067AlphaDummy213, nb067AlphaDummy215 f), (nb067AlphaDummy214, nb067AlphaDummy216 f), (nb067AlphaDummy206, nb067AlphaDummy208 f), (nb067AlphaDummy205, nb067AlphaDummy207 f), (nb067AlphaDummy211, nb067AlphaDummy212 f), (nb067AlphaDummy209, nb067AlphaDummy210 f), (nb067AlphaDummy164, nb067AlphaDummy166 f), (nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy278, nb067AlphaDummy280 f), (nb067AlphaDummy277, nb067AlphaDummy279 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb067AlphaDummy220) (SemanticCore.Class.cv nb067AlphaDummy221)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy219) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy220) (SemanticCore.Class.cv nb067AlphaDummy221))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy223 f)) (SemanticCore.Class.cv (nb067AlphaDummy224 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy222 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy223 f)) (SemanticCore.Class.cv (nb067AlphaDummy224 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0076.

Equations

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