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

Def (Tor.d u)

Applied Tactic: Unfold `race` 10 THEN D 10 THEN Unfold `concurrent` 10 THEN Auto THEN RWH (HypC 16) 0 THENA Auto THE N Thin 18 THEN Thin 18 THEN Unfold `run` 9 THEN Auto THEN BackThruHyp 17 THENW Auto THEN RWH (RevHyp C 25) 0 THENA Auto THEN Unfold `sign_t_ref_rel` 0 THEN Reduce 0 THEN RWH (RevHypC 19) 0 THENA Auto T HEN Auto
Generated subgoals:

1. t0 < u t0 = u

2. u < Tor.t1 u = Tor.t1

3. Def u