Theory Qmsg_Lifting
section "Lifting rules for parallel compositions with QMSG"
theory Qmsg_Lifting
imports Qmsg OAWN_SOS Inv_Cterms OAWN_Invariants
begin
lemma oseq_no_change_on_send:
fixes σ s a σ' s'
assumes "((σ, s), a, (σ', s')) ∈ oseqp_sos Γ i"
shows "case a of
broadcast m ⇒ σ' i = σ i
| groupcast ips m ⇒ σ' i = σ i
| unicast ips m ⇒ σ' i = σ i
| ¬unicast ips ⇒ σ' i = σ i
| send m ⇒ σ' i = σ i
| deliver m ⇒ σ' i = σ i
| _ ⇒ True"
using assms by induction simp_all
lemma qmsg_no_change_on_send_or_receive:
fixes σ s a σ' s'
assumes "((σ, s), a, (σ', s')) ∈ oparp_sos i (oseqp_sos Γ i) (seqp_sos Γ⇩Q⇩M⇩S⇩G)"
and "a ≠ τ"
shows "σ' i = σ i"
proof -
from assms(1) obtain p q p' q'
where "((σ, (p, q)), a, (σ', (p', q'))) ∈ oparp_sos i (oseqp_sos Γ i) (seqp_sos Γ⇩Q⇩M⇩S⇩G)"
by (cases s, cases s', simp)
thus ?thesis
proof
assume "((σ, p), a, (σ', p')) ∈ oseqp_sos Γ i"
and "⋀m. a ≠ receive m"
with ‹a ≠ τ› show "σ' i = σ i"
by - (drule oseq_no_change_on_send, cases a, auto)
next
assume "(q, a, q') ∈ seqp_sos Γ⇩Q⇩M⇩S⇩G"
and "σ' i = σ i"
thus "σ' i = σ i" by simp
next
assume "a = τ" with ‹a ≠ τ› show ?thesis by auto
qed
qed
lemma qmsg_msgs_not_empty:
"qmsg ⊫ onl Γ⇩Q⇩M⇩S⇩G (λ(msgs, l). l = ()-:1 ⟶ msgs ≠ [])"
by inv_cterms
lemma qmsg_send_from_queue:
"qmsg ⊫⇩A (λ((msgs, q), a, _). sendmsg (λm. m∈set msgs) a)"
proof -
have "qmsg ⊫⇩A onll Γ⇩Q⇩M⇩S⇩G (λ((msgs, _), a, _). sendmsg (λm. m∈set msgs) a)"
by (inv_cterms inv add: onl_invariant_sterms [OF qmsg_wf qmsg_msgs_not_empty])
thus ?thesis
by (rule step_invariant_weakenE) (auto dest!: onllD)
qed
lemma qmsg_queue_contents:
"qmsg ⊫⇩A (λ((msgs, q), a, (msgs', q')). case a of
receive m ⇒ set msgs' ⊆ set (msgs @ [m])
| _ ⇒ set msgs' ⊆ set msgs)"
proof -
have "qmsg ⊫⇩A onll Γ⇩Q⇩M⇩S⇩G (λ((msgs, q), a, (msgs', q')).
case a of
receive m ⇒ set msgs' ⊆ set (msgs @ [m])
| _ ⇒ set msgs' ⊆ set msgs)"
by (inv_cterms) (clarsimp simp add: in_set_tl)+
thus ?thesis
by (rule step_invariant_weakenE) (auto dest!: onllD)
qed
lemma qmsg_send_receive_or_tau:
"qmsg ⊫⇩A (λ(_, a, _). ∃m. a = send m ∨ a = receive m ∨ a = τ)"
proof -
have "qmsg ⊫⇩A onll Γ⇩Q⇩M⇩S⇩G (λ(_, a, _). ∃m. a = send m ∨ a = receive m ∨ a = τ)"
by inv_cterms
thus ?thesis
by rule (auto dest!: onllD)
qed
lemma par_qmsg_oreachable:
assumes "(σ, ζ) ∈ oreachable (A ⟨⟨⇘i⇙ qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})"
(is "_ ∈ oreachable _ ?owS _")
and pinv: "A ⊨⇩A (otherwith S {i} (orecvmsg R), other U {i} →)
globala (λ(σ, _, σ'). U (σ i) (σ' i))"
and ustutter: "⋀ξ. U ξ ξ"
and sgivesu: "⋀ξ ξ'. S ξ ξ' ⟹ U ξ ξ'"
and upreservesq: "⋀σ σ' m. ⟦ ∀j. U (σ j) (σ' j); R σ m ⟧ ⟹ R σ' m"
shows "(σ, fst ζ) ∈ oreachable A ?owS (other U {i})
∧ snd ζ ∈ reachable qmsg (recvmsg (R σ))
∧ (∀m∈set (fst (snd ζ)). R σ m)"
using assms(1) proof (induction rule: oreachable_pair_induct)
fix σ pq
assume "(σ, pq) ∈ init (A ⟨⟨⇘i⇙ qmsg)"
then obtain p ms q where "pq = (p, (ms, q))"
and "(σ, p) ∈ init A"
and "(ms, q) ∈ init qmsg"
by (clarsimp simp del: Γ⇩Q⇩M⇩S⇩G_simps)
from this(2) have "(σ, p) ∈ oreachable A ?owS (other U {i})" ..
moreover from ‹(ms, q) ∈ init qmsg› have "(ms, q) ∈ reachable qmsg (recvmsg (R σ))" ..
moreover from ‹(ms, q) ∈ init qmsg› have "ms = []"
unfolding σ⇩Q⇩M⇩S⇩G_def by simp
ultimately show "(σ, fst pq) ∈ oreachable A ?owS (other U {i})
∧ snd pq ∈ reachable qmsg (recvmsg (R σ))
∧ (∀m∈set (fst (snd pq)). R σ m)"
using ‹pq = (p, (ms, q))› by simp
next
note Γ⇩Q⇩M⇩S⇩G_simps [simp del]
case (other σ pq σ')
hence "(σ, fst pq) ∈ oreachable A ?owS (other U {i})"
and "other U {i} σ σ'"
and qr: "snd pq ∈ reachable qmsg (recvmsg (R σ))"
and "∀m∈set (fst (snd pq)). R σ m"
by simp_all
from ‹other U {i} σ σ'› and ustutter have "∀j. U (σ j) (σ' j)"
by (clarsimp elim!: otherE) metis
from ‹other U {i} σ σ'›
and ‹(σ, fst pq) ∈ oreachable A ?owS (other U {i})›
have "(σ', fst pq) ∈ oreachable A ?owS (other U {i})"
by - (rule oreachable_other')
moreover have "∀m∈set (fst (snd pq)). R σ' m"
proof
fix m assume "m ∈ set (fst (snd pq))"
with ‹∀m∈set (fst (snd pq)). R σ m› have "R σ m" ..
with ‹∀j. U (σ j) (σ' j)› show "R σ' m" by (rule upreservesq)
qed
moreover from qr have "snd pq ∈ reachable qmsg (recvmsg (R σ'))"
proof
fix a
assume "recvmsg (R σ) a"
thus "recvmsg (R σ') a"
proof (rule recvmsgE [where R=R])
fix m assume "R σ m"
with ‹∀j. U (σ j) (σ' j)› show "R σ' m" by (rule upreservesq)
qed
qed
ultimately show ?case using qr by simp
next
case (local σ pq σ' pq' a)
obtain p ms q p' ms' q' where "pq = (p, (ms, q))"
and "pq' = (p', (ms', q'))"
by (cases pq, cases pq') metis
with local.hyps local.IH
have pqtr: "((σ, (p, (ms, q))), a, (σ', (p', (ms', q'))))
∈ oparp_sos i (trans A) (seqp_sos Γ⇩Q⇩M⇩S⇩G)"
and por: "(σ, p) ∈ oreachable A ?owS (other U {i})"
and qr: "(ms, q) ∈ reachable qmsg (recvmsg (R σ))"
and "∀m∈set ms. R σ m"
and "?owS σ σ' a"
by (simp_all del: Γ⇩Q⇩M⇩S⇩G_simps)
from ‹?owS σ σ' a› have "∀j. j≠i ⟶ S (σ j) (σ' j)"
by (clarsimp dest!: otherwith_syncD)
with sgivesu have "∀j. j≠i ⟶ U (σ j) (σ' j)" by simp
from ‹?owS σ σ' a› have "orecvmsg R σ a" by (rule otherwithE)
hence "recvmsg (R σ) a" ..
from pqtr have "(σ', p') ∈ oreachable A ?owS (other U {i})
∧ (ms', q') ∈ reachable qmsg (recvmsg (R σ'))
∧ (∀m∈set ms'. R σ' m)"
proof
assume "((σ, p), a, (σ', p')) ∈ trans A"
and "⋀m. a ≠ receive m"
and "(ms', q') = (ms, q)"
from this(1) have ptr: "((σ, p), a, (σ', p')) ∈ trans A" by simp
with pinv por and ‹?owS σ σ' a› have "U (σ i) (σ' i)"
by (auto dest!: ostep_invariantD)
with ‹∀j. j≠i ⟶ U (σ j) (σ' j)› have "∀j. U (σ j) (σ' j)" by auto
hence recvmsg': "⋀a. recvmsg (R σ) a ⟹ recvmsg (R σ') a"
by (auto elim!: recvmsgE [where R=R] upreservesq)
from por ptr ‹?owS σ σ' a› have "(σ', p') ∈ oreachable A ?owS (other U {i})"
by - (rule oreachable_local')
moreover have "(ms', q') ∈ reachable qmsg (recvmsg (R σ'))"
proof -
from qr and ‹(ms', q') = (ms, q)›
have "(ms', q') ∈ reachable qmsg (recvmsg (R σ))" by simp
thus ?thesis by (rule reachable_weakenE) (erule recvmsg')
qed
moreover have "∀m∈set ms'. R σ' m"
proof
fix m
assume "m∈set ms'"
with ‹(ms', q') = (ms, q)› have "m∈set ms" by simp
with ‹∀m∈set ms. R σ m› have "R σ m" ..
with ‹∀j. U (σ j) (σ' j)› show "R σ' m"
by (rule upreservesq)
qed
ultimately show
"(σ', p') ∈ oreachable A ?owS (other U {i})
∧ (ms', q') ∈ reachable qmsg (recvmsg (R σ'))
∧ (∀m∈set ms'. R σ' m)" by simp_all
next
assume qtr: "((ms, q), a, (ms', q')) ∈ seqp_sos Γ⇩Q⇩M⇩S⇩G"
and "⋀m. a ≠ send m"
and "p' = p"
and "σ' i = σ i"
from this(4) and ‹⋀ξ. U ξ ξ› have "U (σ i) (σ' i)" by simp
with ‹∀j. j≠i ⟶ U (σ j) (σ' j)› have "∀j. U (σ j) (σ' j)" by auto
hence recvmsg': "⋀a. recvmsg (R σ) a ⟹ recvmsg (R σ') a"
by (auto elim!: recvmsgE [where R=R] upreservesq)
from qtr have tqtr: "((ms, q), a, (ms', q')) ∈ trans qmsg" by simp
from ‹∀j. U (σ j) (σ' j)› and ‹σ' i = σ i› have "other U {i} σ σ'" by auto
with por and ‹p' = p›
have "(σ', p') ∈ oreachable A ?owS (other U {i})"
by (auto dest: oreachable_other)
moreover have "(ms', q') ∈ reachable qmsg (recvmsg (R σ'))"
proof (rule reachable_weakenE [where P="recvmsg (R σ)"])
from qr tqtr ‹recvmsg (R σ) a› show "(ms', q') ∈ reachable qmsg (recvmsg (R σ))" ..
qed (rule recvmsg')
moreover have "∀m∈set ms'. R σ' m"
proof
fix m
assume "m ∈ set ms'"
moreover have "case a of receive m ⇒ set ms' ⊆ set (ms @ [m]) | _ ⇒ set ms' ⊆ set ms"
proof -
from qr have "(ms, q) ∈ reachable qmsg TT" ..
thus ?thesis using tqtr
by (auto dest!: step_invariantD [OF qmsg_queue_contents])
qed
ultimately have "R σ m" using ‹∀m∈set ms. R σ m› and ‹orecvmsg R σ a›
by (cases a) auto
with ‹∀j. U (σ j) (σ' j)› show "R σ' m"
by (rule upreservesq)
qed
ultimately show "(σ', p') ∈ oreachable A ?owS (other U {i})
∧ (ms', q') ∈ reachable qmsg (recvmsg (R σ'))
∧ (∀m∈set ms'. R σ' m)" by simp
next
fix m
assume "a = τ"
and "((σ, p), receive m, (σ', p')) ∈ trans A"
and "((ms, q), send m, (ms', q')) ∈ seqp_sos Γ⇩Q⇩M⇩S⇩G"
from this(2-3)
have ptr: "((σ, p), receive m, (σ', p')) ∈ trans A"
and qtr: "((ms, q), send m, (ms', q')) ∈ trans qmsg" by simp_all
from qr have "(ms, q) ∈ reachable qmsg TT" ..
with qtr have "m ∈ set ms"
by (auto dest!: step_invariantD [OF qmsg_send_from_queue])
with ‹∀m∈set ms. R σ m› have "R σ m" ..
hence "orecvmsg R σ (receive m)" by simp
with ‹∀j. j≠i ⟶ S (σ j) (σ' j)› have "?owS σ σ' (receive m)"
by (auto intro!: otherwithI)
with pinv por ptr have "U (σ i) (σ' i)"
by (auto dest!: ostep_invariantD)
with ‹∀j. j≠i ⟶ U (σ j) (σ' j)› have "∀j. U (σ j) (σ' j)" by auto
hence recvmsg': "⋀a. recvmsg (R σ) a ⟹ recvmsg (R σ') a"
by (auto elim!: recvmsgE [where R=R] upreservesq)
from por ptr have "(σ', p') ∈ oreachable A ?owS (other U {i})"
using ‹?owS σ σ' (receive m)› by - (erule(1) oreachable_local, simp)
moreover have "(ms', q') ∈ reachable qmsg (recvmsg (R σ'))"
proof (rule reachable_weakenE [where P="recvmsg (R σ)"])
have "recvmsg (R σ) (send m)" by simp
with qr qtr show "(ms', q') ∈ reachable qmsg (recvmsg (R σ))" ..
qed (rule recvmsg')
moreover have "∀m∈set ms'. R σ' m"
proof
fix m
assume "m ∈ set ms'"
moreover have "set ms' ⊆ set ms"
proof -
from qr have "(ms, q) ∈ reachable qmsg TT" ..
thus ?thesis using qtr
by (auto dest!: step_invariantD [OF qmsg_queue_contents])
qed
ultimately have "R σ m" using ‹∀m∈set ms. R σ m› by auto
with ‹∀j. U (σ j) (σ' j)› show "R σ' m"
by (rule upreservesq)
qed
ultimately show "(σ', p') ∈ oreachable A ?owS (other U {i})
∧ (ms', q') ∈ reachable qmsg (recvmsg (R σ'))
∧ (∀m∈set ms'. R σ' m)" by simp
qed
with ‹pq = (p, (ms, q))› and ‹pq' = (p', (ms', q'))› show ?case
by (simp_all del: Γ⇩Q⇩M⇩S⇩G_simps)
qed
lemma par_qmsg_oreachable_statelessassm:
assumes "(σ, ζ) ∈ oreachable (A ⟨⟨⇘i⇙ qmsg)
(λσ _. orecvmsg (λ_. R) σ) (other (λ_ _. True) {i})"
and ustutter: "⋀ξ. U ξ ξ"
shows "(σ, fst ζ) ∈ oreachable A (λσ _. orecvmsg (λ_. R) σ) (other (λ_ _. True) {i})
∧ snd ζ ∈ reachable qmsg (recvmsg R)
∧ (∀m∈set (fst (snd ζ)). R m)"
proof -
from assms(1)
have "(σ, ζ) ∈ oreachable (A ⟨⟨⇘i⇙ qmsg)
(otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)))
(other (λ_ _. True) {i})" by auto
moreover
have "A ⊨⇩A (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)),
other (λ_ _. True) {i} →) globala (λ(σ, _, σ'). True)"
by auto
ultimately
obtain "(σ, fst ζ) ∈ oreachable A
(otherwith (λ_ _. True) {i} (orecvmsg (λ_. R))) (other (λ_ _. True) {i})"
and *: "snd ζ ∈ reachable qmsg (recvmsg R)"
and **: "(∀m∈set (fst (snd ζ)). R m)"
by (auto dest!: par_qmsg_oreachable)
from this(1)
have "(σ, fst ζ) ∈ oreachable A (λσ _. orecvmsg (λ_. R) σ) (other (λ_ _. True) {i})"
by rule auto
thus ?thesis using * ** by simp
qed
lemma lift_into_qmsg:
assumes "A ⊨ (otherwith S {i} (orecvmsg R), other U {i} →) global P"
and "⋀ξ. U ξ ξ"
and "⋀ξ ξ'. S ξ ξ' ⟹ U ξ ξ'"
and "⋀σ σ' m. ⟦ ∀j. U (σ j) (σ' j); R σ m ⟧ ⟹ R σ' m"
and "A ⊨⇩A (otherwith S {i} (orecvmsg R), other U {i} →)
globala (λ(σ, _, σ'). U (σ i) (σ' i))"
shows "A ⟨⟨⇘i⇙ qmsg ⊨ (otherwith S {i} (orecvmsg R), other U {i} →) global P"
proof (rule oinvariant_oreachableI)
fix σ ζ
assume "(σ, ζ) ∈ oreachable (A ⟨⟨⇘i⇙ qmsg) (otherwith S {i} (orecvmsg R)) (other U {i})"
then obtain s where "(σ, s) ∈ oreachable A (otherwith S {i} (orecvmsg R)) (other U {i})"
by (auto dest!: par_qmsg_oreachable [OF _ assms(5,2-4)])
with assms(1) show "global P (σ, ζ)"
by (auto dest: oinvariant_weakenD [OF assms(1)])
qed
lemma lift_step_into_qmsg:
assumes inv: "A ⊨⇩A (otherwith S {i} (orecvmsg R), other U {i} →) globala P"
and ustutter: "⋀ξ. U ξ ξ"
and sgivesu: "⋀ξ ξ'. S ξ ξ' ⟹ U ξ ξ'"
and upreservesq: "⋀σ σ' m. ⟦ ∀j. U (σ j) (σ' j); R σ m ⟧ ⟹ R σ' m"
and self_sync: "A ⊨⇩A (otherwith S {i} (orecvmsg R), other U {i} →)
globala (λ(σ, _, σ'). U (σ i) (σ' i))"
and recv_stutter: "⋀σ σ' m. ⟦ ∀j. U (σ j) (σ' j); σ' i = σ i ⟧ ⟹ P (σ, receive m, σ')"
and receive_right: "⋀σ σ' m. P (σ, receive m, σ') ⟹ P (σ, τ, σ')"
shows "A ⟨⟨⇘i⇙ qmsg ⊨⇩A (otherwith S {i} (orecvmsg R), other U {i} →) globala P"
(is "_ ⊨⇩A (?owS, ?U →) _")
proof (rule ostep_invariantI)
fix σ ζ a σ' ζ'
assume or: "(σ, ζ) ∈ oreachable (A ⟨⟨⇘i⇙ qmsg) ?owS ?U"
and otr: "((σ, ζ), a, (σ', ζ')) ∈ trans (A ⟨⟨⇘i⇙ qmsg)"
and "?owS σ σ' a"
from this(2) have "((σ, ζ), a, (σ', ζ')) ∈ oparp_sos i (trans A) (seqp_sos Γ⇩Q⇩M⇩S⇩G)"
by simp
then obtain s msgs q s' msgs' q'
where "ζ = (s, (msgs, q))" "ζ' = (s', (msgs', q'))"
and "((σ, (s, (msgs, q))), a, (σ', (s', (msgs', q'))))
∈ oparp_sos i (trans A) (seqp_sos Γ⇩Q⇩M⇩S⇩G)"
by (metis prod_cases3)
from this(1-2) and or
obtain "(σ, s) ∈ oreachable A ?owS ?U"
"(msgs, q) ∈ reachable qmsg (recvmsg (R σ))"
"(∀m∈set msgs. R σ m)"
by (auto dest: par_qmsg_oreachable [OF _ self_sync ustutter sgivesu]
elim!: upreservesq)
from otr ‹ζ = (s, (msgs, q))› ‹ζ' = (s', (msgs', q'))›
have "((σ, (s, (msgs, q))), a, (σ', (s', (msgs', q'))))
∈ oparp_sos i (trans A) (seqp_sos Γ⇩Q⇩M⇩S⇩G)"
by simp
hence "globala P ((σ, s), a, (σ', s'))"
proof
assume "((σ, s), a, (σ', s')) ∈ trans A"
with ‹(σ, s) ∈ oreachable A ?owS ?U›
show "globala P ((σ, s), a, (σ', s'))"
using ‹?owS σ σ' a› by (rule ostep_invariantD [OF inv])
next
assume "((msgs, q), a, (msgs', q')) ∈ seqp_sos Γ⇩Q⇩M⇩S⇩G"
and "⋀m. a ≠ send m"
and "σ' i = σ i"
from this(3) and ustutter have "U (σ i) (σ' i)" by simp
with ‹?owS σ σ' a› and sgivesu have "∀j. U (σ j) (σ' j)"
by (clarsimp dest!: otherwith_syncD) metis
moreover have "(∃m. a = receive m) ∨ (a = τ)"
proof -
from ‹(msgs, q) ∈ reachable qmsg (recvmsg (R σ))›
have "(msgs, q) ∈ reachable qmsg TT" ..
moreover from ‹((msgs, q), a, (msgs', q')) ∈ seqp_sos Γ⇩Q⇩M⇩S⇩G›
have "((msgs, q), a, (msgs', q')) ∈ trans qmsg" by simp
ultimately show ?thesis
using ‹⋀m. a ≠ send m›
by (auto dest!: step_invariantD [OF qmsg_send_receive_or_tau])
qed
ultimately show "globala P ((σ, s), a, (σ', s'))"
using ‹σ' i = σ i›
by simp (metis receive_right recv_stutter step_seq_tau)
next
fix m
assume "a = τ"
and "((σ, s), receive m, (σ', s')) ∈ trans A"
and "((msgs, q), send m, (msgs', q')) ∈ seqp_sos Γ⇩Q⇩M⇩S⇩G"
from ‹(msgs, q) ∈ reachable qmsg (recvmsg (R σ))›
have "(msgs, q) ∈ reachable qmsg TT" ..
moreover from ‹((msgs, q), send m, (msgs', q')) ∈ seqp_sos Γ⇩Q⇩M⇩S⇩G›
have "((msgs, q), send m, (msgs', q')) ∈ trans qmsg" by simp
ultimately have "m∈set msgs"
by (auto dest!: step_invariantD [OF qmsg_send_from_queue])
with ‹∀m∈set msgs. R σ m› have "R σ m" ..
with ‹?owS σ σ' a› have "?owS σ σ' (receive m)"
by (auto dest!: otherwith_syncD)
with ‹((σ, s), receive m, (σ', s')) ∈ trans A›
have "globala P ((σ, s), receive m, (σ', s'))"
using ‹(σ, s) ∈ oreachable A ?owS ?U›
by - (rule ostep_invariantD [OF inv])
hence "P (σ, receive m, σ')" by simp
hence "P (σ, τ, σ')" by (rule receive_right)
with ‹a = τ› show "globala P ((σ, s), a, (σ', s'))" by simp
qed
with ‹ζ = (s, (msgs, q))› and ‹ζ' = (s', (msgs', q'))› show "globala P ((σ, ζ), a, (σ', ζ'))"
by simp
qed
lemma lift_step_into_qmsg_statelessassm:
assumes "A ⊨⇩A (λσ _. orecvmsg (λ_. R) σ, other (λ_ _. True) {i} →) globala P"
and "⋀σ σ' m. σ' i = σ i ⟹ P (σ, receive m, σ')"
and "⋀σ σ' m. P (σ, receive m, σ') ⟹ P (σ, τ, σ')"
shows "A ⟨⟨⇘i⇙ qmsg ⊨⇩A (λσ _. orecvmsg (λ_. R) σ, other (λ_ _. True) {i} →) globala P"
proof -
from assms(1) have *: "A ⊨⇩A (otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)),
other (λ_ _. True) {i} →) globala P"
by rule auto
hence "A ⟨⟨⇘i⇙ qmsg ⊨⇩A
(otherwith (λ_ _. True) {i} (orecvmsg (λ_. R)), other (λ_ _. True) {i} →) globala P"
by (rule lift_step_into_qmsg)
(auto elim!: assms(2-3) simp del: step_seq_tau)
thus ?thesis by rule auto
qed
end