update in alpha_1

[helm.git] / matita / matita / lib / turing / ntm.ma

diff --git a/matita/matita/lib/turing/ntm.ma b/matita/matita/lib/turing/ntm.ma
index 603a0a0dafa4aa77f2da9e594e35395589216b55..155b4cb922fb2ae26b641204228f1281350e7665 100644 (file)
--- a/matita/matita/lib/turing/ntm.ma
+++ b/matita/matita/lib/turing/ntm.ma
@@ -122,7 +122,7 @@ let rec mem A (a:A) (l:list A) on l ≝
   [ nil ⇒ False
   | cons hd tl ⇒ a=hd ∨ mem A a tl
   ]. 
-
+(* this no longer works: TODO 
 definition reach ≝ λsig.λM:NTM sig.λc,c1:config sig M.
   ∃q,l,q1,mvs. 
     state ?? c = q ∧ 
@@ -131,14 +131,14 @@ definition reach ≝ λsig.λM:NTM sig.λc,c1:config sig M.
     mem ? 〈〈q,l〉,〈q1,mvs〉〉 (trans ? M)  ∧ 
     state ?? c1 = q1 ∧
     tapes ?? c1 = (compose_vec ??? (tape_move sig) ? (tapes ?? c) mvs).
-
+*)
 (*
 definition empty_tapes ≝ λsig.λn.
 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
 elim n // normalize //
 qed.
 *)
-
+(* this no longer works: TODO
 definition init ≝ λsig.λM:NTM sig.λi:(list sig).
   mk_config ??
     (start sig M)
@@ -147,4 +147,4 @@ definition init ≝ λsig.λM:NTM sig.λi:(list sig).
 definition accepted ≝ λsig.λM:NTM sig.λw:(list sig).
 ∃c. star ? (reach sig M) (init sig M w) c ∧
   accept ?? (state ?? c) = true.
-
+*)
\ No newline at end of file