cfg_in_table_to_tuple

diff --git a/matita/matita/lib/turing/multi_universal/tuples.ma b/matita/matita/lib/turing/multi_universal/tuples.ma
index 86ff4396fee630481dedf646f472e8afbcfc2dff..82ff036dac1d5aca56457d781377a7e338a5fa5c 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/tuples.ma
+++ b/matita/matita/lib/turing/multi_universal/tuples.ma
@@ -118,6 +118,57 @@ lemma table_to_list: ∀n,l,h,c. is_config n c →
   ]
 qed.
 
-axiom cfg_in_table_to_tuple: ∀n,l,h,c. is_config n c → 
+lemma cfg_in_table_to_tuple: ∀n,l,h,c. is_config n c → 
   ∀ll,lr.table_TM n l h = ll@c@lr → 
     ∃out,m,lr0. lr = out@m::lr0 ∧ is_config n (bar::out) ∧ m ≠ bar.
+#n #l #h #c * #qin * #cin * * * #H1 #H2 #H3 #H4  
+#ll #lr lapply ll -ll elim l
+  [>H4 #ll cases ll normalize [|#hd #tl ] #Habs destruct
+  |#t1 #othert #Hind #ll >table_TM_cons #Htuple
+   cut (S n < |ll@c@lr|)
+     [<Htuple >length_append >(length_of_tuple  … (is_tuple … ))
+      /2 by transitive_lt, le_n/] #Hsplit lapply Htuple -Htuple
+   cases (is_tuple … n h t1) #q1 * #c1 * #q2 * #c2 * #m 
+   * * * * * * * #Hq1 #Hq2 #Hc1 #Hc2 #Hm #Hlen1 #Hlen2 
+   whd in ⊢ (???%→?); #Ht1 
+   (* if ll is empty we match the first tuple t1, otherwise
+      we match inside othert *)
+   cases ll
+    [>H4 >Ht1 normalize in ⊢ (???%→?); 
+     >associative_append whd in ⊢ (??%?→?); #Heq destruct (Heq) -Heq
+     >associative_append in e0; #e0
+     lapply (append_l1_injective  … e0) [>H3 @Hlen1] #Heq1
+     lapply (append_l2_injective  … e0) [>H3 @Hlen1]
+     normalize in ⊢ (???%→?); whd in ⊢ (??%?→?); #Htemp 
+     lapply (cons_injective_l ????? Htemp) #Hc1
+     lapply (cons_injective_r ????? Htemp) -Htemp #Heq2
+     %{(q2@[c2])} %{m} %{(table_TM n othert h)} % // %
+     [ <Heq2 >associative_append >associative_append % | %{q2} %{c2} % // % // % // ] 
+    |(* ll not nil *)
+     #b #tl >Ht1 normalize in ⊢ (???%→?); 
+     whd in ⊢ (??%?→?); #Heq destruct (Heq) 
+     cases (compare_append … e0) #l *
+      [* cases l 
+        [#_ #Htab cases (Hind [ ] (sym_eq … Htab)) #out * #m0 * #lr0 * * #Hlr #Hcfg #Hm0
+         %{out} %{m0} %{lr0} % // % //
+        |(* this case is absurd *) 
+         #al #tll #Heq1 >H4 #Heq2 @False_ind 
+         lapply (cons_injective_l ? bar … Heq2) #Hbar <Hbar in Heq1; #Heq1
+         @(absurd (mem ? bar (q1@(c1::q2@[c2; m]))))
+          [>Heq1 @mem_append_l2 %1 //
+          |% #Hmembar cases (mem_append ???? Hmembar) -Hmembar
+            [#Hmembar lapply(Hq1 bar Hmembar) normalize #Habs destruct (Habs)
+            |* [#Habs @absurd //]
+             #Hmembar cases (mem_append ???? Hmembar) -Hmembar
+              [#Hmembar lapply(Hq2 bar Hmembar) normalize #Habs destruct (Habs)
+              |* [#Habs @absurd //] #Hmembar @(absurd ?? Hm) @sym_eq @mem_single //
+              ]
+            ]
+          ]
+        ]
+      |* #Htl #Htab cases (Hind … Htab) #out * #m0 * #lr0 * * #Hlr #Hcfg #Hm0
+        %{out} %{m0} %{lr0} % // % //
+      ] 
+    ]
+  ]
+qed.