(midtape ? (left ? (nth obj ? t1 (niltape ?))) c (right ? (nth obj ? t1 (niltape ?)))) obj)
(mk_tape ? [ ] (option_hd ? (reverse ? (c::ls))) (tail ? (reverse ? (c::ls)))) cfg).
-axiom sem_cfg_to_obj : cfg_to_obj ⊨ R_cfg_to_obj.
-(*@(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
- (sem_seq ??????
- (sem_if ??????????
- (sem_test_null_multi ?? obj ?)
- (sem_seq ?????? (accRealize_to_Realize … (sem_copy_step …))
- (sem_move_multi ? 2 cfg L ?))
- (sem_inject ???? cfg ? (sem_write FSUnialpha null)))
- (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?))
- (sem_move_multi ? 2 cfg R ?)))) //
+lemma sem_cfg_to_obj : cfg_to_obj ⊨ R_cfg_to_obj.
+@(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
+ (sem_seq ??????
+ (sem_if ??????????
+ (acc_sem_inject ?????? cfg ? sem_test_null_char)
+ (sem_nop …)
+ (sem_seq ?????? (accRealize_to_Realize … (sem_copy_step …))
+ (sem_seq ?????? (sem_move_multi ? 2 cfg L ?) (sem_move_multi ? 2 obj L ?))))
+ (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?))
+ (sem_move_multi ? 2 cfg R ?)))) // [@sym_not_eq //]
#ta #tb *
#tc * whd in ⊢ (%→?); #Htc *
#td * *
-[ * #te * * #Hcurtc #Hte
- * destruct (Hte) #te * *
- [ whd in ⊢ (%→%→?); * #x * #y * * -Hcurtc #Hcurtc1 #Hcurtc2 #Hte #Htd
- * #tf * * * whd in ⊢ (%→%→%→%→?); #Htf1 #Htf2 #Htf3 #Htb
- #c #ls #Hta1 %
- [ #lso #x0 #rso #Hta2 >Hta1 in Htc; >eq_mk_tape_rightof
- whd in match (tape_move ???); #Htc
- cut (tf = change_vec ?? tc (mk_tape ? [ ] (None ?) (reverse ? ls@[x])) cfg)
- [@daemon] -Htf1 -Htf2 -Htf3 #Htf destruct (Htf Hte Htd Htc Htb)
- >change_vec_change_vec >change_vec_change_vec >change_vec_change_vec
- >nth_change_vec // >tape_move_mk_tape_R
- @daemon
- | #Hta2 >Htc in Hcurtc1; >nth_change_vec_neq [| @sym_not_eq //]
- >Hta2 #H destruct (H)
- ]
- | * #Hcurtc0 #Hte #_ #_ #c #ls #Hta1 >Hta1 in Htc; >eq_mk_tape_rightof
- whd in match (tape_move ???); #Htc >Htc in Hcurtc0; *
- [ >Htc in Hcurtc; >nth_change_vec_neq [|@sym_not_eq //]
- #Hcurtc #Hcurtc0 >Hcurtc0 in Hcurtc; * #H @False_ind @H %
- | >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H) ]
- ]
-| * #te * * #Hcurtc #Hte
- * whd in ⊢ (%→%→?); #Htd1 #Htd2
- * #tf * * * #Htf1 #Htf2 #Htf3 whd in ⊢ (%→?); #Htb
- #c #ls #Hta1 %
- [ #lso #x #rso #Hta2 >Htc in Hcurtc; >nth_change_vec_neq [|@sym_not_eq //]
- >Hta2 normalize in ⊢ (%→?); #H destruct (H)
- | #_ >Hta1 in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
- destruct (Hte) cut (td = change_vec ?? tc (midtape ? ls null []) cfg)
- [@daemon] -Htd1 -Htd2 #Htd
- -Htf1 cut (tf = change_vec ?? td (mk_tape ? [ ] (None ?) (reverse ? ls@[null])) cfg)
- [@daemon] -Htf2 -Htf3 #Htf destruct (Htf Htd Htc Htb)
+[ * #te * * * #Hcurtc #Hte1 #Hte2 whd in ⊢ (%→?); #Htd destruct (Htd)
+ * #tf * * * #Htf1 #Htf2 #Htf3
+ whd in ⊢ (%→?); #Htb
+ #c #ls #Hta %
+ [ #Hc >Hta in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
+ cut (te = tc) [@daemon] -Hte1 -Hte2 #Hte
+ cut (tf = change_vec ? 3 te (mk_tape ? [ ] (None ?) (reverse ? ls@[c])) cfg)
+ [@daemon] -Htf1 -Htf2 -Htf3 #Htf
+ destruct (Htf Hte Htc Htb)
>change_vec_change_vec >change_vec_change_vec >change_vec_change_vec
- >change_vec_change_vec >change_vec_change_vec >nth_change_vec //
- >reverse_cons >tape_move_mk_tape_R /2/ ]
-]
+ >nth_change_vec // >tape_move_mk_tape_R [| #_ % % ]
+ >reverse_cons %
+ | #Hc >Hta in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
+ >Htc in Hcurtc; >nth_change_vec // normalize in ⊢ (%→?);
+ #H destruct (H) @False_ind cases Hc /2/ ]
+| * #te * * * #Hcurtc #Hte1 #Hte2
+ * #tf * *
+ [ (* purtroppo copy_step assume che la destinazione sia Some (almeno come semantica) *)
+ STOP
+ * #x * #y * * #Hcurte_cfg #Hcurte_obj #Htf
+ * #tg * whd in ⊢ (%→%→?); #Htg #Htd
+ * #th * * * #Hth1 #Hth2 #Hth3
+ whd in ⊢ (%→%); #Htb
+ #c #ls #Hta % #Hc
+ [ >Hta in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
+ >Htc in Hcurtc; >nth_change_vec // normalize in ⊢ (%→?); >Hc
+ * #H @False_ind /2/
+ | >Hta in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
+ cut (te = tc) [@daemon] -Hte1 -Hte2 #Hte
qed.
*)
mmove i FSUnialpha 2 R.
definition unistep ≝
- obj_to_cfg · match_m cfg prg FSUnialpha 2 ·
+ match_m cfg prg FSUnialpha 2 ·
restart_tape cfg · copy prg cfg FSUnialpha 2 ·
- cfg_to_obj · tape_move_obj · restart_tape prg.
+ cfg_to_obj · tape_move_obj · restart_tape prg · obj_to_cfg.
(*
definition legal_tape ≝ λn,l,h,t.
].
definition R_unistep ≝ λn,l,h.λt1,t2: Vector ? 3.
- ∀state,oldc,table.
+ ∀state,char,table.
(* cfg *)
- nth cfg ? t1 (niltape ?) = midtape ? [ ] bar (state@[oldc]) →
- is_config n (bar::state@[oldc]) →
+ 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 char ≝ low_char' (current ? (nth obj ? t1 (niltape ?))) in
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 ∧
+ let new_obj ≝
+ tape_move_mono ? (nth obj ? t1 (niltape ?))
+ 〈Some ? nchar,char_to_move m〉 in
+ let next_char ≝ low_char' (current ? new_obj) in
t2 =
change_vec ??
- (change_vec ?? t1 (midtape ? [ ] bar (nstate@[nchar])) cfg)
- (tape_move_mono ? (nth obj ? t1 (niltape ?)) 〈Some ? nchar,char_to_move m〉) obj.
+ (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)).
-definition low ≝ λM:normalTM.λc:nconfig (no_states M).Vector_of_list ?
+definition low_tapes ≝ λM:normalTM.λc:nconfig (no_states M).Vector_of_list ?
[tape_map ?? bit (ctape ?? c);
midtape ? [ ] bar (bits_of_state ? (nhalt M) (cstate ?? c));
- ?].
+ midtape ? [ ] bar (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M))
+ ].
+
+definition R_unistep_high ≝ λM:normalTM.λc:nconfig (no_states M).λt1,t2.
+ t1 = low_tapes M c →
+ t2 = low_tapes M (step ? M c).
-
- .
\ No newline at end of file
+
\ No newline at end of file