[STATEMENT]
lemma lossless_resource_coinduct [consumes 1, case_names lossless_resource, case_conclusion lossless_resource lossless step, coinduct pred: lossless_resource]:
  assumes "X res"
    and "\<And>res a. \<lbrakk> X res; a \<in> outs_\<I> \<I> \<rbrakk> \<Longrightarrow> lossless_spmf (run_resource res a) \<and>
          (\<forall>(b, res') \<in> set_spmf (run_resource res a). X res' \<or> lossless_resource \<I> res')"
  shows "lossless_resource \<I> res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_resource \<I> res
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
X res

goal (1 subgoal):
 1. lossless_resource \<I> res
[PROOF STEP]
by(rule lossless_resource.coinduct)(auto dest: assms(2))