NF weak partition development: NAR4H5C092M3Part002.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb092SplitAlpha0000 (x y : SemanticCore.Var) (R : SemanticCore.Class) (a b : SemanticCore.Var) : Nominal.TAlphaWff [(nb092AlphaDummy036 R, nb092AlphaDummy037 a b), (nb092AlphaDummy010 R, nb092AlphaDummy011 a b), (nb092AlphaDummy001 R, b), (nb092AlphaDummy000 R, a), (nb092AlphaDummy004 R, nb092AlphaDummy005 x y R a b)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb092AlphaDummy036 R)) (SemanticCore.Class.cab (nb092AlphaDummy006 R) (Compiler.CompactSourceSyntax.synWrex (nb092AlphaDummy007 R) (SemanticCore.Class.cv (nb092AlphaDummy001 R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy006 R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb092AlphaDummy007 R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb092AlphaDummy036 R)) (SemanticCore.Class.cab (nb092AlphaDummy006 R) (Compiler.CompactSourceSyntax.synWrex (nb092AlphaDummy007 R) (SemanticCore.Class.cv (nb092AlphaDummy001 R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy006 R)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb092AlphaDummy007 R))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb092AlphaDummy037 a b)) (SemanticCore.Class.cab (nb092AlphaDummy008 a b) (Compiler.CompactSourceSyntax.synWrex (nb092AlphaDummy009 a b) (SemanticCore.Class.cv b) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy008 a b)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb092AlphaDummy009 a b))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb092AlphaDummy037 a b)) (SemanticCore.Class.cab (nb092AlphaDummy008 a b) (Compiler.CompactSourceSyntax.synWrex (nb092AlphaDummy009 a b) (SemanticCore.Class.cv b) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb092AlphaDummy008 a b)) (Compiler.CompactSourceSyntax.synCun (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb092AlphaDummy009 a b))) (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))))).neg)

Checked nominal proof certificate identified upstream as nb092_split_alpha_0000.

Equations

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