+lemma R_unistep_equiv : ∀M,c,t1,t2.
+ R_unistep (no_states M) (graph_enum ?? (ntrans M)) (nhalt M) t1 t2 →
+ R_unistep_high M c t1 t2.
+#M #c #t1 #t2 #H #Ht1
+lapply (initial_bar ? (nhalt M) (graph_enum ?? (ntrans M)) (nTM_nog ?)) #Htable
+(* tup = current tuple *)
+cut (∃t.t = 〈〈cstate … c,current ? (ctape … c)〉,
+ ntrans M 〈cstate … c,current ? (ctape … c)〉〉) [% //] * #tup #Htup
+(* tup is in the graph *)
+cut (mem ? tup (graph_enum ?? (ntrans M)))
+ [@memb_to_mem >Htup @(graph_enum_complete … (ntrans M)) %] #Hingraph
+(* tupe target = 〈qout,cout,m〉 *)
+lapply (decomp_target ? (ntrans M 〈cstate … c,current ? (ctape … c)〉))
+* #qout * #cout * #m #Htg >Htg in Htup; #Htup
+(* new config *)
+cut (step FinBool M c = mk_config ?? qout (tape_move ? (tape_write ? (ctape … c) cout) m))
+ [>(config_expand … c) whd in ⊢ (??%?); (* >Htg ?? why not?? *)
+ cut (trans ? M 〈cstate … c, current ? (ctape … c)〉 = 〈qout,cout,m〉) [<Htg %] #Heq1
+ >Heq1 %] #Hstep
+(* new state *)
+cut (cstate ?? (step FinBool M c) = qout) [>Hstep %] #Hnew_state
+(* new tape *)
+cut (ctape ?? (step FinBool M c) = tape_move ? (tape_write ? (ctape … c) cout) m)
+ [>Hstep %] #Hnew_tape
+lapply(H (bits_of_state ? (nhalt M) (cstate ?? c))
+ (low_char (current ? (ctape ?? c)))
+ (tail ? (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M)))
+ ??????)
+[<Htable
+ lapply(list_to_table … (nhalt M) …Hingraph) * #ll * #lr #Htable1 %{ll}
+ %{(((bits_of_state ? (nhalt M) qout)@[low_char cout;low_mv m])@lr)}
+ >Htable1 @eq_f <associative_append @eq_f2 // >Htup
+ whd in ⊢ (??%?); @eq_f >associative_append %
+|>Ht1 >obj_low_tapes >map_list_of_tape elim (list_of_tape ??)
+ [#b @False_ind | #b #tl #Hind #a * [#Ha >Ha //| @Hind]]
+|@sym_eq @Htable
+|>Ht1 %
+|%{(bits_of_state ? (nhalt M) (cstate ?? c))} %{(low_char (current ? (ctape ?? c)))}
+ % [% [% [// | cases (current ??) normalize [|#b] % #Hd destruct (Hd)]
+ |>length_map whd in match (length ??); @eq_f //]
+ |//]
+|>Ht1 >cfg_low_tapes //] -H #H
+lapply(H (bits_of_state … (nhalt M) qout) (low_char … cout)
+ (low_mv … m) tup ? Hingraph)
+ [>Htup whd in ⊢ (??%?); @eq_f >associative_append %] -H
+#Ht2 >Ht2 @(eq_vec ? 3 … (niltape ?)) #i #Hi
+cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+ [cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+ [cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi
+ [@False_ind /2/
+ |>Hi >obj_low_tapes >nth_change_vec //
+ >Ht1 >obj_low_tapes >Hstep @map_action
+ ]
+ |>Hi >cfg_low_tapes >nth_change_vec_neq
+ [|% whd in ⊢ (??%?→?); #H destruct (H)]
+ >nth_change_vec // >Hnew_state @eq_f @eq_f >Hnew_tape
+ @eq_f2 [|2:%] >Ht1 >obj_low_tapes >map_move_mono >low_char_current %
+ ]
+ |(* program tapes do not change *)
+ >Hi >prg_low_tapes
+ >nth_change_vec_neq [|% whd in ⊢ (??%?→?); #H destruct (H)]
+ >nth_change_vec_neq [|% whd in ⊢ (??%?→?); #H destruct (H)]
+ >Ht1 >prg_low_tapes //
+ ]
+qed.
+
+
+
+
\ No newline at end of file