+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 ⊢ ((??%%)→?); *)
+
+
+(* sufficent conditions to have a low_level_config *)
+lemma is_low_config: ∀ls,c,rs,M,s,tape,qhd,q_tl,table.
+legal_tape ls c rs →
+table = flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
+lift_tape ls c rs = low_tape_aux M tape →
+〈qhd,false〉::q_tl = m_bits_of_state (no_states M) (nhalt M) s →
+midtape STape (〈grid,false〉::ls)
+ 〈qhd,false〉
+ (q_tl@c::〈grid,false〉::table@〈grid,false〉::rs) =
+ low_config M (mk_config ?? s tape).
+#ls #c #rs #M #s #tape #qhd #q_tl #table #Hlegal #Htable
+#Hlift #Hstate whd in match (low_config ??); <Hstate
+@eq_f3
+ [@eq_f <(left_of_lift ls c rs) >Hlift //
+ | cut (∀A.∀a,b:A.∀l1,l2. a::l1 = b::l2 → a=b)
+ [#A #a #b #l1 #l2 #H destruct (H) %] #Hcut
+ @(Hcut …Hstate)
+ |@eq_f <(current_of_low … Hlegal Hlift) @eq_f @eq_f <Htable @eq_f @eq_f
+ <(right_of_lift ls c rs Hlegal) >Hlift @right_of_low_tape
+ ]
+qed.
+
+lemma unistep_true_to_low_step: ∀t1,t2.
+ R_uni_step_true t1 t2 → low_step_R_true t1 t2.
+#t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
+cases (low_config_eq … eqt1)
+#low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
+***** #Hlow_left #Hlow_right #Htable #Hq_low #Hcurrent_low #Ht1
+letin trg ≝ (t 〈qin,current ? tape〉)
+letin qout_low ≝ (m_bits_of_state n h (\fst trg))
+letin qout_low_hd ≝ (hd ? qout_low 〈bit true,false〉)
+letin qout_low_tl ≝ (tail ? qout_low)
+letin low_act ≝ (low_action (\snd (t 〈qin,current ? tape〉)))
+letin low_cout ≝ (\fst low_act)
+letin low_m ≝ (\snd low_act)
+lapply (Huni_step n table q_low_hd (\fst qout_low_hd)
+ current_low low_cout low_left low_right q_low_tl qout_low_tl low_m … Ht1)
+ [@daemon
+ |>Htable
+ @(trans_to_match n h t 〈qin,current ? tape〉 … (refl …))
+ >Hq_low >Hcurrent_low whd in match (mk_tuple ?????);
+ >(eq_pair_fst_snd … (t …)) whd in ⊢ (??%?);
+ >(eq_pair_fst_snd … (low_action …)) %
+ |//
+ |@daemon
+ ]
+-Ht1 #Huni_step lapply (Huni_step ? (refl …)) -Huni_step *
+#q_low_head_false * #ls1 * #rs1 * #c2 * *
+#Ht2 #Hlift #Hlegal %
+ [whd in ⊢ (??%?); >q_low_head_false in Hq_low;
+ whd in ⊢ ((???%)→?); generalize in match (h qin);
+ #x #H destruct (H) %
+ |>Ht2 whd in match (step FinBool ??);
+ whd in match (trans ???);
+ >(eq_pair_fst_snd … (t ?))
+ @is_low_config // >Hlift
+ <low_tape_move @eq_f2
+ [>Hlow_left >Hlow_right >Hcurrent_low whd in ⊢ (??%%);
+ cases (current …tape) [%] #b whd in ⊢ (??%%); %
+ |whd in match low_cout; whd in match low_m; whd in match low_act;
+ generalize in match (\snd (t ?)); * [%] * #b #mv
+ whd in ⊢ (??(?(???%)?)%); cases mv %
+ ]
+ ]
+qed.
+
+definition low_step_R_false ≝ λt1,t2.
+ ∀M:normalTM.
+ ∀c: nconfig (no_states M).
+ t1 = low_config M c → halt ? M (cstate … c) = true ∧ t1 = t2.
+
+lemma unistep_false_to_low_step: ∀t1,t2.
+ R_uni_step_false t1 t2 → low_step_R_false t1 t2.
+#t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
+cases (low_config_eq … eqt1) #low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
+***** #_ #_ #_ #Hqin #_ #Ht1 whd in match (halt ???);
+cases (Huni_step (h qin) ?) [/2/] >Ht1 whd in ⊢ (??%?); @eq_f
+normalize in Hqin; destruct (Hqin) %
+qed.
+
+definition low_R ≝ λM,qstart,R,t1,t2.
+ ∀tape1. t1 = low_config M (mk_config ?? qstart tape1) →
+ ∃q,tape2.R tape1 tape2 ∧
+ halt ? M q = true ∧ t2 = low_config M (mk_config ?? q tape2).
+
+lemma sem_uni_step1:
+ uni_step ⊨ [us_acc: low_step_R_true, low_step_R_false].
+@daemon (* this no longer works: TODO *) (*
+@(acc_Realize_to_acc_Realize … sem_uni_step)
+ [@unistep_true_to_low_step | @unistep_false_to_low_step ]