Go backward to Factorial Function Go up to Top Go forward to Simultaneous Definitions

Double Recursion

g = lambda n. n equals zero -> one
    [] (g(n minus one) plus
        g(n minus one)) minus one

graph(F⁰(_|_)) = {}
graph(F¹(_|_)) = {(zero, one)}
graph(F¹(_|_)) = {(zero, one), (one, one)}
graph(F²(_|_)) = {(zero, one), (one, one), (two, one)}
...
graph(Fⁱ⁺¹(_|_)) = {(zero, one), ..., (i, one)}

fix F = lambda n. one

Stepwise construction of graph yields insight!