Completed all proofs in if_machine

[helm.git] / matita / matita / lib / turing / mono.ma

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index a192f608ec46475fbbe7c48090f6c04a07bbc8aa..80e3d4aaaaf650d4420628dc631b33a1e6cfde6d 100644 (file)
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -270,6 +270,12 @@ lemma sem_nop :
 @(ex_intro … (mk_config ?? start_nop intape)) % % 
 qed.
 
+lemma nop_single_state: ∀sig.∀q1,q2:states ? (nop sig). q1 = q2.
+normalize #sig * #n #ltn1 * #m #ltm1 
+generalize in match ltn1; generalize in match ltm1;
+<(le_n_O_to_eq … (le_S_S_to_le … ltn1)) <(le_n_O_to_eq … (le_S_S_to_le … ltm1)) 
+// qed.
+
 (************************** Sequential Composition ****************************)
 
 definition seq_trans ≝ λsig. λM1,M2 : TM sig.