X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2FbinaryTM.ma;h=50c8d5851b82cb8b87e9b0461e9e4a1e52ce7b78;hb=1e74e10d6d177c8afe14f20f050812f68aa2b530;hp=b430afa4e60bd0c6f217bfd84af1f281bc666acd;hpb=57103fa96f504f9bffca859dd60317162396657f;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/binaryTM.ma b/matita/matita/lib/turing/multi_universal/binaryTM.ma
index b430afa4e..50c8d5851 100644
--- a/matita/matita/lib/turing/multi_universal/binaryTM.ma
+++ b/matita/matita/lib/turing/multi_universal/binaryTM.ma
@@ -193,51 +193,510 @@ qed.
 axiom binary_to_bin_char :∀sig,csl,csr,a.
   csl@true::csr=bin_char sig a → FS_nth ? (length ? csr) = Some ? a.
 
-lemma binaryTM_phase1_midtape_aux :
+lemma binaryTM_phase0_midtape_aux :
   ∀sig,M,q,ls,a,rs,k.
   halt sig M q=false → 
   ∀csr,csl,t,ch.length ? csr < S (2*FS_crd sig) → 
   t = mk_tape ? (reverse ? csl@ls) (option_hd ? (csr@rs)) (tail ? (csr@rs)) → 
   csl@csr = bin_char sig a → 
+  |csl@csr| = FS_crd sig → 
+  (index_of_FS ? a < |csl| → ch = Some ? a) → 
   loopM ? (mk_binaryTM sig M) (S (length ? csr) + k)
     (mk_config ?? (〈q,bin0,ch,length ? csr〉) t) 
   = loopM ? (mk_binaryTM sig M) k 
       (mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉) 
-        (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [2,3://]
+        (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [2,3:/2 by O/]
 #sig #M #q #ls #a #rs #k #Hhalt #csr elim csr
-[ #csl #t #ch #Hlen #Ht >append_nil #Hcsl >loopM_unfold >loop_S_false [|normalize //]
+[ #csl #t #ch #Hlen #Ht >append_nil #Hcsl #Hlencsl #Hch >loopM_unfold >loop_S_false [|normalize //]
+  >Hch [| >Hlencsl (* lemmatize *) @daemon]
   <loopM_unfold @eq_f >binaryTM_bin0_bin1 @eq_f >Ht 
   whd in match (step ???); whd in match (trans ???); <Hcsl %
 | #c cases c
-  [ #csr0 #IH #csl #t #ch #Hlen #Ht #Heq >loopM_unfold >loop_S_false [|normalize //]
+  [ #csr0 #IH #csl #t #ch #Hlen #Ht #Heq #Hcrd #Hch >loopM_unfold >loop_S_false [|normalize //]
     <loopM_unfold lapply (binary_to_bin_char … Heq) #Ha >binaryTM_bin0_true 
     [| >Ht % ]
-    lapply (IH (csl@[true]) (tape_move FinBool t R) ????)
+    lapply (IH (csl@[true]) (tape_move FinBool t R) ??????)
     [ //
+    | >associative_append @Hcrd
+    | >associative_append @Heq
     | >Ht whd in match (option_hd ??) in ⊢ (??%?); whd in match (tail ??) in ⊢ (??%?);
       cases csr0
       [ cases rs
         [ normalize >rev_append_def >rev_append_def >reverse_append %
         | #r1 #rs1 normalize >rev_append_def >rev_append_def >reverse_append % ]
       | #c1 #csr1 normalize >rev_append_def >rev_append_def >reverse_append % ]
-    | /2/
-    | @(Some ? a) ]
-    #H whd in match (plus ??); >Ha >H @eq_f @eq_f2 //
-    
+    | /2 by lt_S_to_lt/
+    |]
+    #H whd in match (plus ??); >H @eq_f @eq_f2 %
+  | #csr0 #IH #csl #t #ch #Hlen #Ht #Heq #Hcrd #Hch >loopM_unfold >loop_S_false [|normalize //]
+    <loopM_unfold >binaryTM_bin0_false [| >Ht % ]
+    lapply (IH (csl@[false]) (tape_move FinBool t R) ??????)
+    [6: @ch
+    | (* by cases: if index < |csl|, then Hch, else False *)
+       @daemon
+    | >associative_append @Hcrd
+    | >associative_append @Heq
+    | >Ht whd in match (option_hd ??) in ⊢ (??%?); whd in match (tail ??) in ⊢ (??%?);
+      cases csr0
+      [ cases rs
+        [ normalize >rev_append_def >rev_append_def >reverse_append %
+        | #r1 #rs1 normalize >rev_append_def >rev_append_def >reverse_append % ]
+      | #c1 #csr1 normalize >rev_append_def >rev_append_def >reverse_append % ]
+    | /2 by lt_S_to_lt/
+    |]
+    #H whd in match (plus ??); >H @eq_f @eq_f2 %
+  ]
+]
 qed.
 
-
-lemma binaryTM_phase1_midtape :
-  ∀sig,M,t,q,ls,a,rs,ch.
+lemma binaryTM_phase0_midtape :
+  ∀sig,M,t,q,ls,a,rs,ch,k.
+  halt sig M q=false → 
   t = mk_tape ? ls (option_hd ? (bin_char ? a)) (tail ? (bin_char sig a@rs)) →
-  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,FS_crd sig〉) t) 
-  = mk_config ?? (〈q,bin1,ch,to_initN (FS_crd sig) ??〉) 
-      (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs)). [2,3://]
-#sig #M #t #q #ls #a #rs #ch #Ht
-whd in match (step ???); whd in match (trans ???);
->Hcur %
+  loopM ? (mk_binaryTM sig M) (S (length ? (bin_char ? a)) + k)
+    (mk_config ?? (〈q,bin0,ch,length ? (bin_char ? a)〉) t) 
+  = loopM ? (mk_binaryTM sig M) k 
+      (mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉) 
+        (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [|@daemon|//]
+#sig #M #t #q #ls #a #rs #ch #k #Hhalt #Ht
+cut (∃c,cl.bin_char sig a = c::cl) [@daemon] * #c * #cl #Ha >Ha
+>(binaryTM_phase0_midtape_aux ? M q ls a rs ? ? (c::cl) [ ] t ch) //
+[| normalize #Hfalse @False_ind cases (not_le_Sn_O ?) /2/
+| <Ha (* |bin_char sig ?| = FS_crd sig *) @daemon
+| >Ha %
+| >Ht >Ha % ]
+<Ha %
+qed.
+
+lemma binaryTM_phase0_None :
+  ∀sig,M,t,q,ch,k,n.
+  n < 2*FS_crd sig → 
+  halt sig M q=false → 
+  current ? t = None ? →
+  loopM ? (mk_binaryTM sig M) (S k) (mk_config ?? (〈q,bin0,ch,S n〉) t) 
+  = loopM ? (mk_binaryTM sig M) k 
+      (mk_config ?? (〈q,bin4,None ?,to_initN O ??〉) (tape_move ? t R)). [2,3: /2 by le_to_lt_to_lt/ ]  
+#sig #M #t #q #ch #k #n #Hn #Hhalt cases t
+[ >loopM_unfold >loop_S_false [|@Hhalt] //
+| #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] //
+| #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] //
+| #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://]
+#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:/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,k.
+  |ls1| = FS_crd sig → (cur = None ? → rs = [ ]) → 
+  loopM ? (mk_binaryTM sig M) (S (FS_crd sig) + k)
+    (mk_config ?? (〈q,bin1,ch,FS_crd sig〉) (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)))). [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://]
+[ #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|) (S (2*FS_crd sig))
+        (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 #k #Hlen @Hcut // ]
+qed.
+
+lemma binaryTM_bin2_O_L :
+  ∀sig,M,t,q,qn,ch,chn.
+  〈qn,chn,L〉 = trans sig M 〈q,ch〉 → 
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,O〉) t)
+  = mk_config ?? (〈qn,bin3,ch,to_initN (2*(FS_crd sig)) ??〉) (tape_move ? t L).[2,3:/2 by lt_S_to_lt/]
+#sig #M #t #q #qn #ch #chn #Htrans
+whd in match (step ???); whd in match (trans ???); <Htrans %
+qed.
+
+lemma binaryTM_bin2_O_R :
+  ∀sig,M,t,q,qn,ch,chn.
+  〈qn,chn,R〉 = trans sig M 〈q,ch〉 → 
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,O〉) t)
+  = mk_config ?? (〈qn,bin3,ch,to_initN O ??〉) t.[2,3://]
+#sig #M #t #q #qn #ch #chn #Htrans
+whd in match (step ???); whd in match (trans ???); <Htrans %
+qed.
+
+lemma binaryTM_bin2_O_N :
+  ∀sig,M,t,q,qn,ch,chn.
+  〈qn,chn,N〉 = trans sig M 〈q,ch〉 → 
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,O〉) t)
+  = mk_config ?? (〈qn,bin3,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t L).[2,3:/2 by lt_S_to_lt/]
+#sig #M #t #q #qn #ch #chn #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< 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:/2 by le_to_lt_to_lt, transitive_lt/]
+#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< 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:/2 by le_to_lt_to_lt, transitive_lt/]
+#sig #M #t #q #qn #ch #chn #mv #k #Hk #Htrans
+whd in match (step ???); whd in match (trans ???); <Htrans %
+qed.
+
+lemma binaryTM_phase2_Some_R :∀sig,M,q,ch,qn,chn,ls,rs,k,csr.
+  〈qn,Some ? chn,R〉 = trans sig M 〈q,ch〉 → 
+  ∀cur,csl. |cur::csr|<S (2*FS_crd sig) → 
+  |csl@cur::csr| = FS_crd sig →
+  (∃fs.bin_char sig chn = reverse ? csl@fs) → 
+  loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
+    (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs))) 
+  = loopM ? (mk_binaryTM sig M) k 
+      (mk_config ?? (〈qn,bin3,ch,O〉) 
+        (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs))). [2,3://]
+#sig #M #q #ch #qn #chn #ls #rs #k #csr #Htrans elim csr
+[ #cur #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
+  >(binaryTM_bin2_S_Some … Htrans) [| /2 by monotonic_pred/ ]
+  >loop_S_false // @eq_f >(binaryTM_bin2_O_R … Htrans)
+  @eq_f change with (midtape ? (csl@ls) (FS_nth sig O == Some ? chn) rs) in match (tape_write ???);
+  cut (bin_char sig chn = reverse ? csl@[FS_nth sig O == Some sig chn]) [@daemon] #Hfs' >Hfs'
+  >reverse_append >reverse_single >reverse_reverse >associative_append
+  cases rs //
+| #b0 #bs0 #IH #cur #csl #Hcount #Hcrd * #fs #Hfs
+  >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_Some … Htrans) [| @le_S_S_to_le @Hcount ]
+  change with (midtape ? (((FS_nth ? (|b0::bs0|)==Some sig chn)::csl)@ls) b0 (bs0@rs)) 
+    in match (tape_move ? (tape_write ???) ?); @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) [|@daemon]
+      <Hcrd >length_append normalize >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
+      #Hfalse cut (S (S (|bs0|)) = O) /2 by injective_plus_r/ #H destruct (H)
+    | #f0 #fs0 #Hbinchar 
+      cut (bin_char ? chn = reverse ? csl@(FS_nth ? (|b0::bs0|) == Some ? chn)::fs0) [@daemon]
+      -Hbinchar #Hbinchar >Hbinchar %{fs0} >reverse_cons >associative_append %
+    ]
+  ]
+]
 qed.
 
+lemma binaryTM_phase2_Some_L :∀sig,M,q,ch,qn,chn,ls,rs,k,csr.
+  〈qn,Some ? chn,L〉 = trans sig M 〈q,ch〉 → 
+  ∀cur,csl. |cur::csr|<S (2*FS_crd sig) → 
+  |csl@cur::csr| = FS_crd sig →
+  (∃fs.bin_char sig chn = reverse ? csl@fs) → 
+  loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
+    (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs))) 
+  = loopM ? (mk_binaryTM sig M) k 
+      (mk_config ?? (〈qn,bin3,ch,to_initN (2*FS_crd sig) ??〉) 
+        (tape_move ? (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs)) L)). [2,3://]
+#sig #M #q #ch #qn #chn #ls #rs #k #csr #Htrans elim csr
+[ #cur #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
+  >(binaryTM_bin2_S_Some … Htrans) [| /2 by monotonic_pred/ ]
+  >loop_S_false // @eq_f >(binaryTM_bin2_O_L … Htrans)
+  @eq_f change with (midtape ? (csl@ls) (FS_nth sig O == Some ? chn) rs) in match (tape_write ???);
+  cut (bin_char sig chn = reverse ? csl@[FS_nth sig O == Some sig chn]) [@daemon] #Hfs' >Hfs'
+  >reverse_append >reverse_single >reverse_reverse >associative_append @eq_f2 //
+  cases rs //
+| #b0 #bs0 #IH #cur #csl #Hcount #Hcrd * #fs #Hfs
+  >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_Some … Htrans) [| @le_S_S_to_le @Hcount ]
+  change with (midtape ? (((FS_nth ? (|b0::bs0|)==Some sig chn)::csl)@ls) b0 (bs0@rs)) 
+    in match (tape_move ? (tape_write ???) ?); @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) [|@daemon]
+      <Hcrd >length_append normalize >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
+      #Hfalse cut (S (S (|bs0|)) = O) /2 by injective_plus_r/ #H destruct (H)
+    | #f0 #fs0 #Hbinchar 
+      cut (bin_char ? chn = reverse ? csl@(FS_nth ? (|b0::bs0|) == Some ? chn)::fs0) [@daemon]
+      -Hbinchar #Hbinchar >Hbinchar %{fs0} >reverse_cons >associative_append %
+    ]
+  ]
+]
+qed.
+
+lemma binaryTM_phase2_Some_N :∀sig,M,q,ch,qn,chn,ls,rs,k,csr.
+  〈qn,Some ? chn,N〉 = trans sig M 〈q,ch〉 → 
+  ∀cur,csl. |cur::csr|<S (2*FS_crd sig) → 
+  |csl@cur::csr| = FS_crd sig →
+  (∃fs.bin_char sig chn = reverse ? csl@fs) → 
+  loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
+    (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs))) 
+  = loopM ? (mk_binaryTM sig M) k 
+      (mk_config ?? (〈qn,bin3,ch,to_initN (FS_crd sig) ??〉) 
+        (tape_move ? (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs)) L)). [2,3://]
+#sig #M #q #ch #qn #chn #ls #rs #k #csr #Htrans elim csr
+[ #cur #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
+  >(binaryTM_bin2_S_Some … Htrans) [| /2 by monotonic_pred/ ]
+  >loop_S_false // @eq_f >(binaryTM_bin2_O_N … Htrans)
+  @eq_f change with (midtape ? (csl@ls) (FS_nth sig O == Some ? chn) rs) in match (tape_write ???);
+  cut (bin_char sig chn = reverse ? csl@[FS_nth sig O == Some sig chn]) [@daemon] #Hfs' >Hfs'
+  >reverse_append >reverse_single >reverse_reverse >associative_append @eq_f2 //
+  cases rs //
+| #b0 #bs0 #IH #cur #csl #Hcount #Hcrd * #fs #Hfs
+  >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_Some … Htrans) [| @le_S_S_to_le @Hcount ]
+  change with (midtape ? (((FS_nth ? (|b0::bs0|)==Some sig chn)::csl)@ls) b0 (bs0@rs)) 
+    in match (tape_move ? (tape_write ???) ?); @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) [|@daemon]
+      <Hcrd >length_append normalize >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
+      #Hfalse cut (S (S (|bs0|)) = O) /2 by injective_plus_r/ #H destruct (H)
+    | #f0 #fs0 #Hbinchar 
+      cut (bin_char ? chn = reverse ? csl@(FS_nth ? (|b0::bs0|) == Some ? chn)::fs0) [@daemon]
+      -Hbinchar #Hbinchar >Hbinchar %{fs0} >reverse_cons >associative_append %
+    ]
+  ]
+]
+qed.
+
+lemma binaryTM_phase2_None_R :∀sig,M,q,ch,qn,ls,rs,k,csr.
+  〈qn,None ?,R〉 = trans sig M 〈q,ch〉 → 
+  ∀cur,csl. |cur::csr|<S (2*FS_crd sig) → 
+  |csl@cur::csr| = FS_crd sig →
+  loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
+    (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs))) 
+  = loopM ? (mk_binaryTM sig M) k 
+      (mk_config ?? (〈qn,bin3,ch,O〉) 
+        (mk_tape ? (reverse ? csr@cur::csl@ls) (option_hd ? rs) (tail ? rs))). [2,3://]
+#sig #M #q #ch #qn #ls #rs #k #csr #Htrans elim csr
+[ #cur #csl #Hcount #Hcrd >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
+  >(binaryTM_bin2_S_None … Htrans) [| /2 by monotonic_pred/ ]
+  >loop_S_false // @eq_f >(binaryTM_bin2_O_R … Htrans)
+  @eq_f cases rs //
+| #b0 #bs0 #IH #cur #csl #Hcount #Hcrd
+  >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_None … Htrans) [| @le_S_S_to_le @Hcount ]
+  change with (midtape ? ((cur::csl)@ls) b0 (bs0@rs)) 
+    in match (tape_move ???); >reverse_cons >associative_append 
+    normalize in match ([b0]@cur::csl@ls); @IH 
+  <Hcrd >length_append >length_append normalize //
+]
+qed.
+
+lemma binaryTM_phase2_None_L : ∀sig,M,q,ch,qn,ls,rs,k,csr.
+  〈qn,None ?,L〉 = trans sig M 〈q,ch〉 → 
+  ∀cur,csl. |cur::csr|<S (2*FS_crd sig) → 
+  |csl@cur::csr| = FS_crd sig →
+  loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
+    (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs))) 
+  = loopM ? (mk_binaryTM sig M) k 
+      (mk_config ?? (〈qn,bin3,ch,to_initN (2*FS_crd sig) ??〉) 
+        (tape_move ? (mk_tape ? (reverse ? csr@cur::csl@ls) (option_hd ? rs) (tail ? rs)) L)). [2,3://]
+#sig #M #q #ch #qn #ls #rs #k #csr #Htrans elim csr
+[ #cur #csl #Hcount #Hcrd >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
+  >(binaryTM_bin2_S_None … Htrans) [| /2 by monotonic_pred/ ]
+  >loop_S_false // @eq_f >(binaryTM_bin2_O_L … Htrans)
+  @eq_f cases rs //
+| #b0 #bs0 #IH #cur #csl #Hcount #Hcrd
+  >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_None … Htrans) [| @le_S_S_to_le @Hcount ]
+  change with (midtape ? ((cur::csl)@ls) b0 (bs0@rs)) 
+    in match (tape_move ???); >reverse_cons >associative_append 
+    normalize in match ([b0]@cur::csl@ls); @IH 
+  <Hcrd >length_append >length_append normalize //
+]
+qed.
+
+lemma binaryTM_phase2_None_N :∀sig,M,q,ch,qn,ls,rs,k,csr.
+  〈qn,None ?,N〉 = trans sig M 〈q,ch〉 → 
+  ∀cur,csl. |cur::csr|<S (2*FS_crd sig) → 
+  |csl@cur::csr| = FS_crd sig →
+  loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
+    (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs))) 
+  = loopM ? (mk_binaryTM sig M) k 
+      (mk_config ?? (〈qn,bin3,ch,to_initN (FS_crd sig) ??〉) 
+        (tape_move ? (mk_tape ? (reverse ? csr@cur::csl@ls) (option_hd ? rs) (tail ? rs)) L)). [2,3://]
+#sig #M #q #ch #qn #ls #rs #k #csr #Htrans elim csr
+[ #cur #csl #Hcount #Hcrd >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
+  >(binaryTM_bin2_S_None … Htrans) [| /2 by monotonic_pred/ ]
+  >loop_S_false // @eq_f >(binaryTM_bin2_O_N … Htrans)
+  @eq_f cases rs //
+| #b0 #bs0 #IH #cur #csl #Hcount #Hcrd
+  >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_None … Htrans) [| @le_S_S_to_le @Hcount ]
+  change with (midtape ? ((cur::csl)@ls) b0 (bs0@rs)) 
+    in match (tape_move ???); >reverse_cons >associative_append 
+    normalize in match ([b0]@cur::csl@ls); @IH 
+  <Hcrd >length_append >length_append normalize //
+]
+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://]
+#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:/2 by lt_S_to_lt/]
+#sig #M #t #q #ch #k #HSk %
+qed.
+
+lemma binaryTM_phase3 :∀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,bin3,ch,n〉) (mk_tape ? (ls1@ls2) cur rs)) 
+  = loopM ? (mk_binaryTM sig M) k 
+      (mk_config ?? (〈q,bin0,None ?,FS_crd sig〉) 
+        (mk_tape ? ls2 (option_hd ? (reverse ? ls1@option_cons ? cur rs)) 
+          (tail ? (reverse ? ls1@option_cons ? cur rs)))). [2,3://]
+#sig #M #q #ls1 #ls2 #ch #k elim ls1
+[ #n normalize in ⊢ (%→?); #cur #rs #Hn <Hn #Hcrd #Hcur >loopM_unfold >loop_S_false [| % ]
+  >binaryTM_bin3_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_bin3_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,bin3,ch,to_initN (|ls0|) (S (2*FS_crd sig))
+      (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,bin0,〈None ?,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 %
+]
+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. [2,3://]
+#sig #M #t #q #ch #Hcur whd in ⊢ (??%?); >Hcur %
+qed.
+
+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://]
+#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_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) ??〉) t. [2,3://]
+#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:/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,k,n,rs.
+  n<S (2*FS_crd sig) →
+  ∃bs.|bs| = n ∧
+  loopM ? (mk_binaryTM sig M) (S n + k)
+    (mk_config ?? (〈q,bin5,ch,n〉) (mk_tape ? [] (None ?) rs)) 
+  = loopM ? (mk_binaryTM sig M) k 
+      (mk_config ?? (〈q,bin2,ch,FS_crd sig〉) 
+        (mk_tape ? [] (None ?) (bs@rs))). [2,3://]
+#sig #M #q #ch #k #n elim n
+[ #rs #Hlt %{[]} % %
+| #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 plus_to_minus/ ]
+  >loopM_unfold >loop_S_false // >binaryTM_bin5_S
+  >associative_append normalize in match ([false]@?); <IH
+  >loopM_unfold @eq_f @eq_f cases rs //
+]
+qed.
 
 lemma binaryTM_loop :
  ∀sig,M,i,t,q,tf,qf.