Level: Lib Thy Top: 1
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

Conclusion:

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

Applied Tactic: RWH (HypC 12) 0 THENA Auto THEN Fold `ivp` 11 THEN Unfold `race` 10 THEN D 10 THENW Auto THEN Unfold `concurrent` 10 THEN Auto THEN RWH (HypC 12) 0 THENA Auto THEN Unfold `run` 9 THEN Auto THEN BackTh ruHyp 13 THEN Auto
Generated subgoals:

1. t0 u

2. u < w

3. w Tor.t1