Changeset 174
- Timestamp:
- 12/28/07 19:43:51 (4 years ago)
- Files:
-
- trunk/backmath/backmath.d (modified) (4 diffs)
- trunk/backmath/gen_code_for_template.lisp (modified) (2 diffs)
- trunk/backmath/generate_case.lisp (modified) (2 diffs)
- trunk/backmath/generated_rules.d (modified) (55 diffs)
- trunk/backmath/meta.lisp (modified) (32 diffs)
- trunk/backmath/string_stuff.lisp (modified) (1 diff)
Legend:
- Unmodified
- Added
- Removed
- Modified
- Copied
- Moved
trunk/backmath/backmath.d
r173 r174 4 4 Author: Benjamin Shropshire 5 5 6 Copywrite: You may used this code only if you accept all risk involved in doing so. It is highly experimental and probably contains bugs. I DON'T warrant it for any use. 6 Note: 7 If this library can't handle something you feed it it will spit out a 8 line with a message something like this: 9 10 "invalid types used for Sub: (- (*> a (-> (* e a) b)) (/> c (-> (/ d c) b)))" 11 12 If you want to help improve the library (and make it work in your case) 13 then you can add a rule to meta.lisp that will handle the case you are 14 running into. Here is an example of how to generate a rule for the above 15 case: 16 17 start with the given lisp s-expression 18 19 (- (*> a (-> (* e a) b)) (/> c (-> (/ d c) b))) 20 21 replace any known sections with new variables 22 23 (- (*> a (-> e b)) (/> c (-> d b))) 24 25 pull out and name any (_> ...) sections and replace them with the name 26 27 (- W T) 28 W = (*> a (-> e b)) 29 T = (/> c (-> d b)) 30 31 "Invert" the named expressions 32 33 (- W T) 34 (- (* W a) e) = b 35 (- (/ T c) d) = b 36 37 solve for the placeholders 38 39 (- W T) 40 W = (/ (+ b e) a) 41 T = (* (+ b d) c) 42 43 substitute back in 44 45 (- (/ (+ b e) a) (* (+ b d) c)) 46 47 isolate the unknown (in this case "b") 48 49 (- (/ (+ b e) a) (* (+ b d) c)) 50 (- (+ (/ b a) (/ e a)) (+ (* b c) (* d c))) 51 (- (- (+ (/ b a) (/ e a)) (* b c)) (* d c)) 52 (- (+ (- (/ b a) (* b c)) (/ e a)) (* d c)) 53 (- (+ (* b (- (/ 1 a) (* 1 c))) (/ e a)) (* d c)) 54 (- (+ (* b (- (/ 1 a) c)) (/ e a)) (* d c)) 55 (+ (+ (* b (- (/ 1 a) c)) (/ e a)) (- (* d c))) 56 (+ (* b (- (/ 1 a) c)) (/ e a) (- (* d c))) 57 (+ (* b (- (/ 1 a) c)) (- (/ e a) (* d c))) 58 59 solve for the unknown 60 61 y = (+ (* b (- (/ 1 a) c)) (- (/ e a) (* d c))) 62 (- y (- (/ e a) (* d c))) = (* b (- (/ 1 a) c)) 63 (/ (- y (- (/ e a) (* d c))) (- (/ 1 a) c)) = b 64 65 convert to "(+,- (*,/ y a) b) = x" from 66 67 (/ (- y (- (/ e a) (* d c))) (- (/ 1 a) c)) = b 68 (- (/ y (- (/ 1 a) c)) (/ (- (/ e a) (* d c)) (- (/ 1 a) c))) = b 69 70 convert to "assignment form" 71 72 (- (/ y (- (/ 1 a) c)) (/ (- (/ e a) (* d c)) (- (/ 1 a) c))) = b 73 (/ y (- (/ 1 a) c)) = (-> (/ (- (/ e a) (* d c)) (- (/ 1 a) c)) b) 74 y = (/> (- (/ 1 a) c) (-> (/ (- (/ e a) (* d c)) (- (/ 1 a) c)) b)) 75 76 insert the new rule 77 78 ( 79 (- (*> a (-> e b)) (/> c (-> d b))) 80 (/> (- (/ 1 a) c) (-> (/ (- (/ e a) (* d c)) (- (/ 1 a) c)) b)) 81 ) 82 83 in most cases meta.lisp should contain the original case or a generalization 84 of it. 85 86 87 Copywrite: You may used this code only if you accept all risk involved in 88 doing so. It is highly experimental and probably contains bugs. I DON'T 89 warrant it for any use. 7 90 8 91 Version: 0.001 … … 11 94 12 95 import std.stdio; 96 97 98 /* ***************************************************** 99 * Formatting code shamelessly stolen from ddl.meta.conv 100 * 101 * Author: Don Clugston. 102 * License: Public domain. 103 */ 104 105 /* ***************************************************** 106 * char [] fcvt!(real x) 107 * Convert a real number x to %f format 108 */ 109 template fcvt(real x) 110 { 111 static if (x<0) { 112 const real fcvt = "-" ~ .fcvt!(-x); 113 } else static if (x==cast(long)x) { 114 const char [] fcvt = itoa!(cast(long)x); 115 } else { 116 const char [] fcvt = itoa!(cast(long)x) ~ "." ~ chomp!(afterdec!(x - cast(long)x), '0'); 117 } 118 } 119 120 template decimaldigit(int n) { const char [] decimaldigit = "0123456789"[n..n+1]; } 121 122 /* ***************************************************** 123 * char [] itoa!(long n); 124 */ 125 template itoa(long n) 126 { 127 static if (n<0) 128 const char [] itoa = "-" ~ itoa!(-n); 129 else static if (n<10L) 130 const char [] itoa = decimaldigit!(n); 131 else 132 const char [] itoa = itoa!(n/10L) ~ decimaldigit!(n%10L); 133 } 134 135 136 137 13 138 14 139 // symboles for is(Type == Type) tests … … 68 193 69 194 template Val(real r){Value!(r) Val;} 70 struct Value(real r) { private alias Defined DefP; private alias CVal Op; static real get(){return r;} mixin Operate!(typeof(*this)); } 71 struct DefinedT(alias _r) { private alias Defined DefP; private alias Term Op; static real get(){return r;} alias _r r; mixin Operate!(typeof(*this)); } 72 struct UnDefinedT(alias _r) { private alias UnDefined DefP; private alias Term Op; static void set(real v){r = v;} alias _r r; mixin Operate!(typeof(*this)); } 73 74 struct OpAdd (T, U) { private alias Defined DefP; private alias Add Op; static real get(){ return T.get + U.get; } mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; } 75 struct OpSub (T, U) { private alias Defined DefP; private alias Sub Op; static real get(){ return T.get - U.get; } mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; } 76 struct OpMul (T, U) { private alias Defined DefP; private alias Mul Op; static real get(){ return T.get * U.get; } mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; } 77 struct OpDiv (T, U) { private alias Defined DefP; private alias Div Op; static real get(){ return T.get / U.get; } mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; } 78 79 struct OpAddA (T, U) { private alias UnDefined DefP; private alias AddA Op; static void set(real v){ U.set = v + T.get; } mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; } 80 struct OpSubA (T, U) { private alias UnDefined DefP; private alias SubA Op; static void set(real v){ U.set = v - T.get; } mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; } 81 struct OpSubAR(T, U) { private alias UnDefined DefP; private alias SubAR Op; static void set(real v){ U.set = T.get - v; } mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; } 82 struct OpMulA (T, U) { private alias UnDefined DefP; private alias MulA Op; static void set(real v){ U.set = v * T.get; } mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; } 83 struct OpDivA (T, U) { private alias UnDefined DefP; private alias DivA Op; static void set(real v){ U.set = v / T.get; } mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; } 84 struct OpDivAR(T, U) { private alias UnDefined DefP; private alias DivAR Op; static void set(real v){ U.set = T.get / v; } mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; } 85 86 87 real a, b, c, d; 88 89 void main(){} 90 91 unittest 195 struct Value(real r) 196 { 197 private alias Defined DefP; private alias CVal Op; 198 static real get(){return r;} 199 mixin Operate!(typeof(*this)); 200 const char[] LispOf = fcvt!(r); 201 } 202 struct DefinedT(alias _r) 203 { 204 private alias Defined DefP; private alias Term Op; 205 static real get(){return r;} 206 alias _r r; mixin Operate!(typeof(*this)); 207 const char[] LispOf = _r.stringof; 208 } 209 struct UnDefinedT(alias _r) 210 { 211 private alias UnDefined DefP; private alias Term Op; 212 static void set(real v){r = v;} 213 alias _r r; mixin Operate!(typeof(*this)); 214 const char[] LispOf = _r.stringof; 215 } 216 217 struct OpAdd (T, U) 218 { 219 private alias Defined DefP; private alias Add Op; 220 static real get(){ return T.get + U.get; } 221 mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; 222 const char[] LispOf = "(+ "~LHS.LispOf~" "~RHS.LispOf~")"; 223 } 224 struct OpSub (T, U) 225 { 226 private alias Defined DefP; private alias Sub Op; 227 static real get(){ return T.get - U.get; } 228 mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; 229 const char[] LispOf = "(- "~LHS.LispOf~" "~RHS.LispOf~")"; 230 } 231 struct OpMul (T, U) 232 { 233 private alias Defined DefP; private alias Mul Op; 234 static real get(){ return T.get * U.get; } 235 mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; 236 const char[] LispOf = "(* "~LHS.LispOf~" "~RHS.LispOf~")"; 237 } 238 struct OpDiv (T, U) 239 { 240 private alias Defined DefP; private alias Div Op; 241 static real get(){ return T.get / U.get; } 242 mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; 243 const char[] LispOf = "(/ "~LHS.LispOf~" "~RHS.LispOf~")"; 244 } 245 246 struct OpAddA (T, U) 247 { 248 private alias UnDefined DefP; private alias AddA Op; 249 static void set(real v){ U.set = v + T.get; } 250 mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; 251 const char[] LispOf = "(+> "~LHS.LispOf~" "~RHS.LispOf~")"; 252 } 253 struct OpSubA (T, U) 254 { 255 private alias UnDefined DefP; private alias SubA Op; 256 static void set(real v){ U.set = v - T.get; } 257 mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; 258 const char[] LispOf = "(-> "~LHS.LispOf~" "~RHS.LispOf~")"; 259 } 260 struct OpSubAR(T, U) 261 { 262 private alias UnDefined DefP; private alias SubAR Op; 263 static void set(real v){ U.set = T.get - v; } 264 mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; 265 const char[] LispOf = "(-R> "~LHS.LispOf~" "~RHS.LispOf~")"; 266 } 267 struct OpMulA (T, U) 268 { 269 private alias UnDefined DefP; private alias MulA Op; 270 static void set(real v){ U.set = v * T.get; } 271 mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; 272 const char[] LispOf = "(*> "~LHS.LispOf~" "~RHS.LispOf~")"; 273 } 274 struct OpDivA (T, U) 275 { 276 private alias UnDefined DefP; private alias DivA Op; 277 static void set(real v){ U.set = v / T.get; } 278 mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; 279 const char[] LispOf = "(/> "~LHS.LispOf~" "~RHS.LispOf~")"; 280 } 281 struct OpDivAR(T, U) 282 { 283 private alias UnDefined DefP; private alias DivAR Op; 284 static void set(real v){ U.set = T.get / v; } 285 mixin Operate!(typeof(*this)); alias T LHS; alias U RHS; 286 const char[] LispOf = "(/R> "~LHS.LispOf~" "~RHS.LispOf~")"; 287 } 288 289 290 real a, b, c, d, e, f, g; 291 292 void main(){Unittest();} 293 294 295 //unittest 296 void Unittest() 92 297 { 93 298 DefinedT!(a) A; 299 UnDefinedT!(b) B; 94 300 DefinedT!(c) C; 95 301 DefinedT!(d) D; 96 UnDefinedT!(b) B; 302 DefinedT!(e) E; 303 DefinedT!(f) F; 304 DefinedT!(g) G; 97 305 98 306 a=1; … … 134 342 writef("%s == -18\n", b); 135 343 344 (B * A) + E = (B * C) + D; 345 (B / A) + E = (B * C) + D; 346 // (B * A) + E = (B / C) + D; 347 136 348 (B * A) = (B * C) + D; // B * 3 = B * 2 + 3; -> 3 137 349 writef("%s == 3\n", b); 138 139 140 } 350 // (B / A) = (B * C) + D; 351 // (B * A) = (B / C) + D; 352 353 // (B * A) + E = (B * C); 354 // (B / A) + E = (B * C); 355 // (B * A) + E = (B / C); 356 357 (B * A) = (B * C); 358 // (B / A) = (B * C); 359 // (B * A) = (B / C); 360 } trunk/backmath/gen_code_for_template.lisp
r173 r174 5 5 ;;; load rule set 6 6 (load "meta.lisp") 7 8 ;;;;;;;;;;; set this to true to make backmath emit compile time debuggin info 9 (DEFCONSTANT verbose nil) 7 10 8 11 ;; Convert (OP (rules...)) into a text implementation … … 19 22 "{" nl 20 23 (Test_op_and_build opis sorted) 21 " static assert(false, `inavlid type used for " (op_name opis) ": T == ` ~~ T.stringof ~~ ` and V == `~~ V.stringof );" nl 24 " {}" nl 25 " static if(!is(TypeOf" (op_name opis) "))" nl 26 " static assert(false, `invalid types used for " (op_name opis) ": (" (op_symb opis) " ` ~~ T.LispOf ~~ ` `~~ V.LispOf ~~ `)` );" nl 27 (if verbose 28 (concatenate 29 'string 30 " else" nl 31 " pragma(msg, `>> " (op_name opis) ": (" (op_symb opis) " ` ~~ T.LispOf ~~ ` `~~ V.LispOf ~~ `)" 32 " => `" 33 " ~~ TypeOf" (op_name opis) ".LispOf);" nl 34 ) 35 "" 36 ) 22 37 "}" nl 23 38 ) trunk/backmath/generate_case.lisp
r173 r174 10 10 ; (print (list 'type_K type)) 11 11 ; (if (atom type) t (print (list 'type_K 'op (car type)))) 12 (if 13 (atom type) 14 (concatenate 'string "is(" root ".DefP == Defined)") 15 (concatenate 'string 16 (Test_Know_Type_Is (concatenate 'string root ".LHS") (cadr type)) 17 " && " 18 (let ((op (car type))) 19 (cond 20 ( 21 (or 22 (equal op '+) 23 (equal op '-) 24 (equal op '*) 25 (equal op '/) 12 13 (concatenate 'string 14 (if (listp type) 15 (concatenate 'string "is(" root ".Op == " (Op_name (car type)) ") && ") 16 "" 17 ) 18 (if 19 (atom type) 20 (concatenate 'string "is(" root ".DefP == Defined)") 21 (concatenate 'string 22 (Test_Know_Type_Is (concatenate 'string root ".LHS") (cadr type)) 23 " && " 24 (let ((op (car type))) 25 (cond 26 ( 27 (or 28 (equal op '+) 29 (equal op '-) 30 (equal op '*) 31 (equal op '/) 32 ) 33 (Test_Know_Type_Is (concatenate 'string root ".RHS") (caddr type)) 26 34 ) 27 (Test_Know_Type_Is (concatenate 'string root ".RHS") (caddr type)) 35 ( 36 (or 37 (equal op '+>) 38 (equal op '->) 39 (equal op '*>) 40 (equal op '/>) 41 (equal op '-r>) 42 (equal op '/r>) 43 ) 44 (Test_UnKnow_Type_Is (concatenate 'string root ".RHS") (caddr type)) 45 ) 46 ( t (format nil "%%UnKnown(~s)%%" type)) 28 47 ) 29 (30 (or31 (equal op '+>)32 (equal op '->)33 (equal op '*>)34 (equal op '/>)35 (equal op '-r>)36 (equal op '/r>)37 )38 (Test_UnKnow_Type_Is (concatenate 'string root ".RHS") (caddr type))39 )40 ( t (format nil "%%UnKnown(~s)%%" type))41 48 ) 42 49 ) … … 57 64 ; (print (list 'type_U type)) 58 65 ; (if (atom type) t (print (list 'type_U 'op (car type)))) 59 (if 60 (atom type) 61 (concatenate 'string "is(" root ".DefP == UnDefined)") 62 (concatenate 'string 63 (Test_Know_Type_Is (concatenate 'string root ".LHS") (cadr type)) 64 " && " 65 (let ((op (car type))) 66 (cond 67 ( 68 (or 69 (equal op '+) 70 (equal op '-) 71 (equal op '*) 72 (equal op '/) 66 67 (concatenate 'string 68 (if (listp type) 69 (concatenate 'string "is(" root ".Op == " (Op_name (car type)) ") && ") 70 "" 71 ) 72 (if 73 (atom type) 74 (concatenate 'string "is(" root ".DefP == UnDefined)") 75 (concatenate 'string 76 (Test_Know_Type_Is (concatenate 'string root ".LHS") (cadr type)) 77 " && " 78 (let ((op (car type))) 79 (cond 80 ( 81 (or 82 (equal op '+) 83 (equal op '-) 84 (equal op '*) 85 (equal op '/) 86 ) 87 (Test_Know_Type_Is (concatenate 'string root ".RHS") (caddr type)) 73 88 ) 74 (Test_Know_Type_Is (concatenate 'string root ".RHS") (caddr type)) 89 ( 90 (or 91 (equal op '+>) 92 (equal op '->) 93 (equal op '*>) 94 (equal op '/>) 95 (equal op '-r>) 96 (equal op '/r>) 97 ) 98 (Test_UnKnow_Type_Is (concatenate 'string root ".RHS") (caddr type)) 99 ) 100 ( t (format nil "%%UnKnown(~s)%%" type)) 75 101 ) 76 (77 (or78 (equal op '+>)79 (equal op '->)80 (equal op '*>)81 (equal op '/>)82 (equal op '-r>)83 (equal op '/r>)84 )85 (Test_UnKnow_Type_Is (concatenate 'string root ".RHS") (caddr type))86 )87 ( t "%%UnKnown%%")88 102 ) 89 103 ) trunk/backmath/generated_rules.d
r173 r174 1 1 template TypeOfAdd(T, V) 2 2 { 3 static if( // (+ (/R> H X) (/R> E X)) -> (/R> (+ H E) X) 4 is(T.Op == DivAR) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 5 is(V.Op == DivAR) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 6 && is(T.RHS == V.RHS) 7 ) 8 alias OpDivAR!(OpAdd!(T.LHS, V.LHS), T.RHS) TypeOfAdd; 9 else 3 10 static if( // (+ (/> A B) (/> C B)) -> (/> (+ A C) B) 4 11 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && … … 9 16 else 10 17 static if( // (+ (/> A (-> B X)) C) -> (/> A (-> (+ (/ C A) B) X)) 11 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&18 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 12 19 is(V.DefP == Defined) 13 20 /+ no repeats +/ … … 16 23 else 17 24 static if( // (+ (/> K (-> H X)) X) -> (/> (+ K 1) (-> (/ (* H K) (+ K 1)) X)) 18 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&25 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 19 26 is(V.DefP == UnDefined) 20 27 && is(T.RHS.RHS == V) … … 22 29 alias OpDivA!(OpAdd!(T.LHS, Value!(1)), OpSubA!(OpDiv!(OpMul!(T.RHS.LHS, T.LHS), OpAdd!(T.LHS, Value!(1))), T.RHS.RHS)) TypeOfAdd; 23 30 else 31 static if( // (+ (/> A (+> B X)) C) -> (/> A (+> (- B (/ C A)) X)) 32 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 33 is(V.DefP == Defined) 34 /+ no repeats +/ 35 ) 36 alias OpDivA!(T.LHS, OpAddA!(OpSub!(T.RHS.LHS, OpDiv!(V, T.LHS)), T.RHS.RHS)) TypeOfAdd; 37 else 38 static if( // (+ (/> K (+> H X)) X) -> (/> (+ K 1) (+> (/ (* H K) (+ K 1)) X)) 39 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 40 is(V.DefP == UnDefined) 41 && is(T.RHS.RHS == V) 42 ) 43 alias OpDivA!(OpAdd!(T.LHS, Value!(1)), OpAddA!(OpDiv!(OpMul!(T.RHS.LHS, T.LHS), OpAdd!(T.LHS, Value!(1))), T.RHS.RHS)) TypeOfAdd; 44 else 45 static if( // (+ (*> A (+> B X)) C) -> (*> A (+> (- B (* C A)) X)) 46 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 47 is(V.DefP == Defined) 48 /+ no repeats +/ 49 ) 50 alias OpMulA!(T.LHS, OpAddA!(OpSub!(T.RHS.LHS, OpMul!(V, T.LHS)), T.RHS.RHS)) TypeOfAdd; 51 else 52 static if( // (+ (*> K (+> H X)) X) -> (/> (+ (/ 1 K) 1) (+> (/ (/ H K) (+ (/ 1 K) 1)) X)) 53 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 54 is(V.DefP == UnDefined) 55 && is(T.RHS.RHS == V) 56 ) 57 alias OpDivA!(OpAdd!(OpDiv!(Value!(1), T.LHS), Value!(1)), OpAddA!(OpDiv!(OpDiv!(T.RHS.LHS, T.LHS), OpAdd!(OpDiv!(Value!(1), T.LHS), Value!(1))), T.RHS.RHS)) TypeOfAdd; 58 else 59 static if( // (+ C (/> A (-R> B X))) -> (/> A (-R> (+ B (/ C A)) X)) 60 is(T.DefP == Defined) && 61 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubAR) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 62 /+ no repeats +/ 63 ) 64 alias OpDivA!(V.LHS, OpSubAR!(OpAdd!(V.RHS.LHS, OpDiv!(T, V.LHS)), V.RHS.RHS)) TypeOfAdd; 65 else 66 static if( // (+ C (/> A (+> B X))) -> (/> A (+> (- B (/ C A)) X)) 67 is(T.DefP == Defined) && 68 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == AddA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 69 /+ no repeats +/ 70 ) 71 alias OpDivA!(V.LHS, OpAddA!(OpSub!(V.RHS.LHS, OpDiv!(T, V.LHS)), V.RHS.RHS)) TypeOfAdd; 72 else 73 static if( // (+ C (/> A (-> B X))) -> (/> A (-> (+ (/ C A) B) X)) 74 is(T.DefP == Defined) && 75 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 76 /+ no repeats +/ 77 ) 78 alias OpDivA!(V.LHS, OpSubA!(OpAdd!(OpDiv!(T, V.LHS), V.RHS.LHS), V.RHS.RHS)) TypeOfAdd; 79 else 80 static if( // (+ A (/> B X)) -> (/> B (-> (/ A B) X)) 81 is(T.DefP == Defined) && 82 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 83 /+ no repeats +/ 84 ) 85 alias OpDivA!(V.LHS, OpSubA!(OpDiv!(T, V.LHS), V.RHS)) TypeOfAdd; 86 else 87 static if( // (+ X (/> E X)) -> (/> (+ 1 E) X) 88 is(T.DefP == UnDefined) && 89 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 90 && is(T == V.RHS) 91 ) 92 alias OpDivA!(OpAdd!(Value!(1), V.LHS), T) TypeOfAdd; 93 else 24 94 static if( // (+ C (*> A (-R> B X))) -> (*> A (-R> (+ B (* C A)) X)) 25 95 is(T.DefP == Defined) && 26 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)96 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubAR) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 27 97 /+ no repeats +/ 28 98 ) … … 31 101 static if( // (+ C (*> A (+> B X))) -> (*> A (+> (- B (* C A)) X)) 32 102 is(T.DefP == Defined) && 33 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)103 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == AddA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 34 104 /+ no repeats +/ 35 105 ) … … 38 108 static if( // (+ C (*> A (-> B X))) -> (*> A (-> (+ (* C A) B) X)) 39 109 is(T.DefP == Defined) && 40 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)110 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 41 111 /+ no repeats +/ 42 112 ) … … 57 127 alias OpDivA!(OpAdd!(OpDiv!(Value!(1), V.LHS), Value!(1)), T) TypeOfAdd; 58 128 else 59 static if( // (+ C (/> A (-R> B X))) -> (/> A (-R> (+ B (/ C A)) X)) 60 is(T.DefP == Defined) && 61 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 62 /+ no repeats +/ 63 ) 64 alias OpDivA!(V.LHS, OpSubAR!(OpAdd!(V.RHS.LHS, OpDiv!(T, V.LHS)), V.RHS.RHS)) TypeOfAdd; 65 else 66 static if( // (+ C (/> A (+> B X))) -> (/> A (+> (- B (/ C A)) X)) 67 is(T.DefP == Defined) && 68 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 69 /+ no repeats +/ 70 ) 71 alias OpDivA!(V.LHS, OpAddA!(OpSub!(V.RHS.LHS, OpDiv!(T, V.LHS)), V.RHS.RHS)) TypeOfAdd; 72 else 73 static if( // (+ C (/> A (-> B X))) -> (/> A (-> (+ (/ C A) B) X)) 74 is(T.DefP == Defined) && 75 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 76 /+ no repeats +/ 77 ) 78 alias OpDivA!(V.LHS, OpSubA!(OpAdd!(OpDiv!(T, V.LHS), V.RHS.LHS), V.RHS.RHS)) TypeOfAdd; 79 else 80 static if( // (+ A (/> B X)) -> (/> B (-> (/ A B) X)) 81 is(T.DefP == Defined) && 82 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 83 /+ no repeats +/ 84 ) 85 alias OpDivA!(V.LHS, OpSubA!(OpDiv!(T, V.LHS), V.RHS)) TypeOfAdd; 86 else 87 static if( // (+ X (/> E X)) -> (/> (+ 1 E) X) 88 is(T.DefP == UnDefined) && 89 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 129 static if( // (+ A (-> B X)) -> (-> (+ A B) X) 130 is(T.DefP == Defined) && 131 is(V.Op == SubA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 132 /+ no repeats +/ 133 ) 134 alias OpSubA!(OpAdd!(T, V.LHS), V.RHS) TypeOfAdd; 135 else 136 static if( // (+ X (-> E X)) -> (/> 2 (-> (/ E 2) X)) 137 is(T.DefP == UnDefined) && 138 is(V.Op == SubA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 90 139 && is(T == V.RHS) 91 140 ) 92 alias OpDivA!( OpAdd!(Value!(1), V.LHS), T) TypeOfAdd;141 alias OpDivA!(Value!(2), OpSubA!(OpDiv!(V.LHS, Value!(2)), T)) TypeOfAdd; 93 142 else 94 143 static if( // (+ A (+> B X)) -> (+> (- B A) X) … … 106 155 alias OpDivA!(Value!(2), OpAddA!(OpDiv!(V.LHS, Value!(2)), T)) TypeOfAdd; 107 156 else 108 static if( // (+ A (-> B X)) -> (-> (+ A B) X) 109 is(T.DefP == Defined) && 110 is(V.Op == SubA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 111 /+ no repeats +/ 112 ) 113 alias OpSubA!(OpAdd!(T, V.LHS), V.RHS) TypeOfAdd; 114 else 115 static if( // (+ X (-> E X)) -> (/> 2 (-> (/ E 2) X)) 116 is(T.DefP == UnDefined) && 117 is(V.Op == SubA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 118 && is(T == V.RHS) 119 ) 120 alias OpDivA!(Value!(2), OpSubA!(OpDiv!(V.LHS, Value!(2)), T)) TypeOfAdd; 157 static if( // (+ (/> A (-R> B X)) C) -> (/> A (-R> (+ B (/ C A)) X)) 158 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubAR) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 159 is(V.DefP == Defined) 160 /+ no repeats +/ 161 ) 162 alias OpDivA!(T.LHS, OpSubAR!(OpAdd!(T.RHS.LHS, OpDiv!(V, T.LHS)), T.RHS.RHS)) TypeOfAdd; 163 else 164 static if( // (+ (/> B X) A) -> (/> B (-> (/ A B) X)) 165 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 166 is(V.DefP == Defined) 167 /+ no repeats +/ 168 ) 169 alias OpDivA!(T.LHS, OpSubA!(OpDiv!(V, T.LHS), T.RHS)) TypeOfAdd; 170 else 171 static if( // (+ (/> H X) X) -> (/> (+ H 1) X) 172 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 173 is(V.DefP == UnDefined) 174 && is(T.RHS == V) 175 ) 176 alias OpDivA!(OpAdd!(T.LHS, Value!(1)), T.RHS) TypeOfAdd; 121 177 else 122 178 static if( // (+ (*> A (-R> B X)) C) -> (*> A (-R> (+ B (* C A)) X)) 123 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&179 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubAR) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 124 180 is(V.DefP == Defined) 125 181 /+ no repeats +/ … … 127 183 alias OpMulA!(T.LHS, OpSubAR!(OpAdd!(T.RHS.LHS, OpMul!(V, T.LHS)), T.RHS.RHS)) TypeOfAdd; 128 184 else 129 static if( // (+ (*> A (+> B X)) C) -> (*> A (+> (- B (* C A)) X))130 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&131 is(V.DefP == Defined)132 /+ no repeats +/133 )134 alias OpMulA!(T.LHS, OpAddA!(OpSub!(T.RHS.LHS, OpMul!(V, T.LHS)), T.RHS.RHS)) TypeOfAdd;135 else136 185 static if( // (+ (*> A (-> B X)) C) -> (*> A (-> (+ (* C A) B) X)) 137 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&186 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 138 187 is(V.DefP == Defined) 139 188 /+ no repeats +/ … … 155 204 alias OpDivA!(OpAdd!(OpDiv!(Value!(1), T.LHS), Value!(1)), T.RHS) TypeOfAdd; 156 205 else 157 static if( // (+ (/> A (-R> B X)) C) -> (/> A (-R> (+ B (/ C A)) X)) 158 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 159 is(V.DefP == Defined) 160 /+ no repeats +/ 161 ) 162 alias OpDivA!(T.LHS, OpSubAR!(OpAdd!(T.RHS.LHS, OpDiv!(V, T.LHS)), T.RHS.RHS)) TypeOfAdd; 163 else 164 static if( // (+ (/> A (+> B X)) C) -> (/> A (+> (- B (/ C A)) X)) 165 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 166 is(V.DefP == Defined) 167 /+ no repeats +/ 168 ) 169 alias OpDivA!(T.LHS, OpAddA!(OpSub!(T.RHS.LHS, OpDiv!(V, T.LHS)), T.RHS.RHS)) TypeOfAdd; 170 else 171 static if( // (+ (/> B X) A) -> (/> B (-> (/ A B) X)) 172 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 173 is(V.DefP == Defined) 174 /+ no repeats +/ 175 ) 176 alias OpDivA!(T.LHS, OpSubA!(OpDiv!(V, T.LHS), T.RHS)) TypeOfAdd; 177 else 178 static if( // (+ (/> H X) X) -> (/> (+ H 1) X) 179 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 206 static if( // (+ (-> B X) A) -> (-> (+ A B) X) 207 is(T.Op == SubA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 208 is(V.DefP == Defined) 209 /+ no repeats +/ 210 ) 211 alias OpSubA!(OpAdd!(V, T.LHS), T.RHS) TypeOfAdd; 212 else 213 static if( // (+ (-> H X) X) -> (/> 2 (-> (/ H 2) X)) 214 is(T.Op == SubA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 180 215 is(V.DefP == UnDefined) 181 216 && is(T.RHS == V) 182 217 ) 183 alias OpDivA!( OpAdd!(T.LHS, Value!(1)), T.RHS) TypeOfAdd;218 alias OpDivA!(Value!(2), OpSubA!(OpDiv!(T.LHS, Value!(2)), T.RHS)) TypeOfAdd; 184 219 else 185 220 static if( // (+ (+> B X) A) -> (+> (- B A) X) … … 197 232 alias OpDivA!(Value!(2), OpAddA!(OpDiv!(T.LHS, Value!(2)), T.RHS)) TypeOfAdd; 198 233 else 199 static if( // (+ (-> B X) A) -> (-> (+ A B) X)200 is(T.Op == SubA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) &&201 is(V.DefP == Defined)202 /+ no repeats +/203 )204 alias OpSubA!(OpAdd!(V, T.LHS), T.RHS) TypeOfAdd;205 else206 static if( // (+ (-> H X) X) -> (/> 2 (-> (/ H 2) X))207 is(T.Op == SubA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) &&208 is(V.DefP == UnDefined)209 && is(T.RHS == V)210 )211 alias OpDivA!(Value!(2), OpSubA!(OpDiv!(T.LHS, Value!(2)), T.RHS)) TypeOfAdd;212 else213 234 static if( // (+ (-R> B X) A) -> (-R> (+ A B) X) 214 235 is(T.Op == SubAR) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && … … 253 274 alias OpDivA!(Value!(2), T) TypeOfAdd; 254 275 else 255 static assert(false, `inavlid type used for Add: T == ` ~ T.stringof ~ ` and V == `~ V.stringof ); 276 {} 277 static if(!is(TypeOfAdd)) 278 static assert(false, `invalid types used for Add: (+ ` ~ T.LispOf ~ ` `~ V.LispOf ~ `)` ); 256 279 } 257 280 template TypeOfSub(T, V) 258 281 { 282 static if( // (- (*> H X) (*> A (-> B X))) -> (+> (/ B A) (/> (- (/ 1 H) (/ 1 A)) X)) 283 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 284 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 285 && is(T.RHS == V.RHS.RHS) 286 ) 287 alias OpAddA!(OpDiv!(V.RHS.LHS, V.LHS), OpDivA!(OpSub!(OpDiv!(Value!(1), T.LHS), OpDiv!(Value!(1), V.LHS)), T.RHS)) TypeOfSub; 288 else 289 static if( // (- (/> K (-> H X)) (/> F (-> E X))) -> (/> (- K F) (-> (/ (- (* H K) (* E F)) (- K F)) X)) 290 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 291 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 292 && is(T.RHS.RHS == V.RHS.RHS) 293 ) 294 alias OpDivA!(OpSub!(T.LHS, V.LHS), OpSubA!(OpDiv!(OpSub!(OpMul!(T.RHS.LHS, T.LHS), OpMul!(V.RHS.LHS, V.LHS)), OpSub!(T.LHS, V.LHS)), T.RHS.RHS)) TypeOfSub; 295 else 296 static if( // (- (*> A (-> E B)) (/> C (-> D B))) -> (/> (- (/ 1 A) C) (-> (/ (- (/ E A) (* D C)) (- (/ 1 A) C)) B)) 297 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 298 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 299 && is(T.RHS.RHS == V.RHS.RHS) 300 ) 301 alias OpDivA!(OpSub!(OpDiv!(Value!(1), T.LHS), V.LHS), OpSubA!(OpDiv!(OpSub!(OpDiv!(T.RHS.LHS, T.LHS), OpMul!(V.RHS.LHS, V.LHS)), OpSub!(OpDiv!(Value!(1), T.LHS), V.LHS)), T.RHS.RHS)) TypeOfSub; 302 else 303 static if( // (- (/> H X) (/> F (-> E X))) -> (/> (- H F) (+> (/ (* E F) (- H F)) X)) 304 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 305 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 306 && is(T.RHS == V.RHS.RHS) 307 ) 308 alias OpDivA!(OpSub!(T.LHS, V.LHS), OpAddA!(OpDiv!(OpMul!(V.RHS.LHS, V.LHS), OpSub!(T.LHS, V.LHS)), T.RHS)) TypeOfSub; 309 else 310 static if( // (- (/R> A B) (/R> C B)) -> (/R> (- A C) B) 311 is(T.Op == DivAR) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 312 is(V.Op == DivAR) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 313 && is(T.RHS == V.RHS) 314 ) 315 alias OpDivAR!(OpSub!(T.LHS, V.LHS), T.RHS) TypeOfSub; 316 else 317 static if( // (- (/> A B) (/> C B)) -> (/> (- A C) B) 318 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 319 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 320 && is(T.RHS == V.RHS) 321 ) 322 alias OpDivA!(OpSub!(T.LHS, V.LHS), T.RHS) TypeOfSub; 323 else 259 324 static if( // (- A (-R> B X)) -> (+> (- B A) X) 260 325 is(T.DefP == Defined) && … … 271 336 alias OpDivA!(Value!(2), OpAddA!(OpDiv!(V.LHS, Value!(2)), T)) TypeOfSub; 272 337 else 338 static if( // (- C (/> A (-R> B X))) -> (/> A (+> (- B (/ C A)) X)) 339 is(T.DefP == Defined) && 340 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubAR) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 341 /+ no repeats +/ 342 ) 343 alias OpDivA!(V.LHS, OpAddA!(OpSub!(V.RHS.LHS, OpDiv!(T, V.LHS)), V.RHS.RHS)) TypeOfSub; 344 else 345 static if( // (- C (/> A (+> B X))) -> (/> A (-R> (+ (/ C A) B) X)) 346 is(T.DefP == Defined) && 347 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == AddA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 348 /+ no repeats +/ 349 ) 350 alias OpDivA!(V.LHS, OpSubAR!(OpAdd!(OpDiv!(T, V.LHS), V.RHS.LHS), V.RHS.RHS)) TypeOfSub; 351 else 352 static if( // (- C (/> A (-> B X))) -> (/> A (-R> (- (/ C A) B) X)) 353 is(T.DefP == Defined) && 354 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 355 /+ no repeats +/ 356 ) 357 alias OpDivA!(V.LHS, OpSubAR!(OpSub!(OpDiv!(T, V.LHS), V.RHS.LHS), V.RHS.RHS)) TypeOfSub; 358 else 359 static if( // (- A (/> B X)) -> (/> B (-R> (/ A B) X)) 360 is(T.DefP == Defined) && 361 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 362 /+ no repeats +/ 363 ) 364 alias OpDivA!(V.LHS, OpSubAR!(OpDiv!(T, V.LHS), V.RHS)) TypeOfSub; 365 else 366 static if( // (- X (/> E X)) -> (/> (- 1 E) X) 367 is(T.DefP == UnDefined) && 368 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined) 369 && is(T == V.RHS) 370 ) 371 alias OpDivA!(OpSub!(Value!(1), V.LHS), T) TypeOfSub; 372 else 273 373 static if( // (- C (*> A (-R> B X))) -> (*> A (+> (- B (* C A)) X)) 274 374 is(T.DefP == Defined) && 275 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)375 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubAR) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 276 376 /+ no repeats +/ 277 377 ) … … 280 380 static if( // (- C (*> A (+> B X))) -> (*> A (-R> (+ (* C A) B) X)) 281 381 is(T.DefP == Defined) && 282 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)382 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == AddA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 283 383 /+ no repeats +/ 284 384 ) … … 287 387 static if( // (- C (*> A (-> B X))) -> (*> A (-R> (- (* A C) B) X)) 288 388 is(T.DefP == Defined) && 289 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)389 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 290 390 /+ no repeats +/ 291 391 ) … … 306 406 alias OpDivA!(OpSub!(Value!(1), OpDiv!(Value!(1), V.LHS)), T) TypeOfSub; 307 407 else 308 static if( // (- C (/> A (-R> B X))) -> (/> A (+> (- B (/ C A)) X))309 is(T.DefP == Defined) &&310 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)311 /+ no repeats +/312 )313 alias OpDivA!(V.LHS, OpAddA!(OpSub!(V.RHS.LHS, OpDiv!(T, V.LHS)), V.RHS.RHS)) TypeOfSub;314 else315 static if( // (- C (/> A (+> B X))) -> (/> A (-R> (+ (/ C A) B) X))316 is(T.DefP == Defined) &&317 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)318 /+ no repeats +/319 )320 alias OpDivA!(V.LHS, OpSubAR!(OpAdd!(OpDiv!(T, V.LHS), V.RHS.LHS), V.RHS.RHS)) TypeOfSub;321 else322 static if( // (- C (/> A (-> B X))) -> (/> A (-R> (- (/ C A) B) X))323 is(T.DefP == Defined) &&324 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)325 /+ no repeats +/326 )327 alias OpDivA!(V.LHS, OpSubAR!(OpSub!(OpDiv!(T, V.LHS), V.RHS.LHS), V.RHS.RHS)) TypeOfSub;328 else329 static if( // (- A (/> B X)) -> (/> B (-R> (/ A B) X))330 is(T.DefP == Defined) &&331 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined)332 /+ no repeats +/333 )334 alias OpDivA!(V.LHS, OpSubAR!(OpDiv!(T, V.LHS), V.RHS)) TypeOfSub;335 else336 static if( // (- X (/> E X)) -> (/> (- 1 E) X)337 is(T.DefP == UnDefined) &&338 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.DefP == UnDefined)339 && is(T == V.RHS)340 )341 alias OpDivA!(OpSub!(Value!(1), V.LHS), T) TypeOfSub;342 else343 408 static if( // (- (-R> B X) A) -> (-R> (- B A) X) 344 409 is(T.Op == SubAR) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && … … 355 420 alias OpDivA!(Value!(2), OpSubAR!(OpDiv!(T.LHS, Value!(2)), T.RHS)) TypeOfSub; 356 421 else 422 static if( // (- (/> A (-R> B X)) C) -> (/> A (-R> (- B (/ C A)) X)) 423 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubAR) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 424 is(V.DefP == Defined) 425 /+ no repeats +/ 426 ) 427 alias OpDivA!(T.LHS, OpSubAR!(OpSub!(T.RHS.LHS, OpDiv!(V, T.LHS)), T.RHS.RHS)) TypeOfSub; 428 else 429 static if( // (- (/> A (+> B X)) C) -> (/> A (+> (+ (/ C A) B) X)) 430 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 431 is(V.DefP == Defined) 432 /+ no repeats +/ 433 ) 434 alias OpDivA!(T.LHS, OpAddA!(OpAdd!(OpDiv!(V, T.LHS), T.RHS.LHS), T.RHS.RHS)) TypeOfSub; 435 else 436 static if( // (- (/> A (-> B X)) C) -> (/> A (+> (- (/ C A) B) X)) 437 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 438 is(V.DefP == Defined) 439 /+ no repeats +/ 440 ) 441 alias OpDivA!(T.LHS, OpAddA!(OpSub!(OpDiv!(V, T.LHS), T.RHS.LHS), T.RHS.RHS)) TypeOfSub; 442 else 443 static if( // (- (/> B X) A) -> (/> B (+> (/ A B) X)) 444 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 445 is(V.DefP == Defined) 446 /+ no repeats +/ 447 ) 448 alias OpDivA!(T.LHS, OpAddA!(OpDiv!(V, T.LHS), T.RHS)) TypeOfSub; 449 else 450 static if( // (- (/> H X) X) -> (/> (- H 1) X) 451 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 452 is(V.DefP == UnDefined) 453 && is(T.RHS == V) 454 ) 455 alias OpDivA!(OpSub!(T.LHS, Value!(1)), T.RHS) TypeOfSub; 456 else 357 457 static if( // (- (*> A (-R> B X)) C) -> (*> A (-R> (- B (* C A)) X)) 358 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&458 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubAR) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 359 459 is(V.DefP == Defined) 360 460 /+ no repeats +/ … … 363 463 else 364 464 static if( // (- (*> A (+> B X)) C) -> (*> A (+> (+ (* C A) B) X)) 365 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&465 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 366 466 is(V.DefP == Defined) 367 467 /+ no repeats +/ … … 370 470 else 371 471 static if( // (- (*> A (-> B X)) C) -> (*> A (+> (- (* C A) B) X)) 372 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&472 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 373 473 is(V.DefP == Defined) 374 474 /+ no repeats +/ … … 390 490 alias OpDivA!(OpSub!(OpDiv!(Value!(1), T.LHS), Value!(1)), T.RHS) TypeOfSub; 391 491 else 392 static if( // (- (/> A (-R> B X)) C) -> (/> A (-R> (- B (/ C A)) X))393 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&394 is(V.DefP == Defined)395 /+ no repeats +/396 )397 alias OpDivA!(T.LHS, OpSubAR!(OpSub!(T.RHS.LHS, OpDiv!(V, T.LHS)), T.RHS.RHS)) TypeOfSub;398 else399 static if( // (- (/> A (+> B X)) C) -> (/> A (+> (+ (/ C A) B) X))400 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&401 is(V.DefP == Defined)402 /+ no repeats +/403 )404 alias OpDivA!(T.LHS, OpAddA!(OpAdd!(OpDiv!(V, T.LHS), T.RHS.LHS), T.RHS.RHS)) TypeOfSub;405 else406 static if( // (- (/> A (-> B X)) C) -> (/> A (+> (- (/ C A) B) X))407 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&408 is(V.DefP == Defined)409 /+ no repeats +/410 )411 alias OpDivA!(T.LHS, OpAddA!(OpSub!(OpDiv!(V, T.LHS), T.RHS.LHS), T.RHS.RHS)) TypeOfSub;412 else413 static if( // (- (/> B X) A) -> (/> B (+> (/ A B) X))414 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) &&415 is(V.DefP == Defined)416 /+ no repeats +/417 )418 alias OpDivA!(T.LHS, OpAddA!(OpDiv!(V, T.LHS), T.RHS)) TypeOfSub;419 else420 static if( // (- (/> H X) X) -> (/> (- H 1) X)421 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) &&422 is(V.DefP == UnDefined)423 && is(T.RHS == V)424 )425 alias OpDivA!(OpSub!(T.LHS, Value!(1)), T.RHS) TypeOfSub;426 else427 492 static if( // (- (+> B X) A) -> (+> (+ A B) X) 428 493 is(T.Op == AddA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && … … 474 539 alias OpAddA!(V, T) TypeOfSub; 475 540 else 476 static assert(false, `inavlid type used for Sub: T == ` ~ T.stringof ~ ` and V == `~ V.stringof ); 541 {} 542 static if(!is(TypeOfSub)) 543 static assert(false, `invalid types used for Sub: (- ` ~ T.LispOf ~ ` `~ V.LispOf ~ `)` ); 477 544 } 478 545 template TypeOfMul(T, V) 479 546 { 480 547 static if( // (* (/> A (-R> B X)) C) -> (/> (* A C) (-R> B X)) 481 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&548 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubAR) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 482 549 is(V.DefP == Defined) 483 550 /+ no repeats +/ … … 487 554 static if( // (* C (/> A (-R> B X))) -> (/> (* A C) (-R> B X)) 488 555 is(T.DefP == Defined) && 489 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)556 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubAR) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 490 557 /+ no repeats +/ 491 558 ) … … 493 560 else 494 561 static if( // (* (*> A (-R> B X)) C) -> (*> (/ A C) (-R> B X)) 495 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&562 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubAR) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 496 563 is(V.DefP == Defined) 497 564 /+ no repeats +/ … … 501 568 static if( // (* C (*> A (-R> B X))) -> (*> (/ A C) (-R> B X)) 502 569 is(T.DefP == Defined) && 503 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)570 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubAR) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 504 571 /+ no repeats +/ 505 572 ) … … 507 574 else 508 575 static if( // (* (/R> A (+> B X)) C) -> (/R> (* A C) (+> B X)) 509 is(T.Op == DivAR) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&576 is(T.Op == DivAR) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 510 577 is(V.DefP == Defined) 511 578 /+ no repeats +/ … … 515 582 static if( // (* C (/R> A (+> B X))) -> (/R> (* A C) (+> B X)) 516 583 is(T.DefP == Defined) && 517 is(V.Op == DivAR) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)584 is(V.Op == DivAR) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == AddA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 518 585 /+ no repeats +/ 519 586 ) … … 521 588 else 522 589 static if( // (* (/> A (+> B X)) C) -> (/> (* C A) (+> B X)) 523 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&590 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 524 591 is(V.DefP == Defined) 525 592 /+ no repeats +/ … … 529 596 static if( // (* C (/> A (+> B X))) -> (/> (* C A) (+> B X)) 530 597 is(T.DefP == Defined) && 531 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)598 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == AddA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 532 599 /+ no repeats +/ 533 600 ) … … 535 602 else 536 603 static if( // (* (*> A (+> B X)) C) -> (*> (/ A C) (+> B X)) 537 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&604 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 538 605 is(V.DefP == Defined) 539 606 /+ no repeats +/ … … 543 610 static if( // (* C (*> A (+> B X))) -> (*> (/ A C) (+> B X)) 544 611 is(T.DefP == Defined) && 545 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)612 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == AddA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 546 613 /+ no repeats +/ 547 614 ) … … 549 616 else 550 617 static if( // (* (/R> A (-> B X)) C) -> (/R> (* A C) (-> B X)) 551 is(T.Op == DivAR) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&618 is(T.Op == DivAR) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 552 619 is(V.DefP == Defined) 553 620 /+ no repeats +/ … … 557 624 static if( // (* C (/R> A (-> B X))) -> (/R> (* A C) (-> B X)) 558 625 is(T.DefP == Defined) && 559 is(V.Op == DivAR) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)626 is(V.Op == DivAR) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 560 627 /+ no repeats +/ 561 628 ) … … 563 630 else 564 631 static if( // (* (/> A (-> B X)) C) -> (/> (* C A) (-> B X)) 565 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&632 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 566 633 is(V.DefP == Defined) 567 634 /+ no repeats +/ … … 571 638 static if( // (* C (/> A (-> B X))) -> (/> (* C A) (-> B X)) 572 639 is(T.DefP == Defined) && 573 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)640 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 574 641 /+ no repeats +/ 575 642 ) … … 577 644 else 578 645 static if( // (* (*> A (-> B X)) C) -> (*> (/ A C) (-> B X)) 579 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&646 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 580 647 is(V.DefP == Defined) 581 648 /+ no repeats +/ … … 585 652 static if( // (* C (*> A (-> B X))) -> (*> (/ A C) (-> B X)) 586 653 is(T.DefP == Defined) && 587 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)654 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 588 655 /+ no repeats +/ 589 656 ) … … 681 748 alias OpDivA!(V, T) TypeOfMul; 682 749 else 683 static assert(false, `inavlid type used for Mul: T == ` ~ T.stringof ~ ` and V == `~ V.stringof ); 750 {} 751 static if(!is(TypeOfMul)) 752 static assert(false, `invalid types used for Mul: (* ` ~ T.LispOf ~ ` `~ V.LispOf ~ `)` ); 684 753 } 685 754 template TypeOfDiv(T, V) … … 692 761 alias OpMulA!(T.LHS, OpAddA!(T.LHS, T.RHS)) TypeOfDiv; 693 762 else 763 static if( // (/ (-> B X) A) -> (*> A (-> B X)) 764 is(T.Op == SubA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 765 is(V.DefP == Defined) 766 /+ no repeats +/ 767 ) 768 alias OpMulA!(V, OpSubA!(T.LHS, T.RHS)) TypeOfDiv; 769 else 770 static if( // (/ (-> H X) X) -> (-> 1 (/R> H X)) 771 is(T.Op == SubA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 772 is(V.DefP == UnDefined) 773 && is(T.RHS == V) 774 ) 775 alias OpSubA!(Value!(1), OpDivAR!(T.LHS, T.RHS)) TypeOfDiv; 776 else 694 777 static if( // (/ (+> B X) A) -> (*> A (+> B X)) 695 778 is(T.Op == AddA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && … … 706 789 alias OpSubAR!(Value!(1), OpDivAR!(T.LHS, T.RHS)) TypeOfDiv; 707 790 else 708 static if( // (/ (-> B X) A) -> (*> A (-> B X))709 is(T.Op == SubA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) &&710 is(V.DefP == Defined)711 /+ no repeats +/712 )713 alias OpMulA!(V, OpSubA!(T.LHS, T.RHS)) TypeOfDiv;714 else715 static if( // (/ (-> H X) X) -> (-> 1 (/R> H X))716 is(T.Op == SubA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) &&717 is(V.DefP == UnDefined)718 && is(T.RHS == V)719 )720 alias OpSubA!(Value!(1), OpDivAR!(T.LHS, T.RHS)) TypeOfDiv;721 else722 791 static if( // (/ (/> A (-R> B X)) C) -> (*> (/ C A) (-R> B X)) 723 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&792 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubAR) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 724 793 is(V.DefP == Defined) 725 794 /+ no repeats +/ … … 729 798 static if( // (/ C (/> A (-R> B X))) -> (/R> (/ C A) (-R> B X)) 730 799 is(T.DefP == Defined) && 731 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)800 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubAR) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 732 801 /+ no repeats +/ 733 802 ) … … 735 804 else 736 805 static if( // (/ (*> A (-R> B X)) C) -> (*> (* A C) (-R> B X)) 737 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&806 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubAR) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 738 807 is(V.DefP == Defined) 739 808 /+ no repeats +/ … … 743 812 static if( // (/ C (*> A (-R> B X))) -> (/R> (* A C) (-R> B X)) 744 813 is(T.DefP == Defined) && 745 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)814 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubAR) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 746 815 /+ no repeats +/ 747 816 ) … … 749 818 else 750 819 static if( // (/ (/R> A (+> B X)) C) -> (/R> (/ A C) (+> B X)) 751 is(T.Op == DivAR) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&820 is(T.Op == DivAR) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 752 821 is(V.DefP == Defined) 753 822 /+ no repeats +/ … … 757 826 static if( // (/ C (/R> A (+> B X))) -> (*> (/ A C) (+> B X)) 758 827 is(T.DefP == Defined) && 759 is(V.Op == DivAR) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)828 is(V.Op == DivAR) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == AddA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 760 829 /+ no repeats +/ 761 830 ) … … 763 832 else 764 833 static if( // (/ (/> A (+> B X)) C) -> (*> (/ C A) (+> B X)) 765 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&834 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 766 835 is(V.DefP == Defined) 767 836 /+ no repeats +/ … … 771 840 static if( // (/ C (/> A (+> B X))) -> (/R> (/ C A) (+> B X)) 772 841 is(T.DefP == Defined) && 773 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)842 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == AddA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 774 843 /+ no repeats +/ 775 844 ) … … 777 846 else 778 847 static if( // (/ (*> A (+> B X)) C) -> (*> (* C A) (+> B X)) 779 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&848 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == AddA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 780 849 is(V.DefP == Defined) 781 850 /+ no repeats +/ … … 785 854 static if( // (/ C (*> A (+> B X))) -> (/R> (* A C) (+> B X)) 786 855 is(T.DefP == Defined) && 787 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)856 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == AddA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 788 857 /+ no repeats +/ 789 858 ) … … 791 860 else 792 861 static if( // (/ (/R> A (-> B X)) C) -> (/R> (/ A C) (-> B X)) 793 is(T.Op == DivAR) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&862 is(T.Op == DivAR) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 794 863 is(V.DefP == Defined) 795 864 /+ no repeats +/ … … 799 868 static if( // (/ C (/R> A (-> B X))) -> (*> (/ A C) (-> B X)) 800 869 is(T.DefP == Defined) && 801 is(V.Op == DivAR) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)870 is(V.Op == DivAR) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 802 871 /+ no repeats +/ 803 872 ) … … 805 874 else 806 875 static if( // (/ (/> A (-> B X)) C) -> (*> (/ C A) (-> B X)) 807 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&876 is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 808 877 is(V.DefP == Defined) 809 878 /+ no repeats +/ … … 813 882 static if( // (/ C (/> A (-> B X))) -> (/R> (/ C A) (-> B X)) 814 883 is(T.DefP == Defined) && 815 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)884 is(V.Op == DivA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 816 885 /+ no repeats +/ 817 886 ) … … 819 888 else 820 889 static if( // (/ (*> A (-> B X)) C) -> (*> (* C A) (-> B X)) 821 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS. LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) &&890 is(T.Op == MulA) && is(T.LHS.DefP == Defined) && is(T.RHS.Op == SubA) && is(T.RHS.LHS.DefP == Defined) && is(T.RHS.RHS.DefP == UnDefined) && 822 891 is(V.DefP == Defined) 823 892 /+ no repeats +/ … … 827 896 static if( // (/ C (*> A (-> B X))) -> (/R> (* C A) (-> B X)) 828 897 is(T.DefP == Defined) && 829 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS. LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined)898 is(V.Op == MulA) && is(V.LHS.DefP == Defined) && is(V.RHS.Op == SubA) && is(V.RHS.LHS.DefP == Defined) && is(V.RHS.RHS.DefP == UnDefined) 830 899 /+ no repeats +/ 831 900 ) … … 909 978 alias OpMulA!(V, T) TypeOfDiv; 910 979 else 911 static assert(false, `inavlid type used for Div: T == ` ~ T.stringof ~ ` and V == `~ V.stringof ); 980 {} 981 static if(!is(TypeOfDiv)) 982 static assert(false, `invalid types used for Div: (/ ` ~ T.LispOf ~ ` `~ V.LispOf ~ `)` ); 912 983 } 913 984 trunk/backmath/meta.lisp
r173 r174 39 39 40 40 ;a 41 ((+ a b) (+ a b)) ; a42 ((- a b) (- a b)) ; a43 ((* a b) (* a b)) ; a44 ((/ a b) (/ a b)) ; a41 ((+ a b) (+ a b)) ; a 42 ((- a b) (- a b)) ; a 43 ((* a b) (* a b)) ; a 44 ((/ a b) (/ a b)) ; a 45 45 46 46 ;x 47 ((+ a x) (-> a x)) ; (-> a x)48 ((- a x) (-r> a x)) ; (-r> a x)49 ((* a x) (/> a x)) ; (/> a x)50 ((/ a x) (/r> a x)) ; (/r> a x)51 52 ((+ x a) (-> a x)) ; (-> a x)53 ((- x a) (+> a x)) ; (+> a x)54 ((* x a) (/> a x)) ; (/> a x)55 ((/ x a) (*> a x)) ; (*> a x)47 ((+ a x) (-> a x)) ; (-> a x) 48 ((- a x) (-r> a x)) ; (-r> a x) 49 ((* a x) (/> a x)) ; (/> a x) 50 ((/ a x) (/r> a x)) ; (/r> a x) 51 52 ((+ x a) (-> a x)) ; (-> a x) 53 ((- x a) (+> a x)) ; (+> a x) 54 ((* x a) (/> a x)) ; (/> a x) 55 ((/ x a) (*> a x)) ; (*> a x) 56 56 57 57 ;(-> b x) 58 ((+ a (-> b x)) (-> (+ a b) x)) ; (-> a x)59 ((- a (-> b x)) (-r> (- a b) x)) ; (-r> a x)60 ((* a (-> b x)) (/> a (-> b x))) ; (/> a (-> b x)))61 ((/ a (-> b x)) (/r> a (-> b x))) ; (/r> a (-> b x)))62 63 ((+ (-> b x) a) (-> (+ a b) x)) ; (-> a x)64 ((- (-> b x) a) (+> (- a b) x)) ; (+> a x)65 ((* (-> b x) a) (/> a (-> b x))) ; (/> a (-> b x)))66 ((/ (-> b x) a) (*> a (-> b x))) ; (*> a (-> b x)))58 ((+ a (-> b x)) (-> (+ a b) x)) ; (-> a x) 59 ((- a (-> b x)) (-r> (- a b) x)) ; (-r> a x) 60 ((* a (-> b x)) (/> a (-> b x))) ; (/> a (-> b x))) 61 ((/ a (-> b x)) (/r> a (-> b x))) ; (/r> a (-> b x))) 62 63 ((+ (-> b x) a) (-> (+ a b) x)) ; (-> a x) 64 ((- (-> b x) a) (+> (- a b) x)) ; (+> a x) 65 ((* (-> b x) a) (/> a (-> b x))) ; (/> a (-> b x))) 66 ((/ (-> b x) a) (*> a (-> b x))) ; (*> a (-> b x))) 67 67 68 68 ;(+> b x) 69 ((+ a (+> b x)) (+> (- b a) x)) ; (+> a x)70 ((- a (+> b x)) (-r> (+ a b) x)) ; (-r> a x)71 ((* a (+> b x)) (/> a (+> b x))) ; (/> a (+> b x)))72 ((/ a (+> b x)) (/r> a (+> b x))) ; (/r> a (+> b x)))73 74 ((+ (+> b x) a) (+> (- b a) x)) ; (+> a x)75 ((- (+> b x) a) (+> (+ a b) x)) ; (+> a x)76 ((* (+> b x) a) (/> a (+> b x))) ; (/> a (+> b x)))77 ((/ (+> b x) a) (*> a (+> b x))) ; (*> a (+> b x)))69 ((+ a (+> b x)) (+> (- b a) x)) ; (+> a x) 70 ((- a (+> b x)) (-r> (+ a b) x)) ; (-r> a x) 71 ((* a (+> b x)) (/> a (+> b x))) ; (/> a (+> b x))) 72 ((/ a (+> b x)) (/r> a (+> b x))) ; (/r> a (+> b x))) 73 74 ((+ (+> b x) a) (+> (- b a) x)) ; (+> a x) 75 ((- (+> b x) a) (+> (+ a b) x)) ; (+> a x) 76 ((* (+> b x) a) (/> a (+> b x))) ; (/> a (+> b x))) 77 ((/ (+> b x) a) (*> a (+> b x))) ; (*> a (+> b x))) 78 78 79 79 ;(/> b x) 80 ((+ a (/> b x)) (/> b (-> (/ a b) x))) ; (/> a (-> b x)))81 ((- a (/> b x)) (/> b (-r> (/ a b) x))) ; (/> a (-r> b x)))82 ((* a (/> b x)) (/> (* a b) x)) ; (/> a x)83 ((/ a (/> b x)) (/r> (/ a b) x)) ; (/r> a x)84 85 ((+ (/> b x) a) (/> b (-> (/ a b) x))) ; (/> a (-> b x)))86 ((- (/> b x) a) (/> b (+> (/ a b) x))) ; (/> a (+> b x)))87 ((* (/> b x) a) (/> (* a b) x)) ; (/> a x)88 ((/ (/> b x) a) (*> (/ a b) x)) ; (*> a x)80 ((+ a (/> b x)) (/> b (-> (/ a b) x))) ; (/> a (-> b x))) 81 ((- a (/> b x)) (/> b (-r> (/ a b) x))) ; (/> a (-r> b x))) 82 ((* a (/> b x)) (/> (* a b) x)) ; (/> a x) 83 ((/ a (/> b x)) (/r> (/ a b) x)) ; (/r> a x) 84 85 ((+ (/> b x) a) (/> b (-> (/ a b) x))) ; (/> a (-> b x))) 86 ((- (/> b x) a) (/> b (+> (/ a b) x))) ; (/> a (+> b x))) 87 ((* (/> b x) a) (/> (* a b) x)) ; (/> a x) 88 ((/ (/> b x) a) (*> (/ a b) x)) ; (*> a x) 89 89 90 90 ;(*> b x) 91 ((+ a (*> b x)) (*> b (-> (* a b) x))) ; (*> a (-> b x)))92 ((- a (*> b x)) (*> b (-r> (* a b) x))) ; (*> a (-r> b x)))93 ((* a (*> b x)) (*> (/ b a) x)) ; (*> a x)94 ((/ a (*> b x)) (/r> (* a b) x)) ; (/r> a x)95 96 ((+ (*> b x) a) (*> b (-> (* a b) x))) ; (*> a (-> b x)))97 ((- (*> b x) a) (*> b (+> (* a b) x))) ; (*> a (+> b x)))98 ((* (*> b x) a) (*> (/ b a) x)) ; (*> a x)99 ((/ (*> b x) a) (*> (* a b) x)) ; (*> a x)91 ((+ a (*> b x)) (*> b (-> (* a b) x))) ; (*> a (-> b x))) 92 ((- a (*> b x)) (*> b (-r> (* a b) x))) ; (*> a (-r> b x))) 93 ((* a (*> b x)) (*> (/ b a) x)) ; (*> a x) 94 ((/ a (*> b x)) (/r> (* a b) x)) ; (/r> a x) 95 96 ((+ (*> b x) a) (*> b (-> (* a b) x))) ; (*> a (-> b x))) 97 ((- (*> b x) a) (*> b (+> (* a b) x))) ; (*> a (+> b x))) 98 ((* (*> b x) a) (*> (/ b a) x)) ; (*> a x) 99 ((/ (*> b x) a) (*> (* a b) x)) ; (*> a x) 100 100 101 101 ;(-r> b x) 102 ((+ a (-r> b x)) (-r> (+ a b) x)) ; (-r> a x)103 ((- a (-r> b x)) (+> (- b a) x)) ; (+> a x)104 ;--- ((* a (-r> b x)) (/> a (-r> b x)))105 ;--- ((/ a (-r> b x)) (/r> a (-r> b x)))106 107 ((+ (-r> b x) a) (-r> (+ a b) x)) ; (-r> a x)108 ((- (-r> b x) a) (-r> (- b a) x)) ; (-r> a x)109 ;--- ((* (-r> b x) a) (/> a (-r> b x)))110 ;--- ((/ (-r> b x) a) (*> a (-r> b x)))102 ((+ a (-r> b x)) (-r> (+ a b) x)) ; (-r> a x) 103 ((- a (-r> b x)) (+> (- b a) x)) ; (+> a x) 104 ;--- ((* a (-r> b x)) (/> a (-r> b x))) 105 ;--- ((/ a (-r> b x)) (/r> a (-r> b x))) 106 107 ((+ (-r> b x) a) (-r> (+ a b) x)) ; (-r> a x) 108 ((- (-r> b x) a) (-r> (- b a) x)) ; (-r> a x) 109 ;--- ((* (-r> b x) a) (/> a (-r> b x))) 110 ;--- ((/ (-r> b x) a) (*> a (-r> b x))) 111 111 112 112 ;(/r> b x) 113 ;--- ((+ a (/r> b x)) (-> a (/r> b x)))114 ;--- ((- a (/r> b x)) (-r> a (/r> b x)))115 ((* a (/r> b x)) (/r> (* a b) x)) ; (/r> a x)116 ((/ a (/r> b x)) (*> (/ b a) x)) ; (*> a x)117 118 ;--- ((+ (/r> b x) a) (-> a (/r> b x)))119 ;--- ((- (/r> b x) a) (+> a (/r> b x)))120 ((* (/r> b x) a) (/r> (* a b) x)) ; (/r> a x)121 ((/ (/r> b x) a) (/r> (/ b a) x)) ; (/r> a x)113 ;--- ((+ a (/r> b x)) (-> a (/r> b x))) 114 ;--- ((- a (/r> b x)) (-r> a (/r> b x))) 115 ((* a (/r> b x)) (/r> (* a b) x)) ; (/r> a x) 116 ((/ a (/r> b x)) (*> (/ b a) x)) ; (*> a x) 117 118 ;--- ((+ (/r> b x) a) (-> a (/r> b x))) 119 ;--- ((- (/r> b x) a) (+> a (/r> b x))) 120 ((* (/r> b x) a) (/r> (* a b) x)) ; (/r> a x) 121 ((/ (/r> b x) a) (/r> (/ b a) x)) ; (/r> a x) 122 122 123 123 ;(*> a (-> b x)) 124 ((+ c (*> a (-> b x))) (*> a (-> (+(* c a)b) x))) ; (*> a (-> b x))125 ((- c (*> a (-> b x))) (*> a (-r> (- (* a c) b) x))) ; (*> a (-r> b x))126 ((* c (*> a (-> b x))) (*> (/ a c) (-> b x))) ; (*> a (-> b x)))127 ((/ c (*> a (-> b x))) (/r> (* c a ) (-> b x))) ; (/r> a (-> b x))128 129 ((+ (*> a (-> b x)) c) (*> a (-> (+(* c a)b) x))) ; (*> a (-> b x))130 ((- (*> a (-> b x)) c) (*> a (+> (- (* c a) b) x))) ; (*> a (+> b x))131 ((* (*> a (-> b x)) c) (*> (/ a c) (-> b x))) ; (*> a (-> b x))132 ((/ (*> a (-> b x)) c) (*> (* c a) (-> b x))) ; (*> a (-> b x))124 ((+ c (*> a (-> b x))) (*> a (-> (+(* c a)b) x))) ; (*> a (-> b x)) 125 ((- c (*> a (-> b x))) (*> a (-r> (- (* a c) b) x))) ; (*> a (-r> b x)) 126 ((* c (*> a (-> b x))) (*> (/ a c) (-> b x))) ; (*> a (-> b x))) 127 ((/ c (*> a (-> b x))) (/r> (* c a ) (-> b x))) ; (/r> a (-> b x)) 128 129 ((+ (*> a (-> b x)) c) (*> a (-> (+(* c a)b) x))) ; (*> a (-> b x)) 130 ((- (*> a (-> b x)) c) (*> a (+> (- (* c a) b) x))) ; (*> a (+> b x)) 131 ((* (*> a (-> b x)) c) (*> (/ a c) (-> b x))) ; (*> a (-> b x)) 132 ((/ (*> a (-> b x)) c) (*> (* c a) (-> b x))) ; (*> a (-> b x)) 133 133 134 134 ;(/> a (-> b x)) 135 ((+ c (/> a (-> b x))) (/> a (-> (+ (/ c a) b) x))) ; (/> a (-> b x))136 ((- c (/> a (-> b x))) (/> a (-r> (- (/ c a) b) x))) ; (/> a (-r> b x))137 ((* c (/> a (-> b x))) (/> (* c a) (-> b x))) ; (/> a (-> b x))138 ((/ c (/> a (-> b x))) (/r> (/ c a) (-> b x))) ; (/r> a (-> b x))139 140 ((+ (/> a (-> b x)) c) (/> a (-> (+ (/ c a) b) x))) ; (/> a (-> b x))141 ((- (/> a (-> b x)) c) (/> a (+> (- (/ c a) b) x))) ; (/> a (+> b x))142 ((* (/> a (-> b x)) c) (/> (* c a) (-> b x))) ; (/> a (-> b x))143 ((/ (/> a (-> b x)) c) (*> (/ c a) (-> b x))) ; (*> a (-> b x))135 ((+ c (/> a (-> b x))) (/> a (-> (+ (/ c a) b) x))) ; (/> a (-> b x)) 136 ((- c (/> a (-> b x))) (/> a (-r> (- (/ c a) b) x))) ; (/> a (-r> b x)) 137 ((* c (/> a (-> b x))) (/> (* c a) (-> b x))) ; (/> a (-> b x)) 138 ((/ c (/> a (-> b x))) (/r> (/ c a) (-> b x))) ; (/r> a (-> b x)) 139 140 ((+ (/> a (-> b x)) c) (/> a (-> (+ (/ c a) b) x))) ; (/> a (-> b x)) 141 ((- (/> a (-> b x)) c) (/> a (+> (- (/ c a) b) x))) ; (/> a (+> b x)) 142 ((* (/> a (-> b x)) c) (/> (* c a) (-> b x))) ; (/> a (-> b x)) 143 ((/ (/> a (-> b x)) c) (*> (/ c a) (-> b x))) ; (*> a (-> b x)) 144 144 145 145 146 146 ;(/r> a (-> b x)) 147 ;--- ((+ c (/r> a (-> b x))) (-> c (/r> a (-> b x))))148 ;--- ((- c (/r> a (-> b x))) (-r> c (/r> a (-> b x))))149 ((* c (/r> a (-> b x))) (/r> (* a c) (-> b x))) ; (/r> a (-> b x))150 ((/ c (/r> a (-> b x))) (*> (/ a c) (-> b x))) ; (*> a (-> b x))151 152 153 ;--- ((+ (/r> a (-> b x)) c) (-> c (/r> a (-> b x))))154 ;--- ((- (/r> a (-> b x)) c) (+> c (/r> a (-> b x))))155 ((* (/r> a (-> b x)) c) (/r> (* a c) (-> b x))) ; (/r> a (-> b x))156 ((/ (/r> a (-> b x)) c) (/r> (/ a c) (-> b x))) ; (/r> a (-> b x))147 ;--- ((+ c (/r> a (-> b x))) (-> c (/r> a (-> b x)))) 148 ;--- ((- c (/r> a (-> b x))) (-r> c (/r> a (-> b x)))) 149 ((* c (/r> a (-> b x))) (/r> (* a c) (-> b x))) ; (/r> a (-> b x)) 150 ((/ c (/r> a (-> b x))) (*> (/ a c) (-> b x))) ; (*> a (-> b x)) 151 152 153 ;--- ((+ (/r> a (-> b x)) c) (-> c (/r> a (-> b x)))) 154 ;--- ((- (/r> a (-> b x)) c) (+> c (/r> a (-> b x)))) 155 ((* (/r> a (-> b x)) c) (/r> (* a c) (-> b x))) ; (/r> a (-> b x)) 156 ((/ (/r> a (-> b x)) c) (/r> (/ a c) (-> b x))) ; (/r> a (-> b x)) 157 157 158 158 ;(*> a (+> b x)) 159 ((+ c (*> a (+> b x))) (*> a (+> (- b (* c a)) x))) ; (*> a (+> b x))160 ((- c (*> a (+> b x))) (*> a (-r> (+ (* c a) b) x))) ; (*> a (-r> a x))161 ((* c (*> a (+> b x))) (*> (/ a c) (+> b x))) ; (*> a (+> b x))162 ((/ c (*> a (+> b x))) (/r> (* a c) (+> b x))) ; (/r> a (+> b x))163 164 ((+ (*> a (+> b x)) c) (*> a (+> (- b (* c a)) x))) ; (*> a (+> b x))165 ((- (*> a (+> b x)) c) (*> a (+> (+ (* c a) b) x))) ; (*> a (+> b x))166 ((* (*> a (+> b x)) c) (*> (/ a c) (+> b x))) ; (*> a (+> b x))167 ((/ (*> a (+> b x)) c) (*> (* c a) (+> b x))) ; (*> a (+> b x))159 ((+ c (*> a (+> b x))) (*> a (+> (- b (* c a)) x))) ; (*> a (+> b x)) 160 ((- c (*> a (+> b x))) (*> a (-r> (+ (* c a) b) x))) ; (*> a (-r> a x)) 161 ((* c (*> a (+> b x))) (*> (/ a c) (+> b x))) ; (*> a (+> b x)) 162 ((/ c (*> a (+> b x))) (/r> (* a c) (+> b x))) ; (/r> a (+> b x)) 163 164 ((+ (*> a (+> b x)) c) (*> a (+> (- b (* c a)) x))) ; (*> a (+> b x)) 165 ((- (*> a (+> b x)) c) (*> a (+> (+ (* c a) b) x))) ; (*> a (+> b x)) 166 ((* (*> a (+> b x)) c) (*> (/ a c) (+> b x))) ; (*> a (+> b x)) 167 ((/ (*> a (+> b x)) c) (*> (* c a) (+> b x))) ; (*> a (+> b x)) 168 168 169 169 170 170 ;(/> a (+> b x)) 171 ((+ c (/> a (+> b x))) (/> a (+> (- b (/ c a)) x))) ; (/> a (+> b x)) 172 ((- c (/> a (+> b x))) (/> a (-r> (+ (/ c a) b) x))) ; (/> a (-r> b x)) 173 ((* c (/> a (+> b x))) (/> (* c a) (+> b x))) ; (/> a (+> b x)) 174 ((/ c (/> a (+> b x))) (/r> (/ c a) (+> b x))) ; (/r> a (+> b x)) 171 ((+ c (/> a (+> b x))) (/> a (+> (- b (/ c a)) x))) ; (/> a (+> b x)) 172 ((- c (/> a (+> b x))) (/> a (-r> (+ (/ c a) b) x))) ; (/> a (-r> b x)) 173 ((* c (/> a (+> b x))) (/> (* c a) (+> b x))) ; (/> a (+> b x)) 174 ((/ c (/> a (+> b x))) (/r> (/ c a) (+> b x))) ; (/r> a (+> b x)) 175 176 ((+ (/> a (+> b x)) c) (/> a (+> (- b (/ c a)) x))) ; (/> a (+> b x)) 177 ((- (/> a (+> b x)) c) (/> a (+> (+ (/ c a) b) x))) ; (/> a (+> b x)) 178 ((* (/> a (+> b x)) c) (/> (* c a) (+> b x))) ; (/> a (+> b x)) 179 ((/ (/> a (+> b x)) c) (*> (/ c a) (+> b x))) ; (*> a (+> b x)) 180 181 182 ;(/r> a (+> b x)) 183 ;--- ((+ c (/r> a (+> b x))) (-> c (/r> a (+> b x)))) 184 ;--- ((- c (/r> a (+> b x))) (-r> c (/r> a (+> b x)))) 185 ((* c (/r> a (+> b x))) (/r> (* a c) (+> b x))) ; (/r> a (+> b x)) 186 ((/ c (/r> a (+> b x))) (*> (/ a c) (+> b x))) ; (*> a (+> b x)) 187 188 ;--- ((+ (/r> a (+> b x)) c) (-> c (/r> a (+> b x)))) 189 ;--- ((- (/r> a (+> b x)) c) (+> c (/r> a (+> b x)))) 190 ((* (/r> a (+> b x)) c) (/r> (* a c) (+> b x))) ; (/r> a (+> b x)) 191 ((/ (/r> a (+> b x)) c) (/r> (/ a c) (+> b x))) ; (/r> a (+> b x)) 175 192 176 193 177 ((+ (/> a (+> b x)) c) (/> a (+> (- b (/ c a)) x))) ; (/> a (+> b x))178 ((- (/> a (+> b x)) c) (/> a (+> (+ (/ c a) b) x))) ; (/> a (+> b x))179 ((* (/> a (+> b x)) c) (/> (* c a) (+> b x))) ; (/> a (+> b x))180 ((/ (/> a (+> b x)) c) (*> (/ c a) (+> b x))) ; (*> a (+> b x))181 182 183 ;(/r> a (+> b x))184 ;--- ((+ c (/r> a (+> b x))) (-> c (/r> a (+> b x))))185 ;--- ((- c (/r> a (+> b x))) (-r> c (/r> a (+> b x))))186 ((* c (/r> a (+> b x))) (/r> (* a c) (+> b x))) ; (/r> a (+> b x))187 ((/ c (/r> a (+> b x))) (*> (/ a c) (+> b x))) ; (*> a (+> b x))188 189 ;--- ((+ (/r> a (+> b x)) c) (-> c (/r> a (+> b x))))190 ;--- ((- (/r> a (+> b x)) c) (+> c (/r> a (+> b x))))191 ((* (/r> a (+> b x)) c) (/r> (* a c) (+> b x))) ; (/r> a (+> b x))192 ((/ (/r> a (+> b x)) c) (/r> (/ a c) (+> b x))) ; (/r> a (+> b x))193 194 195 194 196 195 ;(*> a (-r> b x)) 197 ((+ c (*> a (-r> b x))) (*> a (-r> (+ b (* c a)) x))) ; (*> a (-r> b x))198 ((- c (*> a (-r> b x))) (*> a (+> (- b (* c a)) x))) ; (*> a (+> b x))199 ((* c (*> a (-r> b x))) (*> (/ a c) (-r> b x))) ; (*> a (-r> b x))200 ((/ c (*> a (-r> b x))) (/r> (* a c) (-r> b x))) ; (/r> a (-r> b x))201 202 ((+ (*> a (-r> b x)) c) (*> a (-r> (+ b (* c a)) x))) ; (*> a (-r> b x))203 ((- (*> a (-r> b x)) c) (*> a (-r> (- b (* c a)) x))) ; (*> a (-r> b x))204 ((* (*> a (-r> b x)) c) (*> (/ a c) (-r> b x))) ; (*> a (-r> b x))205 ((/ (*> a (-r> b x)) c) (*> (* a c) (-r> b x))) ; (*> a (-r> b x))196 ((+ c (*> a (-r> b x))) (*> a (-r> (+ b (* c a)) x))) ; (*> a (-r> b x)) 197 ((- c (*> a (-r> b x))) (*> a (+> (- b (* c a)) x))) ; (*> a (+> b x)) 198 ((* c (*> a (-r> b x))) (*> (/ a c) (-r> b x))) ; (*> a (-r> b x)) 199 ((/ c (*> a (-r> b x))) (/r> (* a c) (-r> b x))) ; (/r> a (-r> b x)) 200 201 ((+ (*> a (-r> b x)) c) (*> a (-r> (+ b (* c a)) x))) ; (*> a (-r> b x)) 202 ((- (*> a (-r> b x)) c) (*> a (-r> (- b (* c a)) x))) ; (*> a (-r> b x)) 203 ((* (*> a (-r> b x)) c) (*> (/ a c) (-r> b x))) ; (*> a (-r> b x)) 204 ((/ (*> a (-r> b x)) c) (*> (* a c) (-r> b x))) ; (*> a (-r> b x)) 206 205 207 206 208 207 ;(/> a (-r> b x)) 209 ((+ c (/> a (-r> b x))) (/> a (-r> (+ b (/ c a)) x))) ; (/> a (-r> b x)) 210 ((- c (/> a (-r> b x))) (/> a (+> (- b (/ c a)) x))) ; (/> a (+> b x)) 211 ((* c (/> a (-r> b x))) (/> (* a c) (-r> b x))) ; (/> a (-r> b x)) 212 ((/ c (/> a (-r> b x))) (/r> (/ c a) (-r> b x))) ; (/r> a (-r> b x)) 213 214 ((+ (/> a (-r> b x)) c) (/> a (-r> (+ b (/ c a)) x))) ; (/> a (-r> b x)) 215 ((- (/> a (-r> b x)) c) (/> a (-r> (- b (/ c a)) x))) ; (/> a (-r> b x)) 216 ((* (/> a (-r> b x)) c) (/> (* a c) (-r> b x))) ; (/> a (-r> b x)) 217 ((/ (/> a (-r> b x)) c) (*> (/ c a) (-r> b x))) ; (*> a (-r> b x)) 218 219 220 221 ((+ x x) (/> 2 x)) 222 223 ;xxx ((- x x) ()) 224 ;qqq ((* x x) ()) 225 ;xxx ((/ x x) ()) 226 227 ((+ (-> h x) x) (/> 2 (-> (/ h 2) x))) ; (/> a (-> b x)) 228 ((+ (+> h x) x) (/> 2 (+> (/ h 2) x))) ; (/> a (+> b x)) 229 230 ((+ (/> h x) x) (/> (+ h 1) x)) ; (/> a x) 231 ((+ (*> h x) x) (/> (+ (/ 1 h) 1) x)) ; (/> a x) 232 ;xxx ((+ (-r> h x) x) ()) 233 ;qqq ((+ (/r> h x) x) ()) 234 235 ((+ x (-> e x)) (/> 2 (-> (/ e 2) x))) ; (/> a (-> b x)) 236 ((+ x (+> e x)) (/> 2 (+> (/ e 2) x))) ; (/> a (+> b x)) 237 ((+ x (/> e x)) (/> (+ 1 e) x)) ; (/> a x) 238 ((+ x (*> e x)) (/> (+ (/ 1 e) 1) x)) ; (/> a x) 239 ;xxx ((+ x (-r> e x)) ()) 240 ;xxx ((+ x (/r> e x)) ()) 241 242 ;xxx ((- (-> h x) x) ()) 243 ;xxx ((- (+> h x) x) ()) 244 ((- (/> h x) x) (/> (- h 1) x)) 245 ((- (*> h x) x) (/> (- (/ 1 h) 1) x)) 246 ((- (-r> h x) x) (/> 2 (-r> (/ h 2) x))) 247 248 ;xxx ((- (/r> h x) x) ()) 249 ;xxx ((- x (-> e x)) ()) 250 ;xxx ((- x (+> e x)) ()) 251 ((- x (/> e x)) (/> (- 1 e) x)) 252 ((- x (*> e x)) (/> (- 1 (/ 1 e)) x)) 253 ((- x (-r> e x)) (/> 2 (+> (/ e 2) x))) 254 ;xxx ((- x (/r> e x)) ()) 255 256 257 258 ;qqq ((* (-> h x) x) ()) 259 ;qqq ((* (+> h x) x) ()) 260 ;qqq ((* (/> h x) x) ()) 261 ;qqq ((* (*> h x) x) ()) 262 ;qqq ((* (-r> h x) x) ()) 263 ;xxx ((* (/r> h x) x) ()) 264 265 ;qqq ((* x (-> e x)) ()) 266 ;qqq ((* x (+> e x)) ()) 267 ;qqq ((* x (/> e x)) ()) 268 ;qqq ((* x (*> e x)) ()) 269 ;qqq ((* x (-r> e x)) ()) 270 ;xxx ((* x (/r> e x)) ()) 271 272 ;xxx ((/ x (-> e x)) ()) 273 ;xxx ((/ x (+> e x)) ()) 274 ;xxx ((/ x (/> e x)) ()) 275 ;xxx ((/ x (*> e x)) ()) 276 ;xxx ((/ x (-r> e x)) ()) 277 ;qqq ((/ x (/r> e x)) ()) 278 279 280 ((/ (-> h x) x) (-> 1 (/r> h x))) 208 ((+ c (/> a (-r> b x))) (/> a (-r> (+ b (/ c a)) x))) ; (/> a (-r> b x)) 209 ((- c (/> a (-r> b x))) (/> a (+> (- b (/ c a)) x))) ; (/> a (+> b x)) 210 ((* c (/> a (-r> b x))) (/> (* a c) (-r> b x))) ; (/> a (-r> b x)) 211 ((/ c (/> a (-r> b x))) (/r> (/ c a) (-r> b x))) ; (/r> a (-r> b x)) 212 213 ((+ (/> a (-r> b x)) c) (/> a (-r> (+ b (/ c a)) x))) ; (/> a (-r> b x)) 214 ((- (/> a (-r> b x)) c) (/> a (-r> (- b (/ c a)) x))) ; (/> a (-r> b x)) 215 ((* (/> a (-r> b x)) c) (/> (* a c) (-r> b x))) ; (/> a (-r> b x)) 216 ((/ (/> a (-r> b x)) c) (*> (/ c a) (-r> b x))) ; (*> a (-r> b x)) 217 218 219 220 ((+ x x) (/> 2 x)) 221 222 ;xxx ((- x x) ()) 223 ;qqq ((* x x) ()) 224 ;xxx ((/ x x) ()) 225 226 ((+ (+> h x) x) (/> 2 (+> (/ h 2) x))) ; (/> a (+> b x)) 227 ((+ (-> h x) x) (/> 2 (-> (/ h 2) x))) ; (/> a (-> b x)) 228 ((+ (*> h x) x) (/> (+ (/ 1 h) 1) x)) ; (/> a x) 229 ((+ (/> h x) x) (/> (+ h 1) x)) ; (/> a x) 230 ;xxx ((+ (-r> h x) x) ()) 231 ;qqq ((+ (/r> h x) x) ()) 232 233 ((+ x (+> e x)) (/> 2 (+> (/ e 2) x))) ; (/> a (+> b x)) 234 ((+ x (-> e x)) (/> 2 (-> (/ e 2) x))) ; (/> a (-> b x)) 235 ((+ x (*> e x)) (/> (+ (/ 1 e) 1) x)) ; (/> a x) 236 ((+ x (/> e x)) (/> (+ 1 e) x)) ; (/> a x) 237 ;xxx ((+ x (-r> e x)) ()) 238 ;xxx ((+ x (/r> e x)) ()) 239 240 ;xxx ((- (+> h x) x) ()) 241 ;xxx ((- (-> h x) x) ()) 242 ((- (*> h x) x) (/> (- (/ 1 h) 1) x)) 243 ((- (/> h x) x) (/> (- h 1) x)) 244 ((- (-r> h x) x) (/> 2 (-r> (/ h 2) x))) 245 ;xxx ((- (/r> h x) x) ()) 246 247 ;xxx ((- x (+> e x)) ()) 248 ;xxx ((- x (-> e x)) ()) 249 ((- x (*> e x)) (/> (- 1 (/ 1 e)) x)) 250 ((- x (/> e x)) (/> (- 1 e) x)) 251 ((- x (-r> e x)) (/> 2 (+> (/ e 2) x))) 252 ;xxx ((- x (/r> e x)) ()) 253 254 ;qqq ((* (+> h x) x) ()) 255 ;qqq ((* (-> h x) x) ()) 256 ;qqq ((* (*> h x) x) ()) 257 ;qqq ((* (/> h x) x) ()) 258 ;qqq ((* (-r> h x) x) ()) 259 ;xxx ((* (/r> h x) x) ()) 260 261 ;qqq ((* x (+> e x)) ()) 262 ;qqq ((* x (-> e x)) ()) 263 ;qqq ((* x (*> e x)) ()) 264 ;qqq ((* x (/> e x)) ()) 265 ;qqq ((* x (-r> e x)) ()) 266 ;xxx ((* x (/r> e x)) ()) 267 281 268 ;| # 282 269 ;;;; PROVEN 283 ((/ (+> h x) x) (-r> 1 (/r> h x))) 284 ;xxx ((/ (/> h x) x) ()) 285 ;xxx ((/ (*> h x) x) ()) 286 ((/ (-r> h x) x) (*> h (+> h x))) 287 ;qqq ((/ (/r> h x) x) ()) 288 289 290 291 ((+ (/> k (-> h x)) x) (/> (+ k 1) (-> (/ (* h k) (+ k 1)) x))) 292 ; ((+ (/r> k (-> h x)) x) ()) 293 ; ((+ (*> k (+> h x)) x) ()) 294 ; ((+ (/> k (+> h x)) x) ()) 295 ; ((+ (/r> k (+> h x)) x) ()) 296 ; ((+ (*> k (-r> h x)) x) ()) 297 ; ((+ (/> k (-r> h x)) x) ()) 298 ; ((+ x (/> f (-> e x))) ()) 299 ; ((+ x (/r> f (-> e x))) ()) 300 ; ((+ x (*> f (+> e x))) ()) 301 ; ((+ x (/> f (+> e x))) ()) 302 ; ((+ x (/r> f (+> e x))) ()) 303 ; ((+ x (*> f (-r> e x))) ()) 304 ; ((+ x (/> f (-r> e x))) ()) 305 ; ((- (/> k (-> h x)) x) ()) 306 ; ((- (/r> k (-> h x)) x) ()) 307 ; ((- (*> k (+> h x)) x) ()) 308 ; ((- (/> k (+> h x)) x) ()) 309 ; ((- (/r> k (+> h x)) x) ()) 310 ; ((- (*> k (-r> h x)) x) ()) 311 ; ((- (/> k (-r> h x)) x) ()) 312 ; ((- x (/> f (-> e x))) ()) 313 ; ((- x (/r> f (-> e x))) ()) 314 ; ((- x (*> f (+> e x))) ()) 315 ; ((- x (/> f (+> e x))) ()) 316 ; ((- x (/r> f (+> e x))) ()) 317 ; ((- x (*> f (-r> e x))) ()) 318 ; ((- x (/> f (-r> e x))) ()) 319 ; ((* (/> k (-> h x)) x) ()) 320 ; ((* (/r> k (-> h x)) x) ()) 321 ; ((* (*> k (+> h x)) x) ()) 322 ; ((* (/> k (+> h x)) x) ()) 323 ; ((* (/r> k (+> h x)) x) ()) 324 ; ((* (*> k (-r> h x)) x) ()) 325 ; ((* (/> k (-r> h x)) x) ()) 326 ; ((* x (/> f (-> e x))) ()) 327 ; ((* x (/r> f (-> e x))) ()) 328 ; ((* x (*> f (+> e x))) ()) 329 ; ((* x (/> f (+> e x))) ()) 330 ; ((* x (/r> f (+> e x))) ()) 331 ; ((* x (*> f (-r> e x))) ()) 332 ; ((* x (/> f (-r> e x))) ()) 333 ; ((/ x (/> f (-> e x))) ()) 334 ; ((/ x (/r> f (-> e x))) ()) 335 ; ((/ x (*> f (+> e x))) ()) 336 ; ((/ x (/> f (+> e x))) ()) 337 ; ((/ x (/r> f (+> e x))) ()) 338 ; ((/ x (*> f (-r> e x))) ()) 339 ; ((/ x (/> f (-r> e x))) ()) 340 ; ((/ (/> k (-> h x)) x) ()) 341 ; ((/ (/r> k (-> h x)) x) ()) 342 ; ((/ (*> k (+> h x)) x) ()) 343 ; ((/ (/> k (+> h x)) x) ()) 344 ; ((/ (/r> k (+> h x)) x) ()) 345 ; ((/ (*> k (-r> h x)) x) ()) 346 ; ((/ (/> k (-r> h x)) x) ()) 347 ; ((+ (-> h x) (-> e x)) ()) 348 ; ((+ (+> h x) (-> e x)) ()) 349 ; ((+ (/> h x) (-> e x)) ()) 350 ; ((+ (*> h x) (-> e x)) ()) 351 ; ((+ (-r> h x) (-> e x)) ()) 352 ; ((+ (/r> h x) (-> e x)) ()) 353 ; ((+ (/> k (-> h x)) (-> e x)) ()) 354 ; ((+ (/r> k (-> h x)) (-> e x)) ()) 355 ; ((+ (*> k (+> h x)) (-> e x)) ()) 356 ; ((+ (/> k (+> h x)) (-> e x)) ()) 357 ; ((+ (/r> k (+> h x)) (-> e x)) ()) 358 ; ((+ (*> k (-r> h x)) (-> e x)) ()) 359 ; ((+ (/> k (-r> h x)) (-> e x)) ()) 360 ; ((+ (-> h x) (+> e x)) ()) 361 ; ((+ (+> h x) (+> e x)) ()) 362 ; ((+ (/> h x) (+> e x)) ()) 363 ; ((+ (*> h x) (+> e x)) ()) 364 ; ((+ (-r> h x) (+> e x)) ()) 365 ; ((+ (/r> h x) (+> e x)) ()) 366 ; ((+ (/> k (-> h x)) (+> e x)) ()) 367 ; ((+ (/r> k (-> h x)) (+> e x)) ()) 368 ; ((+ (*> k (+> h x)) (+> e x)) ()) 369 ; ((+ (/> k (+> h x)) (+> e x)) ()) 370 ; ((+ (/r> k (+> h x)) (+> e x)) ()) 371 ; ((+ (*> k (-r> h x)) (+> e x)) ()) 372 ; ((+ (/> k (-r> h x)) (+> e x)) ()) 373 ; ((+ (-> h x) (/> e x)) ()) 374 ; ((+ (+> h x) (/> e x)) ()) 375 376 377 ((+ (/> a b) (/> c b)) (/> (+ a c) b) ); ("Goal" :use ((:instance lemma_h)) :do-not '(:preprocess))) 378 379 #| 380 381 ; ((+ (*> h x) (/> e x)) ()) 382 ; ((+ (-r> h x) (/> e x)) ()) 383 ; ((+ (/r> h x) (/> e x)) ()) 384 ; ((+ (/> k (-> h x)) (/> e x)) ()) 385 ; ((+ (/r> k (-> h x)) (/> e x)) ()) 386 ; ((+ (*> k (+> h x)) (/> e x)) ()) 387 ; ((+ (/> k (+> h x)) (/> e x)) ()) 388 ; ((+ (/r> k (+> h x)) (/> e x)) ()) 389 ; ((+ (*> k (-r> h x)) (/> e x)) ()) 390 ; ((+ (/> k (-r> h x)) (/> e x)) ()) 391 ; ((+ (-> h x) (*> e x)) ()) 392 ; ((+ (+> h x) (*> e x)) ()) 393 ; ((+ (/> h x) (*> e x)) ()) 394 ; ((+ (*> h x) (*> e x)) ()) 395 ; ((+ (-r> h x) (*> e x)) ()) 396 ; ((+ (/r> h x) (*> e x)) ()) 397 ; ((+ (/> k (-> h x)) (*> e x)) ()) 398 ; ((+ (/r> k (-> h x)) (*> e x)) ()) 399 ; ((+ (*> k (+> h x)) (*> e x)) ()) 400 ; ((+ (/> k (+> h x)) (*> e x)) ()) 401 ; ((+ (/r> k (+> h x)) (*> e x)) ()) 402 ; ((+ (*> k (-r> h x)) (*> e x)) ()) 403 ; ((+ (/> k (-r> h x)) (*> e x)) ()) 404 ; ((+ (-> h x) (-r> e x)) ()) 405 ; ((+ (+> h x) (-r> e x)) ()) 406 ; ((+ (/> h x) (-r> e x)) ()) 407 ; ((+ (*> h x) (-r> e x)) ()) 408 ; ((+ (-r> h x) (-r> e x)) ()) 409 ; ((+ (/r> h x) (-r> e x)) ()) 410 ; ((+ (/> k (-> h x)) (-r> e x)) ()) 411 ; ((+ (/r> k (-> h x)) (-r> e x)) ()) 412 ; ((+ (*> k (+> h x)) (-r> e x)) ()) 413 ; ((+ (/> k (+> h x)) (-r> e x)) ()) 414 ; ((+ (/r> k (+> h x)) (-r> e x)) ()) 415 ; ((+ (*> k (-r> h x)) (-r> e x)) ()) 416 ; ((+ (/> k (-r> h x)) (-r> e x)) ()) 417 ; ((+ (-> h x) (/r> e x)) ()) 418 ; ((+ (+> h x) (/r> e x)) ()) 419 ; ((+ (/> h x) (/r> e x)) ()) 420 ; ((+ (*> h x) (/r> e x)) ()) 421 ; ((+ (-r> h x) (/r> e x)) ()) 422 423 ((+ (/r> a b) (/r> c b)) (/r> (+ a c) b)) 424 425 ; ((+ (/> k (-> h x)) (/r> e x)) ()) 426 ; ((+ (/r> k (-> h x)) (/r> e x)) ()) 427 ; ((+ (*> k (+> h x)) (/r> e x)) ()) 428 ; ((+ (/> k (+> h x)) (/r> e x)) ()) 429 ; ((+ (/r> k (+> h x)) (/r> e x)) ()) 430 ; ((+ (*> k (-r> h x)) (/r> e x)) ()) 431 ; ((+ (/> k (-r> h x)) (/r> e x)) ()) 432 ; ((+ (-> h x) (/> f (-> e x))) ()) 433 ; ((+ (+> h x) (/> f (-> e x))) ()) 434 ; ((+ (/> h x) (/> f (-> e x))) ()) 435 ; ((+ (*> h x) (/> f (-> e x))) ()) 436 ; ((+ (-r> h x) (/> f (-> e x))) ()) 437 ; ((+ (/r> h x) (/> f (-> e x))) ()) 270 271 ((/ (+> h x) x) (-r> 1 (/r> h x))) 272 ((/ (-> h x) x) (-> 1 (/r> h x))) 273 ;xxx ((/ (*> h x) x) ()) 274 ;xxx ((/ (/> h x) x) ()) 275 ((/ (-r> h x) x) (*> h (+> h x))) 276 ;qqq ((/ (/r> h x) x) ()) 277 278 ;xxx ((/ x (-> e x)) ()) 279 ;xxx ((/ x (+> e x)) ()) 280 ;xxx ((/ x (/> e x)) ()) 281 ;xxx ((/ x (*> e x)) ()) 282 ;xxx ((/ x (-r> e x)) ()) 283 ;qqq ((/ x (/r> e x)) ()) 284 285 286 ((+ (*> k (+> h x)) x) (/> (+ (/ 1 k) 1) (+> (/ (/ h k) (+ (/ 1 k) 1)) x))) ; (/> A (+> B x)) 287 ; ((+ (*> k (-r> h x)) x) ()) 288 ((+ (/> k (+> h x)) x) (/> (+ k 1) (+> (/ (* h k) (+ k 1)) x))) ; (/> A (+> B x)) 289 ((+ (/> k (-> h x)) x) (/> (+ k 1) (-> (/ (* h k) (+ k 1)) x))) ; (/> A (-> B x)) 290 ; ((+ (/> k (-r> h x)) x) ()) 291 ; ((+ (/r> k (+> h x)) x) ()) 292 ;xxx ((+ (/r> k (-> h x)) x) ()) 293 294 ; ((+ x (*> f (+> e x))) ()) 295 ; ((+ x (*> f (-r> e x))) ()) 296 ; ((+ x (/> f (+> e x))) ()) 297 ; ((+ x (/> f (-> e x))) ()) 298 ; ((+ x (/> f (-r> e x))) ()) 299 ; ((+ x (/r> f (+> e x))) ()) 300 ; ((+ x (/r> f (-> e x))) ()) 301 302 ; ((- (*> k (+> h x)) x) ()) 303 ; ((- (*> k (-r> h x)) x) ()) 304 ; ((- (/> k (+> h x)) x) ()) 305 ; ((- (/> k (-> h x)) x) ()) 306 ; ((- (/> k (-r> h x)) x) ()) 307 ; ((- (/r> k (+> h x)) x) ()) 308 ; ((- (/r> k (-> h x)) x) ()) 309 310 ; ((- x (*> f (+> e x))) ()) 311 ; ((- x (*> f (-r> e x))) ()) 312 ; ((- x (/> f (+> e x))) ()) 313 ; ((- x (/> f (-> e x))) ()) 314 ; ((- x (/> f (-r> e x))) ()) 315 ; ((- x (/r> f (+> e x))) ()) 316 ; ((- x (/r> f (-> e x))) ()) 317 318 ;qqq ((* (*> k (+> h x)) x) ()) 319 ;qqq ((* (*> k (-r> h x)) x) ()) 320 ;qqq ((* (/> k (+> h x)) x) ()) 321 ;qqq ((* (/> k (-> h x)) x) ()) 322 ;qqq ((* (/> k (-r> h x)) x) ()) 323 ; ((* (/r> k (+> h x)) x) ()) 324 ; ((* (/r> k (-> h x)) x) ()) 325 326 ;qqq ((* x (*> f (+> e x))) ()) 327 ;qqq ((* x (*> f (-r> e x))) ()) 328 ;qqq ((* x (/> f (+> e x))) ()) 329 ;qqq ((* x (/> f (-> e x))) ()) 330 ;qqq ((* x (/> f (-r> e x))) ()) 331 ; ((* x (/r> f (+> e x))) ()) 332 ; ((* x (/r> f (-> e x))) ()) 333 334 ; ((/ x (*> f (+> e x))) ()) 335 ; ((/ x (*> f (-r> e x))) ()) 336 ; ((/ x (/> f (+> e x))) ()) 337 ; ((/ x (/> f (-> e x))) ()) 338 ; ((/ x (/> f (-r> e x))) ()) 339 ; ((/ x (/r> f (+> e x))) ()) 340 ; ((/ x (/r> f (-> e x))) ()) 341 342 ; ((/ (*> k (+> h x)) x) ()) 343 ; ((/ (*> k (-r> h x)) x) ()) 344 ; ((/ (/> k (+> h x)) x) ()) 345 ; ((/ (/> k (-> h x)) x) ()) 346 ; ((/ (/> k (-r> h x)) x) ()) 347 ; ((/ (/r> k (+> h x)) x) ()) 348 ; ((/ (/r> k (-> h x)) x) ()) 349 350 ; ((+ (-> h x) (-> e x)) ()) 351 ; ((+ (+> h x) (-> e x)) ()) 352 ; ((+ (/> h x) (-> e x)) ()) 353 ; ((+ (*> h x) (-> e x)) ()) 354 ; ((+ (-r> h x) (-> e x)) ()) 355 ; ((+ (/r> h x) (-> e x)) ()) 356 ; ((+ (/> k (-> h x)) (-> e x)) ()) 357 ; ((+ (/r> k (-> h x)) (-> e x)) ()) 358 ; ((+ (*> k (+> h x)) (-> e x)) ()) 359 ; ((+ (/> k (+> h x)) (-> e x)) ()) 360 ; ((+ (/r> k (+> h x)) (-> e x)) ()) 361 ; ((+ (*> k (-r> h x)) (-> e x)) ()) 362 ; ((+ (/> k (-r> h x)) (-> e x)) ()) 363 ; ((+ (-> h x) (+> e x)) ()) 364 ; ((+ (+> h x) (+> e x)) ()) 365 ; ((+ (/> h x) (+> e x)) ()) 366 ; ((+ (*> h x) (+> e x)) ()) 367 ; ((+ (-r> h x) (+> e x)) ()) 368 ; ((+ (/r> h x) (+> e x)) ()) 369 ; ((+ (/> k (-> h x)) (+> e x)) ()) 370 ; ((+ (/r> k (-> h x)) (+> e x)) ()) 371 ; ((+ (*> k (+> h x)) (+> e x)) ()) 372 ; ((+ (/> k (+> h x)) (+> e x)) ()) 373 ; ((+ (/r> k (+> h x)) (+> e x)) ()) 374 ; ((+ (*> k (-r> h x)) (+> e x)) ()) 375 ; ((+ (/> k (-r> h x)) (+> e x)) ()) 376 ; ((+ (-> h x) (/> e x)) ()) 377 ; ((+ (+> h x) (/> e x)) ()) 378 ((+ (/> a b) (/> c b)) (/> (+ a c) b) ) 379 ; ((+ (*> h x) (/> e x)) ()) 380 ; ((+ (-r> h x) (/> e x)) ()) 381 ; ((+ (/r> h x) (/> e x)) ()) 382 ; ((+ (/> k (-> h x)) (/> e x)) ()) 383 ; ((+ (/r> k (-> h x)) (/> e x)) ()) 384 ; ((+ (*> k (+> h x)) (/> e x)) ()) 385 ; ((+ (/> k (+> h x)) (/> e x)) ()) 386 ; ((+ (/r> k (+> h x)) (/> e x)) ()) 387 ; ((+ (*> k (-r> h x)) (/> e x)) ()) 388 ; ((+ (/> k (-r> h x)) (/> e x)) ()) 389 ; ((+ (-> h x) (*> e x)) ()) 390 ; ((+ (+> h x) (*> e x)) ()) 391 ; ((+ (/> h x) (*> e x)) ()) 392 ; ((+ (*> h x) (*> e x)) ()) 393 ; ((+ (-r> h x) (*> e x)) ()) 394 ; ((+ (/r> h x) (*> e x)) ()) 395 ; ((+ (/> k (-> h x)) (*> e x)) ()) 396 ; ((+ (/r> k (-> h x)) (*> e x)) ()) 397 ; ((+ (*> k (+> h x)) (*> e x)) ()) 398 ; ((+ (/> k (+> h x)) (*> e x)) ()) 399 ; ((+ (/r> k (+> h x)) (*> e x)) ()) 400 ; ((+ (*> k (-r> h x)) (*> e x)) ()) 401 ; ((+ (/> k (-r> h x)) (*> e x)) ()) 402 ; ((+ (-> h x) (-r> e x)) ()) 403 ; ((+ (+> h x) (-r> e x)) ()) 404 ; ((+ (/> h x) (-r> e x)) ()) 405 ; ((+ (*> h x) (-r> e x)) ()) 406 ; ((+ (-r> h x) (-r> e x)) ()) 407 ; ((+ (/r> h x) (-r> e x)) ()) 408 ; ((+ (/> k (-> h x)) (-r> e x)) ()) 409 ; ((+ (/r> k (-> h x)) (-r> e x)) ()) 410 ; ((+ (*> k (+> h x)) (-r> e x)) ()) 411 ; ((+ (/> k (+> h x)) (-r> e x)) ()) 412 ; ((+ (/r> k (+> h x)) (-r> e x)) ()) 413 ; ((+ (*> k (-r> h x)) (-r> e x)) ()) 414 ; ((+ (/> k (-r> h x)) (-r> e x)) ()) 415 ; ((+ (-> h x) (/r> e x)) ()) 416 ; ((+ (+> h x) (/r> e x)) ()) 417 ; ((+ (/> h x) (/r> e x)) ()) 418 ; ((+ (*> h x) (/r> e x)) ()) 419 ; ((+ (-r> h x) (/r> e x)) ()) 420 ((+ (/r> h x) (/r> e x)) (/r> (+ h e) x)) 421 ; ((+ (/> k (-> h x)) (/r> e x)) ()) 422 ; ((+ (/r> k (-> h x)) (/r> e x)) ()) 423 ; ((+ (*> k (+> h x)) (/r> e x)) ()) 424 ; ((+ (/> k (+> h x)) (/r> e x)) ()) 425 ; ((+ (/r> k (+> h x)) (/r> e x)) ()) 426 ; ((+ (*> k (-r> h x)) (/r> e x)) ()) 427 ; ((+ (/> k (-r> h x)) (/r> e x)) ()) 428 ; ((+ (-> h x) (/> f (-> e x))) ()) 429 ; ((+ (+> h x) (/> f (-> e x))) ()) 430 ; ((+ (/> h x) (/> f (-> e x))) ()) 431 ; ((+ (*> h x) (/> f (-> e x))) ()) 432 ; ((+ (-r> h x) (/> f (-> e x))) ()) 433 ; ((+ (/r> h x) (/> f (-> e x))) ()) 438 434 ; ((+ (/> k (-> h x)) (/> f (-> e x))) ()) 439 435 ; ((+ (/r> k (-> h x)) (/> f (-> e x))) ()) … … 443 439 ; ((+ (*> k (-r> h x)) (/> f (-> e x))) ()) 444 440 ; ((+ (/> k (-r> h x)) (/> f (-> e x))) ()) 445 ; ((+ (-> h x) (/r> f (-> e x))) ())446 ; ((+ (+> h x) (/r> f (-> e x))) ())447 ; ((+ (/> h x) (/r> f (-> e x))) ())448 ; ((+ (*> h x) (/r> f (-> e x))) ())449 ; ((+ (-r> h x) (/r> f (-> e x))) ())450 ; ((+ (/r> h x) (/r> f (-> e x))) ())441 ; ((+ (-> h x) (/r> f (-> e x))) ()) 442 ; ((+ (+> h x) (/r> f (-> e x))) ()) 443 ; ((+ (/> h x) (/r> f (-> e x))) ()) 444 ; ((+ (*> h x) (/r> f (-> e x))) ()) 445 ; ((+ (-r> h x) (/r> f (-> e x))) ()) 446 ; ((+ (/r> h x) (/r> f (-> e x))) ()) 451 447 ; ((+ (/> k (-> h x)) (/r> f (-> e x))) ()) 452 448 ; ((+ (/r> k (-> h x)) (/r> f (-> e x))) ()) … … 456 452 ; ((+ (*> k (-r> h x)) (/r> f (-> e x))) ()) 457 453 ; ((+ (/> k (-r> h x)) (/r> f (-> e x))) ()) 458 ; ((+ (-> h x) (*> f (+> e x))) ())459 ; ((+ (+> h x) (*> f (+> e x))) ())460 ; ((+ (/> h x) (*> f (+> e x))) ())461 ; ((+ (*> h x) (*> f (+> e x))) ())462 ; ((+ (-r> h x) (*> f (+> e x))) ())463 ; ((+ (/r> h x) (*> f (+> e x))) ())454 ; ((+ (-> h x) (*> f (+> e x))) ()) 455 ; ((+ (+> h x) (*> f (+> e x))) ()) 456 ; ((+ (/> h x) (*> f (+> e x))) ()) 457 ; ((+ (*> h x) (*> f (+> e x))) ()) 458 ; ((+ (-r> h x) (*> f (+> e x))) ()) 459 ; ((+ (/r> h x) (*> f (+> e x))) ()) 464 460 ; ((+ (/> k (-> h x)) (*> f (+> e x))) ()) 465 461 ; ((+ (/r> k (-> h x)) (*> f (+> e x))) ()) … … 469 465 ; ((+ (*> k (-r> h x)) (*> f (+> e x))) ()) 470 466 ; ((+ (/> k (-r> h x)) (*> f (+> e x))) ()) 471 ; ((+ (-> h x) (/> f (+> e x))) ())472 ; ((+ (+> h x) (/> f (+> e x))) ())473 ; ((+ (/> h x) (/> f (+> e x))) ())474 ; ((+ (*> h x) (/> f (+> e x))) ())475 ; ((+ (-r> h x) (/> f (+> e x))) ())476 ; ((+ (/r> h x) (/> f (+> e x))) ())467 ; ((+ (-> h x) (/> f (+> e x))) ()) 468 ; ((+ (+> h x) (/> f (+> e x))) ()) 469 ; ((+ (/> h x) (/> f (+> e x))) ()) 470 ; ((+ (*> h x) (/> f (+> e x))) ()) 471 ; ((+ (-r> h x) (/> f (+> e x))) ()) 472 ; ((+ (/r> h x) (/> f (+> e x))) ()) 477 473 ; ((+ (/> k (-> h x)) (/> f (+> e x))) ()) 478 474 ; ((+ (/r> k (-> h x)) (/> f (+> e x))) ()) … … 482 478 ; ((+ (*> k (-r> h x)) (/> f (+> e x))) ()) 483 479 ; ((+ (/> k (-r> h x)) (/> f (+> e x))) ()) 484 ; ((+ (-> h x) (/r> f (+> e x))) ())485 ; ((+ (+> h x) (/r> f (+> e x))) ())486 ; ((+ (/> h x) (/r> f (+> e x))) ())487 ; ((+ (*> h x) (/r> f (+> e x))) ())488 ; ((+ (-r> h x) (/r> f (+> e x))) ())489 ; ((+ (/r> h x) (/r> f (+> e x))) ())480 ; ((+ (-> h x) (/r> f (+> e x))) ()) 481 ; ((+ (+> h x) (/r> f (+> e x))) ()) 482 ; ((+ (/> h x) (/r> f (+> e x))) ()) 483 ; ((+ (*> h x) (/r> f (+> e x))) ()) 484 ; ((+ (-r> h x) (/r> f (+> e x))) ()) 485 ; ((+ (/r> h x) (/r> f (+> e x))) ()) 490 486 ; ((+ (/> k (-> h x)) (/r> f (+> e x))) ()) 491 487 ; ((+ (/r> k (-> h x)) (/r> f (+> e x))) ()) … … 495 491 ; ((+ (*> k (-r> h x)) (/r> f (+> e x))) ()) 496 492 ; ((+ (/> k (-r> h x)) (/r> f (+> e x))) ()) 497 ; ((+ (-> h x) (*> f (-r> e x))) ())498 ; ((+ (+> h x) (*> f (-r> e x))) ())499 ; ((+ (/> h x) (*> f (-r> e x))) ())500 ; ((+ (*> h x) (*> f (-r> e x))) ())501 ; ((+ (-r> h x) (*> f (-r> e x))) ())502 ; ((+ (/r> h x) (*> f (-r> e x))) ())493 ; ((+ (-> h x) (*> f (-r> e x))) ()) 494 ; ((+ (+> h x) (*> f (-r> e x))) ()) 495 ; ((+ (/> h x) (*> f (-r> e x))) ()) 496 ; ((+ (*> h x) (*> f (-r> e x))) ()) 497 ; ((+ (-r> h x) (*> f (-r> e x))) ()) 498 ; ((+ (/r> h x) (*> f (-r> e x))) ()) 503 499 ; ((+ (/> k (-> h x)) (*> f (-r> e x))) ()) 504 500 ; ((+ (/r> k (-> h x)) (*> f (-r> e x))) ()) … … 508 504 ; ((+ (*> k (-r> h x)) (*> f (-r> e x))) ()) 509 505 ; ((+ (/> k (-r> h x)) (*> f (-r> e x))) ()) 510 ; ((+ (-> h x) (/> f (-r> e x))) ())511 ; ((+ (+> h x) (/> f (-r> e x))) ())512 ; ((+ (/> h x) (/> f (-r> e x))) ())513 ; ((+ (*> h x) (/> f (-r> e x))) ())514 ; ((+ (-r> h x) (/> f (-r> e x))) ())515 ; ((+ (/r> h x) (/> f (-r> e x))) ())506 ; ((+ (-> h x) (/> f (-r> e x))) ()) 507 ; ((+ (+> h x) (/> f (-r> e x))) ()) 508 ; ((+ (/> h x) (/> f (-r> e x))) ()) 509 ; ((+ (*> h x) (/> f (-r> e x))) ()) 510 ; ((+ (-r> h x) (/> f (-r> e x))) ()) 511 ; ((+ (/r> h x) (/> f (-r> e x))) ()) 516 512 ; ((+ (/> k (-> h x)) (/> f (-r> e x))) ()) 517 513 ; ((+ (/r> k (-> h x)) (/> f (-r> e x))) ()) … … 521 517 ; ((+ (*> k (-r> h x)) (/> f (-r> e x))) ()) 522 518 ; ((+ (/> k (-r> h x)) (/> f (-r> e x))) ()) 523 ; ((- (-> h x) (-> e x)) ()) 524 ; ((- (+> h x) (-> e x)) ()) 525 ; ((- (/> h x) (-> e x)) ()) 526 ; ((- (*> h x) (-> e x)) ()) 527 ; ((- (-r> h x) (-> e x)) ()) 528 ; ((- (/r> h x) (-> e x)) ()) 529 ; ((- (/> k (-> h x)) (-> e x)) ()) 530 ; ((- (/r> k (-> h x)) (-> e x)) ()) 531 ; ((- (*> k (+> h x)) (-> e x)) ()) 532 ; ((- (/> k (+> h x)) (-> e x)) ()) 533 ; ((- (/r> k (+> h x)) (-> e x)) ()) 534 ; ((- (*> k (-r> h x)) (-> e x)) ()) 535 ; ((- (/> k (-r> h x)) (-> e x)) ()) 536 ; ((- (-> h x) (+> e x)) ()) 537 ; ((- (+> h x) (+> e x)) ()) 538 ; ((- (/> h x) (+> e x)) ()) 539 ; ((- (*> h x) (+> e x)) ()) 540 ; ((- (-r> h x) (+> e x)) ()) 541 ; ((- (/r> h x) (+> e x)) ()) 542 ; ((- (/> k (-> h x)) (+> e x)) ()) 543 ; ((- (/r> k (-> h x)) (+> e x)) ()) 544 ; ((- (*> k (+> h x)) (+> e x)) ()) 545 ; ((- (/> k (+> h x)) (+> e x)) ()) 546 ; ((- (/r> k (+> h x)) (+> e x)) ()) 547 ; ((- (*> k (-r> h x)) (+> e x)) ()) 548 ; ((- (/> k (-r> h x)) (+> e x)) ()) 549 ; ((- (-> h x) (/> e x)) ()) 550 ; ((- (+> h x) (/> e x)) ()) 551 552 ((- (/> a b) (/> c b)) (/> (- a c) b)) 553 554 ; ((- (*> h x) (/> e x)) ()) 555 ; ((- (-r> h x) (/> e x)) ()) 556 ; ((- (/r> h x) (/> e x)) ()) 557 ; ((- (/> k (-> h x)) (/> e x)) ()) 558 ; ((- (/r> k (-> h x)) (/> e x)) ()) 559 ; ((- (*> k (+> h x)) (/> e x)) ()) 560 ; ((- (/> k (+> h x)) (/> e x)) ()) 561 ; ((- (/r> k (+> h x)) (/> e x)) ()) 562 ; ((- (*> k (-r> h x)) (/> e x)) ()) 563 ; ((- (/> k (-r> h x)) (/> e x)) ()) 564 ; ((- (-> h x) (*> e x)) ()) 565 ; ((- (+> h x) (*> e x)) ()) 566 ; ((- (/> h x) (*> e x)) ()) 567 ; ((- (*> h x) (*> e x)) ()) 568 ; ((- (-r> h x) (*> e x)) ()) 569 ; ((- (/r> h x) (*> e x)) ()) 570 ; ((- (/> k (-> h x)) (*> e x)) ()) 571 ; ((- (/r> k (-> h x)) (*> e x)) ()) 572 ; ((- (*> k (+> h x)) (*> e x)) ()) 573 ; ((- (/> k (+> h x)) (*> e x)) ()) 574 ; ((- (/r> k (+> h x)) (*> e x)) ()) 575 ; ((- (*> k (-r> h x)) (*> e x)) ()) 576 ; ((- (/> k (-r> h x)) (*> e x)) ()) 577 ; ((- (-> h x) (-r> e x)) ()) 578 ; ((- (+> h x) (-r> e x)) ()) 579 ; ((- (/> h x) (-r> e x)) ()) 580 ; ((- (*> h x) (-r> e x)) ()) 581 ; ((- (-r> h x) (-r> e x)) ()) 582 ; ((- (/r> h x) (-r> e x)) ()) 583 ; ((- (/> k (-> h x)) (-r> e x)) ()) 584 ; ((- (/r> k (-> h x)) (-r> e x)) ()) 585 ; ((- (*> k (+> h x)) (-r> e x)) ()) 586 ; ((- (/> k (+> h x)) (-r> e x)) ()) 587 ; ((- (/r> k (+> h x)) (-r> e x)) ()) 588 ; ((- (*> k (-r> h x)) (-r> e x)) ()) 589 ; ((- (/> k (-r> h x)) (-r> e x)) ()) 590 ; ((- (-> h x) (/r> e x)) ()) 591 ; ((- (+> h x) (/r> e x)) ()) 592 ; ((- (/> h x) (/r> e x)) ()) 593 ; ((- (*> h x) (/r> e x)) ()) 594 ; ((- (-r> h x) (/r> e x)) ()) 595 596 ((- (/r> a b) (/r> c b)) (/r> (- a c) b)) 597 598 ; ((- (/> k (-> h x)) (/r> e x)) ()) 599 ; ((- (/r> k (-> h x)) (/r> e x)) ()) 600 ; ((- (*> k (+> h x)) (/r> e x)) ()) 601 ; ((- (/> k (+> h x)) (/r> e x)) ()) 602 ; ((- (/r> k (+> h x)) (/r> e x)) ()) 603 ; ((- (*> k (-r> h x)) (/r> e x)) ()) 604 ; ((- (/> k (-r> h x)) (/r> e x)) ()) 605 ; ((- (-> h x) (/> f (-> e x))) ()) 606 ; ((- (+> h x) (/> f (-> e x))) ()) 607 ; ((- (/> h x) (/> f (-> e x))) ()) 608 ; ((- (*> h x) (/> f (-> e x))) ()) 609 ; ((- (-r> h x) (/> f (-> e x))) ()) 610 ; ((- (/r> h x) (/> f (-> e x))) ()) 611 ; ((- (/> k (-> h x)) (/> f (-> e x))) ()) 519 520 ; ((- (+> h x) (+> e x)) ()) 521 ; ((- (-> h x) (+> e x)) ()) 522 ; ((- (*> h x) (+> e x)) ()) 523 ; ((- (/> h x) (+> e x)) ()) 524 ; ((- (-r> h x) (+> e x)) ()) 525 ; ((- (/r> h x) (+> e x)) ()) 526 ; ((- (*> k (+> h x)) (+> e x)) ()) 527 ; ((- (*> k (-r> h x)) (+> e x)) ()) 528 ; ((- (/> k (+> h x)) (+> e x)) ()) 529 ; ((- (/> k (-> h x)) (+> e x)) ()) 530 ; ((- (/> k (-r> h x)) (+> e x)) ()) 531 ; ((- (/r> k (+> h x)) (+> e x)) ()) 532 ; ((- (/r> k (-> h x)) (+> e x)) ()) 533 534 ; ((- (+> h x) (-> e x)) ()) 535 ; ((- (-> h x) (-> e x)) ()) 536 ; ((- (*> h x) (-> e x)) ()) 537 ; ((- (/> h x) (-> e x)) ()) 538 ; ((- (-r> h x) (-> e x)) ()) 539 ; ((- (/r> h x) (-> e x)) ()) 540 ; ((- (*> k (+> h x)) (-> e x)) ()) 541 ; ((- (*> k (-r> h x)) (-> e x)) ()) 542 ; ((- (/> k (-r> h x)) (-> e x)) ()) 543 ; ((- (/> k (+> h x)) (-> e x)) ()) 544 ; ((- (/> k (-> h x)) (-> e x)) ()) 545 ; ((- (/r> k (-> h x)) (-> e x)) ()) 546 ; ((- (/r> k (+> h x)) (-> e x)) ()) 547 548 ; ((- (+> h x) (*> e x)) ()) 549 ; ((- (-> h x) (*> e x)) ()) 550 ; ((- (/> h x) (*> e x)) ()) 551 ; ((- (*> h x) (*> e x)) ()) 552 ; ((- (-r> h x) (*> e x)) ()) 553 ; ((- (/r> h x) (*> e x)) ()) 554 ; ((- (*> k (+> h x)) (*> e x)) ()) 555 ; ((- (*> k (-r> h x)) (*> e x)) ()) 556 ; ((- (/> k (+> h x)) (*> e x)) ()) 557 ; ((- (/> k (-> h x)) (*> e x)) ()) 558 ; ((- (/> k (-r> h x)) (*> e x)) ()) 559 ; ((- (/r> k (+> h x)) (*> e x)) ()) 560 ; ((- (/r> k (-> h x)) (*> e x)) ()) 561 562 ; ((- (-> h x) (/> e x)) ()) 563 ; ((- (+> h x) (/> e x)) ()) 564 ((- (/> a b) (/> c b)) (/> (- a c) b)) 565 ; ((- (*> h x) (/> e x)) ()) 566 ; ((- (-r> h x) (/> e x)) ()) 567 ; ((- (/r> h x) (/> e x)) ()) 568 ; ((- (/> k (-> h x)) (/> e x)) ()) 569 ; ((- (/r> k (-> h x)) (/> e x)) ()) 570 ; ((- (*> k (+> h x)) (/> e x)) ()) 571 ; ((- (/> k (+> h x)) (/> e x)) ()) 572 ; ((- (/r> k (+> h x)) (/> e x)) ()) 573 ; ((- (*> k (-r> h x)) (/> e x)) ()) 574 ; ((- (/> k (-r> h x)) (/> e x)) ()) 575 576 ; ((- (-> h x) (-r> e x)) ()) 577 ; ((- (+> h x) (-r> e x)) ()) 578 ; ((- (/> h x) (-r> e x)) ()) 579 ; ((- (*> h x) (-r> e x)) ()) 580 ; ((- (-r> h x) (-r> e x)) ()) 581 ; ((- (/r> h x) (-r> e x)) ()) 582 ; ((- (/> k (-> h x)) (-r> e x)) ()) 583 ; ((- (/r> k (-> h x)) (-r> e x)) ()) 584 ; ((- (*> k (+> h x)) (-r> e x)) ()) 585 ; ((- (/> k (+> h x)) (-r> e x)) ()) 586 ; ((- (/r> k (+> h x)) (-r> e x)) ()) 587 ; ((- (*> k (-r> h x)) (-r> e x)) ()) 588 ; ((- (/> k (-r> h x)) (-r> e x)) ()) 589 590 ; ((- (-> h x) (/r> e x)) ()) 591 ; ((- (+> h x) (/r> e x)) ()) 592 ; ((- (/> h x) (/r> e x)) ()) 593 ; ((- (*> h x) (/r> e x)) ()) 594 ; ((- (-r> h x) (/r> e x)) ()) 595 ((- (/r> a b) (/r> c b)) (/r> (- a c) b)) 596 597 ; ((- (/> k (-> h x)) (/r> e x)) ()) 598 ; ((- (/r> k (-> h x)) (/r> e x)) ()) 599 ; ((- (*> k (+> h x)) (/r> e x)) ()) 600 ; ((- (/> k (+> h x)) (/r> e x)) ()) 601 ; ((- (/r> k (+> h x)) (/r> e x)) ()) 602 ; ((- (*> k (-r> h x)) (/r> e x)) ()) 603 ; ((- (/> k (-r> h x)) (/r> e x)) ()) 604 605 ; ((- (-> h x) (/> f (-> e x))) ()) 606 ; ((- (+> h x) (/> f (-> e x))) ()) 607 ((- (/> h x) (/> f (-> e x))) (/> (- h f) (+> (/ (* e f) (- h f)) x))) 608 ; ((- (*> h x) (/> f (-> e x))) ()) 609 ; ((- (-r> h x) (/> f (-> e x))) ()) 610 ; ((- (/r> h x) (/> f (-> e x))) ()) 611 612 ; ((- (*> k (+> h x)) (/> f (-> e x))) ()) 613 ((- (*> a (-> e b)) (/> c (-> d b))) (/> (- (/ 1 a) c) (-> (/ (- (/ e a) (* d c)) (- (/ 1 a) c)) b))) 614 ; ((- (*> k (-r> h x)) (/> f (-> e x))) ()) 615 ; ((- (/> k (+> h x)) (/> f (-> e x))) ()) 616 ((- (/> k (-> h x)) (/> f (-> e x))) (/> (- k f) (-> (/ (- (* h k) (* e f)) (- k f)) x))) 617 ; ((- (/> k (-r> h x)) (/> f (-> e x))) ()) 618 ; ((- (/r> k (+> h x)) (/> f (-> e x))) ()) 612 619 ; ((- (/r> k (-> h x)) (/> f (-> e x))) ()) 613 ; ((- (*> k (+> h x)) (/> f (-> e x))) ()) 614 ; ((- (/> k (+> h x)) (/> f (-> e x))) ()) 615 ; ((- (/r> k (+> h x)) (/> f (-> e x))) ()) 616 ; ((- (*> k (-r> h x)) (/> f (-> e x))) ()) 617 ; ((- (/> k (-r> h x)) (/> f (-> e x))) ()) 618 ; ((- (-> h x) (/r> f (-> e x))) ()) 619 ; ((- (+> h x) (/r> f (-> e x))) ()) 620 ; ((- (/> h x) (/r> f (-> e x))) ()) 621 ; ((- (*> h x) (/r> f (-> e x))) ()) 622 ; ((- (-r> h x) (/r> f (-> e x))) ()) 623 ; ((- (/r> h x) (/r> f (-> e x))) ()) 620 621 ; ((- (-> h x) (/r> f (-> e x))) ()) 622 ; ((- (+> h x) (/r> f (-> e x))) ()) 623 ; ((- (/> h x) (/r> f (-> e x))) ()) 624 ; ((- (*> h x) (/r> f (-> e x))) ()) 625 ; ((- (-r> h x) (/r> f (-> e x))) ()) 626 ; ((- (/r> h x) (/r> f (-> e x))) ()) 624 627 ; ((- (/> k (-> h x)) (/r> f (-> e x))) ()) 625 628 ; ((- (/r> k (-> h x)) (/r> f (-> e x))) ()) … … 629 632 ; ((- (*> k (-r> h x)) (/r> f (-> e x))) ()) 630 633 ; ((- (/> k (-r> h x)) (/r> f (-> e x))) ()) 631 ; ((- (-> h x) (*> f (+> e x))) ())632 ; ((- (+> h x) (*> f (+> e x))) ())633 ; ((- (/> h x) (*> f (+> e x))) ())634 ; ((- (*> h x) (*> f (+> e x))) ())635 ; ((- (-r> h x) (*> f (+> e x))) ())636 ; ((- (/r> h x) (*> f (+> e x))) ())634 ; ((- (-> h x) (*> f (+> e x))) ()) 635 ; ((- (+> h x) (*> f (+> e x))) ()) 636 ; ((- (/> h x) (*> f (+> e x))) ()) 637 ; ((- (*> h x) (*> f (+> e x))) ()) 638 ; ((- (-r> h x) (*> f (+> e x))) ()) 639 ; ((- (/r> h x) (*> f (+> e x))) ()) 637 640 ; ((- (/> k (-> h x)) (*> f (+> e x))) ()) 638 641 ; ((- (/r> k (-> h x)) (*> f (+> e x))) ()) … … 642 645 ; ((- (*> k (-r> h x)) (*> f (+> e x))) ()) 643 646 ; ((- (/> k (-r> h x)) (*> f (+> e x))) ()) 644 ; ((- (-> h x) (/> f (+> e x))) ())645 ; ((- (+> h x) (/> f (+> e x))) ())646 ; ((- (/> h x) (/> f (+> e x))) ())647 ; ((- (*> h x) (/> f (+> e x))) ())648 ; ((- (-r> h x) (/> f (+> e x))) ())649 ; ((- (/r> h x) (/> f (+> e x))) ())647 ; ((- (-> h x) (/> f (+> e x))) ()) 648 ; ((- (+> h x) (/> f (+> e x))) ()) 649 ; ((- (/> h x) (/> f (+> e x))) (+> (* e f) (/> (- h f) x))) 650 ; ((- (*> h x) (/> f (+> e x))) ()) 651 ; ((- (-r> h x) (/> f (+> e x))) ()) 652 ; ((- (/r> h x) (/> f (+> e x))) ()) 650 653 ; ((- (/> k (-> h x)) (/> f (+> e x))) ()) 651 654 ; ((- (/r> k (-> h x)) (/> f (+> e x))) ()) … … 655 658 ; ((- (*> k (-r> h x)) (/> f (+> e x))) ()) 656 659 ; ((- (/> k (-r> h x)) (/> f (+> e x))) ()) 657 ; ((- (-> h x) (/r> f (+> e x))) ())658 ; ((- (+> h x) (/r> f (+> e x))) ())659 ; ((- (/> h x) (/r> f (+> e x))) ())660 ; ((- (*> h x) (/r> f (+> e x))) ())661 ; ((- (-r> h x) (/r> f (+> e x))) ())662 ; ((- (/r> h x) (/r> f (+> e x))) ())660 ; ((- (-> h x) (/r> f (+> e x))) ()) 661 ; ((- (+> h x) (/r> f (+> e x))) ()) 662 ; ((- (/> h x) (/r> f (+> e x))) ()) 663 ; ((- (*> h x) (/r> f (+> e x))) ()) 664 ; ((- (-r> h x) (/r> f (+> e x))) ()) 665 ; ((- (/r> h x) (/r> f (+> e x))) ()) 663 666 ; ((- (/> k (-> h x)) (/r> f (+> e x))) ()) 664 667 ; ((- (/r> k (-> h x)) (/r> f (+> e x))) ()) … … 668 671 ; ((- (*> k (-r> h x)) (/r> f (+> e x))) ()) 669 672 ; ((- (/> k (-r> h x)) (/r> f (+> e x))) ()) 670 ; ((- (-> h x) (*> f (-r> e x))) ())671 ; ((- (+> h x) (*> f (-r> e x))) ())672 ; ((- (/> h x) (*> f (-r> e x))) ())673 ; ((- (*> h x) (*> f (-r> e x))) ())674 ; ((- (-r> h x) (*> f (-r> e x))) ())675 ; ((- (/r> h x) (*> f (-r> e x))) ())673 ; ((- (-> h x) (*> f (-r> e x))) ()) 674 ; ((- (+> h x) (*> f (-r> e x))) ()) 675 ; ((- (/> h x) (*> f (-r> e x))) ()) 676 ; ((- (*> h x) (*> f (-r> e x))) ()) 677 ; ((- (-r> h x) (*> f (-r> e x))) ()) 678 ; ((- (/r> h x) (*> f (-r> e x))) ()) 676 679 ; ((- (/> k (-> h x)) (*> f (-r> e x))) ()) 677 680 ; ((- (/r> k (-> h x)) (*> f (-r> e x))) ()) … … 681 684 ; ((- (*> k (-r> h x)) (*> f (-r> e x))) ()) 682 685 ; ((- (/> k (-r> h x)) (*> f (-r> e x))) ()) 683 ; ((- (-> h x) (/> f (-r> e x))) ())684 ; ((- (+> h x) (/> f (-r> e x))) ())685 ; ((- (/> h x) (/> f (-r> e x))) ())686 ; ((- (*> h x) (/> f (-r> e x))) ())687 ; ((- (-r> h x) (/> f (-r> e x))) ())688 ; ((- (/r> h x) (/> f (-r> e x))) ())686 ; ((- (-> h x) (/> f (-r> e x))) ()) 687 ; ((- (+> h x) (/> f (-r> e x))) ()) 688 ; ((- (/> h x) (/> f (-r> e x))) ()) 689 ; ((- (*> h x) (/> f (-r> e x))) ()) 690 ; ((- (-r> h x) (/> f (-r> e x))) ()) 691 ; ((- (/r> h x) (/> f (-r> e x))) ()) 689 692 ; ((- (/> k (-> h x)) (/> f (-r> e x))) ()) 690 693 ; ((- (/r> k (-> h x)) (/> f (-r> e x))) ()) … … 694 697 ; ((- (*> k (-r> h x)) (/> f (-r> e x))) ()) 695 698 ; ((- (/> k (-r> h x)) (/> f (-r> e x))) ()) 696 ; ((* (-> h x) (-> e x)) ())697 ; ((* (+> h x) (-> e x)) ())698 ; ((* (/> h x) (-> e x)) ())699 ; ((* (*> h x) (-> e x)) ())700 ; ((* (-r> h x) (-> e x)) ())701 ; ((* (/r> h x) (-> e x)) ())702 ; ((* (/> k (-> h x)) (-> e x)) ())703 ; ((* (/r> k (-> h x)) (-> e x)) ())704 ; ((* (*> k (+> h x)) (-> e x)) ())705 ; ((* (/> k (+> h x)) (-> e x)) ())706 ; ((* (/r> k (+> h x)) (-> e x)) ())707 ; ((* (*> k (-r> h x)) (-> e x)) ())708 ; ((* (/> k (-r> h x)) (-> e x)) ())709 ; ((* (-> h x) (+> e x)) ())710 ; ((* (+> h x) (+> e x)) ())711 ; ((* (/> h x) (+> e x)) ())712 ; ((* (*> h x) (+> e x)) ())713 ; ((* (-r> h x) (+> e x)) ())714 ; ((* (/r> h x) (+> e x)) ())715 ; ((* (/> k (-> h x)) (+> e x)) ())716 ; ((* (/r> k (-> h x)) (+> e x)) ())717 ; ((* (*> k (+> h x)) (+> e x)) ())718 ; ((* (/> k (+> h x)) (+> e x)) ())719 ; ((* (/r> k (+> h x)) (+> e x)) ())720 ; ((* (*> k (-r> h x)) (+> e x)) ())721 ; ((* (/> k (-r> h x)) (+> e x)) ())722 ; ((* (-> h x) (/> e x)) ())723 ; ((* (+> h x) (/> e x)) ())724 ; ((* (/> h x) (/> e x)) ())725 ; ((* (*> h x) (/> e x)) ())726 ; ((* (-r> h x) (/> e x)) ())727 ; ((* (/r> h x) (/> e x)) ())728 ; ((* (/> k (-> h x)) (/> e x)) ())729 ; ((* (/r> k (-> h x)) (/> e x)) ())730 ; ((* (*> k (+> h x)) (/> e x)) ())731 ; ((* (/> k (+> h x)) (/> e x)) ())732 ; ((* (/r> k (+> h x)) (/> e x)) ())733 ; ((* (*> k (-r> h x)) (/> e x)) ())734 ; ((* (/> k (-r> h x)) (/> e x)) ())735 ; ((* (-> h x) (*> e x)) ())736 ; ((* (+> h x) (*> e x)) ())737 ; ((* (/> h x) (*> e x)) ())738 ; ((* (*> h x) (*> e x)) ())739 ; ((* (-r> h x) (*> e x)) ())740 ; ((* (/r> h x) (*> e x)) ())741 ; ((* (/> k (-> h x)) (*> e x)) ())742 ; ((* (/r> k (-> h x)) (*> e x)) ())743 ; ((* (*> k (+> h x)) (*> e x)) ())744 ; ((* (/> k (+> h x)) (*> e x)) ())745 ; ((* (/r> k (+> h x)) (*> e x)) ())746 ; ((* (*> k (-r> h x)) (*> e x)) ())747 ; ((* (/> k (-r> h x)) (*> e x)) ())748 ; ((* (-> h x) (-r> e x)) ())749 ; ((* (+> h x) (-r> e x)) ())750 ; ((* (/> h x) (-r> e x)) ())751 ; ((* (*> h x) (-r> e x)) ())752 ; ((* (-r> h x) (-r> e x)) ())753 ; ((* (/r> h x) (-r> e x)) ())754 ; ((* (/> k (-> h x)) (-r> e x)) ())755 ; ((* (/r> k (-> h x)) (-r> e x)) ())756 ; ((* (*> k (+> h x)) (-r> e x)) ())757 ; ((* (/> k (+> h x)) (-r> e x)) ())758 ; ((* (/r> k (+> h x)) (-r> e x)) ())759 ; ((* (*> k (-r> h x)) (-r> e x)) ())760 ; ((* (/> k (-r> h x)) (-r> e x)) ())761 ; ((* (-> h x) (/r> e x)) ())762 ; ((* (+> h x) (/r> e x)) ())763 ; ((* (/> h x) (/r> e x)) ())764 ; ((* (*> h x) (/r> e x)) ())765 ; ((* (-r> h x) (/r> e x)) ())766 ; ((* (/r> h x) (/r> e x)) ())767 ; ((* (/> k (-> h x)) (/r> e x)) ())768 ; ((* (/r> k (-> h x)) (/r> e x)) ())769 ; ((* (*> k (+> h x)) (/r> e x)) ())770 ; ((* (/> k (+> h x)) (/r> e x)) ())771 ; ((* (/r> k (+> h x)) (/r> e x)) ())772 ; ((* (*> k (-r> h x)) (/r> e x)) ())773 ; ((* (/> k (-r> h x)) (/r> e x)) ())774 ; ((* (-> h x) (/> f (-> e x))) ())775 ; ((* (+> h x) (/> f (-> e x))) ())776 ; ((* (/> h x) (/> f (-> e x))) ())777 ; ((* (*> h x) (/> f (-> e x))) ())778 ; ((* (-r> h x) (/> f (-> e x))) ())779 ; ((* (/r> h x) (/> f (-> e x))) ())699 ; ((* (-> h x) (-> e x)) ()) 700 ; ((* (+> h x) (-> e x)) ()) 701 ; ((* (/> h x) (-> e x)) ()) 702 ; ((* (*> h x) (-> e x)) ()) 703 ; ((* (-r> h x) (-> e x)) ()) 704 ; ((* (/r> h x) (-> e x)) ()) 705 ; ((* (/> k (-> h x)) (-> e x)) ()) 706 ; ((* (/r> k (-> h x)) (-> e x)) ()) 707 ; ((* (*> k (+> h x)) (-> e x)) ()) 708 ; ((* (/> k (+> h x)) (-> e x)) ()) 709 ; ((* (/r> k (+> h x)) (-> e x)) ()) 710 ; ((* (*> k (-r> h x)) (-> e x)) ()) 711 ; ((* (/> k (-r> h x)) (-> e x)) ()) 712 ; ((* (-> h x) (+> e x)) ()) 713 ; ((* (+> h x) (+> e x)) ()) 714 ; ((* (/> h x) (+> e x)) ()) 715 ; ((* (*> h x) (+> e x)) ()) 716 ; ((* (-r> h x) (+> e x)) ()) 717 ; ((* (/r> h x) (+> e x)) ()) 718 ; ((* (/> k (-> h x)) (+> e x)) ()) 719 ; ((* (/r> k (-> h x)) (+> e x)) ()) 720 ; ((* (*> k (+> h x)) (+> e x)) ()) 721 ; ((* (/> k (+> h x)) (+> e x)) ()) 722 ; ((* (/r> k (+> h x)) (+> e x)) ()) 723 ; ((* (*> k (-r> h x)) (+> e x)) ()) 724 ; ((* (/> k (-r> h x)) (+> e x)) ()) 725 ; ((* (-> h x) (/> e x)) ()) 726 ; ((* (+> h x) (/> e x)) ()) 727 ; ((* (/> h x) (/> e x)) ()) 728 ; ((* (*> h x) (/> e x)) ()) 729 ; ((* (-r> h x) (/> e x)) ()) 730 ; ((* (/r> h x) (/> e x)) ()) 731 ; ((* (/> k (-> h x)) (/> e x)) ()) 732 ; ((* (/r> k (-> h x)) (/> e x)) ()) 733 ; ((* (*> k (+> h x)) (/> e x)) ()) 734 ; ((* (/> k (+> h x)) (/> e x)) ()) 735 ; ((* (/r> k (+> h x)) (/> e x)) ()) 736 ; ((* (*> k (-r> h x)) (/> e x)) ()) 737 ; ((* (/> k (-r> h x)) (/> e x)) ()) 738 ; ((* (-> h x) (*> e x)) ()) 739 ; ((* (+> h x) (*> e x)) ()) 740 ; ((* (/> h x) (*> e x)) ()) 741 ; ((* (*> h x) (*> e x)) ()) 742 ; ((* (-r> h x) (*> e x)) ()) 743 ; ((* (/r> h x) (*> e x)) ()) 744 ; ((* (/> k (-> h x)) (*> e x)) ()) 745 ; ((* (/r> k (-> h x)) (*> e x)) ()) 746 ; ((* (*> k (+> h x)) (*> e x)) ()) 747 ; ((* (/> k (+> h x)) (*> e x)) ()) 748 ; ((* (/r> k (+> h x)) (*> e x)) ()) 749 ; ((* (*> k (-r> h x)) (*> e x)) ()) 750 ; ((* (/> k (-r> h x)) (*> e x)) ()) 751 ; ((* (-> h x) (-r> e x)) ()) 752 ; ((* (+> h x) (-r> e x)) ()) 753 ; ((* (/> h x) (-r> e x)) ()) 754 ; ((* (*> h x) (-r> e x)) ()) 755 ; ((* (-r> h x) (-r> e x)) ()) 756 ; ((* (/r> h x) (-r> e x)) ()) 757 ; ((* (/> k (-> h x)) (-r> e x)) ()) 758 ; ((* (/r> k (-> h x)) (-r> e x)) ()) 759 ; ((* (*> k (+> h x)) (-r> e x)) ()) 760 ; ((* (/> k (+> h x)) (-r> e x)) ()) 761 ; ((* (/r> k (+> h x)) (-r> e x)) ()) 762 ; ((* (*> k (-r> h x)) (-r> e x)) ()) 763 ; ((* (/> k (-r> h x)) (-r> e x)) ()) 764 ; ((* (-> h x) (/r> e x)) ()) 765 ; ((* (+> h x) (/r> e x)) ()) 766 ; ((* (/> h x) (/r> e x)) ()) 767 ; ((* (*> h x) (/r> e x)) ()) 768 ; ((* (-r> h x) (/r> e x)) ()) 769 ; ((* (/r> h x) (/r> e x)) ()) 770 ; ((* (/> k (-> h x)) (/r> e x)) ()) 771 ; ((* (/r> k (-> h x)) (/r> e x)) ()) 772 ; ((* (*> k (+> h x)) (/r> e x)) ()) 773 ; ((* (/> k (+> h x)) (/r> e x)) ()) 774 ; ((* (/r> k (+> h x)) (/r> e x)) ()) 775 ; ((* (*> k (-r> h x)) (/r> e x)) ()) 776 ; ((* (/> k (-r> h x)) (/r> e x)) ()) 777 ; ((* (-> h x) (/> f (-> e x))) ()) 778 ; ((* (+> h x) (/> f (-> e x))) ()) 779 ; ((* (/> h x) (/> f (-> e x))) ()) 780 ; ((* (*> h x) (/> f (-> e x))) ()) 781 ; ((* (-r> h x) (/> f (-> e x))) ()) 782 ; ((* (/r> h x) (/> f (-> e x))) ()) 780 783 ; ((* (/> k (-> h x)) (/> f (-> e x))) ()) 781 784 ; ((* (/r> k (-> h x)) (/> f (-> e x))) ()) … … 785 788 ; ((* (*> k (-r> h x)) (/> f (-> e x))) ()) 786 789 ; ((* (/> k (-r> h x)) (/> f (-> e x))) ()) 787 ; ((* (-> h x) (/r> f (-> e x))) ())788 ; ((* (+> h x) (/r> f (-> e x))) ())789 ; ((* (/> h x) (/r> f (-> e x))) ())790 ; ((* (*> h x) (/r> f (-> e x))) ())791 ; ((* (-r> h x) (/r> f (-> e x))) ())792 ; ((* (/r> h x) (/r> f (-> e x))) ())790 ; ((* (-> h x) (/r> f (-> e x))) ()) 791 ; ((* (+> h x) (/r> f (-> e x))) ()) 792 ; ((* (/> h x) (/r> f (-> e x))) ()) 793 ; ((* (*> h x) (/r> f (-> e x))) ()) 794 ; ((* (-r> h x) (/r> f (-> e x))) ()) 795 ; ((* (/r> h x) (/r> f (-> e x))) ()) 793 796 ; ((* (/> k (-> h x)) (/r> f (-> e x))) ()) 794 797 ; ((* (/r> k (-> h x)) (/r> f (-> e x))) ()) … … 798 801 ; ((* (*> k (-r> h x)) (/r> f (-> e x))) ()) 799 802 ; ((* (/> k (-r> h x)) (/r> f (-> e x))) ()) 800 ; ((* (-> h x) (*> f (+> e x))) ())801 ; ((* (+> h x) (*> f (+> e x))) ())802 ; ((* (/> h x) (*> f (+> e x))) ())803 ; ((* (*> h x) (*> f (+> e x))) ())804 ; ((* (-r> h x) (*> f (+> e x))) ())805 ; ((* (/r> h x) (*> f (+> e x))) ())803 ; ((* (-> h x) (*> f (+> e x))) ()) 804 ; ((* (+> h x) (*> f (+> e x))) ()) 805 ; ((* (/> h x) (*> f (+> e x))) ()) 806 ; ((* (*> h x) (*> f (+> e x))) ()) 807 ; ((* (-r> h x) (*> f (+> e x))) ()) 808 ; ((* (/r> h x) (*> f (+> e x))) ()) 806 809 ; ((* (/> k (-> h x)) (*> f (+> e x))) ()) 807 810 ; ((* (/r> k (-> h x)) (*> f (+> e x))) ()) … … 811 814 ; ((* (*> k (-r> h x)) (*> f (+> e x))) ()) 812 815 ; ((* (/> k (-r> h x)) (*> f (+> e x))) ()) 813 ; ((* (-> h x) (/> f (+> e x))) ())814 ; ((* (+> h x) (/> f (+> e x))) ())815 ; ((* (/> h x) (/> f (+> e x))) ())816 ; ((* (*> h x) (/> f (+> e x))) ())817 ; ((* (-r> h x) (/> f (+> e x))) ())818 ; ((* (/r> h x) (/> f (+> e x))) ())816 ; ((* (-> h x) (/> f (+> e x))) ()) 817 ; ((* (+> h x) (/> f (+> e x))) ()) 818 ; ((* (/> h x) (/> f (+> e x))) ()) 819 ; ((* (*> h x) (/> f (+> e x))) ()) 820 ; ((* (-r> h x) (/> f (+> e x))) ()) 821 ; ((* (/r> h x) (/> f (+> e x))) ()) 819 822 ; ((* (/> k (-> h x)) (/> f (+> e x))) ()) 820 823 ; ((* (/r> k (-> h x)) (/> f (+> e x))) ()) … … 824 827 ; ((* (*> k (-r> h x)) (/> f (+> e x))) ()) 825 828 ; ((* (/> k (-r> h x)) (/> f (+> e x))) ()) 826 ; ((* (-> h x) (/r> f (+> e x))) ())827 ; ((* (+> h x) (/r> f (+> e x))) ())828 ; ((* (/> h x) (/r> f (+> e x))) ())829 ; ((* (*> h x) (/r> f (+> e x))) ())830 ; ((* (-r> h x) (/r> f (+> e x))) ())831 ; ((* (/r> h x) (/r> f (+> e x))) ())829 ; ((* (-> h x) (/r> f (+> e x))) ()) 830 ; ((* (+> h x) (/r> f (+> e x))) ()) 831 ; ((* (/> h x) (/r> f (+> e x))) ()) 832 ; ((* (*> h x) (/r> f (+> e x))) ()) 833 ; ((* (-r> h x) (/r> f (+> e x))) ()) 834 ; ((* (/r> h x) (/r> f (+> e x))) ()) 832 835 ; ((* (/> k (-> h x)) (/r> f (+> e x))) ()) 833 836 ; ((* (/r> k (-> h x)) (/r> f (+> e x))) ()) … … 837 840 ; ((* (*> k (-r> h x)) (/r> f (+> e x))) ()) 838 841 ; ((* (/> k (-r> h x)) (/r> f (+> e x))) ()) 839 ; ((* (-> h x) (*> f (-r> e x))) ())840 ; ((* (+> h x) (*> f (-r> e x))) ())841 ; ((* (/> h x) (*> f (-r> e x))) ())842 ; ((* (*> h x) (*> f (-r> e x))) ())843 ; ((* (-r> h x) (*> f (-r> e x))) ())844 ; ((* (/r> h x) (*> f (-r> e x))) ())842 ; ((* (-> h x) (*> f (-r> e x))) ()) 843 ; ((* (+> h x) (*> f (-r> e x))) ()) 844 ; ((* (/> h x) (*> f (-r> e x))) ()) 845 ; ((* (*> h x) (*> f (-r> e x))) ()) 846 ; ((* (-r> h x) (*> f (-r> e x))) ()) 847 ; ((* (/r> h x) (*> f (-r> e x))) ()) 845 848 ; ((* (/> k (-> h x)) (*> f (-r> e x))) ()) 846 849 ; ((* (/r> k (-> h x)) (*> f (-r> e x))) ()) … … 850 853 ; ((* (*> k (-r> h x)) (*> f (-r> e x))) ()) 851 854 ; ((* (/> k (-r> h x)) (*> f (-r> e x))) ()) 852 ; ((* (-> h x) (/> f (-r> e x))) ())853 ; ((* (+> h x) (/> f (-r> e x))) ())854 ; ((* (/> h x) (/> f (-r> e x))) ())855 ; ((* (*> h x) (/> f (-r> e x))) ())856 ; ((* (-r> h x) (/> f (-r> e x))) ())857 ; ((* (/r> h x) (/> f (-r> e x))) ())855 ; ((* (-> h x) (/> f (-r> e x))) ()) 856 ; ((* (+> h x) (/> f (-r> e x))) ()) 857 ; ((* (/> h x) (/> f (-r> e x))) ()) 858 ; ((* (*> h x) (/> f (-r> e x))) ()) 859 ; ((* (-r> h x) (/> f (-r> e x))) ()) 860 ; ((* (/r> h x) (/> f (-r> e x))) ()) 858 861 ; ((* (/> k (-> h x)) (/> f (-r> e x))) ()) 859 862 ; ((* (/r> k (-> h x)) (/> f (-r> e x))) ()) … … 863 866 ; ((* (*> k (-r> h x)) (/> f (-r> e x))) ()) 864 867 ; ((* (/> k (-r> h x)) (/> f (-r> e x))) ()) 865 ; ((/ (-> h x) (-> e x)) ())866 ; ((/ (+> h x) (-> e x)) ())867 ; ((/ (/> h x) (-> e x)) ())868 ; ((/ (*> h x) (-> e x)) ())869 ; ((/ (-r> h x) (-> e x)) ())870 ; ((/ (/r> h x) (-> e x)) ())871 ; ((/ (/> k (-> h x)) (-> e x)) ())872 ; ((/ (/r> k (-> h x)) (-> e x)) ())873 ; ((/ (*> k (+> h x)) (-> e x)) ())874 ; ((/ (/> k (+> h x)) (-> e x)) ())875 ; ((/ (/r> k (+> h x)) (-> e x)) ())876 ; ((/ (*> k (-r> h x)) (-> e x)) ())877 ; ((/ (/> k (-r> h x)) (-> e x)) ())878 ; ((/ (-> h x) (+> e x)) ())879 ; ((/ (+> h x) (+> e x)) ())880 ; ((/ (/> h x) (+> e x)) ())881 ; ((/ (*> h x) (+> e x)) ())882 ; ((/ (-r> h x) (+> e x)) ())883 ; ((/ (/r> h x) (+> e x)) ())884 ; ((/ (/> k (-> h x)) (+> e x)) ())885 ; ((/ (/r> k (-> h x)) (+> e x)) ())886 ; ((/ (*> k (+> h x)) (+> e x)) ())887 ; ((/ (/> k (+> h x)) (+> e x)) ())888 ; ((/ (/r> k (+> h x)) (+> e x)) ())889 ; ((/ (*> k (-r> h x)) (+> e x)) ())890 ; ((/ (/> k (-r> h x)) (+> e x)) ())891 ; ((/ (-> h x) (/> e x)) ())892 ; ((/ (+> h x) (/> e x)) ())893 ; ((/ (/> h x) (/> e x)) ())894 ; ((/ (*> h x) (/> e x)) ())895 ; ((/ (-r> h x) (/> e x)) ())896 ; ((/ (/r> h x) (/> e x)) ())897 ; ((/ (/> k (-> h x)) (/> e x)) ())898 ; ((/ (/r> k (-> h x)) (/> e x)) ())899 ; ((/ (*> k (+> h x)) (/> e x)) ())900 ; ((/ (/> k (+> h x)) (/> e x)) ())901 ; ((/ (/r> k (+> h x)) (/> e x)) ())902 ; ((/ (*> k (-r> h x)) (/> e x)) ())903 ; ((/ (/> k (-r> h x)) (/> e x)) ())904 ; ((/ (-> h x) (*> e x)) ())905 ; ((/ (+> h x) (*> e x)) ())906 ; ((/ (/> h x) (*> e x)) ())907 ; ((/ (*> h x) (*> e x)) ())908 ; ((/ (-r> h x) (*> e x)) ())909 ; ((/ (/r> h x) (*> e x)) ())910 ; ((/ (/> k (-> h x)) (*> e x)) ())911 ; ((/ (/r> k (-> h x)) (*> e x)) ())912 ; ((/ (*> k (+> h x)) (*> e x)) ())913 ; ((/ (/> k (+> h x)) (*> e x)) ())914 ; ((/ (/r> k (+> h x)) (*> e x)) ())915 ; ((/ (*> k (-r> h x)) (*> e x)) ())916 ; ((/ (/> k (-r> h x)) (*> e x)) ())917 ; ((/ (-> h x) (-r> e x)) ())918 ; ((/ (+> h x) (-r> e x)) ())919 ; ((/ (/> h x) (-r> e x)) ())920 ; ((/ (*> h x) (-r> e x)) ())921 ; ((/ (-r> h x) (-r> e x)) ())922 ; ((/ (/r> h x) (-r> e x)) ())923 ; ((/ (/> k (-> h x)) (-r> e x)) ())924 ; ((/ (/r> k (-> h x)) (-r> e x)) ())925 ; ((/ (*> k (+> h x)) (-r> e x)) ())926 ; ((/ (/> k (+> h x)) (-r> e x)) ())927 ; ((/ (/r> k (+> h x)) (-r> e x)) ())928 ; ((/ (*> k (-r> h x)) (-r> e x)) ())929 ; ((/ (/> k (-r> h x)) (-r> e x)) ())930 ; ((/ (-> h x) (/r> e x)) ())931 ; ((/ (+> h x) (/r> e x)) ())932 ; ((/ (/> h x) (/r> e x)) ())933 ; ((/ (*> h x) (/r> e x)) ())934 ; ((/ (-r> h x) (/r> e x)) ())935 ; ((/ (/r> h x) (/r> e x)) ())936 ; ((/ (/> k (-> h x)) (/r> e x)) ())937 ; ((/ (/r> k (-> h x)) (/r> e x)) ())938 ; ((/ (*> k (+> h x)) (/r> e x)) ())939 ; ((/ (/> k (+> h x)) (/r> e x)) ())940 ; ((/ (/r> k (+> h x)) (/r> e x)) ())941 ; ((/ (*> k (-r> h x)) (/r> e x)) ())942 ; ((/ (/> k (-r> h x)) (/r> e x)) ())943 ; ((/ (-> h x) (/> f (-> e x))) ())944 ; ((/ (+> h x) (/> f (-> e x))) ())945 ; ((/ (/> h x) (/> f (-> e x))) ())946 ; ((/ (*> h x) (/> f (-> e x))) ())947 ; ((/ (-r> h x) (/> f (-> e x))) ())948 ; ((/ (/r> h x) (/> f (-> e x))) ())868 ; ((/ (-> h x) (-> e x)) ()) 869 ; ((/ (+> h x) (-> e x)) ()) 870 ; ((/ (/> h x) (-> e x)) ()) 871 ; ((/ (*> h x) (-> e x)) ()) 872 ; ((/ (-r> h x) (-> e x)) ()) 873 ; ((/ (/r> h x) (-> e x)) ()) 874 ; ((/ (/> k (-> h x)) (-> e x)) ()) 875 ; ((/ (/r> k (-> h x)) (-> e x)) ()) 876 ; ((/ (*> k (+> h x)) (-> e x)) ()) 877 ; ((/ (/> k (+> h x)) (-> e x)) ()) 878 ; ((/ (/r> k (+> h x)) (-> e x)) ()) 879 ; ((/ (*> k (-r> h x)) (-> e x)) ()) 880 ; ((/ (/> k (-r> h x)) (-> e x)) ()) 881 ; ((/ (-> h x) (+> e x)) ()) 882 ; ((/ (+> h x) (+> e x)) ()) 883 ; ((/ (/> h x) (+> e x)) ()) 884 ; ((/ (*> h x) (+> e x)) ()) 885 ; ((/ (-r> h x) (+> e x)) ()) 886 ; ((/ (/r> h x) (+> e x)) ()) 887 ; ((/ (/> k (-> h x)) (+> e x)) ()) 888 ; ((/ (/r> k (-> h x)) (+> e x)) ()) 889 ; ((/ (*> k (+> h x)) (+> e x)) ()) 890 ; ((/ (/> k (+> h x)) (+> e x)) ()) 891 ; ((/ (/r> k (+> h x)) (+> e x)) ()) 892 ; ((/ (*> k (-r> h x)) (+> e x)) ()) 893 ; ((/ (/> k (-r> h x)) (+> e x)) ()) 894 ; ((/ (-> h x) (/> e x)) ()) 895 ; ((/ (+> h x) (/> e x)) ()) 896 ; ((/ (/> h x) (/> e x)) ()) 897 ; ((/ (*> h x) (/> e x)) ()) 898 ; ((/ (-r> h x) (/> e x)) ()) 899 ; ((/ (/r> h x) (/> e x)) ()) 900 ; ((/ (/> k (-> h x)) (/> e x)) ()) 901 ; ((/ (/r> k (-> h x)) (/> e x)) ()) 902 ; ((/ (*> k (+> h x)) (/> e x)) ()) 903 ; ((/ (/> k (+> h x)) (/> e x)) ()) 904 ; ((/ (/r> k (+> h x)) (/> e x)) ()) 905 ; ((/ (*> k (-r> h x)) (/> e x)) ()) 906 ; ((/ (/> k (-r> h x)) (/> e x)) ()) 907 ; ((/ (-> h x) (*> e x)) ()) 908 ; ((/ (+> h x) (*> e x)) ()) 909 ; ((/ (/> h x) (*> e x)) ()) 910 ; ((/ (*> h x) (*> e x)) ()) 911 ; ((/ (-r> h x) (*> e x)) ()) 912 ; ((/ (/r> h x) (*> e x)) ()) 913 ; ((/ (/> k (-> h x)) (*> e x)) ()) 914 ; ((/ (/r> k (-> h x)) (*> e x)) ()) 915 ; ((/ (*> k (+> h x)) (*> e x)) ()) 916 ; ((/ (/> k (+> h x)) (*> e x)) ()) 917 ; ((/ (/r> k (+> h x)) (*> e x)) ()) 918 ; ((/ (*> k (-r> h x)) (*> e x)) ()) 919 ; ((/ (/> k (-r> h x)) (*> e x)) ()) 920 ; ((/ (-> h x) (-r> e x)) ()) 921 ; ((/ (+> h x) (-r> e x)) ()) 922 ; ((/ (/> h x) (-r> e x)) ()) 923 ; ((/ (*> h x) (-r> e x)) ()) 924 ; ((/ (-r> h x) (-r> e x)) ()) 925 ; ((/ (/r> h x) (-r> e x)) ()) 926 ; ((/ (/> k (-> h x)) (-r> e x)) ()) 927 ; ((/ (/r> k (-> h x)) (-r> e x)) ()) 928 ; ((/ (*> k (+> h x)) (-r> e x)) ()) 929 ; ((/ (/> k (+> h x)) (-r> e x)) ()) 930 ; ((/ (/r> k (+> h x)) (-r> e x)) ()) 931 ; ((/ (*> k (-r> h x)) (-r> e x)) ()) 932 ; ((/ (/> k (-r> h x)) (-r> e x)) ()) 933 ; ((/ (-> h x) (/r> e x)) ()) 934 ; ((/ (+> h x) (/r> e x)) ()) 935 ; ((/ (/> h x) (/r> e x)) ()) 936 ; ((/ (*> h x) (/r> e x)) ()) 937 ; ((/ (-r> h x) (/r> e x)) ()) 938 ; ((/ (/r> h x) (/r> e x)) ()) 939 ; ((/ (/> k (-> h x)) (/r> e x)) ()) 940 ; ((/ (/r> k (-> h x)) (/r> e x)) ()) 941 ; ((/ (*> k (+> h x)) (/r> e x)) ()) 942 ; ((/ (/> k (+> h x)) (/r> e x)) ()) 943 ; ((/ (/r> k (+> h x)) (/r> e x)) ()) 944 ; ((/ (*> k (-r> h x)) (/r> e x)) ()) 945 ; ((/ (/> k (-r> h x)) (/r> e x)) ()) 946 ; ((/ (-> h x) (/> f (-> e x))) ()) 947 ; ((/ (+> h x) (/> f (-> e x))) ()) 948 ; ((/ (/> h x) (/> f (-> e x))) ()) 949 ; ((/ (*> h x) (/> f (-> e x))) ()) 950 ; ((/ (-r> h x) (/> f (-> e x))) ()) 951 ; ((/ (/r> h x) (/> f (-> e x))) ()) 949 952 ; ((/ (/> k (-> h x)) (/> f (-> e x))) ()) 950 953 ; ((/ (/r> k (-> h x)) (/> f (-> e x))) ()) … … 954 957 ; ((/ (*> k (-r> h x)) (/> f (-> e x))) ()) 955 958 ; ((/ (/> k (-r> h x)) (/> f (-> e x))) ()) 956 ; ((/ (-> h x) (/r> f (-> e x))) ())957 ; ((/ (+> h x) (/r> f (-> e x))) ())958 ; ((/ (/> h x) (/r> f (-> e x))) ())959 ; ((/ (*> h x) (/r> f (-> e x))) ())960 ; ((/ (-r> h x) (/r> f (-> e x))) ())961 ; ((/ (/r> h x) (/r> f (-> e x))) ())959 ; ((/ (-> h x) (/r> f (-> e x))) ()) 960 ; ((/ (+> h x) (/r> f (-> e x))) ()) 961 ; ((/ (/> h x) (/r> f (-> e x))) ()) 962 ; ((/ (*> h x) (/r> f (-> e x))) ()) 963 ; ((/ (-r> h x) (/r> f (-> e x))) ()) 964 ; ((/ (/r> h x) (/r> f (-> e x))) ()) 962 965 ; ((/ (/> k (-> h x)) (/r> f (-> e x))) ()) 963 966 ; ((/ (/r> k (-> h x)) (/r> f (-> e x))) ()) … … 967 970 ; ((/ (*> k (-r> h x)) (/r> f (-> e x))) ()) 968 971 ; ((/ (/> k (-r> h x)) (/r> f (-> e x))) ()) 969 ; ((/ (-> h x) (*> f (+> e x))) ())970 ; ((/ (+> h x) (*> f (+> e x))) ())971 ; ((/ (/> h x) (*> f (+> e x))) ())972 ; ((/ (*> h x) (*> f (+> e x))) ())973 ; ((/ (-r> h x) (*> f (+> e x))) ())974 ; ((/ (/r> h x) (*> f (+> e x))) ())972 ; ((/ (-> h x) (*> f (+> e x))) ()) 973 ; ((/ (+> h x) (*> f (+> e x))) ()) 974 ; ((/ (/> h x) (*> f (+> e x))) ()) 975 ; ((/ (*> h x) (*> f (+> e x))) ()) 976 ; ((/ (-r> h x) (*> f (+> e x))) ()) 977 ; ((/ (/r> h x) (*> f (+> e x))) ()) 975 978 ; ((/ (/> k (-> h x)) (*> f (+> e x))) ()) 976 979 ; ((/ (/r> k (-> h x)) (*> f (+> e x))) ()) … … 980 983 ; ((/ (*> k (-r> h x)) (*> f (+> e x))) ()) 981 984 ; ((/ (/> k (-r> h x)) (*> f (+> e x))) ()) 982 ; ((/ (-> h x) (/> f (+> e x))) ())983 ; ((/ (+> h x) (/> f (+> e x))) ())984 ; ((/ (/> h x) (/> f (+> e x))) ())985 ; ((/ (*> h x) (/> f (+> e x))) ())986 ; ((/ (-r> h x) (/> f (+> e x))) ())987 ; ((/ (/r> h x) (/> f (+> e x))) ())985 ; ((/ (-> h x) (/> f (+> e x))) ()) 986 ; ((/ (+> h x) (/> f (+> e x))) ()) 987 ; ((/ (/> h x) (/> f (+> e x))) ()) 988 ; ((/ (*> h x) (/> f (+> e x))) ()) 989 ; ((/ (-r> h x) (/> f (+> e x))) ()) 990 ; ((/ (/r> h x) (/> f (+> e x))) ()) 988 991 ; ((/ (/> k (-> h x)) (/> f (+> e x))) ()) 989 992 ; ((/ (/r> k (-> h x)) (/> f (+> e x))) ()) … … 993 996 ; ((/ (*> k (-r> h x)) (/> f (+> e x))) ()) 994 997 ; ((/ (/> k (-r> h x)) (/> f (+> e x))) ()) 995 ; ((/ (-> h x) (/r> f (+> e x))) ())996 ; ((/ (+> h x) (/r> f (+> e x))) ())997 ; ((/ (/> h x) (/r> f (+> e x))) ())998 ; ((/ (*> h x) (/r> f (+> e x))) ())999 ; ((/ (-r> h x) (/r> f (+> e x))) ())1000 ; ((/ (/r> h x) (/r> f (+> e x))) ())998 ; ((/ (-> h x) (/r> f (+> e x))) ()) 999 ; ((/ (+> h x) (/r> f (+> e x))) ()) 1000 ; ((/ (/> h x) (/r> f (+> e x))) ()) 1001 ; ((/ (*> h x) (/r> f (+> e x))) ()) 1002 ; ((/ (-r> h x) (/r> f (+> e x))) ()) 1003 ; ((/ (/r> h x) (/r> f (+> e x))) ()) 1001 1004 ; ((/ (/> k (-> h x)) (/r> f (+> e x))) ()) 1002 1005 ; ((/ (/r> k (-> h x)) (/r> f (+> e x))) ()) … … 1006 1009 ; ((/ (*> k (-r> h x)) (/r> f (+> e x))) ()) 1007 1010 ; ((/ (/> k (-r> h x)) (/r> f (+> e x))) ()) 1008 ; ((/ (-> h x) (*> f (-r> e x))) ())1009 ; ((/ (+> h x) (*> f (-r> e x))) ())1010 ; ((/ (/> h x) (*> f (-r> e x))) ())1011 ; ((/ (*> h x) (*> f (-r> e x))) ())1012 ; ((/ (-r> h x) (*> f (-r> e x))) ())1013 ; ((/ (/r> h x) (*> f (-r> e x))) ())1011 ; ((/ (-> h x) (*> f (-r> e x))) ()) 1012 ; ((/ (+> h x) (*> f (-r> e x))) ()) 1013 ; ((/ (/> h x) (*> f (-r> e x))) ()) 1014 ; ((/ (*> h x) (*> f (-r> e x))) ()) 1015 ; ((/ (-r> h x) (*> f (-r> e x))) ()) 1016 ; ((/ (/r> h x) (*> f (-r> e x))) ()) 1014 1017 ; ((/ (/> k (-> h x)) (*> f (-r> e x))) ()) 1015 1018 ; ((/ (/r> k (-> h x)) (*> f (-r> e x))) ()) … … 1019 1022 ; ((/ (*> k (-r> h x)) (*> f (-r> e x))) ()) 1020 1023 ; ((/ (/> k (-r> h x)) (*> f (-r> e x))) ()) 1021 ; ((/ (-> h x) (/> f (-r> e x))) ())1022 ; ((/ (+> h x) (/> f (-r> e x))) ())1023 ; ((/ (/> h x) (/> f (-r> e x))) ())1024 ; ((/ (*> h x) (/> f (-r> e x))) ())1025 ; ((/ (-r> h x) (/> f (-r> e x))) ())1026 ; ((/ (/r> h x) (/> f (-r> e x))) ())1024 ; ((/ (-> h x) (/> f (-r> e x))) ()) 1025 ; ((/ (+> h x) (/> f (-r> e x))) ()) 1026 ; ((/ (/> h x) (/> f (-r> e x))) ()) 1027 ; ((/ (*> h x) (/> f (-r> e x))) ()) 1028 ; ((/ (-r> h x) (/> f (-r> e x))) ()) 1029 ; ((/ (/r> h x) (/> f (-r> e x))) ()) 1027 1030 ; ((/ (/> k (-> h x)) (/> f (-r> e x))) ()) 1028 1031 ; ((/ (/r> k (-> h x)) (/> f (-r> e x))) ()) … … 1032 1035 ; ((/ (*> k (-r> h x)) (/> f (-r> e x))) ()) 1033 1036 ; ((/ (/> k (-r> h x)) (/> f (-r> e x))) ()) 1034 ; ((+ (*> a (-> b x)) x) ())1035 ; ((+ x (*> a (-> b x))) ())1036 ; ((- (*> a (-> b x)) x) ())1037 ; ((- x (*> a (-> b x))) ())1038 ; ((* (*> a (-> b x)) x) ())1039 ; ((* x (*> a (-> b x))) ())1040 ; ((/ x (*> a (-> b x))) ())1041 ; ((/ (*> a (-> b x)) x) ())1042 ; ((+ (*> a (-> b x)) (-> e x)) ())1043 ; ((+ (*> a (-> b x)) (+> e x)) ())1044 ; ((+ (*> a (-> b x)) (/> e x)) ())1045 ; ((+ (*> a (-> b x)) (*> e x)) ())1046 ; ((+ (*> a (-> b x)) (-r> e x)) ())1047 ; ((+ (*> a (-> b x)) (/r> e x)) ())1048 ; ((+ (-> h x) (*> a (-> b x))) ())1049 ; ((+ (+> h x) (*> a (-> b x))) ())1050 ; ((+ (/> h x) (*> a (-> b x))) ())1051 ; ((+ (*> h x) (*> a (-> b x))) ())1052 ; ((+ (-r> h x) (*> a (-> b x))) ())1053 ; ((+ (/r> h x) (*> a (-> b x))) ())1037 ; ((+ (*> a (-> b x)) x) ()) 1038 ; ((+ x (*> a (-> b x))) ()) 1039 ; ((- (*> a (-> b x)) x) ()) 1040 ; ((- x (*> a (-> b x))) ()) 1041 ; ((* (*> a (-> b x)) x) ()) 1042 ; ((* x (*> a (-> b x))) ()) 1043 ; ((/ x (*> a (-> b x))) ()) 1044 ; ((/ (*> a (-> b x)) x) ()) 1045 ; ((+ (*> a (-> b x)) (-> e x)) ()) 1046 ; ((+ (*> a (-> b x)) (+> e x)) ()) 1047 ; ((+ (*> a (-> b x)) (/> e x)) ()) 1048 ; ((+ (*> a (-> b x)) (*> e x)) ()) 1049 ; ((+ (*> a (-> b x)) (-r> e x)) ()) 1050 ; ((+ (*> a (-> b x)) (/r> e x)) ()) 1051 ; ((+ (-> h x) (*> a (-> b x))) ()) 1052 ; ((+ (+> h x) (*> a (-> b x))) ()) 1053 ; ((+ (/> h x) (*> a (-> b x))) ()) 1054 ; ((+ (*> h x) (*> a (-> b x))) ()) 1055 ; ((+ (-r> h x) (*> a (-> b x))) ()) 1056 ; ((+ (/r> h x) (*> a (-> b x))) ()) 1054 1057 ; ((+ (*> a (-> b x)) (*> a (-> b x))) ()) 1055 1058 ; ((+ (/> k (-> h x)) (*> a (-> b x))) ()) … … 1067 1070 ; ((+ (*> a (-> b x)) (*> f (-r> e x))) ()) 1068 1071 ; ((+ (*> a (-> b x)) (/> f (-r> e x))) ()) 1069 ; ((- (*> a (-> b x)) (-> e x)) ())1070 ; ((- (*> a (-> b x)) (+> e x)) ())1071 ; ((- (*> a (-> b x)) (/> e x)) ())1072 ; ((- (*> a (-> b x)) (*> e x)) ())1073 ; ((- (*> a (-> b x)) (-r> e x)) ())1074 ; ((- (*> a (-> b x)) (/r> e x)) ())1075 ; ((- (-> h x) (*> a (-> b x))) ())1076 ; ((- (+> h x) (*> a (-> b x))) ())1077 ; ((- (/> h x) (*> a (-> b x))) ())1078 ; ((- (*> h x) (*> a (-> b x))) ())1079 ; ((- (-r> h x) (*> a (-> b x))) ())1080 ; ((- (/r> h x) (*> a (-> b x))) ())1072 ; ((- (*> a (-> b x)) (-> e x)) ()) 1073 ; ((- (*> a (-> b x)) (+> e x)) ()) 1074 ; ((- (*> a (-> b x)) (/> e x)) ()) 1075 ; ((- (*> a (-> b x)) (*> e x)) ()) 1076 ; ((- (*> a (-> b x)) (-r> e x)) ()) 1077 ; ((- (*> a (-> b x)) (/r> e x)) ()) 1078 ; ((- (-> h x) (*> a (-> b x))) ()) 1079 ; ((- (+> h x) (*> a (-> b x))) ()) 1080 ; ((- (/> h x) (*> a (-> b x))) ()) 1081 ((- (*> h x) (*> a (-> b x))) (+> (/ b a) (/> (- (/ 1 h) (/ 1 a)) x))) 1082 ; ((- (-r> h x) (*> a (-> b x))) ()) 1083 ; ((- (/r> h x) (*> a (-> b x))) ()) 1081 1084 ; ((- (*> a (-> b x)) (*> a (-> b x))) ()) 1082 1085 ; ((- (/> k (-> h x)) (*> a (-> b x))) ()) … … 1094 1097 ; ((- (*> a (-> b x)) (*> f (-r> e x))) ()) 1095 1098 ; ((- (*> a (-> b x)) (/> f (-r> e x))) ()) 1096 ; ((* (*> a (-> b x)) (-> e x)) ())1097 ; ((* (*> a (-> b x)) (+> e x)) ())1098 ; ((* (*> a (-> b x)) (/> e x)) ())1099 ; ((* (*> a (-> b x)) (*> e x)) ())1100 ; ((* (*> a (-> b x)) (-r> e x)) ())1101 ; ((* (*> a (-> b x)) (/r> e x)) ())1102 ; ((* (-> h x) (*> a (-> b x))) ())1103 ; ((* (+> h x) (*> a (-> b x))) ())1104 ; ((* (/> h x) (*> a (-> b x))) ())1105 ; ((* (*> h x) (*> a (-> b x))) ())1106 ; ((* (-r> h x) (*> a (-> b x))) ())1107 ; ((* (/r> h x) (*> a (-> b x))) ())1099 ; ((* (*> a (-> b x)) (-> e x)) ()) 1100 ; ((* (*> a (-> b x)) (+> e x)) ()) 1101 ; ((* (*> a (-> b x)) (/> e x)) ()) 1102 ; ((* (*> a (-> b x)) (*> e x)) ()) 1103 ; ((* (*> a (-> b x)) (-r> e x)) ()) 1104 ; ((* (*> a (-> b x)) (/r> e x)) ()) 1105 ; ((* (-> h x) (*> a (-> b x))) ()) 1106 ; ((* (+> h x) (*> a (-> b x))) ()) 1107 ; ((* (/> h x) (*> a (-> b x))) ()) 1108 ; ((* (*> h x) (*> a (-> b x))) ()) 1109 ; ((* (-r> h x) (*> a (-> b x))) ()) 1110 ; ((* (/r> h x) (*> a (-> b x))) ()) 1108 1111 ; ((* (*> a (-> b x)) (*> a (-> b x))) ()) 1109 1112 ; ((* (/> k (-> h x)) (*> a (-> b x))) ()) … … 1121 1124 ; ((* (*> a (-> b x)) (*> f (-r> e x))) ()) 1122 1125 ; ((* (*> a (-> b x)) (/> f (-r> e x))) ()) 1123 ; ((/ (*> a (-> b x)) (-> e x)) ())1124 ; ((/ (*> a (-> b x)) (+> e x)) ())1125 ; ((/ (*> a (-> b x)) (/> e x)) ())1126 ; ((/ (*> a (-> b x)) (*> e x)) ())1127 ; ((/ (*> a (-> b x)) (-r> e x)) ())1128 ; ((/ (*> a (-> b x)) (/r> e x)) ())1129 ; ((/ (-> h x) (*> a (-> b x))) ())1130 ; ((/ (+> h x) (*> a (-> b x))) ())1131 ; ((/ (/> h x) (*> a (-> b x))) ())1132 ; ((/ (*> h x) (*> a (-> b x))) ())1133 ; ((/ (-r> h x) (*> a (-> b x))) ())1134 ; ((/ (/r> h x) (*> a (-> b x))) ())1126 ; ((/ (*> a (-> b x)) (-> e x)) ()) 1127 ; ((/ (*> a (-> b x)) (+> e x)) ()) 1128 ; ((/ (*> a (-> b x)) (/> e x)) ()) 1129 ; ((/ (*> a (-> b x)) (*> e x)) ()) 1130 ; ((/ (*> a (-> b x)) (-r> e x)) ()) 1131 ; ((/ (*> a (-> b x)) (/r> e x)) ()) 1132 ; ((/ (-> h x) (*> a (-> b x))) ()) 1133 ; ((/ (+> h x) (*> a (-> b x))) ()) 1134 ; ((/ (/> h x) (*> a (-> b x))) ()) 1135 ; ((/ (*> h x) (*> a (-> b x))) ()) 1136 ; ((/ (-r> h x) (*> a (-> b x))) ()) 1137 ; ((/ (/r> h x) (*> a (-> b x))) ()) 1135 1138 ; ((/ (*> a (-> b x)) (*> a (-> b x))) ()) 1136 1139 ; ((/ (/> k (-> h x)) (*> a (-> b x))) ()) … … 1148 1151 ; ((/ (*> a (-> b x)) (*> f (-r> e x))) ()) 1149 1152 ; ((/ (*> a (-> b x)) (/> f (-r> e x))) ()) 1150 1151 ((- (*> A B) (*> C (-> (* D C) B))) (+> D (/> (- (/ 1 A) (/ 1 C)) B ))) 1152 ((- (/> A B) (/> C (+> (/ D C) B))) (+> D (/> (- A C) B))) 1153 |# 1153 ;| # 1154 1154 ) 1155 1155 ) trunk/backmath/string_stuff.lisp
r173 r174 23 23 ) 24 24 25 (defun op_symb (a) 26 (cond 27 ((equal a '+) "+") 28 ((equal a '-) "-") 29 ((equal a '*) "*") 30 ((equal a '/) "/") 31 ((equal a '+>) "+>") 32 ((equal a '->) "->") 33 ((equal a '*>) "*>") 34 ((equal a '/>) "/>") 35 ((equal a '-r>) "-r>") 36 ((equal a '/r>) "/r>") 37 (t "%invlaid%") 38 ) 39 ) 40 25 41 ;;; ?New-line constant 26 42 (DEFCONSTANT nl "
