X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fbasic_machines.ma;fp=matita%2Fmatita%2Flib%2Fturing%2Fbasic_machines.ma;h=c1559702a59770c27dc68bbfcf98e2d50f6aaa46;hb=8712a9a43384e0f437e8ea97fd66c8ea4da7bcfe;hp=1e5fa3d2ed4a19161ebf8a75058ea40be67d5aef;hpb=1e74e10d6d177c8afe14f20f050812f68aa2b530;p=helm.git

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index 1e5fa3d2e..c1559702a 100644
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -41,6 +41,26 @@ lemma sem_write_strong : ∀alpha,c.Realize ? (write alpha c) (R_write_strong al
   [|% [% |cases t normalize // ] ]
 qed. 
 
+(***************************** replace a with f a *****************************)
+
+definition writef ≝ λalpha,f.
+  mk_TM alpha write_states
+  (λp.let 〈q,a〉 ≝ p in
+    match pi1 … q with 
+    [ O ⇒ 〈wr1,Some ? (f a),N〉
+    | S _ ⇒ 〈wr1,None ?,N〉 ])
+  wr0 (λx.x == wr1).
+
+definition R_writef ≝ λalpha,f,t1,t2.
+  ∀c. current ? t1 = c  →
+  t2 = midtape alpha (left ? t1) (f c) (right ? t1).
+  
+lemma sem_writef : ∀alpha,f.
+  writef alpha f  ⊨ R_writef alpha f.
+#alpha #f #t @(ex_intro … 2) @ex_intro
+  [|% [% |cases t normalize // ] ]
+qed. 
+
 (******************** moves the head one step to the right ********************)
 
 definition move_states ≝ initN 2.