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