+
+lemma loop_S_true :
+ ∀A,n,f,p,a. p a = true →
+ loop A (S n) f p a = Some ? a.
+#A #n #f #p #a #pa normalize >pa //
+qed.
+
+lemma loop_S_false :
+ ∀A,n,f,p,a. p a = false →
+ loop A (S n) f p a = loop A n f p (f a).
+normalize #A #n #f #p #a #Hpa >Hpa %
+qed.
+
+lemma loop_incr : ∀A,f,p,k1,k2,a1,a2.
+ loop A k1 f p a1 = Some ? a2 →
+ loop A (k2+k1) f p a1 = Some ? a2.
+#A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1
+[normalize #a0 #Hfalse destruct
+|#k1' #IH #a0 <plus_n_Sm whd in ⊢ (??%? → ??%?);
+ cases (true_or_false (p a0)) #Hpa0 >Hpa0 whd in ⊢ (??%? → ??%?); // @IH
+]
+qed.
+
+lemma loop_merge : ∀A,f,p,q.(∀b. p b = false → q b = false) →
+ ∀k1,k2,a1,a2,a3,a4.
+ loop A k1 f p a1 = Some ? a2 →
+ f a2 = a3 → q a2 = false →
+ loop A k2 f q a3 = Some ? a4 →
+ loop A (k1+k2) f q a1 = Some ? a4.
+#Sig #f #p #q #Hpq #k1 elim k1
+ [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
+ |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
+ cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
+ [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
+ whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
+ whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
+ |normalize >(Hpq … pa1) normalize #H1 #H2 #H3 @(Hind … H2) //
+ ]
+ ]
+qed.
+
+lemma loop_split : ∀A,f,p,q.(∀b. q b = true → p b = true) →
+ ∀k,a1,a2.
+ loop A k f q a1 = Some ? a2 →
+ ∃k1,a3.
+ loop A k1 f p a1 = Some ? a3 ∧
+ loop A (S(k-k1)) f q a3 = Some ? a2.
+#A #f #p #q #Hpq #k elim k
+ [#a1 #a2 normalize #Heq destruct
+ |#i #Hind #a1 #a2 normalize
+ cases (true_or_false (q a1)) #Hqa1 >Hqa1 normalize
+ [ #Ha1a2 destruct
+ @(ex_intro … 1) @(ex_intro … a2) %
+ [normalize >(Hpq …Hqa1) // |>Hqa1 //]
+ |#Hloop cases (true_or_false (p a1)) #Hpa1
+ [@(ex_intro … 1) @(ex_intro … a1) %
+ [normalize >Hpa1 // |>Hqa1 <Hloop normalize //]
+ |cases (Hind …Hloop) #k2 * #a3 * #Hloop1 #Hloop2
+ @(ex_intro … (S k2)) @(ex_intro … a3) %
+ [normalize >Hpa1 normalize // | @Hloop2 ]
+ ]
+ ]
+ ]
+qed.
+
+lemma loop_eq : ∀sig,f,q,i,j,a,x,y.
+ loop sig i f q a = Some ? x → loop sig j f q a = Some ? y → x = y.
+#sig #f #q #i #j @(nat_elim2 … i j)
+[ #n #a #x #y normalize #Hfalse destruct (Hfalse)
+| #n #a #x #y #H1 normalize #Hfalse destruct (Hfalse)
+| #n1 #n2 #IH #a #x #y normalize cases (q a) normalize
+ [ #H1 #H2 destruct %
+ | /2/ ]
+]
+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
+ [#a #b normalize #Hfalse destruct
+ |#k0 #IH #a #b whd in ⊢ (??%? → ?); cases (true_or_false (p a)) #Hpa
+ [ >Hpa normalize #H1 destruct // | >Hpa normalize @IH ]
+ ]
+qed.
+
+lemma loop_lift : ∀A,B,k,lift,f,g,h,hlift,c1,c2.
+ (∀x.hlift (lift x) = h x) →
+ (∀x.h x = false → lift (f x) = g (lift x)) →
+ loop A k f h c1 = Some ? c2 →
+ loop B k g hlift (lift c1) = Some ? (lift … c2).
+#A #B #k #lift #f #g #h #hlift #c1 #c2 #Hfg #Hhlift
+generalize in match c1; elim k
+[#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
+|#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
+ cases (true_or_false (h c0)) #Hc0 >Hfg >Hc0 normalize
+ [ #Heq destruct (Heq) % | <Hhlift // @IH ]
+qed.
+
+(************************** Realizability *************************************)
+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.