Nominal proof certificates grouped in dependency order.

Certificates from NAR4C067C001Part013.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0010 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy107, nb067AlphaDummy110 f), (nb067AlphaDummy106, nb067AlphaDummy109 f), (nb067AlphaDummy105, nb067AlphaDummy108 f), (nb067AlphaDummy103, nb067AlphaDummy104 f), (nb067AlphaDummy099, nb067AlphaDummy101 f), (nb067AlphaDummy100, nb067AlphaDummy102 f), (nb067AlphaDummy092, nb067AlphaDummy094 f), (nb067AlphaDummy091, nb067AlphaDummy093 f), (nb067AlphaDummy097, nb067AlphaDummy098 f), (nb067AlphaDummy095, nb067AlphaDummy096 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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 nb067AlphaDummy106) (SemanticCore.Class.cv nb067AlphaDummy107)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy105) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy106) (SemanticCore.Class.cv nb067AlphaDummy107))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy109 f)) (SemanticCore.Class.cv (nb067AlphaDummy110 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy108 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy109 f)) (SemanticCore.Class.cv (nb067AlphaDummy110 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0010.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0011 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy099, nb067AlphaDummy101 f), (nb067AlphaDummy100, nb067AlphaDummy102 f), (nb067AlphaDummy092, nb067AlphaDummy094 f), (nb067AlphaDummy091, nb067AlphaDummy093 f), (nb067AlphaDummy097, nb067AlphaDummy098 f), (nb067AlphaDummy095, nb067AlphaDummy096 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy099) (SemanticCore.Class.cv nb067AlphaDummy092)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy100) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy099) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy099) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy099))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy101 f)) (SemanticCore.Class.cv (nb067AlphaDummy094 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy102 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy101 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy101 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy101 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0011.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0012 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy107, nb067AlphaDummy110 f), (nb067AlphaDummy106, nb067AlphaDummy109 f), (nb067AlphaDummy105, nb067AlphaDummy108 f), (nb067AlphaDummy103, nb067AlphaDummy104 f), (nb067AlphaDummy099, nb067AlphaDummy101 f), (nb067AlphaDummy100, nb067AlphaDummy102 f), (nb067AlphaDummy125, nb067AlphaDummy126 f), (nb067AlphaDummy123, nb067AlphaDummy124 f), (nb067AlphaDummy092, nb067AlphaDummy094 f), (nb067AlphaDummy091, nb067AlphaDummy093 f), (nb067AlphaDummy121, nb067AlphaDummy122 f), (nb067AlphaDummy095, nb067AlphaDummy096 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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 nb067AlphaDummy106) (SemanticCore.Class.cv nb067AlphaDummy107)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy105) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy106) (SemanticCore.Class.cv nb067AlphaDummy107))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy109 f)) (SemanticCore.Class.cv (nb067AlphaDummy110 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy108 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy109 f)) (SemanticCore.Class.cv (nb067AlphaDummy110 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0012.

Equations

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

Certificates from NAR4C067C001Part014.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0013 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy099, nb067AlphaDummy101 f), (nb067AlphaDummy100, nb067AlphaDummy102 f), (nb067AlphaDummy125, nb067AlphaDummy126 f), (nb067AlphaDummy123, nb067AlphaDummy124 f), (nb067AlphaDummy092, nb067AlphaDummy094 f), (nb067AlphaDummy091, nb067AlphaDummy093 f), (nb067AlphaDummy121, nb067AlphaDummy122 f), (nb067AlphaDummy095, nb067AlphaDummy096 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy099) (SemanticCore.Class.cv nb067AlphaDummy092)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy100) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy099) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy099) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy099))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy101 f)) (SemanticCore.Class.cv (nb067AlphaDummy094 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy102 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy101 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy101 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy101 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0013.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0014 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy121, nb067AlphaDummy122 f), (nb067AlphaDummy095, nb067AlphaDummy096 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy121) (SemanticCore.Class.cab nb067AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy092 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy091) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy121) (SemanticCore.Class.cab nb067AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy092 (SemanticCore.Class.cv nb067AlphaDummy084) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy091) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy122 f)) (SemanticCore.Class.cab (nb067AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy094 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy122 f)) (SemanticCore.Class.cab (nb067AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy094 f) (SemanticCore.Class.cv (nb067AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0014.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0015 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy143, nb067AlphaDummy146 f), (nb067AlphaDummy142, nb067AlphaDummy145 f), (nb067AlphaDummy141, nb067AlphaDummy144 f), (nb067AlphaDummy139, nb067AlphaDummy140 f), (nb067AlphaDummy135, nb067AlphaDummy137 f), (nb067AlphaDummy136, nb067AlphaDummy138 f), (nb067AlphaDummy128, nb067AlphaDummy130 f), (nb067AlphaDummy127, nb067AlphaDummy129 f), (nb067AlphaDummy133, nb067AlphaDummy134 f), (nb067AlphaDummy131, nb067AlphaDummy132 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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 nb067AlphaDummy142) (SemanticCore.Class.cv nb067AlphaDummy143)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy141) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy142) (SemanticCore.Class.cv nb067AlphaDummy143))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy145 f)) (SemanticCore.Class.cv (nb067AlphaDummy146 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy144 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy145 f)) (SemanticCore.Class.cv (nb067AlphaDummy146 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0015.

Equations

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

Certificates from NAR4C067C001Part015.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0016 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy135, nb067AlphaDummy137 f), (nb067AlphaDummy136, nb067AlphaDummy138 f), (nb067AlphaDummy128, nb067AlphaDummy130 f), (nb067AlphaDummy127, nb067AlphaDummy129 f), (nb067AlphaDummy133, nb067AlphaDummy134 f), (nb067AlphaDummy131, nb067AlphaDummy132 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy135) (SemanticCore.Class.cv nb067AlphaDummy128)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy136) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy135) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy135) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy135))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy137 f)) (SemanticCore.Class.cv (nb067AlphaDummy130 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy138 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy137 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy137 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy137 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0016.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0017 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy143, nb067AlphaDummy146 f), (nb067AlphaDummy142, nb067AlphaDummy145 f), (nb067AlphaDummy141, nb067AlphaDummy144 f), (nb067AlphaDummy139, nb067AlphaDummy140 f), (nb067AlphaDummy135, nb067AlphaDummy137 f), (nb067AlphaDummy136, nb067AlphaDummy138 f), (nb067AlphaDummy161, nb067AlphaDummy162 f), (nb067AlphaDummy159, nb067AlphaDummy160 f), (nb067AlphaDummy128, nb067AlphaDummy130 f), (nb067AlphaDummy127, nb067AlphaDummy129 f), (nb067AlphaDummy157, nb067AlphaDummy158 f), (nb067AlphaDummy131, nb067AlphaDummy132 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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 nb067AlphaDummy142) (SemanticCore.Class.cv nb067AlphaDummy143)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy141) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb067AlphaDummy142) (SemanticCore.Class.cv nb067AlphaDummy143))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb067AlphaDummy145 f)) (SemanticCore.Class.cv (nb067AlphaDummy146 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy144 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb067AlphaDummy145 f)) (SemanticCore.Class.cv (nb067AlphaDummy146 f)))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0017.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0018 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy135, nb067AlphaDummy137 f), (nb067AlphaDummy136, nb067AlphaDummy138 f), (nb067AlphaDummy161, nb067AlphaDummy162 f), (nb067AlphaDummy159, nb067AlphaDummy160 f), (nb067AlphaDummy128, nb067AlphaDummy130 f), (nb067AlphaDummy127, nb067AlphaDummy129 f), (nb067AlphaDummy157, nb067AlphaDummy158 f), (nb067AlphaDummy131, nb067AlphaDummy132 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy136) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy135) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy135) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb067AlphaDummy135))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy138 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy137 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy137 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb067AlphaDummy137 f))))

Checked nominal proof certificate identified upstream as nb067_split_alpha_0018.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0019 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy157, nb067AlphaDummy158 f), (nb067AlphaDummy131, nb067AlphaDummy132 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy157) (SemanticCore.Class.cab nb067AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy128 (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy127) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy157) (SemanticCore.Class.cab nb067AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy128 (SemanticCore.Class.cv nb067AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy127) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy128)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy158 f)) (SemanticCore.Class.cab (nb067AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy130 f) (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy158 f)) (SemanticCore.Class.cab (nb067AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy130 f) (SemanticCore.Class.cv (nb067AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy130 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb067_split_alpha_0019.

Equations

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

Certificates from NAR4C067C001Part016.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0020 (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), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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_0020.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0021 (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), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] (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))) (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))))

Checked nominal proof certificate identified upstream as nb067_split_alpha_0021.

Equations

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

Certificates from NAR4C067C001Part017.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0022 (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), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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_0022.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0023 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(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), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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 nb067AlphaDummy181) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy177) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy177) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy181) (SemanticCore.Class.cv nb067AlphaDummy177)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy177) Compiler.CompactSourceSyntax.synCnnc).neg)) ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy182 f)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy179 f)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy179 f)) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy182 f)) (SemanticCore.Class.cv (nb067AlphaDummy179 f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy179 f)) Compiler.CompactSourceSyntax.synCnnc).neg))

Checked nominal proof certificate identified upstream as nb067_split_alpha_0023.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0024 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy199, nb067AlphaDummy200 f), (nb067AlphaDummy173, nb067AlphaDummy174 f), (nb067AlphaDummy164, nb067AlphaDummy166 f), (nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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_0024.

Equations

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

Certificates from NAR4C067C001Part018.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0025 (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), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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_0025.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0026 (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), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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_0026.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0027 (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), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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_0027.

Equations

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

Certificates from NAR4C067C001Part019.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0028 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(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), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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 nb067AlphaDummy217) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb067AlphaDummy213) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy213) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy217) (SemanticCore.Class.cv nb067AlphaDummy213)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy213) Compiler.CompactSourceSyntax.synCnnc).neg)) ((Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy218 f)) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb067AlphaDummy215 f)) Compiler.CompactSourceSyntax.synC1c)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy215 f)) Compiler.CompactSourceSyntax.synCnnc)).neg.imp (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy218 f)) (SemanticCore.Class.cv (nb067AlphaDummy215 f))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy215 f)) Compiler.CompactSourceSyntax.synCnnc).neg))

Checked nominal proof certificate identified upstream as nb067_split_alpha_0028.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0029 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(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), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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 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 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (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_0029.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067FunctionOccurrence (x y f : SemanticCore.Var) : Nominal.TAlphaClass [(nb067AlphaDummy164, nb067AlphaDummy166 f), (nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv f)

Checked nominal proof certificate identified upstream as nb067_function_occurrence.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0030 (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), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Class.cv nb067AlphaDummy163)) (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb067AlphaDummy166 f)) (SemanticCore.Class.cv (nb067AlphaDummy165 f))) (SemanticCore.Class.cv f))

Checked nominal proof certificate identified upstream as nb067_split_alpha_0030.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0031 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy163, nb067AlphaDummy165 f), (nb067AlphaDummy167, nb067AlphaDummy168 f), (nb067AlphaDummy085, nb067AlphaDummy088 f), (nb067AlphaDummy084, nb067AlphaDummy087 f), (nb067AlphaDummy083, nb067AlphaDummy086 f), (nb067AlphaDummy089, nb067AlphaDummy090 f), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] (SemanticCore.Wff.all nb067AlphaDummy164 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy167) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb067AlphaDummy163) (SemanticCore.Class.cv nb067AlphaDummy164))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb067AlphaDummy164) (SemanticCore.Class.cv nb067AlphaDummy000) (SemanticCore.Class.cv nb067AlphaDummy163))).neg) (SemanticCore.Wff.all (nb067AlphaDummy166 f) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy168 f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb067AlphaDummy165 f)) (SemanticCore.Class.cv (nb067AlphaDummy166 f)))) (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_0031.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0032 (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), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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_0032.

Equations

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

Certificates from NAR4C067C001Part020.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0033 (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), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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_0033.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0034 (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), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 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_0034.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0035 (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), (nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] (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))) (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))))

Checked nominal proof certificate identified upstream as nb067_split_alpha_0035.

Equations

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