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))) }))

fun uint_summation(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_next: (all n:UInt, s:UInt, f:(fn UInt -> UInt). uint_summation(1 + n, s, f) = uint_summation(n, s, f) + f(s + n))