| S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
].
+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.
(cstate ?? outc = acc → Rtrue t (ctape ?? outc)) ∧
(cstate ?? outc ≠ acc → Rfalse t (ctape ?? outc)).
+(* NO OPERATION
+
+ t1 = t2
+ *)
+
+definition nop_states ≝ initN 1.
+
+definition nop ≝
+ λalpha:FinSet.mk_TM alpha nop_states
+ (λp.let 〈q,a〉 ≝ p in 〈q,None ?〉)
+ O (λ_.true).
+
+definition R_nop ≝ λalpha.λt1,t2:tape alpha.t2 = t1.
+
+lemma sem_nop :
+ ∀alpha.Realize alpha (nop alpha) (R_nop alpha).
+#alpha #intape @(ex_intro ?? 1) @ex_intro [| % normalize % ]
+qed.
+
(* Compositions *)
definition seq_trans ≝ λsig. λM1,M2 : TM sig.