X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fbasic_machines.ma;h=f92afc7b9b30c3c1e07fa9e2ccf45c96d4f64eda;hb=fc803c84d8d99e1bf1f5f655312e120dcd87d90e;hp=4f1977dd47ec3ea8b7a2d6afaac77acde3f87e35;hpb=068e5a10f78798a3cbadb8aeed16b2c0d1f1d871;p=helm.git

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index 4f1977dd4..f92afc7b9 100644
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -106,6 +106,30 @@ lemma sem_move_l :
   #ls1 #c1 #rs1 #H destruct cases ls1 // ] ] ]
 qed.
 
+(* a slightly different move machine. *)
+definition smove_states ≝ initN 2.
+
+definition smove0 : smove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
+definition smove1 : smove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
+
+definition trans_smove ≝ 
+ λsig,D.
+ λp:smove_states × (option sig).
+ let 〈q,a〉 ≝ p in match (pi1 … q) with
+ [ O ⇒ 〈smove1,None sig, D〉
+ | S _ ⇒ 〈smove1,None sig, N〉 ].
+
+definition move ≝ 
+  λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1).
+
+definition Rmove ≝ 
+  λalpha,D,t1,t2. t2 = tape_move alpha t1 D.
+
+lemma sem_move_single :
+  ∀alpha,D.move alpha D ⊨ Rmove alpha D.
+#alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ]
+qed.
+
 (********************************* test char **********************************)
 
 (* the test_char machine ends up in two different states q1 and q2 wether or not