+ | #Ht >Ht >binaryTM_bin4_None // <loopM_unfold *)
+ (* 0.2) midtape *)
+ | * #ls * #c * #rs #Ht >Ht >tape_bin_lift_unfold
+ >left_midtape >current_midtape >right_midtape >opt_bin_char_Some
+ >(binaryTM_phase0_midtape … Hhalt ? (refl ??)) [| // ]
+ >(?: 7*S (FS_crd sig) + k0 - S (FS_crd sig) = 6*S (FS_crd sig) + k0) [|/2 by plus_minus/]
+ (*** PHASE 1 ***)
+ >binaryTM_phase1
+ [| cases (bin_list ? rs) normalize // #r0 #rs0 #H destruct (H)
+ | >length_reverse @daemon
+ | // ]
+ >(?:6*S (FS_crd sig) + k0 - S (FS_crd sig) = 5*S (FS_crd sig) + k0) [|/2 by plus_minus/]
+ >reverse_reverse >opt_cons_hd_tl
+ 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 cases chn -chn
+ [ (* no write! *) #Htrans >(binaryTM_phase2_None … Htrans) [2,3: //]
+ >iter_tape_move_R [|@daemon]
+ >(?:5*S (FS_crd sig) + k0 - S (FS_crd sig) = 4*S (FS_crd sig) + k0) [|/2 by plus_minus/]
+ >binaryTM_phase3
+ [|//| cut (S (displ_of_move sig mv) ≤ 2*(S (FS_crd sig)))
+ [ /2 by le_S_S/
+ | #H @(transitive_le ??? H) -H -Hcrd @(transitive_le ? (4*S (FS_crd sig))) /2 by le_plus_a/ ]
+ ]
+ cut (∀sig,M,m,n,cfg,cfg'.m < n → loopM sig M m cfg = Some ? cfg' → loopM sig M n cfg = Some ? cfg') [@daemon]
+ #Hcut <(Hcut ??? (4*S (FS_crd sig) + k0 - S (displ_of_move sig mv)) ??? IH)
+ [| cases mv
+ [ >(?:displ_of_move sig L = 2*FS_crd sig) //
+ >eq_minus_S_pred
+ @(transitive_le ? (pred (4*FS_crd sig+k0-2*FS_crd sig)))
+ [ >(?:4*FS_crd sig+k0-2*FS_crd sig = 2*FS_crd sig + k0)
+ [ cases Hcrd /2 by le_minus_to_plus, le_n/
+ | <plus_minus [2://]
+ >(commutative_times 4) >(commutative_times 2)
+ <distributive_times_minus //
+ ]
+ | @monotonic_pred /2 by monotonic_le_minus_l/ ]
+ | whd in match (displ_of_move ??); @(transitive_le ? (4*1+k0-1))
+ [ //
+ | change with (pred (4*1+k0)) in ⊢ (?%?);
+ >eq_minus_S_pred <minus_n_O @monotonic_pred // ]
+ | >(?:displ_of_move sig N = FS_crd sig) //
+ >eq_minus_S_pred
+ @(transitive_le ? (pred (4*FS_crd sig+k0-1*FS_crd sig)))
+ [ >(?:4*FS_crd sig+k0-1*FS_crd sig = 3*FS_crd sig + k0)
+ [ cases Hcrd /2 by le_minus_to_plus, le_n/
+ | <plus_minus [2://]
+ >(commutative_times 4) >(commutative_times 1)
+ <distributive_times_minus //
+ ]
+ | @monotonic_pred /2 by transitive_le, le_n/ ] ] ]
+ @eq_f @eq_f2
+ [ <state_bin_lift_unfold >Ht whd in match (step ???); <Htrans %
+ | (* must distinguish mv *)
+ cases mv in Htrans; #Htrans
+ [ >(?:displ_of_move ? L = FS_crd sig + FS_crd sig) [| normalize // ]
+ >iter_split >iter_tape_move_L [|@daemon] >Ht cases ls
+ [ normalize in match (rev_bin_list ??);
+ >hd_tech [|@daemon] >tail_tech [|@daemon]
+ >iter_tape_move_L_left // whd in match (step ???);
+ <Htrans whd in match (ctape ???);
+ >tape_bin_lift_unfold %
+ | #l0 #ls0 change with (reverse ? (bin_char ? l0)@rev_bin_list ? ls0) in match (rev_bin_list ??);
+ >iter_tape_move_L [|@daemon]
+ >hd_tech [|@daemon] >tail_tech [|@daemon]
+ whd in match (step ???); <Htrans whd in match (ctape ???);
+ >tape_bin_lift_unfold >left_midtape >current_midtape
+ >opt_bin_char_Some >right_midtape %
+ ]
+ | change with
+ (mk_tape ? (reverse ? (bin_char ? c)@rev_bin_list ? ls)
+ (option_hd ? (bin_list ? rs)) (tail ? (bin_list ? rs)))
+ in ⊢ (??%?);
+ >reverse_bin_char_list <IH
+ >Ht >tape_bin_lift_unfold @eq_f3
+ whd in match (step ???); <Htrans cases rs //
+ #r0 #rs0 whd in match (ctape ???); >current_midtape >opt_bin_char_Some
+ [ <hd_tech in ⊢(???%); // @daemon
+ | >right_midtape <tail_tech // @daemon ]
+ | whd in match (displ_of_move ? N); >iter_tape_move_L [|@daemon]
+ >Ht whd in match (step ???); <Htrans whd in match (ctape ???);
+ >tape_bin_lift_unfold >left_midtape >current_midtape >right_midtape
+ >opt_bin_char_Some lapply Hcrd >(?:FS_crd sig = |bin_char ? c|) [| @daemon ]
+ cases (bin_char ? c) // #H normalize in H; @False_ind
+ cases (not_le_Sn_O O) /2/
+ ]
+ ]
+
+
+