-@(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
- (sem_seq ??????
- (sem_if ??????????
- (sem_test_null_multi ?? obj ?)
- (sem_seq ?????? (sem_copy_char …)
- (sem_seq ?????? (sem_move_multi ? 2 cfg L ?)
- (sem_move_multi ? 2 obj L ?)))
- (sem_inject ???? cfg ? (sem_write FSUnialpha null)))
- (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?))
- (sem_move_multi ? 2 cfg R ?)))) //
-#ta #tb *
-#tc * whd in ⊢ (%→?); #Htc *
-#td * *
-[ * #te * * #Hcurtc #Hte
- * destruct (Hte) #te * whd in ⊢ (%→?); #Hte
- cut (∃x.current ? (nth obj ? tc (niltape ?)) = Some ? x)
- [ cases (current ? (nth obj ? tc (niltape ?))) in Hcurtc;
- [ * #H @False_ind /2/ | #x #_ %{x} % ] ] * #x #Hcurtc'
-(* [ whd in ⊢ (%→%→?); * #x * #y * * -Hcurtc #Hcurtc1 #Hcurtc2 #Hte *)
- * #tf * whd in ⊢ (%→%→?); #Htf #Htd
- * #tg * * * whd in ⊢ (%→%→%→%→?); #Htg1 #Htg2 #Htg3 #Htb
- #c #ls #Hta1 %
- [ #lso #x0 #rso #Hta2 >Hta1 in Htc; >eq_mk_tape_rightof
- whd in match (tape_move ???); #Htc
- cut (tg = change_vec ?? td (mk_tape ? [ ] (None ?) (reverse ? ls@[x])) cfg)
- [ lapply (eq_vec_change_vec ??????? (Htg2 ls x [ ] ?) Htg3) //
- >Htd >nth_change_vec_neq // >Htf >nth_change_vec //
- >Hte >Hcurtc' >nth_change_vec // >Htc >nth_change_vec // ]
- -Htg1 -Htg2 -Htg3 #Htg destruct
- >change_vec_change_vec >change_vec_change_vec
- >change_vec_commute // >change_vec_change_vec
- >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec
- >change_vec_commute // >change_vec_change_vec
- >nth_change_vec // >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec // >nth_change_vec_neq [|@sym_not_eq //]
- >change_vec_commute [|@sym_not_eq //] @eq_f3 //
- [ >Hta2 cases rso in Hta2; whd in match (tape_move_mono ???);
- [ #Hta2 whd in match (tape_move ???); <Hta2 @change_vec_same
- | #r1 #rs1 #Hta2 whd in match (tape_move ???); <Hta2 @change_vec_same ]
- | >tape_move_mk_tape_R [| #_ % %] >reverse_cons
- >nth_change_vec_neq in Hcurtc'; [|@sym_not_eq //] >Hta2
- normalize in ⊢ (%→?); #H destruct (H) %
- ]
- | #Hta2 >Htc in Hcurtc'; >nth_change_vec_neq [| @sym_not_eq //]
- >Hta2 #H destruct (H)
+@(sem_seq_app FSUnialpha 2 ?????
+ (sem_if ??????????
+ (sem_test_null_multi ?? obj ?)
+ (sem_copy_char_N …)
+ (sem_inject ???? cfg ? (sem_write FSUnialpha null)))
+ (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?))
+ (sem_move_multi ? 2 cfg R ?))) //
+#ta #tout *
+#tb * #Hif * #tc * #HM2 #HM3 #c #ls #Hcfg
+(* Hif *)
+cases Hif -Hif
+[ * #t1 * * #Hcurta #Ht1 destruct (Ht1)
+ lapply (not_None_to_Some … Hcurta) * #curta #Hcurtaeq
+ whd in ⊢ (%→?); #Htb % [2: #Hcur @False_ind /2/]
+ #lso #xo #rso #Hobjta cases HM2 whd in ⊢ (%→?); * #_
+ #HM2 #Heq >Htb in HM2; >nth_change_vec [2: @leb_true_to_le %]
+ >Hcfg >Hcurtaeq #HM2 lapply (HM2 … (refl ??)) -HM2
+ whd in match (left ??); whd in match (right ??);
+ >reverse_cons #Htc >HM3 @(eq_vec … (niltape ?)) #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
+ >nth_change_vec_neq [2:@eqb_false_to_not_eq %]
+ <(Heq 0) [2:@eqb_false_to_not_eq %] >Htb
+ >nth_change_vec_neq [2:@eqb_false_to_not_eq %]
+ >nth_change_vec_neq [%|2:@eqb_false_to_not_eq %]
+ |#Hi >Hi >nth_change_vec // >nth_change_vec // >Htc
+ >Hobjta in Hcurtaeq; whd in ⊢ (??%?→?); #Htmp destruct(Htmp)
+ >tape_move_mk_tape_R [2: #_ %1 %] %
+ ]
+ |#Hi >Hi >nth_change_vec_neq [2:@eqb_false_to_not_eq %]
+ >nth_change_vec_neq [2:@eqb_false_to_not_eq %]
+ <(Heq 2) [2:@eqb_false_to_not_eq %] >Htb
+ >nth_change_vec_neq [%|2:@eqb_false_to_not_eq %]
+ ]
+| * #t1 * * #Hcurta #Ht1 destruct (Ht1)
+ * whd in ⊢ (%→?); #Htb lapply (Htb … Hcfg) -Htb #Htb
+ #Htbeq %
+ [#lso #xo #rso #Hmid @False_ind >Hmid in Hcurta;
+ whd in ⊢ (??%?→?); #Htmp destruct (Htmp)]
+ #_ cases HM2 whd in ⊢ (%→?); * #_
+ #HM2 #Heq >Htb in HM2; #HM2 lapply (HM2 … (refl ??)) -HM2
+ #Htc >HM3 @(eq_vec … (niltape ?)) #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
+ >nth_change_vec_neq [2:@eqb_false_to_not_eq %]
+ >nth_change_vec_neq [2:@eqb_false_to_not_eq %]
+ <(Heq 0) [2:@eqb_false_to_not_eq %] >Htb
+ <(Htbeq 0) [2:@eqb_false_to_not_eq %] %
+ |#Hi >Hi >nth_change_vec // >nth_change_vec // >Htc
+ >tape_move_mk_tape_R [2: #_ %1 %] >reverse_cons %