Nominal proof certificates grouped in dependency order.
Certificates from NAR4C077C001Part012.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0002
(x : SemanticCore.Var)
(F I : SemanticCore.Class)
:
Nominal.TAlphaWff
[(nb077AlphaDummy073 F I, nb077AlphaDummy074 x), (nb077AlphaDummy071 F I, nb077AlphaDummy072 x), (nb077AlphaDummy060 F I, nb077AlphaDummy063 x), (nb077AlphaDummy059 F I, nb077AlphaDummy062 x), (nb077AlphaDummy065 F I, nb077AlphaDummy066 x), (nb077AlphaDummy057 F I, nb077AlphaDummy058 x F), (nb077AlphaDummy055 F I, nb077AlphaDummy056 x F), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy013 F I, nb077AlphaDummy014 x F I), (nb077AlphaDummy011 F I, nb077AlphaDummy012 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy073 F I))
(SemanticCore.Class.cab (nb077AlphaDummy067 F I)
(Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy068 F I)
(SemanticCore.Class.cv (nb077AlphaDummy059 F I))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy067 F I))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy073 F I))
(SemanticCore.Class.cab (nb077AlphaDummy067 F I)
(Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy068 F I)
(SemanticCore.Class.cv (nb077AlphaDummy059 F I))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy067 F I))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I))))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy074 x))
(SemanticCore.Class.cab (nb077AlphaDummy069 x)
(Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy070 x) (SemanticCore.Class.cv (nb077AlphaDummy062 x))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy069 x))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy074 x))
(SemanticCore.Class.cab (nb077AlphaDummy069 x)
(Compiler.CompactSourceSyntax.synWrex (nb077AlphaDummy070 x) (SemanticCore.Class.cv (nb077AlphaDummy062 x))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb077AlphaDummy069 x))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x))))))).neg)
Checked nominal proof certificate identified upstream as nb077_split_alpha_0002.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C077C001Part013.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb077SplitAlpha0003
(x : SemanticCore.Var)
(F I : SemanticCore.Class)
:
Nominal.TAlphaWff
[(nb077AlphaDummy101 F I, nb077AlphaDummy102 x), (nb077AlphaDummy099 F I, nb077AlphaDummy100 x), (nb077AlphaDummy068 F I, nb077AlphaDummy070 x), (nb077AlphaDummy067 F I, nb077AlphaDummy069 x), (nb077AlphaDummy097 F I, nb077AlphaDummy098 x), (nb077AlphaDummy071 F I, nb077AlphaDummy072 x), (nb077AlphaDummy060 F I, nb077AlphaDummy063 x), (nb077AlphaDummy059 F I, nb077AlphaDummy062 x), (nb077AlphaDummy065 F I, nb077AlphaDummy066 x), (nb077AlphaDummy057 F I, nb077AlphaDummy058 x F), (nb077AlphaDummy055 F I, nb077AlphaDummy056 x F), (nb077AlphaDummy016 F I, nb077AlphaDummy018 x F I), (nb077AlphaDummy015 F I, nb077AlphaDummy017 x F I), (nb077AlphaDummy013 F I, nb077AlphaDummy014 x F I), (nb077AlphaDummy011 F I, nb077AlphaDummy012 x F I), (nb077AlphaDummy001 F I, nb077AlphaDummy002 x F I), (nb077AlphaDummy004 F I, nb077AlphaDummy006 x F I), (nb077AlphaDummy003 F I, nb077AlphaDummy005 x F I)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy101 F I))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I)))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy101 F I))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy068 F I)))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy102 x))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x)))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb077AlphaDummy102 x))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb077AlphaDummy070 x)))).neg)
Checked nominal proof certificate identified upstream as nb077_split_alpha_0003.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Certificates from NAR4C077C001Part014.