Definition of accRealize

diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma
index 592c9094731da0a7c680912e862586417e24c7b7..0fe4a4f1173be0d8d142ddc79d99bd264265794c 100644 (file)
--- a/matita/matita/lib/turing/if_machine.ma
+++ b/matita/matita/lib/turing/if_machine.ma
@@ -41,10 +41,9 @@ definition ifTM ≝ λsig. λcondM,thenM,elseM : TM sig.
         [ inl s2 ⇒ halt sig thenM s2
         | inr s3 ⇒ halt sig elseM s3 ]]). 
 
-theorem sem_seq: ∀sig,M1,M2,M3,P,R2,R3,q1,q2.
-  Frealize sig M1 P → Realize sig M2 R2 → Realize sig M3 R3 → 
-    Realize sig (ifTN sig M1 M2 M2) 
-      λt1.t2. (P t1 q1 t11 → R2 t11 t2) ∨ (P t1 q2 t12 → R3 t12 t2).
+theorem sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
+  accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 → 
+    Realize sig (ifTM sig M1 M2 M3 acc) (λt1,t2. (Rtrue ∘ R2) t1 t2 ∨ (Rfalse ∘ R3) t1 t2).
 
 (* We do not distinuish an input tape *)
 

diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma
index 7f261e48d814a6861c1eae246dbe970073d20fe1..4078c448340d2c94f1aac3b7fe86e2e7cb7ede63 100644 (file)
--- a/matita/matita/lib/turing/mono.ma
+++ b/matita/matita/lib/turing/mono.ma
@@ -118,6 +118,13 @@ definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
   R t (ctape ?? outc).
 
+
+definition accRealize ≝ λsig.λM:TM sig.λacc:states sig M.λRtrue,Rfalse:relation (tape sig).
+∀t.∃i.∃outc.
+  loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
+  (cstate ?? outc = acc → Rtrue t (ctape ?? outc)) ∧ 
+  (cstate ?? outc ≠ acc → Rfalse t (ctape ?? outc)).
+
 (* Compositions *)
 
 definition seq_trans ≝ λsig. λM1,M2 : TM sig.