ADT NAT [ ] INITIALS ZERO : -> NAT CONSTRUCTORS SUC : NAT -> NAT SELECTORS ADD : NAT * NAT(i) -> NAT ISZERO : NAT(i) -> BOOL MULT : NAT(i) * NAT -> NAT PRED : NAT(i) -> NAT MAX : NAT(i) * NAT(i) -> NAT MIN : NAT(i) * NAT(i) -> NAT GT : NAT(i) * NAT(i) -> BOOL LT : NAT(i) * NAT(i) -> BOOL GE : NAT * NAT -> BOOL LE : NAT * NAT -> BOOL FACT : NAT(i) -> NAT EXP : NAT * NAT(i) -> NAT EVEN : NAT(i) -> BOOL ODD : NAT(i) -> BOOL DIV : NAT * NAT -> NAT MOD : NAT * NAT -> NAT DIVIDES : NAT * NAT -> BOOL SUBS : NAT * NAT(i) -> NAT EQ_NAT (c): NAT(i) * NAT(i) -> BOOL AXIOMS ADD(N1,ZERO) = N1 ADD(N1,SUC(N2)) = SUC(ADD(N1,N2)) ISZERO(ZERO) = TRUE ISZERO(SUC(N1)) = FALSE MULT(ZERO,N1) = ZERO MULT(SUC(N1),N2) = ADD(MULT(N1,N2),N2) PRED(ZERO) = ZERO PRED(SUC(N1)) = N1 MAX(ZERO,ZERO) = ZERO MAX(ZERO,SUC(N1)) = SUC(N1) MAX(SUC(N1),ZERO) = SUC(N1) MAX(SUC(N1),SUC(N2)) = SUC(MAX(N1,N2)) MIN(ZERO,ZERO) = ZERO MIN(ZERO,SUC(N1)) = ZERO MIN(SUC(N1),ZERO) = ZERO MIN(SUC(N1),SUC(N2)) = SUC(MIN(N1,N2)) GT(ZERO,ZERO) = FALSE GT(ZERO,SUC(N1)) = FALSE GT(SUC(N1),ZERO) = TRUE GT(SUC(N1),SUC(N2)) = GT(N1,N2) LT(ZERO,ZERO) = FALSE LT(ZERO,SUC(N1)) = TRUE LT(SUC(N1),ZERO) = FALSE LT(SUC(N1),SUC(N2)) = LT(N1,N2) GE(N1,N2) = OR(EQ_NAT(N1,N2),GT(N1,N2)) LE(N1,N2) = OR(EQ_NAT(N1,N2),LT(N1,N2)) FACT(ZERO) = SUC(ZERO) FACT(SUC(N1)) = MULT(SUC(N1),FACT(N1)) EXP(N1,ZERO) = SUC(ZERO) EXP(N1,SUC(N2)) = MULT(EXP(N1,N2),N1) EVEN(ZERO) = TRUE EVEN(SUC(ZERO)) = FALSE EVEN(SUC(SUC(N1))) = EVEN(N1) ODD(ZERO) = FALSE ODD(SUC(ZERO)) = TRUE ODD(SUC(SUC(N1))) = ODD(N1) DIV(N1,N2) = if ISZERO(N2) then ERROR else if GE(N1,N2) then SUC(DIV(SUBS(N1,N2),N2)) else ZERO fi fi MOD(N1,N2) = if ISZERO(N2) then ERROR else if GE(N1,N2) then MOD(SUBS(N1,N2),N2) else N1 fi fi DIVIDES(N1,N2) = ISZERO(MOD(N2,N1)) SUBS(N1,ZERO) = N1 SUBS(N1,SUC(N2)) = PRED(SUBS(N1,N2)) EQ_NAT(ZERO,ZERO) = TRUE EQ_NAT(ZERO,SUC(N1)) = FALSE EQ_NAT(SUC(N1),ZERO) = FALSE EQ_NAT(SUC(N1),SUC(N2)) = EQ_NAT(N1,N2)