Nominal proof certificates grouped in dependency order.

Certificates from NAR4C056C001Part006.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0000 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy029, nb056AlphaDummy032 f), (nb056AlphaDummy028, nb056AlphaDummy031 f), (nb056AlphaDummy027, nb056AlphaDummy030 f), (nb056AlphaDummy025, nb056AlphaDummy026 f), (nb056AlphaDummy021, nb056AlphaDummy023 f), (nb056AlphaDummy022, nb056AlphaDummy024 f), (nb056AlphaDummy014, nb056AlphaDummy016 f), (nb056AlphaDummy013, nb056AlphaDummy015 f), (nb056AlphaDummy019, nb056AlphaDummy020 f), (nb056AlphaDummy017, nb056AlphaDummy018 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb056AlphaDummy028) (SemanticCore.Class.cv nb056AlphaDummy029)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy027) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb056AlphaDummy028) (SemanticCore.Class.cv nb056AlphaDummy029))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb056AlphaDummy031 f)) (SemanticCore.Class.cv (nb056AlphaDummy032 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy030 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb056AlphaDummy031 f)) (SemanticCore.Class.cv (nb056AlphaDummy032 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0000.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0001 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy014, nb056AlphaDummy016 f), (nb056AlphaDummy013, nb056AlphaDummy015 f), (nb056AlphaDummy019, nb056AlphaDummy020 f), (nb056AlphaDummy017, nb056AlphaDummy018 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy013) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy014))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy015 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy016 f))))

Checked nominal proof certificate identified upstream as nb056_split_alpha_0001.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0002 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy029, nb056AlphaDummy032 f), (nb056AlphaDummy028, nb056AlphaDummy031 f), (nb056AlphaDummy027, nb056AlphaDummy030 f), (nb056AlphaDummy025, nb056AlphaDummy026 f), (nb056AlphaDummy021, nb056AlphaDummy023 f), (nb056AlphaDummy022, nb056AlphaDummy024 f), (nb056AlphaDummy047, nb056AlphaDummy048 f), (nb056AlphaDummy045, nb056AlphaDummy046 f), (nb056AlphaDummy014, nb056AlphaDummy016 f), (nb056AlphaDummy013, nb056AlphaDummy015 f), (nb056AlphaDummy043, nb056AlphaDummy044 f), (nb056AlphaDummy017, nb056AlphaDummy018 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb056AlphaDummy028) (SemanticCore.Class.cv nb056AlphaDummy029)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy027) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb056AlphaDummy028) (SemanticCore.Class.cv nb056AlphaDummy029))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb056AlphaDummy031 f)) (SemanticCore.Class.cv (nb056AlphaDummy032 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy030 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb056AlphaDummy031 f)) (SemanticCore.Class.cv (nb056AlphaDummy032 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0002.

Equations

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

Certificates from NAR4C056C001Part007.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0003 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy021, nb056AlphaDummy023 f), (nb056AlphaDummy022, nb056AlphaDummy024 f), (nb056AlphaDummy047, nb056AlphaDummy048 f), (nb056AlphaDummy045, nb056AlphaDummy046 f), (nb056AlphaDummy014, nb056AlphaDummy016 f), (nb056AlphaDummy013, nb056AlphaDummy015 f), (nb056AlphaDummy043, nb056AlphaDummy044 f), (nb056AlphaDummy017, nb056AlphaDummy018 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy021) (SemanticCore.Class.cv nb056AlphaDummy014)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy022) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy021) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb056AlphaDummy021) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb056AlphaDummy021))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy023 f)) (SemanticCore.Class.cv (nb056AlphaDummy016 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy024 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy023 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb056AlphaDummy023 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb056AlphaDummy023 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0003.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0004 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy043, nb056AlphaDummy044 f), (nb056AlphaDummy017, nb056AlphaDummy018 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy043) (SemanticCore.Class.cab nb056AlphaDummy013 (Compiler.CompactSourceSyntax.synWrex nb056AlphaDummy014 (SemanticCore.Class.cv nb056AlphaDummy006) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy013) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy014)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy043) (SemanticCore.Class.cab nb056AlphaDummy013 (Compiler.CompactSourceSyntax.synWrex nb056AlphaDummy014 (SemanticCore.Class.cv nb056AlphaDummy006) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy013) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy014)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy044 f)) (SemanticCore.Class.cab (nb056AlphaDummy015 f) (Compiler.CompactSourceSyntax.synWrex (nb056AlphaDummy016 f) (SemanticCore.Class.cv (nb056AlphaDummy009 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy015 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy016 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy044 f)) (SemanticCore.Class.cab (nb056AlphaDummy015 f) (Compiler.CompactSourceSyntax.synWrex (nb056AlphaDummy016 f) (SemanticCore.Class.cv (nb056AlphaDummy009 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy015 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy016 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0004.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0005 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy065, nb056AlphaDummy068 f), (nb056AlphaDummy064, nb056AlphaDummy067 f), (nb056AlphaDummy063, nb056AlphaDummy066 f), (nb056AlphaDummy061, nb056AlphaDummy062 f), (nb056AlphaDummy057, nb056AlphaDummy059 f), (nb056AlphaDummy058, nb056AlphaDummy060 f), (nb056AlphaDummy050, nb056AlphaDummy052 f), (nb056AlphaDummy049, nb056AlphaDummy051 f), (nb056AlphaDummy055, nb056AlphaDummy056 f), (nb056AlphaDummy053, nb056AlphaDummy054 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb056AlphaDummy064) (SemanticCore.Class.cv nb056AlphaDummy065)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy063) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb056AlphaDummy064) (SemanticCore.Class.cv nb056AlphaDummy065))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb056AlphaDummy067 f)) (SemanticCore.Class.cv (nb056AlphaDummy068 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy066 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb056AlphaDummy067 f)) (SemanticCore.Class.cv (nb056AlphaDummy068 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0005.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0006 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy050, nb056AlphaDummy052 f), (nb056AlphaDummy049, nb056AlphaDummy051 f), (nb056AlphaDummy055, nb056AlphaDummy056 f), (nb056AlphaDummy053, nb056AlphaDummy054 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy049) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy050))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy051 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy052 f))))

Checked nominal proof certificate identified upstream as nb056_split_alpha_0006.

Equations

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

Certificates from NAR4C056C001Part008.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0007 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy065, nb056AlphaDummy068 f), (nb056AlphaDummy064, nb056AlphaDummy067 f), (nb056AlphaDummy063, nb056AlphaDummy066 f), (nb056AlphaDummy061, nb056AlphaDummy062 f), (nb056AlphaDummy057, nb056AlphaDummy059 f), (nb056AlphaDummy058, nb056AlphaDummy060 f), (nb056AlphaDummy083, nb056AlphaDummy084 f), (nb056AlphaDummy081, nb056AlphaDummy082 f), (nb056AlphaDummy050, nb056AlphaDummy052 f), (nb056AlphaDummy049, nb056AlphaDummy051 f), (nb056AlphaDummy079, nb056AlphaDummy080 f), (nb056AlphaDummy053, nb056AlphaDummy054 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb056AlphaDummy064) (SemanticCore.Class.cv nb056AlphaDummy065)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy063) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb056AlphaDummy064) (SemanticCore.Class.cv nb056AlphaDummy065))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb056AlphaDummy067 f)) (SemanticCore.Class.cv (nb056AlphaDummy068 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy066 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb056AlphaDummy067 f)) (SemanticCore.Class.cv (nb056AlphaDummy068 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0007.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0008 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy057, nb056AlphaDummy059 f), (nb056AlphaDummy058, nb056AlphaDummy060 f), (nb056AlphaDummy083, nb056AlphaDummy084 f), (nb056AlphaDummy081, nb056AlphaDummy082 f), (nb056AlphaDummy050, nb056AlphaDummy052 f), (nb056AlphaDummy049, nb056AlphaDummy051 f), (nb056AlphaDummy079, nb056AlphaDummy080 f), (nb056AlphaDummy053, nb056AlphaDummy054 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy057) (SemanticCore.Class.cv nb056AlphaDummy050)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy058) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy057) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb056AlphaDummy057) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb056AlphaDummy057))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy059 f)) (SemanticCore.Class.cv (nb056AlphaDummy052 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy060 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy059 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb056AlphaDummy059 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb056AlphaDummy059 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0008.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0009 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy079, nb056AlphaDummy080 f), (nb056AlphaDummy053, nb056AlphaDummy054 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy079) (SemanticCore.Class.cab nb056AlphaDummy049 (Compiler.CompactSourceSyntax.synWrex nb056AlphaDummy050 (SemanticCore.Class.cv nb056AlphaDummy007) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy049) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy050)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy079) (SemanticCore.Class.cab nb056AlphaDummy049 (Compiler.CompactSourceSyntax.synWrex nb056AlphaDummy050 (SemanticCore.Class.cv nb056AlphaDummy007) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy049) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy050)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy080 f)) (SemanticCore.Class.cab (nb056AlphaDummy051 f) (Compiler.CompactSourceSyntax.synWrex (nb056AlphaDummy052 f) (SemanticCore.Class.cv (nb056AlphaDummy010 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy051 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy052 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy080 f)) (SemanticCore.Class.cab (nb056AlphaDummy051 f) (Compiler.CompactSourceSyntax.synWrex (nb056AlphaDummy052 f) (SemanticCore.Class.cv (nb056AlphaDummy010 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy051 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy052 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0009.

Equations

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

Certificates from NAR4C056C001Part009.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0010 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy107, nb056AlphaDummy110 f), (nb056AlphaDummy106, nb056AlphaDummy109 f), (nb056AlphaDummy105, nb056AlphaDummy108 f), (nb056AlphaDummy103, nb056AlphaDummy104 f), (nb056AlphaDummy099, nb056AlphaDummy101 f), (nb056AlphaDummy100, nb056AlphaDummy102 f), (nb056AlphaDummy092, nb056AlphaDummy094 f), (nb056AlphaDummy091, nb056AlphaDummy093 f), (nb056AlphaDummy097, nb056AlphaDummy098 f), (nb056AlphaDummy095, nb056AlphaDummy096 f), (nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb056AlphaDummy106) (SemanticCore.Class.cv nb056AlphaDummy107)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy105) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb056AlphaDummy106) (SemanticCore.Class.cv nb056AlphaDummy107))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb056AlphaDummy109 f)) (SemanticCore.Class.cv (nb056AlphaDummy110 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy108 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb056AlphaDummy109 f)) (SemanticCore.Class.cv (nb056AlphaDummy110 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0010.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0011 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy099, nb056AlphaDummy101 f), (nb056AlphaDummy100, nb056AlphaDummy102 f), (nb056AlphaDummy092, nb056AlphaDummy094 f), (nb056AlphaDummy091, nb056AlphaDummy093 f), (nb056AlphaDummy097, nb056AlphaDummy098 f), (nb056AlphaDummy095, nb056AlphaDummy096 f), (nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy099) (SemanticCore.Class.cv nb056AlphaDummy092)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy100) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy099) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb056AlphaDummy099) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb056AlphaDummy099))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy101 f)) (SemanticCore.Class.cv (nb056AlphaDummy094 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy102 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy101 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb056AlphaDummy101 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb056AlphaDummy101 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0011.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0012 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy107, nb056AlphaDummy110 f), (nb056AlphaDummy106, nb056AlphaDummy109 f), (nb056AlphaDummy105, nb056AlphaDummy108 f), (nb056AlphaDummy103, nb056AlphaDummy104 f), (nb056AlphaDummy099, nb056AlphaDummy101 f), (nb056AlphaDummy100, nb056AlphaDummy102 f), (nb056AlphaDummy125, nb056AlphaDummy126 f), (nb056AlphaDummy123, nb056AlphaDummy124 f), (nb056AlphaDummy092, nb056AlphaDummy094 f), (nb056AlphaDummy091, nb056AlphaDummy093 f), (nb056AlphaDummy121, nb056AlphaDummy122 f), (nb056AlphaDummy095, nb056AlphaDummy096 f), (nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb056AlphaDummy106) (SemanticCore.Class.cv nb056AlphaDummy107)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy105) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb056AlphaDummy106) (SemanticCore.Class.cv nb056AlphaDummy107))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb056AlphaDummy109 f)) (SemanticCore.Class.cv (nb056AlphaDummy110 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy108 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb056AlphaDummy109 f)) (SemanticCore.Class.cv (nb056AlphaDummy110 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0012.

Equations

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

Certificates from NAR4C056C001Part010.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0013 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy099, nb056AlphaDummy101 f), (nb056AlphaDummy100, nb056AlphaDummy102 f), (nb056AlphaDummy125, nb056AlphaDummy126 f), (nb056AlphaDummy123, nb056AlphaDummy124 f), (nb056AlphaDummy092, nb056AlphaDummy094 f), (nb056AlphaDummy091, nb056AlphaDummy093 f), (nb056AlphaDummy121, nb056AlphaDummy122 f), (nb056AlphaDummy095, nb056AlphaDummy096 f), (nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy100) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy099) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb056AlphaDummy099) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb056AlphaDummy099))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy102 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy101 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb056AlphaDummy101 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb056AlphaDummy101 f))))

Checked nominal proof certificate identified upstream as nb056_split_alpha_0013.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0014 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy121, nb056AlphaDummy122 f), (nb056AlphaDummy095, nb056AlphaDummy096 f), (nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy121) (SemanticCore.Class.cab nb056AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb056AlphaDummy092 (SemanticCore.Class.cv nb056AlphaDummy086) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy091) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy092)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy121) (SemanticCore.Class.cab nb056AlphaDummy091 (Compiler.CompactSourceSyntax.synWrex nb056AlphaDummy092 (SemanticCore.Class.cv nb056AlphaDummy086) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy091) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy092)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy122 f)) (SemanticCore.Class.cab (nb056AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb056AlphaDummy094 f) (SemanticCore.Class.cv (nb056AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy094 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy122 f)) (SemanticCore.Class.cab (nb056AlphaDummy093 f) (Compiler.CompactSourceSyntax.synWrex (nb056AlphaDummy094 f) (SemanticCore.Class.cv (nb056AlphaDummy088 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy093 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy094 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0014.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0015 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy143, nb056AlphaDummy146 f), (nb056AlphaDummy142, nb056AlphaDummy145 f), (nb056AlphaDummy141, nb056AlphaDummy144 f), (nb056AlphaDummy139, nb056AlphaDummy140 f), (nb056AlphaDummy135, nb056AlphaDummy137 f), (nb056AlphaDummy136, nb056AlphaDummy138 f), (nb056AlphaDummy128, nb056AlphaDummy130 f), (nb056AlphaDummy127, nb056AlphaDummy129 f), (nb056AlphaDummy133, nb056AlphaDummy134 f), (nb056AlphaDummy131, nb056AlphaDummy132 f), (nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb056AlphaDummy142) (SemanticCore.Class.cv nb056AlphaDummy143)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy141) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb056AlphaDummy142) (SemanticCore.Class.cv nb056AlphaDummy143))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb056AlphaDummy145 f)) (SemanticCore.Class.cv (nb056AlphaDummy146 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy144 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb056AlphaDummy145 f)) (SemanticCore.Class.cv (nb056AlphaDummy146 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0015.

Equations

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

Certificates from NAR4C056C001Part011.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0016 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy135, nb056AlphaDummy137 f), (nb056AlphaDummy136, nb056AlphaDummy138 f), (nb056AlphaDummy128, nb056AlphaDummy130 f), (nb056AlphaDummy127, nb056AlphaDummy129 f), (nb056AlphaDummy133, nb056AlphaDummy134 f), (nb056AlphaDummy131, nb056AlphaDummy132 f), (nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy135) (SemanticCore.Class.cv nb056AlphaDummy128)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy136) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy135) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb056AlphaDummy135) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb056AlphaDummy135))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy137 f)) (SemanticCore.Class.cv (nb056AlphaDummy130 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy138 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy137 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb056AlphaDummy137 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb056AlphaDummy137 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0016.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0017 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy143, nb056AlphaDummy146 f), (nb056AlphaDummy142, nb056AlphaDummy145 f), (nb056AlphaDummy141, nb056AlphaDummy144 f), (nb056AlphaDummy139, nb056AlphaDummy140 f), (nb056AlphaDummy135, nb056AlphaDummy137 f), (nb056AlphaDummy136, nb056AlphaDummy138 f), (nb056AlphaDummy161, nb056AlphaDummy162 f), (nb056AlphaDummy159, nb056AlphaDummy160 f), (nb056AlphaDummy128, nb056AlphaDummy130 f), (nb056AlphaDummy127, nb056AlphaDummy129 f), (nb056AlphaDummy157, nb056AlphaDummy158 f), (nb056AlphaDummy131, nb056AlphaDummy132 f), (nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb056AlphaDummy142) (SemanticCore.Class.cv nb056AlphaDummy143)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy141) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb056AlphaDummy142) (SemanticCore.Class.cv nb056AlphaDummy143))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb056AlphaDummy145 f)) (SemanticCore.Class.cv (nb056AlphaDummy146 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy144 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb056AlphaDummy145 f)) (SemanticCore.Class.cv (nb056AlphaDummy146 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0017.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0018 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy135, nb056AlphaDummy137 f), (nb056AlphaDummy136, nb056AlphaDummy138 f), (nb056AlphaDummy161, nb056AlphaDummy162 f), (nb056AlphaDummy159, nb056AlphaDummy160 f), (nb056AlphaDummy128, nb056AlphaDummy130 f), (nb056AlphaDummy127, nb056AlphaDummy129 f), (nb056AlphaDummy157, nb056AlphaDummy158 f), (nb056AlphaDummy131, nb056AlphaDummy132 f), (nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy136) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy135) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb056AlphaDummy135) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb056AlphaDummy135))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy138 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy137 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb056AlphaDummy137 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb056AlphaDummy137 f))))

Checked nominal proof certificate identified upstream as nb056_split_alpha_0018.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0019 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy157, nb056AlphaDummy158 f), (nb056AlphaDummy131, nb056AlphaDummy132 f), (nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy157) (SemanticCore.Class.cab nb056AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb056AlphaDummy128 (SemanticCore.Class.cv nb056AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy127) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy128)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy157) (SemanticCore.Class.cab nb056AlphaDummy127 (Compiler.CompactSourceSyntax.synWrex nb056AlphaDummy128 (SemanticCore.Class.cv nb056AlphaDummy085) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy127) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy128)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy158 f)) (SemanticCore.Class.cab (nb056AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb056AlphaDummy130 f) (SemanticCore.Class.cv (nb056AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy130 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy158 f)) (SemanticCore.Class.cab (nb056AlphaDummy129 f) (Compiler.CompactSourceSyntax.synWrex (nb056AlphaDummy130 f) (SemanticCore.Class.cv (nb056AlphaDummy087 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy129 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy130 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0019.

Equations

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

Certificates from NAR4C056C001Part012.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056VariableOccurrence (f : SemanticCore.Var) : Nominal.TAlphaClass [(nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] (SemanticCore.Class.cv nb056AlphaDummy000) (SemanticCore.Class.cv f)

Checked nominal proof certificate identified upstream as nb056_variable_occurrence.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0020 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy086, nb056AlphaDummy088 f), (nb056AlphaDummy085, nb056AlphaDummy087 f), (nb056AlphaDummy089, nb056AlphaDummy090 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy089) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb056AlphaDummy085) (SemanticCore.Class.cv nb056AlphaDummy086))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb056AlphaDummy086) (SemanticCore.Class.cv nb056AlphaDummy000) (SemanticCore.Class.cv nb056AlphaDummy085)).neg) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy090 f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb056AlphaDummy087 f)) (SemanticCore.Class.cv (nb056AlphaDummy088 f)))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb056AlphaDummy088 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb056AlphaDummy087 f))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0020.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0021 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy179, nb056AlphaDummy182 f), (nb056AlphaDummy178, nb056AlphaDummy181 f), (nb056AlphaDummy177, nb056AlphaDummy180 f), (nb056AlphaDummy175, nb056AlphaDummy176 f), (nb056AlphaDummy171, nb056AlphaDummy173 f), (nb056AlphaDummy172, nb056AlphaDummy174 f), (nb056AlphaDummy164, nb056AlphaDummy166 f), (nb056AlphaDummy163, nb056AlphaDummy165 f), (nb056AlphaDummy169, nb056AlphaDummy170 f), (nb056AlphaDummy167, nb056AlphaDummy168 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb056AlphaDummy178) (SemanticCore.Class.cv nb056AlphaDummy179)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy177) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb056AlphaDummy178) (SemanticCore.Class.cv nb056AlphaDummy179))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb056AlphaDummy181 f)) (SemanticCore.Class.cv (nb056AlphaDummy182 f))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy180 f)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb056AlphaDummy181 f)) (SemanticCore.Class.cv (nb056AlphaDummy182 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0021.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0022 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy164, nb056AlphaDummy166 f), (nb056AlphaDummy163, nb056AlphaDummy165 f), (nb056AlphaDummy169, nb056AlphaDummy170 f), (nb056AlphaDummy167, nb056AlphaDummy168 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy163) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy164))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy165 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy166 f))))

Checked nominal proof certificate identified upstream as nb056_split_alpha_0022.

Equations

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