(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: rnext-one-one 1

1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i:|R|. 
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)
5. i,j:|R|. k:x.destination(out(x))^k(i) = j
6. |R|
7. i : |R|
8. j : |R|
9. destination(out(i)) = destination(out(j))
10. R(source(in(i)))
11. R(destination(out(i)))
12. source(out(i)) = i
13. destination(in(i)) = i
14. in(destination(out(i))) = out(i)
15. out(source(in(i))) = in(i)
16. R(source(in(j)))
17. R(destination(out(j)))
18. source(out(j)) = j
19. destination(in(j)) = j
20. in(destination(out(j))) = out(j)
21. out(source(in(j))) = in(j)
22. in(destination(out(i))) = in(destination(out(j)))
23. out(i) = out(j)
24. source(out(i)) = source(out(j))
25. i = j
  i = j


By: StrongHypSubst -1 0 THEN DVar `j' THEN Unfold `rset` 0 THEN Analyze
THEN
HypSubst -1 0


Generated subgoals:

None

About:
boolassertlambdaapplyfunctionequalandallexists
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