result r ::= guard list * (Match bb | NoMatch | Absurd) guard := bb (equiv S Cₛ Cₜ gs = Yes) ∧ covers(Cₜ, S) ⇒ ∀vₛ≃vₜ ∈ S, Cₛ(vₛ) ≃gs Cₜ(vₜ) (equiv S Cₛ Cₜ gs = No(vₛ,vₜ) ∧ covers(Cₜ, S) ⇒ vₛ≃vₜ ∈ S ∧ Cₛ(vₛ) ≠gs Cₜ(vₜ) (vs,vt) \in S ------------------------- Test(S,false) = No(vs,vt) Test(S,true) = Yes ------------------------------- equiv \emptyset Cs Ct gs ~> Yes ----------------------------------------- equiv S Failure (Leaf BBt) gs ~>No(vs, vt) ----------------------------------------- equiv S (Leaf BBs) Failure gs ~>No(vs, vt) ---------------------------------------------- equiv S Failure Failure gs ~> Test(S, gs = []) rBB = Test(S, equiv_BB BBs BBt) rGuard = Test(s, gs = []) ------------------------------------------------------ equiv S (Leaf BBs) (Leaf BBt) gs ~> Merge(rBB, rGuard) Cs \in (Leaf BBs, Failure) (equiv S Cs Ci gs)^i ~> ri)^i equiv S Cs Cf gs ~> rf ----------------------------------------------------- equiv S Cs (Node(a, (Domi,Ci)^i, Cf)) gs ~> Merge((ri)^i, rf) (equiv S Ci (trim Ct a=Ki) gs ~> ri)^i equiv S Cf (trim Ct (a\notin(K_i)^i)) gs ~> rf ---------------------------------------------------------- equiv S (Node(a, (Ki,Ci)^i, Cf) Ct gs ~> Merge((ri)^i, rf) equiv S Ctrue Ct (gs++[condition]) ~> rt equiv S Cfalse Ct (gs++[condition]) ~> rf ------------------------------------------- equiv S (Guard condition Ctrue Cfalse) Ct gs ~> (Merge rt rf) rCond = Test(S, cond = condition) equiv S Cs Ctrue gs ~> rt equiv S Cs Cfalse gs ~> rf ------------------------------------------- equiv S Cs (Guard condition Ctrue Cfalse) ([cond]++gs) ~> (Merge rt rf) (vs,vt) \in S ------------------------------------------- equiv S Cs (Guard condition Ctrue Cfalse) [] ~> No(vs,vt) (Simplified rules) Idea: only talk about the valid equivalences (no No business) so instead of proving facts of the form equiv S Cs Ct gs ~> r we just prove equiv S Cs Ct gs ------------------------ equiv \emptyset Cs Ct gs -------------------------- equiv S Failure Failure [] equiv_BB BBs BBt ------------------------------- equiv S (Leaf BBs) (Leaf BBt) [] Cs \in (Leaf BBs, Failure) (equiv S Cs Ci gs)^i equiv S Cs Cf gs ----------------------------------------- equiv S Cs (Node(a, (Domi,Ci)^i, Cf)) gs equiv S Ci (trim Ct a=Ki) gs equiv S Cf (trim Ct (a\notin(K_i)^i) gs ------------------------------------- equiv S (Node(a, (Ki,Ci)^i, Cf) Ct gs equiv S Ctrue Ct (gs++[condition]) equiv S Cfalse Ct (gs++[condition]) -------------------------------------------- equiv S (Guard condition Ctrue Cfalse) Ct gs equiv S Cs Ctrue gs equiv S Cs Cfalse gs -------------------------------------------- equiv S Cs (Guard condition Ctrue Cfalse) ([condition]++gs) (Let's forget about those that are below) forall i, (equiv S Ci (Ct/a=Ki) = Yes) equiv S Cf (Ct/a\notin(K_i)^i) = Yes ------------------------------------------- equiv S (Node(a, (Ki,Ci)^i, Cf) Ct gs ~> Yes exists i, (equiv S Ci (Ct/a=Ki) = No(vs,vt)) ------------------------------------------------- equiv S (Node(a, (Ki,Ci)^i, Cf) Ct gs ~> No(vs,vt) equiv S Cf (Ct/a\notin(K_i)^i) = No(vs,vt) ------------------------------------------------- equiv kS (Node(a, (Ki,Ci)^i, Cf) Ct gs ~> No(vs,vt) forall S Cs Ct gs, exists (a unique) r such that (equiv S Cs Ct gs = r) is provable