2020-04-03 15:53:54 +02:00
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
-------------------------------
|
2020-04-05 20:33:38 +02:00
|
|
|
equiv \emptyset Cs Ct gs \to Yes
|
2020-04-03 15:53:54 +02:00
|
|
|
|
|
|
|
|
-----------------------------------------
|
|
|
|
|
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)
|
|
|
|
|
|
|
|
|
|
<guard here>
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
