started unistep

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

diff --git a/matita/matita/lib/turing/multi_universal/tuples.ma b/matita/matita/lib/turing/multi_universal/tuples.ma
index 428d99ccf0f415ec705d79aeec8de150e3a56ad1..86ff4396fee630481dedf646f472e8afbcfc2dff 100644 (file)
--- a/matita/matita/lib/turing/multi_universal/tuples.ma
+++ b/matita/matita/lib/turing/multi_universal/tuples.ma
@@ -118,3 +118,6 @@ 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 → 
+  ∀ll,lr.table_TM n l h = ll@c@lr → 
+    ∃out,m,lr0. lr = out@m::lr0 ∧ is_config n (bar::out) ∧ m ≠ bar.