bit (boolean) simpler constructor no, yes (nay, yea; false, true) control flow command xcond, cond, if statement, if expression (ternary if) natural simpler of arbitrary size constructor zero, successor(natural) basic control flow command primitive repetition (times, nat_iter) destructor predecessor(natural) conversion to bit positive derivative control flow command primitive repetition (times binding, primrec, pascal's for, fold) version number simpler with arbitrary number of predecessors constructor initial, version_successor(version,natural) destructor version_predecessor(version,natural,natural) conversion to natural most_significative_component (leftmost_component) control flow command lexicographic-recursion, recursion + heuristic termination proof, nat_iter + higher-order functions + heuristic termination proof