NF weak partition development: NAR4C076C001Part013.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076SplitAlpha0007 (g m n a b : SemanticCore.Var) : Nominal.TAlphaWff [(nb076AlphaDummy082, nb076AlphaDummy084 g a b), (nb076AlphaDummy081, nb076AlphaDummy083 g a b), (nb076AlphaDummy111, nb076AlphaDummy112 g a b), (nb076AlphaDummy085, nb076AlphaDummy086 g a b), (nb076AlphaDummy002, g), (nb076AlphaDummy001, b), (nb076AlphaDummy000, a), (nb076AlphaDummy005, nb076AlphaDummy006 g m n a b), (nb076AlphaDummy004, n), (nb076AlphaDummy003, m), (nb076AlphaDummy007, nb076AlphaDummy008 g m n a b)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb076AlphaDummy081) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy082)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb076AlphaDummy083 g a b)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb076AlphaDummy084 g a b))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))

Checked nominal proof certificate identified upstream as nb076_split_alpha_0007.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0418 : nb076AlphaDummy002 ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0419 (g : SemanticCore.Var) : g ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0420 : nb076AlphaDummy001 ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0421 (b : SemanticCore.Var) : b ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0422 : nb076AlphaDummy000 ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0423 (a : SemanticCore.Var) : a ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0424 : nb076AlphaDummy005 ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0425 (g m n a b : SemanticCore.Var) : nb076AlphaDummy006 g m n a b ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0426 : nb076AlphaDummy004 ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0427 (n : SemanticCore.Var) : n ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0428 : nb076AlphaDummy003 ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0429 (m : SemanticCore.Var) : m ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0430 : nb076AlphaDummy007 ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_wpp_notmem_0431 (g m n a b : SemanticCore.Var) : nb076AlphaDummy008 g m n a b ∉ Compiler.CompactSourceSyntax.synCen.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_envfresh_0029 (g m n a b : SemanticCore.Var) : Nominal.TEnvFresh [(nb076AlphaDummy002, g), (nb076AlphaDummy001, b), (nb076AlphaDummy000, a), (nb076AlphaDummy005, nb076AlphaDummy006 g m n a b), (nb076AlphaDummy004, n), (nb076AlphaDummy003, m), (nb076AlphaDummy007, nb076AlphaDummy008 g m n a b)] Compiler.CompactSourceSyntax.synCen.fv