*[s [5 0 1]] i.e., *[s [5 [0 1]]] -- because [a b c] == [a [b c]] i.e., *[s 5 [0 1]] -- because [a [b c]] == [a b c] => ^*[s [0 1]] -- by *[a 5 b] => ^*[a b] i.e., ^*[s 0 1] -- because [a [b c]] == [a b c] => ^/[1 s] -- by *[a 0 b] => /[b a] => ^s -- by /[1 a] => a => (s + 1) -- by ^a => (a + 1)