Documentation

LeanPool.NFWeakPartition.NAR4C068C001Part012

NF weak partition development: NAR4C068C001Part012.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0356 :

nb068AlphaDummy350 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy350) (SemanticCore.Class.cv nb068AlphaDummy351)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy350) (SemanticCore.Class.cv nb068AlphaDummy351)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0357 (f : SemanticCore.Var) :

nb068AlphaDummy353 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy353 f)) (SemanticCore.Class.cv (nb068AlphaDummy354 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy353 f)) (SemanticCore.Class.cv (nb068AlphaDummy354 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0358 :

nb068AlphaDummy350 ∈ (SemanticCore.Class.cv nb068AlphaDummy350).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy351).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0359 (f : SemanticCore.Var) :

nb068AlphaDummy353 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy353 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy354 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0360 :

nb068AlphaDummy351 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy350) (SemanticCore.Class.cv nb068AlphaDummy351)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy350) (SemanticCore.Class.cv nb068AlphaDummy351)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0361 (f : SemanticCore.Var) :

nb068AlphaDummy354 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy353 f)) (SemanticCore.Class.cv (nb068AlphaDummy354 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy353 f)) (SemanticCore.Class.cv (nb068AlphaDummy354 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0362 :

nb068AlphaDummy351 ∈ (SemanticCore.Class.cv nb068AlphaDummy350).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy351).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0363 (f : SemanticCore.Var) :

nb068AlphaDummy354 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy353 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy354 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0364 :

nb068AlphaDummy350 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy350)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy351)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0365 (f : SemanticCore.Var) :

nb068AlphaDummy353 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy353 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy354 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0366 :

nb068AlphaDummy350 ∈ (SemanticCore.Class.cv nb068AlphaDummy350).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy350).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0367 (f : SemanticCore.Var) :

nb068AlphaDummy353 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy353 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy353 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0368 :

nb068AlphaDummy351 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy350)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy351)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0369 (f : SemanticCore.Var) :

nb068AlphaDummy354 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy353 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy354 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0370 :

nb068AlphaDummy351 ∈ (SemanticCore.Class.cv nb068AlphaDummy351).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy351).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0371 (f : SemanticCore.Var) :

nb068AlphaDummy354 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy354 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy354 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0372 :

nb068AlphaDummy328 ∈ (SemanticCore.Class.cv nb068AlphaDummy327).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy328).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0373 :

nb068AlphaDummy328 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy327) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy328) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0374 (f : SemanticCore.Var) :

nb068AlphaDummy331 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy330 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy331 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0375 (f : SemanticCore.Var) :

nb068AlphaDummy331 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy330 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0376 :

nb068AlphaDummy328 ∈ (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy328) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy335 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy336 (SemanticCore.Class.cv nb068AlphaDummy328) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy335) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0377 (f : SemanticCore.Var) :

nb068AlphaDummy331 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy337 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy338 f) (SemanticCore.Class.cv (nb068AlphaDummy331 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy337 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0378 :

nb068AlphaDummy336 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0379 (f : SemanticCore.Var) :

nb068AlphaDummy338 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0380 :

nb068AlphaDummy336 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy336)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0381 (f : SemanticCore.Var) :

nb068AlphaDummy338 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy338 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0382 :

nb068AlphaDummy327 ∈ (SemanticCore.Class.cv nb068AlphaDummy327).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy329).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0383 :

nb068AlphaDummy327 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy371 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy372 (SemanticCore.Class.cv nb068AlphaDummy327) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy371) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy371 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy372 (SemanticCore.Class.cv nb068AlphaDummy329) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy371) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0384 (f : SemanticCore.Var) :

nb068AlphaDummy330 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy330 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy332 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0385 (f : SemanticCore.Var) :

nb068AlphaDummy330 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy373 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy374 f) (SemanticCore.Class.cv (nb068AlphaDummy330 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy373 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy373 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy374 f) (SemanticCore.Class.cv (nb068AlphaDummy332 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy373 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0387 (f : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0388 :

nb068AlphaDummy372 ∈ (SemanticCore.Class.cv nb068AlphaDummy372).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0389 (f : SemanticCore.Var) :

nb068AlphaDummy374 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy374 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0390 :

nb068AlphaDummy379 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy379) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy379) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy379).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0392 :

nb068AlphaDummy379 ∈ (SemanticCore.Class.cv nb068AlphaDummy379).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0393 (f : SemanticCore.Var) :

nb068AlphaDummy381 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy381 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0394 :

nb068AlphaDummy386 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy386) (SemanticCore.Class.cv nb068AlphaDummy387)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy386) (SemanticCore.Class.cv nb068AlphaDummy387)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0395 (f : SemanticCore.Var) :

nb068AlphaDummy389 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy389 f)) (SemanticCore.Class.cv (nb068AlphaDummy390 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy389 f)) (SemanticCore.Class.cv (nb068AlphaDummy390 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0396 :

nb068AlphaDummy386 ∈ (SemanticCore.Class.cv nb068AlphaDummy386).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy387).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0397 (f : SemanticCore.Var) :

nb068AlphaDummy389 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy389 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy390 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0398 :

nb068AlphaDummy387 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy386) (SemanticCore.Class.cv nb068AlphaDummy387)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy386) (SemanticCore.Class.cv nb068AlphaDummy387)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0399 (f : SemanticCore.Var) :

nb068AlphaDummy390 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy389 f)) (SemanticCore.Class.cv (nb068AlphaDummy390 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy389 f)) (SemanticCore.Class.cv (nb068AlphaDummy390 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0400 :

nb068AlphaDummy387 ∈ (SemanticCore.Class.cv nb068AlphaDummy386).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy387).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0401 (f : SemanticCore.Var) :

nb068AlphaDummy390 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy389 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy390 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0402 :

nb068AlphaDummy386 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy386)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy387)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0403 (f : SemanticCore.Var) :

nb068AlphaDummy389 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy389 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy390 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0404 :

nb068AlphaDummy386 ∈ (SemanticCore.Class.cv nb068AlphaDummy386).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy386).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0405 (f : SemanticCore.Var) :

nb068AlphaDummy389 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy389 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy389 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0406 :

nb068AlphaDummy387 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy386)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy387)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0407 (f : SemanticCore.Var) :

nb068AlphaDummy390 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy389 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy390 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0408 :

nb068AlphaDummy387 ∈ (SemanticCore.Class.cv nb068AlphaDummy387).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy387).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0409 (f : SemanticCore.Var) :

nb068AlphaDummy390 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy390 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy390 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0410 :

nb068AlphaDummy329 ∈ (SemanticCore.Class.cv nb068AlphaDummy327).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy329).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0411 :

nb068AlphaDummy329 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy371 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy372 (SemanticCore.Class.cv nb068AlphaDummy327) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy371) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy371 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy372 (SemanticCore.Class.cv nb068AlphaDummy329) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy371) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0412 (f : SemanticCore.Var) :

nb068AlphaDummy332 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy330 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy332 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0413 (f : SemanticCore.Var) :

nb068AlphaDummy332 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy373 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy374 f) (SemanticCore.Class.cv (nb068AlphaDummy330 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy373 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy373 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy374 f) (SemanticCore.Class.cv (nb068AlphaDummy332 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy373 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0414 :

nb068AlphaDummy329 ∈ (SemanticCore.Class.cab nb068AlphaDummy371 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy372 (SemanticCore.Class.cv nb068AlphaDummy329) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy371) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy371 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy372 (SemanticCore.Class.cv nb068AlphaDummy329) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy371) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0415 (f : SemanticCore.Var) :

nb068AlphaDummy332 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy373 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy374 f) (SemanticCore.Class.cv (nb068AlphaDummy332 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy373 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy373 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy374 f) (SemanticCore.Class.cv (nb068AlphaDummy332 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy373 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0416 :

nb068AlphaDummy372 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0417 (f : SemanticCore.Var) :

nb068AlphaDummy374 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0418 :

nb068AlphaDummy372 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy372)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0419 (f : SemanticCore.Var) :

nb068AlphaDummy374 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy374 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0424 :

nb068AlphaDummy407 ∈ (SemanticCore.Class.cv nb068AlphaDummy407).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy408).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0425 :

nb068AlphaDummy407 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy413 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy414 (SemanticCore.Class.cv nb068AlphaDummy407) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy413) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy413 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy414 (SemanticCore.Class.cv nb068AlphaDummy408) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy413) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0426 (f : SemanticCore.Var) :

nb068AlphaDummy409 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy409 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy410 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0427 (f : SemanticCore.Var) :

nb068AlphaDummy409 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy415 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy416 f) (SemanticCore.Class.cv (nb068AlphaDummy409 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy415 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy415 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy416 f) (SemanticCore.Class.cv (nb068AlphaDummy410 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy415 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0429 (f : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0430 :

nb068AlphaDummy414 ∈ (SemanticCore.Class.cv nb068AlphaDummy414).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0431 (f : SemanticCore.Var) :

nb068AlphaDummy416 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy416 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0432 :

nb068AlphaDummy421 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy421) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy421) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy421).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0434 :

nb068AlphaDummy421 ∈ (SemanticCore.Class.cv nb068AlphaDummy421).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0435 (f : SemanticCore.Var) :

nb068AlphaDummy423 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy423 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0436 :

nb068AlphaDummy428 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy428) (SemanticCore.Class.cv nb068AlphaDummy429)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy428) (SemanticCore.Class.cv nb068AlphaDummy429)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0437 (f : SemanticCore.Var) :

nb068AlphaDummy431 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy431 f)) (SemanticCore.Class.cv (nb068AlphaDummy432 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy431 f)) (SemanticCore.Class.cv (nb068AlphaDummy432 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0438 :

nb068AlphaDummy428 ∈ (SemanticCore.Class.cv nb068AlphaDummy428).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy429).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0439 (f : SemanticCore.Var) :

nb068AlphaDummy431 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy431 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy432 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0440 :

nb068AlphaDummy429 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy428) (SemanticCore.Class.cv nb068AlphaDummy429)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy428) (SemanticCore.Class.cv nb068AlphaDummy429)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0441 (f : SemanticCore.Var) :

nb068AlphaDummy432 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy431 f)) (SemanticCore.Class.cv (nb068AlphaDummy432 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy431 f)) (SemanticCore.Class.cv (nb068AlphaDummy432 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0442 :

nb068AlphaDummy429 ∈ (SemanticCore.Class.cv nb068AlphaDummy428).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy429).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0443 (f : SemanticCore.Var) :

nb068AlphaDummy432 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy431 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy432 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0444 :

nb068AlphaDummy428 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy428)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy429)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0445 (f : SemanticCore.Var) :

nb068AlphaDummy431 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy431 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy432 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0446 :

nb068AlphaDummy428 ∈ (SemanticCore.Class.cv nb068AlphaDummy428).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy428).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0447 (f : SemanticCore.Var) :

nb068AlphaDummy431 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy431 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy431 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0448 :

nb068AlphaDummy429 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy428)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy429)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0449 (f : SemanticCore.Var) :

nb068AlphaDummy432 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy431 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy432 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0450 :

nb068AlphaDummy429 ∈ (SemanticCore.Class.cv nb068AlphaDummy429).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy429).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0451 (f : SemanticCore.Var) :

nb068AlphaDummy432 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy432 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy432 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0452 :

nb068AlphaDummy408 ∈ (SemanticCore.Class.cv nb068AlphaDummy407).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy408).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0453 :

nb068AlphaDummy408 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy413 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy414 (SemanticCore.Class.cv nb068AlphaDummy407) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy413) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy413 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy414 (SemanticCore.Class.cv nb068AlphaDummy408) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy413) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0454 (f : SemanticCore.Var) :

nb068AlphaDummy410 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy409 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy410 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0455 (f : SemanticCore.Var) :

nb068AlphaDummy410 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy415 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy416 f) (SemanticCore.Class.cv (nb068AlphaDummy409 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy415 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy415 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy416 f) (SemanticCore.Class.cv (nb068AlphaDummy410 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy415 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0456 :

nb068AlphaDummy408 ∈ (SemanticCore.Class.cab nb068AlphaDummy413 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy414 (SemanticCore.Class.cv nb068AlphaDummy408) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy413) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy413 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy414 (SemanticCore.Class.cv nb068AlphaDummy408) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy413) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0457 (f : SemanticCore.Var) :

nb068AlphaDummy410 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy415 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy416 f) (SemanticCore.Class.cv (nb068AlphaDummy410 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy415 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy415 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy416 f) (SemanticCore.Class.cv (nb068AlphaDummy410 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy415 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0458 :

nb068AlphaDummy414 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0459 (f : SemanticCore.Var) :

nb068AlphaDummy416 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0460 :

nb068AlphaDummy414 ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy414)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0461 (f : SemanticCore.Var) :

nb068AlphaDummy416 f ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy416 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0462 :

nb068AlphaDummy408 ∈ (SemanticCore.Class.cv nb068AlphaDummy408).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy407).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0463 :

nb068AlphaDummy408 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy449 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy450 (SemanticCore.Class.cv nb068AlphaDummy408) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy449) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy449 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy450 (SemanticCore.Class.cv nb068AlphaDummy407) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy449) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0464 (f : SemanticCore.Var) :

nb068AlphaDummy410 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy410 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy409 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0465 (f : SemanticCore.Var) :

nb068AlphaDummy410 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy451 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy452 f) (SemanticCore.Class.cv (nb068AlphaDummy410 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy451 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy451 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy452 f) (SemanticCore.Class.cv (nb068AlphaDummy409 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy451 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0467 (f : SemanticCore.Var) :

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0468 :

nb068AlphaDummy450 ∈ (SemanticCore.Class.cv nb068AlphaDummy450).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0469 (f : SemanticCore.Var) :

nb068AlphaDummy452 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy452 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0470 :

nb068AlphaDummy457 ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv nb068AlphaDummy457) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv nb068AlphaDummy457) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy457).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0472 :

nb068AlphaDummy457 ∈ (SemanticCore.Class.cv nb068AlphaDummy457).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0473 (f : SemanticCore.Var) :

nb068AlphaDummy459 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy459 f)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0474 :

nb068AlphaDummy464 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy464) (SemanticCore.Class.cv nb068AlphaDummy465)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy464) (SemanticCore.Class.cv nb068AlphaDummy465)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0475 (f : SemanticCore.Var) :

nb068AlphaDummy467 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy467 f)) (SemanticCore.Class.cv (nb068AlphaDummy468 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy467 f)) (SemanticCore.Class.cv (nb068AlphaDummy468 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0476 :

nb068AlphaDummy464 ∈ (SemanticCore.Class.cv nb068AlphaDummy464).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy465).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0477 (f : SemanticCore.Var) :

nb068AlphaDummy467 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy467 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy468 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0478 :

nb068AlphaDummy465 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy464) (SemanticCore.Class.cv nb068AlphaDummy465)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb068AlphaDummy464) (SemanticCore.Class.cv nb068AlphaDummy465)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0479 (f : SemanticCore.Var) :

nb068AlphaDummy468 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy467 f)) (SemanticCore.Class.cv (nb068AlphaDummy468 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb068AlphaDummy467 f)) (SemanticCore.Class.cv (nb068AlphaDummy468 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0480 :

nb068AlphaDummy465 ∈ (SemanticCore.Class.cv nb068AlphaDummy464).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy465).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0481 (f : SemanticCore.Var) :

nb068AlphaDummy468 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy467 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy468 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0482 :

nb068AlphaDummy464 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy464)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy465)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0483 (f : SemanticCore.Var) :

nb068AlphaDummy467 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy467 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy468 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0484 :

nb068AlphaDummy464 ∈ (SemanticCore.Class.cv nb068AlphaDummy464).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy464).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0485 (f : SemanticCore.Var) :

nb068AlphaDummy467 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy467 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy467 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0486 :

nb068AlphaDummy465 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy464)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb068AlphaDummy465)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0487 (f : SemanticCore.Var) :

nb068AlphaDummy468 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy467 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb068AlphaDummy468 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0488 :

nb068AlphaDummy465 ∈ (SemanticCore.Class.cv nb068AlphaDummy465).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy465).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0489 (f : SemanticCore.Var) :

nb068AlphaDummy468 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy468 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy468 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0490 :

nb068AlphaDummy407 ∈ (SemanticCore.Class.cv nb068AlphaDummy408).fv ∪ (SemanticCore.Class.cv nb068AlphaDummy407).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0491 :

nb068AlphaDummy407 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy449 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy450 (SemanticCore.Class.cv nb068AlphaDummy408) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy449) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb068AlphaDummy449 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy450 (SemanticCore.Class.cv nb068AlphaDummy407) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy449) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0492 (f : SemanticCore.Var) :

nb068AlphaDummy409 f ∈ (SemanticCore.Class.cv (nb068AlphaDummy410 f)).fv ∪ (SemanticCore.Class.cv (nb068AlphaDummy409 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0493 (f : SemanticCore.Var) :

nb068AlphaDummy409 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy451 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy452 f) (SemanticCore.Class.cv (nb068AlphaDummy410 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy451 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb068AlphaDummy451 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy452 f) (SemanticCore.Class.cv (nb068AlphaDummy409 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy451 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0494 :

nb068AlphaDummy407 ∈ (SemanticCore.Class.cab nb068AlphaDummy449 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy450 (SemanticCore.Class.cv nb068AlphaDummy407) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy449) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb068AlphaDummy449 (Compiler.CompactSourceSyntax.synWrex nb068AlphaDummy450 (SemanticCore.Class.cv nb068AlphaDummy407) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb068AlphaDummy449) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0495 (f : SemanticCore.Var) :

nb068AlphaDummy409 f ∈ (SemanticCore.Class.cab (nb068AlphaDummy451 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy452 f) (SemanticCore.Class.cv (nb068AlphaDummy409 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy451 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb068AlphaDummy451 f) (Compiler.CompactSourceSyntax.synWrex (nb068AlphaDummy452 f) (SemanticCore.Class.cv (nb068AlphaDummy409 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb068AlphaDummy451 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0496 :

nb068AlphaDummy450 ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb068AlphaDummy450))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb068_support_mem_0497 (f : SemanticCore.Var) :

nb068AlphaDummy452 f ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb068AlphaDummy452 f)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv