-
-
-
- [ >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/ | % ] | % ] ]]]]]
+ cut (nth src (tape sig) td (niltape sig)=midtape sig (x::ls) c1 tl1)
+ [>Htd >nth_change_vec_neq [2:@(not_to_not … Hneq) //] @nth_change_vec //]
+ #Hsrc_td
+ cut (nth dst (tape sig) td (niltape sig)=midtape sig (x::ls0) c2 tl2)
+ [>Htd @nth_change_vec //]
+ #Hdst_td cases (IH2 … Hsrc_td Hdst_td) -Hsrc_td -Hdst_td
+ [* #rs01 * #rs02 * * #H1 #H2 #H3 %1
+ %{(c2::rs01)} %{rs02} % [% [@eq_f //|normalize @eq_f @H2]]
+ >Htd in H3; >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
+ #H >reverse_cons >associative_append >associative_append @H
+ |* #rs11 * #rs12 * * #H1 #H2 #H3 %2
+ %{(c1::rs11)} %{rs12} % [% [@eq_f //|normalize @eq_f @H2]]
+ >Htd in H3; >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute [2:@(not_to_not … Hneq) //] >change_vec_change_vec
+ #H >reverse_cons >associative_append >associative_append @H
+ ]
+ ]
+ ]
+ ]