NF weak partition development: NAR4H5C095M3Part045.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0099 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy379 D R S_cls E, nb095AlphaDummy380 u S_cls), (nb095AlphaDummy377 D R S_cls E, nb095AlphaDummy378 u S_cls), (nb095AlphaDummy346 D R S_cls E, nb095AlphaDummy348 u S_cls), (nb095AlphaDummy345 D R S_cls E, nb095AlphaDummy347 u S_cls), (nb095AlphaDummy375 D R S_cls E, nb095AlphaDummy376 u S_cls), (nb095AlphaDummy349 D R S_cls E, nb095AlphaDummy350 u S_cls), (nb095AlphaDummy340 D R S_cls E, nb095AlphaDummy342 u S_cls), (nb095AlphaDummy339 D R S_cls E, nb095AlphaDummy341 u S_cls), (nb095AlphaDummy337 D R S_cls E, nb095AlphaDummy338 u S_cls E), (nb095AlphaDummy335 D R S_cls E, nb095AlphaDummy336 u S_cls E), (nb095AlphaDummy794 D R S_cls E, nb095AlphaDummy796 u S_cls E), (nb095AlphaDummy793 D R S_cls E, nb095AlphaDummy795 u S_cls E), (nb095AlphaDummy797 D R S_cls E, nb095AlphaDummy798 u S_cls E), (nb095AlphaDummy791 D R S_cls E, nb095AlphaDummy792 u S_cls E), (nb095AlphaDummy789 D R S_cls E, nb095AlphaDummy790 u S_cls E), (nb095AlphaDummy004 D R S_cls E, nb095AlphaDummy006 x u D R S_cls f E), (nb095AlphaDummy003 D R S_cls E, nb095AlphaDummy005 x u D R S_cls f E), (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 (nb095AlphaDummy379 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy379 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy380 u S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy380 u S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls)))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0099.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0094 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy794 D R S_cls E ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2160 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy794 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0095 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy796 u S_cls E ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2161 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy796 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0096 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy793 D R S_cls E ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2162 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy793 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0097 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy795 u S_cls E ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2163 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy795 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0098 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy797 D R S_cls E ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2164 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy797 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0099 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy798 u S_cls E ∉ S_cls.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2165 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy798 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2166 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy791 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2167 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy792 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2168 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy789 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2169 (u : SemanticCore.Var) (S_cls E : SemanticCore.Class) : nb095AlphaDummy790 u S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2170 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy004 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2171 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy006 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2172 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy003 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_2173 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy005 x u D R S_cls f E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_envfresh_0344 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_S_f : f ∉ S_cls.fv) (dv_S_u : u ∉ S_cls.fv) (dv_S_x : x ∉ S_cls.fv) : Nominal.TEnvFresh [(nb095AlphaDummy340 D R S_cls E, nb095AlphaDummy342 u S_cls), (nb095AlphaDummy339 D R S_cls E, nb095AlphaDummy341 u S_cls), (nb095AlphaDummy337 D R S_cls E, nb095AlphaDummy338 u S_cls E), (nb095AlphaDummy335 D R S_cls E, nb095AlphaDummy336 u S_cls E), (nb095AlphaDummy794 D R S_cls E, nb095AlphaDummy796 u S_cls E), (nb095AlphaDummy793 D R S_cls E, nb095AlphaDummy795 u S_cls E), (nb095AlphaDummy797 D R S_cls E, nb095AlphaDummy798 u S_cls E), (nb095AlphaDummy791 D R S_cls E, nb095AlphaDummy792 u S_cls E), (nb095AlphaDummy789 D R S_cls E, nb095AlphaDummy790 u S_cls E), (nb095AlphaDummy004 D R S_cls E, nb095AlphaDummy006 x u D R S_cls f E), (nb095AlphaDummy003 D R S_cls E, nb095AlphaDummy005 x u D R S_cls f E), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv