From 292ea72d5160e31b8516fe7dfd92bb9e487db9fc Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Mon, 14 Jan 2013 15:47:08 +0000
Subject: [PATCH] wsem_match finished

---
 .../lib/turing/multi_universal/match.ma       | 37 ++++++++-----------
 1 file changed, 15 insertions(+), 22 deletions(-)

diff --git a/matita/matita/lib/turing/multi_universal/match.ma b/matita/matita/lib/turing/multi_universal/match.ma
index 3417463a4..857477e43 100644
--- a/matita/matita/lib/turing/multi_universal/match.ma
+++ b/matita/matita/lib/turing/multi_universal/match.ma
@@ -448,34 +448,27 @@ lapply (sem_while … (sem_match_step src dst sig n Hneq Hsrc Hdst) … Hloop) /
          -H1 #H1 cases (H l2 l3) #H2 @H2 @H1
         ]
       ]
-    | (* in match_step_true manca il caso di fallimento immediato
-         (con i due current diversi) *)
-      @daemon
-      (*
-       #_ lapply (\Pf eqx) -eqx #eqx >Hmidta_dst
-       cases (Htrue ? (refl ??) eqx) -Htrue #Htb #Hendcx #_
-       cases rs0 in Htb;
-       [ #_ %2 #l #l1 cases l
+    | #_ cases (IH x xs ?) -IH
+      [| >Htc >nth_change_vec_neq [|@sym_not_eq //] @Hmidta_src ]
+      >Htc >nth_change_vec // cases rs0
+      [ #_ #_ %2 #l #l1 cases l
        [ normalize cases xs
          [ cases l1
-           [ normalize % #H destruct (H) cases eqx /2/
+           [ normalize % #H destruct (H) cases (\Pf eqx) /2/
            | #tmp1 #l2 normalize % #H destruct (H) ]
          | #tmp1 #l2 normalize % #H destruct (H) ]
        | #tmp1 #l2 normalize % #H destruct (H)cases l2 in e0;
          [ normalize #H1 destruct (H1)
-         | #tmp2 #l3 normalize #H1 destruct (H1) ]
-       ]
-     | #r1 #rs1 normalize in ⊢ (???(????%?)→?); #Htb >Htb in IH; #IH
-       cases (IH ls x xs end rs ? Hnotend Hend Hnotstart) 
-       [| >Htb >nth_change_vec_neq [|@sym_not_eq //] @Hmid_src ] -IH
-       #_ #IH cases (IH Hstart (c::ls0) r1 rs1 ?)
-       [|| >nth_change_vec // ] -IH
-       [ * #l * #l1 * #Hll1 #Hout % %{(c::l)} %{l1} % >Hll1 //
-         >reverse_cons >associative_append #cj0 #ls #Hl1 >(Hout ?? Hl1)
-         >change_vec_commute in ⊢ (??(???%??)?); // @sym_not_eq //
-       | #IH %2 @(not_sub_list_merge_2 ?? (x::xs)) normalize [|@IH]
-         #l1 % #H destruct (H) cases eqx /2/
-       ] *)
+         | #tmp2 #l3 normalize #H1 destruct (H1) ] ]
+      | #r1 #rs1 #_ #IH cases (IH … (refl ??)) -IH
+        [ * #l * #l1 * #Hll1 #Houtc % %{(c::l)} %{l1} % [ >Hll1 % ]
+          >Houtc >change_vec_commute // >change_vec_change_vec 
+          >change_vec_commute [|@sym_not_eq //]
+          >reverse_cons >associative_append %
+        | #Hll1 %2 @(not_sub_list_merge_2 ?? (x::xs)) normalize [|@Hll1]
+         #l1 % #H destruct (H) cases (\Pf eqx) /2/
+        ]
+      ]
     ]
   ]
 ]
-- 
2.39.2