NF weak partition development: NAR4H5C096M3Part003.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096SplitAlpha0003 (D R : SemanticCore.Class) (q : SemanticCore.Var) : Nominal.TAlphaWff [(nb096AlphaDummy071 D R, nb096AlphaDummy072 R q), (nb096AlphaDummy069 D R, nb096AlphaDummy070 R q), (nb096AlphaDummy052 D R, nb096AlphaDummy054 R q), (nb096AlphaDummy051 D R, nb096AlphaDummy053 R q), (nb096AlphaDummy049 D R, nb096AlphaDummy050 D R q), (nb096AlphaDummy047 D R, nb096AlphaDummy048 D R q), (nb096AlphaDummy045 D R, nb096AlphaDummy046 D R q), (nb096AlphaDummy042 D R, nb096AlphaDummy044 D R q), (nb096AlphaDummy041 D R, nb096AlphaDummy043 D R q), (nb096AlphaDummy001 D R, nb096AlphaDummy002 D R q), (nb096AlphaDummy000 D R, q), (nb096AlphaDummy003 D R, nb096AlphaDummy004 D R q)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy071 D R)) (SemanticCore.Class.cab (nb096AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy066 D R) (SemanticCore.Class.cv (nb096AlphaDummy052 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy066 D R))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy071 D R)) (SemanticCore.Class.cab (nb096AlphaDummy065 D R) (Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy066 D R) (SemanticCore.Class.cv (nb096AlphaDummy052 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy065 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy066 D R))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy072 R q)) (SemanticCore.Class.cab (nb096AlphaDummy067 R q) (Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy068 R q) (SemanticCore.Class.cv (nb096AlphaDummy054 R q)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy067 R q)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy068 R q))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy072 R q)) (SemanticCore.Class.cab (nb096AlphaDummy067 R q) (Compiler.CompactSourceSyntax.synWrex (nb096AlphaDummy068 R q) (SemanticCore.Class.cv (nb096AlphaDummy054 R q)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb096AlphaDummy067 R q)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy068 R q))))))).neg)

Checked nominal proof certificate identified upstream as nb096_split_alpha_0003.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096SplitAlpha0004 (D R : SemanticCore.Class) (q : SemanticCore.Var) : Nominal.TAlphaWff [(nb096AlphaDummy099 D R, nb096AlphaDummy100 R q), (nb096AlphaDummy097 D R, nb096AlphaDummy098 R q), (nb096AlphaDummy066 D R, nb096AlphaDummy068 R q), (nb096AlphaDummy065 D R, nb096AlphaDummy067 R q), (nb096AlphaDummy095 D R, nb096AlphaDummy096 R q), (nb096AlphaDummy069 D R, nb096AlphaDummy070 R q), (nb096AlphaDummy052 D R, nb096AlphaDummy054 R q), (nb096AlphaDummy051 D R, nb096AlphaDummy053 R q), (nb096AlphaDummy049 D R, nb096AlphaDummy050 D R q), (nb096AlphaDummy047 D R, nb096AlphaDummy048 D R q), (nb096AlphaDummy045 D R, nb096AlphaDummy046 D R q), (nb096AlphaDummy042 D R, nb096AlphaDummy044 D R q), (nb096AlphaDummy041 D R, nb096AlphaDummy043 D R q), (nb096AlphaDummy001 D R, nb096AlphaDummy002 D R q), (nb096AlphaDummy000 D R, q), (nb096AlphaDummy003 D R, nb096AlphaDummy004 D R q)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy099 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy066 D R)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy099 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy066 D R)))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy100 R q)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy068 R q)))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb096AlphaDummy100 R q)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb096AlphaDummy068 R q)))).neg)

Checked nominal proof certificate identified upstream as nb096_split_alpha_0004.

Equations

• One or more equations did not get rendered due to their size.

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0015 (D R : SemanticCore.Class) : nb096AlphaDummy052 D R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0250 (D R : SemanticCore.Class) : nb096AlphaDummy052 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0016 (R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy054 R q ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0251 (R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy054 R q ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0017 (D R : SemanticCore.Class) : nb096AlphaDummy051 D R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0252 (D R : SemanticCore.Class) : nb096AlphaDummy051 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0018 (R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy053 R q ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0253 (R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy053 R q ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0019 (D R : SemanticCore.Class) : nb096AlphaDummy049 D R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0254 (D R : SemanticCore.Class) : nb096AlphaDummy049 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0020 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy050 D R q ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0255 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy050 D R q ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0021 (D R : SemanticCore.Class) : nb096AlphaDummy047 D R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0256 (D R : SemanticCore.Class) : nb096AlphaDummy047 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0022 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy048 D R q ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0257 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy048 D R q ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0023 (D R : SemanticCore.Class) : nb096AlphaDummy045 D R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0258 (D R : SemanticCore.Class) : nb096AlphaDummy045 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0024 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy046 D R q ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0259 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy046 D R q ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0025 (D R : SemanticCore.Class) : nb096AlphaDummy042 D R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0260 (D R : SemanticCore.Class) : nb096AlphaDummy042 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0026 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy044 D R q ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0261 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy044 D R q ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0027 (D R : SemanticCore.Class) : nb096AlphaDummy041 D R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0262 (D R : SemanticCore.Class) : nb096AlphaDummy041 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0028 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy043 D R q ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0263 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy043 D R q ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0029 (D R : SemanticCore.Class) : nb096AlphaDummy001 D R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0264 (D R : SemanticCore.Class) : nb096AlphaDummy001 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0030 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy002 D R q ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0265 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy002 D R q ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0031 (D R : SemanticCore.Class) : nb096AlphaDummy000 D R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0266 (D R : SemanticCore.Class) : nb096AlphaDummy000 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0267 (R : SemanticCore.Class) (q : SemanticCore.Var) (dv_R_q : q ∉ R.fv) : q ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0032 (D R : SemanticCore.Class) : nb096AlphaDummy003 D R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0268 (D R : SemanticCore.Class) : nb096AlphaDummy003 D R ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_focused_notmem_0033 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy004 D R q ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_wpp_notmem_0269 (D R : SemanticCore.Class) (q : SemanticCore.Var) : nb096AlphaDummy004 D R q ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096_compact_envfresh_0016 (D R : SemanticCore.Class) (q : SemanticCore.Var) (dv_R_q : q ∉ R.fv) : Nominal.TEnvFresh [(nb096AlphaDummy052 D R, nb096AlphaDummy054 R q), (nb096AlphaDummy051 D R, nb096AlphaDummy053 R q), (nb096AlphaDummy049 D R, nb096AlphaDummy050 D R q), (nb096AlphaDummy047 D R, nb096AlphaDummy048 D R q), (nb096AlphaDummy045 D R, nb096AlphaDummy046 D R q), (nb096AlphaDummy042 D R, nb096AlphaDummy044 D R q), (nb096AlphaDummy041 D R, nb096AlphaDummy043 D R q), (nb096AlphaDummy001 D R, nb096AlphaDummy002 D R q), (nb096AlphaDummy000 D R, q), (nb096AlphaDummy003 D R, nb096AlphaDummy004 D R q)] (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096WppRefl0015 (D R : SemanticCore.Class) (q : SemanticCore.Var) (dv_R_q : q ∉ R.fv) : Nominal.TReflOn [(nb096AlphaDummy052 D R, nb096AlphaDummy054 R q), (nb096AlphaDummy051 D R, nb096AlphaDummy053 R q), (nb096AlphaDummy049 D R, nb096AlphaDummy050 D R q), (nb096AlphaDummy047 D R, nb096AlphaDummy048 D R q), (nb096AlphaDummy045 D R, nb096AlphaDummy046 D R q), (nb096AlphaDummy042 D R, nb096AlphaDummy044 D R q), (nb096AlphaDummy041 D R, nb096AlphaDummy043 D R q), (nb096AlphaDummy001 D R, nb096AlphaDummy002 D R q), (nb096AlphaDummy000 D R, q), (nb096AlphaDummy003 D R, nb096AlphaDummy004 D R q)] (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

Checked nominal proof certificate identified upstream as nb096_wpp_refl_0015.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb096WppRefl0015 D R q dv_R_q = ⋯.reflOn