NF weak partition development: NAR4C059C001Part004.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059SplitAlpha0004 (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), (nb059AlphaDummy011 R S_cls, nb059AlphaDummy012 R a), (nb059AlphaDummy009 R S_cls, nb059AlphaDummy010 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_0004.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0009 (R S_cls : SemanticCore.Class) : nb059AlphaDummy014 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0148 (R S_cls : SemanticCore.Class) : nb059AlphaDummy014 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0010 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy016 R a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0149 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy016 R a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0011 (R S_cls : SemanticCore.Class) : nb059AlphaDummy013 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0150 (R S_cls : SemanticCore.Class) : nb059AlphaDummy013 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0012 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy015 R a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0151 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy015 R a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0013 (R S_cls : SemanticCore.Class) : nb059AlphaDummy011 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0152 (R S_cls : SemanticCore.Class) : nb059AlphaDummy011 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0014 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy012 R a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0153 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy012 R a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_relation_support (R : SemanticCore.Class) (a : SemanticCore.Var) {u : SemanticCore.Var} (hu : u ∈ R.fv) : u ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima R (SemanticCore.Class.cv a)) (SemanticCore.Class.cv a)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_predicate_support (R S : SemanticCore.Class) (a : SemanticCore.Var) (ha : a ∉ R.fv) {u : SemanticCore.Var} (hu : u ∈ R.fv) : u ∈ (SemanticCore.Class.cab a (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWss S (SemanticCore.Class.cv a)) (Compiler.CompactSourceSyntax.synWss (Compiler.CompactSourceSyntax.synCima R (SemanticCore.Class.cv a)) (SemanticCore.Class.cv a)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_fresh_relation (R : SemanticCore.Class) (a : SemanticCore.Var) (offset : ℕ) : ReplaySupport.freshVar ((Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima R (SemanticCore.Class.cv a)) (SemanticCore.Class.cv a)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCima R (SemanticCore.Class.cv a)) (SemanticCore.Class.cv a)).fv) offset ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0015 (R S_cls : SemanticCore.Class) : nb059AlphaDummy009 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0154 (R S_cls : SemanticCore.Class) : nb059AlphaDummy009 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0016 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy010 R a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0155 (R : SemanticCore.Class) (a : SemanticCore.Var) : nb059AlphaDummy010 R a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0017 (R S_cls : SemanticCore.Class) : nb059AlphaDummy000 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0156 (R S_cls : SemanticCore.Class) : nb059AlphaDummy000 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0157 (R : SemanticCore.Class) (a : SemanticCore.Var) (dv_R_a : a ∉ R.fv) : a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0018 (R S_cls : SemanticCore.Class) : nb059AlphaDummy002 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0158 (R S_cls : SemanticCore.Class) : nb059AlphaDummy002 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0019 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_R_a : a ∉ R.fv) : nb059AlphaDummy004 R S_cls a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0159 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_R_a : a ∉ R.fv) : nb059AlphaDummy004 R S_cls a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0020 (R S_cls : SemanticCore.Class) : nb059AlphaDummy001 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0160 (R S_cls : SemanticCore.Class) : nb059AlphaDummy001 R S_cls ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_focused_notmem_0021 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_R_a : a ∉ R.fv) : nb059AlphaDummy003 R S_cls a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_wpp_notmem_0161 (R S_cls : SemanticCore.Class) (a : SemanticCore.Var) (dv_R_a : a ∉ R.fv) : nb059AlphaDummy003 R S_cls a ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb059_compact_envfresh_0009 (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), (nb059AlphaDummy011 R S_cls, nb059AlphaDummy012 R a), (nb059AlphaDummy009 R S_cls, nb059AlphaDummy010 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