Nominal proof certificates grouped in dependency order.
Certificates from NAR4C090C001Part113.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090SplitAlpha0090
(v u : SemanticCore.Var)
(A : SemanticCore.Class)
(h : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb090AlphaDummy705 A, nb090AlphaDummy706 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 (nb090AlphaDummy705 A))
(SemanticCore.Class.cab (nb090AlphaDummy699 A)
(Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A)
(Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A))
(SemanticCore.Class.cv (nb090AlphaDummy041 A)))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy705 A))
(SemanticCore.Class.cab (nb090AlphaDummy699 A)
(Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy700 A)
(Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv (nb090AlphaDummy000 A))
(SemanticCore.Class.cv (nb090AlphaDummy041 A)))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy699 A))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy700 A))))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy706 v u h))
(SemanticCore.Class.cab (nb090AlphaDummy701 v u h)
(Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h)
(Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h)
(SemanticCore.Class.cv (nb090AlphaDummy043 v u h)))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy706 v u h))
(SemanticCore.Class.cab (nb090AlphaDummy701 v u h)
(Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy702 v u h)
(Compiler.CompactSourceSyntax.synCfv (SemanticCore.Class.cv h)
(SemanticCore.Class.cv (nb090AlphaDummy043 v u h)))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy701 v u h))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy702 v u h))))))).neg)
Checked nominal proof certificate identified upstream as nb090_split_alpha_0090.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C090C001Part114.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb090SplitAlpha0091
(v u : SemanticCore.Var)
(A : SemanticCore.Class)
(h : SemanticCore.Var)
:
Nominal.TAlphaWff
[(nb090AlphaDummy791 A, nb090AlphaDummy792 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 (nb090AlphaDummy791 A))
(SemanticCore.Class.cab (nb090AlphaDummy785 A)
(Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy791 A))
(SemanticCore.Class.cab (nb090AlphaDummy785 A)
(Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy786 A) (SemanticCore.Class.cv (nb090AlphaDummy042 A))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy785 A))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy786 A))))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy792 v u h))
(SemanticCore.Class.cab (nb090AlphaDummy787 v u h)
(Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h)
(SemanticCore.Class.cv (nb090AlphaDummy044 v u h))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb090AlphaDummy792 v u h))
(SemanticCore.Class.cab (nb090AlphaDummy787 v u h)
(Compiler.CompactSourceSyntax.synWrex (nb090AlphaDummy788 v u h)
(SemanticCore.Class.cv (nb090AlphaDummy044 v u h))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb090AlphaDummy787 v u h))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb090AlphaDummy788 v u h))))))).neg)
Checked nominal proof certificate identified upstream as nb090_split_alpha_0091.
Equations
- One or more equations did not get rendered due to their size.