Nominal proof certificates grouped in dependency order.

Certificates from NAR4C056C001Part013.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056WppRefl0035 (f : SemanticCore.Var) : Nominal.TReflOn [(nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] Compiler.CompactSourceSyntax.synCid.fv

Checked nominal proof certificate identified upstream as nb056_wpp_refl_0035.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056WppRefl0035 f = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056ComposeBinderOccurrence (f : SemanticCore.Var) : Nominal.TAlphaClass [(nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy003, nb056AlphaDummy004 f), (nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] (SemanticCore.Class.cv nb056AlphaDummy011) (SemanticCore.Class.cv (nb056AlphaDummy012 f))

Checked nominal proof certificate identified upstream as nb056_compose_binder_occurrence.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0027 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy001, nb056AlphaDummy002 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy001) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb056AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb056AlphaDummy000))) Compiler.CompactSourceSyntax.synCid)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy001) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv nb056AlphaDummy000) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb056AlphaDummy000))) Compiler.CompactSourceSyntax.synCid)).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy002 f)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid)).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy002 f)) (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCcom (SemanticCore.Class.cv f) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f))) Compiler.CompactSourceSyntax.synCid)).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0027.

Equations

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

Certificates from NAR4C056C001Part014.

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0029 (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), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy014) (SemanticCore.Class.cv nb056AlphaDummy005)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy013) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy014))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy016 f)) (SemanticCore.Class.cv (nb056AlphaDummy008 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy015 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy016 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0029.

Equations

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

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0031 (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), (nb056AlphaDummy000, f)] (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy021) (SemanticCore.Class.cv nb056AlphaDummy014)) (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 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy023 f)) (SemanticCore.Class.cv (nb056AlphaDummy016 f))) (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_0031.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0032 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy017, nb056AlphaDummy018 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy017) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb056AlphaDummy013 (Compiler.CompactSourceSyntax.synWrex nb056AlphaDummy014 (SemanticCore.Class.cv nb056AlphaDummy005) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy013) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy014))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy017) (Compiler.CompactSourceSyntax.synCcompl (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 (nb056AlphaDummy018 f)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb056AlphaDummy015 f) (Compiler.CompactSourceSyntax.synWrex (nb056AlphaDummy016 f) (SemanticCore.Class.cv (nb056AlphaDummy008 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy015 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy016 f)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy018 f)) (Compiler.CompactSourceSyntax.synCcompl (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_0032.

Equations

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

Certificates from NAR4C056C001Part015.

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0034 (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), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy050) (SemanticCore.Class.cv nb056AlphaDummy005)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy049) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy050))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy052 f)) (SemanticCore.Class.cv (nb056AlphaDummy008 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy051 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy052 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0034.

Equations

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

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

Equations

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

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0037 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy079, nb056AlphaDummy080 f), (nb056AlphaDummy053, nb056AlphaDummy054 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 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_0037.

Equations

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

Certificates from NAR4C056C001Part016.

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0039 (f : SemanticCore.Var) : Nominal.TAlphaWff [(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), (nb056AlphaDummy000, f)] (SemanticCore.Wff.all nb056AlphaDummy099 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy099) (SemanticCore.Class.cv nb056AlphaDummy092)) (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).neg (SemanticCore.Wff.all (nb056AlphaDummy101 f) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy101 f)) (SemanticCore.Class.cv (nb056AlphaDummy094 f))) (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).neg

Checked nominal proof certificate identified upstream as nb056_split_alpha_0039.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

Certificates from NAR4C056C001Part017.

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0044 (f : SemanticCore.Var) : Nominal.TAlphaWff [(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), (nb056AlphaDummy000, f)] (SemanticCore.Wff.all nb056AlphaDummy135 (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy135) (SemanticCore.Class.cv nb056AlphaDummy128)) (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).neg (SemanticCore.Wff.all (nb056AlphaDummy137 f) (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy137 f)) (SemanticCore.Class.cv (nb056AlphaDummy130 f))) (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).neg

Checked nominal proof certificate identified upstream as nb056_split_alpha_0044.

Equations

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

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

Equations

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

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

Equations

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

Certificates from NAR4C056C001Part018.

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056DirectVariableOccurrence (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), (nb056AlphaDummy000, f)] (SemanticCore.Class.cv nb056AlphaDummy000) (SemanticCore.Class.cv f)

Checked nominal proof certificate identified upstream as nb056_direct_variable_occurrence.

Equations

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

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

Equations

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

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

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0050 (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), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy164) (SemanticCore.Class.cv nb056AlphaDummy007)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy163) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy164))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy166 f)) (SemanticCore.Class.cv (nb056AlphaDummy010 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy165 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy166 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0050.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0051 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy179, nb056AlphaDummy182 f), (nb056AlphaDummy178, nb056AlphaDummy181 f), (nb056AlphaDummy177, nb056AlphaDummy180 f), (nb056AlphaDummy175, nb056AlphaDummy176 f), (nb056AlphaDummy171, nb056AlphaDummy173 f), (nb056AlphaDummy172, nb056AlphaDummy174 f), (nb056AlphaDummy197, nb056AlphaDummy198 f), (nb056AlphaDummy195, nb056AlphaDummy196 f), (nb056AlphaDummy164, nb056AlphaDummy166 f), (nb056AlphaDummy163, nb056AlphaDummy165 f), (nb056AlphaDummy193, nb056AlphaDummy194 f), (nb056AlphaDummy167, nb056AlphaDummy168 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 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_0051.

Equations

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

Certificates from NAR4C056C001Part019.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0052 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy171, nb056AlphaDummy173 f), (nb056AlphaDummy172, nb056AlphaDummy174 f), (nb056AlphaDummy197, nb056AlphaDummy198 f), (nb056AlphaDummy195, nb056AlphaDummy196 f), (nb056AlphaDummy164, nb056AlphaDummy166 f), (nb056AlphaDummy163, nb056AlphaDummy165 f), (nb056AlphaDummy193, nb056AlphaDummy194 f), (nb056AlphaDummy167, nb056AlphaDummy168 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy171) (SemanticCore.Class.cv nb056AlphaDummy164)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy172) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy171) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb056AlphaDummy171) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv nb056AlphaDummy171))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy173 f)) (SemanticCore.Class.cv (nb056AlphaDummy166 f))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy174 f)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy173 f)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb056AlphaDummy173 f)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb056AlphaDummy173 f)))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0052.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056SplitAlpha0053 (f : SemanticCore.Var) : Nominal.TAlphaWff [(nb056AlphaDummy193, nb056AlphaDummy194 f), (nb056AlphaDummy167, nb056AlphaDummy168 f), (nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy000, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy193) (SemanticCore.Class.cab nb056AlphaDummy163 (Compiler.CompactSourceSyntax.synWrex nb056AlphaDummy164 (SemanticCore.Class.cv nb056AlphaDummy006) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy163) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy164)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb056AlphaDummy193) (SemanticCore.Class.cab nb056AlphaDummy163 (Compiler.CompactSourceSyntax.synWrex nb056AlphaDummy164 (SemanticCore.Class.cv nb056AlphaDummy006) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb056AlphaDummy163) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb056AlphaDummy164)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy194 f)) (SemanticCore.Class.cab (nb056AlphaDummy165 f) (Compiler.CompactSourceSyntax.synWrex (nb056AlphaDummy166 f) (SemanticCore.Class.cv (nb056AlphaDummy009 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy165 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy166 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb056AlphaDummy194 f)) (SemanticCore.Class.cab (nb056AlphaDummy165 f) (Compiler.CompactSourceSyntax.synWrex (nb056AlphaDummy166 f) (SemanticCore.Class.cv (nb056AlphaDummy009 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb056AlphaDummy165 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb056AlphaDummy166 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb056_split_alpha_0053.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056FunctionBinderOccurrence (f : SemanticCore.Var) : Nominal.TAlphaClass [(nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy000, f)] (SemanticCore.Class.cv nb056AlphaDummy011) (SemanticCore.Class.cv (nb056AlphaDummy012 f))

Checked nominal proof certificate identified upstream as nb056_function_binder_occurrence.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb056FunctionVariableOccurrence (f : SemanticCore.Var) : Nominal.TAlphaClass [(nb056AlphaDummy007, nb056AlphaDummy010 f), (nb056AlphaDummy006, nb056AlphaDummy009 f), (nb056AlphaDummy005, nb056AlphaDummy008 f), (nb056AlphaDummy011, nb056AlphaDummy012 f), (nb056AlphaDummy000, f)] (SemanticCore.Class.cv nb056AlphaDummy000) (SemanticCore.Class.cv f)

Checked nominal proof certificate identified upstream as nb056_function_variable_occurrence.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFuns (f : SemanticCore.Var) : Nominal.NPrf (SemanticCore.Wff.classEq Compiler.CompactSourceSyntax.synCfuns (SemanticCore.Class.cab f (Compiler.CompactSourceSyntax.synWfun (SemanticCore.Class.cv f))))

Checked nominal proof certificate identified upstream as nominal_df_funs.

Equations

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