-
-definition tt ≝ ps Bin true.
-definition ff ≝ ps Bin false.
-definition eps ≝ pe Bin.
-definition exp1 ≝ (ff + tt · ff).
-definition exp2 ≝ ff · (eps + tt).
-
-definition exp3 ≝ move Bin true (\fst (•exp1)).
-definition exp4 ≝ move Bin true (\fst (•exp2)).
-definition exp5 ≝ move Bin false (\fst (•exp1)).
-definition exp6 ≝ move Bin false (\fst (•exp2)).
+
+definition equiv ≝ λSig.λre1,re2:re Sig.
+ let e1 ≝ •(blank ? re1) in
+ let e2 ≝ •(blank ? re2) in
+ let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in
+ let sig ≝ (occ Sig e1 e2) in
+ (bisim ? sig n [〈e1,e2〉] []).
+
+theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
+ \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
+#Sig #re1 #re2 %
+ [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
+ cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
+ [<H //] #Hcut
+ cases (bisim_complete … Hcut)
+ [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
+ #Hbisim #Hsub @(bisim_to_sem … Hbisim)
+ @Hsub @memb_hd
+ |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2)))
+ [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
+ |//
+ |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/
+ |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
+ |#p #_ normalize //
+ ]
+ ]
+qed.
+
+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 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) exp10) = true.
+normalize // qed.