(13steps 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-leader1 feasible 1 2 1 1 1
1. R : Id
2. uid : |R|
3. out : |R|IdLnk
4. in : |R|IdLnk
5. ring(R;in;out)
6. Inj(|R|; ; uid)
7. L : |R| List
8. 0<||L||
9. i:|R|. (i  L)
10. i:Id. R(i)  (i  L)
11. i : Id
12. R(i)
  (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(1of(
  (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(ltg))  L)
  (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).
  interface-check(loc.
  (ring-leader1(loc;R;uid;out;in));1of(ltg);1of(2of(ltg));2of(2of(ltg))))
By: Assert (destination(in(i)) = i)

Generated subgoals:

1   destination(in(i)) = i
1 step
2 13. destination(in(i)) = i
  (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(1of(
  (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).(destination(ltg))  L)
  (ltgma-outlinks((ring-leader1(i;R;uid;out;in));i).
  interface-check(loc.
  (ring-leader1(loc;R;uid;out;in));1of(ltg);1of(2of(ltg));2of(2of(ltg))))
1 step

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

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