Nuprl - Proof: ring-leader1 feasible 1

(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

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)

d-feasible(

loc.

(ring-leader1(loc;R;uid;out;in)))

By:	Assert (i:Id. R(i) (i L))

Generated subgoals:

1   i:Id. R(i)  (i  L)
1 step

2 10. i:Id. R(i)  (i  L)
  d-feasible(loc.(ring-leader1(loc;R;uid;out;in)))
10 steps

About:

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