Nominal proof certificates grouped in dependency order.
Certificates from NAR4C073C001Part006.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb073SplitAlpha0002
(x y : SemanticCore.Var)
(dv_x_y : x ≠ y)
:
Nominal.TAlphaWff
[(nb073AlphaDummy012, nb073AlphaDummy013 x y), (nb073AlphaDummy010, nb073AlphaDummy011 x y), (nb073AlphaDummy002, nb073AlphaDummy003 x y), (nb073AlphaDummy001, y), (nb073AlphaDummy000, x), (nb073AlphaDummy004, nb073AlphaDummy005 x y)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb073AlphaDummy012)
(SemanticCore.Class.cab nb073AlphaDummy006
(Compiler.CompactSourceSyntax.synWrex nb073AlphaDummy007
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb073AlphaDummy000)
(SemanticCore.Class.cv nb073AlphaDummy001))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb073AlphaDummy006)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb073AlphaDummy007)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb073AlphaDummy012)
(SemanticCore.Class.cab nb073AlphaDummy006
(Compiler.CompactSourceSyntax.synWrex nb073AlphaDummy007
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv nb073AlphaDummy000)
(SemanticCore.Class.cv nb073AlphaDummy001))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb073AlphaDummy006)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb073AlphaDummy007)))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb073AlphaDummy013 x y))
(SemanticCore.Class.cab (nb073AlphaDummy008 x y)
(Compiler.CompactSourceSyntax.synWrex (nb073AlphaDummy009 x y)
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb073AlphaDummy008 x y))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb073AlphaDummy009 x y))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb073AlphaDummy013 x y))
(SemanticCore.Class.cab (nb073AlphaDummy008 x y)
(Compiler.CompactSourceSyntax.synWrex (nb073AlphaDummy009 x y)
(Compiler.CompactSourceSyntax.synCop (SemanticCore.Class.cv x) (SemanticCore.Class.cv y))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb073AlphaDummy008 x y))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb073AlphaDummy009 x y))))))).neg)
Checked nominal proof certificate identified upstream as nb073_split_alpha_0002.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C073C001Part007.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb073SplitAlpha0003
(x y : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb073AlphaDummy007, nb073AlphaDummy009 x y), (nb073AlphaDummy006, nb073AlphaDummy008 x y), (nb073AlphaDummy072, nb073AlphaDummy073 x y), (nb073AlphaDummy010, nb073AlphaDummy011 x y), (nb073AlphaDummy002, nb073AlphaDummy003 x y), (nb073AlphaDummy001, y), (nb073AlphaDummy000, x), (nb073AlphaDummy004, nb073AlphaDummy005 x y)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb073AlphaDummy007) (SemanticCore.Class.cv nb073AlphaDummy002)).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb073AlphaDummy006)
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb073AlphaDummy007))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb073AlphaDummy009 x y))
(SemanticCore.Class.cv (nb073AlphaDummy003 x y))).imp
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb073AlphaDummy008 x y))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb073AlphaDummy009 x y)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
Checked nominal proof certificate identified upstream as nb073_split_alpha_0003.
Equations
- One or more equations did not get rendered due to their size.