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 (* given a FinSet F:
  18    - get its cardinality
  19    - return its nth element
  20    - return the index of a given element
  21  *)
  22 axiom FS_crd : FinSet → nat.
  23 axiom FS_nth : ∀F:FinSet.nat → option F.
  24 axiom index_of_FS : ∀F:FinSet.F → nat.
  25
  26 (* unary bit representation (with a given length) of a certain number *)
  27 axiom unary_of_nat : nat → nat → (list bool).
  28
  29 axiom FinVector : Type[0] → nat → FinSet.
  30
  31 definition binary_base_states ≝ initN 6.
  32
  33 definition bin0 : binary_base_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 6 (refl …)).
  34 definition bin1 : binary_base_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 6 (refl …)).
  35 definition bin2 : binary_base_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 6 (refl …)).
  36 definition bin3 : binary_base_states ≝ mk_Sig ?? 3 (leb_true_to_le 4 6 (refl …)).
  37 definition bin4 : binary_base_states ≝ mk_Sig ?? 4 (leb_true_to_le 5 6 (refl …)).
  38 definition bin5 : binary_base_states ≝ mk_Sig ?? 5 (leb_true_to_le 6 6 (refl …)).
  39
  40 definition states_binaryTM : FinSet → FinSet → FinSet ≝ λsig,states.
  41  FinProd (FinProd states binary_base_states)
  42          (FinProd (FinOption sig) (initN (S (2 * (FS_crd sig))))).
  43
  44 axiom daemon : ∀T:Type[0].T.
  45
  46 definition to_initN : ∀n,m.n < m → initN m ≝ λn,m,Hn.mk_Sig … n ….// qed.
  47
  48 definition initN_pred : ∀n.∀m:initN n.initN n ≝ λn,m.mk_Sig … (pred (pi1 … m)) ….
  49 cases m #m0 /2 by le_to_lt_to_lt/ qed.
  50
  51 (* controllare i contatori, molti andranno incrementati di uno *)
  52 definition trans_binaryTM : ∀sig,states:FinSet.
  53   (states × (option sig) → states × (option sig) × move) →
  54   ((states_binaryTM sig states) × (option bool) →
  55    (states_binaryTM sig states) × (option bool) × move)
  56 ≝ λsig,states,trans,p.
  57   let 〈s,a〉 ≝ p in
  58   let 〈s0,phase,ch,count〉 ≝ s in
  59   let (H1 : O < S (2*FS_crd sig)) ≝ ? in
  60   let (H2 : FS_crd sig < S (2*FS_crd sig)) ≝ ? in
  61   match pi1 … phase with
  62   [ O ⇒ (*** PHASE 0: read ***)
  63       match pi1 … count with
  64       [ O ⇒ 〈〈s0,bin1,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
  65       | S k ⇒ match a with
  66         [ Some a0 ⇒ if (a0 == true)
  67                     then 〈〈s0,bin0,FS_nth sig k,initN_pred … count〉, None ?,R〉
  68                     else 〈〈s0,bin0,ch,initN_pred … count〉,None ?,R〉
  69         | None ⇒ (* Overflow position! *)
  70           〈〈s0,bin4,None ?,to_initN 0 ? H1〉,None ?,R〉 ] ]
  71   | S phase ⇒ match phase with
  72   [ O ⇒ (*** PHASE 1: restart ***)
  73       match pi1 … count with
  74       [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
  75       | S k ⇒ 〈〈s0,bin1,ch,initN_pred … count〉,None ?,L〉 ]
  76   | S phase ⇒ match phase with
  77   [ O ⇒ (*** PHASE 2: write ***)
  78       let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
  79       match pi1 … count with
  80       [ O ⇒ let mv' ≝ match mv with [ R ⇒ N | _ ⇒ L ] in
  81             let count' ≝ match mv with [ R ⇒ 0 | N ⇒ FS_crd sig | L ⇒ 2*(FS_crd sig) ] in
  82              〈〈s',bin3,ch,to_initN count' ??〉,None ?,mv'〉
  83       | S k ⇒ match a' with
  84          [ None ⇒ 〈〈s0,bin2,ch,initN_pred … count〉,None ?,R〉
  85          | Some a0' ⇒ let out ≝ (FS_nth ? k == a') in
  86                       〈〈s0,bin2,ch,initN_pred … count〉,Some ? out,R〉 ]
  87       ]
  88   | S phase ⇒ match phase with
  89   [ O ⇒ (*** PHASE 3: move head left ***)
  90       match pi1 … count with
  91       [ O ⇒ 〈〈s0,bin0,None ?,to_initN (FS_crd sig) ? H2〉, None ?,N〉 (* the end: restart *)
  92       | S k ⇒ 〈〈s0,bin3,ch,initN_pred … count〉, None ?,L〉 ]
  93   | S phase ⇒ match phase with
  94   [ O ⇒ (*** PHASE 4: check position ***)
  95       match a with
  96       [ None ⇒ (* niltape/rightof: we can write *) 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
  97       | Some _ ⇒ (* leftof *)
  98         let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
  99         match a' with
 100         [ None ⇒ (* we don't write anything: go to end of 2 *) 〈〈s0,bin2,ch,to_initN 0 ? H1〉,None ?,N〉
 101         | Some _ ⇒ (* extend tape *) 〈〈s0,bin5,ch,to_initN (FS_crd sig) ? H2〉,None ?,L〉 ]
 102       ]
 103   | S _ ⇒ (*** PHASE 5: left extension ***)
 104       match pi1 … count with
 105       [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
 106       | S k ⇒ 〈〈s0,bin5,ch,initN_pred … count〉,Some ? false,L〉 ]]]]]].
 107 [2,3: //]
 108 whd in match count'; cases mv whd in ⊢ (?%?); //
 109 qed.
 110
 111 definition halt_binaryTM : ∀sig,M.states_binaryTM sig (states sig M) → bool ≝
 112   λsig,M,s.let 〈s0,phase,ch,count〉 ≝ s in
 113   pi1 … phase == O ∧ halt sig M s0.
 114
 115 (*
 116  * Una mk_binaryTM prende in input una macchina M e produce una macchina che:
 117  * - ha per alfabeto FinBool
 118  * - ha stati di tipo ((states … M) × (initN 7)) ×
 119        ((option sig) × (initN (2*dimensione dell'alfabeto di M + 1))
 120  *   dove il primo elemento corrisponde allo stato della macchina input,
 121  *   il secondo identifica la fase (lettura, scrittura, spostamento)
 122  *   il terzo identifica il carattere oggetto letto
 123  *   il quarto è un contatore
 124  * - la funzione di transizione viene prodotta da trans_binaryTM
 125  * - la funzione di arresto viene prodotta da halt_binaryTM
 126  *)
 127 definition mk_binaryTM ≝
 128   λsig.λM:TM sig.
 129   mk_TM FinBool (states_binaryTM sig (states sig M))
 130     (trans_binaryTM sig (states sig M) (trans sig M))
 131     (〈start sig M,bin0,None ?,FS_crd sig〉) (halt_binaryTM sig M).// qed.
 132
 133 definition bin_char ≝ λsig,ch.unary_of_nat (FS_crd sig) (index_of_FS sig ch).
 134
 135 definition bin_current ≝ λsig,t.match current ? t with
 136 [ None ⇒ [ ] | Some c ⇒ bin_char sig c ].
 137
 138 definition tape_bin_lift ≝ λsig,t.
 139 let ls' ≝ flatten ? (map ?? (bin_char sig) (left ? t)) in
 140 let c' ≝ option_hd ? (bin_current sig t) in
 141 let rs' ≝ tail ? (bin_current sig t)@flatten ? (map ?? (bin_char sig) (right ? t)) in
 142  mk_tape ? ls' c' rs'.
 143
 144 definition R_bin_lift ≝ λsig,R,t1,t2.
 145   ∃u1.t1 = tape_bin_lift sig u1 →
 146   ∃u2.t2 = tape_bin_lift sig u2 ∧ R u1 u2.
 147
 148 definition state_bin_lift :
 149   ∀sig.∀M:TM sig.states sig M → states ? (mk_binaryTM ? M)
 150  ≝ λsig,M,q.〈q,bin0,None ?,FS_crd sig〉.// qed.
 151
 152 lemma lift_halt_binaryTM :
 153   ∀sig,M,q.halt sig M q = halt ? (mk_binaryTM sig M) (state_bin_lift ? M q).
 154 // qed.
 155
 156 lemma binaryTM_bin0_bin1 :
 157   ∀sig,M,t,q,ch.
 158   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,O〉) t)
 159   = mk_config ?? (〈q,bin1,ch,to_initN (FS_crd sig) ??〉) t. //
 160 qed.
 161
 162 lemma binaryTM_bin0_bin4 :
 163   ∀sig,M,t,q,ch,k.
 164   current ? t = None ? → S k <S (2*FS_crd sig) →
 165   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t)
 166   = mk_config ?? (〈q,bin4,None ?,to_initN 0 ??〉) (tape_move ? t R). [2,3://]
 167 #sig #M #t #q #ch #k #Hcur #Hk
 168 whd in match (step ???); whd in match (trans ???);
 169 >Hcur %
 170 qed.
 171
 172 lemma binaryTM_bin0_true :
 173   ∀sig,M,t,q,ch,k.
 174   current ? t = Some ? true → S k <S (2*FS_crd sig) →
 175   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t)
 176   = mk_config ?? (〈q,bin0,FS_nth sig k,to_initN k ??〉) (tape_move ? t R).[2,3:/2 by lt_S_to_lt/]
 177 #sig #M #t #q #ch #k #Hcur #Hk
 178 whd in match (step ???); whd in match (trans ???);
 179 >Hcur %
 180 qed.
 181
 182 lemma binaryTM_bin0_false :
 183   ∀sig,M,t,q,ch,k.
 184   current ? t = Some ? false → S k <S (2*FS_crd sig) →
 185   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,S k〉) t)
 186   = mk_config ?? (〈q,bin0,ch,to_initN k ??〉) (tape_move ? t R).[2,3:/2 by lt_S_to_lt/]
 187 #sig #M #t #q #ch #k #Hcur #Hk
 188 whd in match (step ???); whd in match (trans ???);
 189 >Hcur %
 190 qed.
 191
 192 (* to be checked *)
 193 axiom binary_to_bin_char :∀sig,csl,csr,a.
 194   csl@true::csr=bin_char sig a → FS_nth ? (length ? csr) = Some ? a.
 195
 196 lemma binaryTM_phase0_midtape_aux :
 197   ∀sig,M,q,ls,a,rs,k.
 198   halt sig M q=false →
 199   ∀csr,csl,t,ch.length ? csr < S (2*FS_crd sig) →
 200   t = mk_tape ? (reverse ? csl@ls) (option_hd ? (csr@rs)) (tail ? (csr@rs)) →
 201   csl@csr = bin_char sig a →
 202   |csl@csr| = FS_crd sig →
 203   (index_of_FS ? a < |csl| → ch = Some ? a) →
 204   loopM ? (mk_binaryTM sig M) (S (length ? csr) + k)
 205     (mk_config ?? (〈q,bin0,ch,length ? csr〉) t)
 206   = loopM ? (mk_binaryTM sig M) k
 207       (mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉)
 208         (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [2,3:/2 by O/]
 209 #sig #M #q #ls #a #rs #k #Hhalt #csr elim csr
 210 [ #csl #t #ch #Hlen #Ht >append_nil #Hcsl #Hlencsl #Hch >loopM_unfold >loop_S_false [|normalize //]
 211   >Hch [| >Hlencsl (* lemmatize *) @daemon]
 212   <loopM_unfold @eq_f >binaryTM_bin0_bin1 @eq_f >Ht
 213   whd in match (step ???); whd in match (trans ???); <Hcsl %
 214 | #c cases c
 215   [ #csr0 #IH #csl #t #ch #Hlen #Ht #Heq #Hcrd #Hch >loopM_unfold >loop_S_false [|normalize //]
 216     <loopM_unfold lapply (binary_to_bin_char … Heq) #Ha >binaryTM_bin0_true
 217     [| >Ht % ]
 218     lapply (IH (csl@[true]) (tape_move FinBool t R) ??????)
 219     [ //
 220     | >associative_append @Hcrd
 221     | >associative_append @Heq
 222     | >Ht whd in match (option_hd ??) in ⊢ (??%?); whd in match (tail ??) in ⊢ (??%?);
 223       cases csr0
 224       [ cases rs
 225         [ normalize >rev_append_def >rev_append_def >reverse_append %
 226         | #r1 #rs1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 227       | #c1 #csr1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 228     | /2 by lt_S_to_lt/
 229     |]
 230     #H whd in match (plus ??); >H @eq_f @eq_f2 %
 231   | #csr0 #IH #csl #t #ch #Hlen #Ht #Heq #Hcrd #Hch >loopM_unfold >loop_S_false [|normalize //]
 232     <loopM_unfold >binaryTM_bin0_false [| >Ht % ]
 233     lapply (IH (csl@[false]) (tape_move FinBool t R) ??????)
 234     [6: @ch
 235     | (* by cases: if index < |csl|, then Hch, else False *)
 236        @daemon
 237     | >associative_append @Hcrd
 238     | >associative_append @Heq
 239     | >Ht whd in match (option_hd ??) in ⊢ (??%?); whd in match (tail ??) in ⊢ (??%?);
 240       cases csr0
 241       [ cases rs
 242         [ normalize >rev_append_def >rev_append_def >reverse_append %
 243         | #r1 #rs1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 244       | #c1 #csr1 normalize >rev_append_def >rev_append_def >reverse_append % ]
 245     | /2 by lt_S_to_lt/
 246     |]
 247     #H whd in match (plus ??); >H @eq_f @eq_f2 %
 248   ]
 249 ]
 250 qed.
 251
 252 lemma binaryTM_phase0_midtape :
 253   ∀sig,M,t,q,ls,a,rs,ch,k.
 254   halt sig M q=false →
 255   t = mk_tape ? ls (option_hd ? (bin_char ? a)) (tail ? (bin_char sig a@rs)) →
 256   loopM ? (mk_binaryTM sig M) (S (length ? (bin_char ? a)) + k)
 257     (mk_config ?? (〈q,bin0,ch,length ? (bin_char ? a)〉) t)
 258   = loopM ? (mk_binaryTM sig M) k
 259       (mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉)
 260         (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [|@daemon|//]
 261 #sig #M #t #q #ls #a #rs #ch #k #Hhalt #Ht
 262 cut (∃c,cl.bin_char sig a = c::cl) [@daemon] * #c * #cl #Ha >Ha
 263 >(binaryTM_phase0_midtape_aux ? M q ls a rs ? ? (c::cl) [ ] t ch) //
 264 [| normalize #Hfalse @False_ind cases (not_le_Sn_O ?) /2/
 265 | <Ha (* |bin_char sig ?| = FS_crd sig *) @daemon
 266 | >Ha %
 267 | >Ht >Ha % ]
 268 <Ha %
 269 qed.
 270
 271 lemma binaryTM_phase0_None :
 272   ∀sig,M,t,q,ch,k,n.
 273   n < 2*FS_crd sig →
 274   halt sig M q=false →
 275   current ? t = None ? →
 276   loopM ? (mk_binaryTM sig M) (S k) (mk_config ?? (〈q,bin0,ch,S n〉) t)
 277   = loopM ? (mk_binaryTM sig M) k
 278       (mk_config ?? (〈q,bin4,None ?,to_initN O ??〉) (tape_move ? t R)). [2,3: /2 by le_to_lt_to_lt/ ]
 279 #sig #M #t #q #ch #k #n #Hn #Hhalt cases t
 280 [ >loopM_unfold >loop_S_false [|@Hhalt] //
 281 | #r0 #rs0 >loopM_unfold >loop_S_false [|@Hhalt] //
 282 | #l0 #ls0 >loopM_unfold >loop_S_false [|@Hhalt] //
 283 | #ls #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
 284 qed.
 285
 286 lemma binaryTM_bin1_O :
 287   ∀sig,M,t,q,ch.
 288   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin1,ch,O〉) t)
 289   = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t. [2,3://]
 290 #sig #M #t #q #ch %
 291 qed.
 292
 293 lemma binaryTM_bin1_S :
 294   ∀sig,M,t,q,ch,k. S k <S (2*FS_crd sig) →
 295   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin1,ch,S k〉) t)
 296   = mk_config ?? (〈q,bin1,ch,to_initN k ??〉) (tape_move ? t L). [2,3:/2 by lt_S_to_lt/]
 297 #sig #M #t #q #ch #k #HSk %
 298 qed.
 299
 300 lemma binaryTM_phase1 :
 301   ∀sig,M,q,ls1,ls2,cur,rs,ch,k.
 302   |ls1| = FS_crd sig → (cur = None ? → rs = [ ]) →
 303   loopM ? (mk_binaryTM sig M) (S (FS_crd sig) + k)
 304     (mk_config ?? (〈q,bin1,ch,FS_crd sig〉) (mk_tape ? (ls1@ls2) cur rs))
 305   = loopM ? (mk_binaryTM sig M) k
 306       (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
 307         (mk_tape ? ls2 (option_hd ? (reverse ? ls1@option_cons ? cur rs))
 308           (tail ? (reverse ? ls1@option_cons ? cur rs)))). [2,3:/2 by O/]
 309 cut (∀sig,M,q,ls1,ls2,ch,k,n,cur,rs.
 310   |ls1| = n →  n<S (2*FS_crd sig) → (cur = None ? → rs = [ ]) →
 311   loopM ? (mk_binaryTM sig M) (S n + k)
 312     (mk_config ?? (〈q,bin1,ch,n〉) (mk_tape ? (ls1@ls2) cur rs))
 313   = loopM ? (mk_binaryTM sig M) k
 314       (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
 315         (mk_tape ? ls2 (option_hd ? (reverse ? ls1@option_cons ? cur rs))
 316           (tail ? (reverse ? ls1@option_cons ? cur rs))))) [1,2://]
 317 [ #sig #M #q #ls1 #ls2 #ch #k elim ls1
 318   [ #n normalize in ⊢ (%→?); #cur #rs #Hn <Hn #Hcrd #Hcur >loopM_unfold >loop_S_false [| % ]
 319     >binaryTM_bin1_O cases cur in Hcur;
 320     [ #H >(H (refl ??)) -H %
 321     | #cur' #_ % ]
 322   | #l0 #ls0 #IH * [ #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
 323     #n #cur #rs normalize in ⊢ (%→?); #H destruct (H) #Hlt #Hcur
 324     >loopM_unfold >loop_S_false [|%] >binaryTM_bin1_S
 325     <(?:mk_tape ? (ls0@ls2) (Some ? l0) (option_cons ? cur rs) =
 326         tape_move FinBool (mk_tape FinBool ((l0::ls0)@ls2) cur rs) L)
 327     [| cases cur in Hcur; [ #H >(H ?) // | #cur' #_ % ] ]
 328     >(?:loop (config FinBool (states FinBool (mk_binaryTM sig M))) (S (|ls0|)+k)
 329       (step FinBool (mk_binaryTM sig M))
 330       (λc:config FinBool (states FinBool (mk_binaryTM sig M))
 331        .halt FinBool (mk_binaryTM sig M)
 332        (cstate FinBool (states FinBool (mk_binaryTM sig M)) c))
 333       (mk_config FinBool (states FinBool (mk_binaryTM sig M))
 334        〈q,bin1,ch,to_initN (|ls0|) (S (2*FS_crd sig))
 335         (lt_S_to_lt (|ls0|) (S (2*FS_crd sig)) Hlt)〉
 336        (mk_tape FinBool (ls0@ls2) (Some FinBool l0) (option_cons FinBool cur rs)))
 337       = loopM FinBool (mk_binaryTM sig M) k
 338          (mk_config FinBool (states FinBool (mk_binaryTM sig M))
 339           〈q,bin2,〈ch,FS_crd sig〉〉
 340           (mk_tape FinBool ls2
 341            (option_hd FinBool (reverse FinBool ls0@l0::option_cons FinBool cur rs))
 342            (tail FinBool (reverse FinBool ls0@l0::option_cons FinBool cur rs)))))
 343     [| /2/
 344     | >(?: l0::option_cons ? cur rs = option_cons ? (Some ? l0) (option_cons ? cur rs)) [| % ]
 345       @trans_eq [|| @(IH ??? (refl ??)) [ /2 by lt_S_to_lt/ | #H destruct (H) ] ]
 346       %
 347     ]
 348    >reverse_cons >associative_append %
 349  ]
 350 | #Hcut #sig #M #q #ls1 #ls2 #cur #rs #ch #k #Hlen @Hcut // ]
 351 qed.
 352
 353 lemma binaryTM_bin2_O_L :
 354   ∀sig,M,t,q,qn,ch,chn.
 355   〈qn,chn,L〉 = trans sig M 〈q,ch〉 →
 356   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,O〉) t)
 357   = mk_config ?? (〈qn,bin3,ch,to_initN (2*(FS_crd sig)) ??〉) (tape_move ? t L).[2,3:/2 by lt_S_to_lt/]
 358 #sig #M #t #q #qn #ch #chn #Htrans
 359 whd in match (step ???); whd in match (trans ???); <Htrans %
 360 qed.
 361
 362 lemma binaryTM_bin2_O_R :
 363   ∀sig,M,t,q,qn,ch,chn.
 364   〈qn,chn,R〉 = trans sig M 〈q,ch〉 →
 365   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,O〉) t)
 366   = mk_config ?? (〈qn,bin3,ch,to_initN O ??〉) t.[2,3://]
 367 #sig #M #t #q #qn #ch #chn #Htrans
 368 whd in match (step ???); whd in match (trans ???); <Htrans %
 369 qed.
 370
 371 lemma binaryTM_bin2_O_N :
 372   ∀sig,M,t,q,qn,ch,chn.
 373   〈qn,chn,N〉 = trans sig M 〈q,ch〉 →
 374   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,O〉) t)
 375   = mk_config ?? (〈qn,bin3,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t L).[2,3:/2 by lt_S_to_lt/]
 376 #sig #M #t #q #qn #ch #chn #Htrans
 377 whd in match (step ???); whd in match (trans ???); <Htrans %
 378 qed.
 379
 380 lemma binaryTM_bin2_S_None :
 381   ∀sig,M,t,q,qn,ch,mv,k.
 382   k< 2*FS_crd sig →
 383   〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 →
 384   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,S k〉) t)
 385   = mk_config ?? (〈q,bin2,ch,k〉) (tape_move ? t R).
 386 [2,3:/2 by le_to_lt_to_lt, transitive_lt/]
 387 #sig #M #t #q #qn #ch #mv #k #Hk #Htrans
 388 whd in match (step ???); whd in match (trans ???); <Htrans %
 389 qed.
 390
 391 lemma binaryTM_bin2_S_Some :
 392   ∀sig,M,t,q,qn,ch,chn,mv,k.
 393   k< 2*FS_crd sig →
 394   〈qn,Some ? chn,mv〉 = trans sig M 〈q,ch〉 →
 395   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin2,ch,S k〉) t)
 396   = mk_config ?? (〈q,bin2,ch,k〉) (tape_move ? (tape_write ? t (Some ? (FS_nth ? k == Some ? chn))) R).
 397 [2,3:/2 by le_to_lt_to_lt, transitive_lt/]
 398 #sig #M #t #q #qn #ch #chn #mv #k #Hk #Htrans
 399 whd in match (step ???); whd in match (trans ???); <Htrans %
 400 qed.
 401
 402 lemma binaryTM_phase2_Some_R :∀sig,M,q,ch,qn,chn,ls,rs,k,csr.
 403   〈qn,Some ? chn,R〉 = trans sig M 〈q,ch〉 →
 404   ∀cur,csl. |cur::csr|<S (2*FS_crd sig) →
 405   |csl@cur::csr| = FS_crd sig →
 406   (∃fs.bin_char sig chn = reverse ? csl@fs) →
 407   loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
 408     (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs)))
 409   = loopM ? (mk_binaryTM sig M) k
 410       (mk_config ?? (〈qn,bin3,ch,O〉)
 411         (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs))). [2,3://]
 412 #sig #M #q #ch #qn #chn #ls #rs #k #csr #Htrans elim csr
 413 [ #cur #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
 414   >(binaryTM_bin2_S_Some … Htrans) [| /2 by monotonic_pred/ ]
 415   >loop_S_false // @eq_f >(binaryTM_bin2_O_R … Htrans)
 416   @eq_f change with (midtape ? (csl@ls) (FS_nth sig O == Some ? chn) rs) in match (tape_write ???);
 417   cut (bin_char sig chn = reverse ? csl@[FS_nth sig O == Some sig chn]) [@daemon] #Hfs' >Hfs'
 418   >reverse_append >reverse_single >reverse_reverse >associative_append
 419   cases rs //
 420 | #b0 #bs0 #IH #cur #csl #Hcount #Hcrd * #fs #Hfs
 421   >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_Some … Htrans) [| @le_S_S_to_le @Hcount ]
 422   change with (midtape ? (((FS_nth ? (|b0::bs0|)==Some sig chn)::csl)@ls) b0 (bs0@rs))
 423     in match (tape_move ? (tape_write ???) ?); @IH
 424   [ <Hcrd >length_append >length_append normalize //
 425   | cases fs in Hfs;
 426     [ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ]
 427       -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|@daemon]
 428       <Hcrd >length_append normalize >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
 429       #Hfalse cut (S (S (|bs0|)) = O) /2 by injective_plus_r/ #H destruct (H)
 430     | #f0 #fs0 #Hbinchar
 431       cut (bin_char ? chn = reverse ? csl@(FS_nth ? (|b0::bs0|) == Some ? chn)::fs0) [@daemon]
 432       -Hbinchar #Hbinchar >Hbinchar %{fs0} >reverse_cons >associative_append %
 433     ]
 434   ]
 435 ]
 436 qed.
 437
 438 lemma binaryTM_phase2_Some_L :∀sig,M,q,ch,qn,chn,ls,rs,k,csr.
 439   〈qn,Some ? chn,L〉 = trans sig M 〈q,ch〉 →
 440   ∀cur,csl. |cur::csr|<S (2*FS_crd sig) →
 441   |csl@cur::csr| = FS_crd sig →
 442   (∃fs.bin_char sig chn = reverse ? csl@fs) →
 443   loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
 444     (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs)))
 445   = loopM ? (mk_binaryTM sig M) k
 446       (mk_config ?? (〈qn,bin3,ch,to_initN (2*FS_crd sig) ??〉)
 447         (tape_move ? (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs)) L)). [2,3://]
 448 #sig #M #q #ch #qn #chn #ls #rs #k #csr #Htrans elim csr
 449 [ #cur #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
 450   >(binaryTM_bin2_S_Some … Htrans) [| /2 by monotonic_pred/ ]
 451   >loop_S_false // @eq_f >(binaryTM_bin2_O_L … Htrans)
 452   @eq_f change with (midtape ? (csl@ls) (FS_nth sig O == Some ? chn) rs) in match (tape_write ???);
 453   cut (bin_char sig chn = reverse ? csl@[FS_nth sig O == Some sig chn]) [@daemon] #Hfs' >Hfs'
 454   >reverse_append >reverse_single >reverse_reverse >associative_append @eq_f2 //
 455   cases rs //
 456 | #b0 #bs0 #IH #cur #csl #Hcount #Hcrd * #fs #Hfs
 457   >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_Some … Htrans) [| @le_S_S_to_le @Hcount ]
 458   change with (midtape ? (((FS_nth ? (|b0::bs0|)==Some sig chn)::csl)@ls) b0 (bs0@rs))
 459     in match (tape_move ? (tape_write ???) ?); @IH
 460   [ <Hcrd >length_append >length_append normalize //
 461   | cases fs in Hfs;
 462     [ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ]
 463       -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|@daemon]
 464       <Hcrd >length_append normalize >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
 465       #Hfalse cut (S (S (|bs0|)) = O) /2 by injective_plus_r/ #H destruct (H)
 466     | #f0 #fs0 #Hbinchar
 467       cut (bin_char ? chn = reverse ? csl@(FS_nth ? (|b0::bs0|) == Some ? chn)::fs0) [@daemon]
 468       -Hbinchar #Hbinchar >Hbinchar %{fs0} >reverse_cons >associative_append %
 469     ]
 470   ]
 471 ]
 472 qed.
 473
 474 lemma binaryTM_phase2_Some_N :∀sig,M,q,ch,qn,chn,ls,rs,k,csr.
 475   〈qn,Some ? chn,N〉 = trans sig M 〈q,ch〉 →
 476   ∀cur,csl. |cur::csr|<S (2*FS_crd sig) →
 477   |csl@cur::csr| = FS_crd sig →
 478   (∃fs.bin_char sig chn = reverse ? csl@fs) →
 479   loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
 480     (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs)))
 481   = loopM ? (mk_binaryTM sig M) k
 482       (mk_config ?? (〈qn,bin3,ch,to_initN (FS_crd sig) ??〉)
 483         (tape_move ? (mk_tape ? (reverse ? (bin_char sig chn)@ls) (option_hd ? rs) (tail ? rs)) L)). [2,3://]
 484 #sig #M #q #ch #qn #chn #ls #rs #k #csr #Htrans elim csr
 485 [ #cur #csl #Hcount #Hcrd * #fs #Hfs >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
 486   >(binaryTM_bin2_S_Some … Htrans) [| /2 by monotonic_pred/ ]
 487   >loop_S_false // @eq_f >(binaryTM_bin2_O_N … Htrans)
 488   @eq_f change with (midtape ? (csl@ls) (FS_nth sig O == Some ? chn) rs) in match (tape_write ???);
 489   cut (bin_char sig chn = reverse ? csl@[FS_nth sig O == Some sig chn]) [@daemon] #Hfs' >Hfs'
 490   >reverse_append >reverse_single >reverse_reverse >associative_append @eq_f2 //
 491   cases rs //
 492 | #b0 #bs0 #IH #cur #csl #Hcount #Hcrd * #fs #Hfs
 493   >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_Some … Htrans) [| @le_S_S_to_le @Hcount ]
 494   change with (midtape ? (((FS_nth ? (|b0::bs0|)==Some sig chn)::csl)@ls) b0 (bs0@rs))
 495     in match (tape_move ? (tape_write ???) ?); @IH
 496   [ <Hcrd >length_append >length_append normalize //
 497   | cases fs in Hfs;
 498     [ #Hfalse cut (|bin_char ? chn| = |csl|) [ >Hfalse >length_append >length_reverse // ]
 499       -Hfalse >(?:|bin_char sig chn| = FS_crd sig) [|@daemon]
 500       <Hcrd >length_append normalize >(?:|csl| = |csl|+ O) in ⊢ (???%→?); //
 501       #Hfalse cut (S (S (|bs0|)) = O) /2 by injective_plus_r/ #H destruct (H)
 502     | #f0 #fs0 #Hbinchar
 503       cut (bin_char ? chn = reverse ? csl@(FS_nth ? (|b0::bs0|) == Some ? chn)::fs0) [@daemon]
 504       -Hbinchar #Hbinchar >Hbinchar %{fs0} >reverse_cons >associative_append %
 505     ]
 506   ]
 507 ]
 508 qed.
 509
 510 lemma binaryTM_phase2_None_R :∀sig,M,q,ch,qn,ls,rs,k,csr.
 511   〈qn,None ?,R〉 = trans sig M 〈q,ch〉 →
 512   ∀cur,csl. |cur::csr|<S (2*FS_crd sig) →
 513   |csl@cur::csr| = FS_crd sig →
 514   loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
 515     (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs)))
 516   = loopM ? (mk_binaryTM sig M) k
 517       (mk_config ?? (〈qn,bin3,ch,O〉)
 518         (mk_tape ? (reverse ? csr@cur::csl@ls) (option_hd ? rs) (tail ? rs))). [2,3://]
 519 #sig #M #q #ch #qn #ls #rs #k #csr #Htrans elim csr
 520 [ #cur #csl #Hcount #Hcrd >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
 521   >(binaryTM_bin2_S_None … Htrans) [| /2 by monotonic_pred/ ]
 522   >loop_S_false // @eq_f >(binaryTM_bin2_O_R … Htrans)
 523   @eq_f cases rs //
 524 | #b0 #bs0 #IH #cur #csl #Hcount #Hcrd
 525   >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_None … Htrans) [| @le_S_S_to_le @Hcount ]
 526   change with (midtape ? ((cur::csl)@ls) b0 (bs0@rs))
 527     in match (tape_move ???); >reverse_cons >associative_append
 528     normalize in match ([b0]@cur::csl@ls); @IH
 529   <Hcrd >length_append >length_append normalize //
 530 ]
 531 qed.
 532
 533 lemma binaryTM_phase2_None_L : ∀sig,M,q,ch,qn,ls,rs,k,csr.
 534   〈qn,None ?,L〉 = trans sig M 〈q,ch〉 →
 535   ∀cur,csl. |cur::csr|<S (2*FS_crd sig) →
 536   |csl@cur::csr| = FS_crd sig →
 537   loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
 538     (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs)))
 539   = loopM ? (mk_binaryTM sig M) k
 540       (mk_config ?? (〈qn,bin3,ch,to_initN (2*FS_crd sig) ??〉)
 541         (tape_move ? (mk_tape ? (reverse ? csr@cur::csl@ls) (option_hd ? rs) (tail ? rs)) L)). [2,3://]
 542 #sig #M #q #ch #qn #ls #rs #k #csr #Htrans elim csr
 543 [ #cur #csl #Hcount #Hcrd >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
 544   >(binaryTM_bin2_S_None … Htrans) [| /2 by monotonic_pred/ ]
 545   >loop_S_false // @eq_f >(binaryTM_bin2_O_L … Htrans)
 546   @eq_f cases rs //
 547 | #b0 #bs0 #IH #cur #csl #Hcount #Hcrd
 548   >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_None … Htrans) [| @le_S_S_to_le @Hcount ]
 549   change with (midtape ? ((cur::csl)@ls) b0 (bs0@rs))
 550     in match (tape_move ???); >reverse_cons >associative_append
 551     normalize in match ([b0]@cur::csl@ls); @IH
 552   <Hcrd >length_append >length_append normalize //
 553 ]
 554 qed.
 555
 556 lemma binaryTM_phase2_None_N :∀sig,M,q,ch,qn,ls,rs,k,csr.
 557   〈qn,None ?,N〉 = trans sig M 〈q,ch〉 →
 558   ∀cur,csl. |cur::csr|<S (2*FS_crd sig) →
 559   |csl@cur::csr| = FS_crd sig →
 560   loopM ? (mk_binaryTM sig M) (S (|cur::csr|) + k)
 561     (mk_config ?? (〈q,bin2,ch,|cur::csr|〉) (midtape ? (csl@ls) cur (csr@rs)))
 562   = loopM ? (mk_binaryTM sig M) k
 563       (mk_config ?? (〈qn,bin3,ch,to_initN (FS_crd sig) ??〉)
 564         (tape_move ? (mk_tape ? (reverse ? csr@cur::csl@ls) (option_hd ? rs) (tail ? rs)) L)). [2,3://]
 565 #sig #M #q #ch #qn #ls #rs #k #csr #Htrans elim csr
 566 [ #cur #csl #Hcount #Hcrd >loopM_unfold >loop_S_false // normalize in match (length ? [cur]);
 567   >(binaryTM_bin2_S_None … Htrans) [| /2 by monotonic_pred/ ]
 568   >loop_S_false // @eq_f >(binaryTM_bin2_O_N … Htrans)
 569   @eq_f cases rs //
 570 | #b0 #bs0 #IH #cur #csl #Hcount #Hcrd
 571   >loopM_unfold >loop_S_false // >(binaryTM_bin2_S_None … Htrans) [| @le_S_S_to_le @Hcount ]
 572   change with (midtape ? ((cur::csl)@ls) b0 (bs0@rs))
 573     in match (tape_move ???); >reverse_cons >associative_append
 574     normalize in match ([b0]@cur::csl@ls); @IH
 575   <Hcrd >length_append >length_append normalize //
 576 ]
 577 qed.
 578
 579 lemma binaryTM_bin3_O :
 580   ∀sig,M,t,q,ch.
 581   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin3,ch,O〉) t)
 582   = mk_config ?? (〈q,bin0,None ?,to_initN (FS_crd sig) ??〉) t. [2,3://]
 583 #sig #M #t #q #ch %
 584 qed.
 585
 586 lemma binaryTM_bin3_S :
 587   ∀sig,M,t,q,ch,k. S k <S (2*FS_crd sig) →
 588   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin3,ch,S k〉) t)
 589   = mk_config ?? (〈q,bin3,ch,to_initN k ??〉) (tape_move ? t L). [2,3:/2 by lt_S_to_lt/]
 590 #sig #M #t #q #ch #k #HSk %
 591 qed.
 592
 593 lemma binaryTM_phase3 :∀sig,M,q,ls1,ls2,ch,k,n,cur,rs.
 594   |ls1| = n →  n<S (2*FS_crd sig) → (cur = None ? → rs = [ ]) →
 595   loopM ? (mk_binaryTM sig M) (S n + k)
 596     (mk_config ?? (〈q,bin3,ch,n〉) (mk_tape ? (ls1@ls2) cur rs))
 597   = loopM ? (mk_binaryTM sig M) k
 598       (mk_config ?? (〈q,bin0,None ?,FS_crd sig〉)
 599         (mk_tape ? ls2 (option_hd ? (reverse ? ls1@option_cons ? cur rs))
 600           (tail ? (reverse ? ls1@option_cons ? cur rs)))). [2,3://]
 601 #sig #M #q #ls1 #ls2 #ch #k elim ls1
 602 [ #n normalize in ⊢ (%→?); #cur #rs #Hn <Hn #Hcrd #Hcur >loopM_unfold >loop_S_false [| % ]
 603   >binaryTM_bin3_O cases cur in Hcur;
 604   [ #H >(H (refl ??)) -H %
 605   | #cur' #_ % ]
 606 | #l0 #ls0 #IH * [ #cur #rs normalize in ⊢ (%→?); #H destruct (H) ]
 607   #n #cur #rs normalize in ⊢ (%→?); #H destruct (H) #Hlt #Hcur
 608   >loopM_unfold >loop_S_false [|%] >binaryTM_bin3_S
 609   <(?:mk_tape ? (ls0@ls2) (Some ? l0) (option_cons ? cur rs) =
 610       tape_move FinBool (mk_tape FinBool ((l0::ls0)@ls2) cur rs) L)
 611   [| cases cur in Hcur; [ #H >(H ?) // | #cur' #_ % ] ]
 612   >(?:loop (config FinBool (states FinBool (mk_binaryTM sig M))) (S (|ls0|)+k)
 613     (step FinBool (mk_binaryTM sig M))
 614     (λc:config FinBool (states FinBool (mk_binaryTM sig M))
 615      .halt FinBool (mk_binaryTM sig M)
 616      (cstate FinBool (states FinBool (mk_binaryTM sig M)) c))
 617     (mk_config FinBool (states FinBool (mk_binaryTM sig M))
 618      〈q,bin3,ch,to_initN (|ls0|) (S (2*FS_crd sig))
 619       (lt_S_to_lt (|ls0|) (S (2*FS_crd sig)) Hlt)〉
 620      (mk_tape FinBool (ls0@ls2) (Some FinBool l0) (option_cons FinBool cur rs)))
 621     = loopM FinBool (mk_binaryTM sig M) k
 622        (mk_config FinBool (states FinBool (mk_binaryTM sig M))
 623         〈q,bin0,〈None ?,FS_crd sig〉〉
 624         (mk_tape FinBool ls2
 625          (option_hd FinBool (reverse FinBool ls0@l0::option_cons FinBool cur rs))
 626          (tail FinBool (reverse FinBool ls0@l0::option_cons FinBool cur rs)))))
 627   [| /2/
 628   | >(?: l0::option_cons ? cur rs = option_cons ? (Some ? l0) (option_cons ? cur rs)) [| % ]
 629     @trans_eq [|| @(IH ??? (refl ??)) [ /2 by lt_S_to_lt/ | #H destruct (H) ] ]
 630     %
 631   ]
 632  >reverse_cons >associative_append %
 633 ]
 634 qed.
 635
 636 lemma binaryTM_bin4_None :
 637   ∀sig,M,t,q,ch.
 638   current ? t = None ? →
 639   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
 640   = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t. [2,3://]
 641 #sig #M #t #q #ch #Hcur whd in ⊢ (??%?); >Hcur %
 642 qed.
 643
 644 lemma binaryTM_bin4_noextend :
 645   ∀sig,M,t,q,ch,cur,qn,mv.
 646   current ? t = Some ? cur →
 647   〈qn,None ?,mv〉 = trans sig M 〈q,ch〉 →
 648   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
 649   = mk_config ?? (〈q,bin2,ch,to_initN O ??〉) t. [2,3://]
 650 #sig #M #t #q #ch #cur #qn #mv #Hcur #Htrans
 651 whd in ⊢ (??%?); >Hcur whd in ⊢ (??%?);
 652 whd in match (trans FinBool ??); <Htrans %
 653 qed.
 654
 655 lemma binaryTM_bin4_extend :
 656   ∀sig,M,t,q,ch,cur,qn,an,mv.
 657   current ? t = Some ? cur →
 658   〈qn,Some ? an,mv〉 = trans sig M 〈q,ch〉 →
 659   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin4,ch,O〉) t)
 660   = mk_config ?? (〈q,bin5,ch,to_initN (FS_crd sig) ??〉) (tape_move ? t L). [2,3://]
 661 #sig #M #t #q #ch #cur #qn #an #mv #Hcur #Htrans
 662 whd in ⊢ (??%?); >Hcur whd in ⊢ (??%?);
 663 whd in match (trans FinBool ??); <Htrans %
 664 qed.
 665
 666 lemma binaryTM_bin5_O :
 667   ∀sig,M,t,q,ch.
 668   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin5,ch,O〉) t)
 669   = mk_config ?? (〈q,bin2,ch,to_initN (FS_crd sig) ??〉) t. [2,3://]
 670 #sig #M #t #q #ch %
 671 qed.
 672
 673 lemma binaryTM_bin5_S :
 674   ∀sig,M,t,q,ch,k. S k <S (2*FS_crd sig) →
 675   step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin5,ch,S k〉) t)
 676   = mk_config ?? (〈q,bin5,ch,to_initN k ??〉) (tape_move ? (tape_write ? t (Some ? false)) L). [2,3:/2 by lt_S_to_lt/]
 677 #sig #M #t #q #ch #k #HSk %
 678 qed.
 679
 680 (* extends the tape towards the left with an unimportant sequence that will be
 681    immediately overwritten *)
 682 lemma binaryTM_phase5 :∀sig,M,q,ch,k,n,rs.
 683   n<S (2*FS_crd sig) →
 684   ∃bs.|bs| = n ∧
 685   loopM ? (mk_binaryTM sig M) (S n + k)
 686     (mk_config ?? (〈q,bin5,ch,n〉) (mk_tape ? [] (None ?) rs))
 687   = loopM ? (mk_binaryTM sig M) k
 688       (mk_config ?? (〈q,bin2,ch,FS_crd sig〉)
 689         (mk_tape ? [] (None ?) (bs@rs))). [2,3://]
 690 #sig #M #q #ch #k #n elim n
 691 [ #rs #Hlt %{[]} % %
 692 | #n0 #IH #rs #Hn0 cases (IH (false::rs) ?) [|/2 by lt_S_to_lt/]
 693   #bs * #Hbs -IH #IH
 694   %{(bs@[false])} % [ <Hbs >length_append /2 by plus_to_minus/ ]
 695   >loopM_unfold >loop_S_false // >binaryTM_bin5_S
 696   >associative_append normalize in match ([false]@?); <IH
 697   >loopM_unfold @eq_f @eq_f cases rs //
 698 ]
 699 qed.
 700
 701 lemma binaryTM_loop :
 702  ∀sig,M,i,t,q,tf,qf.
 703  loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) →
 704  ∃k.loopM ? (mk_binaryTM sig M) k
 705   (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) =
 706   Some ? (mk_config ?? (state_bin_lift ? M qf) (tape_bin_lift ? tf)).
 707 #sig #M #i elim i
 708 [ #t #q #qf #tf change with (None ?) in ⊢ (??%?→?); #H destruct (H)
 709 | -i #i #IH #t #q #tf #qf
 710   >loopM_unfold
 711   lapply (refl ? (halt sig M (cstate ?? (mk_config ?? q t))))
 712   cases (halt ?? q) in ⊢ (???%→?); #Hhalt
 713   [ >(loop_S_true ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)
 714     #H destruct (H) %{1} >loopM_unfold >loop_S_true // ]
 715   (* interesting case: more than one step *)
 716   >(loop_S_false ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)
 717   <loopM_unfold >(config_expand ?? (step ???)) #Hloop
 718   lapply (IH … Hloop) -IH * #k0 #IH <config_expand in Hloop; #Hloop
 719   %{(S k0)}
 720
 721
 722
 723 (*
 724 theorem sem_binaryTM : ∀sig,M.
 725   mk_binaryTM sig M ⊫ R_bin_lift ? (R_TM ? M (start ? M)).
 726 #sig #M #t #i generalize in match t; -t
 727 @(nat_elim1 … i) #m #IH #intape #outc #Hloop
 728
 729 *)