NF weak partition development: NAR4C055C001Part005.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0138 : nb055AlphaDummy014 ∈ (SemanticCore.Class.cab nb055AlphaDummy118 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy119 (SemanticCore.Class.cv nb055AlphaDummy014) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy118) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy119))))).fv ∪ (SemanticCore.Class.cab nb055AlphaDummy118 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy119 (SemanticCore.Class.cv nb055AlphaDummy014) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy118) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy119))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0139 (x y : SemanticCore.Var) : nb055AlphaDummy016 x y ∈ (SemanticCore.Class.cab (nb055AlphaDummy120 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy121 x y) (SemanticCore.Class.cv (nb055AlphaDummy016 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy120 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy121 x y)))))).fv ∪ (SemanticCore.Class.cab (nb055AlphaDummy120 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy121 x y) (SemanticCore.Class.cv (nb055AlphaDummy016 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy120 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy121 x y)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0140 : nb055AlphaDummy119 ∈ (SemanticCore.Class.cv nb055AlphaDummy119).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0141 (x y : SemanticCore.Var) : nb055AlphaDummy121 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy121 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0142 : nb055AlphaDummy126 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy126) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb055AlphaDummy126) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy126).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0143 (x y : SemanticCore.Var) : nb055AlphaDummy128 x y ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy128 x y)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb055AlphaDummy128 x y)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy128 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0144 : nb055AlphaDummy126 ∈ (SemanticCore.Class.cv nb055AlphaDummy126).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0145 (x y : SemanticCore.Var) : nb055AlphaDummy128 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy128 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0146 : nb055AlphaDummy133 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb055AlphaDummy133) (SemanticCore.Class.cv nb055AlphaDummy134)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb055AlphaDummy133) (SemanticCore.Class.cv nb055AlphaDummy134)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0147 (x y : SemanticCore.Var) : nb055AlphaDummy136 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb055AlphaDummy136 x y)) (SemanticCore.Class.cv (nb055AlphaDummy137 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb055AlphaDummy136 x y)) (SemanticCore.Class.cv (nb055AlphaDummy137 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0148 : nb055AlphaDummy133 ∈ (SemanticCore.Class.cv nb055AlphaDummy133).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy134).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0149 (x y : SemanticCore.Var) : nb055AlphaDummy136 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy136 x y)).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy137 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0150 : nb055AlphaDummy134 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb055AlphaDummy133) (SemanticCore.Class.cv nb055AlphaDummy134)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb055AlphaDummy133) (SemanticCore.Class.cv nb055AlphaDummy134)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0151 (x y : SemanticCore.Var) : nb055AlphaDummy137 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb055AlphaDummy136 x y)) (SemanticCore.Class.cv (nb055AlphaDummy137 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb055AlphaDummy136 x y)) (SemanticCore.Class.cv (nb055AlphaDummy137 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0152 : nb055AlphaDummy134 ∈ (SemanticCore.Class.cv nb055AlphaDummy133).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy134).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0153 (x y : SemanticCore.Var) : nb055AlphaDummy137 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy136 x y)).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy137 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0154 : nb055AlphaDummy133 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb055AlphaDummy133)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb055AlphaDummy134)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0155 (x y : SemanticCore.Var) : nb055AlphaDummy136 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb055AlphaDummy136 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb055AlphaDummy137 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0156 : nb055AlphaDummy133 ∈ (SemanticCore.Class.cv nb055AlphaDummy133).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy133).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0157 (x y : SemanticCore.Var) : nb055AlphaDummy136 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy136 x y)).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy136 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0158 : nb055AlphaDummy134 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb055AlphaDummy133)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb055AlphaDummy134)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0159 (x y : SemanticCore.Var) : nb055AlphaDummy137 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb055AlphaDummy136 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb055AlphaDummy137 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0160 : nb055AlphaDummy134 ∈ (SemanticCore.Class.cv nb055AlphaDummy134).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy134).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0161 (x y : SemanticCore.Var) : nb055AlphaDummy137 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy137 x y)).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy137 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0162 : nb055AlphaDummy078 ∈ (SemanticCore.Class.cv nb055AlphaDummy014).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy078).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0163 : nb055AlphaDummy078 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb055AlphaDummy118 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy119 (SemanticCore.Class.cv nb055AlphaDummy014) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy118) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy119)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb055AlphaDummy118 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy119 (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy118) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy119)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0164 (x y : SemanticCore.Var) : nb055AlphaDummy079 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy016 x y)).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy079 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0165 (x y : SemanticCore.Var) : nb055AlphaDummy079 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb055AlphaDummy120 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy121 x y) (SemanticCore.Class.cv (nb055AlphaDummy016 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy120 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy121 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb055AlphaDummy120 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy121 x y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy120 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy121 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0166 : nb055AlphaDummy078 ∈ (SemanticCore.Class.cab nb055AlphaDummy118 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy119 (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy118) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy119)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb055AlphaDummy118 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy119 (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy118) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy119)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0167 (x y : SemanticCore.Var) : nb055AlphaDummy079 x y ∈ (SemanticCore.Class.cab (nb055AlphaDummy120 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy121 x y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy120 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy121 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb055AlphaDummy120 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy121 x y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy120 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy121 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0171 (x y : SemanticCore.Var) : nb055AlphaDummy121 x y ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy121 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy121 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0172 : nb055AlphaDummy001 ∈ {nb055AlphaDummy014} ∪ {nb055AlphaDummy015} ∪ (Compiler.CompactSourceSyntax.synWex nb055AlphaDummy078 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb055AlphaDummy014) (SemanticCore.Class.cv nb055AlphaDummy001) (SemanticCore.Class.cv nb055AlphaDummy078)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Class.cv nb055AlphaDummy000) (SemanticCore.Class.cv nb055AlphaDummy015)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0173 (x y : SemanticCore.Var) : y ∈ {nb055AlphaDummy016 x y} ∪ {nb055AlphaDummy017 x y} ∪ (Compiler.CompactSourceSyntax.synWex (nb055AlphaDummy079 x y) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb055AlphaDummy016 x y)) (SemanticCore.Class.cv y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Class.cv x) (SemanticCore.Class.cv (nb055AlphaDummy017 x y))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0174 : nb055AlphaDummy078 ∈ (SemanticCore.Class.cv nb055AlphaDummy078).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy015).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0175 : nb055AlphaDummy078 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb055AlphaDummy154 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy155 (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy154) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy155)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb055AlphaDummy154 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy155 (SemanticCore.Class.cv nb055AlphaDummy015) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy154) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy155)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0176 (x y : SemanticCore.Var) : nb055AlphaDummy079 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy079 x y)).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy017 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0177 (x y : SemanticCore.Var) : nb055AlphaDummy079 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb055AlphaDummy156 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy157 x y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy156 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb055AlphaDummy156 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy157 x y) (SemanticCore.Class.cv (nb055AlphaDummy017 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy156 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0178 : nb055AlphaDummy078 ∈ (SemanticCore.Class.cab nb055AlphaDummy154 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy155 (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy154) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy155))))).fv ∪ (SemanticCore.Class.cab nb055AlphaDummy154 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy155 (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy154) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy155))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0179 (x y : SemanticCore.Var) : nb055AlphaDummy079 x y ∈ (SemanticCore.Class.cab (nb055AlphaDummy156 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy157 x y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy156 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y)))))).fv ∪ (SemanticCore.Class.cab (nb055AlphaDummy156 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy157 x y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy156 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0180 : nb055AlphaDummy155 ∈ (SemanticCore.Class.cv nb055AlphaDummy155).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0181 (x y : SemanticCore.Var) : nb055AlphaDummy157 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy157 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0182 : nb055AlphaDummy162 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb055AlphaDummy162) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb055AlphaDummy162) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy162).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0183 (x y : SemanticCore.Var) : nb055AlphaDummy164 x y ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb055AlphaDummy164 x y)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb055AlphaDummy164 x y)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy164 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0184 : nb055AlphaDummy162 ∈ (SemanticCore.Class.cv nb055AlphaDummy162).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0185 (x y : SemanticCore.Var) : nb055AlphaDummy164 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy164 x y)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0186 : nb055AlphaDummy169 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb055AlphaDummy169) (SemanticCore.Class.cv nb055AlphaDummy170)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb055AlphaDummy169) (SemanticCore.Class.cv nb055AlphaDummy170)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0187 (x y : SemanticCore.Var) : nb055AlphaDummy172 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb055AlphaDummy172 x y)) (SemanticCore.Class.cv (nb055AlphaDummy173 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb055AlphaDummy172 x y)) (SemanticCore.Class.cv (nb055AlphaDummy173 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0188 : nb055AlphaDummy169 ∈ (SemanticCore.Class.cv nb055AlphaDummy169).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy170).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0189 (x y : SemanticCore.Var) : nb055AlphaDummy172 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy172 x y)).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy173 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0190 : nb055AlphaDummy170 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb055AlphaDummy169) (SemanticCore.Class.cv nb055AlphaDummy170)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb055AlphaDummy169) (SemanticCore.Class.cv nb055AlphaDummy170)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0191 (x y : SemanticCore.Var) : nb055AlphaDummy173 x y ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb055AlphaDummy172 x y)) (SemanticCore.Class.cv (nb055AlphaDummy173 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb055AlphaDummy172 x y)) (SemanticCore.Class.cv (nb055AlphaDummy173 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0192 : nb055AlphaDummy170 ∈ (SemanticCore.Class.cv nb055AlphaDummy169).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy170).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0193 (x y : SemanticCore.Var) : nb055AlphaDummy173 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy172 x y)).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy173 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0194 : nb055AlphaDummy169 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb055AlphaDummy169)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb055AlphaDummy170)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0195 (x y : SemanticCore.Var) : nb055AlphaDummy172 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb055AlphaDummy172 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb055AlphaDummy173 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0196 : nb055AlphaDummy169 ∈ (SemanticCore.Class.cv nb055AlphaDummy169).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy169).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0197 (x y : SemanticCore.Var) : nb055AlphaDummy172 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy172 x y)).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy172 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0198 : nb055AlphaDummy170 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb055AlphaDummy169)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb055AlphaDummy170)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0199 (x y : SemanticCore.Var) : nb055AlphaDummy173 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb055AlphaDummy172 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb055AlphaDummy173 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0200 : nb055AlphaDummy170 ∈ (SemanticCore.Class.cv nb055AlphaDummy170).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy170).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0201 (x y : SemanticCore.Var) : nb055AlphaDummy173 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy173 x y)).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy173 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0202 : nb055AlphaDummy015 ∈ (SemanticCore.Class.cv nb055AlphaDummy078).fv ∪ (SemanticCore.Class.cv nb055AlphaDummy015).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0203 : nb055AlphaDummy015 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb055AlphaDummy154 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy155 (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy154) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy155)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb055AlphaDummy154 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy155 (SemanticCore.Class.cv nb055AlphaDummy015) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy154) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy155)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0204 (x y : SemanticCore.Var) : nb055AlphaDummy017 x y ∈ (SemanticCore.Class.cv (nb055AlphaDummy079 x y)).fv ∪ (SemanticCore.Class.cv (nb055AlphaDummy017 x y)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0205 (x y : SemanticCore.Var) : nb055AlphaDummy017 x y ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb055AlphaDummy156 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy157 x y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy156 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb055AlphaDummy156 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy157 x y) (SemanticCore.Class.cv (nb055AlphaDummy017 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy156 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0206 : nb055AlphaDummy015 ∈ (SemanticCore.Class.cab nb055AlphaDummy154 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy155 (SemanticCore.Class.cv nb055AlphaDummy015) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy154) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy155)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb055AlphaDummy154 (Compiler.CompactSourceSyntax.synWrex nb055AlphaDummy155 (SemanticCore.Class.cv nb055AlphaDummy015) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb055AlphaDummy154) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb055AlphaDummy155)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0207 (x y : SemanticCore.Var) : nb055AlphaDummy017 x y ∈ (SemanticCore.Class.cab (nb055AlphaDummy156 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy157 x y) (SemanticCore.Class.cv (nb055AlphaDummy017 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy156 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb055AlphaDummy156 x y) (Compiler.CompactSourceSyntax.synWrex (nb055AlphaDummy157 x y) (SemanticCore.Class.cv (nb055AlphaDummy017 x y)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb055AlphaDummy156 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0211 (x y : SemanticCore.Var) : nb055AlphaDummy157 x y ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb055AlphaDummy157 x y))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0212 : nb055AlphaDummy000 ∈ {nb055AlphaDummy014} ∪ {nb055AlphaDummy015} ∪ (Compiler.CompactSourceSyntax.synWex nb055AlphaDummy078 (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb055AlphaDummy014) (SemanticCore.Class.cv nb055AlphaDummy001) (SemanticCore.Class.cv nb055AlphaDummy078)) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv nb055AlphaDummy078) (SemanticCore.Class.cv nb055AlphaDummy000) (SemanticCore.Class.cv nb055AlphaDummy015)))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb055_support_mem_0213 (x y : SemanticCore.Var) : x ∈ {nb055AlphaDummy016 x y} ∪ {nb055AlphaDummy017 x y} ∪ (Compiler.CompactSourceSyntax.synWex (nb055AlphaDummy079 x y) (Compiler.CompactSourceSyntax.synWa (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb055AlphaDummy016 x y)) (SemanticCore.Class.cv y) (SemanticCore.Class.cv (nb055AlphaDummy079 x y))) (Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb055AlphaDummy079 x y)) (SemanticCore.Class.cv x) (SemanticCore.Class.cv (nb055AlphaDummy017 x y))))).fv