porting of move_char_c

[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 5813606a1afe3717940ab819f7463490ddfd6298..f041d8b259f514351f36b11a20acf8a88cd5eaa2 100644 (file)
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -39,7 +39,6 @@ definition right ≝
  | rightof _ _ ⇒ []
  | midtape _ _ r ⇒ r ].
  
- 
 definition current ≝ 
  λsig.λt:tape sig.match t with
  [ midtape _ c _ ⇒ Some ? c
@@ -284,6 +283,27 @@ 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 start_nop : initN 1 ≝ mk_Sig ?? 0 (le_n … (S 0)).
+
+definition nop ≝ 
+  λalpha:FinSet.mk_TM alpha nop_states
+  (λp.let 〈q,a〉 ≝ p in 〈q,None ?〉)
+  start_nop (λ_.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 … (mk_config ?? start_nop intape)) % % 
+qed.
+
 (* Compositions *)
 
 definition seq_trans ≝ λsig. λM1,M2 : TM sig.