toNat_uint_summation: (all k:UInt, begin:UInt, f:(fn UInt -> UInt). toNat(uint_summation(k, begin, f)) = summation(toNat(k), toNat(begin), fun i { toNat(f(fromNat(i))) }))

define uint_summation : (fn (UInt, UInt, (fn UInt -> UInt)) -> UInt) = fun k:UInt, begin:UInt, f:(fn UInt -> UInt) {
      fromNat(summation(toNat(k), toNat(begin), fun i { toNat(f(fromNat(i))) }))
    }

uint_summation_add: (all a:UInt. (all b:UInt, s:UInt, t:UInt, f:(fn UInt -> UInt), g:(fn UInt -> UInt), h:(fn UInt -> UInt). (if ((all i:Nat. (if i < toNat(a) then g(s + fromNat(i)) = f(s + fromNat(i)))) and (all i:Nat. (if i < toNat(b) then h(t + fromNat(i)) = f((s + a) + fromNat(i))))) then uint_summation(a + b, s, f) = uint_summation(a, s, g) + uint_summation(b, t, h))))

uint_summation_cong: (all k:UInt. (all f:(fn UInt -> UInt), g:(fn UInt -> UInt), s:UInt, t:UInt. (if (all i:Nat. (if i < toNat(k) then f(s + fromNat(i)) = g(t + fromNat(i)))) then uint_summation(k, s, f) = uint_summation(k, t, g))))

uint_summation_const_one: (all n:UInt. (all s:UInt. uint_summation(n, s, fun i:UInt { 1 }) = n))

uint_summation_id: (all n:UInt. 2 * uint_summation(n, 0, fun i:UInt { i }) = n * (n ∸ 1))

uint_summation_next: (all n:UInt, s:UInt, f:(fn UInt -> UInt). uint_summation(1 + n, s, f) = uint_summation(n, s, f) + f(s + n))

uint_summation_pow2_succ: (all n:UInt. 1 + uint_summation(n, 0, fun i:UInt { 2 ^ i }) = 2 ^ n)

uint_summation_pow_succ: (all a:UInt. (if 1 ≤ a then (all n:UInt. 1 + (a ∸ 1) * uint_summation(n, 0, fun i:UInt { a ^ i }) = a ^ n)))