From eb0c4dcf45d7cd3b9eb7af189ea74f5b23e40624 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Sun, 27 Jan 2013 14:38:20 +0000 Subject: [PATCH] sem_exec_move completed --- matita/matita/lib/turing/multi_universal/unistep.ma | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) 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 · -- 2.39.2