[STATEMENT]
lemma expandHnf:
  fixes P :: pi
  and   Q :: pi

  shows "\<forall>R \<in> (expandSet P Q). hnf R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>R\<in>expandSet P Q. hnf R
[PROOF STEP]
by(force simp add: expandSet_def)


[STATEMENT]
lemma expandAction:
  fixes P :: pi
  and   Q :: pi
  and   S :: "pi set"

  assumes "(P, S) \<in> sumComposeSet"
  and     "Q \<in> S"
  and     "Q \<longmapsto> Rs"

  shows "P \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<longmapsto> Rs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(P, S) \<in> sumComposeSet
Q \<in> S
Q \<longmapsto> Rs

goal (1 subgoal):
 1. P \<longmapsto> Rs
[PROOF STEP]
proof(induct arbitrary: Q rule: sumComposeSet.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Q. \<lbrakk>Q \<in> {}; Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<zero> \<longmapsto> Rs
 2. \<And>Q S P Qa. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; \<And>Qa. \<lbrakk>Qa \<in> S - {Q}; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs; Qa \<in> S; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<oplus> Q \<longmapsto> Rs
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
Q \<in> {}
Q \<longmapsto> Rs

goal (2 subgoals):
 1. \<And>Q. \<lbrakk>Q \<in> {}; Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<zero> \<longmapsto> Rs
 2. \<And>Q S P Qa. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; \<And>Qa. \<lbrakk>Qa \<in> S - {Q}; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs; Qa \<in> S; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<oplus> Q \<longmapsto> Rs
[PROOF STEP]
have "Q \<in> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<in> {}
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<in> {}

goal (2 subgoals):
 1. \<And>Q. \<lbrakk>Q \<in> {}; Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<zero> \<longmapsto> Rs
 2. \<And>Q S P Qa. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; \<And>Qa. \<lbrakk>Qa \<in> S - {Q}; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs; Qa \<in> S; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<oplus> Q \<longmapsto> Rs
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
Q \<in> {}

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<And>Q. \<lbrakk>Q \<in> {}; Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<zero> \<longmapsto> Rs
 2. \<And>Q S P Qa. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; \<And>Qa. \<lbrakk>Qa \<in> S - {Q}; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs; Qa \<in> S; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<oplus> Q \<longmapsto> Rs
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<zero> \<longmapsto> Rs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<zero> \<longmapsto> Rs

goal (1 subgoal):
 1. \<And>Q S P Qa. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; \<And>Qa. \<lbrakk>Qa \<in> S - {Q}; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs; Qa \<in> S; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<oplus> Q \<longmapsto> Rs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q S P Qa. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; \<And>Qa. \<lbrakk>Qa \<in> S - {Q}; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs; Qa \<in> S; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<oplus> Q \<longmapsto> Rs
[PROOF STEP]
case(insert Q' S P Q)
[PROOF STATE]
proof (state)
this:
Q' \<in> S
(P, S - {Q'}) \<in> sumComposeSet
\<lbrakk>?Q \<in> S - {Q'}; ?Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs
Q \<in> S
Q \<longmapsto> Rs

goal (1 subgoal):
 1. \<And>Q S P Qa. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; \<And>Qa. \<lbrakk>Qa \<in> S - {Q}; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs; Qa \<in> S; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<oplus> Q \<longmapsto> Rs
[PROOF STEP]
have QTrans: "Q \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<longmapsto> Rs
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> Rs

goal (1 subgoal):
 1. \<And>Q S P Qa. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; \<And>Qa. \<lbrakk>Qa \<in> S - {Q}; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs; Qa \<in> S; Qa \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<oplus> Q \<longmapsto> Rs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
proof(case_tac "Q = Q'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Q = Q' \<Longrightarrow> P \<oplus> Q' \<longmapsto> Rs
 2. Q \<noteq> Q' \<Longrightarrow> P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
assume "Q = Q'"
[PROOF STATE]
proof (state)
this:
Q = Q'

goal (2 subgoals):
 1. Q = Q' \<Longrightarrow> P \<oplus> Q' \<longmapsto> Rs
 2. Q \<noteq> Q' \<Longrightarrow> P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
with QTrans
[PROOF STATE]
proof (chain)
picking this:
Q \<longmapsto> Rs
Q = Q'
[PROOF STEP]
show "P \<oplus> Q' \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto> Rs
Q = Q'

goal (1 subgoal):
 1. P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
by(blast intro: Sum2)
[PROOF STATE]
proof (state)
this:
P \<oplus> Q' \<longmapsto> Rs

goal (1 subgoal):
 1. Q \<noteq> Q' \<Longrightarrow> P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q \<noteq> Q' \<Longrightarrow> P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
assume QineqQ': "Q \<noteq> Q'"
[PROOF STATE]
proof (state)
this:
Q \<noteq> Q'

goal (1 subgoal):
 1. Q \<noteq> Q' \<Longrightarrow> P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
have IH: "\<And>Q. \<lbrakk>Q \<in> S - {Q'}; Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Q. \<lbrakk>Q \<in> S - {Q'}; Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<lbrakk>?Q \<in> S - {Q'}; ?Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> P \<longmapsto> Rs

goal (1 subgoal):
 1. Q \<noteq> Q' \<Longrightarrow> P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
have QinS: "Q \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<in> S
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<in> S

goal (1 subgoal):
 1. Q \<noteq> Q' \<Longrightarrow> P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
with QineqQ'
[PROOF STATE]
proof (chain)
picking this:
Q \<noteq> Q'
Q \<in> S
[PROOF STEP]
have "Q \<in> S - {Q'}"
[PROOF STATE]
proof (prove)
using this:
Q \<noteq> Q'
Q \<in> S

goal (1 subgoal):
 1. Q \<in> S - {Q'}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Q \<in> S - {Q'}

goal (1 subgoal):
 1. Q \<noteq> Q' \<Longrightarrow> P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
hence "P \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
using this:
Q \<in> S - {Q'}

goal (1 subgoal):
 1. P \<longmapsto> Rs
[PROOF STEP]
using QTrans
[PROOF STATE]
proof (prove)
using this:
Q \<in> S - {Q'}
Q \<longmapsto> Rs

goal (1 subgoal):
 1. P \<longmapsto> Rs
[PROOF STEP]
by(rule IH)
[PROOF STATE]
proof (state)
this:
P \<longmapsto> Rs

goal (1 subgoal):
 1. Q \<noteq> Q' \<Longrightarrow> P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> Rs

goal (1 subgoal):
 1. P \<oplus> Q' \<longmapsto> Rs
[PROOF STEP]
by(rule Sum1)
[PROOF STATE]
proof (state)
this:
P \<oplus> Q' \<longmapsto> Rs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<oplus> Q' \<longmapsto> Rs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma expandAction':
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  assumes "(R, S) \<in> sumComposeSet"
  and     "R \<longmapsto> Rs"

  shows "\<exists>P \<in> S. P \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(R, S) \<in> sumComposeSet
R \<longmapsto> Rs

goal (1 subgoal):
 1. \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
proof(induct rule: sumComposeSet.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<zero> \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>{}. P \<longmapsto> Rs
 2. \<And>Q S P. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs; P \<oplus> Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
\<zero> \<longmapsto> Rs

goal (2 subgoals):
 1. \<zero> \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>{}. P \<longmapsto> Rs
 2. \<And>Q S P. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs; P \<oplus> Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
have "\<zero> \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<zero> \<longmapsto> Rs
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<zero> \<longmapsto> Rs

goal (2 subgoals):
 1. \<zero> \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>{}. P \<longmapsto> Rs
 2. \<And>Q S P. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs; P \<oplus> Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
\<zero> \<longmapsto> Rs

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

goal (2 subgoals):
 1. \<zero> \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>{}. P \<longmapsto> Rs
 2. \<And>Q S P. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs; P \<oplus> Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>P\<in>{}. P \<longmapsto> Rs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>{}. P \<longmapsto> Rs

goal (1 subgoal):
 1. \<And>Q S P. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs; P \<oplus> Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q S P. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs; P \<oplus> Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
case(insert Q S P)
[PROOF STATE]
proof (state)
this:
Q \<in> S
(P, S - {Q}) \<in> sumComposeSet
P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs
P \<oplus> Q \<longmapsto> Rs

goal (1 subgoal):
 1. \<And>Q S P. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs; P \<oplus> Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
have QinS: "Q \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<in> S
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<in> S

goal (1 subgoal):
 1. \<And>Q S P. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs; P \<oplus> Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
have "P \<oplus> Q \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> Q \<longmapsto> Rs
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P \<oplus> Q \<longmapsto> Rs

goal (1 subgoal):
 1. \<And>Q S P. \<lbrakk>Q \<in> S; (P, S - {Q}) \<in> sumComposeSet; P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs; P \<oplus> Q \<longmapsto> Rs\<rbrakk> \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<oplus> Q \<longmapsto> Rs

goal (1 subgoal):
 1. \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
proof(induct rule: sumCases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
 2. Q \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
case cSum1
[PROOF STATE]
proof (state)
this:
P \<longmapsto> Rs

goal (2 subgoals):
 1. P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
 2. Q \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
have "P \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<longmapsto> Rs
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P \<longmapsto> Rs

goal (2 subgoals):
 1. P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
 2. Q \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<longmapsto> Rs

goal (2 subgoals):
 1. P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
 2. Q \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
have "P \<longmapsto> Rs \<Longrightarrow> \<exists>P \<in> (S - {Q}). P \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs

goal (2 subgoals):
 1. P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
 2. Q \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> Rs
P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs
[PROOF STEP]
obtain P where PinS: "P \<in> (S - {Q})" and PTrans: "P \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> Rs
P \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S - {Q}. P \<longmapsto> Rs

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>P \<in> S - {Q}; P \<longmapsto> Rs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P \<in> S - {Q}
P \<longmapsto> Rs

goal (2 subgoals):
 1. Pa__ \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
 2. Q \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
proof(case_tac "P = Q")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P = Q \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
 2. P \<noteq> Q \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
assume "P = Q"
[PROOF STATE]
proof (state)
this:
P = Q

goal (2 subgoals):
 1. P = Q \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
 2. P \<noteq> Q \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
with PTrans QinS
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> Rs
Q \<in> S
P = Q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> Rs
Q \<in> S
P = Q

goal (1 subgoal):
 1. \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>S. P \<longmapsto> Rs

goal (1 subgoal):
 1. P \<noteq> Q \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<noteq> Q \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
assume PineqQ: "P \<noteq> Q"
[PROOF STATE]
proof (state)
this:
P \<noteq> Q

goal (1 subgoal):
 1. P \<noteq> Q \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
from PinS
[PROOF STATE]
proof (chain)
picking this:
P \<in> S - {Q}
[PROOF STEP]
have "P \<in> S"
[PROOF STATE]
proof (prove)
using this:
P \<in> S - {Q}

goal (1 subgoal):
 1. P \<in> S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<in> S

goal (1 subgoal):
 1. P \<noteq> Q \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
with PTrans
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> Rs
P \<in> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> Rs
P \<in> S

goal (1 subgoal):
 1. \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>S. P \<longmapsto> Rs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>S. P \<longmapsto> Rs

goal (1 subgoal):
 1. Q \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
case cSum2
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> Rs

goal (1 subgoal):
 1. Q \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
have "Q \<longmapsto> Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<longmapsto> Rs
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> Rs

goal (1 subgoal):
 1. Q \<longmapsto> Rs \<Longrightarrow> \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
with QinS
[PROOF STATE]
proof (chain)
picking this:
Q \<in> S
Q \<longmapsto> Rs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Q \<in> S
Q \<longmapsto> Rs

goal (1 subgoal):
 1. \<exists>P\<in>S. P \<longmapsto> Rs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>S. P \<longmapsto> Rs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P\<in>S. P \<longmapsto> Rs

goal:
No subgoals!
[PROOF STEP]
qed