update in alpha_1

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

diff --git a/matita/matita/lib/turing/oracle.ma b/matita/matita/lib/turing/oracle.ma
index 4b6d7b1c74e5ad762eb37622b0b0a5e003273b79..4e7495d292628954756ce79cccb1d31a61a4627b 100644 (file)
--- a/matita/matita/lib/turing/oracle.ma
+++ b/matita/matita/lib/turing/oracle.ma
@@ -40,14 +40,14 @@ definition option_hd ≝ λA.λl:list A.
   [nil ⇒ None ?
   |cons a _ ⇒ Some ? a
   ].
-
+(* this no longer works: TODO 
 definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
   match \snd m with
   [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
   | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
   | N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
   ].
-
+*)
 definition current_chars ≝ λsig.λM:TM sig.λc:config sig M.
   vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
 
@@ -56,7 +56,7 @@ definition opt_cons ≝ λA.λa:option A.λl:list A.
   [ None ⇒ l
   | Some a ⇒ a::l
   ].
-
+(* this no longer works: TODO 
 definition step ≝ λsig.λM:TM sig.λc:config sig M.
   let 〈news,mvs,outchar〉 ≝ trans sig M 〈state ?? c,current_chars ?? c〉 in
   mk_config ?? 
@@ -74,7 +74,7 @@ definition init ≝ λsig.λM:TM sig.λi:(list sig).
     (start sig M)
     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
     [ ].
-
+*)
 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
   halt sig M (state sig M c).
 
@@ -83,7 +83,7 @@ let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
   [ O ⇒ None ?
   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
   ].
-
+(* this no longer works: TODO 
 (* Compute ? M f states that f is computed by M *)
 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 ∀l.∃i.∃c.
@@ -97,3 +97,4 @@ definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 ∀l.∃i.∃c.
   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
   (isnilb ? (out ?? c) = false).
+*)
\ No newline at end of file