NF weak partition development: NAR4C081C001Part005.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb081SplitAlpha0001 (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.TAlphaWff [(nb081AlphaDummy001 A, y), (nb081AlphaDummy000 A, x), (nb081AlphaDummy002 A, nb081AlphaDummy003 x y A)] ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb081AlphaDummy002 A)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv (nb081AlphaDummy000 A)) (SemanticCore.Class.cv (nb081AlphaDummy001 A)))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv (nb081AlphaDummy000 A)) (SemanticCore.Class.cv (nb081AlphaDummy001 A))) A).neg) ((SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb081AlphaDummy003 x y A)) (Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))).imp (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A).neg)

Checked nominal proof certificate identified upstream as nb081_split_alpha_0001.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfKqrel (x y : SemanticCore.Var) (A : SemanticCore.Class) (dv_A_x : x ∉ A.fv) (dv_A_y : y ∉ A.fv) (dv_x_y : x ≠ y) : Nominal.NPrf (SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCkqrel A) (Compiler.CompactSourceSyntax.synCopab x y (SemanticCore.Wff.classMem (Compiler.CompactSourceSyntax.synCopk (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)) A)))

Checked nominal proof certificate identified upstream as nominal_df_kqrel.

Equations

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