- >change_vec_commute [|@sym_not_eq //] >nth_change_vec // #Hte #_
- whd in ⊢ (?→%); >Hmidta_src >Hmidta_dst normalize in ⊢ (?→??%);
- lapply Hte -Hte @(list_elim_left … ls)
- [ #Hte lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
- >change_vec_commute // >change_vec_change_vec
- >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte
- >Hte * * #_ >nth_change_vec // >reverse_reverse
- #H lapply (H … (refl ??)) -H #Htb1 #Htb2
- cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (midtape sig [] s0 (xs@ci::rs'')) src) (mk_tape sig (s0::ls0) (option_hd sig (xs@cj::rs0')) (tail sig (xs@cj::rs0'))) dst)
- [@daemon] -Htb1 -Htb2 #Htb >Htb >nth_change_vec //
- >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
- >right_mk_tape normalize in match (left ??);
- >length_tail >Hrs0 >length_append whd in ⊢ (?(?%)?);
- >commutative_plus %
- | #l1 #ls1 #_ >(?:reverse ? xs@s0::ls1@[l1] = (reverse ? xs@s0::ls1)@[l1])
- [|@daemon]
- #Hte lapply (Hte ???? (refl ??) ??? (reverse ? xs@s0::ls1) ???)
- STOP
- (refl ??)) -Hte
- >change_vec_commute // >change_vec_change_vec
- >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte
- >Hte * * #_ >nth_change_vec // >reverse_reverse
- #H lapply (H … (refl ??)) -H #Htb1 #Htb2
- cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (midtape sig [] s0 (xs@ci::rs'')) src) (mk_tape sig (s0::ls0) (option_hd sig (xs@cj::rs0')) (tail sig (xs@cj::rs0'))) dst)
- [@daemon] -Htb1 -Htb2 #Htb >Htb >nth_change_vec //
- >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
- >right_mk_tape normalize in match (left ??);
- >length_tail >Hrs0 >length_append whd in ⊢ (?(?%)?);
- >commutative_plus %
-
-
- la
- >Hte in Htb; * * #_ >nth_change_vec // #Htb1
- lapply (Htb1 … (refl ??)) -Htb1 #Htb1 #Htb2 %
- [ @(eq_vec … (niltape ?)) #i #Hi
- cases (true_or_false ((dst : DeqNat) == i)) #Hdsti
- [ <(\P Hdsti) >Htb1 >nth_change_vec // >Hmidta_dst
- >Hrs0 >reverse_reverse cases xs [|#r1 #rs1] %
- | <Htb2 [|@(\Pf Hdsti)] >nth_change_vec_neq [| @(\Pf Hdsti)]
- >Hrs0 >reverse_reverse >nth_change_vec_neq in ⊢ (???%);
- <Hrs <Hmidta_src [|@(\Pf Hdsti)] >change_vec_same % ]
- | >Hmidta_dst %{s'} % [%] #_
- >Hrs0 %{xs} %{ci} %{rs''} %{ls0} %{cj} %{rs0'} % // % //
+ >change_vec_commute [|@sym_not_eq //] >nth_change_vec //
+ cases (lists_length_split ? ls ls0) #lsa * #lsb * * #Hlen #Hlsalsb
+ destruct (Hlsalsb) *
+ [ #Hte #_ #_ <(reverse_reverse … ls) in Hte; <(reverse_reverse … lsa)
+ cut (|reverse ? lsa| = |reverse ? ls|) [ // ] #Hlen'
+ @(list_cases2 … Hlen')
+ [ #H1 #H2 >H1 >H2 -H1 -H2 normalize in match (reverse ? [ ]); #Hte
+ lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
+ >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec #Hte
+ >Hte * * #_ >nth_change_vec // >reverse_reverse
+ #H lapply (H … (refl ??)) -H #Htb1 #Htb2
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (midtape sig [] s0 (xs@ci::rs'')) src) (mk_tape sig (s0::lsb) (option_hd sig (xs@cj::rs0')) (tail sig (xs@cj::rs0'))) dst)
+ [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec //
+ >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
+ >right_mk_tape normalize in match (left ??);
+ >Hmidta_src >Hmidta_dst >length_tail >Hrs0 >length_append
+ normalize in ⊢ (?(?%)(?%?)); >commutative_plus //
+ | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
+ >reverse_cons >reverse_cons #Hte
+ lapply (Hte ci hdb (reverse ? xs@s0::reverse ? tlb) rs'' ?
+ lsb cj hda (reverse ? xs@s0::reverse ? tla) rs0' ??)
+ [ /2 by cons_injective_l, nil/
+ | >length_append >length_append @eq_f @(eq_f ?? S)
+ >H1 in Hlen'; >H2 whd in ⊢ (??%%→?); #Hlen'
+ >length_reverse >length_reverse destruct (Hlen') //
+ | /2 by refl, trans_eq/ ] -Hte
+ #Hte * * #_ >Hte >nth_change_vec // #Htb1 #Htb2
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
+ (mk_tape sig (hda::lsb) (option_hd ? (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0')) (tail ? (reverse sig (reverse sig xs@s0::reverse sig tla)@cj::rs0'))) dst)
+ (midtape ? [ ] hdb (reverse sig (reverse sig xs@s0::reverse sig tlb)@ci::rs'')) src)
+ [@daemon] -Htb1 -Htb2 #Htb >Htb whd
+ >nth_change_vec // >nth_change_vec_neq // >nth_change_vec //
+ >right_mk_tape >Hmidta_src >Hmidta_dst
+ whd in match (left ??); whd in match (left ??); whd in match (right ??);
+ >length_tail >Hrs0 >length_append >length_append >length_reverse
+ >length_append >commutative_plus in match (|reverse ??| + ?);
+ whd in match (|?::?|); >length_reverse >length_reverse
+ <(length_reverse ? ls) <Hlen' >H1 normalize // ]
+ | #_ #Hte #_ <(reverse_reverse … ls0) in Hte; <(reverse_reverse … lsa)
+ cut (|reverse ? lsa| = |reverse ? ls0|) [ // ] #Hlen'
+ @(list_cases2 … Hlen')
+ [ #H1 #H2 >H1 >H2 normalize in match (reverse ? [ ]); #Hte
+ lapply (Hte … (refl ??) … (refl ??) (refl ??)) -Hte
+ >change_vec_change_vec >change_vec_commute [|@sym_not_eq //]
+ >change_vec_change_vec #Hte
+ >Hte * * #_ >nth_change_vec // >reverse_reverse
+ #H lapply (H … (refl ??)) -H #Htb1 #Htb2
+ (* cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (midtape sig [] s0 (xs@ci::rs'')) src) (mk_tape sig (s0::lsb) (option_hd sig (xs@cj::rs0')) (tail sig (xs@cj::rs0'))) dst) *)
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta (mk_tape ? [s0] (option_hd ? (xs@cj::rs0')) (tail ? (xs@cj::rs0'))) dst)
+ (midtape ? lsb s0 (xs@ci::rs'')) src)
+ [@daemon] -Htb1 -Htb2 #Htb >Htb whd >nth_change_vec //
+ >nth_change_vec_neq // >nth_change_vec //
+ >right_mk_tape normalize in match (left ??);
+ >Hmidta_src >Hmidta_dst >length_tail >Hrs0 >length_append
+ >commutative_plus in match (pred ?); normalize
+ >length_append >(?:|lsa| = O)
+ [ normalize <plus_n_Sm <plus_n_Sm // | <(length_reverse ? lsa) >H1 % ]
+ | #hda #hdb #tla #tlb #H1 #H2 >H1 >H2
+ >reverse_cons >reverse_cons #Hte
+ lapply (Hte cj hdb (reverse ? xs@s0::reverse ? tlb) rs0' ?
+ lsb ci hda (reverse ? xs@s0::reverse ? tla) rs'' ??)
+ [ /2 by cons_injective_l, nil/
+ | >length_append >length_append @eq_f @(eq_f ?? S)
+ >H1 in Hlen'; >H2 whd in ⊢ (??%%→?); #Hlen'
+ >length_reverse >length_reverse destruct (Hlen') //
+ | /2 by refl, trans_eq/ ] -Hte
+ #Hte * * #_ >Hte >nth_change_vec_neq // >nth_change_vec // #Htb1 #Htb2
+ cut (tb = change_vec ?? (change_vec (tape sig) (S n) ta
+ (mk_tape sig [hdb] (option_hd ? (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0')) (tail ? (reverse sig (reverse sig xs@s0::reverse sig tlb)@cj::rs0'))) dst)
+ (midtape ? lsb hda (reverse sig (reverse sig xs@s0::reverse sig tla)@ci::rs'')) src)
+ [@daemon] -Htb1 -Htb2 #Htb >Htb whd
+ >nth_change_vec // >nth_change_vec_neq // >nth_change_vec //
+ >right_mk_tape >Hmidta_src >Hmidta_dst
+ whd in match (left ??); whd in match (left ??); whd in match (right ??);
+ >length_tail >Hrs0 >length_append >length_append >length_reverse
+ >length_append >commutative_plus in match (|reverse ??| + ?);
+ whd in match (|?::?|); >length_reverse >length_reverse >Hlen
+ <(length_reverse ? ls0) >H2 whd in match (|?::?|);
+ >length_append normalize //
+ ]