+
+definition low_tape_aux : ∀M:normalTM.tape FinBool → tape STape ≝
+λM:normalTM.λt.
+ let current_low ≝ match current … t with
+ [ None ⇒ None ? | Some b ⇒ Some ? 〈bit b,false〉] in
+ let low_left ≝ map … (λb.〈bit b,false〉) (left … t) in
+ let low_right ≝ map … (λb.〈bit b,false〉) (right … t) in
+ mk_tape STape low_left current_low low_right.
+
+lemma left_of_low_tape: ∀M,t.
+ left ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (left … t).
+#M * //
+qed.
+
+lemma right_of_low_tape: ∀M,t.
+ right ? (low_tape_aux M t) = map … (λb.〈bit b,false〉) (right … t).
+#M * //
+qed.
+
+definition low_move ≝ λaction:option (bool × move).
+ match action with
+ [None ⇒ None ?
+ |Some act ⇒ Some ? (〈〈bit (\fst act),false〉,\snd act〉)].
+
+(* simulation lemma *)
+lemma low_tape_move : ∀M,action,t.
+ tape_move STape (low_tape_aux M t) (low_move action) =
+ low_tape_aux M (tape_move FinBool t action).
+#M * // (* None *)
+* #b #mv #t cases mv cases t //
+ [#ls #c #rs cases ls //|#ls #c #rs cases rs //]
+qed.
+
+lemma left_of_lift: ∀ls,c,rs. left ? (lift_tape ls c rs) = ls.
+#ls * #c #b #rs cases c // cases ls // cases rs //
+qed.
+
+lemma right_of_lift: ∀ls,c,rs. legal_tape ls c rs →
+ right ? (lift_tape ls c rs) = rs.
+#ls * #c #b #rs * #_ cases c // cases ls cases rs // #a #tll #b #tlr
+#H @False_ind cases H [* [#H1 /2/ |#H1 destruct] |#H1 destruct]
+qed.
+
+
+lemma current_of_lift: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
+ current STape (lift_tape ls 〈c,b〉 rs) =
+ match c with [null ⇒ None ? | _ ⇒ Some ? 〈c,b〉].
+#ls #c #b #rs cases c // whd in ⊢ (%→?); * #_
+* [* [#Hnull @False_ind /2/ | #Hls >Hls whd in ⊢ (??%%); cases rs //]
+ |#Hrs >Hrs whd in ⊢ (??%%); cases ls //]
+qed.
+
+lemma current_of_lift_None: ∀ls,c,b,rs. legal_tape ls 〈c,b〉 rs →
+ current STape (lift_tape ls 〈c,b〉 rs) = None ? →
+ c = null.
+#ls #c #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize
+ [#b #H destruct |// |3,4,5:#H destruct ]
+qed.
+
+lemma current_of_lift_Some: ∀ls,c,c1,rs. legal_tape ls c rs →
+ current STape (lift_tape ls c rs) = Some ? c1 →
+ c = c1.
+#ls * #c #cb #b #rs #Hlegal >(current_of_lift … Hlegal) cases c normalize
+ [#b1 #H destruct // |#H destruct |3,4,5:#H destruct //]
+qed.
+
+lemma current_of_low_None: ∀M,t. current FinBool t = None ? →
+ current STape (low_tape_aux M t) = None ?.
+#M #t cases t // #l #b #r whd in ⊢ ((??%?)→?); #H destruct
+qed.
+
+lemma current_of_low_Some: ∀M,t,b. current FinBool t = Some ? b →
+ current STape (low_tape_aux M t) = Some ? 〈bit b,false〉.
+#M #t cases t
+ [#b whd in ⊢ ((??%?)→?); #H destruct
+ |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
+ |#b #l #b1 whd in ⊢ ((??%?)→?); #H destruct
+ |#c #c1 #l #r whd in ⊢ ((??%?)→?); #H destruct %
+ ]
+qed.
+
+lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
+ lift_tape ls c rs = low_tape_aux M tape →
+ c = 〈match current … tape with
+ [ None ⇒ null | Some b ⇒ bit b], false〉.
+#M #tape #ls * #c #cb #rs #Hlegal #Hlift
+cut (current ? (lift_tape ls 〈c,cb〉 rs) = current ? (low_tape_aux M tape))
+ [@eq_f @Hlift] -Hlift #Hlift
+cut (current … tape = None ? ∨ ∃b.current … tape = Some ? b)
+ [cases (current … tape) [%1 // | #b1 %2 /2/ ]] *
+ [#Hcurrent >Hcurrent normalize
+ >(current_of_low_None …Hcurrent) in Hlift; #Hlift
+ >(current_of_lift_None … Hlegal Hlift)
+ @eq_f cases Hlegal * * #Hmarks #_ #_ #_ @(Hmarks 〈c,cb〉) @memb_hd
+ |* #b #Hcurrent >Hcurrent normalize
+ >(current_of_low_Some …Hcurrent) in Hlift; #Hlift
+ @(current_of_lift_Some … Hlegal Hlift)
+ ]
+qed.
+
+(*
+lemma current_of_low:∀M,tape,ls,c,rs. legal_tape ls c rs →
+ lift_tape ls c rs = low_tape_aux M tape →
+ c = 〈match current … tape with
+ [ None ⇒ null | Some b ⇒ bit b], false〉.
+#M #tape #ls * #c #cb #rs * * #_ #H cases (orb_true_l … H)
+ [cases c [2,3,4,5: whd in ⊢ ((??%?)→?); #Hfalse destruct]
+ #b #_ #_ cases tape
+ [whd in ⊢ ((??%%)→?); #H destruct
+ |#a #l whd in ⊢ ((??%%)→?); #H destruct
+ |#a #l whd in ⊢ ((??%%)→?); #H destruct
+ |#a #l #r whd in ⊢ ((??%%)→?); #H destruct //
+ ]
+ |cases c
+ [#b whd in ⊢ ((??%?)→?); #Hfalse destruct
+ |3,4,5:whd in ⊢ ((??%?)→?); #Hfalse destruct]
+ #_ * [* [#Habs @False_ind /2/
+ |#Hls >Hls whd in ⊢ ((??%%)→?); *)
+