progress in termination of marks.ma

[helm.git] / matita / matita / lib / turing / universal / uni_step.ma

diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index 395decac2b3b1fa1b6cc7ee4588993732e35d606..fc663ff2c92114aa363c1a57738b2b1696087769 100644 (file)
--- a/matita/matita/lib/turing/universal/uni_step.ma
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -57,13 +57,8 @@ if is_true(current) (* current state is final *)
 *)
 
 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 → 
@@ -100,7 +95,6 @@ whd in ⊢ (%→?); #Htg cases (Htg … Htf) -Htg -Htf
    >associative_append %
 qed.
 
-
 (* init_copy 
 
            init_current_on_match; (* no marks in current *)
@@ -111,10 +105,8 @@ qed.
 *)
 
 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. 
@@ -240,10 +232,8 @@ cases HR -HR
   ]
 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〉 ].
@@ -255,7 +245,7 @@ definition map_move ≝
        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〉]) → 
@@ -329,7 +319,7 @@ qed.
 
 *)
 
-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
@@ -451,7 +441,7 @@ if is_false(current) (* current state is not final *)
     match_tuple;
     if is_marked(current) = false (* match ok *)
       then 
-           exec_move
+           exec_action
            move_r;
       else sink;
    else nop;
@@ -459,14 +449,12 @@ if is_false(current) (* current state is not final *)
 
 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.
@@ -489,14 +477,16 @@ definition R_uni_step_false ≝ λt1,t2.
   
 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 …)
    …)