(3steps total) PrintForm Definitions Lemmas mb event system 6 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: assert-ma-join-list-is-empty
  L:MsgA List. ma-is-empty((L))  reduce(M,x. ma-is-empty(M) & x;True;L)
By: Inst
Thm* L:MsgA List. ma-is-empty((L)) ~ reduce(M,x. ma-is-empty(M)x;true;L)
[]
THEN
ParallelLast
THEN
HypSubst -1 0
THEN
Thin -1
THEN
ListInd -1
THEN
Reduce 0

Generated subgoals:

1 1. MsgA List
  True  True
Auto
2 1. MsgA List
2. u : MsgA
3. v : MsgA List
4. reduce(M,x. ma-is-empty(M)x;true;v)
4. 
4. reduce(M,x. ma-is-empty(M) & x;True;v)
  (ma-is-empty(u)reduce(M,x. ma-is-empty(M)x;true;v))
  
  ma-is-empty(u) & reduce(M,x. ma-is-empty(M) & x;True;v)
1 step

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

(3steps total) PrintForm Definitions Lemmas mb event system 6 Sections EventSystems Search Doc