fmod INT is *** protecting BOOL . sort Int . op 0 : -> Int . op s : Int -> Int . op p : Int -> Int . op _+_ : Int Int -> Int . op _-_ : Int Int -> Int . op _*_ : Int Int -> Int . op -_ : Int -> Int . op _<=_ : Int Int -> Bool . vars N M : Int . eq s(p(N)) = N . eq p(s(N)) = N . eq 0 + N = N . eq s(M) + N = s(M + N) . eq p(M) + N = p(M + N) . eq N - 0 = N . eq M - s(N) = p(M - N) . eq M - p(N) = s(M - N) . eq 0 * N = 0 . eq s(M) * N = (M * N) + N . eq p(M) * N = (M * N) - N . eq s(M) <= N = M <= p(N) . eq p(M) <= N = M <= s(N) . eq 0 <= 0 = true . eq 0 <= p(0) = false . ceq 0 <= s(M) = true if 0 <= M . ceq 0 <= p(M) = false if not 0 <= M . endfm red s(s(s(0))) * s(s(0)) <= s(s(s(0)) - s(0)) . ***( reduce in INT : (s(s(s(0))) * s(s(0))) <= s(s(s(0)) - s(0)) . rewrites: 34 in -10ms cpu (0ms real) (~ rewrites/second) result Bool: false ) red s(s(s(0))) * p(p(0)) <= s(p(s(0)) - s(0)) . ***( reduce in INT : (s(s(s(0))) * p(p(0))) <= s(p(s(0)) - s(0)) . rewrites: 30 in -10ms cpu (0ms real) (~ rewrites/second) result Bool: true ) set trace on . red p(p(p(s(s(s(0)))))) <= s(p(s(0))) . ***( **************************************** The trace has been extended by hand **************************************** to highlight the subterm being **************************************** rewritten. reduce in INT : p(p(p(s(s(s(0)))))) <= s(p(s(0))) . *********** equation eq p(s(N)) = N . N:Int --> s(s(0)) p(s(s(s(0)))) ---> s(s(0)) **************************************** p(p(p(s(s(s(0)))))) <= s(p(s(0))) **************************************** ------------- **************************************** p(p( s(s(0)) )) <= s(p(s(0))) *********** equation eq p(s(N)) = N . N:Int --> s(0) p(s(s(0))) ---> s(0) **************************************** p(p(s(s(0)))) <= s(p(s(0))) **************************************** ---------- **************************************** p( s(0) ) <= s(p(s(0))) *********** equation eq p(s(N)) = N . N:Int --> 0 p(s(0)) ---> 0 **************************************** p(s(0)) <= s(p(s(0))) **************************************** ------- **************************************** 0 <= s(p(s(0))) *********** equation eq p(s(N)) = N . N:Int --> 0 p(s(0)) ---> 0 **************************************** 0 <= s(p(s(0))) **************************************** ------- **************************************** 0 <= s( 0 ) *********** trial #1 ceq 0 <= s(M) = true if 0 <= M = true . M:Int --> 0 *********** equation eq 0 <= 0 = true . empty substitution 0 <= 0 ---> true *********** success #1 *********** equation ceq 0 <= s(M) = true if 0 <= M = true . M:Int --> 0 0 <= s(0) ---> true rewrites: 6 in -10ms cpu (0ms real) (~ rewrites/second) result Bool: true **************************************** 0 <= s( 0 ) **************************************** --------------- **************************************** true ) set trace off .