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

  15. t0 < t

  16. t Ach.t1

  17. Ach.d t = Tor.d t

  18. s:T. t0 s s < t (Ach.d s) < (Tor.d s)

  19. Def t

  20. n: v:n T t0 = v 0 (i:(n - 1). (v i) < (v (i + 1))) (i:n. (v i) < t Def (v i) t0 (v i))

Conclusion:

False

Applied Tactic: Unfold `run` 6 THEN Auto THEN Unfold `tep` 19 THEN InstHyp [t] 19 THENA Auto THEN D 29 THEN With e (D 12) THENA Auto THEN D 30 THEN D 31 THEN With n + 1 (D 27) THENA Auto THEN D 32 THEN InstLemma `ax_choice` [T;E;t e.Def t I e t = time e ] THENA Auto THEN D 34 THEN InstLemma `phole_aux` [n;i.w (f (v i))] THENA Auto
Generated subgoals:

1. 1 n

2. f (v i) {f:E| f < e}

3. False