(4steps 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-init wf 1 1 1

1. ds : x:Id fp-> Type
2. da : a:Knd fp-> Type
3. init : x:Id fp-> ds(x)?Void
4. a:Id fp-> State(ds)ma-valtype(da; locl(a))Prop
5. kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl))
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. x : Id
11. ds(x)?Top
12. x  dom(init)
13. x  dom(ds)
14. Top
  ds(x)?Void r Void


By: Unfold `fpf-cap` 0 THEN SplitOnConclITE


Generated subgoals:

None

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

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