+definition Pre_copy0 ≝ λt1.
+ ∃ls,c,c0,rs,l1,l3,l4.
+ t1 = midtape STape (l3@l4@〈c0,true〉::ls) 〈c,true〉 (l1@rs) ∧
+ no_marks l1 ∧ no_marks (l3@l4) ∧ |l1| = |l4| ∧
+ (∃l1',bv.〈c,false〉::l1 = l1'@[〈comma,bv〉] ∧ only_bits_or_nulls l1') ∧
+ (∃l4',bg.l4@[〈c0,false〉] = 〈grid,bg〉::l4' ∧ only_bits_or_nulls l4').
+
+definition Pre_copy ≝ λt1.
+ ∃ls,s0,s1,c0,c1,rs,l1,l3,l4.
+ t1 = midtape STape (l3@〈grid,false〉::〈c0,false〉::l4@〈s0,true〉::ls) 〈s1,true〉 (l1@〈c1,false〉::〈comma,false〉::rs) ∧
+ no_marks l1 ∧ no_marks l3 ∧ no_marks l4 ∧ |l1| = |l4| ∧
+ only_bits (l4@[〈s0,false〉]) ∧ only_bits (〈s1,false〉::l1) ∧
+ bit_or_null c0 = true ∧ bit_or_null c1 = true.
+
+lemma list_last: ∀A.∀l:list A.
+ l = [ ] ∨ ∃a,l1. l = l1@[a].
+#A #l <(reverse_reverse ? l) cases (reverse A l)
+ [%1 //
+ |#a #l1 %2 @(ex_intro ?? a) @(ex_intro ?? (reverse ? l1)) //
+ ]
+qed.
+
+lemma terminate_copy0 : ∀t.Pre_copy0 t → Terminate ? copy0 t.
+#t #HPre
+@(terminate_while_guarded ???
+ Pre_copy0 …
+ (acc_Realize_to_acc_GRealize ??? Pre_copy0 … sem_copy_step)
+ … HPre) [%]
+ [ -HPre -t #t1 #t2 * #ls * #c * #c0 * #rs * #l1 * #l3 * #l4
+ * * * * * #Ht1 #Hl1nomarks #Hl3l4nomarks #Hlen
+ * #l1' * #bv * #Hl1 #Hbitsnullsl1' * #l4' * #bg * #Hl4 #Hbitsnullsl4'
+ #HR cases (HR … Ht1) -HR #Hbitnullc
+ cut (∃d1,l1''.l1 = 〈d1,false〉::l1'')
+ [ lapply Hl1nomarks cases l1 in Hl1;
+ [ whd in ⊢ (???%→?); #Hl1
+ lapply (append_l2_injective_r ? [] l1' [〈c,false〉] [〈comma,bv〉] (refl ??) Hl1)
+ #Hc destruct (Hc) normalize in Hbitnullc; destruct (Hbitnullc)
+ | * #d #bd #l1'' #_ #Hl1nomarks >(?:bd = false) [| @(Hl1nomarks 〈d,bd〉) @memb_hd ] /3/ ] ]
+ * #d1 * #l1'' #Hl1''
+ cut (∃d2,l4''.l4 = l4''@[〈d2,false〉])
+ [ lapply Hl4 cases (list_last ? l4)
+ [ #Hl4' >Hl4' in Hlen; >Hl1'' normalize in ⊢ (%→?); #HFalse destruct (HFalse)
+ | * * #d2 #bd2 * #l4'' #Hl4'' >Hl4'' in Hl3l4nomarks; #Hl3l4nomarks #_
+ <(?:bd2 = false) [| @(Hl3l4nomarks 〈d2,bd2〉) @memb_append_l2 @memb_append_l2 @memb_hd ]
+ /3/ ] ]
+ * #d2 * #l4'' #Hl4'' >Hl1'' >Hl4''
+ cut (∃l1''',bv0.〈d1,false〉::l1''=l1'''@[〈comma,bv0〉]∧only_bits_or_nulls l1''')
+ [ <Hl1'' cases (list_last ? l1) in Hl1'';
+ [ #Hl1'' >Hl1''#HFalse destruct(HFalse)
+ | * #a * #l1''' #Hl1''' >Hl1''' in Hl1; #Hl1 #_
+ lapply (append_l2_injective_r ? (〈c,false〉::l1''') l1' [a] [〈comma,bv〉] (refl …) Hl1)
+ #Ha destruct (Ha) %{l1'''} %{bv} % //
+ #x #Hx @Hbitsnullsl1'
+ lapply (append_l1_injective_r ? (〈c,false〉::l1''') l1' [〈comma,bv〉] [〈comma,bv〉] (refl …) Hl1)
+ #H <H @memb_cons @Hx ] ]
+ cut (∃l4''',bg0.l4''@[〈d2,false〉]=〈grid,bg0〉::l4'''∧only_bits_or_nulls l4''')
+ [ <Hl4'' cases (list_last ? l4') in Hl4;
+ [ #Hl4' >Hl4' >Hl4'' cases l4''
+ [ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
+ | #y #yl normalize in ⊢ (%→?); #H1 destruct (H1) cases yl in e0;
+ [ normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
+ | #z #zl normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ] ]
+ | * #a * #l4''' #Hl4''' >Hl4''' #Hl4
+ lapply (append_l1_injective_r ? l4 (〈grid,bg〉::l4''') [〈c0,false〉] [a] (refl …) Hl4)
+ -Hl4 #Hl4 >Hl4 %{l4'''} %{bg} % //
+ #x #Hx @Hbitsnullsl4' >Hl4''' @memb_append_l1 @Hx ] ]
+ #Hl4''' #Hl1'''
+ #HR cases (HR d1 (l3@l4'') c0 d2 ls (l1''@rs) ? ? ?)
+ [3: >associative_append >associative_append %
+ |4: %
+ |5: #x #Hx @Hl3l4nomarks cases (memb_append … Hx)
+ [ @memb_append_l1
+ | >Hl4'' -Hx #Hx @memb_append_l2 @memb_append_l1 @Hx ]
+ | * #x1 * #Hc #Ht2 whd >Ht2
+ %{(〈bit x1,false〉::ls)} %{d1} %{d2} %{rs} %{l1''} %{(〈bit x1,false〉::l3)} %{l4''}
+ % [ % [ % [ % [ %
+ [ >associative_append %
+ | #x #Hx @Hl1nomarks >Hl1'' @memb_cons @Hx ]
+ | #x #Hx cases (orb_true_l … Hx) -Hx #Hx
+ [ >(\P Hx) %
+ | @Hl3l4nomarks cases (memb_append … Hx)
+ [ @memb_append_l1
+ | -Hx #Hx >Hl4'' @memb_append_l2 @memb_append_l1 @Hx ] ] ]
+ | >Hl1'' in Hlen; >Hl4'' >length_append >commutative_plus
+ normalize in ⊢ (%→?); #Hlen destruct (Hlen) @e0 ]
+ | @Hl1''' ]
+ | @Hl4''' ]
+ | * #Hc #Ht2 whd >Ht2
+ %{(〈c0,false〉::ls)} %{d1} %{d2} %{rs} %{l1''} %{(〈null,false〉::l3)} %{l4''}
+ % [ % [ % [ % [ %
+ [ >associative_append %
+ | #x #Hx @Hl1nomarks >Hl1'' @memb_cons @Hx ]
+ | #x #Hx cases (orb_true_l … Hx) -Hx #Hx
+ [ >(\P Hx) %
+ | @Hl3l4nomarks cases (memb_append … Hx)
+ [ @memb_append_l1
+ | -Hx #Hx >Hl4'' @memb_append_l2 @memb_append_l1 @Hx ] ] ]
+ | >Hl1'' in Hlen; >Hl4'' >length_append >commutative_plus
+ normalize in ⊢ (%→?); #Hlen destruct (Hlen) @e0 ]
+ | @Hl1''' ]
+ | @Hl4''' ]
+ ]
+ |cases HPre -HPre #ls * #c * #c0 * #rs * #l1 * #l3 * #l4
+ * * * * * #Ht #Hl1nomarks #Hl3l4nomarks #Hlen
+ * #l1' * #bv * #Hl1 #Hbitsnullsl1'
+ * #l4' * #bg * #Hl4 #Hbitsnullsl4'
+ >Ht lapply Hbitsnullsl1' lapply Hl1 lapply l1' lapply Hl3l4nomarks
+ lapply Hl1nomarks lapply l3 lapply c0 lapply c lapply ls
+ -Hbitsnullsl1' -Hl1 -l1' -Hl3l4nomarks -Hl1nomarks -l3 -Hl4 -c0 -c -ls
+ <(reverse_reverse ? l4) <(length_reverse ? l4) in Hlen; #Hlen
+ @(list_ind2 … Hlen)
+ [ #ls #c #c0 #l3 #_ #_ #l1' #Hl1 #Hbitsnullsl1' cases l1' in Hl1;
+ [| #x * [| #x0 #xs ] normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+ normalize in ⊢ (%→?); #Hl1' destruct (Hl1') % #t1 whd in ⊢ (%→?);
+ #HR cases (HR … (refl …)) whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse)
+ | #xs #ys * #x #bx * #y #by #IH
+ #ls #c #c0 #l3 #Hl1nomarks #Hl3l4nomarks #l1' #Hl1
+ #Hbitsnullsl1' %
+ #t1 whd in ⊢ (%→?); #HR cases (HR … (refl …)) -HR
+ #Hbitnullc #HR
+ lapply (Hl1nomarks 〈x,bx〉 (memb_hd …)) normalize in ⊢ (%→?); #Hbx destruct (Hbx)
+ (*cut (∃d2,l4''.〈y,by〉::ys = l4''@[〈d2,false〉])
+ [ cases (list_last ? ys) in Hl3l4nomarks;
+ [ #Hl4' #Hl3l4nomarks >Hl4' >(?:by = false) [%{y} %{([])} %]
+ @(Hl3l4nomarks 〈y,by〉) @memb_append_l2 @memb_hd
+ | * * #d2 #bd2 * #l4'' #Hl4'' >Hl4'' #Hl3l4nomarks
+ <(?:bd2 = false) [| @(Hl3l4nomarks 〈d2,bd2〉) @memb_append_l2 @memb_cons @memb_append_l2 @memb_hd ]
+ %{d2} %{(〈y,by〉::l4'')} % ] ]
+ * #a0 * #l4'' #Hl4'' >Hl4'' in HR; #HR *)
+ cases (HR x (l3@reverse ? ys) c0 y ls (xs@rs) ? (refl …) ?)
+ [3: >reverse_cons >associative_append >associative_append
+ >(?:by = false) [|@(Hl3l4nomarks 〈y,by〉) @memb_append_l2 >reverse_cons @memb_append_l2 @memb_hd ] %
+ |4: #x #Hx @Hl3l4nomarks >reverse_cons <associative_append @memb_append_l1 @Hx
+ | * #x1 * #Hc #Ht1 >Ht1
+ <(?: (〈bit x1,false〉::l3)@reverse (FSUnialpha×bool) ys@〈y,true〉::〈bit x1,false〉::ls =
+ 〈bit x1,false〉::(l3@reverse (FSUnialpha×bool) ys)@〈y,true〉::〈bit x1,false〉::ls)
+ [cut (∃l1''.〈x,false〉::xs = l1''@[〈comma,bv〉] ∧ only_bits_or_nulls l1'')
+ [lapply Hbitsnullsl1' lapply Hl1 -Hl1 -Hbitsnullsl1' cases l1'
+ [normalize in ⊢(%→?); #Hfalse destruct (Hfalse)
+ |#x2 #l1'' normalize in ⊢ (%→?); #Heq #Hbitsnullsl1' destruct (Heq)
+ %{l1''} % [@e0]
+ #x #Hx @Hbitsnullsl1' @memb_cons @Hx ] ]
+ * #l1'' * #Hl1'' #Hbitsnullsl1''
+ @(IH (〈bit x1,false〉::ls) x y (〈bit x1,false〉::l3) ?? l1'' Hl1'' Hbitsnullsl1'')
+ [#x #Hx @Hl1nomarks @memb_cons @Hx
+ |#x #Hx cases (orb_true_l … Hx) -Hx #Hx
+ [>(\P Hx) %
+ |cases (memb_append … Hx) -Hx #Hx @Hl3l4nomarks
+ [@memb_append_l1 @Hx
+ |@memb_append_l2 >reverse_cons @memb_append_l1 @Hx ] ] ]
+ |>associative_append % ]
+ | * #Hc #Ht1 >Ht1
+ <(?: (〈null,false〉::l3)@reverse (FSUnialpha×bool) ys@〈y,true〉::〈c0,false〉::ls =
+ 〈null,false〉::(l3@reverse (FSUnialpha×bool) ys)@〈y,true〉::〈c0,false〉::ls)
+ [cut (∃l1''.〈x,false〉::xs = l1''@[〈comma,bv〉] ∧ only_bits_or_nulls l1'')
+ [lapply Hbitsnullsl1' lapply Hl1 -Hl1 -Hbitsnullsl1' cases l1'
+ [normalize in ⊢(%→?); #Hfalse destruct (Hfalse)
+ |#x2 #l1'' normalize in ⊢ (%→?); #Heq #Hbitsnullsl1' destruct (Heq)
+ %{l1''} % [@e0]
+ #x #Hx @Hbitsnullsl1' @memb_cons @Hx ] ]
+ * #l1'' * #Hl1'' #Hbitsnullsl1''
+ @(IH (〈c0,false〉::ls) x y (〈null,false〉::l3) ?? l1'' Hl1'' Hbitsnullsl1'')
+ [#x #Hx @Hl1nomarks @memb_cons @Hx
+ |#x #Hx cases (orb_true_l … Hx) -Hx #Hx
+ [>(\P Hx) %
+ |cases (memb_append … Hx) -Hx #Hx @Hl3l4nomarks
+ [@memb_append_l1 @Hx
+ |@memb_append_l2 >reverse_cons @memb_append_l1 @Hx ] ] ]
+ |>associative_append % ]
+]]]
+qed.
+