-]
-qed.
-
-#intape #outtape #ta * #Hcomp1 #Hcomp2 * #tb * * #Hc #Htb
- whd in ⊢ (%→?); #Hout >Hout >Htb whd
- lapply (current_to_midtape sig (nth src ? intape (niltape ?)))
- cases (current … (nth src ? intape (niltape ?))) in Hcomp1;
- [#Hcomp1 #_ %1 % [%1 %2 // | @Hcomp1 %2 %1 %2 %]
- |#c_src lapply (current_to_midtape sig (nth dst ? intape (niltape ?)))
- cases (current … (nth dst ? intape (niltape ?)))
- [#_ #Hcomp1 #_ %1 % [%2 % | @Hcomp1 %2 % % % #H destruct (H)]
- |#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 #Hcomp1
- #Hmid_src cases (Hmid_src c_src (refl …)) -Hmid_src
- #ls_src * #rs_src #Hmid_src
- cases (true_or_false (is_endc c_src)) #Hc_src
- [ % % [ % % %{c_src} % // | @Hcomp1 % %{c_src} % // ]
- | %2 cases (comp_list … rs_src rs_dst is_endc) #xs * #rsi * #rsj * * *
- #Hrs_src #Hrs_dst #Hnotendc #Hneq
- %{ls_src} %{ls_dst} %{rsi} %{rsj} %{c_src} %{xs} %
- [% [% // <Hrs_src //|<Hrs_dst >(\P Hceq) // ]]
- #rsi0 #rsj0 #end #c #Hend #Hc_dst
- >Hrs_src in Hmid_src; >Hend #Hmid_src
- >Hrs_dst in Hmid_dst; >Hc_dst <(\P Hceq) #Hmid_dst
- cut (is_endc end = true ∨ end ≠ c)
- [cases (Hneq … Hend) /2/ -Hneq #Hneq %2 @(Hneq … Hc_dst) ] #Hneq
- lapply (Hcomp2 … Hmid_src Hmid_dst ? Hneq)
- [#c0 #Hc0 cases (orb_true_l … Hc0) -Hc0 #Hc0
- [ >(\P Hc0) //
- | @Hnotendc // ]
- ]
- -Hcomp2 #Hcomp2 <Hcomp2
- % // % [
- >Hcomp2 in Hc; >nth_change_vec_neq [|@sym_not_eq //]
- >nth_change_vec // #H lapply (H ? (refl …))
- cases (is_endc end) [|normalize #H destruct (H) ]
- #_ % // #c0 #Hc0 cases (orb_true_l … Hc0) -Hc0 #Hc0
- [ >(\P Hc0) // | @Hnotendc // ]
- |@Hmid_dst]
- ]
- |#_ #Hcomp1 #Hsrc cases (Hsrc ? (refl ??)) -Hsrc #ls * #rs #Hsrc
- %1 %
- [% % %{c_src} % // lapply (Hc c_src) -Hc >Hcomp1
- [| %2 % % @(not_to_not ??? (\Pf Hceq)) #H destruct (H) // ]
- cases (is_endc c_src) //
- >Hsrc #Hc lapply (Hc (refl ??)) normalize #H destruct (H)
- |@Hcomp1 %2 %1 %1 @(not_to_not ??? (\Pf Hceq)) #H destruct (H) //
- ]
- ]
- ]
- ]
-qed.