NF weak partition development: NAR4C077C001Part009.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0304 (F I : SemanticCore.Class) : nb077AlphaDummy297 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy296 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy297 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0305 (x : SemanticCore.Var) : nb077AlphaDummy300 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy299 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy300 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0306 (F I : SemanticCore.Class) : nb077AlphaDummy297 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy297 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy297 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0308 (F I : SemanticCore.Class) : nb077AlphaDummy061 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy061 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy060 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0309 (F I : SemanticCore.Class) : nb077AlphaDummy061 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy311 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy312 F I) (SemanticCore.Class.cv (nb077AlphaDummy061 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy311 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy311 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy312 F I) (SemanticCore.Class.cv (nb077AlphaDummy060 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy311 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0310 (x : SemanticCore.Var) : nb077AlphaDummy064 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy064 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy063 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0311 (x : SemanticCore.Var) : nb077AlphaDummy064 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy313 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy314 x) (SemanticCore.Class.cv (nb077AlphaDummy064 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy313 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy313 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy314 x) (SemanticCore.Class.cv (nb077AlphaDummy063 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy313 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0312 (F I : SemanticCore.Class) : nb077AlphaDummy061 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy311 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy312 F I) (SemanticCore.Class.cv (nb077AlphaDummy061 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy311 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy311 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy312 F I) (SemanticCore.Class.cv (nb077AlphaDummy061 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy311 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0313 (x : SemanticCore.Var) : nb077AlphaDummy064 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy313 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy314 x) (SemanticCore.Class.cv (nb077AlphaDummy064 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy313 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x)))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy313 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy314 x) (SemanticCore.Class.cv (nb077AlphaDummy064 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy313 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0314 (F I : SemanticCore.Class) : nb077AlphaDummy312 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy312 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0316 (F I : SemanticCore.Class) : nb077AlphaDummy319 F I ∈ (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy319 F I)) Compiler.CompactSourceSyntax.synCnnc).fv ∪ (Compiler.CompactSourceSyntax.synCplc (SemanticCore.Class.cv (nb077AlphaDummy319 F I)) Compiler.CompactSourceSyntax.synC1c).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy319 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0318 (F I : SemanticCore.Class) : nb077AlphaDummy319 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy319 F I)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0319 (x : SemanticCore.Var) : nb077AlphaDummy321 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy321 x)).fv ∪ Compiler.CompactSourceSyntax.synC1c.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0320 (F I : SemanticCore.Class) : nb077AlphaDummy326 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy326 F I)) (SemanticCore.Class.cv (nb077AlphaDummy327 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy326 F I)) (SemanticCore.Class.cv (nb077AlphaDummy327 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0321 (x : SemanticCore.Var) : nb077AlphaDummy329 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy329 x)) (SemanticCore.Class.cv (nb077AlphaDummy330 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy329 x)) (SemanticCore.Class.cv (nb077AlphaDummy330 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0322 (F I : SemanticCore.Class) : nb077AlphaDummy326 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy326 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy327 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0323 (x : SemanticCore.Var) : nb077AlphaDummy329 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy329 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy330 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0324 (F I : SemanticCore.Class) : nb077AlphaDummy327 F I ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy326 F I)) (SemanticCore.Class.cv (nb077AlphaDummy327 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy326 F I)) (SemanticCore.Class.cv (nb077AlphaDummy327 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0325 (x : SemanticCore.Var) : nb077AlphaDummy330 x ∈ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy329 x)) (SemanticCore.Class.cv (nb077AlphaDummy330 x))).fv ∪ (Compiler.CompactSourceSyntax.synCnin (SemanticCore.Class.cv (nb077AlphaDummy329 x)) (SemanticCore.Class.cv (nb077AlphaDummy330 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0326 (F I : SemanticCore.Class) : nb077AlphaDummy327 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy326 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy327 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0327 (x : SemanticCore.Var) : nb077AlphaDummy330 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy329 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy330 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0328 (F I : SemanticCore.Class) : nb077AlphaDummy326 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy326 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy327 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0329 (x : SemanticCore.Var) : nb077AlphaDummy329 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy329 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy330 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0330 (F I : SemanticCore.Class) : nb077AlphaDummy326 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy326 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy326 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0332 (F I : SemanticCore.Class) : nb077AlphaDummy327 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy326 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy327 F I))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0333 (x : SemanticCore.Var) : nb077AlphaDummy330 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy329 x))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cv (nb077AlphaDummy330 x))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0334 (F I : SemanticCore.Class) : nb077AlphaDummy327 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy327 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy327 F I)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0336 (F I : SemanticCore.Class) : nb077AlphaDummy060 F I ∈ (SemanticCore.Class.cv (nb077AlphaDummy061 F I)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy060 F I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0337 (F I : SemanticCore.Class) : nb077AlphaDummy060 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy311 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy312 F I) (SemanticCore.Class.cv (nb077AlphaDummy061 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy311 F I)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy311 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy312 F I) (SemanticCore.Class.cv (nb077AlphaDummy060 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy311 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0338 (x : SemanticCore.Var) : nb077AlphaDummy063 x ∈ (SemanticCore.Class.cv (nb077AlphaDummy064 x)).fv ∪ (SemanticCore.Class.cv (nb077AlphaDummy063 x)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0339 (x : SemanticCore.Var) : nb077AlphaDummy063 x ∈ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy313 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy314 x) (SemanticCore.Class.cv (nb077AlphaDummy064 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy313 x)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x))))))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb077AlphaDummy313 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy314 x) (SemanticCore.Class.cv (nb077AlphaDummy063 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy313 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0340 (F I : SemanticCore.Class) : nb077AlphaDummy060 F I ∈ (SemanticCore.Class.cab (nb077AlphaDummy311 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy312 F I) (SemanticCore.Class.cv (nb077AlphaDummy060 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy311 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy311 F I) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy312 F I) (SemanticCore.Class.cv (nb077AlphaDummy060 F I)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy311 F I)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0341 (x : SemanticCore.Var) : nb077AlphaDummy063 x ∈ (SemanticCore.Class.cab (nb077AlphaDummy313 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy314 x) (SemanticCore.Class.cv (nb077AlphaDummy063 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy313 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv ∪ (SemanticCore.Class.cab (nb077AlphaDummy313 x) (Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy314 x) (SemanticCore.Class.cv (nb077AlphaDummy063 x)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy313 x)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy314 x))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0342 (F I : SemanticCore.Class) : nb077AlphaDummy312 F I ∈ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I)))).fv ∪ (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_support_mem_0344 (F I : SemanticCore.Class) : nb077AlphaDummy312 F I ∈ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I))).fv ∪ (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy312 F I))).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0000 (F I : SemanticCore.Class) : nb077AlphaDummy009 F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_focused_notmem_0000 (F I : SemanticCore.Class) : nb077AlphaDummy009 F I ∉ I.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0000 (F I : SemanticCore.Class) : nb077AlphaDummy009 F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0001 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy010 x F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_focused_notmem_0001 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy010 x F I ∉ I.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0001 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy010 x F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0002 (F I : SemanticCore.Class) : nb077AlphaDummy007 F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_focused_notmem_0002 (F I : SemanticCore.Class) : nb077AlphaDummy007 F I ∉ I.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0002 (F I : SemanticCore.Class) : nb077AlphaDummy007 F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0003 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy008 x F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_focused_notmem_0003 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy008 x F I ∉ I.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0003 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy008 x F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0004 (F I : SemanticCore.Class) : nb077AlphaDummy001 F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_focused_notmem_0004 (F I : SemanticCore.Class) : nb077AlphaDummy001 F I ∉ I.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0004 (F I : SemanticCore.Class) : nb077AlphaDummy001 F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0005 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy002 x F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_focused_notmem_0005 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy002 x F I ∉ I.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0005 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy002 x F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0006 (F I : SemanticCore.Class) : nb077AlphaDummy004 F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_focused_notmem_0006 (F I : SemanticCore.Class) : nb077AlphaDummy004 F I ∉ I.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0006 (F I : SemanticCore.Class) : nb077AlphaDummy004 F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0007 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy006 x F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_focused_notmem_0007 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy006 x F I ∉ I.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0007 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy006 x F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0008 (F I : SemanticCore.Class) : nb077AlphaDummy003 F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_focused_notmem_0008 (F I : SemanticCore.Class) : nb077AlphaDummy003 F I ∉ I.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0008 (F I : SemanticCore.Class) : nb077AlphaDummy003 F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0009 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy005 x F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_focused_notmem_0009 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy005 x F I ∉ I.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_wpp_notmem_0009 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy005 x F I ∉ (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_envfresh_0000 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TEnvFresh [(nb077AlphaDummy009 F I, nb077AlphaDummy010 x F I), (nb077AlphaDummy007 F I, nb077AlphaDummy008 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077WppRefl0000 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TReflOn [(nb077AlphaDummy009 F I, nb077AlphaDummy010 x F I), (nb077AlphaDummy007 F I, nb077AlphaDummy008 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

Checked nominal proof certificate identified upstream as nb077_wpp_refl_0000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077WppRefl0000 x F I = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_envfresh_0001 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TEnvFresh [(nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077WppRefl0001 (x : SemanticCore.Var) (F I : SemanticCore.Class) : Nominal.TReflOn [(nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)] (Compiler.CompactSourceSyntax.synCsn (Compiler.CompactSourceSyntax.synCop Compiler.CompactSourceSyntax.synC0c I)).fv

Checked nominal proof certificate identified upstream as nb077_wpp_refl_0001.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077WppRefl0001 x F I = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0030 (F I : SemanticCore.Class) : nb077AlphaDummy016 F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0031 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy018 x F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0032 (F I : SemanticCore.Class) : nb077AlphaDummy015 F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0033 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy017 x F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0034 (F I : SemanticCore.Class) : nb077AlphaDummy013 F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0035 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy014 x F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0036 (F I : SemanticCore.Class) : nb077AlphaDummy011 F I ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077_compact_fv_empty_0037 (x : SemanticCore.Var) (F I : SemanticCore.Class) : nb077AlphaDummy012 x F I ∉ ∅