*)
definition init_match ≝
- seq ? (mark ?)
- (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c)))
- (seq ? (move_r ?)
- (seq ? (move_r ?)
- (seq ? (mark ?)
- (seq ? (move_l ?)
- (adv_to_mark_l ? (is_marked ?))))))).
+ mark ? · adv_to_mark_r ? (λc:STape.is_grid (\fst c)) · move_r ? ·
+ move_r ? · mark ? · move_l ? · adv_to_mark_l ? (is_marked ?).
definition R_init_match ≝ λt1,t2.
∀ls,l,rs,c,d. no_grids (〈c,false〉::l) → no_marks l →
>associative_append %
qed.
-
(* init_copy
init_current_on_match; (* no marks in current *)
*)
definition init_copy ≝
- seq ? init_current_on_match
- (seq ? (move_r ?)
- (seq ? (adv_to_mark_r ? (is_marked ?))
- (adv_mark_r ?))).
+ init_current_on_match · move_r ? ·
+ adv_to_mark_r ? (is_marked ?) · adv_mark_r ?.
definition R_init_copy ≝ λt1,t2.
∀l1,l2,c,ls,d,rs.
]
qed. *)
-definition exec_move ≝
- seq ? init_copy
- (seq ? copy
- (seq ? (move_r …) move_tape)).
+definition exec_action ≝
+ init_copy · copy · move_r … · move_tape.
definition map_move ≝
λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
mv ≠ null → c1 ≠ null
dal fatto che c1 e mv sono contenuti nella table
*)
-definition R_exec_move ≝ λt1,t2.
+definition R_exec_action ≝ λt1,t2.
∀n,curconfig,ls,rs,c0,c1,s0,s1,table1,newconfig,mv,table2.
table_TM n (table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2) →
no_marks curconfig → only_bits (curconfig@[〈s0,false〉]) →
*)
-lemma sem_exec_move : Realize ? exec_move R_exec_move.
+lemma sem_exec_action : Realize ? exec_action R_exec_action.
#intape
cases (sem_seq … sem_init_copy
(sem_seq … sem_copy
match_tuple;
if is_marked(current) = false (* match ok *)
then
- exec_move
+ exec_action
move_r;
else sink;
else nop;
definition uni_step ≝
ifTM ? (test_char STape (λc.\fst c == bit false))
- (single_finalTM ? (seq ? init_match
- (seq ? match_tuple
+ (single_finalTM ?
+ (init_match · match_tuple ·
(ifTM ? (test_char ? (λc.¬is_marked ? c))
- (seq ? exec_move (move_r …))
- (nop ?) (* sink *)
- tc_true))))
- (nop ?)
- tc_true.
+ (exec_action · move_r …)
+ (nop ?) tc_true)))
+ (nop ?) tc_true.
definition R_uni_step_true ≝ λt1,t2.
∀n,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
axiom sem_match_tuple : Realize ? match_tuple R_match_tuple.
+definition us_acc : states ? uni_step ≝ (inr … (inl … (inr … start_nop))).
+
lemma sem_uni_step :
- accRealize ? uni_step (inr … (inl … (inr … start_nop)))
+ accRealize ? uni_step us_acc
R_uni_step_true R_uni_step_false.
@(acc_sem_if_app STape … (sem_test_char ? (λc:STape.\fst c == bit false))
(sem_seq … sem_init_match
(sem_seq … sem_match_tuple
(sem_if … (* ????????? (sem_test_char … (λc.¬is_marked FSUnialpha c)) *)
- (sem_seq … sem_exec_move (sem_move_r …))
+ (sem_seq … sem_exec_action (sem_move_r …))
(sem_nop …))))
(sem_nop …)
…)