(42steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ring-list
  R:(Id), in,out:(|R|IdLnk).
  ring(R;in;out)  (L:|R| List. 0<||L|| & (i:|R|. (i  L)))
By: Auto THEN Unfold `ring` -1 THEN ExRepD THEN RenameVar `i' -1

Generated subgoal:

1 1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i:|R|. 
4. R(source(in(i))) & R(destination(out(i)))
4. & source(out(i)) = i
4. & & destination(in(i)) = i
4. & & in(destination(out(i))) = out(i)
4. & & out(source(in(i))) = in(i)
5. i,j:|R|. k:. x.destination(out(x))^k(i) = j  Id
6. |R|
  L:|R| List. 0<||L|| & (i:|R|. (i  L))
41 steps

About:
listboolnatural_numberless_thanfunctionimpliesandallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(42steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc