[STATEMENT]
lemma Domain_Rel_cases:
  assumes "(x0,x1) \<in> Domain Rel_OR"
  shows "(\<exists> w0. (x0,w0) \<in> Rel0 \<and> x1 \<in> valid_pub1) \<or> (\<exists> w1. (x1,w1) \<in> Rel1 \<and> x0 \<in> valid_pub0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>w0. (x0, w0) \<in> Rel0 \<and> x1 \<in> valid_pub1) \<or> (\<exists>w1. (x1, w1) \<in> Rel1 \<and> x0 \<in> valid_pub0)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x0, x1) \<in> Domain Rel_OR

goal (1 subgoal):
 1. (\<exists>w0. (x0, w0) \<in> Rel0 \<and> x1 \<in> valid_pub1) \<or> (\<exists>w1. (x1, w1) \<in> Rel1 \<and> x0 \<in> valid_pub0)
[PROOF STEP]
by (meson DomainE Rel_OR.cases)


[STATEMENT]
lemma set_spmf_lists_sample [simp]: "set_spmf (spmf_of_set (carrier L)) = (carrier L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_spmf (spmf_of_set (carrier L)) = carrier L
[PROOF STEP]
using finite_L
[PROOF STATE]
proof (prove)
using this:
finite (carrier L)

goal (1 subgoal):
 1. set_spmf (spmf_of_set (carrier L)) = carrier L
[PROOF STEP]
by simp


[STATEMENT]
lemma lossless_\<Sigma>_S: "lossless_spmf (\<Sigma>1.S x1 e1)" "lossless_spmf (\<Sigma>0.S x0 e0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (\<Sigma>1.S x1 e1) &&& lossless_spmf (\<Sigma>0.S x0 e0)
[PROOF STEP]
using lossless_S
[PROOF STATE]
proof (prove)
using this:
lossless_spmf (?S0.0 ?h0.0 ?e0.0)
lossless_spmf (?S1.0 ?h1.0 ?e1.0)

goal (1 subgoal):
 1. lossless_spmf (\<Sigma>1.S x1 e1) &&& lossless_spmf (\<Sigma>0.S x0 e0)
[PROOF STEP]
by fast +


[STATEMENT]
lemma lossless_init_OR: "lossless_spmf (init_OR (x0,x1) w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (init_OR (x0, x1) w)
[PROOF STEP]
by(cases w;simp add: lossless_\<Sigma>_S split_def lossless_init lossless_S finite_L carrier_L_not_empty)


[STATEMENT]
lemma  "check_OR (x0,x1) (a0,a1) s ((e0,z0), (e1,z1))
             = (s = e0 \<oplus> e1
                   \<and> e0 \<in> challenge_space \<and> e1 \<in> challenge_space
                      \<and> check0 x0 a0 e0 z0 \<and> check1 x1 a1 e1 z1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1) = (s = e0 \<oplus> e1 \<and> e0 \<in> challenge_space \<and> e1 \<in> challenge_space \<and> check0 x0 a0 e0 z0 \<and> check1 x1 a1 e1 z1)
[PROOF STEP]
by(simp add: check_OR_def)


[STATEMENT]
lemma \ss_OR_alt_def: "\ss_OR (x0,x1) ((a0,a1),s,(e0,z0),e1,z1) ((a0,a1),s',(e0',z0'),e1',z1') = do {
    if (e0 \<noteq> e0') then do {w0 :: 'witness0 \<leftarrow> \ss0 x0 (a0,e0,z0) (a0,e0',z0'); return_spmf (Inl w0)}
    else do {w1 :: 'witness1 \<leftarrow> \ss1 x1 (a1,e1,z1) (a1,e1',z1'); return_spmf (Inr w1)}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1') = (if e0 \<noteq> e0' then \ss0 x0 (a0, e0, z0) (a0, e0', z0') \<bind> (\<lambda>w0. return_spmf (Inl w0)) else \ss1 x1 (a1, e1, z1) (a1, e1', z1') \<bind> (\<lambda>w1. return_spmf (Inr w1)))
[PROOF STEP]
by(simp add: \ss_OR_def)


[STATEMENT]
lemma HVZK1:
  assumes "(x1,w1) \<in> Rel1"
  shows "\<forall> c \<in> challenge_space. \<Sigma>_OR.R (x0,x1) (Inr w1) c = \<Sigma>_OR.S (x0,x1) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>challenge_space. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>challenge_space. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> challenge_space \<Longrightarrow> \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> challenge_space \<Longrightarrow> \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
assume c: "c \<in> challenge_space"
[PROOF STATE]
proof (state)
this:
c \<in> challenge_space

goal (1 subgoal):
 1. \<And>c. c \<in> challenge_space \<Longrightarrow> \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
show "\<Sigma>_OR.R (x0,x1) (Inr w1) c = \<Sigma>_OR.S (x0,x1) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
have *: "x \<in> carrier L \<longrightarrow> c \<oplus> c \<oplus> x = x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier L \<longrightarrow> c \<oplus> c \<oplus> x = x
[PROOF STEP]
using c challenge_space_def
[PROOF STATE]
proof (prove)
using this:
c \<in> challenge_space
challenge_space = carrier L

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

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
have "\<Sigma>_OR.R (x0,x1) (Inr w1) c = do {
    (r1, ab1) \<leftarrow> init1 x1 w1;
    eb' \<leftarrow> spmf_of_set (carrier L);
    (ab0', eb0'', zb0') \<leftarrow> \<Sigma>0.S x0 eb';
    let ((r, eb', zb'),a) = ((r1, eb', zb0' ),  ab0' , ab1);
    let eb = c \<oplus> eb';
    zb1 \<leftarrow> response1 r w1 eb;
    let z = ((eb', zb') , (eb, zb1));
    return_spmf (a,c,z)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = 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 ((r, eb', zb'), a) = ((r1, eb', zb0'), ab0', ab1); eb = c \<oplus> eb' in response1 r w1 eb \<bind> (\<lambda>zb1. let z = ((eb', zb'), eb, zb1) in return_spmf (a, c, z)))))
[PROOF STEP]
supply [[simproc del: monad_normalisation]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = 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 ((r, eb', zb'), a) = ((r1, eb', zb0'), ab0', ab1); eb = c \<oplus> eb' in response1 r w1 eb \<bind> (\<lambda>zb1. let z = ((eb', zb'), eb, zb1) in return_spmf (a, c, z)))))
[PROOF STEP]
by(simp add: \<Sigma>_OR.R_def split_def Let_def)
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.R (x0, x1) (Inr w1) c = 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 ((r, eb', zb'), a) = ((r1, eb', zb0'), ab0', ab1); eb = c \<oplus> eb' in response1 r w1 eb \<bind> (\<lambda>zb1. let z = ((eb', zb'), eb, zb1) in return_spmf (a, c, z)))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.R (x0, x1) (Inr w1) c = 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 ((r, eb', zb'), a) = ((r1, eb', zb0'), ab0', ab1); eb = c \<oplus> eb' in response1 r w1 eb \<bind> (\<lambda>zb1. let z = ((eb', zb'), eb, zb1) in return_spmf (a, c, z)))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
have "... = do {
    eb' \<leftarrow> spmf_of_set (carrier L);
    (ab0', eb0'', zb0') \<leftarrow> \<Sigma>0.S x0 eb';
    let eb = c \<oplus> eb';
    (ab1, c', zb1) \<leftarrow> \<Sigma>1.R x1 w1 eb;
    let z = ((eb', zb0'), (eb, zb1));
    return_spmf ((ab0',ab1),c,z)}"
[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 ((r, eb', zb'), a) = ((r1, eb', zb0'), ab0', ab1); eb = c \<oplus> eb' in response1 r w1 eb \<bind> (\<lambda>zb1. let z = ((eb', zb'), eb, zb1) in return_spmf (a, c, z))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = c \<oplus> eb' in \<Sigma>1.R x1 w1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))
[PROOF STEP]
by(simp add: \<Sigma>1.R_def split_def Let_def)
[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 ((r, eb', zb'), a) = ((r1, eb', zb0'), ab0', ab1); eb = c \<oplus> eb' in response1 r w1 eb \<bind> (\<lambda>zb1. let z = ((eb', zb'), eb, zb1) in return_spmf (a, c, z))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = c \<oplus> eb' in \<Sigma>1.R x1 w1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[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 ((r, eb', zb'), a) = ((r1, eb', zb0'), ab0', ab1); eb = c \<oplus> eb' in response1 r w1 eb \<bind> (\<lambda>zb1. let z = ((eb', zb'), eb, zb1) in return_spmf (a, c, z))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = c \<oplus> eb' in \<Sigma>1.R x1 w1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
have "... = do {
    eb' \<leftarrow> spmf_of_set (carrier L);
    (ab0', eb0'', zb0') \<leftarrow> \<Sigma>0.S x0 eb';
    let eb = c \<oplus> eb';
    (ab1, c', zb1) \<leftarrow> \<Sigma>1.S x1 eb;
    let z = ((eb', zb0'), (eb, zb1));
    return_spmf ((ab0',ab1),c,z)}"
[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 = c \<oplus> eb' in \<Sigma>1.R x1 w1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = c \<oplus> eb' in \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
c \<in> challenge_space

goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = c \<oplus> eb' in \<Sigma>1.R x1 w1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = c \<oplus> eb' in \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))
[PROOF STEP]
by(simp add: split_def Let_def \<Sigma>_prot1 \<Sigma>1.HVZK_unfold1 assms challenge_space_def  cong: bind_spmf_cong_simp)
[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 = c \<oplus> eb' in \<Sigma>1.R x1 w1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = c \<oplus> eb' in \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[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 = c \<oplus> eb' in \<Sigma>1.R x1 w1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>0.S x0 eb' \<bind> (\<lambda>(ab0', eb0'', zb0'). let eb = c \<oplus> eb' in \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
have "... = do {
    eb \<leftarrow> map_spmf (\<lambda> eb'. c \<oplus> eb') (spmf_of_set (carrier L));
    (ab1, c', zb1) \<leftarrow> \<Sigma>1.S x1 eb;
    (ab0', eb0'', zb0') \<leftarrow> \<Sigma>0.S x0 (c \<oplus> eb);
    let z = ((c \<oplus> eb, zb0'), (eb, zb1));
    return_spmf ((ab0',ab1),c,z)}"
[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 = c \<oplus> eb' in \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = map_spmf ((\<oplus>) c) (spmf_of_set (carrier L)) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))
[PROOF STEP]
apply(simp add: bind_map_spmf o_def 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'). \<Sigma>1.S x1 (c \<oplus> eb') \<bind> (\<lambda>(ab1, c', zb1). return_spmf ((ab0', ab1), c, (eb', zb0'), c \<oplus> eb', zb1)))) = spmf_of_set (carrier L) \<bind> (\<lambda>x. \<Sigma>1.S x1 (c \<oplus> x) \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> c \<oplus> x) \<bind> (\<lambda>(ab0', eb0'', zb0'). return_spmf ((ab0', ab1), c, (c \<oplus> c \<oplus> x, zb0'), c \<oplus> x, zb1))))
[PROOF STEP]
by(simp add: * split_def cong: bind_spmf_cong_simp)
[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 = c \<oplus> eb' in \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = map_spmf ((\<oplus>) c) (spmf_of_set (carrier L)) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[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 = c \<oplus> eb' in \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). let z = ((eb', zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = map_spmf ((\<oplus>) c) (spmf_of_set (carrier L)) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
have "... = do {
    eb \<leftarrow> (spmf_of_set (carrier L));
    (ab1, c', zb1) \<leftarrow> \<Sigma>1.S x1 eb;
    (ab0', eb0'', zb0') \<leftarrow> \<Sigma>0.S x0 (c \<oplus> eb);
    let z = ((c \<oplus> eb, zb0'), (eb, zb1));
    return_spmf ((ab0',ab1),c,z)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf ((\<oplus>) c) (spmf_of_set (carrier L)) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))
[PROOF STEP]
using assms assms one_time_pad c challenge_space_def
[PROOF STATE]
proof (prove)
using this:
(x1, w1) \<in> Rel1
(x1, w1) \<in> Rel1
?x \<in> carrier L \<Longrightarrow> map_spmf ((\<oplus>) ?x) (spmf_of_set (carrier L)) = spmf_of_set (carrier L)
c \<in> challenge_space
challenge_space = carrier L

goal (1 subgoal):
 1. map_spmf ((\<oplus>) c) (spmf_of_set (carrier L)) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_spmf ((\<oplus>) c) (spmf_of_set (carrier L)) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_spmf ((\<oplus>) c) (spmf_of_set (carrier L)) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
have "... = do {
    eb \<leftarrow> (spmf_of_set (carrier L));
    (ab1, c', zb1) \<leftarrow> \<Sigma>1.S x1 eb;
    (ab0', eb0'', zb0') \<leftarrow> \<Sigma>0.S x0 (c \<oplus> eb);
    let z = ((eb0'', zb0'), (c', zb1));
    return_spmf ((ab0',ab1),c,z)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((eb0'', zb0'), c', zb1) in return_spmf ((ab0', ab1), c, z))))
[PROOF STEP]
by(simp add: \<Sigma>0.S_def \<Sigma>1.S_def bind_map_spmf o_def split_def)
[PROOF STATE]
proof (state)
this:
spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((eb0'', zb0'), c', zb1) in return_spmf ((ab0', ab1), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Sigma>_OR.R (x0, x1) (Inr w1) c = spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))
spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((eb0'', zb0'), c', zb1) in return_spmf ((ab0', ab1), c, z))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Sigma>_OR.R (x0, x1) (Inr w1) c = spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z))))
spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((c \<oplus> eb, zb0'), eb, zb1) in return_spmf ((ab0', ab1), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb. \<Sigma>1.S x1 eb \<bind> (\<lambda>(ab1, c', zb1). \<Sigma>0.S x0 (c \<oplus> eb) \<bind> (\<lambda>(ab0', eb0'', zb0'). let z = ((eb0'', zb0'), c', zb1) in return_spmf ((ab0', ab1), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
by(simp add: Let_def map_spmf_conv_bind_spmf \<Sigma>_OR.S_def split_def)
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.R (x0, x1) (Inr w1) c = \<Sigma>_OR.S (x0, x1) c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HVZK0:
  assumes "(x0,w0) \<in> Rel0"
  shows "\<forall> c \<in> challenge_space. \<Sigma>_OR.R (x0,x1) (Inl w0) c = \<Sigma>_OR.S (x0,x1) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c\<in>challenge_space. \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> challenge_space \<Longrightarrow> \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c. c \<in> challenge_space \<Longrightarrow> \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
assume c: "c \<in> challenge_space"
[PROOF STATE]
proof (state)
this:
c \<in> challenge_space

goal (1 subgoal):
 1. \<And>c. c \<in> challenge_space \<Longrightarrow> \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
show "\<Sigma>_OR.R (x0,x1) (Inl w0) c = \<Sigma>_OR.S (x0,x1) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
have "\<Sigma>_OR.R (x0,x1) (Inl w0) c = do {
    (r0,ab0) \<leftarrow> init0 x0 w0;
    eb' \<leftarrow> spmf_of_set (carrier L);
    (ab1', eb1'', zb1') \<leftarrow> \<Sigma>1.S x1 eb';
    let ((r, eb', zb'),a) = ((r0, eb', zb1'),  ab0,  ab1');
    let eb = c \<oplus> eb';
    zb0 \<leftarrow> response0 r w0 eb;
    let z = ((eb,zb0), (eb',zb'));
    return_spmf (a,c,z)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inl w0) c = 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 ((r, eb', zb'), a) = ((r0, eb', zb1'), ab0, ab1'); eb = c \<oplus> eb' in response0 r w0 eb \<bind> (\<lambda>zb0. let z = ((eb, zb0), eb', zb') in return_spmf (a, c, z)))))
[PROOF STEP]
by(simp add: \<Sigma>_OR.R_def split_def Let_def)
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.R (x0, x1) (Inl w0) c = 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 ((r, eb', zb'), a) = ((r0, eb', zb1'), ab0, ab1'); eb = c \<oplus> eb' in response0 r w0 eb \<bind> (\<lambda>zb0. let z = ((eb, zb0), eb', zb') in return_spmf (a, c, z)))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.R (x0, x1) (Inl w0) c = 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 ((r, eb', zb'), a) = ((r0, eb', zb1'), ab0, ab1'); eb = c \<oplus> eb' in response0 r w0 eb \<bind> (\<lambda>zb0. let z = ((eb, zb0), eb', zb') in return_spmf (a, c, z)))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
have "... = do {
    eb' \<leftarrow> (spmf_of_set (carrier L));
    (ab1', eb1'', zb1') \<leftarrow> \<Sigma>1.S x1 eb';
    let eb = c \<oplus> eb';
    (ab0, c', zb0) \<leftarrow> \<Sigma>0.R x0 w0 eb;
    let z = ((eb,zb0),  (eb',zb1'));
    return_spmf ((ab0,  ab1'),c,z)}"
[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 ((r, eb', zb'), a) = ((r0, eb', zb1'), ab0, ab1'); eb = c \<oplus> eb' in response0 r w0 eb \<bind> (\<lambda>zb0. let z = ((eb, zb0), eb', zb') in return_spmf (a, c, z))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.R x0 w0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z))))
[PROOF STEP]
apply(simp add: \<Sigma>0.R_def split_def Let_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 (c \<oplus> eb') \<bind> (\<lambda>zb0. return_spmf ((snd p, fst pa), c, (c \<oplus> eb', zb0), 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>y. response0 (fst y) w0 (c \<oplus> eb') \<bind> (\<lambda>ya. return_spmf ((snd y, fst p), c, (c \<oplus> eb', ya), 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 (c \<oplus> y) \<bind> (\<lambda>zb0. return_spmf ((snd p, fst pa), c, (c \<oplus> y, zb0), 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>y. response0 (fst y) w0 (c \<oplus> eb') \<bind> (\<lambda>ya. return_spmf ((snd y, fst p), c, (c \<oplus> eb', ya), 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 (c \<oplus> y) \<bind> (\<lambda>zb0. return_spmf ((snd p, fst ya), c, (c \<oplus> y, zb0), 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>y. response0 (fst y) w0 (c \<oplus> eb') \<bind> (\<lambda>ya. return_spmf ((snd y, fst p), c, (c \<oplus> eb', ya), 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 ((r, eb', zb'), a) = ((r0, eb', zb1'), ab0, ab1'); eb = c \<oplus> eb' in response0 r w0 eb \<bind> (\<lambda>zb0. let z = ((eb, zb0), eb', zb') in return_spmf (a, c, z))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.R x0 w0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[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 ((r, eb', zb'), a) = ((r0, eb', zb1'), ab0, ab1'); eb = c \<oplus> eb' in response0 r w0 eb \<bind> (\<lambda>zb0. let z = ((eb, zb0), eb', zb') in return_spmf (a, c, z))))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.R x0 w0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
have "... = do {
    eb' \<leftarrow> (spmf_of_set (carrier L));
    (ab1', eb1'', zb1') \<leftarrow> \<Sigma>1.S x1 eb';
    let eb = c \<oplus> eb';
    (ab0, c', zb0) \<leftarrow> \<Sigma>0.S x0 eb;
    let z = ((eb,zb0), (eb',zb1'));
    return_spmf ((ab0,  ab1'),c,z)}"
[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 = c \<oplus> eb' in \<Sigma>0.R x0 w0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.S x0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z))))
[PROOF STEP]
using c
[PROOF STATE]
proof (prove)
using this:
c \<in> challenge_space

goal (1 subgoal):
 1. spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.R x0 w0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.S x0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z))))
[PROOF STEP]
by(simp add: \<Sigma>_prot0 \<Sigma>0.HVZK_unfold1 assms challenge_space_def split_def Let_def cong: bind_spmf_cong_simp)
[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 = c \<oplus> eb' in \<Sigma>0.R x0 w0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.S x0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Sigma>_OR.R (x0, x1) (Inl w0) c = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.R x0 w0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z))))
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.R x0 w0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.S x0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Sigma>_OR.R (x0, x1) (Inl w0) c = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.R x0 w0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z))))
spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.R x0 w0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z)))) = spmf_of_set (carrier L) \<bind> (\<lambda>eb'. \<Sigma>1.S x1 eb' \<bind> (\<lambda>(ab1', eb1'', zb1'). let eb = c \<oplus> eb' in \<Sigma>0.S x0 eb \<bind> (\<lambda>(ab0, c', zb0). let z = ((eb, zb0), eb', zb1') in return_spmf ((ab0, ab1'), c, z))))

goal (1 subgoal):
 1. \<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c
[PROOF STEP]
by(simp add: \<Sigma>_OR.S_def \<Sigma>1.S_def \<Sigma>0.S_def Let_def o_def bind_map_spmf split_def map_spmf_conv_bind_spmf)
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Sigma>_OR.R (x0, x1) (Inl w0) c = \<Sigma>_OR.S (x0, x1) c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HVZK:
  shows "\<Sigma>_OR.HVZK"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma>_OR.HVZK
[PROOF STEP]
unfolding \<Sigma>_OR.HVZK_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>challenge_space. (\<forall>(h, w)\<in>Rel_OR. \<Sigma>_OR.R h w e = \<Sigma>_OR.S h e) \<and> (\<forall>h\<in>valid_pub_OR. \<forall>(a, z)\<in>set_spmf (S_OR h e). check_OR h a e z)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>e a b ba. \<lbrakk>e \<in> challenge_space; ((a, b), ba) \<in> Rel_OR\<rbrakk> \<Longrightarrow> \<Sigma>_OR.R (a, b) ba e = \<Sigma>_OR.S (a, b) e
 2. \<And>e a b aa ab bb ac bc x ad. \<lbrakk>e \<in> challenge_space; (a, b) \<in> valid_pub_OR; x \<in> carrier L; (ad, ac, bc) \<in> set_spmf (\<Sigma>1.S b x); (aa, ab, bb) \<in> set_spmf (\<Sigma>0.S a (e \<oplus> x))\<rbrakk> \<Longrightarrow> check_OR (a, b) (aa, ad) e ((ab, bb), ac, bc)
[PROOF STEP]
subgoal for e a b w
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>e \<in> challenge_space; ((a, b), w) \<in> Rel_OR\<rbrakk> \<Longrightarrow> \<Sigma>_OR.R (a, b) w e = \<Sigma>_OR.S (a, b) e
[PROOF STEP]
apply(cases w)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>e \<in> challenge_space; ((a, b), w) \<in> Rel_OR; w = Inl aa\<rbrakk> \<Longrightarrow> \<Sigma>_OR.R (a, b) w e = \<Sigma>_OR.S (a, b) e
 2. \<And>ba. \<lbrakk>e \<in> challenge_space; ((a, b), w) \<in> Rel_OR; w = Inr ba\<rbrakk> \<Longrightarrow> \<Sigma>_OR.R (a, b) w e = \<Sigma>_OR.S (a, b) e
[PROOF STEP]
using HVZK0 HVZK1
[PROOF STATE]
proof (prove)
using this:
(?x0.0, ?w0.0) \<in> Rel0 \<Longrightarrow> \<forall>c\<in>challenge_space. \<Sigma>_OR.R (?x0.0, ?x1.0) (Inl ?w0.0) c = \<Sigma>_OR.S (?x0.0, ?x1.0) c
(?x1.0, ?w1.0) \<in> Rel1 \<Longrightarrow> \<forall>c\<in>challenge_space. \<Sigma>_OR.R (?x0.0, ?x1.0) (Inr ?w1.0) c = \<Sigma>_OR.S (?x0.0, ?x1.0) c

goal (2 subgoals):
 1. \<And>aa. \<lbrakk>e \<in> challenge_space; ((a, b), w) \<in> Rel_OR; w = Inl aa\<rbrakk> \<Longrightarrow> \<Sigma>_OR.R (a, b) w e = \<Sigma>_OR.S (a, b) e
 2. \<And>ba. \<lbrakk>e \<in> challenge_space; ((a, b), w) \<in> Rel_OR; w = Inr ba\<rbrakk> \<Longrightarrow> \<Sigma>_OR.R (a, b) w e = \<Sigma>_OR.S (a, b) e
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e a b aa ab bb ac bc x ad. \<lbrakk>e \<in> challenge_space; (a, b) \<in> valid_pub_OR; x \<in> carrier L; (ad, ac, bc) \<in> set_spmf (\<Sigma>1.S b x); (aa, ab, bb) \<in> set_spmf (\<Sigma>0.S a (e \<oplus> x))\<rbrakk> \<Longrightarrow> check_OR (a, b) (aa, ad) e ((ab, bb), ac, bc)
[PROOF STEP]
apply(auto simp add: valid_pub_OR_def \<Sigma>_OR.S_def bind_map_spmf o_def check_OR_def image_def \<Sigma>0.S_def \<Sigma>1.S_def split_def challenge_space_def local.xor_ac(1))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>e a b x ae ba af bd. \<lbrakk>e \<in> carrier L; x \<in> carrier L; (ae, ba) \<in> set_spmf (S1_raw b x); (af, bd) \<in> set_spmf (S0_raw a (e \<oplus> x)); a \<in> valid_pub0; b \<in> valid_pub1\<rbrakk> \<Longrightarrow> check0 a af (e \<oplus> x) bd
 2. \<And>e a b x ae ba af bd. \<lbrakk>e \<in> carrier L; x \<in> carrier L; (ae, ba) \<in> set_spmf (S1_raw b x); (af, bd) \<in> set_spmf (S0_raw a (e \<oplus> x)); a \<in> valid_pub0; b \<in> valid_pub1\<rbrakk> \<Longrightarrow> check1 b ae x ba
[PROOF STEP]
using \<Sigma>0.HVZK_unfold2 \<Sigma>_prot0 challenge_space_def
[PROOF STATE]
proof (prove)
using this:
\<Sigma>0.\<Sigma>_protocol \<Longrightarrow> \<forall>h e out. e \<in> carrier L \<longrightarrow> h \<in> valid_pub0 \<longrightarrow> out \<in> set_spmf (S0_raw h e) \<longrightarrow> check0 h (fst out) e (snd out)
\<Sigma>0.\<Sigma>_protocol
challenge_space = carrier L

goal (2 subgoals):
 1. \<And>e a b x ae ba af bd. \<lbrakk>e \<in> carrier L; x \<in> carrier L; (ae, ba) \<in> set_spmf (S1_raw b x); (af, bd) \<in> set_spmf (S0_raw a (e \<oplus> x)); a \<in> valid_pub0; b \<in> valid_pub1\<rbrakk> \<Longrightarrow> check0 a af (e \<oplus> x) bd
 2. \<And>e a b x ae ba af bd. \<lbrakk>e \<in> carrier L; x \<in> carrier L; (ae, ba) \<in> set_spmf (S1_raw b x); (af, bd) \<in> set_spmf (S0_raw a (e \<oplus> x)); a \<in> valid_pub0; b \<in> valid_pub1\<rbrakk> \<Longrightarrow> check1 b ae x ba
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e a b x ae ba af bd. \<lbrakk>e \<in> carrier L; x \<in> carrier L; (ae, ba) \<in> set_spmf (S1_raw b x); (af, bd) \<in> set_spmf (S0_raw a (e \<oplus> x)); a \<in> valid_pub0; b \<in> valid_pub1\<rbrakk> \<Longrightarrow> check1 b ae x ba
[PROOF STEP]
using \<Sigma>1.HVZK_unfold2 \<Sigma>_prot1 challenge_space_def
[PROOF STATE]
proof (prove)
using this:
\<Sigma>1.\<Sigma>_protocol \<Longrightarrow> \<forall>h e out. e \<in> carrier L \<longrightarrow> h \<in> valid_pub1 \<longrightarrow> out \<in> set_spmf (S1_raw h e) \<longrightarrow> check1 h (fst out) e (snd out)
\<Sigma>1.\<Sigma>_protocol
challenge_space = carrier L

goal (1 subgoal):
 1. \<And>e a b x ae ba af bd. \<lbrakk>e \<in> carrier L; x \<in> carrier L; (ae, ba) \<in> set_spmf (S1_raw b x); (af, bd) \<in> set_spmf (S0_raw a (e \<oplus> x)); a \<in> valid_pub0; b \<in> valid_pub1\<rbrakk> \<Longrightarrow> check1 b ae x ba
[PROOF STEP]
by force


[STATEMENT]
lemma assumes "(x0,x1) \<in> Domain Rel_OR"
  shows "(\<exists> w0. (x0,w0) \<in> Rel0) \<or> (\<exists> w1. (x1,w1) \<in> Rel1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>w0. (x0, w0) \<in> Rel0) \<or> (\<exists>w1. (x1, w1) \<in> Rel1)
[PROOF STEP]
using assms Rel_OR.simps
[PROOF STATE]
proof (prove)
using this:
(x0, x1) \<in> Domain Rel_OR
(((?a1.0, ?a2.0), ?a3.0) \<in> Rel_OR) = ((\<exists>x0 w0 x1. ?a1.0 = x0 \<and> ?a2.0 = x1 \<and> ?a3.0 = Inl w0 \<and> (x0, w0) \<in> Rel0 \<and> x1 \<in> valid_pub1) \<or> (\<exists>x1 w1 x0. ?a1.0 = x0 \<and> ?a2.0 = x1 \<and> ?a3.0 = Inr w1 \<and> (x1, w1) \<in> Rel1 \<and> x0 \<in> valid_pub0))

goal (1 subgoal):
 1. (\<exists>w0. (x0, w0) \<in> Rel0) \<or> (\<exists>w1. (x1, w1) \<in> Rel1)
[PROOF STEP]
by blast


[STATEMENT]
lemma ss:
  assumes valid_pub_OR: "(x0,x1) \<in> valid_pub_OR"
    and check: "check_OR (x0,x1) (a0,a1) s ((e0,z0), (e1,z1))"
    and check': "check_OR (x0,x1) (a0,a1) s' ((e0',z0'), (e1',z1'))"
    and "s \<noteq> s'"
    and challenge_space: "s \<in> challenge_space" "s' \<in> challenge_space"
  shows "lossless_spmf (\ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1')) \<and>
           (\<forall>w'\<in>set_spmf (\ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1')). ((x0,x1), w') \<in> Rel_OR)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have e_or: "e0 \<noteq> e0' \<or> e1 \<noteq> e1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e0 \<noteq> e0' \<or> e1 \<noteq> e1'
[PROOF STEP]
using assms check_OR_def
[PROOF STATE]
proof (prove)
using this:
(x0, x1) \<in> valid_pub_OR
check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1)
check_OR (x0, x1) (a0, a1) s' ((e0', z0'), e1', z1')
s \<noteq> s'
s \<in> challenge_space
s' \<in> challenge_space
check_OR ?X ?A ?s ?Z = (?s = fst (fst ?Z) \<oplus> fst (snd ?Z) \<and> fst (fst ?Z) \<in> challenge_space \<and> fst (snd ?Z) \<in> challenge_space \<and> check0 (fst ?X) (fst ?A) (fst (fst ?Z)) (snd (fst ?Z)) \<and> check1 (snd ?X) (snd ?A) (fst (snd ?Z)) (snd (snd ?Z)))

goal (1 subgoal):
 1. e0 \<noteq> e0' \<or> e1 \<noteq> e1'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e0 \<noteq> e0' \<or> e1 \<noteq> e1'

goal (1 subgoal):
 1. lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
proof(cases "e0 \<noteq> e0'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
e0 \<noteq> e0'

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e0 \<noteq> e0'

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have 2: "x0 \<in> valid_pub0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x0 \<in> valid_pub0
[PROOF STEP]
using valid_pub_OR valid_pub_OR_def
[PROOF STATE]
proof (prove)
using this:
(x0, x1) \<in> valid_pub_OR
valid_pub_OR = {(x0, x1). x0 \<in> valid_pub0 \<and> x1 \<in> valid_pub1}

goal (1 subgoal):
 1. x0 \<in> valid_pub0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x0 \<in> valid_pub0

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x0 \<in> valid_pub0

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have 3: "check0 x0 a0 e0 z0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check0 x0 a0 e0 z0
[PROOF STEP]
using assms check_OR_def
[PROOF STATE]
proof (prove)
using this:
(x0, x1) \<in> valid_pub_OR
check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1)
check_OR (x0, x1) (a0, a1) s' ((e0', z0'), e1', z1')
s \<noteq> s'
s \<in> challenge_space
s' \<in> challenge_space
check_OR ?X ?A ?s ?Z = (?s = fst (fst ?Z) \<oplus> fst (snd ?Z) \<and> fst (fst ?Z) \<in> challenge_space \<and> fst (snd ?Z) \<in> challenge_space \<and> check0 (fst ?X) (fst ?A) (fst (fst ?Z)) (snd (fst ?Z)) \<and> check1 (snd ?X) (snd ?A) (fst (snd ?Z)) (snd (snd ?Z)))

goal (1 subgoal):
 1. check0 x0 a0 e0 z0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
check0 x0 a0 e0 z0

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
check0 x0 a0 e0 z0

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have 4: "check0 x0 a0 e0' z0'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check0 x0 a0 e0' z0'
[PROOF STEP]
using assms check_OR_def
[PROOF STATE]
proof (prove)
using this:
(x0, x1) \<in> valid_pub_OR
check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1)
check_OR (x0, x1) (a0, a1) s' ((e0', z0'), e1', z1')
s \<noteq> s'
s \<in> challenge_space
s' \<in> challenge_space
check_OR ?X ?A ?s ?Z = (?s = fst (fst ?Z) \<oplus> fst (snd ?Z) \<and> fst (fst ?Z) \<in> challenge_space \<and> fst (snd ?Z) \<in> challenge_space \<and> check0 (fst ?X) (fst ?A) (fst (fst ?Z)) (snd (fst ?Z)) \<and> check1 (snd ?X) (snd ?A) (fst (snd ?Z)) (snd (snd ?Z)))

goal (1 subgoal):
 1. check0 x0 a0 e0' z0'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
check0 x0 a0 e0' z0'

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
check0 x0 a0 e0' z0'

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have e: "e0 \<in> carrier L" "e0' \<in> carrier L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e0 \<in> carrier L &&& e0' \<in> carrier L
[PROOF STEP]
using challenge_space_def check check' check_OR_def
[PROOF STATE]
proof (prove)
using this:
challenge_space = carrier L
check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1)
check_OR (x0, x1) (a0, a1) s' ((e0', z0'), e1', z1')
check_OR ?X ?A ?s ?Z = (?s = fst (fst ?Z) \<oplus> fst (snd ?Z) \<and> fst (fst ?Z) \<in> challenge_space \<and> fst (snd ?Z) \<in> challenge_space \<and> check0 (fst ?X) (fst ?A) (fst (fst ?Z)) (snd (fst ?Z)) \<and> check1 (snd ?X) (snd ?A) (fst (snd ?Z)) (snd (snd ?Z)))

goal (1 subgoal):
 1. e0 \<in> carrier L &&& e0' \<in> carrier L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e0 \<in> carrier L
e0' \<in> carrier L

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e0 \<noteq> e0'
x0 \<in> valid_pub0
check0 x0 a0 e0 z0
check0 x0 a0 e0' z0'
e0 \<in> carrier L
e0' \<in> carrier L
[PROOF STEP]
have "(\<forall>w'\<in>set_spmf (\ss0 x0 (a0,e0,z0) (a0,e0',z0')). (x0, w') \<in> Rel0)"
[PROOF STATE]
proof (prove)
using this:
e0 \<noteq> e0'
x0 \<in> valid_pub0
check0 x0 a0 e0 z0
check0 x0 a0 e0' z0'
e0 \<in> carrier L
e0' \<in> carrier L

goal (1 subgoal):
 1. \<forall>w'\<in>set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')). (x0, w') \<in> Rel0
[PROOF STEP]
using True \<Sigma>0.\<Sigma>_protocol_def \<Sigma>0.special_soundness_def \<Sigma>_prot0 challenge_space assms
[PROOF STATE]
proof (prove)
using this:
e0 \<noteq> e0'
x0 \<in> valid_pub0
check0 x0 a0 e0 z0
check0 x0 a0 e0' z0'
e0 \<in> carrier L
e0' \<in> carrier L
e0 \<noteq> e0'
\<Sigma>0.\<Sigma>_protocol \<equiv> \<Sigma>0.completeness \<and> \<Sigma>0.special_soundness \<and> \<Sigma>0.HVZK
\<Sigma>0.special_soundness \<equiv> \<forall>h e e' a z z'. h \<in> valid_pub0 \<longrightarrow> e \<in> carrier L \<longrightarrow> e' \<in> carrier L \<longrightarrow> e \<noteq> e' \<longrightarrow> check0 h a e z \<longrightarrow> check0 h a e' z' \<longrightarrow> lossless_spmf (\ss0 h (a, e, z) (a, e', z')) \<and> (\<forall>w'\<in>set_spmf (\ss0 h (a, e, z) (a, e', z')). (h, w') \<in> Rel0)
\<Sigma>0.\<Sigma>_protocol
s \<in> challenge_space
s' \<in> challenge_space
(x0, x1) \<in> valid_pub_OR
check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1)
check_OR (x0, x1) (a0, a1) s' ((e0', z0'), e1', z1')
s \<noteq> s'
s \<in> challenge_space
s' \<in> challenge_space

goal (1 subgoal):
 1. \<forall>w'\<in>set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')). (x0, w') \<in> Rel0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>w'\<in>set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')). (x0, w') \<in> Rel0

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w'\<in>set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')). (x0, w') \<in> Rel0

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have  "lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))
[PROOF STEP]
using 2 3 4 \ss_OR_def True \<Sigma>_prot0  \<Sigma>0.\<Sigma>_protocol_def \<Sigma>0.special_soundness_def challenge_space_def e
[PROOF STATE]
proof (prove)
using this:
x0 \<in> valid_pub0
check0 x0 a0 e0 z0
check0 x0 a0 e0' z0'
\ss_OR ?X ?C1.0 ?C2.0 = (if fst (fst (snd (snd ?C1.0))) \<noteq> fst (fst (snd (snd ?C2.0))) then \ss0 (fst ?X) (fst (fst ?C1.0), fst (fst (snd (snd ?C1.0))), snd (fst (snd (snd ?C1.0)))) (fst (fst ?C2.0), fst (fst (snd (snd ?C2.0))), snd (fst (snd (snd ?C2.0)))) \<bind> (\<lambda>w0. return_spmf (Inl w0)) else \ss1 (snd ?X) (snd (fst ?C1.0), fst (snd (snd (snd ?C1.0))), snd (snd (snd (snd ?C1.0)))) (snd (fst ?C2.0), fst (snd (snd (snd ?C2.0))), snd (snd (snd (snd ?C2.0)))) \<bind> (\<lambda>w1. return_spmf (Inr w1)))
e0 \<noteq> e0'
\<Sigma>0.\<Sigma>_protocol
\<Sigma>0.\<Sigma>_protocol \<equiv> \<Sigma>0.completeness \<and> \<Sigma>0.special_soundness \<and> \<Sigma>0.HVZK
\<Sigma>0.special_soundness \<equiv> \<forall>h e e' a z z'. h \<in> valid_pub0 \<longrightarrow> e \<in> carrier L \<longrightarrow> e' \<in> carrier L \<longrightarrow> e \<noteq> e' \<longrightarrow> check0 h a e z \<longrightarrow> check0 h a e' z' \<longrightarrow> lossless_spmf (\ss0 h (a, e, z) (a, e', z')) \<and> (\<forall>w'\<in>set_spmf (\ss0 h (a, e, z) (a, e', z')). (h, w') \<in> Rel0)
challenge_space = carrier L
e0 \<in> carrier L
e0' \<in> carrier L

goal (1 subgoal):
 1. lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>w'\<in>set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')). (x0, w') \<in> Rel0
lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))
[PROOF STEP]
have "\<forall> w' \<in> set_spmf (\ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1')). ((x0,x1),  w') \<in> Rel_OR"
[PROOF STATE]
proof (prove)
using this:
\<forall>w'\<in>set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')). (x0, w') \<in> Rel0
lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))

goal (1 subgoal):
 1. \<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR
[PROOF STEP]
apply(auto simp only: \ss_OR_alt_def True)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>w'. \<lbrakk>\<forall>w'\<in>set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')). (x0, w') \<in> Rel0; lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')); w' \<in> set_spmf (if \<not> False then \ss0 x0 (a0, e0, z0) (a0, e0', z0') \<bind> (\<lambda>w0. return_spmf (Inl w0)) else \ss1 x1 (a1, e1, z1) (a1, e1', z1') \<bind> (\<lambda>w1. return_spmf (Inr w1)))\<rbrakk> \<Longrightarrow> ((x0, x1), w') \<in> Rel_OR
[PROOF STEP]
apply(auto simp add: o_def \ss_OR_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>w'\<in>set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')). (x0, w') \<in> Rel0; lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')); x \<in> set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))\<rbrakk> \<Longrightarrow> x1 \<in> valid_pub1
[PROOF STEP]
using assms valid_pub_OR_def
[PROOF STATE]
proof (prove)
using this:
(x0, x1) \<in> valid_pub_OR
check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1)
check_OR (x0, x1) (a0, a1) s' ((e0', z0'), e1', z1')
s \<noteq> s'
s \<in> challenge_space
s' \<in> challenge_space
valid_pub_OR = {(x0, x1). x0 \<in> valid_pub0 \<and> x1 \<in> valid_pub1}

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>w'\<in>set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')). (x0, w') \<in> Rel0; lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0')); x \<in> set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))\<rbrakk> \<Longrightarrow> x1 \<in> valid_pub1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have "lossless_spmf (\ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1'))
[PROOF STEP]
apply(simp add: \ss_OR_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (e0 \<noteq> e0' \<longrightarrow> lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))) \<and> (e0 = e0' \<longrightarrow> lossless_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')))
[PROOF STEP]
using 2 3 4 True \<Sigma>_prot0  \<Sigma>0.\<Sigma>_protocol_def \<Sigma>0.special_soundness_def challenge_space e
[PROOF STATE]
proof (prove)
using this:
x0 \<in> valid_pub0
check0 x0 a0 e0 z0
check0 x0 a0 e0' z0'
e0 \<noteq> e0'
\<Sigma>0.\<Sigma>_protocol
\<Sigma>0.\<Sigma>_protocol \<equiv> \<Sigma>0.completeness \<and> \<Sigma>0.special_soundness \<and> \<Sigma>0.HVZK
\<Sigma>0.special_soundness \<equiv> \<forall>h e e' a z z'. h \<in> valid_pub0 \<longrightarrow> e \<in> carrier L \<longrightarrow> e' \<in> carrier L \<longrightarrow> e \<noteq> e' \<longrightarrow> check0 h a e z \<longrightarrow> check0 h a e' z' \<longrightarrow> lossless_spmf (\ss0 h (a, e, z) (a, e', z')) \<and> (\<forall>w'\<in>set_spmf (\ss0 h (a, e, z) (a, e', z')). (h, w') \<in> Rel0)
s \<in> challenge_space
s' \<in> challenge_space
e0 \<in> carrier L
e0' \<in> carrier L

goal (1 subgoal):
 1. (e0 \<noteq> e0' \<longrightarrow> lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))) \<and> (e0 = e0' \<longrightarrow> lossless_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1'))

goal (2 subgoals):
 1. e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
 2. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR
lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR
lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1'))

goal (1 subgoal):
 1. lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> e0 \<noteq> e0'

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
hence e1_neq_e1': "e1 \<noteq> e1'"
[PROOF STATE]
proof (prove)
using this:
\<not> e0 \<noteq> e0'

goal (1 subgoal):
 1. e1 \<noteq> e1'
[PROOF STEP]
using e_or
[PROOF STATE]
proof (prove)
using this:
\<not> e0 \<noteq> e0'
e0 \<noteq> e0' \<or> e1 \<noteq> e1'

goal (1 subgoal):
 1. e1 \<noteq> e1'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
e1 \<noteq> e1'

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e1 \<noteq> e1'

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have 2: "x1 \<in> valid_pub1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<in> valid_pub1
[PROOF STEP]
using valid_pub_OR valid_pub_OR_def
[PROOF STATE]
proof (prove)
using this:
(x0, x1) \<in> valid_pub_OR
valid_pub_OR = {(x0, x1). x0 \<in> valid_pub0 \<and> x1 \<in> valid_pub1}

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

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x1 \<in> valid_pub1

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have 3: "check1 x1 a1 e1 z1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check1 x1 a1 e1 z1
[PROOF STEP]
using assms check_OR_def
[PROOF STATE]
proof (prove)
using this:
(x0, x1) \<in> valid_pub_OR
check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1)
check_OR (x0, x1) (a0, a1) s' ((e0', z0'), e1', z1')
s \<noteq> s'
s \<in> challenge_space
s' \<in> challenge_space
check_OR ?X ?A ?s ?Z = (?s = fst (fst ?Z) \<oplus> fst (snd ?Z) \<and> fst (fst ?Z) \<in> challenge_space \<and> fst (snd ?Z) \<in> challenge_space \<and> check0 (fst ?X) (fst ?A) (fst (fst ?Z)) (snd (fst ?Z)) \<and> check1 (snd ?X) (snd ?A) (fst (snd ?Z)) (snd (snd ?Z)))

goal (1 subgoal):
 1. check1 x1 a1 e1 z1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
check1 x1 a1 e1 z1

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
check1 x1 a1 e1 z1

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have 4: "check1 x1 a1 e1' z1'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check1 x1 a1 e1' z1'
[PROOF STEP]
using assms check_OR_def
[PROOF STATE]
proof (prove)
using this:
(x0, x1) \<in> valid_pub_OR
check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1)
check_OR (x0, x1) (a0, a1) s' ((e0', z0'), e1', z1')
s \<noteq> s'
s \<in> challenge_space
s' \<in> challenge_space
check_OR ?X ?A ?s ?Z = (?s = fst (fst ?Z) \<oplus> fst (snd ?Z) \<and> fst (fst ?Z) \<in> challenge_space \<and> fst (snd ?Z) \<in> challenge_space \<and> check0 (fst ?X) (fst ?A) (fst (fst ?Z)) (snd (fst ?Z)) \<and> check1 (snd ?X) (snd ?A) (fst (snd ?Z)) (snd (snd ?Z)))

goal (1 subgoal):
 1. check1 x1 a1 e1' z1'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
check1 x1 a1 e1' z1'

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
check1 x1 a1 e1' z1'

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have e: "e1 \<in> carrier L" "e1' \<in> carrier L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e1 \<in> carrier L &&& e1' \<in> carrier L
[PROOF STEP]
using challenge_space_def check check' check_OR_def
[PROOF STATE]
proof (prove)
using this:
challenge_space = carrier L
check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1)
check_OR (x0, x1) (a0, a1) s' ((e0', z0'), e1', z1')
check_OR ?X ?A ?s ?Z = (?s = fst (fst ?Z) \<oplus> fst (snd ?Z) \<and> fst (fst ?Z) \<in> challenge_space \<and> fst (snd ?Z) \<in> challenge_space \<and> check0 (fst ?X) (fst ?A) (fst (fst ?Z)) (snd (fst ?Z)) \<and> check1 (snd ?X) (snd ?A) (fst (snd ?Z)) (snd (snd ?Z)))

goal (1 subgoal):
 1. e1 \<in> carrier L &&& e1' \<in> carrier L
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
e1 \<in> carrier L
e1' \<in> carrier L

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
e1 \<noteq> e1'
x1 \<in> valid_pub1
check1 x1 a1 e1 z1
check1 x1 a1 e1' z1'
e1 \<in> carrier L
e1' \<in> carrier L
[PROOF STEP]
have "(\<forall>w'\<in>set_spmf (\ss1 x1 (a1,e1,z1) (a1,e1',z1')). (x1,w') \<in> Rel1)"
[PROOF STATE]
proof (prove)
using this:
e1 \<noteq> e1'
x1 \<in> valid_pub1
check1 x1 a1 e1 z1
check1 x1 a1 e1' z1'
e1 \<in> carrier L
e1' \<in> carrier L

goal (1 subgoal):
 1. \<forall>w'\<in>set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')). (x1, w') \<in> Rel1
[PROOF STEP]
using False \<Sigma>1.\<Sigma>_protocol_def \<Sigma>1.special_soundness_def \<Sigma>_prot1 e1_neq_e1' challenge_space
[PROOF STATE]
proof (prove)
using this:
e1 \<noteq> e1'
x1 \<in> valid_pub1
check1 x1 a1 e1 z1
check1 x1 a1 e1' z1'
e1 \<in> carrier L
e1' \<in> carrier L
\<not> e0 \<noteq> e0'
\<Sigma>1.\<Sigma>_protocol \<equiv> \<Sigma>1.completeness \<and> \<Sigma>1.special_soundness \<and> \<Sigma>1.HVZK
\<Sigma>1.special_soundness \<equiv> \<forall>h e e' a z z'. h \<in> valid_pub1 \<longrightarrow> e \<in> carrier L \<longrightarrow> e' \<in> carrier L \<longrightarrow> e \<noteq> e' \<longrightarrow> check1 h a e z \<longrightarrow> check1 h a e' z' \<longrightarrow> lossless_spmf (\ss1 h (a, e, z) (a, e', z')) \<and> (\<forall>w'\<in>set_spmf (\ss1 h (a, e, z) (a, e', z')). (h, w') \<in> Rel1)
\<Sigma>1.\<Sigma>_protocol
e1 \<noteq> e1'
s \<in> challenge_space
s' \<in> challenge_space

goal (1 subgoal):
 1. \<forall>w'\<in>set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')). (x1, w') \<in> Rel1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>w'\<in>set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')). (x1, w') \<in> Rel1

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
hence "\<forall>w' \<in> set_spmf (\ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1')). ((x0,x1), w') \<in> Rel_OR"
[PROOF STATE]
proof (prove)
using this:
\<forall>w'\<in>set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')). (x1, w') \<in> Rel1

goal (1 subgoal):
 1. \<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR
[PROOF STEP]
apply(auto simp add: o_def \ss_OR_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>w'\<in>set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')). (x1, w') \<in> Rel1; e0 \<noteq> e0'; x \<in> set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))\<rbrakk> \<Longrightarrow> (x0, x) \<in> Rel0
 2. \<And>x. \<lbrakk>\<forall>w'\<in>set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')). (x1, w') \<in> Rel1; e0 \<noteq> e0'; x \<in> set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))\<rbrakk> \<Longrightarrow> x1 \<in> valid_pub1
 3. \<And>x. \<lbrakk>\<forall>w'\<in>set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')). (x1, w') \<in> Rel1; e0 = e0'; x \<in> set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1'))\<rbrakk> \<Longrightarrow> x0 \<in> valid_pub0
[PROOF STEP]
using False assms \<Sigma>1.L_def assms valid_pub_OR_def
[PROOF STATE]
proof (prove)
using this:
\<not> e0 \<noteq> e0'
(x0, x1) \<in> valid_pub_OR
check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1)
check_OR (x0, x1) (a0, a1) s' ((e0', z0'), e1', z1')
s \<noteq> s'
s \<in> challenge_space
s' \<in> challenge_space
\<Sigma>1.L \<equiv> {x. \<exists>w. (x, w) \<in> Rel1}
(x0, x1) \<in> valid_pub_OR
check_OR (x0, x1) (a0, a1) s ((e0, z0), e1, z1)
check_OR (x0, x1) (a0, a1) s' ((e0', z0'), e1', z1')
s \<noteq> s'
s \<in> challenge_space
s' \<in> challenge_space
valid_pub_OR = {(x0, x1). x0 \<in> valid_pub0 \<and> x1 \<in> valid_pub1}

goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>w'\<in>set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')). (x1, w') \<in> Rel1; e0 \<noteq> e0'; x \<in> set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))\<rbrakk> \<Longrightarrow> (x0, x) \<in> Rel0
 2. \<And>x. \<lbrakk>\<forall>w'\<in>set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')). (x1, w') \<in> Rel1; e0 \<noteq> e0'; x \<in> set_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))\<rbrakk> \<Longrightarrow> x1 \<in> valid_pub1
 3. \<And>x. \<lbrakk>\<forall>w'\<in>set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')). (x1, w') \<in> Rel1; e0 = e0'; x \<in> set_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1'))\<rbrakk> \<Longrightarrow> x0 \<in> valid_pub0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
have "lossless_spmf (\ss_OR (x0,x1) ((a0,a1),s,(e0,z0), e1,z1) ((a0,a1),s',(e0',z0'), e1',z1'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1'))
[PROOF STEP]
apply(simp add: \ss_OR_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (e0 \<noteq> e0' \<longrightarrow> lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))) \<and> (e0 = e0' \<longrightarrow> lossless_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')))
[PROOF STEP]
using 2 3 4 \<Sigma>_prot1 \<Sigma>1.\<Sigma>_protocol_def \<Sigma>1.special_soundness_def False e1_neq_e1' challenge_space e
[PROOF STATE]
proof (prove)
using this:
x1 \<in> valid_pub1
check1 x1 a1 e1 z1
check1 x1 a1 e1' z1'
\<Sigma>1.\<Sigma>_protocol
\<Sigma>1.\<Sigma>_protocol \<equiv> \<Sigma>1.completeness \<and> \<Sigma>1.special_soundness \<and> \<Sigma>1.HVZK
\<Sigma>1.special_soundness \<equiv> \<forall>h e e' a z z'. h \<in> valid_pub1 \<longrightarrow> e \<in> carrier L \<longrightarrow> e' \<in> carrier L \<longrightarrow> e \<noteq> e' \<longrightarrow> check1 h a e z \<longrightarrow> check1 h a e' z' \<longrightarrow> lossless_spmf (\ss1 h (a, e, z) (a, e', z')) \<and> (\<forall>w'\<in>set_spmf (\ss1 h (a, e, z) (a, e', z')). (h, w') \<in> Rel1)
\<not> e0 \<noteq> e0'
e1 \<noteq> e1'
s \<in> challenge_space
s' \<in> challenge_space
e1 \<in> carrier L
e1' \<in> carrier L

goal (1 subgoal):
 1. (e0 \<noteq> e0' \<longrightarrow> lossless_spmf (\ss0 x0 (a0, e0, z0) (a0, e0', z0'))) \<and> (e0 = e0' \<longrightarrow> lossless_spmf (\ss1 x1 (a1, e1, z1) (a1, e1', z1')))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1'))

goal (1 subgoal):
 1. \<not> e0 \<noteq> e0' \<Longrightarrow> lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR
lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1'))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR
lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1'))

goal (1 subgoal):
 1. lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lossless_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (x0, x1) ((a0, a1), s, (e0, z0), e1, z1) ((a0, a1), s', (e0', z0'), e1', z1')). ((x0, x1), w') \<in> Rel_OR)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma special_soundness:
  shows "\<Sigma>_OR.special_soundness"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sigma>_OR.special_soundness
[PROOF STEP]
unfolding \<Sigma>_OR.special_soundness_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h e e' a z z'. h \<in> valid_pub_OR \<longrightarrow> e \<in> challenge_space \<longrightarrow> e' \<in> challenge_space \<longrightarrow> e \<noteq> e' \<longrightarrow> check_OR h a e z \<longrightarrow> check_OR h a e' z' \<longrightarrow> lossless_spmf (\ss_OR h (a, e, z) (a, e', z')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR h (a, e, z) (a, e', z')). (h, w') \<in> Rel_OR)
[PROOF STEP]
using ss prod.collapse
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?x0.0, ?x1.0) \<in> valid_pub_OR; check_OR (?x0.0, ?x1.0) (?a0.0, ?a1.0) ?s ((?e0.0, ?z0.0), ?e1.0, ?z1.0); check_OR (?x0.0, ?x1.0) (?a0.0, ?a1.0) ?s' ((?e0', ?z0'), ?e1', ?z1'); ?s \<noteq> ?s'; ?s \<in> challenge_space; ?s' \<in> challenge_space\<rbrakk> \<Longrightarrow> lossless_spmf (\ss_OR (?x0.0, ?x1.0) ((?a0.0, ?a1.0), ?s, (?e0.0, ?z0.0), ?e1.0, ?z1.0) ((?a0.0, ?a1.0), ?s', (?e0', ?z0'), ?e1', ?z1')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR (?x0.0, ?x1.0) ((?a0.0, ?a1.0), ?s, (?e0.0, ?z0.0), ?e1.0, ?z1.0) ((?a0.0, ?a1.0), ?s', (?e0', ?z0'), ?e1', ?z1')). ((?x0.0, ?x1.0), w') \<in> Rel_OR)
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. \<forall>h e e' a z z'. h \<in> valid_pub_OR \<longrightarrow> e \<in> challenge_space \<longrightarrow> e' \<in> challenge_space \<longrightarrow> e \<noteq> e' \<longrightarrow> check_OR h a e z \<longrightarrow> check_OR h a e' z' \<longrightarrow> lossless_spmf (\ss_OR h (a, e, z) (a, e', z')) \<and> (\<forall>w'\<in>set_spmf (\ss_OR h (a, e, z) (a, e', z')). (h, w') \<in> Rel_OR)
[PROOF STEP]
by fastforce