-qed.
-
-axiom bisim_char: ∀e1,e2:pre Bin.
-(∀w.(beqb (\snd (moves ? w e1)) (\snd (moves ? w e2))) = true) →
-\sem{e1}=1\sem{e2}.
-
-lemma bisim_ok2: ∀e1,e2:pre Bin.
- (beqb (\snd e1) (\snd e2) = true) →
- ∀n.∀frontier:list (space Bin).
- sub_sons [〈e1,e2〉] (frontier@[〈e1,e2〉]) →
- \fst (bisim n frontier [〈e1,e2〉]) = true → \sem{e1}=1\sem{e2}.
-#e1 #e2 #Hnil #n #frontier #init #bisim_true
-letin visited_res ≝ (\snd (bisim n frontier [〈e1,e2〉]))
-cut (bisim n frontier [〈e1,e2〉] = 〈true,visited_res〉)
- [<bisim_true <eq_pair_fst_snd //] #H
-cut (all_true [〈e1,e2〉])
- [#p #Hp cases (orb_true_l … Hp)
- [#eqp <(proj1 … (eqb_true …) eqp) //
- | whd in ⊢ ((??%?)→?); #abs @False_ind /2/
- ]] #allH
-cases (reachable_bisim … allH init … H) * #H1 #H2 #H3
-cut (∀w,p.memb (space Bin) p visited_res = true →
- memb (space Bin) 〈moves ? w (\fst p), moves ? w (\snd p)〉 visited_res = true)
- [#w elim w [* //]
- #a #w1 #Hind * #e11 #e21 #visp >fst_eq >snd_eq >moves_cons >moves_cons
- @(Hind 〈?,?〉) @(H1 〈?,?〉) //] #all_reach
-@bisim_char #w @(H3 〈?,?〉) @(all_reach w 〈?,?〉) @H2 //