(7steps total) PrintForm Definitions mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-send wf
  M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(tg:Id
  M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if source(l) = i
  M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if M.da(rcv(l; tg))
  M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(else Top fi) List.
  M.send(k;l;s;v;ms;i)  Prop
By: Auto THEN Unfold `ma-send` 0 THEN Unfold_MsgA -7 THEN Unfold `fpf-val` 0
THEN
Analyze

Generated subgoals:

1 1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. x:Id fp-> ds(x)?Void
4. a:Id fp-> State(ds)da(locl(a))?TopProp
5. kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send : 
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. x:Id fp-> Knd List
8. ltg:IdLnkId fp-> Knd List
9. Top
10. k : Knd
11. l : IdLnk
12. State(ds)
13. ma-valtype(da; k)
14. i : Id
15. (tg:Idif source(l) = i da(rcv(l; tg))?Top else Top fi) List
  <k,l>  dom(send)  Prop
1 step
2 1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. x:Id fp-> ds(x)?Void
4. a:Id fp-> State(ds)da(locl(a))?TopProp
5. kx:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send : 
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. x:Id fp-> Knd List
8. ltg:IdLnkId fp-> Knd List
9. Top
10. k : Knd
11. l : IdLnk
12. s : State(ds)
13. v : ma-valtype(da; k)
14. i : Id
15. ms : (tg:Idif source(l) = i da(rcv(l; tg))?Top else Top fi) List
16. <k,l>  dom(send)
  (ms
  (=
  (if source(l) = i
  (if concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)(s,v));send(<k,l>)))
  (else nil fi
  ( (tg:Idif source(l) = i da(rcv(l; tg))?Top else Top fi) List)
   Prop
5 steps

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

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