X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Fmarks.ma;h=bfa8b8a748b48c7702770253ac1809da712f8971;hb=ce60ad8a7d4c56f218d95c3547abe896057de040;hp=ede90b649c4d5e0553d588de810cad8c39031c51;hpb=a134bd3b2ef9e59fdbf8bdc64f409e67fa1d7d9e;p=helm.git

diff --git a/matita/matita/lib/turing/universal/marks.ma b/matita/matita/lib/turing/universal/marks.ma
index ede90b649..bfa8b8a74 100644
--- a/matita/matita/lib/turing/universal/marks.ma
+++ b/matita/matita/lib/turing/universal/marks.ma
@@ -111,15 +111,31 @@ lemma sem_atmr_step :
 ]
 qed.
 
+lemma dec_test: ∀alpha,rs,test. 
+ decidable (∀c.memb alpha c rs = true → test c = false).
+#alpha #rs #test elim rs 
+  [%1 #n normalize #H destruct
+  |#a #tl cases (true_or_false (test a)) #Ha 
+    [#_ %2 % #Hall @(absurd ?? not_eq_true_false) <Ha 
+     @Hall @memb_hd 
+    |* [#Hall %1 #c #memc cases (orb_true_l … memc) 
+         [#eqca >(\P eqca) @Ha |@Hall]
+    |#Hnall %2 @(not_to_not … Hnall) #Hall #c #memc @Hall @memb_cons //
+    ]
+  qed.
+
 definition R_adv_to_mark_r ≝ λalpha,test,t1,t2.
   (current ? t1 = None ? → t1 = t2) ∧
   ∀ls,c,rs.
   (t1 = midtape alpha ls c rs  → 
   ((test c = true ∧ t2 = t1) ∨
    (test c = false ∧
-    ∀rs1,b,rs2. rs = rs1@b::rs2 → 
+    (∀rs1,b,rs2. rs = rs1@b::rs2 → 
      test b = true → (∀x.memb ? x rs1 = true → test x = false) → 
-     t2 = midtape ? (reverse ? rs1@c::ls) b rs2))).
+     t2 = midtape ? (reverse ? rs1@c::ls) b rs2) ∧
+     ((∀x.memb ? x rs = true → test x = false) → 
+      ∀a,l.reverse ? (c::rs) = a::l → 
+      t2 = rightof alpha a (l@ls))))).
      
 definition adv_to_mark_r ≝ 
   λalpha,test.whileTM alpha (atmr_step alpha test) atm2.
@@ -149,20 +165,37 @@ lapply (sem_while … (sem_atmr_step alpha test) t i outc Hloop) [%]
    whd in ⊢((??%?)→?); #H destruct (H);
   |#ls #c #rs #Htapea %2
    cases Hleft #ls0 * #a0 * #rs0 * * #Htapea' #Htest #Htapeb
-   >Htapea' in Htapea; #Htapea destruct (Htapea) % // *
+   >Htapea' in Htapea; #Htapea destruct (Htapea) % [ % // ]
+   [*
     [ #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #_
      cases (proj2 ?? IH … Htapeb)
       [ * #_ #Houtc >Houtc >Htapeb %
-      | * #Hfalse >Hfalse in Htestb; #Htestb destruct (Htestb) ]
+      | * * >Htestb #Hfalse destruct (Hfalse) ]
     | #r1 #rs1 #b #rs2 #Hrs >Hrs in Htapeb; #Htapeb #Htestb #Hmemb
      cases (proj2 ?? IH … Htapeb)
       [ * #Hfalse >(Hmemb …) in Hfalse;
         [ #Hft destruct (Hft)
         | @memb_hd ]
-      | * #Htestr1 #H1 >reverse_cons >associative_append
+      | * * #Htestr1 #H1 #_ >reverse_cons >associative_append
        @H1 // #x #Hx @Hmemb @memb_cons //
       ]
     ]
+   |cases rs in Htapeb; normalize in ⊢ (%→?);
+    [#Htapeb #_ #a0 #l whd in ⊢ ((??%?)→?); #Hrev destruct (Hrev) 
+     >Htapeb in IH; #IH cases (proj1 ?? IH … (refl …)) //
+    |#r1 #rs1 #Htapeb #Hmemb
+     cases (proj2 ?? IH … Htapeb) [ * >Hmemb [ #Hfalse destruct(Hfalse) ] @memb_hd ]
+     * #_ #H1 #a #l <(reverse_reverse … l) cases (reverse … l)
+      [#H cut (c::r1::rs1 = [a])
+        [<(reverse_reverse  … (c::r1::rs1)) >H //]
+       #Hrev destruct (Hrev)
+      |#a1 #l2 >reverse_cons >reverse_cons >reverse_cons 
+       #Hrev cut ([c] = [a1])
+        [@(append_l2_injective_r ?? (a::reverse … l2) … Hrev) //]
+       #Ha <Ha >associative_append @H1
+        [#x #membx @Hmemb @memb_cons @membx
+        |<(append_l1_injective_r ?? (a::reverse … l2) … Hrev) //
+        ]
 qed.
 
 lemma terminate_adv_to_mark_r :
@@ -452,9 +485,12 @@ definition R_adv_to_mark_l ≝ λalpha,test,t1,t2.
   (t1 = midtape alpha ls c rs  → 
   ((test c = true → t2 = t1) ∧
    (test c = false →
-    ∀ls1,b,ls2. ls = ls1@b::ls2 → 
+    (∀ls1,b,ls2. ls = ls1@b::ls2 → 
      test b = true → (∀x.memb ? x ls1 = true → test x = false) → 
-     t2 = midtape ? ls2 b (reverse ? ls1@c::rs)))).
+     t2 = midtape ? ls2 b (reverse ? ls1@c::rs)) ∧     
+    ((∀x.memb ? x ls = true → test x = false) →
+      ∀a,l. reverse ? (c::ls) = a::l → t2 = leftof ? a (l@rs))
+     ))).
 
 definition adv_to_mark_l ≝ 
   λalpha,test.whileTM alpha (atml_step alpha test) atm2.
@@ -489,14 +525,35 @@ lapply (sem_while … (sem_atml_step alpha test) t i outc Hloop) [%]
      >Htapea' in Htapea; #H destruct /2/
     |cases Hleft #ls0 * #a * #rs0 *
      * #Htapea1 >Htapea in Htapea1; #H destruct (H) #_ #Htapeb
-     #Hc *
-      [#b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #_
-       cases (proj2 ?? IH … Htapeb) #H1 #_ >H1 // >Htapeb %
-      |#l1 #ls1 #b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #Hmemb
-       cases (proj2 ?? IH … Htapeb) #_ #H1 >reverse_cons >associative_append 
-       @(H1 … (refl …) Htestb)
-        [@Hmemb @memb_hd
-        |#x #memx @Hmemb @memb_cons @memx
+     #Hc %
+      [*
+        [#b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #_
+         cases (proj2 ?? IH … Htapeb) #H1 #_ >H1 // >Htapeb %
+        |#l1 #ls1 #b #ls2 #Hls >Hls in Htapeb; #Htapeb #Htestb #Hmemb 
+         cases (proj2 ?? IH … Htapeb) #_ #H1 >reverse_cons >associative_append
+         @(proj1 ?? (H1 ?) … (refl …) Htestb …)
+          [@Hmemb @memb_hd
+          |#x #memx @Hmemb @memb_cons @memx
+          ]
+        ]
+      |cases ls0 in Htapeb; normalize in ⊢ (%→?);
+        [#Htapeb #Htest #a0 #l whd in ⊢ ((??%?)→?); #Hrev destruct (Hrev) 
+         >Htapeb in IH; #IH cases (proj1 ?? IH … (refl …)) //
+        |#l1 #ls1 #Htapeb
+         cases (proj2 ?? IH … Htapeb) #_ #H1 #Htest #a0 #l
+         <(reverse_reverse … l) cases (reverse … l)
+          [#H cut (a::l1::ls1 = [a0])
+            [<(reverse_reverse  … (a::l1::ls1)) >H //]
+           #Hrev destruct (Hrev)
+          |#a1 #l2 >reverse_cons >reverse_cons >reverse_cons 
+           #Hrev cut ([a] = [a1])
+            [@(append_l2_injective_r ?? (a0::reverse … l2) … Hrev) //]
+           #Ha <Ha >associative_append @(proj2 ?? (H1 ?))
+            [@Htest @memb_hd
+            |#x #membx @Htest @memb_cons @membx
+            |<(append_l1_injective_r ?? (a0::reverse … l2) … Hrev) //
+            ]
+          ]
         ]
       ]
     ]
@@ -551,16 +608,17 @@ definition adv_both_marks ≝ λalpha.
     adv_to_mark_l (FinProd alpha FinBool) (is_marked alpha) · 
       adv_mark_r alpha.
 
-definition R_adv_both_marks ≝ 
-  λalpha,t1,t2.
-    ∀l0,x,a,l1,x0. (∀c.memb ? c l1 = true → is_marked ? c = false) → 
-    (∀l1',a0,l2. t1 = midtape (FinProd … alpha FinBool) 
-        (l1@〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) → 
-     reverse ? (〈x0,false〉::l1) = 〈a,false〉::l1' →
-     t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1'@〈a0,true〉::l2)) ∧
-     (t1 = midtape (FinProd … alpha FinBool) 
-        (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 [ ] → 
-     t2 = rightof ? 〈x0,false〉 (l1@〈a,false〉::〈x,true〉::l0)).
+definition R_adv_both_marks ≝ λalpha,t1,t2.
+  ∀ls,x0,rs.
+    t1 = midtape (FinProd … alpha FinBool) ls 〈x0,true〉 rs →   
+     (rs = [ ] → (* first case: rs empty *)
+       t2 = rightof (FinProd … alpha FinBool) 〈x0,false〉 ls) ∧       
+     (∀l0,x,a,a0,b,l1,l1',l2. 
+       ls = (l1@〈x,true〉::l0) →
+       (∀c.memb ? c l1 = true → is_marked ? c = false) → 
+       rs = (〈a0,b〉::l2) →
+       reverse ? (〈x0,false〉::l1) = 〈a,false〉::l1' →
+       t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1'@〈a0,true〉::l2)).
 
 lemma sem_adv_both_marks :
   ∀alpha.Realize ? (adv_both_marks alpha) (R_adv_both_marks alpha).    
@@ -569,20 +627,22 @@ lemma sem_adv_both_marks :
    (sem_seq ????? (sem_move_l …)
       (sem_seq ????? (sem_adv_to_mark_l ? (is_marked ?)) 
         (sem_adv_mark_r alpha))) …)
-#intape #outtape * #tapea * #Hta * #tb * #Htb * #tc * #Htc #Hout 
-#l0 #x #a #l1 #x0 #Hmarks %
-  [#l1' #a0 #l2 #Hintape #Hrev @(proj1 ?? (proj1 ?? Hout … ) ? false) -Hout
+#intape #outtape * #tapea * #Hta * #tb * #Htb * #tc * #Htc #Hout
+#ls #c #rs #Hintape %
+  [#Hrs >Hrs in Hintape; #Hintape lapply (proj2 ?? (proj1 ?? Hta … ) … Hintape) -Hta #Hta
+   lapply (proj1 … Htb) >Hta -Htb #Htb lapply (Htb (refl …)) -Htb #Htb 
+   lapply (proj1 ?? Htc) <Htb -Htc #Htc lapply (Htc (refl …)) -Htc #Htc
+   @sym_eq >Htc @(proj2 ?? Hout …) <Htc %
+  |#l0 #x #a #a0 #b #l1 #l1' #l2 #Hls #Hmarks #Hrs #Hrev 
+   >Hrs in Hintape; >Hls #Hintape
+   @(proj1 ?? (proj1 ?? Hout … ) ? false) -Hout
    lapply (proj1 … (proj1 … Hta …) … Hintape) #Htapea
    lapply (proj2 … Htb  … Htapea) -Htb
    whd in match (mk_tape ????) ; #Htapeb 
-   lapply (proj2 ?? (proj2 ?? Htc … Htapeb) (refl …) … (refl …)) -Htc #Htc
+   lapply (proj1 ?? (proj2 ?? (proj2 ?? Htc … Htapeb) (refl …))) -Htc #Htc
    change with ((?::?)@?) in match (cons ???); <Hrev >reverse_cons
-   >associative_append @Htc [%|@Hmarks] 
-  |#Hintape lapply (proj2 ?? (proj1 ?? Hta … ) … Hintape) -Hta #Hta
-   lapply (proj1 … Htb) >Hta -Htb #Htb lapply (Htb (refl …)) -Htb #Htb 
-   lapply (proj1 ?? Htc) <Htb -Htc #Htc lapply (Htc (refl …)) -Htc #Htc
-   @sym_eq >Htc @(proj2 ?? Hout …) <Htc % 
-  ]
+   >associative_append @Htc [%|%|@Hmarks]
+  ] 
 qed.
 
 (*
@@ -645,13 +705,52 @@ definition match_and_adv ≝
 
 definition R_match_and_adv ≝ 
   λalpha,f,t1,t2.
-    ∀l0,x,a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) → 
-    t1 = midtape (FinProd … alpha FinBool) 
-        (l1@〈a,false〉::〈x,true〉::l0) 〈x0,true〉 (〈a0,false〉::l2) → 
-    (f 〈x0,true〉 = true ∧ t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (reverse ? l1@〈x0,false〉::〈a0,true〉::l2))
-    ∨ (f 〈x0,true〉 = false ∧ 
-    t2 = midtape ? (l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)).
+    ∀ls,x0,rs.
+     t1 = midtape (FinProd … alpha FinBool) ls 〈x0,true〉 rs →   
+    ((* first case: (f 〈x0,true〉 = false) *)
+     (f 〈x0,true〉 = false) → 
+       t2 = midtape (FinProd … alpha FinBool) ls 〈x0,false〉 rs) ∧   
+    ((f 〈x0,true〉 = true) →  rs = [ ] → (* second case: rs empty *)
+       t2 = rightof (FinProd … alpha FinBool) 〈x0,false〉 ls) ∧       
+    ((f 〈x0,true〉 = true) →  
+     ∀l0,x,a,a0,b,l1,l1',l2. 
+     (* third case: we expect to have a mark on the left! *)
+     ls = (l1@〈x,true〉::l0) → 
+     (∀c.memb ? c l1 = true → is_marked ? c = false) → 
+     rs = 〈a0,b〉::l2 →
+     reverse ? (〈x0,false〉::l1) = 〈a,false〉::l1' →
+       t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1'@〈a0,true〉::l2)).
+
+lemma sem_match_and_adv : 
+  ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
+#alpha #f #intape
+cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
+#k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
+% [ @Hloop ] -Hloop
+(* 
+@(sem_if_app … (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?))
+#intape #outape #Htb * #H *)
+cases Hif -Hif
+[ * #ta * whd in ⊢ (%→%→?); * * #c * #Hcurrent #fc #Hta #Houtc
+  #ls #x #rs #Hintape >Hintape in Hcurrent; whd in ⊢ ((??%?)→?); #H destruct (H) %
+  [%[>fc #H destruct (H) 
+    |#_ #Hrs >Hrs in Hintape; #Hintape >Hintape in Hta; #Hta
+     cases (Houtc … Hta) #Houtc #_ @Houtc //
+    ]
+  |#l0 #x0 #a #a0 #b #l1 #l1' #l2 #Hls #Hmarks #Hrs #Hrev >Hintape in Hta; #Hta
+   @(proj2 ?? (Houtc … Hta) … Hls Hmarks Hrs Hrev)
+  ]
+| * #ta * * #H #Hta * #_ #Houtc #ls #c #rs #Hintape 
+   >Hintape in H; #H lapply(H … (refl …)) #fc %
+  [%[#_ >Hintape in Hta; #Hta @(Houtc … Hta)
+    |>fc #H destruct (H)
+    ]
+  |>fc #H destruct (H)
+  ]
+]
+qed.
 
+(*
 lemma sem_match_and_adv : 
   ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv alpha f).
 #alpha #f #intape
@@ -671,6 +770,31 @@ cases Hif
   * #Hf #Hta %2 % [ @Hf % | >(proj2 ?? Houtc … Hta) % ]
 ]
 qed.
+*)
+
+definition R_match_and_adv_of ≝ 
+  λalpha,t1,t2.current (FinProd … alpha FinBool) t1 = None ? → t2 = t1.
+
+lemma sem_match_and_adv_of : 
+  ∀alpha,f.Realize ? (match_and_adv alpha f) (R_match_and_adv_of alpha).
+#alpha #f #intape
+cases (sem_if ? (test_char ? f) … tc_true (sem_test_char ? f) (sem_adv_both_marks alpha) (sem_clear_mark ?) intape)
+#k * #outc * #Hloop #Hif @(ex_intro ?? k) @(ex_intro ?? outc)
+% [ @Hloop ] -Hloop
+cases Hif
+[ * #ta * whd in ⊢ (%→%→?); #Hta #Houtc #Hcur
+  cases Hta * #x >Hcur * #Hfalse destruct (Hfalse)
+| * #ta * whd in ⊢ (%→%→?); * #_ #Hta * #Houtc #_ <Hta #Hcur >(Houtc Hcur) % ]
+qed.
+
+lemma sem_match_and_adv_full : 
+  ∀alpha,f.Realize ? (match_and_adv alpha f) 
+    (R_match_and_adv alpha f ∩ R_match_and_adv_of alpha).
+#alpha #f #intape cases (sem_match_and_adv ? f intape)
+#i * #outc * #Hloop #HR1 %{i} %{outc} % // % //
+cases (sem_match_and_adv_of ? f intape) #i0 * #outc0 * #Hloop0 #HR2
+>(loop_eq … Hloop Hloop0) //
+qed.
 
 (*
  if x = c
@@ -691,16 +815,41 @@ definition comp_step_subcase ≝ λalpha,c,elseM.
 
 definition R_comp_step_subcase ≝ 
   λalpha,c,RelseM,t1,t2.
-    ∀l0,x,rs.t1 = midtape (FinProd … alpha FinBool) l0 〈x,true〉 rs → 
-    (〈x,true〉 = c ∧
-     ∀a,l1,x0,a0,l2. (∀c.memb ? c l1 = true → is_marked ? c = false) → 
-     rs = 〈a,false〉::l1@〈x0,true〉::〈a0,false〉::l2 → 
-     ((x = x0 ∧
-      t2 = midtape ? (〈x,false〉::l0) 〈a,true〉 (l1@〈x0,false〉::〈a0,true〉::l2)) ∨
-      (x ≠ x0 ∧
-      t2 = midtape (FinProd … alpha FinBool) 
-        (reverse ? l1@〈a,false〉::〈x,true〉::l0) 〈x0,false〉 (〈a0,false〉::l2)))) ∨
-    (〈x,true〉 ≠ c ∧ RelseM t1 t2).
+    ∀ls,x,rs.t1 = midtape (FinProd … alpha FinBool) ls 〈x,true〉 rs → 
+    (〈x,true〉 = c →
+     ((* test true but no marks in rs *)
+      (∀c.memb ? c rs = true → is_marked ? c = false) →
+       ∀a,l. (a::l) = reverse ? (〈x,true〉::rs) → 
+       t2 = rightof (FinProd alpha FinBool) a (l@ls)) ∧ 
+    ∀l1,x0,l2. 
+     (∀c.memb ? c l1 = true → is_marked ? c = false) → 
+      rs = l1@〈x0,true〉::l2 → 
+      (x = x0 → 
+       l2 = [ ] → (* test true but l2 is empty *) 
+       t2 = rightof ? 〈x0,false〉 ((reverse ? l1)@〈x,true〉::ls))  ∧
+      (x = x0 →
+       ∀a,a0,b,l1',l2'. (* test true and l2 is not empty *) 
+       〈a,false〉::l1' = l1@[〈x0,false〉] →
+       l2 = 〈a0,b〉::l2' →
+       t2 = midtape ? (〈x,false〉::ls) 〈a,true〉 (l1'@〈a0,true〉::l2')) ∧
+      (x ≠ x0 →(* test false *)
+      t2 = midtape (FinProd … alpha FinBool) ((reverse ? l1)@〈x,true〉::ls) 〈x0,false〉 l2)) ∧
+    (〈x,true〉 ≠ c → RelseM t1 t2).
+
+lemma dec_marked: ∀alpha,rs. 
+ decidable (∀c.memb ? c rs = true → is_marked alpha c = false).
+#alpha #rs elim rs 
+  [%1 #n normalize #H destruct
+  |#a #tl cases (true_or_false (is_marked ? a)) #Ha 
+    [#_ %2 % #Hall @(absurd ?? not_eq_true_false) <Ha 
+     @Hall @memb_hd 
+    |* [#Hall %1 #c #memc cases (orb_true_l … memc) 
+         [#eqca >(\P eqca) @Ha |@Hall]
+    |#Hnall %2 @(not_to_not … Hnall) #Hall #c #memc @Hall @memb_cons //
+    ]
+  qed.
+
+(* axiom daemon:∀P:Prop.P. *)
 
 lemma sem_comp_step_subcase : 
   ∀alpha,c,elseM,RelseM.
@@ -712,32 +861,101 @@ cases (sem_if ? (test_char ? (λx.x == c)) … tc_true
         (sem_test_char ? (λx.x == c)) 
         (sem_seq ????? (sem_move_r …)
           (sem_seq ????? (sem_adv_to_mark_r ? (is_marked alpha))
-             (sem_match_and_adv ? (λx.x == c)))) Helse intape)
+             (sem_match_and_adv_full ? (λx.x == c)))) Helse intape)
 #k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc)
 % [ @Hloop ] -Hloop cases HR -HR
-[ * #ta * whd in ⊢ (%→?); #Hta * #tb * whd in ⊢ (%→?); #Htb
-  * #tc * whd in ⊢ (%→?); #Htc whd in ⊢ (%→?); #Houtc
-  #l0 #x #rs #Hintape cases (true_or_false (〈x,true〉==c)) #Hc
-  [ % % [ @(\P Hc) ] 
-    #a #l1 #x0 #a0 #l2 #Hl1 #Hrs >Hrs in Hintape; #Hintape
-    >Hintape in Hta; * #_(* #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hx *)
-    #Hta lapply (proj2 … Htb … Hta) -Htb -Hta #Htb
-    cases (Htc … Htb) [ * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
-    -Htc * #_ #Htc lapply (Htc l1 〈x0,true〉 (〈a0,false〉::l2) (refl ??) (refl ??) Hl1)
-    -Htc #Htc cases (Houtc ???????? Htc) -Houtc
-    [ * #Hx0 #Houtc % 
-      % [ <(\P Hx0) in Hc; #Hx lapply (\P Hx) #Hx' destruct (Hx') %
-        | >Houtc >reverse_reverse % ]
-    | * #Hx0 #Houtc %2
-      % [ <(\P Hc) in Hx0; #Hx0 lapply (\Pf Hx0) @not_to_not #Hx' >Hx' %
-        | >Houtc % ]
-    | #x #membx @Hl1 <(reverse_reverse …l1) @memb_reverse @membx ]
-  | %2 % [ @(\Pf Hc) ]
-    >Hintape in Hta; * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) 
-    >Hc #H destruct (H) ]
-| * #ta * whd in ⊢ (%→?); * #Hc #Hta #Helse #ls #c0 #rs #Hintape %2
-  >Hintape in Hta; #Hta % [ @(\Pf (Hc …)) >Hintape % | <Hta @Helse ]
-]
+  [* #ta * whd in ⊢ (%→?); * * #cin * #Hcin #Hcintrue #Hta * #tb * whd in ⊢ (%→?); #Htb
+   * #tc * whd in ⊢ (%→?); #Htc * whd in ⊢ (%→%→?); #Houtc #Houtc1
+   #ls #x #rs #Hintape >Hintape in Hcin; whd in ⊢ ((??%?)→?); #H destruct (H) %
+    [#_ cases (dec_marked ? rs) #Hdec
+      [%
+        [#_ #a #l1 
+         >Hintape in Hta; #Hta
+         lapply (proj2 ?? Htb … Hta) -Htb -Hta cases rs in Hdec;
+           (* by cases on rs *)
+           [#_ whd in ⊢ ((???%)→?); #Htb >Htb in Htc; #Htc
+            lapply (proj1 ?? Htc (refl …)) -Htc #Htc <Htc in Houtc1; #Houtc1
+            normalize in ⊢ (???%→?); #Hl1 destruct(Hl1) @(Houtc1 (refl …))           
+           |#r0 #rs0 #Hdec whd in ⊢ ((???%)→?); #Htb >Htb in Htc; #Htc
+            >reverse_cons >reverse_cons #Hl1
+            cases (proj2 ?? Htc … (refl …))
+            [* >(Hdec …) [ #Hfalse destruct(Hfalse) ] @memb_hd
+            |* #_ -Htc #Htc cut (∃l2.l1 = l2@[〈x,true〉])
+             [generalize in match Hl1; -Hl1 <(reverse_reverse … l1)
+              cases (reverse ? l1)
+              [#Hl1 cut ([a]=〈x,true〉::r0::rs0)
+               [ <(reverse_reverse … (〈x,true〉::r0::rs0))
+                 >reverse_cons >reverse_cons <Hl1 % 
+               | #Hfalse destruct(Hfalse)]
+              |#a0 #l10 >reverse_cons #Heq
+               lapply (append_l2_injective_r ? (a::reverse ? l10) ???? Heq) //
+               #Ha0 destruct(Ha0) /2/ ]
+             |* #l2 #Hl2 >Hl2 in Hl1; #Hl1 
+              lapply (append_l1_injective_r ? (a::l2) … Hl1) // -Hl1 #Hl1
+              >reverse_cons in Htc; #Htc lapply (Htc … (sym_eq … Hl1))
+              [ #x0 #Hmemb @Hdec @memb_cons @Hmemb ]
+              -Htc #Htc >Htc in Houtc1; #Houtc1 >associative_append @Houtc1 % 
+             ]
+            ]
+           ]
+        |#l1 #x0 #l2 #_ #Hrs @False_ind
+         @(absurd ?? not_eq_true_false) 
+         change with (is_marked ? 〈x0,true〉) in match true;
+         @Hdec >Hrs @memb_append_l2 @memb_hd 
+        ]
+      |% [#H @False_ind @(absurd …H Hdec)]
+       (* by cases on l1 *) *
+        [#x0 #l2 #Hdec normalize in ⊢ (%→?); #Hrs >Hrs in Hintape; #Hintape
+         >Hintape in Hta; (* * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hx *)
+         #Hta lapply (proj2 … Htb … Hta) -Htb -Hta 
+         whd in match (mk_tape ????); whd in match (tail ??); #Htb cases Htc -Htc
+         #_ #Htc cases (Htc … Htb) -Htc 
+          [2: * * #Hfalse normalize in Hfalse; destruct (Hfalse) ]
+         * * #Htc >Htb in Htc; -Htb #Htc cases (Houtc … Htc) -Houtc * 
+         #H1 #H2 #H3 cases (true_or_false (x==x0)) #eqxx0
+          [>(\P eqxx0) % [2: #H @False_ind /2/] %
+            [#_ #Hl2 >(H2 … Hl2) <(\P eqxx0) [% | @Hcintrue] 
+            |#_ #a #a0 #b #l1' #l2' normalize in ⊢ (%→?); #Hdes destruct (Hdes)
+             #Hl2 @(H3 … Hdec … Hl2) <(\P eqxx0) [@Hcintrue | % | @reverse_single]
+            ]
+          |% [% #eqx @False_ind lapply (\Pf eqxx0) #Habs @(absurd … eqx Habs)] 
+           #_ @H1 @(\bf ?) @(not_to_not ??? (\Pf eqxx0)) <(\P Hcintrue) 
+           #Hdes destruct (Hdes) %
+          ]
+        |#l1hd #l1tl #x0 #l2 #Hdec normalize in ⊢ (%→?); #Hrs >Hrs in Hintape; #Hintape
+         >Hintape in Hta; (* * * #x1 * whd in ⊢ ((??%?)→?); #H destruct (H) #Hx *)
+         #Hta lapply (proj2 … Htb … Hta) -Htb -Hta 
+         whd in match (mk_tape ????); whd in match (tail ??); #Htb cases Htc -Htc
+         #_ #Htc cases (Htc … Htb) -Htc 
+          [* #Hfalse @False_ind >(Hdec … (memb_hd …)) in Hfalse; #H destruct] 
+         * * #_ #Htc lapply (Htc … (refl …) (refl …) ?) -Htc
+          [#x1 #membx1 @Hdec @memb_cons @membx1] #Htc
+         cases (Houtc … Htc) -Houtc * 
+         #H1 #H2 #H3 #_ cases (true_or_false (x==x0)) #eqxx0
+          [>(\P eqxx0) % [2: #H @False_ind /2/] %
+            [#_ #Hl2 >(H2 … Hl2) <(\P eqxx0) 
+              [>reverse_cons >associative_append % | @Hcintrue] 
+            |#_ #a #a0 #b #l1' #l2' normalize in ⊢ (%→?); #Hdes (* destruct (Hdes) *)
+             #Hl2 @(H3 ?????? (reverse … (l1hd::l1tl)) … Hl2) <(\P eqxx0) 
+              [@Hcintrue 
+              |>reverse_cons >associative_append % 
+              |#c0 #memc @Hdec <(reverse_reverse ? (l1hd::l1tl)) @memb_reverse @memc
+              |>Hdes >reverse_cons >reverse_reverse >(\P eqxx0) %
+              ]
+            ]
+          |% [% #eqx @False_ind lapply (\Pf eqxx0) #Habs @(absurd … eqx Habs)] 
+           #_ >reverse_cons >associative_append @H1 @(\bf ?) 
+           @(not_to_not ??? (\Pf eqxx0)) <(\P Hcintrue) #Hdes 
+           destruct (Hdes) %
+          ]
+        ]
+      ]
+    |>(\P Hcintrue) * #Hfalse @False_ind @Hfalse %
+    ]
+  | * #ta * * #Hcur #Hta #Houtc
+    #l0 #x #rs #Hintape >Hintape in Hcur; #Hcur lapply (Hcur ? (refl …)) -Hcur #Hc %
+    [ #Hfalse >Hfalse in Hc; #Hc cases (\Pf Hc) #Hc @False_ind @Hc %
+    | -Hc #Hc <Hintape <Hta @Houtc ] ]
 qed.
 
 (* 
@@ -763,18 +981,194 @@ definition comp_step ≝
   (nop ?)
   tc_true.
 
+(* da spostare *)
+
+lemma mem_append : ∀A,x,l1,l2. mem A x (l1@l2) → 
+  mem A x l1 ∨ mem A x l2.
+#A #x #l1 elim l1 normalize [/2/]
+#a #tl #Hind #l2 * [#eqxa %1 /2/ |#memx cases (Hind … memx) /3/]
+qed.
+
+let rec split_on A (l:list A) f acc on l ≝ 
+  match l with 
+  [ nil ⇒ 〈acc,nil ?〉
+  | cons a tl ⇒ 
+    if f a then 〈acc,a::tl〉 else split_on A tl f (a::acc) 
+  ].
+  
+lemma split_on_spec: ∀A,l,f,acc,res1,res2.
+  split_on A l f acc = 〈res1,res2〉 → 
+    (∃l1. res1 = l1@acc ∧
+    reverse ? l1@res2 = l ∧ 
+    ∀x. mem ? x l1 → f x = false) ∧ 
+    ∀a,tl. res2 = a::tl → f a = true.
+#A #l #f elim l
+  [#acc #res1 #res2 normalize in ⊢ (%→?); #H destruct % 
+    [@(ex_intro … []) % normalize [% % | #x @False_ind]
+    |#a #tl #H destruct
+    ]
+  |#a #tl #Hind #acc #res1 #res2 normalize in ⊢ (%→?);
+   cases (true_or_false (f a)) #Hfa >Hfa normalize in ⊢ (%→?);
+   #H destruct
+   [% [@(ex_intro … []) % normalize [% % | #x @False_ind]
+      |#a1 #tl1 #H destruct (H) //]
+   |cases (Hind (a::acc) res1 res2 H) * #l1 * *
+    #Hres1 #Htl #Hfalse #Htrue % [2:@Htrue] @(ex_intro … (l1@[a])) % 
+     [% [>associative_append @Hres1 | >reverse_append <Htl % ]
+     |#x #Hmemx cases (mem_append ???? Hmemx) 
+        [@Hfalse | normalize * [#H >H //| @False_ind]
+     ]
+   ]
+  ]
+qed.
+
+axiom mem_reverse: ∀A,l,x. mem A x (reverse ? l) → mem A x l.
+
+lemma split_on_spec_ex: ∀A,l,f.∃l1,l2.
+    l1@l2 = l ∧ (∀x:A. mem ? x l1 → f x = false) ∧ 
+    ∀a,tl. l2 = a::tl → f a = true.
+#A #l #f @(ex_intro … (reverse … (\fst (split_on A l f [])))) 
+@(ex_intro … (\snd (split_on A l f []))) 
+cases (split_on_spec A l f [ ] ?? (eq_pair_fst_snd …)) * #l1 * *
+>append_nil #Hl1 >Hl1 #Hl #Hfalse #Htrue % 
+  [% [@Hl|#x #memx @Hfalse @mem_reverse //] | @Htrue]
+qed.
+
+(* versione esistenziale *)
+
 definition R_comp_step_true ≝ λt1,t2.
-  ∃l0,c,a,l1,c0,a0,l2.
-    t1 = midtape (FinProd … FSUnialpha FinBool) 
-          l0 〈c,true〉 (〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2) ∧
-      (∀c.memb ? c l1 = true → is_marked ? c = false) ∧
-      (bit_or_null c = true → c0 = c →
-        t2 = midtape ? (〈c,false〉::l0) 〈a,true〉 (l1@〈c0,false〉::〈a0,true〉::l2)) ∧
-      (bit_or_null c = true → c0 ≠ c →
-        t2 = midtape (FinProd … FSUnialpha FinBool) 
-         (reverse ? l1@〈a,false〉::〈c,true〉::l0) 〈c0,false〉 (〈a0,false〉::l2)) ∧ 
-      (bit_or_null c = false → 
-        t2 = midtape ? l0 〈c,false〉 (〈a,false〉::l1@〈c0,true〉::〈a0,false〉::l2)).
+  ∃ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls 〈c,true〉 rs ∧
+    ((* bit_or_null c = false *)
+    (bit_or_null c = false → t2 = midtape ? ls 〈c,false〉 rs) ∧
+    (* no marks in rs *)
+    (bit_or_null c = true →
+      (∀c.memb ? c rs = true → is_marked ? c = false) →
+       ∀a,l. (a::l) = reverse ? (〈c,true〉::rs) → 
+       t2 = rightof (FinProd FSUnialpha FinBool) a (l@ls)) ∧
+    (∀l1,c0,l2.
+      bit_or_null c = true →
+      (∀c.memb ? c l1 = true → is_marked ? c = false) → 
+      rs = l1@〈c0,true〉::l2 → 
+      (c = c0 → 
+       l2 = [ ] → (* test true but l2 is empty *) 
+       t2 = rightof ? 〈c0,false〉 ((reverse ? l1)@〈c,true〉::ls))  ∧
+      (c = c0 →
+       ∀a,a0,b,l1',l2'. (* test true and l2 is not empty *) 
+       〈a,false〉::l1' = l1@[〈c0,false〉] →
+       l2 = 〈a0,b〉::l2' →
+       t2 = midtape ? (〈c,false〉::ls) 〈a,true〉 (l1'@〈a0,true〉::l2')) ∧
+      (c ≠ c0 →(* test false *)
+       t2 = midtape (FinProd … FSUnialpha FinBool) 
+         ((reverse ? l1)@〈c,true〉::ls) 〈c0,false〉 l2))).
+
+definition R_comp_step_false ≝ 
+  λt1,t2.
+   ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs → 
+   is_marked ? c = false ∧ t2 = t1.
+
+lemma is_marked_to_exists: ∀alpha,c. is_marked alpha c = true →
+ ∃c'. c = 〈c',true〉.
+#alpha * #c * [#_ @(ex_intro … c) //| normalize #H destruct]
+qed.
+
+lemma exists_current: ∀alpha,c,t. 
+  current alpha t = Some alpha c → ∃ls,rs. t= midtape ? ls c rs. 
+#alpha #c * 
+  [whd in ⊢ (??%?→?); #H destruct
+  |#a #l whd in ⊢ (??%?→?); #H destruct
+  |#a #l whd in ⊢ (??%?→?); #H destruct
+  |#ls #c1 #rs whd in ⊢ (??%?→?); #H destruct
+   @(ex_intro … ls) @(ex_intro … rs) //
+  ]
+qed.
+   
+lemma sem_comp_step : 
+  accRealize ? comp_step (inr … (inl … (inr … start_nop))) 
+    R_comp_step_true R_comp_step_false.
+@(acc_sem_if_app … (sem_test_char ? (is_marked ?))
+        (sem_comp_step_subcase FSUnialpha 〈bit false,true〉 ??
+          (sem_comp_step_subcase FSUnialpha 〈bit true,true〉 ?? 
+            (sem_comp_step_subcase FSUnialpha 〈null,true〉 ?? 
+              (sem_clear_mark …))))
+        (sem_nop …) …)
+[#intape #outape #ta #Hta #Htb cases Hta * #cm * #Hcur 
+ cases (exists_current … Hcur) #ls * #rs #Hintape #cmark
+ cases (is_marked_to_exists … cmark) #c #Hcm
+ >Hintape >Hcm -Hintape -Hcm #Hta
+ @(ex_intro … ls) @(ex_intro … c) @(ex_intro …rs) % [//] lapply Hta -Hta
+ (* #ls #c #rs #Hintape whd in Hta;
+ >Hintape in Hta; * #_ -Hintape  forse non serve *)
+ cases (true_or_false (c==bit false)) #Hc
+  [>(\P Hc) #Hta %
+    [%[whd in ⊢ ((??%?)→?); #Hdes destruct
+      |#Hc @(proj1 ?? (proj1 ?? (Htb … Hta) (refl …)))
+      ]
+    |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (Htb … Hta) (refl …)))
+    ] 
+  |cases (true_or_false (c==bit true)) #Hc1
+    [>(\P Hc1) #Hta  
+      cut (〈bit true, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq %
+      [%[whd in ⊢ ((??%?)→?); #Hdes destruct
+        |#Hc @(proj1 … (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) (refl …)))
+        ]
+      |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta)(refl …)))
+      ]
+    |cases (true_or_false (c==null)) #Hc2
+      [>(\P Hc2) #Hta  
+        cut (〈null, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq
+        cut (〈null, true〉 ≠ 〈bit true, true〉) [% #Hdes destruct] #Hneq1 %
+        [%[whd in ⊢ ((??%?)→?); #Hdes destruct
+          |#Hc @(proj1 … (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
+          ]
+        |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
+        ]
+      |#Hta cut (bit_or_null c = false)
+        [lapply Hc; lapply Hc1; lapply Hc2 -Hc -Hc1 -Hc2
+         cases c normalize [* normalize /2/] /2/] #Hcut %
+        [%[cases (Htb … Hta) #_ -Htb #Htb
+           cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc; destruct] #_ -Htb #Htb 
+           cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc1; destruct] #_ -Htb #Htb 
+           lapply (Htb ?) [% #H destruct (H) normalize in Hc2; destruct] 
+           * #_ #Houttape #_ @(Houttape … Hta)
+          |>Hcut #H destruct 
+          ]
+        |#l1 #c0 #l2 >Hcut #H destruct 
+        ]
+      ]
+    ]
+  ]
+|#intape #outape #ta #Hta #Htb #ls #c #rs #Hintape 
+ >Hintape in Hta; whd in ⊢ (%→?); * #Hmark #Hta % [@Hmark //]
+ whd in Htb; >Htb //
+]
+qed.
+
+(* old universal version  
+
+definition R_comp_step_true ≝ λt1,t2.
+  ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls 〈c,true〉 rs → 
+    (* bit_or_null c = false *)
+    (bit_or_null c = false → t2 = midtape ? ls 〈c,false〉 rs) ∧
+    (* no marks in rs *)
+    (bit_or_null c = true →
+      (∀c.memb ? c rs = true → is_marked ? c = false) →
+       ∀a,l. (a::l) = reverse ? (〈c,true〉::rs) → 
+       t2 = rightof (FinProd FSUnialpha FinBool) a (l@ls)) ∧
+    (∀l1,c0,l2.
+      bit_or_null c = true →
+      (∀c.memb ? c l1 = true → is_marked ? c = false) → 
+      rs = l1@〈c0,true〉::l2 → 
+      (c = c0 → 
+       l2 = [ ] → (* test true but l2 is empty *) 
+       t2 = rightof ? 〈c0,false〉 ((reverse ? l1)@〈c,true〉::ls))  ∧
+      (c = c0 →
+       ∀a,a0,b,l1',l2'. (* test true and l2 is not empty *) 
+       〈a,false〉::l1' = l1@[〈c0,false〉] →
+       l2 = 〈a0,b〉::l2' →
+       t2 = midtape ? (〈c,false〉::ls) 〈a,true〉 (l1'@〈a0,true〉::l2')) ∧
+      (c ≠ c0 →(* test false *)
+       t2 = midtape (FinProd … FSUnialpha FinBool) 
+         ((reverse ? l1)@〈c,true〉::ls) 〈c0,false〉 l2)).
 
 definition R_comp_step_false ≝ 
   λt1,t2.
@@ -795,64 +1189,54 @@ lemma sem_comp_step :
             (sem_comp_step_subcase FSUnialpha 〈null,true〉 ?? 
               (sem_clear_mark …))))
         (sem_nop …) …)
-[#intape #outtape #midtape * * * #c #b * #Hcurrent 
-whd in ⊢ ((??%?)→?); #Hb #Hmidtape >Hmidtape -Hmidtape
- cases (current_to_midtape … Hcurrent) #ls * #rs >Hb #Hintape >Hintape -Hb
- whd in ⊢ (%→?); #Htapea lapply (Htapea … (refl …)) -Htapea
- cases (true_or_false (c == bit false))
-  [(* c = bit false *) #Hc * [2: * >(\P Hc) * #H @False_ind @H //]
-   * #_ #a 
- 
-
-[ #Hstate lapply (H1 Hstate) -H1 -Hstate -H2 *
-  #ta * whd in ⊢ (%→?); #Hleft #Hright #ls #c #rs #Hintape
-  >Hintape in Hleft; * *  
-  cases c in Hintape; #c' #b #Hintape #x * whd in ⊢ (??%?→?); #H destruct (H) 
-  whd in ⊢ (??%?→?); #Hb >Hb #Hta @(ex_intro ?? c') % //
-  cases (Hright … Hta)
-  [ * #Hc' #H1 % % [destruct (Hc') % ]
-    #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
-    cases (H1 … Hl1 Hrs)
-    [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
-    | * #Hneq #Houtc %2 %
-      [ @sym_not_eq //
-      | @Houtc ]
-    ]
-  | * #Hc #Helse1 cases (Helse1 … Hta)
-    [ * #Hc' #H1 % % [destruct (Hc') % ]
-      #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
-      cases (H1 … Hl1 Hrs)
-      [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
-      | * #Hneq #Houtc %2 %
-        [ @sym_not_eq //
-        | @Houtc ]
+[#intape #outape #ta #Hta #Htb #ls #c #rs #Hintape whd in Hta;
+ >Hintape in Hta; * #_ -Hintape (* forse non serve *)
+ cases (true_or_false (c==bit false)) #Hc
+  [>(\P Hc) #Hta %
+    [%[whd in ⊢ ((??%?)→?); #Hdes destruct
+      |#Hc @(proj1 ?? (proj1 ?? (Htb … Hta) (refl …)))
       ]
-    | * #Hc' #Helse2 cases (Helse2 … Hta)
-      [ * #Hc'' #H1 % % [destruct (Hc'') % ]
-        #a #l1 #c0 #a0 #l2 #Hrs >Hrs in Hintape; #Hintape #Hl1
-        cases (H1 … Hl1 Hrs)
-        [ * #Htmp >Htmp -Htmp #Houtc % % // @Houtc
-        | * #Hneq #Houtc %2 %
-          [ @sym_not_eq //
-          | @Houtc ]
+    |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (Htb … Hta) (refl …)))
+    ] 
+  |cases (true_or_false (c==bit true)) #Hc1
+    [>(\P Hc1) #Hta  
+      cut (〈bit true, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq %
+      [%[whd in ⊢ ((??%?)→?); #Hdes destruct
+        |#Hc @(proj1 … (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) (refl …)))
         ]
-      | * #Hc'' whd in ⊢ (%→?); #Helse3 %2 %
-        [ generalize in match Hc''; generalize in match Hc'; generalize in match Hc;
-          cases c'
-          [ * [ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
-              | #Hfalse @False_ind @(absurd ?? Hfalse) % ]
-          | #_ #_ #Hfalse @False_ind @(absurd ?? Hfalse) %
-          |*: #_ #_ #_ % ]
-        | @(Helse3 … Hta)
+      |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (Htb … Hta) Hneq … Hta)(refl …)))
+      ]
+    |cases (true_or_false (c==null)) #Hc2
+      [>(\P Hc2) #Hta  
+        cut (〈null, true〉 ≠ 〈bit false, true〉) [% #Hdes destruct] #Hneq
+        cut (〈null, true〉 ≠ 〈bit true, true〉) [% #Hdes destruct] #Hneq1 %
+        [%[whd in ⊢ ((??%?)→?); #Hdes destruct
+          |#Hc @(proj1 … (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
+          ]
+        |#l1 #c0 #l2 #Hc @(proj2 ?? (proj1 ?? (proj2 ?? (proj2 ?? (Htb … Hta) Hneq … Hta) Hneq1 … Hta) (refl …)))
+        ]
+      |#Hta cut (bit_or_null c = false)
+        [lapply Hc; lapply Hc1; lapply Hc2 -Hc -Hc1 -Hc2
+         cases c normalize [* normalize /2/] /2/] #Hcut %
+        [%[cases (Htb … Hta) #_ -Htb #Htb
+           cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc; destruct] #_ -Htb #Htb 
+           cases (Htb … Hta) [2: % #H destruct (H) normalize in Hc1; destruct] #_ -Htb #Htb 
+           lapply (Htb ?) [% #H destruct (H) normalize in Hc2; destruct] 
+           * #_ #Houttape #_ @(Houttape … Hta)
+          |>Hcut #H destruct 
+          ]
+        |#l1 #c0 #l2 >Hcut #H destruct 
         ]
       ]
     ]
   ]
-| #Hstate lapply (H2 Hstate) -H1 -Hstate -H2 *
-  #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
-  >Hintape in Hleft; * #Hc #Hta % [@Hc % | >Hright //]
+|#intape #outape #ta #Hta #Htb #ls #c #rs #Hintape 
+ >Hintape in Hta; whd in ⊢ (%→?); * #Hmark #Hta % [@Hmark //]
+ whd in Htb; >Htb //
 ]
-qed.
+qed. *)
+ 
+(*   
 definition R_comp_step_true ≝ 
   λt1,t2.
     ∀l0,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) l0 c rs → 
@@ -934,7 +1318,7 @@ cases (acc_sem_if … (sem_test_char ? (is_marked ?))
   #ta * whd in ⊢ (%→%→?); #Hleft #Hright #ls #c #rs #Hintape
   >Hintape in Hleft; * #Hc #Hta % [@Hc % | >Hright //]
 ]
-qed.
+qed.*)
 
 definition compare ≝ 
   whileTM ? comp_step (inr … (inl … (inr … start_nop))).
@@ -985,11 +1369,19 @@ RIFIUTO: c ≠ d
    t2 = midtape ? l0 〈grid,false〉 (l1@〈comma,true〉::l2)) ∨
   (b = bit x ∧ b = c ∧ bs = b0s
   *)
+  
+definition list_cases2: ∀A.∀P:list A →list A →Prop.∀l1,l2. |l1| = |l2| → 
+P [ ] [ ] → (∀a1,a2:A.∀tl1,tl2. |tl1| = |tl2| → P (a1::tl1) (a2::tl2)) → P l1 l2.
+#A #P #l1 #l2 #Hlen lapply Hlen @(list_ind2 … Hlen) //
+#tl1 #tl2 #hd1 #hd2 #Hind normalize #HlenS #H1 #H2 @H2 //
+qed.
+
 definition R_compare :=
   λt1,t2.
   ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs → 
   (∀c'.bit_or_null c' = false → c = 〈c',true〉 → t2 = midtape ? ls 〈c',false〉 rs) ∧
   (∀c'. c = 〈c',false〉 → t2 = t1) ∧
+(* forse manca il caso no marks in rs *)
   ∀b,b0,bs,b0s,l1,l2.
   |bs| = |b0s| → 
   (∀c.memb (FinProd … FSUnialpha FinBool) c bs = true → bit_or_null (\fst c) = true) → 
@@ -1027,26 +1419,83 @@ lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
     cases (Rfalse … Htapea) -Rfalse >Hc whd in ⊢ (??%?→?);#Hfalse destruct (Hfalse)
   ]
 | #tapea #tapeb #tapec #Hleft #Hright #IH #Htapec lapply (IH Htapec) -Htapec -IH #IH
-  whd in Hleft; #ls #c #rs #Htapea cases (Hleft … Htapea) -Hleft
-  #c' * #Hc >Hc cases (true_or_false (bit_or_null c')) #Hc'
-  [2: * 
-    [ * >Hc' #H @False_ind destruct (H)
-    | * #_ #Htapeb cases (IH … Htapeb) * #_ #H #_ %
-      [% 
-        [#c1 #Hc1 #Heqc destruct (Heqc) <Htapeb @(H c1) %
-        |#c1 #Hfalse destruct (Hfalse)
-        ]
-      |#b #b0 #bs #b0s #l1 #l2 #_ #_ #_ #_ #_ #_
-       #Heq destruct (Heq) >Hc' #Hfalse @False_ind destruct (Hfalse)
+  whd in Hleft; #ls #c #rs #Htapea cases Hleft -Hleft
+  #ls0 * #c' * #rs0 * >Htapea #Hdes destruct (Hdes) * * 
+  cases (true_or_false (bit_or_null c')) #Hc'
+  [2: #Htapeb lapply (Htapeb Hc') -Htapeb #Htapeb #_ #_ %
+    [%[#c1 #Hc1 #Heqc destruct (Heqc) 
+       cases (IH … Htapeb) * #_ #H #_ <Htapeb @(H … (refl…)) 
+      |#c1 #Heqc destruct (Heqc) 
       ]
+    |#b #b0 #bs #b0s #l1 #l2 #_ #_ #_ #_ #_ #_
+     #Heq destruct (Heq) >Hc' #Hfalse @False_ind destruct (Hfalse)
     ]
- |#Hleft %
+  |#_ (* no marks in rs ??? *) #_ #Hleft %
     [ %
       [ #c'' #Hc'' #Heq destruct (Heq) >Hc'' in Hc'; #H destruct (H) 
       | #c0 #Hfalse destruct (Hfalse)
       ]
     |#b #b0 #bs #b0s #l1 #l2 #Hlen #Hbs1 #Hb0s1 #Hbs2 #Hb0s2 #Hl1
-     #Heq destruct (Heq) #_ #Hrs cases Hleft -Hleft
+     #Heq destruct (Heq) #_ >append_cons; <associative_append #Hrs
+     cases (Hleft …  Hc' … Hrs) -Hleft
+      [2: #c1 #memc1 cases (memb_append … memc1) -memc1 #memc1
+        [cases (memb_append … memc1) -memc1 #memc1
+          [@Hbs2 @memc1 |>(memb_single … memc1) %]
+        |@Hl1 @memc1
+        ]
+      |* (* manca il caso in cui dopo una parte uguale il 
+            secondo nastro finisca ... ???? *)
+       #_ cases (true_or_false (b==b0)) #eqbb0
+        [2: #_ #Htapeb %2 lapply (Htapeb … (\Pf eqbb0)) -Htapeb #Htapeb
+         cases (IH … Htapeb) * #_ #Hout #_
+         @(ex_intro … []) @(ex_intro … b) @(ex_intro … b0) 
+         @(ex_intro … bs) @(ex_intro … b0s) %
+          [%[%[@(\Pf eqbb0) | %] | %] 
+          |>(Hout … (refl …)) -Hout >Htapeb @eq_f3 [2,3:%]
+           >reverse_append >reverse_append >associative_append 
+           >associative_append %  
+          ]
+        |lapply Hbs1 lapply Hbs2 lapply Hrs -Hbs1 -Hbs2 -Hrs 
+         @(list_cases2 … Hlen)
+          [#Hrs #_ #_ >associative_append >associative_append #Htapeb #_
+           lapply (Htapeb … (\P eqbb0) … (refl …) (refl …)) -Htapeb #Htapeb
+           cases (IH … Htapeb) -IH * #Hout #_ #_ %1 %
+            [>(\P eqbb0) % 
+            |>(Hout grid (refl …) (refl …)) @eq_f 
+             normalize >associative_append %
+            ]
+          |* #a1 #ba1 * #a2 #ba2 #tl1 #tl2 #HlenS #Hrs #Hbs1 #Hbs2 
+           cut (ba1 = false) [@(Hbs1 〈a1,ba1〉) @memb_hd] #Hba1 >Hba1
+           >associative_append >associative_append #Htapeb #_
+           lapply (Htapeb … (\P eqbb0) … (refl …) (refl …)) -Htapeb #Htapeb
+           cases (IH … Htapeb) -IH * #_ #_
+           #IH cases(IH a1 a2 ?? (l1@[〈b0,false〉]) l2 HlenS ????? (refl …) ??)
+            [
+           
+         
+(*
+         cut (∃a,l1'.〈a,false〉::l1'=((bs@[〈grid,false〉])@l1)@[〈b0,false〉])
+          [generalize in match Hbs2; cases bs
+            [#_ @(ex_intro … grid) @(ex_intro … (l1@[〈b0,false〉]))
+             >associative_append %
+            |* #bsc #bsb #bstl #Hbs2 @(ex_intro … bsc) 
+             @(ex_intro … (((bstl@[〈grid,false〉])@l1)@[〈b0,false〉]))
+             normalize @eq_f2 [2:%] @eq_f @sym_eq @(Hbs2 〈bsc,bsb〉) @memb_hd
+            ]
+          ]  
+         * #a * #l1' #H2
+         cut (∃a0,b1,l2'.b0s@〈comma,false〉::l2=〈a0,b1〉::l2')
+          [cases b0s
+            [@(ex_intro … comma) @(ex_intro … false) @(ex_intro … l2) %
+            |* #bsc #bsb #bstl @(ex_intro … bsc) @(ex_intro … bsb) 
+             @(ex_intro … (bstl@〈comma,false〉::l2)) %
+            ]
+          ] *)
+         * #a0 * #b1 * #l2' #H3   
+         lapply (Htapeb … (\P eqbb0) a a0 b1 l1' l2' H2 H3) -Htapeb #Htapeb
+         cases (IH … Htapeb) -IH *
+         
+      
       [2: * >Hc' #Hfalse @False_ind destruct ] * #_
        @(list_cases2 … Hlen)
        [ #Hbs #Hb0s generalize in match Hrs; >Hbs in ⊢ (%→?); >Hb0s in ⊢ (%→?);
@@ -1126,4 +1575,4 @@ lapply (sem_while ?????? sem_comp_step t i outc Hloop) [%]
 ]]]]]
 qed.       
 
-axiom sem_compare : Realize ? compare R_compare.
\ No newline at end of file
+axiom sem_compare : Realize ? compare R_compare.