Nominal proof certificates grouped in dependency order.

Certificates from NAR4C055C001Part006.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0000 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy030, nb055AlphaDummy033 x y), (nb055AlphaDummy029, nb055AlphaDummy032 x y), (nb055AlphaDummy028, nb055AlphaDummy031 x y), (nb055AlphaDummy026, nb055AlphaDummy027 x y), (nb055AlphaDummy022, nb055AlphaDummy024 x y), (nb055AlphaDummy023, nb055AlphaDummy025 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy020, nb055AlphaDummy021 x y), (nb055AlphaDummy018, nb055AlphaDummy019 x y), (nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy012, nb055AlphaDummy013 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb055AlphaDummy029) (SemanticCore.Class.cv nb055AlphaDummy030)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy028) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb055AlphaDummy029) (SemanticCore.Class.cv nb055AlphaDummy030))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb055AlphaDummy032 x y)) (SemanticCore.Class.cv (nb055AlphaDummy033 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy031 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb055AlphaDummy032 x y)) (SemanticCore.Class.cv (nb055AlphaDummy033 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0000.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0001 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy020, nb055AlphaDummy021 x y), (nb055AlphaDummy018, nb055AlphaDummy019 x y), (nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy012, nb055AlphaDummy013 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy014) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy015))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy017 x y))))

Checked nominal proof certificate identified upstream as nb055_split_alpha_0001.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0002 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy030, nb055AlphaDummy033 x y), (nb055AlphaDummy029, nb055AlphaDummy032 x y), (nb055AlphaDummy028, nb055AlphaDummy031 x y), (nb055AlphaDummy026, nb055AlphaDummy027 x y), (nb055AlphaDummy022, nb055AlphaDummy024 x y), (nb055AlphaDummy023, nb055AlphaDummy025 x y), (nb055AlphaDummy048, nb055AlphaDummy049 x y), (nb055AlphaDummy046, nb055AlphaDummy047 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy044, nb055AlphaDummy045 x y), (nb055AlphaDummy018, nb055AlphaDummy019 x y), (nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy012, nb055AlphaDummy013 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb055AlphaDummy029) (SemanticCore.Class.cv nb055AlphaDummy030)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy028) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb055AlphaDummy029) (SemanticCore.Class.cv nb055AlphaDummy030))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb055AlphaDummy032 x y)) (SemanticCore.Class.cv (nb055AlphaDummy033 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy031 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb055AlphaDummy032 x y)) (SemanticCore.Class.cv (nb055AlphaDummy033 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0002.

Equations

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

Certificates from NAR4C055C001Part007.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0003 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy022, nb055AlphaDummy024 x y), (nb055AlphaDummy023, nb055AlphaDummy025 x y), (nb055AlphaDummy048, nb055AlphaDummy049 x y), (nb055AlphaDummy046, nb055AlphaDummy047 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy044, nb055AlphaDummy045 x y), (nb055AlphaDummy018, nb055AlphaDummy019 x y), (nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy012, nb055AlphaDummy013 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy022) (SemanticCore.Class.cv nb055AlphaDummy015)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy023) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy022) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb055AlphaDummy022) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb055AlphaDummy022))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy024 x y)) (SemanticCore.Class.cv (nb055AlphaDummy017 x y))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy025 x y)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy024 x y)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb055AlphaDummy024 x y)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb055AlphaDummy024 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0003.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055VariableOccurrence0 (x y : SemanticCore.Var) : Nominal.TAlphaClass [(nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy044, nb055AlphaDummy045 x y), (nb055AlphaDummy018, nb055AlphaDummy019 x y), (nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy012, nb055AlphaDummy013 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Class.cv nb055AlphaDummy001) (SemanticCore.Class.cv y)

Checked nominal proof certificate identified upstream as nb055_variable_occurrence_0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_variable_occurrence_1 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.TAlphaClass [(nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy020, nb055AlphaDummy021 x y), (nb055AlphaDummy018, nb055AlphaDummy019 x y), (nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy012, nb055AlphaDummy013 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Class.cv nb055AlphaDummy000) (SemanticCore.Class.cv x)

Checked nominal proof certificate identified upstream as nb055_variable_occurrence_1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0004 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy044, nb055AlphaDummy045 x y), (nb055AlphaDummy018, nb055AlphaDummy019 x y), (nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy012, nb055AlphaDummy013 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy044) (SemanticCore.Class.cab nb055AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy015 (SemanticCore.Class.cv nb055AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy014) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy015)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy044) (SemanticCore.Class.cab nb055AlphaDummy014 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy015 (SemanticCore.Class.cv nb055AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy014) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy015)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy045 x y)) (SemanticCore.Class.cab (nb055AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy017 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy017 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy045 x y)) (SemanticCore.Class.cab (nb055AlphaDummy016 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy017 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy016 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy017 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0004.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0005 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy058, nb055AlphaDummy061 x y), (nb055AlphaDummy057, nb055AlphaDummy060 x y), (nb055AlphaDummy056, nb055AlphaDummy059 x y), (nb055AlphaDummy054, nb055AlphaDummy055 x y), (nb055AlphaDummy050, nb055AlphaDummy052 x y), (nb055AlphaDummy051, nb055AlphaDummy053 x y), (nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy012, nb055AlphaDummy013 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb055AlphaDummy057) (SemanticCore.Class.cv nb055AlphaDummy058)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy056) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb055AlphaDummy057) (SemanticCore.Class.cv nb055AlphaDummy058))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb055AlphaDummy060 x y)) (SemanticCore.Class.cv (nb055AlphaDummy061 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy059 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb055AlphaDummy060 x y)) (SemanticCore.Class.cv (nb055AlphaDummy061 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0005.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0006 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy012, nb055AlphaDummy013 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy007) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb055AlphaDummy000) (SemanticCore.Class.cv nb055AlphaDummy001))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy007))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy009 x y)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy009 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0006.

Equations

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

Certificates from NAR4C055C001Part008.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0007 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy058, nb055AlphaDummy061 x y), (nb055AlphaDummy057, nb055AlphaDummy060 x y), (nb055AlphaDummy056, nb055AlphaDummy059 x y), (nb055AlphaDummy054, nb055AlphaDummy055 x y), (nb055AlphaDummy050, nb055AlphaDummy052 x y), (nb055AlphaDummy051, nb055AlphaDummy053 x y), (nb055AlphaDummy076, nb055AlphaDummy077 x y), (nb055AlphaDummy074, nb055AlphaDummy075 x y), (nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy072, nb055AlphaDummy073 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb055AlphaDummy057) (SemanticCore.Class.cv nb055AlphaDummy058)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy056) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb055AlphaDummy057) (SemanticCore.Class.cv nb055AlphaDummy058))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb055AlphaDummy060 x y)) (SemanticCore.Class.cv (nb055AlphaDummy061 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy059 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb055AlphaDummy060 x y)) (SemanticCore.Class.cv (nb055AlphaDummy061 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0007.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0008 (x y : SemanticCore.Var) : Nominal.TAlphaClass [(nb055AlphaDummy076, nb055AlphaDummy077 x y), (nb055AlphaDummy074, nb055AlphaDummy075 x y), (nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy072, nb055AlphaDummy073 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Class.cab nb055AlphaDummy051 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy050 (SemanticCore.Class.cv nb055AlphaDummy007) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy051) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy050) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb055AlphaDummy050) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb055AlphaDummy050))))) (SemanticCore.Class.cab (nb055AlphaDummy053 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy052 x y) (SemanticCore.Class.cv (nb055AlphaDummy009 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy053 x y)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy052 x y)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb055AlphaDummy052 x y)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb055AlphaDummy052 x y))))))

Checked nominal proof certificate identified upstream as nb055_split_alpha_0008.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_variable_occurrence_2 (x y : SemanticCore.Var) : Nominal.TAlphaClass [(nb055AlphaDummy007, nb055AlphaDummy009 x y), (nb055AlphaDummy006, nb055AlphaDummy008 x y), (nb055AlphaDummy072, nb055AlphaDummy073 x y), (nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Class.cv nb055AlphaDummy002) (SemanticCore.Class.cv (nb055AlphaDummy003 x y))

Checked nominal proof certificate identified upstream as nb055_variable_occurrence_2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0009 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb055AlphaDummy010, nb055AlphaDummy011 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy010) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb055AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy007 (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb055AlphaDummy000) (SemanticCore.Class.cv nb055AlphaDummy001)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy006) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy007))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy010) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb055AlphaDummy006 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy007 (SemanticCore.Class.cv nb055AlphaDummy002) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy006) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy007)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy011 x y)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb055AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy009 x y) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy009 x y)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy011 x y)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb055AlphaDummy008 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy009 x y) (SemanticCore.Class.cv (nb055AlphaDummy003 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy008 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy009 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0009.

Equations

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

Certificates from NAR4C055C001Part009.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0010 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy098, nb055AlphaDummy101 x y), (nb055AlphaDummy097, nb055AlphaDummy100 x y), (nb055AlphaDummy096, nb055AlphaDummy099 x y), (nb055AlphaDummy094, nb055AlphaDummy095 x y), (nb055AlphaDummy090, nb055AlphaDummy092 x y), (nb055AlphaDummy091, nb055AlphaDummy093 x y), (nb055AlphaDummy083, nb055AlphaDummy085 x y), (nb055AlphaDummy082, nb055AlphaDummy084 x y), (nb055AlphaDummy088, nb055AlphaDummy089 x y), (nb055AlphaDummy086, nb055AlphaDummy087 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb055AlphaDummy097) (SemanticCore.Class.cv nb055AlphaDummy098)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy096) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb055AlphaDummy097) (SemanticCore.Class.cv nb055AlphaDummy098))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb055AlphaDummy100 x y)) (SemanticCore.Class.cv (nb055AlphaDummy101 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy099 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb055AlphaDummy100 x y)) (SemanticCore.Class.cv (nb055AlphaDummy101 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0010.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0011 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy083, nb055AlphaDummy085 x y), (nb055AlphaDummy082, nb055AlphaDummy084 x y), (nb055AlphaDummy088, nb055AlphaDummy089 x y), (nb055AlphaDummy086, nb055AlphaDummy087 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy082) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy083))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy084 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy085 x y))))

Checked nominal proof certificate identified upstream as nb055_split_alpha_0011.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0012 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy098, nb055AlphaDummy101 x y), (nb055AlphaDummy097, nb055AlphaDummy100 x y), (nb055AlphaDummy096, nb055AlphaDummy099 x y), (nb055AlphaDummy094, nb055AlphaDummy095 x y), (nb055AlphaDummy090, nb055AlphaDummy092 x y), (nb055AlphaDummy091, nb055AlphaDummy093 x y), (nb055AlphaDummy116, nb055AlphaDummy117 x y), (nb055AlphaDummy114, nb055AlphaDummy115 x y), (nb055AlphaDummy083, nb055AlphaDummy085 x y), (nb055AlphaDummy082, nb055AlphaDummy084 x y), (nb055AlphaDummy112, nb055AlphaDummy113 x y), (nb055AlphaDummy086, nb055AlphaDummy087 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb055AlphaDummy097) (SemanticCore.Class.cv nb055AlphaDummy098)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy096) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb055AlphaDummy097) (SemanticCore.Class.cv nb055AlphaDummy098))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb055AlphaDummy100 x y)) (SemanticCore.Class.cv (nb055AlphaDummy101 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy099 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb055AlphaDummy100 x y)) (SemanticCore.Class.cv (nb055AlphaDummy101 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0012.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0013 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy090, nb055AlphaDummy092 x y), (nb055AlphaDummy091, nb055AlphaDummy093 x y), (nb055AlphaDummy116, nb055AlphaDummy117 x y), (nb055AlphaDummy114, nb055AlphaDummy115 x y), (nb055AlphaDummy083, nb055AlphaDummy085 x y), (nb055AlphaDummy082, nb055AlphaDummy084 x y), (nb055AlphaDummy112, nb055AlphaDummy113 x y), (nb055AlphaDummy086, nb055AlphaDummy087 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy090) (SemanticCore.Class.cv nb055AlphaDummy083)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy091) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy090) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb055AlphaDummy090) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb055AlphaDummy090))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy092 x y)) (SemanticCore.Class.cv (nb055AlphaDummy085 x y))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy093 x y)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy092 x y)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb055AlphaDummy092 x y)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb055AlphaDummy092 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0013.

Equations

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

Certificates from NAR4C055C001Part010.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0014 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy112, nb055AlphaDummy113 x y), (nb055AlphaDummy086, nb055AlphaDummy087 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy112) (SemanticCore.Class.cab nb055AlphaDummy082 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy083 (SemanticCore.Class.cv nb055AlphaDummy015) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy082) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy083)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy112) (SemanticCore.Class.cab nb055AlphaDummy082 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy083 (SemanticCore.Class.cv nb055AlphaDummy015) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy082) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy083)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy113 x y)) (SemanticCore.Class.cab (nb055AlphaDummy084 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy085 x y) (SemanticCore.Class.cv (nb055AlphaDummy017 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy084 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy085 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy113 x y)) (SemanticCore.Class.cab (nb055AlphaDummy084 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy085 x y) (SemanticCore.Class.cv (nb055AlphaDummy017 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy084 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy085 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0014.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0015 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy134, nb055AlphaDummy137 x y), (nb055AlphaDummy133, nb055AlphaDummy136 x y), (nb055AlphaDummy132, nb055AlphaDummy135 x y), (nb055AlphaDummy130, nb055AlphaDummy131 x y), (nb055AlphaDummy126, nb055AlphaDummy128 x y), (nb055AlphaDummy127, nb055AlphaDummy129 x y), (nb055AlphaDummy119, nb055AlphaDummy121 x y), (nb055AlphaDummy118, nb055AlphaDummy120 x y), (nb055AlphaDummy124, nb055AlphaDummy125 x y), (nb055AlphaDummy122, nb055AlphaDummy123 x y), (nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb055AlphaDummy133) (SemanticCore.Class.cv nb055AlphaDummy134)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy132) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb055AlphaDummy133) (SemanticCore.Class.cv nb055AlphaDummy134))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb055AlphaDummy136 x y)) (SemanticCore.Class.cv (nb055AlphaDummy137 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy135 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb055AlphaDummy136 x y)) (SemanticCore.Class.cv (nb055AlphaDummy137 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0015.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0016 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy119, nb055AlphaDummy121 x y), (nb055AlphaDummy118, nb055AlphaDummy120 x y), (nb055AlphaDummy124, nb055AlphaDummy125 x y), (nb055AlphaDummy122, nb055AlphaDummy123 x y), (nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy118) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy119))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy120 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy121 x y))))

Checked nominal proof certificate identified upstream as nb055_split_alpha_0016.

Equations

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

Certificates from NAR4C055C001Part011.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0017 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy134, nb055AlphaDummy137 x y), (nb055AlphaDummy133, nb055AlphaDummy136 x y), (nb055AlphaDummy132, nb055AlphaDummy135 x y), (nb055AlphaDummy130, nb055AlphaDummy131 x y), (nb055AlphaDummy126, nb055AlphaDummy128 x y), (nb055AlphaDummy127, nb055AlphaDummy129 x y), (nb055AlphaDummy152, nb055AlphaDummy153 x y), (nb055AlphaDummy150, nb055AlphaDummy151 x y), (nb055AlphaDummy119, nb055AlphaDummy121 x y), (nb055AlphaDummy118, nb055AlphaDummy120 x y), (nb055AlphaDummy148, nb055AlphaDummy149 x y), (nb055AlphaDummy122, nb055AlphaDummy123 x y), (nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb055AlphaDummy133) (SemanticCore.Class.cv nb055AlphaDummy134)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy132) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb055AlphaDummy133) (SemanticCore.Class.cv nb055AlphaDummy134))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb055AlphaDummy136 x y)) (SemanticCore.Class.cv (nb055AlphaDummy137 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy135 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb055AlphaDummy136 x y)) (SemanticCore.Class.cv (nb055AlphaDummy137 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0017.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0018 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy126, nb055AlphaDummy128 x y), (nb055AlphaDummy127, nb055AlphaDummy129 x y), (nb055AlphaDummy152, nb055AlphaDummy153 x y), (nb055AlphaDummy150, nb055AlphaDummy151 x y), (nb055AlphaDummy119, nb055AlphaDummy121 x y), (nb055AlphaDummy118, nb055AlphaDummy120 x y), (nb055AlphaDummy148, nb055AlphaDummy149 x y), (nb055AlphaDummy122, nb055AlphaDummy123 x y), (nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy126) (SemanticCore.Class.cv nb055AlphaDummy119)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy127) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy126) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb055AlphaDummy126) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb055AlphaDummy126))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy128 x y)) (SemanticCore.Class.cv (nb055AlphaDummy121 x y))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy129 x y)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy128 x y)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb055AlphaDummy128 x y)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb055AlphaDummy128 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0018.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0019 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy148, nb055AlphaDummy149 x y), (nb055AlphaDummy122, nb055AlphaDummy123 x y), (nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy148) (SemanticCore.Class.cab nb055AlphaDummy118 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy119 (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy118) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy119)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy148) (SemanticCore.Class.cab nb055AlphaDummy118 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy119 (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy118) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy119)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy149 x y)) (SemanticCore.Class.cab (nb055AlphaDummy120 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy121 x y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy120 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy121 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy149 x y)) (SemanticCore.Class.cab (nb055AlphaDummy120 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy121 x y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy120 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy121 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0019.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0020 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy170, nb055AlphaDummy173 x y), (nb055AlphaDummy169, nb055AlphaDummy172 x y), (nb055AlphaDummy168, nb055AlphaDummy171 x y), (nb055AlphaDummy166, nb055AlphaDummy167 x y), (nb055AlphaDummy162, nb055AlphaDummy164 x y), (nb055AlphaDummy163, nb055AlphaDummy165 x y), (nb055AlphaDummy155, nb055AlphaDummy157 x y), (nb055AlphaDummy154, nb055AlphaDummy156 x y), (nb055AlphaDummy160, nb055AlphaDummy161 x y), (nb055AlphaDummy158, nb055AlphaDummy159 x y), (nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb055AlphaDummy169) (SemanticCore.Class.cv nb055AlphaDummy170)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy168) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb055AlphaDummy169) (SemanticCore.Class.cv nb055AlphaDummy170))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb055AlphaDummy172 x y)) (SemanticCore.Class.cv (nb055AlphaDummy173 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy171 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb055AlphaDummy172 x y)) (SemanticCore.Class.cv (nb055AlphaDummy173 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0020.

Equations

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

Certificates from NAR4C055C001Part012.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0021 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy155, nb055AlphaDummy157 x y), (nb055AlphaDummy154, nb055AlphaDummy156 x y), (nb055AlphaDummy160, nb055AlphaDummy161 x y), (nb055AlphaDummy158, nb055AlphaDummy159 x y), (nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy154) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy155))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy156 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y))))

Checked nominal proof certificate identified upstream as nb055_split_alpha_0021.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0022 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy170, nb055AlphaDummy173 x y), (nb055AlphaDummy169, nb055AlphaDummy172 x y), (nb055AlphaDummy168, nb055AlphaDummy171 x y), (nb055AlphaDummy166, nb055AlphaDummy167 x y), (nb055AlphaDummy162, nb055AlphaDummy164 x y), (nb055AlphaDummy163, nb055AlphaDummy165 x y), (nb055AlphaDummy188, nb055AlphaDummy189 x y), (nb055AlphaDummy186, nb055AlphaDummy187 x y), (nb055AlphaDummy155, nb055AlphaDummy157 x y), (nb055AlphaDummy154, nb055AlphaDummy156 x y), (nb055AlphaDummy184, nb055AlphaDummy185 x y), (nb055AlphaDummy158, nb055AlphaDummy159 x y), (nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv nb055AlphaDummy169) (SemanticCore.Class.cv nb055AlphaDummy170)) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy168) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv nb055AlphaDummy169) (SemanticCore.Class.cv nb055AlphaDummy170))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb055AlphaDummy172 x y)) (SemanticCore.Class.cv (nb055AlphaDummy173 x y))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy171 x y)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb055AlphaDummy172 x y)) (SemanticCore.Class.cv (nb055AlphaDummy173 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0022.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0023 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy162, nb055AlphaDummy164 x y), (nb055AlphaDummy163, nb055AlphaDummy165 x y), (nb055AlphaDummy188, nb055AlphaDummy189 x y), (nb055AlphaDummy186, nb055AlphaDummy187 x y), (nb055AlphaDummy155, nb055AlphaDummy157 x y), (nb055AlphaDummy154, nb055AlphaDummy156 x y), (nb055AlphaDummy184, nb055AlphaDummy185 x y), (nb055AlphaDummy158, nb055AlphaDummy159 x y), (nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy162) (SemanticCore.Class.cv nb055AlphaDummy155)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy163) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy162) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb055AlphaDummy162) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb055AlphaDummy162))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy164 x y)) (SemanticCore.Class.cv (nb055AlphaDummy157 x y))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy165 x y)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy164 x y)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb055AlphaDummy164 x y)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb055AlphaDummy164 x y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0023.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0024 (x y : SemanticCore.Var) : Nominal.TAlphaWff [(nb055AlphaDummy184, nb055AlphaDummy185 x y), (nb055AlphaDummy158, nb055AlphaDummy159 x y), (nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy184) (SemanticCore.Class.cab nb055AlphaDummy154 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy155 (SemanticCore.Class.cv nb055AlphaDummy015) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy154) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy155)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy184) (SemanticCore.Class.cab nb055AlphaDummy154 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy155 (SemanticCore.Class.cv nb055AlphaDummy015) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy154) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy155)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy185 x y)) (SemanticCore.Class.cab (nb055AlphaDummy156 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy157 x y) (SemanticCore.Class.cv (nb055AlphaDummy017 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy156 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy185 x y)) (SemanticCore.Class.cab (nb055AlphaDummy156 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy157 x y) (SemanticCore.Class.cv (nb055AlphaDummy017 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy156 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0024.

Equations

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

Certificates from NAR4C055C001Part013.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055ComposeOccurrence0 (x y : SemanticCore.Var) : Nominal.TAlphaClass [(nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Class.cv nb055AlphaDummy001) (SemanticCore.Class.cv y)

Checked nominal proof certificate identified upstream as nb055_compose_occurrence_0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_compose_occurrence_1 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.TAlphaClass [(nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Class.cv nb055AlphaDummy000) (SemanticCore.Class.cv x)

Checked nominal proof certificate identified upstream as nb055_compose_occurrence_1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0025 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb055AlphaDummy078, nb055AlphaDummy079 x y), (nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb055AlphaDummy014) (SemanticCore.Class.cv nb055AlphaDummy001) (SemanticCore.Class.cv nb055AlphaDummy078)).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Class.cv nb055AlphaDummy000) (SemanticCore.Class.cv nb055AlphaDummy015)).neg) ((Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb055AlphaDummy016 x y)) (SemanticCore.Class.cv y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y))).imp (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Class.cv x) (SemanticCore.Class.cv (nb055AlphaDummy017 x y))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0025.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_compose_occurrence_2 (x y : SemanticCore.Var) : Nominal.TAlphaClass [(nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Class.cv nb055AlphaDummy004) (SemanticCore.Class.cv (nb055AlphaDummy005 x y))

Checked nominal proof certificate identified upstream as nb055_compose_occurrence_2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055ComposeRootOccurrence0 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.TAlphaClass [(nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Class.cv nb055AlphaDummy000) (SemanticCore.Class.cv x)

Checked nominal proof certificate identified upstream as nb055_compose_root_occurrence_0.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_compose_root_occurrence_1 (x y : SemanticCore.Var) : Nominal.TAlphaClass [(nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Class.cv nb055AlphaDummy001) (SemanticCore.Class.cv y)

Checked nominal proof certificate identified upstream as nb055_compose_root_occurrence_1.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055ComposeOccurrence3 (x y : SemanticCore.Var) : Nominal.TAlphaClass [(nb055AlphaDummy015, nb055AlphaDummy017 x y), (nb055AlphaDummy014, nb055AlphaDummy016 x y), (nb055AlphaDummy080, nb055AlphaDummy081 x y), (nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] (SemanticCore.Class.cv nb055AlphaDummy080) (SemanticCore.Class.cv (nb055AlphaDummy081 x y))

Checked nominal proof certificate identified upstream as nb055_compose_occurrence_3.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055SplitAlpha0026 (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb055AlphaDummy002, nb055AlphaDummy003 x y), (nb055AlphaDummy001, y), (nb055AlphaDummy000, x), (nb055AlphaDummy004, nb055AlphaDummy005 x y)] ((SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy004) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb055AlphaDummy000) (SemanticCore.Class.cv nb055AlphaDummy001)) (SemanticCore.Class.cv nb055AlphaDummy002))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy000) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy001) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy002) (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb055AlphaDummy000) (SemanticCore.Class.cv nb055AlphaDummy001)))).neg) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy005 x y)) (Compiler.CompactSourceSyntax.synCop (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) (SemanticCore.Class.cv (nb055AlphaDummy003 x y)))).imp (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) Compiler.CompactSourceSyntax.synCvv) (SemanticCore.Wff.classMem (SemanticCore.Class.cv y) Compiler.CompactSourceSyntax.synCvv)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy003 x y)) (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))).neg)

Checked nominal proof certificate identified upstream as nb055_split_alpha_0026.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfCompose (x y : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCcompose (Compiler.CompactSourceSyntax.synCmpt2 x Compiler.CompactSourceSyntax.synCvv y Compiler.CompactSourceSyntax.synCvv (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))))

Checked nominal proof certificate identified upstream as nominal_df_compose.

Equations

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