NF weak partition development: NAR4C082C001Part005.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082SplitAlpha0002 (A B R : SemanticCore.Class) (p : SemanticCore.Var) : Nominal.TAlphaWff [(nb082AlphaDummy001 A B R, nb082AlphaDummy002 A B R p), (nb082AlphaDummy000 A B R, p), (nb082AlphaDummy003 A B R, nb082AlphaDummy004 A B R p)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb082AlphaDummy003 A B R)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb082AlphaDummy000 A B R)) (SemanticCore.Class.cv (nb082AlphaDummy001 A B R)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb082AlphaDummy004 A B R p)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv p) (SemanticCore.Class.cv (nb082AlphaDummy002 A B R p))))

Checked nominal proof certificate identified upstream as nb082_split_alpha_0002.

Equations

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_wpp_notmem_0106 (A B R : SemanticCore.Class) : nb082AlphaDummy001 A B R ∉ (Compiler.CompactSourceSyntax.synCxpk B B).fv

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_wpp_notmem_0108 (A B R : SemanticCore.Class) : nb082AlphaDummy000 A B R ∉ (Compiler.CompactSourceSyntax.synCxpk B B).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_wpp_notmem_0109 (B : SemanticCore.Class) (p : SemanticCore.Var) (dv_B_p : p ∉ B.fv) : p ∉ (Compiler.CompactSourceSyntax.synCxpk B B).fv

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_wpp_notmem_0110 (A B R : SemanticCore.Class) : nb082AlphaDummy003 A B R ∉ (Compiler.CompactSourceSyntax.synCxpk B B).fv

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_compact_envfresh_0007 (A B R : SemanticCore.Class) (p : SemanticCore.Var) (dv_B_p : p ∉ B.fv) : Nominal.TEnvFresh [(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.synCxpk B B).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082WppRefl0007 (A B R : SemanticCore.Class) (p : SemanticCore.Var) (dv_B_p : p ∉ B.fv) : Nominal.TReflOn [(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.synCxpk B B).fv

Checked nominal proof certificate identified upstream as nb082_wpp_refl_0007.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082WppRefl0007 A B R p dv_B_p = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0005 (A B R : SemanticCore.Class) : nb082AlphaDummy050 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0006 (A B R : SemanticCore.Class) : nb082AlphaDummy050 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0007 (A B R : SemanticCore.Class) : nb082AlphaDummy050 A B R ∉ R.fv

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0011 (A B R : SemanticCore.Class) : nb082AlphaDummy049 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0012 (A B R : SemanticCore.Class) : nb082AlphaDummy049 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0013 (A B R : SemanticCore.Class) : nb082AlphaDummy049 A B R ∉ R.fv

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0017 (A B R : SemanticCore.Class) : nb082AlphaDummy047 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0018 (A B R : SemanticCore.Class) : nb082AlphaDummy047 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0019 (A B R : SemanticCore.Class) : nb082AlphaDummy047 A B R ∉ R.fv

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0023 (A B R : SemanticCore.Class) : nb082AlphaDummy045 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0024 (A B R : SemanticCore.Class) : nb082AlphaDummy045 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0025 (A B R : SemanticCore.Class) : nb082AlphaDummy045 A B R ∉ R.fv

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0029 (A B R : SemanticCore.Class) : nb082AlphaDummy042 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0030 (A B R : SemanticCore.Class) : nb082AlphaDummy042 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0031 (A B R : SemanticCore.Class) : nb082AlphaDummy042 A B R ∉ R.fv

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

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

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

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0035 (A B R : SemanticCore.Class) : nb082AlphaDummy041 A B R ∉ A.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0036 (A B R : SemanticCore.Class) : nb082AlphaDummy041 A B R ∉ B.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb082_focused_notmem_0037 (A B R : SemanticCore.Class) : nb082AlphaDummy041 A B R ∉ R.fv

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

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