Nominal proof certificates grouped in dependency order.
Certificates from NAR4C090C001Part115.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090SplitAlpha0092
(v u : SemanticCore.Var)
(A : SemanticCore.Class)
(h : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb090AlphaDummy819 A, nb090AlphaDummy820 v u h), (nb090AlphaDummy817 A, nb090AlphaDummy818 v u h), (nb090AlphaDummy786 A, nb090AlphaDummy788 v u h), (nb090AlphaDummy785 A, nb090AlphaDummy787 v u h), (nb090AlphaDummy815 A, nb090AlphaDummy816 v u h), (nb090AlphaDummy789 A, nb090AlphaDummy790 v u h), (nb090AlphaDummy777 A, nb090AlphaDummy778 v u h), (nb090AlphaDummy779 A, nb090AlphaDummy780 v u h), (nb090AlphaDummy782 A, nb090AlphaDummy784 v u h), (nb090AlphaDummy781 A, nb090AlphaDummy783 v u h), (nb090AlphaDummy700 A, nb090AlphaDummy702 v u h), (nb090AlphaDummy699 A, nb090AlphaDummy701 v u h), (nb090AlphaDummy775 A, nb090AlphaDummy776 v u h), (nb090AlphaDummy703 A, nb090AlphaDummy704 v u h), (nb090AlphaDummy042 A, nb090AlphaDummy044 v u h), (nb090AlphaDummy041 A, nb090AlphaDummy043 v u h), (nb090AlphaDummy000 A, h), (nb090AlphaDummy002 A, v), (nb090AlphaDummy001 A, u), (nb090AlphaDummy003 A, nb090AlphaDummy004 v u A h)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy819 A))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A)))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy819 A))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A)))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy820 v u h))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h)))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy820 v u h))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h)))).neg)
Checked nominal proof certificate identified upstream as nb090_split_alpha_0092.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C090C001Part116.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090SplitAlpha0093
(v u : SemanticCore.Var)
(A : SemanticCore.Class)
(h : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb090AlphaDummy700 A, nb090AlphaDummy702 v u h), (nb090AlphaDummy699 A, nb090AlphaDummy701 v u h), (nb090AlphaDummy775 A, nb090AlphaDummy776 v u h), (nb090AlphaDummy703 A, nb090AlphaDummy704 v u h), (nb090AlphaDummy042 A, nb090AlphaDummy044 v u h), (nb090AlphaDummy041 A, nb090AlphaDummy043 v u h), (nb090AlphaDummy000 A, h), (nb090AlphaDummy002 A, v), (nb090AlphaDummy001 A, u), (nb090AlphaDummy003 A, nb090AlphaDummy004 v u A h)]
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h))
(Compiler.CompactSourceSyntax.synCun
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h)))
(Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c)))
Checked nominal proof certificate identified upstream as nb090_split_alpha_0093.
Equations
- One or more equations did not get rendered due to their size.