From b43ee563c38b153dd17d7b553e6b38b2f5057661 Mon Sep 17 00:00:00 2001
From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Thu, 17 May 2012 14:12:45 +0000
Subject: [PATCH] Added step machine for universal machine.

---
 .../matita/lib/turing/universal/uni_step.ma   | 55 +++++++++++++++++++
 1 file changed, 55 insertions(+)
 create mode 100644 matita/matita/lib/turing/universal/uni_step.ma

diff --git a/matita/matita/lib/turing/universal/uni_step.ma b/matita/matita/lib/turing/universal/uni_step.ma
new file mode 100644
index 000000000..6ba1aa236
--- /dev/null
+++ b/matita/matita/lib/turing/universal/uni_step.ma
@@ -0,0 +1,55 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
+
+
+(* COMPARE BIT
+
+*)
+
+include "turing/universal/copy.ma".
+
+(*
+
+step :
+
+if is_true(current) (* current state is final *)
+   then nop
+   else 
+   (* init_match *)
+   mark;
+   adv_to_grid_r;
+   move_r;
+   mark;
+   move_l;
+   adv_to_mark_l
+   (* /init_match *)
+   match_tuple;
+   if is_marked(current) = false (* match ok *)
+      then 
+           (* init_copy *)
+           move_l;
+           init_current;
+           move_r;
+           adv_to_mark_r;
+           adv_mark_r;
+           (* /init_copy *)
+           copy;
+           move_r;
+           (* move_tape *)
+           by cases on current: 
+             case bit false: move_tape_l
+             case bit true: move_tape_r
+             case null: adv_to_grid_l; move_l; adv_to_grid_l;
+           move_r;
+           (* /move_tape *)
+      else sink;
+        
+*)
\ No newline at end of file
-- 
2.39.2