+lemma binaryTM_phase0_None_None :
+ ∀sig,M,t,q,ch,n,qn,mv.
+ O < n → n < 2*FS_crd sig →
+ halt sig M q=false →
+ current ? t = None ? →
+ 〈qn,None ?,mv〉 = trans sig M 〈q,None ?〉 →
+ ∀k.O < k →
+ loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin0,ch,n〉) t)
+ = loopM ? (mk_binaryTM sig M) (k-1)
+ (mk_config ?? (〈qn,bin3,None ?,to_initN (displ2_of_move sig mv) ??〉) (tape_move ? t (mv_tech mv))). [| @le_S @le_S //|@le_S_S @le_displ2_of_move]
+#sig #M #t #q #ch #n #qn #mv #HOn #Hn #Hhalt #Hcur #Htrans #k #Hk
+cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
+cases (le_to_eq … HOn) #n0 #Hn0 destruct (Hn0)
+lapply Htrans lapply Hcur -Htrans -Hcur cases t
+[ >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin3 //
+| #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin3 //
+| #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin3 //
+| #ls #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
+qed.
+
+lemma binaryTM_phase0_None_Some :
+ ∀sig,M,t,q,ch,n,qn,chn,mv.
+ O < n → n < 2*FS_crd sig →
+ halt sig M q=false →
+ current ? t = None ? →
+ 〈qn,Some ? chn,mv〉 = trans sig M 〈q,None ?〉 →
+ ∀k.O < k →
+ loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin0,ch,n〉) t)
+ = loopM ? (mk_binaryTM sig M) (k-1)
+ (mk_config ?? (〈q,bin4,None ?,to_initN O ??〉) (tape_move ? t R)). [2,3: /2 by transitive_lt/ ]
+#sig #M #t #q #ch #n #qn #chn #mv #HOn #Hn #Hhalt #Hcur #Htrans #k #Hk
+cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
+cases (le_to_eq … HOn) #n0 #Hn0 destruct (Hn0)
+lapply Htrans lapply Hcur -Hcur -Htrans cases t
+[ >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/
+| #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/
+| #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/
+| #ls #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
+qed.
+
+lemma binaryTM_bin1_O :
+ ∀sig,M,t,q,ch.
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin1,ch,O〉) t)
+ = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t. [2,3:/2 by lt_S_to_lt/]
+#sig #M #t #q #ch %
+qed.
+
+lemma binaryTM_bin1_S :
+ ∀sig,M,t,q,ch,k. S k <S (2*FS_crd sig) →
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin1,ch,S k〉) t)
+ = mk_config ?? (〈q,bin1,ch,to_initN k ??〉) (tape_move ? t L). [2,3:@le_S /2 by lt_S_to_lt/]
+#sig #M #t #q #ch #k #HSk %
+qed.
+
+lemma binaryTM_phase1 :
+ ∀sig,M,q,ls1,ls2,cur,rs,ch.
+ |ls1| = FS_crd sig → (cur = None ? → rs = [ ]) →
+ ∀k.S (FS_crd sig) ≤ k →
+ loopM ? (mk_binaryTM sig M) k
+ (mk_config ?? (〈q,bin1,ch,FS_crd sig〉) (mk_tape ? (ls1@ls2) cur rs))
+ = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
+ (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
+ (mk_tape ? ls2 (option_hd ? (reverse ? ls1@option_cons ? cur rs))
+ (tail ? (reverse ? ls1@option_cons ? cur rs)))). [2,3:/2 by O/]
+cut (∀sig,M,q,ls1,ls2,ch,k,n,cur,rs.
+ |ls1| = n → n<S (2*FS_crd sig) → (cur = None ? → rs = [ ]) →
+ loopM ? (mk_binaryTM sig M) (S n + k)
+ (mk_config ?? (〈q,bin1,ch,n〉) (mk_tape ? (ls1@ls2) cur rs))
+ = loopM ? (mk_binaryTM sig M) k
+ (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
+ (mk_tape ? ls2 (option_hd ? (reverse ? ls1@option_cons ? cur rs))
+ (tail ? (reverse ? ls1@option_cons ? cur rs))))) [1,2:@le_S //]
+[ #sig #M #q #ls1 #ls2 #ch #k elim ls1
+ [ #n normalize in ⊢ (%→?); #cur #rs #Hn <Hn #Hcrd #Hcur >loopM_unfold >loop_S_false [| % ]
+ >binaryTM_bin1_O cases cur in Hcur;
+ [ #H >(H (refl ??)) -H %
+ | #cur' #_ % ]
+ | #l0 #ls0 #IH * [ #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
+ #n #cur #rs normalize in ⊢ (%→?); #H destruct (H) #Hlt #Hcur
+ >loopM_unfold >loop_S_false [|%] >binaryTM_bin1_S
+ <(?:mk_tape ? (ls0@ls2) (Some ? l0) (option_cons ? cur rs) =
+ tape_move FinBool (mk_tape FinBool ((l0::ls0)@ls2) cur rs) L)
+ [| cases cur in Hcur; [ #H >(H ?) // | #cur' #_ % ] ]
+ >(?:loop (config FinBool (states FinBool (mk_binaryTM sig M))) (S (|ls0|)+k)
+ (step FinBool (mk_binaryTM sig M))
+ (λc:config FinBool (states FinBool (mk_binaryTM sig M))
+ .halt FinBool (mk_binaryTM sig M)
+ (cstate FinBool (states FinBool (mk_binaryTM sig M)) c))
+ (mk_config FinBool (states FinBool (mk_binaryTM sig M))
+ 〈q,bin1,ch,to_initN (|ls0|) ?
+ (le_S ?? (lt_S_to_lt (|ls0|) (S (2*FS_crd sig)) Hlt))〉
+ (mk_tape FinBool (ls0@ls2) (Some FinBool l0) (option_cons FinBool cur rs)))
+ = loopM FinBool (mk_binaryTM sig M) k
+ (mk_config FinBool (states FinBool (mk_binaryTM sig M))
+ 〈q,bin2,〈ch,FS_crd sig〉〉
+ (mk_tape FinBool ls2
+ (option_hd FinBool (reverse FinBool ls0@l0::option_cons FinBool cur rs))
+ (tail FinBool (reverse FinBool ls0@l0::option_cons FinBool cur rs)))))
+ [| /2/
+ | >(?: l0::option_cons ? cur rs = option_cons ? (Some ? l0) (option_cons ? cur rs)) [| % ]
+ @trans_eq [|| @(IH ??? (refl ??)) [ /2 by lt_S_to_lt/ | #H destruct (H) ] ]
+ %
+ ]
+ >reverse_cons >associative_append %
+ ]
+| #Hcut #sig #M #q #ls1 #ls2 #cur #rs #ch #Hlen #Hcur #k #Hk
+ cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech @Hcut /2/ ]
+qed.
+
+lemma binaryTM_bin2_O :
+ ∀sig,M,t,q,qn,ch,chn,mv.
+ 〈qn,chn,mv〉 = trans sig M 〈q,ch〉 →
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,O〉) t)
+ = mk_config ?? (〈qn,bin3,ch,to_initN (displ_of_move sig mv) ??〉) t.[2,3:/2 by lt_S_to_lt,le_S_S/]
+#sig #M #t #q #qn #ch #chn #mv #Htrans
+whd in match (step ???); whd in match (trans ???); <Htrans %
+qed.
+
+lemma binaryTM_bin2_S_None :
+ ∀sig,M,t,q,qn,ch,mv,k.
+ k < S (2*FS_crd sig) →
+ 〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 →
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,S k〉) t)
+ = mk_config ?? (〈q,bin2,ch,k〉) (tape_move ? t R).
+[2,3: @le_S_S /2 by lt_to_le/ ]
+#sig #M #t #q #qn #ch #mv #k #Hk #Htrans
+whd in match (step ???); whd in match (trans ???); <Htrans %
+qed.
+
+lemma binaryTM_bin2_S_Some :
+ ∀sig,M,t,q,qn,ch,chn,mv,k.
+ k< S (2*FS_crd sig) →
+ 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,S k〉) t)
+ = mk_config ?? (〈q,bin2,ch,k〉) (tape_move ? (tape_write ? t (Some ? (FS_nth ? k == Some ? chn))) R).
+[2,3: @le_S_S /2 by lt_to_le/ ]
+#sig #M #t #q #qn #ch #chn #mv #k #Hk #Htrans
+whd in match (step ???); whd in match (trans ???); <Htrans %
+qed.
+
+let rec iter (T:Type[0]) f n (t:T) on n ≝
+ match n with [ O ⇒ t | S n0 ⇒ iter T f n0 (f t) ].
+
+lemma binaryTM_phase2_None :∀sig,M,q,ch,qn,mv.
+ 〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 →
+ ∀n.n≤S (2*FS_crd sig) →
+ ∀t,k.S n ≤ k →
+ loopM ? (mk_binaryTM sig M) k
+ (mk_config ?? (〈q,bin2,ch,n〉) t)
+ = loopM ? (mk_binaryTM sig M) (k - S n)
+ (mk_config ?? (〈qn,bin3,ch,to_initN (displ_of_move sig mv) ??〉)
+ (iter ? (λt0.tape_move ? t0 R) n t)). [2,3: @le_S_S /2 by lt_S_to_lt/]
+#sig #M #q #ch #qn #mv #Htrans #n #Hn #t #k #Hk
+cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech lapply Hn lapply t -Hn -t
+elim n
+[ #t #Hle >loopM_unfold >loop_S_false //
+ >(binaryTM_bin2_O … Htrans) //
+| #n0 #IH #t #Hn0 >loopM_unfold >loop_S_false //
+ >(binaryTM_bin2_S_None … Htrans) @(trans_eq ???? (IH …)) //
+]
+qed.
+
+lemma binaryTM_phase2_Some_of : ∀sig,M,q,ch,qn,chn,mv,ls.
+ 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
+ ∀k.S (FS_crd sig) ≤ k →
+ loopM ? (mk_binaryTM sig M) k
+ (mk_config ?? (〈q,bin2,ch,FS_crd sig〉) (mk_tape ? ls (None ?) [ ]))
+ = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
+ (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
+ (mk_tape ? (reverse ? (bin_char sig chn)@ls) (None ?) [ ])). [2,3:@le_S_S //]
+cut (∀sig,M,q,ch,qn,chn,mv,ls,k,n.
+ S n ≤ k → 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
+ ∀csl. n <S (2*FS_crd sig) →
+ |csl| + n = FS_crd sig →
+ (∃fs.bin_char sig chn = reverse ? csl@fs) →
+ loopM ? (mk_binaryTM sig M) k
+ (mk_config ?? (〈q,bin2,ch,n〉) (mk_tape ? (csl@ls) (None ?) [ ]))
+ = loopM ? (mk_binaryTM sig M) (k - S n)
+ (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
+ (mk_tape ? (reverse ? (bin_char sig chn)@ls) (None ?) [ ]))) [1,2:@le_S_S //]
+[ #sig #M #q #ch #qn #chn #mv #ls #k #n #Hk
+ cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
+ #Htrans elim n
+ [ #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // <loopM_unfold
+ cut (fs = [ ])
+ [ cases fs in Hfs; // #f0 #fs0 #H lapply (eq_f ?? (length ?) … H)
+ >length_append >(?:|bin_char sig chn| = FS_crd sig) [|//]
+ <Hcrd >length_reverse #H1 cut (O = |f0::fs0|) [ /2/ ]
+ normalize #H1 destruct (H1) ]
+ #H destruct (H) >append_nil in Hfs; #Hfs
+ >Hfs >reverse_reverse >(binaryTM_bin2_O … Htrans) //
+ | #n0 #IH #csl #Hcount #Hcrd * #fs #Hfs
+ >loopM_unfold >loop_S_false // <loopM_unfold
+ >(?: step FinBool (mk_binaryTM sig M)
+ (mk_config FinBool (states FinBool (mk_binaryTM sig M)) 〈q,bin2,〈ch,S n0〉〉
+ (mk_tape FinBool (csl@ls) (None FinBool) []))
+ = mk_config ?? (〈q,bin2,ch,n0〉)
+ (tape_move ? (tape_write ?
+ (mk_tape ? (csl@ls) (None ?) [ ]) (Some ? (FS_nth ? n0 == Some ? chn))) R))
+ [| /2 by lt_S_to_lt/ | @(binaryTM_bin2_S_Some … Htrans) ]
+ >(?: tape_move ? (tape_write ???) ? =
+ mk_tape ? (((FS_nth ? n0 == Some sig chn)::csl)@ls) (None ?) [ ])
+ [| cases csl // cases ls // ]
+ cases fs in Hfs;
+ [ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ]
+ -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|//]
+ <Hcrd in ⊢ (%→?); >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
+ #Hfalse cut (S n0 = O) /2 by injective_plus_r/ #H destruct (H)
+ | #f0 #fs0 #Hbinchar
+ cut (bin_char ? chn = reverse ? csl@(FS_nth ? n0 == Some ? chn)::fs0)
+ [ >Hbinchar >(bin_char_FS_nth … Hbinchar) >(?:|fs0|=n0) //
+ <(eq_length_bin_char_FS_crd sig chn) in Hcrd; >Hbinchar
+ >length_append >length_reverse whd in ⊢ (???(??%)→?); /2 by injective_S/ ]
+ -Hbinchar #Hbinchar >Hbinchar @(trans_eq ???? (IH …)) //
+ [ %{fs0} >reverse_cons >associative_append @Hbinchar
+ | whd in ⊢ (??%?); <Hcrd // ]
+ @eq_f @eq_f @eq_f3 //
+ ]
+ ]
+| #Hcut #sig #M #q #ch #qn #chn #mv #ls #Htrans #k #Hk
+ @trans_eq
+ [3: @(trans_eq ???? (Hcut ??????? ls ? (FS_crd sig) ? Htrans …)) //
+ [3:@([ ]) | %{(bin_char ? chn)} % | % ]
+ || % ]
+]
+qed.
+
+lemma binaryTM_phase2_Some_ow : ∀sig,M,q,ch,qn,chn,mv,ls,cs,rs.
+ 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
+ |cs| = FS_crd sig →
+ ∀k.S (FS_crd sig) ≤ k →
+ loopM ? (mk_binaryTM sig M) k
+ (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
+ (mk_tape ? ls (option_hd ? (cs@rs)) (tail ? (cs@rs))))
+ = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
+ (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
+ (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs))). [2,3:@le_S_S /2 by O/]
+cut (∀sig,M,q,ch,qn,chn,mv,ls,rs,k,csr.
+ 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
+ ∀csl.|csr|<S (2*FS_crd sig) →
+ |csl@csr| = FS_crd sig →
+ (∃fs.bin_char sig chn = reverse ? csl@fs) →
+ loopM ? (mk_binaryTM sig M) (S (|csr|) + k)
+ (mk_config ?? (〈q,bin2,ch,|csr|〉)
+ (mk_tape ? (csl@ls) (option_hd ? (csr@rs)) (tail ? (csr@rs))))
+ = loopM ? (mk_binaryTM sig M) k
+ (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
+ (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs)))) [1,2: @le_S_S [/2 by lt_to_le/|/2 by le_S/] ]
+[ #sig #M #q #ch #qn #chn #mv #ls #rs #k #csr #Htrans elim csr
+ [ #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // normalize in match (length ? [ ]);
+ >(binaryTM_bin2_O … Htrans) <loopM_unfold @eq_f @eq_f @eq_f3 //
+ cases fs in Hfs; // #f0 #fs0 #H lapply (eq_f ?? (length ?) … H)
+ >length_append >(?:|bin_char sig chn| = FS_crd sig) [|//]
+ <Hcrd >length_reverse >length_append whd in match (|[]|); #H1 cut (O = |f0::fs0|) [ /2 by plus_to_minus/ ]
+ normalize #H1 destruct (H1)
+ | #b0 #bs0 #IH #csl #Hcount #Hcrd * #fs #Hfs
+ >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_Some … Htrans)
+ >(?: tape_move ? (tape_write ???) ? =
+ mk_tape ? (((FS_nth ? (|bs0|)==Some sig chn)::csl)@ls)
+ (option_hd ? (bs0@rs)) (tail ? (bs0@rs)))
+ in match (tape_move ? (tape_write ???) ?);
+ [| cases bs0 // cases rs // ] @IH
+ [ <Hcrd >length_append >length_append normalize //
+ | cases fs in Hfs;
+ [ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ] -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|//]
+ <Hcrd >length_append normalize >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
+ #Hfalse cut (S (|bs0|) = O) /2 by injective_plus_r/ #H destruct (H)
+ | #f0 #fs0 #Hbinchar
+ cut (bin_char ? chn = reverse ? csl@(FS_nth ? (|bs0|) == Some ? chn)::fs0)
+ [ >Hbinchar >(bin_char_FS_nth … Hbinchar) >(?:|fs0|=|bs0|) //
+ <(eq_length_bin_char_FS_crd sig chn) in Hcrd; >Hbinchar
+ >length_append >length_append >length_reverse
+ whd in ⊢ (??(??%)(??%)→?); /2 by injective_S/ ]
+ -Hbinchar #Hbinchar >Hbinchar %{fs0} >reverse_cons >associative_append %
+ ]
+ ]
+ ]
+| #Hcut #sig #M #q #ch #qn #chn #mv #ls #cs #rs #Htrans #Hcrd #k #Hk
+ cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >(?:S (FS_crd sig) +k0-S (FS_crd sig) = k0) [|@minus_tech]
+ @trans_eq
+ [3: @(trans_eq ???? (Hcut ??????? ls ?? cs Htrans [ ] …)) //
+ [ normalize % // | normalize @Hcrd | >Hcrd // ]
+ || @eq_f2 [ >Hcrd % | @eq_f2 // @eq_f cases Hcrd // ] ] ]
+qed.
+
+lemma binaryTM_bin3_O :
+ ∀sig,M,t,q,ch.
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin3,ch,O〉) t)
+ = mk_config ?? (〈q,bin0,None ?,to_initN (FS_crd sig) ??〉) t. [2,3:@le_S //]
+#sig #M #t #q #ch %
+qed.
+
+lemma binaryTM_bin3_S :
+ ∀sig,M,t,q,ch,k. S k ≤ S (2*FS_crd sig) →
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin3,ch,S k〉) t)
+ = mk_config ?? (〈q,bin3,ch,to_initN k ??〉) (tape_move ? t L). [2,3: @le_S_S /2 by lt_to_le/]
+#sig #M #t #q #ch #k #HSk %
+qed.
+
+lemma binaryTM_phase3 :∀sig,M,q,ch,n.
+ n ≤ S (2*FS_crd sig) →
+ ∀t,k.S n ≤ k →
+ loopM ? (mk_binaryTM sig M) k
+ (mk_config ?? (〈q,bin3,ch,n〉) t)
+ = loopM ? (mk_binaryTM sig M) (k - S n)
+ (mk_config ?? (〈q,bin0,None ?,FS_crd sig〉)
+ (iter ? (λt0.tape_move ? t0 L) n t)). [2,3: /2 by lt_S_to_lt, le_to_lt_to_lt/]
+#sig #M #q #ch #n #Hcrd #t #k #Hk
+cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >(minus_tech (S n) k0)
+lapply t lapply Hcrd -t -Hcrd elim n
+[ #Hcrd #t >loopM_unfold >loop_S_false [| % ] >binaryTM_bin3_O //
+| #n0 #IH #Hlt #t >loopM_unfold >loop_S_false [|%] >binaryTM_bin3_S [|@Hlt]
+ <IH [|@lt_to_le @Hlt ]
+ <loopM_unfold % ]
+qed.
+
+lemma binaryTM_bin4_None :
+ ∀sig,M,t,q,ch.
+ current ? t = None ? →
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
+ = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t. [|@le_S_S @le_O_n | @le_S_S // ]
+#sig #M #t #q #ch #Hcur whd in ⊢ (??%?); >Hcur %
+qed.
+
+lemma binaryTM_phase4_write : ∀sig,M,q,ch,t.current ? t = None ? →
+ ∀k.O < k →
+ loopM ? (mk_binaryTM sig M) k
+ (mk_config ?? (〈q,bin4,ch,O〉) t)
+ = loopM ? (mk_binaryTM sig M) (k-1)
+ (mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t). [|@le_S_S @le_O_n|@le_S_S //]
+#sig #M #q #ch #t #Hcur #k #Hk
+cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
+>loopM_unfold >loop_S_false // <loopM_unfold >binaryTM_bin4_None [|//] %
+qed.
+
+(* we don't get here any more! *
+lemma binaryTM_bin4_noextend :
+ ∀sig,M,t,q,ch,cur,qn,mv.
+ current ? t = Some ? cur →
+ 〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 →
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
+ = mk_config ?? (〈q,bin2,ch,to_initN O ??〉) t. [2,3://]
+#sig #M #t #q #ch #cur #qn #mv #Hcur #Htrans
+whd in ⊢ (??%?); >Hcur whd in ⊢ (??%?);
+whd in match (trans FinBool ??); <Htrans %
+qed.
+*)
+
+lemma binaryTM_bin4_extend :
+ ∀sig,M,t,q,ch,cur,qn,an,mv.
+ current ? t = Some ? cur →
+ 〈qn,Some ? an,mv〉 = trans sig M 〈q,ch〉 →
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
+ = mk_config ?? (〈q,bin5,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t L). [2,3:@le_S //]
+#sig #M #t #q #ch #cur #qn #an #mv #Hcur #Htrans
+whd in ⊢ (??%?); >Hcur whd in ⊢ (??%?);
+whd in match (trans FinBool ??); <Htrans %
+qed.
+
+lemma binaryTM_phase4_extend : ∀sig,M,q,ch,t,cur,qn,an,mv.
+ current ? t = Some ? cur → 〈qn,Some ? an,mv〉 = trans sig M 〈q,ch〉 →
+ ∀k.O < k →
+ loopM ? (mk_binaryTM sig M) k
+ (mk_config ?? (〈q,bin4,ch,O〉) t)
+ = loopM ? (mk_binaryTM sig M) (k-1)
+ (mk_config ?? (〈q,bin5,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t L)). [2,3: @le_S //]
+#sig #M #q #ch #t #cur #qn #an #mv #Hcur #Htrans #k #Hk
+cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
+>loopM_unfold >loop_S_false // <loopM_unfold >(binaryTM_bin4_extend … Hcur) [|*://] %
+qed.
+
+lemma binaryTM_bin5_O :
+ ∀sig,M,t,q,ch.
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin5,ch,O〉) t)
+ = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t R). [2,3:@le_S //]
+#sig #M #t #q #ch %
+qed.
+
+lemma binaryTM_bin5_S :
+ ∀sig,M,t,q,ch,k. S k <S (2*FS_crd sig) →
+ step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin5,ch,S k〉) t)
+ = mk_config ?? (〈q,bin5,ch,to_initN k ??〉) (tape_move ? (tape_write ? t (Some ? false)) L). [2,3:@le_S /2 by lt_S_to_lt/]
+#sig #M #t #q #ch #k #HSk %
+qed.
+
+(* extends the tape towards the left with an unimportant sequence that will be
+ immediately overwritten *)
+lemma binaryTM_phase5 :∀sig,M,q,ch,n.
+ ∀rs.n<S (2*FS_crd sig) →
+ ∃bs.|bs| = n ∧
+ ∀k.S n ≤ k →
+ loopM ? (mk_binaryTM sig M) k
+ (mk_config ?? (〈q,bin5,ch,n〉) (mk_tape ? [] (None ?) rs))
+ = loopM ? (mk_binaryTM sig M) (k - S n)
+ (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
+ (mk_tape ? [] (option_hd ? (bs@rs)) (tail ? (bs@rs)))). [2,3:@le_S //]
+#sig #M #q #ch #n elim n
+[ #rs #Hlt %{[]} % // #k #Hk cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech -Hk0
+ cases rs //
+| #n0 #IH #rs #Hn0 cases (IH (false::rs) ?) [|/2 by lt_S_to_lt/]
+ #bs * #Hbs -IH #IH %{(bs@[false])} % [ <Hbs >length_append /2 by increasing_to_injective/ ]
+ #k #Hk cases (le_to_eq … Hk) #k0 #Hk0 >Hk0
+ >loopM_unfold >loop_S_false // >binaryTM_bin5_S
+ >associative_append normalize in match ([false]@?); <(IH (S n0 + k0)) [|//]
+ >loopM_unfold @eq_f @eq_f cases rs //
+]
+qed.
+
+lemma current_None_or_midtape :
+ ∀sig,t.current sig t = None sig ∨ ∃ls,c,rs.t = midtape sig ls c rs.
+#sig * normalize /2/ #ls #c #rs %2 /4 by ex_intro/
+qed.
+
+lemma state_bin_lift_unfold :
+ ∀sig.∀M:TM sig.∀q:states sig M.
+ state_bin_lift sig M q = 〈q,bin0,None ?,FS_crd sig〉.// qed.
+
+axiom current_tape_bin_list :
+ ∀sig,t.current sig t = None ? → current ? (tape_bin_lift sig t) = None ?.
+
+lemma tape_bin_lift_unfold :
+ ∀sig,t. tape_bin_lift sig t =
+ mk_tape ? (rev_bin_list ? (left ? t)) (option_hd ? (opt_bin_char sig (current ? t)))
+ (tail ? (opt_bin_char sig (current ? t))@bin_list ? (right ? t)). //
+qed.
+
+lemma reverse_bin_char_list : ∀sig,c,l.
+ reverse ? (bin_char sig c)@rev_bin_list ? l = rev_bin_list ? (c::l). // qed.
+
+lemma left_midtape : ∀sig,ls,c,rs.left ? (midtape sig ls c rs) = ls.// qed.
+lemma current_midtape : ∀sig,ls,c,rs.current ? (midtape sig ls c rs) = Some ? c.// qed.
+lemma right_midtape : ∀sig,ls,c,rs.right ? (midtape sig ls c rs) = rs.// qed.
+lemma opt_bin_char_Some : ∀sig,c.opt_bin_char sig (Some ? c) = bin_char ? c.// qed.
+
+lemma opt_cons_hd_tl : ∀A,l.option_cons A (option_hd ? l) (tail ? l) = l.
+#A * // qed.
+
+lemma le_tech : ∀a,b,c.a ≤ b → a * c ≤ b * c.
+#a #b #c #H /2 by monotonic_le_times_r/
+qed.
+
+lemma iter_split : ∀T,f,m,n,x.
+ iter T f (m+n) x = iter T f m (iter T f n x).
+#T #f #m #n elim n /2/
+#n0 #IH #x <plus_n_Sm whd in ⊢ (??%(????%)); >IH %
+qed.
+
+lemma iter_O : ∀T,f,x.iter T f O x = x.// qed.
+
+lemma iter_tape_move_R : ∀T,n,ls,cs,rs.|cs| = n →
+ iter ? (λt0.tape_move T t0 R) n (mk_tape ? ls (option_hd ? (cs@rs)) (tail ? (cs@rs)))
+ = mk_tape ? (reverse ? cs@ls) (option_hd ? rs) (tail ? rs).
+#T #n elim n
+[ #ls * [| #c0 #cs0 #rs #H normalize in H; destruct (H) ] #rs #_ %
+| #n0 #IH #ls * [ #rs #H normalize in H; destruct (H) ] #c #cs #rs #Hlen
+ whd in ⊢ (??%?);
+ >(?: (tape_move T (mk_tape T ls (option_hd T ((c::cs)@rs)) (tail T ((c::cs)@rs))) R)
+ = mk_tape ? (c::ls) (option_hd ? (cs@rs)) (tail ? (cs@rs))) in ⊢ (??(????%)?);
+ [| cases cs // cases rs // ] >IH
+ [ >reverse_cons >associative_append %
+ | normalize in Hlen; destruct (Hlen) % ]
+]
+qed.
+
+lemma tail_tech : ∀T,l1,l2.O < |l1| → tail T (l1@l2) = tail ? l1@l2.
+#T * normalize // #l2 #Hfalse @False_ind cases (not_le_Sn_O O) /2/
+qed.
+
+lemma hd_tech : ∀T,l1,l2.O < |l1| → option_hd T (l1@l2) = option_hd ? l1.
+#T * normalize // #l2 #Hfalse @False_ind cases (not_le_Sn_O O) /2/
+qed.
+
+lemma iter_tape_move_L_nil : ∀T,n,rs.
+ iter ? (λt0.tape_move T t0 L) n (mk_tape ? [ ] (None ?) rs) =
+ mk_tape ? [ ] (None ?) rs.
+#T #n #rs elim n // #n0 #IH <IH in ⊢ (???%); cases rs //
+qed.
+
+lemma iter_tape_move_R_nil : ∀T,n,ls.
+ iter ? (λt0.tape_move T t0 R) n (mk_tape ? ls (None ?) [ ]) =
+ mk_tape ? ls (None ?) [ ].
+#T #n #ls elim n // #n0 #IH <IH in ⊢ (???%); cases ls //
+qed.
+
+lemma iter_tape_move_L_left : ∀T,n,cs,rs. O < n →
+ iter ? (λt0.tape_move T t0 L) n
+ (mk_tape ? [ ] (option_hd ? cs) (tail ? cs@rs)) =
+ mk_tape ? [ ] (None ?) (cs@rs).
+#T #n #cs #rs *
+[ cases cs // cases rs //
+| #m #_ whd in ⊢ (??%?); <(iter_tape_move_L_nil ? m) cases cs // cases rs // ]
+qed.
+
+lemma iter_tape_move_L : ∀T,n,ls,cs,rs.|cs| = n →
+ iter ? (λt0.tape_move T t0 L) n (mk_tape ? (reverse ? cs@ls) (option_hd ? rs) (tail ? rs))
+ = mk_tape ? ls (option_hd ? (cs@rs)) (tail ? (cs@rs)).
+#T #n elim n
+[ #ls * [| #c0 #cs0 #rs #H normalize in H; destruct (H) ] #rs #_ %
+| #n0 #IH #ls #cs #rs @(list_elim_left … cs)
+ [ #H normalize in H; destruct (H) ] -cs
+ #c #cs #_ #Hlen >reverse_append whd in ⊢ (??%?);
+ >(?: tape_move T (mk_tape T ((reverse T [c]@reverse T cs)@ls) (option_hd T rs) (tail T rs)) L
+ = mk_tape ? (reverse T cs@ls) (option_hd ? (c::rs)) (tail ? (c::rs))) in ⊢ (??(????%)?);
+ [| cases rs // ] >IH
+ [ >associative_append %
+ | >length_append in Hlen; normalize // ]
+]
+qed.
+
+lemma tape_move_niltape :
+ ∀sig,mv.tape_move sig (niltape ?) mv = niltape ?. #sig * // qed.
+
+lemma iter_tape_move_niltape :
+ ∀sig,mv,n.iter … (λt.tape_move sig t mv) n (niltape ?) = niltape ?.
+#sig #mv #n elim n // -n #n #IH whd in ⊢ (??%?); >tape_move_niltape //
+qed.
+
+lemma tape_move_R_left :
+ ∀sig,rs.tape_move sig (mk_tape ? [ ] (None ?) rs) R =
+ mk_tape ? [ ] (option_hd ? rs) (tail ? rs). #sig * //
+qed.