# Definition

def f(v, i):
    if v == []:
        return 0
    elif i == 0:
        return v[0]
    else:
        return f(v, i - 1) + f(v[1:], i - 1)


# Thorem 1

f(v1 + v2, i) = f(v1, i) + f(v2, i)

Proof by induction is trivial.

# Theorem 2

Let vk be [0, 0, …, 1] with len(vk) = k + 1. Then:

f(v0, i) = 1
f(vk, i) = f(v(k-1), i) * (i - k + 1) / k

examples:
f(v1, i) = i
f(v2, i) = i * (i - 1) / 2
f(v3, i) = i * (i - 1) * (i - 2) / 6

Proof by induction:

i=0 k=0:
    f(v0, 0) = 1
i>0 k=0:
    f(v0, i)
    = f(v0, i - 1) + f([], i - 1)
    = 1 + 0
i=0 k=1:
    0 = v1[0] = f(v1, 0) = f(v0, 0) * (0 - 1 + 1) / 1 = 1 * 0 = 0
i=0 k>1:
    0 = vk[0] = f(vk, 0) = f(v(k - 1), 0) * (0 - k + 1) / k = 0 * (1 - k) / k = 0
i>0 k>1:
    f(vk, i)
    = f(vk, i - 1) + f(v(k-1), i - 1)  | definition
    = f(v(k-1), i - 1) * ((i - 1) - k + 1) / k + f(v(k-1), i - 1)
    = f(v(k-1), i - 1) * (i - k + 1) / k + f(v(k-1), i - 1) * (k - 1) / k  | theorem 1
    = f(v(k-1), i - 1) * (i - k + 1) / k + f(v(k-2), i - 1) * ((i - 1) - (k - 1) + 1) / (k - 1) * (k - 1) / k
    = (f(v(k-1), i - 1) + f(v(k-2), i - 1)) * (i - k + 1) / k  | definition
    = f(v(k-1), i) * (i - k + 1) / k

# Conjectures

f([a, b, …], i) = a * f(v0, i) + b * f(v1, i) + …