NF weak partition development: NAR4H5C095M3Part020.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0032 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy351 D R S_cls E, nb095AlphaDummy352 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), (nb095AlphaDummy293 D R S_cls E, nb095AlphaDummy294 u S_cls f E), (nb095AlphaDummy291 D R S_cls E, nb095AlphaDummy292 u 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 (nb095AlphaDummy351 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy345 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy346 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy340 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy345 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy351 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy345 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy346 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy340 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy345 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy352 u S_cls)) (SemanticCore.Class.cab (nb095AlphaDummy347 u S_cls) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy348 u S_cls) (SemanticCore.Class.cv (nb095AlphaDummy342 u S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy347 u S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy352 u S_cls)) (SemanticCore.Class.cab (nb095AlphaDummy347 u S_cls) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy348 u S_cls) (SemanticCore.Class.cv (nb095AlphaDummy342 u S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy347 u S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0032.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0033 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(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), (nb095AlphaDummy293 D R S_cls E, nb095AlphaDummy294 u S_cls f E), (nb095AlphaDummy291 D R S_cls E, nb095AlphaDummy292 u 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 (nb095AlphaDummy377 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E))))) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy378 u S_cls)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls)))))

Checked nominal proof certificate identified upstream as nb095_split_alpha_0033.

Equations

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0030 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) : nb095AlphaDummy342 u S_cls ∉ S_cls.fv

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0032 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) : nb095AlphaDummy341 u S_cls ∉ S_cls.fv

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

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

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

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

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

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

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0038 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy294 u S_cls f E ∉ S_cls.fv

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0040 (u : SemanticCore.Var) (S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy292 u S_cls f E ∉ S_cls.fv

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

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_1003 (x : SemanticCore.Var) (S_cls : SemanticCore.Class) (dv_S_x : x ∉ S_cls.fv) : x ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_1005 (S_cls : SemanticCore.Class) (f : SemanticCore.Var) (dv_S_f : f ∉ S_cls.fv) : f ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif S_cls Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_envfresh_0120 (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), (nb095AlphaDummy293 D R S_cls E, nb095AlphaDummy294 u S_cls f E), (nb095AlphaDummy291 D R S_cls E, nb095AlphaDummy292 u 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