NF weak partition development: NAR4C058C001Part002.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0028 : nb058AlphaDummy020 ∈ (SemanticCore.Class.cv nb058AlphaDummy020).fv ∪ (SemanticCore.Class.cv nb058AlphaDummy020).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0029 (x : SemanticCore.Var) : nb058AlphaDummy023 x ∈ (SemanticCore.Class.cv (nb058AlphaDummy023 x)).fv ∪ (SemanticCore.Class.cv (nb058AlphaDummy023 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0030 : nb058AlphaDummy021 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb058AlphaDummy020)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb058AlphaDummy021)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0031 (x : SemanticCore.Var) : nb058AlphaDummy024 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb058AlphaDummy023 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb058AlphaDummy024 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0032 : nb058AlphaDummy021 ∈ (SemanticCore.Class.cv nb058AlphaDummy021).fv ∪ (SemanticCore.Class.cv nb058AlphaDummy021).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0033 (x : SemanticCore.Var) : nb058AlphaDummy024 x ∈ (SemanticCore.Class.cv (nb058AlphaDummy024 x)).fv ∪ (SemanticCore.Class.cv (nb058AlphaDummy024 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0034 : nb058AlphaDummy001 ∈ (SemanticCore.Class.cv nb058AlphaDummy000).fv ∪ (SemanticCore.Class.cv nb058AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0035 : nb058AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb058AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb058AlphaDummy006 (SemanticCore.Class.cv nb058AlphaDummy000) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb058AlphaDummy005) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb058AlphaDummy006)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb058AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb058AlphaDummy006 (SemanticCore.Class.cv nb058AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb058AlphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb058AlphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0036 (x : SemanticCore.Var) : nb058AlphaDummy002 x ∈ (SemanticCore.Class.cv x).fv ∪ (SemanticCore.Class.cv (nb058AlphaDummy002 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0037 (x : SemanticCore.Var) : nb058AlphaDummy002 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb058AlphaDummy007 x) (Compiler.CompactSourceSyntax.synWrex (nb058AlphaDummy008 x) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb058AlphaDummy007 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb058AlphaDummy008 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb058AlphaDummy007 x) (Compiler.CompactSourceSyntax.synWrex (nb058AlphaDummy008 x) (SemanticCore.Class.cv (nb058AlphaDummy002 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb058AlphaDummy007 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb058AlphaDummy008 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0038 : nb058AlphaDummy001 ∈ (SemanticCore.Class.cab nb058AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb058AlphaDummy006 (SemanticCore.Class.cv nb058AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb058AlphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb058AlphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb058AlphaDummy005 (Compiler.CompactSourceSyntax.synWrex nb058AlphaDummy006 (SemanticCore.Class.cv nb058AlphaDummy001) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb058AlphaDummy005) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb058AlphaDummy006)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0039 (x : SemanticCore.Var) : nb058AlphaDummy002 x ∈ (SemanticCore.Class.cab (nb058AlphaDummy007 x) (Compiler.CompactSourceSyntax.synWrex (nb058AlphaDummy008 x) (SemanticCore.Class.cv (nb058AlphaDummy002 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb058AlphaDummy007 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb058AlphaDummy008 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb058AlphaDummy007 x) (Compiler.CompactSourceSyntax.synWrex (nb058AlphaDummy008 x) (SemanticCore.Class.cv (nb058AlphaDummy002 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb058AlphaDummy007 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb058AlphaDummy008 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0041 (x : SemanticCore.Var) : nb058AlphaDummy008 x ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb058AlphaDummy008 x)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0043 (x : SemanticCore.Var) : nb058AlphaDummy008 x ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb058AlphaDummy008 x))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb058AlphaDummy008 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0044 : nb058AlphaDummy045 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb058AlphaDummy045) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv nb058AlphaDummy000))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb058AlphaDummy045) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv nb058AlphaDummy000))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0045 (x : SemanticCore.Var) : nb058AlphaDummy046 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb058AlphaDummy046 x)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb058AlphaDummy046 x)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0046 : nb058AlphaDummy045 ∈ (SemanticCore.Class.cv nb058AlphaDummy045).fv ∪ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv nb058AlphaDummy000)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0047 (x : SemanticCore.Var) : nb058AlphaDummy046 x ∈ (SemanticCore.Class.cv (nb058AlphaDummy046 x)).fv ∪ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0048 : nb058AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv nb058AlphaDummy000))) Compiler.CompactSourceSyntax.synC1c).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv nb058AlphaDummy000))) Compiler.CompactSourceSyntax.synC1c).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0049 (x : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x))) Compiler.CompactSourceSyntax.synC1c).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x))) Compiler.CompactSourceSyntax.synC1c).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0050 : nb058AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv nb058AlphaDummy000))).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0051 (x : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCpw (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x))).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0052 : nb058AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv nb058AlphaDummy000)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0053 (x : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0054 : nb058AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb058AlphaDummy045) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv nb058AlphaDummy000))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb058AlphaDummy045) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv nb058AlphaDummy000))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0055 (x : SemanticCore.Var) : x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb058AlphaDummy046 x)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb058AlphaDummy046 x)) (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0056 : nb058AlphaDummy000 ∈ (SemanticCore.Class.cv nb058AlphaDummy045).fv ∪ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv nb058AlphaDummy000)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0057 (x : SemanticCore.Var) : x ∈ (SemanticCore.Class.cv (nb058AlphaDummy046 x)).fv ∪ (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0058 : nb058AlphaDummy000 ∈ (SemanticCore.Class.cv nb058AlphaDummy000).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb058_support_mem_0059 (x : SemanticCore.Var) : x ∈ (SemanticCore.Class.cv x).fv