div_nt_alt: THEORY BEGIN IMPORTING div_nt n: VAR nat m: VAR posnat natdiv(n,m): RECURSIVE nat = (IF n>=m THEN 1+natdiv(n-m, m) ELSE 0 ENDIF) MEASURE (LAMBDA n,m: n) i,k: VAR int j: VAR nonzero_integer is_multiple(i,j): bool = (EXISTS k: i = k*j) rdiv(i,j): integer = IF sgn(i) = sgn(j) THEN natdiv(abs(i),abs(j)) ELSIF is_multiple(i,j) THEN -natdiv(abs(i),abs(j)) ELSE -natdiv(abs(i),abs(j))-1 ENDIF floor_is_natdiv: LEMMA natdiv(n,m) = floor(n/m) rdiv_lem: LEMMA div(i,j) = rdiv(i,j) END div_nt_alt