defintf.red 11 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426
  1. module defintf;
  2. algebraic <<
  3. operator case20,case21,case22,case23,case24,case25,
  4. case26,case27,case28,case29,case30,case31,case32,case33,
  5. case34,case35;
  6. case20_rules :=
  7. { case20(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  8. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  9. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  10. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  11. when n = 0
  12. and m > 0
  13. and epsilon > 0
  14. and phi < 0
  15. and test_1a = 't and test_1b = 't and test_2 = 't
  16. and test_12 = 't
  17. and transform_test('test2,'test12,nil,nil,nil,nil,nil,nil) = 't
  18. };
  19. let case20_rules;
  20. case21_rules :=
  21. { case21(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  22. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  23. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  24. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  25. when m = 0
  26. and n > 0
  27. and epsilon > 0
  28. and phi > 0
  29. and test_1a = 't and test_1b = 't and test_3 = 't
  30. and test_12 = 't
  31. and transform_test('test12,nil,nil,nil,nil,nil,nil,nil) = 't
  32. };
  33. let case21_rules;
  34. case22_rules :=
  35. { case22(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  36. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  37. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  38. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  39. when k*l = 0
  40. and delta > 0
  41. and epsilon > 0
  42. and test_1a = 't and test_1b = 't and test_2 = 't
  43. and test_3 = 't and test_10 = 't and test_12 = 't
  44. and transform_test('test2,'test3,'test10,'test12,nil,nil,nil,
  45. nil)= 't
  46. };
  47. let case22_rules;
  48. case23_rules :=
  49. { case23(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  50. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  51. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  52. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  53. when m*n = 0
  54. and delta > 0
  55. and epsilon > 0
  56. and test_1a = 't and test_1b = 't and test_2 = 't
  57. and test_3 = 't and test_10 = 't and test_12 = 't
  58. and transform_test('test2,'test3,'test10,'test12,nil,nil,nil,
  59. nil) = 't
  60. };
  61. let case23_rules;
  62. case24_rules :=
  63. { case24(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  64. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  65. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  66. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  67. when m + n > p
  68. and l = 0
  69. and phi = 0
  70. and k > 0
  71. and delta > 0
  72. and epsilon < 0
  73. and mylessp(abs(atan(impart omega/repart omega)),m + n - p + 1)
  74. and test_1a = 't and test_1b = 't and test_2 = 't
  75. and test_10 = 't and test_14 = 't and test_15 ='t
  76. and transform_test('test2,'test10,'test14,'test15,nil,nil,nil,
  77. nil) = 't
  78. };
  79. let case24_rules;
  80. case25_rules :=
  81. { case25(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  82. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  83. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  84. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  85. when m + n > q
  86. and k = 0
  87. and phi = 0
  88. and l > 0
  89. and delta > 0
  90. and epsilon < 0
  91. and mylessp(abs(atan(impart omega/repart omega)),m + n - q + 1)
  92. and test_1a = 't and test_1b = 't and test_3 = 't
  93. and test_10 = 't and test_14 = 't and test_15 ='t
  94. and transform_test('test3,'test10,'test14,'test15,nil,nil,nil,
  95. nil) = 't
  96. };
  97. let case25_rules;
  98. case26_rules :=
  99. { case26(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  100. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  101. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  102. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  103. when p = q - 1
  104. and l = 0
  105. and phi = 0
  106. and k > 0
  107. and delta > 0
  108. and epsilon >= 0
  109. and test_arg(abs(atan(impart omega/repart omega)),
  110. epsilon,epsilon + 1)
  111. and test_1a = 't and test_1b = 't and test_2 = 't
  112. and test_10 = 't and test_14 = 't and test_15 = 't
  113. and transform_test('test2,'test10,'test14,'test15,nil,nil,nil,
  114. nil) = 't
  115. };
  116. let case26_rules;
  117. case27_rules :=
  118. { case27(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  119. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  120. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  121. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  122. when p = q + 1
  123. and k = 0
  124. and phi = 0
  125. and l > 0
  126. and delta > 0
  127. and epsilon >= 0
  128. and test_arg(abs(atan(impart omega/repart omega)),
  129. epsilon,epsilon + 1)
  130. and test_1a = 't and test_1b = 't and test_3 = 't
  131. and test_10 = 't and test_14 = 't and test_15 = 't
  132. and transform_test('test3,'test10,'test14,'test15,nil,nil,nil,
  133. nil) = 't
  134. };
  135. let case27_rules;
  136. case28_rules :=
  137. { case28(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  138. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  139. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  140. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  141. when p < q - 1
  142. and l = 0
  143. and phi = 0
  144. and k > 0
  145. and delta > 0
  146. and epsilon >= 0
  147. and test_arg(abs(atan(impart omega/repart omega)),
  148. epsilon,m + n - p + 1)
  149. and test_1a = 't and test_1b = 't and test_2 = 't
  150. and test_10 = 't and test_14 = 't and test_15 = 't
  151. and transform_test('test2,'test10,'test14,'test15,nil,nil,nil,
  152. nil) = 't
  153. };
  154. let case28_rules;
  155. case29_rules :=
  156. { case29(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  157. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  158. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  159. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  160. when p > q + 1
  161. and k = 0
  162. and phi = 0
  163. and l > 0
  164. and delta > 0
  165. and epsilon >= 0
  166. and test_arg(abs(atan(impart omega/repart omega)),
  167. epsilon,m + n - q + 1)
  168. and test_1a = 't and test_1b = 't and test_3 = 't
  169. and test_10 = 't and test_14 = 't and test_15 = 't
  170. and transform_test('test3,'test10,'test14,'test15,nil,nil,nil,
  171. nil) = 't
  172. };
  173. let case29_rules;
  174. case30_rules :=
  175. { case30(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  176. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  177. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  178. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  179. when n = 0
  180. and phi = 0
  181. and k + l > u
  182. and m > 0
  183. and epsilon > 0
  184. and delta < 0
  185. and mylessp(abs(atan(impart sigma/repart sigma)),k + l - u + 1)
  186. and test_1a = 't and test_1b = 't and test_2 = 't
  187. and test_12 = 't and test_14 = 't and test_15 = 't
  188. and transform_test('test2,'test12,'test14,'test15,nil,nil,nil,
  189. nil) = 't
  190. };
  191. let case30_rules;
  192. case31_rules :=
  193. { case31(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  194. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  195. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  196. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  197. when m = 0
  198. and phi = 0
  199. and k + l > v
  200. and n > 0
  201. and epsilon > 0
  202. and delta < 0
  203. and mylessp(abs(atan(impart sigma/repart sigma)),k + l - v + 1)
  204. and test_1a = 't and test_1b = 't and test_3 = 't
  205. and test_12 = 't and test_14 = 't and test_15 = 't
  206. and transform_test('test3,'test12,'test14,'test15,nil,nil,nil,
  207. nil) = 't
  208. };
  209. let case31_rules;
  210. case32_rules :=
  211. { case32(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  212. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  213. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  214. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  215. when n = 0
  216. and phi = 0
  217. and u = v - 1
  218. and m > 0
  219. and epsilon > 0
  220. and delta >= 0
  221. and test_arg(abs(atan(impart sigma/repart sigma)),
  222. delta,delta + 1)
  223. and test_1a = 't and test_1b = 't and test_2 = 't
  224. and test_12 = 't and test_14 = 't and test_15 = 't
  225. and transform_test('test2,'test12,'test14,'test15,nil,nil,nil,
  226. nil) = 't
  227. };
  228. let case32_rules;
  229. case33_rules :=
  230. { case33(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  231. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  232. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  233. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  234. when m = 0
  235. and phi = 0
  236. and u = v + 1
  237. and n > 0
  238. and epsilon > 0
  239. and delta >= 0
  240. and test_arg(abs(atan(impart sigma/repart sigma)),
  241. delta,delta + 1)
  242. and test_1a = 't and test_1b = 't and test_3 = 't
  243. and test_12 = 't and test_14 = 't and test_15 = 't
  244. and transform_test('test3,'test12,'test14,'test15,nil,nil,nil,
  245. nil) = 't
  246. };
  247. let case33_rules;
  248. case34_rules :=
  249. { case34(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  250. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  251. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  252. ~test_11,~test_12,~test_13,~test_14,~test_15) => 't
  253. when n = 0
  254. and phi = 0
  255. and u < v - 1
  256. and m > 0
  257. and epsilon > 0
  258. and delta >= 0
  259. and test_arg(abs(atan(impart sigma/repart sigma)),
  260. delta,k + l - u + 1)
  261. and test_1a = 't and test_1b = 't and test_2 = 't
  262. and test_12 = 't and test_14 = 't and test_15 = 't
  263. and transform_test('test2,'test12,'test14,'test15,nil,nil,nil,
  264. nil) = 't
  265. };
  266. let case34_rules;
  267. case35_rules :=
  268. { case35(~m,~n,~p,~q,~k,~l,~u,~v,~delta,~epsilon,~sigma,~omega,~rho,
  269. ~eta,~mu,~r1,~r2,~phi,~test_1a,~test_1b,~test_2,~test_3,
  270. ~test_4,~test_5,~test_6,~test_7,~test_8,~test_9,~test_10,
  271. ~test_11,~test_12,~test_13,~test_14,~test_15) => t
  272. when m = 0
  273. and phi = 0
  274. and u > v + 1
  275. and n > 0
  276. and epsilon > 0
  277. and delta >= 0
  278. and test_arg(abs(atan(impart sigma/repart sigma)),
  279. delta,k + l - v + 1)
  280. and test_1a = t and test_1b = t and test_3 = t
  281. and test_12 = t and test_14 = t and test_15 = t
  282. and transform_test('test3,'test12,'test14,'test15,nil,nil,nil,
  283. nil) = t
  284. };
  285. let case35_rules;
  286. flag('(test_arg),'boolean);
  287. algebraic procedure test_arg(a,b,c);
  288. begin scalar !*rounded,dmode!*;
  289. if transform_tst neq t then
  290. << on rounded;
  291. if b*pi < a and a < c*pi then << off rounded; return t>>
  292. else << off rounded; return nil>>;
  293. >>
  294. else return t;
  295. end;
  296. >>;
  297. symbolic procedure transform_test(n1,n2,n3,n4,n5,n6,n7,n8);
  298. begin scalar lst,temp,cond_test;
  299. if transform_tst neq t then return t
  300. else
  301. << lst := {n1,n2,n3,n4,n5,n6,n7,n8};
  302. for each i in lst do
  303. if i then temp := lispeval cdr assoc(i,transform_lst) . temp; ;
  304. temp := 'and . temp;
  305. for each j in spec_cond do if j = temp then cond_test := t;
  306. if cond_test neq t then spec_cond := temp . spec_cond;
  307. return nil;
  308. >>;
  309. end;
  310. symbolic operator transform_test;
  311. flag('(sigma_tst),'boolean);
  312. algebraic procedure sigma_tst(sigma);
  313. begin scalar test;
  314. if transform_tst neq t then
  315. << if sigma > 0 then return t else return nil>>
  316. else
  317. << if test neq t then
  318. << symbolic(transform_lst := cons (('sigma_cond .'(list 'greaterp
  319. 'sigma 0)),transform_lst));
  320. test := t>>;
  321. return reval t>>;
  322. end;
  323. flag('(omega_tst),'boolean);
  324. symbolic procedure omega_tst(omega);
  325. begin scalar test;
  326. if transform_tst neq t then
  327. << if omega > 0 then return t else return nil>>
  328. else
  329. << if test neq t then
  330. << symbolic(transform_lst := cons (('omega_cond .'(list 'greaterp
  331. 'omega 0)),transform_lst));
  332. test := t>>;
  333. return reval t>>;
  334. end;
  335. endmodule;
  336. end;