(2steps total) PrintForm Definitions mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ring wf
  R:(Id), in,out:(|R|IdLnk). ring(R;in;out)  Prop
By: Auto THEN Unfold `ring` 0 THEN All (Unfold `rset`) THEN Analyze
THENL
[Analyze THENL [Auto THEN Analyze;Id];Auto;Auto]

Generated subgoal:

1 1. R : Id
2. in : {i:Id| R(i) }IdLnk
3. out : {i:Id| R(i) }IdLnk
4. i:{i:Id| R(i) }. 
4. R(source(in(i))) & R(destination(out(i)))
4. & source(out(i)) = i
4. & & destination(in(i)) = i
4. & & in(destination(out(i))) = out(i)
4. & & out(source(in(i))) = in(i)
  (i,j:{i:Id| R(i) }. k:. x.destination(out(x))^k(i) = j)  Type
1 step

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

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