1load_package redlog; 2 3 4rlset mri; 5 6 7 8{} 9 10on rlverbose; 11 12 13 14mrireal x,y; 15 16 17 18wex := ex(x,0<y-x and 4(y-x)<1 and cong(2x,1,2)); 19 20 21wex := ex x (x - y < 0 and - 4*x + 4*y - 1 < 0 and 2*x - 1 ~2~ 0) 22 23 24rlqe wex$ 25 26++++++ MRI entering mri_qe 27+++++ MRI current block is (ex x) 28++++ MRI picking next variable from (x) ... x (real) 29+++ MRI expanding bounded quantifiers for real qe - no changes 30+++ MRI truncating x 31x_trunc >= 0 and x_trunc - 1 < 0 and x_int + x_trunc - y < 0 32 33 and 4*x_int + 4*x_trunc - 4*y + 1 > 0 and 2*x_int + 2*x_trunc - 1 ~2~ 0 34 35++++ MRI introduced new quantified variables x_trunc and x_int for x 36+++ MRI applying Lemma 3.3 (remove x_trunc from floors) - no changes 37+++ MRI applying Theorem 3.1 Case 2 (remove x_trunc from congruences) 38x_trunc >= 0 and x_trunc - 1 < 0 and x_int + x_trunc - y < 0 39 40 and 4*x_int + 4*x_trunc - 4*y + 1 > 0 and 2*x_trunc - 1 = 0 41 42+++ MRI entering real qe for x_trunc ... finished 432*x_int - 2*y + 1 < 0 and 4*x_int - 4*y + 3 > 0 44 45++++ MRI picking next variable from (x_int) ... x_int (integer) 46+++ MRI applying Lemma 3.2 (remove x_int from floors) - no changes 47+++ MRI applying Theorem 3.1 Case 1 (restrict x_int to integer atfs) 48([2*y] - 2*x_int - 1 > 0 or ([2*y] - 2*x_int - 1 = 0 and [2*y] - 2*y < 0)) 49 50 and [4*y] - 4*x_int - 2 <= 0 51 52+++ MRI entering integer qe for x_int ... finished 53([4*y] - 2*[2*y] <= 0 and [2*y] - 2*y < 0 and [2*y] + 1 ~2~ 0) or bex g0002 [0 54 55 <= g0002 <= 4] ([4*y] - 2*[2*y] + g0002 < 0 and [4*y] + g0002 + 2 ~4~ 0) or bex 56 57 g0002 [ - 2 <= g0002 <= -1] ([4*y] - 2*[2*y] - 2*g0002 <= 0 58 59 and [2*y] + g0002 + 1 ~2~ 0) 60 61 62 63rlexpand ws; 64 65 66([4*y] - 2*[2*y] + 1 < 0 and [2*y] ~2~ 0) 67 68 or ([4*y] - 2*[2*y] + 3 < 0 and [2*y] + 1 ~2~ 0) 69 70 or ([4*y] - 2*[2*y] + 4 < 0 and [4*y] + 2 ~4~ 0) 71 72 or ([4*y] - 2*[2*y] + 3 < 0 and [4*y] + 1 ~4~ 0) 73 74 or ([4*y] - 2*[2*y] + 2 < 0 and [4*y] ~4~ 0) 75 76 or ([4*y] - 2*[2*y] + 1 < 0 and [4*y] + 3 ~4~ 0) 77 78 or ([4*y] - 2*[2*y] < 0 and [4*y] + 2 ~4~ 0) 79 80 or ([2*y] + 1 ~2~ 0 and [2*y] - 2*y < 0 and [4*y] - 2*[2*y] <= 0) 81 82 83end; 84 85Tested on x86_64-pc-windows CSL 86Time (counter 1): 0 ms 87 88End of Lisp run after 0.00+0.09 seconds 89real 0.26 90user 0.01 91sys 0.04 92