Changeset 174

Show
Ignore:
Timestamp:
12/28/07 19:43:51 (4 years ago)
Author:
BCS
Message:

a few more cases in meta.lisp
a MAJOR fix in generate_case.lisp (it would generate bad code)
comment here and there

Files:

Legend:

Unmodified
Added
Removed
Modified
Copied
Moved
  • trunk/backmath/backmath.d

    r173 r174  
    44    Author: Benjamin Shropshire 
    55 
    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. 
    790 
    891    Version: 0.001 
     
    1194 
    1295import 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 */ 
     109template 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 
     120template decimaldigit(int n) { const char [] decimaldigit = "0123456789"[n..n+1]; } 
     121 
     122/* ***************************************************** 
     123 *  char [] itoa!(long n); 
     124 */ 
     125template 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 
    13138 
    14139// symboles for is(Type == Type) tests 
     
    68193 
    69194template 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 
     195struct 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
     202struct 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
     209struct 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 
     217struct 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
     224struct 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
     231struct 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
     238struct 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 
     246struct 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
     253struct 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
     260struct 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
     267struct 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
     274struct 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
     281struct 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 
     290real a, b, c, d, e, f, g; 
     291 
     292void main(){Unittest();} 
     293 
     294 
     295//unittest 
     296void Unittest() 
    92297{ 
    93298    DefinedT!(a)   A; 
     299    UnDefinedT!(b) B; 
    94300    DefinedT!(c)   C; 
    95301    DefinedT!(d)   D; 
    96     UnDefinedT!(b) B; 
     302    DefinedT!(e)   E; 
     303    DefinedT!(f)   F; 
     304    DefinedT!(g)   G; 
    97305 
    98306    a=1; 
     
    134342    writef("%s == -18\n", b); 
    135343 
     344    (B * A) + E = (B * C) + D; 
     345    (B / A) + E = (B * C) + D; 
     346//  (B * A) + E = (B / C) + D; 
     347 
    136348    (B * A) = (B * C) + D; // B * 3 = B * 2 + 3; -> 3 
    137349    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  
    55;;; load rule set 
    66(load "meta.lisp") 
     7 
     8;;;;;;;;;;; set this to true to make backmath emit compile time debuggin info 
     9(DEFCONSTANT verbose nil) 
    710 
    811;; Convert (OP (rules...)) into a text implementation 
     
    1922            "{"  nl  
    2023            (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            ) 
    2237            "}"  nl  
    2338        ) 
  • trunk/backmath/generate_case.lisp

    r173 r174  
    1010;   (print (list 'type_K type)) 
    1111;   (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)) 
    2634                        ) 
    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))             
    2847                    ) 
    29                     ( 
    30                         (or 
    31                             (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)) 
    4148                ) 
    4249            ) 
     
    5764;   (print (list 'type_U type)) 
    5865;   (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)) 
    7388                        ) 
    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))             
    75101                    ) 
    76                     ( 
    77                         (or 
    78                             (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%%") 
    88102                ) 
    89103            ) 
  • trunk/backmath/generated_rules.d

    r173 r174  
    11template TypeOfAdd(T, V) 
    22{ 
     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 
    310    static if( // (+ (/> A B) (/> C B)) -> (/> (+ A C) B) 
    411        is(T.Op == DivA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 
     
    916    else 
    1017    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) && 
    1219        is(V.DefP == Defined) 
    1320         /+ no repeats +/ 
     
    1623    else 
    1724    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) && 
    1926        is(V.DefP == UnDefined) 
    2027         && is(T.RHS.RHS == V) 
     
    2229        alias OpDivA!(OpAdd!(T.LHS, Value!(1)), OpSubA!(OpDiv!(OpMul!(T.RHS.LHS, T.LHS), OpAdd!(T.LHS, Value!(1))), T.RHS.RHS)) TypeOfAdd; 
    2330    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 
    2494    static if( // (+ C (*> A (-R> B X))) -> (*> A (-R> (+ B (* C A)) X)) 
    2595        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) 
    2797         /+ no repeats +/ 
    2898        )  
     
    31101    static if( // (+ C (*> A (+> B X))) -> (*> A (+> (- B (* C A)) X)) 
    32102        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) 
    34104         /+ no repeats +/ 
    35105        )  
     
    38108    static if( // (+ C (*> A (-> B X))) -> (*> A (-> (+ (* C A) B) X)) 
    39109        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) 
    41111         /+ no repeats +/ 
    42112        )  
     
    57127        alias OpDivA!(OpAdd!(OpDiv!(Value!(1), V.LHS), Value!(1)), T) TypeOfAdd; 
    58128    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) 
    90139         && is(T == V.RHS) 
    91140        )  
    92         alias OpDivA!(OpAdd!(Value!(1), V.LHS), T) TypeOfAdd; 
     141        alias OpDivA!(Value!(2), OpSubA!(OpDiv!(V.LHS, Value!(2)), T)) TypeOfAdd; 
    93142    else 
    94143    static if( // (+ A (+> B X)) -> (+> (- B A) X) 
     
    106155        alias OpDivA!(Value!(2), OpAddA!(OpDiv!(V.LHS, Value!(2)), T)) TypeOfAdd; 
    107156    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; 
    121177    else 
    122178    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) && 
    124180        is(V.DefP == Defined) 
    125181         /+ no repeats +/ 
     
    127183        alias OpMulA!(T.LHS, OpSubAR!(OpAdd!(T.RHS.LHS, OpMul!(V, T.LHS)), T.RHS.RHS)) TypeOfAdd; 
    128184    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     else 
    136185    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) && 
    138187        is(V.DefP == Defined) 
    139188         /+ no repeats +/ 
     
    155204        alias OpDivA!(OpAdd!(OpDiv!(Value!(1), T.LHS), Value!(1)), T.RHS) TypeOfAdd; 
    156205    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) && 
    180215        is(V.DefP == UnDefined) 
    181216         && is(T.RHS == V) 
    182217        )  
    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; 
    184219    else 
    185220    static if( // (+ (+> B X) A) -> (+> (- B A) X) 
     
    197232        alias OpDivA!(Value!(2), OpAddA!(OpDiv!(T.LHS, Value!(2)), T.RHS)) TypeOfAdd; 
    198233    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     else 
    206     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     else 
    213234    static if( // (+ (-R> B X) A) -> (-R> (+ A B) X) 
    214235        is(T.Op == SubAR) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 
     
    253274        alias OpDivA!(Value!(2), T) TypeOfAdd; 
    254275    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 ~ `)` ); 
    256279} 
    257280template TypeOfSub(T, V) 
    258281{ 
     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 
    259324    static if( // (- A (-R> B X)) -> (+> (- B A) X) 
    260325        is(T.DefP == Defined) && 
     
    271336        alias OpDivA!(Value!(2), OpAddA!(OpDiv!(V.LHS, Value!(2)), T)) TypeOfSub; 
    272337    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 
    273373    static if( // (- C (*> A (-R> B X))) -> (*> A (+> (- B (* C A)) X)) 
    274374        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) 
    276376         /+ no repeats +/ 
    277377        )  
     
    280380    static if( // (- C (*> A (+> B X))) -> (*> A (-R> (+ (* C A) B) X)) 
    281381        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) 
    283383         /+ no repeats +/ 
    284384        )  
     
    287387    static if( // (- C (*> A (-> B X))) -> (*> A (-R> (- (* A C) B) X)) 
    288388        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) 
    290390         /+ no repeats +/ 
    291391        )  
     
    306406        alias OpDivA!(OpSub!(Value!(1), OpDiv!(Value!(1), V.LHS)), T) TypeOfSub; 
    307407    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     else 
    315     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     else 
    322     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     else 
    329     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     else 
    336     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     else 
    343408    static if( // (- (-R> B X) A) -> (-R> (- B A) X) 
    344409        is(T.Op == SubAR) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 
     
    355420        alias OpDivA!(Value!(2), OpSubAR!(OpDiv!(T.LHS, Value!(2)), T.RHS)) TypeOfSub; 
    356421    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 
    357457    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) && 
    359459        is(V.DefP == Defined) 
    360460         /+ no repeats +/ 
     
    363463    else 
    364464    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) && 
    366466        is(V.DefP == Defined) 
    367467         /+ no repeats +/ 
     
    370470    else 
    371471    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) && 
    373473        is(V.DefP == Defined) 
    374474         /+ no repeats +/ 
     
    390490        alias OpDivA!(OpSub!(OpDiv!(Value!(1), T.LHS), Value!(1)), T.RHS) TypeOfSub; 
    391491    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     else 
    399     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     else 
    406     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     else 
    413     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     else 
    420     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     else 
    427492    static if( // (- (+> B X) A) -> (+> (+ A B) X) 
    428493        is(T.Op == AddA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 
     
    474539        alias OpAddA!(V, T) TypeOfSub; 
    475540    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 ~ `)` ); 
    477544} 
    478545template TypeOfMul(T, V) 
    479546{ 
    480547    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) && 
    482549        is(V.DefP == Defined) 
    483550         /+ no repeats +/ 
     
    487554    static if( // (* C (/> A (-R> B X))) -> (/> (* A C) (-R> B X)) 
    488555        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) 
    490557         /+ no repeats +/ 
    491558        )  
     
    493560    else 
    494561    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) && 
    496563        is(V.DefP == Defined) 
    497564         /+ no repeats +/ 
     
    501568    static if( // (* C (*> A (-R> B X))) -> (*> (/ A C) (-R> B X)) 
    502569        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) 
    504571         /+ no repeats +/ 
    505572        )  
     
    507574    else 
    508575    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) && 
    510577        is(V.DefP == Defined) 
    511578         /+ no repeats +/ 
     
    515582    static if( // (* C (/R> A (+> B X))) -> (/R> (* A C) (+> B X)) 
    516583        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) 
    518585         /+ no repeats +/ 
    519586        )  
     
    521588    else 
    522589    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) && 
    524591        is(V.DefP == Defined) 
    525592         /+ no repeats +/ 
     
    529596    static if( // (* C (/> A (+> B X))) -> (/> (* C A) (+> B X)) 
    530597        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) 
    532599         /+ no repeats +/ 
    533600        )  
     
    535602    else 
    536603    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) && 
    538605        is(V.DefP == Defined) 
    539606         /+ no repeats +/ 
     
    543610    static if( // (* C (*> A (+> B X))) -> (*> (/ A C) (+> B X)) 
    544611        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) 
    546613         /+ no repeats +/ 
    547614        )  
     
    549616    else 
    550617    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) && 
    552619        is(V.DefP == Defined) 
    553620         /+ no repeats +/ 
     
    557624    static if( // (* C (/R> A (-> B X))) -> (/R> (* A C) (-> B X)) 
    558625        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) 
    560627         /+ no repeats +/ 
    561628        )  
     
    563630    else 
    564631    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) && 
    566633        is(V.DefP == Defined) 
    567634         /+ no repeats +/ 
     
    571638    static if( // (* C (/> A (-> B X))) -> (/> (* C A) (-> B X)) 
    572639        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) 
    574641         /+ no repeats +/ 
    575642        )  
     
    577644    else 
    578645    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) && 
    580647        is(V.DefP == Defined) 
    581648         /+ no repeats +/ 
     
    585652    static if( // (* C (*> A (-> B X))) -> (*> (/ A C) (-> B X)) 
    586653        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) 
    588655         /+ no repeats +/ 
    589656        )  
     
    681748        alias OpDivA!(V, T) TypeOfMul; 
    682749    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 ~ `)` ); 
    684753} 
    685754template TypeOfDiv(T, V) 
     
    692761        alias OpMulA!(T.LHS, OpAddA!(T.LHS, T.RHS)) TypeOfDiv; 
    693762    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 
    694777    static if( // (/ (+> B X) A) -> (*> A (+> B X)) 
    695778        is(T.Op == AddA) && is(T.LHS.DefP == Defined) && is(T.RHS.DefP == UnDefined) && 
     
    706789        alias OpSubAR!(Value!(1), OpDivAR!(T.LHS, T.RHS)) TypeOfDiv; 
    707790    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     else 
    715     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     else 
    722791    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) && 
    724793        is(V.DefP == Defined) 
    725794         /+ no repeats +/ 
     
    729798    static if( // (/ C (/> A (-R> B X))) -> (/R> (/ C A) (-R> B X)) 
    730799        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) 
    732801         /+ no repeats +/ 
    733802        )  
     
    735804    else 
    736805    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) && 
    738807        is(V.DefP == Defined) 
    739808         /+ no repeats +/ 
     
    743812    static if( // (/ C (*> A (-R> B X))) -> (/R> (* A C) (-R> B X)) 
    744813        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) 
    746815         /+ no repeats +/ 
    747816        )  
     
    749818    else 
    750819    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) && 
    752821        is(V.DefP == Defined) 
    753822         /+ no repeats +/ 
     
    757826    static if( // (/ C (/R> A (+> B X))) -> (*> (/ A C) (+> B X)) 
    758827        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) 
    760829         /+ no repeats +/ 
    761830        )  
     
    763832    else 
    764833    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) && 
    766835        is(V.DefP == Defined) 
    767836         /+ no repeats +/ 
     
    771840    static if( // (/ C (/> A (+> B X))) -> (/R> (/ C A) (+> B X)) 
    772841        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) 
    774843         /+ no repeats +/ 
    775844        )  
     
    777846    else 
    778847    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) && 
    780849        is(V.DefP == Defined) 
    781850         /+ no repeats +/ 
     
    785854    static if( // (/ C (*> A (+> B X))) -> (/R> (* A C) (+> B X)) 
    786855        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) 
    788857         /+ no repeats +/ 
    789858        )  
     
    791860    else 
    792861    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) && 
    794863        is(V.DefP == Defined) 
    795864         /+ no repeats +/ 
     
    799868    static if( // (/ C (/R> A (-> B X))) -> (*> (/ A C) (-> B X)) 
    800869        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) 
    802871         /+ no repeats +/ 
    803872        )  
     
    805874    else 
    806875    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) && 
    808877        is(V.DefP == Defined) 
    809878         /+ no repeats +/ 
     
    813882    static if( // (/ C (/> A (-> B X))) -> (/R> (/ C A) (-> B X)) 
    814883        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) 
    816885         /+ no repeats +/ 
    817886        )  
     
    819888    else 
    820889    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) && 
    822891        is(V.DefP == Defined) 
    823892         /+ no repeats +/ 
     
    827896    static if( // (/ C (*> A (-> B X))) -> (/R> (* C A) (-> B X)) 
    828897        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) 
    830899         /+ no repeats +/ 
    831900        )  
     
    909978        alias OpMulA!(V, T) TypeOfDiv; 
    910979    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 ~ `)` ); 
    912983} 
    913984 
  • trunk/backmath/meta.lisp

    r173 r174  
    3939 
    4040;a 
    41     ((+ a b)        (+ a b))      ; a 
    42     ((- a b)        (- a b))      ; a 
    43     ((* a b)        (* a b))      ; a 
    44     ((/ a b)        (/ a b))      ; a 
     41    ((+ a b)                   (+ a b))       ; a 
     42    ((- a b)                   (- a b))       ; a 
     43    ((* a b)                   (* a b))       ; a 
     44    ((/ a b)                   (/ a b))       ; a 
    4545 
    4646;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) 
    5656 
    5757;(-> 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))) 
    6767 
    6868;(+> 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))) 
    7878 
    7979;(/> 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) 
    8989 
    9090;(*> 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) 
    100100 
    101101;(-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))) 
    111111 
    112112;(/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) 
    122122 
    123123;(*> 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)) 
    133133 
    134134;(/> 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)) 
    144144 
    145145 
    146146;(/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)) 
    157157 
    158158;(*> 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)) 
    168168 
    169169 
    170170;(/> 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)) 
    175192     
    176193 
    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  
    195194 
    196195;(*> 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)) 
    206205 
    207206 
    208207;(/> 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 
    281268;| # 
    282269;;;; 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)))          ()) 
    438434;   ((+ (/> k (-> h x)) (/> f (-> e x)))        ()) 
    439435;   ((+ (/r> k (-> h x)) (/> f (-> e x)))       ()) 
     
    443439;   ((+ (*> k (-r> h x)) (/> f (-> e x)))       ()) 
    444440;   ((+ (/> 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)))        ()) 
    451447;   ((+ (/> k (-> h x)) (/r> f (-> e x)))       ()) 
    452448;   ((+ (/r> k (-> h x)) (/r> f (-> e x)))      ()) 
     
    456452;   ((+ (*> k (-r> h x)) (/r> f (-> e x)))      ()) 
    457453;   ((+ (/> 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)))         ()) 
    464460;   ((+ (/> k (-> h x)) (*> f (+> e x)))        ()) 
    465461;   ((+ (/r> k (-> h x)) (*> f (+> e x)))       ()) 
     
    469465;   ((+ (*> k (-r> h x)) (*> f (+> e x)))       ()) 
    470466;   ((+ (/> 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)))         ()) 
    477473;   ((+ (/> k (-> h x)) (/> f (+> e x)))        ()) 
    478474;   ((+ (/r> k (-> h x)) (/> f (+> e x)))       ()) 
     
    482478;   ((+ (*> k (-r> h x)) (/> f (+> e x)))       ()) 
    483479;   ((+ (/> 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)))        ()) 
    490486;   ((+ (/> k (-> h x)) (/r> f (+> e x)))       ()) 
    491487;   ((+ (/r> k (-> h x)) (/r> f (+> e x)))      ()) 
     
    495491;   ((+ (*> k (-r> h x)) (/r> f (+> e x)))      ()) 
    496492;   ((+ (/> 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)))        ()) 
    503499;   ((+ (/> k (-> h x)) (*> f (-r> e x)))       ()) 
    504500;   ((+ (/r> k (-> h x)) (*> f (-r> e x)))      ()) 
     
    508504;   ((+ (*> k (-r> h x)) (*> f (-r> e x)))      ()) 
    509505;   ((+ (/> 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)))        ()) 
    516512;   ((+ (/> k (-> h x)) (/> f (-r> e x)))       ()) 
    517513;   ((+ (/r> k (-> h x)) (/> f (-r> e x)))      ()) 
     
    521517;   ((+ (*> k (-r> h x)) (/> f (-r> e x)))      ()) 
    522518;   ((+ (/> 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)))       ()) 
    612619;   ((- (/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)))         ()) 
    624627;   ((- (/> k (-> h x)) (/r> f (-> e x)))       ()) 
    625628;   ((- (/r> k (-> h x)) (/r> f (-> e x)))      ()) 
     
    629632;   ((- (*> k (-r> h x)) (/r> f (-> e x)))      ()) 
    630633;   ((- (/> 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)))         ()) 
    637640;   ((- (/> k (-> h x)) (*> f (+> e x)))        ()) 
    638641;   ((- (/r> k (-> h x)) (*> f (+> e x)))       ()) 
     
    642645;   ((- (*> k (-r> h x)) (*> f (+> e x)))       ()) 
    643646;   ((- (/> 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)))         ()) 
    650653;   ((- (/> k (-> h x)) (/> f (+> e x)))        ()) 
    651654;   ((- (/r> k (-> h x)) (/> f (+> e x)))       ()) 
     
    655658;   ((- (*> k (-r> h x)) (/> f (+> e x)))       ()) 
    656659;   ((- (/> 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)))        ()) 
    663666;   ((- (/> k (-> h x)) (/r> f (+> e x)))       ()) 
    664667;   ((- (/r> k (-> h x)) (/r> f (+> e x)))      ()) 
     
    668671;   ((- (*> k (-r> h x)) (/r> f (+> e x)))      ()) 
    669672;   ((- (/> 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)))        ()) 
    676679;   ((- (/> k (-> h x)) (*> f (-r> e x)))       ()) 
    677680;   ((- (/r> k (-> h x)) (*> f (-r> e x)))      ()) 
     
    681684;   ((- (*> k (-r> h x)) (*> f (-r> e x)))      ()) 
    682685;   ((- (/> 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)))        ()) 
    689692;   ((- (/> k (-> h x)) (/> f (-r> e x)))       ()) 
    690693;   ((- (/r> k (-> h x)) (/> f (-r> e x)))      ()) 
     
    694697;   ((- (*> k (-r> h x)) (/> f (-r> e x)))      ()) 
    695698;   ((- (/> 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)))         ()) 
    780783;   ((* (/> k (-> h x)) (/> f (-> e x)))        ()) 
    781784;   ((* (/r> k (-> h x)) (/> f (-> e x)))       ()) 
     
    785788;   ((* (*> k (-r> h x)) (/> f (-> e x)))       ()) 
    786789;   ((* (/> 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)))        ()) 
    793796;   ((* (/> k (-> h x)) (/r> f (-> e x)))       ()) 
    794797;   ((* (/r> k (-> h x)) (/r> f (-> e x)))      ()) 
     
    798801;   ((* (*> k (-r> h x)) (/r> f (-> e x)))      ()) 
    799802;   ((* (/> 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)))         ()) 
    806809;   ((* (/> k (-> h x)) (*> f (+> e x)))        ()) 
    807810;   ((* (/r> k (-> h x)) (*> f (+> e x)))       ()) 
     
    811814;   ((* (*> k (-r> h x)) (*> f (+> e x)))       ()) 
    812815;   ((* (/> 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)))         ()) 
    819822;   ((* (/> k (-> h x)) (/> f (+> e x)))        ()) 
    820823;   ((* (/r> k (-> h x)) (/> f (+> e x)))       ()) 
     
    824827;   ((* (*> k (-r> h x)) (/> f (+> e x)))       ()) 
    825828;   ((* (/> 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)))        ()) 
    832835;   ((* (/> k (-> h x)) (/r> f (+> e x)))       ()) 
    833836;   ((* (/r> k (-> h x)) (/r> f (+> e x)))      ()) 
     
    837840;   ((* (*> k (-r> h x)) (/r> f (+> e x)))      ()) 
    838841;   ((* (/> 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)))        ()) 
    845848;   ((* (/> k (-> h x)) (*> f (-r> e x)))       ()) 
    846849;   ((* (/r> k (-> h x)) (*> f (-r> e x)))      ()) 
     
    850853;   ((* (*> k (-r> h x)) (*> f (-r> e x)))      ()) 
    851854;   ((* (/> 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)))        ()) 
    858861;   ((* (/> k (-> h x)) (/> f (-r> e x)))       ()) 
    859862;   ((* (/r> k (-> h x)) (/> f (-r> e x)))      ()) 
     
    863866;   ((* (*> k (-r> h x)) (/> f (-r> e x)))      ()) 
    864867;   ((* (/> 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)))         ()) 
    949952;   ((/ (/> k (-> h x)) (/> f (-> e x)))        ()) 
    950953;   ((/ (/r> k (-> h x)) (/> f (-> e x)))       ()) 
     
    954957;   ((/ (*> k (-r> h x)) (/> f (-> e x)))       ()) 
    955958;   ((/ (/> 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)))        ()) 
    962965;   ((/ (/> k (-> h x)) (/r> f (-> e x)))       ()) 
    963966;   ((/ (/r> k (-> h x)) (/r> f (-> e x)))      ()) 
     
    967970;   ((/ (*> k (-r> h x)) (/r> f (-> e x)))      ()) 
    968971;   ((/ (/> 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)))         ()) 
    975978;   ((/ (/> k (-> h x)) (*> f (+> e x)))        ()) 
    976979;   ((/ (/r> k (-> h x)) (*> f (+> e x)))       ()) 
     
    980983;   ((/ (*> k (-r> h x)) (*> f (+> e x)))       ()) 
    981984;   ((/ (/> 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)))         ()) 
    988991;   ((/ (/> k (-> h x)) (/> f (+> e x)))        ()) 
    989992;   ((/ (/r> k (-> h x)) (/> f (+> e x)))       ()) 
     
    993996;   ((/ (*> k (-r> h x)) (/> f (+> e x)))       ()) 
    994997;   ((/ (/> 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)))        ()) 
    10011004;   ((/ (/> k (-> h x)) (/r> f (+> e x)))       ()) 
    10021005;   ((/ (/r> k (-> h x)) (/r> f (+> e x)))      ()) 
     
    10061009;   ((/ (*> k (-r> h x)) (/r> f (+> e x)))      ()) 
    10071010;   ((/ (/> 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)))        ()) 
    10141017;   ((/ (/> k (-> h x)) (*> f (-r> e x)))       ()) 
    10151018;   ((/ (/r> k (-> h x)) (*> f (-r> e x)))      ()) 
     
    10191022;   ((/ (*> k (-r> h x)) (*> f (-r> e x)))      ()) 
    10201023;   ((/ (/> 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)))        ()) 
    10271030;   ((/ (/> k (-> h x)) (/> f (-r> e x)))       ()) 
    10281031;   ((/ (/r> k (-> h x)) (/> f (-r> e x)))      ()) 
     
    10321035;   ((/ (*> k (-r> h x)) (/> f (-r> e x)))      ()) 
    10331036;   ((/ (/> 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)))         ()) 
    10541057;   ((+ (*> a (-> b x)) (*> a (-> b x)))        ()) 
    10551058;   ((+ (/> k (-> h x)) (*> a (-> b x)))        ()) 
     
    10671070;   ((+ (*> a (-> b x)) (*> f (-r> e x)))       ()) 
    10681071;   ((+ (*> 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)))         ()) 
    10811084;   ((- (*> a (-> b x)) (*> a (-> b x)))        ()) 
    10821085;   ((- (/> k (-> h x)) (*> a (-> b x)))        ()) 
     
    10941097;   ((- (*> a (-> b x)) (*> f (-r> e x)))       ()) 
    10951098;   ((- (*> 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)))         ()) 
    11081111;   ((* (*> a (-> b x)) (*> a (-> b x)))        ()) 
    11091112;   ((* (/> k (-> h x)) (*> a (-> b x)))        ()) 
     
    11211124;   ((* (*> a (-> b x)) (*> f (-r> e x)))       ()) 
    11221125;   ((* (*> 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)))         ()) 
    11351138;   ((/ (*> a (-> b x)) (*> a (-> b x)))        ()) 
    11361139;   ((/ (/> k (-> h x)) (*> a (-> b x)))        ()) 
     
    11481151;   ((/ (*> a (-> b x)) (*> f (-r> e x)))       ()) 
    11491152;   ((/ (*> 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;| # 
    11541154    ) 
    11551155) 
  • trunk/backmath/string_stuff.lisp

    r173 r174  
    2323) 
    2424 
     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 
    2541;;; ?New-line constant 
    2642(DEFCONSTANT nl "