(64steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: change-lemma 1 1 2 1

1. es : ES
2. x : Id
3. i : Id
4. T : Type
5. x,y:T. Dec(x = y)
6. vartype(i;xT
7. e' : E
8. e : E
9. e:E. loc(e) = i  (x when e T
10. e:E. loc(e) = i  (x after e T
11. e  e' 
12. loc(e') = i
13. (x after e') = (x when e)
14. (ev[ee'].(x after ev) = (x when ev))
  ev:E. e  ev  & ev  e'  & (x after ev) = (x when ev T


By: Unfold `l_exists` -1 THEN ParallelOp -1


Generated subgoals:

1 14. ev : {e:E| loc(e) = i  Id }
15. (ev  [ee']) & (x after ev) = (x when ev T
  e  ev  & ev  e'  & (x after ev) = (x when ev T

3 steps
2 14. ev : {e:E| loc(e) = i  Id }
15. (ev  [ee'])
16. (x after ev) = (x when ev T
17. e1 : E
18. e  e1  & e1  e' 
  (x after e1 T

3 steps
3 14. ev : {e:E| loc(e) = i  Id }
15. (ev  [ee'])
16. (x after ev) = (x when ev T
17. e1 : E
18. e  e1  & e1  e' 
  (x when e1 T

3 steps

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

(64steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc