X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fif_machine.ma;h=7b73d006d7a827d78743b81d633eb9f138e052ff;hb=544aa49f420b6049bc9419bf7d2c20b781293ca7;hp=592c9094731da0a7c680912e862586417e24c7b7;hpb=09a348f01d0a42a1936a3e90803fd27dd49984f4;p=helm.git

diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma
index 592c90947..7b73d006d 100644
--- a/matita/matita/lib/turing/if_machine.ma
+++ b/matita/matita/lib/turing/if_machine.ma
@@ -39,13 +39,56 @@ definition ifTM ≝ λsig. λcondM,thenM,elseM : TM sig.
       [ inl _ ⇒ false 
       | inr s' ⇒ match s' with 
         [ 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).
-
+        | inr s3 ⇒ halt sig elseM s3 ]]).
+        
+axiom daemon : ∀X:Prop.X. 
+
+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).
+#sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t 
+cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse 
+cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
+  [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2
+   @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2)))
+   %
+   [@(loop_split ??????????? 
+    (loop_lift ??? 
+      (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3)))
+      (step sig M1) (step sig (ifTM sig M1 M2 M3 acc)) 
+      (λc.halt sig M1 (cstate … c)) 
+      (λc.halt_liftL ?? (halt sig M1) (cstate … c)) 
+      … Hloop1))
+     [* *
+       [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
+       | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
+     || #c0 #Hhalt @daemon  (* <step_lift_confL // *)
+     | #x <p_halt_liftL %
+     |6:cases outc1 #s1 #t1 %
+     |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2) 
+       [ * #s2 #t2 %
+       | #c0 #Hhalt @daemon (* <step_lift_confR // *) ]
+     |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
+      generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10 
+      >(trans_liftL_true sig M1 M2 ??) 
+       [ whd in ⊢ (??%?); whd in ⊢ (???%);
+         @config_eq whd in ⊢ (???%); //
+       | @(loop_Some ?????? Hloop10) ]       
+     ||4:cases outc1 #s1 #t1 %
+     |5:
+         
+         @(loop_liftR … Hloop2) 
+         |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
+          generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10 
+          >(trans_liftL_true sig M1 M2 ??) 
+           [ whd in ⊢ (??%?); whd in ⊢ (???%);
+             @config_eq //
+           | @(loop_Some ?????? Hloop10) ]
+           ]
+| @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
+  % //
+]
+qed.
 (* We do not distinuish an input tape *)
 
 record TM (sig:FinSet): Type[1] ≝