+ | normalize in match (displ_of_move ??);
+ change with (mk_tape ?? (option_hd ? [ ]) (tail ? [ ])) in ⊢ (??(????%)?);
+ >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
+ normalize in match (tape_move ???); >tape_bin_lift_unfold
+ >opt_bin_char_Some >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] % ]
+ ]
+ | #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 [|<plus_minus [|//] // ]
+ >phase3 [|<plus_minus [|//] <plus_minus [|//] // ]
+ >(?: 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)
+ [| <plus_minus [|//] <plus_minus [|//] // ]
+ -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 [|>eq_length_bin_char_FS_crd // ]
+ >append_nil in ⊢ (??(????(???%?))?); >tail_tech [|>eq_length_bin_char_FS_crd // ]
+ >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
+ >append_nil >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
+ normalize in match (tape_move ???);
+ >tape_bin_lift_unfold @eq_f2
+ [ >hd_tech [|>eq_length_bin_char_FS_crd // ] %
+ | >tail_tech [|>eq_length_bin_char_FS_crd // ] >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 [|>eq_length_bin_char_FS_crd // ]
+ normalize in match (tape_move ???); >tape_bin_lift_unfold
+ >opt_bin_char_Some >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] % ]
+ ]
+ ]
+ ]
+ (*** midtape ***)
+ | * #ls * #c * #rs #Ht >Ht
+ cut (∃qn,chn,mv.〈qn,chn,mv〉 = trans ? M 〈q,Some ? c〉)
+ [ cases (trans ? M 〈q,Some ? c〉) * #qn #chn #mv /4 by ex_intro/ ]
+ * #qn * #chn * #mv #Htrans
+ cut (tape_bin_lift ? t = ?) [| >tape_bin_lift_unfold % ]
+ >Ht in ⊢ (???%→?); >opt_bin_char_Some >left_midtape >right_midtape #Ht'
+ lapply (binaryTM_phase0_midtape ?? (tape_bin_lift ? t) q … (None ?) Hcrd Hhalt Ht')
+ lapply (binaryTM_phase1 ?? q (reverse ? (bin_char ? c)) (rev_bin_list ? ls)
+ (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)) (Some ? c) ??)
+ [ cases (bin_list ? rs) // #r0 #rs0 normalize in ⊢ (%→?); #H destruct (H)
+ | >length_reverse >eq_length_bin_char_FS_crd // |]
+ >opt_cons_hd_tl >reverse_reverse
+ cases chn in Htrans; -chn
+ [ #Htrans
+ lapply (binaryTM_phase2_None … Htrans (FS_crd sig) ?
+ (mk_tape FinBool (rev_bin_list sig ls)
+ (option_hd FinBool (bin_char sig c@bin_list sig rs))
+ (tail FinBool (bin_char sig c@bin_list sig rs)))) [//]
+ lapply (binaryTM_phase3 ? M qn (Some ? c) (displ_of_move sig mv) ?
+ (mk_tape FinBool (reverse bool (bin_char sig c)@rev_bin_list ? ls)
+ (option_hd FinBool (bin_list sig rs)) (tail FinBool (bin_list sig rs)))) [//]
+ cases (IH (tape_move ? (tape_write ? (midtape ? ls c rs) (None ?)) mv) qn) -IH #k0 * #Hk0 * #IH #IHNone
+ #phase3 #phase2 #phase1 #phase0
+ %{(S (FS_crd sig) + 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 <Ht >phase0 [|//]
+ >phase1 [|/2 by monotonic_le_minus_l/]
+ >phase2 [|/2 by monotonic_le_minus_l/]
+ >iter_tape_move_R [|>eq_length_bin_char_FS_crd // ]
+ >phase3 [|/2 by monotonic_le_minus_l/]
+ -phase0 -phase1 -phase2 -phase3
+ >(?: S (FS_crd sig) + S (FS_crd sig) + S (FS_crd sig) + S (displ_of_move sig mv) + k0
+ - S (FS_crd sig) - S (FS_crd sig) - S (FS_crd sig) - S (displ_of_move sig mv)
+ = k0) [| <plus_minus [|//] <plus_minus [|//] <plus_minus [|//] // ]
+ <state_bin_lift_unfold
+ >(?: iter ? (λt0.tape_move ? t0 L) (displ_of_move sig mv)
+ (mk_tape ? (reverse ? (bin_char sig c)@rev_bin_list ? ls)
+ (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)))
+ = tape_bin_lift ? (tape_move ? (tape_write ? (midtape ? ls c rs) (None ?)) mv))
+ [ % #Hloop
+ [ @IH <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans %
+ | @IHNone <Hloop @eq_f whd in ⊢ (???%); >Ht <Htrans % ]
+ | normalize in match (tape_write ???); cases mv in Htrans; #Htrans
+ [ >(?:displ_of_move sig L = FS_crd sig+FS_crd sig) [|normalize //]
+ >iter_split >iter_tape_move_L [| >eq_length_bin_char_FS_crd // ]
+ cases ls
+ [ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ]
+ >iter_tape_move_L_left [|//]
+ >tape_bin_lift_unfold %
+ | #l0 #ls0 >(?:rev_bin_list ? (l0::ls0) = reverse ? (bin_char ? l0)@rev_bin_list ? ls0) [|%]
+ normalize in match (tape_move ???);
+ >iter_tape_move_L [|>eq_length_bin_char_FS_crd // ]
+ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ]
+ >tape_bin_lift_unfold % ]
+ | normalize in match (displ_of_move ??); >iter_O cases rs
+ [ normalize in match (tape_move ???); >tape_bin_lift_unfold %
+ | #r0 #rs0 normalize in match (tape_move ???);
+ >tape_bin_lift_unfold >opt_bin_char_Some
+ >left_midtape >right_midtape
+ >(?:bin_list ? (r0::rs0) = bin_char ? r0@bin_list ? rs0) [|%]
+ >hd_tech [|>eq_length_bin_char_FS_crd // ]
+ >tail_tech [|>eq_length_bin_char_FS_crd // ] %