-| #td #te * #c0 * * #Hc0 #Hc0nosep #Hd #Hstar #IH #He
- lapply (IH He) -IH * * #IH1 #IH2 #IH3 % [ %
- [ #ls #x #xs #rs #sep #Hsrc_tc #Hnosep #Hsep #ls0 #x0 #target
- #c #rs0 #Hlen #Hdst_tc
- >Hsrc_tc in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
- <(change_vec_same … td src (niltape ?)) in Hd:(???(???(???%??)??));
- <(change_vec_same … td dst (niltape ?)) in ⊢(???(???(???%??)??)→?);
- >Hdst_tc >Hsrc_tc >(change_vec_change_vec ?) >change_vec_change_vec
- >(change_vec_commute ?? td ?? dst src) [|@(sym_not_eq … Hneq)]
- >change_vec_change_vec @(list_cases2 … Hlen)
- [ #Hxsnil #Htargetnil #Hd>(IH2 … Hsep)
- [ >Hd -Hd >Hxsnil >Htargetnil @(eq_vec … (niltape ?))
- #i #Hi cases (decidable_eq_nat i src) #Hisrc
- [ >Hisrc >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
- >nth_change_vec // >nth_change_vec //
- >(nth_change_vec_neq … src dst) [|@(sym_not_eq … Hneq)]
- >nth_change_vec // whd in ⊢ (??%?); %
- | cases (decidable_eq_nat i dst) #Hidst
- [ >Hidst >nth_change_vec // >nth_change_vec //
- >nth_change_vec_neq // >Hdst_tc >Htargetnil %
- | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
- >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
- >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
- >nth_change_vec_neq [|@(sym_not_eq … Hisrc)] % ]
- ]
- | >Hd >nth_change_vec_neq [|@(sym_not_eq … Hneq)]
- >nth_change_vec // >nth_change_vec // >Hxsnil % ]
- |#hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
- >(IH1 (c0::ls) hd1 tl1 rs sep ?? Hsep (c0::ls0) hd2 tl2 c rs0)
- [ >Hd >(change_vec_commute … ?? td ?? src dst) //
- >change_vec_change_vec
- >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
- >change_vec_change_vec
- >reverse_cons >associative_append >associative_append %
- | >Hd >nth_change_vec // >nth_change_vec_neq // >Hdst_tc >Htarget //
- | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
- | <Hxs #c1 #Hc1 @Hnosep @memb_cons //
- | >Hd >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec // >nth_change_vec // ]
- ]
- | #c #Hc #Hsepc >Hc in Hc0; #Hcc0 destruct (Hcc0) >Hc0nosep in Hsepc;
- #H destruct (H)
- ]
-| #HNone >HNone in Hc0; #Hc0 destruct (Hc0) ] ]
+|#tc #td * #x * #y * * #Hcx #Hcy #Htd #Hstar #IH #He lapply (IH He) -IH *
+ #IH1 #IH2 %
+ [* [>Hcx #H destruct (H) | >Hcy #H destruct (H)]
+ |#ls #x' #y' #rs #ls0 #rs0 #Hnth_src #Hnth_dst
+ >Hnth_src in Hcx; whd in ⊢ (??%?→?); #H destruct (H)
+ >Hnth_dst in Hcy; whd in ⊢ (??%?→?); #H destruct (H)
+ >Hnth_src in Htd; >Hnth_dst -Hnth_src -Hnth_dst
+ cases rs
+ [(* the source tape is empty after the move *)
+ lapply (IH1 ?) [@daemon]
+ #Hout (* whd in match (tape_move ???); *) #Htemp %1 %{([])} %{rs0} %
+ [% [// | // ]
+ |whd in match (reverse ??); whd in match (reverse ??);
+ >Hout >Htemp @eq_f2 // cases rs0 //
+ ]
+ |#c1 #tl1 cases rs0
+ [(* the dst tape is empty after the move *)
+ lapply (IH1 ?) [@daemon]
+ #Hout (* whd in match (tape_move ???); *) #Htemp %2 %{[ ]} %{(c1::tl1)} %
+ [% [// | // ]
+ |whd in match (reverse ??); whd in match (reverse ??);
+ >Hout >Htemp @eq_f2 //
+ ]
+ |#c2 #tl2 whd in match (tape_move_mono ???); whd in match (tape_move_mono ???);
+ #Htd
+
+
+
+ [ >Hci >Hcj * [ *
+ [ * #H @False_ind @H % | #H destruct (H)] | #H destruct (H)]
+ | #ls #c0 #rs #ls0 #rs0 cases rs
+ [ -IH2 #Hnthi #Hnthj % %2 %{rs0} % [%]
+ >Hnthi in Hd; #Hd >Hd in IH1; #IH1 >IH1
+ [| % %2 >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec // % ]
+ >Hnthj cases rs0 [| #r1 #rs1 ] %
+ | #r1 #rs1 #Hnthi cases rs0
+ [ -IH2 #Hnthj % % %{(r1::rs1)} % [%]
+ >Hnthj in Hd; #Hd >Hd in IH1; #IH1 >IH1
+ [| %2 >nth_change_vec // ]
+ >nth_change_vec //
+ | #r2 #rs2 #Hnthj lapply IH2; >Hd in IH1; >Hnthi >Hnthj
+ >nth_change_vec //
+ >nth_change_vec_neq [| @sym_not_eq // ] >nth_change_vec //
+ cases (true_or_false (r1 == r2)) #Hr1r2
+ [ >(\P Hr1r2) #_ #IH2 cases (IH2 … (refl ??) (refl ??)) [ *
+ [ * #rs' * #Hrs1 #Hcurout_j % % %{rs'}
+ >Hrs1 >Hcurout_j normalize % //
+ | * #rs0' * #Hrs2 #Hcurout_i % %2 %{rs0'}
+ >Hrs2 >Hcurout_i % //
+ >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute [|@sym_not_eq//] >change_vec_change_vec
+ >reverse_cons >associative_append >associative_append % ]
+ | * #xs * #ci * #cj * #rs' * #rs0' * * * #Hcicj #Hrs1 #Hrs2
+ >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute [| @sym_not_eq ] // >change_vec_change_vec
+ #Houtc %2 %{(r2::xs)} %{ci} %{cj} %{rs'} %{rs0'}
+ % [ % [ % [ // | >Hrs1 // ] | >Hrs2 // ]
+ | >reverse_cons >associative_append >associative_append >Houtc % ] ]
+ | lapply (\Pf Hr1r2) -Hr1r2 #Hr1r2 #IH1 #_ %2
+ >IH1 [| % % normalize @(not_to_not … Hr1r2) #H destruct (H) % ]
+ %{[]} %{r1} %{r2} %{rs1} %{rs2} % [ % [ % /2/ | % ] | % ] ]]]]]