1. E :

2. T :

3. L :

4. Ach : Signature(E;T;L)

5. Tor : Signature(E;T;L)

6. u : T

7. w : T

8. Run(E;T;L;Ach)

9. Order(E;e,f.e < f)

10. IrLinorder(T;t,u.t < u)

11. IrLinorder(L;x,y.x < y)

12. t0 < Tor.t1

13. r,u:T. t0 r r < u u Tor.t1 (Tor.d r) < (Tor.d u)

14. e,f:E. I e I f (e < f (time e) < (time f))

15. e:E. n:. w:{f:E| f < e} n. Inj({f:E| f < e} ;n;w)

16. Def t0

17. r:T. t0 r r Tor.t1 Def r Def (Tor.d r)

18. < = <

19. < = <

20. < = <

21. I = I

22. time = time

23. Def = Def

24. Def = Def

25. t0 = t0

26. Tor.t1 < Ach.t1 (t:T (t0 < t t Ach.t1 Ach.d t = Tor.d t (s:T. t0 s s < t (Ach.d s) < (Tor.d s))) Def t)

27. IVP(Ach)

28. Ach.d w = Tor.d w

29. t0 u

30. u < w

31. w Ach.t1

32. w Tor.t1

33. (Ach.d u) < (Tor.d u)

34. Def u

35. Def w

t0 u

None