From 0716716134a7820a822561cd6c55d5e71412acfd Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 15 Jun 2012 11:02:45 +0000
Subject: [PATCH] middot notation

---
 matita/matita/lib/turing/basic_machines.ma    |  16 +-
 matita/matita/lib/turing/char_move.ma         | 208 ------------------
 matita/matita/lib/turing/mono.ma              |   2 +-
 matita/matita/lib/turing/move_char.ma         |  26 +--
 matita/matita/lib/turing/universal/marks.ma   |  20 +-
 .../lib/turing/universal/match_machines.ma    |  18 +-
 .../matita/lib/turing/universal/move_tape.ma  |  70 +++---
 .../matita/lib/turing/universal/uni_step.ma   |  32 +--
 8 files changed, 73 insertions(+), 319 deletions(-)
 delete mode 100644 matita/matita/lib/turing/char_move.ma

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index eed6ad1f6..56a0bf4b1 100644
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -194,7 +194,7 @@ definition swap1 : initN 4 ≝ mk_Sig ?? 1 (leb_true_to_le 2 4 (refl …)).
 definition swap2 : initN 4 ≝ mk_Sig ?? 2 (leb_true_to_le 3 4 (refl …)).
 definition swap3 : initN 4 ≝ mk_Sig ?? 3 (leb_true_to_le 4 4 (refl …)).
 
-definition swap ≝ 
+definition swap_r ≝ 
  λalpha:FinSet.λfoo:alpha.
  mk_TM alpha (swap_states alpha)
  (λp.let 〈q,a〉 ≝ p in
@@ -222,8 +222,8 @@ definition Rswap ≝
     t1 = midtape alpha ls b (a::rs) → 
     t2 = midtape alpha ls a (b::rs).
 
-lemma sem_swap : ∀alpha,foo.
-  swap alpha foo ⊨ Rswap alpha. 
+lemma sem_swap_r : ∀alpha,foo.
+  swap_r alpha foo ⊨ Rswap alpha. 
 #alpha #foo *
   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
    % [% |#a #b #ls #rs #H destruct]
@@ -238,12 +238,12 @@ lemma sem_swap : ∀alpha,foo.
   ]
 qed.
 
-definition swap_r ≝ 
+definition swap_l ≝ 
  λalpha:FinSet.λfoo:alpha.
  mk_TM alpha (swap_states alpha)
  (λp.let 〈q,a〉 ≝ p in
   let 〈q',b〉 ≝ q in
-  let q' ≝ pi1 nat (λi.i<4) q' in (* perche' devo passare il predicato ??? *)
+  let q' ≝ pi1 nat (λi.i<4) q' in
   match a with 
   [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
   | Some a' ⇒ 
@@ -260,14 +260,14 @@ definition swap_r ≝
   〈swap0,foo〉
   (λq.\fst q == swap3).
 
-definition Rswap_r ≝ 
+definition Rswap_l ≝ 
   λalpha,t1,t2.
    ∀a,b,ls,rs.  
     t1 = midtape alpha (a::ls) b rs → 
     t2 = midtape alpha (b::ls) a rs.
 
-lemma sem_swap_r : ∀alpha,foo.
-  swap_r alpha foo ⊨ Rswap_r alpha. 
+lemma sem_swap_l : ∀alpha,foo.
+  swap_l alpha foo ⊨ Rswap_l alpha. 
 #alpha #foo *
   [@(ex_intro ?? 2) @(ex_intro … (mk_config ?? 〈swap3,foo〉 (niltape ?)))
    % [% |#a #b #ls #rs #H destruct]
diff --git a/matita/matita/lib/turing/char_move.ma b/matita/matita/lib/turing/char_move.ma
deleted file mode 100644
index 66d92830a..000000000
--- a/matita/matita/lib/turing/char_move.ma
+++ /dev/null
@@ -1,208 +0,0 @@
-include "turing/turing.ma".
-
-(* 
-Simboli:
-0 1 *0 *1 # | ,
-
-[lista di simboli] fa match su un simbolo qualunque nella lista
-ad esempio [#|,] fa match con la gratella "#", la barra verticale "|" e la virgola ","
-
-Convenzione variabili:
-- x,y,z,D     = bit (non marcati)
-- *x,*y,*z,*D = bit marcati
-- c,d,e = caratteri (bit marcati e non marcati e separatori)
-
-Convenzioni mosse:
-c/D --> Q : leggo c, scrivo c, mi sposto a D e passo allo stato Q
-c/d/D --> Q : leggo c, scrivo d, mi sposto a D e passo allo stato Q
-
-*)
-
-inductive alpha_uni : Type[0] ≝ 
-| bit : bool → alpha_uni
-| mark : bool → alpha_uni
-| grid : alpha_uni | bar : alpha_uni | comma : alpha_uni.
-
-inductive Qmatch : Type[0] ≝
-| qm0 : Qmatch | qm1 : Qmatch | qm2 : bool → Qmatch | qm3 : bool → Qmatch
-| qm4 : Qmatch | qm5 : Qmatch | qm6 : Qmatch | qm7 : Qmatch 
-| qm8 : Qmatch | qm9 : Qmatch 
-| qmsuccess : Qmatch | qmfailure : Qmatch | qmsink : Qmatch.
-
-definition bool_eqb ≝ λb1,b2:bool.¬ (xorb b1 b2).
-
-(*
-==================================
-MACCHINE PER SPOSTARE LA "TESTINA"
-================================
-
-Lo spostamento a sx si ottiene mediante
-
-ls x # current y # macchina # rs
-----C--->
-ls x # current # y macchina # rs
-----B--->
-ls x # current # macchina # y rs
-----B--->
-ls # x current # macchina # y rs
-----C--->
-ls # current x # macchina # y rs
-
-
-Lo spostamento a dx si ottiene mediante
-
-ls # current x # macchina # y rs
-----A--->
-ls x # current # macchina # y rs
-----A--->
-ls x # current # macchina y # rs
-----A--->
-ls x # current y # macchina # rs
-
-
-MACCHINA A
-----------
-Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua sinistra.
-
-Input:
-  
-  ls # cs x rs
-          ^
-          0
-
-Output:
-  ls x # cs rs
-     ^
-     4
-
-STATO 0:
-  \forall x.x/L --> 1(x)
-
-STATO 1(x):
-  \forall c != #. c/x/R --> 2(c)
-  #/x/R --> 3
-
-STATO 2(c):
-  \forall d. d/c/L --> 0
-
-STATO 3:
-  \forall c. c/#/L --> 4
-
-STATO 4:
-  stato finale
-*)
-
-(* struttura generica della semantica *) 
-lemma move_char_sem: ∀inc. prec inc → ∃i. ∃outc. loop i step inc = Some outc 
-∧ postc outc inc. 
-
-lemma sequential : ∀M1,M2. 
-
-definition pre c ≝ 
-  let s ≝ state c in
-  let tp ≝ tape c in
-  let left ≝ 
-  
-definition post c1 c2 ≝
-  let s1 ≝ state c1 in
-  let tp1 ≝ tape c1 in
-  let leftt ≝ left tp1 in
-  let rightt ≝ right tp1 in
-  c2 = mk_config finals 
-  
-
-
-match s with
- [ q0 ⇒ match c with
-   [ bit x ⇒ 〈q1 x,〈c,L〉〉
-   | _ ⇒ 〈qsink,〈c,N〉〉 ]
- | q1 x ⇒ match c with
-   [ grid ⇒ 〈q3,〈bit x,R〉〉
-   | _ ⇒ 〈q2 c,〈bit x,R〉〉 ]
- | q2 d ⇒ 〈q0,〈d,L〉〉
- | q3 ⇒ 〈q4,〈grid,L〉〉
- | q4 ⇒ (* finale *) ].
-
-(*
-MACCHINA B
-----------
-Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua destra.
-
-Input:
-
-  ls x cs # rs
-     ^
-     0
-
-Output:
-  ls cs # x rs
-          ^
-          4
-
-STATO 0:
-  \forall x.x/R --> 1(x)
-
-STATO 1(x):
-  \forall c != #. c/x/L --> 2(c)
-  #/x/L --> 3
-
-STATO 2(c):
-  \forall d. d/c/R --> 0
-
-STATO 3:
-  \forall c. c/#/L --> 4
-
-STATO 4:
-  stato finale
-*)
-
-match s with
-[ q0 ⇒ match c with
-  [ bit x ⇒ 〈q1 x,〈c,R〉〉
-  | _ ⇒ 〈qsink,〈c,N〉〉]
-| q1 x ⇒ match c with
-  [ grid ⇒ 〈q3,〈bit x,L〉〉
-  | _ ⇒ 〈q2 c,〈bit x,L〉〉 ]
-| q2 d ⇒ 〈q0,〈d,R〉〉
-| q3 ⇒ 〈q4,〈grid,L〉〉 
-| q4 ⇒ (* finale *) ].
-
-(*
-MACCHINA C
-----------
-Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
-
-Input:
-  ls x cs # rs
-     ^
-     0
-
-Output:
-  ls cs x # rs
-        ^
-        3
-
-STATO 0:
-  \forall x. x/R --> 1(x)
-
-STATO 1(x):
-  \forall c != #. c/x/L --> 2(c)
-  #/#/L --> 3
-
-STATO 2(c):
-  \forall d. d/c/R --> 0
-
-STATO 3:
-  stato finale
-
-*)
-
-match s with 
-[ q0 ⇒ match c with
-  [ bit x ⇒ 〈q1 x,〈c,R〉〉
-  | _ ⇒ 〈qsink,〈c,N〉〉 ]
-| q1 x ⇒ match c with
-  [ grid ⇒ 〈q3,〈grid,L〉〉
-  | _ ⇒ 〈q2 c,〈bit x,L〉〉
-| q2 d ⇒ 〈q0,〈c,R〉〉
-| q3 ⇒ (* finale *) ].
diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 8ac107226..e117fc7be 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -342,7 +342,7 @@ definition seq ≝ λsig. λM1,M2 : TM sig.
     (λs.match s with 
       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]). 
 
-notation "a · b" non associative with precedence 65 for @{ 'middot $a $b}.
+notation "a · b" right associative with precedence 65 for @{ 'middot $a $b}.
 interpretation "sequential composition" 'middot a b = (seq ? a b).
 
 definition lift_confL ≝ 
diff --git a/matita/matita/lib/turing/move_char.ma b/matita/matita/lib/turing/move_char.ma
index aae21e7a9..a0bf18996 100644
--- a/matita/matita/lib/turing/move_char.ma
+++ b/matita/matita/lib/turing/move_char.ma
@@ -30,29 +30,29 @@ Final state = 〈4,#〉
 include "turing/basic_machines.ma".
 include "turing/if_machine.ma".
 
-definition mcc_step ≝ λalpha:FinSet.λsep:alpha.
+definition mcr_step ≝ λalpha:FinSet.λsep:alpha.
   ifTM alpha (test_char ? (λc.¬c==sep))
-     (single_finalTM … (seq … (swap_r alpha sep) (move_r ?))) (nop ?) tc_true.
+     (single_finalTM … (swap_l alpha sep · move_r ?)) (nop ?) tc_true.
 
-definition Rmcc_step_true ≝ 
+definition Rmcr_step_true ≝ 
   λalpha,sep,t1,t2.
    ∀a,b,ls,rs.  
     t1 = midtape alpha (a::ls) b rs → 
     b ≠ sep ∧
     t2 = mk_tape alpha (a::b::ls) (option_hd ? rs) (tail ? rs).
 
-definition Rmcc_step_false ≝ 
+definition Rmcr_step_false ≝ 
   λalpha,sep,t1,t2.
     left ? t1 ≠ [] →  current alpha t1 ≠ None alpha → 
       current alpha t1 = Some alpha sep ∧ t2 = t1.
     
-lemma sem_mcc_step :
+lemma sem_mcr_step :
   ∀alpha,sep.
-  mcc_step alpha sep ⊨ 
-    [inr … (inl … (inr … start_nop)): Rmcc_step_true alpha sep, Rmcc_step_false alpha sep].  
+  mcr_step alpha sep ⊨ 
+    [inr … (inl … (inr … start_nop)): Rmcr_step_true alpha sep, Rmcr_step_false alpha sep].  
 #alpha #sep 
   @(acc_sem_if_app … 
-     (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_r …)) (sem_nop …))
+     (sem_test_char …) (sem_seq …(sem_swap_l …) (sem_move_r …)) (sem_nop …))
   [#intape #outtape #tapea whd in ⊢ (%→%→%);
    #Htapea * #tapeb * whd in ⊢ (%→%→?);
    #Htapeb #Houttape #a #b #ls #rs #Hintape
@@ -70,7 +70,7 @@ qed.
 
 (* the move_char (variant c) machine *)
 definition move_char_r ≝ 
-  λalpha,sep.whileTM alpha (mcc_step alpha sep) (inr … (inl … (inr … start_nop))).
+  λalpha,sep.whileTM alpha (mcr_step alpha sep) (inr … (inl … (inr … start_nop))).
 
 definition R_move_char_r ≝ 
   λalpha,sep,t1,t2.
@@ -84,7 +84,7 @@ lemma sem_move_char_r :
   ∀alpha,sep.
   WRealize alpha (move_char_r alpha sep) (R_move_char_r alpha sep).
 #alpha #sep #inc #i #outc #Hloop
-lapply (sem_while … (sem_mcc_step alpha sep) inc i outc Hloop) [%]
+lapply (sem_while … (sem_mcr_step alpha sep) inc i outc Hloop) [%]
 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 [ #tapea whd in ⊢ (% → ?); #H1 #b #a #ls #rs #Htapea
   %
@@ -125,7 +125,7 @@ lemma terminate_move_char_r :
   ∀alpha,sep.∀t,b,a,ls,rs. t = midtape alpha (a::ls) b rs →  
   (b = sep ∨ memb ? sep rs = true) → Terminate alpha (move_char_r alpha sep) t.
 #alpha #sep #t #b #a #ls #rs #Ht #Hsep
-@(terminate_while … (sem_mcc_step alpha sep))
+@(terminate_while … (sem_mcr_step alpha sep))
   [%
   |generalize in match Hsep; -Hsep
    generalize in match Ht; -Ht
@@ -178,7 +178,7 @@ include "turing/if_machine.ma".
 
 definition mcl_step ≝ λalpha:FinSet.λsep:alpha.
   ifTM alpha (test_char ? (λc.¬c==sep))
-     (single_finalTM … (seq … (swap alpha sep) (move_l ?))) (nop ?) tc_true.
+     (single_finalTM … (swap_r alpha sep · move_l ?)) (nop ?) tc_true.
      
 definition Rmcl_step_true ≝ 
   λalpha,sep,t1,t2.
@@ -201,7 +201,7 @@ lemma sem_mcl_step :
     [mcls_acc alpha sep: Rmcl_step_true alpha sep, Rmcl_step_false alpha sep].
 #alpha #sep 
 @(acc_sem_if_app … 
-  (sem_test_char …) (sem_seq …(sem_swap …) (sem_move_l …)) (sem_nop …))
+  (sem_test_char …) (sem_seq …(sem_swap_r …) (sem_move_l …)) (sem_nop …))
   [#intape #outtape #tapea whd in ⊢ (%→%→%);
    #Htapea * #tapeb * whd in ⊢ (%→%→?);
    #Htapeb #Houttape #a #b #ls #rs #Hintape
diff --git a/matita/matita/lib/turing/universal/marks.ma b/matita/matita/lib/turing/universal/marks.ma
index 829f56dc5..2a8199266 100644
--- a/matita/matita/lib/turing/universal/marks.ma
+++ b/matita/matita/lib/turing/universal/marks.ma
@@ -319,8 +319,7 @@ qed.
 
 definition adv_mark_r ≝ 
   λalpha:FinSet.
-    seq ? (clear_mark alpha)
-      (seq ? (move_r ?) (mark alpha)).
+    clear_mark alpha · move_r ? · mark alpha.
       
 definition R_adv_mark_r ≝ λalpha,t1,t2.
   ∀ls,c,d,b,rs.
@@ -443,11 +442,10 @@ qed.
         ^
 *)
 
-definition adv_both_marks ≝ 
-  λalpha.seq ? (adv_mark_r alpha)
-    (seq ? (move_l ?)
-     (seq ? (adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha))
-       (adv_mark_r alpha))).
+definition adv_both_marks ≝ λalpha.
+  adv_mark_r alpha · move_l ? ·
+    adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha) · 
+      adv_mark_r alpha.
 
 definition R_adv_both_marks ≝ 
   λalpha,t1,t2.
@@ -542,11 +540,9 @@ qed.
       else M
 *)
 
-definition comp_step_subcase ≝ 
-  λalpha,c,elseM.ifTM ? (test_char ? (λx.x == c))
-    (seq ? (move_r …)
-      (seq ? (adv_to_mark_r ? (is_marked alpha)) 
-      (match_and_adv ? (λx.x == c))))
+definition comp_step_subcase ≝ λalpha,c,elseM.
+  ifTM ? (test_char ? (λx.x == c))
+    (move_r … · adv_to_mark_r ? (is_marked alpha) · match_and_adv ? (λx.x == c))
     elseM tc_true.
 
 definition R_comp_step_subcase ≝ 
diff --git a/matita/matita/lib/turing/universal/match_machines.ma b/matita/matita/lib/turing/universal/match_machines.ma
index ea7ab99db..b1765e693 100644
--- a/matita/matita/lib/turing/universal/match_machines.ma
+++ b/matita/matita/lib/turing/universal/match_machines.ma
@@ -40,7 +40,7 @@ if current (* x *) = #
  *)
  
 definition mark_next_tuple ≝ 
-  seq ? (adv_to_mark_r ? bar_or_grid)
+  adv_to_mark_r ? bar_or_grid ·
      (ifTM ? (test_char ? (λc:STape.is_bar (\fst c)))
        (move_right_and_mark ?) (nop ?) tc_true).
 
@@ -135,9 +135,7 @@ lapply (sem_seq ? (adv_to_mark_r ? bar_or_grid)
 qed.
 
 definition init_current_on_match ≝ 
-  (seq ? (move_l ?)
-    (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
-      (seq ? (move_r ?) (mark ?)))).
+  move_l ? · adv_to_mark_l ? (λc:STape.is_grid (\fst c)) · move_r ? · mark ?.
           
 definition R_init_current_on_match ≝ λt1,t2.
   ∀l1,l2,c,rs. no_grids l1 → is_grid c = false → 
@@ -239,10 +237,8 @@ qed.
 *)
 
 definition init_current ≝ 
-  seq ? (adv_to_mark_l ? (is_marked ?))
-    (seq ? (clear_mark ?)
-       (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
-          (seq ? (move_r ?) (mark ?)))).
+  adv_to_mark_l ? (is_marked ?) ·clear_mark ? ·
+    adv_to_mark_l ? (λc:STape.is_grid (\fst c)) · move_r ? · mark ?.
           
 definition R_init_current ≝ λt1,t2.
   ∀l1,c,l2,b,l3,c1,rs,c0,b0. no_marks l1 → no_grids l2 → is_grid c = false → 
@@ -283,12 +279,12 @@ qed.
 definition match_tuple_step ≝ 
   ifTM ? (test_char ? (λc:STape.¬ is_grid (\fst c))) 
    (single_finalTM ? 
-     (seq ? compare
+     (compare ·
       (ifTM ? (test_char ? (λc:STape.is_grid (\fst c)))
         (nop ?)
-        (seq ? mark_next_tuple 
+        (mark_next_tuple ·
            (ifTM ? (test_char ? (λc:STape.is_grid (\fst c)))
-             (mark ?) (seq ? (move_l ?) init_current) tc_true)) tc_true)))
+             (mark ?) (move_l ? · init_current) tc_true)) tc_true)))
     (nop ?) tc_true.
 
 definition R_match_tuple_step_true ≝ λt1,t2.
diff --git a/matita/matita/lib/turing/universal/move_tape.ma b/matita/matita/lib/turing/universal/move_tape.ma
index ab16d56c7..4e9b9ec1f 100644
--- a/matita/matita/lib/turing/universal/move_tape.ma
+++ b/matita/matita/lib/turing/universal/move_tape.ma
@@ -90,17 +90,17 @@ swap
 (* l1 # l2 r  ---> l1 r # l2 
            ^          ^
  *)
-definition mtr_aux ≝ 
-  seq ? (move_l …) (seq ? (move_char_l STape 〈grid,false〉)
-   (swap STape 〈grid,false〉)).
-definition R_mtr_aux ≝ λt1,t2.
+definition move_after_left_bar ≝ 
+  move_l … · move_char_l STape 〈grid,false〉 · swap_r STape 〈grid,false〉.
+  
+definition R_move_after_left_bar ≝ λt1,t2.
   ∀l1,l2,l3,r. t1 = midtape STape (l2@〈grid,false〉::l1) r l3 → no_grids l2 → 
   t2 = midtape STape l1 r (〈grid,false〉::reverse ? l2@l3).
 
-lemma sem_mtr_aux : Realize ? mtr_aux R_mtr_aux.
+lemma sem_move_after_left_bar : Realize ? move_after_left_bar R_move_after_left_bar.
 #intape 
 cases (sem_seq … (sem_move_l …) (sem_seq … (ssem_move_char_l STape 〈grid,false〉)
-        (sem_swap STape 〈grid,false〉)) intape)
+        (sem_swap_r STape 〈grid,false〉)) intape)
 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)  % [@Hloop] -Hloop
 #l1 #l2 #l3  #r #Hintape #Hl2
 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
@@ -121,9 +121,8 @@ cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
 qed.
 
 definition move_tape_r ≝ 
-  seq ? (move_r …) (seq ? init_cell (seq ? (move_l …) 
-   (seq ? (swap STape 〈grid,false〉) 
-     (seq ? mtr_aux (seq ? (move_l …) (seq ? mtr_aux (move_r …))))))).
+  move_r … · init_cell · move_l … · swap_r STape 〈grid,false〉 ·
+    move_after_left_bar · move_l … · move_after_left_bar · move_r ….
 
 definition R_move_tape_r ≝ λt1,t2.
   ∀rs,n,table,c0,bc0,curconfig,ls0.
@@ -140,8 +139,8 @@ definition R_move_tape_r ≝ λt1,t2.
 lemma sem_move_tape_r : Realize ? move_tape_r R_move_tape_r.
 #tapein 
 cases (sem_seq …(sem_move_r …) (sem_seq … sem_init_cell (sem_seq … (sem_move_l …)
-   (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … sem_mtr_aux
-     (sem_seq … (sem_move_l …) (sem_seq … sem_mtr_aux (sem_move_r …))))))) tapein)
+   (sem_seq … (sem_swap_r STape 〈grid,false〉) (sem_seq … sem_move_after_left_bar
+     (sem_seq … (sem_move_l …) (sem_seq … sem_move_after_left_bar (sem_move_r …))))))) tapein)
 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
 #rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Htapein
 cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein) -Hta #Hta
@@ -196,15 +195,15 @@ MOVE TAPE LEFT:
      ^
 *)
 definition mtl_aux ≝ 
-  seq ? (swap STape 〈grid,false〉)
-   (seq ? (move_r …) (seq ? (move_r …) (seq ? (move_char_r STape 〈grid,false〉) (move_l …)))).
+  swap_r STape 〈grid,false〉 · move_r … · move_r … · 
+    move_char_r STape 〈grid,false〉 · move_l ….
 definition R_mtl_aux ≝ λt1,t2.
   ∀l1,l2,l3,r. t1 = midtape STape l1 r (〈grid,false〉::l2@〈grid,false〉::l3) → no_grids l2 → 
   t2 = midtape STape (reverse ? l2@〈grid,false〉::l1) r (〈grid,false〉::l3).
 
 lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
 #intape 
-cases (sem_seq … (sem_swap STape 〈grid,false〉) (sem_seq … (sem_move_r …)
+cases (sem_seq … (sem_swap_r STape 〈grid,false〉) (sem_seq … (sem_move_r …)
         (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_r STape 〈grid,false〉) 
           (sem_move_l …)))) intape)
 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
@@ -253,20 +252,16 @@ cases ls1 in Hnogrids;
 qed.
 
 definition move_tape_l : TM STape ≝ 
-  seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
-  (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
-   (seq ? (move_l …)
-    (seq ? init_cell
-     (seq ? mtl_aux
-      (seq ? (swap_r STape 〈grid,false〉)
-       (seq ? mtl_aux
-        (seq ? (swap STape 〈grid,false〉)
-         (seq ? (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c))))
-          (seq ? (move_l …) (adv_to_mark_l … (λc:STape.is_grid (\fst c)))))))))))).
+  (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
+    (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
+     move_l … · init_cell · mtl_aux · swap_l STape 〈grid,false〉 ·
+       mtl_aux ·swap_r STape 〈grid,false〉 ·
+         (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))) ·
+           (move_l … · adv_to_mark_l … (λc:STape.is_grid (\fst c))).
         
 (*  seq ? (move_r …) (seq ? init_cell (seq ? (move_l …) 
    (seq ? (swap STape 〈grid,false〉) 
-     (seq ? mtr_aux (seq ? (move_l …) mtr_aux))))). *)
+     (seq ? move_after_left_bar (seq ? (move_l …) move_after_left_bar))))). *)
 
 definition R_move_tape_l ≝ λt1,t2.
   ∀rs,n,table,c0,bc0,curconfig,ls0.
@@ -288,9 +283,9 @@ cases (sem_seq … sem_ml_atml
    (sem_seq … (sem_move_l …)
     (sem_seq … sem_init_cell
      (sem_seq … sem_mtl_aux 
-      (sem_seq … (sem_swap_r STape 〈grid,false〉)
+      (sem_seq … (sem_swap_l STape 〈grid,false〉)
        (sem_seq … sem_mtl_aux
-        (sem_seq … (sem_swap STape 〈grid,false〉)
+        (sem_seq … (sem_swap_r STape 〈grid,false〉)
          (sem_seq … sem_ml_atml sem_ml_atml)))))))) tapein)
 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
 #rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Hls0 #Htapein
@@ -396,19 +391,6 @@ definition move_of_unialpha ≝
   [ bit x ⇒ match x with [ true ⇒ R | false ⇒ L ]
   | _ ⇒ N ].
 
-definition R_uni_step ≝ λt1,t2.
-  ∀n,table,c,c1,ls,rs,curs,curc,news,newc,mv.
-  table_TM n table → 
-  match_in_table n (〈c,false〉::curs) 〈curc,false〉 
-    (〈c1,false〉::news) 〈newc,false〉 〈mv,false〉 table → 
-  t1 = midtape STape (〈grid,false〉::ls) 〈c,false〉 
-    (curs@〈curc,false〉::〈grid,false〉::table@〈grid,false〉::rs) → 
-  ∀t1',ls1,rs1.t1' = lift_tape ls 〈curc,false〉 rs → 
-  (t2 = midtape STape (〈grid,false〉::ls1) 〈c1,false〉 
-    (news@〈newc,false〉::〈grid,false〉::table@〈grid,false〉::rs1) ∧
-   lift_tape ls1 〈newc,false〉 rs1 = 
-   tape_move STape t1' (Some ? 〈〈newc,false〉,move_of_unialpha mv〉)).
-
 definition no_nulls ≝ 
  λl:list STape.∀x.memb ? x l = true → is_null (\fst x) = false.
  
@@ -676,11 +658,11 @@ definition move_tape ≝
   ifTM ? (test_char ? (λc:STape.c == 〈bit false,false〉)) 
     (* spostamento a sinistra: verificare se per caso non conviene spostarsi 
        sulla prima grid invece dell'ultima *)
-    (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_l)
+    (adv_to_mark_r ? (λc:STape.is_grid (\fst c)) · move_tape_l)
     (ifTM ? (test_char ? (λc:STape.c == 〈bit true,false〉)) 
-       (seq ? (adv_to_mark_r ? (λc:STape.is_grid (\fst c))) move_tape_r)
-       (seq ? (adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
-          (seq ? (move_l …) (adv_to_mark_l ? (λc:STape.is_grid (\fst c))))) 
+       (adv_to_mark_r ? (λc:STape.is_grid (\fst c)) · move_tape_r)
+       (adv_to_mark_l ? (λc:STape.is_grid (\fst c)) ·
+          move_l … · adv_to_mark_l ? (λc:STape.is_grid (\fst c)))
        tc_true) tc_true.
            
 definition R_move_tape ≝ λt1,t2.
diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
index 39b05addf..fc663ff2c 100644
--- 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. 
@@ -241,9 +233,7 @@ cases HR -HR
 qed. *)
 
 definition exec_action ≝ 
-  seq ? init_copy
-    (seq ? copy
-      (seq ? (move_r …) move_tape)).
+  init_copy · copy · move_r … · move_tape.
 
 definition map_move ≝ 
   λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
@@ -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_action (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.
-- 
2.39.2