[STATEMENT]
lemma inputPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   x :: name

  assumes PSimQ: "\<forall>y. P[x::=y] \<sim> Q[x::=y]"

  shows "a<x>.P \<sim> a<x>.Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
let ?X = "{(a<x>.P, a<x>.Q) | a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
fix axP axQ p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
assume "(axP, axQ) \<in> ?X"
[PROOF STATE]
proof (state)
this:
(axP, axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(axP, axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
obtain a x P Q where A: "\<forall>y. P[x::=y] \<sim> Q[x::=y]" and B: "axP = a<x>.P" and C: "axQ = a<x>.Q"
[PROOF STATE]
proof (prove)
using this:
(axP, axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. (\<And>P x Q a. \<lbrakk>\<forall>y. P[x::=y] \<sim> Q[x::=y]; axP = a<x>.P; axQ = a<x>.Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y. P[x::=y] \<sim> Q[x::=y]
axP = a<x>.P
axQ = a<x>.Q

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
have "\<And>y. ((p::name prm) \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. P[x::=y] \<sim> Q[x::=y]
[PROOF STEP]
have "P[x::=(rev p \<bullet> y)] \<sim> Q[x::=(rev p \<bullet> y)]"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. P[x::=y] \<sim> Q[x::=y]

goal (1 subgoal):
 1. P[x::=(rev p \<bullet> y)] \<sim> Q[x::=(rev p \<bullet> y)]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P[x::=(rev p \<bullet> y)] \<sim> Q[x::=(rev p \<bullet> y)]

goal (1 subgoal):
 1. \<And>y. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
hence "(p \<bullet> (P[x::=(rev p \<bullet> y)])) \<sim> p \<bullet> (Q[x::=(rev p \<bullet> y)])"
[PROOF STATE]
proof (prove)
using this:
P[x::=(rev p \<bullet> y)] \<sim> Q[x::=(rev p \<bullet> y)]

goal (1 subgoal):
 1. p \<bullet> P[x::=(rev p \<bullet> y)] \<sim> p \<bullet> Q[x::=(rev p \<bullet> y)]
[PROOF STEP]
by(rule bisimClosed)
[PROOF STATE]
proof (state)
this:
p \<bullet> P[x::=(rev p \<bullet> y)] \<sim> p \<bullet> Q[x::=(rev p \<bullet> y)]

goal (1 subgoal):
 1. \<And>y. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
thus "(p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> P[x::=(rev p \<bullet> y)] \<sim> p \<bullet> Q[x::=(rev p \<bullet> y)]

goal (1 subgoal):
 1. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
by(simp add: eqvts pt_pi_rev[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
(p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(p \<bullet> P)[(p \<bullet> x)::=?y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=?y]

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
hence "((p::name prm) \<bullet> axP, p \<bullet> axQ) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> P)[(p \<bullet> x)::=?y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=?y]

goal (1 subgoal):
 1. (p \<bullet> axP, p \<bullet> axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
using B C
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> P)[(p \<bullet> x)::=?y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=?y]
axP = a<x>.P
axQ = a<x>.Q

goal (1 subgoal):
 1. (p \<bullet> axP, p \<bullet> axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(p \<bullet> axP, p \<bullet> axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?axP2, ?axQ2) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (?p2 \<bullet> ?axP2, ?p2 \<bullet> ?axQ2) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
hence "eqvt ?X"
[PROOF STATE]
proof (prove)
using this:
(?axP2, ?axQ2) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (?p2 \<bullet> ?axP2, ?p2 \<bullet> ?axQ2) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. eqvt {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
by(simp add: eqvt_def)
[PROOF STATE]
proof (state)
this:
eqvt {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
from PSimQ
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. P[x::=y] \<sim> Q[x::=y]
[PROOF STEP]
have "(a<x>.P, a<x>.Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. P[x::=y] \<sim> Q[x::=y]

goal (1 subgoal):
 1. (a<x>.P, a<x>.Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a<x>.P, a<x>.Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(a<x>.P, a<x>.Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
proof(coinduct rule: bisimCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> R \<leadsto>[({(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (S, R) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
case(cSim P Q)
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> R \<leadsto>[({(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (S, R) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. P \<leadsto>[({(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<union> bisim)] Q
[PROOF STEP]
using \<open>eqvt ?X\<close>
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
eqvt {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. P \<leadsto>[({(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<union> bisim)] Q
[PROOF STEP]
by(force intro: inputPres)
[PROOF STATE]
proof (state)
this:
P \<leadsto>[({(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<union> bisim)] Q

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (S, R) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (S, R) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
case(cSym P Q)
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (S, R) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. (Q, P) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
by(blast dest: symmetric)
[PROOF STATE]
proof (state)
this:
(Q, P) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a<x>.P \<sim> a<x>.Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma outputPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P \<sim> Q"

  shows "a{b}.P \<sim> a{b}.Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a{b}.P \<sim> a{b}.Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a{b}.P \<sim> a{b}.Q
[PROOF STEP]
let ?X = "{(a{b}.P, a{b}.Q), (a{b}.Q, a{b}.P)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a{b}.P \<sim> a{b}.Q
[PROOF STEP]
have "(a{b}.P, a{b}.Q) \<in> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a{b}.P, a{b}.Q) \<in> {(a{b}.P, a{b}.Q), (a{b}.Q, a{b}.P)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a{b}.P, a{b}.Q) \<in> {(a{b}.P, a{b}.Q), (a{b}.Q, a{b}.P)}

goal (1 subgoal):
 1. a{b}.P \<sim> a{b}.Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(a{b}.P, a{b}.Q) \<in> {(a{b}.P, a{b}.Q), (a{b}.Q, a{b}.P)}

goal (1 subgoal):
 1. a{b}.P \<sim> a{b}.Q
[PROOF STEP]
using \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (prove)
using this:
(a{b}.P, a{b}.Q) \<in> {(a{b}.P, a{b}.Q), (a{b}.Q, a{b}.P)}
P \<sim> Q

goal (1 subgoal):
 1. a{b}.P \<sim> a{b}.Q
[PROOF STEP]
by(coinduct rule: bisimCoinduct)
      (auto intro: Strong_Late_Sim_Pres.outputPres dest: symmetric)
[PROOF STATE]
proof (state)
this:
a{b}.P \<sim> a{b}.Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matchPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P \<sim> Q"

  shows "[a\<frown>b]P \<sim> [a\<frown>b]Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<frown>b]P \<sim> [a\<frown>b]Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a\<frown>b]P \<sim> [a\<frown>b]Q
[PROOF STEP]
let ?X = "{([a\<frown>b]P, [a\<frown>b]Q), ([a\<frown>b]Q, [a\<frown>b]P)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a\<frown>b]P \<sim> [a\<frown>b]Q
[PROOF STEP]
have "([a\<frown>b]P, [a\<frown>b]Q) \<in> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([a\<frown>b]P, [a\<frown>b]Q) \<in> {([a\<frown>b]P, [a\<frown>b]Q), ([a\<frown>b]Q, [a\<frown>b]P)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([a\<frown>b]P, [a\<frown>b]Q) \<in> {([a\<frown>b]P, [a\<frown>b]Q), ([a\<frown>b]Q, [a\<frown>b]P)}

goal (1 subgoal):
 1. [a\<frown>b]P \<sim> [a\<frown>b]Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
([a\<frown>b]P, [a\<frown>b]Q) \<in> {([a\<frown>b]P, [a\<frown>b]Q), ([a\<frown>b]Q, [a\<frown>b]P)}

goal (1 subgoal):
 1. [a\<frown>b]P \<sim> [a\<frown>b]Q
[PROOF STEP]
using \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (prove)
using this:
([a\<frown>b]P, [a\<frown>b]Q) \<in> {([a\<frown>b]P, [a\<frown>b]Q), ([a\<frown>b]Q, [a\<frown>b]P)}
P \<sim> Q

goal (1 subgoal):
 1. [a\<frown>b]P \<sim> [a\<frown>b]Q
[PROOF STEP]
by(coinduct rule: bisimCoinduct)
      (auto intro: Strong_Late_Sim_Pres.matchPres dest: symmetric bisimE)
[PROOF STATE]
proof (state)
this:
[a\<frown>b]P \<sim> [a\<frown>b]Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mismatchPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P \<sim> Q"

  shows "[a\<noteq>b]P \<sim> [a\<noteq>b]Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<noteq>b]P \<sim> [a\<noteq>b]Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a\<noteq>b]P \<sim> [a\<noteq>b]Q
[PROOF STEP]
let ?X = "{([a\<noteq>b]P, [a\<noteq>b]Q), ([a\<noteq>b]Q, [a\<noteq>b]P)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a\<noteq>b]P \<sim> [a\<noteq>b]Q
[PROOF STEP]
have "([a\<noteq>b]P, [a\<noteq>b]Q) \<in> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([a\<noteq>b]P, [a\<noteq>b]Q) \<in> {([a\<noteq>b]P, [a\<noteq>b]Q), ([a\<noteq>b]Q, [a\<noteq>b]P)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([a\<noteq>b]P, [a\<noteq>b]Q) \<in> {([a\<noteq>b]P, [a\<noteq>b]Q), ([a\<noteq>b]Q, [a\<noteq>b]P)}

goal (1 subgoal):
 1. [a\<noteq>b]P \<sim> [a\<noteq>b]Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
([a\<noteq>b]P, [a\<noteq>b]Q) \<in> {([a\<noteq>b]P, [a\<noteq>b]Q), ([a\<noteq>b]Q, [a\<noteq>b]P)}

goal (1 subgoal):
 1. [a\<noteq>b]P \<sim> [a\<noteq>b]Q
[PROOF STEP]
using \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (prove)
using this:
([a\<noteq>b]P, [a\<noteq>b]Q) \<in> {([a\<noteq>b]P, [a\<noteq>b]Q), ([a\<noteq>b]Q, [a\<noteq>b]P)}
P \<sim> Q

goal (1 subgoal):
 1. [a\<noteq>b]P \<sim> [a\<noteq>b]Q
[PROOF STEP]
by(coinduct rule: bisimCoinduct)
      (auto intro: Strong_Late_Sim_Pres.mismatchPres dest: symmetric bisimE)
[PROOF STATE]
proof (state)
this:
[a\<noteq>b]P \<sim> [a\<noteq>b]Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumPres:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  assumes "P \<sim> Q"

  shows "P \<oplus> R \<sim> Q \<oplus> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> R \<sim> Q \<oplus> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<oplus> R \<sim> Q \<oplus> R
[PROOF STEP]
let ?X = "{(P \<oplus> R, Q \<oplus> R), (Q \<oplus> R, P \<oplus> R)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<oplus> R \<sim> Q \<oplus> R
[PROOF STEP]
have "(P \<oplus> R, Q \<oplus> R) \<in> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> R, Q \<oplus> R) \<in> {(P \<oplus> R, Q \<oplus> R), (Q \<oplus> R, P \<oplus> R)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(P \<oplus> R, Q \<oplus> R) \<in> {(P \<oplus> R, Q \<oplus> R), (Q \<oplus> R, P \<oplus> R)}

goal (1 subgoal):
 1. P \<oplus> R \<sim> Q \<oplus> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<oplus> R, Q \<oplus> R) \<in> {(P \<oplus> R, Q \<oplus> R), (Q \<oplus> R, P \<oplus> R)}

goal (1 subgoal):
 1. P \<oplus> R \<sim> Q \<oplus> R
[PROOF STEP]
using \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (prove)
using this:
(P \<oplus> R, Q \<oplus> R) \<in> {(P \<oplus> R, Q \<oplus> R), (Q \<oplus> R, P \<oplus> R)}
P \<sim> Q

goal (1 subgoal):
 1. P \<oplus> R \<sim> Q \<oplus> R
[PROOF STEP]
by(coinduct rule: bisimCoinduct)
      (auto intro: Strong_Late_Sim_Pres.sumPres reflexive dest: symmetric bisimE)
[PROOF STATE]
proof (state)
this:
P \<oplus> R \<sim> Q \<oplus> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma resPres:
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes "P \<sim> Q"

  shows "<\<nu>x>P \<sim> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>x>P \<sim> <\<nu>x>Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>P \<sim> <\<nu>x>Q
[PROOF STEP]
let ?X = "{x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>P \<sim> <\<nu>x>Q
[PROOF STEP]
from \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "(<\<nu>x>P, <\<nu>x>Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. (<\<nu>x>P, <\<nu>x>Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(<\<nu>x>P, <\<nu>x>Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (1 subgoal):
 1. <\<nu>x>P \<sim> <\<nu>x>Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(<\<nu>x>P, <\<nu>x>Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (1 subgoal):
 1. <\<nu>x>P \<sim> <\<nu>x>Q
[PROOF STEP]
proof(coinduct rule: bisimCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
case(cSim xP xQ)
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
fix P Q a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
assume PSimQ: "P \<leadsto>[bisim] Q"
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bisim] Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bisim] Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
have "\<And>P Q a. P \<sim> Q \<Longrightarrow> (<\<nu>a>P, <\<nu>a>Q) \<in> ?X \<union> bisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q a. P \<sim> Q \<Longrightarrow> (<\<nu>a>P, <\<nu>a>Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?P \<sim> ?Q \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?P \<sim> ?Q \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
have "bisim \<subseteq> ?X \<union> bisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bisim \<subseteq> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bisim \<subseteq> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim \<subseteq> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
have "eqvt bisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt bisim
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eqvt bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqvt bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
have "eqvt ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
by(auto simp add: eqvt_def) (blast intro: bisimClosed)
[PROOF STATE]
proof (state)
this:
eqvt {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
hence "eqvt (?X \<union> bisim)"
[PROOF STATE]
proof (prove)
using this:
eqvt {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (1 subgoal):
 1. eqvt ({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eqvt ({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[bisim] Q
?P \<sim> ?Q \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
bisim \<subseteq> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
eqvt bisim
eqvt ({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)
[PROOF STEP]
have "<\<nu>a>P \<leadsto>[(?X \<union> bisim)] <\<nu>a>Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bisim] Q
?P \<sim> ?Q \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
bisim \<subseteq> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
eqvt bisim
eqvt ({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)

goal (1 subgoal):
 1. <\<nu>a>P \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] <\<nu>a>Q
[PROOF STEP]
by(rule Strong_Late_Sim_Pres.resPres)
[PROOF STATE]
proof (state)
this:
<\<nu>a>P \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] <\<nu>a>Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?Pa2 \<leadsto>[bisim] ?Qa2 \<Longrightarrow> <\<nu>?a2>?Pa2 \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] <\<nu>?a2>?Qa2

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
with \<open>(xP, xQ) \<in> ?X\<close>
[PROOF STATE]
proof (chain)
picking this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
?Pa2 \<leadsto>[bisim] ?Qa2 \<Longrightarrow> <\<nu>?a2>?Pa2 \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] <\<nu>?a2>?Qa2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
?Pa2 \<leadsto>[bisim] ?Qa2 \<Longrightarrow> <\<nu>?a2>?Pa2 \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] <\<nu>?a2>?Qa2

goal (1 subgoal):
 1. xP \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] xQ
[PROOF STEP]
by(auto dest: bisimE)
[PROOF STATE]
proof (state)
this:
xP \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] xQ

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
case(cSym xP xQ)
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (1 subgoal):
 1. (xQ, xP) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
by(auto dest: symmetric)
[PROOF STATE]
proof (state)
this:
(xQ, xP) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
<\<nu>x>P \<sim> <\<nu>x>Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parPres:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  assumes "P \<sim> Q"

  shows "P \<parallel> R \<sim> Q \<parallel> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
let ?X = "{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) | lst P R Q. P \<sim> Q}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
have EmptyChain: "\<And>P Q. P \<parallel> Q = resChain [] (P \<parallel> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q. P \<parallel> Q = resChain [] (P \<parallel> Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?P \<parallel> ?Q = resChain [] (?P \<parallel> ?Q)

goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
with \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
?P \<parallel> ?Q = resChain [] (?P \<parallel> ?Q)
[PROOF STEP]
have "(P \<parallel> R, Q \<parallel> R) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q
?P \<parallel> ?Q = resChain [] (?P \<parallel> ?Q)

goal (1 subgoal):
 1. (P \<parallel> R, Q \<parallel> R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(P \<parallel> R, Q \<parallel> R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<parallel> R, Q \<parallel> R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
proof(coinduct rule: bisimCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
case(cSim PR QR)
[PROOF STATE]
proof (state)
this:
(PR, QR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(PR, QR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
fix P Q R lst
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
assume "P \<sim> Q"
[PROOF STATE]
proof (state)
this:
P \<sim> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
hence "P \<leadsto>[bisim] Q"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. P \<leadsto>[bisim] Q
[PROOF STEP]
by(rule bisimE)
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bisim] Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bisim] Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
note \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (state)
this:
P \<sim> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<sim> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
have "\<And>P Q R. P \<sim> Q \<Longrightarrow> (P \<parallel> R, Q \<parallel> R) \<in> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q R. P \<sim> Q \<Longrightarrow> (P \<parallel> R, Q \<parallel> R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
by auto (blast intro: EmptyChain)
[PROOF STATE]
proof (state)
this:
?P \<sim> ?Q \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?P \<sim> ?Q \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?P \<sim> ?Q \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
fix xP xQ x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
assume "(xP, xQ) \<in> ?X"
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(xP, xQ) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
obtain P Q R lst
          where "P \<sim> Q" and "xP = resChain lst (P \<parallel> R)" and xQeq: "xQ = resChain lst (Q \<parallel> R)"
[PROOF STATE]
proof (prove)
using this:
(xP, xQ) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (1 subgoal):
 1. (\<And>P Q lst R. \<lbrakk>P \<sim> Q; xP = resChain lst (P \<parallel> R); xQ = resChain lst (Q \<parallel> R)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P \<sim> Q
xP = resChain lst (P \<parallel> R)
xQ = resChain lst (Q \<parallel> R)

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<sim> Q
xP = resChain lst (P \<parallel> R)
xQ = resChain lst (Q \<parallel> R)

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
hence "(resChain (x#lst) (P \<parallel> R), resChain (x#lst) (Q \<parallel> R)) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q
xP = resChain lst (P \<parallel> R)
xQ = resChain lst (Q \<parallel> R)

goal (1 subgoal):
 1. (resChain (x # lst) (P \<parallel> R), resChain (x # lst) (Q \<parallel> R)) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(resChain (x # lst) (P \<parallel> R), resChain (x # lst) (Q \<parallel> R)) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
xP = resChain lst (P \<parallel> R)
xQ = resChain lst (Q \<parallel> R)
(resChain (x # lst) (P \<parallel> R), resChain (x # lst) (Q \<parallel> R)) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
have "(<\<nu>x>xP, <\<nu>x>xQ) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q
xP = resChain lst (P \<parallel> R)
xQ = resChain lst (Q \<parallel> R)
(resChain (x # lst) (P \<parallel> R), resChain (x # lst) (Q \<parallel> R)) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (1 subgoal):
 1. (<\<nu>x>xP, <\<nu>x>xQ) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(<\<nu>x>xP, <\<nu>x>xQ) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?xP2, ?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (<\<nu>?x2>?xP2, <\<nu>?x2>?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
note ResPres = this
[PROOF STATE]
proof (state)
this:
(?xP2, ?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (<\<nu>?x2>?xP2, <\<nu>?x2>?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(?xP2, ?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (<\<nu>?x2>?xP2, <\<nu>?x2>?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
have "eqvt bisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt bisim
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eqvt bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqvt bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
have "eqvt ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
by(auto simp add: eqvt_def) (blast intro: bisimClosed)
[PROOF STATE]
proof (state)
this:
eqvt {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[bisim] Q
P \<sim> Q
?P \<sim> ?Q \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
(?xP2, ?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (<\<nu>?x2>?xP2, <\<nu>?x2>?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
eqvt bisim
eqvt {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
have "P \<parallel> R \<leadsto>[(?X)] Q \<parallel> R"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bisim] Q
P \<sim> Q
?P \<sim> ?Q \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
(?xP2, ?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (<\<nu>?x2>?xP2, <\<nu>?x2>?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
eqvt bisim
eqvt {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}] Q \<parallel> R
[PROOF STEP]
by(rule parPres)
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}] Q \<parallel> R

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
hence "resChain lst (P \<parallel> R) \<leadsto>[?X] (resChain lst (Q \<parallel> R))"
[PROOF STATE]
proof (prove)
using this:
P \<parallel> R \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}] Q \<parallel> R

goal (1 subgoal):
 1. resChain lst (P \<parallel> R) \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}] resChain lst (Q \<parallel> R)
[PROOF STEP]
using \<open>eqvt ?X\<close> ResPres
[PROOF STATE]
proof (prove)
using this:
P \<parallel> R \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}] Q \<parallel> R
eqvt {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
(?xP2, ?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (<\<nu>?x2>?xP2, <\<nu>?x2>?xQ2) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (1 subgoal):
 1. resChain lst (P \<parallel> R) \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}] resChain lst (Q \<parallel> R)
[PROOF STEP]
by(rule resChainI)
[PROOF STATE]
proof (state)
this:
resChain lst (P \<parallel> R) \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}] resChain lst (Q \<parallel> R)

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
hence "resChain lst (P \<parallel> R) \<leadsto>[(?X \<union> bisim)] (resChain lst (Q \<parallel> R))"
[PROOF STATE]
proof (prove)
using this:
resChain lst (P \<parallel> R) \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}] resChain lst (Q \<parallel> R)

goal (1 subgoal):
 1. resChain lst (P \<parallel> R) \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] resChain lst (Q \<parallel> R)
[PROOF STEP]
by(force intro: Strong_Late_Sim.monotonic)
[PROOF STATE]
proof (state)
this:
resChain lst (P \<parallel> R) \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] resChain lst (Q \<parallel> R)

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?Pa2 \<sim> ?Qa2 \<Longrightarrow> resChain ?lst2 (?Pa2 \<parallel> ?Ra2) \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] resChain ?lst2 (?Qa2 \<parallel> ?Ra2)

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> R \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
with \<open>(PR, QR) \<in> ?X\<close>
[PROOF STATE]
proof (chain)
picking this:
(PR, QR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
?Pa2 \<sim> ?Qa2 \<Longrightarrow> resChain ?lst2 (?Pa2 \<parallel> ?Ra2) \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] resChain ?lst2 (?Qa2 \<parallel> ?Ra2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(PR, QR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
?Pa2 \<sim> ?Qa2 \<Longrightarrow> resChain ?lst2 (?Pa2 \<parallel> ?Ra2) \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] resChain ?lst2 (?Qa2 \<parallel> ?Ra2)

goal (1 subgoal):
 1. PR \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] QR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
PR \<leadsto>[({(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<union> bisim)] QR

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
case(cSym PR QR)
[PROOF STATE]
proof (state)
this:
(PR, QR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q} \<Longrightarrow> (S, R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(PR, QR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal (1 subgoal):
 1. (QR, PR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}
[PROOF STEP]
by(blast dest: symmetric)
[PROOF STATE]
proof (state)
this:
(QR, PR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P R Q. P \<sim> Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<sim> Q \<parallel> R

goal:
No subgoals!
[PROOF STEP]
qed


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

  assumes PBiSimQ: "P \<sim> Q"

  shows "!P \<sim> !Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. !P \<sim> !Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. !P \<sim> !Q
[PROOF STEP]
let ?X = "bangRel bisim"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. !P \<sim> !Q
[PROOF STEP]
from PBiSimQ
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "(!P, !Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. (!P, !Q) \<in> bangRel bisim
[PROOF STEP]
by(rule Rel.BRBang)
[PROOF STATE]
proof (state)
this:
(!P, !Q) \<in> bangRel bisim

goal (1 subgoal):
 1. !P \<sim> !Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(!P, !Q) \<in> bangRel bisim

goal (1 subgoal):
 1. !P \<sim> !Q
[PROOF STEP]
proof(coinduct rule: bisimCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> R \<leadsto>[(bangRel bisim \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> (S, R) \<in> bangRel bisim
[PROOF STEP]
case(cSim bP bQ)
[PROOF STATE]
proof (state)
this:
(bP, bQ) \<in> bangRel bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> R \<leadsto>[(bangRel bisim \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> (S, R) \<in> bangRel bisim
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(bP, bQ) \<in> bangRel bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> R \<leadsto>[(bangRel bisim \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> (S, R) \<in> bangRel bisim
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> R \<leadsto>[(bangRel bisim \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> (S, R) \<in> bangRel bisim
[PROOF STEP]
assume "(P, Q) \<in> ?X"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> bangRel bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> R \<leadsto>[(bangRel bisim \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> (S, R) \<in> bangRel bisim
[PROOF STEP]
hence "P \<leadsto>[?X] Q"
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> bangRel bisim

goal (1 subgoal):
 1. P \<leadsto>[bangRel bisim] Q
[PROOF STEP]
proof(induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> !P \<leadsto>[bangRel bisim] !Q
 2. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> !P \<leadsto>[bangRel bisim] !Q
 2. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
assume "P \<sim> Q"
[PROOF STATE]
proof (state)
this:
P \<sim> Q

goal (3 subgoals):
 1. \<And>P Q. P \<sim> Q \<Longrightarrow> !P \<leadsto>[bangRel bisim] !Q
 2. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
thus "!P \<leadsto>[?X] !Q"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. !P \<leadsto>[bangRel bisim] !Q
[PROOF STEP]
using bisimE bisimEqvt
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q
?P \<sim> ?Q \<Longrightarrow> ?P \<leadsto>[bisim] ?Q
eqvt bisim

goal (1 subgoal):
 1. !P \<leadsto>[bangRel bisim] !Q
[PROOF STEP]
by(rule Strong_Late_Sim_Pres.bangPres)
[PROOF STATE]
proof (state)
this:
!P \<leadsto>[bangRel bisim] !Q

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
fix P Q R T
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
assume RBiSimT: "R \<sim> T"
[PROOF STATE]
proof (state)
this:
R \<sim> T

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
assume PBangRelQ: "(P, Q) \<in> ?X"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> bangRel bisim

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
assume PSimQ: "P \<leadsto>[?X] Q"
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bangRel bisim] Q

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
from RBiSimT
[PROOF STATE]
proof (chain)
picking this:
R \<sim> T
[PROOF STEP]
have "R \<leadsto>[bisim] T"
[PROOF STATE]
proof (prove)
using this:
R \<sim> T

goal (1 subgoal):
 1. R \<leadsto>[bisim] T
[PROOF STEP]
by(blast dest: bisimE)
[PROOF STATE]
proof (state)
this:
R \<leadsto>[bisim] T

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>R \<sim> T; (P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
thus "R \<parallel> P \<leadsto>[?X] T \<parallel> Q"
[PROOF STATE]
proof (prove)
using this:
R \<leadsto>[bisim] T

goal (1 subgoal):
 1. R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
[PROOF STEP]
using PSimQ RBiSimT PBangRelQ Rel.BRPar Rel.BRRes bisimEqvt eqvtBangRel
[PROOF STATE]
proof (prove)
using this:
R \<leadsto>[bisim] T
P \<leadsto>[bangRel bisim] Q
R \<sim> T
(P, Q) \<in> bangRel bisim
\<lbrakk>(?R, ?T) \<in> ?Rel; (?P, ?Q) \<in> bangRel ?Rel\<rbrakk> \<Longrightarrow> (?R \<parallel> ?P, ?T \<parallel> ?Q) \<in> bangRel ?Rel
(?P, ?Q) \<in> bangRel ?Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> bangRel ?Rel
eqvt bisim
eqvt ?Rel \<Longrightarrow> eqvt (bangRel ?Rel)

goal (1 subgoal):
 1. R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q
[PROOF STEP]
by(blast intro: Strong_Late_Sim_Pres.parCompose)
[PROOF STATE]
proof (state)
this:
R \<parallel> P \<leadsto>[bangRel bisim] T \<parallel> Q

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
fix P Q a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
assume "P \<leadsto>[?X] Q"
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bangRel bisim] Q

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bangRel bisim] Q

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
from eqvtBangRel bisimEqvt
[PROOF STATE]
proof (chain)
picking this:
eqvt ?Rel \<Longrightarrow> eqvt (bangRel ?Rel)
eqvt bisim
[PROOF STEP]
have "eqvt ?X"
[PROOF STATE]
proof (prove)
using this:
eqvt ?Rel \<Longrightarrow> eqvt (bangRel ?Rel)
eqvt bisim

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

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel bisim; P \<leadsto>[bangRel bisim] Q\<rbrakk> \<Longrightarrow> <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[bangRel bisim] Q
eqvt (bangRel bisim)
[PROOF STEP]
show "<\<nu>a>P \<leadsto>[?X] <\<nu>a>Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bangRel bisim] Q
eqvt (bangRel bisim)

goal (1 subgoal):
 1. <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
using Rel.BRRes
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bangRel bisim] Q
eqvt (bangRel bisim)
(?P, ?Q) \<in> bangRel ?Rel \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> bangRel ?Rel

goal (1 subgoal):
 1. <\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q
[PROOF STEP]
by(blast intro: Strong_Late_Sim_Pres.resPres)
[PROOF STATE]
proof (state)
this:
<\<nu>a>P \<leadsto>[bangRel bisim] <\<nu>a>Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bangRel bisim] Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> R \<leadsto>[(bangRel bisim \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> (S, R) \<in> bangRel bisim
[PROOF STEP]
hence "P \<leadsto>[((bangRel bisim) \<union> bisim)] Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bangRel bisim] Q

goal (1 subgoal):
 1. P \<leadsto>[(bangRel bisim \<union> bisim)] Q
[PROOF STEP]
by(rule_tac Strong_Late_Sim.monotonic) auto
[PROOF STATE]
proof (state)
this:
P \<leadsto>[(bangRel bisim \<union> bisim)] Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> R \<leadsto>[(bangRel bisim \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> (S, R) \<in> bangRel bisim
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?Pa2, ?Qa2) \<in> bangRel bisim \<Longrightarrow> ?Pa2 \<leadsto>[(bangRel bisim \<union> bisim)] ?Qa2

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> R \<leadsto>[(bangRel bisim \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> (S, R) \<in> bangRel bisim
[PROOF STEP]
with \<open>(bP, bQ) \<in> ?X\<close>
[PROOF STATE]
proof (chain)
picking this:
(bP, bQ) \<in> bangRel bisim
(?Pa2, ?Qa2) \<in> bangRel bisim \<Longrightarrow> ?Pa2 \<leadsto>[(bangRel bisim \<union> bisim)] ?Qa2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(bP, bQ) \<in> bangRel bisim
(?Pa2, ?Qa2) \<in> bangRel bisim \<Longrightarrow> ?Pa2 \<leadsto>[(bangRel bisim \<union> bisim)] ?Qa2

goal (1 subgoal):
 1. bP \<leadsto>[(bangRel bisim \<union> bisim)] bQ
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bP \<leadsto>[(bangRel bisim \<union> bisim)] bQ

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> (S, R) \<in> bangRel bisim
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> (S, R) \<in> bangRel bisim
[PROOF STEP]
case(cSym bP bQ)
[PROOF STATE]
proof (state)
this:
(bP, bQ) \<in> bangRel bisim

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> bangRel bisim \<Longrightarrow> (S, R) \<in> bangRel bisim
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(bP, bQ) \<in> bangRel bisim

goal (1 subgoal):
 1. (bQ, bP) \<in> bangRel bisim
[PROOF STEP]
by(metis bangRelSymetric symmetric)
[PROOF STATE]
proof (state)
this:
(bQ, bP) \<in> bangRel bisim

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma T2: "\<lfloor>\<P> \<G>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<G>\<^bold>\<in>\<P>\<rfloor>
[PROOF STEP]
by (metis A3 G_def) \<comment>\<open>From A3\<close>


[STATEMENT]
lemma L1: "\<lfloor>\<P>(\<lambda>x.(x\<^bold>=x))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>x. x\<^bold>=x\<^bold>\<in>\<P>\<rfloor>
[PROOF STEP]
by (metis A2' A3)


[STATEMENT]
theorem T6: "\<lfloor>\<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"  \<comment>\<open>Proof found by sledgehammer\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
have T1: "\<lfloor>\<^bold>\<forall>X.((\<P> X) \<^bold>\<rightarrow> \<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E X))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (x\<^bold>\<in>\<P> \<^bold>\<rightarrow> \<^bold>\<diamond>x\<^bold>\<in>q8) w\<rfloor>
[PROOF STEP]
by (metis A1' A2')
[PROOF STATE]
proof (state)
this:
\<lfloor>\<lambda>w. \<forall>x. (x\<^bold>\<in>\<P> \<^bold>\<rightarrow> \<^bold>\<diamond>x\<^bold>\<in>q8) w\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
have T3: "\<lfloor>\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
using T1 T2
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<lambda>w. \<forall>x. (x\<^bold>\<in>\<P> \<^bold>\<rightarrow> \<^bold>\<diamond>x\<^bold>\<in>q8) w\<rfloor>
\<lfloor>\<G>\<^bold>\<in>\<P>\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
have T5: "\<lfloor>(\<^bold>\<diamond>(\<^bold>\<exists>\<^sup>E \<G>)) \<^bold>\<rightarrow> \<^bold>\<box>(\<^bold>\<exists>\<^sup>E \<G>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8 \<^bold>\<rightarrow> \<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
by (metis A1' A2' T2)
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8 \<^bold>\<rightarrow> \<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8 \<^bold>\<rightarrow> \<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
using T3
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8 \<^bold>\<rightarrow> \<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
\<lfloor>\<^bold>\<diamond>\<G>\<^bold>\<in>q8\<rfloor>

goal (1 subgoal):
 1. \<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lfloor>\<^bold>\<box>\<G>\<^bold>\<in>q8\<rfloor>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick[satisfy]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops \<comment>\<open>Consistency: model found\<close>


[STATEMENT]
lemma MC: "\<lfloor>\<^bold>\<forall>\<Phi>.(\<Phi> \<^bold>\<rightarrow> \<^bold>\<box>\<Phi>)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (x \<^bold>\<rightarrow> \<^bold>\<box>x) w\<rfloor>
[PROOF STEP]
oops \<comment>\<open>Countermodel\<close>


[STATEMENT]
lemma MT: "\<lfloor>\<^bold>\<forall>x y.(((\<G> x) \<^bold>\<and> (\<G> y)) \<^bold>\<rightarrow> (x\<^bold>=y))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x xa. (\<G> x \<^bold>\<and> \<G> xa) w \<longrightarrow> x = xa\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x xa. (\<G> x \<^bold>\<and> \<G> xa) w \<longrightarrow> x = xa\<rfloor>
[PROOF STEP]
oops \<comment>\<open>Countermodel.\<close>


[STATEMENT]
lemma A1: "\<lfloor>\<^bold>\<forall>X.((\<^bold>\<not>(\<P> X))\<^bold>\<leftrightarrow>(\<P>(\<^bold>\<rightharpoondown>X)))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (\<^bold>\<not>x\<^bold>\<in>\<P>) w = \<^bold>\<rightharpoondown>x\<^bold>\<in>\<P> w\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (\<^bold>\<not>x\<^bold>\<in>\<P>) w = \<^bold>\<rightharpoondown>x\<^bold>\<in>\<P> w\<rfloor>
[PROOF STEP]
oops \<comment>\<open>Countermodel\<close>


[STATEMENT]
lemma A4: "\<lfloor>\<^bold>\<forall>X.((\<P> X) \<^bold>\<rightarrow> \<^bold>\<box>(\<P> X))\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (x\<^bold>\<in>\<P> \<^bold>\<rightarrow> \<^bold>\<box>x\<^bold>\<in>\<P>) w\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. \<forall>x. (x\<^bold>\<in>\<P> \<^bold>\<rightarrow> \<^bold>\<box>x\<^bold>\<in>\<P>) w\<rfloor>
[PROOF STEP]
oops \<comment>\<open>Countermodel\<close>


[STATEMENT]
lemma A5: "\<lfloor>\<P> \<N>\<E>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<N>\<E>\<^bold>\<in>\<P>\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<N>\<E>\<^bold>\<in>\<P>\<rfloor>
[PROOF STEP]
oops \<comment>\<open>Countermodel\<close>


[STATEMENT]
theorem F1: "\<lfloor>Filter \<P>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. ((\<^bold>U\<^bold>\<in>\<P> \<^bold>\<and> \<^bold>\<not>\<^bold>\<emptyset>\<^bold>\<in>\<P>) w \<and> (\<forall>x xa. x\<^bold>\<in>\<P> w \<and> (\<forall>xb. (x xb \<^bold>\<rightarrow> xa xb) w) \<longrightarrow> xa\<^bold>\<in>\<P> w)) \<and> (\<forall>x xa. (x\<^bold>\<in>\<P> \<^bold>\<and> xa\<^bold>\<in>\<P> \<^bold>\<rightarrow> x\<^bold>\<sqinter>xa\<^bold>\<in>\<P>) w)\<rfloor>
[PROOF STEP]
oops \<comment>\<open>Proof found by sledgehammer, but reconstruction timeout\<close>


[STATEMENT]
theorem U1: "\<lfloor>UFilter \<P>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. (((\<^bold>U\<^bold>\<in>\<P> \<^bold>\<and> \<^bold>\<not>\<^bold>\<emptyset>\<^bold>\<in>\<P>) w \<and> (\<forall>x xa. x\<^bold>\<in>\<P> w \<and> (\<forall>xb. (x xb \<^bold>\<rightarrow> xa xb) w) \<longrightarrow> xa\<^bold>\<in>\<P> w)) \<and> (\<forall>x xa. (x\<^bold>\<in>\<P> \<^bold>\<and> xa\<^bold>\<in>\<P> \<^bold>\<rightarrow> x\<^bold>\<sqinter>xa\<^bold>\<in>\<P>) w)) \<and> (\<forall>x. (x\<^bold>\<in>\<P> \<^bold>\<or> \<^bold>\<rightharpoondown>x\<^bold>\<in>\<P>) w)\<rfloor>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<lambda>w. (((\<^bold>U\<^bold>\<in>\<P> \<^bold>\<and> \<^bold>\<not>\<^bold>\<emptyset>\<^bold>\<in>\<P>) w \<and> (\<forall>x xa. x\<^bold>\<in>\<P> w \<and> (\<forall>xb. (x xb \<^bold>\<rightarrow> xa xb) w) \<longrightarrow> xa\<^bold>\<in>\<P> w)) \<and> (\<forall>x xa. (x\<^bold>\<in>\<P> \<^bold>\<and> xa\<^bold>\<in>\<P> \<^bold>\<rightarrow> x\<^bold>\<sqinter>xa\<^bold>\<in>\<P>) w)) \<and> (\<forall>x. (x\<^bold>\<in>\<P> \<^bold>\<or> \<^bold>\<rightharpoondown>x\<^bold>\<in>\<P>) w)\<rfloor>
[PROOF STEP]
oops  \<comment>\<open>Countermodel\<close>


[STATEMENT]
lemma case_resource_conv_run_resource: "case_resource f res = f (run_resource res)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case res of Resource x \<Rightarrow> f x) = f (run_resource res)
[PROOF STEP]
by(fact resource.case_eq_if)


[STATEMENT]
lemma map_resource_sel [simp]:
  "run_resource (map_resource res) a' = map_spmf (map_prod b map_resource) (run_resource res (a a'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_resource (local.map_resource res) a' = map_spmf (map_prod b local.map_resource) (run_resource res (a a'))
[PROOF STEP]
by simp


[STATEMENT]
lemma map_resource_ctr [simp, code]:
  "map_resource (Resource f) = Resource (map_spmf (map_prod b map_resource) \<circ> f \<circ> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.map_resource (Resource f) = Resource (map_spmf (map_prod b local.map_resource) \<circ> f \<circ> a)
[PROOF STEP]
by(rule resource.expand; simp add: fun_eq_iff)


[STATEMENT]
lemma map_resource_id [simp]: "map_resource id id res = res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_resource id id res = res
[PROOF STEP]
by(simp add: map_resource_id1 resource.map_id)


[STATEMENT]
lemma rel_resource_coinduct [consumes 1, case_names rel_resource, coinduct pred: rel_resource]:
  assumes "X res1 res2"
    and "\<And>res1 res2. X res1 res2 \<Longrightarrow>
         rel_fun A (rel_spmf (rel_prod B (\<lambda>res1 res2. X res1 res2 \<or> rel_resource A B res1 res2)))
            (run_resource res1) (run_resource res2)"
  shows "rel_resource A B res1 res2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A B res1 res2
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
X res1 res2

goal (1 subgoal):
 1. rel_resource A B res1 res2
[PROOF STEP]
by(rule rel_resource.coinduct)(simp add: assms(2))


[STATEMENT]
lemma rel_resource_simps [simp, code]:
  "rel_resource A B (Resource f) (Resource g) \<longleftrightarrow> rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) f g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A B (Resource f) (Resource g) = rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) f g
[PROOF STEP]
by(subst rel_resource.simps) simp


[STATEMENT]
lemma rel_resourceD:
  "rel_resource A B res1 res2 \<Longrightarrow> rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1) (run_resource res2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A B res1 res2 \<Longrightarrow> rel_fun A (rel_spmf (rel_prod B (rel_resource A B))) (run_resource res1) (run_resource res2)
[PROOF STEP]
by(blast elim: rel_resource.cases)


[STATEMENT]
lemma rel_resource_eq1: "rel_resource (=) = rel_resource'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource (=) = rel_resource'
[PROOF STEP]
proof(intro ext iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. rel_resource (=) x xa xb \<Longrightarrow> rel_resource' x xa xb
 2. \<And>x xa xb. rel_resource' x xa xb \<Longrightarrow> rel_resource (=) x xa xb
[PROOF STEP]
show "rel_resource' B res1 res2" if "rel_resource (=) B res1 res2" for B res1 res2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource' B res1 res2
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
rel_resource (=) B res1 res2

goal (1 subgoal):
 1. rel_resource' B res1 res2
[PROOF STEP]
by(coinduction arbitrary: res1 res2)(auto elim: rel_resource.cases)
[PROOF STATE]
proof (state)
this:
rel_resource (=) ?B1 ?res1.1 ?res2.1 \<Longrightarrow> rel_resource' ?B1 ?res1.1 ?res2.1

goal (1 subgoal):
 1. \<And>x xa xb. rel_resource' x xa xb \<Longrightarrow> rel_resource (=) x xa xb
[PROOF STEP]
show "rel_resource (=) B res1 res2" if "rel_resource' B res1 res2" for B res1 res2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource (=) B res1 res2
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
rel_resource' B res1 res2

goal (1 subgoal):
 1. rel_resource (=) B res1 res2
[PROOF STEP]
by(coinduction arbitrary: res1 res2)(auto 4 4 elim: resource.rel_cases intro: spmf_rel_mono_strong simp add: rel_fun_def)
[PROOF STATE]
proof (state)
this:
rel_resource' ?B2 ?res1.2 ?res2.2 \<Longrightarrow> rel_resource (=) ?B2 ?res1.2 ?res2.2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_resource_eq: (* [relator_eq] *) "rel_resource (=) (=) = (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource (=) (=) = (=)
[PROOF STEP]
by(simp add: rel_resource_eq1 resource.rel_eq)


[STATEMENT]
lemma rel_resource_mono:
  assumes "A' \<le> A" "B \<le> B'"
  shows "rel_resource A B \<le> rel_resource A' B'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A B \<le> rel_resource A' B'
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. rel_resource A B x y \<Longrightarrow> rel_resource A' B' x y
[PROOF STEP]
show "rel_resource A' B' res1 res2" if "rel_resource A B res1 res2" for res1 res2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A' B' res1 res2
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
rel_resource A B res1 res2

goal (1 subgoal):
 1. rel_resource A' B' res1 res2
[PROOF STEP]
by(coinduct)(auto dest: rel_resourceD elim!: rel_spmf_mono prod.rel_mono_strong rel_fun_mono intro: assms[THEN predicate2D])
[PROOF STATE]
proof (state)
this:
rel_resource A B ?res1.0 ?res2.0 \<Longrightarrow> rel_resource A' B' ?res1.0 ?res2.0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_resource_conversep: "rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> = (rel_resource A B)\<inverse>\<inverse>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> = (rel_resource A B)\<inverse>\<inverse>
[PROOF STEP]
proof(intro ext iffI; simp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa. rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> x xa \<Longrightarrow> rel_resource A B xa x
 2. \<And>x xa. rel_resource A B xa x \<Longrightarrow> rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> x xa
[PROOF STEP]
show "rel_resource A B res1 res2" if "rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> res2 res1"
    for A :: "'a1 \<Rightarrow> 'a2 \<Rightarrow> bool" and B :: "'c1 \<Rightarrow> 'c2 \<Rightarrow> bool" and res1 res2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A B res1 res2
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> res2 res1

goal (1 subgoal):
 1. rel_resource A B res1 res2
[PROOF STEP]
by(coinduct)
      (drule rel_resourceD, rewrite in \<hole> conversep_iff[symmetric]
        , subst rel_fun_conversep[symmetric], subst spmf_rel_conversep[symmetric], erule rel_fun_mono
        , auto simp add: prod.rel_conversep[symmetric] rel_fun_def conversep_iff[abs_def]  elim:rel_spmf_mono prod.rel_mono_strong)
[PROOF STATE]
proof (state)
this:
rel_resource ?A1\<inverse>\<inverse> ?B1\<inverse>\<inverse> ?res2.1 ?res1.1 \<Longrightarrow> rel_resource ?A1 ?B1 ?res1.1 ?res2.1

goal (1 subgoal):
 1. \<And>x xa. rel_resource A B xa x \<Longrightarrow> rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> x xa
[PROOF STEP]
from this[of "A\<inverse>\<inverse>" "B\<inverse>\<inverse>"]
[PROOF STATE]
proof (chain)
picking this:
rel_resource A\<inverse>\<inverse>\<inverse>\<inverse> B\<inverse>\<inverse>\<inverse>\<inverse> ?res2.1 ?res1.1 \<Longrightarrow> rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> ?res1.1 ?res2.1
[PROOF STEP]
show "rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> res2 res1" if "rel_resource A B res1 res2" for res1 res2
[PROOF STATE]
proof (prove)
using this:
rel_resource A\<inverse>\<inverse>\<inverse>\<inverse> B\<inverse>\<inverse>\<inverse>\<inverse> ?res2.1 ?res1.1 \<Longrightarrow> rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> ?res1.1 ?res2.1

goal (1 subgoal):
 1. rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> res2 res1
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
rel_resource A\<inverse>\<inverse>\<inverse>\<inverse> B\<inverse>\<inverse>\<inverse>\<inverse> ?res2.1 ?res1.1 \<Longrightarrow> rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> ?res1.1 ?res2.1
rel_resource A B res1 res2

goal (1 subgoal):
 1. rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> res2 res1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rel_resource A B ?res1.1 ?res2.1 \<Longrightarrow> rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> ?res2.1 ?res1.1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_resource_map_resource'1:
  "rel_resource A B (map_resource' f res1) res2 = rel_resource A (\<lambda>x. B (f x)) res1 res2"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A B (map_resource' f res1) res2 = rel_resource A (\<lambda>x. B (f x)) res1 res2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rel_resource A B (map_resource' f res1) res2 \<Longrightarrow> rel_resource A (\<lambda>x. B (f x)) res1 res2
 2. rel_resource A (\<lambda>x. B (f x)) res1 res2 \<Longrightarrow> rel_resource A B (map_resource' f res1) res2
[PROOF STEP]
show ?rhs if ?lhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A (\<lambda>x. B (f x)) res1 res2
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
rel_resource A B (map_resource' f res1) res2

goal (1 subgoal):
 1. rel_resource A (\<lambda>x. B (f x)) res1 res2
[PROOF STEP]
by(coinduction arbitrary: res1 res2)
      (drule rel_resourceD, auto simp add: map_resource.sel map_resource_id1[symmetric] rel_fun_comp spmf_rel_map prod.rel_map[abs_def]
        elim!: rel_fun_mono rel_spmf_mono prod.rel_mono[THEN predicate2D, rotated -1])
[PROOF STATE]
proof (state)
this:
rel_resource A B (map_resource' f res1) res2 \<Longrightarrow> rel_resource A (\<lambda>x. B (f x)) res1 res2

goal (1 subgoal):
 1. rel_resource A (\<lambda>x. B (f x)) res1 res2 \<Longrightarrow> rel_resource A B (map_resource' f res1) res2
[PROOF STEP]
show ?lhs if ?rhs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A B (map_resource' f res1) res2
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
rel_resource A (\<lambda>x. B (f x)) res1 res2

goal (1 subgoal):
 1. rel_resource A B (map_resource' f res1) res2
[PROOF STEP]
by(coinduction arbitrary: res1 res2)
      (drule rel_resourceD, auto simp add: map_resource.sel map_resource_id1[symmetric] rel_fun_comp spmf_rel_map prod.rel_map[abs_def]
        elim!: rel_fun_mono rel_spmf_mono prod.rel_mono[THEN predicate2D, rotated -1])
[PROOF STATE]
proof (state)
this:
rel_resource A (\<lambda>x. B (f x)) res1 res2 \<Longrightarrow> rel_resource A B (map_resource' f res1) res2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rel_resource_map_resource'2:
  "rel_resource A B res1 (map_resource' f res2) = rel_resource A (\<lambda>x y. B x (f y)) res1 res2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_resource A B res1 (map_resource' f res2) = rel_resource A (\<lambda>x y. B x (f y)) res1 res2
[PROOF STEP]
using rel_resource_map_resource'1[of "conversep A" "conversep B" f res2 res1]
[PROOF STATE]
proof (prove)
using this:
rel_resource A\<inverse>\<inverse> B\<inverse>\<inverse> (map_resource' f res2) res1 = rel_resource A\<inverse>\<inverse> (\<lambda>x. B\<inverse>\<inverse> (f x)) res2 res1

goal (1 subgoal):
 1. rel_resource A B res1 (map_resource' f res2) = rel_resource A (\<lambda>x y. B x (f y)) res1 res2
[PROOF STEP]
by(rewrite in "\<hole> = _" conversep_iff[symmetric]
      , rewrite in "_ = \<hole>" conversep_iff[symmetric])
    (simp only: rel_resource_conversep[symmetric]
      , simp only: conversep_iff[abs_def])