More progress.

diff --git a/matita/matita/lib/MONADS/speranza.ma b/matita/matita/lib/MONADS/speranza.ma
index 95d4dda94e966970816621656e07cb82dcde6f84..99f60c26348bad39c190e9187aa62fdc1130370b 100644 (file)
--- a/matita/matita/lib/MONADS/speranza.ma
+++ b/matita/matita/lib/MONADS/speranza.ma
@@ -120,22 +120,26 @@ lemma admissible_leaf_cons:
  #n #p1 elim p1 //
 qed.
 
+(*
+lemma admissible_node_cons:
+ ∀x1,x2,p1,p2.
+  admissible (node x1 x2) (rev_append bool p1 [true]@p2)=true →
+   admissible x2 p1=true.
+ #x1 #x2 #p1 elim p1 normalize // #dir #tl #IH #p2 cases x2 normalize
+ [ #n *)
+
 theorem update_correct2:
  ∀A,v,p1,p2,k,t.
-  admissible t (reverse … p2 @ p1) = true →
+  admissible t (p2 @ reverse … p1) = true →
    update A v k p1 〈t,p2〉 = update … v k [] 〈t,reverse … p1 @ p2〉.
 #A #v #p1 elim p1 normalize //
 #dir #ptl #IH #p2 #k #t cases dir normalize nodelta cases t normalize nodelta
 [1,3: #n >admissible_leaf_cons #abs destruct
-|*: #x1 #x2 change with (reverse ? (?::ptl)) in match (rev_append ???); >reverse_cons
-      >associative_append #H normalize >IH //
-
- normalize change with (reverse ? (true::ptl)) in match (rev_append bool ptl [true]);
-[>(reverse_cons … true ptl) | >(reverse_cons … false ptl)]
-[ >(associative_append ??[?]) 
-  
-
+|*: #x1 #x2 #H >IH // >rev_append_cons >(?:admissible ? p2 = true) try %
+    <rev_append_cons in H; change with (reverse ??) in match (rev_append ???);
+    
 
+(* OLD
 theorem update_correct:
  ∀v,p1,p2,t.
   let 〈t',res〉 ≝ setleaf_fun v t (reverse … p1 @ p2) in 
@@ -156,4 +160,5 @@ theorem update_correct:
   #path #IH #x elim x normalize
     [ #v cases res normalize lapply (IH (leaf v)) -IH elim path
       normalize // * normalize
-      [2: #path' #IH #IH2 @IH
\ No newline at end of file
+      [2: #path' #IH #IH2 @IH
+*)
\ No newline at end of file