NF weak partition development: NAR4H5C095M3Part011.
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0006
(x u : SemanticCore.Var)
(D R S_cls : SemanticCore.Class)
(f : SemanticCore.Var)
(E : SemanticCore.Class)
:
Nominal.TAlphaWff
[(nb095AlphaDummy139 D R S_cls E, nb095AlphaDummy140 f), (nb095AlphaDummy137 D R S_cls E, nb095AlphaDummy138 f), (nb095AlphaDummy092 D R S_cls E, nb095AlphaDummy094 f), (nb095AlphaDummy091 D R S_cls E, nb095AlphaDummy093 f), (nb095AlphaDummy095 D R S_cls E, nb095AlphaDummy096 f), (nb095AlphaDummy013 D R S_cls E, nb095AlphaDummy016 f), (nb095AlphaDummy012 D R S_cls E, nb095AlphaDummy015 f), (nb095AlphaDummy011 D R S_cls E, nb095AlphaDummy014 f), (nb095AlphaDummy017 D R S_cls E, nb095AlphaDummy018 f), (nb095AlphaDummy009 D R S_cls E, nb095AlphaDummy010 f), (nb095AlphaDummy007 D R S_cls E, nb095AlphaDummy008 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy139 D R S_cls E))
(SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E)
(Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E)
(SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy139 D R S_cls E))
(SemanticCore.Class.cab (nb095AlphaDummy133 D R S_cls E)
(Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy134 D R S_cls E)
(SemanticCore.Class.cv (nb095AlphaDummy092 D R S_cls E))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy133 D R S_cls E))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E))))))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy140 f))
(SemanticCore.Class.cab (nb095AlphaDummy135 f)
(Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))))))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy140 f))
(SemanticCore.Class.cab (nb095AlphaDummy135 f)
(Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy136 f) (SemanticCore.Class.cv (nb095AlphaDummy094 f))
(SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy135 f))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f))))))).neg)
Checked nominal proof certificate identified upstream as nb095_split_alpha_0006.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0007
(x u : SemanticCore.Var)
(D R S_cls : SemanticCore.Class)
(f : SemanticCore.Var)
(E : SemanticCore.Class)
:
Nominal.TAlphaWff
[(nb095AlphaDummy167 D R S_cls E, nb095AlphaDummy168 f), (nb095AlphaDummy165 D R S_cls E, nb095AlphaDummy166 f), (nb095AlphaDummy134 D R S_cls E, nb095AlphaDummy136 f), (nb095AlphaDummy133 D R S_cls E, nb095AlphaDummy135 f), (nb095AlphaDummy163 D R S_cls E, nb095AlphaDummy164 f), (nb095AlphaDummy137 D R S_cls E, nb095AlphaDummy138 f), (nb095AlphaDummy092 D R S_cls E, nb095AlphaDummy094 f), (nb095AlphaDummy091 D R S_cls E, nb095AlphaDummy093 f), (nb095AlphaDummy095 D R S_cls E, nb095AlphaDummy096 f), (nb095AlphaDummy013 D R S_cls E, nb095AlphaDummy016 f), (nb095AlphaDummy012 D R S_cls E, nb095AlphaDummy015 f), (nb095AlphaDummy011 D R S_cls E, nb095AlphaDummy014 f), (nb095AlphaDummy017 D R S_cls E, nb095AlphaDummy018 f), (nb095AlphaDummy009 D R S_cls E, nb095AlphaDummy010 f), (nb095AlphaDummy007 D R S_cls E, nb095AlphaDummy008 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)]
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy167 D R S_cls E))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E)))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy167 D R S_cls E))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy134 D R S_cls E)))).neg)
((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy168 f))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f)))).imp
(SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy168 f))
(Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy136 f)))).neg)
Checked nominal proof certificate identified upstream as nb095_split_alpha_0007.
Equations
- One or more equations did not get rendered due to their size.