NF weak partition development: NAR4C083C001Part004.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb083SplitAlpha0001
(A B C R : SemanticCore.Class)
(b c : SemanticCore.Var)
(dv_A_b : b ∉ A.fv)
(dv_A_c : c ∉ A.fv)
(dv_B_b : b ∉ B.fv)
(dv_B_c : c ∉ B.fv)
(dv_C_b : b ∉ C.fv)
(dv_C_c : c ∉ C.fv)
(dv_R_b : b ∉ R.fv)
(dv_R_c : c ∉ R.fv)
(dv_b_c : b ≠ c)
:
Nominal.TAlphaWff [(nb083AlphaDummy000 A B C R, b)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb083AlphaDummy000 A B C R)) A).imp
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb083AlphaDummy000 A B C R))
(Compiler.CompactSourceSyntax.synCsep2 B C))
(Compiler.CompactSourceSyntax.synWral (nb083AlphaDummy001 A B C R) A
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb083AlphaDummy001 A B C R))
(Compiler.CompactSourceSyntax.synCsep2 B C)).imp
(Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv (nb083AlphaDummy000 A B C R)) R
(SemanticCore.Class.cv (nb083AlphaDummy001 A B C R)))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv b) A).imp
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synCsep2 B C))
(Compiler.CompactSourceSyntax.synWral c A
((SemanticCore.Wff.classMem (SemanticCore.Class.cv c) (Compiler.CompactSourceSyntax.synCsep2 B C)).imp
(Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv b) R (SemanticCore.Class.cv c))))).neg)
Checked nominal proof certificate identified upstream as nb083_split_alpha_0001.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nominalDfFpiv
(A B C R : SemanticCore.Class)
(b c : SemanticCore.Var)
(__dv_A_B : Disjoint A.fv B.fv)
(__dv_A_C : Disjoint A.fv C.fv)
(__dv_A_R : Disjoint A.fv R.fv)
(dv_A_b : b ∉ A.fv)
(dv_A_c : c ∉ A.fv)
(__dv_B_C : Disjoint B.fv C.fv)
(__dv_B_R : Disjoint B.fv R.fv)
(dv_B_b : b ∉ B.fv)
(dv_B_c : c ∉ B.fv)
(__dv_C_R : Disjoint C.fv R.fv)
(dv_C_b : b ∉ C.fv)
(dv_C_c : c ∉ C.fv)
(dv_R_b : b ∉ R.fv)
(dv_R_c : c ∉ R.fv)
(dv_b_c : b ≠ c)
:
Nominal.NPrf
(SemanticCore.Wff.classEq (Compiler.CompactSourceSyntax.synCfpiv R A B C)
(Compiler.CompactSourceSyntax.synCrab b A
(Compiler.CompactSourceSyntax.synWa
(SemanticCore.Wff.classMem (SemanticCore.Class.cv b) (Compiler.CompactSourceSyntax.synCsep2 B C))
(Compiler.CompactSourceSyntax.synWral c A
((SemanticCore.Wff.classMem (SemanticCore.Class.cv c) (Compiler.CompactSourceSyntax.synCsep2 B C)).imp
(Compiler.CompactSourceSyntax.synWbr (SemanticCore.Class.cv b) R (SemanticCore.Class.cv c)))))))
Checked nominal proof certificate identified upstream as nominal_df_fpiv.
Equations
- One or more equations did not get rendered due to their size.