NF weak partition development: NAR4H5C093M3Part005.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093SplitAlpha0007 (A : SemanticCore.Class) (r d : SemanticCore.Var) (dv_d_r : d ≠ r) : Nominal.TAlphaWff [(nb093AlphaDummy050 A, nb093AlphaDummy051 r d), (nb093AlphaDummy048 A, nb093AlphaDummy049 r d), (nb093AlphaDummy000 A, d), (nb093AlphaDummy001 A, r), (nb093AlphaDummy006 A, nb093AlphaDummy007 r d), (nb093AlphaDummy004 A, nb093AlphaDummy005 A r d), (nb093AlphaDummy002 A, nb093AlphaDummy003 A r d)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy050 A)) (SemanticCore.Class.cab (nb093AlphaDummy044 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy045 A) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv (nb093AlphaDummy001 A)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb093AlphaDummy001 A)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy044 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy045 A))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy050 A)) (SemanticCore.Class.cab (nb093AlphaDummy044 A) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy045 A) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv (nb093AlphaDummy001 A)) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv (nb093AlphaDummy001 A)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy044 A)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy045 A))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy051 r d)) (SemanticCore.Class.cab (nb093AlphaDummy046 r d) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy047 r d) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy046 r d)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy047 r d))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy051 r d)) (SemanticCore.Class.cab (nb093AlphaDummy046 r d) (Compiler.CompactSourceSyntax.synWrex (nb093AlphaDummy047 r d) (Compiler.CompactSourceSyntax.synCdif (SemanticCore.Class.cv r) (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv r))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy046 r d)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy047 r d))))))).neg)

Checked nominal proof certificate identified upstream as nb093_split_alpha_0007.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093SplitAlpha0008 (A : SemanticCore.Class) (r d : SemanticCore.Var) : Nominal.TAlphaWff [(nb093AlphaDummy045 A, nb093AlphaDummy047 r d), (nb093AlphaDummy044 A, nb093AlphaDummy046 r d), (nb093AlphaDummy158 A, nb093AlphaDummy159 r d), (nb093AlphaDummy048 A, nb093AlphaDummy049 r d), (nb093AlphaDummy000 A, d), (nb093AlphaDummy001 A, r), (nb093AlphaDummy006 A, nb093AlphaDummy007 r d), (nb093AlphaDummy004 A, nb093AlphaDummy005 A r d), (nb093AlphaDummy002 A, nb093AlphaDummy003 A r d)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy045 A)) (SemanticCore.Class.cv (nb093AlphaDummy000 A))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy044 A)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy045 A))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb093AlphaDummy047 r d)) (SemanticCore.Class.cv d)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb093AlphaDummy046 r d)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb093AlphaDummy047 r d))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb093_split_alpha_0008.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0422 (A : SemanticCore.Class) : nb093AlphaDummy000 A ∉ Compiler.CompactSourceSyntax.synCfound.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0423 (d : SemanticCore.Var) : d ∉ Compiler.CompactSourceSyntax.synCfound.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0424 (A : SemanticCore.Class) : nb093AlphaDummy001 A ∉ Compiler.CompactSourceSyntax.synCfound.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0425 (r : SemanticCore.Var) : r ∉ Compiler.CompactSourceSyntax.synCfound.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0426 (A : SemanticCore.Class) : nb093AlphaDummy006 A ∉ Compiler.CompactSourceSyntax.synCfound.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0427 (r d : SemanticCore.Var) : nb093AlphaDummy007 r d ∉ Compiler.CompactSourceSyntax.synCfound.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0428 (A : SemanticCore.Class) : nb093AlphaDummy004 A ∉ Compiler.CompactSourceSyntax.synCfound.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0429 (A : SemanticCore.Class) (r d : SemanticCore.Var) : nb093AlphaDummy005 A r d ∉ Compiler.CompactSourceSyntax.synCfound.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0430 (A : SemanticCore.Class) : nb093AlphaDummy002 A ∉ Compiler.CompactSourceSyntax.synCfound.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_wpp_notmem_0431 (A : SemanticCore.Class) (r d : SemanticCore.Var) : nb093AlphaDummy003 A r d ∉ Compiler.CompactSourceSyntax.synCfound.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb093_compact_envfresh_0029 (A : SemanticCore.Class) (r d : SemanticCore.Var) : Nominal.TEnvFresh [(nb093AlphaDummy000 A, d), (nb093AlphaDummy001 A, r), (nb093AlphaDummy006 A, nb093AlphaDummy007 r d), (nb093AlphaDummy004 A, nb093AlphaDummy005 A r d), (nb093AlphaDummy002 A, nb093AlphaDummy003 A r d)] Compiler.CompactSourceSyntax.synCfound.fv