?- brutCV('xml/qrd.xml').

1 : a=d*q+r et r<d et 0<=r et Q(d,b)et non 0>b-d imp a=b*q+r et r>=0 et r<b

2 : 0<=a et Q(t,b)et non t-a<=0 imp a=t*0+a et a<t et 0<=a et Q(t,b)

3 : a>=0 et b>0 imp 0<=a et Q(b,b)

4 : 0<=a et Q(t,b)et t-a<=0 imp 0<=a et Q(2*t,b)

5 : a=d*q+r et r<d et 0<=r et Q(d,b)et 0>b-d imp (r-d/2>=0 imp a=d/2* (2*q+1)+ (r-d/2)et r-d/2<d/2 et 0<=r-d/2 et Q(d/2,b))

6 : a=d*q+r et r<d et 0<=r et Q(d,b)et 0>b-d imp (non r-d/2>=0 imp a=d/2* (2*q)+r et r<d/2 et 0<=r et Q(d/2,b))

true ;
false.