NF weak partition development: NAR4H5C091M3BPart008.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091SplitAlpha0013 (D R : SemanticCore.Class) (p : SemanticCore.Var) : Nominal.TAlphaWff [(nb091AlphaDummy184 D R, nb091AlphaDummy186 D R p), (nb091AlphaDummy183 D R, nb091AlphaDummy185 D R p), (nb091AlphaDummy213 D R, nb091AlphaDummy214 D R p), (nb091AlphaDummy187 D R, nb091AlphaDummy188 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)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy184 D R)) (SemanticCore.Class.cv (nb091AlphaDummy041 D R))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy183 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy186 D R p)) (SemanticCore.Class.cv (nb091AlphaDummy043 D R p))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy185 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb091_split_alpha_0013.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091SplitAlpha0014 (D R : SemanticCore.Class) (p : SemanticCore.Var) : Nominal.TAlphaWff [(nb091AlphaDummy187 D R, nb091AlphaDummy188 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)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy187 D R)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy183 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy184 D R) (SemanticCore.Class.cv (nb091AlphaDummy042 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy183 D R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy187 D R)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy183 D R) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy184 D R) (SemanticCore.Class.cv (nb091AlphaDummy041 D R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy183 D R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy184 D R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy188 D R p)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy185 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy186 D R p) (SemanticCore.Class.cv (nb091AlphaDummy044 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy185 D R p)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb091AlphaDummy188 D R p)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb091AlphaDummy185 D R p) (Compiler.CompactSourceSyntax.synWrex (nb091AlphaDummy186 D R p) (SemanticCore.Class.cv (nb091AlphaDummy043 D R p)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb091AlphaDummy185 D R p)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb091AlphaDummy186 D R p))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)

Checked nominal proof certificate identified upstream as nb091_split_alpha_0014.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0578 (D R : SemanticCore.Class) : nb091AlphaDummy042 D R ∉ (Compiler.CompactSourceSyntax.synChwniso D).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0579 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy044 D R p ∉ (Compiler.CompactSourceSyntax.synChwniso D).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0580 (D R : SemanticCore.Class) : nb091AlphaDummy041 D R ∉ (Compiler.CompactSourceSyntax.synChwniso D).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0581 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy043 D R p ∉ (Compiler.CompactSourceSyntax.synChwniso D).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0582 (D R : SemanticCore.Class) : nb091AlphaDummy001 D R ∉ (Compiler.CompactSourceSyntax.synChwniso D).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0583 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy002 D R p ∉ (Compiler.CompactSourceSyntax.synChwniso D).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0584 (D R : SemanticCore.Class) : nb091AlphaDummy000 D R ∉ (Compiler.CompactSourceSyntax.synChwniso D).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0585 (D : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) : p ∉ (Compiler.CompactSourceSyntax.synChwniso D).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0586 (D R : SemanticCore.Class) : nb091AlphaDummy003 D R ∉ (Compiler.CompactSourceSyntax.synChwniso D).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_wpp_notmem_0587 (D R : SemanticCore.Class) (p : SemanticCore.Var) : nb091AlphaDummy004 D R p ∉ (Compiler.CompactSourceSyntax.synChwniso D).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091_compact_envfresh_0048 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) : Nominal.TEnvFresh [(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.synChwniso D).fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091WppRefl0045 (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) : Nominal.TReflOn [(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.synChwniso D).fv

Checked nominal proof certificate identified upstream as nb091_wpp_refl_0045.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb091WppRefl0045 D R p dv_D_p = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfHnwcutmap (D R : SemanticCore.Class) (p : SemanticCore.Var) (dv_D_p : p ∉ D.fv) (dv_R_p : p ∉ R.fv) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synChnwcutmap R D) (Compiler.CompactSourceSyntax.synCmpt p (Compiler.CompactSourceSyntax.synCpw1 (Compiler.CompactSourceSyntax.synCpw1 D)) (Compiler.CompactSourceSyntax.synCec (Compiler.CompactSourceSyntax.synChnwcutcode R D (Compiler.CompactSourceSyntax.synCuni (Compiler.CompactSourceSyntax.synCuni (SemanticCore.Class.cv p)))) (Compiler.CompactSourceSyntax.synChwniso D))))

Checked nominal proof certificate identified upstream as nominal_df_hnwcutmap.

Equations

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