[STATEMENT]
lemma subterms_stermsl_ctermsl:
  assumes "q \<in> subterms p"
      and "r \<in> stermsl q"
    shows "r \<in> ctermsl p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> ctermsl p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
q \<in> subterms p
r \<in> stermsl q

goal (1 subgoal):
 1. r \<in> ctermsl p
[PROOF STEP]
proof (induct p)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}\<langle>x2\<rangle>
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}\<langle>x2\<rangle>
p)
 2. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}\<lbrakk>x2\<rbrakk>
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}\<lbrakk>x2\<rbrakk>
p)
 3. \<And>p1 p2. \<lbrakk>\<lbrakk>q \<in> subterms p1; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> subterms p2; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> subterms (p1
\<oplus>
p2); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>\<lbrakk>q \<in> subterms p1; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> subterms p2; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> subterms ({x1}unicast(x2, x3) .
p1 \<triangleright> p2); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2)
 5. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}broadcast(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}broadcast(x2) .
p)
 6. \<And>x1 x2 x3 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}groupcast(x2, x3) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}groupcast(x2, x3) .
p)
 7. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}send(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}send(x2) .
p)
 8. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}deliver(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}deliver(x2) .
p)
 9. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}receive(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}receive(x2) .
p)
 10. \<And>x. \<lbrakk>q \<in> subterms (call(x)); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (call(x))
[PROOF STEP]
fix p1 p2
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}\<langle>x2\<rangle>
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}\<langle>x2\<rangle>
p)
 2. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}\<lbrakk>x2\<rbrakk>
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}\<lbrakk>x2\<rbrakk>
p)
 3. \<And>p1 p2. \<lbrakk>\<lbrakk>q \<in> subterms p1; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> subterms p2; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> subterms (p1
\<oplus>
p2); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>\<lbrakk>q \<in> subterms p1; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> subterms p2; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> subterms ({x1}unicast(x2, x3) .
p1 \<triangleright> p2); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2)
 5. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}broadcast(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}broadcast(x2) .
p)
 6. \<And>x1 x2 x3 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}groupcast(x2, x3) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}groupcast(x2, x3) .
p)
 7. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}send(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}send(x2) .
p)
 8. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}deliver(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}deliver(x2) .
p)
 9. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}receive(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}receive(x2) .
p)
 10. \<And>x. \<lbrakk>q \<in> subterms (call(x)); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (call(x))
[PROOF STEP]
assume IH1: "q \<in> subterms p1 \<Longrightarrow> r \<in> stermsl q \<Longrightarrow> r \<in> ctermsl p1"
       and IH2: "q \<in> subterms p2 \<Longrightarrow> r \<in> stermsl q \<Longrightarrow> r \<in> ctermsl p2"
       and *: "q \<in> subterms (p1 \<oplus> p2)"
       and "r \<in> stermsl q"
[PROOF STATE]
proof (state)
this:
\<lbrakk>q \<in> subterms p1; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1
\<lbrakk>q \<in> subterms p2; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2
q \<in> subterms (p1
\<oplus>
p2)
r \<in> stermsl q

goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}\<langle>x2\<rangle>
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}\<langle>x2\<rangle>
p)
 2. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}\<lbrakk>x2\<rbrakk>
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}\<lbrakk>x2\<rbrakk>
p)
 3. \<And>p1 p2. \<lbrakk>\<lbrakk>q \<in> subterms p1; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> subterms p2; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> subterms (p1
\<oplus>
p2); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>\<lbrakk>q \<in> subterms p1; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> subterms p2; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> subterms ({x1}unicast(x2, x3) .
p1 \<triangleright> p2); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2)
 5. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}broadcast(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}broadcast(x2) .
p)
 6. \<And>x1 x2 x3 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}groupcast(x2, x3) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}groupcast(x2, x3) .
p)
 7. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}send(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}send(x2) .
p)
 8. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}deliver(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}deliver(x2) .
p)
 9. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}receive(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}receive(x2) .
p)
 10. \<And>x. \<lbrakk>q \<in> subterms (call(x)); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (call(x))
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
q \<in> subterms (p1
\<oplus>
p2)
[PROOF STEP]
have "q \<in> {p1 \<oplus> p2} \<union> subterms p1 \<union> subterms p2"
[PROOF STATE]
proof (prove)
using this:
q \<in> subterms (p1
\<oplus>
p2)

goal (1 subgoal):
 1. q \<in> {p1
\<oplus>
p2} \<union> subterms p1 \<union> subterms p2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q \<in> {p1
\<oplus>
p2} \<union> subterms p1 \<union> subterms p2

goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}\<langle>x2\<rangle>
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}\<langle>x2\<rangle>
p)
 2. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}\<lbrakk>x2\<rbrakk>
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}\<lbrakk>x2\<rbrakk>
p)
 3. \<And>p1 p2. \<lbrakk>\<lbrakk>q \<in> subterms p1; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> subterms p2; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> subterms (p1
\<oplus>
p2); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>\<lbrakk>q \<in> subterms p1; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> subterms p2; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> subterms ({x1}unicast(x2, x3) .
p1 \<triangleright> p2); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2)
 5. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}broadcast(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}broadcast(x2) .
p)
 6. \<And>x1 x2 x3 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}groupcast(x2, x3) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}groupcast(x2, x3) .
p)
 7. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}send(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}send(x2) .
p)
 8. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}deliver(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}deliver(x2) .
p)
 9. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}receive(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}receive(x2) .
p)
 10. \<And>x. \<lbrakk>q \<in> subterms (call(x)); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (call(x))
[PROOF STEP]
thus "r \<in> ctermsl (p1 \<oplus> p2)"
[PROOF STATE]
proof (prove)
using this:
q \<in> {p1
\<oplus>
p2} \<union> subterms p1 \<union> subterms p2

goal (1 subgoal):
 1. r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
proof (elim UnE)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. q \<in> {p1
\<oplus>
p2} \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 2. q \<in> subterms p1 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 3. q \<in> subterms p2 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
assume "q \<in> {p1 \<oplus> p2}"
[PROOF STATE]
proof (state)
this:
q \<in> {p1
\<oplus>
p2}

goal (3 subgoals):
 1. q \<in> {p1
\<oplus>
p2} \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 2. q \<in> subterms p1 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 3. q \<in> subterms p2 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
with \<open>r \<in> stermsl q\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<in> stermsl q
q \<in> {p1
\<oplus>
p2}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<in> stermsl q
q \<in> {p1
\<oplus>
p2}

goal (1 subgoal):
 1. r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
by simp (metis stermsl_ctermsl)
[PROOF STATE]
proof (state)
this:
r \<in> ctermsl (p1
\<oplus>
p2)

goal (2 subgoals):
 1. q \<in> subterms p1 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 2. q \<in> subterms p2 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q \<in> subterms p1 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 2. q \<in> subterms p2 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
assume "q \<in> subterms p1"
[PROOF STATE]
proof (state)
this:
q \<in> subterms p1

goal (2 subgoals):
 1. q \<in> subterms p1 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 2. q \<in> subterms p2 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
hence "r \<in> ctermsl p1"
[PROOF STATE]
proof (prove)
using this:
q \<in> subterms p1

goal (1 subgoal):
 1. r \<in> ctermsl p1
[PROOF STEP]
using \<open>r \<in> stermsl q\<close>
[PROOF STATE]
proof (prove)
using this:
q \<in> subterms p1
r \<in> stermsl q

goal (1 subgoal):
 1. r \<in> ctermsl p1
[PROOF STEP]
by (rule IH1)
[PROOF STATE]
proof (state)
this:
r \<in> ctermsl p1

goal (2 subgoals):
 1. q \<in> subterms p1 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
 2. q \<in> subterms p2 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<in> ctermsl p1

goal (1 subgoal):
 1. r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r \<in> ctermsl (p1
\<oplus>
p2)

goal (1 subgoal):
 1. q \<in> subterms p2 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> subterms p2 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
assume "q \<in> subterms p2"
[PROOF STATE]
proof (state)
this:
q \<in> subterms p2

goal (1 subgoal):
 1. q \<in> subterms p2 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
hence "r \<in> ctermsl p2"
[PROOF STATE]
proof (prove)
using this:
q \<in> subterms p2

goal (1 subgoal):
 1. r \<in> ctermsl p2
[PROOF STEP]
using \<open>r \<in> stermsl q\<close>
[PROOF STATE]
proof (prove)
using this:
q \<in> subterms p2
r \<in> stermsl q

goal (1 subgoal):
 1. r \<in> ctermsl p2
[PROOF STEP]
by (rule IH2)
[PROOF STATE]
proof (state)
this:
r \<in> ctermsl p2

goal (1 subgoal):
 1. q \<in> subterms p2 \<Longrightarrow> r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
r \<in> ctermsl p2

goal (1 subgoal):
 1. r \<in> ctermsl (p1
\<oplus>
p2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r \<in> ctermsl (p1
\<oplus>
p2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
r \<in> ctermsl (p1
\<oplus>
p2)

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}\<langle>x2\<rangle>
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}\<langle>x2\<rangle>
p)
 2. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}\<lbrakk>x2\<rbrakk>
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}\<lbrakk>x2\<rbrakk>
p)
 3. \<And>x1 x2 x3 p1 p2. \<lbrakk>\<lbrakk>q \<in> subterms p1; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p1; \<lbrakk>q \<in> subterms p2; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p2; q \<in> subterms ({x1}unicast(x2, x3) .
p1 \<triangleright> p2); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}unicast(x2, x3) .
p1 \<triangleright> p2)
 4. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}broadcast(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}broadcast(x2) .
p)
 5. \<And>x1 x2 x3 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}groupcast(x2, x3) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}groupcast(x2, x3) .
p)
 6. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}send(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}send(x2) .
p)
 7. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}deliver(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}deliver(x2) .
p)
 8. \<And>x1 x2 p. \<lbrakk>\<lbrakk>q \<in> subterms p; r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl p; q \<in> subterms ({x1}receive(x2) .
p); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl ({x1}receive(x2) .
p)
 9. \<And>x. \<lbrakk>q \<in> subterms (call(x)); r \<in> stermsl q\<rbrakk> \<Longrightarrow> r \<in> ctermsl (call(x))
[PROOF STEP]
qed auto


[STATEMENT]
lemma subterms_sterms_cterms:
  assumes wf: "wellformed \<Gamma>"
      and "p \<in> subterms (\<Gamma> pn)"
    shows "sterms \<Gamma> p \<subseteq> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sterms \<Gamma> p \<subseteq> cterms \<Gamma>
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
p \<in> subterms (\<Gamma> pn)

goal (1 subgoal):
 1. sterms \<Gamma> p \<subseteq> cterms \<Gamma>
[PROOF STEP]
proof (induct p)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
 10. \<And>x. call(x) \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> (call(x)) \<subseteq> cterms \<Gamma>
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
 10. \<And>x. call(x) \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> (call(x)) \<subseteq> cterms \<Gamma>
[PROOF STEP]
assume "call(p) \<in> subterms (\<Gamma> pn)"
[PROOF STATE]
proof (state)
this:
call(p) \<in> subterms (\<Gamma> pn)

goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
 10. \<And>x. call(x) \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> (call(x)) \<subseteq> cterms \<Gamma>
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wellformed \<Gamma>
[PROOF STEP]
have "sterms \<Gamma> (call(p)) = sterms \<Gamma> (\<Gamma> p)"
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>

goal (1 subgoal):
 1. sterms \<Gamma> (call(p)) = sterms \<Gamma> (\<Gamma> p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> (call(p)) = sterms \<Gamma> (\<Gamma> p)

goal (10 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
 10. \<And>x. call(x) \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> (call(x)) \<subseteq> cterms \<Gamma>
[PROOF STEP]
thus "sterms \<Gamma> (call(p)) \<subseteq> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> (call(p)) = sterms \<Gamma> (\<Gamma> p)

goal (1 subgoal):
 1. sterms \<Gamma> (call(p)) \<subseteq> cterms \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> (call(p)) \<subseteq> cterms \<Gamma>

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
[PROOF STEP]
fix p1 p2
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
[PROOF STEP]
assume IH1: "p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>"
       and IH2: "p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>"
       and *: "p1 \<oplus> p2 \<in> subterms (\<Gamma> pn)"
[PROOF STATE]
proof (state)
this:
p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>
p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>
p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)
[PROOF STEP]
have "p1 \<in> subterms (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)

goal (1 subgoal):
 1. p1 \<in> subterms (\<Gamma> pn)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p1 \<in> subterms (\<Gamma> pn)

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
[PROOF STEP]
hence "sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
p1 \<in> subterms (\<Gamma> pn)

goal (1 subgoal):
 1. sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>
[PROOF STEP]
by (rule IH1)
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)
[PROOF STEP]
have "p2 \<in> subterms (\<Gamma> pn)"
[PROOF STATE]
proof (prove)
using this:
p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)

goal (1 subgoal):
 1. p2 \<in> subterms (\<Gamma> pn)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p2 \<in> subterms (\<Gamma> pn)

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
[PROOF STEP]
hence "sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
p2 \<in> subterms (\<Gamma> pn)

goal (1 subgoal):
 1. sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>
[PROOF STEP]
by (rule IH2)
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>

goal (9 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; p1
\<oplus>
p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 9. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>
sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>
[PROOF STEP]
show "sterms \<Gamma> (p1 \<oplus> p2 ) \<subseteq> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>
sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>

goal (1 subgoal):
 1. sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>
sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>
wellformed \<Gamma>

goal (1 subgoal):
 1. sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sterms \<Gamma> (p1
\<oplus>
p2) \<subseteq> cterms \<Gamma>

goal (8 subgoals):
 1. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<langle>x2\<rangle>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<langle>x2\<rangle>
p) \<subseteq> cterms \<Gamma>
 2. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}\<lbrakk>x2\<rbrakk>
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}\<lbrakk>x2\<rbrakk>
p) \<subseteq> cterms \<Gamma>
 3. \<And>x1 x2 x3 p1 p2. \<lbrakk>p1 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p1 \<subseteq> cterms \<Gamma>; p2 \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p2 \<subseteq> cterms \<Gamma>; {x1}unicast(x2, x3) .
p1 \<triangleright> p2 \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}unicast(x2, x3) .
p1 \<triangleright> p2) \<subseteq> cterms \<Gamma>
 4. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}broadcast(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}broadcast(x2) .
p) \<subseteq> cterms \<Gamma>
 5. \<And>x1 x2 x3 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}groupcast(x2, x3) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}groupcast(x2, x3) .
p) \<subseteq> cterms \<Gamma>
 6. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}send(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}send(x2) .
p) \<subseteq> cterms \<Gamma>
 7. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}deliver(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}deliver(x2) .
p) \<subseteq> cterms \<Gamma>
 8. \<And>x1 x2 p. \<lbrakk>p \<in> subterms (\<Gamma> pn) \<Longrightarrow> sterms \<Gamma> p \<subseteq> cterms \<Gamma>; {x1}receive(x2) .
p \<in> subterms (\<Gamma> pn)\<rbrakk> \<Longrightarrow> sterms \<Gamma> ({x1}receive(x2) .
p) \<subseteq> cterms \<Gamma>
[PROOF STEP]
qed (auto elim!: subterms_in_cterms [OF \<open>wellformed \<Gamma>\<close>])


[STATEMENT]
lemma subterms_sterms_in_cterms:
  assumes "wellformed \<Gamma>"
      and "p \<in> subterms (\<Gamma> pn)"
      and "q \<in> sterms \<Gamma> p"
    shows "q \<in> cterms \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> cterms \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellformed \<Gamma>
p \<in> subterms (\<Gamma> pn)
q \<in> sterms \<Gamma> p

goal (1 subgoal):
 1. q \<in> cterms \<Gamma>
[PROOF STEP]
by (auto dest!: subterms_sterms_cterms [OF \<open>wellformed \<Gamma>\<close>])


[STATEMENT]
lemma intf_of_assnI: "intf_of_assn R TYPE('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intf_of_assn R TYPE('a)
[PROOF STEP]
by simp


[STATEMENT]
lemma intf_of_assn_fallback: "intf_of_assn (R :: 'a \<Rightarrow> _ \<Rightarrow> assn) TYPE('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. intf_of_assn R TYPE('a)
[PROOF STEP]
by simp


[STATEMENT]
lemma rel2p_fref[rel2p]: "rel2p (fref P R S)
    = (\<lambda>f g. (\<forall>x y. P y \<longrightarrow> rel2p R x y \<longrightarrow> rel2p S (f x) (g y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel2p ([P]\<^sub>f R \<rightarrow> S) = (\<lambda>f g. \<forall>x y. P y \<longrightarrow> rel2p R x y \<longrightarrow> rel2p S (f x) (g y))
[PROOF STEP]
by (auto simp: fref_def rel2p_def[abs_def])


[STATEMENT]
lemma fref_cons:
    assumes "(f,g) \<in> [P]\<^sub>f R \<rightarrow> S"
    assumes "\<And>c a. (c,a)\<in>R' \<Longrightarrow> Q a \<Longrightarrow> P a"
    assumes "R' \<subseteq> R"
    assumes "S \<subseteq> S'"
    shows "(f,g) \<in> [Q]\<^sub>f R' \<rightarrow> S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> [Q]\<^sub>f R' \<rightarrow> S'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> [P]\<^sub>f R \<rightarrow> S
\<lbrakk>(?c, ?a) \<in> R'; Q ?a\<rbrakk> \<Longrightarrow> P ?a
R' \<subseteq> R
S \<subseteq> S'

goal (1 subgoal):
 1. (f, g) \<in> [Q]\<^sub>f R' \<rightarrow> S'
[PROOF STEP]
unfolding fref_def
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> {(f, g). \<forall>x y. P y \<and> (x, y) \<in> R \<longrightarrow> (f x, g y) \<in> S}
\<lbrakk>(?c, ?a) \<in> R'; Q ?a\<rbrakk> \<Longrightarrow> P ?a
R' \<subseteq> R
S \<subseteq> S'

goal (1 subgoal):
 1. (f, g) \<in> {(f, g). \<forall>x y. Q y \<and> (x, y) \<in> R' \<longrightarrow> (f x, g y) \<in> S'}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma frefI[intro?]:
    assumes "\<And>x y. \<lbrakk>P y; (x,y)\<in>R\<rbrakk> \<Longrightarrow> (f x, g y)\<in>S"
    shows "(f,g)\<in>fref P R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> [P]\<^sub>f R \<rightarrow> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P ?y; (?x, ?y) \<in> R\<rbrakk> \<Longrightarrow> (f ?x, g ?y) \<in> S

goal (1 subgoal):
 1. (f, g) \<in> [P]\<^sub>f R \<rightarrow> S
[PROOF STEP]
unfolding fref_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>P ?y; (?x, ?y) \<in> R\<rbrakk> \<Longrightarrow> (f ?x, g ?y) \<in> S

goal (1 subgoal):
 1. (f, g) \<in> {(f, g). \<forall>x y. P y \<and> (x, y) \<in> R \<longrightarrow> (f x, g y) \<in> S}
[PROOF STEP]
by auto


[STATEMENT]
lemma fref_ncI: "(f,g)\<in>R\<rightarrow>S \<Longrightarrow> (f,g)\<in>R\<rightarrow>\<^sub>fS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> R \<rightarrow> S \<Longrightarrow> (f, g) \<in> R \<rightarrow>\<^sub>f S
[PROOF STEP]
apply (rule frefI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(f, g) \<in> R \<rightarrow> S; True; (x, y) \<in> R\<rbrakk> \<Longrightarrow> (f x, g y) \<in> S
[PROOF STEP]
apply parametricity
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma frefD:
    assumes "(f,g)\<in>fref P R S"
    shows "\<lbrakk>P y; (x,y)\<in>R\<rbrakk> \<Longrightarrow> (f x, g y)\<in>S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P y; (x, y) \<in> R\<rbrakk> \<Longrightarrow> (f x, g y) \<in> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> [P]\<^sub>f R \<rightarrow> S

goal (1 subgoal):
 1. \<lbrakk>P y; (x, y) \<in> R\<rbrakk> \<Longrightarrow> (f x, g y) \<in> S
[PROOF STEP]
unfolding fref_def
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> {(f, g). \<forall>x y. P y \<and> (x, y) \<in> R \<longrightarrow> (f x, g y) \<in> S}

goal (1 subgoal):
 1. \<lbrakk>P y; (x, y) \<in> R\<rbrakk> \<Longrightarrow> (f x, g y) \<in> S
[PROOF STEP]
by auto


[STATEMENT]
lemma fref_ncD: "(f,g)\<in>R\<rightarrow>\<^sub>fS \<Longrightarrow> (f,g)\<in>R\<rightarrow>S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> R \<rightarrow>\<^sub>f S \<Longrightarrow> (f, g) \<in> R \<rightarrow> S
[PROOF STEP]
apply (rule fun_relI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. \<lbrakk>(f, g) \<in> R \<rightarrow>\<^sub>f S; (a, a') \<in> R\<rbrakk> \<Longrightarrow> (f a, g a') \<in> S
[PROOF STEP]
apply (drule frefD)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a a'. (a, a') \<in> R \<Longrightarrow> True
 2. \<And>a a'. (a, a') \<in> R \<Longrightarrow> (?x2 a a', ?y2 a a') \<in> R
 3. \<And>a a'. \<lbrakk>(a, a') \<in> R; (f (?x2 a a'), g (?y2 a a')) \<in> S\<rbrakk> \<Longrightarrow> (f a, g a') \<in> S
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a'. (a, a') \<in> R \<Longrightarrow> (?x2 a a', ?y2 a a') \<in> R
 2. \<And>a a'. \<lbrakk>(a, a') \<in> R; (f (?x2 a a'), g (?y2 a a')) \<in> S\<rbrakk> \<Longrightarrow> (f a, g a') \<in> S
[PROOF STEP]
apply assumption+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fref_compI:
    "fref P R1 R2 O fref Q S1 S2 \<subseteq>
      fref (\<lambda>x. Q x \<and> (\<forall>y. (y,x)\<in>S1 \<longrightarrow> P y)) (R1 O S1) (R2 O S2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([P]\<^sub>f R1 \<rightarrow> R2) O ([Q]\<^sub>f S1 \<rightarrow> S2) \<subseteq> [\<lambda>x. Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> P y)]\<^sub>f R1 O S1 \<rightarrow> R2 O S2
[PROOF STEP]
unfolding fref_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(f, g). \<forall>x y. P y \<and> (x, y) \<in> R1 \<longrightarrow> (f x, g y) \<in> R2} O {(f, g). \<forall>x y. Q y \<and> (x, y) \<in> S1 \<longrightarrow> (f x, g y) \<in> S2} \<subseteq> {(f, g). \<forall>x y. (Q y \<and> (\<forall>ya. (ya, y) \<in> S1 \<longrightarrow> P ya)) \<and> (x, y) \<in> R1 O S1 \<longrightarrow> (f x, g y) \<in> R2 O S2}
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z xb yb za. \<lbrakk>\<forall>xa ya. P ya \<and> (xa, ya) \<in> R1 \<longrightarrow> (x xa, y ya) \<in> R2; \<forall>x ya. Q ya \<and> (x, ya) \<in> S1 \<longrightarrow> (y x, z ya) \<in> S2; Q za; \<forall>y. (y, za) \<in> S1 \<longrightarrow> P y; (xb, yb) \<in> R1; (yb, za) \<in> S1\<rbrakk> \<Longrightarrow> (x xb, z za) \<in> R2 O S2
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fref_compI':
    "\<lbrakk> (f,g)\<in>fref P R1 R2; (g,h)\<in>fref Q S1 S2 \<rbrakk>
      \<Longrightarrow> (f,h) \<in> fref (\<lambda>x. Q x \<and> (\<forall>y. (y,x)\<in>S1 \<longrightarrow> P y)) (R1 O S1) (R2 O S2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(f, g) \<in> [P]\<^sub>f R1 \<rightarrow> R2; (g, h) \<in> [Q]\<^sub>f S1 \<rightarrow> S2\<rbrakk> \<Longrightarrow> (f, h) \<in> [\<lambda>x. Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> P y)]\<^sub>f R1 O S1 \<rightarrow> R2 O S2
[PROOF STEP]
using fref_compI[of P R1 R2 Q S1 S2]
[PROOF STATE]
proof (prove)
using this:
([P]\<^sub>f R1 \<rightarrow> R2) O ([Q]\<^sub>f S1 \<rightarrow> S2) \<subseteq> [\<lambda>x. Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> P y)]\<^sub>f R1 O S1 \<rightarrow> R2 O S2

goal (1 subgoal):
 1. \<lbrakk>(f, g) \<in> [P]\<^sub>f R1 \<rightarrow> R2; (g, h) \<in> [Q]\<^sub>f S1 \<rightarrow> S2\<rbrakk> \<Longrightarrow> (f, h) \<in> [\<lambda>x. Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> P y)]\<^sub>f R1 O S1 \<rightarrow> R2 O S2
[PROOF STEP]
by auto


[STATEMENT]
lemma fref_unit_conv:
    "(\<lambda>_. c, \<lambda>_. a) \<in> fref P unit_rel S \<longleftrightarrow> (P () \<longrightarrow> (c,a)\<in>S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>_. c, \<lambda>_. a) \<in> [P]\<^sub>f unit_rel \<rightarrow> S) = (P () \<longrightarrow> (c, a) \<in> S)
[PROOF STEP]
by (auto simp: fref_def)


[STATEMENT]
lemma fref_uncurry_conv:
    "(uncurry c, uncurry a) \<in> fref P (R1\<times>\<^sub>rR2) S
    \<longleftrightarrow> (\<forall>x1 y1 x2 y2. P (y1,y2) \<longrightarrow> (x1,y1)\<in>R1 \<longrightarrow> (x2,y2)\<in>R2 \<longrightarrow> (c x1 x2, a y1 y2) \<in> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((uncurry c, uncurry a) \<in> [P]\<^sub>f R1 \<times>\<^sub>r R2 \<rightarrow> S) = (\<forall>x1 y1 x2 y2. P (y1, y2) \<longrightarrow> (x1, y1) \<in> R1 \<longrightarrow> (x2, y2) \<in> R2 \<longrightarrow> (c x1 x2, a y1 y2) \<in> S)
[PROOF STEP]
by (auto simp: fref_def)


[STATEMENT]
lemma fref_mono: "\<lbrakk> \<And>x. P' x \<Longrightarrow> P x; R' \<subseteq> R; S \<subseteq> S' \<rbrakk>
    \<Longrightarrow> fref P R S \<subseteq> fref P' R' S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. P' x \<Longrightarrow> P x; R' \<subseteq> R; S \<subseteq> S'\<rbrakk> \<Longrightarrow> [P]\<^sub>f R \<rightarrow> S \<subseteq> [P']\<^sub>f R' \<rightarrow> S'
[PROOF STEP]
unfolding fref_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. P' x \<Longrightarrow> P x; R' \<subseteq> R; S \<subseteq> S'\<rbrakk> \<Longrightarrow> {(f, g). \<forall>x y. P y \<and> (x, y) \<in> R \<longrightarrow> (f x, g y) \<in> S} \<subseteq> {(f, g). \<forall>x y. P' y \<and> (x, y) \<in> R' \<longrightarrow> (f x, g y) \<in> S'}
[PROOF STEP]
by auto blast


[STATEMENT]
lemma fref_composeI:
    assumes FR1: "(f,g)\<in>fref P R1 R2"
    assumes FR2: "(g,h)\<in>fref Q S1 S2"
    assumes C1: "\<And>x. P' x \<Longrightarrow> Q x"
    assumes C2: "\<And>x y. \<lbrakk>P' x; (y,x)\<in>S1\<rbrakk> \<Longrightarrow> P y"
    assumes R1: "R' \<subseteq> R1 O S1"
    assumes R2: "R2 O S2 \<subseteq> S'"
    assumes FH: "f'=f" "h'=h"
    shows "(f',h') \<in> fref P' R' S'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f', h') \<in> [P']\<^sub>f R' \<rightarrow> S'
[PROOF STEP]
unfolding FH
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, h) \<in> [P']\<^sub>f R' \<rightarrow> S'
[PROOF STEP]
apply (rule subsetD[OF fref_mono fref_compI'[OF FR1 FR2]])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. P' x \<Longrightarrow> Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> P y)
 2. R' \<subseteq> R1 O S1
 3. R2 O S2 \<subseteq> S'
[PROOF STEP]
using C1 C2
[PROOF STATE]
proof (prove)
using this:
P' ?x \<Longrightarrow> Q ?x
\<lbrakk>P' ?x; (?y, ?x) \<in> S1\<rbrakk> \<Longrightarrow> P ?y

goal (3 subgoals):
 1. \<And>x. P' x \<Longrightarrow> Q x \<and> (\<forall>y. (y, x) \<in> S1 \<longrightarrow> P y)
 2. R' \<subseteq> R1 O S1
 3. R2 O S2 \<subseteq> S'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. R' \<subseteq> R1 O S1
 2. R2 O S2 \<subseteq> S'
[PROOF STEP]
using R1
[PROOF STATE]
proof (prove)
using this:
R' \<subseteq> R1 O S1

goal (2 subgoals):
 1. R' \<subseteq> R1 O S1
 2. R2 O S2 \<subseteq> S'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2 O S2 \<subseteq> S'
[PROOF STEP]
using R2
[PROOF STATE]
proof (prove)
using this:
R2 O S2 \<subseteq> S'

goal (1 subgoal):
 1. R2 O S2 \<subseteq> S'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fref_triv: "A\<subseteq>Id \<Longrightarrow> (f,f)\<in>[P]\<^sub>f A \<rightarrow> Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> Id \<Longrightarrow> (f, f) \<in> [P]\<^sub>f A \<rightarrow> Id
[PROOF STEP]
by (auto simp: fref_def)


[STATEMENT]
lemma hfrefI[intro?]:
    assumes "\<And>c a. P a \<Longrightarrow> hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)"
    shows "(f,g)\<in>hfref P RS T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, g) \<in> [P]\<^sub>a RS \<rightarrow> T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P ?a \<Longrightarrow> hn_refine (fst RS ?a ?c) (f ?c) (snd RS ?a ?c) T (g ?a)

goal (1 subgoal):
 1. (f, g) \<in> [P]\<^sub>a RS \<rightarrow> T
[PROOF STEP]
unfolding hfref_def
[PROOF STATE]
proof (prove)
using this:
P ?a \<Longrightarrow> hn_refine (fst RS ?a ?c) (f ?c) (snd RS ?a ?c) T (g ?a)

goal (1 subgoal):
 1. (f, g) \<in> {(f, g). \<forall>c a. P a \<longrightarrow> hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)}
[PROOF STEP]
by blast


[STATEMENT]
lemma hfrefD:
    assumes "(f,g)\<in>hfref P RS T"
    shows "\<And>c a. P a \<Longrightarrow> hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a. P a \<Longrightarrow> hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> [P]\<^sub>a RS \<rightarrow> T

goal (1 subgoal):
 1. \<And>c a. P a \<Longrightarrow> hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)
[PROOF STEP]
unfolding hfref_def
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> {(f, g). \<forall>c a. P a \<longrightarrow> hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)}

goal (1 subgoal):
 1. \<And>c a. P a \<Longrightarrow> hn_refine (fst RS a c) (f c) (snd RS a c) T (g a)
[PROOF STEP]
by blast


[STATEMENT]
lemma hfref_to_ASSERT_conv:
    "NO_MATCH (\<lambda>_. True) P \<Longrightarrow> (a,b)\<in>[P]\<^sub>a R \<rightarrow> S \<longleftrightarrow> (a,\<lambda>x. ASSERT (P x) \<then> b x) \<in> R \<rightarrow>\<^sub>a S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NO_MATCH (\<lambda>_. True) P \<Longrightarrow> ((a, b) \<in> [P]\<^sub>a R \<rightarrow> S) = ((a, \<lambda>x. ASSERT (P x) \<bind> (\<lambda>_. b x)) \<in> R \<rightarrow>\<^sub>a S)
[PROOF STEP]
unfolding hfref_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NO_MATCH (\<lambda>_. True) P \<Longrightarrow> ((a, b) \<in> {(f, g). \<forall>c a. P a \<longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (g a)}) = ((a, \<lambda>x. ASSERT (P x) \<bind> (\<lambda>_. b x)) \<in> {(f, g). \<forall>c a. True \<longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (g a)})
[PROOF STEP]
apply (clarsimp; safe; clarsimp?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c aa. \<forall>c aa. P aa \<longrightarrow> hn_refine (fst R aa c) (a c) (snd R aa c) S (b aa) \<Longrightarrow> hn_refine (fst R aa c) (a c) (snd R aa c) S (ASSERT (P aa) \<bind> (\<lambda>_. b aa))
 2. \<And>c aa. \<lbrakk>\<forall>c aa. hn_refine (fst R aa c) (a c) (snd R aa c) S (ASSERT (P aa) \<bind> (\<lambda>_. b aa)); P aa\<rbrakk> \<Longrightarrow> hn_refine (fst R aa c) (a c) (snd R aa c) S (b aa)
[PROOF STEP]
apply (rule hn_refine_nofailI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c aa. \<lbrakk>\<forall>c aa. P aa \<longrightarrow> hn_refine (fst R aa c) (a c) (snd R aa c) S (b aa); nofail (ASSERT (P aa) \<bind> (\<lambda>_. b aa))\<rbrakk> \<Longrightarrow> hn_refine (fst R aa c) (a c) (snd R aa c) S (ASSERT (P aa) \<bind> (\<lambda>_. b aa))
 2. \<And>c aa. \<lbrakk>\<forall>c aa. hn_refine (fst R aa c) (a c) (snd R aa c) S (ASSERT (P aa) \<bind> (\<lambda>_. b aa)); P aa\<rbrakk> \<Longrightarrow> hn_refine (fst R aa c) (a c) (snd R aa c) S (b aa)
[PROOF STEP]
apply (simp add: refine_pw_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c aa. \<lbrakk>\<forall>c aa. hn_refine (fst R aa c) (a c) (snd R aa c) S (ASSERT (P aa) \<bind> (\<lambda>_. b aa)); P aa\<rbrakk> \<Longrightarrow> hn_refine (fst R aa c) (a c) (snd R aa c) S (b aa)
[PROOF STEP]
subgoal for xc xa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>c aa. hn_refine (fst R aa c) (a c) (snd R aa c) S (ASSERT (P aa) \<bind> (\<lambda>_. b aa)); P xa\<rbrakk> \<Longrightarrow> hn_refine (fst R xa xc) (a xc) (snd R xa xc) S (b xa)
[PROOF STEP]
apply (drule spec[of _ xc])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P xa; \<forall>aa. hn_refine (fst R aa xc) (a xc) (snd R aa xc) S (ASSERT (P aa) \<bind> (\<lambda>_. b aa))\<rbrakk> \<Longrightarrow> hn_refine (fst R xa xc) (a xc) (snd R xa xc) S (b xa)
[PROOF STEP]
apply (drule spec[of _ xa])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P xa; hn_refine (fst R xa xc) (a xc) (snd R xa xc) S (ASSERT (P xa) \<bind> (\<lambda>_. b xa))\<rbrakk> \<Longrightarrow> hn_refine (fst R xa xc) (a xc) (snd R xa xc) S (b xa)
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma keep_drop_sels[simp]:
    "fst (R\<^sup>k) = R"
    "snd (R\<^sup>k) = R"
    "fst (R\<^sup>d) = R"
    "snd (R\<^sup>d) = invalid_assn R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst (R\<^sup>k) = R &&& snd (R\<^sup>k) = R) &&& fst (R\<^sup>d) = R &&& snd (R\<^sup>d) = invalid_assn R
[PROOF STEP]
by auto


[STATEMENT]
lemma hf_pres_fst[simp]: "fst (hf_pres R k) = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (hf_pres R k) = R
[PROOF STEP]
by (cases k) auto


[STATEMENT]
lemma hfprod_fst_snd[simp]:
    "fst (A *\<^sub>a B) = prod_assn (fst A) (fst B)"
    "snd (A *\<^sub>a B) = prod_assn (snd A) (snd B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (A *\<^sub>a B) = fst A \<times>\<^sub>a fst B &&& snd (A *\<^sub>a B) = snd A \<times>\<^sub>a snd B
[PROOF STEP]
unfolding hfprod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (fst A \<times>\<^sub>a fst B, snd A \<times>\<^sub>a snd B) = fst A \<times>\<^sub>a fst B &&& snd (fst A \<times>\<^sub>a fst B, snd A \<times>\<^sub>a snd B) = snd A \<times>\<^sub>a snd B
[PROOF STEP]
by auto


[STATEMENT]
lemma fref_to_pure_hfref':
    assumes "(f,g) \<in> [P]\<^sub>f R\<rightarrow>\<langle>S\<rangle>nres_rel"
    assumes "\<And>x. x\<in>Domain R \<inter> R\<inverse>``Collect P \<Longrightarrow> f x = RETURN (f' x)"
    shows "(return o f', g) \<in> [P]\<^sub>a (pure R)\<^sup>k\<rightarrow>pure S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (return \<circ> f', g) \<in> [P]\<^sub>a (pure R)\<^sup>k \<rightarrow> pure S
[PROOF STEP]
apply (rule hfrefI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a. P a \<Longrightarrow> hn_refine (fst ((pure R)\<^sup>k) a c) ((return \<circ> f') c) (snd ((pure R)\<^sup>k) a c) (pure S) (g a)
[PROOF STEP]
apply (rule hn_refineI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a. \<lbrakk>P a; nofail (g a)\<rbrakk> \<Longrightarrow> <fst ((pure R)\<^sup>k) a c> (return \<circ> f') c <\<lambda>r. snd ((pure R)\<^sup>k) a c * (\<exists>\<^sub>Ax. pure S x r * \<up> (RETURN x \<le> g a))>\<^sub>t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> [P]\<^sub>f R \<rightarrow> \<langle>S\<rangle>nres_rel
?x \<in> Domain R \<inter> R\<inverse> `` Collect P \<Longrightarrow> f ?x = RETURN (f' ?x)

goal (1 subgoal):
 1. \<And>c a. \<lbrakk>P a; nofail (g a)\<rbrakk> \<Longrightarrow> <fst ((pure R)\<^sup>k) a c> (return \<circ> f') c <\<lambda>r. snd ((pure R)\<^sup>k) a c * (\<exists>\<^sub>Ax. pure S x r * \<up> (RETURN x \<le> g a))>\<^sub>t
[PROOF STEP]
apply ((sep_auto simp: fref_def pure_def pw_le_iff pw_nres_rel_iff
      refine_pw_simps eintros del: exI))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c a aa b. \<lbrakk>P a; nofail (g a); \<forall>x y. P y \<and> (x, y) \<in> R \<longrightarrow> nofail (g y) \<longrightarrow> nofail (f x) \<and> (\<forall>xa. inres (f x) xa \<longrightarrow> (\<exists>s'. (xa, s') \<in> S \<and> inres (g y) s')); \<And>x. x \<in> Domain R \<and> x \<in> R\<inverse> `` Collect P \<Longrightarrow> f x = RETURN (f' x); (c, a) \<in> R; (aa, b) \<Turnstile> emp\<rbrakk> \<Longrightarrow> \<exists>x. (f' c, x) \<in> S \<and> inres (g a) x
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hf2hnr:
    assumes "(f,g) \<in> [P]\<^sub>a R \<rightarrow> S"
    shows "\<forall>x xi. P x \<longrightarrow> hn_refine (emp * hn_ctxt (fst R) x xi) (f$xi) (emp * hn_ctxt (snd R) x xi) S (g$x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x xi. P x \<longrightarrow> hn_refine (emp * hn_ctxt (fst R) x xi) (f $ xi) (emp * hn_ctxt (snd R) x xi) S (g $ x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> [P]\<^sub>a R \<rightarrow> S

goal (1 subgoal):
 1. \<forall>x xi. P x \<longrightarrow> hn_refine (emp * hn_ctxt (fst R) x xi) (f $ xi) (emp * hn_ctxt (snd R) x xi) S (g $ x)
[PROOF STEP]
unfolding hfref_def
[PROOF STATE]
proof (prove)
using this:
(f, g) \<in> {(f, g). \<forall>c a. P a \<longrightarrow> hn_refine (fst R a c) (f c) (snd R a c) S (g a)}

goal (1 subgoal):
 1. \<forall>x xi. P x \<longrightarrow> hn_refine (emp * hn_ctxt (fst R) x xi) (f $ xi) (emp * hn_ctxt (snd R) x xi) S (g $ x)
[PROOF STEP]
by (auto simp: hn_ctxt_def)


[STATEMENT]
lemma to_hnr_prod_fst_snd:
    "fst (A *\<^sub>a B) = to_hnr_prod (fst A) (fst B)"
    "snd (A *\<^sub>a B) = to_hnr_prod (snd A) (snd B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (A *\<^sub>a B) = to_hnr_prod (fst A) (fst B) &&& snd (A *\<^sub>a B) = to_hnr_prod (snd A) (snd B)
[PROOF STEP]
unfolding hfprod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (fst A \<times>\<^sub>a fst B, snd A \<times>\<^sub>a snd B) = to_hnr_prod (fst A) (fst B) &&& snd (fst A \<times>\<^sub>a fst B, snd A \<times>\<^sub>a snd B) = to_hnr_prod (snd A) (snd B)
[PROOF STEP]
by auto


[STATEMENT]
lemma hnr_uncurry_unfold: "
    (\<forall>x xi. P x \<longrightarrow>
      hn_refine
        (\<Gamma> * hn_ctxt (to_hnr_prod A B) x xi)
        (fi xi)
        (\<Gamma>' * hn_ctxt (to_hnr_prod A' B') x xi)
        R
        (f x))
\<longleftrightarrow> (\<forall>b bi a ai. P (a,b) \<longrightarrow>
      hn_refine
        (\<Gamma> * hn_ctxt B b bi * hn_ctxt A a ai)
        (fi (ai,bi))
        (\<Gamma>' * hn_ctxt B' b bi * hn_ctxt A' a ai)
        R
        (f (a,b))
    )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x xi. P x \<longrightarrow> hn_refine (\<Gamma> * hn_ctxt (to_hnr_prod A B) x xi) (fi xi) (\<Gamma>' * hn_ctxt (to_hnr_prod A' B') x xi) R (f x)) = (\<forall>b bi a ai. P (a, b) \<longrightarrow> hn_refine (\<Gamma> * hn_ctxt B b bi * hn_ctxt A a ai) (fi (ai, bi)) (\<Gamma>' * hn_ctxt B' b bi * hn_ctxt A' a ai) R (f (a, b)))
[PROOF STEP]
by (auto simp: hn_ctxt_def prod_assn_def star_aci)


[STATEMENT]
lemma hnr_intro_dummy:
    "\<forall>x xi. P x \<longrightarrow> hn_refine (\<Gamma> x xi) (c xi) (\<Gamma>' x xi) R (a x) \<Longrightarrow> \<forall>x xi. P x \<longrightarrow> hn_refine (emp*\<Gamma> x xi) (c xi) (emp*\<Gamma>' x xi) R (a x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x xi. P x \<longrightarrow> hn_refine (\<Gamma> x xi) (c xi) (\<Gamma>' x xi) R (a x) \<Longrightarrow> \<forall>x xi. P x \<longrightarrow> hn_refine (emp * \<Gamma> x xi) (c xi) (emp * \<Gamma>' x xi) R (a x)
[PROOF STEP]
by simp


[STATEMENT]
lemma hn_ctxt_ctxt_fix_conv: "hn_ctxt (hn_ctxt R) = hn_ctxt R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_ctxt (hn_ctxt R) = hn_ctxt R
[PROOF STEP]
by (simp add: hn_ctxt_def[abs_def])


[STATEMENT]
lemma uncurry_APP: "uncurry f$(a,b) = f$a$b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uncurry f $ (a, b) = f $ a $ b
[PROOF STEP]
by auto


[STATEMENT]
lemma norm_RETURN_o:
    "\<And>f. (RETURN o f)$x = (RETURN$(f$x))"
    "\<And>f. (RETURN oo f)$x$y = (RETURN$(f$x$y))"
    "\<And>f. (RETURN ooo f)$x$y$z = (RETURN$(f$x$y$z))"
    "\<And>f. (\<lambda>x. RETURN ooo f x)$x$y$z$a = (RETURN$(f$x$y$z$a))"
    "\<And>f. (\<lambda>x y. RETURN ooo f x y)$x$y$z$a$b = (RETURN$(f$x$y$z$a$b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>f. (RETURN \<circ> f) $ x = RETURN $ (f $ x)) &&& (\<And>f. (RETURN \<circ>\<circ> f) $ x $ y = RETURN $ (f $ x $ y))) &&& (\<And>f. (RETURN \<circ>\<circ>\<circ> f) $ x $ y $ z = RETURN $ (f $ x $ y $ z)) &&& (\<And>f. (\<lambda>x. RETURN \<circ>\<circ>\<circ> f x) $ x $ y $ z $ a = RETURN $ (f $ x $ y $ z $ a)) &&& (\<And>f. (\<lambda>x y. RETURN \<circ>\<circ>\<circ> f x y) $ x $ y $ z $ a $ b = RETURN $ (f $ x $ y $ z $ a $ b))
[PROOF STEP]
by auto


[STATEMENT]
lemma norm_return_o:
    "\<And>f. (return o f)$x = (return$(f$x))"
    "\<And>f. (return oo f)$x$y = (return$(f$x$y))"
    "\<And>f. (return ooo f)$x$y$z = (return$(f$x$y$z))"
    "\<And>f. (\<lambda>x. return ooo f x)$x$y$z$a = (return$(f$x$y$z$a))"
    "\<And>f. (\<lambda>x y. return ooo f x y)$x$y$z$a$b = (return$(f$x$y$z$a$b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>f. (return \<circ> f) $ x = return $ (f $ x)) &&& (\<And>f. (return \<circ>\<circ> f) $ x $ y = return $ (f $ x $ y))) &&& (\<And>f. (return \<circ>\<circ>\<circ> f) $ x $ y $ z = return $ (f $ x $ y $ z)) &&& (\<And>f. (\<lambda>x. return \<circ>\<circ>\<circ> f x) $ x $ y $ z $ a = return $ (f $ x $ y $ z $ a)) &&& (\<And>f. (\<lambda>x y. return \<circ>\<circ>\<circ> f x y) $ x $ y $ z $ a $ b = return $ (f $ x $ y $ z $ a $ b))
[PROOF STEP]
by auto


[STATEMENT]
lemma hn_val_unit_conv_emp[simp]: "hn_val unit_rel x y = emp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_val unit_rel x y = emp
[PROOF STEP]
by (auto simp: hn_ctxt_def pure_def)


[STATEMENT]
lemma pure_unit_rel_eq_empty: "unit_assn x y = emp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unit_assn x y = emp
[PROOF STEP]
by (auto simp: pure_def)


[STATEMENT]
lemma uc_hfprod_sel:
    "fst (A *\<^sub>a B) a c = (case (a,c) of ((a1,a2),(c1,c2)) \<Rightarrow> fst A a1 c1 * fst B a2 c2)"
    "snd (A *\<^sub>a B) a c = (case (a,c) of ((a1,a2),(c1,c2)) \<Rightarrow> snd A a1 c1 * snd B a2 c2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (A *\<^sub>a B) a c = (case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> fst A a1 c1 * fst B a2 c2) &&& snd (A *\<^sub>a B) a c = (case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> snd A a1 c1 * snd B a2 c2)
[PROOF STEP]
unfolding hfprod_def prod_assn_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (\<lambda>a c. case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> fst A a1 c1 * fst B a2 c2, \<lambda>a c. case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> snd A a1 c1 * snd B a2 c2) a c = (case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> fst A a1 c1 * fst B a2 c2) &&& snd (\<lambda>a c. case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> fst A a1 c1 * fst B a2 c2, \<lambda>a c. case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> snd A a1 c1 * snd B a2 c2) a c = (case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> snd A a1 c1 * snd B a2 c2)
[PROOF STEP]
by auto


[STATEMENT]
lemma fref_param1: "R\<rightarrow>S = fref (\<lambda>_. True) R S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<rightarrow> S = R \<rightarrow>\<^sub>f S
[PROOF STEP]
by (auto simp: fref_def fun_relD)


[STATEMENT]
lemma fref_nest: "fref P1 R1 (fref P2 R2 S)
    \<equiv> CURRY (fref (\<lambda>(a,b). P1 a \<and> P2 b) (R1\<times>\<^sub>rR2) S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [P1]\<^sub>f R1 \<rightarrow> [P2]\<^sub>f R2 \<rightarrow> S \<equiv> CURRY ([\<lambda>(a, b). P1 a \<and> P2 b]\<^sub>f R1 \<times>\<^sub>r R2 \<rightarrow> S)
[PROOF STEP]
apply (rule eq_reflection)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [P1]\<^sub>f R1 \<rightarrow> [P2]\<^sub>f R2 \<rightarrow> S = CURRY ([\<lambda>(a, b). P1 a \<and> P2 b]\<^sub>f R1 \<times>\<^sub>r R2 \<rightarrow> S)
[PROOF STEP]
by (auto simp: fref_def CURRY_def)


[STATEMENT]
lemma in_CURRY_conv: "(f,g) \<in> CURRY R \<longleftrightarrow> (uncurry f, uncurry g) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f, g) \<in> CURRY R) = ((uncurry f, uncurry g) \<in> R)
[PROOF STEP]
unfolding CURRY_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((f, g) \<in> {(f, g). (uncurry f, uncurry g) \<in> R}) = ((uncurry f, uncurry g) \<in> R)
[PROOF STEP]
by auto


[STATEMENT]
lemma uncurry0_APP[simp]: "uncurry0 c $ x = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uncurry0 c $ x = c
[PROOF STEP]
by auto


[STATEMENT]
lemma fref_param0I: "(c,a)\<in>R \<Longrightarrow> (uncurry0 c, uncurry0 a) \<in> fref (\<lambda>_. True) unit_rel R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, a) \<in> R \<Longrightarrow> (uncurry0 c, uncurry0 a) \<in> unit_rel \<rightarrow>\<^sub>f R
[PROOF STEP]
by (auto simp: fref_def)


[STATEMENT]
lemma hr_compI: "(b,a)\<in>R2 \<Longrightarrow> R1 b c \<Longrightarrow>\<^sub>A hr_comp R1 R2 a c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b, a) \<in> R2 \<Longrightarrow> R1 b c \<Longrightarrow>\<^sub>A hr_comp R1 R2 a c
[PROOF STEP]
unfolding hr_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b, a) \<in> R2 \<Longrightarrow> R1 b c \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. R1 b c * \<up> ((b, a) \<in> R2)
[PROOF STEP]
by sep_auto


[STATEMENT]
lemma hr_comp_Id1[simp]: "hr_comp (pure Id) R = pure R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hr_comp id_assn R = pure R
[PROOF STEP]
unfolding hr_comp_def[abs_def] pure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a c. \<exists>\<^sub>Ab. \<up> ((c, b) \<in> Id) * \<up> ((b, a) \<in> R)) = (\<lambda>a c. \<up> ((c, a) \<in> R))
[PROOF STEP]
apply (intro ext ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a c. \<exists>\<^sub>Ab. \<up> ((c, b) \<in> Id) * \<up> ((b, a) \<in> R) \<Longrightarrow>\<^sub>A \<up> ((c, a) \<in> R)
 2. \<And>a c. \<up> ((c, a) \<in> R) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. \<up> ((c, b) \<in> Id) * \<up> ((b, a) \<in> R)
[PROOF STEP]
by sep_auto+


[STATEMENT]
lemma hr_comp_Id2[simp]: "hr_comp R Id = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hr_comp R Id = R
[PROOF STEP]
unfolding hr_comp_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> Id)) = R
[PROOF STEP]
apply (intro ext ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a c. \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> Id) \<Longrightarrow>\<^sub>A R a c
 2. \<And>a c. R a c \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. R b c * \<up> ((b, a) \<in> Id)
[PROOF STEP]
by sep_auto+


[STATEMENT]
lemma hr_comp_emp[simp]: "hr_comp (\<lambda>a c. emp) R a c = \<up>(\<exists>b. (b,a)\<in>R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hr_comp (\<lambda>a c. emp) R a c = \<up> (\<exists>b. (b, a) \<in> R)
[PROOF STEP]
unfolding hr_comp_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>\<^sub>Ab. emp * \<up> ((b, a) \<in> R)) = \<up> (\<exists>b. (b, a) \<in> R)
[PROOF STEP]
apply (intro ext ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<exists>\<^sub>Ab. emp * \<up> ((b, a) \<in> R) \<Longrightarrow>\<^sub>A \<up> (\<exists>b. (b, a) \<in> R)
 2. \<up> (\<exists>b. (b, a) \<in> R) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. emp * \<up> ((b, a) \<in> R)
[PROOF STEP]
apply sep_auto+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hr_comp_prod_conv[simp]:
    "hr_comp (prod_assn Ra Rb) (Ra' \<times>\<^sub>r Rb')
    = prod_assn (hr_comp Ra Ra') (hr_comp Rb Rb')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hr_comp (Ra \<times>\<^sub>a Rb) (Ra' \<times>\<^sub>r Rb') = hr_comp Ra Ra' \<times>\<^sub>a hr_comp Rb Rb'
[PROOF STEP]
unfolding hr_comp_def[abs_def] prod_assn_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a c. \<exists>\<^sub>Ab. (case (b, c) of ((a1, a2), c1, c2) \<Rightarrow> Ra a1 c1 * Rb a2 c2) * \<up> ((b, a) \<in> Ra' \<times>\<^sub>r Rb')) = (\<lambda>a c. case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> (\<exists>\<^sub>Ab. Ra b c1 * \<up> ((b, a1) \<in> Ra')) * (\<exists>\<^sub>Ab. Rb b c2 * \<up> ((b, a2) \<in> Rb')))
[PROOF STEP]
apply (intro ext ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a c. \<exists>\<^sub>Ab. (case (b, c) of ((a1, a2), c1, c2) \<Rightarrow> Ra a1 c1 * Rb a2 c2) * \<up> ((b, a) \<in> Ra' \<times>\<^sub>r Rb') \<Longrightarrow>\<^sub>A (case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> (\<exists>\<^sub>Ab. Ra b c1 * \<up> ((b, a1) \<in> Ra')) * (\<exists>\<^sub>Ab. Rb b c2 * \<up> ((b, a2) \<in> Rb')))
 2. \<And>a c. (case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> (\<exists>\<^sub>Ab. Ra b c1 * \<up> ((b, a1) \<in> Ra')) * (\<exists>\<^sub>Ab. Rb b c2 * \<up> ((b, a2) \<in> Rb'))) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. (case (b, c) of ((a1, a2), c1, c2) \<Rightarrow> Ra a1 c1 * Rb a2 c2) * \<up> ((b, a) \<in> Ra' \<times>\<^sub>r Rb')
[PROOF STEP]
apply solve_entails
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a c b. (b, a) \<in> Ra' \<times>\<^sub>r Rb' \<Longrightarrow> (case b of (a1, a2) \<Rightarrow> case c of (c1, c2) \<Rightarrow> Ra a1 c1 * Rb a2 c2) \<Longrightarrow>\<^sub>A (case a of (a1, a2) \<Rightarrow> case c of (c1, c2) \<Rightarrow> \<exists>\<^sub>Ab ba. Ra ba c1 * \<up> ((ba, a1) \<in> Ra') * Rb b c2 * \<up> ((b, a2) \<in> Rb'))
 2. \<And>a c. (case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> (\<exists>\<^sub>Ab. Ra b c1 * \<up> ((b, a1) \<in> Ra')) * (\<exists>\<^sub>Ab. Rb b c2 * \<up> ((b, a2) \<in> Rb'))) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. (case (b, c) of ((a1, a2), c1, c2) \<Rightarrow> Ra a1 c1 * Rb a2 c2) * \<up> ((b, a) \<in> Ra' \<times>\<^sub>r Rb')
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(ab, a) \<in> Ra'; (bb, b) \<in> Rb'\<rbrakk> \<Longrightarrow> Ra ab aa * Rb bb ba \<Longrightarrow>\<^sub>A \<exists>\<^sub>Abb bc. Ra bc aa * Rb bb ba * \<up> ((bc, a) \<in> Ra' \<and> (bb, b) \<in> Rb')
 2. \<And>a c. (case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> (\<exists>\<^sub>Ab. Ra b c1 * \<up> ((b, a1) \<in> Ra')) * (\<exists>\<^sub>Ab. Rb b c2 * \<up> ((b, a2) \<in> Rb'))) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. (case (b, c) of ((a1, a2), c1, c2) \<Rightarrow> Ra a1 c1 * Rb a2 c2) * \<up> ((b, a) \<in> Ra' \<times>\<^sub>r Rb')
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a c. (case (a, c) of ((a1, a2), c1, c2) \<Rightarrow> (\<exists>\<^sub>Ab. Ra b c1 * \<up> ((b, a1) \<in> Ra')) * (\<exists>\<^sub>Ab. Rb b c2 * \<up> ((b, a2) \<in> Rb'))) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. (case (b, c) of ((a1, a2), c1, c2) \<Rightarrow> Ra a1 c1 * Rb a2 c2) * \<up> ((b, a) \<in> Ra' \<times>\<^sub>r Rb')
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<exists>\<^sub>Abb bc. Ra bc aa * Rb bb ba * \<up> ((bc, a) \<in> Ra' \<and> (bb, b) \<in> Rb') \<Longrightarrow>\<^sub>A \<exists>\<^sub>Abb. (case bb of (a1, a2) \<Rightarrow> Ra a1 aa * Rb a2 ba) * \<up> ((bb, a, b) \<in> Ra' \<times>\<^sub>r Rb')
[PROOF STEP]
apply (intro ent_ex_preI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba bb bc. Ra bc aa * Rb bb ba * \<up> ((bc, a) \<in> Ra' \<and> (bb, b) \<in> Rb') \<Longrightarrow>\<^sub>A \<exists>\<^sub>Abb. (case bb of (a1, a2) \<Rightarrow> Ra a1 aa * Rb a2 ba) * \<up> ((bb, a, b) \<in> Ra' \<times>\<^sub>r Rb')
[PROOF STEP]
apply (rule ent_ex_postI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba bb bc. Ra bc aa * Rb bb ba * \<up> ((bc, a) \<in> Ra' \<and> (bb, b) \<in> Rb') \<Longrightarrow>\<^sub>A (case ?b23 a b aa ba bb bc of (a1, a2) \<Rightarrow> Ra a1 aa * Rb a2 ba) * \<up> ((?b23 a b aa ba bb bc, a, b) \<in> Ra' \<times>\<^sub>r Rb')
[PROOF STEP]
apply (sep_auto split: prod.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hr_comp_pure: "hr_comp (pure R) S = pure (R O S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hr_comp (pure R) S = pure (R O S)
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. hr_comp (pure R) S x xa = pure (R O S) x xa
[PROOF STEP]
apply (rule ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. hr_comp (pure R) S x xa \<Longrightarrow>\<^sub>A pure (R O S) x xa
 2. \<And>x xa. pure (R O S) x xa \<Longrightarrow>\<^sub>A hr_comp (pure R) S x xa
[PROOF STEP]
unfolding hr_comp_def[abs_def]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<exists>\<^sub>Ab. pure R b xa * \<up> ((b, x) \<in> S) \<Longrightarrow>\<^sub>A pure (R O S) x xa
 2. \<And>x xa. pure (R O S) x xa \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ab. pure R b xa * \<up> ((b, x) \<in> S)
[PROOF STEP]
apply (sep_auto simp: pure_def)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hr_comp_is_pure[safe_constraint_rules]: "is_pure A \<Longrightarrow> is_pure (hr_comp A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure A \<Longrightarrow> is_pure (hr_comp A B)
[PROOF STEP]
by (auto simp: hr_comp_pure is_pure_conv)


[STATEMENT]
lemma hr_comp_the_pure: "is_pure A \<Longrightarrow> the_pure (hr_comp A B) = the_pure A O B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_pure A \<Longrightarrow> the_pure (hr_comp A B) = the_pure A O B
[PROOF STEP]
unfolding is_pure_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>R'. A = pure R' \<Longrightarrow> the_pure (hr_comp A B) = the_pure A O B
[PROOF STEP]
by (clarsimp simp: hr_comp_pure)


[STATEMENT]
lemma rdomp_hrcomp_conv: "rdomp (hr_comp A R) x \<longleftrightarrow> (\<exists>y. rdomp A y \<and> (y,x)\<in>R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rdomp (hr_comp A R) x = (\<exists>y. rdomp A y \<and> (y, x) \<in> R)
[PROOF STEP]
by (auto simp: rdomp_def hr_comp_def)