[STATEMENT]
lemma hvzk_sim_inverse_rewrite:
  assumes h: "h =  \<^bold>g [^] (x1 :: nat) \<otimes> g' [^] (x2 :: nat)"
  shows "\<^bold>g [^] (((z1::nat) + order \<G> * c * x1 - c * x1) mod (order \<G>))
            \<otimes> g' [^] (((z2::nat) + order \<G> * c * x2 - c * x2) mod (order \<G>))
                = (\<^bold>g [^] z1 \<otimes> g' [^] z2) \<otimes> (inv h [^] c)"
(is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have in_carrier1: "(g' [^] x2) [^] c \<in> carrier \<G>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g' [^] x2) [^] c \<in> carrier \<G>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(g' [^] x2) [^] c \<in> carrier \<G>

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have in_carrier2: "(\<^bold>g [^] x1) [^] c \<in> carrier \<G>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<^bold>g [^] x1) [^] c \<in> carrier \<G>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<^bold>g [^] x1) [^] c \<in> carrier \<G>

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have pow_distrib1: "order \<G> * c * x1 - c * x1 = (order \<G> - 1) * c * x1"
    and pow_distrib2: "order \<G> * c * x2 - c * x2 = (order \<G> - 1) * c * x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order \<G> * c * x1 - c * x1 = (order \<G> - 1) * c * x1 &&& order \<G> * c * x2 - c * x2 = (order \<G> - 1) * c * x2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h = \<^bold>g [^] x1 \<otimes> g' [^] x2

goal (1 subgoal):
 1. order \<G> * c * x1 - c * x1 = (order \<G> - 1) * c * x1 &&& order \<G> * c * x2 - c * x2 = (order \<G> - 1) * c * x2
[PROOF STEP]
by (simp add: diff_mult_distrib)+
[PROOF STATE]
proof (state)
this:
order \<G> * c * x1 - c * x1 = (order \<G> - 1) * c * x1
order \<G> * c * x2 - c * x2 = (order \<G> - 1) * c * x2

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have "?lhs = \<^bold>g [^] (z1 + order \<G> * c * x1 - c * x1) \<otimes> g' [^] (z2 + order \<G> * c  * x2 - c * x2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] (z1 + order \<G> * c * x1 - c * x1) \<otimes> g' [^] (z2 + order \<G> * c * x2 - c * x2)
[PROOF STEP]
by (simp add: pow_carrier_mod)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] (z1 + order \<G> * c * x1 - c * x1) \<otimes> g' [^] (z2 + order \<G> * c * x2 - c * x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] (z1 + order \<G> * c * x1 - c * x1) \<otimes> g' [^] (z2 + order \<G> * c * x2 - c * x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have "... = \<^bold>g [^] (z1 + (order \<G> * c * x1 - c * x1)) \<otimes> g' [^] (z2 + (order \<G> * c * x2 - c * x2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] (z1 + order \<G> * c * x1 - c * x1) \<otimes> g' [^] (z2 + order \<G> * c * x2 - c * x2) = \<^bold>g [^] (z1 + (order \<G> * c * x1 - c * x1)) \<otimes> g' [^] (z2 + (order \<G> * c * x2 - c * x2))
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
h = \<^bold>g [^] x1 \<otimes> g' [^] x2

goal (1 subgoal):
 1. \<^bold>g [^] (z1 + order \<G> * c * x1 - c * x1) \<otimes> g' [^] (z2 + order \<G> * c * x2 - c * x2) = \<^bold>g [^] (z1 + (order \<G> * c * x1 - c * x1)) \<otimes> g' [^] (z2 + (order \<G> * c * x2 - c * x2))
[PROOF STEP]
by (smt Nat.add_diff_assoc diff_zero le_simps(1) nat_0_less_mult_iff neq0_conv pow_distrib1 pow_distrib2 prime_gt_1_nat prime_order zero_less_diff)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (z1 + order \<G> * c * x1 - c * x1) \<otimes> g' [^] (z2 + order \<G> * c * x2 - c * x2) = \<^bold>g [^] (z1 + (order \<G> * c * x1 - c * x1)) \<otimes> g' [^] (z2 + (order \<G> * c * x2 - c * x2))

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (z1 + order \<G> * c * x1 - c * x1) \<otimes> g' [^] (z2 + order \<G> * c * x2 - c * x2) = \<^bold>g [^] (z1 + (order \<G> * c * x1 - c * x1)) \<otimes> g' [^] (z2 + (order \<G> * c * x2 - c * x2))

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have "... =  \<^bold>g [^] z1 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] z2 \<otimes> g' [^] (order \<G> * c * x2 - c * x2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] (z1 + (order \<G> * c * x1 - c * x1)) \<otimes> g' [^] (z2 + (order \<G> * c * x2 - c * x2)) = \<^bold>g [^] z1 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] z2 \<otimes> g' [^] (order \<G> * c * x2 - c * x2)
[PROOF STEP]
using nat_pow_mult
[PROOF STATE]
proof (prove)
using this:
?x \<in> carrier \<G> \<Longrightarrow> ?x [^] ?n \<otimes> ?x [^] ?m = ?x [^] (?n + ?m)

goal (1 subgoal):
 1. \<^bold>g [^] (z1 + (order \<G> * c * x1 - c * x1)) \<otimes> g' [^] (z2 + (order \<G> * c * x2 - c * x2)) = \<^bold>g [^] z1 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] z2 \<otimes> g' [^] (order \<G> * c * x2 - c * x2)
[PROOF STEP]
by (simp add: m_assoc)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (z1 + (order \<G> * c * x1 - c * x1)) \<otimes> g' [^] (z2 + (order \<G> * c * x2 - c * x2)) = \<^bold>g [^] z1 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] z2 \<otimes> g' [^] (order \<G> * c * x2 - c * x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (z1 + (order \<G> * c * x1 - c * x1)) \<otimes> g' [^] (z2 + (order \<G> * c * x2 - c * x2)) = \<^bold>g [^] z1 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] z2 \<otimes> g' [^] (order \<G> * c * x2 - c * x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have "... = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] (order \<G> * c * x2 - c * x2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] z2 \<otimes> g' [^] (order \<G> * c * x2 - c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] (order \<G> * c * x2 - c * x2)
[PROOF STEP]
by (smt add.commute g'_def generator_closed m_assoc nat_pow_closed nat_pow_mult nat_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] z2 \<otimes> g' [^] (order \<G> * c * x2 - c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] (order \<G> * c * x2 - c * x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] z2 \<otimes> g' [^] (order \<G> * c * x2 - c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] (order \<G> * c * x2 - c * x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have "... = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] ((order \<G> - 1) * c * x1) \<otimes> g' [^] ((order \<G> - 1) * c * x2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] (order \<G> * c * x2 - c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] ((order \<G> - 1) * c * x1) \<otimes> g' [^] ((order \<G> - 1) * c * x2)
[PROOF STEP]
using pow_distrib1 pow_distrib2
[PROOF STATE]
proof (prove)
using this:
order \<G> * c * x1 - c * x1 = (order \<G> - 1) * c * x1
order \<G> * c * x2 - c * x2 = (order \<G> - 1) * c * x2

goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] (order \<G> * c * x2 - c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] ((order \<G> - 1) * c * x1) \<otimes> g' [^] ((order \<G> - 1) * c * x2)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] (order \<G> * c * x2 - c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] ((order \<G> - 1) * c * x1) \<otimes> g' [^] ((order \<G> - 1) * c * x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] (order \<G> * c * x1 - c * x1) \<otimes> g' [^] (order \<G> * c * x2 - c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] ((order \<G> - 1) * c * x1) \<otimes> g' [^] ((order \<G> - 1) * c * x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have "... = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (\<^bold>g [^] (order \<G> - 1)) [^] (c * x1) \<otimes> (g' [^] ((order \<G> - 1))) [^] (c * x2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] ((order \<G> - 1) * c * x1) \<otimes> g' [^] ((order \<G> - 1) * c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (\<^bold>g [^] (order \<G> - 1)) [^] (c * x1) \<otimes> (g' [^] (order \<G> - 1)) [^] (c * x2)
[PROOF STEP]
by (simp add: more_arith_simps(11) nat_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] ((order \<G> - 1) * c * x1) \<otimes> g' [^] ((order \<G> - 1) * c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (\<^bold>g [^] (order \<G> - 1)) [^] (c * x1) \<otimes> (g' [^] (order \<G> - 1)) [^] (c * x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> \<^bold>g [^] ((order \<G> - 1) * c * x1) \<otimes> g' [^] ((order \<G> - 1) * c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (\<^bold>g [^] (order \<G> - 1)) [^] (c * x1) \<otimes> (g' [^] (order \<G> - 1)) [^] (c * x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have "... = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (inv (\<^bold>g [^] c)) [^] x1 \<otimes> (inv (g' [^] c)) [^] x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (\<^bold>g [^] (order \<G> - 1)) [^] (c * x1) \<otimes> (g' [^] (order \<G> - 1)) [^] (c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (\<^bold>g [^] c) [^] x1 \<otimes> inv (g' [^] c) [^] x2
[PROOF STEP]
using assms neg_power_inverse  inverse_pow_pow nat_pow_pow prime_gt_1_nat prime_order
[PROOF STATE]
proof (prove)
using this:
h = \<^bold>g [^] x1 \<otimes> g' [^] x2
\<lbrakk>?g \<in> carrier \<G>; ?x < order \<G>\<rbrakk> \<Longrightarrow> ?g [^] (order \<G> - ?x) = inv (?g [^] ?x)
?a \<in> carrier \<G> \<Longrightarrow> inv (?a [^] ?r) = inv ?a [^] ?r
?x \<in> carrier \<G> \<Longrightarrow> (?x [^] ?n) [^] ?m = ?x [^] (?n * ?m)
prime ?p \<Longrightarrow> 1 < ?p
prime (order \<G>)

goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (\<^bold>g [^] (order \<G> - 1)) [^] (c * x1) \<otimes> (g' [^] (order \<G> - 1)) [^] (c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (\<^bold>g [^] c) [^] x1 \<otimes> inv (g' [^] c) [^] x2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (\<^bold>g [^] (order \<G> - 1)) [^] (c * x1) \<otimes> (g' [^] (order \<G> - 1)) [^] (c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (\<^bold>g [^] c) [^] x1 \<otimes> inv (g' [^] c) [^] x2

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (\<^bold>g [^] (order \<G> - 1)) [^] (c * x1) \<otimes> (g' [^] (order \<G> - 1)) [^] (c * x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (\<^bold>g [^] c) [^] x1 \<otimes> inv (g' [^] c) [^] x2

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have "... = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (inv ((\<^bold>g [^] c) [^] x1)) \<otimes> (inv ((g' [^] c) [^] x2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (\<^bold>g [^] c) [^] x1 \<otimes> inv (g' [^] c) [^] x2 = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] c) [^] x1) \<otimes> inv ((g' [^] c) [^] x2)
[PROOF STEP]
by (simp add: inverse_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (\<^bold>g [^] c) [^] x1 \<otimes> inv (g' [^] c) [^] x2 = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] c) [^] x1) \<otimes> inv ((g' [^] c) [^] x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (\<^bold>g [^] c) [^] x1 \<otimes> inv (g' [^] c) [^] x2 = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] c) [^] x1) \<otimes> inv ((g' [^] c) [^] x2)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have "... = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> ((inv ((\<^bold>g [^] x1) [^] c)) \<otimes> (inv ((g' [^] x2) [^] c)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] c) [^] x1) \<otimes> inv ((g' [^] c) [^] x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (inv ((\<^bold>g [^] x1) [^] c) \<otimes> inv ((g' [^] x2) [^] c))
[PROOF STEP]
by (simp add: mult.commute cyclic_group_assoc nat_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] c) [^] x1) \<otimes> inv ((g' [^] c) [^] x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (inv ((\<^bold>g [^] x1) [^] c) \<otimes> inv ((g' [^] x2) [^] c))

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] c) [^] x1) \<otimes> inv ((g' [^] c) [^] x2) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (inv ((\<^bold>g [^] x1) [^] c) \<otimes> inv ((g' [^] x2) [^] c))

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have "... = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (inv ((\<^bold>g [^] x1) [^] c) \<otimes> inv ((g' [^] x2) [^] c)) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c)
[PROOF STEP]
using inverse_split in_carrier2 in_carrier1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<in> carrier \<G>; ?b \<in> carrier \<G>\<rbrakk> \<Longrightarrow> inv (?a \<otimes> ?b) = inv ?a \<otimes> inv ?b
(\<^bold>g [^] x1) [^] c \<in> carrier \<G>
(g' [^] x2) [^] c \<in> carrier \<G>

goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (inv ((\<^bold>g [^] x1) [^] c) \<otimes> inv ((g' [^] x2) [^] c)) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (inv ((\<^bold>g [^] x1) [^] c) \<otimes> inv ((g' [^] x2) [^] c)) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> (inv ((\<^bold>g [^] x1) [^] c) \<otimes> inv ((g' [^] x2) [^] c)) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
have "... = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (h [^] c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (h [^] c)
[PROOF STEP]
using h  cyclic_group_commute monoid_comm_monoidI
[PROOF STATE]
proof (prove)
using this:
h = \<^bold>g [^] x1 \<otimes> g' [^] x2
\<lbrakk>?a \<in> carrier \<G>; ?b \<in> carrier \<G>\<rbrakk> \<Longrightarrow> ?a \<otimes> ?b = ?b \<otimes> ?a
(\<And>x y. \<lbrakk>x \<in> carrier \<G>; y \<in> carrier \<G>\<rbrakk> \<Longrightarrow> x \<otimes> y = y \<otimes> x) \<Longrightarrow> Group.comm_monoid \<G>

goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (h [^] c)
[PROOF STEP]
by (simp add: pow_mult_distrib)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (h [^] c)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c)
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (h [^] c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c)
\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv ((\<^bold>g [^] x1) [^] c \<otimes> (g' [^] x2) [^] c) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv (h [^] c)

goal (1 subgoal):
 1. \<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c
[PROOF STEP]
by (simp add: h inverse_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>) = \<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hv_zk:
  assumes "h =  \<^bold>g [^] x1 \<otimes> g' [^] x2"
  shows "\<Sigma>_protocols_base.R h (x1,x2) c = \<Sigma>_protocols_base.S h c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
have "\<Sigma>_protocols_base.R h (x1,x2) c = do {
    r1 \<leftarrow> sample_uniform (order \<G>);
    r2 \<leftarrow> sample_uniform (order \<G>);
    let z1 = (r1 + c * x1) mod (order \<G>);
    let z2 = (r2 + c * x2) mod (order \<G>);
    return_spmf ( \<^bold>g [^] r1 \<otimes> g' [^] r2 ,c,(z1,z2))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = sample_uniform (order \<G>) \<bind> (\<lambda>r1. sample_uniform (order \<G>) \<bind> (\<lambda>r2. let z1 = (r1 + c * x1) mod order \<G>; z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] r1 \<otimes> g' [^] r2, c, z1, z2)))
[PROOF STEP]
by(simp add: \<Sigma>_protocols_base.R_def R2_def; simp add: add.commute init_def split_def response_def)
[PROOF STATE]
proof (state)
this:
local.\<Sigma>_protocols_base.R h (x1, x2) c = sample_uniform (order \<G>) \<bind> (\<lambda>r1. sample_uniform (order \<G>) \<bind> (\<lambda>r2. let z1 = (r1 + c * x1) mod order \<G>; z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] r1 \<otimes> g' [^] r2, c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.\<Sigma>_protocols_base.R h (x1, x2) c = sample_uniform (order \<G>) \<bind> (\<lambda>r1. sample_uniform (order \<G>) \<bind> (\<lambda>r2. let z1 = (r1 + c * x1) mod order \<G>; z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] r1 \<otimes> g' [^] r2, c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
have "... = do {
    r2 \<leftarrow> sample_uniform (order \<G>);
    z1 \<leftarrow> map_spmf (\<lambda> r1. (r1 + c * x1) mod (order \<G>)) (sample_uniform (order \<G>));
    let z2 = (r2 + c * x2) mod (order \<G>);
    return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod (order \<G>)) \<otimes> g' [^] r2 ,c,(z1,z2))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform (order \<G>) \<bind> (\<lambda>r1. sample_uniform (order \<G>) \<bind> (\<lambda>r2. let z1 = (r1 + c * x1) mod order \<G>; z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] r1 \<otimes> g' [^] r2, c, z1, z2))) = sample_uniform (order \<G>) \<bind> (\<lambda>r2. map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. let z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] r2, c, z1, z2)))
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def hvzk_z1_r1_tuple_rewrite assms cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
sample_uniform (order \<G>) \<bind> (\<lambda>r1. sample_uniform (order \<G>) \<bind> (\<lambda>r2. let z1 = (r1 + c * x1) mod order \<G>; z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] r1 \<otimes> g' [^] r2, c, z1, z2))) = sample_uniform (order \<G>) \<bind> (\<lambda>r2. map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. let z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] r2, c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform (order \<G>) \<bind> (\<lambda>r1. sample_uniform (order \<G>) \<bind> (\<lambda>r2. let z1 = (r1 + c * x1) mod order \<G>; z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] r1 \<otimes> g' [^] r2, c, z1, z2))) = sample_uniform (order \<G>) \<bind> (\<lambda>r2. map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. let z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] r2, c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
have "... = do {
    z1 \<leftarrow> map_spmf (\<lambda> r1. (r1 + c * x1) mod (order \<G>)) (sample_uniform (order \<G>));
    z2 \<leftarrow> map_spmf (\<lambda> r2. (r2 + c * x2) mod (order \<G>)) (sample_uniform (order \<G>));
    return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod (order \<G>)) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod (order \<G>)) ,c,(z1,z2))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform (order \<G>) \<bind> (\<lambda>r2. map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. let z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] r2, c, z1, z2))) = map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (r2 + c * x2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2)))
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def hvzk_z2_r2_tuple_rewrite cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
sample_uniform (order \<G>) \<bind> (\<lambda>r2. map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. let z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] r2, c, z1, z2))) = map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (r2 + c * x2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform (order \<G>) \<bind> (\<lambda>r2. map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. let z2 = (r2 + c * x2) mod order \<G> in return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] r2, c, z1, z2))) = map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (r2 + c * x2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
have "... = do {
    z1 \<leftarrow> map_spmf (\<lambda> r1. (c * x1 + r1) mod (order \<G>)) (sample_uniform (order \<G>));
    z2 \<leftarrow> map_spmf (\<lambda> r2. (c * x2 + r2) mod (order \<G>)) (sample_uniform (order \<G>));
    return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod (order \<G>)) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod (order \<G>)) ,c,(z1,z2))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (r2 + c * x2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2))) = map_spmf (\<lambda>r1. (c * x1 + r1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (c * x2 + r2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2)))
[PROOF STEP]
by(simp add: add.commute)
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (r2 + c * x2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2))) = map_spmf (\<lambda>r1. (c * x1 + r1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (c * x2 + r2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>r1. (r1 + c * x1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (r2 + c * x2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2))) = map_spmf (\<lambda>r1. (c * x1 + r1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (c * x2 + r2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
have "... = do {
    z1 \<leftarrow> (sample_uniform (order \<G>));
    z2 \<leftarrow> (sample_uniform (order \<G>));
    return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod (order \<G>)) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod (order \<G>)) ,c,(z1,z2))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_spmf (\<lambda>r1. (c * x1 + r1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (c * x2 + r2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2))) = sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2)))
[PROOF STEP]
by(simp add: samp_uni_plus_one_time_pad)
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>r1. (c * x1 + r1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (c * x2 + r2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2))) = sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_spmf (\<lambda>r1. (c * x1 + r1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z1. map_spmf (\<lambda>r2. (c * x2 + r2) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2))) = sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
have "... = do {
    z1 \<leftarrow> (sample_uniform (order \<G>));
    z2 \<leftarrow> (sample_uniform (order \<G>));
    return_spmf ((\<^bold>g [^] z1 \<otimes> g' [^] z2) \<otimes> (inv h [^] c) ,c,(z1,z2))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2))) = sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c, c, z1, z2)))
[PROOF STEP]
by(simp add: hvzk_sim_inverse_rewrite assms cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2))) = sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c, c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.\<Sigma>_protocols_base.R h (x1, x2) c = sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2)))
sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2))) = sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c, c, z1, z2)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.\<Sigma>_protocols_base.R h (x1, x2) c = sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2)))
sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] ((z1 + order \<G> * c * x1 - c * x1) mod order \<G>) \<otimes> g' [^] ((z2 + order \<G> * c * x2 - c * x2) mod order \<G>), c, z1, z2))) = sample_uniform (order \<G>) \<bind> (\<lambda>z1. sample_uniform (order \<G>) \<bind> (\<lambda>z2. return_spmf (\<^bold>g [^] z1 \<otimes> g' [^] z2 \<otimes> inv h [^] c, c, z1, z2)))

goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c
[PROOF STEP]
by(simp add: \<Sigma>_protocols_base.S_def S2_def bind_map_spmf map_spmf_conv_bind_spmf)
[PROOF STATE]
proof (state)
this:
local.\<Sigma>_protocols_base.R h (x1, x2) c = local.\<Sigma>_protocols_base.S h c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HVZK:
  shows "\<Sigma>_protocols_base.HVZK"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.HVZK
[PROOF STEP]
unfolding \<Sigma>_protocols_base.HVZK_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e\<in>challenge_space. (\<forall>(h, w)\<in>R. local.\<Sigma>_protocols_base.R h w e = local.\<Sigma>_protocols_base.S h e) \<and> (\<forall>h\<in>valid_pub. \<forall>(a, z)\<in>set_spmf (S2 h e). check h a e z)
[PROOF STEP]
apply(auto simp add: R_def challenge_space_def hv_zk S2_def check_def valid_pub_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e h aa b. \<lbrakk>e < order \<G>; h \<in> carrier \<G>; b < order \<G>; aa < order \<G>\<rbrakk> \<Longrightarrow> \<^bold>g [^] aa \<otimes> g' [^] b = \<^bold>g [^] aa \<otimes> g' [^] b \<otimes> inv h [^] e \<otimes> h [^] e
[PROOF STEP]
by (metis (no_types, lifting) cyclic_group_commute g'_in_carrier generator_closed inv_closed inv_solve_left inverse_pow_pow m_closed nat_pow_closed)


[STATEMENT]
lemma ss_rewrite:
  assumes "h \<in> carrier \<G>"
    and "a \<in> carrier \<G>"
    and "e < order \<G>"
    and "\<^bold>g [^] z1 \<otimes> g' [^] z1' = a \<otimes> h [^] e"
    and "e' < e"
    and "\<^bold>g [^] z2 \<otimes> g' [^] z2' = a \<otimes> h [^] e' "
  shows "h = \<^bold>g [^] ((int z1 - int z2) * fst (bezw (e - e') (order \<G>)) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * fst (bezw (e - e') (order \<G>)) mod int (order \<G>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
have gcd: "gcd (e - e') (order \<G>) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (e - e') (order \<G>) = 1
[PROOF STEP]
using prime_field assms prime_order
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime ?q; ?a < ?q; ?a \<noteq> 0\<rbrakk> \<Longrightarrow> coprime ?a ?q
h \<in> carrier \<G>
a \<in> carrier \<G>
e < order \<G>
\<^bold>g [^] z1 \<otimes> g' [^] z1' = a \<otimes> h [^] e
e' < e
\<^bold>g [^] z2 \<otimes> g' [^] z2' = a \<otimes> h [^] e'
prime (order \<G>)

goal (1 subgoal):
 1. gcd (e - e') (order \<G>) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gcd (e - e') (order \<G>) = 1

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
have "\<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e) = a
[PROOF STEP]
by (simp add: inv_solve_right' assms)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e) = a

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e) = a

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
have "\<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = a
[PROOF STEP]
by (simp add: assms inv_solve_right')
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = a

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e) = a
\<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = a
[PROOF STEP]
have "\<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = \<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e) = a
\<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = a

goal (1 subgoal):
 1. \<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = \<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e)
[PROOF STEP]
using g'_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e) = a
\<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = a
g' = \<^bold>g [^] x

goal (1 subgoal):
 1. \<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = \<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e)
[PROOF STEP]
by (simp add: nat_pow_pow)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = \<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e)

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = \<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e)

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
obtain t :: nat where t: "h = \<^bold>g [^] t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. h = \<^bold>g [^] t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms generatorE
[PROOF STATE]
proof (prove)
using this:
h \<in> carrier \<G>
a \<in> carrier \<G>
e < order \<G>
\<^bold>g [^] z1 \<otimes> g' [^] z1' = a \<otimes> h [^] e
e' < e
\<^bold>g [^] z2 \<otimes> g' [^] z2' = a \<otimes> h [^] e'
\<lbrakk>?x \<in> carrier \<G>; \<And>n. ?x = \<^bold>g [^] n \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>t. h = \<^bold>g [^] t \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
h = \<^bold>g [^] t

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = \<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e)
h = \<^bold>g [^] t
[PROOF STEP]
have "\<^bold>g [^] z2 \<otimes> \<^bold>g [^] (x * z2') \<otimes> \<^bold>g [^] (t * e) = \<^bold>g [^] z1 \<otimes> \<^bold>g [^] (x * z1') \<otimes> (\<^bold>g [^] (t * e'))"
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = \<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e)
h = \<^bold>g [^] t

goal (1 subgoal):
 1. \<^bold>g [^] z2 \<otimes> \<^bold>g [^] (x * z2') \<otimes> \<^bold>g [^] (t * e) = \<^bold>g [^] z1 \<otimes> \<^bold>g [^] (x * z1') \<otimes> \<^bold>g [^] (t * e')
[PROOF STEP]
using assms(2) assms(4) cyclic_group_commute m_assoc g'_def nat_pow_pow
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] z2 \<otimes> g' [^] z2' \<otimes> inv (h [^] e') = \<^bold>g [^] z1 \<otimes> g' [^] z1' \<otimes> inv (h [^] e)
h = \<^bold>g [^] t
a \<in> carrier \<G>
\<^bold>g [^] z1 \<otimes> g' [^] z1' = a \<otimes> h [^] e
\<lbrakk>?a \<in> carrier \<G>; ?b \<in> carrier \<G>\<rbrakk> \<Longrightarrow> ?a \<otimes> ?b = ?b \<otimes> ?a
\<lbrakk>?x \<in> carrier \<G>; ?y \<in> carrier \<G>; ?z \<in> carrier \<G>\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<otimes> ?z = ?x \<otimes> (?y \<otimes> ?z)
g' = \<^bold>g [^] x
?x \<in> carrier \<G> \<Longrightarrow> (?x [^] ?n) [^] ?m = ?x [^] (?n * ?m)

goal (1 subgoal):
 1. \<^bold>g [^] z2 \<otimes> \<^bold>g [^] (x * z2') \<otimes> \<^bold>g [^] (t * e) = \<^bold>g [^] z1 \<otimes> \<^bold>g [^] (x * z1') \<otimes> \<^bold>g [^] (t * e')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] z2 \<otimes> \<^bold>g [^] (x * z2') \<otimes> \<^bold>g [^] (t * e) = \<^bold>g [^] z1 \<otimes> \<^bold>g [^] (x * z1') \<otimes> \<^bold>g [^] (t * e')

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "\<^bold>g [^] (z2 + x * z2' + t * e) = \<^bold>g [^] (z1 + x * z1' + t * e')"
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] z2 \<otimes> \<^bold>g [^] (x * z2') \<otimes> \<^bold>g [^] (t * e) = \<^bold>g [^] z1 \<otimes> \<^bold>g [^] (x * z1') \<otimes> \<^bold>g [^] (t * e')

goal (1 subgoal):
 1. \<^bold>g [^] (z2 + x * z2' + t * e) = \<^bold>g [^] (z1 + x * z1' + t * e')
[PROOF STEP]
by (simp add: nat_pow_mult)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] (z2 + x * z2' + t * e) = \<^bold>g [^] (z1 + x * z1' + t * e')

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[z2 + x * z2' + t * e = z1 + x * z1' + t * e'] (mod order \<G>)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] (z2 + x * z2' + t * e) = \<^bold>g [^] (z1 + x * z1' + t * e')

goal (1 subgoal):
 1. [z2 + x * z2' + t * e = z1 + x * z1' + t * e'] (mod order \<G>)
[PROOF STEP]
using group_eq_pow_eq_mod order_gt_0
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] (z2 + x * z2' + t * e) = \<^bold>g [^] (z1 + x * z1' + t * e')
\<lbrakk>\<^bold>g [^] ?a = \<^bold>g [^] ?b; 0 < order \<G>\<rbrakk> \<Longrightarrow> [?a = ?b] (mod order \<G>)
0 < order \<G>

goal (1 subgoal):
 1. [z2 + x * z2' + t * e = z1 + x * z1' + t * e'] (mod order \<G>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[z2 + x * z2' + t * e = z1 + x * z1' + t * e'] (mod order \<G>)

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[int z2 + int x * int z2' + int t * int e = int z1 + int x * int z1' + int t * int e'] (mod order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[z2 + x * z2' + t * e = z1 + x * z1' + t * e'] (mod order \<G>)

goal (1 subgoal):
 1. [int z2 + int x * int z2' + int t * int e = int z1 + int x * int z1' + int t * int e'] (mod int (order \<G>))
[PROOF STEP]
using cong_int_iff
[PROOF STATE]
proof (prove)
using this:
[z2 + x * z2' + t * e = z1 + x * z1' + t * e'] (mod order \<G>)
[int ?m = int ?q] (mod int ?n) = [?m = ?q] (mod ?n)

goal (1 subgoal):
 1. [int z2 + int x * int z2' + int t * int e = int z1 + int x * int z1' + int t * int e'] (mod int (order \<G>))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
[int z2 + int x * int z2' + int t * int e = int z1 + int x * int z1' + int t * int e'] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int e - int t * int e'] (mod order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[int z2 + int x * int z2' + int t * int e = int z1 + int x * int z1' + int t * int e'] (mod int (order \<G>))

goal (1 subgoal):
 1. [int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int e - int t * int e'] (mod int (order \<G>))
[PROOF STEP]
by (smt cong_diff_iff_cong_0 cong_sym)
[PROOF STATE]
proof (state)
this:
[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int e - int t * int e'] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * (e - e')] (mod order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int e - int t * int e'] (mod int (order \<G>))

goal (1 subgoal):
 1. [int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int (e - e')] (mod int (order \<G>))
[PROOF STEP]
using int_distrib(4) assms
[PROOF STATE]
proof (prove)
using this:
[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int e - int t * int e'] (mod int (order \<G>))
?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0
h \<in> carrier \<G>
a \<in> carrier \<G>
e < order \<G>
\<^bold>g [^] z1 \<otimes> g' [^] z1' = a \<otimes> h [^] e
e' < e
\<^bold>g [^] z2 \<otimes> g' [^] z2' = a \<otimes> h [^] e'

goal (1 subgoal):
 1. [int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int (e - e')] (mod int (order \<G>))
[PROOF STEP]
by (simp add: of_nat_diff)
[PROOF STATE]
proof (state)
this:
[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int (e - e')] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[(int z1 + int x * int z1' - int z2 - int x * int z2') * fst (bezw (e - e') (order \<G>)) = int t * (e - e') * fst (bezw (e - e') (order \<G>))] (mod order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int (e - e')] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int z1 + int x * int z1' - int z2 - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t * int (e - e') * Number_Theory_Aux.inverse (e - e') (order \<G>)] (mod int (order \<G>))
[PROOF STEP]
using cong_scalar_right
[PROOF STATE]
proof (prove)
using this:
[int z1 + int x * int z1' - int z2 - int x * int z2' = int t * int (e - e')] (mod int (order \<G>))
[?b = ?c] (mod ?a) \<Longrightarrow> [?b * ?d = ?c * ?d] (mod ?a)

goal (1 subgoal):
 1. [(int z1 + int x * int z1' - int z2 - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t * int (e - e') * Number_Theory_Aux.inverse (e - e') (order \<G>)] (mod int (order \<G>))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[(int z1 + int x * int z1' - int z2 - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t * int (e - e') * Number_Theory_Aux.inverse (e - e') (order \<G>)] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[(int z1 + int x * int z1' - int z2 - int x * int z2') * fst (bezw (e - e') (order \<G>)) = int t * ((e - e') * fst (bezw (e - e') (order \<G>)))] (mod order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[(int z1 + int x * int z1' - int z2 - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t * int (e - e') * Number_Theory_Aux.inverse (e - e') (order \<G>)] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int z1 + int x * int z1' - int z2 - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t * (int (e - e') * Number_Theory_Aux.inverse (e - e') (order \<G>))] (mod int (order \<G>))
[PROOF STEP]
by (simp add: mult.assoc)
[PROOF STATE]
proof (state)
this:
[(int z1 + int x * int z1' - int z2 - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t * (int (e - e') * Number_Theory_Aux.inverse (e - e') (order \<G>))] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[(int z1 + int x * int z1' - int z2 - int x * int z2') * fst (bezw (e - e') (order \<G>)) = int t * 1] (mod order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[(int z1 + int x * int z1' - int z2 - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t * (int (e - e') * Number_Theory_Aux.inverse (e - e') (order \<G>))] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int z1 + int x * int z1' - int z2 - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t * 1] (mod int (order \<G>))
[PROOF STEP]
by (metis (no_types, opaque_lifting) cong_scalar_left cong_trans inverse gcd)
[PROOF STATE]
proof (state)
this:
[(int z1 + int x * int z1' - int z2 - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t * 1] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[(int z1 - int z2 + int x * int z1' - int x * int z2') * fst (bezw (e - e') (order \<G>)) = int t] (mod order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[(int z1 + int x * int z1' - int z2 - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t * 1] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int z1 - int z2 + int x * int z1' - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
[(int z1 - int z2 + int x * int z1' - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[(int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order \<G>)) = int t] (mod order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[(int z1 - int z2 + int x * int z1' - int x * int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
by (simp add: Rings.ring_distribs(4) add_diff_eq)
[PROOF STATE]
proof (state)
this:
[(int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "[nat ((int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order \<G>)) mod (order \<G>)) = int t] (mod order \<G>)"
[PROOF STATE]
proof (prove)
using this:
[(int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) = int t] (mod int (order \<G>))

goal (1 subgoal):
 1. [int (nat ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))) = int t] (mod int (order \<G>))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[int (nat ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))) = int t] (mod int (order \<G>))

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "\<^bold>g [^] (nat ((int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order \<G>)) mod (order \<G>))) = \<^bold>g [^] t"
[PROOF STATE]
proof (prove)
using this:
[int (nat ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))) = int t] (mod int (order \<G>))

goal (1 subgoal):
 1. \<^bold>g [^] nat ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
using cong_int_iff finite_carrier pow_generator_eq_iff_cong
[PROOF STATE]
proof (prove)
using this:
[int (nat ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))) = int t] (mod int (order \<G>))
[int ?m = int ?q] (mod int ?n) = [?m = ?q] (mod ?n)
finite (carrier \<G>)
finite (carrier \<G>) \<Longrightarrow> (\<^bold>g [^] ?x = \<^bold>g [^] ?y) = [?x = ?y] (mod order \<G>)

goal (1 subgoal):
 1. \<^bold>g [^] nat ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] nat ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "\<^bold>g [^] ((int z1 - int z2 + int x * (int z1' - int z2')) * fst (bezw (e - e') (order \<G>))) = \<^bold>g [^] t"
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] nat ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t

goal (1 subgoal):
 1. \<^bold>g [^] ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
using pow_generator_mod_int
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] nat ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t
\<^bold>g [^] (?k mod int (order \<G>)) = \<^bold>g [^] ?k

goal (1 subgoal):
 1. \<^bold>g [^] ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "\<^bold>g [^] ((int z1 - int z2) * fst (bezw (e - e') (order \<G>)) + int x * (int z1' - int z2') * fst (bezw (e - e') (order \<G>))) = \<^bold>g [^] t"
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ((int z1 - int z2 + int x * (int z1' - int z2')) * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t

goal (1 subgoal):
 1. \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) + int x * (int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
by (metis Rings.ring_distribs(2) t)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) + int x * (int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
hence "\<^bold>g [^] ((int z1 - int z2) * fst (bezw (e - e') (order \<G>))) \<otimes> \<^bold>g [^] (int x * (int z1' - int z2') * fst (bezw (e - e') (order \<G>))) = \<^bold>g [^] t"
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) + int x * (int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t

goal (1 subgoal):
 1. \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>)) \<otimes> \<^bold>g [^] (int x * (int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
using int_pow_mult
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) + int x * (int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t
?x \<in> carrier \<G> \<Longrightarrow> ?x [^] (?i + ?j) = ?x [^] ?i \<otimes> ?x [^] ?j

goal (1 subgoal):
 1. \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>)) \<otimes> \<^bold>g [^] (int x * (int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>)) \<otimes> \<^bold>g [^] (int x * (int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>)) \<otimes> \<^bold>g [^] (int x * (int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>)) = \<^bold>g [^] t

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) g'_def generator_closed int_pow_int int_pow_pow mod_mult_right_eq more_arith_simps(11) pow_generator_mod_int t)
[PROOF STATE]
proof (state)
this:
h = \<^bold>g [^] ((int z1 - int z2) * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int z1' - int z2') * Number_Theory_Aux.inverse (e - e') (order \<G>) mod int (order \<G>))

goal:
No subgoals!
[PROOF STEP]
qed