Nominal proof certificates grouped in dependency order.
Certificates from NAR4C074C001Part010.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb074SplitAlpha0006
(x : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb074AlphaDummy119, nb074AlphaDummy120 x), (nb074AlphaDummy088, nb074AlphaDummy090 x), (nb074AlphaDummy087, nb074AlphaDummy089 x), (nb074AlphaDummy117, nb074AlphaDummy118 x), (nb074AlphaDummy091, nb074AlphaDummy092 x), (nb074AlphaDummy082, nb074AlphaDummy084 x), (nb074AlphaDummy081, nb074AlphaDummy083 x), (nb074AlphaDummy085, nb074AlphaDummy086 x), (nb074AlphaDummy042, nb074AlphaDummy044 x), (nb074AlphaDummy041, nb074AlphaDummy043 x), (nb074AlphaDummy001, nb074AlphaDummy002 x), (nb074AlphaDummy000, x), (nb074AlphaDummy003, nb074AlphaDummy004 x)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb074AlphaDummy119)
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb074AlphaDummy088)))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb074AlphaDummy119)
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb074AlphaDummy120 x))
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb074AlphaDummy090 x))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb074AlphaDummy120 x))
(Compiler.CompactSourceSyntax.synCcompl
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)
Checked nominal proof certificate identified upstream as nb074_split_alpha_0006.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C074C001Part011.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb074SplitAlpha0007
(x : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb074AlphaDummy129, nb074AlphaDummy130 x), (nb074AlphaDummy127, nb074AlphaDummy128 x), (nb074AlphaDummy082, nb074AlphaDummy084 x), (nb074AlphaDummy081, nb074AlphaDummy083 x), (nb074AlphaDummy085, nb074AlphaDummy086 x), (nb074AlphaDummy042, nb074AlphaDummy044 x), (nb074AlphaDummy041, nb074AlphaDummy043 x), (nb074AlphaDummy001, nb074AlphaDummy002 x), (nb074AlphaDummy000, x), (nb074AlphaDummy003, nb074AlphaDummy004 x)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv nb074AlphaDummy129)
(SemanticCore.Class.cab nb074AlphaDummy123
(Compiler.CompactSourceSyntax.synWrex nb074AlphaDummy124 (SemanticCore.Class.cv nb074AlphaDummy082)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb074AlphaDummy123)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb074AlphaDummy124)))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv nb074AlphaDummy129)
(SemanticCore.Class.cab nb074AlphaDummy123
(Compiler.CompactSourceSyntax.synWrex nb074AlphaDummy124 (SemanticCore.Class.cv nb074AlphaDummy082)
(SemanticCore.Wff.classEq (SemanticCore.Class.cv nb074AlphaDummy123)
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv nb074AlphaDummy124)))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb074AlphaDummy130 x))
(SemanticCore.Class.cab (nb074AlphaDummy125 x)
(Compiler.CompactSourceSyntax.synWrex (nb074AlphaDummy126 x) (SemanticCore.Class.cv (nb074AlphaDummy084 x))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb074AlphaDummy125 x))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb074AlphaDummy126 x))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb074AlphaDummy130 x))
(SemanticCore.Class.cab (nb074AlphaDummy125 x)
(Compiler.CompactSourceSyntax.synWrex (nb074AlphaDummy126 x) (SemanticCore.Class.cv (nb074AlphaDummy084 x))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb074AlphaDummy125 x))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb074AlphaDummy126 x))))))).neg)
Checked nominal proof certificate identified upstream as nb074_split_alpha_0007.
Equations
- One or more equations did not get rendered due to their size.