1on rlverbose;
2
3% Ordered fields standard form:
4rlset ofsf;
5rlset();
6
7% Chains
8-3/5<x>y>z<=a<>b>c<5/3;
9
10% For-loop actions.
11g := for i:=1:6 mkor
12   for j := 1:6 mkand
13      mkid(a,i) <= mkid(a,j);
14
15% Quantifier elimination and variants
16h := rlsimpl rlall g;
17rlmatrix h;
18on rlrealtime;
19rlqe h;
20off rlrealtime;
21
22h := rlsimpl rlall(g,{a2});
23rlqe h;
24
25off rlqeheu,rlqedfs;
26rlqe ex(x,a*x**2+b*x+c>0);
27on rlqedfs;
28rlqe ex(x,a*x**2+b*x+c>0);
29on rlqeheu;
30
31rlqe(ex(x,a*x**2+b*x+c>0),{a<0});
32
33rlgqe ex(x,a*x**2+b*x+c>0);
34rlthsimpl ({a*b*c=0,b<>0});
35
36
37rlqe ex({x,y},(for i:=1:5 product mkid(a,i)*x**10-mkid(b,i)*y**2)<=0);
38
39sol := rlqe ex(x,a1*a2*x**2+b*x+c>0);
40rlatnum sol;
41rldepth sol;
42
43rlatl sol;
44rlatml sol;
45rlterml sol;
46rltermml sol;
47rlifacl sol;
48rlifacml sol;
49
50rlstruct(sol, fac=no, w);
51rlstruct(sol);
52
53rltab sol;
54rlatnum ws;
55rlgsn sol;
56rlatnum ws;
57
58off rlverbose;
59
60rlqea ex(x,m*x+b=0);
61
62% Substitution
63sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x>a));
64
65% Boolean normal forms.
66f1 := x=0 and b>=0;
67f2 := a=0;
68f := f1 or f2;
69
70rlcnf f;
71
72rldnf ws;
73
74rlcnf f;
75
76% Negation normal form and prenex normal form
77hugo := a=0 and b=0 and y<0 equiv ex(y,y>=a) or a>0;
78rlnnf hugo;
79rlpnf hugo;
80
81% Length and Part
82part(hugo,0);
83part(hugo,2,1,2);
84length ws;
85length hugo;
86length part(hugo,1);
87
88% Tableau
89mats := all(t,ex({l,u},(
90(t>=0 and t<=1) impl
91(l>0 and u<=1 and
92  -t*x1+t*x2+2*t*x1*u+u=l*x1 and
93  -2*t*x2+t*x2*u=l*x2))));
94sol := rlgsn rlqe mats;
95rltab(sol,{x1>0,x1<0,x1=0});
96
97% Part on psopfn / cleanupfn
98part(rlqe ex(x,m*x+b=0),1);
99walter := (x>0 and y>0);
100rlsimpl(true,rlatl walter);
101part(rlatl walter,1,1);
102
103% QE by partial CAD:
104cox6 := ex({u,v},x=u*v and y=u**2 and z=v**2)$
105rlcad cox6;
106
107% Generate Theory
108rlgentheo({a=0}, a*x+b<>0);
109
110% Algebraically closed fields standard form:
111sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x<>a));
112
113rlset acfsf;
114
115rlsimpl(x^2+y^2+1<>0);
116
117rlqe ex(x,x^2=y);
118
119clear f;
120h := rlqe ex(x,x^3+a*x^2+b*x+c=0 and x^3+d*x^2+e*x+f=0);
121rlstruct h;
122rlqe rlall (h equiv resultant(x^3+a*x^2+b*x+c,x^3+d*x^2+e*x+f,x)=0);
123clear h;
124
125% Discretely valued fields standard form:
126rlset dvfsf;
127sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,x~a));
128
129% P-adic Balls, taken from Andreas Dolzmann, Thomas Sturm. P-adic
130% Constraint Solving, Proceedings of the ISSAC '99.
131rlset dvfsf;
132rlqe all(r_1,all(r_2,all(a,all(b,
133ex(x,r_1||x-a and r_2||x-b and r_1|r_2) impl
134all(y,r_2||y-b impl r_1||y-a)))));
135rlmkcanonic ws;
136rlset(dvfsf,100003);
137rlqe all(r_1,all(r_2,all(a,all(b,
138ex(x,r_1||x-a and r_2||x-b and r_1|r_2) impl
139all(y,r_2||y-b impl r_1||y-a)))));
140
141% Size of the Residue Field, taken from Andreas Dolzmann, Thomas
142% Sturm. P-adic Constraint Solving. Proceedings of the ISSAC '99.
143rlset(dvfsf);
144rlqe ex(x,x~1 and x-1~1 and x-2~1 and x-3~1 and 2~1 and 3~1);
145rlexplats ws;
146rldnf ws;
147
148% Differentially closed fields standard form:
149rlset dcfsf;
150sub(x=a,x=0 and a=0 and ex(x,x=y) and ex(a,d(x, 4) <> a));
151
152% An Example on Differential Algebras by E. Pankratiev taken from A. Dolzmann,
153% T. Sturm. Generalized Constraint Solving over Differential Algebras.
154% Proceedings of the CASC 2004.
155pankratiev := all(x,d(x, 1)**2 + x = 0 impl (d(x, 1) = a or d(x, 2) = b));
156rlqe pankratiev;
157
158% Selecting contexts:
159
160rlset acfsf;
161f:= ex(x,m*x+b=0);
162rlqe f;
163rlset dcfsf;
164rlqe f;
165rlset dvfsf;
166rlqe f;
167rlset ofsf;
168rlqe f;
169
170end;  % of file
171