-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
-cases m0
- [#mv #_ #Htg #_
-
-
-
-
-
-[ *
-
- 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.
+>append_cons <Hrs1 >reverse_append >reverse_single
+<Hrs2 >(append_cons … bar ll) >Hll1 >reverse_cons
+#sem_exec_move
+lapply
+ (sem_exec_move ? m ?
+ (([nchar]@reverse FSUnialpha sn)
+ @fn::reverse FSUnialpha (ll1@(fo::so)@[char])) lr0 … (refl ??) ????)
+ [ cut (tuple_TM (S n) (tuple_encoding n h t)) // >Htuple
+ * #qin * #cin * #qout * #cout * #mv * * * * #_ #Hmv #_ #_
+ normalize >(?: bar::qin@cin::qout@[cout;mv] = (bar::qin@cin::qout@[cout])@[mv])
+ [| normalize >associative_append normalize >associative_append % ]
+ >(?: bar::(state@[char])@(nstate@[nchar])@[m] = (bar::(state@[char])@(nstate@[nchar]))@[m])
+ [|normalize >associative_append >associative_append >associative_append >associative_append >associative_append % ]
+ #Heq lapply (append_l2_injective_r ?????? Heq) // #H destruct (H) //
+ | cases newconfig #qout * #cout * * * #_ #Hcout #_ #H destruct (H) -H
+ lapply (append_l2_injective_r ?????? e0) // #H destruct (H) @Hcout
+ |@Hbits_obj
+ |whd in ⊢ (??%?); >associative_append >associative_append
+ >associative_append %
+ |#Htb >Htb @(eq_vec … (niltape ?)) (* tape by tape *) #i #lei2
+ cases (le_to_or_lt_eq … (le_S_S_to_le …lei2))
+ [#lei1 cases (le_to_or_lt_eq … (le_S_S_to_le …lei1))
+ [#lei0 lapply(le_n_O_to_eq … (le_S_S_to_le …lei0)) #eqi <eqi
+ (* obj tape *)
+ >nth_change_vec [2:@leb_true_to_le %] %
+ |(* cfg tape *) #eqi >eqi
+ >nth_change_vec_neq [2:@eqb_false_to_not_eq %]
+ >nth_change_vec [2:@leb_true_to_le %]
+ whd in ⊢ (??%?); cut (∀A.∀l:list A.[]@l = l) [//] #Hnil >Hnil
+ >reverse_append >reverse_single >reverse_reverse %
+ (* idem *)
+ ]
+ |(* prg tape *) #eqi >eqi
+ >nth_change_vec_neq [2:@eqb_false_to_not_eq %]
+ >nth_change_vec_neq [2:@eqb_false_to_not_eq %]
+ >Hta_prg whd in ⊢ (??%?); @eq_f @(cons_injective_r ? bar bar)
+ >Htable >Hintable >reverse_append >reverse_cons
+ >reverse_reverse >reverse_cons >reverse_reverse
+ >associative_append >associative_append >associative_append
+ >(append_cons ? bar ll) >Hll1 @eq_f @eq_f <Hstate_exp @eq_f
+ >Hnewstate_exp >Hlr normalize >associative_append >associative_append %
+ ]
+ ]
+qed.