NF weak partition development: NAR4H5C091M3BPart006.
theorem
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0065
(D R : SemanticCore.Class)
(p : SemanticCore.Var)
:
nb091AlphaDummy062 D R p ∉ R.fv
theorem
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0067
(D R : SemanticCore.Class)
(p : SemanticCore.Var)
:
nb091AlphaDummy061 D R p ∉ R.fv
theorem
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_focused_notmem_0069
(D R : SemanticCore.Class)
(p : SemanticCore.Var)
:
nb091AlphaDummy064 D R p ∉ R.fv
theorem
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_envfresh_0024
(D R : SemanticCore.Class)
(p : SemanticCore.Var)
(dv_R_p : p ∉ R.fv)
:
Nominal.TEnvFresh
[(nb091AlphaDummy106 D R, nb091AlphaDummy108 R p), (nb091AlphaDummy105 D R, nb091AlphaDummy107 R p), (nb091AlphaDummy103 D R, nb091AlphaDummy104 D R p), (nb091AlphaDummy101 D R, nb091AlphaDummy102 D R p), (nb091AlphaDummy060 D R, nb091AlphaDummy062 D R p), (nb091AlphaDummy059 D R, nb091AlphaDummy061 D R p), (nb091AlphaDummy063 D R, nb091AlphaDummy064 D R p), (nb091AlphaDummy057 D R, nb091AlphaDummy058 D R p), (nb091AlphaDummy055 D R, nb091AlphaDummy056 D R p), (nb091AlphaDummy048 D R, nb091AlphaDummy050 D R p), (nb091AlphaDummy047 D R, nb091AlphaDummy049 D R p), (nb091AlphaDummy053 D R, nb091AlphaDummy054 D R p), (nb091AlphaDummy051 D R, nb091AlphaDummy052 D R p), (nb091AlphaDummy045 D R, nb091AlphaDummy046 D R p), (nb091AlphaDummy042 D R, nb091AlphaDummy044 D R p), (nb091AlphaDummy041 D R, nb091AlphaDummy043 D R p), (nb091AlphaDummy001 D R, nb091AlphaDummy002 D R p), (nb091AlphaDummy000 D R, p), (nb091AlphaDummy003 D R, nb091AlphaDummy004 D R p)]
(Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv