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