[STATEMENT]
lemma d2:
  assumes d2: "d2 = (((e2 + q - x) mod q)*b + (q - r)) mod q"
    and s1: "s1 = (x*((y + (q - b)) mod q) + (q - r)) mod q"
    and s2: "s2 = (x*y + (q - s1)) mod q"
    and x: "x < q"
    and y: "y < q"
    and r: "r < q"
    and b: "b < q"
    and e2: "e2 < q"
  shows "d2  = (e2*b + (q - s2)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
have s1_le_q: "s1 < q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 < q
[PROOF STEP]
using s1 q_gt_0
[PROOF STATE]
proof (prove)
using this:
s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q
0 < q

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

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
have s2_le_q: "s2 < q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2 < q
[PROOF STEP]
using s2 q_gt_0
[PROOF STATE]
proof (prove)
using this:
s2 = (x * y + (q - s1)) mod q
0 < q

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

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
have xb: "(x*b) mod q = (s2  + (q - r)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
have "s1 = (x*(y + (q - b)) + (q - r)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 = (x * (y + (q - b)) + (q - r)) mod q
[PROOF STEP]
using s1 b
[PROOF STATE]
proof (prove)
using this:
s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q
b < q

goal (1 subgoal):
 1. s1 = (x * (y + (q - b)) + (q - r)) mod q
[PROOF STEP]
by (metis mod_add_left_eq mod_mult_right_eq)
[PROOF STATE]
proof (state)
this:
s1 = (x * (y + (q - b)) + (q - r)) mod q

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1 = (x * (y + (q - b)) + (q - r)) mod q
[PROOF STEP]
have s1_dist: "s1 = (x*y + x*(q - b) + (q - r)) mod q"
[PROOF STATE]
proof (prove)
using this:
s1 = (x * (y + (q - b)) + (q - r)) mod q

goal (1 subgoal):
 1. s1 = (x * y + x * (q - b) + (q - r)) mod q
[PROOF STEP]
by(metis distrib_left)
[PROOF STATE]
proof (state)
this:
s1 = (x * y + x * (q - b) + (q - r)) mod q

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1 = (x * y + x * (q - b) + (q - r)) mod q
[PROOF STEP]
have "s1 = (x*y + x*q - x*b + (q - r)) mod q"
[PROOF STATE]
proof (prove)
using this:
s1 = (x * y + x * (q - b) + (q - r)) mod q

goal (1 subgoal):
 1. s1 = (x * y + x * q - x * b + (q - r)) mod q
[PROOF STEP]
using distrib_left b diff_mult_distrib2
[PROOF STATE]
proof (prove)
using this:
s1 = (x * y + x * (q - b) + (q - r)) mod q
?a * (?b + ?c) = ?a * ?b + ?a * ?c
b < q
?k * (?m - ?n) = ?k * ?m - ?k * ?n

goal (1 subgoal):
 1. s1 = (x * y + x * q - x * b + (q - r)) mod q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s1 = (x * y + x * q - x * b + (q - r)) mod q

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1 = (x * y + x * q - x * b + (q - r)) mod q
[PROOF STEP]
have "[s1 = x*y + x*q - x*b + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
s1 = (x * y + x * q - x * b + (q - r)) mod q

goal (1 subgoal):
 1. [s1 = x * y + x * q - x * b + (q - r)] (mod q)
[PROOF STEP]
by(simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[s1 = x * y + x * q - x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[s1 = x * y + x * q - x * b + (q - r)] (mod q)
[PROOF STEP]
have "[s1 + x * b = x*y + x*q - x*b + x*b + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[s1 = x * y + x * q - x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. [s1 + x * b = x * y + x * q - x * b + x * b + (q - r)] (mod q)
[PROOF STEP]
by (metis add.commute add.left_commute cong_add_lcancel_nat)
[PROOF STATE]
proof (state)
this:
[s1 + x * b = x * y + x * q - x * b + x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[s1 + x * b = x * y + x * q - x * b + x * b + (q - r)] (mod q)
[PROOF STEP]
have "[s1 + x*b = x*y + x*q + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[s1 + x * b = x * y + x * q - x * b + x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. [s1 + x * b = x * y + x * q + (q - r)] (mod q)
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
[s1 + x * b = x * y + x * q - x * b + x * b + (q - r)] (mod q)
b < q

goal (1 subgoal):
 1. [s1 + x * b = x * y + x * q + (q - r)] (mod q)
[PROOF STEP]
by (simp add: algebra_simps)
        (metis add_diff_inverse_nat diff_diff_left diff_mult_distrib2 less_imp_add_positive mult.commute not_add_less1 zero_less_diff)
[PROOF STATE]
proof (state)
this:
[s1 + x * b = x * y + x * q + (q - r)] (mod q)

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[s1 + x * b = x * y + x * q + (q - r)] (mod q)
[PROOF STEP]
have s1_xb: "[s1 + x*b = q + x*y + x*q + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[s1 + x * b = x * y + x * q + (q - r)] (mod q)

goal (1 subgoal):
 1. [s1 + x * b = q + x * y + x * q + (q - r)] (mod q)
[PROOF STEP]
by (smt mod_add_cong mod_add_self1 cong_def)
[PROOF STATE]
proof (state)
this:
[s1 + x * b = q + x * y + x * q + (q - r)] (mod q)

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[s1 + x * b = q + x * y + x * q + (q - r)] (mod q)
[PROOF STEP]
have "[x*b = q + x*y + x*q + (q - r) - s1] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[s1 + x * b = q + x * y + x * q + (q - r)] (mod q)

goal (1 subgoal):
 1. [x * b = q + x * y + x * q + (q - r) - s1] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [s1 + x * b = q + x * y + x * q + (q - r)] (mod q) \<Longrightarrow> [x * b = q + x * y + x * q + (q - r) - s1] (mod q)
[PROOF STEP]
have "q + x*y + x*q + (q - r) - s1 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q + x * y + x * q + (q - r) - s1
[PROOF STEP]
using s1_le_q
[PROOF STATE]
proof (prove)
using this:
s1 < q

goal (1 subgoal):
 1. 0 < q + x * y + x * q + (q - r) - s1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < q + x * y + x * q + (q - r) - s1

goal (1 subgoal):
 1. [s1 + x * b = q + x * y + x * q + (q - r)] (mod q) \<Longrightarrow> [x * b = q + x * y + x * q + (q - r) - s1] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < q + x * y + x * q + (q - r) - s1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < q + x * y + x * q + (q - r) - s1

goal (1 subgoal):
 1. [x * b = q + x * y + x * q + (q - r) - s1] (mod q)
[PROOF STEP]
by (metis add_diff_inverse_nat less_numeral_extra(3) s1_xb cong_add_lcancel_nat nat_diff_split)
[PROOF STATE]
proof (state)
this:
[x * b = q + x * y + x * q + (q - r) - s1] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[x * b = q + x * y + x * q + (q - r) - s1] (mod q)

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x * b = q + x * y + x * q + (q - r) - s1] (mod q)
[PROOF STEP]
have "[x*b = x*y + x*q + (q - r) + q - s1] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[x * b = q + x * y + x * q + (q - r) - s1] (mod q)

goal (1 subgoal):
 1. [x * b = x * y + x * q + (q - r) + q - s1] (mod q)
[PROOF STEP]
by (metis add.assoc add.commute)
[PROOF STATE]
proof (state)
this:
[x * b = x * y + x * q + (q - r) + q - s1] (mod q)

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x * b = x * y + x * q + (q - r) + q - s1] (mod q)
[PROOF STEP]
have "[x*b = x*y + (q - r) + q - s1] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[x * b = x * y + x * q + (q - r) + q - s1] (mod q)

goal (1 subgoal):
 1. [x * b = x * y + (q - r) + q - s1] (mod q)
[PROOF STEP]
by (smt Nat.add_diff_assoc cong_def less_imp_le_nat mod_mult_self1 s1_le_q semiring_normalization_rules(23))
[PROOF STATE]
proof (state)
this:
[x * b = x * y + (q - r) + q - s1] (mod q)

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[x * b = x * y + (q - r) + q - s1] (mod q)
[PROOF STEP]
have "(x*b) mod q = (x*y  + (q - r) + q - s1) mod q"
[PROOF STATE]
proof (prove)
using this:
[x * b = x * y + (q - r) + q - s1] (mod q)

goal (1 subgoal):
 1. x * b mod q = (x * y + (q - r) + q - s1) mod q
[PROOF STEP]
by(simp add: cong_def)
[PROOF STATE]
proof (state)
this:
x * b mod q = (x * y + (q - r) + q - s1) mod q

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x * b mod q = (x * y + (q - r) + q - s1) mod q
[PROOF STEP]
have "(x*b) mod q = (x*y  + (q - r) + (q - s1)) mod q"
[PROOF STATE]
proof (prove)
using this:
x * b mod q = (x * y + (q - r) + q - s1) mod q

goal (1 subgoal):
 1. x * b mod q = (x * y + (q - r) + (q - s1)) mod q
[PROOF STEP]
using add.assoc s1_le_q
[PROOF STATE]
proof (prove)
using this:
x * b mod q = (x * y + (q - r) + q - s1) mod q
?a + ?b + ?c = ?a + (?b + ?c)
s1 < q

goal (1 subgoal):
 1. x * b mod q = (x * y + (q - r) + (q - s1)) mod q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x * b mod q = (x * y + (q - r) + (q - s1)) mod q

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x * b mod q = (x * y + (q - r) + (q - s1)) mod q
[PROOF STEP]
have "(x*b) mod q = (x*y  + (q - s1) + (q - r)) mod q"
[PROOF STATE]
proof (prove)
using this:
x * b mod q = (x * y + (q - r) + (q - s1)) mod q

goal (1 subgoal):
 1. x * b mod q = (x * y + (q - s1) + (q - r)) mod q
[PROOF STEP]
using add.commute
[PROOF STATE]
proof (prove)
using this:
x * b mod q = (x * y + (q - r) + (q - s1)) mod q
?a + ?b = ?b + ?a

goal (1 subgoal):
 1. x * b mod q = (x * y + (q - s1) + (q - r)) mod q
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
x * b mod q = (x * y + (q - s1) + (q - r)) mod q

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x * b mod q = (x * y + (q - s1) + (q - r)) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x * b mod q = (x * y + (q - s1) + (q - r)) mod q

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
using s2
[PROOF STATE]
proof (prove)
using this:
x * b mod q = (x * y + (q - s1) + (q - r)) mod q
s2 = (x * y + (q - s1)) mod q

goal (1 subgoal):
 1. x * b mod q = (s2 + (q - r)) mod q
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
x * b mod q = (s2 + (q - r)) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x * b mod q = (s2 + (q - r)) mod q

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
have "d2 = (((e2 + q - x) mod q)*b + (q - r)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d2 = ((e2 + q - x) mod q * b + (q - r)) mod q
[PROOF STEP]
using d2
[PROOF STATE]
proof (prove)
using this:
d2 = ((e2 + q - x) mod q * b + (q - r)) mod q

goal (1 subgoal):
 1. d2 = ((e2 + q - x) mod q * b + (q - r)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d2 = ((e2 + q - x) mod q * b + (q - r)) mod q

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d2 = ((e2 + q - x) mod q * b + (q - r)) mod q
[PROOF STEP]
have "d2 = (((e2 + q - x))*b + (q - r)) mod q"
[PROOF STATE]
proof (prove)
using this:
d2 = ((e2 + q - x) mod q * b + (q - r)) mod q

goal (1 subgoal):
 1. d2 = ((e2 + q - x) * b + (q - r)) mod q
[PROOF STEP]
using mod_add_cong mod_mult_left_eq
[PROOF STATE]
proof (prove)
using this:
d2 = ((e2 + q - x) mod q * b + (q - r)) mod q
\<lbrakk>?a mod ?c = ?a' mod ?c; ?b mod ?c = ?b' mod ?c\<rbrakk> \<Longrightarrow> (?a + ?b) mod ?c = (?a' + ?b') mod ?c
?a mod ?c * ?b mod ?c = ?a * ?b mod ?c

goal (1 subgoal):
 1. d2 = ((e2 + q - x) * b + (q - r)) mod q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
d2 = ((e2 + q - x) * b + (q - r)) mod q

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d2 = ((e2 + q - x) * b + (q - r)) mod q
[PROOF STEP]
have "d2 = (e2*b + q*b - x*b + (q - r)) mod q"
[PROOF STATE]
proof (prove)
using this:
d2 = ((e2 + q - x) * b + (q - r)) mod q

goal (1 subgoal):
 1. d2 = (e2 * b + q * b - x * b + (q - r)) mod q
[PROOF STEP]
by (simp add: distrib_right diff_mult_distrib)
[PROOF STATE]
proof (state)
this:
d2 = (e2 * b + q * b - x * b + (q - r)) mod q

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d2 = (e2 * b + q * b - x * b + (q - r)) mod q
[PROOF STEP]
have a: "[d2 = e2*b + q*b - x*b + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
d2 = (e2 * b + q * b - x * b + (q - r)) mod q

goal (1 subgoal):
 1. [d2 = e2 * b + q * b - x * b + (q - r)] (mod q)
[PROOF STEP]
by(simp add: cong_def)
[PROOF STATE]
proof (state)
this:
[d2 = e2 * b + q * b - x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[d2 = e2 * b + q * b - x * b + (q - r)] (mod q)
[PROOF STEP]
have b:"[d2 = q + q + e2*b + q*b - x*b + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[d2 = e2 * b + q * b - x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [d2 = e2 * b + q * b - x * b + (q - r)] (mod q) \<Longrightarrow> [d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)
[PROOF STEP]
have "[e2*b + q*b - x*b + (q - r) = q + q + e2*b + q*b - x*b + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)
[PROOF STEP]
by (smt assms Nat.add_diff_assoc add.commute cong_def less_imp_le_nat mod_add_self2
          mult.commute nat_mult_le_cancel_disj semiring_normalization_rules(23))
[PROOF STATE]
proof (state)
this:
[e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = e2 * b + q * b - x * b + (q - r)] (mod q) \<Longrightarrow> [d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)
[PROOF STEP]
using cong_trans a
[PROOF STATE]
proof (prove)
using this:
[e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)
[d2 = e2 * b + q * b - x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)
[PROOF STEP]
have "[d2 = q + q + e2*b + q*b - (x*b) mod q + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q) \<Longrightarrow> [d2 = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
have "[q + q + e2*b + q*b - (x*b)  + (q - r) = q + q + e2*b + q*b - (x*b) mod q + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
proof(cases "b = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b = 0 \<Longrightarrow> [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
 2. b \<noteq> 0 \<Longrightarrow> [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b = 0

goal (2 subgoals):
 1. b = 0 \<Longrightarrow> [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
 2. b \<noteq> 0 \<Longrightarrow> [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b = 0

goal (1 subgoal):
 1. [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
b \<noteq> 0

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
have "q*b - (x*b) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q * b - x * b
[PROOF STEP]
using False x
[PROOF STATE]
proof (prove)
using this:
b \<noteq> 0
x < q

goal (1 subgoal):
 1. 0 < q * b - x * b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < q * b - x * b

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < q * b - x * b
[PROOF STEP]
have 1: "q + q + e2*b + q*b - (x*b) > 0"
[PROOF STATE]
proof (prove)
using this:
0 < q * b - x * b

goal (1 subgoal):
 1. 0 < q + q + e2 * b + q * b - x * b
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
0 < q + q + e2 * b + q * b - x * b

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < q + q + e2 * b + q * b - x * b
[PROOF STEP]
have 2:"q + q + e2*b + q*b - (x*b) mod q > 0"
[PROOF STATE]
proof (prove)
using this:
0 < q + q + e2 * b + q * b - x * b

goal (1 subgoal):
 1. 0 < q + q + e2 * b + q * b - x * b mod q
[PROOF STEP]
by (simp add: q_gt_0 trans_less_add1)
[PROOF STATE]
proof (state)
this:
0 < q + q + e2 * b + q * b - x * b mod q

goal (1 subgoal):
 1. b \<noteq> 0 \<Longrightarrow> [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < q + q + e2 * b + q * b - x * b mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < q + q + e2 * b + q * b - x * b mod q

goal (1 subgoal):
 1. [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
using 1 2 minus_mod_cancel
[PROOF STATE]
proof (prove)
using this:
0 < q + q + e2 * b + q * b - x * b mod q
0 < q + q + e2 * b + q * b - x * b
0 < q + q + e2 * b + q * b - x * b mod q
\<lbrakk>0 < ?a - ?b; 0 < ?a - ?b mod q\<rbrakk> \<Longrightarrow> [?a - ?b + ?c = ?a - ?b mod q + ?c] (mod q)

goal (1 subgoal):
 1. [q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q) \<Longrightarrow> [d2 = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
using cong_trans b
[PROOF STATE]
proof (prove)
using this:
[q + q + e2 * b + q * b - x * b + (q - r) = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)
[d2 = q + q + e2 * b + q * b - x * b + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[d2 = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[d2 = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[d2 = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
[PROOF STEP]
have c: "[d2 = q + q + e2*b + q*b - (s2  + (q - r)) mod q + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[d2 = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r)] (mod q)
[PROOF STEP]
using xb
[PROOF STATE]
proof (prove)
using this:
[d2 = q + q + e2 * b + q * b - x * b mod q + (q - r)] (mod q)
x * b mod q = (s2 + (q - r)) mod q

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r)] (mod q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[d2 = q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r)] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[d2 = q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r)] (mod q)
[PROOF STEP]
have "[d2 = q + q + e2*b + q*b - (s2  + (q - r)) + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[d2 = q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r)] (mod q) \<Longrightarrow> [d2 = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
have "[q + q + e2*b + q*b - (s2  + (q - r)) mod q + (q - r) = q + q + e2*b + q*b - (s2  + (q - r)) + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
have "q + q + e2*b + q*b - (s2  + (q - r)) mod q > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q + q + e2 * b + q * b - (s2 + (q - r)) mod q
[PROOF STEP]
by (metis diff_is_0_eq gr0I le_less_trans mod_less_divisor not_add_less1 q_gt_0 semiring_normalization_rules(23) trans_less_add2)
[PROOF STATE]
proof (state)
this:
0 < q + q + e2 * b + q * b - (s2 + (q - r)) mod q

goal (1 subgoal):
 1. [q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < q + q + e2 * b + q * b - (s2 + (q - r)) mod q

goal (1 subgoal):
 1. [q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
have"q + q + e2*b + q*b - (s2  + (q - r)) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q + q + e2 * b + q * b - (s2 + (q - r))
[PROOF STEP]
using s2_le_q
[PROOF STATE]
proof (prove)
using this:
s2 < q

goal (1 subgoal):
 1. 0 < q + q + e2 * b + q * b - (s2 + (q - r))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < q + q + e2 * b + q * b - (s2 + (q - r))

goal (1 subgoal):
 1. [q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < q + q + e2 * b + q * b - (s2 + (q - r)) mod q
0 < q + q + e2 * b + q * b - (s2 + (q - r))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < q + q + e2 * b + q * b - (s2 + (q - r)) mod q
0 < q + q + e2 * b + q * b - (s2 + (q - r))

goal (1 subgoal):
 1. [q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
using minus_mod_cancel cong_sym
[PROOF STATE]
proof (prove)
using this:
0 < q + q + e2 * b + q * b - (s2 + (q - r)) mod q
0 < q + q + e2 * b + q * b - (s2 + (q - r))
\<lbrakk>0 < ?a - ?b; 0 < ?a - ?b mod q\<rbrakk> \<Longrightarrow> [?a - ?b + ?c = ?a - ?b mod q + ?c] (mod q)
[?b = ?c] (mod ?a) \<Longrightarrow> [?c = ?b] (mod ?a)

goal (1 subgoal):
 1. [q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r)] (mod q) \<Longrightarrow> [d2 = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
using cong_trans c
[PROOF STATE]
proof (prove)
using this:
[q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r) = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)
[d2 = q + q + e2 * b + q * b - (s2 + (q - r)) mod q + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[d2 = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[d2 = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[d2 = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)
[PROOF STEP]
have d: "[d2 = q + q + e2*b + q*b - s2 - (q - r) + (q - r)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[d2 = q + q + e2 * b + q * b - (s2 + (q - r)) + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - s2 - (q - r) + (q - r)] (mod q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[d2 = q + q + e2 * b + q * b - s2 - (q - r) + (q - r)] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[d2 = q + q + e2 * b + q * b - s2 - (q - r) + (q - r)] (mod q)
[PROOF STEP]
have "[d2 = q + q + e2*b + q*b - s2 ] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[d2 = q + q + e2 * b + q * b - s2 - (q - r) + (q - r)] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - s2] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - s2 - (q - r) + (q - r)] (mod q) \<Longrightarrow> [d2 = q + q + e2 * b + q * b - s2] (mod q)
[PROOF STEP]
have "q + q + e2*b + q*b - s2 - (q - r) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q + q + e2 * b + q * b - s2 - (q - r)
[PROOF STEP]
using s2_le_q
[PROOF STATE]
proof (prove)
using this:
s2 < q

goal (1 subgoal):
 1. 0 < q + q + e2 * b + q * b - s2 - (q - r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < q + q + e2 * b + q * b - s2 - (q - r)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - s2 - (q - r) + (q - r)] (mod q) \<Longrightarrow> [d2 = q + q + e2 * b + q * b - s2] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < q + q + e2 * b + q * b - s2 - (q - r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < q + q + e2 * b + q * b - s2 - (q - r)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - s2] (mod q)
[PROOF STEP]
using d cong_trans
[PROOF STATE]
proof (prove)
using this:
0 < q + q + e2 * b + q * b - s2 - (q - r)
[d2 = q + q + e2 * b + q * b - s2 - (q - r) + (q - r)] (mod q)
\<lbrakk>[?b = ?c] (mod ?a); [?c = ?d] (mod ?a)\<rbrakk> \<Longrightarrow> [?b = ?d] (mod ?a)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b + q * b - s2] (mod q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[d2 = q + q + e2 * b + q * b - s2] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[d2 = q + q + e2 * b + q * b - s2] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[d2 = q + q + e2 * b + q * b - s2] (mod q)
[PROOF STEP]
have "[d2 = q + q + e2*b - s2] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[d2 = q + q + e2 * b + q * b - s2] (mod q)

goal (1 subgoal):
 1. [d2 = q + q + e2 * b - s2] (mod q)
[PROOF STEP]
by (smt Nat.add_diff_assoc2 cong_def less_imp_le_nat mod_mult_self1 mult.commute s2_le_q semiring_normalization_rules(23) trans_less_add2)
[PROOF STATE]
proof (state)
this:
[d2 = q + q + e2 * b - s2] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[d2 = q + q + e2 * b - s2] (mod q)
[PROOF STEP]
have "[d2 = q + e2*b + q - s2] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[d2 = q + q + e2 * b - s2] (mod q)

goal (1 subgoal):
 1. [d2 = q + e2 * b + q - s2] (mod q)
[PROOF STEP]
by(simp add: add.commute add.assoc)
[PROOF STATE]
proof (state)
this:
[d2 = q + e2 * b + q - s2] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[d2 = q + e2 * b + q - s2] (mod q)
[PROOF STEP]
have "[d2 = e2*b + q - s2] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[d2 = q + e2 * b + q - s2] (mod q)

goal (1 subgoal):
 1. [d2 = e2 * b + q - s2] (mod q)
[PROOF STEP]
by (smt Nat.add_diff_assoc2 add.commute cong_def less_imp_le_nat mod_add_self2 s2_le_q trans_less_add2)
[PROOF STATE]
proof (state)
this:
[d2 = e2 * b + q - s2] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[d2 = e2 * b + q - s2] (mod q)
[PROOF STEP]
have "[d2 = e2*b + (q - s2)] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[d2 = e2 * b + q - s2] (mod q)

goal (1 subgoal):
 1. [d2 = e2 * b + (q - s2)] (mod q)
[PROOF STEP]
by (simp add: less_imp_le_nat s2_le_q)
[PROOF STATE]
proof (state)
this:
[d2 = e2 * b + (q - s2)] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[d2 = e2 * b + (q - s2)] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[d2 = e2 * b + (q - s2)] (mod q)

goal (1 subgoal):
 1. d2 = (e2 * b + (q - s2)) mod q
[PROOF STEP]
by(simp add: cong_def d2)
[PROOF STATE]
proof (state)
this:
d2 = (e2 * b + (q - s2)) mod q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma d2_P2:
  assumes x: "x < q" and y: "y < q" and r: "b < q" and b: "e2 < q" and e2: "r < q"
  shows "((y, b, ((e2 + q - x) mod q * b + q - r) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) =
                ((y, b, (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q,
                      (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((y, b, ((e2 + q - x) mod q * b + q - r) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((y, b, (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((y, b, ((e2 + q - x) mod q * b + q - r) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((y, b, (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)
[PROOF STEP]
have "((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q"
    (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q
[PROOF STEP]
have d2: "(((e2 + q - x) mod q)*b + (q - r)) mod q  = (e2*b + (q - ((x*y + (q - ((x*((y + (q - b)) mod q) + (q - r)) mod q))) mod q))) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + (q - r)) mod q = (e2 * b + (q - (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q)) mod q
[PROOF STEP]
using assms d2
[PROOF STATE]
proof (prove)
using this:
x < q
y < q
b < q
e2 < q
r < q
\<lbrakk>?d2.0 = ((?e2.0 + q - ?x) mod q * ?b + (q - ?r)) mod q; ?s1.0 = (?x * ((?y + (q - ?b)) mod q) + (q - ?r)) mod q; ?s2.0 = (?x * ?y + (q - ?s1.0)) mod q; ?x < q; ?y < q; ?r < q; ?b < q; ?e2.0 < q\<rbrakk> \<Longrightarrow> ?d2.0 = (?e2.0 * ?b + (q - ?s2.0)) mod q

goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + (q - r)) mod q = (e2 * b + (q - (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q)) mod q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((e2 + q - x) mod q * b + (q - r)) mod q = (e2 * b + (q - (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q)) mod q

goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q
[PROOF STEP]
have "?lhs = (((e2 + q - x) mod q)*b + (q - r)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + q - r) mod q = ((e2 + q - x) mod q * b + (q - r)) mod q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x < q
y < q
b < q
e2 < q
r < q

goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + q - r) mod q = ((e2 + q - x) mod q * b + (q - r)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((e2 + q - x) mod q * b + q - r) mod q = ((e2 + q - x) mod q * b + (q - r)) mod q

goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((e2 + q - x) mod q * b + q - r) mod q = ((e2 + q - x) mod q * b + (q - r)) mod q

goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q
[PROOF STEP]
have "?rhs = (e2*b + (q - ((x*y + (q - ((x*((y + (q - b)) mod q) + (q - r)) mod q))) mod q))) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q = (e2 * b + (q - (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q)) mod q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x < q
y < q
b < q
e2 < q
r < q

goal (1 subgoal):
 1. (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q = (e2 * b + (q - (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q)) mod q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q = (e2 * b + (q - (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q)) mod q

goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((e2 + q - x) mod q * b + q - r) mod q = ((e2 + q - x) mod q * b + (q - r)) mod q
(e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q = (e2 * b + (q - (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q)) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((e2 + q - x) mod q * b + q - r) mod q = ((e2 + q - x) mod q * b + (q - r)) mod q
(e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q = (e2 * b + (q - (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q)) mod q

goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q
[PROOF STEP]
using assms d2
[PROOF STATE]
proof (prove)
using this:
((e2 + q - x) mod q * b + q - r) mod q = ((e2 + q - x) mod q * b + (q - r)) mod q
(e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q = (e2 * b + (q - (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q)) mod q
x < q
y < q
b < q
e2 < q
r < q
((e2 + q - x) mod q * b + (q - r)) mod q = (e2 * b + (q - (x * y + (q - (x * ((y + (q - b)) mod q) + (q - r)) mod q)) mod q)) mod q

goal (1 subgoal):
 1. ((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q

goal (1 subgoal):
 1. ((y, b, ((e2 + q - x) mod q * b + q - r) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((y, b, (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q

goal (1 subgoal):
 1. ((y, b, ((e2 + q - x) mod q * b + q - r) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((y, b, (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((e2 + q - x) mod q * b + q - r) mod q = (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q
x < q
y < q
b < q
e2 < q
r < q

goal (1 subgoal):
 1. ((y, b, ((e2 + q - x) mod q * b + q - r) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((y, b, (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
((y, b, ((e2 + q - x) mod q * b + q - r) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) = ((y, b, (e2 * b + q - (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q) mod q, e2), (x * ((y + q - b) mod q) + q - r) mod q, (x * y + q - (x * ((y + q - b) mod q) + q - r) mod q) mod q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma s1:
  assumes s2: "s2 = (x*y + q - s1) mod q"
    and x: "x < q"
    and y: "y < q"
    and s1: "s1 < q"
  shows "s1 = (x*y + q - s2) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 = (x * y + q - s2) mod q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s1 = (x * y + q - s2) mod q
[PROOF STEP]
have s2_le_q:"s2 < q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2 < q
[PROOF STEP]
using s2 q_gt_0
[PROOF STATE]
proof (prove)
using this:
s2 = (x * y + q - s1) mod q
0 < q

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

goal (1 subgoal):
 1. s1 = (x * y + q - s2) mod q
[PROOF STEP]
have "[s2 = x*y + q - s1] (mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [s2 = x * y + q - s1] (mod q)
[PROOF STEP]
by(simp add: cong_def s2)
[PROOF STATE]
proof (state)
this:
[s2 = x * y + q - s1] (mod q)

goal (1 subgoal):
 1. s1 = (x * y + q - s2) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[s2 = x * y + q - s1] (mod q)
[PROOF STEP]
have "[s2 = x*y + q - s1] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[s2 = x * y + q - s1] (mod q)

goal (1 subgoal):
 1. [s2 = x * y + q - s1] (mod q)
[PROOF STEP]
using add.assoc
[PROOF STATE]
proof (prove)
using this:
[s2 = x * y + q - s1] (mod q)
?a + ?b + ?c = ?a + (?b + ?c)

goal (1 subgoal):
 1. [s2 = x * y + q - s1] (mod q)
[PROOF STEP]
by (simp add: less_imp_le_nat s1)
[PROOF STATE]
proof (state)
this:
[s2 = x * y + q - s1] (mod q)

goal (1 subgoal):
 1. s1 = (x * y + q - s2) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[s2 = x * y + q - s1] (mod q)
[PROOF STEP]
have s1_s2: "[s2 + s1 = x*y + q] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[s2 = x * y + q - s1] (mod q)

goal (1 subgoal):
 1. [s2 + s1 = x * y + q] (mod q)
[PROOF STEP]
by (metis (mono_tags, lifting) cong_def le_add2 le_add_diff_inverse2 le_trans mod_add_left_eq order.strict_implies_order s1)
[PROOF STATE]
proof (state)
this:
[s2 + s1 = x * y + q] (mod q)

goal (1 subgoal):
 1. s1 = (x * y + q - s2) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[s2 + s1 = x * y + q] (mod q)
[PROOF STEP]
have "[s1 = x*y + q - s2] (mod q)"
[PROOF STATE]
proof (prove)
using this:
[s2 + s1 = x * y + q] (mod q)

goal (1 subgoal):
 1. [s1 = x * y + q - s2] (mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [s2 + s1 = x * y + q] (mod q) \<Longrightarrow> [s1 = x * y + q - s2] (mod q)
[PROOF STEP]
have "x*y + q - s2 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x * y + q - s2
[PROOF STEP]
using s2_le_q
[PROOF STATE]
proof (prove)
using this:
s2 < q

goal (1 subgoal):
 1. 0 < x * y + q - s2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < x * y + q - s2

goal (1 subgoal):
 1. [s2 + s1 = x * y + q] (mod q) \<Longrightarrow> [s1 = x * y + q - s2] (mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < x * y + q - s2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < x * y + q - s2

goal (1 subgoal):
 1. [s1 = x * y + q - s2] (mod q)
[PROOF STEP]
by (metis s1_s2 add_diff_cancel_left' cong_diff_nat cong_def le_add1 less_imp_le_nat zero_less_diff)
[PROOF STATE]
proof (state)
this:
[s1 = x * y + q - s2] (mod q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[s1 = x * y + q - s2] (mod q)

goal (1 subgoal):
 1. s1 = (x * y + q - s2) mod q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[s1 = x * y + q - s2] (mod q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[s1 = x * y + q - s2] (mod q)

goal (1 subgoal):
 1. s1 = (x * y + q - s2) mod q
[PROOF STEP]
by(simp add: cong_def s1)
[PROOF STATE]
proof (state)
this:
s1 = (x * y + q - s2) mod q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma s1_P2:
  assumes x: "x < q"
    and y: "y < q"
    and "b < q"
    and "e2 < q"
    and "r < q"
    and "s1 < q"
  shows "((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), r, (x * y + q - r) mod q) =
                ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), (x * y + q - (x * y + q - r) mod q) mod q, (x * y + q - r) mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), r, (x * y + q - r) mod q) = ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), (x * y + q - (x * y + q - r) mod q) mod q, (x * y + q - r) mod q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), r, (x * y + q - r) mod q) = ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), (x * y + q - (x * y + q - r) mod q) mod q, (x * y + q - r) mod q)
[PROOF STEP]
have "s1 = (x*y + q - ((x*y + q - s1) mod q)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 = (x * y + q - (x * y + q - s1) mod q) mod q
[PROOF STEP]
using assms secure_mult.s1 secure_mult_axioms
[PROOF STATE]
proof (prove)
using this:
x < q
y < q
b < q
e2 < q
r < q
s1 < q
\<lbrakk>secure_mult ?q; ?s2.0 = (?x * ?y + ?q - ?s1.0) mod ?q; ?x < ?q; ?y < ?q; ?s1.0 < ?q\<rbrakk> \<Longrightarrow> ?s1.0 = (?x * ?y + ?q - ?s2.0) mod ?q
secure_mult q

goal (1 subgoal):
 1. s1 = (x * y + q - (x * y + q - s1) mod q) mod q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s1 = (x * y + q - (x * y + q - s1) mod q) mod q

goal (1 subgoal):
 1. ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), r, (x * y + q - r) mod q) = ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), (x * y + q - (x * y + q - r) mod q) mod q, (x * y + q - r) mod q)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s1 = (x * y + q - (x * y + q - s1) mod q) mod q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s1 = (x * y + q - (x * y + q - s1) mod q) mod q

goal (1 subgoal):
 1. ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), r, (x * y + q - r) mod q) = ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), (x * y + q - (x * y + q - r) mod q) mod q, (x * y + q - r) mod q)
[PROOF STEP]
using assms s1
[PROOF STATE]
proof (prove)
using this:
s1 = (x * y + q - (x * y + q - s1) mod q) mod q
x < q
y < q
b < q
e2 < q
r < q
s1 < q
\<lbrakk>?s2.0 = (?x * ?y + q - ?s1.0) mod q; ?x < q; ?y < q; ?s1.0 < q\<rbrakk> \<Longrightarrow> ?s1.0 = (?x * ?y + q - ?s2.0) mod q

goal (1 subgoal):
 1. ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), r, (x * y + q - r) mod q) = ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), (x * y + q - (x * y + q - r) mod q) mod q, (x * y + q - r) mod q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), r, (x * y + q - r) mod q) = ((y, b, (e2 * b + q - (x * y + q - r) mod q) mod q, e2), (x * y + q - (x * y + q - r) mod q) mod q, (x * y + q - r) mod q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem P2_security:
  assumes "x < q" "y < q"
  shows "sim_non_det_def.perfect_sec_P2 x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P2 x y
[PROOF STEP]
including monad_normalisation
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P2 x y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P2 x y
[PROOF STEP]
have "((funct x y) \<bind> (\<lambda> (s1',s2'). (sim_non_det_def.Ideal2 y x s2'))) = R2 x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
have "R2 x y = do {
      a :: nat \<leftarrow> sample_uniform q;
      b :: nat \<leftarrow> sample_uniform q;
      r :: nat \<leftarrow> sample_uniform q;
      let c1 = a;
      let d1 = r;
      let c2 = b;
      let d2 = ((a*b + (q - r)) mod q);
      let e2 = (x + c1) mod q;
      let e1 = (y + (q - c2)) mod q;
      let s1 = (x*e1 + (q - r)) mod q;
      let s2 = (e2 * c2 + (q - d2)) mod q;
      return_spmf ((y, c2, d2, e2), s1, s2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R2 x y = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - r)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((y, c2, d2, e2), s1, s2))))
[PROOF STEP]
by(simp add: R2_def TI_def Let_def)
[PROOF STATE]
proof (state)
this:
R2 x y = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - r)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((y, c2, d2, e2), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R2 x y = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - r)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((y, c2, d2, e2), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
have "... = do {
      a :: nat \<leftarrow> sample_uniform q;
      b :: nat \<leftarrow> sample_uniform q;
      r :: nat \<leftarrow> sample_uniform q;
      let c1 = a;
      let d1 = r;
      let c2 = b;
      let e2 = (x + c1) mod q;
      let d2 = ((((e2 + q - x) mod q)*b + (q - r)) mod q);
      let s1 = (x*((y + (q - c2)) mod q) + (q - r)) mod q;
      return_spmf ((y, c2, d2, e2), (s1, (x*y + (q - s1)) mod q))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - r)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((y, c2, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; e2 = (x + c1) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q))))
[PROOF STEP]
by(simp add: Let_def s1_s2_P2 assms c1_P2 cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - r)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((y, c2, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; e2 = (x + c1) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; d2 = (a * b + (q - r)) mod q; e2 = (x + c1) mod q; e1 = (y + (q - c2)) mod q; s1 = (x * e1 + (q - r)) mod q; s2 = (e2 * c2 + (q - d2)) mod q in return_spmf ((y, c2, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; e2 = (x + c1) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
have "... = do {
      b :: nat \<leftarrow> sample_uniform q;
      r :: nat \<leftarrow> sample_uniform q;
      let d1 = r;
      let c2 = b;
      e2 \<leftarrow> map_spmf (\<lambda> c1. (x + c1) mod q) (sample_uniform q);
      let d2 = ((((e2 + q - x) mod q)*b + (q - r)) mod q);
      let s1 = (x*((y + (q - c2)) mod q) + (q - r)) mod q;
      return_spmf ((y, c2, d2, e2), s1, (x*y + (q - s1)) mod q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; e2 = (x + c1) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in map_spmf (\<lambda>c1. (x + c1) mod q) (sample_uniform q) \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q))))
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; e2 = (x + c1) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in map_spmf (\<lambda>c1. (x + c1) mod q) (sample_uniform q) \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>a. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let c1 = a; d1 = r; c2 = b; e2 = (x + c1) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in map_spmf (\<lambda>c1. (x + c1) mod q) (sample_uniform q) \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
have "... = do {
      b :: nat \<leftarrow> sample_uniform q;
      r :: nat \<leftarrow> sample_uniform q;
      let d1 = r;
      let c2 = b;
      e2 \<leftarrow> sample_uniform q;
      let d2 = (((e2 + q - x) mod q)*b + (q - r)) mod q;
      let s1 = (x*((y + (q - c2)) mod q) + (q - r)) mod q;
      return_spmf ((y, c2, d2, e2), s1, (x*y + (q - s1)) mod q)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in map_spmf (\<lambda>c1. (x + c1) mod q) (sample_uniform q) \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in sample_uniform q \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q))))
[PROOF STEP]
by(simp add: samp_uni_plus_one_time_pad)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in map_spmf (\<lambda>c1. (x + c1) mod q) (sample_uniform q) \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in sample_uniform q \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in map_spmf (\<lambda>c1. (x + c1) mod q) (sample_uniform q) \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in sample_uniform q \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
have "... = do {
      b :: nat \<leftarrow> sample_uniform q;
      r :: nat \<leftarrow> sample_uniform q;
      e2 \<leftarrow> sample_uniform q;
      let s1 = (x*((y + (q - b)) mod q) + (q - r)) mod q;
      let s2 = (x*y + (q - s1)) mod q;
      let d2 = (((e2 + q - x) mod q)*b + (q - r)) mod q;
      return_spmf ((y, b, d2, e2), s1, s2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in sample_uniform q \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in sample_uniform q \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. let d1 = r; c2 = b in sample_uniform q \<bind> (\<lambda>e2. let d2 = ((e2 + q - x) mod q * b + (q - r)) mod q; s1 = (x * ((y + (q - c2)) mod q) + (q - r)) mod q in return_spmf ((y, c2, d2, e2), s1, (x * y + (q - s1)) mod q)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
have "... = do {
      b :: nat \<leftarrow> sample_uniform q;
      r :: nat \<leftarrow> sample_uniform q;
      e2 \<leftarrow> sample_uniform q;
      let s1 = (x*((y + (q - b)) mod q) + (q - r)) mod q;
      let s2 = (x*y + (q - s1)) mod q;
      let d2 = (e2*b + (q - s2)) mod q;
      return_spmf ((y, b, d2, e2), s1, s2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))
[PROOF STEP]
by(simp add: d2_P2 assms Let_def cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = ((e2 + q - x) mod q * b + (q - r)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
have "... = do {
      b :: nat \<leftarrow> sample_uniform q;
      e2 \<leftarrow> sample_uniform q;
      s1 \<leftarrow> map_spmf (\<lambda> r. (x*((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q);
      let s2 = (x*y + (q - s1)) mod q;
      let d2 = (e2*b + (q - s2)) mod q;
      return_spmf ((y, b, d2, e2), s1, s2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))
[PROOF STEP]
by(simp add: bind_map_spmf o_def Let_def)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>r. sample_uniform q \<bind> (\<lambda>e2. let s1 = (x * ((y + (q - b)) mod q) + (q - r)) mod q; s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
have "... = do {
      b :: nat \<leftarrow> sample_uniform q;
      e2 \<leftarrow> sample_uniform q;
      s1 \<leftarrow> sample_uniform q;
      let s2 = (x*y + (q - s1)) mod q;
      let d2 = (e2*b + (q - s2)) mod q;
      return_spmf ((y, b, d2, e2), s1, s2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))
[PROOF STEP]
by(simp add: samp_uni_minus_one_time_pad)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. map_spmf (\<lambda>r. (x * ((y + (q - b)) mod q) + (q - r)) mod q) (sample_uniform q) \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
have "... = do {
      b :: nat \<leftarrow> sample_uniform q;
      e2 \<leftarrow> sample_uniform q;
      s1 \<leftarrow> sample_uniform q;
      let s2 = (x*y + (q - s1)) mod q;
      let d2 = (e2*b + (q - s2)) mod q;
      return_spmf ((y, b, d2, e2), (x*y + (q - s2)) mod q, s2)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), (x * y + (q - s2)) mod q, s2))))
[PROOF STEP]
by(simp add: s1_P2 assms Let_def cong: bind_spmf_cong_simp)
[PROOF STATE]
proof (state)
this:
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), (x * y + (q - s2)) mod q, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R2 x y = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), (x * y + (q - s2)) mod q, s2))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R2 x y = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2))))
sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), s1, s2)))) = sample_uniform q \<bind> (\<lambda>b. sample_uniform q \<bind> (\<lambda>e2. sample_uniform q \<bind> (\<lambda>s1. let s2 = (x * y + (q - s1)) mod q; d2 = (e2 * b + (q - s2)) mod q in return_spmf ((y, b, d2, e2), (x * y + (q - s2)) mod q, s2))))

goal (1 subgoal):
 1. funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
by(simp add: funct_def Let_def sim_non_det_def.Ideal2_def Out2_def S2_def R2_def)
[PROOF STATE]
proof (state)
this:
funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y

goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P2 x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
funct x y \<bind> (\<lambda>(s1', s2'). local.sim_non_det_def.Ideal2 y x s2') = R2 x y

goal (1 subgoal):
 1. local.sim_non_det_def.perfect_sec_P2 x y
[PROOF STEP]
by(simp add: sim_non_det_def.perfect_sec_P2_def)
[PROOF STATE]
proof (state)
this:
local.sim_non_det_def.perfect_sec_P2 x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma s1_s2_P1:  assumes "x < q" "xa < q" "xb < q" "xc < q" "y < q"
  shows "((x, xa, xb, (y + q - xc) mod q), (x * ((y + q - xc) mod q) + q - xb) mod q, ((x + xa) mod q * xc + q - (xa * xc + q - xb) mod q) mod q) =
         ((x, xa, xb, (y + q - xc) mod q), (x * ((y + q - xc) mod q) + q - xb) mod q, (x * y + q - (x * ((y + q - xc) mod q) + q - xb) mod q) mod q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, xa, xb, (y + q - xc) mod q), (x * ((y + q - xc) mod q) + q - xb) mod q, ((x + xa) mod q * xc + q - (xa * xc + q - xb) mod q) mod q) = ((x, xa, xb, (y + q - xc) mod q), (x * ((y + q - xc) mod q) + q - xb) mod q, (x * y + q - (x * ((y + q - xc) mod q) + q - xb) mod q) mod q)
[PROOF STEP]
using assms s1_s2
[PROOF STATE]
proof (prove)
using this:
x < q
xa < q
xb < q
xc < q
y < q
\<lbrakk>?x < q; ?a < q; ?b < q; ?r < q; ?y < q\<rbrakk> \<Longrightarrow> ((?x + ?a) mod q * ?b + q - (?a * ?b + q - ?r) mod q) mod q = (?x * ?y + q - (?x * ((?y + q - ?b) mod q) + q - ?r) mod q) mod q

goal (1 subgoal):
 1. ((x, xa, xb, (y + q - xc) mod q), (x * ((y + q - xc) mod q) + q - xb) mod q, ((x + xa) mod q * xc + q - (xa * xc + q - xb) mod q) mod q) = ((x, xa, xb, (y + q - xc) mod q), (x * ((y + q - xc) mod q) + q - xb) mod q, (x * y + q - (x * ((y + q - xc) mod q) + q - xb) mod q) mod q)
[PROOF STEP]
by metis


[STATEMENT]
lemma mod_minus: assumes "a - b > 0" and "c - d > 0"
  shows "(a - b + (c - d mod q)) mod q = (a - b + (c - d)) mod q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a - b + (c - d mod q)) mod q = (a - b + (c - d)) mod q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < a - b
0 < c - d

goal (1 subgoal):
 1. (a - b + (c - d mod q)) mod q = (a - b + (c - d)) mod q
[PROOF STEP]
by (metis cong_def minus_mod mod_add_right_eq zero_less_diff)