matita/matita/lib/turing/multi_universal/binaryTM.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "turing/mono.ma".
  16
  17 lemma le_to_eq : ∀m,n.m ≤ n → ∃k. n = m + k. /3 by plus_minus, ex_intro/
  18 qed.
  19
  20 lemma minus_tech : ∀a,b.a + b - a = b. // qed.
  21
  22 lemma loop_incr2 : ∀sig,M,m,n,cfg,cfg'.m ≤ n →
  23   loopM sig M m cfg = Some ? cfg' → loopM sig M n cfg = Some ? cfg'.
  24 #sig #M #m #n #cfg #cfg' #H cases (le_to_eq … H) #k #Hk >Hk
  25 >commutative_plus @loop_incr
  26 qed.
  27
  28 (* given a FinSet F:
  29    - get its cardinality
  30    - return its nth element
  31    - return the index of a given element
  32  *)
  33 definition FS_crd ≝ λF:FinSet.|enum F|.
  34 definition FS_nth ≝ λF:FinSet.λn.nth_opt ? n (enum F).
  35 definition index_of_FS_aux ≝ λF:FinSet.λf.position_of ? (λx.x==f) (enum F).
  36
  37 lemma index_of_FS_aux_None :
  38   ∀F,f.index_of_FS_aux F f = None ? → False.
  39 #F #f #e cut (memb ? f (enum F) = false)
  40 [ generalize in match e; -e normalize in ⊢ (%→?); generalize in match O;
  41   elim (enum F) //
  42   #hd #tl #IH #n whd in ⊢ (??%?→?); cases (true_or_false (hd==f))
  43   #Hbool >Hbool normalize
  44   [ #H destruct (H)
  45   | #H >(\bf ?) [| @sym_not_eq @(\Pf Hbool) ] @IH // ]
  46 | >enum_complete #H destruct (H) ]
  47 qed.
  48
  49 definition index_of_FS : ∀F:FinSet.F → nat ≝ λF,f.
  50 match index_of_FS_aux F f
  51 return (λx:option nat.index_of_FS_aux F f = x → nat) with
  52 [ None ⇒ λe.?
  53 | Some n ⇒ λe.n ] (refl ??).cases (index_of_FS_aux_None … e)
  54 qed.
  55
  56 (* unary bit representation (with a given length) of a certain number *)
  57 let rec unary_of_nat n k on n ≝
  58   match n with [ O ⇒ [ ] | S q ⇒ (eqb q k)::unary_of_nat q k].
  59
  60 lemma lt_FS_index_crd_aux : ∀sig,c,n.index_of_FS_aux sig c = Some ? n → n < FS_crd sig.
  61 #sig #c #n whd in ⊢ (??%?→?); >(?:FS_crd sig = O + FS_crd sig) //
  62 generalize in match O; normalize in match (FS_crd sig); elim (enum sig)
  63 normalize [ #n0 #H destruct (H) ]
  64 #hd #tl #IH #n0 cases (hd==c) normalize
  65 [ #H destruct (H) //
  66 | #H lapply (IH ? H) // ]
  67 qed.
  68
  69 lemma index_of_FS_def : ∀sig,c,n.index_of_FS sig c = n → index_of_FS_aux sig c = Some ? n.
  70 #sig #c #n whd in ⊢ (??%?→?); lapply (refl ? (index_of_FS_aux sig c))
  71 cases (index_of_FS_aux sig c) in ⊢ (???%→??(match % return ? with [ _ ⇒ ? | _ ⇒ ? ] ?)?→%);
  72 [ #e cases (index_of_FS_aux_None ?? e)
  73 | normalize // ]
  74 qed.
  75
  76 lemma index_of_FS_def2 : ∀sig,c.index_of_FS_aux sig c = Some ? (index_of_FS sig c)./2/
  77 qed.
  78
  79 lemma lt_FS_index_crd: ∀sig,c.index_of_FS sig c < FS_crd sig.
  80 #sig #c @(lt_FS_index_crd_aux sig c ? (index_of_FS_def2 …))
  81 qed.
  82
  83 lemma le_position_of_aux : ∀T,f,l,k,n.position_of_aux T f l k = Some ? n → k ≤ n.
  84 #T #f #l elim l normalize
  85 [ #k #n #H destruct (H)
  86 | #hd #tl #IH #k #n cases (f hd) normalize
  87   [ #H destruct (H) %
  88   | #H lapply (IH … H) /2 by lt_to_le/ ]
  89 ]
  90 qed.
  91
  92 lemma nth_index_of_FS_aux :
  93 ∀sig,a,n.index_of_FS_aux sig a = Some ? n → FS_nth sig n = Some ? a.
  94 #sig #a #n normalize >(?:n = O + n) in ⊢ (%→?); //
  95 lapply O lapply n -n elim (enum sig) normalize
  96 [ #n #k #H destruct (H)
  97 | #hd #tl #IH #n #k cases (true_or_false (hd==a)) #Ha >Ha normalize
  98   [ #H destruct (H) >(?:n = O) // >(\P Ha) //
  99   | cases n
 100     [ <plus_n_O #H @False_ind lapply (le_position_of_aux … H) #H1
 101       cases (not_le_Sn_n k) /2/
 102     | #n0 #Hrec @(IH ? (S k)) >Hrec /2 by eq_f/ ]
 103   ]
 104 ]
 105 qed.
 106
 107 lemma nth_index_of_FS : ∀sig,a.FS_nth sig (index_of_FS ? a) = Some ? a.
 108 #sig #a @nth_index_of_FS_aux >index_of_FS_def2 %
 109 qed.
 110
 111 definition bin_char ≝ λsig,ch.unary_of_nat (FS_crd sig) (index_of_FS sig ch).
 112
 113 definition opt_bin_char ≝ λsig,c.match c with
 114 [ None ⇒ [ ] | Some c0 ⇒ bin_char sig c0 ].
 115
 116 lemma eq_length_bin_char_FS_crd : ∀sig,c.|bin_char sig c| = FS_crd sig.
 117 #sig #c whd in ⊢ (??(??%)?); elim (FS_crd sig) //
 118 #n #IH <IH in ⊢ (???%); %
 119 qed.
 120
 121 lemma bin_char_FS_nth_tech :
 122   ∀sig,c,l1,b,l2.bin_char sig c = l1@b::l2 → b = (((|l2|):DeqNat) == index_of_FS sig c).
 123 #sig #c #l1 #b #l2 #Hbin lapply (eq_length_bin_char_FS_crd sig c)
 124 >Hbin #Hlen lapply Hbin lapply Hlen -Hlen -Hbin
 125 whd in match (bin_char ??); lapply l2 lapply c lapply l1 -l2 -c -l1
 126 elim (FS_crd sig)
 127 [ #l1 #b #l2 normalize in ⊢ (??%?→?); cases l1
 128   [ normalize #H destruct (H) | #hd #tl normalize #H destruct (H) ]
 129 | #n #IH #l1 #b #l2 whd in ⊢ (?→??%?→?); cases l1
 130   [ whd in ⊢ (??%?→???%→?); #Hlen destruct (Hlen)
 131     #H <(cons_injective_l ????? H) @eq_f2 //
 132   | #b0 #l10 #Hlen #H lapply (cons_injective_r ????? H) -H #H @(IH … H)
 133     normalize in Hlen; destruct (Hlen) % ]
 134 ]
 135 qed.
 136
 137 lemma nth_opt_memb : ∀T:DeqSet.∀l,n,t.nth_opt T n l = Some ? t → memb T t l = true.
 138 #T #l elim l normalize [ #n #t #H destruct (H) ]
 139 #hd #tl #IH #n #t cases n normalize
 140 [ #Ht destruct (Ht) >(\b (refl ? t)) %
 141 | #n0 #Ht cases (t==hd) // @(IH … Ht) ]
 142 qed.
 143
 144 lemma FS_nth_neq :
 145 ∀sig,m,n. m ≠ n →
 146 ∀s1,s2.FS_nth sig m = Some ? s1 → FS_nth sig n = Some ? s2 → s1 ≠ s2.
 147 #sig #m #n #Hneq #s1 #s2 lapply (enum_unique sig) lapply Hneq
 148 lapply n lapply m -n -m normalize elim (enum sig)
 149 [ #m #n #_ #_ normalize #H destruct (H)
 150 | #hd #tl #IH #m #n #Hneq whd in ⊢ (??%?→?);
 151   cases (true_or_false (hd ∈ tl)) #Hbool >Hbool normalize in ⊢ (%→?);
 152   [ #H destruct (H)
 153   | #H cases m in Hneq;
 154     [ #Hneq whd in ⊢ (??%?→?); #H1 destruct (H1) cases n in Hneq;
 155       [ * #H cases (H (refl ??))
 156       | #n0 #_ whd in ⊢ (??%?→?); #Htl % #Heq destruct (Heq)
 157         >(nth_opt_memb … Htl) in Hbool; #Hfalse destruct (Hfalse)
 158       ]
 159     | #m0 #Hneq whd in ⊢ (??%?→?); #H1
 160       whd in ⊢ (??%?→?); cases n in Hneq;
 161       [ #_ whd in ⊢ (??%?→?); #H2 destruct (H2) % #Heq destruct (Heq)
 162         >(nth_opt_memb … H1) in Hbool; #Hfalse destruct (Hfalse)
 163       | #n0 #Hneq whd in ⊢ (??%?→?); @(IH m0 n0 ? H … H1)
 164         % #Heq cases Hneq /2/
 165       ]
 166     ]
 167   ]
 168 ]
 169 qed.
 170
 171 lemma nth_opt_Some : ∀T,l,n.n < |l| → ∃t.nth_opt T n l = Some ? t.
 172 #T #l elim l
 173 [ normalize #n #H @False_ind cases (not_le_Sn_O n) /2/
 174 | #hd #tl #IH #n normalize cases n
 175   [ #_ %{hd} //
 176   | #n0 #Hlt cases (IH n0 ?) [| @le_S_S_to_le // ]
 177     #t #Ht normalize %{t} // ]
 178 ]
 179 qed.
 180
 181 corollary FS_nth_Some : ∀sig,n.n < FS_crd sig → ∃s.FS_nth sig n = Some ? s.
 182 #sig #n @nth_opt_Some
 183 qed.
 184
 185 lemma bin_char_FS_nth :
 186   ∀sig,c,l1,b,l2.bin_char sig c = l1@b::l2 → b = (FS_nth sig (|l2|) == Some ? c).
 187 #sig #c #l1 #b #l2 #H >(bin_char_FS_nth_tech … H)
 188 cases (true_or_false (((|l2|):DeqNat)==index_of_FS sig c)) #Hbool >Hbool
 189 [ >(?:(|l2|)=index_of_FS sig c) [|change with ((|l2|):DeqNat) in ⊢ (??%?); @(\P Hbool) ]
 190   @sym_eq @(\b ?) @nth_index_of_FS
 191 | <nth_index_of_FS @sym_eq @(\bf ?) % #Hfalse
 192   cases (FS_nth_Some sig (|l2|) ?) [| <(eq_length_bin_char_FS_crd sig c) >H >length_append normalize // ]
 193   #s1 #H1
 194   cases (FS_nth_Some sig (index_of_FS sig c) ?) [|//]
 195   #s2 #H2
 196   cases (FS_nth_neq … H1 H2) [| @(\Pf Hbool) ]
 197   #Hfalse2 @Hfalse2 <Hfalse in H2; >H1 #HSome destruct (HSome) %
 198 ]
 199 qed.
 200
 201 corollary binary_to_bin_char :∀sig,csl,csr,a.
 202   csl@true::csr=bin_char sig a → FS_nth ? (length ? csr) = Some ? a.
 203 #sig #csl #csr #a #H @(\P ?) @sym_eq @bin_char_FS_nth //
 204 qed.
 205
 206 (* axiom FinVector : Type[0] → nat → FinSet.*)
 207
 208 definition binary_base_states ≝ initN 6.
 209
 210 definition bin0 : binary_base_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 6 (refl …)).
 211 definition bin1 : binary_base_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 6 (refl …)).
 212 definition bin2 : binary_base_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 6 (refl …)).
 213 definition bin3 : binary_base_states ≝ mk_Sig ?? 3 (leb_true_to_le 4 6 (refl …)).
 214 definition bin4 : binary_base_states ≝ mk_Sig ?? 4 (leb_true_to_le 5 6 (refl …)).
 215 definition bin5 : binary_base_states ≝ mk_Sig ?? 5 (leb_true_to_le 6 6 (refl …)).
 216
 217 definition states_binaryTM : FinSet → FinSet → FinSet ≝ λsig,states.
 218  FinProd (FinProd states binary_base_states)
 219          (FinProd (FinOption sig) (initN (S (S (2 * (FS_crd sig)))))).
 220
 221 definition to_initN : ∀n,m.n < m → initN m ≝ λn,m,Hn.mk_Sig … n ….// qed.
 222
 223 definition initN_pred : ∀n.∀m:initN n.initN n ≝ λn,m.mk_Sig … (pred (pi1 … m)) ….
 224 cases m #m0 /2 by le_to_lt_to_lt/ qed.
 225
 226 definition displ_of_move ≝ λsig,mv.
 227   match mv with
 228   [ L ⇒ 2*FS_crd sig
 229   | N ⇒ FS_crd sig
 230   | R ⇒ O ].
 231
 232 lemma le_displ_of_move : ∀sig,mv.displ_of_move sig mv ≤ S (2*FS_crd sig).
 233 #sig * /2 by le_S/
 234 qed.
 235
 236 definition displ2_of_move ≝ λsig,mv.
 237   match mv with
 238   [ L ⇒ FS_crd sig
 239   | N ⇒ O
 240   | R ⇒ O ].
 241
 242 lemma le_displ2_of_move : ∀sig,mv.displ2_of_move sig mv ≤ S (2*FS_crd sig).
 243 #sig * /2 by lt_to_le/
 244 qed.
 245
 246 definition mv_tech ≝ λmv.match mv with [ N ⇒ N | _ ⇒ R ].
 247
 248 definition trans_binaryTM : ∀sig,states:FinSet.
 249   (states × (option sig) → states × (option sig) × move) →
 250   ((states_binaryTM sig states) × (option bool) →
 251    (states_binaryTM sig states) × (option bool) × move)
 252 ≝ λsig,states,trans,p.
 253   let 〈s,a〉 ≝ p in
 254   let 〈s0,phase,ch,count〉 ≝ s in
 255   let (H1 : O < S (S (2*FS_crd sig))) ≝ ? in
 256   let (H2 : FS_crd sig < S (S (2*FS_crd sig))) ≝ ? in
 257   match pi1 … phase with
 258   [ O ⇒ (*** PHASE 0: read ***)
 259       match pi1 … count with
 260       [ O ⇒ 〈〈s0,bin1,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
 261       | S k ⇒ match a with
 262         [ Some a0 ⇒ if (a0 == true)
 263                     then 〈〈s0,bin0,FS_nth sig k,initN_pred … count〉, None ?,R〉
 264                     else 〈〈s0,bin0,ch,initN_pred … count〉,None ?,R〉
 265         | None ⇒ (* Overflow position! *)
 266           let 〈s',a',mv〉 ≝ trans 〈s0,None ?〉 in
 267           match a' with
 268           [ 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〉
 269           | Some _ ⇒ (* maybe extend tape *) 〈〈s0,bin4,None ?,to_initN O ? H1〉,None ?,R〉 ] ] ]
 270   | S phase ⇒ match phase with
 271   [ O ⇒ (*** PHASE 1: restart ***)
 272       match pi1 … count with
 273       [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
 274       | S k ⇒ 〈〈s0,bin1,ch,initN_pred … count〉,None ?,L〉 ]
 275   | S phase ⇒ match phase with
 276   [ O ⇒ (*** PHASE 2: write ***)
 277       let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
 278       match pi1 … count with
 279       [ O ⇒ 〈〈s',bin3,ch,to_initN (displ_of_move sig mv) ??〉,None ?,N〉
 280       | S k ⇒ match a' with
 281          [ None ⇒ 〈〈s0,bin2,ch,initN_pred … count〉,None ?,R〉
 282          | Some a0' ⇒ let out ≝ (FS_nth ? k == a') in
 283                       〈〈s0,bin2,ch,initN_pred … count〉,Some ? out,R〉 ]
 284       ]
 285   | S phase ⇒ match phase with
 286   [ O ⇒ (*** PHASE 3: move head left ***)
 287       match pi1 … count with
 288       [ O ⇒ 〈〈s0,bin0,None ?,to_initN (FS_crd sig) ? H2〉, None ?,N〉 (* the end: restart *)
 289       | S k ⇒ 〈〈s0,bin3,ch,initN_pred … count〉, None ?,L〉 ]
 290   | S phase ⇒ match phase with
 291   [ O ⇒ (*** PHASE 4: check position ***)
 292       match a with
 293       [ None ⇒ (* niltape/rightof: we can write *) 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
 294       | Some _ ⇒ (* leftof *)
 295         let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
 296         match a' with
 297         [ None ⇒ (* (vacuous) go to end of 2 *) 〈〈s0,bin2,ch,to_initN 0 ? H1〉,None ?,N〉
 298         | Some _ ⇒ (* extend tape *) 〈〈s0,bin5,ch,to_initN (FS_crd sig) ? H2〉,None ?,L〉 ]
 299       ]
 300   | S _ ⇒ (*** PHASE 5: left extension ***)
 301       match pi1 … count with
 302       [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,R〉
 303       | S k ⇒ 〈〈s0,bin5,ch,initN_pred … count〉,Some ? false,L〉 ]]]]]].
 304 [ /2 by le_to_lt_to_lt/ | /2 by le_S_S/ |*: /2 by lt_S_to_lt/]
 305 qed.
 306
 307 definition halt_binaryTM : ∀sig,M.states_binaryTM sig (states sig M) → bool ≝
 308   λsig,M,s.let 〈s0,phase,ch,count〉 ≝ s in
 309   pi1 … phase == O ∧ halt sig M s0.
 310
 311 (*
 312  * Una mk_binaryTM prende in input una macchina M e produce una macchina che:
 313  * - ha per alfabeto FinBool
 314  * - ha stati di tipo ((states … M) × (initN 7)) ×
 315        ((option sig) × (initN (2*dimensione dell'alfabeto di M + 1))
 316  *   dove il primo elemento corrisponde allo stato della macchina input,
 317  *   il secondo identifica la fase (lettura, scrittura, spostamento)
 318  *   il terzo identifica il carattere oggetto letto
 319  *   il quarto è un contatore
 320  * - la funzione di transizione viene prodotta da trans_binaryTM
 321  * - la funzione di arresto viene prodotta da halt_binaryTM
 322  *)
 323 definition mk_binaryTM ≝
 324   λsig.λM:TM sig.
 325   mk_TM FinBool (states_binaryTM sig (states sig M))
 326     (trans_binaryTM sig (states sig M) (trans sig M))
 327     (〈start sig M,bin0,None ?,FS_crd sig〉) (halt_binaryTM sig M).
 328 /2 by lt_S_to_lt/ qed.
 329
 330 definition bin_list ≝ λsig,l.flatten ? (map ?? (bin_char sig) l).
 331 definition rev_bin_list ≝ λsig,l.flatten ? (map ?? (λc.reverse ? (bin_char sig c)) l).
 332
 333 definition tape_bin_lift ≝ λsig,t.
 334 let ls' ≝ rev_bin_list ? (left ? t) in
 335 let c' ≝ option_hd ? (opt_bin_char sig (current ? t)) in
 336 let rs' ≝ (tail ? (opt_bin_char sig (current ? t))@bin_list ? (right ? t)) in
 337  mk_tape ? ls' c' rs'.
 338
 339 definition state_bin_lift :
 340   ∀sig.∀M:TM sig.states sig M → states ? (mk_binaryTM ? M)
 341  ≝ λsig,M,q.〈q,bin0,None ?,FS_crd sig〉./2 by lt_S_to_lt/ qed.
 342
 343 lemma lift_halt_binaryTM :
 344   ∀sig,M,q.halt sig M q = halt ? (mk_binaryTM sig M) (state_bin_lift ? M q).
 345 // qed.
 346
 347 lemma binaryTM_bin0_bin1 :
 348   ∀sig,M,t,q,ch.
 349   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,O〉) t)
 350   = mk_config ?? (〈q,bin1,ch,to_initN (FS_crd sig) ??〉) t. //
 351 qed.
 352
 353 lemma binaryTM_bin0_bin3 :
 354   ∀sig,M,t,q,ch,k,qn,mv.
 355   current ? t = None ? → S k <S (2*FS_crd sig) →
 356   〈qn,None ?,mv〉 = trans sig M 〈q,None ?〉 →
 357   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t)
 358   = 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]
 359 #sig #M #t #q #ch #k #qn #mv #Hcur #Hk #Htrans
 360 whd in match (step ???); whd in match (trans ???);
 361 >Hcur <Htrans %
 362 qed.
 363
 364 lemma binaryTM_bin0_bin4 :
 365   ∀sig,M,t,q,ch,k,qn,chn,mv.
 366   current ? t = None ? → S k <S (2*FS_crd sig) →
 367   〈qn,Some ? chn,mv〉 = trans sig M 〈q,None ?〉 →
 368   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t)
 369   = mk_config ?? (〈q,bin4,None ?,to_initN 0 ??〉) (tape_move ? t R). [2,3:/2 by transitive_lt/]
 370 #sig #M #t #q #ch #k #qn #chn #mv #Hcur #Hk #Htrans
 371 whd in match (step ???); whd in match (trans ???);
 372 >Hcur <Htrans %
 373 qed.
 374
 375 lemma binaryTM_bin0_true :
 376   ∀sig,M,t,q,ch,k.
 377   current ? t = Some ? true → S k <S (2*FS_crd sig) →
 378   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t)
 379   = mk_config ?? (〈q,bin0,FS_nth sig k,to_initN k ??〉) (tape_move ? t R).[2,3:@le_S /2 by lt_S_to_lt/]
 380 #sig #M #t #q #ch #k #Hcur #Hk
 381 whd in match (step ???); whd in match (trans ???);
 382 >Hcur %
 383 qed.
 384
 385 lemma binaryTM_bin0_false :
 386   ∀sig,M,t,q,ch,k.
 387   current ? t = Some ? false → S k <S (2*FS_crd sig) →
 388   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t)
 389   = mk_config ?? (〈q,bin0,ch,to_initN k ??〉) (tape_move ? t R).[2,3:@le_S /2 by lt_S_to_lt/]
 390 #sig #M #t #q #ch #k #Hcur #Hk
 391 whd in match (step ???); whd in match (trans ???);
 392 >Hcur %
 393 qed.
 394
 395 lemma binaryTM_phase0_midtape_aux :
 396   ∀sig,M,q,ls,a,rs,k.
 397   halt sig M q=false →
 398   ∀csr,csl,t,ch.length ? csr < S (2*FS_crd sig) →
 399   t = mk_tape ? (reverse ? csl@ls) (option_hd ? (csr@rs)) (tail ? (csr@rs)) →
 400   csl@csr = bin_char sig a →
 401   |csl@csr| = FS_crd sig →
 402   (|csr| ≤ index_of_FS ? a → ch = Some ? a) →
 403   loopM ? (mk_binaryTM sig M) (S (length ? csr) + k)
 404     (mk_config ?? (〈q,bin0,ch,length ? csr〉) t)
 405   = loopM ? (mk_binaryTM sig M) k
 406       (mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉)
 407         (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [2,3:@le_S /2 by O/]
 408 #sig #M #q #ls #a #rs #k #Hhalt #csr elim csr
 409 [ #csl #t #ch #Hlen #Ht >append_nil #Hcsl #Hlencsl #Hch >loopM_unfold >loop_S_false [|normalize //]
 410   >Hch [| >Hlencsl // ]
 411   <loopM_unfold @eq_f >binaryTM_bin0_bin1 @eq_f >Ht
 412   whd in match (step ???); whd in match (trans ???); <Hcsl %
 413 | #c cases c
 414   [ #csr0 #IH #csl #t #ch #Hlen #Ht #Heq #Hcrd #Hch >loopM_unfold >loop_S_false [|normalize //]
 415     <loopM_unfold lapply (binary_to_bin_char … Heq) #Ha >binaryTM_bin0_true
 416     [| >Ht % ]
 417     lapply (IH (csl@[true]) (tape_move FinBool t R) ??????)
 418     [ //
 419     | >associative_append @Hcrd
 420     | >associative_append @Heq
 421     | >Ht whd in match (option_hd ??) in ⊢ (??%?); whd in match (tail ??) in ⊢ (??%?);
 422       cases csr0
 423       [ cases rs
 424         [ normalize >rev_append_def >rev_append_def >reverse_append %
 425         | #r1 #rs1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 426       | #c1 #csr1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 427     | /2 by lt_S_to_lt/
 428     |]
 429     #H whd in match (plus ??); >Ha >H @eq_f @eq_f2 %
 430   | #csr0 #IH #csl #t #ch #Hlen #Ht #Heq #Hcrd #Hch >loopM_unfold >loop_S_false [|normalize //]
 431     <loopM_unfold >binaryTM_bin0_false [| >Ht % ]
 432     lapply (IH (csl@[false]) (tape_move FinBool t R) ??????)
 433     [6: @ch
 434     | #Hle cases (le_to_or_lt_eq … Hle) [ @Hch ]
 435       #Hindex lapply (bin_char_FS_nth … (sym_eq … Heq)) >Hindex
 436       >(nth_index_of_FS sig a) >(\b (refl ? (Some sig a))) #H destruct (H)
 437     | >associative_append @Hcrd
 438     | >associative_append @Heq
 439     | >Ht whd in match (option_hd ??) in ⊢ (??%?); whd in match (tail ??) in ⊢ (??%?);
 440       cases csr0
 441       [ cases rs
 442         [ normalize >rev_append_def >rev_append_def >reverse_append %
 443         | #r1 #rs1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 444       | #c1 #csr1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 445     | /2 by lt_S_to_lt/
 446     |]
 447     #H whd in match (plus ??); >H @eq_f @eq_f2 %
 448   ]
 449 ]
 450 qed.
 451
 452 lemma binaryTM_phase0_midtape :
 453   ∀sig,M,t,q,ls,a,rs,ch.
 454   O < FS_crd sig →
 455   halt sig M q=false →
 456   t = mk_tape ? ls (option_hd ? (bin_char ? a)) (tail ? (bin_char sig a)@rs) →
 457   ∀k.S (FS_crd sig) ≤ k →
 458   loopM ? (mk_binaryTM sig M) k
 459     (mk_config ?? (〈q,bin0,ch,FS_crd sig〉) t)
 460   = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
 461       (mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉)
 462         (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [|*:@le_S //]
 463 #sig #M #t #q #ls #a #rs #ch #Hcrd #Hhalt #Ht #k #Hk
 464 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >(minus_tech (S (FS_crd sig)))
 465 cut (∃c,cl.bin_char sig a = c::cl)
 466 [ lapply (refl ? (|bin_char ? a|)) >eq_length_bin_char_FS_crd in ⊢ (???%→?);
 467   cases (bin_char ? a) [|/3 by ex_intro/] normalize in ⊢ (??%?→?); #H
 468   <H in Hcrd; -H #H cases (not_le_Sn_O O) #Hfalse cases (Hfalse H) ]
 469 * #c * #cl #Ha >Ha
 470 cut (FS_crd sig = |bin_char sig a|) [/2 by plus_minus_m_m/] #Hlen
 471 @(trans_eq ?? (loopM ? (mk_binaryTM ? M) (S (|c::cl|) + k0)
 472    (mk_config ?? 〈q,bin0,〈ch,|c::cl|〉〉 t)))
 473 [ @le_S_S <Ha <Hlen // | @eq_f2 // @eq_f2 // @eq_f <Ha >Hlen % ]
 474 >(binaryTM_phase0_midtape_aux ? M q ls a rs ? ? (c::cl) [ ] t ch) //
 475 [| <Ha <Hlen lapply (lt_FS_index_crd sig a) #Hlt #Hle
 476    lapply (transitive_le ??? Hlt Hle) #H cases (not_le_Sn_n (index_of_FS ? a))
 477    #H1 @False_ind /2/
 478 | <Ha >Hlen %
 479 | >Ha %
 480 | >Ht >Ha %
 481 | <Ha <Hlen // ]
 482 <Ha %
 483 qed.
 484
 485 lemma binaryTM_phase0_None_None :
 486   ∀sig,M,t,q,ch,n,qn,mv.
 487   O < n →  n < 2*FS_crd sig →
 488   halt sig M q=false →
 489   current ? t = None ? →
 490   〈qn,None ?,mv〉 = trans sig M 〈q,None ?〉 →
 491   ∀k.O < k →
 492   loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin0,ch,n〉) t)
 493   = loopM ? (mk_binaryTM sig M) (k-1)
 494       (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]
 495 #sig #M #t #q #ch #n #qn #mv #HOn #Hn #Hhalt #Hcur #Htrans #k #Hk
 496 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 497 cases (le_to_eq … HOn) #n0 #Hn0 destruct (Hn0)
 498 lapply Htrans lapply Hcur -Htrans -Hcur cases t
 499 [ >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin3 //
 500 | #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin3 //
 501 | #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin3 //
 502 | #ls #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
 503 qed.
 504
 505 lemma binaryTM_phase0_None_Some :
 506   ∀sig,M,t,q,ch,n,qn,chn,mv.
 507   O < n →  n < 2*FS_crd sig →
 508   halt sig M q=false →
 509   current ? t = None ? →
 510   〈qn,Some ? chn,mv〉 = trans sig M 〈q,None ?〉 →
 511   ∀k.O < k →
 512   loopM ? (mk_binaryTM sig M) k (mk_config ?? (〈q,bin0,ch,n〉) t)
 513   = loopM ? (mk_binaryTM sig M) (k-1)
 514       (mk_config ?? (〈q,bin4,None ?,to_initN O ??〉) (tape_move ? t R)). [2,3: /2 by transitive_lt/ ]
 515 #sig #M #t #q #ch #n #qn #chn #mv #HOn #Hn #Hhalt #Hcur #Htrans #k #Hk
 516 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 517 cases (le_to_eq … HOn) #n0 #Hn0 destruct (Hn0)
 518 lapply Htrans lapply Hcur -Hcur -Htrans cases t
 519 [ >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/
 520 | #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/
 521 | #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] #Hcur #Htrans >binaryTM_bin0_bin4 // /2 by refl, transitive_lt/
 522 | #ls #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
 523 qed.
 524
 525 lemma binaryTM_bin1_O :
 526   ∀sig,M,t,q,ch.
 527   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin1,ch,O〉) t)
 528   = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t. [2,3:/2 by lt_S_to_lt/]
 529 #sig #M #t #q #ch %
 530 qed.
 531
 532 lemma binaryTM_bin1_S :
 533   ∀sig,M,t,q,ch,k. S k <S (2*FS_crd sig) →
 534   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin1,ch,S k〉) t)
 535   = mk_config ?? (〈q,bin1,ch,to_initN k ??〉) (tape_move ? t L). [2,3:@le_S /2 by lt_S_to_lt/]
 536 #sig #M #t #q #ch #k #HSk %
 537 qed.
 538
 539 lemma binaryTM_phase1 :
 540   ∀sig,M,q,ls1,ls2,cur,rs,ch.
 541   |ls1| = FS_crd sig → (cur = None ? → rs = [ ]) →
 542   ∀k.S (FS_crd sig) ≤ k →
 543   loopM ? (mk_binaryTM sig M) k
 544     (mk_config ?? (〈q,bin1,ch,FS_crd sig〉) (mk_tape ? (ls1@ls2) cur rs))
 545   = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
 546       (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
 547         (mk_tape ? ls2 (option_hd ? (reverse ? ls1@option_cons ? cur rs))
 548           (tail ? (reverse ? ls1@option_cons ? cur rs)))). [2,3:/2 by O/]
 549 cut (∀sig,M,q,ls1,ls2,ch,k,n,cur,rs.
 550   |ls1| = n →  n<S (2*FS_crd sig) → (cur = None ? → rs = [ ]) →
 551   loopM ? (mk_binaryTM sig M) (S n + k)
 552     (mk_config ?? (〈q,bin1,ch,n〉) (mk_tape ? (ls1@ls2) cur rs))
 553   = loopM ? (mk_binaryTM sig M) k
 554       (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
 555         (mk_tape ? ls2 (option_hd ? (reverse ? ls1@option_cons ? cur rs))
 556           (tail ? (reverse ? ls1@option_cons ? cur rs))))) [1,2:@le_S //]
 557 [ #sig #M #q #ls1 #ls2 #ch #k elim ls1
 558   [ #n normalize in ⊢ (%→?); #cur #rs #Hn <Hn #Hcrd #Hcur >loopM_unfold >loop_S_false [| % ]
 559     >binaryTM_bin1_O cases cur in Hcur;
 560     [ #H >(H (refl ??)) -H %
 561     | #cur' #_ % ]
 562   | #l0 #ls0 #IH * [ #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
 563     #n #cur #rs normalize in ⊢ (%→?); #H destruct (H) #Hlt #Hcur
 564     >loopM_unfold >loop_S_false [|%] >binaryTM_bin1_S
 565     <(?:mk_tape ? (ls0@ls2) (Some ? l0) (option_cons ? cur rs) =
 566         tape_move FinBool (mk_tape FinBool ((l0::ls0)@ls2) cur rs) L)
 567     [| cases cur in Hcur; [ #H >(H ?) // | #cur' #_ % ] ]
 568     >(?:loop (config FinBool (states FinBool (mk_binaryTM sig M))) (S (|ls0|)+k)
 569       (step FinBool (mk_binaryTM sig M))
 570       (λc:config FinBool (states FinBool (mk_binaryTM sig M))
 571        .halt FinBool (mk_binaryTM sig M)
 572        (cstate FinBool (states FinBool (mk_binaryTM sig M)) c))
 573       (mk_config FinBool (states FinBool (mk_binaryTM sig M))
 574        〈q,bin1,ch,to_initN (|ls0|) ?
 575         (le_S ?? (lt_S_to_lt (|ls0|) (S (2*FS_crd sig)) Hlt))〉
 576        (mk_tape FinBool (ls0@ls2) (Some FinBool l0) (option_cons FinBool cur rs)))
 577       = loopM FinBool (mk_binaryTM sig M) k
 578          (mk_config FinBool (states FinBool (mk_binaryTM sig M))
 579           〈q,bin2,〈ch,FS_crd sig〉〉
 580           (mk_tape FinBool ls2
 581            (option_hd FinBool (reverse FinBool ls0@l0::option_cons FinBool cur rs))
 582            (tail FinBool (reverse FinBool ls0@l0::option_cons FinBool cur rs)))))
 583     [| /2/
 584     | >(?: l0::option_cons ? cur rs = option_cons ? (Some ? l0) (option_cons ? cur rs)) [| % ]
 585       @trans_eq [|| @(IH ??? (refl ??)) [ /2 by lt_S_to_lt/ | #H destruct (H) ] ]
 586       %
 587     ]
 588    >reverse_cons >associative_append %
 589  ]
 590 | #Hcut #sig #M #q #ls1 #ls2 #cur #rs #ch #Hlen #Hcur #k #Hk
 591   cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech @Hcut /2/ ]
 592 qed.
 593
 594 lemma binaryTM_bin2_O :
 595   ∀sig,M,t,q,qn,ch,chn,mv.
 596   〈qn,chn,mv〉 = trans sig M 〈q,ch〉 →
 597   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,O〉) t)
 598   = mk_config ?? (〈qn,bin3,ch,to_initN (displ_of_move sig mv) ??〉) t.[2,3:/2 by lt_S_to_lt,le_S_S/]
 599 #sig #M #t #q #qn #ch #chn #mv #Htrans
 600 whd in match (step ???); whd in match (trans ???); <Htrans %
 601 qed.
 602
 603 lemma binaryTM_bin2_S_None :
 604   ∀sig,M,t,q,qn,ch,mv,k.
 605   k < S (2*FS_crd sig) →
 606   〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 →
 607   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,S k〉) t)
 608   = mk_config ?? (〈q,bin2,ch,k〉) (tape_move ? t R).
 609 [2,3: @le_S_S /2 by lt_to_le/ ]
 610 #sig #M #t #q #qn #ch #mv #k #Hk #Htrans
 611 whd in match (step ???); whd in match (trans ???); <Htrans %
 612 qed.
 613
 614 lemma binaryTM_bin2_S_Some :
 615   ∀sig,M,t,q,qn,ch,chn,mv,k.
 616   k< S (2*FS_crd sig) →
 617   〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
 618   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,S k〉) t)
 619   = mk_config ?? (〈q,bin2,ch,k〉) (tape_move ? (tape_write ? t (Some ? (FS_nth ? k == Some ? chn))) R).
 620 [2,3: @le_S_S /2 by lt_to_le/ ]
 621 #sig #M #t #q #qn #ch #chn #mv #k #Hk #Htrans
 622 whd in match (step ???); whd in match (trans ???); <Htrans %
 623 qed.
 624
 625 let rec iter (T:Type[0]) f n (t:T) on n ≝
 626   match n with [ O ⇒ t | S n0 ⇒ iter T f n0 (f t) ].
 627
 628 lemma binaryTM_phase2_None :∀sig,M,q,ch,qn,mv.
 629   〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 →
 630   ∀n.n≤S (2*FS_crd sig) →
 631   ∀t,k.S n ≤ k →
 632   loopM ? (mk_binaryTM sig M) k
 633     (mk_config ?? (〈q,bin2,ch,n〉) t)
 634   = loopM ? (mk_binaryTM sig M) (k - S n)
 635       (mk_config ?? (〈qn,bin3,ch,to_initN (displ_of_move sig mv) ??〉)
 636         (iter ? (λt0.tape_move ? t0 R) n t)). [2,3: @le_S_S /2 by lt_S_to_lt/]
 637 #sig #M #q #ch #qn #mv #Htrans #n #Hn #t #k #Hk
 638 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech lapply Hn lapply t -Hn -t
 639 elim n
 640 [ #t #Hle >loopM_unfold >loop_S_false //
 641   >(binaryTM_bin2_O … Htrans) //
 642 | #n0 #IH #t #Hn0 >loopM_unfold >loop_S_false //
 643   >(binaryTM_bin2_S_None … Htrans) @(trans_eq ???? (IH …)) //
 644 ]
 645 qed.
 646
 647 lemma binaryTM_phase2_Some_of : ∀sig,M,q,ch,qn,chn,mv,ls.
 648   〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
 649   ∀k.S (FS_crd sig) ≤ k →
 650   loopM ? (mk_binaryTM sig M) k
 651     (mk_config ?? (〈q,bin2,ch,FS_crd sig〉) (mk_tape ? ls (None ?) [ ]))
 652   = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
 653       (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
 654         (mk_tape ? (reverse ? (bin_char sig chn)@ls) (None ?) [ ])). [2,3:@le_S_S //]
 655 cut (∀sig,M,q,ch,qn,chn,mv,ls,k,n.
 656   S n ≤ k → 〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
 657   ∀csl. n <S (2*FS_crd sig) →
 658   |csl| + n = FS_crd sig →
 659   (∃fs.bin_char sig chn = reverse ? csl@fs) →
 660   loopM ? (mk_binaryTM sig M) k
 661     (mk_config ?? (〈q,bin2,ch,n〉) (mk_tape ? (csl@ls) (None ?) [ ]))
 662   = loopM ? (mk_binaryTM sig M) (k - S n)
 663       (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
 664         (mk_tape ? (reverse ? (bin_char sig chn)@ls) (None ?) [ ]))) [1,2:@le_S_S //]
 665 [ #sig #M #q #ch #qn #chn #mv #ls #k #n #Hk
 666   cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 667   #Htrans elim n
 668   [ #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // <loopM_unfold
 669     cut (fs = [ ])
 670     [ cases fs in Hfs; // #f0 #fs0 #H lapply (eq_f ?? (length ?) … H)
 671       >length_append >(?:|bin_char sig chn| = FS_crd sig) [|//]
 672       <Hcrd >length_reverse #H1 cut (O = |f0::fs0|) [ /2/ ]
 673       normalize #H1 destruct (H1) ]
 674     #H destruct (H) >append_nil in Hfs; #Hfs
 675     >Hfs >reverse_reverse >(binaryTM_bin2_O … Htrans) //
 676   | #n0 #IH #csl #Hcount #Hcrd * #fs #Hfs
 677     >loopM_unfold >loop_S_false // <loopM_unfold
 678     >(?: step FinBool (mk_binaryTM sig M)
 679          (mk_config FinBool (states FinBool (mk_binaryTM sig M)) 〈q,bin2,〈ch,S n0〉〉
 680          (mk_tape FinBool (csl@ls) (None FinBool) []))
 681         = mk_config ?? (〈q,bin2,ch,n0〉)
 682           (tape_move ? (tape_write ?
 683             (mk_tape ? (csl@ls) (None ?) [ ]) (Some ? (FS_nth ? n0 == Some ? chn))) R))
 684     [| /2 by lt_S_to_lt/ | @(binaryTM_bin2_S_Some … Htrans) ]
 685     >(?: tape_move ? (tape_write ???) ? =
 686           mk_tape ? (((FS_nth ? n0 == Some sig chn)::csl)@ls) (None ?) [ ])
 687     [| cases csl // cases ls // ]
 688     cases fs in Hfs;
 689     [ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ]
 690       -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|//]
 691       <Hcrd in ⊢ (%→?); >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
 692       #Hfalse cut (S n0 = O) /2 by injective_plus_r/ #H destruct (H)
 693     | #f0 #fs0 #Hbinchar
 694       cut (bin_char ? chn = reverse ? csl@(FS_nth ? n0 == Some ? chn)::fs0)
 695       [ >Hbinchar >(bin_char_FS_nth … Hbinchar) >(?:|fs0|=n0) //
 696         <(eq_length_bin_char_FS_crd sig chn) in Hcrd; >Hbinchar
 697         >length_append >length_reverse whd in ⊢ (???(??%)→?); /2 by injective_S/ ]
 698       -Hbinchar #Hbinchar >Hbinchar @(trans_eq ???? (IH …)) //
 699       [ %{fs0} >reverse_cons >associative_append @Hbinchar
 700       | whd in ⊢ (??%?); <Hcrd // ]
 701       @eq_f @eq_f @eq_f3 //
 702     ]
 703   ]
 704 | #Hcut #sig #M #q #ch #qn #chn #mv #ls #Htrans #k #Hk
 705   @trans_eq
 706   [3: @(trans_eq ???? (Hcut ??????? ls ? (FS_crd sig) ? Htrans …)) //
 707     [3:@([ ]) | %{(bin_char ? chn)} % | % ]
 708   || % ]
 709 ]
 710 qed.
 711
 712 lemma binaryTM_phase2_Some_ow : ∀sig,M,q,ch,qn,chn,mv,ls,cs,rs.
 713   〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
 714   |cs| = FS_crd sig →
 715   ∀k.S (FS_crd sig) ≤ k →
 716   loopM ? (mk_binaryTM sig M) k
 717     (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
 718       (mk_tape ? ls (option_hd ? (cs@rs)) (tail ? (cs@rs))))
 719   = loopM ? (mk_binaryTM sig M) (k - S (FS_crd sig))
 720       (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
 721         (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs))). [2,3:@le_S_S /2 by O/]
 722 cut (∀sig,M,q,ch,qn,chn,mv,ls,rs,k,csr.
 723      〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
 724      ∀csl.|csr|<S (2*FS_crd sig) →
 725      |csl@csr| = FS_crd sig →
 726      (∃fs.bin_char sig chn = reverse ? csl@fs) →
 727      loopM ? (mk_binaryTM sig M) (S (|csr|) + k)
 728        (mk_config ?? (〈q,bin2,ch,|csr|〉)
 729          (mk_tape ? (csl@ls) (option_hd ? (csr@rs)) (tail ? (csr@rs))))
 730      = loopM ? (mk_binaryTM sig M) k
 731          (mk_config ?? (〈qn,bin3,ch,displ_of_move sig mv〉)
 732            (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/] ]
 733 [ #sig #M #q #ch #qn #chn #mv #ls #rs #k #csr #Htrans elim csr
 734   [ #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // normalize in match (length ? [ ]);
 735     >(binaryTM_bin2_O … Htrans) <loopM_unfold @eq_f @eq_f @eq_f3 //
 736     cases fs in Hfs; // #f0 #fs0 #H lapply (eq_f ?? (length ?) … H)
 737     >length_append >(?:|bin_char sig chn| = FS_crd sig) [|//]
 738     <Hcrd >length_reverse >length_append whd in match (|[]|); #H1 cut (O = |f0::fs0|) [ /2 by plus_to_minus/ ]
 739     normalize #H1 destruct (H1)
 740   | #b0 #bs0 #IH #csl #Hcount #Hcrd * #fs #Hfs
 741     >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_Some … Htrans)
 742     >(?: tape_move ? (tape_write ???) ? =
 743           mk_tape ? (((FS_nth ? (|bs0|)==Some sig chn)::csl)@ls)
 744             (option_hd ? (bs0@rs)) (tail ? (bs0@rs)))
 745       in match (tape_move ? (tape_write ???) ?);
 746     [| cases bs0 // cases rs // ] @IH
 747     [ <Hcrd >length_append >length_append normalize //
 748     | cases fs in Hfs;
 749       [ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ]      -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|//]
 750         <Hcrd >length_append normalize >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
 751         #Hfalse cut (S (|bs0|) = O) /2 by injective_plus_r/ #H destruct (H)
 752       | #f0 #fs0 #Hbinchar
 753         cut (bin_char ? chn = reverse ? csl@(FS_nth ? (|bs0|) == Some ? chn)::fs0)
 754         [ >Hbinchar >(bin_char_FS_nth … Hbinchar) >(?:|fs0|=|bs0|) //
 755           <(eq_length_bin_char_FS_crd sig chn) in Hcrd; >Hbinchar
 756           >length_append >length_append >length_reverse
 757           whd in ⊢ (??(??%)(??%)→?); /2 by injective_S/ ]
 758         -Hbinchar #Hbinchar >Hbinchar %{fs0} >reverse_cons >associative_append %
 759       ]
 760     ]
 761   ]
 762 | #Hcut #sig #M #q #ch #qn #chn #mv #ls #cs #rs #Htrans #Hcrd #k #Hk
 763   cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >(?:S (FS_crd sig) +k0-S (FS_crd sig) = k0) [|@minus_tech]
 764   @trans_eq
 765   [3: @(trans_eq ???? (Hcut ??????? ls ?? cs Htrans [ ] …)) //
 766     [ normalize % // | normalize @Hcrd | >Hcrd // ]
 767   || @eq_f2 [ >Hcrd % | @eq_f2 // @eq_f cases Hcrd // ] ] ]
 768 qed.
 769
 770 lemma binaryTM_bin3_O :
 771   ∀sig,M,t,q,ch.
 772   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin3,ch,O〉) t)
 773   = mk_config ?? (〈q,bin0,None ?,to_initN (FS_crd sig) ??〉) t. [2,3:@le_S //]
 774 #sig #M #t #q #ch %
 775 qed.
 776
 777 lemma binaryTM_bin3_S :
 778   ∀sig,M,t,q,ch,k. S k ≤ S (2*FS_crd sig) →
 779   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin3,ch,S k〉) t)
 780   = mk_config ?? (〈q,bin3,ch,to_initN k ??〉) (tape_move ? t L). [2,3: @le_S_S /2 by lt_to_le/]
 781 #sig #M #t #q #ch #k #HSk %
 782 qed.
 783
 784 lemma binaryTM_phase3 :∀sig,M,q,ch,n.
 785   n ≤ S (2*FS_crd sig) →
 786   ∀t,k.S n ≤ k →
 787   loopM ? (mk_binaryTM sig M) k
 788     (mk_config ?? (〈q,bin3,ch,n〉) t)
 789   = loopM ? (mk_binaryTM sig M) (k - S n)
 790       (mk_config ?? (〈q,bin0,None ?,FS_crd sig〉)
 791         (iter ? (λt0.tape_move ? t0 L) n t)). [2,3: /2 by lt_S_to_lt, le_to_lt_to_lt/]
 792 #sig #M #q #ch #n #Hcrd #t #k #Hk
 793 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >(minus_tech (S n) k0)
 794 lapply t lapply Hcrd -t -Hcrd elim n
 795 [ #Hcrd #t >loopM_unfold >loop_S_false [| % ] >binaryTM_bin3_O //
 796 | #n0 #IH #Hlt #t >loopM_unfold >loop_S_false [|%] >binaryTM_bin3_S [|@Hlt]
 797   <IH [|@lt_to_le @Hlt ]
 798   <loopM_unfold % ]
 799 qed.
 800
 801 lemma binaryTM_bin4_None :
 802   ∀sig,M,t,q,ch.
 803   current ? t = None ? →
 804   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
 805   = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t. [|@le_S_S @le_O_n | @le_S_S // ]
 806 #sig #M #t #q #ch #Hcur whd in ⊢ (??%?); >Hcur %
 807 qed.
 808
 809 lemma binaryTM_phase4_write : ∀sig,M,q,ch,t.current ? t = None ? →
 810   ∀k.O < k →
 811   loopM ? (mk_binaryTM sig M) k
 812     (mk_config ?? (〈q,bin4,ch,O〉) t)
 813   = loopM ? (mk_binaryTM sig M) (k-1)
 814       (mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t). [|@le_S_S @le_O_n|@le_S_S //]
 815 #sig #M #q #ch #t #Hcur #k #Hk
 816 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 817 >loopM_unfold >loop_S_false // <loopM_unfold >binaryTM_bin4_None [|//] %
 818 qed.
 819
 820 (* we don't get here any more! *
 821 lemma binaryTM_bin4_noextend :
 822   ∀sig,M,t,q,ch,cur,qn,mv.
 823   current ? t = Some ? cur →
 824   〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 →
 825   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
 826   = mk_config ?? (〈q,bin2,ch,to_initN O ??〉) t. [2,3://]
 827 #sig #M #t #q #ch #cur #qn #mv #Hcur #Htrans
 828 whd in ⊢ (??%?); >Hcur whd in ⊢ (??%?);
 829 whd in match (trans FinBool ??); <Htrans %
 830 qed.
 831 *)
 832
 833 lemma binaryTM_bin4_extend :
 834   ∀sig,M,t,q,ch,cur,qn,an,mv.
 835   current ? t = Some ? cur →
 836   〈qn,Some ? an,mv〉 = trans sig M 〈q,ch〉 →
 837   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
 838   = mk_config ?? (〈q,bin5,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t L). [2,3:@le_S //]
 839 #sig #M #t #q #ch #cur #qn #an #mv #Hcur #Htrans
 840 whd in ⊢ (??%?); >Hcur whd in ⊢ (??%?);
 841 whd in match (trans FinBool ??); <Htrans %
 842 qed.
 843
 844 lemma binaryTM_phase4_extend : ∀sig,M,q,ch,t,cur,qn,an,mv.
 845   current ? t = Some ? cur → 〈qn,Some ? an,mv〉 = trans sig M 〈q,ch〉 →
 846   ∀k.O < k →
 847   loopM ? (mk_binaryTM sig M) k
 848     (mk_config ?? (〈q,bin4,ch,O〉) t)
 849   = loopM ? (mk_binaryTM sig M) (k-1)
 850       (mk_config ?? (〈q,bin5,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t L)). [2,3: @le_S //]
 851 #sig #M #q #ch #t #cur #qn #an #mv #Hcur #Htrans #k #Hk
 852 cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech
 853 >loopM_unfold >loop_S_false // <loopM_unfold >(binaryTM_bin4_extend … Hcur) [|*://] %
 854 qed.
 855
 856 lemma binaryTM_bin5_O :
 857   ∀sig,M,t,q,ch.
 858   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin5,ch,O〉) t)
 859   = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t R). [2,3:@le_S //]
 860 #sig #M #t #q #ch %
 861 qed.
 862
 863 lemma binaryTM_bin5_S :
 864   ∀sig,M,t,q,ch,k. S k <S (2*FS_crd sig) →
 865   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin5,ch,S k〉) t)
 866   = 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/]
 867 #sig #M #t #q #ch #k #HSk %
 868 qed.
 869
 870 (* extends the tape towards the left with an unimportant sequence that will be
 871    immediately overwritten *)
 872 lemma binaryTM_phase5 :∀sig,M,q,ch,n.
 873   ∀rs.n<S (2*FS_crd sig) →
 874   ∃bs.|bs| = n ∧
 875   ∀k.S n ≤ k →
 876   loopM ? (mk_binaryTM sig M) k
 877     (mk_config ?? (〈q,bin5,ch,n〉) (mk_tape ? [] (None ?) rs))
 878   = loopM ? (mk_binaryTM sig M) (k - S n)
 879       (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
 880         (mk_tape ? [] (option_hd ? (bs@rs)) (tail ? (bs@rs)))). [2,3:@le_S //]
 881 #sig #M #q #ch #n elim n
 882 [ #rs #Hlt %{[]} % // #k #Hk cases (le_to_eq … Hk) #k0 #Hk0 >Hk0 >minus_tech -Hk0
 883   cases rs //
 884 | #n0 #IH #rs #Hn0 cases (IH (false::rs) ?) [|/2 by lt_S_to_lt/]
 885   #bs * #Hbs -IH #IH %{(bs@[false])} % [ <Hbs >length_append /2 by increasing_to_injective/ ]
 886   #k #Hk cases (le_to_eq … Hk) #k0 #Hk0 >Hk0
 887   >loopM_unfold >loop_S_false // >binaryTM_bin5_S
 888   >associative_append normalize in match ([false]@?); <(IH (S n0 + k0)) [|//]
 889   >loopM_unfold @eq_f @eq_f cases rs //
 890 ]
 891 qed.
 892
 893 lemma current_None_or_midtape :
 894   ∀sig,t.current sig t = None sig ∨ ∃ls,c,rs.t = midtape sig ls c rs.
 895 #sig * normalize /2/ #ls #c #rs %2 /4 by ex_intro/
 896 qed.
 897
 898 lemma state_bin_lift_unfold :
 899   ∀sig.∀M:TM sig.∀q:states sig M.
 900   state_bin_lift sig M q = 〈q,bin0,None ?,FS_crd sig〉.// qed.
 901
 902 axiom current_tape_bin_list :
 903  ∀sig,t.current sig t = None ? → current ? (tape_bin_lift sig t) = None ?.
 904
 905 lemma tape_bin_lift_unfold :
 906  ∀sig,t. tape_bin_lift sig t =
 907  mk_tape ? (rev_bin_list ? (left ? t)) (option_hd ? (opt_bin_char sig (current ? t)))
 908    (tail ? (opt_bin_char sig (current ? t))@bin_list ? (right ? t)). //
 909 qed.
 910
 911 lemma reverse_bin_char_list : ∀sig,c,l.
 912   reverse ? (bin_char sig c)@rev_bin_list ? l = rev_bin_list ? (c::l). // qed.
 913
 914 lemma left_midtape : ∀sig,ls,c,rs.left ? (midtape sig ls c rs) = ls.// qed.
 915 lemma current_midtape : ∀sig,ls,c,rs.current ? (midtape sig ls c rs) = Some ? c.// qed.
 916 lemma right_midtape : ∀sig,ls,c,rs.right ? (midtape sig ls c rs) = rs.// qed.
 917 lemma opt_bin_char_Some : ∀sig,c.opt_bin_char sig (Some ? c) = bin_char ? c.// qed.
 918
 919 lemma opt_cons_hd_tl : ∀A,l.option_cons A (option_hd ? l) (tail ? l) = l.
 920 #A * // qed.
 921
 922 lemma le_tech : ∀a,b,c.a ≤ b → a * c ≤ b * c.
 923 #a #b #c #H /2 by monotonic_le_times_r/
 924 qed.
 925
 926 lemma iter_split : ∀T,f,m,n,x.
 927   iter T f (m+n) x = iter T f m (iter T f n x).
 928 #T #f #m #n elim n /2/
 929 #n0 #IH #x <plus_n_Sm whd in ⊢ (??%(????%)); >IH %
 930 qed.
 931
 932 lemma iter_O : ∀T,f,x.iter T f O x = x.// qed.
 933
 934 lemma iter_tape_move_R : ∀T,n,ls,cs,rs.|cs| = n →
 935   iter ? (λt0.tape_move T t0 R) n (mk_tape ? ls (option_hd ? (cs@rs)) (tail ? (cs@rs)))
 936   = mk_tape ? (reverse ? cs@ls) (option_hd ? rs) (tail ? rs).
 937 #T #n elim n
 938 [ #ls * [| #c0 #cs0 #rs #H normalize in H; destruct (H) ] #rs #_ %
 939 | #n0 #IH #ls * [ #rs #H normalize in H; destruct (H) ] #c #cs #rs #Hlen
 940   whd in ⊢ (??%?);
 941   >(?: (tape_move T (mk_tape T ls (option_hd T ((c::cs)@rs)) (tail T ((c::cs)@rs))) R)
 942     = mk_tape ? (c::ls) (option_hd ? (cs@rs)) (tail ? (cs@rs))) in ⊢ (??(????%)?);
 943   [| cases cs // cases rs // ] >IH
 944   [ >reverse_cons >associative_append %
 945   | normalize in Hlen; destruct (Hlen) % ]
 946 ]
 947 qed.
 948
 949 lemma tail_tech : ∀T,l1,l2.O < |l1| → tail T (l1@l2) = tail ? l1@l2.
 950 #T * normalize // #l2 #Hfalse @False_ind cases (not_le_Sn_O O) /2/
 951 qed.
 952
 953 lemma hd_tech : ∀T,l1,l2.O < |l1| → option_hd T (l1@l2) = option_hd ? l1.
 954 #T * normalize // #l2 #Hfalse @False_ind cases (not_le_Sn_O O) /2/
 955 qed.
 956
 957 lemma iter_tape_move_L_nil : ∀T,n,rs.
 958   iter ? (λt0.tape_move T t0 L) n (mk_tape ? [ ] (None ?) rs) =
 959   mk_tape ? [ ] (None ?) rs.
 960 #T #n #rs elim n // #n0 #IH <IH in ⊢ (???%); cases rs //
 961 qed.
 962
 963 lemma iter_tape_move_R_nil : ∀T,n,ls.
 964   iter ? (λt0.tape_move T t0 R) n (mk_tape ? ls (None ?) [ ]) =
 965   mk_tape ? ls (None ?) [ ].
 966 #T #n #ls elim n // #n0 #IH <IH in ⊢ (???%); cases ls //
 967 qed.
 968
 969 lemma iter_tape_move_L_left : ∀T,n,cs,rs. O < n →
 970   iter ? (λt0.tape_move T t0 L) n
 971     (mk_tape ? [ ] (option_hd ? cs) (tail ? cs@rs)) =
 972   mk_tape ? [ ] (None ?) (cs@rs).
 973 #T #n #cs #rs *
 974 [ cases cs // cases rs //
 975 | #m #_ whd in ⊢ (??%?); <(iter_tape_move_L_nil ? m) cases cs // cases rs // ]
 976 qed.
 977
 978 lemma iter_tape_move_L : ∀T,n,ls,cs,rs.|cs| = n →
 979   iter ? (λt0.tape_move T t0 L) n (mk_tape ? (reverse ? cs@ls) (option_hd ? rs) (tail ? rs))
 980   = mk_tape ? ls (option_hd ? (cs@rs)) (tail ? (cs@rs)).
 981 #T #n elim n
 982 [ #ls * [| #c0 #cs0 #rs #H normalize in H; destruct (H) ] #rs #_ %
 983 | #n0 #IH #ls #cs #rs @(list_elim_left … cs)
 984   [ #H normalize in H; destruct (H) ] -cs
 985   #c #cs #_ #Hlen >reverse_append whd in ⊢ (??%?);
 986   >(?: tape_move T (mk_tape T ((reverse T [c]@reverse T cs)@ls) (option_hd T rs) (tail T rs)) L
 987     = mk_tape ? (reverse T cs@ls) (option_hd ? (c::rs)) (tail ? (c::rs))) in ⊢ (??(????%)?);
 988   [| cases rs // ] >IH
 989   [ >associative_append %
 990   | >length_append in Hlen; normalize // ]
 991 ]
 992 qed.
 993
 994 lemma tape_move_niltape :
 995   ∀sig,mv.tape_move sig (niltape ?) mv = niltape ?. #sig * // qed.
 996
 997 lemma iter_tape_move_niltape :
 998   ∀sig,mv,n.iter … (λt.tape_move sig t mv) n (niltape ?) = niltape ?.
 999 #sig #mv #n elim n // -n #n #IH whd in ⊢ (??%?); >tape_move_niltape //
1000 qed.
1001
1002 lemma tape_move_R_left :
1003   ∀sig,rs.tape_move sig (mk_tape ? [ ] (None ?) rs) R =
1004   mk_tape ? [ ] (option_hd ? rs) (tail ? rs). #sig * //
1005 qed.
1006
1007 lemma binaryTM_loop :
1008  ∀sig,M,i,tf,qf. O < FS_crd sig →
1009  ∀t,q.∃k.i ≤ k ∧
1010  ((loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) →
1011   loopM ? (mk_binaryTM sig M) k
1012     (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) =
1013   Some ? (mk_config ?? (state_bin_lift ? M qf) (tape_bin_lift ? tf))) ∧
1014  (loopM sig M i (mk_config ?? q t) = None ? →
1015   loopM ? (mk_binaryTM sig M) k
1016     (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) = None ?)).
1017 #sig #M #i #tf #qf #Hcrd elim i
1018 [ #t #q %{O} % // % // change with (None ?) in ⊢ (??%?→?); #H destruct (H)
1019 | -i #i #IH #t #q >loopM_unfold
1020   lapply (refl ? (halt sig M (cstate ?? (mk_config ?? q t))))
1021   cases (halt ?? q) in ⊢ (???%→?); #Hhalt
1022   [ %{(S i)} % //
1023     >(loop_S_true ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt) %
1024     [| #H destruct (H)]
1025     #H destruct (H) >loopM_unfold >loop_S_true // ]
1026   (* interesting case: more than one step *)
1027   >(loop_S_false ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)cases (current_None_or_midtape ? t)
1028   (*** current = None ***)
1029   [ #Hcur lapply (current_tape_bin_list … Hcur) #Hcur'
1030     cut (∃qn,chn,mv.〈qn,chn,mv〉 = trans ? M 〈q,None ?〉)
1031     [ cases (trans ? M 〈q,None ?〉) * #qn #chn #mv /4 by ex_intro/ ]
1032     * #qn * #chn * #mv cases chn -chn
1033     [ #Htrans lapply (binaryTM_phase0_None_None … (None ?) (FS_crd sig) … Hhalt Hcur' Htrans) // [/2 by monotonic_lt_plus_l/]
1034       lapply (binaryTM_phase3 ? M qn (None ?) (displ2_of_move sig mv) ? (tape_move FinBool (tape_bin_lift sig t) (mv_tech mv))) [//]
1035       cases (IH (tape_move ? t mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
1036       #phase3 #phase0 %{(S (S (displ2_of_move sig mv))+k0)} %
1037       [ @le_S_S @(le_plus O) // ]
1038       >state_bin_lift_unfold >phase0 [|//]
1039       >phase3 [|//]
1040       >(?: S (S (displ2_of_move sig mv))+k0-1-S (displ2_of_move sig mv) = k0)
1041       [| /2 by refl, plus_to_minus/ ]
1042       cut (tape_move sig t mv=tape_move sig (tape_write sig t (None sig)) mv) [%] #Hcut
1043       >(?: iter ? (λt0.tape_move ? t0 L) (displ2_of_move sig mv) (tape_move ? (tape_bin_lift ? t) (mv_tech mv))
1044            =tape_bin_lift ? (tape_move ? t mv))
1045       [|cases t in Hcur;
1046         [4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H)
1047         | #_ whd in match (tape_bin_lift ??);
1048           >tape_move_niltape >iter_tape_move_niltape >tape_move_niltape %
1049         | #r0 #rs0 #_ cases mv
1050           [ >tape_bin_lift_unfold whd in match (mv_tech L); whd in match (displ2_of_move sig L);
1051             whd in match (rev_bin_list ??); whd in match (option_hd ??);
1052             whd in match (right ??); >(?: []@bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
1053             >tape_move_R_left >hd_tech [| >eq_length_bin_char_FS_crd // ]
1054             >tail_tech [| >eq_length_bin_char_FS_crd // ]
1055             >iter_tape_move_L_left //
1056           | >tape_bin_lift_unfold whd in match (mv_tech R); whd in match (displ2_of_move sig R);
1057             whd in match (rev_bin_list ??); whd in match (option_hd ??);
1058             whd in match (right ??); >(?: []@bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
1059             whd in match (tape_move ? (leftof ???) R);
1060             >tape_bin_lift_unfold >left_midtape >opt_bin_char_Some >right_midtape
1061             >iter_O >tape_move_R_left >hd_tech [| >eq_length_bin_char_FS_crd // ]
1062             >tail_tech [| >eq_length_bin_char_FS_crd // ] //
1063           | >tape_bin_lift_unfold % ]
1064         | #l0 #ls0 #_ cases mv
1065           [ >tape_bin_lift_unfold whd in match (mv_tech L); whd in match (displ2_of_move sig L);
1066             whd in match (bin_list ??); >append_nil whd in match (option_hd ??);
1067             whd in match (left ??); whd in match (tail ??);
1068             whd in match (tape_move ? (rightof ???) L);
1069             >(?: rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
1070             >(?:tape_move ? (mk_tape ? ? (None ?) [ ]) R =
1071                  mk_tape ? (reverse ? (bin_char ? l0)@rev_bin_list ? ls0) (None ?) [ ])
1072             [| cases (reverse ? (bin_char ? l0)@rev_bin_list ? ls0) //]
1073             >(?:None ? = option_hd ? [ ]) // >iter_tape_move_L [|@eq_length_bin_char_FS_crd]
1074             >append_nil >tape_bin_lift_unfold >left_midtape >current_midtape >right_midtape
1075             >opt_bin_char_Some >append_nil %
1076           | >tape_bin_lift_unfold whd in match (mv_tech R); whd in match (displ2_of_move sig R);
1077             whd in match (bin_list ??); >append_nil whd in match (option_hd ??);
1078             whd in match (left ??); whd in match (tail ??); >iter_O cases (rev_bin_list ??) //
1079           | >tape_bin_lift_unfold % ]
1080         ]
1081       ]
1082       %
1083       [ #Hloop @IH <Hloop @eq_f whd in ⊢ (???%); >Hcur <Htrans @eq_f @Hcut
1084       | #Hloop @IHNone <Hloop @eq_f whd in ⊢ (???%); >Hcur <Htrans @eq_f @Hcut ]
1085     | #chn #Htrans
1086       lapply (binaryTM_phase0_None_Some … (None ?) (FS_crd sig) … Hhalt Hcur' Htrans) // [/2 by monotonic_lt_plus_l/]
1087       cases t in Hcur;
1088       [ 4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H)
1089       | 2: #r0 #rs0 #_ cut (∃b,bs.bin_char ? r0 = b::bs)
1090         [ <(eq_length_bin_char_FS_crd sig r0) in Hcrd; cases (bin_char ? r0)
1091           [ cases (not_le_Sn_O O) #H #H1 cases (H H1) |/3 by ex_intro/] ]
1092         * #b * #bs #Hbs
1093         lapply (binaryTM_phase4_extend ???? (tape_move ? (tape_bin_lift ? (leftof ? r0 rs0)) R) b … Htrans)
1094         [ >tape_bin_lift_unfold whd in match (option_hd ??); whd in match (tail ??);
1095           whd in match (right ??);
1096           >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
1097           >Hbs % ]
1098         cases (binaryTM_phase5 ? M q (None ?) (FS_crd sig) (bin_list ? (r0::rs0)) ?) [|//]
1099         #cs * #Hcs
1100         lapply (binaryTM_phase2_Some_ow ?? q (None ?) … [ ] ? (bin_list ? (r0::rs0)) Htrans Hcs)
1101         lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ?
1102                  (mk_tape FinBool (reverse bool (bin_char sig chn)@[])
1103                    (option_hd FinBool (bin_list sig (r0::rs0))) (tail FinBool (bin_list sig (r0::rs0))))) [//]
1104         cases (IH (tape_move ? (tape_write ? (leftof ? r0 rs0) (Some ? chn)) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
1105         #phase3 #phase2 #phase5 #phase4 #phase0
1106         %{(1 + 1 + (S (FS_crd sig)) + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} %
1107         [ @le_S_S @(le_plus O) // ]
1108         >state_bin_lift_unfold >phase0 [|//]
1109         >phase4 [|//]
1110         >(?: loopM ? (mk_binaryTM ??) ? (mk_config ?? 〈q,bin5,None ?,to_initN ???〉 ?) = ?)
1111         [|| @(trans_eq ????? (phase5 ??))
1112           [ @eq_f @eq_f
1113             >tape_bin_lift_unfold whd in match (rev_bin_list ??);
1114             whd in match (right ??); whd in match (bin_list ??);
1115             <(eq_length_bin_char_FS_crd sig r0) in Hcrd; cases (bin_char ? r0) //
1116             cases (not_le_Sn_O O) #H #H1 cases (H H1)
1117           | @le_S_S >associative_plus >associative_plus >commutative_plus @(le_plus O) //
1118           |]]
1119         >phase2
1120         [|<plus_minus [|//] <plus_minus [|//] <plus_minus [|//] // ]
1121         >phase3 [|<plus_minus [|//] <plus_minus [|//] // ]
1122         >(?: 1+1+S (FS_crd sig)+S (FS_crd sig)+S (displ_of_move sig mv)+k0-1-1
1123               -S (FS_crd sig)-S (FS_crd sig) -S (displ_of_move sig mv) = k0)
1124         [|<plus_minus [|//] <plus_minus [|//] // ]
1125         -phase0 -phase2 -phase3 -phase4 -phase5 <state_bin_lift_unfold
1126         >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
1127               (mk_tape ? (reverse ? (bin_char sig chn)@[])
1128                 (option_hd FinBool (bin_list sig (r0::rs0)))
1129                 (tail FinBool (bin_list sig (r0::rs0))))
1130            = tape_bin_lift ? (tape_move ? (tape_write ? (leftof ? r0 rs0) (Some ? chn)) mv))
1131         [ % #Hloop
1132           [ @IH <Hloop @eq_f whd in ⊢ (???%); <Htrans %
1133           | @IHNone <Hloop @eq_f whd in ⊢ (???%); <Htrans % ]
1134         | >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
1135           cases mv
1136           [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
1137             >iter_split >iter_tape_move_L [|@eq_length_bin_char_FS_crd]
1138             >hd_tech [|>eq_length_bin_char_FS_crd // ]
1139             >tail_tech [|>eq_length_bin_char_FS_crd // ] >iter_tape_move_L_left [|//]
1140             whd in match (tape_move ???); >tape_bin_lift_unfold %
1141           | normalize in match (displ_of_move ??); >iter_O
1142             normalize in match (tape_move ???);
1143             >tape_bin_lift_unfold >opt_bin_char_Some
1144             >hd_tech [|>eq_length_bin_char_FS_crd // ]
1145             >tail_tech [| >eq_length_bin_char_FS_crd // ] %
1146           | normalize in match (displ_of_move ??);
1147             >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
1148             normalize in match (tape_move ???); >tape_bin_lift_unfold
1149             >opt_bin_char_Some >hd_tech [|>eq_length_bin_char_FS_crd // ]
1150             >tail_tech [|>eq_length_bin_char_FS_crd // ] % ]
1151         ]
1152       | #_ lapply (binaryTM_phase4_write ? M q (None ?) (niltape ?) (refl ??))
1153         lapply (binaryTM_phase2_Some_of ?? q (None ?) … [ ] Htrans)
1154         lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ?
1155                  (mk_tape FinBool (reverse bool (bin_char sig chn)@[]) (None ?) [ ])) [//]
1156         cases (IH (tape_move ? (midtape ? [ ] chn [ ]) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
1157         #phase3 #phase2 #phase4 #phase0
1158         %{(1 + 1 + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} %
1159         [ @le_S_S @(le_plus O) // ]
1160         >state_bin_lift_unfold >phase0 [|//]
1161         >phase4 [|//]
1162         >phase2 [| <plus_minus [|//] // ]
1163         >phase3 [| <plus_minus [|//] <plus_minus [|//] // ]
1164         >(?: 1+1+S (FS_crd sig) + S (displ_of_move sig mv)+k0-1-1
1165               -S (FS_crd sig)-S (displ_of_move sig mv) = k0)
1166         [| <plus_minus [|//] <plus_minus [|//] // ]
1167         -phase0 -phase2 -phase3 -phase4 <state_bin_lift_unfold
1168         >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
1169               (mk_tape ? (reverse ? (bin_char sig chn)@[]) (None ?) [ ])
1170            = tape_bin_lift ? (tape_move ? (tape_write ? (niltape ?) (Some ? chn)) mv))
1171         [ % #Hloop
1172           [ @IH <Hloop @eq_f whd in ⊢ (???%); <Htrans %
1173           | @IHNone <Hloop @eq_f whd in ⊢ (???%); <Htrans % ]
1174         | cases mv
1175           [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
1176             >iter_split change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????(????%))?);
1177             >iter_tape_move_L [| >eq_length_bin_char_FS_crd // ]
1178             >append_nil in ⊢ (??(????(???%?))?);
1179             >tail_tech [| >eq_length_bin_char_FS_crd // ]
1180             >iter_tape_move_L_left [|//]
1181             normalize in match (tape_move ???);
1182             >tape_bin_lift_unfold %
1183           | normalize in match (displ_of_move ??); >iter_O
1184             normalize in match (tape_move ???);
1185             >tape_bin_lift_unfold %
1186           | normalize in match (displ_of_move ??);
1187             change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????%)?);
1188             >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
1189             normalize in match (tape_move ???); >tape_bin_lift_unfold
1190             >opt_bin_char_Some >hd_tech [|>eq_length_bin_char_FS_crd // ]
1191             >tail_tech [|>eq_length_bin_char_FS_crd // ] % ]
1192         ]
1193       | #l0 #ls0 #_ lapply (binaryTM_phase4_write ? M q (None ?) (tape_bin_lift ? (rightof ? l0 ls0)) ?)
1194         [ >tape_bin_lift_unfold >current_mk_tape % ]
1195         lapply (binaryTM_phase2_Some_of ?? q (None ?) … (rev_bin_list ? (l0::ls0)) Htrans)
1196         lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ?
1197                  (mk_tape FinBool (reverse bool (bin_char sig chn)@rev_bin_list ? (l0::ls0)) (None ?) [ ])) [//]
1198         cases (IH (tape_move ? (midtape ? (l0::ls0) chn [ ]) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
1199         #phase3 #phase2 #phase4 #phase0
1200         %{(1 + 1 + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} %
1201         [ @le_S_S @(le_plus O) // ]
1202         >state_bin_lift_unfold >phase0 [|//]
1203         >(?:tape_move ? (tape_bin_lift ? (rightof ? l0 ls0)) R = tape_bin_lift ? (rightof ? l0 ls0))
1204         [| >tape_bin_lift_unfold normalize in match (option_hd ??); normalize in match (right ??);
1205            normalize in match (tail ??); normalize in match (left ??);
1206            >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
1207            cases (reverse ? (bin_char ? l0)) // cases (rev_bin_list ? ls0) // ]
1208         >phase4 [|//]
1209         >phase2 [|<plus_minus [|//] // ]
1210         >phase3 [|<plus_minus [|//] <plus_minus [|//] // ]
1211         >(?: 1+1+S (FS_crd sig) + S (displ_of_move sig mv)+k0-1-1
1212               -S (FS_crd sig)-S (displ_of_move sig mv) = k0)
1213         [| <plus_minus [|//] <plus_minus [|//] // ]
1214         -phase0 -phase2 -phase3 -phase4 <state_bin_lift_unfold
1215         >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
1216               (mk_tape ? (reverse ? (bin_char sig chn)@rev_bin_list ? (l0::ls0)) (None ?) [ ])
1217            = tape_bin_lift ? (tape_move ? (tape_write ? (rightof ? l0 ls0) (Some ? chn)) mv))
1218         [ % #Hloop
1219           [ @IH <Hloop @eq_f whd in ⊢ (???%); <Htrans %
1220           | @IHNone <Hloop @eq_f whd in ⊢ (???%); <Htrans % ]
1221         | cases mv
1222           [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
1223             >iter_split change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????(????%))?);
1224             >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
1225             >append_nil in ⊢ (??(????(???%?))?); >tail_tech [|>eq_length_bin_char_FS_crd // ]
1226             >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
1227             >append_nil >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
1228             normalize in match (tape_move ???);
1229             >tape_bin_lift_unfold @eq_f2
1230             [ >hd_tech [|>eq_length_bin_char_FS_crd // ] %
1231             | >tail_tech [|>eq_length_bin_char_FS_crd // ] >opt_bin_char_Some
1232               normalize in match (bin_list ??); >append_nil %]
1233           | normalize in match (displ_of_move ??); >iter_O
1234             normalize in match (tape_move ???);
1235             >tape_bin_lift_unfold %
1236           | normalize in match (displ_of_move ??);
1237             change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????%)?);
1238             >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
1239             normalize in match (tape_move ???); >tape_bin_lift_unfold
1240             >opt_bin_char_Some >hd_tech [|>eq_length_bin_char_FS_crd // ]
1241             >tail_tech [|>eq_length_bin_char_FS_crd // ] % ]
1242         ]
1243       ]
1244     ]
1245   (*** midtape ***)
1246   | * #ls * #c * #rs #Ht >Ht
1247     cut (∃qn,chn,mv.〈qn,chn,mv〉 = trans ? M 〈q,Some ? c〉)
1248     [ cases (trans ? M 〈q,Some ? c〉) * #qn #chn #mv /4 by ex_intro/ ]
1249     * #qn * #chn * #mv #Htrans
1250     cut (tape_bin_lift ? t = ?) [| >tape_bin_lift_unfold % ]
1251     >Ht in ⊢ (???%→?); >opt_bin_char_Some >left_midtape >right_midtape #Ht'
1252     lapply (binaryTM_phase0_midtape ?? (tape_bin_lift ? t) q … (None ?) Hcrd Hhalt Ht')
1253     lapply (binaryTM_phase1 ?? q (reverse ? (bin_char ? c)) (rev_bin_list ? ls)
1254              (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)) (Some ? c) ??)
1255     [ cases (bin_list ? rs) // #r0 #rs0 normalize in ⊢ (%→?); #H destruct (H)
1256     | >length_reverse >eq_length_bin_char_FS_crd // |]
1257     >opt_cons_hd_tl >reverse_reverse
1258     cases chn in Htrans; -chn
1259     [ #Htrans
1260       lapply (binaryTM_phase2_None … Htrans (FS_crd sig) ?
1261                (mk_tape FinBool (rev_bin_list sig ls)
1262                  (option_hd FinBool (bin_char sig c@bin_list sig rs))
1263                  (tail FinBool (bin_char sig c@bin_list sig rs)))) [//]
1264       lapply (binaryTM_phase3 ? M qn (Some ? c) (displ_of_move sig mv) ?
1265                (mk_tape FinBool (reverse bool (bin_char sig c)@rev_bin_list ? ls)
1266                (option_hd FinBool (bin_list sig rs)) (tail FinBool (bin_list sig rs)))) [//]
1267       cases (IH (tape_move ? (tape_write ? (midtape ? ls c rs) (None ?)) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
1268       #phase3 #phase2 #phase1 #phase0
1269       %{(S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0)} %
1270       [ @le_S_S @(le_plus O) // ]
1271       >state_bin_lift_unfold <Ht >phase0 [|//]
1272       >phase1 [|/2 by monotonic_le_minus_l/]
1273       >phase2 [|/2 by monotonic_le_minus_l/]
1274       >iter_tape_move_R [|>eq_length_bin_char_FS_crd // ]
1275       >phase3 [|/2 by monotonic_le_minus_l/]
1276       -phase0 -phase1 -phase2 -phase3
1277       >(?: S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0
1278            - S (FS_crd sig) - S (FS_crd sig) - S (FS_crd sig) - S (displ_of_move sig mv)
1279          = k0) [| <plus_minus [|//] <plus_minus [|//] <plus_minus [|//] // ]
1280       <state_bin_lift_unfold
1281       >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
1282             (mk_tape ? (reverse ? (bin_char sig c)@rev_bin_list ? ls)
1283               (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)))
1284          = tape_bin_lift ? (tape_move ? (tape_write ? (midtape ? ls c rs) (None ?)) mv))
1285       [ % #Hloop
1286         [ @IH <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans %
1287         | @IHNone <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans % ]
1288       | normalize in match (tape_write ???); cases mv in Htrans; #Htrans
1289         [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
1290           >iter_split >iter_tape_move_L [| >eq_length_bin_char_FS_crd // ]
1291           cases ls
1292           [ >hd_tech [|>eq_length_bin_char_FS_crd // ]
1293             >tail_tech [|>eq_length_bin_char_FS_crd // ]
1294             >iter_tape_move_L_left [|//]
1295             >tape_bin_lift_unfold %
1296           | #l0 #ls0 >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
1297             normalize in match (tape_move ???);
1298             >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
1299             >hd_tech [|>eq_length_bin_char_FS_crd // ]
1300             >tail_tech [|>eq_length_bin_char_FS_crd // ]
1301             >tape_bin_lift_unfold % ]
1302         | normalize in match (displ_of_move ??); >iter_O cases rs
1303           [ normalize in match (tape_move ???); >tape_bin_lift_unfold %
1304           | #r0 #rs0 normalize in match (tape_move ???);
1305             >tape_bin_lift_unfold >opt_bin_char_Some
1306             >left_midtape >right_midtape
1307             >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
1308             >hd_tech [|>eq_length_bin_char_FS_crd // ]
1309             >tail_tech [|>eq_length_bin_char_FS_crd // ] %
1310           ]
1311         | normalize in match (displ_of_move ??); >iter_tape_move_L
1312           [|>eq_length_bin_char_FS_crd // ]
1313           >hd_tech [|>eq_length_bin_char_FS_crd // ]
1314           >tail_tech [|>eq_length_bin_char_FS_crd // ] >tape_bin_lift_unfold %
1315         ]
1316       ]
1317     | #chn #Htrans
1318       lapply (binaryTM_phase2_Some_ow ?? q (Some ? c) ??? (rev_bin_list ? ls) (bin_char ? c) (bin_list ? rs) Htrans ?)
1319       [>eq_length_bin_char_FS_crd // ]
1320       lapply (binaryTM_phase3 ? M qn (Some ? c) (displ_of_move sig mv) ?
1321                (mk_tape FinBool (reverse bool (bin_char sig chn)@rev_bin_list ? ls)
1322                (option_hd FinBool (bin_list sig rs)) (tail FinBool (bin_list sig rs)))) [//]
1323       cases (IH (tape_move ? (tape_write ? (midtape ? ls c rs) (Some ? chn)) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
1324       #phase3 #phase2 #phase1 #phase0
1325       %{(S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0)} %
1326       [ @le_S_S @(le_plus O) // ]
1327       >state_bin_lift_unfold <Ht >phase0 [|//]
1328       >phase1 [|/2 by monotonic_le_minus_l/]
1329       >phase2 [|/2 by monotonic_le_minus_l/]
1330       >phase3 [|/2 by monotonic_le_minus_l/]
1331       -phase0 -phase1 -phase2 -phase3
1332       >(?: S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0
1333            - S (FS_crd sig) - S (FS_crd sig) - S (FS_crd sig) - S (displ_of_move sig mv)
1334          = k0)
1335       [| <plus_minus [|//] <plus_minus [|//] <plus_minus [|//] // ]
1336       <state_bin_lift_unfold
1337       >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
1338             (mk_tape ? (reverse ? (bin_char sig chn)@rev_bin_list ? ls)
1339               (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)))
1340          = tape_bin_lift ? (tape_move ? (tape_write ? (midtape ? ls c rs) (Some ? chn)) mv))
1341       [ % #Hloop
1342         [ @IH <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans %
1343         | @IHNone <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans % ]
1344       | normalize in match (tape_write ???); cases mv in Htrans; #Htrans
1345         [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
1346           >iter_split >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
1347           cases ls
1348           [ >hd_tech [|>eq_length_bin_char_FS_crd // ]
1349             >tail_tech [|>eq_length_bin_char_FS_crd // ] >iter_tape_move_L_left [|//]
1350             >tape_bin_lift_unfold %
1351           | #l0 #ls0 >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
1352             normalize in match (tape_move ???);
1353             >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
1354             >hd_tech [|>eq_length_bin_char_FS_crd // ]
1355             >tail_tech [|>eq_length_bin_char_FS_crd // ]
1356             >tape_bin_lift_unfold % ]
1357         | normalize in match (displ_of_move ??); >iter_O cases rs
1358           [ normalize in match (tape_move ???); >tape_bin_lift_unfold %
1359           | #r0 #rs0 normalize in match (tape_move ???);
1360             >tape_bin_lift_unfold >opt_bin_char_Some
1361             >left_midtape >right_midtape
1362             >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
1363             >hd_tech [|>eq_length_bin_char_FS_crd // ]
1364             >tail_tech [|>eq_length_bin_char_FS_crd // ] %
1365           ]
1366         | normalize in match (displ_of_move ??); >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
1367           >hd_tech [|>eq_length_bin_char_FS_crd // ]
1368           >tail_tech [|>eq_length_bin_char_FS_crd // ] >tape_bin_lift_unfold %
1369         ]
1370       ]
1371     ]
1372   ]
1373 ]
1374 qed.
1375
1376 definition R_bin_lift ≝ λsig,R,t1,t2.
1377   ∀u1.t1 = tape_bin_lift sig u1 →
1378   ∃u2.t2 = tape_bin_lift sig u2 ∧ R u1 u2.
1379
1380 theorem sem_binaryTM :
1381   ∀sig,M,R.O < FS_crd sig → M ⊫ R → mk_binaryTM sig M ⊫ R_bin_lift ? R.
1382 #sig #M #R #Hcrd #HM #t #k #outc #Hloopbin #u #Ht
1383 lapply (refl ? (loopM ? M k (initc ? M u))) cases (loopM ? M k (initc ? M u)) in ⊢ (???%→?);
1384 [ #H cases (binaryTM_loop ? M k u (start ? M) Hcrd u (start ? M))
1385   #k0 * #Hlt * #_ #H1 lapply (H1 H) -H -H1 <Ht
1386   whd in match (initc ???) in Hloopbin; whd in match (start ??) in Hloopbin;
1387   >state_bin_lift_unfold >(loop_incr2 … Hlt Hloopbin) #H destruct (H)
1388 | * #qf #tf #H cases (binaryTM_loop ? M k tf qf Hcrd u (start ? M))
1389   #k0 * #Hlt * #H1 #_ lapply (H1 H) -H1 <Ht
1390   whd in match (initc ???) in Hloopbin; whd in match (start ??) in Hloopbin;
1391   >state_bin_lift_unfold >(loop_incr2 … Hlt Hloopbin) #Heq destruct (Heq)
1392   % [| % [%]] @(HM … H)
1393 qed.