(145steps 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 realizes 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. (loc.(ring-leader1(loc;R;uid;out;in)))  Dsys
8. D' : Dsys
9. loc.(ring-leader1(loc;R;uid;out;in))  D'
10. w : World
11. p : FairFifo
12. PossibleWorld(D';w)
13. L : |R| List
14. 0<||L||
15. i:|R|. (i  L)
16. ldr : |R|
17. (ldr  L)
18. (xL.uid(x)uid(ldr))
  e@ldr.kind(e) = locl("leader")
  & (i:|R|. e@i.kind(e) = locl("leader")  i = ldr  |R|)
By: Assert
(i:|R|. 
(e@i.kind(e) = rcv((in(i)); "vote") & (valtype(e) r ) & val(e) = uid(ldr))

Generated subgoals:

1   i:|R|. 
  e@i.kind(e) = rcv((in(i)); "vote")
  & (valtype(e) r ) & val(e) = uid(ldr)  
45 steps
2 19. i:|R|. 
19. e@i.kind(e) = rcv((in(i)); "vote")
19. & (valtype(e) r ) & val(e) = uid(ldr)  
  e@ldr.kind(e) = locl("leader")
  & (i:|R|. e@i.kind(e) = locl("leader")  i = ldr  |R|)
97 steps

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

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