- ∀src,dst,sig,n,is_sep,v,t.src < S n → dst < S n →
- current ? t = None ? →
- step sig n (copy_step src dst sig n is_sep)
- (mk_mconfig ??? copy0 (change_vec ? (S n) v t src)) =
- mk_mconfig ??? copy2 (change_vec ? (S n) v t src).
-#src #dst #sig #n #is_sep #v #t #Hsrc #Hdst #Hcurrent
-whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
-[ >current_chars_change_vec // whd in match (trans ????);
- >nth_change_vec // >Hcurrent %
-| >current_chars_change_vec // whd in match (trans ????);
- >nth_change_vec // >Hcurrent @tape_move_null_action
-]
-qed.
-
-lemma copy_q0_q2_sep :
- ∀src,dst,sig,n,is_sep,v,t.src < S n → dst < S n →
- ∀s.current ? t = Some ? s → is_sep s = true →
- step sig n (copy_step src dst sig n is_sep)
- (mk_mconfig ??? copy0 (change_vec ? (S n) v t src)) =
- mk_mconfig ??? copy2 (change_vec ? (S n) v t src).
-#src #dst #sig #n #is_sep #v #t #Hsrc #Hdst #s #Hcurrent #Hsep
-whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
-[ >current_chars_change_vec // whd in match (trans ????);
- >nth_change_vec // >Hcurrent whd in ⊢ (??(???%)?); >Hsep %
-| >current_chars_change_vec // whd in match (trans ????);
- >nth_change_vec // >Hcurrent whd in ⊢ (??(???????(???%))?);
- >Hsep @tape_move_null_action
-]
-qed.
-
-lemma change_vec_commute : ∀A,n,v,a,b,i,j. i ≠ j →
- change_vec A n (change_vec A n v a i) b j
- = change_vec A n (change_vec A n v b j) a i.
-#A #n #v #a #b #i #j #Hij @(eq_vec … a)
-#k #Hk cases (decidable_eq_nat k i) #Hki
-[ >Hki >nth_change_vec // >(nth_change_vec_neq ??????? (sym_not_eq … Hij))
- >nth_change_vec //
-| cases (decidable_eq_nat k j) #Hkj
- [ >Hkj >nth_change_vec // >(nth_change_vec_neq ??????? Hij) >nth_change_vec //
- | >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
- >(nth_change_vec_neq ??????? (sym_not_eq … Hkj))
- >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
- >(nth_change_vec_neq ??????? (sym_not_eq … Hkj)) //
- ]
-]
+ ∀src,dst,sig,n,v.src < S n → dst < S n →
+ (nth src ? (current_chars ?? v) (None ?) = None ? ∨
+ nth dst ? (current_chars ?? v) (None ?) = None ?) →
+ step sig n (copy_step src dst sig n) (mk_mconfig ??? copy0 v)
+ = mk_mconfig ??? copy2 v.
+#src #dst #sig #n #v #Hi #Hj
+whd in ⊢ (? → ??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (?→??%?);
+* #Hcurrent
+[ @eq_f2
+ [ whd in ⊢ (??(???%)?); >Hcurrent %
+ | whd in ⊢ (??(????(???%))?); >Hcurrent @tape_move_null_action ]
+| @eq_f2
+ [ whd in ⊢ (??(???%)?); >Hcurrent cases (nth src ?? (None sig)) //
+ | whd in ⊢ (??(????(???%))?); >Hcurrent
+ cases (nth src ?? (None sig)) [|#x] @tape_move_null_action ] ]