Closed some daemons

diff --git a/matita/matita/lib/turing/multi_universal/compare.ma b/matita/matita/lib/turing/multi_universal/compare.ma
index 423a5af33eac4299396c494db20010bb579efa67..501b7bc77369b75b82cf4e2742bb2e494ff12b71 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/compare.ma
+++ b/matita/matita/lib/turing/multi_universal/compare.ma
@@ -155,24 +155,21 @@ lapply (refl ? (current ? (nth i ? int (niltape ?))))
 cases (current ? (nth i ? int (niltape ?))) in ⊢ (???%→?);
 [ #Hcuri %{2} %
   [| % [ %
-    [ whd in ⊢ (??%?); >comp_q0_q2_null /2/ % <Hcuri in ⊢ (???%); 
-      @sym_eq @nth_vec_map
+    [ whd in ⊢ (??%?); >comp_q0_q2_null /2/ 
     | normalize in ⊢ (%→?); #H destruct (H) ]
   | #_ % // % %2 // ] ]
 | #a #Ha lapply (refl ? (current ? (nth j ? int (niltape ?))))
   cases (current ? (nth j ? int (niltape ?))) in ⊢ (???%→?);
   [ #Hcurj %{2} %
     [| % [ %
-       [ whd in ⊢ (??%?); >comp_q0_q2_null /2/ %2 <Hcurj in ⊢ (???%); 
-         @sym_eq @nth_vec_map
+       [ whd in ⊢ (??%?); >comp_q0_q2_null /2/ %2
        | normalize in ⊢ (%→?); #H destruct (H) ]
        | #_ % // >Ha >Hcurj % % % #H destruct (H) ] ]
   | #b #Hb %{2} cases (true_or_false (a == b)) #Hab
     [ %
       [| % [ % 
         [whd in ⊢  (??%?);  >(comp_q0_q1 … a Hneq Hi Hj) //
-          [>(\P Hab) <Hb @sym_eq @nth_vec_map
-          |<Ha @sym_eq @nth_vec_map ]
+         >(\P Hab) <Hb @sym_eq @nth_vec_map
         | #_ whd >(\P Hab) %{b} % // % // <(\P Hab) // ]
         | * #H @False_ind @H %
       ] ]
@@ -293,5 +290,6 @@ qed.
 lemma sem_compare : ∀i,j,sig,n.
   i ≠ j → i < S n → j < S n → 
   compare i j sig n ⊨ R_compare i j sig n.
-#i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize /2/
+#i #j #sig #n #Hneq #Hi #Hj @WRealize_to_Realize 
+  [/2/| @wsem_compare // ]
 qed.

diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma
index 38dba8d729e416420c4ed6450884a7448e4689a1..da7481f5e1a6494469e3e355d5f8192596bce719 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/match.ma
+++ b/matita/matita/lib/turing/multi_universal/match.ma
@@ -124,6 +124,7 @@ definition R_rewind ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
    ∀ls0,y,rs0.nth dst ? int (niltape ?) = midtape sig ls0 y rs0 → 
    outt = int).
 
+(*
 theorem accRealize_to_Realize :
   ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc.
   M ⊨ [ acc: Rtrue, Rfalse ] →  M ⊨ Rtrue ∪ Rfalse.
@@ -133,6 +134,7 @@ cases (HR t) #k * #outc * * #Hloop
 cases (true_or_false (cstate sig (states sig n M) n outc == acc)) #Hcase
 [ % @Htrue @(\P Hcase) | %2 @Hfalse @(\Pf Hcase) ]
 qed.
+*)
 
 lemma sem_rewind : ∀src,dst,sig,n.
   src ≠ dst → src < S n → dst < S n → 
@@ -239,16 +241,13 @@ lemma sem_match_step :
 [ #ta #tb #tc * lapply (refl ? (current ? (nth src ? ta (niltape ?))))
   cases (current ? (nth src ? ta (niltape ?))) in ⊢ (???%→%);
   [ #Hcurta_src #Hcomp #_ * #td * >Hcomp [| % %2 %]
-    whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
-    >(?:nth src ? (current_chars ?? ta) (None ?) = None ?)
-    [ normalize in ⊢ (%→?); #H destruct (H)
-    | @daemon ]
+    whd in ⊢ (%→?); * whd in ⊢ (??%?→?); 
+    >nth_current_chars >Hcurta_src normalize in ⊢ (%→?); #H destruct (H)
   | #s #Hs lapply (refl ? (current ? (nth dst ? ta (niltape ?))))
     cases (current ? (nth dst ? ta (niltape ?))) in ⊢ (???%→%);
     [ #Hcurta_dst #Hcomp #_ * #td * >Hcomp [| %2 %]
-      whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
-      >(?:nth src ? (current_chars ?? ta) (None ?) = Some ? s) [|@daemon]
-      >(?:nth dst ? (current_chars ?? ta) (None ?) = None ?) [|@daemon]
+      whd in ⊢ (%→?); * whd in ⊢ (??%?→?); 
+      >nth_current_chars >nth_current_chars >Hs >Hcurta_dst 
       normalize in ⊢ (%→?); #H destruct (H)
     | #s0 #Hs0
       cases (current_to_midtape … Hs) #ls * #rs #Hmidta_src >Hmidta_src
@@ -257,11 +256,15 @@ lemma sem_match_step :
       [ lapply (\P Hss0) -Hss0 #Hss0 destruct (Hss0) 
         #_ #Hcomp cases (Hcomp ????? (refl ??) (refl ??)) -Hcomp [ *
         [ * #rs' * #_ #Hcurtc_dst * #td * whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
-          >(?:nth dst ? (current_chars ?? tc) (None ?) = None ?) [|@daemon]
-          cases (nth src ? (current_chars ?? tc) (None ?))
-          [| #x ] normalize in ⊢ (%→?); #H destruct (H)
+          >nth_current_chars >nth_current_chars >Hcurtc_dst 
+          cases (current ? (nth src …)) [| #x ] 
+          normalize in ⊢ (%→?); #H destruct (H) 
         | * #rs0' * #_ #Hcurtc_src * #td * whd in ⊢ (%→?); * whd in ⊢ (??%?→?);
-          >(?:nth src ? (current_chars ?? tc) (None ?) = None ?) [|@daemon]
+          >(?:nth src ? (current_chars ?? tc) (None ?) = None ?) 
+          [|>nth_current_chars >Hcurtc_src >nth_change_vec_neq 
+            [>nth_change_vec [cases (append ???) // | @Hsrc] 
+            |@(not_to_not … Hneq) //
+            ]]
           normalize in ⊢ (%→?); #H destruct (H) ]
         | * #xs * #ci * #cj * #rs'' * #rs0' * * * #Hcicj #Hrs #Hrs0
           #Htc * #td * * #Hmatch #Htd destruct (Htd) * #te * *
@@ -310,18 +313,20 @@ lemma sem_match_step :
     | >(?:tc=ta) in Htest; 
       [|@Hcomp1 % % >Hta_src >Hta_dst @(not_to_not ??? (\Pf Hxx0)) normalize
         #Hxx0' destruct (Hxx0') % ]
-      whd in ⊢ (??%?→?); >(?:nth src ? (current_chars ?? ta) (None ?) = Some ? x)
-      [| @daemon ]
-      >(?:nth dst ? (current_chars ?? ta) (None ?) = Some ? x0) [|@daemon]
+      whd in ⊢ (??%?→?); 
+      >nth_current_chars >Hta_src >nth_current_chars >Hta_dst 
       whd in ⊢ (??%?→?); #Hfalse destruct (Hfalse) ] -Hcomp1
       cases (Hcomp2 … Hta_src Hta_dst) [ *
       [ * #rs' * #Hxs #Hcurtc % %2 %{ls0} %{rs0} %{rs'} % // % //
       | * #rs0' * #Hxs #Htc %2 >Htc %{ls0} %{rs0'} % // ]
       | * #xs0 * #ci * #cj * #rs' * #rs0' * * *
         #Hci #Hxs #Hrs0 #Htc @False_ind
-        whd in Htest:(??%?);
-        >(?:nth src ? (current_chars ?? tc) (None ?) = Some ? ci) in Htest; [|@daemon]
-        >(?:nth dst ? (current_chars ?? tc) (None ?) = Some ? cj) [|@daemon]
+        whd in Htest:(??%?); 
+        >(?:nth src ? (current_chars ?? tc) (None ?) = Some ? ci) in Htest; 
+        [|>nth_current_chars >Htc >nth_change_vec_neq [|@(not_to_not … Hneq) //]
+          >nth_change_vec //]
+        >(?:nth dst ? (current_chars ?? tc) (None ?) = Some ? cj) 
+        [|>nth_current_chars >Htc >nth_change_vec //]
         normalize #H destruct (H) ] ] ]
 qed.
 

diff --git a/matita/matita/lib/turing/multi_universal/moves.ma b/matita/matita/lib/turing/multi_universal/moves.ma
index df620b3520d63f5076a24be061661e7717201fe6..f725a1940202b8bf641152ce2eeb21d433e5f98d 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/moves.ma
+++ b/matita/matita/lib/turing/multi_universal/moves.ma
@@ -159,14 +159,12 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
 [ #Hcursrc %{2} %
   [| % [ %
     [ whd in ⊢ (??%?); >parmove_q0_q2_null_src /2/
-      <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
     | normalize in ⊢ (%→?); #H destruct (H) ]
     | #_ % // % %2 // ] ]
 | #a #Ha cases (true_or_false (is_sep a)) #Hsep
   [ %{2} %
     [| % [ %
       [ whd in ⊢ (??%?); >(parmove_q0_q2_sep … Hsep) /2/
-        <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
       | normalize in ⊢ (%→?); #H destruct (H) ]
       | #_ % // % % %{a} % // ] ]
   | lapply (refl ? (current ? (nth dst ? int (niltape ?))))
@@ -174,15 +172,11 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
     [ #Hcurdst %{2} %
       [| % [ %
         [ whd in ⊢ (??%?); >(parmove_q0_q2_null_dst … Hsep) /2/ 
-          [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
-          | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ]
         | normalize in ⊢ (%→?); #H destruct (H) ]
         | #_ % // %2 // ] ]
     | #b #Hb %{2} %
       [| % [ % 
         [whd in ⊢  (??%?);  >(parmove_q0_q1 … Hneq Hsrc Hdst ? b ?? Hsep) //
-          [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
-          | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ]
         | #_ %{a} %{b} % // % // % // ]
         | * #H @False_ind @H % ]
 ]]]]

diff --git a/matita/matita/lib/turing/multi_universal/moves_2.ma b/matita/matita/lib/turing/multi_universal/moves_2.ma
index 072d3a15a4b2f3fbd89d58f3a94d163f4a2b296f..14f072b4ee966d0ec56602cb7cbac1aaef4e74b3 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/moves_2.ma
+++ b/matita/matita/lib/turing/multi_universal/moves_2.ma
@@ -137,7 +137,6 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
 [ #Hcursrc %{2} %
   [| % [ %
     [ whd in ⊢ (??%?); >parmove_q0_q2_null_src /2/
-      <(nth_vec_map ?? (current …) src ? int (niltape ?)) //
     | normalize in ⊢ (%→?); #H destruct (H) ]
     | #_ % // % // ] ]
 | #a #Ha lapply (refl ? (current ? (nth dst ? int (niltape ?))))
@@ -145,8 +144,6 @@ cases (current ? (nth src ? int (niltape ?))) in ⊢ (???%→?);
   [ #Hcurdst %{2} %
     [| % [ %
       [ whd in ⊢ (??%?); >(parmove_q0_q2_null_dst …) /2/ 
-        [ <(nth_vec_map ?? (current …) dst ? int (niltape ?)) //
-        | <(nth_vec_map ?? (current …) src ? int (niltape ?)) // ]
       | normalize in ⊢ (%→?); #H destruct (H) ]
       | #_ % // %2 // ] ]
   | #b #Hb %{2} %