NF weak partition development: NAR4C084C001Part004.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0005
(x y : SemanticCore.Var)
(A B R : SemanticCore.Class)
(d : SemanticCore.Var)
(dv_R_d : d ∉ R.fv)
(dv_R_x : x ∉ R.fv)
(dv_R_y : y ∉ R.fv)
:
Nominal.TReflOn
[(nb084AlphaDummy004 A B R, nb084AlphaDummy006 x y A R), (nb084AlphaDummy003 A B R, nb084AlphaDummy005 x y A R), (nb084AlphaDummy002 A B R, y), (nb084AlphaDummy001 A B R, x), (nb084AlphaDummy000 A B R, d)]
R.fv
Checked nominal proof certificate identified upstream as nb084_focused_refl_0005.
Equations
- NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb084FocusedRefl0005 x y A B R d dv_R_d dv_R_x dv_R_y = ⋯.reflOn
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFdif
(x y : SemanticCore.Var)
(A B R : SemanticCore.Class)
(d : SemanticCore.Var)
(__dv_A_B : Disjoint A.fv B.fv)
(__dv_A_R : Disjoint A.fv R.fv)
(dv_A_d : d ∉ A.fv)
(dv_A_x : x ∉ A.fv)
(dv_A_y : y ∉ A.fv)
(__dv_B_R : Disjoint B.fv R.fv)
(dv_B_d : d ∉ B.fv)
(dv_B_x : x ∉ B.fv)
(dv_B_y : y ∉ B.fv)
(dv_R_d : d ∉ R.fv)
(dv_R_x : x ∉ R.fv)
(dv_R_y : y ∉ R.fv)
(dv_d_x : d ≠ x)
(dv_d_y : d ≠ y)
(dv_x_y : x ≠ y)
:
Nominal.NPrf
(SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfdif R A B)
(Compiler.CompactSourceSyntax.synCrab d A
(Compiler.CompactSourceSyntax.synWrex x B
(Compiler.CompactSourceSyntax.synWrex y B
(SemanticCore.Wff.classMem (SemanticCore.Class.cv d)
(Compiler.CompactSourceSyntax.synCfpiv R A (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)))))))
Checked nominal proof certificate identified upstream as nominal_df_fdif.
Equations
- One or more equations did not get rendered due to their size.