-definition rb_tapes ≝ λQ,sig,n,ls.λa:MTA Q sig (S n).λrs.
- vec_map ?? (to_sig_tape ??) n (readback ? (S n) ls (vec … a) rs n).
-
+let rec rb_tapes Q sig n ls (a:MTA Q sig (S n)) rs i on i ≝
+ match i with
+ [ O ⇒ mk_Vector ? 0 (nil ?) (refl ??)
+ | S j ⇒ vec_cons_right ? (to_sig_tape ?? (rb_trace_i ? (S n) ls (vec … a) rs j)) j
+ (rb_tapes Q sig n ls a rs j)].
+
+lemma nth_rb_tapes : ∀Q,sig,n,ls.∀a:MTA Q sig (S n).∀rs,j,i. i < j →
+ nth i ? (rb_tapes Q sig n ls (a:MTA Q sig (S n)) rs j) (niltape ?) =
+ to_sig_tape ?? (rb_trace_i ? (S n) ls (vec … a) rs i).
+#Q #sig #n #ls #a #rs #j elim j
+ [#i #H @False_ind /2/
+ |#k #Hind #i #lti cases (le_to_or_lt_eq … (le_S_S_to_le … lti))
+ [#Hlt >nth_cons_right_lt [@Hind //|//]
+ |#Heq >Heq @nth_cons_right_n
+ ]
+ ]
+qed.
+
+