NF weak partition development: NAR4H5C092M3Part002.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092SplitAlpha0001 (x y : SemanticCore.Var) (R : SemanticCore.Class) (a b : SemanticCore.Var) : Nominal.TAlphaWff [(nb092AlphaDummy043 R, nb092AlphaDummy045 x y), (nb092AlphaDummy042 R, nb092AlphaDummy044 x y), (nb092AlphaDummy072 R, nb092AlphaDummy073 x y), (nb092AlphaDummy046 R, nb092AlphaDummy047 x y), (nb092AlphaDummy003 R, y), (nb092AlphaDummy002 R, x), (nb092AlphaDummy001 R, b), (nb092AlphaDummy000 R, a), (nb092AlphaDummy004 R, nb092AlphaDummy005 x y R a b)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb092AlphaDummy043 R)) (SemanticCore.Class.cv (nb092AlphaDummy003 R))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy042 R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb092AlphaDummy043 R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb092AlphaDummy045 x y)) (SemanticCore.Class.cv y)).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy044 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb092AlphaDummy045 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb092_split_alpha_0001.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092SplitAlpha0002 (x y : SemanticCore.Var) (R : SemanticCore.Class) (a b : SemanticCore.Var) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb092AlphaDummy046 R, nb092AlphaDummy047 x y), (nb092AlphaDummy003 R, y), (nb092AlphaDummy002 R, x), (nb092AlphaDummy001 R, b), (nb092AlphaDummy000 R, a), (nb092AlphaDummy004 R, nb092AlphaDummy005 x y R a b)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb092AlphaDummy046 R)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb092AlphaDummy042 R) (Compiler.CompactSourceSyntax.synWrex (nb092AlphaDummy043 R) (SemanticCore.Class.cv (nb092AlphaDummy002 R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy042 R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb092AlphaDummy043 R)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb092AlphaDummy046 R)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb092AlphaDummy042 R) (Compiler.CompactSourceSyntax.synWrex (nb092AlphaDummy043 R) (SemanticCore.Class.cv (nb092AlphaDummy003 R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy042 R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb092AlphaDummy043 R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb092AlphaDummy047 x y)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb092AlphaDummy044 x y) (Compiler.CompactSourceSyntax.synWrex (nb092AlphaDummy045 x y) (SemanticCore.Class.cv x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy044 x y)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb092AlphaDummy045 x y)))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb092AlphaDummy047 x y)) (Compiler.CompactSourceSyntax.synCcompl (SemanticCore.Class.cab (nb092AlphaDummy044 x y) (Compiler.CompactSourceSyntax.synWrex (nb092AlphaDummy045 x y) (SemanticCore.Class.cv y) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy044 x y)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb092AlphaDummy045 x y))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))))))).neg)

Checked nominal proof certificate identified upstream as nb092_split_alpha_0002.

Equations

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092_focused_notmem_0000 (R : SemanticCore.Class) : nb092AlphaDummy003 R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092_focused_notmem_0001 (R : SemanticCore.Class) : nb092AlphaDummy002 R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092_focused_notmem_0002 (R : SemanticCore.Class) : nb092AlphaDummy001 R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092_focused_notmem_0003 (R : SemanticCore.Class) : nb092AlphaDummy000 R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092_focused_notmem_0004 (R : SemanticCore.Class) : nb092AlphaDummy004 R ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092_focused_notmem_0005 (x y : SemanticCore.Var) (R : SemanticCore.Class) (a b : SemanticCore.Var) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) : nb092AlphaDummy005 x y R a b ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092_compact_envfresh_0014 (x y : SemanticCore.Var) (R : SemanticCore.Class) (a b : SemanticCore.Var) (dv_R_a : a ∉ R.fv) (dv_R_b : b ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) : Nominal.TEnvFresh [(nb092AlphaDummy003 R, y), (nb092AlphaDummy002 R, x), (nb092AlphaDummy001 R, b), (nb092AlphaDummy000 R, a), (nb092AlphaDummy004 R, nb092AlphaDummy005 x y R a b)] R.fv

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092FocusedRefl0000 (x y : SemanticCore.Var) (R : SemanticCore.Class) (a b : SemanticCore.Var) (dv_R_a : a ∉ R.fv) (dv_R_b : b ∉ R.fv) (dv_R_x : x ∉ R.fv) (dv_R_y : y ∉ R.fv) : Nominal.TReflOn [(nb092AlphaDummy003 R, y), (nb092AlphaDummy002 R, x), (nb092AlphaDummy001 R, b), (nb092AlphaDummy000 R, a), (nb092AlphaDummy004 R, nb092AlphaDummy005 x y R a b)] R.fv

Checked nominal proof certificate identified upstream as nb092_focused_refl_0000.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092FocusedRefl0000 x y R a b dv_R_a dv_R_b dv_R_x dv_R_y = ⋯.reflOn