+ match_m cfg prg FSUnialpha 2 ·
+ restart_tape cfg · copy prg cfg FSUnialpha 2 ·
+ cfg_to_obj · tape_move_obj · restart_tape prg · obj_to_cfg.
+
+(*
+definition legal_tape ≝ λn,l,h,t.
+ ∃state,char,table.
+ nth cfg ? t1 (niltape ?) = midtape ? [ ] bar (state@[char]) →
+ is_config n (bar::state@[char]) →
+ nth prg ? t1 (niltape ?) = midtape ? [ ] bar table →
+ bar::table = table_TM n l h → *)
+
+definition list_of_tape ≝ λsig,t.
+ left sig t@option_cons ? (current ? t) (right ? t).
+
+definition low_char' ≝ λc.
+ match c with
+ [ None ⇒ null
+ | Some b ⇒ if (is_bit b) then b else null
+ ].
+
+lemma low_char_option : ∀s.
+ low_char' (option_map FinBool FSUnialpha bit s) = low_char s.
+* //
+qed.
+
+definition R_unistep ≝ λn,l,h.λt1,t2: Vector ? 3.
+ ∀state,char,table.
+ (* cfg *)
+ nth cfg ? t1 (niltape ?) = midtape ? [ ] bar (state@[char]) →
+ is_config n (bar::state@[char]) →
+ (* prg *)
+ nth prg ? t1 (niltape ?) = midtape ? [ ] bar table →
+ bar::table = table_TM n l h →
+ (* obj *)
+ only_bits (list_of_tape ? (nth obj ? t1 (niltape ?))) →
+ let conf ≝ (bar::state@[char]) in
+ (∃ll,lr.bar::table = ll@conf@lr) →
+(*
+ ∃nstate,nchar,m,t. tuple_encoding n h t = (conf@nstate@[nchar;m]) ∧
+ mem ? t l ∧ *)
+ ∀nstate,nchar,m,t.
+ tuple_encoding n h t = (conf@nstate@[nchar;m])→
+ mem ? t l →
+ let new_obj ≝
+ tape_move_mono ? (nth obj ? t1 (niltape ?))
+ 〈char_to_bit_option nchar,char_to_move m〉 in
+ let next_char ≝ low_char' (current ? new_obj) in
+ t2 =
+ change_vec ??
+ (change_vec ?? t1 (midtape ? [ ] bar (nstate@[next_char])) cfg)
+ new_obj obj.
+
+definition tape_map ≝ λA,B:FinSet.λf:A→B.λt.
+ mk_tape B (map ?? f (left ? t))
+ (option_map ?? f (current ? t))
+ (map ?? f (right ? t)).
+
+lemma map_list_of_tape: ∀A,B,f,t.
+ list_of_tape B (tape_map ?? f t) = map ?? f (list_of_tape A t).
+#A #B #f * // normalize // #ls #c #rs <map_append %
+qed.
+
+lemma low_char_current : ∀t.
+ low_char' (current FSUnialpha (tape_map FinBool FSUnialpha bit t))
+ = low_char (current FinBool t).
+* // qed.
+
+definition low_tapes: ∀M:normalTM.∀c:nconfig (no_states M).Vector ? 3 ≝
+λM:normalTM.λc:nconfig (no_states M).Vector_of_list ?
+ [tape_map ?? bit (ctape ?? c);
+ midtape ? [ ] bar
+ ((bits_of_state ? (nhalt M) (cstate ?? c))@[low_char (current ? (ctape ?? c))]);
+ midtape ? [ ] bar (tail ? (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M)))
+ ].
+
+lemma obj_low_tapes: ∀M,c.
+ nth obj ? (low_tapes M c) (niltape ?) = tape_map ?? bit (ctape ?? c).
+// qed.
+
+lemma cfg_low_tapes: ∀M,c.
+ nth cfg ? (low_tapes M c) (niltape ?) =
+ midtape ? [ ] bar
+ ((bits_of_state ? (nhalt M) (cstate ?? c))@[low_char (current ? (ctape ?? c))]).
+// qed.
+
+lemma prg_low_tapes: ∀M,c.
+ nth prg ? (low_tapes M c) (niltape ?) =
+ midtape ? [ ] bar (tail ? (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M))).
+// qed.
+
+(* commutation lemma for write *)
+lemma map_write: ∀t,cout.
+ tape_write ? (tape_map FinBool ? bit t) (char_to_bit_option (low_char cout))
+ = tape_map ?? bit (tape_write ? t cout).
+#t * // #b whd in match (char_to_bit_option ?);
+whd in ⊢ (??%%); @eq_f3 [elim t // | // | elim t //]
+qed.
+
+(* commutation lemma for moves *)
+lemma map_move: ∀t,m.
+ tape_move ? (tape_map FinBool ? bit t) (char_to_move (low_mv m))
+ = tape_map ?? bit (tape_move ? t m).
+#t * // whd in match (char_to_move ?);
+ [cases t // * // | cases t // #ls #a * //]
+qed.
+
+(* commutation lemma for actions *)
+lemma map_action: ∀t,cout,m.
+ tape_move ? (tape_write ? (tape_map FinBool ? bit t)
+ (char_to_bit_option (low_char cout))) (char_to_move (low_mv m))
+ = tape_map ?? bit (tape_move ? (tape_write ? t cout) m).
+#t #cout #m >map_write >map_move %
+qed.
+
+lemma map_move_mono: ∀t,cout,m.
+ tape_move_mono ? (tape_map FinBool ? bit t)
+ 〈char_to_bit_option (low_char cout), char_to_move (low_mv m)〉
+ = tape_map ?? bit (tape_move_mono ? t 〈cout,m〉).
+@map_action
+qed.
+
+definition R_unistep_high ≝ λM:normalTM.λt1,t2.
+∀c:nconfig (no_states M).
+ t1 = low_tapes M c →
+ t2 = low_tapes M (step ? M c).
+
+lemma R_unistep_equiv : ∀M,t1,t2.
+ R_unistep (no_states M) (graph_enum ?? (ntrans M)) (nhalt M) t1 t2 →
+ R_unistep_high M t1 t2.
+#M #t1 #t2 #H whd whd in match (nconfig ?); #c #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 @(eq_vec ? 3 ?? (niltape ?) ?) >Ht2 #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.