unistep_aux

[helm.git] / matita / matita / lib / turing / multi_universal / compare.ma

diff --git a/matita/matita/lib/turing/multi_universal/compare.ma b/matita/matita/lib/turing/multi_universal/compare.ma
index 501b7bc77369b75b82cf4e2742bb2e494ff12b71..8ad92d1e8b8f299e8908c63c36424cc3e397c24f 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/compare.ma
+++ b/matita/matita/lib/turing/multi_universal/compare.ma
@@ -189,6 +189,17 @@ qed.
 definition compare ≝ λi,j,sig,n.
   whileTM … (compare_step i j sig n) comp1.
 
+(*    (∃rs'.rs = rs0@rs' ∧ current ? (nth j ? outt (niltape ?)) = None ?) ∨
+    (∃rs0'.rs0 = rs@rs0' ∧ 
+     outt = change_vec ?? 
+            (change_vec ?? int  
+              (mk_tape sig (reverse sig rs@x::ls) (None sig) []) i)
+            (mk_tape sig (reverse sig rs@x::ls0) (option_hd sig rs0')
+            (tail sig rs0')) j) ∨
+    (∃xs,ci,cj,rs',rs0'.ci ≠ cj ∧ rs = xs@ci::rs' ∧ rs0 = xs@cj::rs0' ∧
+     outt = change_vec ?? 
+            (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs') i)
+            (midtape sig (reverse ? xs@x::ls0) cj rs0') j)).*)
 definition R_compare ≝ 
   λi,j,sig,n.λint,outt: Vector (tape sig) (S n).
   ((current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨
@@ -198,7 +209,11 @@ definition R_compare ≝
 (*    nth i ? int (niltape ?) = midtape sig ls x (xs@ci::rs) → *)
     nth i ? int (niltape ?) = midtape sig ls x rs →
     nth j ? int (niltape ?) = midtape sig ls0 x rs0 →
-    (∃rs'.rs = rs0@rs' ∧ current ? (nth j ? outt (niltape ?)) = None ?) ∨
+    (∃rs'.rs = rs0@rs' ∧ 
+     outt = change_vec ?? 
+            (change_vec ?? int  
+              (mk_tape sig (reverse sig rs0@x::ls) (option_hd sig rs') (tail ? rs')) i)
+            (mk_tape sig (reverse sig rs0@x::ls0) (None ?) [ ]) j) ∨
     (∃rs0'.rs0 = rs@rs0' ∧ 
      outt = change_vec ?? 
             (change_vec ?? int  
@@ -208,7 +223,7 @@ definition R_compare ≝
     (∃xs,ci,cj,rs',rs0'.ci ≠ cj ∧ rs = xs@ci::rs' ∧ rs0 = xs@cj::rs0' ∧
      outt = change_vec ?? 
             (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs') i)
-            (midtape sig (reverse ? xs@x::ls0) cj rs0') j)).
+            (midtape sig (reverse ? xs@x::ls0) cj rs0') j)).            
           
 lemma wsem_compare : ∀i,j,sig,n.i ≠ j → i < S n → j < S n → 
   compare i j sig n ⊫ R_compare i j sig n.
@@ -242,14 +257,17 @@ lapply (sem_while … (sem_comp_step i j sig n Hneq Hi Hj) … Hloop) //
       [ -IH2 #Hnthj % % %{(r1::rs1)} % [%]
         >Hnthj in Hd; #Hd >Hd in IH1; #IH1 >IH1
         [| %2 >nth_change_vec // ]
-        >nth_change_vec //
+        >Hnthi >Hnthj %
       | #r2 #rs2 #Hnthj lapply IH2; >Hd in IH1; >Hnthi >Hnthj
         >nth_change_vec //
         >nth_change_vec_neq [| @sym_not_eq // ] >nth_change_vec //
         cases (true_or_false (r1 == r2)) #Hr1r2
         [ >(\P Hr1r2) #_ #IH2 cases (IH2 … (refl ??) (refl ??)) [ *
           [ * #rs' * #Hrs1 #Hcurout_j % % %{rs'}
-            >Hrs1 >Hcurout_j normalize % //
+            >Hrs1 % 
+            [ % 
+            | >Hcurout_j >change_vec_commute // >change_vec_change_vec
+              >change_vec_commute // @sym_not_eq // ]
           | * #rs0' * #Hrs2 #Hcurout_i % %2 %{rs0'}
             >Hrs2 >Hcurout_i % //
             >change_vec_commute // >change_vec_change_vec