From 3a47f3e553f17690908dfcacfdfa58c0da378a9b Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 6 Nov 2013 17:20:18 +0000
Subject: [PATCH] Full rework of the semantics of the binary machine (now
 completely working up to arithmetical proofs)

---
 .../lib/turing/multi_universal/binaryTM.ma    | 649 +++++++++++++-----
 1 file changed, 465 insertions(+), 184 deletions(-)

diff --git a/matita/matita/lib/turing/multi_universal/binaryTM.ma b/matita/matita/lib/turing/multi_universal/binaryTM.ma
index f2af60587..410c32716 100644
--- a/matita/matita/lib/turing/multi_universal/binaryTM.ma
+++ b/matita/matita/lib/turing/multi_universal/binaryTM.ma
@@ -58,7 +58,18 @@ lemma le_displ_of_move : ∀sig,mv.displ_of_move sig mv ≤ S (2*FS_crd sig).
 #sig * /2 by le_S/
 qed.
 
-(* controllare i contatori, molti andranno incrementati di uno *)
+definition displ2_of_move ≝ λsig,mv.
+  match mv with
+  [ L ⇒ FS_crd sig
+  | N ⇒ O
+  | R ⇒ O ].
+  
+lemma le_displ2_of_move : ∀sig,mv.displ2_of_move sig mv ≤ S (2*FS_crd sig).
+#sig * /2 by lt_to_le/
+qed.
+
+definition mv_tech ≝ λmv.match mv with [ N ⇒ N | _ ⇒ R ].
+
 definition trans_binaryTM : ∀sig,states:FinSet.
   (states × (option sig) → states × (option sig) × move) → 
   ((states_binaryTM sig states) × (option bool) → 
@@ -79,7 +90,7 @@ definition trans_binaryTM : ∀sig,states:FinSet.
         | None ⇒ (* Overflow position! *)
           let 〈s',a',mv〉 ≝ trans 〈s0,None ?〉 in
           match a' with
-          [ None ⇒ (* we don't write anything: go to end of 2 *) 〈〈s0,bin2,None ?,to_initN 0 ? H1〉,None ?,N〉
+          [ None ⇒ (* we don't write anything: go to end of 3 *) 〈〈s',bin3,None ?,to_initN (displ2_of_move sig mv) ??〉,None ?,mv_tech mv〉
           | Some _ ⇒ (* maybe extend tape *) 〈〈s0,bin4,None ?,to_initN O ? H1〉,None ?,R〉 ] ] ]
   | S phase ⇒ match phase with
   [ O ⇒ (*** PHASE 1: restart ***)
@@ -115,7 +126,7 @@ definition trans_binaryTM : ∀sig,states:FinSet.
       match pi1 … count with
       [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,R〉
       | S k ⇒ 〈〈s0,bin5,ch,initN_pred … count〉,Some ? false,L〉 ]]]]]].
-[2,3: /2 by lt_S_to_lt/] /2 by le_S_S/
+[ /2 by le_to_lt_to_lt/ | /2 by le_S_S/ |*: /2 by lt_S_to_lt/]
 qed.
 
 definition halt_binaryTM : ∀sig,M.states_binaryTM sig (states sig M) → bool ≝ 
@@ -155,10 +166,6 @@ let c' ≝ option_hd ? (opt_bin_char sig (current ? t)) in
 let rs' ≝ (tail ? (opt_bin_char sig (current ? t))@bin_list ? (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〉./2 by lt_S_to_lt/ qed.
@@ -173,12 +180,12 @@ lemma binaryTM_bin0_bin1 :
   = mk_config ?? (〈q,bin1,ch,to_initN (FS_crd sig) ??〉) t. //
 qed.
 
-lemma binaryTM_bin0_bin2 :
+lemma binaryTM_bin0_bin3 :
   ∀sig,M,t,q,ch,k,qn,mv.
   current ? t = None ? → S k <S (2*FS_crd sig) → 
   〈qn,None ?,mv〉 = trans sig M 〈q,None ?〉 → 
   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t) 
-  = mk_config ?? (〈q,bin2,None ?,to_initN O ??〉) t. [2,3:/2 by transitive_lt/]
+  = mk_config ?? (〈qn,bin3,None ?,to_initN (displ2_of_move sig mv) ??〉) (tape_move ? t (mv_tech mv)). [|@le_S //|@le_S_S @le_displ2_of_move]
 #sig #M #t #q #ch #k #qn #mv #Hcur #Hk #Htrans
 whd in match (step ???); whd in match (trans ???);
 >Hcur <Htrans %
@@ -281,16 +288,17 @@ qed.
 lemma minus_tech : ∀a,b.a + b - a = b. // qed.
 
 lemma binaryTM_phase0_midtape :
-  ∀sig,M,t,q,ls,a,rs,ch,k.
-  halt sig M q=false → S (FS_crd sig) ≤ k → 
+  ∀sig,M,t,q,ls,a,rs,ch.
+  halt sig M q=false → 
   t = mk_tape ? ls (option_hd ? (bin_char ? a)) (tail ? (bin_char sig a)@rs) →
+  ∀k.S (FS_crd sig) ≤ k → 
   loopM ? (mk_binaryTM sig M) k
     (mk_config ?? (〈q,bin0,ch,FS_crd sig〉) t) 
   = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
       (mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉) 
         (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [|*:@le_S //]
-#sig #M #t #q #ls #a #rs #ch #k #Hhalt #Hk #Ht
-cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
+#sig #M #t #q #ls #a #rs #ch #Hhalt #Ht #k #Hk
+cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >(minus_tech (S (FS_crd sig)))
 cut (∃c,cl.bin_char sig a = c::cl) [@daemon] * #c * #cl #Ha >Ha
 cut (FS_crd sig = |bin_char sig a|) [@daemon] #Hlen
 @(trans_eq ?? (loopM ? (mk_binaryTM ? M) (S (|c::cl|) + k0)
@@ -306,37 +314,39 @@ cut (FS_crd sig = |bin_char sig a|) [@daemon] #Hlen
 qed.
 
 lemma binaryTM_phase0_None_None :
-  ∀sig,M,t,q,ch,k,n,qn,mv.
-  O < n →  n < 2*FS_crd sig → O < k → 
+  ∀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 ?? (〈q,bin2,None ?,to_initN O ??〉) t). [2,3: /2 by transitive_lt/ ]
-#sig #M #t #q #ch #k #n #qn #mv #HOn #Hn #Hk #Hhalt
+      (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)
-cases t
-[ >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin2 // /2 by refl, transitive_lt/
-| #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin2 // /2 by refl, transitive_lt/
-| #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin2 // /2 by refl, transitive_lt/
+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,k,n,qn,chn,mv.
-  O < n →  n < 2*FS_crd sig → O < k → 
+  ∀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 #k #n #qn #chn #mv #HOn #Hn #Hk #Hhalt
+#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)
-cases t
+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/
@@ -358,8 +368,9 @@ lemma binaryTM_bin1_S :
 qed.
 
 lemma binaryTM_phase1 :
-  ∀sig,M,q,ls1,ls2,cur,rs,ch,k.
-  S (FS_crd sig) ≤ k → |ls1| = FS_crd sig → (cur = None ? → rs = [ ]) → 
+  ∀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))
@@ -407,8 +418,8 @@ cut (∀sig,M,q,ls1,ls2,ch,k,n,cur,rs.
     ]
    >reverse_cons >associative_append %
  ]
-| #Hcut #sig #M #q #ls1 #ls2 #cur #rs #ch #k #Hk #Hlen 
-  cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech @Hcut // ]
+| #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 :
@@ -445,26 +456,28 @@ 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,k,n. S n ≤ k → 
-  ∀t.n≤S (2*FS_crd sig) → 
+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 #k #n #Hk
-cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
+#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 #Htrans >loopM_unfold >loop_S_false //
+[ #t #Hle >loopM_unfold >loop_S_false //
   >(binaryTM_bin2_O … Htrans) //
-| #n0 #IH #t #Hn0 #Htrans >loopM_unfold >loop_S_false // 
+| #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,k.
-  S (FS_crd sig) ≤ k → 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 → 
+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))
@@ -512,11 +525,11 @@ cut (∀sig,M,q,ch,qn,chn,mv,ls,k,n.
       cut (bin_char ? chn = reverse ? csl@(FS_nth ? n0 == Some ? chn)::fs0) [@daemon]
       -Hbinchar #Hbinchar >Hbinchar @(trans_eq ???? (IH …)) //
       [ %{fs0} >reverse_cons >associative_append @Hbinchar
-      | whd in ⊢ (??%?); /2 by / ]
+      | whd in ⊢ (??%?); <Hcrd // ]
       @eq_f @eq_f @eq_f3 //
     ]
   ]
-| #Hcut #sig #M #q #ch #qn #chn #mv #ls #k #Hk #Htrans 
+| #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)} % | % ]
@@ -524,9 +537,10 @@ cut (∀sig,M,q,ch,qn,chn,mv,ls,k,n.
 ]
 qed.
 
-lemma binaryTM_phase2_Some_ow : ∀sig,M,q,ch,qn,chn,mv,ls,k,cs,rs.
-  S (FS_crd sig) ≤ k → 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 → 
+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))))
@@ -570,7 +584,7 @@ cut (∀sig,M,q,ch,qn,chn,mv,ls,rs,k,csr.
       ]
     ]
   ]
-| #Hcut #sig #M #q #ch #qn #chn #mv #ls #k #cs #rs #Hk #Htrans #Hcrd
+| #Hcut #sig #M #q #ch #qn #chn #mv #ls #cs #rs #Htrans #Hcrd #k #Hk
   cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech @trans_eq 
   [3: @(trans_eq ???? (Hcut ??????? ls ?? cs Htrans [ ] …)) //
     [ normalize % // | normalize @Hcrd | >Hcrd // ]
@@ -591,18 +605,20 @@ lemma binaryTM_bin3_S :
 #sig #M #t #q #ch #k #HSk %
 qed.
 
-lemma binaryTM_phase3 :∀sig,M,q,ch,k,n.
-  S n ≤ k → n ≤ S (2*FS_crd sig) →
-  ∀t.loopM ? (mk_binaryTM sig M) k
+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 #k #n #Hk
-cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech elim n
-[ #Hcrd #t >loopM_unfold >loop_S_false [| % ] >binaryTM_bin3_O // 
-| #n0 #IH #Hlt #t >loopM_unfold >loop_S_false [|%] >binaryTM_bin3_S [|//]  
-  <IH [|/2 by lt_to_le/]
+#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.
 
@@ -610,19 +626,19 @@ 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: @le_S //]
+  = 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,k,t.
-  O < k → current ? t = None ? →
+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). [2,3: @le_S //]
-#sig #M #q #ch #k #t #Hk #Hcur 
+      (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 //
+>loopM_unfold >loop_S_false // <loopM_unfold >binaryTM_bin4_None [|//] %
 qed.
 
 (* we don't get here any more! *
@@ -649,16 +665,16 @@ whd in ⊢ (??%?); >Hcur whd in ⊢ (??%?);
 whd in match (trans FinBool ??); <Htrans %
 qed.
 
-lemma binaryTM_phase4_extend : ∀sig,M,q,ch,k,t,cur,qn,an,mv.
-  O < k → current ? t = Some ? cur →
-  〈qn,Some ? an,mv〉 = trans sig M 〈q,ch〉 → 
+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 #k #t #cur #qn #an #mv #Hk #Hcur #Htrans 
+#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 //
+>loopM_unfold >loop_S_false // <loopM_unfold >(binaryTM_bin4_extend … Hcur) [|*://] %
 qed.
 
 lemma binaryTM_bin5_O :
@@ -677,23 +693,23 @@ 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. S n ≤ k →   
+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 #k #n #Hk
-cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
-elim n
-[ #rs #Hlt %{[]} % // 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/ ]
+#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
+  >associative_append normalize in match ([false]@?); <(IH (S n0 + k0)) [|//]
   >loopM_unfold @eq_f @eq_f cases rs //
 ]
 qed.
@@ -737,6 +753,8 @@ lemma iter_split : ∀T,f,m,n,x.
 #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).
@@ -760,19 +778,25 @@ 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.
+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 // ]
+| #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 → 
@@ -791,130 +815,387 @@ lemma iter_tape_move_L : ∀T,n,ls,cs,rs.|cs| = n →
 ]
 qed.
 
+axiom loop_increase : ∀sig,M,m,n,cfg,cfg'.m < n → 
+  loopM sig M m cfg = Some ? cfg' → loopM sig M n cfg = Some ? cfg'.
+
 lemma binaryTM_loop :
- ∀sig,M,i,t,q,tf,qf.
- O < FS_crd sig → 
- 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 #Hcrd change with (None ?) in ⊢ (??%?→?); #H destruct (H)
-| -i #i #IH #t #q #tf #qf #Hcrd >loopM_unfold
+ ∀sig,M,i,tf,qf. O < FS_crd sig → 
+ ∀t,q.∃k.i ≤ k ∧ 
+ ((loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) →
+  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))) ∧
+ (loopM sig M i (mk_config ?? q t) = None ? →
+  loopM ? (mk_binaryTM sig M) k 
+    (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) = None ?)).
+#sig #M #i #tf #qf #Hcrd elim i
+[ #t #q %{O} % // % // change with (None ?) in ⊢ (??%?→?); #H destruct (H)
+| -i #i #IH #t #q >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) [@Hcrd] -IH * #k0 #IH <config_expand in Hloop; #Hloop
-  %{(7*(S (FS_crd sig)) + k0)}
-  (*** PHASE 0 ***)
-  >state_bin_lift_unfold cases (current_None_or_midtape ? t)
-  (* 0.1) current = None *)
-  [ (* #Hcur >state_bin_lift_unfold in ⊢ (??%?); 
-    lapply (current_tape_bin_list … Hcur) #Hcur' 
-    >binaryTM_phase0_None /2 by monotonic_lt_plus_l/
-    >(?: FS_crd sig + k0 = S (FS_crd sig + k0 - 1)) [|@daemon]
-    >loopM_unfold >loop_S_false // lapply (refl ? t) cases t in ⊢ (???%→?);
-    [4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H) normalize in Hcur; destruct (Hcur)
-    | #Ht >Ht >binaryTM_bin4_None // <loopM_unfold *)
-  (* 0.2) midtape *)
-  | * #ls * #c * #rs #Ht >Ht >tape_bin_lift_unfold
-    >left_midtape >current_midtape >right_midtape >opt_bin_char_Some
-    >(binaryTM_phase0_midtape … Hhalt ? (refl ??)) [| // ]
-    >(?: 7*S (FS_crd sig) + k0 - S (FS_crd sig) = 6*S (FS_crd sig) + k0) [|/2 by plus_minus/]
-    (*** PHASE 1 ***)
-    >binaryTM_phase1
-    [| cases (bin_list ? rs) normalize // #r0 #rs0 #H destruct (H)
-    | >length_reverse @daemon
-    | // ]
-    >(?:6*S (FS_crd sig) + k0 - S (FS_crd sig) = 5*S (FS_crd sig) + k0) [|/2 by plus_minus/]
-    >reverse_reverse >opt_cons_hd_tl
+  [ %{(S i)} % // 
+    >(loop_S_true ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt) %
+    [| #H destruct (H)]
+    #H destruct (H) >loopM_unfold >loop_S_true // ]
+  (* interesting case: more than one step *)
+  >(loop_S_false ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)cases (current_None_or_midtape ? t)
+  (*** current = None ***)
+  [ #Hcur lapply (current_tape_bin_list … Hcur) #Hcur'
+    cut (∃qn,chn,mv.〈qn,chn,mv〉 = trans ? M 〈q,None ?〉)
+    [ cases (trans ? M 〈q,None ?〉) * #qn #chn #mv /4 by ex_intro/ ]
+    * #qn * #chn * #mv cases chn -chn
+    [ #Htrans lapply (binaryTM_phase0_None_None … (None ?) (FS_crd sig) … Hhalt Hcur' Htrans) // [/2 by monotonic_lt_plus_l/]
+      lapply (binaryTM_phase3 ? M qn (None ?) (displ2_of_move sig mv) ? (tape_move FinBool (tape_bin_lift sig t) (mv_tech mv))) [//]
+      cases (IH (tape_move ? t mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
+      #phase3 #phase0 %{(S (S (displ2_of_move sig mv))+k0)} %
+      [ @le_S_S @(le_plus O) // ]
+      >state_bin_lift_unfold >phase0 [|//]
+      >phase3 [|//] 
+      >(?: S (S (displ2_of_move sig mv))+k0-1-S (displ2_of_move sig mv) = k0)
+      [| /2 by refl, plus_to_minus/ ]
+      cut (tape_move sig t mv=tape_move sig (tape_write sig t (None sig)) mv) [%] #Hcut 
+      >(?: iter ? (λt0.tape_move ? t0 L) (displ2_of_move sig mv) (tape_move ? (tape_bin_lift ? t) (mv_tech mv))
+           =tape_bin_lift ? (tape_move ? t mv))
+      [|cases t in Hcur;
+        [4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H)
+        | #_ whd in match (tape_bin_lift ??);
+          (* TODO *)
+          (* ∀mv.tape_move ? (niltape ?) mv = niltape ? *)
+          (* ∀n.iter ? (λt.tape_move ? t ?) n (niltape ?) = niltape ? *)
+          @daemon
+        | #r0 #rs0 #_ cases mv
+          [ >tape_bin_lift_unfold whd in match (mv_tech L); whd in match (displ2_of_move sig L);
+            whd in match (rev_bin_list ??); whd in match (option_hd ??); 
+            whd in match (right ??); >(?: []@bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
+            (* TODO *)
+            (* tape_move (mk_tape [ ] (None ?) rs R = ... *)
+            (* use iter_tape_move_R *)
+            @daemon
+          | >tape_bin_lift_unfold whd in match (mv_tech R); whd in match (displ2_of_move sig R);
+            whd in match (rev_bin_list ??); whd in match (option_hd ??); 
+            whd in match (right ??); >(?: []@bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
+            whd in match (tape_move ? (leftof ???) R);
+            >tape_bin_lift_unfold >left_midtape >opt_bin_char_Some >right_midtape
+            >iter_O
+            (* TODO *)
+            (* tape_move (mk_tape [ ] (None ?) rs R = ... *)
+            @daemon
+          | >tape_bin_lift_unfold % ]
+        | #l0 #ls0 #_ cases mv
+          [ >tape_bin_lift_unfold whd in match (mv_tech L); whd in match (displ2_of_move sig L);
+            whd in match (bin_list ??); >append_nil whd in match (option_hd ??); 
+            whd in match (left ??); whd in match (tail ??);
+            whd in match (tape_move ? (rightof ???) L);
+            >(?: rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
+            (* TODO *)
+            (* tape_move (mk_tape ls (None ?) [ ] R = ... *)
+            (* use iter_tape_move_L *)
+            @daemon
+          | >tape_bin_lift_unfold whd in match (mv_tech R); whd in match (displ2_of_move sig R);
+            whd in match (bin_list ??); >append_nil whd in match (option_hd ??); 
+            whd in match (left ??); whd in match (tail ??); >iter_O cases (rev_bin_list ??) //
+          | >tape_bin_lift_unfold % ]
+        ]
+      ]
+      %
+      [ #Hloop @IH <Hloop @eq_f whd in ⊢ (???%); >Hcur <Htrans @eq_f @Hcut
+      | #Hloop @IHNone <Hloop @eq_f whd in ⊢ (???%); >Hcur <Htrans @eq_f @Hcut ]
+    | #chn #Htrans 
+      lapply (binaryTM_phase0_None_Some … (None ?) (FS_crd sig) … Hhalt Hcur' Htrans) // [/2 by monotonic_lt_plus_l/]
+      cases t in Hcur;
+      [ 4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H)
+      | 2: #r0 #rs0 #_ cut (∃b,bs.bin_char ? r0 = b::bs) [ @daemon ] * #b * #bs #Hbs 
+        lapply (binaryTM_phase4_extend ???? (tape_move ? (tape_bin_lift ? (leftof ? r0 rs0)) R) b … Htrans)
+        [ >tape_bin_lift_unfold whd in match (option_hd ??); whd in match (tail ??);
+          whd in match (right ??);
+          >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
+          >Hbs % ]
+        cases (binaryTM_phase5 ? M q (None ?) (FS_crd sig) (bin_list ? (r0::rs0)) ?) [|//]
+        #cs * #Hcs
+        lapply (binaryTM_phase2_Some_ow ?? q (None ?) … [ ] ? (bin_list ? (r0::rs0)) Htrans Hcs)
+        lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ? 
+                 (mk_tape FinBool (reverse bool (bin_char sig chn)@[])
+                   (option_hd FinBool (bin_list sig (r0::rs0))) (tail FinBool (bin_list sig (r0::rs0))))) [//]
+        cases (IH (tape_move ? (tape_write ? (leftof ? r0 rs0) (Some ? chn)) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
+        #phase3 #phase2 #phase5 #phase4 #phase0 
+        %{(1 + 1 + (S (FS_crd sig)) + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} %
+        [ @le_S_S @(le_plus O) // ]
+        >state_bin_lift_unfold >phase0 [|//]
+        >phase4 [|//] 
+        >(?: loopM ? (mk_binaryTM ??) ? (mk_config ?? 〈q,bin5,None ?,to_initN ???〉 ?) = ?)
+        [|| @(trans_eq ????? (phase5 ??)) 
+          [ @eq_f @eq_f
+            >tape_bin_lift_unfold whd in match (rev_bin_list ??);
+            whd in match (right ??); whd in match (bin_list ??);
+            cases (bin_char ? r0) // (* bin_char can't be nil *) @daemon
+          | @le_S_S >associative_plus >associative_plus >commutative_plus @(le_plus O) //
+          |]]
+        >phase2 [| (*arith*) @daemon ]
+        >phase3 [| (*arith*) @daemon ]
+        >(?: 1+1+S (FS_crd sig)+S (FS_crd sig)+S (displ_of_move sig mv)+k0-1-1
+              -S (FS_crd sig)-S (FS_crd sig) -S (displ_of_move sig mv) = k0) 
+        [| (*arith*) @daemon ]
+        -phase0 -phase2 -phase3 -phase4 -phase5 <state_bin_lift_unfold
+        >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
+              (mk_tape ? (reverse ? (bin_char sig chn)@[])
+                (option_hd FinBool (bin_list sig (r0::rs0)))
+                (tail FinBool (bin_list sig (r0::rs0))))
+           = tape_bin_lift ? (tape_move ? (tape_write ? (leftof ? r0 rs0) (Some ? chn)) mv))
+        [ % #Hloop
+          [ @IH <Hloop @eq_f whd in ⊢ (???%); <Htrans %
+          | @IHNone <Hloop @eq_f whd in ⊢ (???%); <Htrans % ]
+        | >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%] 
+          cases mv
+          [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
+            >iter_split >iter_tape_move_L [| @daemon ]
+            >hd_tech [|@daemon] >tail_tech [|@daemon] >iter_tape_move_L_left [|//]
+            whd in match (tape_move ???); >tape_bin_lift_unfold %
+          | normalize in match (displ_of_move ??); >iter_O
+            normalize in match (tape_move ???); 
+            >tape_bin_lift_unfold >opt_bin_char_Some
+            >hd_tech [|@daemon] >tail_tech [| @daemon ] %
+          | normalize in match (displ_of_move ??);
+            >iter_tape_move_L [|@daemon]
+            normalize in match (tape_move ???); >tape_bin_lift_unfold
+            >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ]
+        ]
+      | #_ lapply (binaryTM_phase4_write ? M q (None ?) (niltape ?) (refl ??))
+        lapply (binaryTM_phase2_Some_of ?? q (None ?) … [ ] Htrans)
+        lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ? 
+                 (mk_tape FinBool (reverse bool (bin_char sig chn)@[]) (None ?) [ ])) [//]
+        cases (IH (tape_move ? (midtape ? [ ] chn [ ]) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
+        #phase3 #phase2 #phase4 #phase0
+        %{(1 + 1 + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} %
+        [ @le_S_S @(le_plus O) // ]
+        >state_bin_lift_unfold >phase0 [|//]
+        >phase4 [|//]
+        >phase2 [|(*arith *) @daemon]
+        >phase3 [| (*arith*) @daemon ]
+        >(?: 1+1+S (FS_crd sig) + S (displ_of_move sig mv)+k0-1-1
+              -S (FS_crd sig)-S (displ_of_move sig mv) = k0) 
+        [| (*arith*) @daemon ]
+        -phase0 -phase2 -phase3 -phase4 <state_bin_lift_unfold
+        >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
+              (mk_tape ? (reverse ? (bin_char sig chn)@[]) (None ?) [ ])
+           = tape_bin_lift ? (tape_move ? (tape_write ? (niltape ?) (Some ? chn)) mv))
+        [ % #Hloop
+          [ @IH <Hloop @eq_f whd in ⊢ (???%); <Htrans %
+          | @IHNone <Hloop @eq_f whd in ⊢ (???%); <Htrans % ]
+        | cases mv
+          [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
+            >iter_split change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????(????%))?);
+            >iter_tape_move_L [| @daemon ]
+            >append_nil in ⊢ (??(????(???%?))?); >tail_tech [|@daemon] 
+            >iter_tape_move_L_left [|//]
+            normalize in match (tape_move ???);
+            >tape_bin_lift_unfold %
+          | normalize in match (displ_of_move ??); >iter_O
+            normalize in match (tape_move ???); 
+            >tape_bin_lift_unfold %
+          | normalize in match (displ_of_move ??);
+            change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????%)?);
+            >iter_tape_move_L [|@daemon]
+            normalize in match (tape_move ???); >tape_bin_lift_unfold
+            >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ]
+        ]
+      | #l0 #ls0 #_ lapply (binaryTM_phase4_write ? M q (None ?) (tape_bin_lift ? (rightof ? l0 ls0)) ?) 
+        [ >tape_bin_lift_unfold >current_mk_tape % ]
+        lapply (binaryTM_phase2_Some_of ?? q (None ?) … (rev_bin_list ? (l0::ls0)) Htrans)
+        lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ? 
+                 (mk_tape FinBool (reverse bool (bin_char sig chn)@rev_bin_list ? (l0::ls0)) (None ?) [ ])) [//]
+        cases (IH (tape_move ? (midtape ? (l0::ls0) chn [ ]) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
+        #phase3 #phase2 #phase4 #phase0
+        %{(1 + 1 + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} %
+        [ @le_S_S @(le_plus O) // ]
+        >state_bin_lift_unfold >phase0 [|//]
+        >(?:tape_move ? (tape_bin_lift ? (rightof ? l0 ls0)) R = tape_bin_lift ? (rightof ? l0 ls0))
+        [| >tape_bin_lift_unfold normalize in match (option_hd ??); normalize in match (right ??);
+           normalize in match (tail ??); normalize in match (left ??);
+           >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
+           cases (reverse ? (bin_char ? l0)) // cases (rev_bin_list ? ls0) // ]
+        >phase4 [|//]
+        >phase2 [|(*arith *) @daemon]
+        >phase3 [| (*arith*) @daemon]
+        >(?: 1+1+S (FS_crd sig) + S (displ_of_move sig mv)+k0-1-1
+              -S (FS_crd sig)-S (displ_of_move sig mv) = k0) 
+        [| (*arith*) @daemon ]
+        -phase0 -phase2 -phase3 -phase4 <state_bin_lift_unfold
+        >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
+              (mk_tape ? (reverse ? (bin_char sig chn)@rev_bin_list ? (l0::ls0)) (None ?) [ ])
+           = tape_bin_lift ? (tape_move ? (tape_write ? (rightof ? l0 ls0) (Some ? chn)) mv))
+        [ % #Hloop
+          [ @IH <Hloop @eq_f whd in ⊢ (???%); <Htrans %
+          | @IHNone <Hloop @eq_f whd in ⊢ (???%); <Htrans % ]
+        | cases mv
+          [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
+            >iter_split change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????(????%))?);
+            >iter_tape_move_L [| @daemon ]
+            >append_nil in ⊢ (??(????(???%?))?); >tail_tech [|@daemon] 
+            >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
+            >append_nil >iter_tape_move_L [|@daemon]
+            normalize in match (tape_move ???);
+            >tape_bin_lift_unfold @eq_f2
+            [ >hd_tech [|@daemon] %
+            | >tail_tech [|@daemon] >opt_bin_char_Some normalize in match (bin_list ??); >append_nil %]
+          | normalize in match (displ_of_move ??); >iter_O
+            normalize in match (tape_move ???); 
+            >tape_bin_lift_unfold %
+          | normalize in match (displ_of_move ??);
+            change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????%)?);
+            >iter_tape_move_L [|@daemon]
+            normalize in match (tape_move ???); >tape_bin_lift_unfold
+            >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ]
+        ]
+      ]
+    ]
+  (*** midtape ***)
+  | * #ls * #c * #rs #Ht >Ht     
     cut (∃qn,chn,mv.〈qn,chn,mv〉 = trans ? M 〈q,Some ? c〉)
     [ cases (trans ? M 〈q,Some ? c〉) * #qn #chn #mv /4 by ex_intro/ ]
-    * #qn * #chn * #mv cases chn -chn
-    [ (* no write! *) #Htrans >(binaryTM_phase2_None … Htrans) [2,3: //]
+    * #qn * #chn * #mv #Htrans
+    cut (tape_bin_lift ? t = ?) [| >tape_bin_lift_unfold % ] 
+    >Ht in ⊢ (???%→?); >opt_bin_char_Some >left_midtape >right_midtape #Ht'
+    lapply (binaryTM_phase0_midtape ?? (tape_bin_lift ? t) q … (None ?) Hhalt Ht')
+    lapply (binaryTM_phase1 ?? q (reverse ? (bin_char ? c)) (rev_bin_list ? ls) 
+             (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)) (Some ? c) ??)
+    [ cases (bin_list ? rs) // @daemon | >length_reverse @daemon |]
+    >opt_cons_hd_tl >reverse_reverse
+    cases chn in Htrans; -chn
+    [ #Htrans 
+      lapply (binaryTM_phase2_None … Htrans (FS_crd sig) ? 
+               (mk_tape FinBool (rev_bin_list sig ls)
+                 (option_hd FinBool (bin_char sig c@bin_list sig rs))
+                 (tail FinBool (bin_char sig c@bin_list sig rs)))) [//]
+      lapply (binaryTM_phase3 ? M qn (Some ? c) (displ_of_move sig mv) ? 
+               (mk_tape FinBool (reverse bool (bin_char sig c)@rev_bin_list ? ls)
+               (option_hd FinBool (bin_list sig rs)) (tail FinBool (bin_list sig rs)))) [//]
+      cases (IH (tape_move ? (tape_write ? (midtape ? ls c rs) (None ?)) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
+      #phase3 #phase2 #phase1 #phase0
+      %{(S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0)} %
+      [ @le_S_S @(le_plus O) // ]
+      >state_bin_lift_unfold <Ht >phase0 [|//]
+      >phase1 [|/2 by monotonic_le_minus_l/]
+      >phase2 [|/2 by monotonic_le_minus_l/]
       >iter_tape_move_R [|@daemon]
-      >(?:5*S (FS_crd sig) + k0 - S (FS_crd sig) = 4*S (FS_crd sig) + k0) [|/2 by plus_minus/]
-      >binaryTM_phase3 
-      [|//| cut (S (displ_of_move sig mv) ≤ 2*(S (FS_crd sig)))
-        [ /2 by le_S_S/ 
-        | #H @(transitive_le ??? H) -H -Hcrd @(transitive_le ? (4*S (FS_crd sig))) /2 by le_plus_a/ ]
-      ]
-      cut (∀sig,M,m,n,cfg,cfg'.m < n → loopM sig M m cfg = Some ? cfg' → loopM sig M n cfg = Some ? cfg') [@daemon]
-      #Hcut <(Hcut ??? (4*S (FS_crd sig) + k0 - S (displ_of_move sig mv)) ??? IH)
-      [| cases mv 
-        [ >(?:displ_of_move sig L = 2*FS_crd sig) //
-          >eq_minus_S_pred
-          @(transitive_le ? (pred (4*FS_crd sig+k0-2*FS_crd sig)))
-          [ >(?:4*FS_crd sig+k0-2*FS_crd sig = 2*FS_crd sig + k0) 
-            [ cases Hcrd /2 by le_minus_to_plus, le_n/
-            | <plus_minus [2://] 
-              >(commutative_times 4) >(commutative_times 2) 
-              <distributive_times_minus //
-            ]
-          | @monotonic_pred /2 by monotonic_le_minus_l/ ]
-        | whd in match (displ_of_move ??); @(transitive_le ? (4*1+k0-1)) 
-          [ //
-          | change with (pred (4*1+k0)) in ⊢ (?%?);
-             >eq_minus_S_pred <minus_n_O @monotonic_pred // ]
-        | >(?:displ_of_move sig N = FS_crd sig) //
-          >eq_minus_S_pred
-          @(transitive_le ? (pred (4*FS_crd sig+k0-1*FS_crd sig)))
-          [ >(?:4*FS_crd sig+k0-1*FS_crd sig = 3*FS_crd sig + k0) 
-            [ cases Hcrd /2 by le_minus_to_plus, le_n/
-            | <plus_minus [2://]
-              >(commutative_times 4) >(commutative_times 1) 
-              <distributive_times_minus //
-            ]
-          | @monotonic_pred /2 by transitive_le, le_n/ ] ] ] 
-      @eq_f @eq_f2 
-      [ <state_bin_lift_unfold >Ht whd in match (step ???); <Htrans %
-      | (* must distinguish mv *)
-        cases mv in Htrans; #Htrans
-        [ >(?:displ_of_move ? L = FS_crd sig + FS_crd sig) [| normalize // ]
-          >iter_split >iter_tape_move_L [|@daemon] >Ht cases ls
-          [ normalize in match (rev_bin_list ??); 
-            >hd_tech [|@daemon] >tail_tech [|@daemon]
-            >iter_tape_move_L_left // whd in match (step ???);
-            <Htrans whd in match (ctape ???);
+      >phase3 [|/2 by monotonic_le_minus_l/]
+      -phase0 -phase1 -phase2 -phase3
+      >(?: S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0
+           - S (FS_crd sig) - S (FS_crd sig) - S (FS_crd sig) - S (displ_of_move sig mv)
+         = k0) [| (*arith*) @daemon]
+      <state_bin_lift_unfold
+      >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
+            (mk_tape ? (reverse ? (bin_char sig c)@rev_bin_list ? ls) 
+              (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)))
+         = tape_bin_lift ? (tape_move ? (tape_write ? (midtape ? ls c rs) (None ?)) mv))
+      [ % #Hloop
+        [ @IH <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans %
+        | @IHNone <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans % ]
+      | normalize in match (tape_write ???); cases mv in Htrans; #Htrans
+        [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
+          >iter_split >iter_tape_move_L [| @daemon ]
+          cases ls
+          [ >hd_tech [|@daemon] >tail_tech [|@daemon] >iter_tape_move_L_left [|//]
             >tape_bin_lift_unfold %
-          | #l0 #ls0 change with (reverse ? (bin_char ? l0)@rev_bin_list ? ls0) in match (rev_bin_list ??);
+          | #l0 #ls0 >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
+            normalize in match (tape_move ???);
             >iter_tape_move_L [|@daemon]
             >hd_tech [|@daemon] >tail_tech [|@daemon]
-            whd in match (step ???); <Htrans whd in match (ctape ???);
-            >tape_bin_lift_unfold >left_midtape >current_midtape
-            >opt_bin_char_Some >right_midtape %
+            >tape_bin_lift_unfold % ]
+        | normalize in match (displ_of_move ??); >iter_O cases rs
+          [ normalize in match (tape_move ???); >tape_bin_lift_unfold %
+          | #r0 #rs0 normalize in match (tape_move ???);
+            >tape_bin_lift_unfold >opt_bin_char_Some
+            >left_midtape >right_midtape
+            >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
+            >hd_tech [|@daemon] >tail_tech [|@daemon] %
           ]
-        | change with 
-            (mk_tape ? (reverse ? (bin_char ? c)@rev_bin_list ? ls)
+        | normalize in match (displ_of_move ??); >iter_tape_move_L [|@daemon]
+          >hd_tech [|@daemon] >tail_tech [|@daemon] >tape_bin_lift_unfold %
+        ]
+      ]
+    | #chn #Htrans 
+      lapply (binaryTM_phase2_Some_ow ?? q (Some ? c) ??? (rev_bin_list ? ls) (bin_char ? c) (bin_list ? rs) Htrans ?)
+      [@daemon]
+      lapply (binaryTM_phase3 ? M qn (Some ? c) (displ_of_move sig mv) ? 
+               (mk_tape FinBool (reverse bool (bin_char sig chn)@rev_bin_list ? ls)
+               (option_hd FinBool (bin_list sig rs)) (tail FinBool (bin_list sig rs)))) [//]
+      cases (IH (tape_move ? (tape_write ? (midtape ? ls c rs) (Some ? chn)) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
+      #phase3 #phase2 #phase1 #phase0
+      %{(S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0)} %
+      [ @le_S_S @(le_plus O) // ]
+      >state_bin_lift_unfold <Ht >phase0 [|//]
+      >phase1 [|/2 by monotonic_le_minus_l/]
+      >phase2 [|/2 by monotonic_le_minus_l/]
+      >phase3 [|/2 by monotonic_le_minus_l/]
+      -phase0 -phase1 -phase2 -phase3
+      >(?: S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0
+           - S (FS_crd sig) - S (FS_crd sig) - S (FS_crd sig) - S (displ_of_move sig mv)
+         = k0) [| (*arith*) @daemon]
+      <state_bin_lift_unfold
+      >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
+            (mk_tape ? (reverse ? (bin_char sig chn)@rev_bin_list ? ls) 
               (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)))
-          in ⊢ (??%?);
-          >reverse_bin_char_list <IH
-          >Ht >tape_bin_lift_unfold @eq_f3
-          whd in match (step ???); <Htrans cases rs //
-          #r0 #rs0 whd in match (ctape ???); >current_midtape >opt_bin_char_Some
-          [ <hd_tech in ⊢(???%); // @daemon 
-          | >right_midtape <tail_tech // @daemon ]
-        | whd in match (displ_of_move ? N); >iter_tape_move_L [|@daemon]
-          >Ht whd in match (step ???); <Htrans whd in match (ctape ???);
-          >tape_bin_lift_unfold >left_midtape >current_midtape >right_midtape
-          >opt_bin_char_Some lapply Hcrd >(?:FS_crd sig = |bin_char ? c|) [| @daemon ]
-          cases (bin_char ? c) // #H normalize in H; @False_ind
-          cases (not_le_Sn_O O) /2/
+         = tape_bin_lift ? (tape_move ? (tape_write ? (midtape ? ls c rs) (Some ? chn)) mv))
+      [ % #Hloop
+        [ @IH <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans %
+        | @IHNone <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans % ]
+      | normalize in match (tape_write ???); cases mv in Htrans; #Htrans
+        [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
+          >iter_split >iter_tape_move_L [| @daemon ]
+          cases ls
+          [ >hd_tech [|@daemon] >tail_tech [|@daemon] >iter_tape_move_L_left [|//]
+            >tape_bin_lift_unfold %
+          | #l0 #ls0 >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
+            normalize in match (tape_move ???);
+            >iter_tape_move_L [|@daemon]
+            >hd_tech [|@daemon] >tail_tech [|@daemon]
+            >tape_bin_lift_unfold % ]
+        | normalize in match (displ_of_move ??); >iter_O cases rs
+          [ normalize in match (tape_move ???); >tape_bin_lift_unfold %
+          | #r0 #rs0 normalize in match (tape_move ???);
+            >tape_bin_lift_unfold >opt_bin_char_Some
+            >left_midtape >right_midtape
+            >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
+            >hd_tech [|@daemon] >tail_tech [|@daemon] %
+          ]
+        | normalize in match (displ_of_move ??); >iter_tape_move_L [|@daemon]
+          >hd_tech [|@daemon] >tail_tech [|@daemon] >tape_bin_lift_unfold %
         ]
       ]
-         
-          
-         
-
+    ]
+  ]
+]
+qed.
 
+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.
+  
 (*
-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
+∀sig,M,i,tf,qf. O < FS_crd sig → 
+ ∀t,q.∃k.i ≤ k ∧ 
+ ((loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) →
+  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))) ∧
+ (loopM sig M i (mk_config ?? q t) = None ? →
+  loopM ? (mk_binaryTM sig M) k 
+    (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) = None ?)).
+    *)
+axiom loop_incr : ∀sig,M,m,n,cfg,cfg'.m ≤ n → 
+  loopM sig M m cfg = Some ? cfg' → loopM sig M n cfg = Some ? cfg'.
+
+theorem sem_binaryTM : 
+  ∀sig,M,R.O < FS_crd sig → M ⊫ R → mk_binaryTM sig M ⊫ R_bin_lift ? R.
+#sig #M #R #Hcrd #HM #t #k #outc #Hloopbin #u #Ht
+lapply (refl ? (loopM ? M k (initc ? M u))) cases (loopM ? M k (initc ? M u)) in ⊢ (???%→?);
+[ #H cases (binaryTM_loop ? M k u (start ? M) Hcrd u (start ? M))
+  #k0 * #Hlt * #_ #H1 lapply (H1 H) -H -H1 <Ht
+  whd in match (initc ???) in Hloopbin; whd in match (start ??) in Hloopbin;
+  >state_bin_lift_unfold >(loop_incr … Hlt Hloopbin) #H destruct (H)
+| * #qf #tf #H cases (binaryTM_loop ? M k tf qf Hcrd u (start ? M))
+  #k0 * #Hlt * #H1 #_ lapply (H1 H) -H1 <Ht
+  whd in match (initc ???) in Hloopbin; whd in match (start ??) in Hloopbin;
+  >state_bin_lift_unfold >(loop_incr … Hlt Hloopbin) #Heq destruct (Heq)
+  % [| % [%]] @(HM … H)
+qed.
\ No newline at end of file
-- 
2.39.2