Nominal proof certificates grouped in dependency order.

Certificates from NAR4C067C001Part021.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067WppRefl0050 (x y f : SemanticCore.Var) : Nominal.TReflOn [(nb067AlphaDummy081, nb067AlphaDummy082 f), (nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] Compiler.CompactSourceSyntax.synCid.fv

Checked nominal proof certificate identified upstream as nb067_wpp_refl_0050.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067WppRefl0050 x y f = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0038 (x y f : SemanticCore.Var) : Nominal.TAlphaClass [(nb067AlphaDummy079, nb067AlphaDummy080 f), (nb067AlphaDummy000, f), (nb067AlphaDummy003, nb067AlphaDummy004 x y f), (nb067AlphaDummy002, y), (nb067AlphaDummy001, x), (nb067AlphaDummy005, nb067AlphaDummy006 x y f)] (SemanticCore.Class.cab nb067AlphaDummy081 (Compiler.CompactSourceSyntax.synWnan (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy081) (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb067AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb067AlphaDummy081) Compiler.CompactSourceSyntax.synCid))) (SemanticCore.Class.cab (nb067AlphaDummy082 f) (Compiler.CompactSourceSyntax.synWnan (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy082 f)) (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy082 f)) Compiler.CompactSourceSyntax.synCid)))

Checked nominal proof certificate identified upstream as nb067_split_alpha_0038.

Equations

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

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0040 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy092, nb067AlphaDummy094 f), (nb067AlphaDummy091, nb067AlphaDummy093 f), (nb067AlphaDummy097, nb067AlphaDummy098 f), (nb067AlphaDummy095, nb067AlphaDummy096 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 nb067AlphaDummy091) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy092))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy094 f))))

Checked nominal proof certificate identified upstream as nb067_split_alpha_0040.

Equations

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

Certificates from NAR4C067C001Part022.

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

Equations

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

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0043 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb067AlphaDummy121, nb067AlphaDummy122 f), (nb067AlphaDummy095, nb067AlphaDummy096 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 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_0043.

Equations

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

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

Equations

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

Certificates from NAR4C067C001Part023.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067SplitAlpha0045 (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), (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 nb067AlphaDummy135) (SemanticCore.Class.cv nb067AlphaDummy128)) (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 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb067AlphaDummy137 f)) (SemanticCore.Class.cv (nb067AlphaDummy130 f))) (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_0045.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

Certificates from NAR4C067C001Part024.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

Certificates from NAR4C067C001Part025.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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