From b43ee563c38b153dd17d7b553e6b38b2f5057661 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 17 May 2012 14:12:45 +0000 Subject: [PATCH 1/1] 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