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