NF weak partition development: NAR4H5C092M3Part003.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092SplitAlpha0003
(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)
(dv_a_b : a ≠ b)
(dv_a_x : a ≠ x)
(dv_b_x : b ≠ x)
(dv_b_y : b ≠ y)
(dv_x_y : x ≠ y)
:
Nominal.TAlphaWff
[(nb092AlphaDummy001 R, b), (nb092AlphaDummy000 R, a), (nb092AlphaDummy004 R, nb092AlphaDummy005 x y R a b)]
((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy004 R))
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb092AlphaDummy000 R))
(SemanticCore.Class.cv (nb092AlphaDummy001 R)))).imp
(Compiler.CompactSourceSyntax.synWrex (nb092AlphaDummy002 R) (SemanticCore.Class.cv (nb092AlphaDummy000 R))
(Compiler.CompactSourceSyntax.synWrex (nb092AlphaDummy003 R) (SemanticCore.Class.cv (nb092AlphaDummy001 R))
(Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb092AlphaDummy002 R)) R
(SemanticCore.Class.cv (nb092AlphaDummy003 R))))).neg)
((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy005 x y R a b))
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv a) (SemanticCore.Class.cv b))).imp
(Compiler.CompactSourceSyntax.synWrex x (SemanticCore.Class.cv a)
(Compiler.CompactSourceSyntax.synWrex y (SemanticCore.Class.cv b)
(Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y)))).neg)
Checked nominal proof certificate identified upstream as nb092_split_alpha_0003.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfLnqrel
(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)
(dv_a_b : a ≠ b)
(dv_a_x : a ≠ x)
(__dv_a_y : a ≠ y)
(dv_b_x : b ≠ x)
(dv_b_y : b ≠ y)
(dv_x_y : x ≠ y)
:
Nominal.NPrf
(SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synClnqrel R)
(Compiler.CompactSourceSyntax.synCopab a b
(Compiler.CompactSourceSyntax.synWrex x (SemanticCore.Class.cv a)
(Compiler.CompactSourceSyntax.synWrex y (SemanticCore.Class.cv b)
(Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv x) R (SemanticCore.Class.cv y))))))
Checked nominal proof certificate identified upstream as nominal_df_lnqrel.
Equations
- One or more equations did not get rendered due to their size.