-definition o2c_states ≝ initN 3.
-
-definition copy0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
-definition copy1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
-definition copy2 : copy_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 3 (refl …)).
-
-
-definition trans_copy_step ≝
- λsrc,dst.λsig:FinSet.λn.
- λp:copy_states × (Vector (option sig) (S n)).
- let 〈q,a〉 ≝ p in
- match pi1 … q with
- [ O ⇒ match nth src ? a (None ?) with
- [ None ⇒ 〈copy2,null_action sig n〉
- | Some ai ⇒ match nth dst ? a (None ?) with
- [ None ⇒ 〈copy2,null_action ? n〉
- | Some aj ⇒
- 〈copy1,change_vec ? (S n)
- (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src)
- (〈Some ? ai,R〉) dst〉
- ]
- ]
- | S q ⇒ match q with
- [ O ⇒ (* 1 *) 〈copy1,null_action ? n〉
- | S _ ⇒ (* 2 *) 〈copy2,null_action ? n〉 ] ].
-
-definition copy_step ≝
- λsrc,dst,sig,n.
- mk_mTM sig n copy_states (trans_copy_step src dst sig n)
- copy0 (λq.q == copy1 ∨ q == copy2).
-
-definition R_comp_step_true ≝
- λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
- ∃x,y.
- current ? (nth src ? int (niltape ?)) = Some ? x ∧
- current ? (nth dst ? int (niltape ?)) = Some ? y ∧
- outt = change_vec ??
- (change_vec ?? int
- (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src)
- (tape_move_mono ? (nth dst ? int (niltape ?)) 〈Some ? x, R〉) dst.
-
-definition R_comp_step_false ≝
- λsrc,dst:nat.λsig,n.λint,outt: Vector (tape sig) (S n).
- (current ? (nth src ? int (niltape ?)) = None ? ∨
- current ? (nth dst ? int (niltape ?)) = None ?) ∧ outt = int.
-
-lemma copy_q0_q2_null :
- ∀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 ] ]
-qed.
-
-lemma copy_q0_q1 :
- ∀src,dst,sig,n,v,a,b.src ≠ dst → src < S n → dst < S n →
- nth src ? (current_chars ?? v) (None ?) = Some ? a →
- nth dst ? (current_chars ?? v) (None ?) = Some ? b →
- step sig n (copy_step src dst sig n) (mk_mconfig ??? copy0 v) =
- mk_mconfig ??? copy1
- (change_vec ? (S n)
- (change_vec ?? v
- (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src)
- (tape_move_mono ? (nth dst ? v (niltape ?)) 〈Some ? a, R〉) dst).
-#src #dst #sig #n #v #a #b #Heq #Hsrc #Hdst #Ha1 #Ha2
-whd in ⊢ (??%?); >(eq_pair_fst_snd … (trans ????)) whd in ⊢ (??%?); @eq_f2
-[ whd in match (trans ????);
- >Ha1 >Ha2 whd in ⊢ (??(???%)?); >(\b ?) //
-| whd in match (trans ????);
- >Ha1 >Ha2 whd in ⊢ (??(????(???%))?); >(\b ?) //
- change with (change_vec ?????) in ⊢ (??(????%)?);
- <(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
- <(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
- >tape_move_multi_def
- >pmap_change >pmap_change <tape_move_multi_def
- >tape_move_null_action
- @eq_f2 // >nth_change_vec_neq //
-]