- | >Htc >change_vec_commute // >nth_change_vec // ] -Hte
- >Htc >change_vec_commute // >change_vec_change_vec
- >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte
- >Hte in Htb; * * #_ >reverse_reverse #Htbdst1 #Htbdst2 -Hte @(eq_vec … (niltape ?))
- #i #Hi cases (decidable_eq_nat i dst) #Hidst
- [ >Hidst >nth_change_vec // >(Htbdst1 ls0 s (xs@cj'::rs0'))
- [| >nth_change_vec // ]
- >Htadst_mid cases xs //
- | >nth_change_vec_neq [|@sym_not_eq // ]
- <Htbdst2 [| @sym_not_eq // ] >nth_change_vec_neq [| @sym_not_eq // ]
- <Htasrc_mid >change_vec_same % ]
- | >Hcurta_src in Htest; whd in ⊢(??%?→?);
- >Htc >change_vec_commute //
- change with (current ? (niltape ?)) in match (None ?);
- <nth_vec_map >nth_change_vec // whd in ⊢ (??%?→?);
- cases (is_endc ci) whd in ⊢ (??%?→?); #H destruct (H) %
- ]
- ]
-|#intape #outtape #ta * #Hcomp1 #Hcomp2 * #tb * * #Hc #Htb
- whd in ⊢ (%→?); #Hout >Hout >Htb whd
- #ls #c_src #xs #end #rs #Hmid_src #Hnotend #Hend
- lapply (current_to_midtape sig (nth dst ? intape (niltape ?)))
- cases (current … (nth dst ? intape (niltape ?))) in Hcomp1;
- [#Hcomp1 #_ %1 % % [% | @Hcomp1 %2 %2 % ]
- |#c_dst cases (true_or_false (c_src == c_dst)) #Hceq
- [#_ #Hmid_dst cases (Hmid_dst c_dst (refl …)) -Hmid_dst
- #ls_dst * #rs_dst #Hmid_dst
- cases (comp_list … (xs@end::rs) rs_dst is_endc) #xs1 * #rsi * #rsj * * *
- #Hrs_src #Hrs_dst #Hnotendxs1 #Hneq >Hrs_dst in Hmid_dst; #Hmid_dst
- cut (∃r1,rs1.rsi = r1::rs1) [@daemon] * #r1 * #rs1 #Hrs1 >Hrs1 in Hrs_src;
- #Hrs_src >Hrs_src in Hmid_src; #Hmid_src <(\P Hceq) in Hmid_dst; #Hmid_dst
- lapply (Hcomp2 ??????? Hmid_src Hmid_dst ?)
- [ #c0 #Hc0 cases (orb_true_l … Hc0) -Hc0 #Hc0
- [ >(\P Hc0) @Hnotend @memb_hd | @Hnotendxs1 //] ]
- *
- [ * #Hrsj >Hrsj #Hta % %2 >Hta >nth_change_vec // cases (reverse ? xs1) //
- | * #cj * #rs2 * #Hrsj #Hta lapply (Hta ?)
- [ cases (Hneq ?? Hrs1) /2/ #Hr1 %2 @(Hr1 ?? Hrsj) ] -Hta #Hta
- %2 >Hta in Hc; whd in ⊢ (??%?→?);
- change with (current ? (niltape ?)) in match (None ?);
- <nth_vec_map >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
- whd in ⊢ (??%?→?); #Hc cut (is_endc r1 = true)
- [ cases (is_endc r1) in Hc; whd in ⊢ (??%?→?); //
- change with (current ? (niltape ?)) in match (None ?);
- <nth_vec_map >nth_change_vec // normalize #H destruct (H) ]
- #Hendr1 cut (xs = xs1)
- [ lapply Hnotendxs1 lapply Hnotend lapply Hrs_src lapply xs1
- -Hnotendxs1 -Hnotend -Hrs_src -xs1 elim xs
- [ * normalize in ⊢ (%→?); //
- #x2 #xs2 normalize in ⊢ (%→?); #Heq destruct (Heq) #_ #Hnotendxs1
- lapply (Hnotendxs1 ? (memb_hd …)) >Hend #H destruct (H)
- | #x2 #xs2 #IH *
- [ normalize in ⊢ (%→?); #Heq destruct (Heq) #Hnotendc
- >Hnotendc in Hendr1; [| @memb_cons @memb_hd ]
- normalize in ⊢ (%→?); #H destruct (H)
- | #x3 #xs3 normalize in ⊢ (%→?); #Heq destruct (Heq)
- #Hnotendc #Hnotendcxs1 @eq_f @IH
- [ @(cons_injective_r … Heq)
- | #c0 #Hc0 @Hnotendc cases (orb_true_l … Hc0) -Hc0 #Hc0
- [ >(\P Hc0) @memb_hd
- | @memb_cons @memb_cons // ]
- | #c #Hc @Hnotendcxs1 @memb_cons // ]
- ]
- ]
- | #Hxsxs1 destruct (Hxsxs1) >Hmid_dst %{ls_dst} %{rsj} % //
- #rsj0 #c >Hrsj #Hrsj0 destruct (Hrsj0)
- lapply (append_l2_injective … Hrs_src) // #Hrs' destruct (Hrs') %
- ]
- ]
- |#Hcomp1 #Hsrc cases (Hsrc ? (refl ??)) -Hsrc #ls0 * #rs0 #Hdst
- @False_ind lapply (Hcomp1 ?) [%2 %1 %1 >Hmid_src normalize
- @(not_to_not ??? (\Pf Hceq)) #H destruct //] #Hintape >Hintape in Hc;
- whd in ⊢(??%?→?); >Hmid_src
- change with (current ? (niltape ?)) in match (None ?);
- <nth_vec_map >Hmid_src whd in ⊢ (??%?→?);
- >(Hnotend c_src) [|@memb_hd]
- change with (current ? (niltape ?)) in match (None ?);
- <nth_vec_map >Hmid_src whd in ⊢ (??%?→?); >Hdst normalize #H destruct (H)
- ]