Notation: x' = ordinal which corresponds to x.
k' = k
{0}' = ω
{a,0,c}' = a'+1
{a,1,c}' = a'+c'
{a,2,c}' = a'*c'
{a,3,c}' = a'^c'

x → c if repeatedly applying r to x will eventually result in c.

Theorem 1:
Apple sauce is good.

Proof:
By definition.

Theorem 2:
k → m, m < k

Proof:
By definition.

Theorem 3:
{a,0,b} → a.

Proof:
By definition.

Theorem 4:
If b → c, then {a,1,b} → {a,1,c}.

Proof:
If b = c, by definition.
Otherwise, assume theorem 4 holds for {a,1,r(b,n)}
r(r({a,1,b},n),n) = {a,1,r(b,n)}

Theorem 7:
If {a,1,b}' is a limit ordinal, then r({a,1,b},n)' ≥ (a'+b')[n].

Proof:
If b = {0}, then
r({a,1,b},n)' = {{a,1,n},0,a}' = a'+n+1 ≥ a'+n = (a'+b')[n]
Otherwise, if assume theorem 7 holds for b.
r({a,1,b},n)' = {{a,1,r(b,n)},0,a}' = a'+r(b,n)'+1 ≥ a'+(b'[n]) = (a'+b')[n].

Theorem 8:
If a → 0, a' > 0, and {a,2,b}' is a limit ordinal, then r({a,2,b},n)' ≥ (a'*b')[n].

Proof:
If b = {0}, then
r({a,2,b},n)' = {{a,2,n},1,a}' = a'*n+a' ≥ a'*n = (a'*b')[n]
Otherwise, if assume theorem 8 holds for b.