0 GTRS
tail(cons(X)) → L incr(nil) → nil incr(cons(X)) → cons(s(X)) adx(nil) → nil adx(cons(X)) → incr(cons(X)) nats → adx(zeros) zeros → cons(0) head(cons(X)) → X