+definition eqbnat ≝ λn,m:nat. eqb n m.
+
+lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
+#n #m % [@eqb_true_to_eq | @eq_to_eqb_true]
+qed.
+
+definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true.
+
+definition a ≝ s DeqNat 0.
+definition b ≝ s DeqNat 1.
+definition c ≝ s DeqNat 2.
+
+definition exp1 ≝ ((a·b)^*·a).
+definition exp2 ≝ a·(b·a)^*.
+definition exp4 ≝ (b·a)^*.
+
+definition exp5 ≝ (a·(a·(a·b)^*·b)^*·b)^*.
+
+example
+ moves1: \snd (moves DeqNat [0;1;0] (•(blank ? exp2))) = true.
+normalize //
+qed.
+
+example
+ moves2: \snd (moves DeqNat [0;1;0;0;0] (•(blank ? exp2))) = false.
+normalize // qed.
+
+example
+ moves3: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1] (•(blank ? exp5))) = true.
+normalize // qed.
+
+example
+ moves4: \snd (moves DeqNat [0;0;0;1;0;1;1;0;1;1;1;0] (•(blank ? exp5))) = false.
+normalize // qed.
+
+definition exp6 ≝ a·(a ·a ·b^* + b^* ).
+definition exp7 ≝ a · a^* · b^*.
+
+definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
+definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
+
+example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
+normalize // qed.
+
+definition exp10 ≝ a·a·a·a·a·a·a·a·a·a·a·a·(a^* ).
+definition exp11 ≝ (a·a·a·a·a + a·a·a·a·a·a·a)^*.
+
+example ex2 : \fst (equiv ? (exp10+exp11) exp11) = false.
+normalize // qed.
+
+definition exp12 ≝
+ (a·a·a·a·a·a·a·a)·(a·a·a·a·a·a·a·a)·(a·a·a·a·a·a·a·a)·(a^* ).
+
+example ex3 : \fst (equiv ? (exp12+exp11) exp11) = true.
+normalize // qed.
+
+let rec raw (n:nat) ≝
+ match n with
+ [ O ⇒ a
+ | S p ⇒ a · (raw p)
+ ].
+
+let rec alln (n:nat) ≝
+ match n with
+ [O ⇒ ϵ
+ |S m ⇒ raw m + alln m
+ ].
+
+definition testA ≝ λx,y,z,b.
+ let e1 ≝ raw x in
+ let e2 ≝ raw y in
+ let e3 ≝ (raw z) · a^* in
+ let e4 ≝ (e1 + e2)^* in
+ \fst (equiv ? (e3+e4) e4) = b.
+
+example ex4 : testA 2 4 7 true.
+normalize // qed.
+
+example ex5 : testA 3 4 10 false.
+normalize // qed.
+
+example ex6 : testA 3 4 11 true.
+normalize // qed.
+
+example ex7 : testA 4 5 18 false.
+normalize // qed.
+
+example ex8 : testA 4 5 19 true.
+normalize // qed.
+
+example ex9 : testA 4 6 22 false.
+normalize // qed.
+
+example ex10 : testA 4 6 23 true.
+normalize // qed.
+
+definition testB ≝ λn,b.
+ \fst (equiv ? ((alln n)·((raw n)^* )) a^* ) = b.
+
+example ex11 : testB 6 true.
+normalize // qed.
+
+example ex12 : testB 8 true.
+normalize // qed.
+
+example ex13 : testB 10 true.
+normalize // qed.
+
+example ex14 : testB 12 true.
+normalize // qed.
+
+example ex15 : testB 14 true.
+normalize // qed.
+
+example ex16 : testB 16 true.
+normalize // qed.