[STATEMENT]
lemma DiamondTwo:
fixes
  cfg cfg1 cfg2 :: "('p,'v,'s) configuration" and
  Q :: "'p set" and
  msg :: "('p, 'v) message"
assumes
  QReach: "qReachable cfg Q cfg1" and
  Step: "cfg  \<turnstile> msg \<mapsto> cfg2"
        "\<exists>p\<in>Proc - Q. isReceiverOf p msg"
shows
  "\<exists> (cfg' :: ('p,'v,'s) configuration) . (cfg1  \<turnstile> msg \<mapsto> cfg')
  \<and> qReachable cfg2 Q cfg'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
qReachable cfg Q cfg1
cfg \<turnstile> msg \<mapsto> cfg2
\<exists>p\<in>Proc - Q. isReceiverOf p msg

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
proof(induct rule: qReachable.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cfg1 Q. \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
 2. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
fix cfg Q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cfg1 Q. \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
 2. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
have "qReachable cfg2 Q cfg2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qReachable cfg2 Q cfg2
[PROOF STEP]
using qReachable.simps(1)
[PROOF STATE]
proof (prove)
using this:
qReachable ?a1.0 ?a2.0 ?a3.0 = ((\<exists>cfg1 Q. ?a1.0 = cfg1 \<and> ?a2.0 = Q \<and> ?a3.0 = cfg1) \<or> (\<exists>cfg1 Q cfg2 msg cfg3. ?a1.0 = cfg1 \<and> ?a2.0 = Q \<and> ?a3.0 = cfg3 \<and> qReachable cfg1 Q cfg2 \<and> cfg2 \<turnstile> msg \<mapsto> cfg3 \<and> (\<exists>p\<in>Q. isReceiverOf p msg)))

goal (1 subgoal):
 1. qReachable cfg2 Q cfg2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qReachable cfg2 Q cfg2

goal (2 subgoals):
 1. \<And>cfg1 Q. \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
 2. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qReachable cfg2 Q cfg2

goal (2 subgoals):
 1. \<And>cfg1 Q. \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
 2. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
assume "cfg \<turnstile> msg \<mapsto> cfg2" "\<exists>p\<in>UNIV - Q. isReceiverOf p msg"
[PROOF STATE]
proof (state)
this:
cfg \<turnstile> msg \<mapsto> cfg2
\<exists>p\<in>Proc - Q. isReceiverOf p msg

goal (2 subgoals):
 1. \<And>cfg1 Q. \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
 2. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qReachable cfg2 Q cfg2
cfg \<turnstile> msg \<mapsto> cfg2
\<exists>p\<in>Proc - Q. isReceiverOf p msg
[PROOF STEP]
have "(cfg \<turnstile> msg \<mapsto> cfg2) \<and> qReachable cfg2 Q cfg2"
[PROOF STATE]
proof (prove)
using this:
qReachable cfg2 Q cfg2
cfg \<turnstile> msg \<mapsto> cfg2
\<exists>p\<in>Proc - Q. isReceiverOf p msg

goal (1 subgoal):
 1. cfg \<turnstile> msg \<mapsto> cfg2 \<and> qReachable cfg2 Q cfg2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cfg \<turnstile> msg \<mapsto> cfg2 \<and> qReachable cfg2 Q cfg2

goal (2 subgoals):
 1. \<And>cfg1 Q. \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
 2. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
thus "\<exists>cfg'.(cfg \<turnstile> msg \<mapsto> cfg') \<and> qReachable cfg2 Q cfg'"
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> msg \<mapsto> cfg2 \<and> qReachable cfg2 Q cfg2

goal (1 subgoal):
 1. \<exists>cfg'. cfg \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
fix cfg Q cfg1' msga cfg1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
assume   "(cfg \<turnstile> msg \<mapsto> cfg2)"
    "(\<exists>p\<in>UNIV - Q. isReceiverOf p msg)"
    "((cfg \<turnstile> msg \<mapsto> cfg2) \<Longrightarrow>
     (\<exists>p\<in>UNIV - Q. isReceiverOf p msg) \<Longrightarrow>
     (\<exists>cfg'. (cfg1' \<turnstile> msg \<mapsto> cfg') \<and> qReachable cfg2 Q cfg'))"
[PROOF STATE]
proof (state)
this:
cfg \<turnstile> msg \<mapsto> cfg2
\<exists>p\<in>Proc - Q. isReceiverOf p msg
\<lbrakk>cfg \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1' \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
hence "(\<exists>cfg'. (cfg1' \<turnstile> msg \<mapsto> cfg') \<and> (\<exists>p\<in>UNIV - Q. isReceiverOf p msg)
        \<and> qReachable cfg2 Q cfg')"
[PROOF STATE]
proof (prove)
using this:
cfg \<turnstile> msg \<mapsto> cfg2
\<exists>p\<in>Proc - Q. isReceiverOf p msg
\<lbrakk>cfg \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg1' \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'

goal (1 subgoal):
 1. \<exists>cfg'. cfg1' \<turnstile> msg \<mapsto> cfg' \<and> (\<exists>p\<in>Proc - Q. isReceiverOf p msg) \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg1' \<turnstile> msg \<mapsto> cfg' \<and> (\<exists>p\<in>Proc - Q. isReceiverOf p msg) \<and> qReachable cfg2 Q cfg'

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>cfg'. cfg1' \<turnstile> msg \<mapsto> cfg' \<and> (\<exists>p\<in>Proc - Q. isReceiverOf p msg) \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
obtain cfg' where Cfg': "(cfg1' \<turnstile> msg \<mapsto> cfg')"
    "(\<exists>p\<in>UNIV - Q. isReceiverOf p msg)" "qReachable cfg2 Q cfg'"
[PROOF STATE]
proof (prove)
using this:
\<exists>cfg'. cfg1' \<turnstile> msg \<mapsto> cfg' \<and> (\<exists>p\<in>Proc - Q. isReceiverOf p msg) \<and> qReachable cfg2 Q cfg'

goal (1 subgoal):
 1. (\<And>cfg'. \<lbrakk>cfg1' \<turnstile> msg \<mapsto> cfg'; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg2 Q cfg'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cfg1' \<turnstile> msg \<mapsto> cfg'
\<exists>p\<in>Proc - Q. isReceiverOf p msg
qReachable cfg2 Q cfg'

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfg1' \<turnstile> msg \<mapsto> cfg'
\<exists>p\<in>Proc - Q. isReceiverOf p msg
qReachable cfg2 Q cfg'
[PROOF STEP]
obtain p where P: "p\<in>UNIV - Q" "isReceiverOf p msg"
[PROOF STATE]
proof (prove)
using this:
cfg1' \<turnstile> msg \<mapsto> cfg'
\<exists>p\<in>Proc - Q. isReceiverOf p msg
qReachable cfg2 Q cfg'

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> Proc - Q; isReceiverOf p msg\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<in> Proc - Q
isReceiverOf p msg

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
assume Step2: "(cfg1' \<turnstile> msga \<mapsto> cfg1)"
    "(\<exists>p\<in>Q. isReceiverOf p msga)"
    "(qReachable cfg Q cfg1')"
[PROOF STATE]
proof (state)
this:
cfg1' \<turnstile> msga \<mapsto> cfg1
\<exists>p\<in>Q. isReceiverOf p msga
qReachable cfg Q cfg1'

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cfg1' \<turnstile> msga \<mapsto> cfg1
\<exists>p\<in>Q. isReceiverOf p msga
qReachable cfg Q cfg1'
[PROOF STEP]
obtain p' where P': "p'\<in>Q" "isReceiverOf p' msga"
[PROOF STATE]
proof (prove)
using this:
cfg1' \<turnstile> msga \<mapsto> cfg1
\<exists>p\<in>Q. isReceiverOf p msga
qReachable cfg Q cfg1'

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>p' \<in> Q; isReceiverOf p' msga\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p' \<in> Q
isReceiverOf p' msga

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
from P'(1) P(1)
[PROOF STATE]
proof (chain)
picking this:
p' \<in> Q
p \<in> Proc - Q
[PROOF STEP]
have notEq: "p \<noteq> p'"
[PROOF STATE]
proof (prove)
using this:
p' \<in> Q
p \<in> Proc - Q

goal (1 subgoal):
 1. p \<noteq> p'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<noteq> p'

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
with P(2) P'(2)
[PROOF STATE]
proof (chain)
picking this:
isReceiverOf p msg
isReceiverOf p' msga
p \<noteq> p'
[PROOF STEP]
have "\<not> isReceiverOf p' msg" "\<not> isReceiverOf p msga"
[PROOF STATE]
proof (prove)
using this:
isReceiverOf p msg
isReceiverOf p' msga
p \<noteq> p'

goal (1 subgoal):
 1. \<not> isReceiverOf p' msg &&& \<not> isReceiverOf p msga
[PROOF STEP]
using UniqueReceiverOf[of p' msga p] UniqueReceiverOf[of p msg p']
[PROOF STATE]
proof (prove)
using this:
isReceiverOf p msg
isReceiverOf p' msga
p \<noteq> p'
\<lbrakk>isReceiverOf p' msga; p \<noteq> p'\<rbrakk> \<Longrightarrow> \<not> isReceiverOf p msga
\<lbrakk>isReceiverOf p msg; p' \<noteq> p\<rbrakk> \<Longrightarrow> \<not> isReceiverOf p' msg

goal (1 subgoal):
 1. \<not> isReceiverOf p' msg &&& \<not> isReceiverOf p msga
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> isReceiverOf p' msg
\<not> isReceiverOf p msga

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
with notEq P'(2) P(2) Cfg'(1) Step2(1)
[PROOF STATE]
proof (chain)
picking this:
p \<noteq> p'
isReceiverOf p' msga
isReceiverOf p msg
cfg1' \<turnstile> msg \<mapsto> cfg'
cfg1' \<turnstile> msga \<mapsto> cfg1
\<not> isReceiverOf p' msg
\<not> isReceiverOf p msga
[PROOF STEP]
have
    "\<exists>cfg''. (cfg' \<turnstile> msga \<mapsto> cfg'') \<and> (cfg1 \<turnstile> msg \<mapsto> cfg'')"
[PROOF STATE]
proof (prove)
using this:
p \<noteq> p'
isReceiverOf p' msga
isReceiverOf p msg
cfg1' \<turnstile> msg \<mapsto> cfg'
cfg1' \<turnstile> msga \<mapsto> cfg1
\<not> isReceiverOf p' msg
\<not> isReceiverOf p msga

goal (1 subgoal):
 1. \<exists>cfg''. cfg' \<turnstile> msga \<mapsto> cfg'' \<and> cfg1 \<turnstile> msg \<mapsto> cfg''
[PROOF STEP]
using DiamondOne
[PROOF STATE]
proof (prove)
using this:
p \<noteq> p'
isReceiverOf p' msga
isReceiverOf p msg
cfg1' \<turnstile> msg \<mapsto> cfg'
cfg1' \<turnstile> msga \<mapsto> cfg1
\<not> isReceiverOf p' msg
\<not> isReceiverOf p msga
\<lbrakk>?cfg \<turnstile> ?m \<mapsto> ?cfg1.0; ?p \<noteq> ?q; isReceiverOf ?p ?m; \<not> isReceiverOf ?p ?m'; isReceiverOf ?q ?m'; \<not> isReceiverOf ?q ?m; ?cfg \<turnstile> ?m' \<mapsto> ?cfg2.0\<rbrakk> \<Longrightarrow> \<exists>cfg'. ?cfg1.0 \<turnstile> ?m' \<mapsto> cfg' \<and> ?cfg2.0 \<turnstile> ?m \<mapsto> cfg'

goal (1 subgoal):
 1. \<exists>cfg''. cfg' \<turnstile> msga \<mapsto> cfg'' \<and> cfg1 \<turnstile> msg \<mapsto> cfg''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>cfg''. cfg' \<turnstile> msga \<mapsto> cfg'' \<and> cfg1 \<turnstile> msg \<mapsto> cfg''

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>cfg''. cfg' \<turnstile> msga \<mapsto> cfg'' \<and> cfg1 \<turnstile> msg \<mapsto> cfg''
[PROOF STEP]
obtain cfg'' where Cfg'': "cfg' \<turnstile> msga \<mapsto> cfg''" "cfg1 \<turnstile> msg \<mapsto> cfg''"
[PROOF STATE]
proof (prove)
using this:
\<exists>cfg''. cfg' \<turnstile> msga \<mapsto> cfg'' \<and> cfg1 \<turnstile> msg \<mapsto> cfg''

goal (1 subgoal):
 1. (\<And>cfg''. \<lbrakk>cfg' \<turnstile> msga \<mapsto> cfg''; cfg1 \<turnstile> msg \<mapsto> cfg''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cfg' \<turnstile> msga \<mapsto> cfg''
cfg1 \<turnstile> msg \<mapsto> cfg''

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
from Cfg''(1) Step2(2) Cfg'(3)
[PROOF STATE]
proof (chain)
picking this:
cfg' \<turnstile> msga \<mapsto> cfg''
\<exists>p\<in>Q. isReceiverOf p msga
qReachable cfg2 Q cfg'
[PROOF STEP]
have "qReachable cfg2 Q cfg''"
[PROOF STATE]
proof (prove)
using this:
cfg' \<turnstile> msga \<mapsto> cfg''
\<exists>p\<in>Q. isReceiverOf p msga
qReachable cfg2 Q cfg'

goal (1 subgoal):
 1. qReachable cfg2 Q cfg''
[PROOF STEP]
using qReachable.simps[of cfg2 Q cfg'']
[PROOF STATE]
proof (prove)
using this:
cfg' \<turnstile> msga \<mapsto> cfg''
\<exists>p\<in>Q. isReceiverOf p msga
qReachable cfg2 Q cfg'
qReachable cfg2 Q cfg'' = ((\<exists>cfg1 Q. cfg2 = cfg1 \<and> Q = Q \<and> cfg'' = cfg1) \<or> (\<exists>cfg1 Q cfg2a msg cfg3. cfg2 = cfg1 \<and> Q = Q \<and> cfg'' = cfg3 \<and> qReachable cfg1 Q cfg2a \<and> cfg2a \<turnstile> msg \<mapsto> cfg3 \<and> (\<exists>p\<in>Q. isReceiverOf p msg)))

goal (1 subgoal):
 1. qReachable cfg2 Q cfg''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qReachable cfg2 Q cfg''

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
with Cfg'(2) Cfg''(2)
[PROOF STATE]
proof (chain)
picking this:
\<exists>p\<in>Proc - Q. isReceiverOf p msg
cfg1 \<turnstile> msg \<mapsto> cfg''
qReachable cfg2 Q cfg''
[PROOF STEP]
have
    "(cfg1 \<turnstile> msg \<mapsto> cfg'') \<and> qReachable cfg2 Q cfg''"
[PROOF STATE]
proof (prove)
using this:
\<exists>p\<in>Proc - Q. isReceiverOf p msg
cfg1 \<turnstile> msg \<mapsto> cfg''
qReachable cfg2 Q cfg''

goal (1 subgoal):
 1. cfg1 \<turnstile> msg \<mapsto> cfg'' \<and> qReachable cfg2 Q cfg''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cfg1 \<turnstile> msg \<mapsto> cfg'' \<and> qReachable cfg2 Q cfg''

goal (1 subgoal):
 1. \<And>cfg1 Q cfg2a msga cfg3. \<lbrakk>qReachable cfg1 Q cfg2a; \<lbrakk>cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg2a \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'; cfg2a \<turnstile> msga \<mapsto> cfg3; \<exists>p\<in>Q. isReceiverOf p msga; cfg1 \<turnstile> msg \<mapsto> cfg2; \<exists>p\<in>Proc - Q. isReceiverOf p msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. cfg3 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
thus "\<exists>cfg'. (cfg1 \<turnstile> msg \<mapsto> cfg') \<and> qReachable cfg2 Q cfg'"
[PROOF STATE]
proof (prove)
using this:
cfg1 \<turnstile> msg \<mapsto> cfg'' \<and> qReachable cfg2 Q cfg''

goal (1 subgoal):
 1. \<exists>cfg'. cfg1 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. cfg1 \<turnstile> msg \<mapsto> cfg' \<and> qReachable cfg2 Q cfg'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Diamond:
fixes
  cfg cfg1 cfg2 :: "('p,'v,'s) configuration" and
  Q :: "'p set"
assumes
  QReach: "qReachable cfg Q cfg1" and
  WithoutQReach: "withoutQReachable cfg Q cfg2"
shows
  "\<exists> cfg'. withoutQReachable cfg1 Q cfg'
     \<and> qReachable cfg2 Q cfg'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
define notQ where "notQ \<equiv> UNIV - Q"
[PROOF STATE]
proof (state)
this:
notQ \<equiv> Proc - Q

goal (1 subgoal):
 1. \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
with WithoutQReach
[PROOF STATE]
proof (chain)
picking this:
qReachable cfg (Proc - Q) cfg2
notQ \<equiv> Proc - Q
[PROOF STEP]
have "qReachable cfg notQ cfg2"
[PROOF STATE]
proof (prove)
using this:
qReachable cfg (Proc - Q) cfg2
notQ \<equiv> Proc - Q

goal (1 subgoal):
 1. qReachable cfg notQ cfg2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
qReachable cfg notQ cfg2

goal (1 subgoal):
 1. \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
qReachable cfg notQ cfg2

goal (1 subgoal):
 1. \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
using QReach notQ_def
[PROOF STATE]
proof (prove)
using this:
qReachable cfg notQ cfg2
qReachable cfg Q cfg1
notQ \<equiv> Proc - Q

goal (1 subgoal):
 1. \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
proof (induct rule: qReachable.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cfg1a. qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg1a Q cfg'
 2. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
fix cfg2
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cfg1a. qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg1a Q cfg'
 2. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
assume "qReachable cfg2 Q cfg1"
[PROOF STATE]
proof (state)
this:
qReachable cfg2 Q cfg1

goal (2 subgoals):
 1. \<And>cfg1a. qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg1a Q cfg'
 2. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
qReachable cfg2 Q cfg1

goal (2 subgoals):
 1. \<And>cfg1a. qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg1a Q cfg'
 2. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
have "qReachable cfg1 (UNIV - Q) cfg1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qReachable cfg1 (Proc - Q) cfg1
[PROOF STEP]
using qReachable.simps
[PROOF STATE]
proof (prove)
using this:
qReachable ?a1.0 ?a2.0 ?a3.0 = ((\<exists>cfg1 Q. ?a1.0 = cfg1 \<and> ?a2.0 = Q \<and> ?a3.0 = cfg1) \<or> (\<exists>cfg1 Q cfg2 msg cfg3. ?a1.0 = cfg1 \<and> ?a2.0 = Q \<and> ?a3.0 = cfg3 \<and> qReachable cfg1 Q cfg2 \<and> cfg2 \<turnstile> msg \<mapsto> cfg3 \<and> (\<exists>p\<in>Q. isReceiverOf p msg)))

goal (1 subgoal):
 1. qReachable cfg1 (Proc - Q) cfg1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qReachable cfg1 (Proc - Q) cfg1

goal (2 subgoals):
 1. \<And>cfg1a. qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg1a Q cfg'
 2. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
qReachable cfg2 Q cfg1
qReachable cfg1 (Proc - Q) cfg1
[PROOF STEP]
show
      "\<exists>cfg'. qReachable cfg1 (UNIV - Q) cfg'
        \<and> qReachable cfg2 Q cfg'"
[PROOF STATE]
proof (prove)
using this:
qReachable cfg2 Q cfg1
qReachable cfg1 (Proc - Q) cfg1

goal (1 subgoal):
 1. \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'

goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
fix cfg cfg2' cfg2 msg
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
assume Ass1: " qReachable cfg Q cfg1" "qReachable cfg (UNIV - Q) cfg2' "
[PROOF STATE]
proof (state)
this:
qReachable cfg Q cfg1
qReachable cfg (Proc - Q) cfg2'

goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
assume Ass2:  "cfg2' \<turnstile> msg \<mapsto> cfg2" "\<exists>p\<in>UNIV - Q. isReceiverOf p msg"
[PROOF STATE]
proof (state)
this:
cfg2' \<turnstile> msg \<mapsto> cfg2
\<exists>p\<in>Proc - Q. isReceiverOf p msg

goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
assume "qReachable cfg Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (UNIV - Q) cfg'
      \<and> qReachable cfg2' Q cfg'"
[PROOF STATE]
proof (state)
this:
qReachable cfg Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2' Q cfg'

goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
with Ass1(1)
[PROOF STATE]
proof (chain)
picking this:
qReachable cfg Q cfg1
qReachable cfg Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2' Q cfg'
[PROOF STEP]
have "\<exists>cfg'. qReachable cfg1 (UNIV - Q) cfg'
      \<and> qReachable cfg2' Q cfg'"
[PROOF STATE]
proof (prove)
using this:
qReachable cfg Q cfg1
qReachable cfg Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2' Q cfg'

goal (1 subgoal):
 1. \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2' Q cfg'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2' Q cfg'

goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2' Q cfg'
[PROOF STEP]
obtain cfg' where
      Cfg'1: "qReachable cfg2' Q cfg'" and
      Cfg':  "qReachable cfg1 (UNIV - Q) cfg'"
[PROOF STATE]
proof (prove)
using this:
\<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2' Q cfg'

goal (1 subgoal):
 1. (\<And>cfg'. \<lbrakk>qReachable cfg2' Q cfg'; qReachable cfg1 (Proc - Q) cfg'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
qReachable cfg2' Q cfg'
qReachable cfg1 (Proc - Q) cfg'

goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
from Cfg'1 Ass2
[PROOF STATE]
proof (chain)
picking this:
qReachable cfg2' Q cfg'
cfg2' \<turnstile> msg \<mapsto> cfg2
\<exists>p\<in>Proc - Q. isReceiverOf p msg
[PROOF STEP]
have
      "\<exists>cfg''.(cfg' \<turnstile> msg \<mapsto> cfg'') \<and> qReachable cfg2 Q cfg''"
[PROOF STATE]
proof (prove)
using this:
qReachable cfg2' Q cfg'
cfg2' \<turnstile> msg \<mapsto> cfg2
\<exists>p\<in>Proc - Q. isReceiverOf p msg

goal (1 subgoal):
 1. \<exists>cfg''. cfg' \<turnstile> msg \<mapsto> cfg'' \<and> qReachable cfg2 Q cfg''
[PROOF STEP]
using DiamondTwo
[PROOF STATE]
proof (prove)
using this:
qReachable cfg2' Q cfg'
cfg2' \<turnstile> msg \<mapsto> cfg2
\<exists>p\<in>Proc - Q. isReceiverOf p msg
\<lbrakk>qReachable ?cfg ?Q ?cfg1.0; ?cfg \<turnstile> ?msg \<mapsto> ?cfg2.0; \<exists>p\<in>Proc - ?Q. isReceiverOf p ?msg\<rbrakk> \<Longrightarrow> \<exists>cfg'. ?cfg1.0 \<turnstile> ?msg \<mapsto> cfg' \<and> qReachable ?cfg2.0 ?Q cfg'

goal (1 subgoal):
 1. \<exists>cfg''. cfg' \<turnstile> msg \<mapsto> cfg'' \<and> qReachable cfg2 Q cfg''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>cfg''. cfg' \<turnstile> msg \<mapsto> cfg'' \<and> qReachable cfg2 Q cfg''

goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>cfg''. cfg' \<turnstile> msg \<mapsto> cfg'' \<and> qReachable cfg2 Q cfg''
[PROOF STEP]
obtain cfg'' where
      Cfg'': "cfg' \<turnstile> msg \<mapsto> cfg''" "qReachable cfg2 Q cfg''"
[PROOF STATE]
proof (prove)
using this:
\<exists>cfg''. cfg' \<turnstile> msg \<mapsto> cfg'' \<and> qReachable cfg2 Q cfg''

goal (1 subgoal):
 1. (\<And>cfg''. \<lbrakk>cfg' \<turnstile> msg \<mapsto> cfg''; qReachable cfg2 Q cfg''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cfg' \<turnstile> msg \<mapsto> cfg''
qReachable cfg2 Q cfg''

goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
from Cfg' Cfg''(1) Ass2(2)
[PROOF STATE]
proof (chain)
picking this:
qReachable cfg1 (Proc - Q) cfg'
cfg' \<turnstile> msg \<mapsto> cfg''
\<exists>p\<in>Proc - Q. isReceiverOf p msg
[PROOF STEP]
have "qReachable cfg1 (UNIV - Q) cfg''"
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1 (Proc - Q) cfg'
cfg' \<turnstile> msg \<mapsto> cfg''
\<exists>p\<in>Proc - Q. isReceiverOf p msg

goal (1 subgoal):
 1. qReachable cfg1 (Proc - Q) cfg''
[PROOF STEP]
using qReachable.simps[of cfg1 "UNIV-Q" cfg'']
[PROOF STATE]
proof (prove)
using this:
qReachable cfg1 (Proc - Q) cfg'
cfg' \<turnstile> msg \<mapsto> cfg''
\<exists>p\<in>Proc - Q. isReceiverOf p msg
qReachable cfg1 (Proc - Q) cfg'' = ((\<exists>cfg1a Qa. cfg1 = cfg1a \<and> Proc - Q = Qa \<and> cfg'' = cfg1a) \<or> (\<exists>cfg1a Qa cfg2 msg cfg3. cfg1 = cfg1a \<and> Proc - Q = Qa \<and> cfg'' = cfg3 \<and> qReachable cfg1a Qa cfg2 \<and> cfg2 \<turnstile> msg \<mapsto> cfg3 \<and> (\<exists>p\<in>Qa. isReceiverOf p msg)))

goal (1 subgoal):
 1. qReachable cfg1 (Proc - Q) cfg''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
qReachable cfg1 (Proc - Q) cfg''

goal (1 subgoal):
 1. \<And>cfg1a cfg2 msg cfg3. \<lbrakk>qReachable cfg1a (Proc - Q) cfg2; qReachable cfg1a Q cfg1 \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'; cfg2 \<turnstile> msg \<mapsto> cfg3; \<exists>p\<in>Proc - Q. isReceiverOf p msg; qReachable cfg1a Q cfg1\<rbrakk> \<Longrightarrow> \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg3 Q cfg'
[PROOF STEP]
with Cfg''
[PROOF STATE]
proof (chain)
picking this:
cfg' \<turnstile> msg \<mapsto> cfg''
qReachable cfg2 Q cfg''
qReachable cfg1 (Proc - Q) cfg''
[PROOF STEP]
show
      "\<exists>cfg'. qReachable cfg1 (UNIV - Q) cfg'
        \<and> qReachable cfg2 Q cfg'"
[PROOF STATE]
proof (prove)
using this:
cfg' \<turnstile> msg \<mapsto> cfg''
qReachable cfg2 Q cfg''
qReachable cfg1 (Proc - Q) cfg''

goal (1 subgoal):
 1. \<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>cfg'. qReachable cfg1 (Proc - Q) cfg' \<and> qReachable cfg2 Q cfg'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma FiniteMessages:
fixes
  cfg  :: "('p, 'v, 's) configuration"
assumes
  FiniteProcs: "finite Proc" and
  FiniteSends: "\<And> p s m. finite {v. v \<in># (sends p s m)}" and
  InitReachable: "initReachable cfg"
shows "finite {msg . msg \<in># msgs cfg}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
proof(-)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
have "\<exists> init . initial init \<and> reachable init cfg"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>init. initial init \<and> reachable init cfg
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite Proc
finite {v. v \<in># sends ?p ?s ?m}
initReachable cfg

goal (1 subgoal):
 1. \<exists>init. initial init \<and> reachable init cfg
[PROOF STEP]
unfolding initReachable_def
[PROOF STATE]
proof (prove)
using this:
finite Proc
finite {v. v \<in># sends ?p ?s ?m}
\<exists>cfg0. initial cfg0 \<and> reachable cfg0 cfg

goal (1 subgoal):
 1. \<exists>init. initial init \<and> reachable init cfg
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>init. initial init \<and> reachable init cfg

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>init. initial init \<and> reachable init cfg
[PROOF STEP]
obtain init where Init: "initial init" "reachable init cfg"
[PROOF STATE]
proof (prove)
using this:
\<exists>init. initial init \<and> reachable init cfg

goal (1 subgoal):
 1. (\<And>init. \<lbrakk>initial init; reachable init cfg\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
initial init
reachable init cfg

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
have InitMsgs:"{msg . msg \<in># msgs init}
    = { msg . (msg \<in># msgs init) \<and> (\<exists> p v. <p, v> = msg)}
      \<union> { msg . (msg \<in># msgs init) \<and> (\<exists> v.  <\<bottom>, outM v> = msg)}
      \<union> { msg . (msg \<in># msgs init) \<and> (\<exists> p v.  <p, inM v> = msg)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {msg. msg \<in># msgs init} = {msg. msg \<in># msgs init \<and> (\<exists>p v. <p, v> = msg)} \<union> {msg. msg \<in># msgs init \<and> (\<exists>v. <\<bottom>, outM v> = msg)} \<union> {msg. msg \<in># msgs init \<and> (\<exists>p v. <p, inM v> = msg)}
[PROOF STEP]
by (auto,metis message.exhaust)
[PROOF STATE]
proof (state)
this:
{msg. msg \<in># msgs init} = {msg. msg \<in># msgs init \<and> (\<exists>p v. <p, v> = msg)} \<union> {msg. msg \<in># msgs init \<and> (\<exists>v. <\<bottom>, outM v> = msg)} \<union> {msg. msg \<in># msgs init \<and> (\<exists>p v. <p, inM v> = msg)}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
have A:"{ msg . (msg \<in># msgs init) \<and> (\<exists> p v. <p, v> = msg)} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {msg. msg \<in># msgs init \<and> (\<exists>p v. <p, v> = msg)} = {}
[PROOF STEP]
using initial_def[of init] Init(1)
[PROOF STATE]
proof (prove)
using this:
initial init \<equiv> (\<forall>p. \<exists>v. msgs init <p, inM v> = 1) \<and> (\<forall>p m1 m2. m1 \<in># msgs init \<and> m2 \<in># msgs init \<and> isReceiverOf p m1 \<and> isReceiverOf p m2 \<longrightarrow> m1 = m2) \<and> (\<forall>v. msgs init <\<bottom>, outM v> = 0) \<and> (\<forall>p v. msgs init <p, v> = 0) \<and> states init = start
initial init

goal (1 subgoal):
 1. {msg. msg \<in># msgs init \<and> (\<exists>p v. <p, v> = msg)} = {}
[PROOF STEP]
by (auto, metis less_not_refl3)
[PROOF STATE]
proof (state)
this:
{msg. msg \<in># msgs init \<and> (\<exists>p v. <p, v> = msg)} = {}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
have B:"{ msg . (msg \<in># msgs init) \<and> (\<exists> v.  <\<bottom>, outM v> = msg)} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {msg. msg \<in># msgs init \<and> (\<exists>v. <\<bottom>, outM v> = msg)} = {}
[PROOF STEP]
using initial_def[of init] Init(1)
[PROOF STATE]
proof (prove)
using this:
initial init \<equiv> (\<forall>p. \<exists>v. msgs init <p, inM v> = 1) \<and> (\<forall>p m1 m2. m1 \<in># msgs init \<and> m2 \<in># msgs init \<and> isReceiverOf p m1 \<and> isReceiverOf p m2 \<longrightarrow> m1 = m2) \<and> (\<forall>v. msgs init <\<bottom>, outM v> = 0) \<and> (\<forall>p v. msgs init <p, v> = 0) \<and> states init = start
initial init

goal (1 subgoal):
 1. {msg. msg \<in># msgs init \<and> (\<exists>v. <\<bottom>, outM v> = msg)} = {}
[PROOF STEP]
by (auto, metis less_not_refl3)
[PROOF STATE]
proof (state)
this:
{msg. msg \<in># msgs init \<and> (\<exists>v. <\<bottom>, outM v> = msg)} = {}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
have "\<forall> p . finite {<p, inM True>, <p, inM False>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. finite {<p, inM True>, <p, inM False>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>p. finite {<p, inM True>, <p, inM False>}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>p. finite {<p, inM True>, <p, inM False>}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
have SubsetMsg:
    "\<forall> p. { msg . (msg \<in># msgs init)
      \<and> (\<exists> v::bool .  <p, inM v> = msg)}
      \<subseteq> {<p, inM True>, <p, inM False>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)} \<subseteq> {<p, inM True>, <p, inM False>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>p. {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)} \<subseteq> {<p, inM True>, <p, inM False>}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>p. finite {<p, inM True>, <p, inM False>}
\<forall>p. {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)} \<subseteq> {<p, inM True>, <p, inM False>}
[PROOF STEP]
have AllFinite:
    "\<forall> p. finite { msg . (msg \<in># msgs init)
      \<and> (\<exists> v::bool .  <p, inM v> = msg)}"
[PROOF STATE]
proof (prove)
using this:
\<forall>p. finite {<p, inM True>, <p, inM False>}
\<forall>p. {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)} \<subseteq> {<p, inM True>, <p, inM False>}

goal (1 subgoal):
 1. \<forall>p. finite {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)}
[PROOF STEP]
using finite_subset
[PROOF STATE]
proof (prove)
using this:
\<forall>p. finite {<p, inM True>, <p, inM False>}
\<forall>p. {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)} \<subseteq> {<p, inM True>, <p, inM False>}
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. \<forall>p. finite {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)}
[PROOF STEP]
by (clarify, auto)
[PROOF STATE]
proof (state)
this:
\<forall>p. finite {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
have " { msg . (msg \<in># msgs init)
    \<and> (\<exists> p\<in>Proc . \<exists> v::bool.  <p, inM v> = msg)}
      = (\<Union> p \<in> Proc . { msg . (msg \<in># msgs init)
    \<and> (\<exists> v::bool .  <p, inM v> = msg)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {msg. msg \<in># msgs init \<and> (\<exists>p\<in>Proc. \<exists>v. <p, inM v> = msg)} = (\<Union>p. {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{msg. msg \<in># msgs init \<and> (\<exists>p\<in>Proc. \<exists>v. <p, inM v> = msg)} = (\<Union>p. {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)})

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
hence "finite  { msg . (msg \<in># msgs init)
    \<and> (\<exists> p\<in>Proc . \<exists> v::bool.  <p, inM v> = msg)}"
[PROOF STATE]
proof (prove)
using this:
{msg. msg \<in># msgs init \<and> (\<exists>p\<in>Proc. \<exists>v. <p, inM v> = msg)} = (\<Union>p. {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)})

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs init \<and> (\<exists>p\<in>Proc. \<exists>v. <p, inM v> = msg)}
[PROOF STEP]
using AllFinite FiniteProcs
[PROOF STATE]
proof (prove)
using this:
{msg. msg \<in># msgs init \<and> (\<exists>p\<in>Proc. \<exists>v. <p, inM v> = msg)} = (\<Union>p. {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)})
\<forall>p. finite {msg. msg \<in># msgs init \<and> (\<exists>v. <p, inM v> = msg)}
finite Proc

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs init \<and> (\<exists>p\<in>Proc. \<exists>v. <p, inM v> = msg)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {msg. msg \<in># msgs init \<and> (\<exists>p\<in>Proc. \<exists>v. <p, inM v> = msg)}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
hence InitFinite:"finite {msg . msg \<in># msgs init}"
[PROOF STATE]
proof (prove)
using this:
finite {msg. msg \<in># msgs init \<and> (\<exists>p\<in>Proc. \<exists>v. <p, inM v> = msg)}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs init}
[PROOF STEP]
by (auto simp add: A B InitMsgs)
[PROOF STATE]
proof (state)
this:
finite {msg. msg \<in># msgs init}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
using Init(2) InitFinite
[PROOF STATE]
proof (prove)
using this:
reachable init cfg
finite {msg. msg \<in># msgs init}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg}
[PROOF STEP]
proof(induct rule: reachable.induct, simp_all)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1 cfg2 msg cfg3. \<lbrakk>reachable cfg1 cfg2; finite {msg. msg \<in># msgs cfg2}; cfg2 \<turnstile> msg \<mapsto> cfg3; finite {msg. msg \<in># msgs cfg1}; reachable init cfg; finite {msg. msg \<in># msgs init}\<rbrakk> \<Longrightarrow> finite {msg. msg \<in># msgs cfg3}
[PROOF STEP]
fix cfg1 cfg2 msg cfg3
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cfg1 cfg2 msg cfg3. \<lbrakk>reachable cfg1 cfg2; finite {msg. msg \<in># msgs cfg2}; cfg2 \<turnstile> msg \<mapsto> cfg3; finite {msg. msg \<in># msgs cfg1}; reachable init cfg; finite {msg. msg \<in># msgs init}\<rbrakk> \<Longrightarrow> finite {msg. msg \<in># msgs cfg3}
[PROOF STEP]
assume assmsInduct:"reachable cfg1 cfg2"
      "finite {msg. msg \<in># msgs cfg2}" "cfg2 \<turnstile> msg \<mapsto> cfg3"
      "finite {msg. msg \<in># msgs cfg1}" "reachable init cfg"
      "finite {msg. msg \<in># msgs init}"
[PROOF STATE]
proof (state)
this:
reachable cfg1 cfg2
finite {msg. msg \<in># msgs cfg2}
cfg2 \<turnstile> msg \<mapsto> cfg3
finite {msg. msg \<in># msgs cfg1}
reachable init cfg
finite {msg. msg \<in># msgs init}

goal (1 subgoal):
 1. \<And>cfg1 cfg2 msg cfg3. \<lbrakk>reachable cfg1 cfg2; finite {msg. msg \<in># msgs cfg2}; cfg2 \<turnstile> msg \<mapsto> cfg3; finite {msg. msg \<in># msgs cfg1}; reachable init cfg; finite {msg. msg \<in># msgs init}\<rbrakk> \<Longrightarrow> finite {msg. msg \<in># msgs cfg3}
[PROOF STEP]
from assmsInduct(3)
[PROOF STATE]
proof (chain)
picking this:
cfg2 \<turnstile> msg \<mapsto> cfg3
[PROOF STEP]
obtain p where "isReceiverOf p msg "
[PROOF STATE]
proof (prove)
using this:
cfg2 \<turnstile> msg \<mapsto> cfg3

goal (1 subgoal):
 1. (\<And>p. isReceiverOf p msg \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis StepOutMsg isReceiverOf.simps(1) isReceiverOf.simps(2)
       message.exhaust)
[PROOF STATE]
proof (state)
this:
isReceiverOf p msg

goal (1 subgoal):
 1. \<And>cfg1 cfg2 msg cfg3. \<lbrakk>reachable cfg1 cfg2; finite {msg. msg \<in># msgs cfg2}; cfg2 \<turnstile> msg \<mapsto> cfg3; finite {msg. msg \<in># msgs cfg1}; reachable init cfg; finite {msg. msg \<in># msgs init}\<rbrakk> \<Longrightarrow> finite {msg. msg \<in># msgs cfg3}
[PROOF STEP]
hence "msgs cfg3 = ((msgs cfg2 -# msg) \<union># (sends p (states cfg2 p)
      (unpackMessage msg) ))"
[PROOF STATE]
proof (prove)
using this:
isReceiverOf p msg

goal (1 subgoal):
 1. msgs cfg3 = msgs cfg2 -# msg \<union># sends p (states cfg2 p) (unpackMessage msg)
[PROOF STEP]
using assmsInduct(3)
[PROOF STATE]
proof (prove)
using this:
isReceiverOf p msg
cfg2 \<turnstile> msg \<mapsto> cfg3

goal (1 subgoal):
 1. msgs cfg3 = msgs cfg2 -# msg \<union># sends p (states cfg2 p) (unpackMessage msg)
[PROOF STEP]
by (cases msg, auto simp add: add.commute)
[PROOF STATE]
proof (state)
this:
msgs cfg3 = msgs cfg2 -# msg \<union># sends p (states cfg2 p) (unpackMessage msg)

goal (1 subgoal):
 1. \<And>cfg1 cfg2 msg cfg3. \<lbrakk>reachable cfg1 cfg2; finite {msg. msg \<in># msgs cfg2}; cfg2 \<turnstile> msg \<mapsto> cfg3; finite {msg. msg \<in># msgs cfg1}; reachable init cfg; finite {msg. msg \<in># msgs init}\<rbrakk> \<Longrightarrow> finite {msg. msg \<in># msgs cfg3}
[PROOF STEP]
hence MsgSet: "{msg. msg \<in>#  msgs cfg3 }
      = {m. m \<in># ((msgs cfg2 -# msg) \<union># (sends p (states cfg2 p)
        (unpackMessage msg) )) } "
[PROOF STATE]
proof (prove)
using this:
msgs cfg3 = msgs cfg2 -# msg \<union># sends p (states cfg2 p) (unpackMessage msg)

goal (1 subgoal):
 1. {msg. msg \<in># msgs cfg3} = {m. sends p (states cfg2 p) (unpackMessage msg) m \<in># (+) ((msgs cfg2 -# msg) m)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{msg. msg \<in># msgs cfg3} = {m. sends p (states cfg2 p) (unpackMessage msg) m \<in># (+) ((msgs cfg2 -# msg) m)}

goal (1 subgoal):
 1. \<And>cfg1 cfg2 msg cfg3. \<lbrakk>reachable cfg1 cfg2; finite {msg. msg \<in># msgs cfg2}; cfg2 \<turnstile> msg \<mapsto> cfg3; finite {msg. msg \<in># msgs cfg1}; reachable init cfg; finite {msg. msg \<in># msgs init}\<rbrakk> \<Longrightarrow> finite {msg. msg \<in># msgs cfg3}
[PROOF STEP]
have "{v. v \<in># (msgs cfg2 -# msg)} \<subseteq> {msg. msg \<in># msgs cfg2}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v. msgs cfg2 v \<in># If (v = msg) (msgs cfg2 v - 1)} \<subseteq> {msg. msg \<in># msgs cfg2}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{v. msgs cfg2 v \<in># If (v = msg) (msgs cfg2 v - 1)} \<subseteq> {msg. msg \<in># msgs cfg2}

goal (1 subgoal):
 1. \<And>cfg1 cfg2 msg cfg3. \<lbrakk>reachable cfg1 cfg2; finite {msg. msg \<in># msgs cfg2}; cfg2 \<turnstile> msg \<mapsto> cfg3; finite {msg. msg \<in># msgs cfg1}; reachable init cfg; finite {msg. msg \<in># msgs init}\<rbrakk> \<Longrightarrow> finite {msg. msg \<in># msgs cfg3}
[PROOF STEP]
from finite_subset[OF this]
[PROOF STATE]
proof (chain)
picking this:
finite {msg. msg \<in># msgs cfg2} \<Longrightarrow> finite {v. msgs cfg2 v \<in># If (v = msg) (msgs cfg2 v - 1)}
[PROOF STEP]
have "finite {v. (v \<in># sends p (states cfg2 p) (unpackMessage msg))
        \<or> (v \<in># (msgs cfg2 -# msg))}"
[PROOF STATE]
proof (prove)
using this:
finite {msg. msg \<in># msgs cfg2} \<Longrightarrow> finite {v. msgs cfg2 v \<in># If (v = msg) (msgs cfg2 v - 1)}

goal (1 subgoal):
 1. finite {v. v \<in># sends p (states cfg2 p) (unpackMessage msg) \<or> msgs cfg2 v \<in># If (v = msg) (msgs cfg2 v - 1)}
[PROOF STEP]
using FiniteSends assmsInduct(2)
[PROOF STATE]
proof (prove)
using this:
finite {msg. msg \<in># msgs cfg2} \<Longrightarrow> finite {v. msgs cfg2 v \<in># If (v = msg) (msgs cfg2 v - 1)}
finite {v. v \<in># sends ?p ?s ?m}
finite {msg. msg \<in># msgs cfg2}

goal (1 subgoal):
 1. finite {v. v \<in># sends p (states cfg2 p) (unpackMessage msg) \<or> msgs cfg2 v \<in># If (v = msg) (msgs cfg2 v - 1)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {v. v \<in># sends p (states cfg2 p) (unpackMessage msg) \<or> msgs cfg2 v \<in># If (v = msg) (msgs cfg2 v - 1)}

goal (1 subgoal):
 1. \<And>cfg1 cfg2 msg cfg3. \<lbrakk>reachable cfg1 cfg2; finite {msg. msg \<in># msgs cfg2}; cfg2 \<turnstile> msg \<mapsto> cfg3; finite {msg. msg \<in># msgs cfg1}; reachable init cfg; finite {msg. msg \<in># msgs init}\<rbrakk> \<Longrightarrow> finite {msg. msg \<in># msgs cfg3}
[PROOF STEP]
thus "finite {msg. msg \<in># msgs cfg3}"
[PROOF STATE]
proof (prove)
using this:
finite {v. v \<in># sends p (states cfg2 p) (unpackMessage msg) \<or> msgs cfg2 v \<in># If (v = msg) (msgs cfg2 v - 1)}

goal (1 subgoal):
 1. finite {msg. msg \<in># msgs cfg3}
[PROOF STEP]
unfolding MsgSet
[PROOF STATE]
proof (prove)
using this:
finite {v. v \<in># sends p (states cfg2 p) (unpackMessage msg) \<or> msgs cfg2 v \<in># If (v = msg) (msgs cfg2 v - 1)}

goal (1 subgoal):
 1. finite {m. sends p (states cfg2 p) (unpackMessage msg) m \<in># (+) ((msgs cfg2 -# msg) m)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {msg. msg \<in># msgs cfg3}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {msg. msg \<in># msgs cfg}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma TC_DEFL: "TC('t::tycon)\<cdot>DEFL('a) = DEFL('a\<cdot>'t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TC('t)\<cdot>DEFL('a) = DEFL('a\<cdot>'t)
[PROOF STEP]
by (rule DEFL_app [symmetric])


[STATEMENT]
lemma DEFL_app_mono [simp, intro]:
  "DEFL('a) \<sqsubseteq> DEFL('b) \<Longrightarrow> DEFL('a\<cdot>'t::tycon) \<sqsubseteq> DEFL('b\<cdot>'t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DEFL('a) \<sqsubseteq> DEFL('b) \<Longrightarrow> DEFL('a\<cdot>'t) \<sqsubseteq> DEFL('b\<cdot>'t)
[PROOF STEP]
apply (simp add: DEFL_app)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DEFL('a) \<sqsubseteq> DEFL('b) \<Longrightarrow> TC('t)\<cdot>DEFL('a) \<sqsubseteq> TC('t)\<cdot>DEFL('b)
[PROOF STEP]
apply (erule monofun_cfun_arg)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma param_it_to_list[param]: "(it_to_list,it_to_list) \<in>
    (Rs \<rightarrow> (Ra \<rightarrow> bool_rel) \<rightarrow>
    (Rb \<rightarrow> \<langle>Rb\<rangle>list_rel \<rightarrow> \<langle>Rb\<rangle>list_rel) \<rightarrow> \<langle>Rc\<rangle>list_rel \<rightarrow> Rd) \<rightarrow> Rs \<rightarrow> Rd"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (it_to_list, it_to_list) \<in> (Rs \<rightarrow> (Ra \<rightarrow> bool_rel) \<rightarrow> (Rb \<rightarrow> \<langle>Rb\<rangle>list_rel \<rightarrow> \<langle>Rb\<rangle>list_rel) \<rightarrow> \<langle>Rc\<rangle>list_rel \<rightarrow> Rd) \<rightarrow> Rs \<rightarrow> Rd
[PROOF STEP]
unfolding it_to_list_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>it s. it s (\<lambda>_. True) (\<lambda>x l. l @ [x]) [], \<lambda>it s. it s (\<lambda>_. True) (\<lambda>x l. l @ [x]) []) \<in> (Rs \<rightarrow> (Ra \<rightarrow> bool_rel) \<rightarrow> (Rb \<rightarrow> \<langle>Rb\<rangle>list_rel \<rightarrow> \<langle>Rb\<rangle>list_rel) \<rightarrow> \<langle>Rc\<rangle>list_rel \<rightarrow> Rd) \<rightarrow> Rs \<rightarrow> Rd
[PROOF STEP]
by parametricity


[STATEMENT]
lemma key_rel_UNIV[simp]: "key_rel (\<lambda>_ _. True) = (\<lambda>_ _. True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. key_rel (\<lambda>_ _. True) = (\<lambda>_ _. True)
[PROOF STEP]
unfolding key_rel_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a b. True) = (\<lambda>_ _. True)
[PROOF STEP]
by auto


[STATEMENT]
lemma set_to_sorted_list_itype[autoref_itype]:
    "set_to_sorted_list R ::\<^sub>i \<langle>I\<rangle>\<^sub>ii_set \<rightarrow>\<^sub>i \<langle>\<langle>I\<rangle>\<^sub>ii_list\<rangle>\<^sub>ii_nres"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_to_sorted_list R ::\<^sub>i \<langle>I\<rangle>\<^sub>ii_set \<rightarrow>\<^sub>i \<langle>\<langle>I\<rangle>\<^sub>ii_list\<rangle>\<^sub>ii_nres
[PROOF STEP]
by simp


[STATEMENT]
lemma set_to_sorted_list_pat[autoref_op_pat]:
    "it_to_sorted_list R S \<equiv> OP (set_to_sorted_list R) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_sorted_list R S \<equiv> OP (set_to_sorted_list R) S
[PROOF STEP]
unfolding set_to_sorted_list_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_sorted_list R S \<equiv> OP (it_to_sorted_list R) S
[PROOF STEP]
by auto


[STATEMENT]
lemma map_to_sorted_list_itype[autoref_itype]:
    "map_to_sorted_list R ::\<^sub>i \<langle>Rk,Rv\<rangle>\<^sub>ii_map \<rightarrow>\<^sub>i \<langle>\<langle>\<langle>Rk,Rv\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_list\<rangle>\<^sub>ii_nres"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_to_sorted_list R ::\<^sub>i \<langle>Rk, Rv\<rangle>\<^sub>ii_map \<rightarrow>\<^sub>i \<langle>\<langle>\<langle>Rk, Rv\<rangle>\<^sub>ii_prod\<rangle>\<^sub>ii_list\<rangle>\<^sub>ii_nres
[PROOF STEP]
by simp


[STATEMENT]
lemma map_to_sorted_list_pat[autoref_op_pat]:
    "it_to_sorted_list (key_rel R) (map_to_set M)
      \<equiv> OP (map_to_sorted_list R) M"
    "it_to_sorted_list (\<lambda>_ _. True) (map_to_set M)
      \<equiv> OP (map_to_sorted_list (\<lambda>_ _. True)) M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (it_to_sorted_list (key_rel R) (map_to_set M) \<equiv> OP (map_to_sorted_list R) M) &&& it_to_sorted_list (\<lambda>_ _. True) (map_to_set M) \<equiv> OP (map_to_sorted_list (\<lambda>_ _. True)) M
[PROOF STEP]
unfolding map_to_sorted_list_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (it_to_sorted_list (key_rel R) (map_to_set M) \<equiv> OP (\<lambda>M. it_to_sorted_list (key_rel R) (map_to_set M)) M) &&& it_to_sorted_list (\<lambda>_ _. True) (map_to_set M) \<equiv> OP (\<lambda>M. it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set M)) M
[PROOF STEP]
by auto


[STATEMENT]
lemma is_set_to_sorted_listE:
    assumes "is_set_to_sorted_list ordR Rk Rs tsl"
    assumes "(s,s')\<in>\<langle>Rk\<rangle>Rs"
    obtains l' where "(tsl s,l')\<in>\<langle>Rk\<rangle>list_rel"
    and "RETURN l' \<le> it_to_sorted_list ordR s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>(tsl s, l') \<in> \<langle>Rk\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list ordR s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_set_to_sorted_list ordR Rk Rs tsl
(s, s') \<in> \<langle>Rk\<rangle>Rs

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>(tsl s, l') \<in> \<langle>Rk\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list ordR s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_set_to_sorted_list_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s s'. (s, s') \<in> \<langle>Rk\<rangle>Rs \<longrightarrow> (\<exists>l'. (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list ordR s')
(s, s') \<in> \<langle>Rk\<rangle>Rs

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>(tsl s, l') \<in> \<langle>Rk\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list ordR s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma it_to_sorted_list_weaken:
    "R\<le>R' \<Longrightarrow> it_to_sorted_list R s \<le> it_to_sorted_list R' s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<le> R' \<Longrightarrow> it_to_sorted_list R s \<le> it_to_sorted_list R' s
[PROOF STEP]
unfolding it_to_sorted_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<le> R' \<Longrightarrow> SPEC (\<lambda>l. distinct l \<and> s = set l \<and> sorted_wrt R l) \<le> SPEC (\<lambda>l. distinct l \<and> s = set l \<and> sorted_wrt R' l)
[PROOF STEP]
by (auto intro!: sorted_wrt_mono_rel[where P=R])


[STATEMENT]
lemma set_to_list_by_set_to_sorted_list[autoref_ga_rules]:
    assumes "GEN_ALGO_tag (is_set_to_sorted_list ordR Rk Rs tsl)"
    shows "is_set_to_list Rk Rs tsl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_set_to_list Rk Rs tsl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
GEN_ALGO_tag (is_set_to_sorted_list ordR Rk Rs tsl)

goal (1 subgoal):
 1. is_set_to_list Rk Rs tsl
[PROOF STEP]
unfolding is_set_to_list_def is_set_to_sorted_list_def autoref_tag_defs
[PROOF STATE]
proof (prove)
using this:
\<forall>s s'. (s, s') \<in> \<langle>Rk\<rangle>Rs \<longrightarrow> (\<exists>l'. (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list ordR s')

goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> \<langle>Rk\<rangle>Rs \<longrightarrow> (\<exists>l'. (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (\<lambda>_ _. True) s')
[PROOF STEP]
apply (safe)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>s s'. (s, s') \<in> \<langle>Rk\<rangle>Rs \<longrightarrow> (\<exists>l'. (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list ordR s'); (s, s') \<in> \<langle>Rk\<rangle>Rs\<rbrakk> \<Longrightarrow> \<exists>l'. (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (\<lambda>_ _. True) s'
[PROOF STEP]
apply (drule spec, drule spec, drule (1) mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> \<langle>Rk\<rangle>Rs; \<exists>l'. (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list ordR s'\<rbrakk> \<Longrightarrow> \<exists>l'. (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (\<lambda>_ _. True) s'
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' l'. \<lbrakk>(s, s') \<in> \<langle>Rk\<rangle>Rs; (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list ordR s'\<rbrakk> \<Longrightarrow> \<exists>l'. (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (\<lambda>_ _. True) s'
[PROOF STEP]
apply (rule exI, rule conjI, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' l'. \<lbrakk>(s, s') \<in> \<langle>Rk\<rangle>Rs; (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list ordR s'\<rbrakk> \<Longrightarrow> RETURN l' \<le> it_to_sorted_list (\<lambda>_ _. True) s'
[PROOF STEP]
apply (rule order_trans, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' l'. \<lbrakk>(s, s') \<in> \<langle>Rk\<rangle>Rs; (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list ordR s'\<rbrakk> \<Longrightarrow> it_to_sorted_list ordR s' \<le> it_to_sorted_list (\<lambda>_ _. True) s'
[PROOF STEP]
apply (rule it_to_sorted_list_weaken)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' l'. \<lbrakk>(s, s') \<in> \<langle>Rk\<rangle>Rs; (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list ordR s'\<rbrakk> \<Longrightarrow> ordR \<le> (\<lambda>_ _. True)
[PROOF STEP]
by blast


[STATEMENT]
lemma det_fold_setI[intro?]:
    assumes "\<And>l. \<lbrakk>distinct l; sorted_wrt R l\<rbrakk>
      \<Longrightarrow> foldli l c f \<sigma> = result (set l)"
    shows "det_fold_set R c f \<sigma> result"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det_fold_set R c f \<sigma> result
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct ?l; sorted_wrt R ?l\<rbrakk> \<Longrightarrow> foldli ?l c f \<sigma> = result (set ?l)

goal (1 subgoal):
 1. det_fold_set R c f \<sigma> result
[PROOF STEP]
unfolding det_fold_set_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct ?l; sorted_wrt R ?l\<rbrakk> \<Longrightarrow> foldli ?l c f \<sigma> = result (set ?l)

goal (1 subgoal):
 1. \<forall>l. distinct l \<and> sorted_wrt R l \<longrightarrow> foldli l c f \<sigma> = result (set l)
[PROOF STEP]
by auto


[STATEMENT]
lemma det_fold_sorted_set:
    assumes 1: "det_fold_set ordR c' f' \<sigma>' result"
    assumes 2: "is_set_to_sorted_list ordR Rk Rs tsl"
    assumes SREF[param]: "(s,s')\<in>\<langle>Rk\<rangle>Rs"
    assumes [param]:  "(c,c')\<in>R\<sigma>\<rightarrow>Id"
    assumes [param]: "(f,f')\<in>Rk \<rightarrow> R\<sigma> \<rightarrow> R\<sigma>"
    assumes [param]: "(\<sigma>,\<sigma>')\<in>R\<sigma>"
    shows "(foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>
[PROOF STEP]
obtain tsl' where
      [param]: "(tsl s,tsl') \<in> \<langle>Rk\<rangle>list_rel"
      and IT: "RETURN tsl' \<le> it_to_sorted_list ordR s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tsl'. \<lbrakk>(tsl s, tsl') \<in> \<langle>Rk\<rangle>list_rel; RETURN tsl' \<le> it_to_sorted_list ordR s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 2 SREF
[PROOF STATE]
proof (prove)
using this:
is_set_to_sorted_list ordR Rk Rs tsl
(s, s') \<in> \<langle>Rk\<rangle>Rs

goal (1 subgoal):
 1. (\<And>tsl'. \<lbrakk>(tsl s, tsl') \<in> \<langle>Rk\<rangle>list_rel; RETURN tsl' \<le> it_to_sorted_list ordR s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule is_set_to_sorted_listE)
[PROOF STATE]
proof (state)
this:
(tsl s, tsl') \<in> \<langle>Rk\<rangle>list_rel
RETURN tsl' \<le> it_to_sorted_list ordR s'

goal (1 subgoal):
 1. (foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>
[PROOF STEP]
have "(foldli (tsl s) c f \<sigma>, foldli tsl' c' f' \<sigma>') \<in> R\<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (foldli (tsl s) c f \<sigma>, foldli tsl' c' f' \<sigma>') \<in> R\<sigma>
[PROOF STEP]
by parametricity
[PROOF STATE]
proof (state)
this:
(foldli (tsl s) c f \<sigma>, foldli tsl' c' f' \<sigma>') \<in> R\<sigma>

goal (1 subgoal):
 1. (foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(foldli (tsl s) c f \<sigma>, foldli tsl' c' f' \<sigma>') \<in> R\<sigma>

goal (1 subgoal):
 1. (foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>
[PROOF STEP]
have "foldli tsl' c' f' \<sigma>' = result s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli tsl' c' f' \<sigma>' = result s'
[PROOF STEP]
using 1 IT
[PROOF STATE]
proof (prove)
using this:
det_fold_set ordR c' f' \<sigma>' result
RETURN tsl' \<le> it_to_sorted_list ordR s'

goal (1 subgoal):
 1. foldli tsl' c' f' \<sigma>' = result s'
[PROOF STEP]
unfolding det_fold_set_def it_to_sorted_list_def
[PROOF STATE]
proof (prove)
using this:
\<forall>l. distinct l \<and> sorted_wrt ordR l \<longrightarrow> foldli l c' f' \<sigma>' = result (set l)
RETURN tsl' \<le> SPEC (\<lambda>l. distinct l \<and> s' = set l \<and> sorted_wrt ordR l)

goal (1 subgoal):
 1. foldli tsl' c' f' \<sigma>' = result s'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
foldli tsl' c' f' \<sigma>' = result s'

goal (1 subgoal):
 1. (foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>

goal (1 subgoal):
 1. (foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_fold_set:
    assumes "det_fold_set (\<lambda>_ _. True) c' f' \<sigma>' result"
    assumes "is_set_to_list Rk Rs tsl"
    assumes "(s,s')\<in>\<langle>Rk\<rangle>Rs"
    assumes "(c,c')\<in>R\<sigma>\<rightarrow>Id"
    assumes "(f,f')\<in>Rk \<rightarrow> R\<sigma> \<rightarrow> R\<sigma>"
    assumes "(\<sigma>,\<sigma>')\<in>R\<sigma>"
    shows "(foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
det_fold_set (\<lambda>_ _. True) c' f' \<sigma>' result
is_set_to_list Rk Rs tsl
(s, s') \<in> \<langle>Rk\<rangle>Rs
(c, c') \<in> R\<sigma> \<rightarrow> bool_rel
(f, f') \<in> Rk \<rightarrow> R\<sigma> \<rightarrow> R\<sigma>
(\<sigma>, \<sigma>') \<in> R\<sigma>

goal (1 subgoal):
 1. (foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>
[PROOF STEP]
unfolding  is_set_to_list_def
[PROOF STATE]
proof (prove)
using this:
det_fold_set (\<lambda>_ _. True) c' f' \<sigma>' result
is_set_to_sorted_list (\<lambda>_ _. True) Rk Rs tsl
(s, s') \<in> \<langle>Rk\<rangle>Rs
(c, c') \<in> R\<sigma> \<rightarrow> bool_rel
(f, f') \<in> Rk \<rightarrow> R\<sigma> \<rightarrow> R\<sigma>
(\<sigma>, \<sigma>') \<in> R\<sigma>

goal (1 subgoal):
 1. (foldli (tsl s) c f \<sigma>, result s') \<in> R\<sigma>
[PROOF STEP]
by (rule det_fold_sorted_set)


[STATEMENT]
lemma is_map_to_sorted_listE:
    assumes "is_map_to_sorted_list ordR Rk Rv Rm tsl"
    assumes "(m,m')\<in>\<langle>Rk,Rv\<rangle>Rm"
    obtains l' where "(tsl m,l')\<in>\<langle>\<langle>Rk,Rv\<rangle>prod_rel\<rangle>list_rel"
    and "RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>(tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_map_to_sorted_list ordR Rk Rv Rm tsl
(m, m') \<in> \<langle>Rk, Rv\<rangle>Rm

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>(tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_map_to_sorted_list_def
[PROOF STATE]
proof (prove)
using this:
\<forall>m m'. (m, m') \<in> \<langle>Rk, Rv\<rangle>Rm \<longrightarrow> (\<exists>l'. (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m'))
(m, m') \<in> \<langle>Rk, Rv\<rangle>Rm

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>(tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma map_to_list_by_map_to_sorted_list[autoref_ga_rules]:
    assumes "GEN_ALGO_tag (is_map_to_sorted_list ordR Rk Rv Rm tsl)"
    shows "is_map_to_list Rk Rv Rm tsl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_map_to_list Rk Rv Rm tsl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
GEN_ALGO_tag (is_map_to_sorted_list ordR Rk Rv Rm tsl)

goal (1 subgoal):
 1. is_map_to_list Rk Rv Rm tsl
[PROOF STEP]
unfolding is_map_to_list_def is_map_to_sorted_list_def autoref_tag_defs
[PROOF STATE]
proof (prove)
using this:
\<forall>m m'. (m, m') \<in> \<langle>Rk, Rv\<rangle>Rm \<longrightarrow> (\<exists>l'. (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m'))

goal (1 subgoal):
 1. \<forall>m m'. (m, m') \<in> \<langle>Rk, Rv\<rangle>Rm \<longrightarrow> (\<exists>l'. (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m'))
[PROOF STEP]
apply (safe)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>\<forall>m m'. (m, m') \<in> \<langle>Rk, Rv\<rangle>Rm \<longrightarrow> (\<exists>l'. (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')); (m, m') \<in> \<langle>Rk, Rv\<rangle>Rm\<rbrakk> \<Longrightarrow> \<exists>l'. (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
apply (drule spec, drule spec, drule (1) mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m'. \<lbrakk>(m, m') \<in> \<langle>Rk, Rv\<rangle>Rm; \<exists>l'. (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')\<rbrakk> \<Longrightarrow> \<exists>l'. (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
apply (elim exE conjE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m' l'. \<lbrakk>(m, m') \<in> \<langle>Rk, Rv\<rangle>Rm; (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')\<rbrakk> \<Longrightarrow> \<exists>l'. (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
apply (rule exI, rule conjI, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m' l'. \<lbrakk>(m, m') \<in> \<langle>Rk, Rv\<rangle>Rm; (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')\<rbrakk> \<Longrightarrow> RETURN l' \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
apply (rule order_trans, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m' l'. \<lbrakk>(m, m') \<in> \<langle>Rk, Rv\<rangle>Rm; (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')\<rbrakk> \<Longrightarrow> it_to_sorted_list (key_rel ordR) (map_to_set m') \<le> it_to_sorted_list (key_rel (\<lambda>_ _. True)) (map_to_set m')
[PROOF STEP]
apply (rule it_to_sorted_list_weaken)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m' l'. \<lbrakk>(m, m') \<in> \<langle>Rk, Rv\<rangle>Rm; (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')\<rbrakk> \<Longrightarrow> key_rel ordR \<le> key_rel (\<lambda>_ _. True)
[PROOF STEP]
unfolding key_rel_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m m' l'. \<lbrakk>(m, m') \<in> \<langle>Rk, Rv\<rangle>Rm; (tsl m, l') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list (\<lambda>a b. ordR (fst a) (fst b)) (map_to_set m')\<rbrakk> \<Longrightarrow> (\<lambda>a b. ordR (fst a) (fst b)) \<le> (\<lambda>a b. True)
[PROOF STEP]
by blast


[STATEMENT]
lemma det_fold_mapI[intro?]:
    assumes "\<And>l. \<lbrakk>distinct (map fst l); sorted_wrt (key_rel R) l\<rbrakk>
      \<Longrightarrow> foldli l c f \<sigma> = result (map_of l)"
    shows "det_fold_map R c f \<sigma> result"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det_fold_map R c f \<sigma> result
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (map fst ?l); sorted_wrt (key_rel R) ?l\<rbrakk> \<Longrightarrow> foldli ?l c f \<sigma> = result (map_of ?l)

goal (1 subgoal):
 1. det_fold_map R c f \<sigma> result
[PROOF STEP]
unfolding det_fold_map_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>distinct (map fst ?l); sorted_wrt (key_rel R) ?l\<rbrakk> \<Longrightarrow> foldli ?l c f \<sigma> = result (map_of ?l)

goal (1 subgoal):
 1. \<forall>l. distinct (map fst l) \<and> sorted_wrt (key_rel R) l \<longrightarrow> foldli l c f \<sigma> = result (map_of l)
[PROOF STEP]
by auto


[STATEMENT]
lemma det_fold_map_aux:
    assumes 1: "\<lbrakk>distinct (map fst l); sorted_wrt (key_rel R) l \<rbrakk>
      \<Longrightarrow> foldli l c f \<sigma> = result (map_of l)"
    assumes 2: "RETURN l \<le> it_to_sorted_list (key_rel R) (map_to_set m)"
    shows "foldli l c f \<sigma> = result m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli l c f \<sigma> = result m
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. foldli l c f \<sigma> = result m
[PROOF STEP]
from 2
[PROOF STATE]
proof (chain)
picking this:
RETURN l \<le> it_to_sorted_list (key_rel R) (map_to_set m)
[PROOF STEP]
have "distinct l" and "set l = map_to_set m"
      and SORTED: "sorted_wrt (key_rel R) l"
[PROOF STATE]
proof (prove)
using this:
RETURN l \<le> it_to_sorted_list (key_rel R) (map_to_set m)

goal (1 subgoal):
 1. distinct l &&& set l = map_to_set m &&& sorted_wrt (key_rel R) l
[PROOF STEP]
unfolding it_to_sorted_list_def
[PROOF STATE]
proof (prove)
using this:
RETURN l \<le> SPEC (\<lambda>l. distinct l \<and> map_to_set m = set l \<and> sorted_wrt (key_rel R) l)

goal (1 subgoal):
 1. distinct l &&& set l = map_to_set m &&& sorted_wrt (key_rel R) l
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
distinct l
set l = map_to_set m
sorted_wrt (key_rel R) l

goal (1 subgoal):
 1. foldli l c f \<sigma> = result m
[PROOF STEP]
hence "\<forall>(k,v)\<in>set l. \<forall>(k',v')\<in>set l. k=k' \<longrightarrow> v=v'"
[PROOF STATE]
proof (prove)
using this:
distinct l
set l = map_to_set m
sorted_wrt (key_rel R) l

goal (1 subgoal):
 1. \<forall>(k, v)\<in>set l. \<forall>(k', v')\<in>set l. k = k' \<longrightarrow> v = v'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct l; set l = map_to_set m; sorted_wrt (key_rel R) l\<rbrakk> \<Longrightarrow> \<forall>x\<in>map_to_set m. case x of (k, v) \<Rightarrow> \<forall>x\<in>map_to_set m. case x of (k', v') \<Rightarrow> k = k' \<longrightarrow> v = v'
[PROOF STEP]
unfolding map_to_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct l; set l = {(k, v). m k = Some v}; sorted_wrt (key_rel R) l\<rbrakk> \<Longrightarrow> \<forall>x\<in>{(k, v). m k = Some v}. case x of (k, v) \<Rightarrow> \<forall>x\<in>{(k, v). m k = Some v}. case x of (k', v') \<Rightarrow> k = k' \<longrightarrow> v = v'
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>(k, v)\<in>set l. \<forall>(k', v')\<in>set l. k = k' \<longrightarrow> v = v'

goal (1 subgoal):
 1. foldli l c f \<sigma> = result m
[PROOF STEP]
with \<open>distinct l\<close>
[PROOF STATE]
proof (chain)
picking this:
distinct l
\<forall>(k, v)\<in>set l. \<forall>(k', v')\<in>set l. k = k' \<longrightarrow> v = v'
[PROOF STEP]
have DF: "distinct (map fst l)"
[PROOF STATE]
proof (prove)
using this:
distinct l
\<forall>(k, v)\<in>set l. \<forall>(k', v')\<in>set l. k = k' \<longrightarrow> v = v'

goal (1 subgoal):
 1. distinct (map fst l)
[PROOF STEP]
apply (induct l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct []; \<forall>(k, v)\<in>set []. \<forall>(k', v')\<in>set []. k = k' \<longrightarrow> v = v'\<rbrakk> \<Longrightarrow> distinct (map fst [])
 2. \<And>a l. \<lbrakk>\<lbrakk>distinct l; \<forall>(k, v)\<in>set l. \<forall>(k', v')\<in>set l. k = k' \<longrightarrow> v = v'\<rbrakk> \<Longrightarrow> distinct (map fst l); distinct (a # l); \<forall>(k, v)\<in>set (a # l). \<forall>(k', v')\<in>set (a # l). k = k' \<longrightarrow> v = v'\<rbrakk> \<Longrightarrow> distinct (map fst (a # l))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a l. \<lbrakk>\<lbrakk>distinct l; \<forall>(k, v)\<in>set l. \<forall>(k', v')\<in>set l. k = k' \<longrightarrow> v = v'\<rbrakk> \<Longrightarrow> distinct (map fst l); distinct (a # l); \<forall>(k, v)\<in>set (a # l). \<forall>(k', v')\<in>set (a # l). k = k' \<longrightarrow> v = v'\<rbrakk> \<Longrightarrow> distinct (map fst (a # l))
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
distinct (map fst l)

goal (1 subgoal):
 1. foldli l c f \<sigma> = result m
[PROOF STEP]
with \<open>set l = map_to_set m\<close>
[PROOF STATE]
proof (chain)
picking this:
set l = map_to_set m
distinct (map fst l)
[PROOF STEP]
have [simp]: "m = map_of l"
[PROOF STATE]
proof (prove)
using this:
set l = map_to_set m
distinct (map fst l)

goal (1 subgoal):
 1. m = map_of l
[PROOF STEP]
by (metis map_of_map_to_set)
[PROOF STATE]
proof (state)
this:
m = map_of l

goal (1 subgoal):
 1. foldli l c f \<sigma> = result m
[PROOF STEP]
from 1[OF DF SORTED]
[PROOF STATE]
proof (chain)
picking this:
foldli l c f \<sigma> = result (map_of l)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
foldli l c f \<sigma> = result (map_of l)

goal (1 subgoal):
 1. foldli l c f \<sigma> = result m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
foldli l c f \<sigma> = result m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_fold_sorted_map:
    assumes 1: "det_fold_map ordR c' f' \<sigma>' result"
    assumes 2: "is_map_to_sorted_list ordR Rk Rv Rm tsl"
    assumes MREF[param]: "(m,m')\<in>\<langle>Rk,Rv\<rangle>Rm"
    assumes [param]:  "(c,c')\<in>R\<sigma>\<rightarrow>Id"
    assumes [param]: "(f,f')\<in>\<langle>Rk,Rv\<rangle>prod_rel \<rightarrow> R\<sigma> \<rightarrow> R\<sigma>"
    assumes [param]: "(\<sigma>,\<sigma>')\<in>R\<sigma>"
    shows "(foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>
[PROOF STEP]
obtain tsl' where
      [param]: "(tsl m,tsl') \<in> \<langle>\<langle>Rk,Rv\<rangle>prod_rel\<rangle>list_rel"
      and IT: "RETURN tsl' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tsl'. \<lbrakk>(tsl m, tsl') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN tsl' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 2 MREF
[PROOF STATE]
proof (prove)
using this:
is_map_to_sorted_list ordR Rk Rv Rm tsl
(m, m') \<in> \<langle>Rk, Rv\<rangle>Rm

goal (1 subgoal):
 1. (\<And>tsl'. \<lbrakk>(tsl m, tsl') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel; RETURN tsl' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule is_map_to_sorted_listE)
[PROOF STATE]
proof (state)
this:
(tsl m, tsl') \<in> \<langle>Rk \<times>\<^sub>r Rv\<rangle>list_rel
RETURN tsl' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')

goal (1 subgoal):
 1. (foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>
[PROOF STEP]
have "(foldli (tsl m) c f \<sigma>, foldli tsl' c' f' \<sigma>') \<in> R\<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (foldli (tsl m) c f \<sigma>, foldli tsl' c' f' \<sigma>') \<in> R\<sigma>
[PROOF STEP]
by parametricity
[PROOF STATE]
proof (state)
this:
(foldli (tsl m) c f \<sigma>, foldli tsl' c' f' \<sigma>') \<in> R\<sigma>

goal (1 subgoal):
 1. (foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(foldli (tsl m) c f \<sigma>, foldli tsl' c' f' \<sigma>') \<in> R\<sigma>

goal (1 subgoal):
 1. (foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>
[PROOF STEP]
have "foldli tsl' c' f' \<sigma>' = result m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli tsl' c' f' \<sigma>' = result m'
[PROOF STEP]
using det_fold_map_aux[of tsl' ordR c' f' \<sigma>' result] 1 IT
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>distinct (map fst tsl'); sorted_wrt (key_rel ordR) tsl'\<rbrakk> \<Longrightarrow> foldli tsl' c' f' \<sigma>' = result (map_of tsl'); RETURN tsl' \<le> it_to_sorted_list (key_rel ordR) (map_to_set ?m)\<rbrakk> \<Longrightarrow> foldli tsl' c' f' \<sigma>' = result ?m
det_fold_map ordR c' f' \<sigma>' result
RETURN tsl' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')

goal (1 subgoal):
 1. foldli tsl' c' f' \<sigma>' = result m'
[PROOF STEP]
unfolding det_fold_map_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<lbrakk>distinct (map fst tsl'); sorted_wrt (key_rel ordR) tsl'\<rbrakk> \<Longrightarrow> foldli tsl' c' f' \<sigma>' = result (map_of tsl'); RETURN tsl' \<le> it_to_sorted_list (key_rel ordR) (map_to_set ?m)\<rbrakk> \<Longrightarrow> foldli tsl' c' f' \<sigma>' = result ?m
\<forall>l. distinct (map fst l) \<and> sorted_wrt (key_rel ordR) l \<longrightarrow> foldli l c' f' \<sigma>' = result (map_of l)
RETURN tsl' \<le> it_to_sorted_list (key_rel ordR) (map_to_set m')

goal (1 subgoal):
 1. foldli tsl' c' f' \<sigma>' = result m'
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
foldli tsl' c' f' \<sigma>' = result m'

goal (1 subgoal):
 1. (foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>

goal (1 subgoal):
 1. (foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma det_fold_map:
    assumes "det_fold_map (\<lambda>_ _. True) c' f' \<sigma>' result"
    assumes "is_map_to_list Rk Rv Rm tsl"
    assumes "(m,m')\<in>\<langle>Rk,Rv\<rangle>Rm"
    assumes "(c,c')\<in>R\<sigma>\<rightarrow>Id"
    assumes "(f,f')\<in>\<langle>Rk,Rv\<rangle>prod_rel \<rightarrow> R\<sigma> \<rightarrow> R\<sigma>"
    assumes "(\<sigma>,\<sigma>')\<in>R\<sigma>"
    shows "(foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
det_fold_map (\<lambda>_ _. True) c' f' \<sigma>' result
is_map_to_list Rk Rv Rm tsl
(m, m') \<in> \<langle>Rk, Rv\<rangle>Rm
(c, c') \<in> R\<sigma> \<rightarrow> bool_rel
(f, f') \<in> Rk \<times>\<^sub>r Rv \<rightarrow> R\<sigma> \<rightarrow> R\<sigma>
(\<sigma>, \<sigma>') \<in> R\<sigma>

goal (1 subgoal):
 1. (foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>
[PROOF STEP]
unfolding is_map_to_list_def
[PROOF STATE]
proof (prove)
using this:
det_fold_map (\<lambda>_ _. True) c' f' \<sigma>' result
is_map_to_sorted_list (\<lambda>_ _. True) Rk Rv Rm tsl
(m, m') \<in> \<langle>Rk, Rv\<rangle>Rm
(c, c') \<in> R\<sigma> \<rightarrow> bool_rel
(f, f') \<in> Rk \<times>\<^sub>r Rv \<rightarrow> R\<sigma> \<rightarrow> R\<sigma>
(\<sigma>, \<sigma>') \<in> R\<sigma>

goal (1 subgoal):
 1. (foldli (tsl m) c f \<sigma>, result m') \<in> R\<sigma>
[PROOF STEP]
by (rule det_fold_sorted_map)


[STATEMENT]
lemma set_to_sorted_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 11)"
  assumes TSL: "SIDE_GEN_ALGO (is_set_to_sorted_list R Rk Rs tsl)"
  shows "(\<lambda>s. RETURN (tsl s), set_to_sorted_list R)
    \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>\<langle>Rk\<rangle>list_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. RETURN (tsl s), set_to_sorted_list R) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>\<langle>Rk\<rangle>list_rel\<rangle>nres_rel
[PROOF STEP]
proof (intro fun_relI nres_relI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R a')
[PROOF STEP]
fix s s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R a')
[PROOF STEP]
assume "(s,s')\<in>\<langle>Rk\<rangle>Rs"
[PROOF STATE]
proof (state)
this:
(s, s') \<in> \<langle>Rk\<rangle>Rs

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R a')
[PROOF STEP]
with TSL
[PROOF STATE]
proof (chain)
picking this:
SIDE_GEN_ALGO (is_set_to_sorted_list R Rk Rs tsl)
(s, s') \<in> \<langle>Rk\<rangle>Rs
[PROOF STEP]
obtain l' where
    R1: "(tsl s, l') \<in> \<langle>Rk\<rangle>list_rel"
      and R2: "RETURN l' \<le> set_to_sorted_list R s'"
[PROOF STATE]
proof (prove)
using this:
SIDE_GEN_ALGO (is_set_to_sorted_list R Rk Rs tsl)
(s, s') \<in> \<langle>Rk\<rangle>Rs

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>(tsl s, l') \<in> \<langle>Rk\<rangle>list_rel; RETURN l' \<le> set_to_sorted_list R s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_set_to_sorted_list_def set_to_sorted_list_def autoref_tag_defs
[PROOF STATE]
proof (prove)
using this:
\<forall>s s'. (s, s') \<in> \<langle>Rk\<rangle>Rs \<longrightarrow> (\<exists>l'. (tsl s, l') \<in> \<langle>Rk\<rangle>list_rel \<and> RETURN l' \<le> it_to_sorted_list R s')
(s, s') \<in> \<langle>Rk\<rangle>Rs

goal (1 subgoal):
 1. (\<And>l'. \<lbrakk>(tsl s, l') \<in> \<langle>Rk\<rangle>list_rel; RETURN l' \<le> it_to_sorted_list R s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(tsl s, l') \<in> \<langle>Rk\<rangle>list_rel
RETURN l' \<le> set_to_sorted_list R s'

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R a')
[PROOF STEP]
have "RETURN (tsl s) \<le> \<Down>(\<langle>Rk\<rangle>list_rel) (RETURN l')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RETURN (tsl s) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (RETURN l')
[PROOF STEP]
by (rule RETURN_refine) fact
[PROOF STATE]
proof (state)
this:
RETURN (tsl s) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (RETURN l')

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R a')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
RETURN (tsl s) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (RETURN l')

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R a')
[PROOF STEP]
note R2
[PROOF STATE]
proof (state)
this:
RETURN l' \<le> set_to_sorted_list R s'

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> RETURN (tsl a) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R a')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
RETURN (tsl s) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R s')
[PROOF STEP]
show "RETURN (tsl s) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R s')"
[PROOF STATE]
proof (prove)
using this:
RETURN (tsl s) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R s')

goal (1 subgoal):
 1. RETURN (tsl s) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R s')
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
RETURN (tsl s) \<le> \<Down> (\<langle>Rk\<rangle>list_rel) (set_to_sorted_list R s')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_to_list_by_tsl[autoref_rules]:
  assumes "MINOR_PRIO_TAG (- 10)"
  assumes TSL: "SIDE_GEN_ALGO (is_set_to_list Rk Rs tsl)"
  shows "(\<lambda>s. RETURN (tsl s), set_to_sorted_list (\<lambda>_ _. True))
    \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>\<langle>Rk\<rangle>list_rel\<rangle>nres_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. RETURN (tsl s), set_to_sorted_list (\<lambda>_ _. True)) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>\<langle>Rk\<rangle>list_rel\<rangle>nres_rel
[PROOF STEP]
using assms(2-)
[PROOF STATE]
proof (prove)
using this:
SIDE_GEN_ALGO (is_set_to_list Rk Rs tsl)

goal (1 subgoal):
 1. (\<lambda>s. RETURN (tsl s), set_to_sorted_list (\<lambda>_ _. True)) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>\<langle>Rk\<rangle>list_rel\<rangle>nres_rel
[PROOF STEP]
unfolding is_set_to_list_def
[PROOF STATE]
proof (prove)
using this:
SIDE_GEN_ALGO (is_set_to_sorted_list (\<lambda>_ _. True) Rk Rs tsl)

goal (1 subgoal):
 1. (\<lambda>s. RETURN (tsl s), set_to_sorted_list (\<lambda>_ _. True)) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>\<langle>Rk\<rangle>list_rel\<rangle>nres_rel
[PROOF STEP]
by (rule set_to_sorted_list_by_tsl[OF PRIO_TAGI])