- #Htrue cases (Htrue ? (refl ??)) -Htrue #_ #Htrue
- <(change_vec_same … t1 dst (niltape ?))
- cases (Htrue Hstart Hnotstart) -Htrue
- cases (true_or_false (start == s)) #Hs
- [ lapply (\P Hs) -Hs #Hs <Hs #_ #Htrue
- cut (∃ls0,xs0,ci,rs,rs0.
- nth src ? t (niltape ?) = midtape sig [ ] start (xs0@ci::rs) ∧
- nth dst ? t (niltape ?) = midtape sig ls0 s (xs0@rs0) ∧
- (is_endc ci = true ∨ (is_endc ci = false ∧ (∀b,tlb.rs0 = b::tlb → ci ≠ b))))
- [cases (comp_list ? (xs@[end]) (r0::rs0) is_endc) #xs0 * #xs1 * #xs2
- * * * #Hxs #Hrs #Hxs0notend #Hcomp >Hrs
- cut (∃y,ys. xs1 = y::ys)
- [ lapply Hxs0notend lapply Hxs lapply xs0 elim xs
- [ *
- [ normalize #Hxs1 <Hxs1 #_ %{end} %{[]} %
- | #z #zs normalize in ⊢ (%→?); #H destruct (H) #H
- lapply (H ? (memb_hd …)) -H >Hend #H1 destruct (H1)
- ]
- | #y #ys #IH0 *
- [ normalize in ⊢ (%→?); #Hxs1 <Hxs1 #_ %{y} %{(ys@[end])} %
- | #z #zs normalize in ⊢ (%→?); #H destruct (H) #Hmemb
- @(IH0 ? e0 ?) #c #Hc @Hmemb @memb_cons // ] ] ] * #y * #ys #Hxs1
- >Hxs1 in Hxs; #Hxs >Hmid_src >Hmid_dst >Hxs >Hrs
- %{ls} %{xs0} %{y} %{ys} %{xs2}
- % [ % // | @Hcomp // ] ]
- * #ls0 * #xs0 * #ci * #rs * #rs0 * * #Hmid_src' #Hmid_dst' #Hcomp
- <Hmid_src in Htrue; >nth_change_vec // >Hs #Htrue destruct (Hs)
- lapply (Htrue ??????? Hmid_src' Hmid_dst' ?) -Htrue
- [ #c0 #Hc0 @Hnotend cases (orb_true_l … Hc0) -Hc0 #Hc0
- [ whd in ⊢ (??%?); >Hc0 %
- | @memb_cons >Hmid_src in Hmid_src'; #Hmid_src' destruct (Hmid_src')
- lapply e0 -e0 @(list_elim_left … rs)
- [ #e0 destruct (e0) lapply (append_l1_injective_r ?????? e0) //
- | #x1 #xs1 #_ >append_cons in ⊢ (???%→?);
- <associative_append #e0 lapply (append_l1_injective_r ?????? e0) //
- #e1 >e1 @memb_append_l1 @memb_append_l1 // ] ]
- | * * #Hciendc cases rs0 in Hcomp;
- [ #_ * #H @False_ind @H %
- | #r1 #rs1 * [ >Hciendc #H destruct (H) ]
- * #_ #Hcomp lapply (Hcomp ?? (refl ??)) -Hcomp #Hcomp #_ #Htrue
- cases (Htrue ?? (refl ??) Hcomp) #Ht1 #_ >Ht1 @(IH ?? (s::ls) r0)
- [ >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src
- | >nth_change_vec // >Hmid_dst % ] ] ]
- | >Hmid_dst >nth_change_vec // lapply (\Pf Hs) -Hs #Hs #Htrue #_
- cases (Htrue ? (refl ??) Hs) #Ht1 #_ >Ht1 @(IH ?? (s::ls) r0)
- [ >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src
- | >nth_change_vec // ] ] ] ]