X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2FbinaryTM.ma;h=c06b69c0e846247826fcdffbcdf7f234c6dc0548;hb=31790e8f6fa051f710f41e4c17d67701874ba331;hp=75cd9f49cb14e7e72c4c71b760182d261ec9ae6b;hpb=4aa431513ffa0ce0accf81e6e9ea4b9314d468e3;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/binaryTM.ma b/matita/matita/lib/turing/multi_universal/binaryTM.ma
index 75cd9f49c..c06b69c0e 100644
--- a/matita/matita/lib/turing/multi_universal/binaryTM.ma
+++ b/matita/matita/lib/turing/multi_universal/binaryTM.ma
@@ -24,26 +24,30 @@ axiom FS_nth : ∀F:FinSet.nat → option F.
 axiom index_of_FS : ∀F:FinSet.F → nat.
 
 (* unary bit representation (with a given length) of a certain number *)
-axiom unary_of_nat : nat → nat → nat.
+axiom unary_of_nat : nat → nat → (list bool).
 
 axiom FinVector : Type[0] → nat → FinSet.
 
-definition binary_base_states ≝ initN 7.
+definition binary_base_states ≝ initN 6.
 
-definition bin0 : binary_base_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 7 (refl …)).
-definition bin1 : binary_base_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 7 (refl …)).
-definition bin2 : binary_base_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 7 (refl …)).
-definition bin3 : binary_base_states ≝ mk_Sig ?? 3 (leb_true_to_le 4 7 (refl …)).
-definition bin4 : binary_base_states ≝ mk_Sig ?? 4 (leb_true_to_le 5 7 (refl …)).
-definition bin5 : binary_base_states ≝ mk_Sig ?? 5 (leb_true_to_le 6 7 (refl …)).
-definition bin6 : binary_base_states ≝ mk_Sig ?? 6 (leb_true_to_le 7 7 (refl …)).
+definition bin0 : binary_base_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 6 (refl …)).
+definition bin1 : binary_base_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 6 (refl …)).
+definition bin2 : binary_base_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 6 (refl …)).
+definition bin3 : binary_base_states ≝ mk_Sig ?? 3 (leb_true_to_le 4 6 (refl …)).
+definition bin4 : binary_base_states ≝ mk_Sig ?? 4 (leb_true_to_le 5 6 (refl …)).
+definition bin5 : binary_base_states ≝ mk_Sig ?? 5 (leb_true_to_le 6 6 (refl …)).
 
 definition states_binaryTM : FinSet → FinSet → FinSet ≝ λsig,states.
  FinProd (FinProd states binary_base_states) 
-         (FinProd (FinOption sig) (initN (2 * (FS_crd sig)))).
+         (FinProd (FinOption sig) (initN (S (2 * (FS_crd sig))))).
 
 axiom daemon : ∀T:Type[0].T.
 
+definition to_initN : ∀n,m.n < m → initN m ≝ λn,m,Hn.mk_Sig … n ….// qed.
+
+definition initN_pred : ∀n.∀m:initN n.initN n ≝ λn,m.mk_Sig … (pred (pi1 … m)) …. 
+cases m #m0 /2 by le_to_lt_to_lt/ qed.
+
 (* controllare i contatori, molti andranno incrementati di uno *)
 definition trans_binaryTM : ∀sig,states:FinSet.
   (states × (option sig) → states × (option sig) × move) → 
@@ -52,69 +56,385 @@ definition trans_binaryTM : ∀sig,states:FinSet.
 ≝ λsig,states,trans,p.
   let 〈s,a〉 ≝ p in
   let 〈s0,phase,ch,count〉 ≝ s in
+  let (H1 : O < S (2*FS_crd sig)) ≝ ? in
+  let (H2 : FS_crd sig < S (2*FS_crd sig)) ≝ ? in
   match pi1 … phase with
   [ O ⇒ (*** PHASE 0: read ***)
-      match a with
-      [ Some a0 ⇒ 
-        match count with
-        [ O ⇒ 〈〈s0,1,ch,FS_crd sig〉,None ?,N〉
-        | S k ⇒ if (a0 == true) 
-                then 〈〈s0,0,FS_nth sig k,k〉, None ?,R〉
-                else 〈〈s0,0,ch,k〉,None ?,R〉 ]
-      | None ⇒ (* Overflow position! *)
-          〈〈s0,4,None ?,0〉,None ?,R〉 ]
+      match pi1 … count with
+      [ O ⇒ 〈〈s0,bin1,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
+      | S k ⇒ match a with
+        [ Some a0 ⇒ if (a0 == true) 
+                    then 〈〈s0,bin0,FS_nth sig k,initN_pred … count〉, None ?,R〉
+                    else 〈〈s0,bin0,ch,initN_pred … count〉,None ?,R〉 
+        | None ⇒ (* Overflow position! *)
+          〈〈s0,bin4,None ?,to_initN 0 ? H1〉,None ?,R〉 ] ]
   | S phase ⇒ match phase with
   [ O ⇒ (*** PHASE 1: restart ***)
-      match count with
-      [ O ⇒ 〈〈s0,2,ch,FS_crd sig〉,None ?,N〉
-      | S k ⇒ 〈〈s0,1,ch,k〉,None ?,L〉 ]
+      match pi1 … count with
+      [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
+      | S k ⇒ 〈〈s0,bin1,ch,initN_pred … count〉,None ?,L〉 ]
   | S phase ⇒ match phase with
   [ O ⇒ (*** PHASE 2: write ***)
       let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
-      match count with
+      match pi1 … count with
       [ O ⇒ let mv' ≝ match mv with [ R ⇒ N | _ ⇒ L ] in
             let count' ≝ match mv with [ R ⇒ 0 | N ⇒ FS_crd sig | L ⇒ 2*(FS_crd sig) ] in
-             〈〈s',3,ch,count'〉,None ?,mv'〉
+             〈〈s',bin3,ch,to_initN count' ??〉,None ?,mv'〉
       | S k ⇒ match a' with
-         [ None ⇒ 〈〈s0,2,ch,k〉,None ?,R〉
-         | Some a0' ⇒ let out ≝ (FS_nth k == a') in
-                      〈〈s0,2,ch,k〉,Some ? out,R〉 ]
+         [ None ⇒ 〈〈s0,bin2,ch,initN_pred … count〉,None ?,R〉
+         | Some a0' ⇒ let out ≝ (FS_nth ? k == a') in
+                      〈〈s0,bin2,ch,initN_pred … count〉,Some ? out,R〉 ]
       ]
   | S phase ⇒ match phase with
   [ O ⇒ (*** PHASE 3: move head left ***)
-      match count with
-      [ O ⇒ 〈〈s0,6,ch,O〉, None ?,N〉
-      | S k ⇒ 〈〈s0,3,ch,k〉, None ?,L〉 ]
+      match pi1 … count with
+      [ O ⇒ 〈〈s0,bin0,None ?,to_initN (FS_crd sig) ? H2〉, None ?,N〉 (* the end: restart *)
+      | S k ⇒ 〈〈s0,bin3,ch,initN_pred … count〉, None ?,L〉 ]
   | S phase ⇒ match phase with
   [ O ⇒ (*** PHASE 4: check position ***)
       match a with
-      [ None ⇒ (* niltape/rightof: we can write *) 〈〈s0,2,ch,FS_crd sig〉,None ?,N〉
+      [ None ⇒ (* niltape/rightof: we can write *) 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
       | Some _ ⇒ (* leftof *)
         let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
         match a' with
-        [ None ⇒ (* we don't write anything: go to end of 2 *) 〈〈s0,2,ch,0〉,None ?,N〉
-        | Some _ ⇒ (* extend tape *) 〈〈s0,5,ch,FS_crd sig〉,None ?,L〉 ]
+        [ None ⇒ (* we don't write anything: go to end of 2 *) 〈〈s0,bin2,ch,to_initN 0 ? H1〉,None ?,N〉
+        | Some _ ⇒ (* extend tape *) 〈〈s0,bin5,ch,to_initN (FS_crd sig) ? H2〉,None ?,L〉 ]
       ]
-  | S phase ⇒ match phase with
-  [ O ⇒ (*** PHASE 5: left extension ***)
-      match count with
-      [ O ⇒ 〈〈s0,2,ch,FS_crd sig〉,None ?,N〉
-      | S k ⇒ 〈〈s0,5,ch,k〉,Some ? false,L〉 ]
-  | S _ ⇒ (*** PHASE 6: stop ***) 〈s,None ?,N〉 ]]]]]].  
+  | S _ ⇒ (*** PHASE 5: left extension ***)
+      match pi1 … count with
+      [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
+      | S k ⇒ 〈〈s0,bin5,ch,initN_pred … count〉,Some ? false,L〉 ]]]]]].
+[2,3: //]
+whd in match count'; cases mv whd in ⊢ (?%?); //
+qed.
+
+definition halt_binaryTM : ∀sig,M.states_binaryTM sig (states sig M) → bool ≝ 
+  λsig,M,s.let 〈s0,phase,ch,count〉 ≝ s in
+  pi1 … phase == O ∧ halt sig M s0.
 
 (*
  * Una mk_binaryTM prende in input una macchina M e produce una macchina che:
  * - ha per alfabeto FinBool
- * - ha stati di tipo (states … M) × (initN 3) × (initN (dimensione dell'alfabeto di M))
+ * - ha stati di tipo ((states … M) × (initN 7)) × 
+       ((option sig) × (initN (2*dimensione dell'alfabeto di M + 1))
  *   dove il primo elemento corrisponde allo stato della macchina input,
  *   il secondo identifica la fase (lettura, scrittura, spostamento)
- *   il terzo è un contatore
- * - (la funzione di transizione è complessa al punto di rendere discutibile 
+ *   il terzo identifica il carattere oggetto letto
+ *   il quarto è un contatore
+ * - la funzione di transizione viene prodotta da trans_binaryTM
+ * - la funzione di arresto viene prodotta da halt_binaryTM
  *)
 definition mk_binaryTM ≝ 
-  λsig.λM:TM sig.mk_TM FinBool (FinProd (states … M) (FinProd (initN 3) (initN
-{ no_states : nat;
-  pos_no_states : (0 < no_states); 
-  ntrans : trans_source no_states → trans_target no_states;
-  nhalt : initN no_states → bool
-}.
\ No newline at end of file
+  λsig.λM:TM sig.
+  mk_TM FinBool (states_binaryTM sig (states sig M)) 
+    (trans_binaryTM sig (states sig M) (trans sig M)) 
+    (〈start sig M,bin0,None ?,FS_crd sig〉) (halt_binaryTM sig M).// qed.
+
+definition bin_char ≝ λsig,ch.unary_of_nat (FS_crd sig) (index_of_FS sig ch).
+
+definition bin_current ≝ λsig,t.match current ? t with
+[ None ⇒ [ ] | Some c ⇒ bin_char sig c ].
+
+definition tape_bin_lift ≝ λsig,t.
+let ls' ≝ flatten ? (map ?? (bin_char sig) (left ? t)) in
+let c' ≝ option_hd ? (bin_current sig t) in
+let rs' ≝ tail ? (bin_current sig t)@flatten ? (map ?? (bin_char sig) (right ? t)) in
+ mk_tape ? ls' c' rs'.
+
+definition R_bin_lift ≝ λsig,R,t1,t2.
+  ∃u1.t1 = tape_bin_lift sig u1 → 
+  ∃u2.t2 = tape_bin_lift sig u2 ∧ R u1 u2.
+  
+definition state_bin_lift :
+  ∀sig.∀M:TM sig.states sig M → states ? (mk_binaryTM ? M)
+ ≝ λsig,M,q.〈q,bin0,None ?,FS_crd sig〉.// qed.
+
+lemma lift_halt_binaryTM : 
+  ∀sig,M,q.halt sig M q = halt ? (mk_binaryTM sig M) (state_bin_lift ? M q).
+// qed.
+
+lemma binaryTM_bin0_bin1 :
+  ∀sig,M,t,q,ch.
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,O〉) t) 
+  = mk_config ?? (〈q,bin1,ch,to_initN (FS_crd sig) ??〉) t. //
+qed.
+
+lemma binaryTM_bin0_bin4 :
+  ∀sig,M,t,q,ch,k.
+  current ? t = None ? → S k <S (2*FS_crd sig) → 
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t) 
+  = mk_config ?? (〈q,bin4,None ?,to_initN 0 ??〉) (tape_move ? t R). [2,3://]
+#sig #M #t #q #ch #k #Hcur #Hk
+whd in match (step ???); whd in match (trans ???);
+>Hcur %
+qed.
+
+lemma binaryTM_bin0_true :
+  ∀sig,M,t,q,ch,k.
+  current ? t = Some ? true → S k <S (2*FS_crd sig) → 
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t) 
+  = mk_config ?? (〈q,bin0,FS_nth sig k,to_initN k ??〉) (tape_move ? t R).[2,3:/2 by lt_S_to_lt/]
+#sig #M #t #q #ch #k #Hcur #Hk
+whd in match (step ???); whd in match (trans ???);
+>Hcur %
+qed.
+
+lemma binaryTM_bin0_false :
+  ∀sig,M,t,q,ch,k.
+  current ? t = Some ? false → S k <S (2*FS_crd sig) → 
+  step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t) 
+  = mk_config ?? (〈q,bin0,ch,to_initN k ??〉) (tape_move ? t R).[2,3:/2 by lt_S_to_lt/]
+#sig #M #t #q #ch #k #Hcur #Hk
+whd in match (step ???); whd in match (trans ???);
+>Hcur %
+qed.
+
+(* to be checked *)
+axiom binary_to_bin_char :∀sig,csl,csr,a.
+  csl@true::csr=bin_char sig a → FS_nth ? (length ? csr) = Some ? a.
+
+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:/2 by O/]
+#sig #M #q #ls #a #rs #k #Hhalt #csr elim csr
+[ #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 #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) ??????)
+    [ //
+    | >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 %
+  | #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_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)) →
+  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_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.
+
+STOP
+
+lemma binaryTM_loop :
+ ∀sig,M,i,t,q,tf,qf.
+ loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) →
+ ∃k.loopM ? (mk_binaryTM sig M) k 
+  (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) = 
+  Some ? (mk_config ?? (state_bin_lift ? M qf) (tape_bin_lift ? tf)).
+#sig #M #i elim i
+[ #t #q #qf #tf change with (None ?) in ⊢ (??%?→?); #H destruct (H)
+| -i #i #IH #t #q #tf #qf
+  >loopM_unfold 
+  lapply (refl ? (halt sig M (cstate ?? (mk_config ?? q t))))
+  cases (halt ?? q) in ⊢ (???%→?); #Hhalt
+  [ >(loop_S_true ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)
+    #H destruct (H) %{1} >loopM_unfold >loop_S_true // ]
+  (* interesting case: more than one step *)
+  >(loop_S_false ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)
+  <loopM_unfold >(config_expand ?? (step ???)) #Hloop 
+  lapply (IH … Hloop) -IH * #k0 #IH <config_expand in Hloop; #Hloop
+  %{(S k0)}
+  
+
+
+(*
+theorem sem_binaryTM : ∀sig,M.
+  mk_binaryTM sig M ⊫ R_bin_lift ? (R_TM ? M (start ? M)).
+#sig #M #t #i generalize in match t; -t
+@(nat_elim1 … i) #m #IH #intape #outc #Hloop
+
+*)
\ No newline at end of file