+
+lemma lt_obj : obj < 3. // qed.
+lemma lt_cfg : cfg < 3. // qed.
+lemma lt_prg : prg < 3. // qed.
+
+definition R_copy_strict ≝
+ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+ ((current ? (nth src ? int (niltape ?)) = None ? ∨
+ current ? (nth dst ? int (niltape ?)) = None ?) → outt = int) ∧
+ (∀ls,x,x0,rs,ls0,rs0.
+ nth src ? int (niltape ?) = midtape sig ls x rs →
+ nth dst ? int (niltape ?) = midtape sig ls0 x0 rs0 →
+ |rs0| ≤ |rs| →
+ (∃rs1,rs2.rs = rs1@rs2 ∧ |rs1| = |rs0| ∧
+ outt = change_vec ??
+ (change_vec ?? int
+ (mk_tape sig (reverse sig rs1@x::ls) (option_hd sig rs2)
+ (tail sig rs2)) src)
+ (mk_tape sig (reverse sig rs1@x::ls0) (None sig) []) dst)).
+
+axiom sem_copy_strict : ∀src,dst,sig,n. src ≠ dst → src < S n → dst < S n →
+ copy src dst sig n ⊨ R_copy_strict src dst sig n.
+
+lemma sem_unistep : ∀n,l,h.unistep ⊨ R_unistep n l h.
+#n #l #h
+@(sem_seq_app ??????? (sem_match_m cfg prg FSUnialpha 2 ???)
+ (sem_seq ?????? (sem_restart_tape ???)
+ (sem_seq ?????? (sem_move_multi ? 2 cfg R ?)
+ (sem_seq ?????? (sem_copy_strict prg cfg FSUnialpha 2 ???)
+ (sem_seq ?????? sem_cfg_to_obj
+ (sem_seq ?????? sem_tape_move_obj
+ (sem_seq ?????? (sem_restart_tape ???) sem_obj_to_cfg)))))))
+ /2 by le_n,sym_not_eq/
+#ta #tb #HR #state #char #table #Hta_cfg #Hcfg #Hta_prg #Htable
+#Hbits_obj #Htotaltable
+#nstate #nchar #m #t #Htuple #Hmatch
+cases HR -HR #tc * whd in ⊢ (%→?);
+>Hta_cfg #H cases (H ?? (refl ??)) -H
+(* prg starts with a bar, so it's not empty *) #_
+>Hta_prg #H lapply (H ??? (refl ??)) -H *
+[| cases Htotaltable #ll * #lr #H >H
+ #Hfalse @False_ind cases (Hfalse ll lr) #H1 @H1 //]
+* #ll * #lr * #Hintable -Htotaltable #Htc
+* #td * whd in ⊢ (%→?); >Htc
+>nth_change_vec_neq [|@sym_not_eq //] >(nth_change_vec ?????? lt_cfg)
+#Htd lapply (Htd ? (refl ??)) -Htd
+>change_vec_commute [|@sym_not_eq //] >change_vec_change_vec
+>(?: list_of_tape ? (mk_tape ? (reverse ? (state@[char])@[bar]) (None ?) [ ]) =
+ bar::state@[char])
+[|whd in ⊢ (??%?); >left_mk_tape >reverse_append >reverse_reverse
+ >current_mk_tape >right_mk_tape normalize >append_nil % ]
+whd in ⊢ (???(???(????%?)??)→?); whd in match (tail ??); #Htd
+(* move cfg to R *)
+* #te * whd in ⊢ (%→?); >Htd
+>change_vec_commute [|@sym_not_eq //] >change_vec_change_vec
+>nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
+>Htable in Hintable; #Hintable #Hte
+(* copy *)
+cases (cfg_in_table_to_tuple ???? Hcfg ?? Hintable)
+#newstate * #m0 * #lr0 * * #Hlr destruct (Hlr) #Hnewcfg #Hm0
+cut (∃fo,so,co.state = fo::so@[co] ∧ |so| = n)
+[ @daemon ] * #fo * #so * #co * #Hstate_exp #Hsolen
+cut (∃fn,sn,cn.newstate = fn::sn@[cn] ∧ |sn| = n)
+[ @daemon ] * #fn * #sn * #cn * #Hnewstate_exp #Hsnlen
+* #tf * * #_ >Hte >(nth_change_vec ?????? lt_prg)
+>nth_change_vec_neq [|@sym_not_eq //] >(nth_change_vec ?????? lt_cfg)
+>Hstate_exp >Hnewstate_exp
+whd in match (mk_tape ????); whd in match (tape_move ???);
+#Htf cases (Htf ?????? (refl ??) (refl ??) ?)
+[| whd in match (tail ??); >length_append >length_append
+ >Hsolen >length_append >length_append >Hsnlen
+ <plus_n_Sm <plus_n_Sm <plus_n_Sm <plus_n_O <plus_n_O normalize // ]
+#rs1 * #rs2 whd in match (tail ??); * *
+>append_cons #Hrs1rs2 #Hrs1len
+>change_vec_change_vec >change_vec_commute [|@sym_not_eq //]
+>change_vec_change_vec #Htf
+(* cfg to obj *)
+* #tg * whd in ⊢ (%→?); >Htf
+>nth_change_vec_neq [|@sym_not_eq //]
+>(nth_change_vec ?????? lt_cfg)
+lapply (append_l1_injective ?????? Hrs1rs2)
+[ >Hsnlen >Hrs1len >length_append >length_append >length_append >length_append
+ normalize >Hsolen >Hsnlen % ]
+#Hrs1 <Hrs1 >reverse_append #Htg cases (Htg ?? (refl ??)) -Htg #Htg1 #Htg2
+
+
+
+
+
+[ *
+
+ match_m cfg prg FSUnialpha 2 ·
+ restart_tape cfg · copy prg cfg FSUnialpha 2 ·
+ cfg_to_obj · tape_move_obj · restart_tape prg · obj_to_cfg.