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