Progress.

[helm.git] / matita / matita / lib / turing / universal / marks.ma

diff --git a/matita/matita/lib/turing/universal/marks.ma b/matita/matita/lib/turing/universal/marks.ma
index 12a9f16352da5b9be7ffae300231d99094d56df9..d3ef41c8dae110dabb054871d9d07f2aeeb58ce7 100644 (file)
--- a/matita/matita/lib/turing/universal/marks.ma
+++ b/matita/matita/lib/turing/universal/marks.ma
@@ -16,6 +16,7 @@
 
 include "turing/while_machine.ma".
 include "turing/if_machine.ma".
+include "turing/universal/tests.ma".
 
 (* ADVANCE TO MARK (right)
 
@@ -580,27 +581,6 @@ qed.
               ^
 *)
 
-include "turing/universal/tests.ma".
-
-(* NO OPERATION
-
-  t1 = t2
-  *)
-  
-definition nop_states ≝ initN 1.
-
-definition nop ≝ 
-  λalpha:FinSet.mk_TM alpha nop_states
-  (λp.let 〈q,a〉 ≝ p in 〈q,None ?〉)
-  O (λ_.true).
-  
-definition R_nop ≝ λalpha.λt1,t2:tape alpha.t2 = t1.
-
-lemma sem_nop :
-  ∀alpha.Realize alpha (nop alpha) (R_nop alpha).
-#alpha #intape @(ex_intro ?? 1) @ex_intro [| % normalize % ]
-qed.
-
 definition match_and_adv ≝ 
   λalpha,f.ifTM ? (test_char ? f)
      (adv_both_marks alpha) (nop ?) tc_true.