PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: es-valtype-w-valtype
  i:Id, w:World, p:FairFifo, t:.
  isnull(a(i;t))  (valtype(<i,t>) ~ valtype(i;a(i;t)))
By: UnivCD
THEN
Repeat
(Unfolds
([`es-kind`
(;`es-lnk`
(;`es-tag`
(;`es-act`
(;`es-loc`
(;`es-valtype`
(;`es-isrcv`
(;`es-rcvtype`
(;`es-acttype`
(;`w-es`
(;`w-valtype`
(;`kindcase`
(;`w-ekind`
(;`w-act`
(;`w-V`
(;`w-TA`]
(0
(THEN
(Reduce 0)
THEN
SplitOnConclITE
THEN
SplitOnConclITE
THEN
Try Trivial
THEN
Try
(RWO Thm* k:Knd. islocal(k) ~ isrcv(k) -1 THEN RW assert_pushdownC -1
(THEN
(Complete Auto)

Generated subgoals:

None

About:
pairassertsqequalimpliesall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Search Doc