NAME fractions MODE PROOF SORTS Q SIGNATURE divide: Q Q -> Q plus: Q Q -> Q minus: Q -> Q zero: -> Q one: -> Q a: -> Q ORDERING KBO plus=1, minus=1, divide=1, zero=1, one=1, a=1 divide > plus > minus > zero > one > a VARIABLES x,y,z : Q EQUATIONS plus(x,zero) = x plus(x,minus(x)) = zero plus(x,plus(y,z)) = plus(plus(x,y),z) plus(divide(x,z),divide(y,z)) = divide(plus(x,y),z) divide(x,x) = one % The previous equation allows to derive zero = one. % To fix the bug, replace it by % divide(plus(a,one),plus(a,one)) = one CONCLUSION divide(a,plus(a,one)) = plus(one,divide(minus(one),plus(a,one)))