+definition Terminate ≝ λsig,n.λM:mTM sig n.λt. ∃i,outc.
+ loopM sig n M i (initc sig n M t) = Some ? outc.
+
+(* notation "M \vDash R" non associative with precedence 45 for @{ 'models $M $R}. *)
+interpretation "multi realizability" 'models M R = (Realize ?? M R).
+
+(* notation "M \VDash R" non associative with precedence 45 for @{ 'wmodels $M $R}. *)
+interpretation "weak multi realizability" 'wmodels M R = (WRealize ?? M R).
+
+interpretation "multi termination" 'fintersects M t = (Terminate ?? M t).
+
+lemma WRealize_to_Realize : ∀sig,n .∀M: mTM sig n.∀R.
+ (∀t.M ↓ t) → M ⊫ R → M ⊨ R.
+#sig #n #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,n.∀M:mTM sig n.∀R.
+ M ⊨ R → M ⊫ R.
+#sig #n #M #R #H1 #inc #i #outc #Hloop
+cases (H1 inc) #k * #outc1 * #Hloop1 #HR >(loop_eq … Hloop Hloop1) //
+qed.
+
+definition accRealize ≝ λsig,n.λM:mTM sig n.λacc:states sig n M.λRtrue,Rfalse.
+∀t.∃i.∃outc.
+ loopM sig n M i (initc sig n M t) = Some ? outc ∧
+ (cstate ??? outc = acc → Rtrue t (ctapes ??? outc)) ∧
+ (cstate ??? outc ≠ acc → Rfalse t (ctapes ??? outc)).
+
+(* notation "M ⊨ [q: R1,R2]" non associative with precedence 45 for @{ 'cmodels $M $q $R1 $R2}. *)
+interpretation "conditional multi realizability" 'cmodels M q R1 R2 = (accRealize ?? M q R1 R2).
+
+(*************************** guarded realizablity *****************************)
+definition GRealize ≝ λsig,n.λM:mTM sig n.
+ λPre:Vector (tape sig) ? →Prop.λR:relation (Vector (tape sig) ?).
+ ∀t.Pre t → ∃i.∃outc.
+ loopM sig n M i (initc sig n M t) = Some ? outc ∧ R t (ctapes ??? outc).
+
+definition accGRealize ≝ λsig,n.λM:mTM sig n.λacc:states sig n M.
+λPre: Vector (tape sig) ? → Prop.λRtrue,Rfalse.
+∀t.Pre t → ∃i.∃outc.
+ loopM sig n M i (initc sig n M t) = Some ? outc ∧
+ (cstate ??? outc = acc → Rtrue t (ctapes ??? outc)) ∧
+ (cstate ??? outc ≠ acc → Rfalse t (ctapes ??? outc)).
+
+lemma WRealize_to_GRealize : ∀sig,n.∀M: mTM sig n.∀Pre,R.
+ (∀t.Pre t → M ↓ t) → M ⊫ R → GRealize sig n M Pre R.
+#sig #n #M #Pre #R #HT #HW #t #HPre cases (HT … t HPre) #i * #outc #Hloop
+@(ex_intro … i) @(ex_intro … outc) % // @(HW … i) //
+qed.
+
+lemma Realize_to_GRealize : ∀sig,n.∀M: mTM sig n.∀P,R.
+ M ⊨ R → GRealize sig n M P R.
+#alpha #n #M #Pre #R #HR #t #HPre
+cases (HR t) -HR #k * #outc * #Hloop #HR
+@(ex_intro ?? k) @(ex_intro ?? outc) %
+ [ @Hloop | @HR ]
+qed.
+
+lemma acc_Realize_to_acc_GRealize: ∀sig,n.∀M:mTM sig n.∀q:states sig n M.∀P,R1,R2.
+ M ⊨ [q:R1,R2] → accGRealize sig n M q P R1 R2.
+#alpha #n #M #q #Pre #R1 #R2 #HR #t #HPre
+cases (HR t) -HR #k * #outc * * #Hloop #HRtrue #HRfalse
+@(ex_intro ?? k) @(ex_intro ?? outc) %
+ [ % [@Hloop] @HRtrue | @HRfalse]
+qed.
+
+(******************************** monotonicity ********************************)
+lemma Realize_to_Realize : ∀sig,n.∀M:mTM sig n.∀R1,R2.
+ R1 ⊆ R2 → M ⊨ R1 → M ⊨ R2.
+#alpha #n #M #R1 #R2 #Himpl #HR1 #intape
+cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
+@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
+qed.
+
+lemma WRealize_to_WRealize: ∀sig,n.∀M:mTM sig n.∀R1,R2.
+ R1 ⊆ R2 → WRealize sig n M R1 → WRealize sig n M R2.
+#alpha #n #M #R1 #R2 #Hsub #HR1 #intape #i #outc #Hloop
+@Hsub @(HR1 … i) @Hloop
+qed.
+
+lemma GRealize_to_GRealize : ∀sig,n.∀M:mTM sig n.∀P,R1,R2.
+ R1 ⊆ R2 → GRealize sig n M P R1 → GRealize sig n M P R2.
+#alpha #n #M #P #R1 #R2 #Himpl #HR1 #intape #HP
+cases (HR1 intape HP) -HR1 #k * #outc * #Hloop #HR1
+@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
+qed.
+
+lemma GRealize_to_GRealize_2 : ∀sig,n.∀M:mTM sig n.∀P1,P2,R1,R2.
+ P2 ⊆ P1 → R1 ⊆ R2 → GRealize sig n M P1 R1 → GRealize sig n M P2 R2.
+#alpha #n #M #P1 #P2 #R1 #R2 #Himpl1 #Himpl2 #H1 #intape #HP
+cases (H1 intape (Himpl1 … HP)) -H1 #k * #outc * #Hloop #H1
+@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
+qed.
+
+lemma acc_Realize_to_acc_Realize: ∀sig,n.∀M:mTM sig n.∀q:states sig n M.
+ ∀R1,R2,R3,R4.
+ R1 ⊆ R3 → R2 ⊆ R4 → M ⊨ [q:R1,R2] → M ⊨ [q:R3,R4].
+#alpha #n #M #q #R1 #R2 #R3 #R4 #Hsub13 #Hsub24 #HRa #intape
+cases (HRa intape) -HRa #k * #outc * * #Hloop #HRtrue #HRfalse
+@(ex_intro ?? k) @(ex_intro ?? outc) %
+ [ % [@Hloop] #Hq @Hsub13 @HRtrue // | #Hq @Hsub24 @HRfalse //]
+qed.
+
+(**************************** A canonical relation ****************************)
+
+definition R_mTM ≝ λsig,n.λM:mTM sig n.λq.λt1,t2.
+∃i,outc.
+ loopM ? n M i (mk_mconfig ??? q t1) = Some ? outc ∧
+ t2 = (ctapes ??? outc).
+
+lemma R_mTM_to_R: ∀sig,n.∀M:mTM sig n.∀R. ∀t1,t2.
+ M ⊫ R → R_mTM ?? M (start sig n M) t1 t2 → R t1 t2.
+#sig #n #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
+#Hloop #Ht2 >Ht2 @(HMR … Hloop)
+qed.
+
+(******************************** NOP Machine *********************************)
+
+(* NO OPERATION
+ t1 = t2
+
+definition nop_states ≝ initN 1.
+definition start_nop : initN 1 ≝ mk_Sig ?? 0 (le_n … 1). *)
+
+definition nop ≝
+ λalpha:FinSet.λn.mk_mTM alpha n nop_states
+ (λp.let 〈q,a〉 ≝ p in 〈q,mk_Vector ? (S n) (make_list ? (None ?) (S n)) ?〉)
+ start_nop (λ_.true).
+elim n normalize //
+qed.
+
+definition R_nop ≝ λalpha,n.λt1,t2:Vector (tape alpha) (S n).t2 = t1.
+
+lemma sem_nop :
+ ∀alpha,n.nop alpha n⊨ R_nop alpha n.
+#alpha #n #intapes @(ex_intro ?? 1)
+@(ex_intro … (mk_mconfig ??? start_nop intapes)) % %
+qed.
+
+lemma nop_single_state: ∀sig,n.∀q1,q2:states ? n (nop sig n). q1 = q2.
+normalize #sig #n0 * #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 null_action ≝ λsig.λn.
+mk_Vector ? (S n) (make_list (option (sig × move)) (None ?) (S n)) ?.
+elim (S n) // normalize //
+qed.
+
+lemma tape_move_null_action: ∀sig,n,tapes.
+ pmap_vec ??? (tape_move sig) (S n) tapes (null_action sig n) = tapes.
+#sig #n #tapes cases tapes -tapes #tapes whd in match (null_action ??);
+#Heq @Vector_eq <Heq -Heq elim tapes //
+#a #tl #Hind whd in ⊢ (??%?); @eq_f2 // @Hind
+qed.
+
+definition seq_trans ≝ λsig,n. λM1,M2 : mTM sig n.
+λp. let 〈s,a〉 ≝ p in
+ match s with
+ [ inl s1 ⇒
+ if halt sig n M1 s1 then 〈inr … (start sig n M2), null_action sig n〉
+ else let 〈news1,m〉 ≝ trans sig n M1 〈s1,a〉 in 〈inl … news1,m〉
+ | inr s2 ⇒ let 〈news2,m〉 ≝ trans sig n M2 〈s2,a〉 in 〈inr … news2,m〉