Level: Lib Thy Top: 3
Hypotheses:

  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. Run(E;T;L;Tor)

  10. Ach Tor

  11. b,e:T. a:L. t0 b b < e e Ach.t1 (Ach.d b) < a a < (Ach.d e) Def b Def a Def e (t:T. b < t t < e Ach.d t = a Def t)

  12. Ach.d w = Tor.d w

  13. t0 u

  14. u < w

  15. w Ach.t1

  16. w Tor.t1

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

  18. Def u

  19. Def w

  20. t:T. u < t t < w Ach.d t = Tor.d u Def t

Conclusion:

v:T. u < v v < w Def v

Applied Tactic: D 20 THENW Auto THEN With t (D 0) THEN Auto
Generated subgoals:

None