NF weak partition development: NAR4H5C095M3Part012.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0008 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy175 D R S_cls E, nb095AlphaDummy176 f), (nb095AlphaDummy173 D R S_cls E, nb095AlphaDummy174 f), (nb095AlphaDummy013 D R S_cls E, nb095AlphaDummy016 f), (nb095AlphaDummy012 D R S_cls E, nb095AlphaDummy015 f), (nb095AlphaDummy011 D R S_cls E, nb095AlphaDummy014 f), (nb095AlphaDummy017 D R S_cls E, nb095AlphaDummy018 f), (nb095AlphaDummy009 D R S_cls E, nb095AlphaDummy010 f), (nb095AlphaDummy007 D R S_cls E, nb095AlphaDummy008 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy175 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy175 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy169 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy170 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy169 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy176 f)) (SemanticCore.Class.cab (nb095AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy172 f) (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy176 f)) (SemanticCore.Class.cab (nb095AlphaDummy171 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy172 f) (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy171 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0008.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0009 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy201 D R S_cls E, nb095AlphaDummy202 f), (nb095AlphaDummy170 D R S_cls E, nb095AlphaDummy172 f), (nb095AlphaDummy169 D R S_cls E, nb095AlphaDummy171 f), (nb095AlphaDummy199 D R S_cls E, nb095AlphaDummy200 f), (nb095AlphaDummy173 D R S_cls E, nb095AlphaDummy174 f), (nb095AlphaDummy013 D R S_cls E, nb095AlphaDummy016 f), (nb095AlphaDummy012 D R S_cls E, nb095AlphaDummy015 f), (nb095AlphaDummy011 D R S_cls E, nb095AlphaDummy014 f), (nb095AlphaDummy017 D R S_cls E, nb095AlphaDummy018 f), (nb095AlphaDummy009 D R S_cls E, nb095AlphaDummy010 f), (nb095AlphaDummy007 D R S_cls E, nb095AlphaDummy008 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy201 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy170 D R S_cls E))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy202 f)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy172 f)))))

Checked nominal proof certificate identified upstream as nb095_split_alpha_0009.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0010 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_f_u : f ≠ u) (dv_f_x : f ≠ x) : Nominal.TAlphaWff [(nb095AlphaDummy012 D R S_cls E, nb095AlphaDummy015 f), (nb095AlphaDummy011 D R S_cls E, nb095AlphaDummy014 f), (nb095AlphaDummy017 D R S_cls E, nb095AlphaDummy018 f), (nb095AlphaDummy009 D R S_cls E, nb095AlphaDummy010 f), (nb095AlphaDummy007 D R S_cls E, nb095AlphaDummy008 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy017 D R S_cls E)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E)))).imp (Compiler.CompactSourceSyntax.synWex (nb095AlphaDummy013 D R S_cls E) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy011 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E))) (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy013 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy000 D R S_cls E)) (SemanticCore.Class.cv (nb095AlphaDummy012 D R S_cls E))))).neg) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy018 f)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb095AlphaDummy014 f)) (SemanticCore.Class.cv (nb095AlphaDummy015 f)))).imp (Compiler.CompactSourceSyntax.synWex (nb095AlphaDummy016 f) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy014 f)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)) (SemanticCore.Class.cv (nb095AlphaDummy016 f))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb095AlphaDummy016 f)) (SemanticCore.Class.cv f) (SemanticCore.Class.cv (nb095AlphaDummy015 f))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0010.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0506 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy009 D R S_cls E ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0507 (f : SemanticCore.Var) : nb095AlphaDummy010 f ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0508 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy007 D R S_cls E ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0509 (f : SemanticCore.Var) : nb095AlphaDummy008 f ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0510 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy001 D R S_cls E ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0511 (u : SemanticCore.Var) : u ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0512 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy002 D R S_cls E ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0513 (x : SemanticCore.Var) : x ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0514 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy000 D R S_cls E ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_0515 (f : SemanticCore.Var) : f ∉ Compiler.CompactSourceSyntax.synCid.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_envfresh_0037 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TEnvFresh [(nb095AlphaDummy009 D R S_cls E, nb095AlphaDummy010 f), (nb095AlphaDummy007 D R S_cls E, nb095AlphaDummy008 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] Compiler.CompactSourceSyntax.synCid.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095WppRefl0035 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TReflOn [(nb095AlphaDummy009 D R S_cls E, nb095AlphaDummy010 f), (nb095AlphaDummy007 D R S_cls E, nb095AlphaDummy008 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] Compiler.CompactSourceSyntax.synCid.fv

Checked nominal proof certificate identified upstream as nb095_wpp_refl_0035.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095WppRefl0035 x u D R S_cls f E = ⋯.reflOn