exp2.aa

*import exp
*import exp1
*import sum
*func E
*var n

specify(exp.T2): \Aa: E(a, 2) = n(1 + 2^{-a}) + 2^{-a} \sum_{i=1}^a{ 2^{i} E(i, 1) / 2 }
equate(exp1.Exp_a_1): \Aa: E(a, 2) = n(1 + 2^{-a}) + 2^{-a} \sum_{i=1}^a{ 2^{i} n(i + 2^{-i}) / 2 }
factor: \Aa: E(a, 2) = n(1 + 2^{-a}) + n 2^{-a} \sum_{i=1}^a{ 2^{i} (i + 2^{-i}) / 2 }
factor: \Aa: E(a, 2) = n(1 + 2^{-a}) + (n / 2) 2^{-a} \sum_{i=1}^a{ 2^{i} (i + 2^{-i}) }
distrib: \Aa: E(a, 2) = n(1 + 2^{-a}) + (n / 2) 2^{-a} \sum_{i=1}^a{ 2^{i} i + 1 }
unarydistrib: \Aa: E(a, 2) = n(1 + 2^{-a}) + (n / 2) 2^{-a} (\sum_{i=1}^a{ 2^{i} i } + \sum_{i=1}^a{ 1 })
equate(sum.Sum_pow_2_i): \Aa: E(a, 2) = n(1 + 2^{-a}) + (n / 2) 2^{-a} (2^{a + 1} (a - 1) + 2 + \sum_{i=1}^a{ 1 })
equate(sum.Sum_const): \Aa: E(a, 2) = n(1 + 2^{-a}) + (n / 2) 2^{-a} (2^{a + 1} (a - 1) + 2 + a)
factor: \Aa: E(a, 2) = n(1 + 2^{-a} + (1 / 2) 2^{-a} (2^{a + 1} (a - 1) + 2 + a))
distrib: \Aa: E(a, 2) = n(1 + 2^{-a} + (1 / 2) (2(a - 1) + (2 + a) 2^{-a}))
distrib: \Aa: E(a, 2) = n(a + 2^{-a} + (2 + a) 2^{-a} / 2)
factor: \Aa: E(a, 2) = n(a + 2^{-a} (a + 4) / 2)
theorem Exp_a_2: \Aa: E(a, 2) = n(a + 2^{-a} (a + 4) / 2)