[STATEMENT]
lemma Wbis_raw_coind2:
assumes "theta \<subseteq> Wretr theta" and 
"theta ^-1 \<subseteq> Wretr (theta ^-1)"
shows "theta \<subseteq> Wbis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. theta \<subseteq> Wbis
[PROOF STEP]
using assms mono_Retr bis_raw_coind2
[PROOF STATE]
proof (prove)
using this:
theta \<subseteq> Wretr theta
theta\<inverse> \<subseteq> Wretr (theta\<inverse>)
Bisim.mono Sretr
Bisim.mono ZOretr
Bisim.mono ZOretrT
Bisim.mono Wretr
Bisim.mono WretrT
Bisim.mono RetrT
\<lbrakk>Bisim.mono ?Retr; ?theta \<subseteq> ?Retr ?theta; ?theta\<inverse> \<subseteq> ?Retr (?theta\<inverse>)\<rbrakk> \<Longrightarrow> ?theta \<subseteq> bis ?Retr

goal (1 subgoal):
 1. theta \<subseteq> Wbis
[PROOF STEP]
unfolding Wbis_def
[PROOF STATE]
proof (prove)
using this:
theta \<subseteq> Wretr theta
theta\<inverse> \<subseteq> Wretr (theta\<inverse>)
Bisim.mono Sretr
Bisim.mono ZOretr
Bisim.mono ZOretrT
Bisim.mono Wretr
Bisim.mono WretrT
Bisim.mono RetrT
\<lbrakk>Bisim.mono ?Retr; ?theta \<subseteq> ?Retr ?theta; ?theta\<inverse> \<subseteq> ?Retr (?theta\<inverse>)\<rbrakk> \<Longrightarrow> ?theta \<subseteq> bis ?Retr

goal (1 subgoal):
 1. theta \<subseteq> bis Wretr
[PROOF STEP]
by blast