X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fturing%2Fmono.ma;h=e89d710c948d2cf157d516e703f9c61ce76033d0;hb=690675dde36407d039e9d05047bc7909202170c1;hp=5813606a1afe3717940ab819f7463490ddfd6298;hpb=5c1794aba0652c0b0bce80a9ffc426192327709f;p=helm.git

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 5813606a1..e89d710c9 100644
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -284,6 +284,25 @@ definition accRealize ≝ λsig.λM:TM sig.λacc:states sig M.λRtrue,Rfalse:rel
   (cstate ?? outc = acc → Rtrue t (ctape ?? outc)) ∧ 
   (cstate ?? outc ≠ acc → Rfalse t (ctape ?? outc)).
 
+(* 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.
+
 (* Compositions *)
 
 definition seq_trans ≝ λsig. λM1,M2 : TM sig.