X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Fmoves_2.ma;h=e56a0f183e434fe96c09a9402e3f982ad631b32b;hb=225887a9f23aac79d4cca907da026917b7df04dc;hp=d86b89a6a00a769084280d483435b755b3b672d8;hpb=789726e7f992ff6a37b91799fb081f8013703b49;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/moves_2.ma b/matita/matita/lib/turing/multi_universal/moves_2.ma
index d86b89a6a..e56a0f183 100644
--- a/matita/matita/lib/turing/multi_universal/moves_2.ma
+++ b/matita/matita/lib/turing/multi_universal/moves_2.ma
@@ -170,6 +170,13 @@ definition R_parmoveL ≝
     outt = change_vec ?? 
            (change_vec ?? int (mk_tape sig [] (None ?) (reverse ? xs@x::rs)) src)
            (mk_tape sig (tail ? ls0) (option_hd ? ls0) (reverse ? target@x0::rs0)) dst) ∧
+  (∀x,xs,rs.
+    nth dst ? int (niltape ?) = midtape sig xs x rs → 
+    ∀ls0,x0,target,rs0.|xs| = |target| → 
+    nth src ? int (niltape ?) = midtape sig (target@ls0) x0 rs0 → 
+    outt = change_vec ?? 
+           (change_vec ?? int (mk_tape sig [] (None ?) (reverse ? xs@x::rs)) dst)
+           (mk_tape sig (tail ? ls0) (option_hd ? ls0) (reverse ? target@x0::rs0)) src) ∧
   ((current ? (nth src ? int (niltape ?)) = None ? ∨
     current ? (nth dst ? int (niltape ?)) = None ?) →
     outt = int).
@@ -179,14 +186,22 @@ lemma wsem_parmoveL : ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n 
 #src #dst #sig #n #Hneq #Hsrc #Hdst #ta #k #outc #Hloop
 lapply (sem_while … (sem_parmove_step src dst sig n L Hneq Hsrc Hdst) … Hloop) //
 -Hloop * #tb * #Hstar @(star_ind_l ??????? Hstar) -Hstar
-[ whd in ⊢ (%→?); * #H #Houtc % [2: #_ @Houtc ] cases H
-  [ #Hcurtb #x #xs #rs #Hsrctb >Hsrctb in Hcurtb; normalize in ⊢ (%→?);
-    #Hfalse destruct (Hfalse)
-  | #Hcur_dst #x #xs #rs #Hsrctb #ls0 #x0 #target 
-    #rs0 #Hlen #Hdsttb >Hdsttb in Hcur_dst; normalize in ⊢ (%→?); #H destruct (H)
+[ whd in ⊢ (%→?); * #H #Houtc % [2: #_ @Houtc ] cases H #Hcurtb
+  [ % 
+    [ #x #xs #rs #Hsrctb >Hsrctb in Hcurtb; normalize in ⊢ (%→?);
+      #Hfalse destruct (Hfalse)
+    | #x #xs #rs #Hdsttb #ls0 #x0 #target #rs0 #Hlen #Hsrctb >Hsrctb in Hcurtb;
+      normalize in ⊢ (%→?); #H destruct (H)
+    ]
+  | %
+    [ #x #xs #rs #Hsrctb #ls0 #x0 #target 
+      #rs0 #Hlen #Hdsttb >Hdsttb in Hcurtb; normalize in ⊢ (%→?); #H destruct (H)
+    | #x #xs #rs #Hdsttb >Hdsttb in Hcurtb; normalize in ⊢ (%→?);
+      #Hfalse destruct (Hfalse)
+    ]
   ]  
 | #td #te * #c0 * #c1 * * #Hc0 #Hc1 #Hd #Hstar #IH #He 
-  lapply (IH He) -IH * #IH1 #IH2 %
+  lapply (IH He) -IH * * #IH1a #IH1b #IH2 % [ %
   [ #x #xs #rs #Hsrc_td #ls0 #x0 #target
     #rs0 #Hlen #Hdst_td
     >Hsrc_td in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
@@ -211,20 +226,55 @@ lapply (sem_while … (sem_parmove_step src dst sig n L Hneq Hsrc Hdst) … Hloo
         ]
       ]
     | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
-      >(IH1 hd1 tl1 (c0::rs) ? ls0 hd2 tl2 (x0::rs0))
+      >(IH1a hd1 tl1 (c0::rs) ? ls0 hd2 tl2 (x0::rs0))
       [ >Hd >(change_vec_commute … ?? td ?? src dst) //
-       >change_vec_change_vec
-       >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
-       >change_vec_change_vec
-       >reverse_cons >associative_append
-       >reverse_cons >associative_append % 
-     | >Hd >nth_change_vec //
-     | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
-     | >Hd >nth_change_vec_neq [|@sym_not_eq //]
-       >nth_change_vec // ]
-   ]
- | >Hc0 >Hc1 * [ #Hc0 destruct (Hc0) | #Hc1 destruct (Hc1) ]
- ] ]
+        >change_vec_change_vec
+        >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
+        >change_vec_change_vec
+        >reverse_cons >associative_append
+        >reverse_cons >associative_append % 
+      | >Hd >nth_change_vec //
+      | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
+      | >Hd >nth_change_vec_neq [|@sym_not_eq //]
+        >nth_change_vec // ]
+    ]
+  | #x #xs #rs #Hdst_td #ls0 #x0 #target
+    #rs0 #Hlen #Hsrc_td
+    >Hdst_td in Hc0; normalize in ⊢ (%→?); #Hc0 destruct (Hc0)
+    >Hsrc_td in Hd; >Hdst_td @(list_cases2 … Hlen)
+    [ #Hxsnil #Htargetnil >Hxsnil >Htargetnil #Hd >IH2 
+      [2: %2 >Hd >nth_change_vec //]
+      >Hd -Hd @(eq_vec … (niltape ?))
+      #i #Hi cases (decidable_eq_nat i dst) #Hidst
+      [ >Hidst >(nth_change_vec_neq … dst src) //
+        >nth_change_vec // >nth_change_vec //
+      | cases (decidable_eq_nat i src) #Hisrc
+        [ >Hisrc >nth_change_vec // >(nth_change_vec_neq …) [|@sym_not_eq //]
+          >Hsrc_td in Hc1; >Htargetnil
+          normalize in ⊢ (%→?); #Hc1 destruct (Hc1) >nth_change_vec //
+          cases ls0 //
+        | >nth_change_vec_neq [|@(sym_not_eq … Hidst)]
+          >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
+          >nth_change_vec_neq [|@(sym_not_eq … Hisrc)]
+          >nth_change_vec_neq [|@(sym_not_eq … Hidst)] % 
+        ]
+      ]
+    | #hd1 #hd2 #tl1 #tl2 #Hxs #Htarget >Hxs >Htarget #Hd
+      >(IH1b hd1 tl1 (x::rs) ? ls0 hd2 tl2 (x0::rs0))
+      [ >Hd >(change_vec_commute … ?? td ?? dst src) [|@sym_not_eq //]
+        >change_vec_change_vec
+        >(change_vec_commute … ?? td ?? src dst) //
+        >change_vec_change_vec
+        >reverse_cons >associative_append
+        >reverse_cons >associative_append
+        >change_vec_commute [|@sym_not_eq //] %
+      | >Hd >nth_change_vec_neq [|@sym_not_eq //] >nth_change_vec //
+      | >Hxs in Hlen; >Htarget normalize #Hlen destruct (Hlen) //
+      | >Hd >nth_change_vec // ]
+    ]
+  ]
+| >Hc0 >Hc1 * [ #Hc0 destruct (Hc0) | #Hc1 destruct (Hc1) ]
+] ]
 qed.
  
 lemma terminate_parmoveL :  ∀src,dst,sig,n,t.
@@ -321,6 +371,23 @@ lapply (sem_while … (sem_mte_step sig R) … Hloop) //
     | #ls1 #c1 #rs1 #H destruct (H) >reverse_cons >associative_append @IH % ] ] ]
 qed.
 
+lemma terminate_move_to_end_r :  ∀sig,t.move_to_end sig R ↓ t.
+#sig #t @(terminate_while … (sem_mte_step sig R …)) //
+cases t
+[ % #t1 * #ls * #c * #rs * #H destruct
+|2,3: #a0 #al0 % #t1 * #ls * #c * #rs * #H destruct
+| #ls #c #rs lapply c -c lapply ls -ls elim rs
+  [ #ls #c % #t1 * #ls0 * #c0 * #rs0 * #Hmid #Ht1 destruct %
+    #t2 * #ls1 * #c1 * #rs1 * normalize in ⊢ (%→?); #H destruct
+  | #r0 #rs0 #IH #ls #c % #t1 * #ls1 * #c1 * #rs1 * #Hmid #Ht1 destruct @IH
+  ]
+]
+qed.
+
+lemma sem_move_to_end_r : ∀sig. move_to_end sig R ⊨ R_move_to_end_r sig.
+#sig @WRealize_to_Realize //
+qed.
+
 definition R_move_to_end_l ≝ 
   λsig,int,outt.
   (current ? int = None ? → outt = int) ∧
@@ -340,4 +407,21 @@ lapply (sem_while … (sem_mte_step sig L) … Hloop) //
     lapply (IH Hfalse) -IH * #_ #IH %
     [ normalize in ⊢ (%→?); #H destruct (H)
     | #ls1 #c1 #rs1 #H destruct (H) >reverse_cons >associative_append @IH % ] ] ]
-qed.
\ No newline at end of file
+qed.
+
+lemma terminate_move_to_end_l :  ∀sig,t.move_to_end sig L ↓ t.
+#sig #t @(terminate_while … (sem_mte_step sig L …)) //
+cases t
+[ % #t1 * #ls * #c * #rs * #H destruct
+|2,3: #a0 #al0 % #t1 * #ls * #c * #rs * #H destruct
+| #ls elim ls
+  [ #c #rs % #t1 * #ls0 * #c0 * #rs0 * #Hmid #Ht1 destruct %
+    #t2 * #ls1 * #c1 * #rs1 * normalize in ⊢ (%→?); #H destruct
+  | #l0 #ls0 #IH #c #rs % #t1 * #ls1 * #c1 * #rs1 * #Hmid #Ht1 destruct @IH
+  ]
+]
+qed.
+
+lemma sem_move_to_end_l : ∀sig. move_to_end sig L ⊨ R_move_to_end_l sig.
+#sig @WRealize_to_Realize //
+qed.