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

  9. 1 < n

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

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: D 10 THENW Auto THEN InstLemma `successor` [E;T;L;Ach;Tor;v (n - 2);w]THENA Auto
Generated subgoals:

1. t0 (v (n - 2))

2. (v (n - 2)) < w

3. (Ach.d (v (n - 2))) < (Tor.d (v (n - 2)))

4. Def (v (n - 2))

5. 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))