NF weak partition development: NAR4C059C001Part005.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059SplitAlpha0007 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) : Nominal.TAlphaWff [(nb059AlphaDummy018 R S_cls, nb059AlphaDummy020 R a), (nb059AlphaDummy017 R S_cls, nb059AlphaDummy019 R a), (nb059AlphaDummy023 R S_cls, nb059AlphaDummy024 R a), (nb059AlphaDummy021 R S_cls, nb059AlphaDummy022 R a), (nb059AlphaDummy014 R S_cls, nb059AlphaDummy016 R a), (nb059AlphaDummy013 R S_cls, nb059AlphaDummy015 R a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls)) (SemanticCore.Class.cv (nb059AlphaDummy014 R S_cls))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy017 R S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy020 R a)) (SemanticCore.Class.cv (nb059AlphaDummy016 R a))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy019 R a)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy020 R a)))).neg)

Checked nominal proof certificate identified upstream as nb059_split_alpha_0007.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059SplitAlpha0008 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) : Nominal.TAlphaWff [(nb059AlphaDummy033 R S_cls, nb059AlphaDummy036 R a), (nb059AlphaDummy032 R S_cls, nb059AlphaDummy035 R a), (nb059AlphaDummy031 R S_cls, nb059AlphaDummy034 R a), (nb059AlphaDummy029 R S_cls, nb059AlphaDummy030 R a), (nb059AlphaDummy025 R S_cls, nb059AlphaDummy027 R a), (nb059AlphaDummy026 R S_cls, nb059AlphaDummy028 R a), (nb059AlphaDummy051 R S_cls, nb059AlphaDummy052 R a), (nb059AlphaDummy049 R S_cls, nb059AlphaDummy050 R a), (nb059AlphaDummy018 R S_cls, nb059AlphaDummy020 R a), (nb059AlphaDummy017 R S_cls, nb059AlphaDummy019 R a), (nb059AlphaDummy047 R S_cls, nb059AlphaDummy048 R a), (nb059AlphaDummy021 R S_cls, nb059AlphaDummy022 R a), (nb059AlphaDummy014 R S_cls, nb059AlphaDummy016 R a), (nb059AlphaDummy013 R S_cls, nb059AlphaDummy015 R a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb059AlphaDummy032 R S_cls)) (SemanticCore.Class.cv (nb059AlphaDummy033 R S_cls))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy031 R S_cls)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb059AlphaDummy032 R S_cls)) (SemanticCore.Class.cv (nb059AlphaDummy033 R S_cls)))).neg) ((SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCin (SemanticCore.Class.cv (nb059AlphaDummy035 R a)) (SemanticCore.Class.cv (nb059AlphaDummy036 R a))) Compiler.CompactSourceSyntax.synC0).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy034 R a)) (Compiler.CompactSourceSyntax.synCun (SemanticCore.Class.cv (nb059AlphaDummy035 R a)) (SemanticCore.Class.cv (nb059AlphaDummy036 R a)))).neg)

Checked nominal proof certificate identified upstream as nb059_split_alpha_0008.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059SplitAlpha0009 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) : Nominal.TAlphaWff [(nb059AlphaDummy025 R S_cls, nb059AlphaDummy027 R a), (nb059AlphaDummy026 R S_cls, nb059AlphaDummy028 R a), (nb059AlphaDummy051 R S_cls, nb059AlphaDummy052 R a), (nb059AlphaDummy049 R S_cls, nb059AlphaDummy050 R a), (nb059AlphaDummy018 R S_cls, nb059AlphaDummy020 R a), (nb059AlphaDummy017 R S_cls, nb059AlphaDummy019 R a), (nb059AlphaDummy047 R S_cls, nb059AlphaDummy048 R a), (nb059AlphaDummy021 R S_cls, nb059AlphaDummy022 R a), (nb059AlphaDummy014 R S_cls, nb059AlphaDummy016 R a), (nb059AlphaDummy013 R S_cls, nb059AlphaDummy015 R a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy025 R S_cls)) (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy026 R S_cls)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy025 R S_cls)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb059AlphaDummy025 R S_cls)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb059AlphaDummy025 R S_cls)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy027 R a)) (SemanticCore.Class.cv (nb059AlphaDummy020 R a))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy028 R a)) (Compiler.CompactSourceSyntax.synCif (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy027 R a)) Compiler.CompactSourceSyntax.synCnnc) (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb059AlphaDummy027 R a)) Compiler.CompactSourceSyntax.synC1c) (SemanticCore.Class.cv (nb059AlphaDummy027 R a)))).neg)

Checked nominal proof certificate identified upstream as nb059_split_alpha_0009.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059SplitAlpha0010 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) : Nominal.TAlphaWff [(nb059AlphaDummy047 R S_cls, nb059AlphaDummy048 R a), (nb059AlphaDummy021 R S_cls, nb059AlphaDummy022 R a), (nb059AlphaDummy014 R S_cls, nb059AlphaDummy016 R a), (nb059AlphaDummy013 R S_cls, nb059AlphaDummy015 R a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy047 R S_cls)) (SemanticCore.Class.cab (nb059AlphaDummy017 R S_cls) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy018 R S_cls) (SemanticCore.Class.cv (nb059AlphaDummy013 R S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy017 R S_cls)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy047 R S_cls)) (SemanticCore.Class.cab (nb059AlphaDummy017 R S_cls) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy018 R S_cls) (SemanticCore.Class.cv (nb059AlphaDummy013 R S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy017 R S_cls)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy018 R S_cls))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy048 R a)) (SemanticCore.Class.cab (nb059AlphaDummy019 R a) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy020 R a) (SemanticCore.Class.cv (nb059AlphaDummy015 R a)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy019 R a)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy020 R a))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb059AlphaDummy048 R a)) (SemanticCore.Class.cab (nb059AlphaDummy019 R a) (Compiler.CompactSourceSyntax.synWrex (nb059AlphaDummy020 R a) (SemanticCore.Class.cv (nb059AlphaDummy015 R a)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb059AlphaDummy019 R a)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb059AlphaDummy020 R a))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb059_split_alpha_0010.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_compact_envfresh_0017 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_R_a : a ∉ R.fv) : Nominal.TEnvFresh [(nb059AlphaDummy014 R S_cls, nb059AlphaDummy016 R a), (nb059AlphaDummy013 R S_cls, nb059AlphaDummy015 R a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] R.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059WppRefl0017 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_R_a : a ∉ R.fv) : Nominal.TReflOn [(nb059AlphaDummy014 R S_cls, nb059AlphaDummy016 R a), (nb059AlphaDummy013 R S_cls, nb059AlphaDummy015 R a), (nb059AlphaDummy000 R S_cls, a), (nb059AlphaDummy002 R S_cls, nb059AlphaDummy004 R S_cls a), (nb059AlphaDummy001 R S_cls, nb059AlphaDummy003 R S_cls a)] R.fv

Checked nominal proof certificate identified upstream as nb059_wpp_refl_0017.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059WppRefl0017 R S_cls a dv_R_a = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfClos1 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_R_a : a ∉ R.fv) (dv_S_a : a ∉ S_cls.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCclos1 S_cls R) (Compiler.CompactSourceSyntax.synCint (SemanticCore.Class.cab a (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss S_cls (SemanticCore.Class.cv a)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCima R (SemanticCore.Class.cv a)) (SemanticCore.Class.cv a))))))

Checked nominal proof certificate identified upstream as nominal_df_clos1.

Equations

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