[STATEMENT]
lemma length_helper: assumes p: "prime p" and q: "prime q" and x: "(length (nat_to_bv (p * q)) - Suc 0) mod 8 ~= 0" and mgf: "(MGF (sha1 (generate_M' (sha1 m) salt))
  (length
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt))))))) ~= []"
  and len: "length (sha1 M) + sLen + 16 \<le> (length (nat_to_bv (p * q))) - Suc 0"
  shows "length
  (remzero
  (maskedDB_zero
  (bvxor
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt)))))
  (MGF (sha1 (generate_M' (sha1 m) salt))
  (length
  (generate_DB
  (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
  (length (sha1 (generate_M' (sha1 m) salt))))))))
  (length (nat_to_bv (p * q)) - Suc 0) @
  sha1 (generate_M' (sha1 m) salt) @ BC))
  < length (nat_to_bv (p * q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
from mgf
[PROOF STATE]
proof (chain)
picking this:
MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) \<noteq> []
[PROOF STEP]
have round: "168 <= roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8"
[PROOF STATE]
proof (prove)
using this:
MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) \<noteq> []

goal (1 subgoal):
 1. 168 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8
[PROOF STEP]
proof (simp only: sha1len sLen_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) 160))) \<noteq> [] \<Longrightarrow> 168 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8
[PROOF STEP]
from len
[PROOF STATE]
proof (chain)
picking this:
length (sha1 M) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
have "160 + sLen +16 \<le> length (nat_to_bv (p * q)) - Suc 0"
[PROOF STATE]
proof (prove)
using this:
length (sha1 M) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. 160 + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
by (simp add: sha1len)
[PROOF STATE]
proof (state)
this:
160 + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) 160))) \<noteq> [] \<Longrightarrow> 168 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
160 + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
have len1: "176 <= length (nat_to_bv (p * q)) - Suc 0"
[PROOF STATE]
proof (prove)
using this:
160 + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. 176 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
176 \<le> length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) 160))) \<noteq> [] \<Longrightarrow> 168 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8
[PROOF STEP]
have "length (nat_to_bv (p*q)) - Suc 0 <= (roundup (length (nat_to_bv (p * q)) - Suc 0) 8) * 8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (nat_to_bv (p * q)) - Suc 0 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8
[PROOF STEP]
unfolding roundup
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
proof (cases "(length (nat_to_bv (p*q)) - Suc 0) mod 8 = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
 2. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
assume len2: "(length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0"
[PROOF STATE]
proof (state)
this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0

goal (2 subgoals):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
 2. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0
[PROOF STEP]
have "(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = (length (nat_to_bv (p * q)) - Suc 0) div 8 * 8"
[PROOF STATE]
proof (prove)
using this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0

goal (1 subgoal):
 1. (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = (length (nat_to_bv (p * q)) - Suc 0) div 8 * 8
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = (length (nat_to_bv (p * q)) - Suc 0) div 8 * 8

goal (2 subgoals):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
 2. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = (length (nat_to_bv (p * q)) - Suc 0) div 8 * 8

goal (2 subgoals):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
 2. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
have "(length (nat_to_bv (p * q)) - Suc 0) div 8 * 8 = (length (nat_to_bv (p * q)) - Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (length (nat_to_bv (p * q)) - Suc 0) div 8 * 8 = length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
using len2
[PROOF STATE]
proof (prove)
using this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0

goal (1 subgoal):
 1. (length (nat_to_bv (p * q)) - Suc 0) div 8 * 8 = length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(length (nat_to_bv (p * q)) - Suc 0) div 8 * 8 = length (nat_to_bv (p * q)) - Suc 0

goal (2 subgoals):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
 2. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = (length (nat_to_bv (p * q)) - Suc 0) div 8 * 8
(length (nat_to_bv (p * q)) - Suc 0) div 8 * 8 = length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
show "length (nat_to_bv (p * q)) - Suc 0
        \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8"
[PROOF STATE]
proof (prove)
using this:
(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = (length (nat_to_bv (p * q)) - Suc 0) div 8 * 8
(length (nat_to_bv (p * q)) - Suc 0) div 8 * 8 = length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8

goal (1 subgoal):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
assume len2: "(length (nat_to_bv (p*q)) - Suc 0) mod 8 ~= 0"
[PROOF STATE]
proof (state)
this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0

goal (1 subgoal):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0
[PROOF STEP]
have "(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = ((length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8"
[PROOF STATE]
proof (prove)
using this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0

goal (1 subgoal):
 1. (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = ((length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = ((length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8

goal (1 subgoal):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = ((length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8

goal (1 subgoal):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
have "length (nat_to_bv (p*q)) - Suc 0 <= ((length (nat_to_bv (p*q)) - Suc 0) div 8 + 1)*8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (nat_to_bv (p * q)) - Suc 0 \<le> ((length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (nat_to_bv (p * q)) - Suc 0 \<le> ((length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8

goal (1 subgoal):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0 \<Longrightarrow> length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = ((length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
length (nat_to_bv (p * q)) - Suc 0 \<le> ((length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
show "length (nat_to_bv (p * q)) - Suc 0
        \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8"
[PROOF STATE]
proof (prove)
using this:
(if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8 = ((length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
length (nat_to_bv (p * q)) - Suc 0 \<le> ((length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8

goal (1 subgoal):
 1. length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (nat_to_bv (p * q)) - Suc 0 \<le> (if (length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0 then (length (nat_to_bv (p * q)) - Suc 0) div 8 else (length (nat_to_bv (p * q)) - Suc 0) div 8 + 1) * 8

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (nat_to_bv (p * q)) - Suc 0 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8

goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) 160))) \<noteq> [] \<Longrightarrow> 168 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (nat_to_bv (p * q)) - Suc 0 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8
[PROOF STEP]
show "168 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8"
[PROOF STATE]
proof (prove)
using this:
length (nat_to_bv (p * q)) - Suc 0 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8

goal (1 subgoal):
 1. 168 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8
[PROOF STEP]
using len1
[PROOF STATE]
proof (prove)
using this:
length (nat_to_bv (p * q)) - Suc 0 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8
176 \<le> length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. 168 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
168 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
168 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0
[PROOF STEP]
have a: "length
    (remzero
    (maskedDB_zero
    (bvxor
    (generate_DB
    (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
    (length (sha1 (generate_M' (sha1 m) salt)))))
    (MGF (sha1 (generate_M' (sha1 m) salt))
    (length
    (generate_DB
    (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
    (length (sha1 (generate_M' (sha1 m) salt))))))))
    (length (nat_to_bv (p * q)) - Suc 0) @
    sha1 (generate_M' (sha1 m) salt) @ BC)) <= length ((bvxor
    (generate_DB
    (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
    (length (sha1 (generate_M' (sha1 m) salt)))))
    (MGF (sha1 (generate_M' (sha1 m) salt))
    (length
    (generate_DB
    (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
    (length (sha1 (generate_M' (sha1 m) salt)))))))) @
    sha1 (generate_M' (sha1 m) salt) @ BC) - (8 - (length (nat_to_bv (p*q)) - Suc 0) mod 8)"
[PROOF STATE]
proof (prove)
using this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)
[PROOF STEP]
using length_bound and length_bound2
[PROOF STATE]
proof (prove)
using this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0
\<lbrakk>?emBits mod 8 \<noteq> 0; 8 \<le> length ?maskedDB\<rbrakk> \<Longrightarrow> length (remzero (maskedDB_zero ?maskedDB ?emBits @ ?a @ ?b)) \<le> length (?maskedDB @ ?a @ ?b) - (8 - ?emBits mod 8)
8 \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt))))) (MGF (sha1 (generate_M' (sha1 ?m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt))))))))

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
have b: " length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
             (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @
            sha1 (generate_M' (sha1 m) salt) @ BC) =  length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
             (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) +168"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168
[PROOF STEP]
using length_helper1
[PROOF STATE]
proof (prove)
using this:
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt))))) (MGF (sha1 (generate_M' (sha1 ?m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt))))))) @ sha1 (generate_M' (sha1 ?m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt))))) (MGF (sha1 (generate_M' (sha1 ?m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt)))))))) + 168

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
have c: "length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
           (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) =
            (roundup (length (nat_to_bv (p * q)) - Suc 0) 8) * 8 - 168"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
using p and q and length_helper2 and mgf and len
[PROOF STATE]
proof (prove)
using this:
prime p
prime q
\<lbrakk>prime ?p; prime ?q; MGF (sha1 (generate_M' (sha1 ?m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt)))))) \<noteq> []; length (sha1 ?M) + sLen + 16 \<le> length (nat_to_bv (?p * ?q)) - Suc 0\<rbrakk> \<Longrightarrow> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt))))) (MGF (sha1 (generate_M' (sha1 ?m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt)))))))) = roundup (length (nat_to_bv (?p * ?q)) - Suc 0) 8 * 8 - 168
MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) \<noteq> []
length (sha1 M) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
from a and b and c
[PROOF STATE]
proof (chain)
picking this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168
[PROOF STEP]
have " length (remzero (maskedDB_zero
                    (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
                      (MGF (sha1 (generate_M' (sha1 m) salt))
                        (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))))
                    (length (nat_to_bv (p * q)) - Suc 0) @
                   sha1 (generate_M' (sha1 m) salt) @ BC)) <=  roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168 +168 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)"
[PROOF STATE]
proof (prove)
using this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) @ sha1 (generate_M' (sha1 m) salt) @ BC) = length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) + 168
length (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168 + 168 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168 + 168 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168 + 168 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)
[PROOF STEP]
have "length (remzero (maskedDB_zero
                    (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))
                      (MGF (sha1 (generate_M' (sha1 m) salt))
                        (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))))
                    (length (nat_to_bv (p * q)) - Suc 0) @
                   sha1 (generate_M' (sha1 m) salt) @ BC)) <= roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)"
[PROOF STATE]
proof (prove)
using this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168 + 168 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)
[PROOF STEP]
using round
[PROOF STATE]
proof (prove)
using this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - 168 + 168 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)
168 \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
have "  roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8) = (length (nat_to_bv (p*q))-Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8) = length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
using x and emBits_roundup_cancel2
[PROOF STATE]
proof (prove)
using this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0
?emBits mod 8 \<noteq> 0 \<Longrightarrow> roundup ?emBits 8 * 8 - (8 - ?emBits mod 8) = ?emBits

goal (1 subgoal):
 1. roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8) = length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8) = length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8) = length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
have "0<length (nat_to_bv (p*q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length (nat_to_bv (p * q))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < length (nat_to_bv (p * q))
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
prime p
[PROOF STEP]
have s: "1<p"
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. 1 < p
[PROOF STEP]
by (simp add: prime_nat_iff)
[PROOF STATE]
proof (state)
this:
1 < p

goal (1 subgoal):
 1. 0 < length (nat_to_bv (p * q))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 < p

goal (1 subgoal):
 1. 0 < length (nat_to_bv (p * q))
[PROOF STEP]
from q
[PROOF STATE]
proof (chain)
picking this:
prime q
[PROOF STEP]
have "1<q"
[PROOF STATE]
proof (prove)
using this:
prime q

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

goal (1 subgoal):
 1. 0 < length (nat_to_bv (p * q))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 < p
1 < q
[PROOF STEP]
have "p<p*q"
[PROOF STATE]
proof (prove)
using this:
1 < p
1 < q

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

goal (1 subgoal):
 1. 0 < length (nat_to_bv (p * q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p < p * q
[PROOF STEP]
have "1<p*q"
[PROOF STATE]
proof (prove)
using this:
p < p * q

goal (1 subgoal):
 1. 1 < p * q
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
p < p * q
1 < p

goal (1 subgoal):
 1. 1 < p * q
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
1 < p * q

goal (1 subgoal):
 1. 0 < length (nat_to_bv (p * q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 < p * q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 < p * q

goal (1 subgoal):
 1. 0 < length (nat_to_bv (p * q))
[PROOF STEP]
using len_nat_to_bv_pos
[PROOF STATE]
proof (prove)
using this:
1 < p * q
1 < ?a \<Longrightarrow> 0 < length (nat_to_bv ?a)

goal (1 subgoal):
 1. 0 < length (nat_to_bv (p * q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < length (nat_to_bv (p * q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < length (nat_to_bv (p * q))

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)
roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8) = length (nat_to_bv (p * q)) - Suc 0
0 < length (nat_to_bv (p * q))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) \<le> roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8)
roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 - (8 - (length (nat_to_bv (p * q)) - Suc 0) mod 8) = length (nat_to_bv (p * q)) - Suc 0
0 < length (nat_to_bv (p * q))

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_emsapss_smaller_pq: "\<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 ~= 0\<rbrakk> \<Longrightarrow>  length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p*q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0\<rbrakk> \<Longrightarrow> length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0\<rbrakk> \<Longrightarrow> length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
assume a: "emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []"
[PROOF STATE]
proof (state)
this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0\<rbrakk> \<Longrightarrow> length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
assume p: "prime p" and q: "prime q"
[PROOF STATE]
proof (state)
this:
prime p
prime q

goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0\<rbrakk> \<Longrightarrow> length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
assume x: "(length (nat_to_bv (p * q)) - Suc 0) mod 8 ~= 0"
[PROOF STATE]
proof (state)
this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0\<rbrakk> \<Longrightarrow> length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
have b: " emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)= emsapss_encode_help1 (sha1 m)
    (length (nat_to_bv (p * q)) - Suc 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
proof (simp only: emsapss_encode_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (if 2 ^ 64 \<le> length m \<or> 2 ^ 32 * 160 < length (nat_to_bv (p * q)) - Suc 0 then [] else emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
[PROOF STEP]
show "(if ((2^64 \<le> length m) \<or> (2^32 * 160 < (length (nat_to_bv (p*q)) - Suc 0)))
      then []
      else (emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p*q))- Suc 0))) = (emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p*q)) - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []

goal (1 subgoal):
 1. (if 2 ^ 64 \<le> length m \<or> 2 ^ 32 * 160 < length (nat_to_bv (p * q)) - Suc 0 then [] else emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
by (auto simp add: emsapss_encode_def)
[PROOF STATE]
proof (state)
this:
(if 2 ^ 64 \<le> length m \<or> 2 ^ 32 * 160 < length (nat_to_bv (p * q)) - Suc 0 then [] else emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)

goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0\<rbrakk> \<Longrightarrow> length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
have c: "length (remzero (emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p*q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remzero (emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
proof (simp only: emsapss_encode_help1_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (remzero (if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
from a and b
[PROOF STATE]
proof (chain)
picking this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
have d: "(if ((length (nat_to_bv (p * q)) - Suc 0) < (length (sha1 m) + sLen + 16))
      then []
      else (emsapss_encode_help2 (generate_M' (sha1 m) salt)
      (length (nat_to_bv (p * q)) - Suc 0))) = (emsapss_encode_help2 ((generate_M' (sha1 m)) salt) (length (nat_to_bv (p*q)) - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)

goal (1 subgoal):
 1. (if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
by (auto simp add: emsapss_encode_def emsapss_encode_help1_def)
[PROOF STATE]
proof (state)
this:
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)

goal (1 subgoal):
 1. length (remzero (if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
from d
[PROOF STATE]
proof (chain)
picking this:
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
have len: "length (sha1 m) + sLen + 16 <= (length (nat_to_bv (p*q))) - Suc 0"
[PROOF STATE]
proof (prove)
using this:
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)

goal (1 subgoal):
 1. length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
proof (cases "length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0); length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16\<rbrakk> \<Longrightarrow> length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
 2. \<lbrakk>(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0); \<not> length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16\<rbrakk> \<Longrightarrow> length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
assume "length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16"
[PROOF STATE]
proof (state)
this:
length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16

goal (2 subgoals):
 1. \<lbrakk>(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0); length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16\<rbrakk> \<Longrightarrow> length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
 2. \<lbrakk>(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0); \<not> length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16\<rbrakk> \<Longrightarrow> length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16
[PROOF STEP]
have len1: "(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then []
      else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = []"
[PROOF STATE]
proof (prove)
using this:
length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16

goal (1 subgoal):
 1. (if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = []

goal (2 subgoals):
 1. \<lbrakk>(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0); length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16\<rbrakk> \<Longrightarrow> length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
 2. \<lbrakk>(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0); \<not> length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16\<rbrakk> \<Longrightarrow> length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
assume len2:  "(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then []
      else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) =
     emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)"
[PROOF STATE]
proof (state)
this:
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)

goal (2 subgoals):
 1. \<lbrakk>(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0); length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16\<rbrakk> \<Longrightarrow> length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
 2. \<lbrakk>(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0); \<not> length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16\<rbrakk> \<Longrightarrow> length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
from len1 and len2 and a and b
[PROOF STATE]
proof (chain)
picking this:
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = []
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
show "length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0"
[PROOF STATE]
proof (prove)
using this:
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = []
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)

goal (1 subgoal):
 1. length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
by (auto simp add: emsapss_encode_def emsapss_encode_help1_def)
[PROOF STATE]
proof (state)
this:
length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. \<lbrakk>(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0); \<not> length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16\<rbrakk> \<Longrightarrow> length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0); \<not> length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16\<rbrakk> \<Longrightarrow> length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
assume "\<not> length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16"
[PROOF STATE]
proof (state)
this:
\<not> length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16

goal (1 subgoal):
 1. \<lbrakk>(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0); \<not> length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16\<rbrakk> \<Longrightarrow> length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16
[PROOF STEP]
show "length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0"
[PROOF STATE]
proof (prove)
using this:
\<not> length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16

goal (1 subgoal):
 1. length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. length (remzero (if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
have e: "length (remzero (emsapss_encode_help2 (generate_M' (sha1 m) salt)
   (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remzero (emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
proof (simp only: emsapss_encode_help2_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (remzero (emsapss_encode_help3 (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
show "length
          (remzero
          (emsapss_encode_help3 (sha1 (generate_M' (sha1 m) salt))
          (length (nat_to_bv (p * q)) - Suc 0)))
          < length (nat_to_bv (p * q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remzero (emsapss_encode_help3 (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
proof (simp add: emsapss_encode_help3_def emsapss_encode_help4_def emsapss_encode_help5_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (remzero (emsapss_encode_help6 (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
show "length
            (remzero
            (emsapss_encode_help6
            (generate_DB
            (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
            (length (sha1 (generate_M' (sha1 m) salt)))))
            (MGF (sha1 (generate_M' (sha1 m) salt))
            (length
            (generate_DB
            (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
            (length (sha1 (generate_M' (sha1 m) salt)))))))
            (sha1 (generate_M' (sha1 m) salt))
            (length (nat_to_bv (p * q)) - Suc 0)))
            < length (nat_to_bv (p * q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remzero (emsapss_encode_help6 (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
proof (simp only: emsapss_encode_help6_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (remzero (if MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) = [] then [] else emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
from a and b and d
[PROOF STATE]
proof (chain)
picking this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
have mgf: "MGF (sha1 (generate_M' (sha1 m) salt))
              (length
              (generate_DB
              (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
              (length (sha1 (generate_M' (sha1 m) salt)))))) ~=
              []"
[PROOF STATE]
proof (prove)
using this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)

goal (1 subgoal):
 1. MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) \<noteq> []
[PROOF STEP]
by (auto simp add: emsapss_encode_def emsapss_encode_help1_def emsapss_encode_help2_def emsapss_encode_help3_def emsapss_encode_help4_def emsapss_encode_help5_def emsapss_encode_help6_def)
[PROOF STATE]
proof (state)
this:
MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) \<noteq> []

goal (1 subgoal):
 1. length (remzero (if MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) = [] then [] else emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
from a and b and d
[PROOF STATE]
proof (chain)
picking this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
have f: "(if MGF (sha1 (generate_M' (sha1 m) salt))
              (length
              (generate_DB
              (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
              (length (sha1 (generate_M' (sha1 m) salt)))))) =
              []
              then []
              else (emsapss_encode_help7
              (bvxor
              (generate_DB
              (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
              (length (sha1 (generate_M' (sha1 m) salt)))))
              (MGF (sha1 (generate_M' (sha1 m) salt))
              (length
              (generate_DB
              (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
              (length (sha1 (generate_M' (sha1 m) salt))))))))
              (sha1 (generate_M' (sha1 m) salt))
              (length (nat_to_bv (p * q)) - Suc 0))) = (emsapss_encode_help7
              (bvxor
              (generate_DB
              (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
              (length (sha1 (generate_M' (sha1 m) salt)))))
              (MGF (sha1 (generate_M' (sha1 m) salt))
              (length
              (generate_DB
              (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
              (length (sha1 (generate_M' (sha1 m) salt))))))))
              (sha1 (generate_M' (sha1 m) salt))
              (length (nat_to_bv (p * q)) - Suc 0))"
[PROOF STATE]
proof (prove)
using this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)

goal (1 subgoal):
 1. (if MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) = [] then [] else emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
by (auto simp add: emsapss_encode_def emsapss_encode_help1_def emsapss_encode_help2_def
                emsapss_encode_help3_def emsapss_encode_help4_def emsapss_encode_help5_def
                emsapss_encode_help6_def)
[PROOF STATE]
proof (state)
this:
(if MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) = [] then [] else emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0)

goal (1 subgoal):
 1. length (remzero (if MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) = [] then [] else emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
have "length (remzero (emsapss_encode_help7
              (bvxor
              (generate_DB
              (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
              (length (sha1 (generate_M' (sha1 m) salt)))))
              (MGF (sha1 (generate_M' (sha1 m) salt))
              (length
              (generate_DB
              (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
              (length (sha1 (generate_M' (sha1 m) salt))))))))
              (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remzero (emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
proof (simp add: emsapss_encode_help7_def emsapss_encode_help8_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
from p and q and x
[PROOF STATE]
proof (chain)
picking this:
prime p
prime q
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0
[PROOF STEP]
show " length
                (remzero
                (maskedDB_zero
                (bvxor
                (generate_DB
                (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
                (length (sha1 (generate_M' (sha1 m) salt)))))
                (MGF (sha1 (generate_M' (sha1 m) salt))
                (length
                (generate_DB
                (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
                (length (sha1 (generate_M' (sha1 m) salt))))))))
                (length (nat_to_bv (p * q)) - Suc 0) @
                sha1 (generate_M' (sha1 m) salt) @ BC))
                < length (nat_to_bv (p * q))"
[PROOF STATE]
proof (prove)
using this:
prime p
prime q
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
using "length_helper" and len and mgf
[PROOF STATE]
proof (prove)
using this:
prime p
prime q
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0
\<lbrakk>prime ?p; prime ?q; (length (nat_to_bv (?p * ?q)) - Suc 0) mod 8 \<noteq> 0; MGF (sha1 (generate_M' (sha1 ?m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt)))))) \<noteq> []; length (sha1 ?M) + sLen + 16 \<le> length (nat_to_bv (?p * ?q)) - Suc 0\<rbrakk> \<Longrightarrow> length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt))))) (MGF (sha1 (generate_M' (sha1 ?m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (?p * ?q)) - Suc 0) (length (sha1 (generate_M' (sha1 ?m) salt)))))))) (length (nat_to_bv (?p * ?q)) - Suc 0) @ sha1 (generate_M' (sha1 ?m) salt) @ BC)) < length (nat_to_bv (?p * ?q))
length (sha1 m) + sLen + 16 \<le> length (nat_to_bv (p * q)) - Suc 0
MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) \<noteq> []

goal (1 subgoal):
 1. length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remzero (maskedDB_zero (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (length (nat_to_bv (p * q)) - Suc 0) @ sha1 (generate_M' (sha1 m) salt) @ BC)) < length (nat_to_bv (p * q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (remzero (emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal (1 subgoal):
 1. length (remzero (if MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) = [] then [] else emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (remzero (emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
show "length
              (remzero
              (if MGF (sha1 (generate_M' (sha1 m) salt))
              (length
              (generate_DB
              (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
              (length (sha1 (generate_M' (sha1 m) salt)))))) =
              []
              then []
              else emsapss_encode_help7
              (bvxor
              (generate_DB
              (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
              (length (sha1 (generate_M' (sha1 m) salt)))))
              (MGF (sha1 (generate_M' (sha1 m) salt))
              (length
              (generate_DB
              (generate_PS (length (nat_to_bv (p * q)) - Suc 0)
              (length (sha1 (generate_M' (sha1 m) salt))))))))
              (sha1 (generate_M' (sha1 m) salt))
              (length (nat_to_bv (p * q)) - Suc 0)))
              < length (nat_to_bv (p * q))"
[PROOF STATE]
proof (prove)
using this:
length (remzero (emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal (1 subgoal):
 1. length (remzero (if MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) = [] then [] else emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
length (remzero (emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
(if MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) = [] then [] else emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0)

goal (1 subgoal):
 1. length (remzero (if MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) = [] then [] else emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remzero (if MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))) = [] then [] else emsapss_encode_help7 (bvxor (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt)))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (remzero (emsapss_encode_help6 (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))) (MGF (sha1 (generate_M' (sha1 m) salt)) (length (generate_DB (generate_PS (length (nat_to_bv (p * q)) - Suc 0) (length (sha1 (generate_M' (sha1 m) salt))))))) (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (remzero (emsapss_encode_help3 (sha1 (generate_M' (sha1 m) salt)) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (remzero (emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal (1 subgoal):
 1. length (remzero (if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
from d and e
[PROOF STATE]
proof (chain)
picking this:
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)
length (remzero (emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
show "length
      (remzero
      (if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16
      then []
      else emsapss_encode_help2 (generate_M' (sha1 m) salt)
      (length (nat_to_bv (p * q)) - Suc 0)))
      < length (nat_to_bv (p * q))"
[PROOF STATE]
proof (prove)
using this:
(if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)) = emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0)
length (remzero (emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal (1 subgoal):
 1. length (remzero (if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remzero (if length (nat_to_bv (p * q)) - Suc 0 < length (sha1 m) + sLen + 16 then [] else emsapss_encode_help2 (generate_M' (sha1 m) salt) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (remzero (emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0\<rbrakk> \<Longrightarrow> length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
from b and c
[PROOF STATE]
proof (chain)
picking this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)
length (remzero (emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) = emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0)
length (remzero (emsapss_encode_help1 (sha1 m) (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal (1 subgoal):
 1. length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal:
No subgoals!
[PROOF STEP]
qed