Nominal proof certificates grouped in dependency order.

Certificates from NAR4C067C001Part031.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0077 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(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.classMem (SemanticCore.Class.cv nb067AlphaDummy213) (SemanticCore.Class.cv nb067AlphaDummy206)).imp (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))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy215 f)) (SemanticCore.Class.cv (nb067AlphaDummy208 f))).imp (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)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0077.

Equations

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

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0079 (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), (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 nb067AlphaDummy213) (SemanticCore.Class.cv nb067AlphaDummy206)).imp (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))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy215 f)) (SemanticCore.Class.cv (nb067AlphaDummy208 f))).imp (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)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0079.

Equations

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

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

Equations

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

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

Equations

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

Certificates from NAR4C067C001Part032.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0082 (x y f : SemanticCore.Var) (dv_f_y : f ≠ y) : Nominal.TAlphaWff [(nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv nb067AlphaDummy000)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy002)).neg) ((Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f)).imp (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCdm (SemanticCore.Class.cv f)) (SemanticCore.Class.cv y)).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0082.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0083 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy341, nb067AlphaDummy344 f), (nb067AlphaDummy340, nb067AlphaDummy343 f), (nb067AlphaDummy339, nb067AlphaDummy342 f), (nb067AlphaDummy337, nb067AlphaDummy338 f), (nb067AlphaDummy333, nb067AlphaDummy335 f), (nb067AlphaDummy334, nb067AlphaDummy336 f), (nb067AlphaDummy326, nb067AlphaDummy328 f), (nb067AlphaDummy325, nb067AlphaDummy327 f), (nb067AlphaDummy331, nb067AlphaDummy332 f), (nb067AlphaDummy329, nb067AlphaDummy330 f), (nb067AlphaDummy322, nb067AlphaDummy324 f), (nb067AlphaDummy321, nb067AlphaDummy323 f), (nb067AlphaDummy319, nb067AlphaDummy320 x f), (nb067AlphaDummy317, nb067AlphaDummy318 x 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 nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy339) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy342 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0083.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0084 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy333, nb067AlphaDummy335 f), (nb067AlphaDummy334, nb067AlphaDummy336 f), (nb067AlphaDummy326, nb067AlphaDummy328 f), (nb067AlphaDummy325, nb067AlphaDummy327 f), (nb067AlphaDummy331, nb067AlphaDummy332 f), (nb067AlphaDummy329, nb067AlphaDummy330 f), (nb067AlphaDummy322, nb067AlphaDummy324 f), (nb067AlphaDummy321, nb067AlphaDummy323 f), (nb067AlphaDummy319, nb067AlphaDummy320 x f), (nb067AlphaDummy317, nb067AlphaDummy318 x 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 nb067AlphaDummy333) (SemanticCore.Class.cv nb067AlphaDummy326)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy334) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy333) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy333) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy333)))).neg (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy335 f)) (SemanticCore.Class.cv (nb067AlphaDummy328 f))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy336 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy335 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy335 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy335 f))))).neg

Checked nominal proof certificate identified upstream as nb067_split_alpha_0084.

Equations

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

Certificates from NAR4C067C001Part033.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0085 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy341, nb067AlphaDummy344 f), (nb067AlphaDummy340, nb067AlphaDummy343 f), (nb067AlphaDummy339, nb067AlphaDummy342 f), (nb067AlphaDummy337, nb067AlphaDummy338 f), (nb067AlphaDummy333, nb067AlphaDummy335 f), (nb067AlphaDummy334, nb067AlphaDummy336 f), (nb067AlphaDummy359, nb067AlphaDummy360 f), (nb067AlphaDummy357, nb067AlphaDummy358 f), (nb067AlphaDummy326, nb067AlphaDummy328 f), (nb067AlphaDummy325, nb067AlphaDummy327 f), (nb067AlphaDummy355, nb067AlphaDummy356 f), (nb067AlphaDummy329, nb067AlphaDummy330 f), (nb067AlphaDummy322, nb067AlphaDummy324 f), (nb067AlphaDummy321, nb067AlphaDummy323 f), (nb067AlphaDummy319, nb067AlphaDummy320 x f), (nb067AlphaDummy317, nb067AlphaDummy318 x 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 nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy339) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy342 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0085.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0086 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy333, nb067AlphaDummy335 f), (nb067AlphaDummy334, nb067AlphaDummy336 f), (nb067AlphaDummy359, nb067AlphaDummy360 f), (nb067AlphaDummy357, nb067AlphaDummy358 f), (nb067AlphaDummy326, nb067AlphaDummy328 f), (nb067AlphaDummy325, nb067AlphaDummy327 f), (nb067AlphaDummy355, nb067AlphaDummy356 f), (nb067AlphaDummy329, nb067AlphaDummy330 f), (nb067AlphaDummy322, nb067AlphaDummy324 f), (nb067AlphaDummy321, nb067AlphaDummy323 f), (nb067AlphaDummy319, nb067AlphaDummy320 x f), (nb067AlphaDummy317, nb067AlphaDummy318 x f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy333) (SemanticCore.Class.cv nb067AlphaDummy326)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy334) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy333) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy333) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy333))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy335 f)) (SemanticCore.Class.cv (nb067AlphaDummy328 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy336 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy335 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy335 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy335 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0086.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0087 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy355, nb067AlphaDummy356 f), (nb067AlphaDummy329, nb067AlphaDummy330 f), (nb067AlphaDummy322, nb067AlphaDummy324 f), (nb067AlphaDummy321, nb067AlphaDummy323 f), (nb067AlphaDummy319, nb067AlphaDummy320 x f), (nb067AlphaDummy317, nb067AlphaDummy318 x f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy355) (SemanticCore.Class.cab nb067AlphaDummy325 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy326 (SemanticCore.Class.cv nb067AlphaDummy321) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy325) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy355) (SemanticCore.Class.cab nb067AlphaDummy325 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy326 (SemanticCore.Class.cv nb067AlphaDummy321) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy325) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy356 f)) (SemanticCore.Class.cab (nb067AlphaDummy327 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy328 f) (SemanticCore.Class.cv (nb067AlphaDummy323 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy327 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy356 f)) (SemanticCore.Class.cab (nb067AlphaDummy327 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy328 f) (SemanticCore.Class.cv (nb067AlphaDummy323 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy327 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0087.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0088 (x y f : SemanticCore.Var) (dv_f_x : f ≠ x) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb067AlphaDummy319, nb067AlphaDummy320 x f), (nb067AlphaDummy317, nb067AlphaDummy318 x f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy319) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb067AlphaDummy000))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy319) (SemanticCore.Class.cv nb067AlphaDummy001)).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy320 x f)) (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy320 x f)) (SemanticCore.Class.cv x)).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0088.

Equations

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

Certificates from NAR4C067C001Part034.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0089 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy341, nb067AlphaDummy344 f), (nb067AlphaDummy340, nb067AlphaDummy343 f), (nb067AlphaDummy339, nb067AlphaDummy342 f), (nb067AlphaDummy337, nb067AlphaDummy338 f), (nb067AlphaDummy333, nb067AlphaDummy335 f), (nb067AlphaDummy334, nb067AlphaDummy336 f), (nb067AlphaDummy326, nb067AlphaDummy328 f), (nb067AlphaDummy325, nb067AlphaDummy327 f), (nb067AlphaDummy331, nb067AlphaDummy332 f), (nb067AlphaDummy329, nb067AlphaDummy330 f), (nb067AlphaDummy322, nb067AlphaDummy324 f), (nb067AlphaDummy321, nb067AlphaDummy323 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 nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy339) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy342 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0089.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0090 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy326, nb067AlphaDummy328 f), (nb067AlphaDummy325, nb067AlphaDummy327 f), (nb067AlphaDummy331, nb067AlphaDummy332 f), (nb067AlphaDummy329, nb067AlphaDummy330 f), (nb067AlphaDummy322, nb067AlphaDummy324 f), (nb067AlphaDummy321, nb067AlphaDummy323 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy325) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy327 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))))

Checked nominal proof certificate identified upstream as nb067_split_alpha_0090.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0091 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy341, nb067AlphaDummy344 f), (nb067AlphaDummy340, nb067AlphaDummy343 f), (nb067AlphaDummy339, nb067AlphaDummy342 f), (nb067AlphaDummy337, nb067AlphaDummy338 f), (nb067AlphaDummy333, nb067AlphaDummy335 f), (nb067AlphaDummy334, nb067AlphaDummy336 f), (nb067AlphaDummy359, nb067AlphaDummy360 f), (nb067AlphaDummy357, nb067AlphaDummy358 f), (nb067AlphaDummy326, nb067AlphaDummy328 f), (nb067AlphaDummy325, nb067AlphaDummy327 f), (nb067AlphaDummy355, nb067AlphaDummy356 f), (nb067AlphaDummy329, nb067AlphaDummy330 f), (nb067AlphaDummy322, nb067AlphaDummy324 f), (nb067AlphaDummy321, nb067AlphaDummy323 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 nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy339) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy342 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0091.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0092 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy333, nb067AlphaDummy335 f), (nb067AlphaDummy334, nb067AlphaDummy336 f), (nb067AlphaDummy359, nb067AlphaDummy360 f), (nb067AlphaDummy357, nb067AlphaDummy358 f), (nb067AlphaDummy326, nb067AlphaDummy328 f), (nb067AlphaDummy325, nb067AlphaDummy327 f), (nb067AlphaDummy355, nb067AlphaDummy356 f), (nb067AlphaDummy329, nb067AlphaDummy330 f), (nb067AlphaDummy322, nb067AlphaDummy324 f), (nb067AlphaDummy321, nb067AlphaDummy323 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy333) (SemanticCore.Class.cv nb067AlphaDummy326)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy334) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy333) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy333) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy333))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy335 f)) (SemanticCore.Class.cv (nb067AlphaDummy328 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy336 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy335 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy335 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy335 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0092.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0093 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy355, nb067AlphaDummy356 f), (nb067AlphaDummy329, nb067AlphaDummy330 f), (nb067AlphaDummy322, nb067AlphaDummy324 f), (nb067AlphaDummy321, nb067AlphaDummy323 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy355) (SemanticCore.Class.cab nb067AlphaDummy325 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy326 (SemanticCore.Class.cv nb067AlphaDummy321) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy325) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy355) (SemanticCore.Class.cab nb067AlphaDummy325 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy326 (SemanticCore.Class.cv nb067AlphaDummy321) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy325) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy356 f)) (SemanticCore.Class.cab (nb067AlphaDummy327 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy328 f) (SemanticCore.Class.cv (nb067AlphaDummy323 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy327 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy356 f)) (SemanticCore.Class.cab (nb067AlphaDummy327 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy328 f) (SemanticCore.Class.cv (nb067AlphaDummy323 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy327 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0093.

Equations

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

Certificates from NAR4C067C001Part035.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0094 (x y f : SemanticCore.Var) (dv_f_x : f ≠ x) (dv_f_y : f ≠ y) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy005) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy001) (SemanticCore.Class.cv nb067AlphaDummy002)) (SemanticCore.Class.cv nb067AlphaDummy003))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy001) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy002) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy003) (SemanticCore.Class.cab nb067AlphaDummy000 (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy002) (SemanticCore.Class.cv nb067AlphaDummy001))))).neg) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy006 x y f)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy004 x y f)) (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv y) (SemanticCore.Class.cv x))))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0094.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfMap (x y f : SemanticCore.Var) (dv_f_x : f ≠ x) (dv_f_y : f ≠ y) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCmap (Compiler.CompactSourceSyntax.synCmpt2 x Compiler.CompactSourceSyntax.synCvv y Compiler.CompactSourceSyntax.synCvv (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWf (SemanticCore.Class.cv f) (SemanticCore.Class.cv y) (SemanticCore.Class.cv x)))))

Checked nominal proof certificate identified upstream as nominal_df_map.

Equations

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