Nominal proof certificates grouped in dependency order.

Certificates from NAR4C068C001Part023.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068WppRefl0042 (x y f : SemanticCore.Var) : Nominal.TReflOn [(nb068AlphaDummy043, nb068AlphaDummy044 f), (nb068AlphaDummy041, nb068AlphaDummy042 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] Compiler.CompactSourceSyntax.synCid.fv

Checked nominal proof certificate identified upstream as nb068_wpp_refl_0042.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0033 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy041, nb068AlphaDummy042 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy041) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb068AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))) Compiler.CompactSourceSyntax.synCid)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy041) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb068AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb068AlphaDummy000))) Compiler.CompactSourceSyntax.synCid)).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy042 f)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy042 f)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid)).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0033.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0034 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy069, nb068AlphaDummy072 f), (nb068AlphaDummy068, nb068AlphaDummy071 f), (nb068AlphaDummy067, nb068AlphaDummy070 f), (nb068AlphaDummy065, nb068AlphaDummy066 f), (nb068AlphaDummy061, nb068AlphaDummy063 f), (nb068AlphaDummy062, nb068AlphaDummy064 f), (nb068AlphaDummy054, nb068AlphaDummy056 f), (nb068AlphaDummy053, nb068AlphaDummy055 f), (nb068AlphaDummy059, nb068AlphaDummy060 f), (nb068AlphaDummy057, nb068AlphaDummy058 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy067) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy070 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0034.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0035 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy054, nb068AlphaDummy056 f), (nb068AlphaDummy053, nb068AlphaDummy055 f), (nb068AlphaDummy059, nb068AlphaDummy060 f), (nb068AlphaDummy057, nb068AlphaDummy058 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0035.

Equations

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

Certificates from NAR4C068C001Part024.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0036 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy069, nb068AlphaDummy072 f), (nb068AlphaDummy068, nb068AlphaDummy071 f), (nb068AlphaDummy067, nb068AlphaDummy070 f), (nb068AlphaDummy065, nb068AlphaDummy066 f), (nb068AlphaDummy061, nb068AlphaDummy063 f), (nb068AlphaDummy062, nb068AlphaDummy064 f), (nb068AlphaDummy087, nb068AlphaDummy088 f), (nb068AlphaDummy085, nb068AlphaDummy086 f), (nb068AlphaDummy054, nb068AlphaDummy056 f), (nb068AlphaDummy053, nb068AlphaDummy055 f), (nb068AlphaDummy083, nb068AlphaDummy084 f), (nb068AlphaDummy057, nb068AlphaDummy058 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy067) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy068) (SemanticCore.Class.cv nb068AlphaDummy069))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy070 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy071 f)) (SemanticCore.Class.cv (nb068AlphaDummy072 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0036.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0037 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy061, nb068AlphaDummy063 f), (nb068AlphaDummy062, nb068AlphaDummy064 f), (nb068AlphaDummy087, nb068AlphaDummy088 f), (nb068AlphaDummy085, nb068AlphaDummy086 f), (nb068AlphaDummy054, nb068AlphaDummy056 f), (nb068AlphaDummy053, nb068AlphaDummy055 f), (nb068AlphaDummy083, nb068AlphaDummy084 f), (nb068AlphaDummy057, nb068AlphaDummy058 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy061) (SemanticCore.Class.cv nb068AlphaDummy054)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy062) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy061) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy061) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy061))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy063 f)) (SemanticCore.Class.cv (nb068AlphaDummy056 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy064 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy063 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy063 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy063 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0037.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0038 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy083, nb068AlphaDummy084 f), (nb068AlphaDummy057, nb068AlphaDummy058 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy083) (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy083) (SemanticCore.Class.cab nb068AlphaDummy053 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy054 (SemanticCore.Class.cv nb068AlphaDummy046) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy053) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy054)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy084 f)) (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy084 f)) (SemanticCore.Class.cab (nb068AlphaDummy055 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy056 f) (SemanticCore.Class.cv (nb068AlphaDummy049 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy055 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy056 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0038.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0039 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy105, nb068AlphaDummy108 f), (nb068AlphaDummy104, nb068AlphaDummy107 f), (nb068AlphaDummy103, nb068AlphaDummy106 f), (nb068AlphaDummy101, nb068AlphaDummy102 f), (nb068AlphaDummy097, nb068AlphaDummy099 f), (nb068AlphaDummy098, nb068AlphaDummy100 f), (nb068AlphaDummy090, nb068AlphaDummy092 f), (nb068AlphaDummy089, nb068AlphaDummy091 f), (nb068AlphaDummy095, nb068AlphaDummy096 f), (nb068AlphaDummy093, nb068AlphaDummy094 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy103) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy106 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0039.

Equations

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

Certificates from NAR4C068C001Part025.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0040 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy090, nb068AlphaDummy092 f), (nb068AlphaDummy089, nb068AlphaDummy091 f), (nb068AlphaDummy095, nb068AlphaDummy096 f), (nb068AlphaDummy093, nb068AlphaDummy094 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0040.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0041 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy105, nb068AlphaDummy108 f), (nb068AlphaDummy104, nb068AlphaDummy107 f), (nb068AlphaDummy103, nb068AlphaDummy106 f), (nb068AlphaDummy101, nb068AlphaDummy102 f), (nb068AlphaDummy097, nb068AlphaDummy099 f), (nb068AlphaDummy098, nb068AlphaDummy100 f), (nb068AlphaDummy123, nb068AlphaDummy124 f), (nb068AlphaDummy121, nb068AlphaDummy122 f), (nb068AlphaDummy090, nb068AlphaDummy092 f), (nb068AlphaDummy089, nb068AlphaDummy091 f), (nb068AlphaDummy119, nb068AlphaDummy120 f), (nb068AlphaDummy093, nb068AlphaDummy094 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy103) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy104) (SemanticCore.Class.cv nb068AlphaDummy105))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy106 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy107 f)) (SemanticCore.Class.cv (nb068AlphaDummy108 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0041.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0042 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy097, nb068AlphaDummy099 f), (nb068AlphaDummy098, nb068AlphaDummy100 f), (nb068AlphaDummy123, nb068AlphaDummy124 f), (nb068AlphaDummy121, nb068AlphaDummy122 f), (nb068AlphaDummy090, nb068AlphaDummy092 f), (nb068AlphaDummy089, nb068AlphaDummy091 f), (nb068AlphaDummy119, nb068AlphaDummy120 f), (nb068AlphaDummy093, nb068AlphaDummy094 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy097) (SemanticCore.Class.cv nb068AlphaDummy090)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy098) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy097) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy097) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy097))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy099 f)) (SemanticCore.Class.cv (nb068AlphaDummy092 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy100 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy099 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy099 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy099 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0042.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0043 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy119, nb068AlphaDummy120 f), (nb068AlphaDummy093, nb068AlphaDummy094 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy119) (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy119) (SemanticCore.Class.cab nb068AlphaDummy089 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy090 (SemanticCore.Class.cv nb068AlphaDummy047) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy089) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy090)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy120 f)) (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy120 f)) (SemanticCore.Class.cab (nb068AlphaDummy091 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy092 f) (SemanticCore.Class.cv (nb068AlphaDummy050 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy091 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy092 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0043.

Equations

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

Certificates from NAR4C068C001Part026.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0044 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy147, nb068AlphaDummy150 f), (nb068AlphaDummy146, nb068AlphaDummy149 f), (nb068AlphaDummy145, nb068AlphaDummy148 f), (nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy137, nb068AlphaDummy138 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy145) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy148 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0044.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0045 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy137, nb068AlphaDummy138 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) (SemanticCore.Class.cv nb068AlphaDummy132)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy140) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy139))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) (SemanticCore.Class.cv (nb068AlphaDummy134 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy142 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy141 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0045.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0046 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy147, nb068AlphaDummy150 f), (nb068AlphaDummy146, nb068AlphaDummy149 f), (nb068AlphaDummy145, nb068AlphaDummy148 f), (nb068AlphaDummy143, nb068AlphaDummy144 f), (nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy165, nb068AlphaDummy166 f), (nb068AlphaDummy163, nb068AlphaDummy164 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy145) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy146) (SemanticCore.Class.cv nb068AlphaDummy147))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy148 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy149 f)) (SemanticCore.Class.cv (nb068AlphaDummy150 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0046.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0047 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy139, nb068AlphaDummy141 f), (nb068AlphaDummy140, nb068AlphaDummy142 f), (nb068AlphaDummy165, nb068AlphaDummy166 f), (nb068AlphaDummy163, nb068AlphaDummy164 f), (nb068AlphaDummy132, nb068AlphaDummy134 f), (nb068AlphaDummy131, nb068AlphaDummy133 f), (nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy140) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy139) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy139))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy142 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy141 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy141 f))))

Checked nominal proof certificate identified upstream as nb068_split_alpha_0047.

Equations

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

Certificates from NAR4C068C001Part027.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0048 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy161, nb068AlphaDummy162 f), (nb068AlphaDummy135, nb068AlphaDummy136 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy161) (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy161) (SemanticCore.Class.cab nb068AlphaDummy131 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy132 (SemanticCore.Class.cv nb068AlphaDummy126) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy131) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy132)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy162 f)) (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy162 f)) (SemanticCore.Class.cab (nb068AlphaDummy133 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy134 f) (SemanticCore.Class.cv (nb068AlphaDummy128 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy133 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy134 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0048.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0049 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy183, nb068AlphaDummy186 f), (nb068AlphaDummy182, nb068AlphaDummy185 f), (nb068AlphaDummy181, nb068AlphaDummy184 f), (nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy173, nb068AlphaDummy174 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy181) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy184 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0049.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0050 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy173, nb068AlphaDummy174 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) (SemanticCore.Class.cv nb068AlphaDummy168)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy176) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy175) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb068AlphaDummy175))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) (SemanticCore.Class.cv (nb068AlphaDummy170 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy178 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb068AlphaDummy177 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb068AlphaDummy177 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0050.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068SplitAlpha0051 (x y f : SemanticCore.Var) : Nominal.TAlphaWff [(nb068AlphaDummy183, nb068AlphaDummy186 f), (nb068AlphaDummy182, nb068AlphaDummy185 f), (nb068AlphaDummy181, nb068AlphaDummy184 f), (nb068AlphaDummy179, nb068AlphaDummy180 f), (nb068AlphaDummy175, nb068AlphaDummy177 f), (nb068AlphaDummy176, nb068AlphaDummy178 f), (nb068AlphaDummy201, nb068AlphaDummy202 f), (nb068AlphaDummy199, nb068AlphaDummy200 f), (nb068AlphaDummy168, nb068AlphaDummy170 f), (nb068AlphaDummy167, nb068AlphaDummy169 f), (nb068AlphaDummy197, nb068AlphaDummy198 f), (nb068AlphaDummy171, nb068AlphaDummy172 f), (nb068AlphaDummy126, nb068AlphaDummy128 f), (nb068AlphaDummy125, nb068AlphaDummy127 f), (nb068AlphaDummy129, nb068AlphaDummy130 f), (nb068AlphaDummy047, nb068AlphaDummy050 f), (nb068AlphaDummy046, nb068AlphaDummy049 f), (nb068AlphaDummy045, nb068AlphaDummy048 f), (nb068AlphaDummy051, nb068AlphaDummy052 f), (nb068AlphaDummy000, f), (nb068AlphaDummy002, y), (nb068AlphaDummy001, x), (nb068AlphaDummy003, nb068AlphaDummy004 x y f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy181) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb068AlphaDummy182) (SemanticCore.Class.cv nb068AlphaDummy183))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy184 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb068AlphaDummy185 f)) (SemanticCore.Class.cv (nb068AlphaDummy186 f)))).neg)

Checked nominal proof certificate identified upstream as nb068_split_alpha_0051.

Equations

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