Added a turing/universal directory for the universal turing machine (and

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

diff --git a/matita/matita/lib/turing/while_machine.ma b/matita/matita/lib/turing/while_machine.ma
index f8be66d25b2436bde02cba182ec2a3251c701ac2..52a0a79b75e62d44b7ab1e25abc83af29b7d381c 100644 (file)
--- a/matita/matita/lib/turing/while_machine.ma
+++ b/matita/matita/lib/turing/while_machine.ma
@@ -9,8 +9,8 @@
      \ /   GNU General Public License Version 2   
       V_____________________________________________________________*)
 
-include "turing/mono.ma".
 include "basics/star.ma".
+include "turing/mono.ma".
 
 definition while_trans ≝ λsig. λM : TM sig. λq:states sig M. λp.
   let 〈s,a〉 ≝ p in
@@ -24,7 +24,7 @@ definition whileTM ≝ λsig. λM : TM sig. λqacc: states ? M.
     (start sig M)
     (λs.halt sig M s ∧ ¬ s==qacc).
     
-axiom daemon : ∀X:Prop.X.
+(* axiom daemon : ∀X:Prop.X. *)
 
 lemma while_trans_false : ∀sig,M,q,p.
   \fst p ≠ q → trans sig (whileTM sig M q) p = trans sig M p.
@@ -122,7 +122,9 @@ cases (loop_split ?? (λc. halt sig M (cstate ?? c)) ????? Hloop)
    ]
  ]
 qed.
-(*
+
+
+(* (*
 
 (* We do not distinuish an input tape *)