Nominal proof certificates grouped in dependency order.
Certificates from NAR4C073C001Part004.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb073SplitAlpha0000
(x y : SemanticCore.Var)
(dv_x_y : x ≠ y)
:
Nominal.TAlphaWff
[(nb073AlphaDummy020, nb073AlphaDummy021 x y), (nb073AlphaDummy018, nb073AlphaDummy019 x y), (nb073AlphaDummy007, nb073AlphaDummy009 x y), (nb073AlphaDummy006, nb073AlphaDummy008 x y), (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 nb073AlphaDummy020)
(SemanticCore.Class.cab nb073AlphaDummy014
(Compiler.CompactSourceSyntax.synWrex nb073AlphaDummy015 (SemanticCore.Class.cv nb073AlphaDummy000)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb073AlphaDummy014)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb073AlphaDummy015)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb073AlphaDummy020)
(SemanticCore.Class.cab nb073AlphaDummy014
(Compiler.CompactSourceSyntax.synWrex nb073AlphaDummy015 (SemanticCore.Class.cv nb073AlphaDummy000)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb073AlphaDummy014)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb073AlphaDummy015)))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb073AlphaDummy021 x y))
(SemanticCore.Class.cab (nb073AlphaDummy016 x y)
(Compiler.CompactSourceSyntax.synWrex (nb073AlphaDummy017 x y) (SemanticCore.Class.cv x)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb073AlphaDummy016 x y))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb073AlphaDummy017 x y))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb073AlphaDummy021 x y))
(SemanticCore.Class.cab (nb073AlphaDummy016 x y)
(Compiler.CompactSourceSyntax.synWrex (nb073AlphaDummy017 x y) (SemanticCore.Class.cv x)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb073AlphaDummy016 x y))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb073AlphaDummy017 x y))))))).neg)
Checked nominal proof certificate identified upstream as nb073_split_alpha_0000.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C073C001Part005.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb073SplitAlpha0001
(x y : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb073AlphaDummy046, nb073AlphaDummy047 x y), (nb073AlphaDummy015, nb073AlphaDummy017 x y), (nb073AlphaDummy014, nb073AlphaDummy016 x y), (nb073AlphaDummy044, nb073AlphaDummy045 x y), (nb073AlphaDummy018, nb073AlphaDummy019 x y), (nb073AlphaDummy007, nb073AlphaDummy009 x y), (nb073AlphaDummy006, nb073AlphaDummy008 x y), (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 nb073AlphaDummy046)
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb073AlphaDummy015)))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb073AlphaDummy046)
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb073AlphaDummy047 x y))
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb073AlphaDummy017 x y))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb073AlphaDummy047 x y))
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
Checked nominal proof certificate identified upstream as nb073_split_alpha_0001.
Equations
- One or more equations did not get rendered due to their size.