[STATEMENT]
theorem tight_bound:
  assumes T_def: "\<And> numbers l. length numbers = 2^l \<Longrightarrow> l > 0 \<Longrightarrow>
                               T numbers  = (2^l - 1) * 14 + l *15*2^(l-1) + 2^l"
                 "\<And> numbers l. l =0 \<Longrightarrow> length numbers = 2^l \<Longrightarrow> T numbers = 1"
  shows " length numbers = 2^l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers =  T numbers"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length numbers = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers = T numbers
[PROOF STEP]
proof(induction numbers arbitrary: l rule: T\<^sub>F\<^sub>N\<^sub>T\<^sub>T.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
case (3 x y numbers)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = length (x # y # numbers); ?xa = evens_odds True (x # y # numbers); ?xb = evens_odds False (x # y # numbers); ?xc = FNTT ?xa; ?xd = FNTT ?xb; length ?xa = 2 ^ ?l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T ?xa = T ?xa
\<lbrakk>?x = length (x # y # numbers); ?xa = evens_odds True (x # y # numbers); ?xb = evens_odds False (x # y # numbers); ?xc = FNTT ?xa; ?xd = FNTT ?xb; length ?xb = 2 ^ ?l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T ?xb = T ?xb
length (x # y # numbers) = 2 ^ l

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
text \<open>Some definitions for making term rewriting simpler.\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = length (x # y # numbers); ?xa = evens_odds True (x # y # numbers); ?xb = evens_odds False (x # y # numbers); ?xc = FNTT ?xa; ?xd = FNTT ?xb; length ?xa = 2 ^ ?l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T ?xa = T ?xa
\<lbrakk>?x = length (x # y # numbers); ?xa = evens_odds True (x # y # numbers); ?xb = evens_odds False (x # y # numbers); ?xc = FNTT ?xa; ?xd = FNTT ?xb; length ?xb = 2 ^ ?l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T ?xb = T ?xb
length (x # y # numbers) = 2 ^ l

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
define  nn where "nn = length (x # y # numbers)"
[PROOF STATE]
proof (state)
this:
nn = length (x # y # numbers)

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
define  nums1 where "nums1 = evens_odds True (x # y # numbers)"
[PROOF STATE]
proof (state)
this:
nums1 = evens_odds True (x # y # numbers)

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
define  nums2 where "nums2 = evens_odds False (x # y # numbers)"
[PROOF STATE]
proof (state)
this:
nums2 = evens_odds False (x # y # numbers)

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
define fntt1  where "fntt1 = local.FNTT nums1"
[PROOF STATE]
proof (state)
this:
fntt1 = FNTT nums1

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
define fntt2 where "fntt2 = local.FNTT nums2"
[PROOF STATE]
proof (state)
this:
fntt2 = FNTT nums2

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
define sum1 where "sum1 = map2 (+) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])"
[PROOF STATE]
proof (state)
this:
sum1 = map2 (+) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
define sum2 where "sum2 = map2 (-) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])"
[PROOF STATE]
proof (state)
this:
sum2 = map2 (-) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
text \<open>Unfolding the running time function and combining it with the definitions above.\<close>
[PROOF STATE]
proof (state)
this:
sum2 = map2 (-) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have TFNNT_simp: " T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) =
                    1 + T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) + 3 +
                    T_\<^sub>e\<^sub>o True (x # y # numbers) + T_\<^sub>e\<^sub>o False (x # y # numbers) + 2 +
                    local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 +
                    2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] +
                    2 *
                    T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) +
                    T\<^sub>a\<^sub>p\<^sub>p sum1 sum2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = 1 + T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) + 3 + T_\<^sub>e\<^sub>o True (x # y # numbers) + T_\<^sub>e\<^sub>o False (x # y # numbers) + 2 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) + T\<^sub>a\<^sub>p\<^sub>p sum1 sum2
[PROOF STEP]
apply(subst  T\<^sub>F\<^sub>N\<^sub>T\<^sub>T.simps(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) + 3 + (let nn = length (x # y # numbers); nums1 = evens_odds True (x # y # numbers); nums2 = evens_odds False (x # y # numbers) in T_\<^sub>e\<^sub>o True (x # y # numbers) + T_\<^sub>e\<^sub>o False (x # y # numbers) + 2 + (let fntt1 = FNTT nums1; fntt2 = FNTT nums2 in T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + (let sum1 = map2 (+) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]); sum2 = map2 (-) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) in 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) + T\<^sub>a\<^sub>p\<^sub>p sum1 sum2))) = 1 + T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) + 3 + T_\<^sub>e\<^sub>o True (x # y # numbers) + T_\<^sub>e\<^sub>o False (x # y # numbers) + 2 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) + T\<^sub>a\<^sub>p\<^sub>p sum1 sum2
[PROOF STEP]
unfolding Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) + 3 + (T_\<^sub>e\<^sub>o True (x # y # numbers) + T_\<^sub>e\<^sub>o False (x # y # numbers) + 2 + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (evens_odds True (x # y # numbers)) + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (evens_odds False (x # y # numbers)) + (2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2] + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) (FNTT (evens_odds True (x # y # numbers))) (map2 (\<lambda>xa ya. xa * \<omega> ^ (n div length (x # y # numbers) * ya)) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2]) + T\<^sub>a\<^sub>p\<^sub>p (map2 (+) (FNTT (evens_odds True (x # y # numbers))) (map2 (\<lambda>xa ya. xa * \<omega> ^ (n div length (x # y # numbers) * ya)) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2])) (map2 (-) (FNTT (evens_odds True (x # y # numbers))) (map2 (\<lambda>xa ya. xa * \<omega> ^ (n div length (x # y # numbers) * ya)) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2]))))) = 1 + T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) + 3 + T_\<^sub>e\<^sub>o True (x # y # numbers) + T_\<^sub>e\<^sub>o False (x # y # numbers) + 2 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) + T\<^sub>a\<^sub>p\<^sub>p sum1 sum2
[PROOF STEP]
unfolding sum2_def sum1_def fntt1_def fntt2_def nums1_def nums2_def nn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) + 3 + (T_\<^sub>e\<^sub>o True (x # y # numbers) + T_\<^sub>e\<^sub>o False (x # y # numbers) + 2 + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (evens_odds True (x # y # numbers)) + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (evens_odds False (x # y # numbers)) + (2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2] + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) (FNTT (evens_odds True (x # y # numbers))) (map2 (\<lambda>xa ya. xa * \<omega> ^ (n div length (x # y # numbers) * ya)) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2]) + T\<^sub>a\<^sub>p\<^sub>p (map2 (+) (FNTT (evens_odds True (x # y # numbers))) (map2 (\<lambda>xa ya. xa * \<omega> ^ (n div length (x # y # numbers) * ya)) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2])) (map2 (-) (FNTT (evens_odds True (x # y # numbers))) (map2 (\<lambda>xa ya. xa * \<omega> ^ (n div length (x # y # numbers) * ya)) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2]))))) = 1 + T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) + 3 + T_\<^sub>e\<^sub>o True (x # y # numbers) + T_\<^sub>e\<^sub>o False (x # y # numbers) + 2 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (evens_odds True (x # y # numbers)) + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (evens_odds False (x # y # numbers)) + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2] + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) (FNTT (evens_odds True (x # y # numbers))) (map2 (\<lambda>xa ya. xa * \<omega> ^ (n div length (x # y # numbers) * ya)) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2]) + T\<^sub>a\<^sub>p\<^sub>p (map2 (+) (FNTT (evens_odds True (x # y # numbers))) (map2 (\<lambda>xa ya. xa * \<omega> ^ (n div length (x # y # numbers) * ya)) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2])) (map2 (-) (FNTT (evens_odds True (x # y # numbers))) (map2 (\<lambda>xa ya. xa * \<omega> ^ (n div length (x # y # numbers) * ya)) (FNTT (evens_odds False (x # y # numbers))) [0..<length (x # y # numbers) div 2]))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = 1 + T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) + 3 + T_\<^sub>e\<^sub>o True (x # y # numbers) + T_\<^sub>e\<^sub>o False (x # y # numbers) + 2 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) + T\<^sub>a\<^sub>p\<^sub>p sum1 sum2

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
text \<open>Application of lemmas related to running times of auxiliary functions.\<close>
[PROOF STATE]
proof (state)
this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = 1 + T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) + 3 + T_\<^sub>e\<^sub>o True (x # y # numbers) + T_\<^sub>e\<^sub>o False (x # y # numbers) + 2 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] + 2 * T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) + T\<^sub>a\<^sub>p\<^sub>p sum1 sum2

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have length_nums1: "length nums1 = (2::nat)^(l-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length nums1 = 2 ^ (l - 1)
[PROOF STEP]
unfolding nums1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (evens_odds True (x # y # numbers)) = 2 ^ (l - 1)
[PROOF STEP]
using evens_odds_length[of "x # y # numbers"] 3(3) xyz
[PROOF STATE]
proof (prove)
using this:
length (evens_odds True (x # y # numbers)) = (length (x # y # numbers) + 1) div 2 \<and> length (evens_odds False (x # y # numbers)) = length (x # y # numbers) div 2
length (x # y # numbers) = 2 ^ l
Suc (Suc (length ?xs)) = 2 ^ ?l \<Longrightarrow> length (?x # evens_odds True ?xs) = 2 ^ (?l - 1)

goal (1 subgoal):
 1. length (evens_odds True (x # y # numbers)) = 2 ^ (l - 1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
length nums1 = 2 ^ (l - 1)

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have length_nums2: "length nums2 = (2::nat)^(l-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length nums2 = 2 ^ (l - 1)
[PROOF STEP]
unfolding nums2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (evens_odds False (x # y # numbers)) = 2 ^ (l - 1)
[PROOF STEP]
using evens_odds_length[of "x # y # numbers"] 3(3)
[PROOF STATE]
proof (prove)
using this:
length (evens_odds True (x # y # numbers)) = (length (x # y # numbers) + 1) div 2 \<and> length (evens_odds False (x # y # numbers)) = length (x # y # numbers) div 2
length (x # y # numbers) = 2 ^ l

goal (1 subgoal):
 1. length (evens_odds False (x # y # numbers)) = 2 ^ (l - 1)
[PROOF STEP]
by (metis One_nat_def le_0_eq length_Cons lessI list.size(4) neq0_conv not_add_less2 not_less_eq_eq pos2 power_Suc0_right power_diff_power_eq power_eq_if)
[PROOF STATE]
proof (state)
this:
length nums2 = 2 ^ (l - 1)

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have length_simp: "T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) = (2::nat) ^l +1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) = 2 ^ l + 1
[PROOF STEP]
using T_length_linear[of "x#y#numbers"]  3(3)
[PROOF STATE]
proof (prove)
using this:
T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) = length (x # y # numbers) + 1
length (x # y # numbers) = 2 ^ l

goal (1 subgoal):
 1. T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) = 2 ^ l + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T\<^sub>l\<^sub>e\<^sub>n\<^sub>g\<^sub>t\<^sub>h (x # y # numbers) = 2 ^ l + 1

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have even_odd_simp: " T_\<^sub>e\<^sub>o b (x # y # numbers) = (2::nat)^l + 1" for b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T_\<^sub>e\<^sub>o b (x # y # numbers) = 2 ^ l + 1
[PROOF STEP]
by (metis "3.prems" T_eo_linear)+
[PROOF STATE]
proof (state)
this:
T_\<^sub>e\<^sub>o ?b (x # y # numbers) = 2 ^ l + 1

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have 02: "(length fntt2) =  (length [0..<nn div 2])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length fntt2 = length [0..<nn div 2]
[PROOF STEP]
unfolding fntt2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (FNTT nums2) = length [0..<nn div 2]
[PROOF STEP]
apply(subst FNTT_length[of _ "l-1"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length nums2 = 2 ^ (l - 1)
 2. length nums2 = length [0..<nn div 2]
[PROOF STEP]
unfolding nums2_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (evens_odds False (x # y # numbers)) = 2 ^ (l - 1)
 2. length (evens_odds False (x # y # numbers)) = length [0..<nn div 2]
[PROOF STEP]
using length_nums2 nums2_def
[PROOF STATE]
proof (prove)
using this:
length nums2 = 2 ^ (l - 1)
nums2 = evens_odds False (x # y # numbers)

goal (2 subgoals):
 1. length (evens_odds False (x # y # numbers)) = 2 ^ (l - 1)
 2. length (evens_odds False (x # y # numbers)) = length [0..<nn div 2]
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (evens_odds False (x # y # numbers)) = length [0..<nn div 2]
[PROOF STEP]
by (simp add: evens_odds_length nn_def)
[PROOF STATE]
proof (state)
this:
length fntt2 = length [0..<nn div 2]

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have 03: "(length fntt1) =  (length [0..<nn div 2])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length fntt1 = length [0..<nn div 2]
[PROOF STEP]
unfolding fntt1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (FNTT nums1) = length [0..<nn div 2]
[PROOF STEP]
apply(subst FNTT_length[of _ "l-1"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length nums1 = 2 ^ (l - 1)
 2. length nums1 = length [0..<nn div 2]
[PROOF STEP]
unfolding nums1_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (evens_odds True (x # y # numbers)) = 2 ^ (l - 1)
 2. length (evens_odds True (x # y # numbers)) = length [0..<nn div 2]
[PROOF STEP]
using length_nums1 nums1_def
[PROOF STATE]
proof (prove)
using this:
length nums1 = 2 ^ (l - 1)
nums1 = evens_odds True (x # y # numbers)

goal (2 subgoals):
 1. length (evens_odds True (x # y # numbers)) = 2 ^ (l - 1)
 2. length (evens_odds True (x # y # numbers)) = length [0..<nn div 2]
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (evens_odds True (x # y # numbers)) = length [0..<nn div 2]
[PROOF STEP]
by (metis "02" FNTT_length fntt2_def length_nums1 length_nums2 nums1_def)
[PROOF STATE]
proof (state)
this:
length fntt1 = length [0..<nn div 2]

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have map21_simp: "T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] = (2::nat)^l + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] = 2 ^ l + 1
[PROOF STEP]
apply(subst T_map_2_linear'[of 1])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 0 < 1
 2. \<And>x y. 1 = 1
 3. min (length fntt2) (length [0..<nn div 2]) * (1 + 1) + 1 = 2 ^ l + 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. 1 = 1
 2. min (length fntt2) (length [0..<nn div 2]) * (1 + 1) + 1 = 2 ^ l + 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (length fntt2) (length [0..<nn div 2]) * (1 + 1) + 1 = 2 ^ l + 1
[PROOF STEP]
by (smt (z3) "02" "3"(3) FNTT_length div_less evens_odds_length fntt2_def length_nums2 lessI less_numeral_extra(3) min.idem mult.commute nat_1_add_1 nums2_def plus_1_eq_Suc power_eq_if power_not_zero zero_power2)
[PROOF STATE]
proof (state)
this:
T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt2 [0..<nn div 2] = 2 ^ l + 1

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have map22_simp: "T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) =
        (2::nat)^l + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) = 2 ^ l + 1
[PROOF STEP]
apply(subst T_map_2_linear'[of 1])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 0 < 1
 2. \<And>x y. 1 = 1
 3. min (length fntt1) (length (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])) * (1 + 1) + 1 = 2 ^ l + 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. 1 = 1
 2. min (length fntt1) (length (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])) * (1 + 1) + 1 = 2 ^ l + 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (length fntt1) (length (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])) * (1 + 1) + 1 = 2 ^ l + 1
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (length fntt1) (min (length fntt2) (nn div 2)) + min (length fntt1) (min (length fntt2) (nn div 2)) = 2 ^ l
[PROOF STEP]
unfolding fntt1_def fntt2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (length (FNTT nums1)) (min (length (FNTT nums2)) (nn div 2)) + min (length (FNTT nums1)) (min (length (FNTT nums2)) (nn div 2)) = 2 ^ l
[PROOF STEP]
unfolding nn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (length (FNTT nums1)) (min (length (FNTT nums2)) (length (x # y # numbers) div 2)) + min (length (FNTT nums1)) (min (length (FNTT nums2)) (length (x # y # numbers) div 2)) = 2 ^ l
[PROOF STEP]
apply(subst FNTT_length[of _ "l-1"], (rule length_nums1)?, (rule length_nums2)?,
                 (subst length_nums1)?,  (subst length_nums2)?,  (subst 3(3))?)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (2 ^ (l - 1)) (min (2 ^ (l - 1)) (2 ^ l div 2)) + min (2 ^ (l - 1)) (min (2 ^ (l - 1)) (2 ^ l div 2)) = 2 ^ l
[PROOF STEP]
apply (metis (no_types, lifting) "3"(3) div_less evens_odds_length length_nums2 lessI min_def mult_2 nat_1_add_1 nums2_def plus_1_eq_Suc power_eq_if power_not_zero zero_neq_numeral)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
T\<^sub>m\<^sub>a\<^sub>p\<^sub>2 (\<lambda>x y. 1) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2]) = 2 ^ l + 1

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have sum1_simp: "length sum1 = 2^(l-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length sum1 = 2 ^ (l - 1)
[PROOF STEP]
unfolding sum1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map2 (+) fntt1 (map2 (\<lambda>x y. x * \<omega> ^ (n div nn * y)) fntt2 [0..<nn div 2])) = 2 ^ (l - 1)
[PROOF STEP]
apply(subst map2_length)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (length fntt1) (min (length fntt2) (length [0..<nn div 2])) = 2 ^ (l - 1)
[PROOF STEP]
apply(subst 02, subst 03)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (length [0..<nn div 2]) (min (length [0..<nn div 2]) (length [0..<nn div 2])) = 2 ^ (l - 1)
[PROOF STEP]
unfolding nn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (length [0..<length (x # y # numbers) div 2]) (min (length [0..<length (x # y # numbers) div 2]) (length [0..<length (x # y # numbers) div 2])) = 2 ^ (l - 1)
[PROOF STEP]
using 3(3)
[PROOF STATE]
proof (prove)
using this:
length (x # y # numbers) = 2 ^ l

goal (1 subgoal):
 1. min (length [0..<length (x # y # numbers) div 2]) (min (length [0..<length (x # y # numbers) div 2]) (length [0..<length (x # y # numbers) div 2])) = 2 ^ (l - 1)
[PROOF STEP]
by (metis "02" FNTT_length fntt2_def length_nums2 min.idem nn_def)
[PROOF STATE]
proof (state)
this:
length sum1 = 2 ^ (l - 1)

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have app_simp: "T\<^sub>a\<^sub>p\<^sub>p sum1 sum2 = (2::nat)^(l-1) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>a\<^sub>p\<^sub>p sum1 sum2 = 2 ^ (l - 1) + 1
[PROOF STEP]
by(subst T_app_linear, subst sum1_simp, simp)
[PROOF STATE]
proof (state)
this:
T\<^sub>a\<^sub>p\<^sub>p sum1 sum2 = 2 ^ (l - 1) + 1

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
let ?T1 = "(2^(l-1) - 1) * 14 + (l-1) *15*2^(l-1 -1) + 2^(l-1)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
text \<open>Induction hypotheses\<close>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have IH_pluged1: "local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 = ?T1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply(subst "3.IH"(1)[of nn nums1 nums2 fntt1 fntt2 "l-1",
                            OF nn_def nums1_def nums2_def fntt1_def fntt2_def length_nums1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T nums1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply(cases "l \<le> 1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. l \<le> 1 \<Longrightarrow> T nums1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
 2. \<not> l \<le> 1 \<Longrightarrow> T nums1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> 1 \<Longrightarrow> T nums1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply(subst T_def(2)[of "l-1"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. l \<le> 1 \<Longrightarrow> l - 1 = 0
 2. l \<le> 1 \<Longrightarrow> length nums1 = 2 ^ (l - 1)
 3. l \<le> 1 \<Longrightarrow> 1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> 1 \<Longrightarrow> l - 1 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. l \<le> 1 \<Longrightarrow> length nums1 = 2 ^ (l - 1)
 2. l \<le> 1 \<Longrightarrow> 1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply(rule length_nums1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> 1 \<Longrightarrow> 1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> l \<le> 1 \<Longrightarrow> T nums1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply(subst T_def(1)[OF length_nums1])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> l \<le> 1 \<Longrightarrow> 0 < l - 1
 2. \<not> l \<le> 1 \<Longrightarrow> (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> l \<le> 1 \<Longrightarrow> 0 < l - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> l \<le> 1 \<Longrightarrow> (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> l \<le> 1 \<Longrightarrow> (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have IH_pluged2: "local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 = ?T1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply(subst "3.IH"(2)[of nn nums1 _ fntt1 fntt2 "l-1", OF nn_def nums1_def nums2_def fntt1_def
                           fntt2_def length_nums2 ])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T nums2 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply(cases "l \<le> 1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. l \<le> 1 \<Longrightarrow> T nums2 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
 2. \<not> l \<le> 1 \<Longrightarrow> T nums2 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> 1 \<Longrightarrow> T nums2 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply(subst T_def(2)[of "l-1"])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. l \<le> 1 \<Longrightarrow> l - 1 = 0
 2. l \<le> 1 \<Longrightarrow> length nums2 = 2 ^ (l - 1)
 3. l \<le> 1 \<Longrightarrow> 1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> 1 \<Longrightarrow> l - 1 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. l \<le> 1 \<Longrightarrow> length nums2 = 2 ^ (l - 1)
 2. l \<le> 1 \<Longrightarrow> 1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply(rule length_nums2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<le> 1 \<Longrightarrow> 1 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> l \<le> 1 \<Longrightarrow> T nums2 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
apply(subst T_def(1)[OF length_nums2])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<not> l \<le> 1 \<Longrightarrow> 0 < l - 1
 2. \<not> l \<le> 1 \<Longrightarrow> (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> l \<le> 1 \<Longrightarrow> 0 < l - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> l \<le> 1 \<Longrightarrow> (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> l \<le> 1 \<Longrightarrow> (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 = (2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have " T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) =
        14 + (3 * 2 ^ l + (local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 +
        (local.T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + (5 * 2^(l-1) + 4 * (2 ^ l div 2)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = 14 + (3 * 2 ^ l + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))))
[PROOF STEP]
apply(subst TFNNT_simp, subst map21_simp, subst map22_simp, subst  length_simp,
          subst app_simp, subst even_odd_simp, subst even_odd_simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + (2 ^ l + 1) + 3 + (2 ^ l + 1) + (2 ^ l + 1) + 2 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + 2 * (2 ^ l + 1) + 2 * (2 ^ l + 1) + (2 ^ (l - 1) + 1) = 14 + (3 * 2 ^ l + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))))
[PROOF STEP]
apply(auto simp add: algebra_simps power_eq_if[of 2 l])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = 14 + (3 * 2 ^ l + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))))

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
text \<open>Proof that the term $T\text{-}def$ indeed fulfills the recursive properties, i.e.
          $t(2^l) = 2 \cdot t(2^{l-1}) + s$\<close>
[PROOF STATE]
proof (state)
this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = 14 + (3 * 2 ^ l + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))))

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = 14 + (3 * 2 ^ l + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))))

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have "\<dots> = 14 + (3 * 2 ^ l + (?T1 + (?T1 + (5 * 2^(l-1) + 4 * (2 ^ l div 2)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 14 + (3 * 2 ^ l + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2))))) = 14 + (3 * 2 ^ l + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))))
[PROOF STEP]
apply(subst IH_pluged1, subst IH_pluged2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 14 + (3 * 2 ^ l + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2))))) = 14 + (3 * 2 ^ l + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
14 + (3 * 2 ^ l + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2))))) = 14 + (3 * 2 ^ l + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))))

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
14 + (3 * 2 ^ l + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums1 + (T\<^sub>F\<^sub>N\<^sub>T\<^sub>T nums2 + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2))))) = 14 + (3 * 2 ^ l + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))))

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have "\<dots> =  14 + (6 * 2 ^ (l-1) +
          2*((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) +
       (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 14 + (3 * 2 ^ l + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2))))) = 14 + (6 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))
[PROOF STEP]
by (smt (verit) "3"(3) add.assoc div_less evens_odds_length left_add_twice length_nums2 lessI mult.assoc mult_2_right nat_1_add_1 numeral_Bit0 nums2_def plus_1_eq_Suc power_eq_if power_not_zero zero_neq_numeral)
[PROOF STATE]
proof (state)
this:
14 + (3 * 2 ^ l + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2))))) = 14 + (6 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
14 + (3 * 2 ^ l + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2))))) = 14 + (6 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2)))

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have "\<dots> =  14 +  15 * 2 ^ (l-1) +
     2*((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 14 + (6 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2))) = 14 + 15 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1))
[PROOF STEP]
by (smt (z3) "3"(3) add.assoc add.commute calculation diff_diff_left distrib_left div2_Suc_Suc evens_odds_length left_add_twice length_Cons length_nums2 mult.assoc mult.commute mult_2 mult_2_right numeral_Bit0 numeral_Bit1 numeral_plus_numeral nums2_def one_add_one)
[PROOF STATE]
proof (state)
this:
14 + (6 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2))) = 14 + 15 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1))

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
14 + (6 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) + (5 * 2 ^ (l - 1) + 4 * (2 ^ l div 2))) = 14 + 15 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1))

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have "... = 14 + 15 * 2 ^ (l-1) +
                    (2 ^ l - 2) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 14 + 15 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) = 14 + 15 * 2 ^ (l - 1) + (2 ^ l - 2) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
apply(cases "l > 1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 1 < l \<Longrightarrow> 14 + 15 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) = 14 + 15 * 2 ^ (l - 1) + (2 ^ l - 2) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l
 2. \<not> 1 < l \<Longrightarrow> 14 + 15 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) = 14 + 15 * 2 ^ (l - 1) + (2 ^ l - 2) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
apply (smt (verit, del_insts) add.assoc diff_is_0_eq distrib_left_numeral left_diff_distrib' less_imp_le_nat mult.assoc mult_2 mult_2_right nat_1_add_1 not_le not_one_le_zero power_eq_if)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 1 < l \<Longrightarrow> 14 + 15 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) = 14 + 15 * 2 ^ (l - 1) + (2 ^ l - 2) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
by (smt (z3) "3"(3) add.commute add.right_neutral cancel_comm_monoid_add_class.diff_cancel diff_add_inverse2 diff_is_0_eq div_less_dividend evens_odds_length length_nums2 mult_2 mult_eq_0_iff nat_1_add_1 not_le nums2_def power_eq_if)
[PROOF STATE]
proof (state)
this:
14 + 15 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) = 14 + 15 * 2 ^ (l - 1) + (2 ^ l - 2) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
14 + 15 * 2 ^ (l - 1) + 2 * ((2 ^ (l - 1) - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1 - 1) + 2 ^ (l - 1)) = 14 + 15 * 2 ^ (l - 1) + (2 ^ l - 2) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have "\<dots> =  15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 14 + 15 * 2 ^ (l - 1) + (2 ^ l - 2) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = 15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
by (smt (z3) "3"(3) One_nat_def add.commute combine_common_factor diff_add_inverse2 diff_diff_left list.size(4) nat_1_add_1 nat_mult_1)
[PROOF STATE]
proof (state)
this:
14 + 15 * 2 ^ (l - 1) + (2 ^ l - 2) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = 15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
14 + 15 * 2 ^ (l - 1) + (2 ^ l - 2) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = 15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
have "\<dots> = (2^l - 1) * 14 + l *15*2^(l-1) + 2^l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
apply(cases "l > 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 < l \<Longrightarrow> 15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l
 2. \<not> 0 < l \<Longrightarrow> 15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < l \<Longrightarrow> 15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
using group_cancel.add1 group_cancel.add2 less_numeral_extra(3) mult.assoc mult_eq_if
[PROOF STATE]
proof (prove)
using this:
?A \<equiv> ?k + ?a \<Longrightarrow> ?A + ?b \<equiv> ?k + (?a + ?b)
?B \<equiv> ?k + ?b \<Longrightarrow> ?a + ?B \<equiv> ?k + (?a + ?b)
\<not> (0::?'a) < (0::?'a)
?a * ?b * ?c = ?a * (?b * ?c)
?m * ?n = (if ?m = 0 then 0 else ?n + (?m - 1) * ?n)

goal (1 subgoal):
 1. 0 < l \<Longrightarrow> 15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
by auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 0 < l \<Longrightarrow> 15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
using "3"(3)
[PROOF STATE]
proof (prove)
using this:
length (x # y # numbers) = 2 ^ l

goal (1 subgoal):
 1. \<not> 0 < l \<Longrightarrow> 15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
text \<open>By the previous proposition, we can conclude that $T$ is indeed a suitable term for describing the running time\<close>
[PROOF STATE]
proof (state)
this:
15 * 2 ^ (l - 1) + (2 ^ l - 1) * 14 + (l - 1) * 15 * 2 ^ (l - 1) + 2 ^ l = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
have "T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = T (x # y # numbers)"
[PROOF STATE]
proof (prove)
using this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = T (x # y # numbers)
[PROOF STEP]
using T_def(1)[of "x#y#numbers" l]
[PROOF STATE]
proof (prove)
using this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l
\<lbrakk>length (x # y # numbers) = 2 ^ l; 0 < l\<rbrakk> \<Longrightarrow> T (x # y # numbers) = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = T (x # y # numbers)
[PROOF STEP]
by (metis "3.prems" bits_1_div_2 diff_is_0_eq' evens_odds_length length_nums2 neq0_conv nums2_def power_0 zero_le_one zero_neq_one)
[PROOF STATE]
proof (state)
this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = T (x # y # numbers)

goal (3 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
 3. \<And>v vb vc l. \<lbrakk>\<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xa = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xa = T xa; \<And>x xa xb xc xd l. \<lbrakk>x = length (v # vb # vc); xa = evens_odds True (v # vb # vc); xb = evens_odds False (v # vb # vc); xc = FNTT xa; xd = FNTT xb; length xb = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T xb = T xb; length (v # vb # vc) = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (v # vb # vc) = T (v # vb # vc)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = T (x # y # numbers)

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = T (x # y # numbers)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T (x # y # numbers) = T (x # y # numbers)

goal (2 subgoals):
 1. \<And>l. length [] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [] = T []
 2. \<And>a l. length [a] = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T [a] = T [a]
[PROOF STEP]
qed (auto simp add: assms)


[STATEMENT]
theorem log_lin_time:
  assumes "length numbers = 2^l"
  shows "T\<^sub>F\<^sub>N\<^sub>T\<^sub>T  numbers \<le> 30 * l * length numbers + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
[PROOF STEP]
have 00: "T\<^sub>F\<^sub>N\<^sub>T\<^sub>T  numbers  = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
using tight_bound[of "\<lambda> xs. (length xs - 1) * 14 + (Discrete.log (length xs)) * 15 *
                            2 ^ ( (Discrete.log (length xs)) - 1) + length xs" numbers l]
          assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>numbers l. \<lbrakk>length numbers = 2 ^ l; 0 < l\<rbrakk> \<Longrightarrow> (length numbers - 1) * 14 + Discrete.log (length numbers) * 15 * 2 ^ (Discrete.log (length numbers) - 1) + length numbers = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l; \<And>numbers l. \<lbrakk>l = 0; length numbers = 2 ^ l\<rbrakk> \<Longrightarrow> (length numbers - 1) * 14 + Discrete.log (length numbers) * 15 * 2 ^ (Discrete.log (length numbers) - 1) + length numbers = 1; length numbers = 2 ^ l\<rbrakk> \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers = (length numbers - 1) * 14 + Discrete.log (length numbers) * 15 * 2 ^ (Discrete.log (length numbers) - 1) + length numbers
length numbers = 2 ^ l

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
[PROOF STEP]
have " l * 15 * 2 ^ (l - 1) \<le> 15 * l * length numbers"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l * 15 * 2 ^ (l - 1) \<le> 15 * l * length numbers
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length numbers = 2 ^ l

goal (1 subgoal):
 1. l * 15 * 2 ^ (l - 1) \<le> 15 * l * length numbers
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
l * 15 * 2 ^ (l - 1) \<le> 15 * l * length numbers

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l * 15 * 2 ^ (l - 1) \<le> 15 * l * length numbers

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
[PROOF STEP]
have "(2 ^ l - 1) * 14  + 2^l\<le> 15 * length numbers "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length numbers = 2 ^ l

goal (1 subgoal):
 1. (2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
[PROOF STEP]
hence "(2 ^ l - 1) * 14 + 2^l \<le> 15 * l * length numbers +1"
[PROOF STATE]
proof (prove)
using this:
(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers

goal (1 subgoal):
 1. (2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * l * length numbers + 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers
length numbers = 2 ^ l

goal (1 subgoal):
 1. (2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * l * length numbers + 1
[PROOF STEP]
apply(cases l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers; length numbers = 2 ^ l; l = 0\<rbrakk> \<Longrightarrow> (2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * l * length numbers + 1
 2. \<And>nat. \<lbrakk>(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers; length numbers = 2 ^ l; l = Suc nat\<rbrakk> \<Longrightarrow> (2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * l * length numbers + 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers; length numbers = 2 ^ l; l = 0\<rbrakk> \<Longrightarrow> (2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * l * length numbers + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers; length numbers = 2 ^ l; l = Suc nat\<rbrakk> \<Longrightarrow> (2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * l * length numbers + 1
[PROOF STEP]
by (metis (no_types) add.commute le_add1 mult.assoc mult.commute
          mult_le_mono nat_mult_1 plus_1_eq_Suc trans_le_add2)
[PROOF STATE]
proof (state)
this:
(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * l * length numbers + 1

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l * 15 * 2 ^ (l - 1) \<le> 15 * l * length numbers
(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers
(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * l * length numbers + 1
[PROOF STEP]
have " (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l \<le>  30 * l * length numbers +1"
[PROOF STATE]
proof (prove)
using this:
l * 15 * 2 ^ (l - 1) \<le> 15 * l * length numbers
(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * length numbers
(2 ^ l - 1) * 14 + 2 ^ l \<le> 15 * l * length numbers + 1

goal (1 subgoal):
 1. (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l \<le> 30 * l * length numbers + 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
(2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l \<le> 30 * l * length numbers + 1

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l \<le> 30 * l * length numbers + 1
[PROOF STEP]
show  ?thesis
[PROOF STATE]
proof (prove)
using this:
(2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l \<le> 30 * l * length numbers + 1

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
[PROOF STEP]
using 00
[PROOF STATE]
proof (prove)
using this:
(2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l \<le> 30 * l * length numbers + 1
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers = (2 ^ l - 1) * 14 + l * 15 * 2 ^ (l - 1) + 2 ^ l

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem log_lin_time_explicitly:
  assumes "length numbers = 2^l"
  shows "T\<^sub>F\<^sub>N\<^sub>T\<^sub>T  numbers \<le> 30 * Discrete.log (length numbers) * length numbers + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * Discrete.log (length numbers) * length numbers + 1
[PROOF STEP]
using log_lin_time[of numbers l] assms
[PROOF STATE]
proof (prove)
using this:
length numbers = 2 ^ l \<Longrightarrow> T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * l * length numbers + 1
length numbers = 2 ^ l

goal (1 subgoal):
 1. T\<^sub>F\<^sub>N\<^sub>T\<^sub>T numbers \<le> 30 * Discrete.log (length numbers) * length numbers + 1
[PROOF STEP]
by simp


[STATEMENT]
lemma bijections_in_domain_permutation:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
finite A
finite B
card A = card B
[PROOF STEP]
obtain f where f: "f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
using this:
finite A
finite B
card A = card B

goal (1 subgoal):
 1. (\<And>f. f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis finite_same_card_bij_on_ext_funcset mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B
[PROOF STEP]
have proj_f: "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = domain_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = domain_permutation A B `` {f}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> domain_permutation A B `` {f}
 2. domain_permutation A B `` {f} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
from f
[PROOF STATE]
proof (chain)
picking this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
show "{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> domain_permutation A B `` {f}"
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> domain_permutation A B `` {f}
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))} `` {f}
[PROOF STEP]
by (auto elim: obtain_domain_permutation_for_two_bijections)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<subseteq> domain_permutation A B `` {f}

goal (1 subgoal):
 1. domain_permutation A B `` {f} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. domain_permutation A B `` {f} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
show "domain_permutation A B `` {f} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain_permutation A B `` {f} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
fix f'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
assume "f' \<in> domain_permutation A B `` {f}"
[PROOF STATE]
proof (state)
this:
f' \<in> domain_permutation A B `` {f}

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
have "(f', f) \<in> domain_permutation A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f', f) \<in> domain_permutation A B
[PROOF STEP]
using \<open>f' \<in> domain_permutation A B `` {f}\<close> equiv_domain_permutation[of A B]
[PROOF STATE]
proof (prove)
using this:
f' \<in> domain_permutation A B `` {f}
equiv (A \<rightarrow>\<^sub>E B) (domain_permutation A B)

goal (1 subgoal):
 1. (f', f) \<in> domain_permutation A B
[PROOF STEP]
by (simp add: equiv_class_eq_iff)
[PROOF STATE]
proof (state)
this:
(f', f) \<in> domain_permutation A B

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(f', f) \<in> domain_permutation A B
[PROOF STEP]
obtain p where "p permutes A" "\<forall>x\<in>A. f' x = f (p x)"
[PROOF STATE]
proof (prove)
using this:
(f', f) \<in> domain_permutation A B

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f' x = f (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
(f', f) \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))}

goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p permutes A; \<forall>x\<in>A. f' x = f (p x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p permutes A
\<forall>x\<in>A. f' x = f (p x)

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
p permutes A
\<forall>x\<in>A. f' x = f (p x)
[PROOF STEP]
have "bij_betw (f \<circ> p) A B"
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f' x = f (p x)

goal (1 subgoal):
 1. bij_betw (f \<circ> p) A B
[PROOF STEP]
using bij_betw_comp_iff f permutes_imp_bij
[PROOF STATE]
proof (prove)
using this:
p permutes A
\<forall>x\<in>A. f' x = f (p x)
bij_betw ?f ?A ?A' \<Longrightarrow> bij_betw ?f' ?A' ?A'' = bij_betw (?f' \<circ> ?f) ?A ?A''
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
?p permutes ?S \<Longrightarrow> bij_betw ?p ?S ?S

goal (1 subgoal):
 1. bij_betw (f \<circ> p) A B
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
bij_betw (f \<circ> p) A B

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
bij_betw (f \<circ> p) A B
[PROOF STEP]
have "bij_betw f' A B"
[PROOF STATE]
proof (prove)
using this:
bij_betw (f \<circ> p) A B

goal (1 subgoal):
 1. bij_betw f' A B
[PROOF STEP]
using \<open>\<forall>x\<in>A. f' x = f (p x)\<close>
[PROOF STATE]
proof (prove)
using this:
bij_betw (f \<circ> p) A B
\<forall>x\<in>A. f' x = f (p x)

goal (1 subgoal):
 1. bij_betw f' A B
[PROOF STEP]
by (metis (mono_tags, lifting) bij_betw_cong comp_apply)
[PROOF STATE]
proof (state)
this:
bij_betw f' A B

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bij_betw f' A B

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
have "f' \<in> A \<rightarrow>\<^sub>E B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
using \<open>f' \<in> domain_permutation A B `` {f}\<close>
[PROOF STATE]
proof (prove)
using this:
f' \<in> domain_permutation A B `` {f}

goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
unfolding domain_permutation_def
[PROOF STATE]
proof (prove)
using this:
f' \<in> {(f, f'). (f, f') \<in> (A \<rightarrow>\<^sub>E B) \<times> (A \<rightarrow>\<^sub>E B) \<and> (\<exists>p. p permutes A \<and> (\<forall>x\<in>A. f x = f' (p x)))} `` {f}

goal (1 subgoal):
 1. f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. \<And>x. x \<in> domain_permutation A B `` {f} \<Longrightarrow> x \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bij_betw f' A B
f' \<in> A \<rightarrow>\<^sub>E B
[PROOF STEP]
show "f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}"
[PROOF STATE]
proof (prove)
using this:
bij_betw f' A B
f' \<in> A \<rightarrow>\<^sub>E B

goal (1 subgoal):
 1. f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f' \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
domain_permutation A B `` {f} \<subseteq> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = domain_permutation A B `` {f}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = domain_permutation A B `` {f}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B}
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} = domain_permutation A B `` {f}

goal (1 subgoal):
 1. {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B
[PROOF STEP]
by (simp add: quotientI)
[PROOF STATE]
proof (state)
this:
{f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} \<in> {f \<in> A \<rightarrow>\<^sub>E B. bij_betw f A B} // domain_permutation A B

goal:
No subgoals!
[PROOF STEP]
qed