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