NF weak partition development: NAR4C076C001Part005.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_support_mem_0176 : nb076AlphaDummy002 ∈ (SemanticCore.Class.cab nb076AlphaDummy081 (Compiler.CompactSourceSyntax.synWrex nb076AlphaDummy082 (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv nb076AlphaDummy001) (SemanticCore.Class.cv nb076AlphaDummy002)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb076AlphaDummy081) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy082)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb076AlphaDummy081 (Compiler.CompactSourceSyntax.synWrex nb076AlphaDummy082 (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv nb076AlphaDummy001) (SemanticCore.Class.cv nb076AlphaDummy002)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb076AlphaDummy081) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy082)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_support_mem_0177 (g a b : SemanticCore.Var) : g ∈ (SemanticCore.Class.cab (nb076AlphaDummy083 g a b) (Compiler.CompactSourceSyntax.synWrex (nb076AlphaDummy084 g a b) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv b) (SemanticCore.Class.cv g)) (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))))).fv ∪ (SemanticCore.Class.cab (nb076AlphaDummy083 g a b) (Compiler.CompactSourceSyntax.synWrex (nb076AlphaDummy084 g a b) (Compiler.CompactSourceSyntax.synCxp (SemanticCore.Class.cv b) (SemanticCore.Class.cv g)) (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))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_support_mem_0178 : nb076AlphaDummy002 ∈ {nb076AlphaDummy113} ∪ {nb076AlphaDummy114} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb076AlphaDummy113) (SemanticCore.Class.cv nb076AlphaDummy001)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb076AlphaDummy114) (SemanticCore.Class.cv nb076AlphaDummy002))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_support_mem_0179 (g b : SemanticCore.Var) : g ∈ {nb076AlphaDummy115 g b} ∪ {nb076AlphaDummy116 g b} ∪ (Compiler.CompactSourceSyntax.synWa (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb076AlphaDummy115 g b)) (SemanticCore.Class.cv b)) (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb076AlphaDummy116 g b)) (SemanticCore.Class.cv g))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_support_mem_0180 : nb076AlphaDummy002 ∈ (SemanticCore.Class.cv nb076AlphaDummy001).fv ∪ (SemanticCore.Class.cv nb076AlphaDummy002).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_support_mem_0181 (g b : SemanticCore.Var) : g ∈ (SemanticCore.Class.cv b).fv ∪ (SemanticCore.Class.cv g).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_support_mem_0182 : nb076AlphaDummy082 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy082))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_support_mem_0183 (g a b : SemanticCore.Var) : nb076AlphaDummy084 g a b ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb076AlphaDummy084 g a b)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_support_mem_0184 : nb076AlphaDummy082 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy082)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb076AlphaDummy082)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_support_mem_0185 (g a b : SemanticCore.Var) : nb076AlphaDummy084 g a b ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb076AlphaDummy084 g a b))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb076AlphaDummy084 g a b))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0028 : nb076AlphaDummy005 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0029 (g m n a b : SemanticCore.Var) : nb076AlphaDummy006 g m n a b ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0030 : nb076AlphaDummy004 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0031 (n : SemanticCore.Var) : n ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0032 : nb076AlphaDummy003 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0033 (m : SemanticCore.Var) : m ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0034 : nb076AlphaDummy007 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb076_compact_fv_empty_0035 (g m n a b : SemanticCore.Var) : nb076AlphaDummy008 g m n a b ∉ ∅