-(* 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.