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

  7. Run(E;T;L;Tor)

  8. Ach Tor

  9. Ach.t1 Tor.t1

  10. IVP(Ach)

  11. TEP

  12. Ach || Tor

  13. t0 = t0

  14. 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

Conclusion:

False

Applied Tactic: D 14 THEN Auto THEN InstLemma `sequence` [E;T;L;Ach;Tor;t] THENA Auto
Generated subgoals:

1. t Tor.t1

2. (Ach.d s) < (Tor.d s)

3. False