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

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

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))
[PROOF STEP]
have "\<^bold>g [^] fst z \<otimes> g' [^] snd z \<otimes> inv (h [^] e) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] fst z \<otimes> g' [^] snd z \<otimes> inv (h [^] e) = a
[PROOF STEP]
using a h_mem a_mem
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] fst z \<otimes> g' [^] snd z = a \<otimes> h [^] e
h \<in> carrier \<G>
a \<in> carrier \<G>

goal (1 subgoal):
 1. \<^bold>g [^] fst z \<otimes> g' [^] snd z \<otimes> inv (h [^] e) = a
[PROOF STEP]
by (simp add: inv_solve_right')
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] fst z \<otimes> g' [^] snd z \<otimes> inv (h [^] e) = a

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

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))
[PROOF STEP]
have "\<^bold>g [^] fst z' \<otimes> g' [^] snd z' \<otimes> inv (h [^] e') = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] fst z' \<otimes> g' [^] snd z' \<otimes> inv (h [^] e') = a
[PROOF STEP]
using a h_mem a_mem
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] fst z \<otimes> g' [^] snd z = a \<otimes> h [^] e
h \<in> carrier \<G>
a \<in> carrier \<G>

goal (1 subgoal):
 1. \<^bold>g [^] fst z' \<otimes> g' [^] snd z' \<otimes> inv (h [^] e') = a
[PROOF STEP]
by (simp add: assms(4) inv_solve_right')
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] fst z' \<otimes> g' [^] snd z' \<otimes> inv (h [^] e') = a

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

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

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

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

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (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 h_mem generatorE
[PROOF STATE]
proof (prove)
using this:
h \<in> carrier \<G>
\<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 (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<^bold>g [^] fst z \<otimes> \<^bold>g [^] (x * snd z) \<otimes> inv (h [^] e) = \<^bold>g [^] fst z' \<otimes> \<^bold>g [^] (x * snd z') \<otimes> inv (h [^] e')
h = \<^bold>g [^] t
[PROOF STEP]
have "\<^bold>g [^] fst z \<otimes> \<^bold>g [^] (x * snd z) \<otimes> \<^bold>g [^] (t * e') = \<^bold>g [^] fst z' \<otimes> \<^bold>g [^] (x * snd z') \<otimes> \<^bold>g [^] (t * e)"
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] fst z \<otimes> \<^bold>g [^] (x * snd z) \<otimes> inv (h [^] e) = \<^bold>g [^] fst z' \<otimes> \<^bold>g [^] (x * snd z') \<otimes> inv (h [^] e')
h = \<^bold>g [^] t

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

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

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

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

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

goal (1 subgoal):
 1. [fst z + x * snd z + t * e' = fst z' + x * snd z' + t * e] (mod order \<G>)
[PROOF STEP]
using group_eq_pow_eq_mod order_gt_0
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] (fst z + x * snd z + t * e') = \<^bold>g [^] (fst z' + x * snd z' + 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. [fst z + x * snd z + t * e' = fst z' + x * snd z' + t * e] (mod order \<G>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[fst z + x * snd z + t * e' = fst z' + x * snd z' + t * e] (mod order \<G>)

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

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

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

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

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

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

goal (1 subgoal):
 1. [int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [int (fst z) - int (fst z') + int x * int (snd z) - int x * int (snd z') = int t * int e - int t * int e'] (mod int (order \<G>)) \<Longrightarrow> [int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
have "[int (fst z) + (int (x * snd z) - (int (fst z') + int (x * snd z'))) = int t * (int e - int e')] (mod int (order \<G>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [int (fst z) + (int (x * snd z) - (int (fst z') + int (x * snd z'))) = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
by (simp add: Rings.ring_distribs(4) \<open>[int (fst z) - int (fst z') + int x * int (snd z) - int x * int (snd z') = int t * int e - int t * int e'] (mod int (order \<G>))\<close> add_diff_add add_diff_eq)
[PROOF STATE]
proof (state)
this:
[int (fst z) + (int (x * snd z) - (int (fst z') + int (x * snd z'))) = int t * (int e - int e')] (mod int (order \<G>))

goal (1 subgoal):
 1. [int (fst z) - int (fst z') + int x * int (snd z) - int x * int (snd z') = int t * int e - int t * int e'] (mod int (order \<G>)) \<Longrightarrow> [int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[int (fst z) + (int (x * snd z) - (int (fst z') + int (x * snd z'))) = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
have "\<exists>i. [int (fst z) + (int x * int (snd z) - (int (fst z') + i * int (snd z'))) = int t * (int e - int e') + int (snd z') * (int x - i)] (mod int (order \<G>))"
[PROOF STATE]
proof (prove)
using this:
[int (fst z) + (int (x * snd z) - (int (fst z') + int (x * snd z'))) = int t * (int e - int e')] (mod int (order \<G>))

goal (1 subgoal):
 1. \<exists>i. [int (fst z) + (int x * int (snd z) - (int (fst z') + i * int (snd z'))) = int t * (int e - int e') + int (snd z') * (int x - i)] (mod int (order \<G>))
[PROOF STEP]
by (metis (no_types) add.commute arith_simps(49) cancel_comm_monoid_add_class.diff_cancel int_ops(7) mult_eq_0_iff)
[PROOF STATE]
proof (state)
this:
\<exists>i. [int (fst z) + (int x * int (snd z) - (int (fst z') + i * int (snd z'))) = int t * (int e - int e') + int (snd z') * (int x - i)] (mod int (order \<G>))

goal (1 subgoal):
 1. [int (fst z) - int (fst z') + int x * int (snd z) - int x * int (snd z') = int t * int e - int t * int e'] (mod int (order \<G>)) \<Longrightarrow> [int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. [int (fst z) + (int x * int (snd z) - (int (fst z') + i * int (snd z'))) = int t * (int e - int e') + int (snd z') * (int x - i)] (mod int (order \<G>))
[PROOF STEP]
have "\<exists>i. [int (fst z) - int (fst z') + (int x * (int (snd z) - int (snd z')) + i) = int t * (int e - int e') + i] (mod int (order \<G>))"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. [int (fst z) + (int x * int (snd z) - (int (fst z') + i * int (snd z'))) = int t * (int e - int e') + int (snd z') * (int x - i)] (mod int (order \<G>))

goal (1 subgoal):
 1. \<exists>i. [int (fst z) - int (fst z') + (int x * (int (snd z) - int (snd z')) + i) = int t * (int e - int e') + i] (mod int (order \<G>))
[PROOF STEP]
by (metis (no_types) add_diff_add add_diff_eq mult_diff_mult mult_of_nat_commute)
[PROOF STATE]
proof (state)
this:
\<exists>i. [int (fst z) - int (fst z') + (int x * (int (snd z) - int (snd z')) + i) = int t * (int e - int e') + i] (mod int (order \<G>))

goal (1 subgoal):
 1. [int (fst z) - int (fst z') + int x * int (snd z) - int x * int (snd z') = int t * int e - int t * int e'] (mod int (order \<G>)) \<Longrightarrow> [int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. [int (fst z) - int (fst z') + (int x * (int (snd z) - int (snd z')) + i) = int t * (int e - int e') + i] (mod int (order \<G>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>i. [int (fst z) - int (fst z') + (int x * (int (snd z) - int (snd z')) + i) = int t * (int e - int e') + i] (mod int (order \<G>))

goal (1 subgoal):
 1. [int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * (int e - int e')] (mod int (order \<G>))
[PROOF STEP]
by (metis (no_types) add.assoc cong_add_rcancel)
[PROOF STATE]
proof (state)
this:
[int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * (int e - int e')] (mod int (order \<G>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * (int e - int e')] (mod int (order \<G>))

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

goal (1 subgoal):
 1. [int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * (int e mod int (order \<G>) - int e' mod int (order \<G>)) mod int (order \<G>)] (mod int (order \<G>))
[PROOF STEP]
by (metis (mono_tags, lifting) cong_def mod_diff_eq mod_mod_trivial mod_mult_right_eq)
[PROOF STATE]
proof (state)
this:
[int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * (int e mod int (order \<G>) - int e' mod int (order \<G>)) mod int (order \<G>)] (mod int (order \<G>))

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

goal (1 subgoal):
 1. [int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * int (e mod order \<G> - e' mod order \<G>) mod int (order \<G>)] (mod int (order \<G>))
[PROOF STEP]
using e_e'_mod
[PROOF STATE]
proof (prove)
using this:
[int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z')) = int t * (int e mod int (order \<G>) - int e' mod int (order \<G>)) mod int (order \<G>)] (mod int (order \<G>))
e' mod order \<G> < e mod order \<G>

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

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

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

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

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

goal (1 subgoal):
 1. [(int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z'))) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t * (int ((e mod order \<G> - e' mod order \<G>) mod order \<G>) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))
[PROOF STEP]
by (metis (no_types, lifting) Groups.mult_ac(1) cong_mod_right less_imp_diff_less mod_less mod_mult_left_eq mod_mult_right_eq order_gt_0 unique_euclidean_semiring_numeral_class.pos_mod_bound)
[PROOF STATE]
proof (state)
this:
[(int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z'))) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t * (int ((e mod order \<G> - e' mod order \<G>) mod order \<G>) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))

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

goal (1 subgoal):
 1. [(int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z'))) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t * 1] (mod int (order \<G>))
[PROOF STEP]
using inverse gcd
[PROOF STATE]
proof (prove)
using this:
[(int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z'))) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t * (int ((e mod order \<G> - e' mod order \<G>) mod order \<G>) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))
gcd ?x ?q = 1 \<Longrightarrow> [int ?x * Number_Theory_Aux.inverse ?x ?q = 1] (mod int ?q)
gcd ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) = 1

goal (1 subgoal):
 1. [(int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z'))) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t * 1] (mod int (order \<G>))
[PROOF STEP]
by (smt Num.of_nat_simps(5) Number_Theory_Aux.inverse cong_def mod_mult_right_eq more_arith_simps(6) of_nat_1)
[PROOF STATE]
proof (state)
this:
[(int (fst z) - int (fst z') + int x * (int (snd z) - int (snd z'))) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t * 1] (mod int (order \<G>))

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

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

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

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>))
[PROOF STEP]
by (metis (no_types, opaque_lifting) cong_mod_left distrib_right mod_mult_right_eq)
[PROOF STATE]
proof (state)
this:
[(int (fst z) - int (fst z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>))

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

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>)) \<Longrightarrow> [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>))
[PROOF STEP]
have "[(int (fst z) - int (fst z')) * fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) = (int (fst z) - int (fst z')) * (fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>))] (mod int (order \<G>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) = (int (fst z) - int (fst z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))
[PROOF STEP]
by (metis (no_types) cong_def mod_mult_right_eq)
[PROOF STATE]
proof (state)
this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) = (int (fst z) - int (fst z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>)) \<Longrightarrow> [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) = (int (fst z) - int (fst z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) = (int (fst z) - int (fst z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>))
[PROOF STEP]
by (meson \<open>[(int (fst z) - int (fst z')) * (fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>)) + int x * (int (snd z) - int (snd z')) * (fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>)) = int t] (mod int (order \<G>))\<close> cong_add_rcancel cong_mod_left cong_trans)
[PROOF STATE]
proof (state)
this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>))

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

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>)) \<Longrightarrow> [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
have "int x * ((int (snd z) - int (snd z')) * (fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>))) mod int (order \<G>) = int x * ((int (snd z) - int (snd z')) * fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>))) mod int (order \<G>) mod int (order \<G>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int x * ((int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))) mod int (order \<G>) = int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) mod int (order \<G>)
[PROOF STEP]
by (metis (no_types) mod_mod_trivial mod_mult_right_eq)
[PROOF STATE]
proof (state)
this:
int x * ((int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))) mod int (order \<G>) = int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) mod int (order \<G>)

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>)) \<Longrightarrow> [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int x * ((int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))) mod int (order \<G>) = int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) mod int (order \<G>)
[PROOF STEP]
have "[int x * ((int (snd z) - int (snd z')) * fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>))) mod int (order \<G>) = int x * ((int (snd z) - int (snd z')) * (fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>)))] (mod int (order \<G>))"
[PROOF STATE]
proof (prove)
using this:
int x * ((int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))) mod int (order \<G>) = int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) mod int (order \<G>)

goal (1 subgoal):
 1. [int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = int x * ((int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)))] (mod int (order \<G>))
[PROOF STEP]
by (metis (no_types) cong_def)
[PROOF STATE]
proof (state)
this:
[int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = int x * ((int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)))] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>)) \<Longrightarrow> [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = int x * ((int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)))] (mod int (order \<G>))
[PROOF STEP]
have "[(int (fst z) - int (fst z')) * fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) + int x * ((int (snd z) - int (snd z')) * fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>))) mod int (order \<G>) = (int (fst z) - int (fst z')) * fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>))] (mod int (order \<G>))"
[PROOF STATE]
proof (prove)
using this:
[int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = int x * ((int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)))] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = (int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))
[PROOF STEP]
by (metis (no_types) Groups.mult_ac(1) cong_add cong_refl)
[PROOF STATE]
proof (state)
this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = (int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>)) \<Longrightarrow> [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = (int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))
[PROOF STEP]
have "[(int (fst z) - int (fst z')) * fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) + int x * ((int (snd z) - int (snd z')) * fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>))) mod int (order \<G>) = int t] (mod int (order \<G>))"
[PROOF STATE]
proof (prove)
using this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = (int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
using \<open>[(int (fst z) - int (fst z')) * fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (fst (bezw ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>)) = int t] (mod int (order \<G>))\<close> cong_trans
[PROOF STATE]
proof (prove)
using this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = (int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))] (mod int (order \<G>))
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>))
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)

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

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * (Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = int t] (mod int (order \<G>)) \<Longrightarrow> [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>)) mod int (order \<G>) = int t] (mod int (order \<G>))

goal (1 subgoal):
 1. [(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))
[PROOF STEP]
by (metis (no_types) Groups.mult_ac(1))
[PROOF STATE]
proof (state)
this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[(int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) = int t] (mod int (order \<G>))

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

goal (1 subgoal):
 1. \<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
by (metis cong_def int_pow_int pow_generator_mod_int)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t

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

goal (1 subgoal):
 1. \<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) \<otimes> \<^bold>g [^] (int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
using int_pow_mult
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>) + int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (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 (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) \<otimes> \<^bold>g [^] (int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) \<otimes> \<^bold>g [^] (int x * (int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t

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

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

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

goal (1 subgoal):
 1. \<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t
[PROOF STEP]
by (smt g'_def cyclic_group.generator_closed int_pow_int int_pow_pow mod_mult_right_eq more_arith_simps(11) okamoto_axioms okamoto_def pow_generator_mod_int)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) = \<^bold>g [^] t

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

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

goal (1 subgoal):
 1. h = \<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h = \<^bold>g [^] ((int (fst z) - int (fst z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>)) \<otimes> g' [^] ((int (snd z) - int (snd z')) * Number_Theory_Aux.inverse ((e mod order \<G> - e' mod order \<G>) mod order \<G>) (order \<G>) mod int (order \<G>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma special_soundness:
  shows "\<Sigma>_protocols_base.special_soundness"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.special_soundness
[PROOF STEP]
unfolding \<Sigma>_protocols_base.special_soundness_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>h e e' a z z'. h \<in> valid_pub \<longrightarrow> e \<in> challenge_space \<longrightarrow> e' \<in> challenge_space \<longrightarrow> e \<noteq> e' \<longrightarrow> check h a e z \<longrightarrow> check h a e' z' \<longrightarrow> lossless_spmf (ss_adversary h (a, e, z) (a, e', z')) \<and> (\<forall>w'\<in>set_spmf (ss_adversary h (a, e, z) (a, e', z')). (h, w') \<in> R)
[PROOF STEP]
by(auto simp add: valid_pub_def check_def R_def ss_adversary_def Let_def ss_rewrite challenge_space_def split_def)


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


[STATEMENT]
lemma reduction_to_dis_log:
  shows "okamoto_\<Sigma>_commit.rel_advantage \ = dis_log.advantage (dis_log_alt.adversary2 \)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
have exp_rewrite: "\<^bold>g [^] w1 \<otimes> g' [^] w2 =  \<^bold>g [^] (w1 + x * w2)" for w1 w2 :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>g [^] w1 \<otimes> g' [^] w2 = \<^bold>g [^] (w1 + x * w2)
[PROOF STEP]
by (simp add: nat_pow_mult nat_pow_pow g'_def)
[PROOF STATE]
proof (state)
this:
\<^bold>g [^] ?w1.1 \<otimes> g' [^] ?w2.1 = \<^bold>g [^] (?w1.1 + x * ?w2.1)

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
have "okamoto_\<Sigma>_commit.rel_game \ = TRY do {
    w1 \<leftarrow> sample_uniform (order \<G>);
    w2 \<leftarrow> sample_uniform (order \<G>);
    let h = (\<^bold>g [^] w1 \<otimes> g' [^] w2);
    (w1',w2') \<leftarrow> \ h;
    return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')} ELSE return_spmf False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_game \ = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let h = \<^bold>g [^] w1 \<otimes> g' [^] w2 in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False
[PROOF STEP]
unfolding okamoto_\<Sigma>_commit.rel_game_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY G \<bind> (\<lambda>(h, w). \ h \<bind> (\<lambda>w'. return_spmf ((h, w') \<in> R))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let h = \<^bold>g [^] w1 \<otimes> g' [^] w2 in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False
[PROOF STEP]
by(simp add: Let_def split_def R_def G_def)
[PROOF STATE]
proof (state)
this:
okamoto_\<Sigma>_commit.rel_game \ = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let h = \<^bold>g [^] w1 \<otimes> g' [^] w2 in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
okamoto_\<Sigma>_commit.rel_game \ = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let h = \<^bold>g [^] w1 \<otimes> g' [^] w2 in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
have "... = TRY do {
    w1 \<leftarrow> sample_uniform (order \<G>);
    w2 \<leftarrow> sample_uniform (order \<G>);
    let w = (w1 + x * w2) mod (order \<G>);
    let h = \<^bold>g [^] w;
    (w1',w2') \<leftarrow> \ h;
    return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')} ELSE return_spmf False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let h = \<^bold>g [^] w1 \<otimes> g' [^] w2 in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let w = (w1 + x * w2) mod order \<G>; h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False
[PROOF STEP]
using g'_def exp_rewrite pow_generator_mod
[PROOF STATE]
proof (prove)
using this:
g' = \<^bold>g [^] x
\<^bold>g [^] ?w1.1 \<otimes> g' [^] ?w2.1 = \<^bold>g [^] (?w1.1 + x * ?w2.1)
\<^bold>g [^] (?k mod order \<G>) = \<^bold>g [^] ?k

goal (1 subgoal):
 1. TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let h = \<^bold>g [^] w1 \<otimes> g' [^] w2 in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let w = (w1 + x * w2) mod order \<G>; h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let h = \<^bold>g [^] w1 \<otimes> g' [^] w2 in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let w = (w1 + x * w2) mod order \<G>; h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let h = \<^bold>g [^] w1 \<otimes> g' [^] w2 in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let w = (w1 + x * w2) mod order \<G>; h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
have "... = TRY do {
    w2 \<leftarrow> sample_uniform (order \<G>);
    w \<leftarrow> map_spmf (\<lambda> w1. (x * w2 + w1) mod (order \<G>)) (sample_uniform (order \<G>));
    let h = \<^bold>g [^] w;
    (w1',w2') \<leftarrow> \ h;
    return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')} ELSE return_spmf False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let w = (w1 + x * w2) mod order \<G>; h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. map_spmf (\<lambda>w1. (x * w2 + w1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let w = (w1 + x * w2) mod order \<G>; h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. map_spmf (\<lambda>w1. (x * w2 + w1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def add.commute)
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let w = (w1 + x * w2) mod order \<G>; h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. map_spmf (\<lambda>w1. (x * w2 + w1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>w1. sample_uniform (order \<G>) \<bind> (\<lambda>w2. let w = (w1 + x * w2) mod order \<G>; h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. map_spmf (\<lambda>w1. (x * w2 + w1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
have "... = TRY do {
    w2 :: nat \<leftarrow> sample_uniform (order \<G>);
    w \<leftarrow> sample_uniform (order \<G>);
    let h = \<^bold>g [^] w;
    (w1',w2') \<leftarrow> \ h;
    return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')} ELSE return_spmf False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. map_spmf (\<lambda>w1. (x * w2 + w1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False
[PROOF STEP]
using samp_uni_plus_one_time_pad add.commute
[PROOF STATE]
proof (prove)
using this:
map_spmf (\<lambda>b. (?y + b) mod ?q) (sample_uniform ?q) = sample_uniform ?q
?a + ?b = ?b + ?a

goal (1 subgoal):
 1. TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. map_spmf (\<lambda>w1. (x * w2 + w1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. map_spmf (\<lambda>w1. (x * w2 + w1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. map_spmf (\<lambda>w1. (x * w2 + w1) mod order \<G>) (sample_uniform (order \<G>)) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
have "... = TRY do {
    w \<leftarrow> sample_uniform (order \<G>);
    let h = \<^bold>g [^] w;
    (w1',w2') \<leftarrow> \ h;
    return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')} ELSE return_spmf False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2'))) ELSE return_spmf False
[PROOF STEP]
by(simp add: bind_spmf_const)
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2'))) ELSE return_spmf False

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>w2. sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2')))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2'))) ELSE return_spmf False

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
have "... = dis_log_alt.dis_log2 \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2'))) ELSE return_spmf False = local.dis_log_alt.dis_log2 \
[PROOF STEP]
apply(simp add: dis_log_alt.dis_log2_def Let_def dis_log_alt.g'_def g'_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TRY sample_uniform (order \<G>) \<bind> (\<lambda>w. \ (\<^bold>g [^] w) \<bind> (\<lambda>(w1', w2'). return_spmf (\<^bold>g [^] w = \<^bold>g [^] w1' \<otimes> (\<^bold>g [^] x) [^] w2'))) ELSE return_spmf False = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w. \ (\<^bold>g [^] w) \<bind> (\<lambda>(w1', w2'). return_spmf [w = w1' + x * w2'] (mod order \<G>))) ELSE return_spmf False
[PROOF STEP]
apply(intro try_spmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. sample_uniform (order \<G>) \<bind> (\<lambda>w. \ (\<^bold>g [^] w) \<bind> (\<lambda>(w1', w2'). return_spmf (\<^bold>g [^] w = \<^bold>g [^] w1' \<otimes> (\<^bold>g [^] x) [^] w2'))) = sample_uniform (order \<G>) \<bind> (\<lambda>w. \ (\<^bold>g [^] w) \<bind> (\<lambda>(w1', w2'). return_spmf [w = w1' + x * w2'] (mod order \<G>)))
 2. \<not> lossless_spmf (sample_uniform (order \<G>) \<bind> (\<lambda>w. \ (\<^bold>g [^] w) \<bind> (\<lambda>(w1', w2'). return_spmf [w = w1' + x * w2'] (mod order \<G>)))) \<Longrightarrow> return_spmf False = return_spmf False
[PROOF STEP]
apply(intro bind_spmf_cong[OF refl]; clarsimp?)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa a b. \<lbrakk>xa < order \<G>; (a, b) \<in> set_spmf (\ (\<^bold>g [^] xa))\<rbrakk> \<Longrightarrow> (\<^bold>g [^] xa = \<^bold>g [^] a \<otimes> (\<^bold>g [^] x) [^] b) = [xa = a + x * b] (mod order \<G>)
 2. \<not> lossless_spmf (sample_uniform (order \<G>) \<bind> (\<lambda>w. \ (\<^bold>g [^] w) \<bind> (\<lambda>(w1', w2'). return_spmf [w = w1' + x * w2'] (mod order \<G>)))) \<Longrightarrow> return_spmf False = return_spmf False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa a b. \<lbrakk>xa < order \<G>; (a, b) \<in> set_spmf (\ (\<^bold>g [^] a \<otimes> (\<^bold>g [^] x) [^] b)); \<^bold>g [^] xa = \<^bold>g [^] a \<otimes> (\<^bold>g [^] x) [^] b\<rbrakk> \<Longrightarrow> [xa = a + x * b] (mod order \<G>)
 2. \<And>xa a b. \<lbrakk>xa < order \<G>; (a, b) \<in> set_spmf (\ (\<^bold>g [^] xa)); [xa = a + x * b] (mod order \<G>)\<rbrakk> \<Longrightarrow> \<^bold>g [^] xa = \<^bold>g [^] a \<otimes> (\<^bold>g [^] x) [^] b
[PROOF STEP]
using exp_rewrite pow_generator_mod g'_def
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ?w1.1 \<otimes> g' [^] ?w2.1 = \<^bold>g [^] (?w1.1 + x * ?w2.1)
\<^bold>g [^] (?k mod order \<G>) = \<^bold>g [^] ?k
g' = \<^bold>g [^] x

goal (2 subgoals):
 1. \<And>xa a b. \<lbrakk>xa < order \<G>; (a, b) \<in> set_spmf (\ (\<^bold>g [^] a \<otimes> (\<^bold>g [^] x) [^] b)); \<^bold>g [^] xa = \<^bold>g [^] a \<otimes> (\<^bold>g [^] x) [^] b\<rbrakk> \<Longrightarrow> [xa = a + x * b] (mod order \<G>)
 2. \<And>xa a b. \<lbrakk>xa < order \<G>; (a, b) \<in> set_spmf (\ (\<^bold>g [^] xa)); [xa = a + x * b] (mod order \<G>)\<rbrakk> \<Longrightarrow> \<^bold>g [^] xa = \<^bold>g [^] a \<otimes> (\<^bold>g [^] x) [^] b
[PROOF STEP]
apply (metis group_eq_pow_eq_mod okamoto_axioms okamoto_base.order_gt_0 okamoto_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa a b. \<lbrakk>xa < order \<G>; (a, b) \<in> set_spmf (\ (\<^bold>g [^] xa)); [xa = a + x * b] (mod order \<G>)\<rbrakk> \<Longrightarrow> \<^bold>g [^] xa = \<^bold>g [^] a \<otimes> (\<^bold>g [^] x) [^] b
[PROOF STEP]
using exp_rewrite g'_def order_gt_0_iff_finite pow_generator_eq_iff_cong
[PROOF STATE]
proof (prove)
using this:
\<^bold>g [^] ?w1.1 \<otimes> g' [^] ?w2.1 = \<^bold>g [^] (?w1.1 + x * ?w2.1)
g' = \<^bold>g [^] x
(0 < order \<G>) = finite (carrier \<G>)
finite (carrier \<G>) \<Longrightarrow> (\<^bold>g [^] ?x = \<^bold>g [^] ?y) = [?x = ?y] (mod order \<G>)

goal (1 subgoal):
 1. \<And>xa a b. \<lbrakk>xa < order \<G>; (a, b) \<in> set_spmf (\ (\<^bold>g [^] xa)); [xa = a + x * b] (mod order \<G>)\<rbrakk> \<Longrightarrow> \<^bold>g [^] xa = \<^bold>g [^] a \<otimes> (\<^bold>g [^] x) [^] b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
TRY sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2'))) ELSE return_spmf False = local.dis_log_alt.dis_log2 \

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
okamoto_\<Sigma>_commit.rel_game \ = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2'))) ELSE return_spmf False
TRY sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2'))) ELSE return_spmf False = local.dis_log_alt.dis_log2 \
[PROOF STEP]
have "okamoto_\<Sigma>_commit.rel_game \ = dis_log_alt.dis_log2 \"
[PROOF STATE]
proof (prove)
using this:
okamoto_\<Sigma>_commit.rel_game \ = TRY sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2'))) ELSE return_spmf False
TRY sample_uniform (order \<G>) \<bind> (\<lambda>w. let h = \<^bold>g [^] w in \ h \<bind> (\<lambda>(w1', w2'). return_spmf (h = \<^bold>g [^] w1' \<otimes> g' [^] w2'))) ELSE return_spmf False = local.dis_log_alt.dis_log2 \

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_game \ = local.dis_log_alt.dis_log2 \
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
okamoto_\<Sigma>_commit.rel_game \ = local.dis_log_alt.dis_log2 \

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
hence "okamoto_\<Sigma>_commit.rel_advantage \ = dis_log_alt.advantage2 \"
[PROOF STATE]
proof (prove)
using this:
okamoto_\<Sigma>_commit.rel_game \ = local.dis_log_alt.dis_log2 \

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log_alt.advantage2 \
[PROOF STEP]
by(simp add: okamoto_\<Sigma>_commit.rel_advantage_def dis_log_alt.advantage2_def)
[PROOF STATE]
proof (state)
this:
okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log_alt.advantage2 \

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log_alt.advantage2 \

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)
[PROOF STEP]
by (simp add: dis_log_alt_reductions.dis_log_adv2 cyclic_group_axioms dis_log_alt.dis_log_alt_axioms dis_log_alt_reductions.intro)
[PROOF STATE]
proof (state)
this:
okamoto_\<Sigma>_commit.rel_advantage \ = local.dis_log.advantage (local.dis_log_alt.adversary2 \)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma commitment_correct: "okamoto_\<Sigma>_commit.abstract_com.correct"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.abstract_com.correct
[PROOF STEP]
by(simp add: okamoto_\<Sigma>_commit.commit_correct)


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

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


[STATEMENT]
lemma binding:
  shows "okamoto_\<Sigma>_commit.abstract_com.bind_advantage \<A>
          \<le> dis_log.advantage (dis_log_alt.adversary2 (okamoto_\<Sigma>_commit.adversary \<A>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.abstract_com.bind_advantage \<A> \<le> local.dis_log.advantage (local.dis_log_alt.adversary2 (okamoto_\<Sigma>_commit.adversary \<A>))
[PROOF STEP]
using okamoto_\<Sigma>_commit.bind_advantage reduction_to_dis_log
[PROOF STATE]
proof (prove)
using this:
okamoto_\<Sigma>_commit.abstract_com.bind_advantage ?\<A> \<le> okamoto_\<Sigma>_commit.rel_advantage (okamoto_\<Sigma>_commit.adversary ?\<A>)
okamoto_\<Sigma>_commit.rel_advantage ?\<A> = local.dis_log.advantage (local.dis_log_alt.adversary2 ?\<A>)

goal (1 subgoal):
 1. okamoto_\<Sigma>_commit.abstract_com.bind_advantage \<A> \<le> local.dis_log.advantage (local.dis_log_alt.adversary2 (okamoto_\<Sigma>_commit.adversary \<A>))
[PROOF STEP]
by auto


[STATEMENT]
theorem sigma_protocol:
  shows "\<Sigma>_protocols_base.\<Sigma>_protocol n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.\<Sigma>_protocols_base.\<Sigma>_protocol n
[PROOF STEP]
by(simp add: \<Sigma>_protocol)


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

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


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

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


[STATEMENT]
lemma asymp_computational_binding:
  assumes "negligible (\<lambda> n. dis_log.advantage n (dis_log_alt.adversary2 (okamoto_\<Sigma>_commit.adversary n (\<A> n))))"
  shows "negligible (\<lambda> n. okamoto_\<Sigma>_commit.abstract_com.bind_advantage n (\<A> n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. okamoto_\<Sigma>_commit.abstract_com.bind_advantage n (\<A> n))
[PROOF STEP]
using okamoto_\<Sigma>_commit.bind_advantage assms okamoto_\<Sigma>_commit.abstract_com.bind_advantage_def negligible_le binding
[PROOF STATE]
proof (prove)
using this:
okamoto_\<Sigma>_commit.abstract_com.bind_advantage ?\<eta> ?\<A> \<le> okamoto_\<Sigma>_commit.rel_advantage ?\<eta> (okamoto_\<Sigma>_commit.adversary ?\<eta> ?\<A>)
Negligible.negligible (\<lambda>n. local.dis_log.advantage n (local.dis_log_alt.adversary2 (okamoto_\<Sigma>_commit.adversary n (\<A> n))))
okamoto_\<Sigma>_commit.abstract_com.bind_advantage ?\<eta> ?\<A> \<equiv> spmf (okamoto_\<Sigma>_commit.abstract_com.bind_game ?\<eta> ?\<A>) True
\<lbrakk>Negligible.negligible ?g; \<And>\<eta>. \<bar>?f \<eta>\<bar> \<le> ?g \<eta>\<rbrakk> \<Longrightarrow> Negligible.negligible ?f
okamoto_\<Sigma>_commit.abstract_com.bind_advantage ?\<eta> ?\<A> \<le> local.dis_log.advantage ?\<eta> (local.dis_log_alt.adversary2 (okamoto_\<Sigma>_commit.adversary ?\<eta> ?\<A>))

goal (1 subgoal):
 1. Negligible.negligible (\<lambda>n. okamoto_\<Sigma>_commit.abstract_com.bind_advantage n (\<A> n))
[PROOF STEP]
by auto


[STATEMENT]
lemma tauPres:
  fixes P :: pi
  and   Q :: pi

  assumes "P \<sim> Q"

  shows "\<tau>.(P) \<sim> \<tau>.(Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>.P \<sim> \<tau>.Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<tau>.P \<sim> \<tau>.Q
[PROOF STEP]
let ?X = "{(\<tau>.(P), \<tau>.(Q)), (\<tau>.(Q), \<tau>.(P))}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<tau>.P \<sim> \<tau>.Q
[PROOF STEP]
have "(\<tau>.(P), \<tau>.(Q)) \<in> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<tau>.P, \<tau>.Q) \<in> {(\<tau>.P, \<tau>.Q), (\<tau>.Q, \<tau>.P)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<tau>.P, \<tau>.Q) \<in> {(\<tau>.P, \<tau>.Q), (\<tau>.Q, \<tau>.P)}

goal (1 subgoal):
 1. \<tau>.P \<sim> \<tau>.Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<tau>.P, \<tau>.Q) \<in> {(\<tau>.P, \<tau>.Q), (\<tau>.Q, \<tau>.P)}

goal (1 subgoal):
 1. \<tau>.P \<sim> \<tau>.Q
[PROOF STEP]
using \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (prove)
using this:
(\<tau>.P, \<tau>.Q) \<in> {(\<tau>.P, \<tau>.Q), (\<tau>.Q, \<tau>.P)}
P \<sim> Q

goal (1 subgoal):
 1. \<tau>.P \<sim> \<tau>.Q
[PROOF STEP]
by(coinduct rule: bisimCoinduct)
      (auto intro: Strong_Late_Sim_Pres.tauPres dest: symmetric)
[PROOF STATE]
proof (state)
this:
\<tau>.P \<sim> \<tau>.Q

goal:
No subgoals!
[PROOF STEP]
qed