NF weak partition development: NAR5H088P001Part005.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088SplitAlpha0002 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : Nominal.TAlphaWff [(nb088AlphaDummy001 A B C R, nb088AlphaDummy002 u A B C R), (nb088AlphaDummy000 A B C R, u), (nb088AlphaDummy003 A B C R, nb088AlphaDummy004 u A B C R)] (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy003 A B C R)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb088AlphaDummy000 A B C R)) (SemanticCore.Class.cv (nb088AlphaDummy001 A B C R)))) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb088AlphaDummy004 u A B C R)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv u) (SemanticCore.Class.cv (nb088AlphaDummy002 u A B C R))))

Checked nominal proof certificate identified upstream as nb088_split_alpha_0002.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_focused_notmem_0000 (A B C R : SemanticCore.Class) : nb088AlphaDummy001 A B C R ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_wpp_notmem_0106 (A B C R : SemanticCore.Class) : nb088AlphaDummy001 A B C R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 C)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_focused_notmem_0001 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : nb088AlphaDummy002 u A B C R ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_wpp_notmem_0107 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : nb088AlphaDummy002 u A B C R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 C)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_focused_notmem_0002 (A B C R : SemanticCore.Class) : nb088AlphaDummy000 A B C R ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_wpp_notmem_0108 (A B C R : SemanticCore.Class) : nb088AlphaDummy000 A B C R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 C)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_wpp_notmem_0109 (u : SemanticCore.Var) (C : SemanticCore.Class) (dv_C_u : u ∉ C.fv) : u ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 C)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_focused_notmem_0003 (A B C R : SemanticCore.Class) : nb088AlphaDummy003 A B C R ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_wpp_notmem_0110 (A B C R : SemanticCore.Class) : nb088AlphaDummy003 A B C R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 C)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_focused_notmem_0004 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : nb088AlphaDummy004 u A B C R ∉ C.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_wpp_notmem_0111 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) : nb088AlphaDummy004 u A B C R ∉ (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 C)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088_compact_envfresh_0007 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) (dv_C_u : u ∉ C.fv) : Nominal.TEnvFresh [(nb088AlphaDummy001 A B C R, nb088AlphaDummy002 u A B C R), (nb088AlphaDummy000 A B C R, u), (nb088AlphaDummy003 A B C R, nb088AlphaDummy004 u A B C R)] (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 C)).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088WppRefl0007 (u : SemanticCore.Var) (A B C R : SemanticCore.Class) (dv_C_u : u ∉ C.fv) : Nominal.TReflOn [(nb088AlphaDummy001 A B C R, nb088AlphaDummy002 u A B C R), (nb088AlphaDummy000 A B C R, u), (nb088AlphaDummy003 A B C R, nb088AlphaDummy004 u A B C R)] (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 C)).fv

Checked nominal proof certificate identified upstream as nb088_wpp_refl_0007.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb088WppRefl0007 u A B C R dv_C_u = ⋯.reflOn