From 2dee545ec9874703b954b57c3b4c300f6cf3b8a2 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 10 May 2012 07:38:44 +0000 Subject: [PATCH] axiomatization of acc_if --- matita/matita/lib/turing/if_machine.ma | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/matita/matita/lib/turing/if_machine.ma b/matita/matita/lib/turing/if_machine.ma index 28983b11e..8e2ed3ac1 100644 --- a/matita/matita/lib/turing/if_machine.ma +++ b/matita/matita/lib/turing/if_machine.ma @@ -58,6 +58,14 @@ axiom tdaemon : ∀X:Type[0].X. axiom 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). + +axiom acc_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 → + accRealize sig + (ifTM sig M1 (single_finalTM … M2) M3 acc) + (inr … (inl … (inr … 0))) + (Rtrue ∘ R2) + (Rfalse ∘ R3). (* #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse -- 2.39.2