[STATEMENT]
lemma lossless_inline[rotated]:
  fixes gpv :: "('a, 'call, 'ret) gpv"
  assumes gpv: "lossless_gpv \<I> gpv" "\<I> \<turnstile>g gpv \<surd>"
  and lossless: "\<And>s x. x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_gpv \<I>' (callee s x)"
  shows "lossless_gpv \<I>' (inline callee gpv s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_gpv \<I>' (inline callee gpv s)
[PROOF STEP]
using gpv
[PROOF STATE]
proof (prove)
using this:
lossless_gpv \<I> gpv
\<I> \<turnstile>g gpv \<surd>

goal (1 subgoal):
 1. lossless_gpv \<I>' (inline callee gpv s)
[PROOF STEP]
proof(induction arbitrary: s rule: lossless_WT_gpv_induct_strong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
case (lossless_gpv p)
[PROOF STATE]
proof (state)
this:
lossless_spmf p
IO ?out ?c \<in> set_spmf p \<Longrightarrow> ?out \<in> outs_\<I> \<I>
?gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> ?gpv
?gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g ?gpv \<surd>
?gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee ?gpv ?s)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
have lp: "lossless_gpv \<I> (GPV p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_gpv \<I> (GPV p)
[PROOF STEP]
by(rule lossless_sub_gpvsI)(auto intro: lossless_gpv.hyps)
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I> (GPV p)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I> (GPV p)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
have wp: "\<I> \<turnstile>g GPV p \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<I> \<turnstile>g GPV p \<surd>
[PROOF STEP]
by(rule WT_sub_gpvsI)(auto intro: lossless_gpv.hyps)
[PROOF STATE]
proof (state)
this:
\<I> \<turnstile>g GPV p \<surd>

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lossless_gpv \<I> (GPV p)
\<I> \<turnstile>g GPV p \<surd>
[PROOF STEP]
have "lossless_spmf (the_gpv (inline callee (GPV p) s))"
[PROOF STATE]
proof (prove)
using this:
lossless_gpv \<I> (GPV p)
\<I> \<turnstile>g GPV p \<surd>

goal (1 subgoal):
 1. lossless_spmf (the_gpv (inline callee (GPV p) s))
[PROOF STEP]
by(auto simp add: inline_sel intro: lossless_spmf_inline1 lossless_gpv_lossless_spmfD[OF lossless])
[PROOF STATE]
proof (state)
this:
lossless_spmf (the_gpv (inline callee (GPV p) s))

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lossless_spmf (the_gpv (inline callee (GPV p) s))

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
lossless_spmf (the_gpv (inline callee (GPV p) s))

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
fix out c input
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
assume IO: "IO out c \<in> set_spmf (the_gpv (inline callee (GPV p) s))"
      and "input \<in> responses_\<I> \<I>' out"
[PROOF STATE]
proof (state)
this:
IO out c \<in> set_spmf (the_gpv (inline callee (GPV p) s))
input \<in> responses_\<I> \<I>' out

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
from IO
[PROOF STATE]
proof (chain)
picking this:
IO out c \<in> set_spmf (the_gpv (inline callee (GPV p) s))
[PROOF STEP]
obtain callee' rpv
      where Inr: "Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)"
      and c: "c = (\<lambda>input. callee' input \<bind> (\<lambda>(x, y). inline callee (rpv x) y))"
[PROOF STATE]
proof (prove)
using this:
IO out c \<in> set_spmf (the_gpv (inline callee (GPV p) s))

goal (1 subgoal):
 1. (\<And>callee' rpv. \<lbrakk>Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s); c = (\<lambda>input. callee' input \<bind> (\<lambda>(x, y). inline callee (rpv x) y))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(clarsimp simp add: inline_sel split: sum.split_asm)
[PROOF STATE]
proof (state)
this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
c = (\<lambda>input. callee' input \<bind> (\<lambda>(x, y). inline callee (rpv x) y))

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
from Inr \<open>input \<in> _\<close> lossless lp wp
[PROOF STATE]
proof (chain)
picking this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
input \<in> responses_\<I> \<I>' out
?x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_gpv \<I>' (callee ?s ?x)
lossless_gpv \<I> (GPV p)
\<I> \<turnstile>g GPV p \<surd>
[PROOF STEP]
have "lossless_gpv \<I>' (callee' input)"
[PROOF STATE]
proof (prove)
using this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
input \<in> responses_\<I> \<I>' out
?x \<in> outs_\<I> \<I> \<Longrightarrow> lossless_gpv \<I>' (callee ?s ?x)
lossless_gpv \<I> (GPV p)
\<I> \<turnstile>g GPV p \<surd>

goal (1 subgoal):
 1. lossless_gpv \<I>' (callee' input)
[PROOF STEP]
by(rule lossless_inline1)
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (callee' input)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (callee' input)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (callee' input)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
fix x s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
assume "(x, s') \<in> results_gpv \<I>' (callee' input)"
[PROOF STATE]
proof (state)
this:
(x, s') \<in> results_gpv \<I>' (callee' input)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
with Inr
[PROOF STATE]
proof (chain)
picking this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
(x, s') \<in> results_gpv \<I>' (callee' input)
[PROOF STEP]
have "rpv x \<in> sub_gpvs \<I> (GPV p)"
[PROOF STATE]
proof (prove)
using this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
(x, s') \<in> results_gpv \<I>' (callee' input)

goal (1 subgoal):
 1. rpv x \<in> sub_gpvs \<I> (GPV p)
[PROOF STEP]
using \<open>input \<in> _\<close> wp
[PROOF STATE]
proof (prove)
using this:
Inr (out, callee', rpv) \<in> set_spmf (inline1 callee (GPV p) s)
(x, s') \<in> results_gpv \<I>' (callee' input)
input \<in> responses_\<I> \<I>' out
\<I> \<turnstile>g GPV p \<surd>

goal (1 subgoal):
 1. rpv x \<in> sub_gpvs \<I> (GPV p)
[PROOF STEP]
by(rule inline1_in_sub_gpvs)
[PROOF STATE]
proof (state)
this:
rpv x \<in> sub_gpvs \<I> (GPV p)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
hence "lossless_gpv \<I>' (inline callee (rpv x) s')"
[PROOF STATE]
proof (prove)
using this:
rpv x \<in> sub_gpvs \<I> (GPV p)

goal (1 subgoal):
 1. lossless_gpv \<I>' (inline callee (rpv x) s')
[PROOF STEP]
by(rule lossless_gpv.IH)
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (inline callee (rpv x) s')

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?x2, ?s'2) \<in> results_gpv \<I>' (callee' input) \<Longrightarrow> lossless_gpv \<I>' (inline callee (rpv ?x2) ?s'2)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lossless_gpv \<I>' (callee' input)
(?x2, ?s'2) \<in> results_gpv \<I>' (callee' input) \<Longrightarrow> lossless_gpv \<I>' (inline callee (rpv ?x2) ?s'2)
[PROOF STEP]
have "lossless_gpv \<I>' (c input)"
[PROOF STATE]
proof (prove)
using this:
lossless_gpv \<I>' (callee' input)
(?x2, ?s'2) \<in> results_gpv \<I>' (callee' input) \<Longrightarrow> lossless_gpv \<I>' (inline callee (rpv ?x2) ?s'2)

goal (1 subgoal):
 1. lossless_gpv \<I>' (c input)
[PROOF STEP]
unfolding c
[PROOF STATE]
proof (prove)
using this:
lossless_gpv \<I>' (callee' input)
(?x2, ?s'2) \<in> results_gpv \<I>' (callee' input) \<Longrightarrow> lossless_gpv \<I>' (inline callee (rpv ?x2) ?s'2)

goal (1 subgoal):
 1. lossless_gpv \<I>' (callee' input \<bind> (\<lambda>(x, y). inline callee (rpv x) y))
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (c input)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>IO ?out2 ?c2 \<in> set_spmf (the_gpv (inline callee (GPV p) s)); ?input2 \<in> responses_\<I> \<I>' ?out2\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (?c2 ?input2)

goal (1 subgoal):
 1. \<And>p s. \<lbrakk>lossless_spmf p; \<And>out c. IO out c \<in> set_spmf p \<Longrightarrow> out \<in> outs_\<I> \<I>; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I> gpv; \<And>gpv. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> \<I> \<turnstile>g gpv \<surd>; \<And>gpv s. gpv \<in> sub_gpvs \<I> (GPV p) \<Longrightarrow> lossless_gpv \<I>' (inline callee gpv s)\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lossless_spmf (the_gpv (inline callee (GPV p) s))
\<lbrakk>IO ?out2 ?c2 \<in> set_spmf (the_gpv (inline callee (GPV p) s)); ?input2 \<in> responses_\<I> \<I>' ?out2\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (?c2 ?input2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
lossless_spmf (the_gpv (inline callee (GPV p) s))
\<lbrakk>IO ?out2 ?c2 \<in> set_spmf (the_gpv (inline callee (GPV p) s)); ?input2 \<in> responses_\<I> \<I>' ?out2\<rbrakk> \<Longrightarrow> lossless_gpv \<I>' (?c2 ?input2)

goal (1 subgoal):
 1. lossless_gpv \<I>' (inline callee (GPV p) s)
[PROOF STEP]
by(rule lossless_gpvI)
[PROOF STATE]
proof (state)
this:
lossless_gpv \<I>' (inline callee (GPV p) s)

goal:
No subgoals!
[PROOF STEP]
qed