]
qed.
+lemma loop_p_true :
+ ∀A,k,f,p,a.p a = true → loop A (S k) f p a = Some ? a.
+#A #k #f #p #a #Ha normalize >Ha %
+qed.
+
lemma loop_Some :
∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
#A #k #f #p elim k
definition loopM ≝ λsig,M,i,cin.
loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) cin.
+lemma loopM_unfold : ∀sig,M,i,cin.
+ loopM sig M i cin = loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) cin.
+// qed.
+
definition initc ≝ λsig.λM:TM sig.λt.
mk_config sig (states sig M) (start sig M) t.
loopM sig M i (initc sig M t) = Some ? outc ∧
(cstate ?? outc = acc → Rtrue t (ctape ?? outc)) ∧
(cstate ?? outc ≠ acc → Rfalse t (ctape ?? outc)).
+
+notation "M ⊨ [q: R1,R2]" non associative with precedence 45 for @{ 'cmodels $M $q $R1 $R2}.
+interpretation "conditional realizability" 'cmodels M q R1 R2 = (accRealize ? M q R1 R2).
(******************************** NOP Machine *********************************)
@(ex_intro … (mk_config ?? start_nop intape)) % %
qed.
+lemma nop_single_state: ∀sig.∀q1,q2:states ? (nop sig). q1 = q2.
+normalize #sig * #n #ltn1 * #m #ltm1
+generalize in match ltn1; generalize in match ltm1;
+<(le_n_O_to_eq … (le_S_S_to_le … ltn1)) <(le_n_O_to_eq … (le_S_S_to_le … ltm1))
+// qed.
+
(************************** Sequential Composition ****************************)
definition seq_trans ≝ λsig. λM1,M2 : TM sig.
notation "a · b" non associative with precedence 65 for @{ 'middot $a $b}.
interpretation "sequential composition" 'middot a b = (seq ? a b).
-definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
- ∃am.R1 a1 am ∧ R2 am a2.
-
-interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
-
definition lift_confL ≝
λsig,S1,S2,c.match c with
[ mk_config s t ⇒ mk_config sig (FinSum S1 S2) (inl … s) t ].