+(* 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.
+