cgb.rlg 57 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808809810811812813814815816817818819820821822823824825826827828829830831832833834835836837838839840841842843844845846847848849850851852853854855856857858859860861862863864865866867868869870871872873874875876877878879880881882883884885886887888889890891892893894895896897898899900901902903904905906907908909910911912913914915916917918919920921922923924925926927928929930931932933934935936937938939940941942943944945946947948949950951952953954955956957958959960961962963964965966967968969970971972973974975976977978979980981982983984985986987988989990991992993994995996997998999100010011002100310041005100610071008100910101011101210131014101510161017101810191020102110221023102410251026102710281029103010311032103310341035103610371038103910401041104210431044104510461047104810491050105110521053105410551056105710581059106010611062106310641065106610671068106910701071107210731074107510761077107810791080108110821083108410851086108710881089109010911092109310941095109610971098109911001101110211031104110511061107110811091110111111121113111411151116111711181119112011211122112311241125112611271128112911301131113211331134113511361137113811391140114111421143114411451146114711481149115011511152115311541155115611571158115911601161116211631164116511661167116811691170117111721173117411751176117711781179118011811182118311841185118611871188118911901191119211931194119511961197119811991200120112021203120412051206120712081209121012111212121312141215121612171218121912201221122212231224122512261227122812291230123112321233123412351236123712381239124012411242124312441245124612471248124912501251125212531254125512561257125812591260126112621263126412651266126712681269127012711272127312741275127612771278127912801281128212831284128512861287128812891290129112921293129412951296129712981299130013011302130313041305130613071308130913101311131213131314131513161317131813191320132113221323132413251326132713281329133013311332133313341335133613371338133913401341134213431344134513461347134813491350135113521353135413551356135713581359136013611362136313641365136613671368136913701371137213731374137513761377137813791380138113821383138413851386138713881389139013911392139313941395139613971398139914001401140214031404140514061407140814091410141114121413141414151416141714181419142014211422142314241425142614271428142914301431143214331434143514361437143814391440144114421443144414451446144714481449145014511452145314541455145614571458145914601461146214631464146514661467146814691470147114721473147414751476147714781479148014811482148314841485148614871488148914901491149214931494149514961497149814991500150115021503150415051506150715081509151015111512151315141515151615171518151915201521152215231524152515261527152815291530153115321533153415351536153715381539154015411542154315441545154615471548154915501551155215531554155515561557155815591560156115621563156415651566156715681569157015711572157315741575157615771578157915801581158215831584158515861587158815891590159115921593159415951596159715981599160016011602160316041605160616071608160916101611161216131614161516161617161816191620162116221623162416251626162716281629163016311632163316341635163616371638163916401641164216431644164516461647164816491650165116521653165416551656165716581659166016611662166316641665166616671668166916701671167216731674167516761677167816791680168116821683168416851686168716881689169016911692169316941695169616971698169917001701170217031704170517061707170817091710171117121713171417151716171717181719172017211722172317241725172617271728172917301731173217331734173517361737173817391740174117421743174417451746174717481749175017511752175317541755175617571758175917601761176217631764176517661767176817691770177117721773177417751776177717781779178017811782178317841785178617871788178917901791179217931794179517961797179817991800180118021803180418051806180718081809181018111812181318141815181618171818181918201821182218231824182518261827182818291830183118321833183418351836183718381839184018411842184318441845184618471848184918501851185218531854185518561857185818591860186118621863186418651866186718681869187018711872187318741875187618771878187918801881188218831884188518861887188818891890189118921893189418951896189718981899190019011902190319041905190619071908190919101911191219131914191519161917191819191920192119221923192419251926192719281929193019311932193319341935193619371938193919401941194219431944194519461947194819491950195119521953195419551956195719581959196019611962196319641965196619671968196919701971197219731974197519761977197819791980198119821983198419851986198719881989199019911992199319941995199619971998199920002001200220032004200520062007200820092010201120122013201420152016201720182019202020212022202320242025202620272028202920302031203220332034203520362037203820392040204120422043204420452046204720482049205020512052205320542055205620572058205920602061206220632064206520662067206820692070207120722073207420752076207720782079208020812082208320842085208620872088208920902091209220932094209520962097209820992100210121022103210421052106210721082109211021112112211321142115211621172118211921202121212221232124212521262127212821292130213121322133213421352136213721382139214021412142214321442145214621472148214921502151215221532154215521562157215821592160216121622163216421652166216721682169217021712172217321742175217621772178217921802181218221832184218521862187218821892190219121922193219421952196219721982199220022012202220322042205220622072208220922102211221222132214221522162217221822192220222122222223222422252226222722282229223022312232223322342235223622372238223922402241224222432244224522462247224822492250225122522253225422552256225722582259226022612262226322642265226622672268226922702271227222732274227522762277227822792280228122822283228422852286228722882289229022912292229322942295229622972298229923002301230223032304230523062307
  1. Tue Apr 15 00:35:15 2008 run on win32
  2. % ----------------------------------------------------------------------
  3. % $Id: cgb.tst,v 1.3 2003/10/12 14:55:24 sturm Exp $
  4. % ----------------------------------------------------------------------
  5. % Copyright (c) 1999 Andreas Dolzmann and Thomas Sturm
  6. % ----------------------------------------------------------------------
  7. % $Log: cgb.tst,v $
  8. % Revision 1.3 2003/10/12 14:55:24 sturm
  9. % The bootstrapping technique via remflag('(load!-package),'eval); does
  10. % not work for CSL. Added corresponding preprocessing directive for now.
  11. % As a consequence, under CSL "redlog" has to be loaded explicitly when
  12. % using CGB.
  13. %
  14. % Revision 1.2 1999/04/13 21:50:44 sturm
  15. % Removed echo, and gbverbose settings. There is no gbverbose.
  16. %
  17. % Revision 1.1 1999/04/05 08:30:45 dolzmann
  18. % Copied and overworked Rev. 1.6 of the old cgb version.
  19. %
  20. % ----------------------------------------------------------------------
  21. load_package redlog;
  22. % Examples taken from the manual:
  23. load_package groebner;
  24. % 1 Introduction
  25. oo := torder({x,y},lex)$
  26. cgb {a*x,x+y};
  27. {x + y,a*x,a*y}
  28. gsys {a*x,x+y};
  29. {{a <> 0,{x + y,a*x,a*y}},
  30. {a = 0,{x + y}}}
  31. torder oo;
  32. {{x,y},lex}
  33. % 4 CGB: Comprehensive Groebner Basis
  34. oo := torder({x,y},lex)$
  35. cgb {a*x+y,x+b*y};
  36. {x + b*y,a*x + y,(a*b - 1)*y}
  37. torder oo;
  38. {{x,y},lex}
  39. % 5 GSYS: Groebner System
  40. oo := torder({x,y},lex)$
  41. gsys {a*x+y,x+b*y};
  42. {{a*b - 1 <> 0 and a <> 0,
  43. {a*x + y,x + b*y,(a*b - 1)*y}},
  44. {a <> 0 and a*b - 1 = 0,
  45. {a*x + y,x + b*y}},
  46. {a = 0,{a*x + y,x + b*y}}}
  47. torder oo;
  48. {{x,y},lex}
  49. % 6 GSYS2CGB: Groebner System to CGB
  50. oo := torder({x,y},lex)$
  51. gsys {a*x+y,x+b*y};
  52. {{a*b - 1 <> 0 and a <> 0,
  53. {a*x + y,x + b*y,(a*b - 1)*y}},
  54. {a <> 0 and a*b - 1 = 0,
  55. {a*x + y,x + b*y}},
  56. {a = 0,{a*x + y,x + b*y}}}
  57. gsys2cgb ws;
  58. {x + b*y,a*x + y,(a*b - 1)*y}
  59. torder oo;
  60. {{x,y},lex}
  61. % 7 Switch CGBREAL: Computing over the Real Numbers
  62. oo := torder({x,y},lex)$
  63. off cgbreal;
  64. gsys {a*x+y,x-a*y};
  65. 2
  66. {{a + 1 <> 0 and a <> 0,
  67. 2
  68. {a*x + y,x - a*y,(a + 1)*y}},
  69. 2
  70. {a <> 0 and a + 1 = 0,{a*x + y,x - a*y}},
  71. {a = 0,{a*x + y,x - a*y}}}
  72. on cgbreal;
  73. gsys({a*x+y,x-a*y});
  74. {{a <> 0,
  75. 2
  76. {a*x + y,x - a*y,(a + 1)*y}},
  77. {a = 0,{a*x + y,x - a*y}}}
  78. torder oo;
  79. {{x,y},lex}
  80. % Miscellaneous examples:
  81. % Dolzmann's Example
  82. oo := torder({x,y,z},lex);
  83. oo := {{},lex}
  84. cgb({a*x+b*y,c*x+d*y,(a*d-b*c)*z});
  85. {c*x + d*y,
  86. a*x + b*y,
  87. (a*d - b*c)*y,
  88. (a*d - b*c)*z}
  89. gsys({a*x+b*y,c*x+d*y,(a*d-b*c)*z});
  90. {{a*d - b*c <> 0 and a <> 0 and c <> 0,
  91. {a*x + b*y,
  92. c*x + d*y,
  93. (a*d - b*c)*y,
  94. (a*d - b*c)*z}},
  95. {a*d - b*c <> 0 and a <> 0 and d <> 0 and c = 0,
  96. {a*x + b*y,c*x + d*y,(a*d - b*c)*z}},
  97. {a*d - b*c <> 0 and a <> 0 and c = 0 and d = 0,
  98. {a*x + b*y,(a*d - b*c)*z}},
  99. {a*d - b*c <> 0 and b <> 0 and c <> 0 and a = 0,
  100. {a*x + b*y,c*x + d*y,(a*d - b*c)*z}},
  101. {a*d - b*c <> 0 and b <> 0 and d <> 0 and a = 0 and c = 0,
  102. {a*x + b*y,c*x + d*y,(a*d - b*c)*z}},
  103. {a*d - b*c <> 0 and b <> 0 and a = 0 and c = 0 and d = 0,
  104. {a*x + b*y,(a*d - b*c)*z}},
  105. {a*d - b*c <> 0 and c <> 0 and a = 0 and b = 0,
  106. {c*x + d*y,(a*d - b*c)*z}},
  107. {a*d - b*c <> 0 and d <> 0 and a = 0 and b = 0 and c = 0,
  108. {c*x + d*y,(a*d - b*c)*z}},
  109. {a*d - b*c <> 0 and a = 0 and b = 0 and c = 0 and d = 0,
  110. {(a*d - b*c)*z}},
  111. {a <> 0 and c <> 0 and a*d - b*c = 0,
  112. {a*x + b*y,c*x + d*y}},
  113. {a <> 0 and d <> 0 and a*d - b*c = 0 and c = 0,
  114. {a*x + b*y,c*x + d*y}},
  115. {a <> 0 and a*d - b*c = 0 and c = 0 and d = 0,
  116. {a*x + b*y}},
  117. {b <> 0 and c <> 0 and a*d - b*c = 0 and a = 0,
  118. {a*x + b*y,c*x + d*y}},
  119. {b <> 0 and d <> 0 and a*d - b*c = 0 and a = 0 and c = 0,
  120. {a*x + b*y,c*x + d*y}},
  121. {b <> 0 and a*d - b*c = 0 and a = 0 and c = 0 and d = 0,
  122. {a*x + b*y}},
  123. {c <> 0 and a*d - b*c = 0 and a = 0 and b = 0,
  124. {c*x + d*y}},
  125. {d <> 0 and a*d - b*c = 0 and a = 0 and b = 0 and c = 0,
  126. {c*x + d*y}},
  127. {a*d - b*c = 0 and a = 0 and b = 0 and c = 0 and d = 0,
  128. {}}}
  129. gsys2cgb ws;
  130. {c*x + d*y,
  131. a*x + b*y,
  132. (a*d - b*c)*y,
  133. (a*d - b*c)*z}
  134. torder oo;
  135. {{x,y,z},lex}
  136. % Forsman's Example (hybrid control system).
  137. oo := torder({x1,x2,y2,y1,y0},lex);
  138. oo := {{},lex}
  139. gsys({(u1*u2-u1)*x1+u2*x2+y2,(u2-1)*x1+u2*x2+y1,-x2+y0});
  140. {{u1*u2 - u1 <> 0,
  141. {(u1*u2 - u1)*x1 + u2*x2 + y2,
  142. (u2 - 1)*x1 + u2*x2 + y1,
  143. x2 - y0,
  144. y2 - u1*y1 - (u1*u2 - u2)*y0}},
  145. {u2 - 1 <> 0 and u2 <> 0 and u1*u2 - u1 = 0,
  146. {(u1*u2 - u1)*x1 + u2*x2 + y2,
  147. (u2 - 1)*x1 + u2*x2 + y1,
  148. (u1*u2 - u1)*x1 + y2 + u2*y0,
  149. x2 - y0}},
  150. {u1*u2 - u1 = 0 and u2 - 1 = 0,
  151. {(u1*u2 - u1)*x1 + u2*x2 + y2,
  152. (u2 - 1)*x1 + u2*x2 + y1,
  153. (u1*u2 - u1 - u2 + 1)*x1 + y2 - y1,
  154. (u2 - 1)*x1 + y1 + u2*y0,
  155. x2 - y0}},
  156. {u1*u2 - u1 = 0 and u2 = 0,
  157. {(u1*u2 - u1)*x1 + u2*x2 + y2,
  158. (u2 - 1)*x1 + u2*x2 + y1,
  159. x2 - y0}}}
  160. torder oo;
  161. {{x1,x2,y2,y1,y0},lex}
  162. % Weispfenning's Example
  163. oo := torder({x,y},lex);
  164. oo := {{},lex}
  165. gsys({v*x*y + x,u*y^2 + x^2});
  166. {{u*v <> 0 and v <> 0,
  167. 2 2
  168. {x + u*y ,
  169. v*x*y + x,
  170. 3 2
  171. (u*v)*y + u*y }},
  172. {u <> 0 and v <> 0 and u*v = 0,
  173. 2 2
  174. {x + u*y ,
  175. 3 3
  176. (u*v )*x*y + u*x,
  177. v*x*y + x,
  178. 3 2
  179. (u*v)*y + u*y }},
  180. {u <> 0 and v = 0,
  181. 2 2
  182. {v*x *y - u*y ,
  183. 2 2
  184. x + u*y ,
  185. v*x*y + x}},
  186. {v <> 0 and u*v = 0 and u = 0,
  187. 2 2
  188. {x + u*y ,v*x*y + x}},
  189. {u = 0 and v = 0,
  190. 2 2
  191. {x + u*y ,v*x*y + x}}}
  192. torder oo;
  193. {{x,y},lex}
  194. % The folllowing three examples are taken from
  195. % Weispfenning, Comprehensive Groebner Bases,
  196. % J. Symbolic Computation (1992) 14, 1-29
  197. % Weispfenning's Example 7.1
  198. oo := torder({x},lex);
  199. oo := {{},lex}
  200. gsys({a0*x**2 + a1*x + a2,b0*x**2 + b1*x + b2});
  201. 3 2 2 2 2 2 2
  202. {{a0 *b2 - a0 *a1*b1*b2 - 2*a0 *a2*b0*b2 + a0 *a2*b1 + a0*a1 *b0*b2
  203. 2 2
  204. - a0*a1*a2*b0*b1 + a0*a2 *b0 <> 0 and a0*b1 - a1*b0 <> 0 and a0 <> 0
  205. and b0 <> 0,
  206. 3 2 2 2 2 2 2
  207. {a0 *b2 - a0 *a1*b1*b2 - 2*a0 *a2*b0*b2 + a0 *a2*b1 + a0*a1 *b0*b2
  208. 2 2
  209. - a0*a1*a2*b0*b1 + a0*a2 *b0 }},
  210. 3 2 2
  211. {a0*b1 - a1*b0 <> 0 and a0 <> 0 and b0 <> 0 and a0 *b2 - a0 *a1*b1*b2
  212. 2 2 2 2 2 2
  213. - 2*a0 *a2*b0*b2 + a0 *a2*b1 + a0*a1 *b0*b2 - a0*a1*a2*b0*b1 + a0*a2 *b0
  214. = 0,
  215. 2
  216. {a0*x + a1*x + a2,
  217. 2
  218. b0*x + b1*x + b2,
  219. (a0*b1 - a1*b0)*x + (a0*b2 - a2*b0)}},
  220. 2 2
  221. {a0*b2 - a1*b1*b2 + a2*b1 <> 0 and a0 <> 0 and b1 <> 0 and b0 = 0,
  222. 3 2 2 2
  223. {(a0*b0*b1)*x - (a0*b0*b2 - a1*b0*b1)*x - (a0*b2 - a1*b1*b2 + a2*b1 )}},
  224. {a0*b2 - a2*b0 <> 0 and a0 <> 0 and b0 <> 0 and a0*b1 - a1*b0 = 0,
  225. {(a0*b1 - a1*b0)*x + (a0*b2 - a2*b0)}},
  226. {a0 <> 0 and b0 <> 0 and a0*b1 - a1*b0 = 0 and a0*b2 - a2*b0 = 0,
  227. 2 2
  228. {a0*x + a1*x + a2,b0*x + b1*x + b2}},
  229. 2 2
  230. {a0 <> 0 and b1 <> 0 and a0*b2 - a1*b1*b2 + a2*b1 = 0 and b0 = 0,
  231. 2 2
  232. {a0*x + a1*x + a2,b0*x + b1*x + b2}},
  233. {a0 <> 0 and b2 <> 0 and b0 = 0 and b1 = 0,
  234. 2
  235. {b0*x + b1*x + b2}},
  236. {a0 <> 0 and b0 = 0 and b1 = 0 and b2 = 0,
  237. 2
  238. {a0*x + a1*x + a2}},
  239. 2 2
  240. {a1 *b2 - a1*a2*b1 + a2 *b0 <> 0 and a1 <> 0 and b0 <> 0 and a0 = 0,
  241. 3 2 2 2
  242. {(a0*a1*b0)*x + (a0*a1*b1 - a0*a2*b0)*x - (a1 *b2 - a1*a2*b1 + a2 *b0)}},
  243. {a1*b2 - a2*b1 <> 0 and a1 <> 0 and b1 <> 0 and a0 = 0 and b0 = 0,
  244. 2
  245. {(a0*b1 - a1*b0)*x - (a1*b2 - a2*b1)}},
  246. 2 2
  247. {a1 <> 0 and b0 <> 0 and a0 = 0 and a1 *b2 - a1*a2*b1 + a2 *b0 = 0,
  248. 2 2
  249. {a0*x + a1*x + a2,b0*x + b1*x + b2}},
  250. {a1 <> 0 and b1 <> 0 and a0 = 0 and a1*b2 - a2*b1 = 0 and b0 = 0,
  251. 2 2
  252. {a0*x + a1*x + a2,b0*x + b1*x + b2}},
  253. {a1 <> 0 and b2 <> 0 and a0 = 0 and b0 = 0 and b1 = 0,
  254. 2
  255. {b0*x + b1*x + b2}},
  256. {a1 <> 0 and a0 = 0 and b0 = 0 and b1 = 0 and b2 = 0,
  257. 2
  258. {a0*x + a1*x + a2}},
  259. {a2 <> 0 and a0 = 0 and a1 = 0,
  260. 2
  261. {a0*x + a1*x + a2}},
  262. {b0 <> 0 and a0 = 0 and a1 = 0 and a2 = 0,
  263. 2
  264. {b0*x + b1*x + b2}},
  265. {b1 <> 0 and a0 = 0 and a1 = 0 and a2 = 0 and b0 = 0,
  266. 2
  267. {b0*x + b1*x + b2}},
  268. {b2 <> 0 and a0 = 0 and a1 = 0 and a2 = 0 and b0 = 0 and b1 = 0,
  269. 2
  270. {b0*x + b1*x + b2}},
  271. {a0 = 0 and a1 = 0 and a2 = 0 and b0 = 0 and b1 = 0 and b2 = 0,
  272. {}}}
  273. torder oo;
  274. {{x},lex}
  275. % Weispfenning's Example 7.2
  276. oo := torder({x,y},lex);
  277. oo := {{},lex}
  278. gsys({v*x*y + u*x**2 + x,u*y**2 + x**2});
  279. 4 3
  280. {{u *v + u*v <> 0 and u <> 0 and v <> 0,
  281. 2
  282. {u*x + v*x*y + x,
  283. 2 2
  284. x + u*y ,
  285. 2 2
  286. v*x*y + x - u *y ,
  287. 3 5 2 3 3 5 2 2 2
  288. u *x + (u *v + u *v )*y - (u - u *v )*y ,
  289. 7 2 4 4 4 4 3 3 4 2 2
  290. (u *v + u *v )*y + (2*u *v )*y + (u *v )*y }},
  291. 4 3
  292. {u <> 0 and v <> 0 and u *v + u*v = 0,
  293. 2
  294. {u*x + v*x*y + x,
  295. 2 2
  296. x + u*y ,
  297. 2 2
  298. v*x*y + x - u *y ,
  299. 3 5 2 3 3 5 2 2 2
  300. u *x + (u *v + u *v )*y - (u - u *v )*y ,
  301. 7 2 4 4 4 4 3 3 4 2 2
  302. (u *v + u *v )*y + (2*u *v )*y + (u *v )*y }},
  303. {u <> 0 and v = 0,
  304. 2 3 3 5 4 2 2
  305. {(u*v)*x *y + (u *v)*x*y - u *y - u *y ,
  306. 2
  307. u*x + v*x*y + x,
  308. 2 2
  309. x + u*y ,
  310. 2 2
  311. v*x*y + x - u *y }},
  312. {v <> 0 and u = 0,
  313. 2 2 2
  314. {u*x + v*x*y + x,x + u*y }},
  315. {u = 0 and v = 0,
  316. 2 2 2
  317. {u*x + v*x*y + x,x + u*y }}}
  318. torder oo;
  319. {{x,y},lex}
  320. % Weispfenning's Example 7.3
  321. oo := torder({x1,x2,x3,x4},lex);
  322. oo := {{},lex}
  323. gsys {x4 - (a4-a2),x1 + x2 + x3 + x4 + (a1 + a3 + a4),
  324. x1*x3 + x1*x4 + x2*x3 + x3*x4 - (a1*a4 + a1*a3 + a3*a4),x1*x3*x4 - a1*a3*a4};
  325. 2 2 3 2 2
  326. {{a1*a2 - a1*a2*a3 - 3*a1*a2*a4 + 2*a1*a4 - a2 + a2 *a3 + 4*a2 *a4
  327. 2 2 3
  328. - 3*a2*a3*a4 - 5*a2*a4 + 2*a3*a4 + 2*a4 <> 0 and a2 - a4 = 0,
  329. 2
  330. {(a2 - a4)*x2*x3 - (a2 - a4)*x2*x4 + (a1*a2 - a1*a2*a3 - 3*a1*a2*a4
  331. 2 3 2 2 2 2
  332. + 2*a1*a4 - a2 + a2 *a3 + 4*a2 *a4 - 3*a2*a3*a4 - 5*a2*a4 + 2*a3*a4
  333. 3
  334. + 2*a4 )}},
  335. {a2 - a4 <> 0,
  336. {x1*x3*x4 - a1*a3*a4,
  337. x1*x3 + x1*x4 + x2*x3 + x3*x4 - (a1*a3 + a1*a4 + a3*a4),
  338. x1 + x2 + x3 + x4 + (a1 + a3 + a4),
  339. 2
  340. (a2 - a4)*x2 - x3 - (a1 - a2 + a3 + 2*a4)*x3
  341. 2 2
  342. + (a1*a2 - a1*a3 - 2*a1*a4 - a2 + a2*a3 + 3*a2*a4 - 2*a3*a4 - 2*a4 ),
  343. 3 2
  344. x3 + (a1 + a3 + a4)*x3 + (a1*a3 + a1*a4 + a3*a4)*x3 - a1*a3*a4,
  345. x4 + (a2 - a4)}},
  346. 2 2 3 2 2
  347. {a1*a2 - a1*a2*a3 - 3*a1*a2*a4 + 2*a1*a4 - a2 + a2 *a3 + 4*a2 *a4
  348. 2 2 3
  349. - 3*a2*a3*a4 - 5*a2*a4 + 2*a3*a4 + 2*a4 = 0 and a2 - a4 = 0,
  350. {x1*x3*x4 - a1*a3*a4,
  351. x1*x3 + x1*x4 + x2*x3 + x3*x4 - (a1*a3 + a1*a4 + a3*a4),
  352. x1 + x2 + x3 + x4 + (a1 + a3 + a4),
  353. 2
  354. (a2 - a4)*x2 - x3 - (a1 - a2 + a3 + 2*a4)*x3
  355. 2 2
  356. + (a1*a2 - a1*a3 - 2*a1*a4 - a2 + a2*a3 + 3*a2*a4 - 2*a3*a4 - 2*a4 ),
  357. x4 + (a2 - a4)}}}
  358. torder oo;
  359. {{x1,x2,x3,x4},lex}
  360. % Pesch's example (Circle through three points)
  361. oo := torder({y,x},revgradlex);
  362. oo := {{},lex}
  363. gsys({2*b2*y + 2*a2*x - b2**2 + a2**2,2*b1*y + 2*a1*x - b1**2 + a1**2});
  364. 2 2 2 2
  365. {{a1 *a2 - a1*a2 + a1*b2 - a2*b1 <> 0 and a1 <> 0 and a2 <> 0 and b1 = 0
  366. and b2 = 0,
  367. 2 2 2 2
  368. {(2*a1*b2 - 2*a2*b1)*y - (a1 *a2 - a1*a2 + a1*b2 - a2*b1 )}},
  369. 2 2 2 2
  370. {a1 *b2 - a2 *b1 - b1 *b2 + b1*b2 <> 0 and b1 <> 0 and b2 <> 0
  371. and a1*b2 - a2*b1 = 0,
  372. 2 2 2 2
  373. {(2*a1*b2 - 2*a2*b1)*x + (a1 *b2 - a2 *b1 - b1 *b2 + b1*b2 )}},
  374. 2 2
  375. {a1 - b1 <> 0 and a1 = 0 and b1 = 0,
  376. 2 2
  377. {(2*b1)*y + (2*a1)*x + (a1 - b1 )}},
  378. {a1*b2 - a2*b1 <> 0 and b1 <> 0 and b2 <> 0,
  379. 2 2
  380. {(2*b1)*y + (2*a1)*x + (a1 - b1 ),
  381. 2 2
  382. (2*b2)*y + (2*a2)*x + (a2 - b2 ),
  383. 2 2 2 2
  384. (2*a1*b2 - 2*a2*b1)*x + (a1 *b2 - a2 *b1 - b1 *b2 + b1*b2 )}},
  385. 2 2
  386. {a1 <> 0 and a2 - b2 <> 0 and a2 = 0 and b1 = 0 and b2 = 0,
  387. 2 2
  388. {(2*b2)*y + (2*a2)*x + (a2 - b2 )}},
  389. 2 2 2 2
  390. {a1 <> 0 and a2 <> 0 and a1 *a2 - a1*a2 + a1*b2 - a2*b1 = 0 and b1 = 0
  391. and b2 = 0,
  392. 2 2
  393. {(2*b1)*y + (2*a1)*x + (a1 - b1 ),
  394. 2 2
  395. (2*b2)*y + (2*a2)*x + (a2 - b2 )}},
  396. {a1 <> 0 and b2 <> 0 and b1 = 0,
  397. 2 2
  398. {(2*b1)*y + (2*a1)*x + (a1 - b1 ),
  399. 2 2
  400. (2*b2)*y + (2*a2)*x + (a2 - b2 )}},
  401. 2 2
  402. {a1 <> 0 and a2 - b2 = 0 and a2 = 0 and b1 = 0 and b2 = 0,
  403. 2 2
  404. {(2*b1)*y + (2*a1)*x + (a1 - b1 )}},
  405. 2 2
  406. {a2 - b2 <> 0 and b1 <> 0 and a2 = 0 and b2 = 0,
  407. 2 2
  408. {(2*b2)*y + (2*a2)*x + (a2 - b2 )}},
  409. 2 2 2 2
  410. {a2 - b2 <> 0 and a1 - b1 = 0 and a1 = 0 and a2 = 0 and b1 = 0 and b2 = 0,
  411. 2 2
  412. {(2*b2)*y + (2*a2)*x + (a2 - b2 )}},
  413. {a2 <> 0 and b1 <> 0 and b2 = 0,
  414. 2 2
  415. {(2*b1)*y + (2*a1)*x + (a1 - b1 ),
  416. 2 2
  417. (2*b2)*y + (2*a2)*x + (a2 - b2 )}},
  418. 2 2
  419. {a2 <> 0 and a1 - b1 = 0 and a1 = 0 and b1 = 0 and b2 = 0,
  420. 2 2
  421. {(2*b2)*y + (2*a2)*x + (a2 - b2 )}},
  422. 2 2 2 2
  423. {b1 <> 0 and b2 <> 0 and a1 *b2 - a2 *b1 - b1 *b2 + b1*b2 = 0
  424. and a1*b2 - a2*b1 = 0,
  425. 2 2
  426. {(2*b1)*y + (2*a1)*x + (a1 - b1 ),
  427. 2 2
  428. (2*b2)*y + (2*a2)*x + (a2 - b2 )}},
  429. 2 2
  430. {b1 <> 0 and a2 - b2 = 0 and a2 = 0 and b2 = 0,
  431. 2 2
  432. {(2*b1)*y + (2*a1)*x + (a1 - b1 )}},
  433. 2 2
  434. {b2 <> 0 and a1 - b1 = 0 and a1 = 0 and b1 = 0,
  435. 2 2
  436. {(2*b2)*y + (2*a2)*x + (a2 - b2 )}},
  437. 2 2 2 2
  438. {a1 - b1 = 0 and a1 = 0 and a2 - b2 = 0 and a2 = 0 and b1 = 0 and b2 = 0,
  439. {}}}
  440. torder oo;
  441. {{y,x},revgradlex}
  442. % Effelterre's example (Aspect graphs)
  443. f1 := -4-4*v**2-4*u**2+40*v*v1+24*v-120*v1+8*u-40*v2-68*v1**2-100*v2**2+40*u*v2+
  444. 24*v1*v2-4*v1**2*u-4*v2**2*v**2+24*v2**2*v-24*v1*u*v2+8*v*v1*u*v2$
  445. f2 := 8*v*v1*u*v2-4*v1**2*u**2+4*v1**2-4*v2**2*v**2+4*v2**2-16*v**2-16*u**2+16$
  446. f3 := 16*v-48*u+16*v*v1**2-48*u*v2**2-12*v1**2*u+4*v2**2*v-36*v*v1*v2+
  447. 12*v1*u*v2+12*v*v2**2*u-
  448. 80*u*v1+80*v2*v-20*v1*u*v2**2+20*v2*v*v1**2-20*v1**3*u+20*v2**3*v-12*v1**2*v*u+
  449. 12*v2*v**2*v1-12*v1*u**2*v2$
  450. f4 := -160u*v2-1596v2**2+3200*v2-1596-4*u**2+160*u$
  451. % Special case I2, v1=0
  452. oo := torder({v,u},lex);
  453. oo := {{},lex}
  454. gsys(sub(v1=0,{f1,f2,f4}));
  455. 16 15 14
  456. {{1000557799569*v2 - 8971728968760*v2 + 32332553961916*v2
  457. 13 12 11
  458. - 56816638983720*v2 + 43557281160966*v2 - 2232864400680*v2
  459. 10 9 8
  460. - 2141149653636*v2 - 24710286679320*v2 + 22557177598385*v2
  461. 7 6 5
  462. - 4364899181280*v2 + 1970637124608*v2 - 2915313822720*v2
  463. 4 3 2
  464. + 1467702460416*v2 - 1340557025280*v2 + 685570158592*v2 - 140796887040*v2
  465. 7 6 5 4
  466. + 63647907840 <> 0 and 55175*v2 - 184787*v2 + 144885*v2 + 44895*v2
  467. 3 2
  468. - 13020*v2 - 35580*v2 + 320*v2 - 6368 <> 0,
  469. 16 15 14
  470. {1000557799569*v2 - 8971728968760*v2 + 32332553961916*v2
  471. 13 12 11
  472. - 56816638983720*v2 + 43557281160966*v2 - 2232864400680*v2
  473. 10 9 8
  474. - 2141149653636*v2 - 24710286679320*v2 + 22557177598385*v2
  475. 7 6 5
  476. - 4364899181280*v2 + 1970637124608*v2 - 2915313822720*v2
  477. 4 3 2
  478. + 1467702460416*v2 - 1340557025280*v2 + 685570158592*v2 - 140796887040*v2
  479. + 63647907840}},
  480. 8 7 6 5 4
  481. {3389663*v2 - 14658420*v2 + 20230730*v2 - 6945060*v2 - 3218385*v2
  482. 3 2 7
  483. - 497040*v2 + 1656704*v2 - 257280*v2 + 255872 <> 0 and 55175*v2
  484. 6 5 4 3 2
  485. - 184787*v2 + 144885*v2 + 44895*v2 - 13020*v2 - 35580*v2 + 320*v2 - 6368
  486. = 0,
  487. 7 6 5 4 3 2
  488. {(220700*v2 - 739148*v2 + 579540*v2 + 179580*v2 - 52080*v2 - 142320*v2
  489. 8 7 6
  490. + 1280*v2 - 25472)*u + (3389663*v2 - 14658420*v2 + 20230730*v2
  491. 5 4 3 2
  492. - 6945060*v2 - 3218385*v2 - 497040*v2 + 1656704*v2 - 257280*v2
  493. + 255872)}},
  494. 7 6 5 4 3 2
  495. {55175*v2 - 184787*v2 + 144885*v2 + 44895*v2 - 13020*v2 - 35580*v2
  496. 16 15
  497. + 320*v2 - 6368 <> 0 and 1000557799569*v2 - 8971728968760*v2
  498. 14 13 12
  499. + 32332553961916*v2 - 56816638983720*v2 + 43557281160966*v2
  500. 11 10 9
  501. - 2232864400680*v2 - 2141149653636*v2 - 24710286679320*v2
  502. 8 7 6
  503. + 22557177598385*v2 - 4364899181280*v2 + 1970637124608*v2
  504. 5 4 3
  505. - 2915313822720*v2 + 1467702460416*v2 - 1340557025280*v2
  506. 2
  507. + 685570158592*v2 - 140796887040*v2 + 63647907840 = 0,
  508. 2 2 2 2 2
  509. {(v2 + 1)*v - (6*v2 + 6)*v + u - (10*v2 + 2)*u + (25*v2 + 10*v2 + 1),
  510. 2 2 2 2
  511. (v2 + 4)*v + 4*u - (v2 + 4),
  512. 4 2 3 2
  513. (6*v2 + 30*v2 + 24)*v - (110*v2 - 122*v2 - 40*v2 - 8)*u
  514. 4 3 2
  515. - (1223*v2 - 2390*v2 + 1303*v2 + 40*v2 + 8),
  516. 2 2
  517. u + (40*v2 - 40)*u + (399*v2 - 800*v2 + 399),
  518. 7 6 5 4 3 2
  519. (220700*v2 - 739148*v2 + 579540*v2 + 179580*v2 - 52080*v2 - 142320*v2
  520. 8 7 6
  521. + 1280*v2 - 25472)*u + (3389663*v2 - 14658420*v2 + 20230730*v2
  522. 5 4 3 2
  523. - 6945060*v2 - 3218385*v2 - 497040*v2 + 1656704*v2 - 257280*v2
  524. + 255872)}},
  525. 8 7 6 5 4
  526. {3389663*v2 - 14658420*v2 + 20230730*v2 - 6945060*v2 - 3218385*v2
  527. 3 2 7
  528. - 497040*v2 + 1656704*v2 - 257280*v2 + 255872 = 0 and 55175*v2
  529. 6 5 4 3 2
  530. - 184787*v2 + 144885*v2 + 44895*v2 - 13020*v2 - 35580*v2 + 320*v2 - 6368
  531. = 0,
  532. 2 2 2 2 2
  533. {(v2 + 1)*v - (6*v2 + 6)*v + u - (10*v2 + 2)*u + (25*v2 + 10*v2 + 1),
  534. 2 2 2 2
  535. (v2 + 4)*v + 4*u - (v2 + 4),
  536. 4 2 3 2
  537. (6*v2 + 30*v2 + 24)*v - (110*v2 - 122*v2 - 40*v2 - 8)*u
  538. 4 3 2
  539. - (1223*v2 - 2390*v2 + 1303*v2 + 40*v2 + 8),
  540. 2 2
  541. u + (40*v2 - 40)*u + (399*v2 - 800*v2 + 399)}}}
  542. torder oo;
  543. {{v,u},lex}
  544. clear f1,f2,f3,f4;
  545. % Sit's Example 2.2
  546. oo := torder({z2,z2},revgradlex);
  547. oo := {{},lex}
  548. gsys({d*z2 + c*z1 - v,b*z2 + a*z1 - u});
  549. {{a*d*z1 - b*c*z1 + b*v - d*u <> 0 and b <> 0 and d <> 0,
  550. {a*d*z1 - b*c*z1 + b*v - d*u}},
  551. {a*z1 - u <> 0 and b = 0,
  552. {b*z2 + (a*z1 - u)}},
  553. {b <> 0 and c*z1 - v <> 0 and d = 0,
  554. {d*z2 + (c*z1 - v)}},
  555. {b <> 0 and d <> 0 and a*d*z1 - b*c*z1 + b*v - d*u = 0,
  556. {b*z2 + (a*z1 - u),d*z2 + (c*z1 - v)}},
  557. {b <> 0 and c*z1 - v = 0 and d = 0,
  558. {b*z2 + (a*z1 - u)}},
  559. {c*z1 - v <> 0 and a*z1 - u = 0 and b = 0 and d = 0,
  560. {d*z2 + (c*z1 - v)}},
  561. {d <> 0 and a*z1 - u = 0 and b = 0,
  562. {d*z2 + (c*z1 - v)}},
  563. {a*z1 - u = 0 and b = 0 and c*z1 - v = 0 and d = 0,
  564. {}}}
  565. torder oo;
  566. {{z2,z2},revgradlex}
  567. % Sit's Example 2.3
  568. oo := torder({z2,z2},revgradlex);
  569. oo := {{},lex}
  570. gsys({x**3*z2 + (x**2+1)*z1,x**2*z2 + x*z1 - 1});
  571. 2
  572. {{x *z1 + z1 <> 0 and x = 0,
  573. 3 2
  574. {x *z2 + (x *z1 + z1)}},
  575. 2
  576. {x*z1 - 1 <> 0 and x *z1 + z1 = 0 and x = 0,
  577. 2
  578. {x *z2 + (x*z1 - 1)}},
  579. {x + z1 <> 0 and x <> 0,{x + z1}},
  580. {x <> 0 and x + z1 = 0,
  581. 3 2 2
  582. {x *z2 + (x *z1 + z1),x *z2 + (x*z1 - 1)}},
  583. 2
  584. {x *z1 + z1 = 0 and x*z1 - 1 = 0 and x = 0,{}}}
  585. torder oo;
  586. {{z2,z2},revgradlex}
  587. % Sit's Example 3.3
  588. oo := torder({z3,z2,z2},revgradlex);
  589. oo := {{},lex}
  590. gsys({z3 + b*z2 + a*z1 - 1,a*z3 + z2 + b*z1 - 1,b*z3 + a*z2 + z1 - 1});
  591. 3 2
  592. {{a *z1 - a - 2*a*b*z1 + a*b + a + z1 - 1 <> 0 and a <> 0 and b = 0,
  593. 2 3 2
  594. {(a*b - b)*z3 - (a *z1 - a - 2*a*b*z1 + a*b + a + z1 - 1)}},
  595. 3 2 3 2 2
  596. {a *z1 - a - 3*a*b*z1 + a*b + a + b *z1 - b + b + z1 - 1 <> 0 and a - b <> 0
  597. and a <> 0 and b <> 0,
  598. 3 2 3 2
  599. {a *z1 - a - 3*a*b*z1 + a*b + a + b *z1 - b + b + z1 - 1}},
  600. 2
  601. {a *z1 - a - b*z1 + 1 <> 0 and a <> 0 and b <> 0 and a*b*z1 - b - z1 + 1 = 0
  602. 2
  603. and a*b - 1 = 0 and a - b = 0,
  604. 2
  605. {(a*b - 1)*z2 + (a *z1 - a - b*z1 + 1)}},
  606. 3 2
  607. {2*a*b*z1 - a - b *z1 + b - b - z1 + 1 <> 0 and b <> 0 and a = 0,
  608. 2 2 3 2
  609. {(a - a*b )*z3 + (2*a*b*z1 - a - b *z1 + b - b - z1 + 1)}},
  610. 2
  611. {a*b*z1 - b - z1 + 1 <> 0 and a <> 0 and b <> 0 and a - b = 0,
  612. 2
  613. {(a - b )*z2 - (a*b*z1 - b - z1 + 1)}},
  614. 2
  615. {a*b - 1 <> 0 and a <> 0 and b <> 0 and a*b*z1 - b - z1 + 1 = 0 and a - b = 0,
  616. {z3 + b*z2 + (a*z1 - 1),
  617. b*z3 + a*z2 + (z1 - 1),
  618. a*z3 + z2 + (b*z1 - 1),
  619. 2
  620. (a*b - 1)*z2 + (a *z1 - a - b*z1 + 1)}},
  621. 2
  622. {a - b <> 0 and a <> 0 and b <> 0
  623. 3 2 3 2
  624. and a *z1 - a - 3*a*b*z1 + a*b + a + b *z1 - b + b + z1 - 1 = 0,
  625. {z3 + b*z2 + (a*z1 - 1),
  626. b*z3 + a*z2 + (z1 - 1),
  627. a*z3 + z2 + (b*z1 - 1),
  628. 2
  629. (a - b )*z2 - (a*b*z1 - b - z1 + 1)}},
  630. 2
  631. {a <> 0 and b <> 0 and a *z1 - a - b*z1 + 1 = 0 and a*b*z1 - b - z1 + 1 = 0
  632. 2
  633. and a*b - 1 = 0 and a - b = 0,
  634. {z3 + b*z2 + (a*z1 - 1),
  635. b*z3 + a*z2 + (z1 - 1),
  636. a*z3 + z2 + (b*z1 - 1)}},
  637. 3 2
  638. {a <> 0 and a *z1 - a - 2*a*b*z1 + a*b + a + z1 - 1 = 0 and b = 0,
  639. {z3 + b*z2 + (a*z1 - 1),
  640. b*z3 + a*z2 + (z1 - 1),
  641. a*z3 + z2 + (b*z1 - 1)}},
  642. 3 2
  643. {b <> 0 and 2*a*b*z1 - a - b *z1 + b - b - z1 + 1 = 0 and a = 0,
  644. {z3 + b*z2 + (a*z1 - 1),
  645. b*z3 + a*z2 + (z1 - 1),
  646. a*z3 + z2 + (b*z1 - 1)}},
  647. {z1 - 1 <> 0 and a = 0 and b = 0,
  648. {b*z3 + a*z2 + (z1 - 1)}},
  649. {a = 0 and b = 0 and z1 - 1 = 0,
  650. {z3 + b*z2 + (a*z1 - 1),a*z3 + z2 + (b*z1 - 1)}}}
  651. torder oo;
  652. {{z3,z2,z2},revgradlex}
  653. % Sit's Example 8.3
  654. oo := torder({z4,z3,z2,z2},revgradlex);
  655. oo := {{},lex}
  656. gsys({z4 + c*z3 + b*z2 + a*z1 - w2,2*z4 + z2 - w1,a*z4 - z3 - w4,d*z4 + z3 +
  657. 2*z1 - w3,z4 + z1 - w5});
  658. 3 2 2 2 2 2 2 2 2
  659. {{a *c*z1 + a *b*c*w1 + a *c *w3 - 2*a *c *z1 + a *c*d*z1 - a *c*w2 + a *z1
  660. 2
  661. + a*b*c*d*w1 - 2*a*b*c*w3 - 2*a*b*c*w4 + 4*a*b*c*z1 + a*b*w1 - a*c *d*w4
  662. - a*c*d*w2 + 2*a*c*w3 + a*c*w4 - 4*a*c*z1 + a*d*z1 - a*w2 + b*d*w1 - 2*b*w3
  663. - 2*b*w4 + 4*b*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 <> 0 and a*b + b*d <> 0
  664. and a*c + 1 <> 0 and a <> 0 and d <> 0,
  665. 3 2 2 2 2 2 2 2 2
  666. {a *c*z1 + a *b*c*w1 + a *c *w3 - 2*a *c *z1 + a *c*d*z1 - a *c*w2 + a *z1
  667. 2
  668. + a*b*c*d*w1 - 2*a*b*c*w3 - 2*a*b*c*w4 + 4*a*b*c*z1 + a*b*w1 - a*c *d*w4
  669. - a*c*d*w2 + 2*a*c*w3 + a*c*w4 - 4*a*c*z1 + a*d*z1 - a*w2 + b*d*w1 - 2*b*w3
  670. - 2*b*w4 + 4*b*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1}},
  671. 3 2 2 2 2
  672. {a *c*z1 + a *b*c*w1 - a *c*w2 - a *c*w5 + a *c*z1 - 2*a*b*c*w4 + 2*a*b*w5
  673. - 2*a*b*z1 + 2*a*c*w4 - a*w5 + a*z1 - 2*b*w4 + w4 <> 0 and a*b <> 0
  674. and a*c - 2*b + 1 <> 0 and a <> 0 and d <> 0 and a*c + 1 = 0
  675. and a*w3 - 2*a*z1 - d*w4 = 0 and a + d = 0,
  676. 2 2 3 2 2
  677. {(a *c - 2*a*b*c + 2*a*c - 2*b + 1)*z3 + (a *c*z1 + a *b*c*w1 - a *c*w2
  678. 2 2
  679. - a *c*w5 + a *c*z1 - 2*a*b*c*w4 + 2*a*b*w5 - 2*a*b*z1 + 2*a*c*w4 - a*w5
  680. + a*z1 - 2*b*w4 + w4)}},
  681. 3 2 2 2 2 2
  682. {a *z1 + 2*a *b*c*w3 - 4*a *b*c*z1 + a *b*w1 + a *d*z1 - a *w2 - 2*a*b*c*d*w4
  683. + a*b*d*w1 - 2*a*b*w4 - a*d*w2 + a*w4 - 2*b*d*w4 + d*w4 <> 0 and a*b <> 0
  684. and a + d <> 0 and a <> 0 and d <> 0 and a*c + 1 = 0,
  685. 2 2 3
  686. {(2*a *b*c - a *c + 2*a*b*c*d + 2*a*b - a*c*d - a + 2*b*d - d)*z3 - (a *z1
  687. 2 2 2 2 2
  688. + 2*a *b*c*w3 - 4*a *b*c*z1 + a *b*w1 + a *d*z1 - a *w2 - 2*a*b*c*d*w4
  689. + a*b*d*w1 - 2*a*b*w4 - a*d*w2 + a*w4 - 2*b*d*w4 + d*w4)}},
  690. 2 2 2 2 2 2
  691. {a *c *w5 - a *c *z1 + a *c*z1 + a*b*c*w1 - 2*a*b*c*w5 + 2*a*b*c*z1 - a*c *w4
  692. - a*c*w2 + 2*a*c*w5 - 2*a*c*z1 + a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - c*w4 - w2
  693. + w5 - z1 <> 0 and a*c - 2*b + 1 <> 0 and a*c + 1 <> 0 and a <> 0 and d <> 0
  694. 2
  695. and a *z1 + a*c*w3 - 2*a*c*z1 + a*d*z1 - a*w2 - c*d*w4 - d*w2 + w3 + w4 - 2*z1
  696. = 0 and a*b + b*d = 0,
  697. 2 2 2 2 2 2
  698. {a *c *w5 - a *c *z1 + a *c*z1 + a*b*c*w1 - 2*a*b*c*w5 + 2*a*b*c*z1 - a*c *w4
  699. - a*c*w2 + 2*a*c*w5 - 2*a*c*z1 + a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - c*w4 - w2
  700. + w5 - z1}},
  701. 2 2 2 2
  702. {a *c*w3 - 2*a *c*z1 + a *w5 - a *z1 - a*c*d*w4 + a*d*w5 - a*d*z1 - a*w4 - d*w4
  703. 3
  704. <> 0 and a*b <> 0 and a + d <> 0 and a <> 0 and d <> 0 and a *z1
  705. 2 2 2 2 2
  706. + 2*a *b*c*w3 - 4*a *b*c*z1 + a *b*w1 + a *d*z1 - a *w2 - 2*a*b*c*d*w4
  707. + a*b*d*w1 - 2*a*b*w4 - a*d*w2 + a*w4 - 2*b*d*w4 + d*w4 = 0 and a*c + 1 = 0,
  708. 2 2 2 2 2
  709. {(a *c + a*c*d + a + d)*z3 - (a *c*w3 - 2*a *c*z1 + a *w5 - a *z1 - a*c*d*w4
  710. + a*d*w5 - a*d*z1 - a*w4 - d*w4)}},
  711. 2 2
  712. {a *c*w5 - a *c*z1 + a*c*d*w5 - a*c*d*z1 - a*c*w3 - a*c*w4 + 2*a*c*z1 + a*w5
  713. - a*z1 + d*w5 - d*z1 - w3 - w4 + 2*z1 <> 0 and a*b + b*d <> 0
  714. 3 2 2 2
  715. and a*c + 1 <> 0 and a <> 0 and d <> 0 and a *c*z1 + a *b*c*w1 + a *c *w3
  716. 2 2 2 2 2
  717. - 2*a *c *z1 + a *c*d*z1 - a *c*w2 + a *z1 + a*b*c*d*w1 - 2*a*b*c*w3
  718. 2
  719. - 2*a*b*c*w4 + 4*a*b*c*z1 + a*b*w1 - a*c *d*w4 - a*c*d*w2 + 2*a*c*w3 + a*c*w4
  720. - 4*a*c*z1 + a*d*z1 - a*w2 + b*d*w1 - 2*b*w3 - 2*b*w4 + 4*b*z1 - c*d*w4
  721. - d*w2 + w3 + w4 - 2*z1 = 0,
  722. 2 2
  723. {a *c*w5 - a *c*z1 + a*c*d*w5 - a*c*d*z1 - a*c*w3 - a*c*w4 + 2*a*c*z1 + a*w5
  724. - a*z1 + d*w5 - d*z1 - w3 - w4 + 2*z1}},
  725. 2
  726. {a *z1 + a*b*w1 + a*c*w3 - 2*a*c*z1 - a*w2 - 2*b*w3 - 2*b*w4 + 4*b*z1 + w3 + w4
  727. - 2*z1 <> 0 and a*b <> 0 and a <> 0 and d = 0,
  728. 2
  729. {(a*c*d - 2*b*d + d)*z4 - (a *z1 + a*b*w1 + a*c*w3 - 2*a*c*z1 - a*w2 - 2*b*w3
  730. - 2*b*w4 + 4*b*z1 + w3 + w4 - 2*z1)}},
  731. 2
  732. {a *z1 + a*b*w1 - a*w2 - 2*b*w4 + w4 <> 0 and a*b <> 0 and a <> 0 and d <> 0
  733. and a*c - 2*b + 1 = 0 and a*c + 1 = 0 and a*w3 - 2*a*z1 - d*w4 = 0
  734. and a + d = 0,
  735. 2
  736. {(a*c - 2*b + 1)*z3 + (a *z1 + a*b*w1 - a*w2 - 2*b*w4 + w4)}},
  737. 2
  738. {a *z1 + a*c*w3 - 2*a*c*z1 + a*d*z1 - a*w2 - c*d*w4 - d*w2 + w3 + w4 - 2*z1
  739. <> 0 and a*c + 1 <> 0 and a <> 0 and d <> 0 and a*b + b*d = 0,
  740. 2
  741. {(a*b + b*d)*z2 + (a *z1 + a*c*w3 - 2*a*c*z1 + a*d*z1 - a*w2 - c*d*w4 - d*w2
  742. + w3 + w4 - 2*z1)}},
  743. 2
  744. {a *z1 + a*c*w3 - 2*a*c*z1 - a*w2 + w3 + w4 - 2*z1 <> 0 and a <> 0 and a*b = 0
  745. and d = 0,
  746. {(a*c*d + d)*z4 - (a*b)*z2
  747. 2
  748. - (a *z1 + a*c*w3 - 2*a*c*z1 - a*w2 + w3 + w4 - 2*z1)}},
  749. 2
  750. {a *z1 - a*w2 + w4 <> 0 and a <> 0 and d <> 0 and a*b = 0 and a*c + 1 = 0,
  751. 2
  752. {(a*c + 1)*z3 + (a*b)*z2 + (a *z1 - a*w2 + w4)}},
  753. 3 2
  754. {a*b + b*d <> 0 and a*c + 1 <> 0 and a <> 0 and d <> 0 and a *c*z1 + a *b*c*w1
  755. 2 2 2 2 2 2 2
  756. + a *c *w3 - 2*a *c *z1 + a *c*d*z1 - a *c*w2 + a *z1 + a*b*c*d*w1
  757. 2
  758. - 2*a*b*c*w3 - 2*a*b*c*w4 + 4*a*b*c*z1 + a*b*w1 - a*c *d*w4 - a*c*d*w2
  759. + 2*a*c*w3 + a*c*w4 - 4*a*c*z1 + a*d*z1 - a*w2 + b*d*w1 - 2*b*w3 - 2*b*w4
  760. 2 2
  761. + 4*b*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 = 0 and a *c*w5 - a *c*z1
  762. + a*c*d*w5 - a*c*d*z1 - a*c*w3 - a*c*w4 + 2*a*c*z1 + a*w5 - a*z1 + d*w5
  763. - d*z1 - w3 - w4 + 2*z1 = 0,
  764. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  765. a*z4 - z3 - w4,
  766. d*z4 + z3 - (w3 - 2*z1),
  767. 2*z4 + z2 - w1,
  768. z4 - (w5 - z1),
  769. 2
  770. (a*c + 1)*z3 + (a*b)*z2 + (a *z1 - a*w2 + w4),
  771. 2
  772. (a*b + b*d)*z2 + (a *z1 + a*c*w3 - 2*a*c*z1 + a*d*z1 - a*w2 - c*d*w4 - d*w2
  773. + w3 + w4 - 2*z1)}},
  774. 3 2
  775. {a*b <> 0 and a*c - 2*b + 1 <> 0 and a <> 0 and d <> 0 and a *c*z1 + a *b*c*w1
  776. 2 2 2
  777. - a *c*w2 - a *c*w5 + a *c*z1 - 2*a*b*c*w4 + 2*a*b*w5 - 2*a*b*z1 + 2*a*c*w4
  778. - a*w5 + a*z1 - 2*b*w4 + w4 = 0 and a*c + 1 = 0 and a*w3 - 2*a*z1 - d*w4 = 0
  779. and a + d = 0,
  780. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  781. a*z4 - z3 - w4,
  782. d*z4 + z3 - (w3 - 2*z1),
  783. 2*z4 + z2 - w1,
  784. z4 - (w5 - z1),
  785. 2
  786. (a*c + 1)*z3 + (a*b)*z2 + (a *z1 - a*w2 + w4),
  787. 2
  788. (a*c - 2*b + 1)*z3 + (a *z1 + a*b*w1 - a*w2 - 2*b*w4 + w4)}},
  789. {a*b <> 0 and a*w3 - 2*a*z1 - d*w4 <> 0 and a <> 0 and d <> 0 and a*c + 1 = 0
  790. and a + d = 0,
  791. {(a + d)*z3 - (a*w3 - 2*a*z1 - d*w4)}},
  792. 2
  793. {a*b <> 0 and a*w5 - a*z1 - w3 - w4 + 2*z1 <> 0 and a <> 0 and a *z1 + a*b*w1
  794. + a*c*w3 - 2*a*c*z1 - a*w2 - 2*b*w3 - 2*b*w4 + 4*b*z1 + w3 + w4 - 2*z1 = 0
  795. and d = 0,
  796. {d*z4 + (a*w5 - a*z1 - w3 - w4 + 2*z1)}},
  797. 3 2
  798. {a*b <> 0 and a + d <> 0 and a <> 0 and d <> 0 and a *z1 + 2*a *b*c*w3
  799. 2 2 2 2
  800. - 4*a *b*c*z1 + a *b*w1 + a *d*z1 - a *w2 - 2*a*b*c*d*w4 + a*b*d*w1
  801. - 2*a*b*w4 - a*d*w2 + a*w4 - 2*b*d*w4 + d*w4 = 0 and
  802. 2 2 2 2
  803. a *c*w3 - 2*a *c*z1 + a *w5 - a *z1 - a*c*d*w4 + a*d*w5 - a*d*z1 - a*w4 - d*w4
  804. = 0 and a*c + 1 = 0,
  805. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  806. a*z4 - z3 - w4,
  807. d*z4 + z3 - (w3 - 2*z1),
  808. 2*z4 + z2 - w1,
  809. z4 - (w5 - z1),
  810. 2
  811. (a*c + 1)*z3 + (a*b)*z2 + (a *z1 - a*w2 + w4),
  812. (a + d)*z3 - (a*w3 - 2*a*z1 - d*w4)}},
  813. 2
  814. {a*b <> 0 and a <> 0 and d <> 0 and a *z1 + a*b*w1 - a*w2 - 2*b*w4 + w4 = 0
  815. and a*c - 2*b + 1 = 0 and a*c + 1 = 0 and a*w3 - 2*a*z1 - d*w4 = 0
  816. and a + d = 0,
  817. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  818. a*z4 - z3 - w4,
  819. d*z4 + z3 - (w3 - 2*z1),
  820. 2*z4 + z2 - w1,
  821. z4 - (w5 - z1),
  822. 2
  823. (a*c + 1)*z3 + (a*b)*z2 + (a *z1 - a*w2 + w4),
  824. z3 - (a*w5 - a*z1 - w4)}},
  825. 2
  826. {a*b <> 0 and a <> 0 and a *z1 + a*b*w1 + a*c*w3 - 2*a*c*z1 - a*w2 - 2*b*w3
  827. - 2*b*w4 + 4*b*z1 + w3 + w4 - 2*z1 = 0 and a*w5 - a*z1 - w3 - w4 + 2*z1 = 0
  828. and d = 0,
  829. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  830. a*z4 - z3 - w4,
  831. d*z4 + z3 - (w3 - 2*z1),
  832. 2*z4 + z2 - w1,
  833. (a*c*d + d)*z4 - (a*b)*z2
  834. 2
  835. - (a *z1 + a*c*w3 - 2*a*c*z1 - a*w2 + w3 + w4 - 2*z1),
  836. z4 - (w5 - z1)}},
  837. 2 2
  838. {a*c*d *z1 + b*c*d *w1 - 2*b*c*d*w3 + 4*b*c*d*z1 - 2*b*d*w5 + 2*b*d*z1 + 2*b*w3
  839. 2 2 2
  840. - 4*b*z1 - c*d *w2 - c*d *w5 + c*d *z1 + 2*c*d*w3 - 4*c*d*z1 + d*w5 - d*z1
  841. - w3 + 2*z1 <> 0 and a <> 0 and b*d <> 0 and 2*b + c*d - 1 <> 0 and d <> 0
  842. 2
  843. and a *z1 - a*w2 + w4 = 0 and a*b = 0 and a*c + 1 = 0 and c*d - 1 = 0,
  844. 2 2 2 2
  845. {(2*b*c*d - 2*b + c *d - 2*c*d + 1)*z3 + (a*c*d *z1 + b*c*d *w1 - 2*b*c*d*w3
  846. 2 2
  847. + 4*b*c*d*z1 - 2*b*d*w5 + 2*b*d*z1 + 2*b*w3 - 4*b*z1 - c*d *w2 - c*d *w5
  848. 2
  849. + c*d *z1 + 2*c*d*w3 - 4*c*d*z1 + d*w5 - d*z1 - w3 + 2*z1)}},
  850. {a*c*d*z1 - a*z1 + b*c*d*w1 - 2*b*c*d*w5 + 2*b*c*d*z1 - b*w1 + 2*b*w5 - 2*b*z1
  851. 2 2 2 2 2 2
  852. - c *d *w5 + c *d *z1 + c *d*w3 - 2*c *d*z1 - c*d*w2 + 2*c*d*w5 - 2*c*d*z1
  853. - c*w3 + 2*c*z1 + w2 - w5 + z1 <> 0 and a <> 0 and 2*b + c*d - 1 <> 0
  854. 2
  855. and c*d - 1 <> 0 and d <> 0 and a *z1 - a*w2 + w4 = 0 and a*b = 0
  856. and a*c + 1 = 0,
  857. {a*c*d*z1 - a*z1 + b*c*d*w1 - 2*b*c*d*w5 + 2*b*c*d*z1 - b*w1 + 2*b*w5 - 2*b*z1
  858. 2 2 2 2 2 2
  859. - c *d *w5 + c *d *z1 + c *d*w3 - 2*c *d*z1 - c*d*w2 + 2*c*d*w5 - 2*c*d*z1
  860. - c*w3 + 2*c*z1 + w2 - w5 + z1}},
  861. {a*c*w1 + 2*a*z1 - 2*c*w4 + w1 - 2*w2 <> 0 and a*c + 1 <> 0 and a <> 0
  862. and d <> 0 and
  863. 2
  864. a *z1 + a*c*w3 - 2*a*c*z1 + a*d*z1 - a*w2 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 = 0
  865. and a*b + b*d = 0 and a*c - 2*b + 1 = 0,
  866. {(a*c - 2*b + 1)*z2 - (a*c*w1 + 2*a*z1 - 2*c*w4 + w1 - 2*w2)}},
  867. {a*c*w5 - a*c*z1 + a*z1 - c*w4 - w2 + w5 - z1 <> 0 and a*c + 1 <> 0 and a <> 0
  868. and d <> 0 and
  869. 2
  870. a *z1 + a*c*w3 - 2*a*c*z1 + a*d*z1 - a*w2 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 = 0
  871. and a*b + b*d = 0 and a*c*w1 + 2*a*z1 - 2*c*w4 + w1 - 2*w2 = 0
  872. and a*c - 2*b + 1 = 0 and b = 0,
  873. {b*z2 + (a*c*w5 - a*c*z1 + a*z1 - c*w4 - w2 + w5 - z1)}},
  874. 2 2
  875. {a*c - 2*b + 1 <> 0 and a*c + 1 <> 0 and a <> 0 and d <> 0 and a *c *w5
  876. 2 2 2 2
  877. - a *c *z1 + a *c*z1 + a*b*c*w1 - 2*a*b*c*w5 + 2*a*b*c*z1 - a*c *w4 - a*c*w2
  878. + 2*a*c*w5 - 2*a*c*z1 + a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - c*w4 - w2 + w5 - z1
  879. = 0 and
  880. 2
  881. a *z1 + a*c*w3 - 2*a*c*z1 + a*d*z1 - a*w2 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 = 0
  882. and a*b + b*d = 0,
  883. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  884. a*z4 - z3 - w4,
  885. d*z4 + z3 - (w3 - 2*z1),
  886. 2*z4 + z2 - w1,
  887. z4 - (w5 - z1),
  888. 2
  889. (a*c + 1)*z3 + (a*b)*z2 + (a *z1 - a*w2 + w4),
  890. (a*c - 2*b + 1)*z2 - (a*c*w1 + 2*a*z1 - 2*c*w4 + w1 - 2*w2)}},
  891. {a*c + 1 <> 0 and a <> 0 and b <> 0 and d <> 0 and
  892. 2
  893. a *z1 + a*c*w3 - 2*a*c*z1 + a*d*z1 - a*w2 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 = 0
  894. and a*b + b*d = 0 and a*c*w1 + 2*a*z1 - 2*c*w4 + w1 - 2*w2 = 0
  895. and a*c - 2*b + 1 = 0,
  896. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  897. a*z4 - z3 - w4,
  898. d*z4 + z3 - (w3 - 2*z1),
  899. 2*z4 + z2 - w1,
  900. z4 - (w5 - z1),
  901. 2
  902. (a*c + 1)*z3 + (a*b)*z2 + (a *z1 - a*w2 + w4),
  903. b*z2 + (a*c*w5 - a*c*z1 + a*z1 - c*w4 - w2 + w5 - z1)}},
  904. {a*c + 1 <> 0 and a <> 0 and d <> 0 and
  905. 2
  906. a *z1 + a*c*w3 - 2*a*c*z1 + a*d*z1 - a*w2 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 = 0
  907. and a*b + b*d = 0 and a*c*w1 + 2*a*z1 - 2*c*w4 + w1 - 2*w2 = 0
  908. and a*c*w5 - a*c*z1 + a*z1 - c*w4 - w2 + w5 - z1 = 0 and a*c - 2*b + 1 = 0
  909. and b = 0,
  910. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  911. a*z4 - z3 - w4,
  912. d*z4 + z3 - (w3 - 2*z1),
  913. 2*z4 + z2 - w1,
  914. z4 - (w5 - z1),
  915. 2
  916. (a*c + 1)*z3 + (a*b)*z2 + (a *z1 - a*w2 + w4)}},
  917. {a*d*z1 + b*d*w1 - 2*b*w3 - 2*b*w4 + 4*b*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1
  918. <> 0 and b*d <> 0 and d <> 0 and a = 0,
  919. {(2*a*b + a*c*d - a)*z4 + (a*d*z1 + b*d*w1 - 2*b*w3 - 2*b*w4 + 4*b*z1 - c*d*w4
  920. - d*w2 + w3 + w4 - 2*z1)}},
  921. {a*d*z1 + b*d*w1 - 2*b*w3 + 4*b*z1 - d*w2 + w3 - 2*z1 <> 0 and a <> 0
  922. 2
  923. and b*d <> 0 and d <> 0 and a *z1 - a*w2 + w4 = 0 and a*b = 0 and a*c + 1 = 0
  924. and 2*b + c*d - 1 = 0 and c*d - 1 = 0,
  925. {(2*b + c*d - 1)*z3 + (a*d*z1 + b*d*w1 - 2*b*w3 + 4*b*z1 - d*w2 + w3 - 2*z1)}}
  926. ,
  927. {a*d*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 <> 0 and d <> 0 and a = 0 and b*d = 0,
  928. {(a*c*d - a)*z4 + (b*d)*z2 + (a*d*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1)}},
  929. 2
  930. {a*d*z1 - d*w2 + w3 - 2*z1 <> 0 and a <> 0 and d <> 0 and a *z1 - a*w2 + w4 = 0
  931. and a*b = 0 and a*c + 1 = 0 and b*d = 0 and c*d - 1 = 0,
  932. {(c*d - 1)*z3 + (b*d)*z2 + (a*d*z1 - d*w2 + w3 - 2*z1)}},
  933. {2*a*z1 - c*d*w1 + 2*c*w3 - 4*c*z1 + w1 - 2*w2 <> 0 and a <> 0 and c*d - 1 <> 0
  934. 2
  935. and d <> 0 and a *z1 - a*w2 + w4 = 0 and a*b = 0 and a*c + 1 = 0
  936. and 2*b + c*d - 1 = 0,
  937. {(2*b + c*d - 1)*z2 + (2*a*z1 - c*d*w1 + 2*c*w3 - 4*c*z1 + w1 - 2*w2)}},
  938. {2*a*z1 + 2*c*w3 - 4*c*z1 + w1 - 2*w2 <> 0 and a <> 0
  939. 2
  940. and a *z1 + a*c*w3 - 2*a*c*z1 - a*w2 + w3 + w4 - 2*z1 = 0 and a*b = 0
  941. and 2*b - 1 = 0 and d = 0,
  942. {(2*c*d)*z4 - (2*b - 1)*z2 - (2*a*z1 + 2*c*w3 - 4*c*z1 + w1 - 2*w2)}},
  943. {2*a*z1 - 2*c*w4 + w1 - 2*w2 <> 0 and d <> 0
  944. and a*d*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 = 0 and a = 0 and b*d = 0
  945. and 2*b - 1 = 0,
  946. {(2*a*c)*z4 + (2*b - 1)*z2 + (2*a*z1 - 2*c*w4 + w1 - 2*w2)}},
  947. {2*a*z1 - 2*c*w4 + w1 - 2*w2 <> 0 and a = 0 and 2*b - 1 = 0 and d = 0
  948. and w3 + w4 - 2*z1 = 0,
  949. {(2*a*c)*z4 + (2*b - 1)*z2 + (2*a*z1 - 2*c*w4 + w1 - 2*w2)}},
  950. 2
  951. {2*a*z1 + w1 - 2*w2 <> 0 and a <> 0 and d <> 0 and a *z1 - a*w2 + w4 = 0
  952. and a*b = 0 and a*c + 1 = 0 and a*d*z1 - d*w2 + w3 - 2*z1 = 0 and b*d = 0
  953. and 2*b - 1 = 0 and c*d - 1 = 0 and c = 0,
  954. {(2*c)*z3 + (2*b - 1)*z2 + (2*a*z1 + w1 - 2*w2)}},
  955. {a*z1 + b*w1 - 2*b*w5 + 2*b*z1 + c*w3 - 2*c*z1 - w2 + w5 - z1 <> 0 and a <> 0
  956. 2
  957. and 2*b - 1 <> 0 and a *z1 + a*c*w3 - 2*a*c*z1 - a*w2 + w3 + w4 - 2*z1 = 0
  958. and a*b = 0 and d = 0,
  959. {(c*d)*z4 - (a*z1 + b*w1 - 2*b*w5 + 2*b*z1 + c*w3 - 2*c*z1 - w2 + w5 - z1)}},
  960. {a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - c*w4 - w2 + w5 - z1 <> 0 and 2*b - 1 <> 0
  961. and d <> 0 and a*d*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 = 0 and a = 0
  962. and b*d = 0,
  963. {(a*c)*z4 + (a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - c*w4 - w2 + w5 - z1)}},
  964. {a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - c*w4 - w2 + w5 - z1 <> 0 and 2*b - 1 <> 0
  965. and a = 0 and d = 0 and w3 + w4 - 2*z1 = 0,
  966. {(a*c)*z4 + (a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - c*w4 - w2 + w5 - z1)}},
  967. {a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - w2 + w5 - z1 <> 0 and a <> 0 and 2*b - 1 <> 0
  968. 2
  969. and d <> 0 and a *z1 - a*w2 + w4 = 0 and a*b = 0 and a*c + 1 = 0
  970. and a*d*z1 - d*w2 + w3 - 2*z1 = 0 and b*d = 0 and c*d - 1 = 0 and c = 0,
  971. {c*z3 + (a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - w2 + w5 - z1)}},
  972. {a*z1 - c*d*w5 + c*d*z1 + c*w3 - 2*c*z1 - w2 + w5 - z1 <> 0 and a <> 0
  973. 2
  974. and c*d - 1 <> 0 and d <> 0 and a *z1 - a*w2 + w4 = 0 and a*b = 0
  975. and a*c + 1 = 0 and 2*a*z1 - c*d*w1 + 2*c*w3 - 4*c*z1 + w1 - 2*w2 = 0
  976. and 2*b + c*d - 1 = 0 and b = 0,
  977. {b*z2 + (a*z1 - c*d*w5 + c*d*z1 + c*w3 - 2*c*z1 - w2 + w5 - z1)}},
  978. {a <> 0 and b*d <> 0 and 2*b + c*d - 1 <> 0 and d <> 0
  979. 2 2 2
  980. and a *z1 - a*w2 + w4 = 0 and a*b = 0 and a*c*d *z1 + b*c*d *w1 - 2*b*c*d*w3
  981. 2 2
  982. + 4*b*c*d*z1 - 2*b*d*w5 + 2*b*d*z1 + 2*b*w3 - 4*b*z1 - c*d *w2 - c*d *w5
  983. 2
  984. + c*d *z1 + 2*c*d*w3 - 4*c*d*z1 + d*w5 - d*z1 - w3 + 2*z1 = 0 and a*c + 1 = 0
  985. and c*d - 1 = 0,
  986. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  987. a*z4 - z3 - w4,
  988. d*z4 + z3 - (w3 - 2*z1),
  989. 2*z4 + z2 - w1,
  990. z4 - (w5 - z1),
  991. (c*d - 1)*z3 + (b*d)*z2 + (a*d*z1 - d*w2 + w3 - 2*z1),
  992. (2*b + c*d - 1)*z3 + (a*d*z1 + b*d*w1 - 2*b*w3 + 4*b*z1 - d*w2 + w3 - 2*z1)}}
  993. ,
  994. 2
  995. {a <> 0 and b*d <> 0 and d <> 0 and a *z1 - a*w2 + w4 = 0 and a*b = 0
  996. and a*c + 1 = 0 and a*d*z1 + b*d*w1 - 2*b*w3 + 4*b*z1 - d*w2 + w3 - 2*z1 = 0
  997. and 2*b + c*d - 1 = 0 and c*d - 1 = 0,
  998. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  999. a*z4 - z3 - w4,
  1000. d*z4 + z3 - (w3 - 2*z1),
  1001. 2*z4 + z2 - w1,
  1002. z4 - (w5 - z1),
  1003. (c*d - 1)*z3 + (b*d)*z2 + (a*d*z1 - d*w2 + w3 - 2*z1),
  1004. z3 + (d*w5 - d*z1 - w3 + 2*z1)}},
  1005. {a <> 0 and 2*b + c*d - 1 <> 0 and c*d - 1 <> 0 and d <> 0
  1006. 2
  1007. and a *z1 - a*w2 + w4 = 0 and a*b = 0 and a*c*d*z1 - a*z1 + b*c*d*w1
  1008. 2 2 2 2
  1009. - 2*b*c*d*w5 + 2*b*c*d*z1 - b*w1 + 2*b*w5 - 2*b*z1 - c *d *w5 + c *d *z1
  1010. 2 2
  1011. + c *d*w3 - 2*c *d*z1 - c*d*w2 + 2*c*d*w5 - 2*c*d*z1 - c*w3 + 2*c*z1 + w2
  1012. - w5 + z1 = 0 and a*c + 1 = 0,
  1013. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1014. a*z4 - z3 - w4,
  1015. d*z4 + z3 - (w3 - 2*z1),
  1016. 2*z4 + z2 - w1,
  1017. z4 - (w5 - z1),
  1018. (c*d - 1)*z3 + (b*d)*z2 + (a*d*z1 - d*w2 + w3 - 2*z1),
  1019. (2*b + c*d - 1)*z2 + (2*a*z1 - c*d*w1 + 2*c*w3 - 4*c*z1 + w1 - 2*w2)}},
  1020. 2
  1021. {a <> 0 and 2*b - 1 <> 0 and d <> 0 and a *z1 - a*w2 + w4 = 0 and a*b = 0
  1022. and a*c + 1 = 0 and a*d*z1 - d*w2 + w3 - 2*z1 = 0
  1023. and a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - w2 + w5 - z1 = 0 and b*d = 0
  1024. and c*d - 1 = 0 and c = 0,
  1025. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1026. a*z4 - z3 - w4,
  1027. d*z4 + z3 - (w3 - 2*z1),
  1028. 2*z4 + z2 - w1,
  1029. z4 - (w5 - z1),
  1030. (2*c)*z3 + (2*b - 1)*z2 + (2*a*z1 + w1 - 2*w2)}},
  1031. {a <> 0 and 2*b - 1 <> 0
  1032. 2
  1033. and a *z1 + a*c*w3 - 2*a*c*z1 - a*w2 + w3 + w4 - 2*z1 = 0 and a*b = 0
  1034. and a*z1 + b*w1 - 2*b*w5 + 2*b*z1 + c*w3 - 2*c*z1 - w2 + w5 - z1 = 0
  1035. and d = 0,
  1036. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1037. a*z4 - z3 - w4,
  1038. d*z4 + z3 - (w3 - 2*z1),
  1039. 2*z4 + z2 - w1,
  1040. (2*c*d)*z4 - (2*b - 1)*z2 - (2*a*z1 + 2*c*w3 - 4*c*z1 + w1 - 2*w2),
  1041. z4 - (w5 - z1)}},
  1042. 2
  1043. {a <> 0 and b <> 0 and c*d - 1 <> 0 and d <> 0 and a *z1 - a*w2 + w4 = 0
  1044. and a*b = 0 and a*c + 1 = 0
  1045. and 2*a*z1 - c*d*w1 + 2*c*w3 - 4*c*z1 + w1 - 2*w2 = 0 and 2*b + c*d - 1 = 0,
  1046. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1047. a*z4 - z3 - w4,
  1048. d*z4 + z3 - (w3 - 2*z1),
  1049. 2*z4 + z2 - w1,
  1050. z4 - (w5 - z1),
  1051. (c*d - 1)*z3 + (b*d)*z2 + (a*d*z1 - d*w2 + w3 - 2*z1),
  1052. b*z2 + (a*z1 - c*d*w5 + c*d*z1 + c*w3 - 2*c*z1 - w2 + w5 - z1)}},
  1053. 2
  1054. {a <> 0 and c*d - 1 <> 0 and d <> 0 and a *z1 - a*w2 + w4 = 0 and a*b = 0
  1055. and a*c + 1 = 0 and 2*a*z1 - c*d*w1 + 2*c*w3 - 4*c*z1 + w1 - 2*w2 = 0
  1056. and a*z1 - c*d*w5 + c*d*z1 + c*w3 - 2*c*z1 - w2 + w5 - z1 = 0
  1057. and 2*b + c*d - 1 = 0 and b = 0,
  1058. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1059. a*z4 - z3 - w4,
  1060. d*z4 + z3 - (w3 - 2*z1),
  1061. 2*z4 + z2 - w1,
  1062. z4 - (w5 - z1),
  1063. (c*d - 1)*z3 + (b*d)*z2 + (a*d*z1 - d*w2 + w3 - 2*z1)}},
  1064. 2
  1065. {a <> 0 and c <> 0 and d <> 0 and a *z1 - a*w2 + w4 = 0 and a*b = 0
  1066. and a*c + 1 = 0 and a*d*z1 - d*w2 + w3 - 2*z1 = 0 and b*d = 0 and c*d - 1 = 0
  1067. ,
  1068. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1069. a*z4 - z3 - w4,
  1070. d*z4 + z3 - (w3 - 2*z1),
  1071. 2*z4 + z2 - w1,
  1072. z4 - (w5 - z1),
  1073. (2*c)*z3 + (2*b - 1)*z2 + (2*a*z1 + w1 - 2*w2),
  1074. z2 - (w1 - 2*w5 + 2*z1)}},
  1075. 2
  1076. {a <> 0 and d <> 0 and a *z1 - a*w2 + w4 = 0 and a*b = 0 and a*c + 1 = 0
  1077. and a*d*z1 - d*w2 + w3 - 2*z1 = 0 and 2*a*z1 + w1 - 2*w2 = 0 and b*d = 0
  1078. and 2*b - 1 = 0 and c*d - 1 = 0 and c = 0,
  1079. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1080. a*z4 - z3 - w4,
  1081. d*z4 + z3 - (w3 - 2*z1),
  1082. 2*z4 + z2 - w1,
  1083. z4 - (w5 - z1),
  1084. c*z3 + b*z2 + (a*z1 - w2 + w5 - z1)}},
  1085. 2
  1086. {a <> 0 and a *z1 + a*c*w3 - 2*a*c*z1 - a*w2 + w3 + w4 - 2*z1 = 0 and a*b = 0
  1087. and 2*a*z1 + 2*c*w3 - 4*c*z1 + w1 - 2*w2 = 0 and 2*b - 1 = 0 and d = 0,
  1088. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1089. a*z4 - z3 - w4,
  1090. d*z4 + z3 - (w3 - 2*z1),
  1091. 2*z4 + z2 - w1,
  1092. (c*d)*z4 - b*z2 - (a*z1 + c*w3 - 2*c*z1 - w2 + w5 - z1),
  1093. z4 - (w5 - z1)}},
  1094. {b*d <> 0 and d*w5 - d*z1 - w3 - w4 + 2*z1 <> 0 and d <> 0 and
  1095. a*d*z1 + b*d*w1 - 2*b*w3 - 2*b*w4 + 4*b*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1
  1096. = 0 and a = 0,
  1097. {a*z4 + (d*w5 - d*z1 - w3 - w4 + 2*z1)}},
  1098. {b*d <> 0 and d <> 0 and
  1099. a*d*z1 + b*d*w1 - 2*b*w3 - 2*b*w4 + 4*b*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1
  1100. = 0 and a = 0 and d*w5 - d*z1 - w3 - w4 + 2*z1 = 0,
  1101. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1102. a*z4 - z3 - w4,
  1103. d*z4 + z3 - (w3 - 2*z1),
  1104. 2*z4 + z2 - w1,
  1105. (a*c*d - a)*z4 + (b*d)*z2 + (a*d*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1),
  1106. z4 - (w5 - z1)}},
  1107. {2*b - 1 <> 0 and d <> 0 and a*d*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 = 0
  1108. and a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - c*w4 - w2 + w5 - z1 = 0 and a = 0
  1109. and b*d = 0,
  1110. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1111. a*z4 - z3 - w4,
  1112. d*z4 + z3 - (w3 - 2*z1),
  1113. 2*z4 + z2 - w1,
  1114. (2*a*c)*z4 + (2*b - 1)*z2 + (2*a*z1 - 2*c*w4 + w1 - 2*w2),
  1115. z4 - (w5 - z1)}},
  1116. {2*b - 1 <> 0 and a*z1 + b*w1 - 2*b*w5 + 2*b*z1 - c*w4 - w2 + w5 - z1 = 0
  1117. and a = 0 and d = 0 and w3 + w4 - 2*z1 = 0,
  1118. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1119. a*z4 - z3 - w4,
  1120. d*z4 + z3 - (w3 - 2*z1),
  1121. 2*z4 + z2 - w1,
  1122. (2*a*c)*z4 + (2*b - 1)*z2 + (2*a*z1 - 2*c*w4 + w1 - 2*w2),
  1123. z4 - (w5 - z1)}},
  1124. {d <> 0 and a*d*z1 - c*d*w4 - d*w2 + w3 + w4 - 2*z1 = 0
  1125. and 2*a*z1 - 2*c*w4 + w1 - 2*w2 = 0 and a = 0 and b*d = 0 and 2*b - 1 = 0,
  1126. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1127. a*z4 - z3 - w4,
  1128. d*z4 + z3 - (w3 - 2*z1),
  1129. 2*z4 + z2 - w1,
  1130. (a*c)*z4 + b*z2 + (a*z1 - c*w4 - w2 + w5 - z1),
  1131. z4 - (w5 - z1)}},
  1132. {w3 + w4 - 2*z1 <> 0 and a = 0 and d = 0,
  1133. {(a + d)*z4 - (w3 + w4 - 2*z1)}},
  1134. {2*a*z1 - 2*c*w4 + w1 - 2*w2 = 0 and a = 0 and 2*b - 1 = 0 and d = 0
  1135. and w3 + w4 - 2*z1 = 0,
  1136. {z4 + c*z3 + b*z2 + (a*z1 - w2),
  1137. a*z4 - z3 - w4,
  1138. d*z4 + z3 - (w3 - 2*z1),
  1139. 2*z4 + z2 - w1,
  1140. (a*c)*z4 + b*z2 + (a*z1 - c*w4 - w2 + w5 - z1),
  1141. z4 - (w5 - z1)}}}
  1142. torder oo;
  1143. {{z4,z3,z2,z2},revgradlex}
  1144. % Two dimensional transportation problem
  1145. oo := torder({x33,x32,x31,x23,x22,x21,x13,x12,x11},lex);
  1146. oo := {{},lex}
  1147. gsys({x11+x12+x13-a1,x11+x21+x31-b1,x12+x22+x32-b2,x13+x23+x33-b3,
  1148. x21+x22+x23-a2,x31+x32+x33-a3});
  1149. {{a1 + a2 + a3 - b1 - b2 - b3 <> 0,
  1150. {a1 + a2 + a3 - b1 - b2 - b3}},
  1151. {a1 + a2 + a3 - b1 - b2 - b3 = 0,
  1152. {x33 + x32 + x31 - a3,
  1153. x33 + x23 + x13 - b3,
  1154. x32 + x22 + x12 - b2,
  1155. x31 + x21 + x11 - b1,
  1156. x23 + x22 + x21 - a2,
  1157. x13 + x12 + x11 - a1}}}
  1158. torder oo;
  1159. {{x33,x32,x31,x23,x22,x21,x13,x12,x11},lex}
  1160. % Thomas Weis's Example 1
  1161. oo := torder({x,y,z},lex);
  1162. oo := {{},lex}
  1163. gsys({z*y*x-b*y*x-b*z*x+b**2*x-b*z*y+b**2*y+b**2*z-(n3+b**3),
  1164. z*y*x-a*y*x-a*z*x+a**2*x-a*z*y+a**2*y+a**2*z-(n3+a**3),
  1165. z*y*x-n1});
  1166. 3 3
  1167. {{a *b - a*b + a*n1 - a*n3 - b*n1 + b*n3 <> 0 and a - b <> 0
  1168. 2 2
  1169. and a *b - a*b = 0,
  1170. 2 2 2 2 2 2
  1171. {(a *b - a*b )*x + (a *b - a*b )*y + (a *b - a*b )*z
  1172. 3 3
  1173. - (a *b - a*b + a*n1 - a*n3 - b*n1 + b*n3)}},
  1174. 3
  1175. {a - n1 + n3 <> 0 and a - b = 0 and a = 0,
  1176. 2 2 2 3
  1177. {a*x*y + a*x*z - a *x + a*y*z - a *y - a *z + (a - n1 + n3)}},
  1178. 2 2
  1179. {a *b - a*b <> 0 and a - b <> 0,
  1180. 2 2 2 3
  1181. {x*y*z - a*x*y - a*x*z + a *x - a*y*z + a *y + a *z - (a + n3),
  1182. 2 2 2 3
  1183. x*y*z - b*x*y - b*x*z + b *x - b*y*z + b *y + b *z - (b + n3),
  1184. x*y*z - n1,
  1185. 2 2 2 2
  1186. (a - b)*x*y + (a - b)*x*z - (a - b )*x + (a - b)*y*z - (a - b )*y
  1187. 2 2 3 3
  1188. - (a - b )*z + (a - b ),
  1189. 2 2 2 2 2 2
  1190. (a *b - a*b )*x + (a *b - a*b )*y + (a *b - a*b )*z
  1191. 3 3
  1192. - (a *b - a*b + a*n1 - a*n3 - b*n1 + b*n3),
  1193. 2 2 2 2 2
  1194. (a *b - a*b )*y + (a *b - a*b )*y*z
  1195. 3 3 2 2 2
  1196. - (a *b - a*b + a*n1 - a*n3 - b*n1 + b*n3)*y + (a *b - a*b )*z
  1197. 3 3
  1198. - (a *b - a*b + a*n1 - a*n3 - b*n1 + b*n3)*z
  1199. 3 2 2 3 2 2 2 2
  1200. + (a *b - a *b + a *n1 - a *n3 - b *n1 + b *n3),
  1201. 2 2 3 3 3 2
  1202. (a *b - a*b )*z - (a *b - a*b + a*n1 - a*n3 - b*n1 + b*n3)*z
  1203. 3 2 2 3 2 2 2 2 2 2
  1204. + (a *b - a *b + a *n1 - a *n3 - b *n1 + b *n3)*z - (a *b*n1 - a*b *n1)}},
  1205. 3 3 2 2
  1206. {a - b <> 0 and a *b - a*b + a*n1 - a*n3 - b*n1 + b*n3 = 0 and a *b - a*b = 0
  1207. ,
  1208. 2 2 2 3
  1209. {x*y*z - a*x*y - a*x*z + a *x - a*y*z + a *y + a *z - (a + n3),
  1210. 2 2 2 3
  1211. x*y*z - b*x*y - b*x*z + b *x - b*y*z + b *y + b *z - (b + n3),
  1212. x*y*z - n1,
  1213. 2 2 2 2
  1214. (a - b)*x*y + (a - b)*x*z - (a - b )*x + (a - b)*y*z - (a - b )*y
  1215. 2 2 3 3
  1216. - (a - b )*z + (a - b ),
  1217. 2 2 2 2 2 2 2 2
  1218. (a - b)*x*z - (a - b )*x*z + (a *b - a*b )*x + (a - b)*y*z - (a - b )*y*z
  1219. 2 2 2 2 2 3 2 2 3
  1220. + (a *b - a*b )*y - (a - b )*z + (a + a *b - a*b - b )*z
  1221. 3 3
  1222. - (a *b - a*b - a*n3 + b*n3),
  1223. 2 2 2 2 2 2 2 2 2 2 2
  1224. (a - b)*y *z - (a - b )*y *z + (a *b - a*b )*y - (a - b )*y*z
  1225. 3 2 2 3 3 3
  1226. + (a + a *b - a*b - b )*y*z - (a *b - a*b - a*n3 + b*n3)*y
  1227. 2 2 2 3 3
  1228. + (a *b - a*b )*z - (a *b - a*b - a*n3 + b*n3)*z
  1229. 3 2 2 3 2 2
  1230. + (a *b - a *b - a *n3 + b *n3)}},
  1231. {a <> 0 and a - b = 0,
  1232. 2 2 2 3
  1233. {x*y*z - a*x*y - a*x*z + a *x - a*y*z + a *y + a *z - (a + n3),
  1234. 2 2 2 3
  1235. x*y*z - b*x*y - b*x*z + b *x - b*y*z + b *y + b *z - (b + n3),
  1236. x*y*z - n1,
  1237. 2 2 2 3
  1238. a*x*y + a*x*z - a *x + a*y*z - a *y - a *z + (a - n1 + n3),
  1239. 2 2 2 2 2 2 3
  1240. a*x*z - a *x*z + a*y*z - a *y*z - a *z + (a - n1 + n3)*z + a*n1,
  1241. 2 2 2 2 2 2 3
  1242. a*y *z - a *y *z - a *y*z + (a - n1 + n3)*y*z + (a*n1)*y + (a*n1)*z
  1243. 2
  1244. - a *n1}},
  1245. 3
  1246. {a - n1 + n3 = 0 and a - b = 0 and a = 0,
  1247. 2 2 2 3
  1248. {x*y*z - a*x*y - a*x*z + a *x - a*y*z + a *y + a *z - (a + n3),
  1249. 2 2 2 3
  1250. x*y*z - b*x*y - b*x*z + b *x - b*y*z + b *y + b *z - (b + n3),
  1251. x*y*z - n1}}}
  1252. torder oo;
  1253. {{x,y,z},lex}
  1254. % Thomas Weis's Example 2
  1255. oo := torder({z,y,x,w},lex);
  1256. oo := {{},lex}
  1257. gsys({w*x*y*z-x*y*z-w*y*z+y*z-w*x*z+x*z+w*z-z-w*x*y+x*y+w*y-
  1258. y+w*x-x-w-(b-1),
  1259. w*x*y*z-2*x*y*z-2*w*y*z+4*y*z-2*w*x*z+4*x*z+4*w*z-8*z-2*w*x*y+4x*y+
  1260. 4*w*y-8*y+4*w*x-8*x-8*w-(c-16),
  1261. w*x*y*z-a,z+y+x+w-v});
  1262. {{true,
  1263. {z*y*x*w - z*y*x - z*y*w + z*y - z*x*w + z*x + z*w - z - y*x*w + y*x + y*w - y
  1264. + x*w - x - w - (b - 1),
  1265. z*y*x*w - 2*z*y*x - 2*z*y*w + 4*z*y - 2*z*x*w + 4*z*x + 4*z*w - 8*z - 2*y*x*w
  1266. + 4*y*x + 4*y*w - 8*y + 4*x*w - 8*x - 8*w - (c - 16),
  1267. z*y*x*w - a,
  1268. z + y + x + w - v,
  1269. 2 2 2 2 2
  1270. y *x + y *w - 3*y + y*x + 2*y*x*w - (v + 3)*y*x + y*w - (v + 3)*y*w
  1271. 2 2 2 2
  1272. + (3*v)*y + x *w - 3*x + x*w - (v + 3)*x*w + (3*v)*x - 3*w + (3*v)*w
  1273. + (b - c - 7*v + 15),
  1274. 2 2 2
  1275. 2*y + 2*y*x + 2*y*w - (2*v)*y + 2*x + 2*x*w - (2*v)*x + 2*w - (2*v)*w
  1276. + (a - 2*b + c + 6*v - 14),
  1277. 3 2 2 2
  1278. 2*x + 2*x *w - (2*v)*x + 2*x*w - (2*v)*x*w + (a - 2*b + c + 6*v - 14)*x
  1279. 3 2
  1280. + 2*w - (2*v)*w + (a - 2*b + c + 6*v - 14)*w - (3*a - 4*b + c + 4*v - 12),
  1281. 4 3 2
  1282. 2*w - (2*v)*w + (a - 2*b + c + 6*v - 14)*w - (3*a - 4*b + c + 4*v - 12)*w
  1283. + 2*a}}}
  1284. torder oo;
  1285. {{z,y,x,w},lex}
  1286. end;
  1287. Time for test: 451 ms, plus GC time: 21 ms