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. w : T

  7. Run(E;T;L;Ach) Run(E;T;L;Tor) Ach Tor IVP(Ach) Ach.d w = Tor.d w t0 < w (w Ach.t1 w Tor.t1) (s:T. t0 s s < w (Ach.d s) < (Tor.d s)) Def w

  8. n :

Conclusion:

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

Applied Tactic: NSubsetInd 8 THENW Auto
Generated subgoals:

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

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