X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fmulti_universal%2Funistep.ma;h=9d76d7494d4611263e1b5cf7ba981ebeeb725667;hb=eb0c4dcf45d7cd3b9eb7af189ea74f5b23e40624;hp=7fa80f38108f5be846c922bf2591e43966dd90cf;hpb=3447747453bbf439d071d21dcb68149cae3a9068;p=helm.git

diff --git a/matita/matita/lib/turing/multi_universal/unistep.ma b/matita/matita/lib/turing/multi_universal/unistep.ma
index 7fa80f381..9d76d7494 100644
--- a/matita/matita/lib/turing/multi_universal/unistep.ma
+++ b/matita/matita/lib/turing/multi_universal/unistep.ma
@@ -1,4 +1,4 @@
-(*
+#(*
     ||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.           
@@ -78,7 +78,16 @@ whd in semM4; >Ht3 in semM4;
      >Hprg whd in match (list_of_tape ??); >reverse_append
      >reverse_single % 
     ]
-  |
+  |#b #Hcurrent @(list_of_tape_write ? is_bit … (char_to_bit_option c) ? Honlybits)
+    [#b0 cases c
+      [#b1 whd in ⊢ (??%?→?); #Hbit destruct (Hbit) %
+      |whd in ⊢ (??%?→?); #Hbit destruct (Hbit)
+      |whd in ⊢ (??%?→?); #Hbit destruct (Hbit)
+      ]
+    |>(list_of_tape_move … (char_to_move m)) @current_in_list @Hcurrent
+    ]
+  ]
+qed.
        
 definition unistep ≝ 
   match_m cfg prg FSUnialpha 2 ·