(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
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))
  i:|R|. 
  e@i.kind(e) = rcv((in(i)); "vote")
  & (valtype(e) r ) & val(e) = uid(ldr)  
By: Assert
(d:, i:|R|.
(d(ldr;i) = d
(
(e@i.kind(e) = rcv((in(i)); "vote") & (valtype(e) r ) & val(e) = uid(ldr))

Generated subgoals:

1   d:, i:|R|.
  d(ldr;i) = d
  
  e@i.kind(e) = rcv((in(i)); "vote")
  & (valtype(e) r ) & val(e) = uid(ldr)  
43 steps
2 19. d:, i:|R|.
19. d(ldr;i) = d
19. 
19. e@i.kind(e) = rcv((in(i)); "vote")
19. & (valtype(e) r ) & val(e) = uid(ldr)  
  i:|R|. 
  e@i.kind(e) = rcv((in(i)); "vote")
  & (valtype(e) r ) & val(e) = uid(ldr)  
1 step

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