Last change
on this file since 1 was 1, checked in by Marek Rychlik, 15 years ago |
First import of a version circa 1997.
|
File size:
426 bytes
|
Line | |
---|
1 | if get('geometry2, 'version)=false then load(geometry2);
|
---|
2 | X:[x1,y1]; Y:[x2,y2]; O1:[a,0]; O2:[-a,0];
|
---|
3 | vars:[x1,y1,x2,y2,r1,r2,s1,s2,v]; params:[a];
|
---|
4 | cover:[[],[a]];
|
---|
5 | u:2/(1-a^2);
|
---|
6 | concl:r1+s1-u*r1*s1;
|
---|
7 |
|
---|
8 |
|
---|
9 | eqns:[
|
---|
10 | distance(X,O1,r1),
|
---|
11 | distance(X,O2,r2),
|
---|
12 | r1+r2-2,
|
---|
13 | distance(Y,O1,s1),
|
---|
14 | distance(Y,O2,s2),
|
---|
15 | s1+s2-2,
|
---|
16 | collinear(X,Y,O1),
|
---|
17 | 1-v*concl
|
---|
18 | ];
|
---|
19 |
|
---|
20 | eqns:expand(eqns);
|
---|
21 | cover:expand(cover);
|
---|
22 | stringout("klee.out",eqns,vars,params,cover);
|
---|
Note:
See
TracBrowser
for help on using the repository browser.