Documentation

LeanPool.NFWeakPartition.NAR4C067C001Part009

NF weak partition development: NAR4C067C001Part009.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0320 :

nb067AlphaDummy297 ∈ (SemanticCore.Class.cv nb067AlphaDummy296).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy297).fv

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

nb067AlphaDummy300 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy299 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy300 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0322 :

nb067AlphaDummy296 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy296)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy297)).fv

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

nb067AlphaDummy299 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy299 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy300 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0324 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0326 :

nb067AlphaDummy297 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy296)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy297)).fv

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

nb067AlphaDummy300 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy299 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy300 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0328 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0330 :

nb067AlphaDummy277 ∈ (SemanticCore.Class.cv nb067AlphaDummy278).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy277).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0331 :

nb067AlphaDummy277 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy281 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy282 (SemanticCore.Class.cv nb067AlphaDummy278) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy281) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy281 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy282 (SemanticCore.Class.cv nb067AlphaDummy277) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy281) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb067AlphaDummy279 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy280 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy279 f)).fv

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

nb067AlphaDummy279 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy283 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy284 f) (SemanticCore.Class.cv (nb067AlphaDummy280 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy283 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy283 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy284 f) (SemanticCore.Class.cv (nb067AlphaDummy279 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy283 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0334 :

nb067AlphaDummy277 ∈ (SemanticCore.Class.cab nb067AlphaDummy281 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy282 (SemanticCore.Class.cv nb067AlphaDummy277) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy281) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy281 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy282 (SemanticCore.Class.cv nb067AlphaDummy277) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy281) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy282)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb067AlphaDummy279 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy283 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy284 f) (SemanticCore.Class.cv (nb067AlphaDummy279 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy283 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy283 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy284 f) (SemanticCore.Class.cv (nb067AlphaDummy279 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy283 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy284 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0336 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0338 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0340 :

nb067AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv nb067AlphaDummy000)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

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

f ∈ (Compiler.CompactSourceSyntax.synCcnv (SemanticCore.Class.cv f)).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0342 :

nb067AlphaDummy322 ∈ (SemanticCore.Class.cv nb067AlphaDummy322).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy321).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0343 :

nb067AlphaDummy322 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy325 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy326 (SemanticCore.Class.cv nb067AlphaDummy322) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy325) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy325 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy326 (SemanticCore.Class.cv nb067AlphaDummy321) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy325) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb067AlphaDummy324 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy324 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy323 f)).fv

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

nb067AlphaDummy324 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy327 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy328 f) (SemanticCore.Class.cv (nb067AlphaDummy324 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy327 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy327 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy328 f) (SemanticCore.Class.cv (nb067AlphaDummy323 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy327 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0348 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0350 :

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0352 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0354 :

nb067AlphaDummy340 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341)).fv

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

nb067AlphaDummy343 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0356 :

nb067AlphaDummy340 ∈ (SemanticCore.Class.cv nb067AlphaDummy340).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy341).fv

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

nb067AlphaDummy343 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy343 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy344 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0358 :

nb067AlphaDummy341 ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv nb067AlphaDummy340) (SemanticCore.Class.cv nb067AlphaDummy341)).fv

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

nb067AlphaDummy344 f ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb067AlphaDummy343 f)) (SemanticCore.Class.cv (nb067AlphaDummy344 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0360 :

nb067AlphaDummy341 ∈ (SemanticCore.Class.cv nb067AlphaDummy340).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy341).fv

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

nb067AlphaDummy344 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy343 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy344 f)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0362 :

nb067AlphaDummy340 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy340)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy341)).fv

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

nb067AlphaDummy343 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy343 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy344 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0364 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0366 :

nb067AlphaDummy341 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy340)).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv nb067AlphaDummy341)).fv

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

nb067AlphaDummy344 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy343 f))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb067AlphaDummy344 f))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0368 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0370 :

nb067AlphaDummy321 ∈ (SemanticCore.Class.cv nb067AlphaDummy322).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy321).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0371 :

nb067AlphaDummy321 ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy325 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy326 (SemanticCore.Class.cv nb067AlphaDummy322) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy325) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab nb067AlphaDummy325 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy326 (SemanticCore.Class.cv nb067AlphaDummy321) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy325) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

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

nb067AlphaDummy323 f ∈ (SemanticCore.Class.cv (nb067AlphaDummy324 f)).fv ∪ (SemanticCore.Class.cv (nb067AlphaDummy323 f)).fv

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

nb067AlphaDummy323 f ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy327 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy328 f) (SemanticCore.Class.cv (nb067AlphaDummy324 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy327 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb067AlphaDummy327 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy328 f) (SemanticCore.Class.cv (nb067AlphaDummy323 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy327 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0374 :

nb067AlphaDummy321 ∈ (SemanticCore.Class.cab nb067AlphaDummy325 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy326 (SemanticCore.Class.cv nb067AlphaDummy321) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy325) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab nb067AlphaDummy325 (Compiler.CompactSourceSyntax.synWrex nb067AlphaDummy326 (SemanticCore.Class.cv nb067AlphaDummy321) (SemanticCore.Wff.classEq (SemanticCore.Class.cv nb067AlphaDummy325) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb067AlphaDummy326)) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

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

nb067AlphaDummy323 f ∈ (SemanticCore.Class.cab (nb067AlphaDummy327 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy328 f) (SemanticCore.Class.cv (nb067AlphaDummy323 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy327 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb067AlphaDummy327 f) (Compiler.CompactSourceSyntax.synWrex (nb067AlphaDummy328 f) (SemanticCore.Class.cv (nb067AlphaDummy323 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb067AlphaDummy327 f)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb067AlphaDummy328 f))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0376 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0378 :

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0380 :

nb067AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy001)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0381 (x f : SemanticCore.Var) :

f ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv x)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0382 :

nb067AlphaDummy000 ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb067AlphaDummy000)).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0383 (x f : SemanticCore.Var) :

f ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)).fv ∪ (SemanticCore.Class.cv x).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0384 :

nb067AlphaDummy000 ∈ (SemanticCore.Class.cv nb067AlphaDummy000).fv ∪ Compiler.CompactSourceSyntax.synCvv.fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0386 :

nb067AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy001)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb067AlphaDummy000)) (SemanticCore.Class.cv nb067AlphaDummy001)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0387 (x f : SemanticCore.Var) :

x ∈ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv x)).fv ∪ (Compiler.CompactSourceSyntax.synCnin (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)) (SemanticCore.Class.cv x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0388 :

nb067AlphaDummy001 ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv nb067AlphaDummy000)).fv ∪ (SemanticCore.Class.cv nb067AlphaDummy001).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_support_mem_0389 (x f : SemanticCore.Var) :

x ∈ (Compiler.CompactSourceSyntax.synCrn (SemanticCore.Class.cv f)).fv ∪ (SemanticCore.Class.cv x).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_compact_fv_empty_0028 :

nb067AlphaDummy003 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_compact_fv_empty_0029 (x y f : SemanticCore.Var) :

nb067AlphaDummy004 x y f ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_compact_fv_empty_0030 :

nb067AlphaDummy002 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_compact_fv_empty_0031 (y : SemanticCore.Var) :

y ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_compact_fv_empty_0032 :

nb067AlphaDummy001 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_compact_fv_empty_0033 (x : SemanticCore.Var) :

x ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_compact_fv_empty_0034 :

nb067AlphaDummy005 ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb067_compact_fv_empty_0035 (x y f : SemanticCore.Var) :

nb067AlphaDummy006 x y f ∉ ∅