X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Funiversal%2Ftuples.ma;h=0faa4eece58844e8925519b42899d97c2b799be3;hb=0460fd3dc2909efe0baa6592281d0cf0527165ff;hp=9c6c7a09fc0fdb62aaae0923018e27fec60a50a4;hpb=0c1a9706c7227db49453b29f749bf6ff2077cf68;p=helm.git

diff --git a/matita/matita/lib/turing/universal/tuples.ma b/matita/matita/lib/turing/universal/tuples.ma
index 9c6c7a09f..0faa4eece 100644
--- a/matita/matita/lib/turing/universal/tuples.ma
+++ b/matita/matita/lib/turing/universal/tuples.ma
@@ -19,7 +19,8 @@ include "turing/universal/marks.ma".
 definition STape ≝ FinProd … FSUnialpha FinBool.
 
 definition only_bits ≝ λl.
-  ∀c.memb STape c l = true → is_bit (\fst c) = true.
+  ∀c.memb STape c l
+   = true → is_bit (\fst c) = true.
 
 definition only_bits_or_nulls ≝ λl.
   ∀c.memb STape c l = true → bit_or_null (\fst c) = true.
@@ -81,16 +82,6 @@ inductive match_in_table (n:nat) (qin:list STape) (cin: STape)
    match_in_table n qin cin qout cout mv  
      (mk_tuple qin0 cin0 qout0 cout0 mv0@tb).
      
-axiom append_l1_injective : 
-  ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l1 = l2.
-axiom append_l2_injective : 
-  ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l3 = l4.
-axiom append_l1_injective_r :
-  ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l1 = l2.
-axiom append_l2_injective_r : 
-  ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l3 = l4.
-axiom cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2.
-axiom cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
 axiom tuple_len : ∀n,t.tuple_TM n t → |t| = 2*n+6.
 axiom append_eq_tech1 :
   ∀A,l1,l2,l3,l4.l1@l2 = l3@l4 → |l1| < |l3| → ∃la:list A.l1@la = l3.
@@ -155,7 +146,24 @@ lemma generic_match_to_match_in_table_tech :
   [ #la * #lb * #HT1c #HT0 %{lb} >HT1c @(eq_f2 ??? (append ?) (c::la)) //
     >HT0 in Ht'; >HT1c >associative_append in ⊢ (???%→?); #Ht'
     <(append_l1_injective_r … Ht') // <(cons_injective_l ????? Ht) %
-  |@daemon ]
+  |@(noteq_to_eqnot ? true) @(not_to_not … not_eq_true_false) #Hbar @sym_eq 
+   cases (memb_append … Hbar) -Hbar #Hbar
+    [@(Hqin2 … Hbar) 
+    |cases (orb_true_l … Hbar) -Hbar
+      [#Hbar lapply (\P Hbar) -Hbar #Hbar destruct (Hbar) @Hcin
+      |whd in ⊢ ((??%?)→?); #Hbar cases (memb_append … Hbar) -Hbar #Hbar
+        [@(Hqout2 … Hbar)
+        |cases (orb_true_l … Hbar) -Hbar
+          [#Hbar lapply (\P Hbar) -Hbar #Hbar destruct (Hbar) @Hcout
+          |#Hbar cases (orb_true_l … Hbar) -Hbar 
+            [whd in ⊢ ((??%?)→?); #Hbar @Hbar
+            |#Hbar lapply (memb_single … Hbar) -Hbar #Hbar destruct (Hbar) @Hmv
+            ]
+          ]
+        ]
+      ]
+    ]
+  ]
 qed.
     
 lemma generic_match_to_match_in_table :
@@ -337,6 +345,8 @@ definition R_mark_next_tuple ≝
     ∨
     (no_bars rs1 ∧ t2 = midtape ? (reverse ? rs1@c::ls) 〈grid,false〉 rs2).
      
+axiom daemon :∀P:Prop.P.
+
 axiom tech_split :
   ∀A:DeqSet.∀f,l.
    (∀x.memb A x l = true → f x = false) ∨