+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.
+
+definition initc ≝ λsig.λM:TM sig.λt.
+ mk_config sig (states sig M) (start sig M) t.
+
+definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
+∀t.∃i.∃outc.
+ loopM sig M i (initc sig M t) = Some ? outc ∧ R t (ctape ?? outc).
+
+definition WRealize ≝ λsig.λM:TM sig.λR:relation (tape sig).
+∀t,i,outc.
+ loopM sig M i (initc sig M t) = Some ? outc → R t (ctape ?? outc).
+
+definition Terminate ≝ λsig.λM:TM sig.λt. ∃i,outc.
+ loopM sig M i (initc sig M t) = Some ? outc.
+
+notation "M \vDash R" non associative with precedence 45 for @{ 'models $M $R}.
+interpretation "realizability" 'models M R = (Realize ? M R).
+
+notation "M \VDash R" non associative with precedence 45 for @{ 'wmodels $M $R}.
+interpretation "weak realizability" 'wmodels M R = (WRealize ? M R).
+
+interpretation "termination" 'fintersects M t = (Terminate ? M t).
+
+lemma WRealize_to_Realize : ∀sig.∀M: TM sig.∀R.
+ (∀t.M ↓ t) → M ⊫ R → M ⊨ R.
+#sig #M #R #HT #HW #t cases (HT … t) #i * #outc #Hloop
+@(ex_intro … i) @(ex_intro … outc) % // @(HW … i) //
+qed.
+
+theorem Realize_to_WRealize : ∀sig.∀M:TM sig.∀R.
+ M ⊨ R → M ⊫ R.
+#sig #M #R #H1 #inc #i #outc #Hloop
+cases (H1 inc) #k * #outc1 * #Hloop1 #HR >(loop_eq … Hloop Hloop1) //