content: {-
      Haskell version of ...
  
  ! Text of rule base for Boyer benchmark !
  
  ! Started by Tony Kitto on 6th April 1988                                  !
  ! Changes Log                                                              !
  ! 07-04-88 ADK Corrected errors in rules
  ! 08-04-88 ADK Modified "or" rule to remove extra final (f) of book definition
  
  Haskell version:
  
      23-06-93 JSM initial version
  
  -}
  
  module Rulebasetext (rules) where
  
  rules :: [String]
  
  -- Rule base extracted from Gabriel pages 118 to 126
  
  rules = [
               "(equal (compile form)\
                      \(reverse (codegen (optimize form) (nil) ) ) )",
               "(equal (eqp x y)\
                      \(equal (fix x)\
                             \(fix y) ) )",
               "(equal (greaterp x y)\
                      \(lessp y x) )",
               "(equal (lesseqp x y)\
                      \(not (lessp y x) ) )",
               "(equal (greatereqp x y)\
                      \(not (lessp y x) ) )",
               "(equal (boolean x)\
                      \(or (equal x (t) )\
                          \(equal x (f) ) )",
               "(equal (iff x y)\
                      \(and (implies x y)\
                           \(implies y x) ) )",
               "(equal (even1 x)\
                      \(if (zerop x)\
                          \(t)\
                          \(odd (1- x) ) ) )",
               "(equal (countps- l pred)\
                      \(countps-loop l pred (zero) ) )",
               "(equal (fact- i)\
                      \(fact-loop i 1) )",
  
               "(equal (reverse- x)\
                      \(reverse-loop x (nil) ) )",
               "(equal (divides x y)\
                      \(zerop (remainder y x) ) )",
               "(equal (assume-true var alist)\
                      \(cons (cons var (t) )\
                       \alist) )",
               "(equal (assume-false var alist)\
                      \(cons (cons var (f) )\
                            \alist) )",
               "(equal (tautology-checker x)\
                      \(tautologyp (normalize x)\
                                  \(nil) ) )",
               "(equal (falsify x)\
                      \(falsify1 (normalize x)\
                                \(nil) ) )",
               "(equal (prime x)\
                      \(and (not (zerop x))\
                           \(not (equal x (add1 (zero) ) ) )\
                           \(prime1 x (1- x) ) ) )",
               "(equal (and p q)\
                      \(if p (if q (t) (f) ) (f) ) )",
               "(equal (or p q)\
                      \(if p (t) (if q (t) (f) ) ) )", -- book has extra (f)
               "(equal (not p)\
                      \(if p (f) (t) ) )",
  
               "(equal (implies p q)\
                      \(if p (if q (t) (f) ) (t) ) )",
               "(equal (fix x)\
                      \(if (numberp x) x (zero) ) )",
               "(equal (if (if a b c) d e)\
                      \(if a (if b d e) (if c d e) ) )",
               "(equal (zerop x)\
                      \(or (equal x (zero) )\
                          \(not (numberp x) ) ) )",
               "(equal (plus (plus x y) z )\
                      \(plus x (plus y z) ) )",
               "(equal (equal (plus a b) (zero ) )\
                      \(and (zerop a) (zerop b) ) )",
               "(equal (difference x x)\
                      \(zero) )",
               "(equal (equal (plus a b) (plus a c) )\
                      \(equal (fix b) (fix c) ) )",
               "(equal (equal (zero) (difference x y) )\
                      \(not (lessp y x) ) )",
               "(equal (equal x (difference x y) )\
                      \(and (numberp x)\
                           \(or (equal x (zero) )\
                               \(zerop y) ) ) )",
  
               "(equal (meaning (plus-tree (append x y) ) a)\
                      \(plus (meaning (plus-tree x) a)\
                            \(meaning (plus-tree y) a) ) )",
               "(equal (meaning (plus-tree (plus-fringe x) ) a)\
                      \(fix (meaning x a) ) )",
               "(equal (append (append x y) z)\
                      \(append x (append y z) ) )",
               "(equal (reverse (append a b) )\
                      \(append (reverse b) (reverse a) ) )",
               "(equal (times x (plus y z) )\
                      \(plus (times x y)\
                            \(times x z) ) )",
               "(equal (times (times x y) z)\
                      \(times x (times y z) ) )",
               "(equal (equal (times x y) (zero) )\
                      \(or (zerop x)\
                          \(zerop y) ) )",
               "(equal (exec (append x y)\
                             \pds envrn)\
                      \(exec y (exec x pds envrn)\
                            \envrn) )",
               "(equal (mc-flatten x y)\
                      \(append (flatten x)\
                             \y) )",
               "(equal (member x (append a b) )\
                      \(or (member x a)\
                          \(member x b) ) )",
  
               "(equal (member x (reverse y) )\
                      \(member x y) )",
               "(equal (length (reverse x) )\
                      \(length x) )",
               "(equal (member a (intersect b c) )\
                      \(and (member a b)\
                           \(member a c) ) )",
               "(equal (nth (zero)\
                            \i)\
                      \(zero) )",
               "(equal (exp i (plus j k) )\
                      \(times (exp i j)\
                             \(exp i k) ) )",
               "(equal (exp i (times j k) )\
                      \(exp (exp i j)\
                           \k) )",
               "(equal (reverse-loop x y)\
                      \(append (reverse x)\
                              \y) )",
               "(equal (reverse-loop x (nil) )\
                      \(reverse x) )",
               "(equal (count-list z (sort-lp x y) )\
                      \(plus (count-list z x)\
                            \(count-list z y) ) )",
               "(equal (equal (append a b)\
                             \(append a c) )\
                      \(equal b c) )",
  
               "(equal (plus (remainder x y)\
                            \(times y (quotient x y) ) )\
                      \(fix x) )",
               "(equal (power-eval (big-plus1 l i base)\
                                  \base)\
                      \(plus (power-eval l base)\
                            \i) )",
               "(equal (power-eval (big-plus x y i base)\
                                  \base)\
                      \(plus i (plus (power-eval x base)\
                                    \(power-eval y base) ) ) )",
               "(equal (remainder y 1)\
                      \(zero) )",
               "(equal (lessp (remainder x y)\
                             \y)\
                      \(not (zerop y) ) )",
               "(equal (remainder x x)\
                      \(zero) )",
               "(equal (lessp (quotient i j)\
                             \i)\
                      \(and (not (zerop i) )\
                           \(or (zerop j)\
                               \(not (equal j 1) ) ) ) )",
               "(equal (lessp (remainder x y)\
                             \x)\
                      \(and (not (zerop y) )\
                           \(not (zerop x) )\
                           \(not (lessp x y) ) ) )",
               "(equal (power-eval (power-rep i base)\
                                  \base)\
                      \(fix i) )",
               "(equal (power-eval (big-plus (power-rep i base)\
                                            \(power-rep j base)\
                                            \(zero)\
                                            \base)\
                                   \base)\
                      \(plus i j) )",
  
               "(equal (gcd x y)\
                      \(gcd y x) )",
               "(equal (nth (append a b)\
                           \i)\
                      \(append (nth a i)\
                              \(nth b (difference i (length a) ) ) ) )",
               "(equal (difference (plus x y)\
                                  \x)\
                      \(fix y) )",
               "(equal (difference (plus y x)\
                                  \x)\
                      \(fix y) )",
               "(equal (difference (plus x y)\
                                  \(plus x z) )\
                      \(difference y z) )",
               "(equal (times x (difference c w) )\
                      \(difference (times c x)\
                                  \(times w x) ) )",
               "(equal (remainder (times x z)\
                                 \z)\
                      \(zero) )",
               "(equal (difference (plus b (plus a c) )\
                                  \a)\
                      \(plus b c) )",
               "(equal (difference (add1 (plus y z)\
                                  \z)\
                      \(add1 y) )",
               "(equal (lessp (plus x y)\
                             \(plus x z ) )\
                      \(lessp y z) )",
  
               "(equal (lessp (times x z)\
                             \(times y z) )\
                      \(and (not (zerop z) )\
                           \(lessp x y) ) )",
               "(equal (lessp y (plus x y) )\
                      \(not (zerop x) ) )",
               "(equal (gcd (times x z)\
                           \(times y z) )\
                      \(times z (gcd x y) ) )",
               "(equal (value (normalize x)\
                             \a)\
                      \(value x a) )",
               "(equal (equal (flatten x)\
                             \(cons y (nil) ) )\
                      \(and (nlistp x)\
                           \(equal x y) ) )",
               "(equal (listp (gopher x) )\
                      \(listp x) )",
               "(equal (samefringe x y)\
                      \(equal (flatten x)\
                             \(flatten y) ) )",
               "(equal (equal (greatest-factor x y)\
                             \(zero) )\
                      \(and (or (zerop y)\
                               \(equal y 1) )\
                           \(equal x (zero) ) ) )",
               "(equal (equal (greatest-factor x y)\
                             \1)\
                      \(equal x 1) )",
               "(equal (numberp (greatest-factor x y) )\
                      \(not (and (or (zerop y)\
                                    \(equal y 1) )\
                                \(not (numberp x) ) ) ) )",
  
               "(equal (times-list (append x y) )\
                      \(times (times-list x)\
                             \(times-list y) ) )",
               "(equal (prime-list (append x y) )\
                      \(and (prime-list x)\
                           \(prime-list y) ) )",
               "(equal (equal z (times w z) )\
                      \(and (numberp z)\
                           \(or (equal z (zero) )\
                               \(equal w 1) ) ) )",
               "(equal (greatereqpr x y)\
                      \(not (lessp x y) ) )",
               "(equal (equal x (times x y) )\
                      \(or (equal x (zero) )\
                          \(and (numberp x)\
                               \(equal y 1) ) ) )",
               "(equal (remainder (times y x)\
                                 \y)\
                      \(zero) )",
               "(equal (equal (times a b)\
                             \1)\
                      \(and (not (equal a (zero) ) )\
                           \(not (equal b (zero) ) )\
                           \(numberp a)\
                           \(numberp b)\
                           \(equal (1- a)\
                                  \(zero) )\
                           \(equal (1- b)\
                                  \(zero) ) ) )",
               "(equal (lessp (length (delete x l) )\
                             \(length l) )\
                      \(member x l) )",
               "(equal (sort2 (delete x l) )\
                      \(delete x (sort2 l) ) )",
               "(equal (dsort x)\
                      \(sort2 x) )",
  
               "(equal (length\
                       \(cons \
                        \x1\
                        \(cons \
                         \x2\
                         \(cons \
                          \x3\
                          \(cons \
                           \x4\
                           \(cons \
                            \x5\
                            \(cons x6 x7) ) ) ) ) ) )\
                      \(plus 6 (length x7) ) )",
               "(equal (difference (add1 (add1 x) )\
                                  \2)\
                      \(fix x) )",
               "(equal (quotient (plus x (plus x y) )\
                                \2)\
                      \(plus x (quotient y 2) ) )",
               "(equal (sigma (zero)\
                             \i)\
                      \(quotient (times i (add1 i) )\
                                \2) )",
               "(equal (plus x (add1 y) )\
                      \(if (numberp y)\
                          \(add1 (plus x y) )\
                          \(add1 x) ) )",
               "(equal (equal (difference x y)\
                             \(difference z y) )\
                      \(if (lessp x y)\
                          \(not (lessp y z) )\
                          \(if (lessp z y)\
                              \(not (lessp y x) )\
                              \(equal (fix x)\
                                     \(fix z) ) ) ) )",
               "(equal (meaning (plus-tree (delete x y) )\
                               \a)\
                      \(if (member x y)\
                          \(difference (meaning (plus-tree y)\
                                               \a)\
                                      \(meaning x a) )\
                          \(meaning (plus-tree y)\
                                   \a) ) )",
               "(equal (times x (add1 y) )\
                      \(if (numberp y)\
                          \(plus x (times x y) )\
                          \(fix x) ) )",
               "(equal (nth (nil)\
                           \i)\
                      \(if (zerop i)\
                          \(nil)\
                          \(zero) ) )",
               "(equal (last (append a b) )\
                      \(if (listp b)\
                          \(last b)\
                          \(if (listp a)\
                              \(cons (car (last a) )\
                                   \b)\
                              \b) ) )",
  
               "(equal (equal (lessp x y)\
                             \z)\
                      \(if (lessp x y)\
                          \(equal t z)\
                          \(equal f z) ) )",
               "(equal (assignment x (append a b) )\
                      \(if (assignedp x a)\
                          \(assignment x a)\
                          \(assignment x b) ) )",
               "(equal (car (gopher x) )\
                      \(if (listp x)\
                         \(car (flatten x) )\
                          \(zero) ) )",
               "(equal (flatten (cdr (gopher x) ) )\
                      \(if (listp x)\
                          \(cdr (flatten x) )\
                          \(cons (zero)\
                                \(nil) ) ) )",
               "(equal (quotient (times y x)\
                                \y)\
                      \(if (zerop y)\
                          \(zero)\
                          \(fix x) ) )",
               "(equal (get j (set i val mem) )\
                      \(if (eqp j i)\
                          \val\
                          \(get j mem) ) )"]
  
  