[STATEMENT]
lemma correct0:
  assumes e_in_carrier: "e \<in> carrier L"
    and "(x0,w0) \<in> Rel0"
    and valid_pub: "x1 \<in> valid_pub1"
  shows "\<Sigma>_OR.completeness_game (x0,x1) (Inl w0) e = return_spmf True"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
have "x \<in> carrier L \<longrightarrow> e = (e \<oplus> x) \<oplus> x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier L \<longrightarrow> e = (e \<oplus> x) \<oplus> x
[PROOF STEP]
using e_in_carrier xor_assoc
[PROOF STATE]
proof (prove)
using this:
e \<in> carrier L
\<lbrakk>?x \<in> carrier L; ?y \<in> carrier L; ?z \<in> carrier L\<rbrakk> \<Longrightarrow> (?x \<oplus> ?y) \<oplus> ?z = ?x \<oplus> ?y \<oplus> ?z

goal (1 subgoal):
 1. x \<in> carrier L \<longrightarrow> e = (e \<oplus> x) \<oplus> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?x \<in> carrier L \<longrightarrow> e = (e \<oplus> ?x) \<oplus> ?x

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
hence "?lhs = do {
    (r0,ab0) \<leftarrow> init0 x0 w0;
    eb' \<leftarrow> spmf_of_set (carrier L);
    (ab1', eb1'', zb1') \<leftarrow> \<Sigma>1.S x1 eb';
    let eb = e \<oplus> eb';
    zb0 \<leftarrow> response0 r0 w0 eb;
    return_spmf ((check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1'))}"
[PROOF STATE]
proof (prove)
using this:
?x \<in> carrier L \<longrightarrow> e = (e \<oplus> ?x) \<oplus> ?x

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = init0 x0 w0 \<bind> (\<lambda>(r0, ab0). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1')))))
[PROOF STEP]
by(simp add: \<Sigma>_OR.completeness_game_def split_def Let_def challenge_space_def assms check_OR_def cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = init0 x0 w0 \<bind> (\<lambda>(r0, ab0). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1')))))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = init0 x0 w0 \<bind> (\<lambda>(r0, ab0). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1')))))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
have "... = do {
    eb' \<leftarrow> spmf_of_set (carrier L);
    (ab1', eb1'', zb1') \<leftarrow> \<Sigma>1.S x1 eb';
    let eb = e \<oplus> eb';
    (r0,ab0) \<leftarrow> init0 x0 w0;
    zb0 \<leftarrow> response0 r0 w0 eb;
    return_spmf ((check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1'))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init0 x0 w0 \<bind> (\<lambda>(r0, ab0). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1'))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1')))))
[PROOF STEP]
apply(simp add: Let_def split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init0 x0 w0 \<bind> (\<lambda>p. spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>pa. response0 (fst p) w0 (e \<oplus> eb') \<bind> (\<lambda>zb0. return_spmf (check0 x0 (snd p) (e \<oplus> eb') zb0 \<and> check1 x1 (fst pa) eb' (snd (snd pa))))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>p. init0 x0 w0 \<bind> (\<lambda>pa. response0 (fst pa) w0 (e \<oplus> eb') \<bind> (\<lambda>zb0. return_spmf (check0 x0 (snd pa) (e \<oplus> eb') zb0 \<and> check1 x1 (fst p) eb' (snd (snd p)))))))
[PROOF STEP]
apply(rewrite bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>y. init0 x0 w0 \<bind> (\<lambda>p. \<Sigma>1.S x1 y \<bind> (\<lambda>pa. response0 (fst p) w0 (e \<oplus> y) \<bind> (\<lambda>zb0. return_spmf (check0 x0 (snd p) (e \<oplus> y) zb0 \<and> check1 x1 (fst pa) y (snd (snd pa))))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>p. init0 x0 w0 \<bind> (\<lambda>pa. response0 (fst pa) w0 (e \<oplus> eb') \<bind> (\<lambda>zb0. return_spmf (check0 x0 (snd pa) (e \<oplus> eb') zb0 \<and> check1 x1 (fst p) eb' (snd (snd p)))))))
[PROOF STEP]
apply(rewrite bind_commute_spmf[of _ "\<Sigma>1.S _ _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>y. \<Sigma>1.S x1 y \<bind> (\<lambda>ya. init0 x0 w0 \<bind> (\<lambda>p. response0 (fst p) w0 (e \<oplus> y) \<bind> (\<lambda>zb0. return_spmf (check0 x0 (snd p) (e \<oplus> y) zb0 \<and> check1 x1 (fst ya) y (snd (snd ya))))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>p. init0 x0 w0 \<bind> (\<lambda>pa. response0 (fst pa) w0 (e \<oplus> eb') \<bind> (\<lambda>zb0. return_spmf (check0 x0 (snd pa) (e \<oplus> eb') zb0 \<and> check1 x1 (fst p) eb' (snd (snd p)))))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
init0 x0 w0 \<bind> (\<lambda>(r0, ab0). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1'))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1')))))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
init0 x0 w0 \<bind> (\<lambda>(r0, ab0). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1'))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1')))))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
have "... = do {
    eb' :: 'e \<leftarrow> spmf_of_set (carrier L);
    (ab1', eb1'', zb1') \<leftarrow> \<Sigma>1.S x1 eb';
    return_spmf (check1 x1 ab1' eb' zb1')}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1'))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1')))
[PROOF STEP]
apply(simp add: Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 (e \<oplus> eb') \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 (e \<oplus> eb') zb0 \<and> check1 x1 ab1' eb' zb1'))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1')))
[PROOF STEP]
apply(intro bind_spmf_cong; clarsimp?)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a aa b. \<lbrakk>x \<in> carrier L; (a, aa, b) \<in> set_spmf (\<Sigma>1.S x1 x)\<rbrakk> \<Longrightarrow> init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 (e \<oplus> x) \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 (e \<oplus> x) zb0 \<and> check1 x1 a x b))) = return_spmf (check1 x1 a x b)
[PROOF STEP]
subgoal for e' a e z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e' \<in> carrier L; (a, e, z) \<in> set_spmf (\<Sigma>1.S x1 e')\<rbrakk> \<Longrightarrow> init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 (e \<oplus> e') \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 (e \<oplus> e') zb0 \<and> check1 x1 a e' z))) = return_spmf (check1 x1 a e' z)
[PROOF STEP]
apply(cases "check1 x1 a e' z")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>e' \<in> carrier L; (a, e, z) \<in> set_spmf (\<Sigma>1.S x1 e'); check1 x1 a e' z\<rbrakk> \<Longrightarrow> init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 (e \<oplus> e') \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 (e \<oplus> e') zb0 \<and> check1 x1 a e' z))) = return_spmf (check1 x1 a e' z)
 2. \<lbrakk>e' \<in> carrier L; (a, e, z) \<in> set_spmf (\<Sigma>1.S x1 e'); \<not> check1 x1 a e' z\<rbrakk> \<Longrightarrow> init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 (e \<oplus> e') \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 (e \<oplus> e') zb0 \<and> check1 x1 a e' z))) = return_spmf (check1 x1 a e' z)
[PROOF STEP]
using \<Sigma>0.complete_game_return_true \<Sigma>_prot0 \<Sigma>0.completeness_game_def \<Sigma>0.\<Sigma>_protocol_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?h, ?w) \<in> Rel0; \<Sigma>0.completeness; \<forall>h w. lossless_spmf (init0 h w); \<forall>r w e. lossless_spmf (response0 r w e); ?e \<in> carrier L\<rbrakk> \<Longrightarrow> \<Sigma>0.completeness_game ?h ?w ?e = return_spmf True
\<Sigma>0.\<Sigma>_protocol
\<Sigma>0.completeness_game ?h ?w ?e = init0 ?h ?w \<bind> (\<lambda>(r, a). response0 r ?w ?e \<bind> (\<lambda>z. return_spmf (check0 ?h a ?e z)))
\<Sigma>0.\<Sigma>_protocol \<equiv> \<Sigma>0.completeness \<and> \<Sigma>0.special_soundness \<and> \<Sigma>0.HVZK

goal (2 subgoals):
 1. \<lbrakk>e' \<in> carrier L; (a, e, z) \<in> set_spmf (\<Sigma>1.S x1 e'); check1 x1 a e' z\<rbrakk> \<Longrightarrow> init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 (e \<oplus> e') \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 (e \<oplus> e') zb0 \<and> check1 x1 a e' z))) = return_spmf (check1 x1 a e' z)
 2. \<lbrakk>e' \<in> carrier L; (a, e, z) \<in> set_spmf (\<Sigma>1.S x1 e'); \<not> check1 x1 a e' z\<rbrakk> \<Longrightarrow> init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 (e \<oplus> e') \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 (e \<oplus> e') zb0 \<and> check1 x1 a e' z))) = return_spmf (check1 x1 a e' z)
[PROOF STEP]
by(auto simp add: assms bind_spmf_const lossless_init lossless_response lossless_weight_spmfD split_def cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1'))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1')))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = e \<oplus> eb' in init0 x0 w0 \<bind> (\<lambda>(r0, ab0). response0 r0 w0 eb \<bind> (\<lambda>zb0. return_spmf (check0 x0 ab0 eb zb0 \<and> check1 x1 ab1' eb' zb1'))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1')))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
have "... = do {
    eb' :: 'e \<leftarrow> spmf_of_set (carrier L);
    (ab1', eb1'', zb1') \<leftarrow> \<Sigma>1.S x1 eb';
    return_spmf (True)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1'))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf True))
[PROOF STEP]
apply(intro bind_spmf_cong; clarsimp?)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a aa b. \<lbrakk>x \<in> carrier L; (a, aa, b) \<in> set_spmf (\<Sigma>1.S x1 x)\<rbrakk> \<Longrightarrow> check1 x1 a x b
[PROOF STEP]
subgoal for x a aa b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier L; (a, aa, b) \<in> set_spmf (\<Sigma>1.S x1 x)\<rbrakk> \<Longrightarrow> check1 x1 a x b
[PROOF STEP]
using  \<Sigma>_prot1
[PROOF STATE]
proof (prove)
using this:
\<Sigma>1.\<Sigma>_protocol

goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier L; (a, aa, b) \<in> set_spmf (\<Sigma>1.S x1 x)\<rbrakk> \<Longrightarrow> check1 x1 a x b
[PROOF STEP]
apply(auto simp add: \<Sigma>1.S_def split_def image_def \<Sigma>1.HVZK_unfold2_alt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier L; \<Sigma>1.\<Sigma>_protocol; (a, b) \<in> set_spmf (S1_raw x1 x); aa = x\<rbrakk> \<Longrightarrow> check1 x1 a x b
[PROOF STEP]
using \<Sigma>1.S_def split_def image_def \<Sigma>1.HVZK_unfold2_alt \<Sigma>_prot1 valid_pub
[PROOF STATE]
proof (prove)
using this:
\<Sigma>1.S ?h ?e = map_spmf (\<lambda>(a, z). (a, ?e, z)) (S1_raw ?h ?e)
case_prod = (\<lambda>c p. c (fst p) (snd p))
?f ` ?A = {y. \<exists>x\<in>?A. y = ?f x}
\<Sigma>1.\<Sigma>_protocol \<Longrightarrow> \<forall>h a e z. e \<in> carrier L \<longrightarrow> h \<in> valid_pub1 \<longrightarrow> (a, z) \<in> set_spmf (S1_raw h e) \<longrightarrow> check1 h a e z
\<Sigma>1.\<Sigma>_protocol
x1 \<in> valid_pub1

goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier L; \<Sigma>1.\<Sigma>_protocol; (a, b) \<in> set_spmf (S1_raw x1 x); aa = x\<rbrakk> \<Longrightarrow> check1 x1 a x b
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1'))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf True))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1')))
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1'))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf True))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1')))
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1'))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf True))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
using \<Sigma>1.HVZK_unfold2_alt
[PROOF STATE]
proof (prove)
using this:
\<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1')))
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf (check1 x1 ab1' eb' zb1'))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). return_spmf True))
\<Sigma>1.\<Sigma>_protocol \<Longrightarrow> \<forall>h a e z. e \<in> carrier L \<longrightarrow> h \<in> valid_pub1 \<longrightarrow> (a, z) \<in> set_spmf (S1_raw h e) \<longrightarrow> check1 h a e z

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True
[PROOF STEP]
by(simp add: bind_spmf_const Let_def \<Sigma>1.HVZK_unfold2_alt split_def lossless_\<Sigma>_S lossless_weight_spmfD carrier_L_not_empty finite_L)
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.completeness_game (x0, x1) (Inl w0) e = return_spmf True

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma correct1:
  assumes rel1: "(x1,w1) \<in> Rel1"
    and valid_pub: "x0 \<in> valid_pub0"
    and e_in_carrier: "e \<in> carrier L"
  shows "\<Sigma>_OR.completeness_game (x0,x1) (Inr w1) e = return_spmf True"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
have x1_inL: "x1 \<in> \<Sigma>1.L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<in> \<Sigma>1.L
[PROOF STEP]
using \<Sigma>1.L_def rel1
[PROOF STATE]
proof (prove)
using this:
\<Sigma>1.L \<equiv> {x. \<exists>w. (x, w) \<in> Rel1}
(x1, w1) \<in> Rel1

goal (1 subgoal):
 1. x1 \<in> \<Sigma>1.L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x1 \<in> \<Sigma>1.L

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
have "x \<in> carrier L \<longrightarrow> e = x \<oplus> e \<oplus> x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier L \<longrightarrow> e = x \<oplus> e \<oplus> x
[PROOF STEP]
by (simp add: e_in_carrier xor_assoc xor_commute  local.xor_ac(3))
[PROOF STATE]
proof (state)
this:
?x \<in> carrier L \<longrightarrow> e = ?x \<oplus> e \<oplus> ?x

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
hence "?lhs = do {
    (r1, ab1) \<leftarrow> init1 x1 w1;
    eb' \<leftarrow> spmf_of_set (carrier L);
    (ab0', eb0'', zb0') \<leftarrow> \<Sigma>0.S x0 eb';
    let eb = e \<oplus> eb';
    zb1 \<leftarrow> response1 r1 w1 eb;
    return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1)}"
[PROOF STATE]
proof (prove)
using this:
?x \<in> carrier L \<longrightarrow> e = ?x \<oplus> e \<oplus> ?x

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = init1 x1 w1 \<bind> (\<lambda>(r1, ab1). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1)))))
[PROOF STEP]
by(simp add: \<Sigma>_OR.completeness_game_def split_def Let_def assms challenge_space_def check_OR_def cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = init1 x1 w1 \<bind> (\<lambda>(r1, ab1). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1)))))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = init1 x1 w1 \<bind> (\<lambda>(r1, ab1). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1)))))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
have "... = do {
    eb' \<leftarrow> spmf_of_set (carrier L);
    (ab0', eb0'', zb0') \<leftarrow> \<Sigma>0.S x0 eb';
    let eb = e \<oplus> eb';
    (r1, ab1) \<leftarrow> init1 x1 w1;
    zb1 \<leftarrow> response1 r1 w1 eb;
    return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init1 x1 w1 \<bind> (\<lambda>(r1, ab1). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1)))))
[PROOF STEP]
apply(simp add: Let_def split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. init1 x1 w1 \<bind> (\<lambda>p. spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>pa. response1 (fst p) w1 (e \<oplus> eb') \<bind> (\<lambda>zb1. return_spmf (check0 x0 (fst pa) eb' (snd (snd pa)) \<and> check1 x1 (snd p) (e \<oplus> eb') zb1))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>p. init1 x1 w1 \<bind> (\<lambda>pa. response1 (fst pa) w1 (e \<oplus> eb') \<bind> (\<lambda>zb1. return_spmf (check0 x0 (fst p) eb' (snd (snd p)) \<and> check1 x1 (snd pa) (e \<oplus> eb') zb1)))))
[PROOF STEP]
apply(rewrite bind_commute_spmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>y. init1 x1 w1 \<bind> (\<lambda>p. \<Sigma>0.S x0 y \<bind> (\<lambda>pa. response1 (fst p) w1 (e \<oplus> y) \<bind> (\<lambda>zb1. return_spmf (check0 x0 (fst pa) y (snd (snd pa)) \<and> check1 x1 (snd p) (e \<oplus> y) zb1))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>p. init1 x1 w1 \<bind> (\<lambda>pa. response1 (fst pa) w1 (e \<oplus> eb') \<bind> (\<lambda>zb1. return_spmf (check0 x0 (fst p) eb' (snd (snd p)) \<and> check1 x1 (snd pa) (e \<oplus> eb') zb1)))))
[PROOF STEP]
apply(rewrite bind_commute_spmf[of _ "\<Sigma>0.S _ _"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>y. \<Sigma>0.S x0 y \<bind> (\<lambda>ya. init1 x1 w1 \<bind> (\<lambda>p. response1 (fst p) w1 (e \<oplus> y) \<bind> (\<lambda>zb1. return_spmf (check0 x0 (fst ya) y (snd (snd ya)) \<and> check1 x1 (snd p) (e \<oplus> y) zb1))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>p. init1 x1 w1 \<bind> (\<lambda>pa. response1 (fst pa) w1 (e \<oplus> eb') \<bind> (\<lambda>zb1. return_spmf (check0 x0 (fst p) eb' (snd (snd p)) \<and> check1 x1 (snd pa) (e \<oplus> eb') zb1)))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
init1 x1 w1 \<bind> (\<lambda>(r1, ab1). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1)))))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
init1 x1 w1 \<bind> (\<lambda>(r1, ab1). spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1)))))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
have "... = do {
    eb' \<leftarrow> spmf_of_set (carrier L);
    (ab0', eb0'', zb0') \<leftarrow> \<Sigma>0.S x0 eb';
    return_spmf (check0 x0 ab0' eb' zb0')}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0')))
[PROOF STEP]
apply(simp add: Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 (e \<oplus> eb') \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 (e \<oplus> eb') zb1))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0')))
[PROOF STEP]
apply(intro bind_spmf_cong; clarsimp?)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a aa b. \<lbrakk>x \<in> carrier L; (a, aa, b) \<in> set_spmf (\<Sigma>0.S x0 x)\<rbrakk> \<Longrightarrow> init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 (e \<oplus> x) \<bind> (\<lambda>zb1. return_spmf (check0 x0 a x b \<and> check1 x1 ab1 (e \<oplus> x) zb1))) = return_spmf (check0 x0 a x b)
[PROOF STEP]
subgoal for e' a e z
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e' \<in> carrier L; (a, e, z) \<in> set_spmf (\<Sigma>0.S x0 e')\<rbrakk> \<Longrightarrow> init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 (e \<oplus> e') \<bind> (\<lambda>zb1. return_spmf (check0 x0 a e' z \<and> check1 x1 ab1 (e \<oplus> e') zb1))) = return_spmf (check0 x0 a e' z)
[PROOF STEP]
apply(cases "check0 x0 a e' z")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>e' \<in> carrier L; (a, e, z) \<in> set_spmf (\<Sigma>0.S x0 e'); check0 x0 a e' z\<rbrakk> \<Longrightarrow> init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 (e \<oplus> e') \<bind> (\<lambda>zb1. return_spmf (check0 x0 a e' z \<and> check1 x1 ab1 (e \<oplus> e') zb1))) = return_spmf (check0 x0 a e' z)
 2. \<lbrakk>e' \<in> carrier L; (a, e, z) \<in> set_spmf (\<Sigma>0.S x0 e'); \<not> check0 x0 a e' z\<rbrakk> \<Longrightarrow> init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 (e \<oplus> e') \<bind> (\<lambda>zb1. return_spmf (check0 x0 a e' z \<and> check1 x1 ab1 (e \<oplus> e') zb1))) = return_spmf (check0 x0 a e' z)
[PROOF STEP]
using \<Sigma>1.complete_game_return_true \<Sigma>_prot1 \<Sigma>1.completeness_game_def \<Sigma>1.\<Sigma>_protocol_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?h, ?w) \<in> Rel1; \<Sigma>1.completeness; \<forall>h w. lossless_spmf (init1 h w); \<forall>r w e. lossless_spmf (response1 r w e); ?e \<in> carrier L\<rbrakk> \<Longrightarrow> \<Sigma>1.completeness_game ?h ?w ?e = return_spmf True
\<Sigma>1.\<Sigma>_protocol
\<Sigma>1.completeness_game ?h ?w ?e = init1 ?h ?w \<bind> (\<lambda>(r, a). response1 r ?w ?e \<bind> (\<lambda>z. return_spmf (check1 ?h a ?e z)))
\<Sigma>1.\<Sigma>_protocol \<equiv> \<Sigma>1.completeness \<and> \<Sigma>1.special_soundness \<and> \<Sigma>1.HVZK

goal (2 subgoals):
 1. \<lbrakk>e' \<in> carrier L; (a, e, z) \<in> set_spmf (\<Sigma>0.S x0 e'); check0 x0 a e' z\<rbrakk> \<Longrightarrow> init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 (e \<oplus> e') \<bind> (\<lambda>zb1. return_spmf (check0 x0 a e' z \<and> check1 x1 ab1 (e \<oplus> e') zb1))) = return_spmf (check0 x0 a e' z)
 2. \<lbrakk>e' \<in> carrier L; (a, e, z) \<in> set_spmf (\<Sigma>0.S x0 e'); \<not> check0 x0 a e' z\<rbrakk> \<Longrightarrow> init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 (e \<oplus> e') \<bind> (\<lambda>zb1. return_spmf (check0 x0 a e' z \<and> check1 x1 ab1 (e \<oplus> e') zb1))) = return_spmf (check0 x0 a e' z)
[PROOF STEP]
by(auto simp add: x1_inL assms bind_spmf_const lossless_init lossless_response lossless_weight_spmfD split_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0')))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = e \<oplus> eb' in init1 x1 w1 \<bind> (\<lambda>(r1, ab1). response1 r1 w1 eb \<bind> (\<lambda>zb1. return_spmf (check0 x0 ab0' eb' zb0' \<and> check1 x1 ab1 eb zb1))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0')))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
have "... = do {
    eb' \<leftarrow> spmf_of_set (carrier L);
    (ab0', eb0'', zb0') \<leftarrow> \<Sigma>0.S x0 eb';
    return_spmf (True)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0'))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf True))
[PROOF STEP]
apply(intro bind_spmf_cong; clarsimp?)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a aa b. \<lbrakk>x \<in> carrier L; (a, aa, b) \<in> set_spmf (\<Sigma>0.S x0 x)\<rbrakk> \<Longrightarrow> check0 x0 a x b
[PROOF STEP]
subgoal for x a aa b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier L; (a, aa, b) \<in> set_spmf (\<Sigma>0.S x0 x)\<rbrakk> \<Longrightarrow> check0 x0 a x b
[PROOF STEP]
using  \<Sigma>_prot0
[PROOF STATE]
proof (prove)
using this:
\<Sigma>0.\<Sigma>_protocol

goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier L; (a, aa, b) \<in> set_spmf (\<Sigma>0.S x0 x)\<rbrakk> \<Longrightarrow> check0 x0 a x b
[PROOF STEP]
by(auto simp add: valid_pub valid_pub_OR_def \<Sigma>0.S_def split_def image_def \<Sigma>0.HVZK_unfold2_alt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0'))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf True))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0')))
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0'))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf True))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0')))
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0'))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf True))

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True
[PROOF STEP]
apply(simp add: \<Sigma>0.HVZK_unfold2 Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf True)); spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0'))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf True))\<rbrakk> \<Longrightarrow> spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf True)) = return_spmf True
[PROOF STEP]
using \<Sigma>0.complete_game_return_true \<Sigma>_OR.completeness_game_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?h, ?w) \<in> Rel0; \<Sigma>0.completeness; \<forall>h w. lossless_spmf (init0 h w); \<forall>r w e. lossless_spmf (response0 r w e); ?e \<in> carrier L\<rbrakk> \<Longrightarrow> \<Sigma>0.completeness_game ?h ?w ?e = return_spmf True
\<Sigma>_OR.completeness_game ?h ?w ?e = init_OR ?h ?w \<bind> (\<lambda>(r, a). response_OR r ?w ?e \<bind> (\<lambda>z. return_spmf (check_OR ?h a ?e z)))

goal (1 subgoal):
 1. \<lbrakk>\<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf True)); spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf (check0 x0 ab0' eb' zb0'))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf True))\<rbrakk> \<Longrightarrow> spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf True)) = return_spmf True
[PROOF STEP]
by(simp add: bind_spmf_const split_def lossless_\<Sigma>_S(2) lossless_weight_spmfD Let_def carrier_L_not_empty finite_L)
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.completeness_game (x0, x1) (Inr w1) e = return_spmf True

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma completeness':
  assumes  Rel_OR_asm: "((x0,x1), w) \<in> Rel_OR"
  shows "\<forall> e \<in> carrier L. spmf (\<Sigma>_OR.completeness_game (x0,x1) w e) True = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>carrier L. spmf (\<Sigma>_OR.completeness_game (x0, x1) w e) True = 1
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. e \<in> carrier L \<Longrightarrow> spmf (\<Sigma>_OR.completeness_game (x0, x1) w e) True = 1
[PROOF STEP]
fix e
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. e \<in> carrier L \<Longrightarrow> spmf (\<Sigma>_OR.completeness_game (x0, x1) w e) True = 1
[PROOF STEP]
assume asm: "e \<in> carrier L"
[PROOF STATE]
proof (state)
this:
e \<in> carrier L

goal (1 subgoal):
 1. \<And>e. e \<in> carrier L \<Longrightarrow> spmf (\<Sigma>_OR.completeness_game (x0, x1) w e) True = 1
[PROOF STEP]
hence "(\<Sigma>_OR.completeness_game (x0,x1) w e) = return_spmf True"
[PROOF STATE]
proof (prove)
using this:
e \<in> carrier L

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
[PROOF STEP]
proof(cases w)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>e \<in> carrier L; w = Inl a\<rbrakk> \<Longrightarrow> \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
 2. \<And>b. \<lbrakk>e \<in> carrier L; w = Inr b\<rbrakk> \<Longrightarrow> \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
[PROOF STEP]
case inl: (Inl a)
[PROOF STATE]
proof (state)
this:
w = Inl a

goal (2 subgoals):
 1. \<And>a. \<lbrakk>e \<in> carrier L; w = Inl a\<rbrakk> \<Longrightarrow> \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
 2. \<And>b. \<lbrakk>e \<in> carrier L; w = Inr b\<rbrakk> \<Longrightarrow> \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w = Inl a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w = Inl a

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
[PROOF STEP]
using asm correct0 assms inl
[PROOF STATE]
proof (prove)
using this:
w = Inl a
e \<in> carrier L
\<lbrakk>?e \<in> carrier L; (?x0.0, ?w0.0) \<in> Rel0; ?x1.0 \<in> valid_pub1\<rbrakk> \<Longrightarrow> \<Sigma>_OR.completeness_game (?x0.0, ?x1.0) (Inl ?w0.0) ?e = return_spmf True
((x0, x1), w) \<in> Rel_OR
w = Inl a

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True

goal (1 subgoal):
 1. \<And>b. \<lbrakk>e \<in> carrier L; w = Inr b\<rbrakk> \<Longrightarrow> \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>e \<in> carrier L; w = Inr b\<rbrakk> \<Longrightarrow> \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
[PROOF STEP]
case inr: (Inr b)
[PROOF STATE]
proof (state)
this:
w = Inr b

goal (1 subgoal):
 1. \<And>b. \<lbrakk>e \<in> carrier L; w = Inr b\<rbrakk> \<Longrightarrow> \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w = Inr b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w = Inr b

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
[PROOF STEP]
using asm correct1 assms inr
[PROOF STATE]
proof (prove)
using this:
w = Inr b
e \<in> carrier L
\<lbrakk>(?x1.0, ?w1.0) \<in> Rel1; ?x0.0 \<in> valid_pub0; ?e \<in> carrier L\<rbrakk> \<Longrightarrow> \<Sigma>_OR.completeness_game (?x0.0, ?x1.0) (Inr ?w1.0) ?e = return_spmf True
((x0, x1), w) \<in> Rel_OR
w = Inr b

goal (1 subgoal):
 1. \<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True

goal (1 subgoal):
 1. \<And>e. e \<in> carrier L \<Longrightarrow> spmf (\<Sigma>_OR.completeness_game (x0, x1) w e) True = 1
[PROOF STEP]
thus "spmf (\<Sigma>_OR.completeness_game (x0,x1) w e) True = 1"
[PROOF STATE]
proof (prove)
using this:
\<Sigma>_OR.completeness_game (x0, x1) w e = return_spmf True

goal (1 subgoal):
 1. spmf (\<Sigma>_OR.completeness_game (x0, x1) w e) True = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
spmf (\<Sigma>_OR.completeness_game (x0, x1) w e) True = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma completeness: shows "\<Sigma>_OR.completeness"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma>_OR.completeness
[PROOF STEP]
unfolding \<Sigma>_OR.completeness_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h w e. (h, w) \<in> Rel_OR \<longrightarrow> e \<in> challenge_space \<longrightarrow> spmf (\<Sigma>_OR.completeness_game h w e) True = 1
[PROOF STEP]
using completeness' challenge_space_def
[PROOF STATE]
proof (prove)
using this:
((?x0.0, ?x1.0), ?w) \<in> Rel_OR \<Longrightarrow> \<forall>e\<in>carrier L. spmf (\<Sigma>_OR.completeness_game (?x0.0, ?x1.0) ?w e) True = 1
challenge_space = carrier L

goal (1 subgoal):
 1. \<forall>h w e. (h, w) \<in> Rel_OR \<longrightarrow> e \<in> challenge_space \<longrightarrow> spmf (\<Sigma>_OR.completeness_game h w e) True = 1
[PROOF STEP]
by auto


[STATEMENT]
lemma \<Sigma>_protocol: shows "\<Sigma>_OR.\<Sigma>_protocol"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma>_OR.\<Sigma>_protocol
[PROOF STEP]
by(simp add: completeness HVZK special_soundness \<Sigma>_OR.\<Sigma>_protocol_def)


[STATEMENT]
lemma "OR_\<Sigma>_commit.abstract_com.correct"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OR_\<Sigma>_commit.abstract_com.correct
[PROOF STEP]
using OR_\<Sigma>_commit.commit_correct
[PROOF STATE]
proof (prove)
using this:
OR_\<Sigma>_commit.abstract_com.correct

goal (1 subgoal):
 1. OR_\<Sigma>_commit.abstract_com.correct
[PROOF STEP]
by simp


[STATEMENT]
lemma "OR_\<Sigma>_commit.abstract_com.perfect_hiding_ind_cpa \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OR_\<Sigma>_commit.abstract_com.perfect_hiding_ind_cpa \
[PROOF STEP]
using OR_\<Sigma>_commit.perfect_hiding
[PROOF STATE]
proof (prove)
using this:
OR_\<Sigma>_commit.abstract_com.perfect_hiding_ind_cpa ?\

goal (1 subgoal):
 1. OR_\<Sigma>_commit.abstract_com.perfect_hiding_ind_cpa \
[PROOF STEP]
by blast


[STATEMENT]
lemma bind_advantage_bound_dis_log:
  shows "OR_\<Sigma>_commit.abstract_com.bind_advantage \<A> \<le> OR_\<Sigma>_commit.rel_advantage (OR_\<Sigma>_commit.adversary \<A>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OR_\<Sigma>_commit.abstract_com.bind_advantage \<A> \<le> OR_\<Sigma>_commit.rel_advantage (OR_\<Sigma>_commit.adversary \<A>)
[PROOF STEP]
using OR_\<Sigma>_commit.bind_advantage
[PROOF STATE]
proof (prove)
using this:
OR_\<Sigma>_commit.abstract_com.bind_advantage ?\<A> \<le> OR_\<Sigma>_commit.rel_advantage (OR_\<Sigma>_commit.adversary ?\<A>)

goal (1 subgoal):
 1. OR_\<Sigma>_commit.abstract_com.bind_advantage \<A> \<le> OR_\<Sigma>_commit.rel_advantage (OR_\<Sigma>_commit.adversary \<A>)
[PROOF STEP]
by simp


[STATEMENT]
lemma grid_ge_min:
  shows "t 0 \<le> t j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t 0 \<le> t j
[PROOF STEP]
proof (induct j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t 0 \<le> t 0
 2. \<And>j. t 0 \<le> t j \<Longrightarrow> t 0 \<le> t (Suc j)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t 0 \<le> t 0
 2. \<And>j. t 0 \<le> t j \<Longrightarrow> t 0 \<le> t (Suc j)
[PROOF STEP]
assume "t 0 \<le> t j"
[PROOF STATE]
proof (state)
this:
t 0 \<le> t j

goal (2 subgoals):
 1. t 0 \<le> t 0
 2. \<And>j. t 0 \<le> t j \<Longrightarrow> t 0 \<le> t (Suc j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
t 0 \<le> t j

goal (2 subgoals):
 1. t 0 \<le> t 0
 2. \<And>j. t 0 \<le> t j \<Longrightarrow> t 0 \<le> t (Suc j)
[PROOF STEP]
from grid
[PROOF STATE]
proof (chain)
picking this:
t ?i \<le> t (Suc ?i)
[PROOF STEP]
have "t j \<le> t (Suc j)"
[PROOF STATE]
proof (prove)
using this:
t ?i \<le> t (Suc ?i)

goal (1 subgoal):
 1. t j \<le> t (Suc j)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
t j \<le> t (Suc j)

goal (2 subgoals):
 1. t 0 \<le> t 0
 2. \<And>j. t 0 \<le> t j \<Longrightarrow> t 0 \<le> t (Suc j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
t 0 \<le> t (Suc j)
[PROOF STEP]
show "t 0 \<le> t (Suc j)"
[PROOF STATE]
proof (prove)
using this:
t 0 \<le> t (Suc j)

goal (1 subgoal):
 1. t 0 \<le> t (Suc j)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
t 0 \<le> t (Suc j)

goal (1 subgoal):
 1. t 0 \<le> t 0
[PROOF STEP]
qed simp


[STATEMENT]
lemma grid_mono:
  assumes "j \<le> n"
  shows "t j \<le> t n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t j \<le> t n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
j \<le> n

goal (1 subgoal):
 1. t j \<le> t n
[PROOF STEP]
proof (induct rule: inc_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t n \<le> t n
 2. \<And>na. \<lbrakk>j \<le> na; na < n; t (Suc na) \<le> t n\<rbrakk> \<Longrightarrow> t na \<le> t n
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t n \<le> t n
 2. \<And>na. \<lbrakk>j \<le> na; na < n; t (Suc na) \<le> t n\<rbrakk> \<Longrightarrow> t na \<le> t n
[PROOF STEP]
assume "j < n" "t (Suc j) \<le> t n"
[PROOF STATE]
proof (state)
this:
j < n
t (Suc j) \<le> t n

goal (2 subgoals):
 1. t n \<le> t n
 2. \<And>na. \<lbrakk>j \<le> na; na < n; t (Suc na) \<le> t n\<rbrakk> \<Longrightarrow> t na \<le> t n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < n
t (Suc j) \<le> t n

goal (2 subgoals):
 1. t n \<le> t n
 2. \<And>na. \<lbrakk>j \<le> na; na < n; t (Suc na) \<le> t n\<rbrakk> \<Longrightarrow> t na \<le> t n
[PROOF STEP]
with grid
[PROOF STATE]
proof (chain)
picking this:
t ?i \<le> t (Suc ?i)
j < n
t (Suc j) \<le> t n
[PROOF STEP]
have "t j \<le> t (Suc j)"
[PROOF STATE]
proof (prove)
using this:
t ?i \<le> t (Suc ?i)
j < n
t (Suc j) \<le> t n

goal (1 subgoal):
 1. t j \<le> t (Suc j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t j \<le> t (Suc j)

goal (2 subgoals):
 1. t n \<le> t n
 2. \<And>na. \<lbrakk>j \<le> na; na < n; t (Suc na) \<le> t n\<rbrakk> \<Longrightarrow> t na \<le> t n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
j < n
t (Suc j) \<le> t n
t j \<le> t (Suc j)
[PROOF STEP]
show "t j \<le> t n"
[PROOF STATE]
proof (prove)
using this:
j < n
t (Suc j) \<le> t n
t j \<le> t (Suc j)

goal (1 subgoal):
 1. t j \<le> t n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t j \<le> t n

goal (1 subgoal):
 1. t n \<le> t n
[PROOF STEP]
qed simp


[STATEMENT]
lemma grid_stepsize_nonneg:
  shows "stepsize j \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> stepsize j
[PROOF STEP]
using grid
[PROOF STATE]
proof (prove)
using this:
t ?i \<le> t (Suc ?i)

goal (1 subgoal):
 1. 0 \<le> stepsize j
[PROOF STEP]
unfolding stepsize_def
[PROOF STATE]
proof (prove)
using this:
t ?i \<le> t (Suc ?i)

goal (1 subgoal):
 1. 0 \<le> t (Suc j) - t j
[PROOF STEP]
by (simp add: field_simps order_less_imp_le)


[STATEMENT]
lemma grid_stepsize_sum:
  shows "(\<Sum>i\<in>{0..<n}. stepsize i) = t n - t 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum stepsize {0..<n} = t n - t 0
[PROOF STEP]
by (induct n) (simp_all add: stepsize_def)


[STATEMENT]
lemma max_stepsize_ge_stepsize:
  assumes "j \<le> n"
  shows "max_stepsize n \<ge> stepsize j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stepsize j \<le> max_stepsize n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
j \<le> n

goal (1 subgoal):
 1. stepsize j \<le> max_stepsize n
[PROOF STEP]
by (auto simp: max_stepsize_def)


[STATEMENT]
lemma max_stepsize_nonneg:
  shows "max_stepsize n \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> max_stepsize n
[PROOF STEP]
using grid_stepsize_nonneg[of 0]
    max_stepsize_ge_stepsize[of 0 n]
[PROOF STATE]
proof (prove)
using this:
0 \<le> stepsize 0
0 \<le> n \<Longrightarrow> stepsize 0 \<le> max_stepsize n

goal (1 subgoal):
 1. 0 \<le> max_stepsize n
[PROOF STEP]
by simp


[STATEMENT]
lemma max_stepsize_mono:
  assumes "j \<le> n"
  shows "max_stepsize j \<le> max_stepsize n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_stepsize j \<le> max_stepsize n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
j \<le> n

goal (1 subgoal):
 1. max_stepsize j \<le> max_stepsize n
[PROOF STEP]
by (auto intro!: Max_mono simp: max_stepsize_def)


[STATEMENT]
lemma min_stepsize_le_stepsize:
  assumes "j \<le> n"
  shows "min_stepsize n \<le> stepsize j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_stepsize n \<le> stepsize j
[PROOF STEP]
using grid assms
[PROOF STATE]
proof (prove)
using this:
t ?i \<le> t (Suc ?i)
j \<le> n

goal (1 subgoal):
 1. min_stepsize n \<le> stepsize j
[PROOF STEP]
by (auto simp add: min_stepsize_def)


[STATEMENT]
lemma (in grid) grid_interval_notempty: "t 0 \<le> t n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t 0 \<le> t n
[PROOF STEP]
using grid_ge_min[of n]
[PROOF STATE]
proof (prove)
using this:
t 0 \<le> t n

goal (1 subgoal):
 1. t 0 \<le> t n
[PROOF STEP]
.


[STATEMENT]
lemma consistentD:
  assumes "consistent x t T B p incr"
  assumes "h \<ge> 0" "t + h \<le> T"
  shows "dist (x (t + h)) (discrete_evolution incr (t + h) t (x t)) \<le> B * h ^ (p + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (x (t + h)) (discrete_evolution incr (t + h) t (x t)) \<le> B * h ^ (p + 1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
consistent x t T B p incr
0 \<le> h
t + h \<le> T

goal (1 subgoal):
 1. dist (x (t + h)) (discrete_evolution incr (t + h) t (x t)) \<le> B * h ^ (p + 1)
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h\<ge>0. t + h \<le> T \<longrightarrow> dist (x (t + h)) (discrete_evolution incr (t + h) t (x t)) \<le> B * h ^ (p + 1)
0 \<le> h
t + h \<le> T

goal (1 subgoal):
 1. dist (x (t + h)) (discrete_evolution incr (t + h) t (x t)) \<le> B * h ^ (p + 1)
[PROOF STEP]
by auto


[STATEMENT]
lemma consistentI[intro]:
  fixes x::"real\<Rightarrow>'a::real_normed_vector"
  assumes "\<And>h. h > 0 \<Longrightarrow> t + h \<le> T \<Longrightarrow>
    dist (x (t + h)) (discrete_evolution incr (t + h) t (x t)) \<le> B * h ^ (p + 1)"
  shows "consistent x t T B p incr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent x t T B p incr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?h; t + ?h \<le> T\<rbrakk> \<Longrightarrow> dist (x (t + ?h)) (discrete_evolution incr (t + ?h) t (x t)) \<le> B * ?h ^ (p + 1)

goal (1 subgoal):
 1. consistent x t T B p incr
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < ?h; t + ?h \<le> T\<rbrakk> \<Longrightarrow> dist (x (t + ?h)) (discrete_evolution incr (t + ?h) t (x t)) \<le> B * ?h ^ (p + 1)

goal (1 subgoal):
 1. \<forall>h\<ge>0. t + h \<le> T \<longrightarrow> dist (x (t + h)) (discrete_evolution incr (t + h) t (x t)) \<le> B * h ^ (p + 1)
[PROOF STEP]
by safe (case_tac "h = 0", auto simp: discrete_evolution_def)


[STATEMENT]
lemma consistent_imp_nonneg_constant:
  assumes "consistent x t T B p incr"
  assumes "t < T"
  shows "B \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> B
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
consistent x t T B p incr
t < T
[PROOF STEP]
have "T - t > 0"
[PROOF STATE]
proof (prove)
using this:
consistent x t T B p incr
t < T

goal (1 subgoal):
 1. 0 < T - t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < T - t

goal (1 subgoal):
 1. 0 \<le> B
[PROOF STEP]
have "0 \<le> dist (x T) (discrete_evolution incr T t (x t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> dist (x T) (discrete_evolution incr T t (x t))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> dist (x T) (discrete_evolution incr T t (x t))

goal (1 subgoal):
 1. 0 \<le> B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<le> dist (x T) (discrete_evolution incr T t (x t))

goal (1 subgoal):
 1. 0 \<le> B
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
consistent x t T B p incr
t < T
[PROOF STEP]
have "... \<le> B * (T - t) ^ (p + 1)"
[PROOF STATE]
proof (prove)
using this:
consistent x t T B p incr
t < T

goal (1 subgoal):
 1. dist (x T) (discrete_evolution incr T t (x t)) \<le> B * (T - t) ^ (p + 1)
[PROOF STEP]
unfolding consistent_def
[PROOF STATE]
proof (prove)
using this:
\<forall>h\<ge>0. t + h \<le> T \<longrightarrow> dist (x (t + h)) (discrete_evolution incr (t + h) t (x t)) \<le> B * h ^ (p + 1)
t < T

goal (1 subgoal):
 1. dist (x T) (discrete_evolution incr T t (x t)) \<le> B * (T - t) ^ (p + 1)
[PROOF STEP]
by (auto dest: spec[where x="T - t"])
[PROOF STATE]
proof (state)
this:
dist (x T) (discrete_evolution incr T t (x t)) \<le> B * (T - t) ^ (p + 1)

goal (1 subgoal):
 1. 0 \<le> B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 \<le> B * (T - t) ^ (p + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> B * (T - t) ^ (p + 1)

goal (1 subgoal):
 1. 0 \<le> B
[PROOF STEP]
using zero_less_power[OF \<open>T - t > 0\<close>, of "p+1"]
[PROOF STATE]
proof (prove)
using this:
0 \<le> B * (T - t) ^ (p + 1)
0 < (T - t) ^ (p + 1)

goal (1 subgoal):
 1. 0 \<le> B
[PROOF STEP]
by (simp add: zero_le_mult_iff)
[PROOF STATE]
proof (state)
this:
0 \<le> B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stepsize_inverse:
  assumes "L \<ge> 0" "h \<ge> 0" "B \<ge> 0" "r \<ge> 0" "p > 0" "T1 \<ge> T2" "T2 \<ge> 0"
  assumes max_step: "h \<le> root p (r * L / B / (exp (L * T1 + 1) - 1))"
  shows  "B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
assume "L = 0"
[PROOF STATE]
proof (state)
this:
L = 0

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
L = 0

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
using \<open>r \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
L = 0
0 \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
L = 0 \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
L = 0 \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
L = 0 \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
assume B_pos: "B > 0"
[PROOF STATE]
proof (state)
this:
0 < B

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
assume "L > 0"
[PROOF STATE]
proof (state)
this:
0 < L

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
from \<open>0 \<le> T2\<close> \<open>T1 \<ge> T2\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<le> T2
T2 \<le> T1
[PROOF STEP]
have "T1 \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> T2
T2 \<le> T1

goal (1 subgoal):
 1. 0 \<le> T1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> T1

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
hence eg: "(exp (L * T1 + 1) - 1) > 0"
[PROOF STATE]
proof (prove)
using this:
0 \<le> T1

goal (1 subgoal):
 1. 0 < exp (L * T1 + 1) - 1
[PROOF STEP]
using \<open>L > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> T1
0 < L

goal (1 subgoal):
 1. 0 < exp (L * T1 + 1) - 1
[PROOF STEP]
by (auto intro!: add_nonneg_pos)
[PROOF STATE]
proof (state)
this:
0 < exp (L * T1 + 1) - 1

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
have "B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le>
      B * (root p (r * L / B / (exp (L * T1 + 1) - 1)) ^ p
      * (exp (L * T2 + 1) - 1)) / L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> B * (root p (r * L / B / (exp (L * T1 + 1) - 1)) ^ p * (exp (L * T2 + 1) - 1)) / L
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 \<le> L
0 \<le> h
0 \<le> B
0 \<le> r
0 < p
T2 \<le> T1
0 \<le> T2
h \<le> root p (r * L / B / (exp (L * T1 + 1) - 1))

goal (1 subgoal):
 1. B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> B * (root p (r * L / B / (exp (L * T1 + 1) - 1)) ^ p * (exp (L * T2 + 1) - 1)) / L
[PROOF STEP]
by (auto simp add: ge_iff_diff_ge_0[symmetric] divide_simps
               intro!: mult_left_mono mult_right_mono power_mono)
[PROOF STATE]
proof (state)
this:
B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> B * (root p (r * L / B / (exp (L * T1 + 1) - 1)) ^ p * (exp (L * T2 + 1) - 1)) / L

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> B * (root p (r * L / B / (exp (L * T1 + 1) - 1)) ^ p * (exp (L * T2 + 1) - 1)) / L

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
have "root p (r * L / B / (exp (L * T1 + 1) - 1)) ^ p =
      (r * L / B / (exp (L * T1 + 1) - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. root p (r * L / B / (exp (L * T1 + 1) - 1)) ^ p = r * L / B / (exp (L * T1 + 1) - 1)
[PROOF STEP]
using assms B_pos \<open>T1 \<ge> 0\<close> \<open>L > 0\<close> \<open>B > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> L
0 \<le> h
0 \<le> B
0 \<le> r
0 < p
T2 \<le> T1
0 \<le> T2
h \<le> root p (r * L / B / (exp (L * T1 + 1) - 1))
0 < B
0 \<le> T1
0 < L
0 < B

goal (1 subgoal):
 1. root p (r * L / B / (exp (L * T1 + 1) - 1)) ^ p = r * L / B / (exp (L * T1 + 1) - 1)
[PROOF STEP]
by (subst real_root_pow_pos2[OF \<open>p > 0\<close>])
         (auto intro!: divide_nonneg_pos add_nonneg_pos mult_pos_pos)
[PROOF STATE]
proof (state)
this:
root p (r * L / B / (exp (L * T1 + 1) - 1)) ^ p = r * L / B / (exp (L * T1 + 1) - 1)

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> B * (r * L / B / (exp (L * T1 + 1) - 1) * (exp (L * T2 + 1) - 1)) / L
[PROOF STEP]
have "B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le>
      r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1))"
[PROOF STATE]
proof (prove)
using this:
B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> B * (r * L / B / (exp (L * T1 + 1) - 1) * (exp (L * T2 + 1) - 1)) / L

goal (1 subgoal):
 1. B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1))
[PROOF STEP]
using B_pos \<open>L > 0\<close> eg \<open>r \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> B * (r * L / B / (exp (L * T1 + 1) - 1) * (exp (L * T2 + 1) - 1)) / L
0 < B
0 < L
0 < exp (L * T1 + 1) - 1
0 \<le> r

goal (1 subgoal):
 1. B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1))
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1))

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1))

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
have "... \<le> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r
[PROOF STEP]
using \<open>T1 \<ge> T2\<close> \<open>0 \<le> T2\<close>
[PROOF STATE]
proof (prove)
using this:
T2 \<le> T1
0 \<le> T2

goal (1 subgoal):
 1. r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r
[PROOF STEP]
proof (cases "T1 = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>T2 \<le> T1; 0 \<le> T2; T1 = 0\<rbrakk> \<Longrightarrow> r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r
 2. \<lbrakk>T2 \<le> T1; 0 \<le> T2; T1 \<noteq> 0\<rbrakk> \<Longrightarrow> r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r
[PROOF STEP]
assume "T1 \<noteq> 0"
[PROOF STATE]
proof (state)
this:
T1 \<noteq> 0

goal (2 subgoals):
 1. \<lbrakk>T2 \<le> T1; 0 \<le> T2; T1 = 0\<rbrakk> \<Longrightarrow> r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r
 2. \<lbrakk>T2 \<le> T1; 0 \<le> T2; T1 \<noteq> 0\<rbrakk> \<Longrightarrow> r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r
[PROOF STEP]
with \<open>T1 \<ge> T2\<close> \<open>0 \<le> T2\<close>
[PROOF STATE]
proof (chain)
picking this:
T2 \<le> T1
0 \<le> T2
T1 \<noteq> 0
[PROOF STEP]
have "T1 > 0"
[PROOF STATE]
proof (prove)
using this:
T2 \<le> T1
0 \<le> T2
T1 \<noteq> 0

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

goal (2 subgoals):
 1. \<lbrakk>T2 \<le> T1; 0 \<le> T2; T1 = 0\<rbrakk> \<Longrightarrow> r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r
 2. \<lbrakk>T2 \<le> T1; 0 \<le> T2; T1 \<noteq> 0\<rbrakk> \<Longrightarrow> r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r
[PROOF STEP]
using \<open>L > 0\<close> \<open>0 \<le> T2\<close> \<open>T1 \<ge> 0\<close> add_0_left \<open>T1 > 0\<close> \<open>T1 \<ge> T2\<close>
[PROOF STATE]
proof (prove)
using this:
0 < L
0 \<le> T2
0 \<le> T1
(0::?'a) + ?a = ?a
0 < T1
T2 \<le> T1

goal (1 subgoal):
 1. r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r
[PROOF STEP]
by (intro mult_right_le_one_le \<open>r \<ge> 0\<close>)
           (subst pos_le_divide_eq pos_divide_le_eq, auto simp add: intro!: add_pos_pos)+
[PROOF STATE]
proof (state)
this:
r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r

goal (1 subgoal):
 1. \<lbrakk>T2 \<le> T1; 0 \<le> T2; T1 = 0\<rbrakk> \<Longrightarrow> r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
r * ((exp (L * T2 + 1) - 1) / (exp (L * T1 + 1) - 1)) \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> r
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
B * (h ^ p * (exp (L * T2 + 1) - 1)) / L \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < B; 0 < L\<rbrakk> \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < B; 0 < L\<rbrakk> \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 < B; 0 < L\<rbrakk> \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
assume "\<not>0<B"
[PROOF STATE]
proof (state)
this:
\<not> 0 < B

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
hence "B = 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < B

goal (1 subgoal):
 1. B = 0
[PROOF STEP]
using \<open>B \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 0 < B
0 \<le> B

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

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
hence ?thesis
[PROOF STATE]
proof (prove)
using this:
B = 0

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
using \<open>r \<ge> 0\<close>
[PROOF STATE]
proof (prove)
using this:
B = 0
0 \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> 0 < B \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
L = 0 \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
\<lbrakk>0 < B; 0 < L\<rbrakk> \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
\<not> 0 < B \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L = 0 \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
\<lbrakk>0 < B; 0 < L\<rbrakk> \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
\<not> 0 < B \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
L = 0 \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
\<lbrakk>0 < B; 0 < L\<rbrakk> \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
\<not> 0 < B \<Longrightarrow> B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
0 \<le> L
0 \<le> h
0 \<le> B
0 \<le> r
0 < p
T2 \<le> T1
0 \<le> T2
h \<le> root p (r * L / B / (exp (L * T1 + 1) - 1))

goal (1 subgoal):
 1. B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * T2 + 1) - 1) * h ^ p \<le> r

goal:
No subgoals!
[PROOF STEP]
qed