unistep_aux

[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 39ecff800e79b11143e0db2d901a8112beaf4d65..bab3ab1ba067d1e1c23665fc6924def2603a176b 100644 (file)
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -109,6 +109,10 @@ definition tape_move ≝ λsig.λt: tape sig.λm:move.
     | N ⇒ t
     ].
 
+definition tape_move_mono ≝ 
+  λsig,t,mv.
+  tape_move sig (tape_write sig t (\fst mv)) (\snd mv).
+
 record config (sig,states:FinSet): Type[0] ≝ 
 { cstate : states;
   ctape: tape sig