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 e89d710c948d2cf157d516e703f9c61ce76033d0..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
@@ -290,17 +289,19 @@ definition accRealize ≝ λsig.λM:TM sig.λacc:states sig M.λRtrue,Rfalse:rel
   *)
   
 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 ?〉)
-  O (λ_.true).
+  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 [| % normalize % ]
+#alpha #intape @(ex_intro ?? 1) 
+@(ex_intro … (mk_config ?? start_nop intape)) % % 
 qed.
 
 (* Compositions *)