+ [ %{(S i)} % //
+ >(loop_S_true ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt) %
+ [| #H destruct (H)]
+ #H destruct (H) >loopM_unfold >loop_S_true // ]
+ (* interesting case: more than one step *)
+ >(loop_S_false ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt)cases (current_None_or_midtape ? t)
+ (*** current = None ***)
+ [ #Hcur lapply (current_tape_bin_list … Hcur) #Hcur'
+ cut (∃qn,chn,mv.〈qn,chn,mv〉 = trans ? M 〈q,None ?〉)
+ [ cases (trans ? M 〈q,None ?〉) * #qn #chn #mv /4 by ex_intro/ ]
+ * #qn * #chn * #mv cases chn -chn
+ [ #Htrans lapply (binaryTM_phase0_None_None … (None ?) (FS_crd sig) … Hhalt Hcur' Htrans) // [/2 by monotonic_lt_plus_l/]
+ lapply (binaryTM_phase3 ? M qn (None ?) (displ2_of_move sig mv) ? (tape_move FinBool (tape_bin_lift sig t) (mv_tech mv))) [//]
+ cases (IH (tape_move ? t mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
+ #phase3 #phase0 %{(S (S (displ2_of_move sig mv))+k0)} %
+ [ @le_S_S @(le_plus O) // ]
+ >state_bin_lift_unfold >phase0 [|//]
+ >phase3 [|//]
+ >(?: S (S (displ2_of_move sig mv))+k0-1-S (displ2_of_move sig mv) = k0)
+ [| /2 by refl, plus_to_minus/ ]
+ cut (tape_move sig t mv=tape_move sig (tape_write sig t (None sig)) mv) [%] #Hcut
+ >(?: iter ? (λt0.tape_move ? t0 L) (displ2_of_move sig mv) (tape_move ? (tape_bin_lift ? t) (mv_tech mv))
+ =tape_bin_lift ? (tape_move ? t mv))
+ [|cases t in Hcur;
+ [4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H)
+ | #_ whd in match (tape_bin_lift ??);
+ (* TODO *)
+ (* ∀mv.tape_move ? (niltape ?) mv = niltape ? *)
+ (* ∀n.iter ? (λt.tape_move ? t ?) n (niltape ?) = niltape ? *)
+ @daemon
+ | #r0 #rs0 #_ cases mv
+ [ >tape_bin_lift_unfold whd in match (mv_tech L); whd in match (displ2_of_move sig L);
+ whd in match (rev_bin_list ??); whd in match (option_hd ??);
+ whd in match (right ??); >(?: []@bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
+ (* TODO *)
+ (* tape_move (mk_tape [ ] (None ?) rs R = ... *)
+ (* use iter_tape_move_R *)
+ @daemon
+ | >tape_bin_lift_unfold whd in match (mv_tech R); whd in match (displ2_of_move sig R);
+ whd in match (rev_bin_list ??); whd in match (option_hd ??);
+ whd in match (right ??); >(?: []@bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
+ whd in match (tape_move ? (leftof ???) R);
+ >tape_bin_lift_unfold >left_midtape >opt_bin_char_Some >right_midtape
+ >iter_O
+ (* TODO *)
+ (* tape_move (mk_tape [ ] (None ?) rs R = ... *)
+ @daemon
+ | >tape_bin_lift_unfold % ]
+ | #l0 #ls0 #_ cases mv
+ [ >tape_bin_lift_unfold whd in match (mv_tech L); whd in match (displ2_of_move sig L);
+ whd in match (bin_list ??); >append_nil whd in match (option_hd ??);
+ whd in match (left ??); whd in match (tail ??);
+ whd in match (tape_move ? (rightof ???) L);
+ >(?: rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
+ (* TODO *)
+ (* tape_move (mk_tape ls (None ?) [ ] R = ... *)
+ (* use iter_tape_move_L *)
+ @daemon
+ | >tape_bin_lift_unfold whd in match (mv_tech R); whd in match (displ2_of_move sig R);
+ whd in match (bin_list ??); >append_nil whd in match (option_hd ??);
+ whd in match (left ??); whd in match (tail ??); >iter_O cases (rev_bin_list ??) //
+ | >tape_bin_lift_unfold % ]
+ ]
+ ]
+ %
+ [ #Hloop @IH <Hloop @eq_f whd in ⊢ (???%); >Hcur <Htrans @eq_f @Hcut
+ | #Hloop @IHNone <Hloop @eq_f whd in ⊢ (???%); >Hcur <Htrans @eq_f @Hcut ]
+ | #chn #Htrans
+ lapply (binaryTM_phase0_None_Some … (None ?) (FS_crd sig) … Hhalt Hcur' Htrans) // [/2 by monotonic_lt_plus_l/]
+ cases t in Hcur;
+ [ 4: #ls #c #rs normalize in ⊢ (%→?); #H destruct (H)
+ | 2: #r0 #rs0 #_ cut (∃b,bs.bin_char ? r0 = b::bs) [ @daemon ] * #b * #bs #Hbs
+ lapply (binaryTM_phase4_extend ???? (tape_move ? (tape_bin_lift ? (leftof ? r0 rs0)) R) b … Htrans)
+ [ >tape_bin_lift_unfold whd in match (option_hd ??); whd in match (tail ??);
+ whd in match (right ??);
+ >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
+ >Hbs % ]
+ cases (binaryTM_phase5 ? M q (None ?) (FS_crd sig) (bin_list ? (r0::rs0)) ?) [|//]
+ #cs * #Hcs
+ lapply (binaryTM_phase2_Some_ow ?? q (None ?) … [ ] ? (bin_list ? (r0::rs0)) Htrans Hcs)
+ lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ?
+ (mk_tape FinBool (reverse bool (bin_char sig chn)@[])
+ (option_hd FinBool (bin_list sig (r0::rs0))) (tail FinBool (bin_list sig (r0::rs0))))) [//]
+ cases (IH (tape_move ? (tape_write ? (leftof ? r0 rs0) (Some ? chn)) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
+ #phase3 #phase2 #phase5 #phase4 #phase0
+ %{(1 + 1 + (S (FS_crd sig)) + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} %
+ [ @le_S_S @(le_plus O) // ]
+ >state_bin_lift_unfold >phase0 [|//]
+ >phase4 [|//]
+ >(?: loopM ? (mk_binaryTM ??) ? (mk_config ?? 〈q,bin5,None ?,to_initN ???〉 ?) = ?)
+ [|| @(trans_eq ????? (phase5 ??))
+ [ @eq_f @eq_f
+ >tape_bin_lift_unfold whd in match (rev_bin_list ??);
+ whd in match (right ??); whd in match (bin_list ??);
+ cases (bin_char ? r0) // (* bin_char can't be nil *) @daemon
+ | @le_S_S >associative_plus >associative_plus >commutative_plus @(le_plus O) //
+ |]]
+ >phase2 [| (*arith*) @daemon ]
+ >phase3 [| (*arith*) @daemon ]
+ >(?: 1+1+S (FS_crd sig)+S (FS_crd sig)+S (displ_of_move sig mv)+k0-1-1
+ -S (FS_crd sig)-S (FS_crd sig) -S (displ_of_move sig mv) = k0)
+ [| (*arith*) @daemon ]
+ -phase0 -phase2 -phase3 -phase4 -phase5 <state_bin_lift_unfold
+ >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
+ (mk_tape ? (reverse ? (bin_char sig chn)@[])
+ (option_hd FinBool (bin_list sig (r0::rs0)))
+ (tail FinBool (bin_list sig (r0::rs0))))
+ = tape_bin_lift ? (tape_move ? (tape_write ? (leftof ? r0 rs0) (Some ? chn)) mv))
+ [ % #Hloop
+ [ @IH <Hloop @eq_f whd in ⊢ (???%); <Htrans %
+ | @IHNone <Hloop @eq_f whd in ⊢ (???%); <Htrans % ]
+ | >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
+ cases mv
+ [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
+ >iter_split >iter_tape_move_L [| @daemon ]
+ >hd_tech [|@daemon] >tail_tech [|@daemon] >iter_tape_move_L_left [|//]
+ whd in match (tape_move ???); >tape_bin_lift_unfold %
+ | normalize in match (displ_of_move ??); >iter_O
+ normalize in match (tape_move ???);
+ >tape_bin_lift_unfold >opt_bin_char_Some
+ >hd_tech [|@daemon] >tail_tech [| @daemon ] %
+ | normalize in match (displ_of_move ??);
+ >iter_tape_move_L [|@daemon]
+ normalize in match (tape_move ???); >tape_bin_lift_unfold
+ >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ]
+ ]
+ | #_ lapply (binaryTM_phase4_write ? M q (None ?) (niltape ?) (refl ??))
+ lapply (binaryTM_phase2_Some_of ?? q (None ?) … [ ] Htrans)
+ lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ?
+ (mk_tape FinBool (reverse bool (bin_char sig chn)@[]) (None ?) [ ])) [//]
+ cases (IH (tape_move ? (midtape ? [ ] chn [ ]) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
+ #phase3 #phase2 #phase4 #phase0
+ %{(1 + 1 + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} %
+ [ @le_S_S @(le_plus O) // ]
+ >state_bin_lift_unfold >phase0 [|//]
+ >phase4 [|//]
+ >phase2 [|(*arith *) @daemon]
+ >phase3 [| (*arith*) @daemon ]
+ >(?: 1+1+S (FS_crd sig) + S (displ_of_move sig mv)+k0-1-1
+ -S (FS_crd sig)-S (displ_of_move sig mv) = k0)
+ [| (*arith*) @daemon ]
+ -phase0 -phase2 -phase3 -phase4 <state_bin_lift_unfold
+ >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
+ (mk_tape ? (reverse ? (bin_char sig chn)@[]) (None ?) [ ])
+ = tape_bin_lift ? (tape_move ? (tape_write ? (niltape ?) (Some ? chn)) mv))
+ [ % #Hloop
+ [ @IH <Hloop @eq_f whd in ⊢ (???%); <Htrans %
+ | @IHNone <Hloop @eq_f whd in ⊢ (???%); <Htrans % ]
+ | cases mv
+ [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
+ >iter_split change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????(????%))?);
+ >iter_tape_move_L [| @daemon ]
+ >append_nil in ⊢ (??(????(???%?))?); >tail_tech [|@daemon]
+ >iter_tape_move_L_left [|//]
+ normalize in match (tape_move ???);
+ >tape_bin_lift_unfold %
+ | normalize in match (displ_of_move ??); >iter_O
+ normalize in match (tape_move ???);
+ >tape_bin_lift_unfold %
+ | normalize in match (displ_of_move ??);
+ change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????%)?);
+ >iter_tape_move_L [|@daemon]
+ normalize in match (tape_move ???); >tape_bin_lift_unfold
+ >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ]
+ ]
+ | #l0 #ls0 #_ lapply (binaryTM_phase4_write ? M q (None ?) (tape_bin_lift ? (rightof ? l0 ls0)) ?)
+ [ >tape_bin_lift_unfold >current_mk_tape % ]
+ lapply (binaryTM_phase2_Some_of ?? q (None ?) … (rev_bin_list ? (l0::ls0)) Htrans)
+ lapply (binaryTM_phase3 ? M qn (None ?) (displ_of_move sig mv) ?
+ (mk_tape FinBool (reverse bool (bin_char sig chn)@rev_bin_list ? (l0::ls0)) (None ?) [ ])) [//]
+ cases (IH (tape_move ? (midtape ? (l0::ls0) chn [ ]) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
+ #phase3 #phase2 #phase4 #phase0
+ %{(1 + 1 + (S (FS_crd sig)) + S (displ_of_move sig mv) + k0)} %
+ [ @le_S_S @(le_plus O) // ]
+ >state_bin_lift_unfold >phase0 [|//]
+ >(?:tape_move ? (tape_bin_lift ? (rightof ? l0 ls0)) R = tape_bin_lift ? (rightof ? l0 ls0))
+ [| >tape_bin_lift_unfold normalize in match (option_hd ??); normalize in match (right ??);
+ normalize in match (tail ??); normalize in match (left ??);
+ >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
+ cases (reverse ? (bin_char ? l0)) // cases (rev_bin_list ? ls0) // ]
+ >phase4 [|//]
+ >phase2 [|(*arith *) @daemon]
+ >phase3 [| (*arith*) @daemon]
+ >(?: 1+1+S (FS_crd sig) + S (displ_of_move sig mv)+k0-1-1
+ -S (FS_crd sig)-S (displ_of_move sig mv) = k0)
+ [| (*arith*) @daemon ]
+ -phase0 -phase2 -phase3 -phase4 <state_bin_lift_unfold
+ >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
+ (mk_tape ? (reverse ? (bin_char sig chn)@rev_bin_list ? (l0::ls0)) (None ?) [ ])
+ = tape_bin_lift ? (tape_move ? (tape_write ? (rightof ? l0 ls0) (Some ? chn)) mv))
+ [ % #Hloop
+ [ @IH <Hloop @eq_f whd in ⊢ (???%); <Htrans %
+ | @IHNone <Hloop @eq_f whd in ⊢ (???%); <Htrans % ]
+ | cases mv
+ [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
+ >iter_split change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????(????%))?);
+ >iter_tape_move_L [| @daemon ]
+ >append_nil in ⊢ (??(????(???%?))?); >tail_tech [|@daemon]
+ >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
+ >append_nil >iter_tape_move_L [|@daemon]
+ normalize in match (tape_move ???);
+ >tape_bin_lift_unfold @eq_f2
+ [ >hd_tech [|@daemon] %
+ | >tail_tech [|@daemon] >opt_bin_char_Some normalize in match (bin_list ??); >append_nil %]
+ | normalize in match (displ_of_move ??); >iter_O
+ normalize in match (tape_move ???);
+ >tape_bin_lift_unfold %
+ | normalize in match (displ_of_move ??);
+ change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????%)?);
+ >iter_tape_move_L [|@daemon]
+ normalize in match (tape_move ???); >tape_bin_lift_unfold
+ >opt_bin_char_Some >hd_tech [|@daemon] >tail_tech [|@daemon] % ]
+ ]
+ ]
+ ]
+ (*** midtape ***)
+ | * #ls * #c * #rs #Ht >Ht