The **dom** predicate defined earlier in the chapter is used here
to demonstrate induction.
Given the definitions

~<T>== (<T>) -> void some <v>:<A>.<P>== <v>:(<A>)#(<P>) N== {n:int| ~(n<0)} true== (0 in int) D(<x>)== rec(dom,x. int_eq(f(x); 0; true; dom(x+1)); <x>)figure sketches the proof of

f:N->N, r:D(0) >> some y:N. f(y)=0.Although

**Figure:** A Sample Proof Using Recursion

Thu Sep 14 08:45:18 EDT 1995