NF weak partition development: NAR4C082C001Part006.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0039 (A B R : SemanticCore.Class) (p : SemanticCore.Var) : nb082AlphaDummy043 A B R p ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0040 (A B R : SemanticCore.Class) (p : SemanticCore.Var) : nb082AlphaDummy043 A B R p ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_wpp_notmem_0123 (A B R : SemanticCore.Class) (p : SemanticCore.Var) : nb082AlphaDummy043 A B R p ∉ (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0041 (A B R : SemanticCore.Class) : nb082AlphaDummy001 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0042 (A B R : SemanticCore.Class) : nb082AlphaDummy001 A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_wpp_notmem_0124 (A B R : SemanticCore.Class) : nb082AlphaDummy001 A B R ∉ (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0043 (A B R : SemanticCore.Class) (p : SemanticCore.Var) : nb082AlphaDummy002 A B R p ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0044 (A B R : SemanticCore.Class) (p : SemanticCore.Var) : nb082AlphaDummy002 A B R p ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_wpp_notmem_0125 (A B R : SemanticCore.Class) (p : SemanticCore.Var) : nb082AlphaDummy002 A B R p ∉ (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0045 (A B R : SemanticCore.Class) : nb082AlphaDummy000 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0046 (A B R : SemanticCore.Class) : nb082AlphaDummy000 A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_wpp_notmem_0126 (A B R : SemanticCore.Class) : nb082AlphaDummy000 A B R ∉ (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_wpp_notmem_0127 (A B R : SemanticCore.Class) (p : SemanticCore.Var) (dv_A_p : p ∉ A.fv) (dv_B_p : p ∉ B.fv) (dv_R_p : p ∉ R.fv) : p ∉ (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0047 (A B R : SemanticCore.Class) : nb082AlphaDummy003 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0048 (A B R : SemanticCore.Class) : nb082AlphaDummy003 A B R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_wpp_notmem_0128 (A B R : SemanticCore.Class) : nb082AlphaDummy003 A B R ∉ (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0049 (A B R : SemanticCore.Class) (p : SemanticCore.Var) : nb082AlphaDummy004 A B R p ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0050 (A B R : SemanticCore.Class) (p : SemanticCore.Var) : nb082AlphaDummy004 A B R p ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_wpp_notmem_0129 (A B R : SemanticCore.Class) (p : SemanticCore.Var) : nb082AlphaDummy004 A B R p ∉ (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_compact_envfresh_0008 (A B R : SemanticCore.Class) (p : SemanticCore.Var) (dv_A_p : p ∉ A.fv) (dv_B_p : p ∉ B.fv) (dv_R_p : p ∉ R.fv) : Nominal.TEnvFresh [(nb082AlphaDummy050 A B R, nb082AlphaDummy052 A B R p), (nb082AlphaDummy049 A B R, nb082AlphaDummy051 A B R p), (nb082AlphaDummy047 A B R, nb082AlphaDummy048 A B R p), (nb082AlphaDummy045 A B R, nb082AlphaDummy046 A B R p), (nb082AlphaDummy042 A B R, nb082AlphaDummy044 A B R p), (nb082AlphaDummy041 A B R, nb082AlphaDummy043 A B R p), (nb082AlphaDummy001 A B R, nb082AlphaDummy002 A B R p), (nb082AlphaDummy000 A B R, p), (nb082AlphaDummy003 A B R, nb082AlphaDummy004 A B R p)] (Compiler.CompactSourceSyntax.synCcnvk (Compiler.CompactSourceSyntax.synCfdminsep R A B)).fv