minlog 4.0.99.20100221-5.2 / usr / share / minlog / lib / realsimp.scm

; $Id: realsimp.scm 2156 2008-01-25 13:25:12Z schimans $

; Based on ~schwicht/wwwpublic/seminars/prosemss04/numbers.scm,v 1.23 
; 2004/11/02.  This is the final part of this file.

(display "loading realsimp.scm ...") (newline)


; 4. Simplification of Real Terms 
; ===============================

; General description of the simplification procedure for number
; terms.  Reals x,y,z are built from Cauchy sequences v of rationals
; and moduli M by RealConstr v M.  Rationals a,b,c are built from
; integers i,j and positive numbers k by pairing i#k (viewed as
; quotient), und integers are either positive or zero or negative.

; Positive terms r are built form positive variables n,m and the
; constant One by the constructors SZero and SOne and the arithmetical
; functions S, PosPlus, PosTimes, PosMinus, PosExp.

; Integer terms s are built form integer variables i,j and integer
; constructor terms IntPos r, IntZero, IntNeg r with a positive term r
; by the arithmetical functions IntPlus, IntTimes, IntMinus, IntExp.
; A positive term r can be coerced into the integer term IntP r.

; Rational terms t are built form rational variables a,b and rational
; constructor terms s#r with an integer term s and a positive term r
; by the arithmetical functions RatPlus, RatTimes, RatMinus, RatDiv,
; RatExp.  A positive term r can be coerced into the rational term
; IntP r#1, and an integer term s can be coerced into the rational term
; s#1.

; Real terms u are built form real variables x,y and real constructor
; terms RealConstr v w with v a term of type pos=>rat and w a term of
; type pos=>pos by the arithmetical functions RealPlus, RealTimes,
; RealMinus, RealDiv, RealExp.  A rational term t can be coerced into
; the real term RealConstr([n]t)([k]1).

; Simplification starts by unfolding exponentials, using the rules 
; exp x 1          -> x, 
; exp x(SZero y)   -> (exp x y)*(exp x y), 
; exp x(SOne y)    -> (exp x(SZero y))*x, 
; exp x(S y)       -> (exp x y)*x, 
; exp x(y+z)       -> (exp x y)*(exp x z),
; exp x(y*z)       -> exp(exp x y)z.

; Next we want to push the constructors inside, to allow more
; simplifications.  For the number types pos, int, rat, real the
; precise meaning is somewhat different:

; pos.  The constructors are One, SZero, SOne.  If they are part of a
; numerical term, they are not touched.  Otherwise they are removed, via
; SZero r -> r*2
; SOne r  -> r*2+1

; int.  The constructors are IntN, IntZero, IntP.  IntN is removed using 0-,
; IntZero is removed using 0, and IntP is pushed inside, through + and *:
; IntN r -> 0-IntP r
; IntZero -> 0
; IntP(r o s) -> IntP r o IntP s for o one of + *

; rat.  The constructor is RatConstr #.  r#s with s not 1 is replaced
; using /, and in r#1 the #1 is pushed inside, through + - *:
; r#s -> (r#1)/(IntP s#1) if s is not 1
; (r o s)#1 -> r#1 o s#1 for o one of + - *

; real.  The constructor is RealConstr.  In RealConstr([n]r o s)([k]1)
; with a constant Cauchy sequence (i.e., n not in r,s) the constructor
; is pushed inside.
; RealConstr([n]r o s)([k]1) -> RealConstr([n]r)([k]1) o RealConstr([n]s)([k]1)
; for o one of + - * /

; Next we employ an operator term-to-numerator-and-denominator, and
; then apply some operators to the numerator and denominator
; separately.  By a monom we mean a product whose factors are neither
; sums nor differences.  For a single monom, we collect its general
; numeric terms into a product number and write each factor as a list
; of a string and its power, for example (27 ("a" 2) ("b" 1) ("c" 3)).
; Then we sort and join stringpowers as well as summands, to make
; cancellation possible.  To describe the form of the simplified term,
; we use the following terminology.  sp (stringpower): a list of two
; elements, a string and a positive integer (Scheme object).  sps
; (stringpowers): a list (possibly empty) of stringpowers.  nsps
; (num-with-stringpowers): a list (num sp1 sp2 ...) containing at
; least the number.  nsps-list: a list (possibly empty) of nsps.

; So when given a quotient num1 common-sps1 non-common-nsps-list1 /
; num2 common-sps2 non-common-nsps-list2, we then produce a product of
; (/ num1 num2) and the quotient cancelled-common-sps1
; non-common-nsps-list1 / cancelled-common-sps2 non-common-nsps-list2
; in case non-common-nsps-list1 and non-common-nsps-list2 differ, and
; cancelled-common-sps1 / cancelled-common-sps2 in case
; non-common-nsps-list1 and non-common-nsps-list2 are equal.

(define (num-and-type-to-gen-numeric-term n type)
  (let ((string (type-to-string type)))
    (if (integer? n)
	(if (positive? n)
	    (cond ((equal? (py "pos") type) (make-numeric-term n))
		  ((equal? (py "int") type) (int-to-int-term n))
		  ((equal? (py "rat") type) (rat-to-rat-term n))
		  ((equal? (py "real") type) (rat-to-real-term n))
		  (else (myerror "num-and-type-to-gen-numeric-term"
				 "unexpected type" string)))
	    (cond ((equal? (py "int") type) (int-to-int-term n))
		  ((equal? (py "rat") type) (rat-to-rat-term n))
		  ((equal? (py "real") type) (rat-to-real-term n))
		  (else (myerror "num-and-type-to-gen-numeric-term"
				 "unexpected type" string))))
	(cond ((equal? (py "rat") type) (rat-to-rat-term n))
	      ((equal? (py "real") type) (rat-to-real-term n))
	      (else (myerror "num-and-type-to-gen-numeric-term"
			     "unexpected type" string))))))

(define (is-gen-numeric-term? term)
  (let ((type (term-to-type term)))
    (or (and (equal? (py "pos") type) (is-numeric-term? term))
	(and (equal? (py "int") type) (is-int-numeric-term? term))
	(and (equal? (py "rat") type) (is-rat-numeric-term? term))
	(and (equal? (py "real") type) (is-real-numeric-term? term)))))

(define (gen-numeric-term-to-number term)
  (let ((type (term-to-type term)))
    (cond
     ((equal? (py "pos") type) (numeric-term-to-number term))
     ((equal? (py "int") type) (int-numeric-term-to-number term))
     ((equal? (py "rat") type) (rat-numeric-term-to-number term))
     ((equal? (py "real") type) (real-numeric-term-to-number term))
     (else (myerror "gen-numeric-term-to-number"
		    "pos, int, rat or real expected"
		    (type-to-string type))))))

(define (term-to-term-with-unfolded-exponents term)
  (case (tag term)
    ((term-in-var-form term-in-const-form)
     term)
    ((term-in-app-form)    
     (let* ((op (term-in-app-form-to-final-op term))
	    (args (term-in-app-form-to-args term))
	    (type (term-to-type term))
	    (string (cond ((equal? (py "pos") type) "Pos")
			  ((equal? (py "int") type) "Int")
			  ((equal? (py "rat") type) "Rat")
			  ((equal? (py "real") type) "Real")
			  (else (myerror "term-to-term-with-unfolded-exponents"
					 "unexpected type"
					 (type-to-string type))))))
       (if
	(and (term-in-const-form? op)
	     (let* ((name (const-to-name (term-in-const-form-to-const op)))
		    (l (string-length name))
		    (exp-string
		     (substring name (max 0 (- l (string-length "Exp"))) l)))
	       (string=? "Exp" exp-string))
	     (= 2 (length args)))
	(let* ((exp (cadr args))
	       (expop (term-in-app-form-to-final-op exp)))
	  (cond
	   ((and (term-in-const-form? exp)
		 (string=? "One" (const-to-name
				  (term-in-const-form-to-const exp))))
	    (car args))
	   ((and (term-in-const-form? expop)
		 (string=? "SZero" (const-to-name
				    (term-in-const-form-to-const expop))))
	    (let* ((exparg (term-in-app-form-to-arg exp))
		   (prev (term-to-term-with-unfolded-exponents
			  (mk-term-in-app-form op (car args) exparg))))
	      (mk-term-in-app-form
	       (make-term-in-const-form
		(pconst-name-to-pconst (string-append string "Times")))
	       prev prev)))
	   ((and (term-in-const-form? expop)
		 (string=? "SOne" (const-to-name
				   (term-in-const-form-to-const expop))))
	    (let* ((exparg (term-in-app-form-to-arg exp))
		   (prev (term-to-term-with-unfolded-exponents
			  (mk-term-in-app-form op (car args) exparg)))
		   (timesconst (make-term-in-const-form
				(pconst-name-to-pconst
				 (string-append string "Times")))))
	      (mk-term-in-app-form
	       timesconst
	       (mk-term-in-app-form timesconst prev prev)
	       (car args))))
	   ((and (term-in-const-form? expop)
		 (string=? "S" (const-to-name
				      (term-in-const-form-to-const expop))))
	    (let* ((exparg (term-in-app-form-to-arg exp))
		   (prev (term-to-term-with-unfolded-exponents
			  (mk-term-in-app-form op (car args) exparg))))
	      (mk-term-in-app-form
	       (make-term-in-const-form
		(pconst-name-to-pconst (string-append string "Times")))
	       prev (car args))))
	   ((and (term-in-const-form? expop)
		 (string=? "PosPlus" (const-to-name
				      (term-in-const-form-to-const expop))))
	    (let* ((expargs (term-in-app-form-to-args exp))
		   (exparg1 (car expargs))
		   (exparg2 (cadr expargs))
		   (prev1 (term-to-term-with-unfolded-exponents
			   (mk-term-in-app-form op (car args) exparg1)))
		   (prev2 (term-to-term-with-unfolded-exponents
			   (mk-term-in-app-form op (car args) exparg2))))
	      (mk-term-in-app-form
	       (make-term-in-const-form
		(pconst-name-to-pconst (string-append string "Times")))
	       prev1 prev2)))
	   ((and (term-in-const-form? expop)
		 (string=? "PosTimes" (const-to-name
				       (term-in-const-form-to-const expop))))
	    (let* ((expargs (term-in-app-form-to-args exp))
		   (exparg1 (car expargs))
		   (exparg2 (cadr expargs)))
	      (term-to-term-with-unfolded-exponents
	       (mk-term-in-app-form
		op (mk-term-in-app-form op (car args) exparg1) exparg2))))
	   (else
	    (apply mk-term-in-app-form
		   (cons op (map term-to-term-with-unfolded-exponents
				 args))))))
	(apply mk-term-in-app-form
	       (cons op (map term-to-term-with-unfolded-exponents args))))))
    ((term-in-abst-form)
     (let ((var (term-in-abst-form-to-var term))
	   (kernel (term-in-abst-form-to-kernel term)))
       (make-term-in-abst-form
	var (term-to-term-with-unfolded-exponents kernel))))
    ((term-in-pair-form)
     (let ((left (term-in-pair-form-to-left term))
	   (right (term-in-pair-form-to-right term)))
       (make-term-in-pair-form
	(term-to-term-with-unfolded-exponents left)
	(term-to-term-with-unfolded-exponents right))))
    ((term-in-lcomp-form)
     (make-term-in-lcomp-form
      (term-to-term-with-unfolded-exponents
       (term-in-lcomp-form-to-kernel term))))
    ((term-in-rcomp-form)
     (make-term-in-rcomp-form
      (term-to-term-with-unfolded-exponents
       (term-in-rcomp-form-to-kernel term))))
    ((term-in-if-form)
     (let* ((test (term-in-if-form-to-test term))
	    (alts (term-in-if-form-to-alts term))
	    (rest (term-in-if-form-to-rest term))
	    (prev (term-to-term-with-unfolded-exponents test))
	    (prevs (map term-to-term-with-unfolded-exponents alts)))
       (apply make-term-in-if-form (cons prev (cons prevs rest)))))
    (else (myerror "term-to-term-with-unfolded-exponents: term expected"
		   term))))

; (pp (term-to-term-with-unfolded-exponents (pt "(exp 2(SZero n))")))
; (pp (term-to-term-with-unfolded-exponents (pt "(exp 2(SOne n))")))
; (pp (term-to-term-with-unfolded-exponents (pt "(exp 2 2)")))
; (pp (term-to-term-with-unfolded-exponents (pt "(exp 2(k+1))")))
; (pp (term-to-term-with-unfolded-exponents (pt "(exp 2(k+7))")))
; (pp (term-to-term-with-unfolded-exponents (pt "(exp 2(S k))")))
; (pp (term-to-term-with-unfolded-exponents (pt "(exp 2(k+k1))")))
; (pp (term-to-term-with-unfolded-exponents (pt "(exp 2(n*m))")))
; (pp (term-to-term-with-unfolded-exponents (pt "exp a 1")))
; (pp (term-to-term-with-unfolded-exponents (pt "(exp a 7)+(exp b 2)")))
; (pp (term-to-term-with-unfolded-exponents (pt "(exp a 7)/(exp b 2)")))
; (pp (term-to-term-with-unfolded-exponents (pt "exp x 1")))
; (pp (term-to-term-with-unfolded-exponents (pt "exp x 2")))

(define (term-to-term-with-constructors-pushed-inside term)
  (if (not (member (term-to-type term)
		   (list (py "pos") (py "int") (py "rat") (py "real"))))
      (myerror "term-to-term-with-constructors-pushed-inside"
	       "term of type pos, int, rat or real expected"
	       (term-to-string term)))
  (cond
   ((or (term-in-var-form? term)
	(term-in-const-form? term)
	(is-gen-numeric-term? term))
    term)
   ((term-in-app-form? term)    
    (let ((op (term-in-app-form-to-final-op term))
	  (args (term-in-app-form-to-args term)))
      (cond
       ((and (= 2 (length args))
	     (term-in-const-form? op)
	     (member (const-to-name (term-in-const-form-to-const op))
		     '("PosPlus" "PosTimes"
		       "IntPlus" "IntMinus" "IntTimes"
		       "RatPlus" "RatMinus" "RatTimes" "RatDiv"
		       "RealPlus" "RealMinus" "RealTimes" "RealDiv")))
	(apply mk-term-in-app-form
	       (cons op (map term-to-term-with-constructors-pushed-inside
			     args))))
       ((and (= 1 (length args))
	     (term-in-const-form? op)
	     (string=? (const-to-name (term-in-const-form-to-const op))
		       "SZero"))
	(mk-term-in-app-form
	 (make-term-in-const-form (pconst-name-to-pconst "PosTimes"))
	 (make-numeric-term 2)
	 (term-to-term-with-constructors-pushed-inside (car args))))
       ((and (= 1 (length args))
	     (term-in-const-form? op)
	     (string=? (const-to-name (term-in-const-form-to-const op))
		       "SOne"))
	(mk-term-in-app-form
	 (make-term-in-const-form (pconst-name-to-pconst "PosPlus"))
	 (mk-term-in-app-form
	  (make-term-in-const-form (pconst-name-to-pconst "PosTimes"))
	  (make-numeric-term 2)
	  (term-to-term-with-constructors-pushed-inside (car args)))
	 (make-numeric-term 1)))
       ((and (= 1 (length args))
	     (term-in-const-form? op)
	     (string=? (const-to-name (term-in-const-form-to-const op))
		       "IntNeg"))
	(mk-term-in-app-form
	 (make-term-in-const-form (pconst-name-to-pconst "IntMinus"))
	 (make-numeric-term 0)
	 (term-to-term-with-constructors-pushed-inside (car args))))
       ((and (= 1 (length args))
	     (term-in-const-form? op)
	     (string=? (const-to-name (term-in-const-form-to-const op))
		       "IntPos"))
	(let* ((arg (car args))
	       (mod-arg (term-to-term-with-constructors-pushed-inside arg))
	       (op1 (term-in-app-form-to-final-op mod-arg))
	       (args1 (term-in-app-form-to-args mod-arg)))
	  (cond
	   ((and (term-in-const-form? op1)
		 (string=? "PosPlus" (const-to-name
				      (term-in-const-form-to-const op1)))
		 (= 2 (length args1)))
	    (mk-term-in-app-form
	     (make-term-in-const-form (pconst-name-to-pconst "IntPlus"))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form op (car args1)))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form op (cadr args1)))))
	   ((and (term-in-const-form? op1)
		 (string=? "PosTimes" (const-to-name
				       (term-in-const-form-to-const op1)))
		 (= 2 (length args1)))
	    (mk-term-in-app-form
	     (make-term-in-const-form (pconst-name-to-pconst "IntTimes"))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form op (car args1)))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form op (cadr args1)))))
	   (else
	    (mk-term-in-app-form
	     op (term-to-term-with-constructors-pushed-inside (car args)))))))
       ((and (= 2 (length args))
	     (term-in-const-form? op)
	     (string=? (const-to-name (term-in-const-form-to-const op))
		       "RatConstr"))
	(let ((left (car args))
	      (right (cadr args)))
	  (if
	   (not (and (is-numeric-term? right)
		     (= 1 (numeric-term-to-number right))))
	   (mk-term-in-app-form
	    (make-term-in-const-form (pconst-name-to-pconst "RatDiv"))
	    (term-to-term-with-constructors-pushed-inside
	     (mk-term-in-app-form op left (make-numeric-term 1)))
	    (term-to-term-with-constructors-pushed-inside
	     (pos-term-to-rat-term right)))
	   (let* ((mod-left
		   (term-to-term-with-constructors-pushed-inside left))
		  (op1 (term-in-app-form-to-final-op mod-left))
		  (args1 (term-in-app-form-to-args mod-left)))
	     (cond
	      ((and (term-in-const-form? op1)
		    (string=? "IntPlus" (const-to-name
					 (term-in-const-form-to-const op1)))
		    (= 2 (length args1)))
	       (mk-term-in-app-form
		(make-term-in-const-form (pconst-name-to-pconst "RatPlus"))
		(term-to-term-with-constructors-pushed-inside
		 (mk-term-in-app-form
		  op (car args1) (make-numeric-term 1)))
		(term-to-term-with-constructors-pushed-inside
		 (mk-term-in-app-form
		  op (cadr args1) (make-numeric-term 1)))))
	      ((and (term-in-const-form? op1)
		    (string=? "IntMinus" (const-to-name
					  (term-in-const-form-to-const op1)))
		    (= 2 (length args1)))
	       (mk-term-in-app-form
		(make-term-in-const-form (pconst-name-to-pconst "RatMinus"))
		(term-to-term-with-constructors-pushed-inside
		 (mk-term-in-app-form
		  op (car args1) (make-numeric-term 1)))
		(term-to-term-with-constructors-pushed-inside
		 (mk-term-in-app-form
		  op (cadr args1) (make-numeric-term 1)))))
	      ((and (term-in-const-form? op1)
		    (string=? "IntTimes" (const-to-name
					  (term-in-const-form-to-const op1)))
		    (= 2 (length args1)))
	       (mk-term-in-app-form
		(make-term-in-const-form (pconst-name-to-pconst "RatTimes"))
		(term-to-term-with-constructors-pushed-inside
		 (mk-term-in-app-form
		  op (car args1) (make-numeric-term 1)))
		(term-to-term-with-constructors-pushed-inside
		 (mk-term-in-app-form
		  op (cadr args1) (make-numeric-term 1)))))
	      (else
	       (mk-term-in-app-form
		op
		(term-to-term-with-constructors-pushed-inside left)
		(term-to-term-with-constructors-pushed-inside right))))))))
       ((and (= 2 (length args))
	     (term-in-const-form? op)
	     (string=? (const-to-name (term-in-const-form-to-const op))
		       "RealConstr")
	     (term-in-abst-form? (car args))
	     (not (member (term-in-abst-form-to-var (car args))
			  (term-to-free
			   (term-in-abst-form-to-kernel (car args))))))
	(let* ((var (term-in-abst-form-to-var (car args)))
	       (kernel (term-in-abst-form-to-kernel (car args)))
	       (op1 (term-in-app-form-to-final-op kernel))
	       (args1 (term-in-app-form-to-args kernel)))
	  (cond
	   ((and (term-in-const-form? op1)
		 (string=? "RatPlus" (const-to-name
				      (term-in-const-form-to-const op1)))
		 (= 2 (length args1)))
	    (mk-term-in-app-form
	     (make-term-in-const-form (pconst-name-to-pconst "RealPlus"))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form
	       (make-term-in-const-form (constr-name-to-constr "RealConstr"))
	       (make-term-in-abst-form var (car args1))
	       (cadr args)))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form
	       (make-term-in-const-form (constr-name-to-constr "RealConstr"))
	       (make-term-in-abst-form var (cadr args1))
	       (cadr args)))))
	   ((and (term-in-const-form? op1)
		 (string=? "RatTimes" (const-to-name
				       (term-in-const-form-to-const op1)))
		 (= 2 (length args1)))
	    (mk-term-in-app-form
	     (make-term-in-const-form (pconst-name-to-pconst "RealTimes"))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form
	       (make-term-in-const-form (constr-name-to-constr "RealConstr"))
	       (make-term-in-abst-form var (car args1))
	       (cadr args)))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form
	       (make-term-in-const-form (constr-name-to-constr "RealConstr"))
	       (make-term-in-abst-form var (cadr args1))
	       (cadr args)))))
	   ((and (term-in-const-form? op1)
		 (string=? "RatMinus" (const-to-name
				       (term-in-const-form-to-const op1)))
		 (= 2 (length args1)))
	    (mk-term-in-app-form
	     (make-term-in-const-form (pconst-name-to-pconst "RealMinus"))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form
	       (make-term-in-const-form (constr-name-to-constr "RealConstr"))
	       (make-term-in-abst-form var (car args1))
	       (cadr args)))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form
	       (make-term-in-const-form (constr-name-to-constr "RealConstr"))
	       (make-term-in-abst-form var (cadr args1))
	       (cadr args)))))
	   ((and (term-in-const-form? op1)
		 (string=? "RatDiv" (const-to-name
				     (term-in-const-form-to-const op1)))
		 (= 2 (length args1)))
	    (mk-term-in-app-form
	     (make-term-in-const-form (pconst-name-to-pconst "RealDiv"))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form
	       (make-term-in-const-form (constr-name-to-constr "RealConstr"))
	       (make-term-in-abst-form var (car args1))
	       (cadr args)))
	     (term-to-term-with-constructors-pushed-inside
	      (mk-term-in-app-form
	       (make-term-in-const-form (constr-name-to-constr "RealConstr"))
	       (make-term-in-abst-form var (cadr args1))
	       (cadr args)))))
	   (else term))))
       (else term))))
   (else term)))

; (pp (term-to-term-with-constructors-pushed-inside (pt "IntP(SZero(SOne n))#m")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "IntP n#m")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "IntN(n1+n2)#m")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "IntP(n1+n2)#1")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "n1-n2#1")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "IntP(n1*n2)#1")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "IntP(n1*n2)#m")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "IntP(n1+n2+n3)#1")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "IntP(n1+n2+n3)#m")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "IntP(n1+n2+n3)#m1+m2")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "i#1")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "i1+i2-n#1")))
; (pp (term-to-term-with-constructors-pushed-inside (pt "RealConstr([n]a*b)([k]1)")))

; We now define term-to-numerator-and-denominator
; ttnd(a1+a2) := let ttnd(a1)=n1/d1, ttnd(a2)=n2/d2 in (n1*d2 + d1*n2)/(d1*d2)
; ttnd(a1-a2) := let ttnd(a1)=n1/d1, ttnd(a2)=n2/d2 in (n1*d2 - d1*n2)/(d1*d2)
; ttnd(a1*a2) := let ttnd(a1)=n1/d1, ttnd(a2)=n2/d2 in (n1*n2)/(d1*d2)
; ttnd(a1/a2) := let ttnd(a1)=n1/d1, ttnd(a2)=n2/d2 in (n1*d2)/(d1*n2)

(define (term-to-numerator-and-denominator term)
  (let* ((type (term-to-type term))
	 (string (cond ((equal? (py "pos") type) "Pos")
		       ((equal? (py "int") type) "Int")
		       ((equal? (py "rat") type) "Rat")
		       ((equal? (py "real") type) "Real")
		       (else (myerror "term-to-numerator-and-denominator"
				      "unexpected type"
				      (type-to-string type))))))
    (if
     (term-in-app-form? term)
     (let* ((op (term-in-app-form-to-final-op term))
	    (args (term-in-app-form-to-args term))
	    (make-times-term
	     (lambda (arg1 arg2)
	       (cond ((and (is-gen-numeric-term? arg1)
			   (= 1 (gen-numeric-term-to-number arg1)))
		      arg2)
		     ((and (is-gen-numeric-term? arg2)
			   (= 1 (gen-numeric-term-to-number arg2)))
		      arg1)
		     (else (mk-term-in-app-form
			    (make-term-in-const-form
			     (pconst-name-to-pconst
			      (string-append string "Times")))
			    arg1 arg2))))))
       (if
	(or (not (and (term-in-const-form? op)
		      (= 2 (length args))
		      (not (string=? (const-to-name
				      (term-in-const-form-to-const op))
				     "RealConstr"))))
	    (is-gen-numeric-term? term))
	(list term (num-and-type-to-gen-numeric-term 1 type))
	(let* ((arg1 (car args))
	       (arg2 (cadr args))
	       (prev1 (term-to-numerator-and-denominator arg1))
	       (n1 (car prev1))
	       (d1 (cadr prev1))
	       (prev2 (term-to-numerator-and-denominator arg2))
	       (n2 (car prev2))
	       (d2 (cadr prev2))
	       (name (const-to-name (term-in-const-form-to-const op)))
	       (l (string-length name)))
	  (cond
	   ((string=? (substring name (max 0 (- l (string-length "Plus"))) l)
		      "Plus")
	    (list (mk-term-in-app-form
		   (make-term-in-const-form
		    (pconst-name-to-pconst (string-append string "Plus")))
		   (make-times-term n1 d2)
		   (make-times-term d1 n2))
		  (make-times-term d1 d2)))
	   ((string=? (substring name (max 0 (- l (string-length "Minus"))) l)
		      "Minus")
	    (list (mk-term-in-app-form
		   (make-term-in-const-form
		    (pconst-name-to-pconst (string-append string "Minus")))
		   (make-times-term n1 d2)
		   (make-times-term d1 n2))
		  (make-times-term d1 d2)))
	   ((string=? (substring name (max 0 (- l (string-length "Times"))) l)
		      "Times")
	    (list (make-times-term n1 n2) (make-times-term d1 d2)))
	   ((string=? (substring name (max 0 (- l (string-length "Div"))) l)
		      "Div")
	    (list (make-times-term n1 d2) (make-times-term d1 n2)))
	   ((and (string=? name "RatConstr")  (string=? "Rat" string))
	    (list (int-term-to-rat-term arg1) (pos-term-to-rat-term arg2)))
	   (else (list term (num-and-type-to-gen-numeric-term 1 type)))))))
     (list term (num-and-type-to-gen-numeric-term 1 type)))))

; (map term-to-string (term-to-numerator-and-denominator (pt "a")))
; (map term-to-string (term-to-numerator-and-denominator (pt "a/b")))
; (map term-to-string (term-to-numerator-and-denominator (pt "a*b")))
; (map term-to-string (term-to-numerator-and-denominator (pt "a+b")))
; (map term-to-string (term-to-numerator-and-denominator (pt "(a1/b1)/(a2/b2)")))
; (map term-to-string (term-to-numerator-and-denominator (pt "i#6")))
; (map term-to-string (term-to-numerator-and-denominator (pt "x/y")))
; (map term-to-string (term-to-numerator-and-denominator (pt "x*y")))
; (map term-to-string (term-to-numerator-and-denominator (pt "x+y")))
; (map term-to-string (term-to-numerator-and-denominator (pt "(x1/y1)/(x2/y2)")))

; Next, some operators are applied to the numerator and denominator
; separately: term-to-posmonoms-and-negmonoms needs distribute-prod,
; which distributes * over two lists.

(define (term-to-posmonoms-and-negmonoms term) ;yields a list of monom-lists
  (let* ((op (term-in-app-form-to-final-op term))
	 (args (term-in-app-form-to-args term))
	 (type (term-to-type term))
	 (string (cond ((equal? (py "pos") type) "Pos")
		       ((equal? (py "int") type) "Int")
		       ((equal? (py "rat") type) "Rat")
		       ((equal? (py "real") type) "Real")
		       (else (myerror "term-to-posmonoms-and-negmonoms"
				      "unexpected type"
				      (type-to-string type)))))
	 (make-times-term
	  (lambda (arg1 arg2)
	    (cond ((and (is-gen-numeric-term? arg1)
			(= 1 (gen-numeric-term-to-number arg1)))
		   arg2)
		  ((and (is-gen-numeric-term? arg2)
			(= 1 (gen-numeric-term-to-number arg2)))
		   arg1)
		  (else (mk-term-in-app-form
			 (make-term-in-const-form
			  (pconst-name-to-pconst
			   (string-append string "Times")))
			 arg1 arg2)))))
	 (distribute-prod
	  (lambda (terms1 terms2)
	    (do ((l terms1 (cdr l))
		 (res '() (append res
				  (map (lambda (y) (make-times-term (car l) y))
				       terms2))))
		((null? l) res)))))
    (if
     (or (not (and (term-in-const-form? op)
		   (= 2 (length args))
		   (not (string=? (const-to-name
				   (term-in-const-form-to-const op))
				  "RealConstr"))))
	 (is-gen-numeric-term? term))
     (if (and (term-in-const-form? op) (= 1 (length args))
	      (string=? "S"
			(const-to-name (term-in-const-form-to-const op))))
	 (let* ((arg (car args))
		(prev (term-to-posmonoms-and-negmonoms arg))
		(posprev (car prev))
		(negprev (cadr prev)))
	   (list (append posprev (list (pt "1"))) negprev))
	 (list (list term) '()))
     (let* ((arg1 (car args))
	    (arg2 (cadr args))
	    (prev1 (term-to-posmonoms-and-negmonoms arg1))
	    (prev2 (term-to-posmonoms-and-negmonoms arg2))
	    (posprev1 (car prev1))
	    (negprev1 (cadr prev1))
	    (posprev2 (car prev2))
	    (negprev2 (cadr prev2))
	    (name (const-to-name (term-in-const-form-to-const op)))
	    (l (string-length name)))
       (cond
	((string=? (substring name (max 0 (- l (string-length "Plus"))) l)
		   "Plus")
	 (list (append posprev1 posprev2) (append negprev1 negprev2)))
	((string=? (substring name (max 0 (- l (string-length "Minus"))) l)
		   "Minus")
	 (list (append posprev1 negprev2) (append negprev1 posprev2)))
	((string=? (substring name (max 0 (- l (string-length "Times"))) l)
		   "Times")
	 (list (append (distribute-prod posprev1 posprev2)
		       (distribute-prod negprev1 negprev2))
	       (append (distribute-prod posprev1 negprev2)
		       (distribute-prod negprev1 posprev2))))
	(else (list (list term) '())))))))

; monom-to-num-with-stringpowers collects general numeric terms into a
; product number and writes each factor as a list of a string and its
; power: (27 ("a" 2) ("b" 1) ("c" 3))

(define (monom-to-num-with-stringpowers monom)
  (let ((op (term-in-app-form-to-final-op monom)))
    (if
     (and (term-in-const-form? op)
	  (let* ((name (const-to-name (term-in-const-form-to-const op)))
		 (l (string-length name))
		 (times-string
		  (substring name (max 0 (- l (string-length "Times"))) l)))
	    (string=? "Times" times-string)))
     (let* ((args (term-in-app-form-to-args monom))
	    (arg1 (if (= 2 (length args))
		      (car args)
		      (myerror "monom-to-num-with-stringpowers"
			       "2 args expected"
			       (map term-to-string args))))
	    (arg2 (cadr args))
	    (num-with-stringpowers1 (monom-to-num-with-stringpowers arg1))
	    (num1 (car num-with-stringpowers1))
	    (stringpowers1 (cdr num-with-stringpowers1))
	    (num-with-stringpowers2 (monom-to-num-with-stringpowers arg2))
	    (num2 (car num-with-stringpowers2))
	    (stringpowers2 (cdr num-with-stringpowers2)))
       (cons (* num1 num2) (append stringpowers1 stringpowers2)))
     (if (is-gen-numeric-term? monom)
	 (cons (gen-numeric-term-to-number monom) '())
	 (cons 1 (list (list (term-to-string monom) 1)))))))

; We now aim at term-to-joined-num-joined-stringpowers-list. It sorts
; and joins stringpowers as well as summands.

(define (stringpowers-to-joined-stringpowers stringpowers)
  (if (<= (length stringpowers) 1)
      stringpowers
      (let* ((fst (car stringpowers))
	     (string1 (car fst))
	     (num1 (cadr fst))
	     (prev (stringpowers-to-joined-stringpowers (cdr stringpowers)))
	     (snd (car prev))
	     (string2 (car snd))
	     (num2 (cadr snd)))
	(if (string=? string1 string2)
	    (cons (list string1 (+ num1 num2)) (cdr prev))
	    (cons fst prev)))))

(define (num-stringpowers-list-to-joined-num-joined-stringpowers-list
	 num-stringpowers-list)
  (if (null? num-stringpowers-list)
      '()
      (let* ((fst (car num-stringpowers-list))
	     (num1 (car fst))
	     (joined-stringpowers1
	      (stringpowers-to-joined-stringpowers (cdr fst)))
	     (prev
	      (num-stringpowers-list-to-joined-num-joined-stringpowers-list
	       (cdr num-stringpowers-list))))
	(if (null? prev)
	    (list (cons num1 joined-stringpowers1))
	    (let* ((snd (car prev))
		   (num2 (car snd))
		   (joined-stringpowers2 (cdr snd)))
	      (if (and (= (length joined-stringpowers1)
			  (length joined-stringpowers2))
		       (apply and-op (map stringpower=?
					  joined-stringpowers1
					  joined-stringpowers2)))
		  (if (zero? (+ num1 num2))
		      (cdr prev)
		      (cons (cons (+ num1 num2) joined-stringpowers1)
			    (cdr prev)))
		  (cons (cons num1 joined-stringpowers1) prev)))))))

(define (stringpower<? stringpower1 stringpower2)
  (string<? (car stringpower1) (car stringpower2)))

(define (stringpower=? stringpower1 stringpower2)
  (and (string=? (car stringpower1) (car stringpower2))
       (= (cadr stringpower1) (cadr stringpower2))))

(define (stringpower-and-type-to-term stringpower type)
  (let* ((type-string
	  (cond ((equal? (py "pos") type) "Pos")
		((equal? (py "int") type) "Int")
		((equal? (py "rat") type) "Rat")
		((equal? (py "real") type) "Real")
		(else (myerror "stringpower-and-type-to-term"
			       "unexpected type"
			       (type-to-string type)))))
	 (string (car stringpower))
	 (num (cadr stringpower)))
    (if (= 1 num)
	(pt string)
	(mk-term-in-app-form
	 (make-term-in-const-form
	  (pconst-name-to-pconst (string-append type-string "Exp")))
	 (pt string)
	 (make-numeric-term num)))))

(define (stringpowers-and-type-to-term stringpowers type)
  (if (null? stringpowers)
      (num-and-type-to-gen-numeric-term 1 type)
      (apply mk-* (map (lambda (x) (stringpower-and-type-to-term x type))
		       stringpowers))))

(define (num-stringpowers-and-type-to-term num-stringpowers type)
  (let* ((num (car num-stringpowers))
	 (num-term (num-and-type-to-gen-numeric-term num type))
	 (stringpowers (cdr num-stringpowers)))
    (if (null? stringpowers)
	num-term
	(if (= 1 num)
	    (apply
	     mk-* (map (lambda (x) (stringpower-and-type-to-term x type))
		       stringpowers))
	    (apply
	     mk-* (cons num-term
			(map (lambda (x) (stringpower-and-type-to-term x type))
			     stringpowers)))))))

; Insertion sort

(define (insert x less? sorted-list)
  (if (null? sorted-list)
      (list x)
      (let ((fst (car sorted-list)))
	(if (less? x fst)
	    (cons x sorted-list)
	    (cons fst (insert x less? (cdr sorted-list)))))))

(define (insertsort less? l)
  (if (null? l)
      l
      (insert (car l) less? (insertsort less? (cdr l)))))

; Lexicographic extension of an ordering

(define (lex-ext equality? less?)
  (lambda (l1 l2)
    (and (not (null? l2))
	 (or (null? l1)
	     (let ((fst1 (car l1))
		   (fst2 (car l2)))
	       (or (less? fst1 fst2)
		   (and (equality? fst1 fst2)
			((lex-ext  equality? less?) (cdr l1) (cdr l2)))))))))

(define (mk-+ term . terms)
  (if (null? terms)
      term
      (let* ((init-terms (list-head terms (- (length terms) 1)))
	     (y (car (last-pair terms)))
	     (x (apply mk-+ (cons term init-terms)))
	     (type1 (term-to-type x))
	     (type2 (term-to-type y))
	     (type (types-lub type1 type2))
	     (type-string
	      (cond ((equal? (py "pos") type) "Pos")
		    ((equal? (py "int") type) "Int")
		    ((equal? (py "rat") type) "Rat")
		    ((equal? (py "real") type) "Real")
		    (else (myerror "mk-+" "unexpected type"
				   (type-to-string type)))))
	     (internal-name (string-append type-string "Plus")))
	(mk-term-in-app-form
	 (make-term-in-const-form (pconst-name-to-pconst internal-name))
	 x y))))

(define (mk-* term . terms)
  (if (null? terms)
      term
      (let* ((init-terms (list-head terms (- (length terms) 1)))
	     (y (car (last-pair terms)))
	     (x (apply mk-* (cons term init-terms)))
	     (type1 (term-to-type x))
	     (type2 (term-to-type y))
	     (type (types-lub type1 type2))
	     (type-string
	      (cond ((equal? (py "pos") type) "Pos")
		    ((equal? (py "int") type) "Int")
		    ((equal? (py "rat") type) "Rat")
		    ((equal? (py "real") type) "Real")
		    (else (myerror "mk-*" "unexpected type"
				   (type-to-string type)))))
	     (internal-name (string-append type-string "Times")))
	(mk-term-in-app-form
	 (make-term-in-const-form (pconst-name-to-pconst internal-name))
	 x y))))

(define (mk-/ term1 term2)
  (let* ((type (term-to-type term1))
	 (string (cond ; ((equal? (py "pos") type) "Pos")
; 		       ((equal? (py "int") type) "Int")
		       ((equal? (py "rat") type) "Rat")
		       ((equal? (py "real") type) "Real")
		       (else (myerror "mk-/" "unexpected type"
				      (type-to-string type))))))
    (apply mk-term-in-app-form
	   (cons (make-term-in-const-form
		  (pconst-name-to-pconst (string-append string "Div")))
		 (list term1 term2)))))

; We use ratnums-to-ratnum-and-intnums to turn a list of Scheme
; rationals into a Scheme rational and a list of Scheme integers
; without a common divisor: (n1/d1 n2/d2 n3/d3) -> (n/d (i1 i2 i3))
; such that (n/d)*i1=n1/d1 etc.

(define (ratnums-to-ratnum-and-intnums ratnum . ratnums)
  (let* ((denoms (cons (denominator ratnum) (map denominator ratnums)))
	 (m (apply lcm denoms))
	 (nums (map (lambda (x) (* m x)) (cons ratnum ratnums)))
	 (g (apply gcd nums))
	 (red-nums (map (lambda (x) (/ x g)) nums)))
    (list (/ g m) red-nums)))

; (ratnums-to-ratnum-and-intnums (/ 20 3) (/ 16 4))
; (ratnums-to-ratnum-and-intnums (/ 20 3) (/ 17 4))
; (ratnums-to-ratnum-and-intnums (/ -1 3) (/ 1 4))
; (ratnums-to-ratnum-and-intnums 6 4 32)
; (ratnums-to-ratnum-and-intnums 8 4 32)

(define (nsps-list-to-ratnum-and-nsps-list nsps-list)
  (if (null? nsps-list)
      (list 0 '())
      (let* ((ratnums (map car nsps-list))
	     (sps-list (map cdr nsps-list))
	     (ratnum-and-intnums (apply ratnums-to-ratnum-and-intnums ratnums))
	     (ratnum (car ratnum-and-intnums))
	     (intnums (cadr ratnum-and-intnums)))
	(list ratnum (map (lambda (x y) (cons x y)) intnums sps-list)))))

; We now simplify a quotient of two joined-num-joined-stringpowers-lists
; ((27 ("a1" 2) ("a2" 1)) (9 ("a1" 3)) / ((13) (27 ("b1" 1) ("b2" 3)))
; We turn the numerator and denominator from sums into products, to
; make cancellation possible.  Apply distributivity backwards.
; Uses nsps-list-to-common-sps-and-non-common-nsps-list where
; sps is short for stringpowers, nsps is short for num-stringpowers.
; It is assumed that nums are integers without a common divisor.
; Example:
; (define nspsl '((3 ("a" 1) ("b" 2) ("c" 1)) (4 ("a" 3) ("b" 1) ("c" 1)) (5 ("a" 2) ("b" 2))))
; (nsps-list-to-common-sps-and-non-common-nsps-list nspsl)
; ((("a" 1) ("b" 1)) ;common-sps
;  ((3 ("b" 1) ("c" 1)) (4 ("a" 2) ("c" 1)) (5 ("a" 1) ("b" 1))))
; ((("a" 1) ("b" 1)) ;common-sps
;  (3 ("b" 1) ("c" 1))
;  (4 ("a" 2) ("c" 1))
;  (5 ("a" 1) ("b" 1)))

(define (nsps-list-to-common-sps-and-non-common-nsps-list nsps-list)
  (if (null? nsps-list)
      (list '() '())
      (let* ((nums (map car nsps-list))
	     (sps-list (map cdr nsps-list))
	     (common-sps-and-non-common-sps-list
	      (sps-list-to-common-sps-and-non-common-sps-list sps-list))
	     (common-sps (car common-sps-and-non-common-sps-list))
	     (non-common-sps-list (cadr common-sps-and-non-common-sps-list))
	     (non-common-nsps-list
	      (map (lambda (num sps) (cons num sps))
		   nums non-common-sps-list))
	     (sorted-non-common-nsps-list
	       (insertsort
		(lambda (x y)
		  ((lex-ext stringpower=? stringpower<?) (cdr x) (cdr y)))
		non-common-nsps-list)))
	(list common-sps sorted-non-common-nsps-list))))

(define (sps-list-to-common-sps-and-non-common-sps-list sps-list)
  (if
   (apply and-op (map pair? sps-list))
   (let* ((sps (map car sps-list))
	  (strings (map car sps)))
     (if
      (string-list=? strings)
      (let* ((string (car strings))
	     (powers (map cadr sps))
	     (m (apply min powers))
	     (rest-powers (map (lambda (x) (- x m)) powers)) ;one is 0
	     (red-sps-list
	      (map (lambda (rest-power sps)
		     (if (zero? rest-power)
			 (cdr sps)
			 (cons (list string rest-power) (cdr sps))))
		   rest-powers sps-list))
	     (prev (sps-list-to-common-sps-and-non-common-sps-list
		    red-sps-list))
	     (prev-common-sps (car prev))
	     (prev-non-common-sps-list (cadr prev)))
	(list (cons (list string m) prev-common-sps) prev-non-common-sps-list))
      (let* ((string (apply string-max strings))
	     (ncsps-list
	      (map (lambda (sps)
		     (list-transform-positive sps
		       (lambda (sp) (string<? (car sp) string))))
		   sps-list))
	     (red-sps-list
	      (map (lambda (sps)
		     (list-transform-positive sps
		       (lambda (sp) (not (string<? (car sp) string)))))
		   sps-list))
	     (prev (sps-list-to-common-sps-and-non-common-sps-list
		    red-sps-list))
	     (prev-common-sps (car prev))
	     (prev-non-common-sps-list (cadr prev)))
	(list prev-common-sps (map (lambda (ncsps x) (append ncsps x))
				   ncsps-list prev-non-common-sps-list)))))
   (list '() sps-list)))

(define (string-max string . strings)
  (do ((l strings (cdr l))
       (res string (if (string<? res (car l)) (car l) res)))
      ((null? l) res)))

; (define sps-list '((("a" 1) ("b" 2) ("c" 1)) (("a" 3) ("b" 1) ("c" 1)) (("a" 2) ("b" 2))))
; (sps-list-to-common-sps-and-non-common-sps-list sps-list)

; ((("a" 1) ("b" 1)) ;common-sps
;  ((("b" 1) ("c" 1)) (("a" 2) ("c" 1)) (("a" 1) ("b" 1))))

; Cancellation:  We are given a quotient
; num1 common-sps1 non-common-nsps-list1 /
; num2 common-sps2 non-common-nsps-list2
; and produce a product of (/ num1 num2) and the quotient 
; cancelled-common-sps1 non-common-nsps-list1 /
; cancelled-common-sps2 non-common-nsps-list2
; in case non-common-nsps-list1 and non-common-nsps-list2 differ, and 
; cancelled-common-sps1 / cancelled-common-sps2
; in case non-common-nsps-list1 and non-common-nsps-list2 are equal.
; For this we need cancel-common-sps.

(define (cancel-common-sps sps1 sps2)
  (if
   (or (null? sps1) (null? sps2))
   (list sps1 sps2)
   (let ((s1 (caar sps1))
	 (p1 (cadar sps1))
	 (s2 (caar sps2))
	 (p2 (cadar sps2)))
     (cond
      ((string=? s1 s2)
       (let* ((prev (cancel-common-sps (cdr sps1) (cdr sps2)))
	      (prev-sps1 (car prev))
	      (prev-sps2 (cadr prev)))
	 (cond
	  ((= p1 p2) (list prev-sps1 prev-sps2))
	  ((< p1 p2) (list prev-sps1 (cons (list s2 (- p2 p1)) prev-sps2)))
	  ((> p1 p2) (list (cons (list s1 (- p1 p2)) prev-sps1) prev-sps2)))))
      ((string<? s1 s2)
       (let* ((prev (cancel-common-sps (cdr sps1) sps2))
	      (prev-sps1 (car prev))
	      (prev-sps2 (cadr prev)))
	 (list (cons (car sps1) prev-sps1) prev-sps2)))
      ((string>? s1 s2)
       (let* ((prev (cancel-common-sps sps1 (cdr sps2)))
	      (prev-sps1 (car prev))
	      (prev-sps2 (cadr prev)))
	 (list prev-sps1 (cons (car sps2) prev-sps2))))))))

; (cancel-common-sps '(("a" 3) ("c" 2)) '(("a" 2) ("b" 5) ("c" 3)))
; ((("a" 1)) (("b" 5) ("c" 1)))

; Finally construct the result term: take mk-* for the common-sps and
; mk-+ with mk-* for the non-common-nsps-list.

; The general procedure packaging the previous ones together:

(define (term-to-ratnum-and-common-sps-and-non-common-nsps-list term)
  (let* ((posmonoms-and-negmonoms (term-to-posmonoms-and-negmonoms term))
	 (posmonoms (car posmonoms-and-negmonoms))
	 (negmonoms (cadr posmonoms-and-negmonoms))
	 (pos-num-with-stringpowers-list
	  (list-transform-positive (map monom-to-num-with-stringpowers
					posmonoms)
	    (lambda (x) (not (zero? (car x))))))
	 (neg-num-with-stringpowers-list
	  (list-transform-positive (map monom-to-num-with-stringpowers
					negmonoms)
	    (lambda (x) (not (zero? (car x))))))
	 (num-with-stringpowers-list
	  (append pos-num-with-stringpowers-list
		  (map (lambda (nsps) (cons (- (car nsps)) (cdr nsps)))
		       neg-num-with-stringpowers-list)))
	 (num-with-sorted-stringpowers-list
	  (map (lambda (x) (cons (car x) (insertsort stringpower<? (cdr x))))
	       num-with-stringpowers-list))
	 (sorted-num-with-sorted-stringpowers-list
	  (insertsort
	   (lambda (x y)
	     ((lex-ext stringpower=? stringpower<?) (cdr x) (cdr y)))
	   num-with-sorted-stringpowers-list))
	 (joined-num-joined-stringpowers-list
	  (num-stringpowers-list-to-joined-num-joined-stringpowers-list
	   sorted-num-with-sorted-stringpowers-list))
	 (ratnum-and-nsps-list (nsps-list-to-ratnum-and-nsps-list
				joined-num-joined-stringpowers-list))
	 (ratnum (car ratnum-and-nsps-list))
	 (nsps-list (cadr ratnum-and-nsps-list))
	 (common-sps-and-non-common-nsps-list
	  (nsps-list-to-common-sps-and-non-common-nsps-list nsps-list)))
    (cons ratnum common-sps-and-non-common-nsps-list)))
  
(define (equal-nsps-lists-of-different-signs? nsps-list1 nsps-list2)
  (and (pair? nsps-list1)
       (= (length nsps-list1) (length nsps-list2))
       (let ((nums1 (map car nsps-list1))
	     (nums2 (map car nsps-list2)))
	 (apply and-op (map (lambda (n1 n2) (= n1 (- n2))) nums1 nums2)))
       (let ((sps1 (map cdr nsps-list1))
	     (sps2 (map cdr nsps-list2)))
	 (equal? sps1 sps2))))

;(equal-nsps-lists-of-different-signs? '((1) (-7 ("a" 2))) '((-1) (7 ("a" 2))))

(define (term-to-num-and-sps1-and-nsps-list1-and-sps2-and-nsps-list2 term)
  (let* ((term-with-unfolded-exps
	  (term-to-term-with-unfolded-exponents term))
	 (term-with-arith-free-outer-number-constrs
	  (term-to-term-with-constructors-pushed-inside
	   term-with-unfolded-exps))
	 (numer-and-denom (term-to-numerator-and-denominator
			   term-with-arith-free-outer-number-constrs))
	 (numer (car numer-and-denom))
	 (denom (cadr numer-and-denom))
	 (ratnum-and-common-sps-and-non-common-nsps-list1
	  (term-to-ratnum-and-common-sps-and-non-common-nsps-list numer))
	 (ratnum1 (car ratnum-and-common-sps-and-non-common-nsps-list1))
	 (common-sps1 (cadr ratnum-and-common-sps-and-non-common-nsps-list1))
	 (non-common-nsps-list1
	  (caddr ratnum-and-common-sps-and-non-common-nsps-list1))
	 (ratnum-and-common-sps-and-non-common-nsps-list2
	  (term-to-ratnum-and-common-sps-and-non-common-nsps-list denom))
	 (ratnum2 (car ratnum-and-common-sps-and-non-common-nsps-list2))
	 (common-sps2 (cadr ratnum-and-common-sps-and-non-common-nsps-list2))
	 (non-common-nsps-list2
	  (caddr ratnum-and-common-sps-and-non-common-nsps-list2))
	 (ratnum (/ ratnum1 ratnum2))
	 (cancelled-common-sps (cancel-common-sps common-sps1 common-sps2))
	 (cancelled-common-sps1 (car cancelled-common-sps))
	 (cancelled-common-sps2 (cadr cancelled-common-sps))
	 (equal-nsps-lists? (equal? non-common-nsps-list1
				    non-common-nsps-list2))
	 (diff-signs? (equal-nsps-lists-of-different-signs?
		       non-common-nsps-list1 non-common-nsps-list2))
	 (cancelled-nsps-list1 (cond (equal-nsps-lists? '((1)))
				     (diff-signs? '((-1)))
				     (else non-common-nsps-list1)))
	 (cancelled-nsps-list2 (if (or equal-nsps-lists? diff-signs?)
				   '((1))
				   non-common-nsps-list2)))
    (list ratnum
	  cancelled-common-sps1 cancelled-nsps-list1
	  cancelled-common-sps2 cancelled-nsps-list2)))

; (term-to-num-and-sps1-and-nsps-list1-and-sps2-and-nsps-list2 (pt "(IntN 3#1)*a*a"))
; => (3 (("a" 2)) ((-1)) () ((1)))

; (term-to-num-and-sps1-and-nsps-list1-and-sps2-and-nsps-list2 (pt "(a+b)/((IntN 1#1)*a-b)"))
; => (1 () ((-1)) () ((1)))

(define (nsps-list-and-type-to-term num-stringpowers-list type)
  (if (null? num-stringpowers-list)
      (num-and-type-to-gen-numeric-term 0 type)
      (let ((prod-terms
	     (map (lambda (x) (num-stringpowers-and-type-to-term x type))
		  num-stringpowers-list)))
	(apply mk-+ prod-terms))))

(define (sps-and-nsps-list-and-type-to-pos?-and-term sps nsps-list type)
  (cond
   ((equal? '((1)) nsps-list)
    (list #t (stringpowers-and-type-to-term sps type)))
   ((equal? '((-1)) nsps-list)
    (list #f (stringpowers-and-type-to-term sps type)))
   (else
    (list #t
	  (if (null? sps)
	      (nsps-list-and-type-to-term nsps-list type)
	      (mk-* (apply mk-* (map (lambda (x)
				       (stringpower-and-type-to-term x type))
				     sps))
		    (nsps-list-and-type-to-term nsps-list type)))))))

(define (simp-term term)
  (let* ((x (term-to-num-and-sps1-and-nsps-list1-and-sps2-and-nsps-list2 term))
	 (num (car x))
	 (sps1 (cadr x))
	 (nsps-list1 (caddr x))
	 (sps2 (cadddr x))
	 (nsps-list2 (car (cddddr x)))
	 (type (term-to-type term))
	 (pos1?-and-numer-term
	  (sps-and-nsps-list-and-type-to-pos?-and-term sps1 nsps-list1 type))
	 (pos1? (car pos1?-and-numer-term))
	 (numer-term (cadr pos1?-and-numer-term))
	 (pos2?-and-denom-term
	  (sps-and-nsps-list-and-type-to-pos?-and-term sps2 nsps-list2 type))
	 (pos2? (car pos2?-and-denom-term))
	 (denom-term (cadr pos2?-and-denom-term))
	 (numer-is-1? (and (null? sps1) (equal? '((1)) nsps-list1)))
	 (denom-is-1? (and (null? sps2) (equal? '((1)) nsps-list2)))
	 (pos? (or (and pos1? pos2?) (and (not pos1?) (not pos2?))))
	 (signed-num (if pos? num (- num))))
    (if denom-is-1?
	(if (= 1 signed-num)
	    numer-term
	    (if numer-is-1?
		(num-and-type-to-gen-numeric-term signed-num type)
		(mk-* (num-and-type-to-gen-numeric-term signed-num type)
		      numer-term)))
	(if (= 1 signed-num)
	    (mk-/ numer-term denom-term)
	    (mk-* (num-and-type-to-gen-numeric-term signed-num type)
		  (mk-/ numer-term denom-term))))))

; Tests
; (pp (simp-term (pt "(IntP 1#2)")))
; (pp (simp-term (pt "a/b")))
; (pp (simp-term (pt "(a*a)/b")))
; (pp (simp-term (pt "(a*a)/(a*b)")))
; (pp (simp-term (pt "((IntP 1#2)*a*a)/(a*b)")))
; (pp (simp-term (pt "(a*a+a*b)/(a*b)")))
; (pp (simp-term (pt "a*a+(IntP 2#1)*a*b+b*b")))
; (pp (simp-term (pt "(a+b)*(a+b)")))
; (pp (simp-term (pt "exp(a+b)2")))
; (pp (simp-term (pt "(a+b)/(a+b)")))
; (pp (simp-term (pt "(a+b)*(a+b)/(a+b)")))

; (pp (simp-term (pt "(IntP 1#exp 2(k+1))+(IntP 1#exp 2(k+1))")))

; Tests
; (pp (simp-term (pt "(exp 2(k+1))")))
; (pp (simp-term (pt "(IntP 2#1)*((IntP 1#1)/(IntP 2#1))")))
; (pp (simp-term (pt "(IntP 2#1)*(IntP 1#2)")))
; (pp (simp-term (pt "(IntP 2#1)*(IntP 1#2*3)")))
; (pp (simp-term (pt "(IntP 1#2*3)")))

; (pp (simp-term (pt "exp(1#2)(k+1)")))

; (pp (simp-term (pt "(exp(1#2)(k+1))+(exp(1#2)(k+1))")))
; (pp (simp-term (pt "(exp(1#2)(k+2))+(exp(1#2)(k+1))+(exp(1#2)(k+2))")))

; (pp (simp-term (pt "S(l+l+k)")))

; (pp (simp-term (pt "(x*x)/y")))

(define (positive-num-stringpowers-list? nsps-list type)
  (and (pair? nsps-list)
       (= 1 (length (car nsps-list)))
       (number? (caar nsps-list))
       (positive? (caar nsps-list))
       (apply and-op
	      (map (lambda (nsps)
		     (and (positive? (car nsps))
			  (or (equal? (py "pos") type)
			      (apply and-op
				     (map even? (map cadr (cdr nsps)))))))
		   nsps-list))))

(define (negative-num-stringpowers-list? nsps-list type)
  (and (pair? nsps-list)
       (= 1 (length (car nsps-list)))
       (number? (caar nsps-list))
       (negative? (caar nsps-list))
       (apply and-op
	      (map (lambda (nsps)
		     (and (negative? (car nsps))
			  (or (equal? (py "pos") type)
			      (apply and-op
				     (map even? (map cadr (cdr nsps)))))))
		   nsps-list))))

; (negative-num-stringpowers-list? '((-1) (-3 ("a" 2) ("b" 2) ("c" 6))) (py "rat"))

; (positive-num-stringpowers-list? '((1) (3 ("a" 2) ("b" 2) ("c" 6)) (4 ("a" 4) ("b" 2))) (py "rat"))

(define (term-to-non-zero-strings-and-factor-strings term)
  (let ((op (term-in-app-form-to-final-op term))
	(args (term-in-app-form-to-args term)))
    (if
     (or (not (and (term-in-const-form? op) (= 2 (length args))))
	 (is-gen-numeric-term? term))
     (list '() (list (term-to-string term)))
     (let* ((arg1 (car args))
	    (arg2 (cadr args))
	    (prev1 (term-to-non-zero-strings-and-factor-strings arg1))
	    (non-zero-strings1 (car prev1))
	    (factor-strings1 (cadr prev1))
	    (prev2 (term-to-non-zero-strings-and-factor-strings arg2))
	    (non-zero-strings2 (car prev2))
	    (factor-strings2 (cadr prev2))
	    (name (const-to-name (term-in-const-form-to-const op)))
	    (l (string-length name)))
       (cond
	((or (string=? (substring name (max 0 (- l (string-length "Plus"))) l)
		       "Plus")
	     (string=? (substring name (max 0 (- l (string-length "Minus"))) l)
		       "Minus"))
	 (list (union non-zero-strings1 non-zero-strings2)
	       (list (term-to-string term))))
	((string=? (substring name (max 0 (- l (string-length "Times"))) l)
		   "Times")
	 (list (union non-zero-strings1 non-zero-strings2)
	       (union factor-strings1 factor-strings2)))
	((string=? (substring name (max 0 (- l (string-length "Div"))) l)
		   "Div")
	 (list (union non-zero-strings1 non-zero-strings2 factor-strings2)
	       factor-strings1))
	(else (list '() (list (term-to-string term)))))))))

; (term-to-non-zero-strings-and-factor-strings (pt "(a+c)/b"))
; (term-to-non-zero-strings-and-factor-strings (pt "(a/b)/(c1/c2)"))
; (term-to-non-zero-strings-and-factor-strings (pt "((a+b)*c)/(c1*c2)"))
; (term-to-non-zero-strings-and-factor-strings (pt "(x+z)/y"))
; (term-to-non-zero-strings-and-factor-strings (pt "((x+b)*z)/(z1*z2)"))

(define (term-to-non-zero-strings term)
  (car (term-to-non-zero-strings-and-factor-strings term)))

; simp-comparison simplifies a comparison (using =, <= or <) of two
; terms (of type pos, int or rat).  It proceeds as follows.

; (1) Transform r1=r2 into 0=(r1-r2), and similarly for <= and <. So we
; can assume that the lhs is 0.

; (2) Using the field axioms (in particular commutativity and
; distributivity), bring the rhs in a form number times quotient of two
; terms (numerator and denominator), each of which is a product of some
; powers and a polynomial.

; (3) Simplify, by cancelling equal factors in numerator and
; denominator, removing the denominator by multiplying with the
; (positive) square of the denominator, removing non-zero factors from
; the numerator and reducing power factors to exponent 1 (for =) and 1
; or 2 (for <, <=)

(define (is-comparison? atom-or-pred)
  (or (and (atom-form? atom-or-pred)
	   (let* ((kernel (atom-form-to-kernel atom-or-pred))
		  (op (term-in-app-form-to-final-op kernel)))
	     (and 
	      (term-in-const-form? op)
	      (member (const-to-name (term-in-const-form-to-const op))
		      '("=" "PosLt" "PosLe" "IntLt" "IntLe"
			"RatEq" "RatLt" "RatLe"))
	      (= 2 (length (term-in-app-form-to-args kernel))))))
      (and (predicate-form? atom-or-pred)
	   (let ((pred (predicate-form-to-predicate atom-or-pred)))
	     (and (idpredconst-form? pred)
		  (member (idpredconst-to-name pred)
			  '("RealEq" "RealLe")))))))

(define (positive-exponential-string? string)
  (let* ((term (pt string))
	 (op (term-in-app-form-to-final-op term))
	 (args (term-in-app-form-to-args term)))
    (and (term-in-const-form? op)
	 (member (const-to-name (term-in-const-form-to-const op))
		 '("PosExp" "IntExp" "RatExp" "RealExp"))
	 (= 2 (length args))
	 (is-gen-numeric-term? (car args))
	 (positive? (gen-numeric-term-to-number (car args))))))

(define (simp-comparison atom-or-pred)
  (if
   (is-comparison? atom-or-pred)
   (let* ((name (if (atom-form? atom-or-pred)
		    (const-to-name (term-in-const-form-to-const
				    (term-in-app-form-to-final-op
				     (atom-form-to-kernel atom-or-pred))))
		    (idpredconst-to-name
		     (predicate-form-to-predicate atom-or-pred))))
	  (op-is-=? (member name '("=" "RatEq" "RealEq")))
	  (op-is-<=? (member name '("PosLe" "IntLe" "RatLe" "RealLe")))
	  (op-is-<? (member name '("PosLt" "IntLt" "RatLt")))
	  (args (if (atom-form? atom-or-pred)
		    (term-in-app-form-to-args
		     (atom-form-to-kernel atom-or-pred))
		    (predicate-form-to-args atom-or-pred)))
	  (arg1 (if (= 2 (length args))
		    (car args)
		    (myerror "simp-comparison" "2 args expected"
			     (map term-to-string args))))
	  (arg2 (cadr args))
	  (type (term-to-type arg1))
	  (minus-const
	   (cond
	    ((equal? (py "pos") type) (pconst-name-to-pconst "PosMinus"))
	    ((equal? (py "int") type) (pconst-name-to-pconst "IntMinus"))
	    ((equal? (py "rat") type) (pconst-name-to-pconst "RatMinus"))
	    ((equal? (py "real") type) (pconst-name-to-pconst "RealMinus"))
	    (else (myerror "simp-comparison"
			   "unexpected type" (type-to-string type)))))
	  (x (term-to-num-and-sps1-and-nsps-list1-and-sps2-and-nsps-list2
	      (mk-term-in-app-form
	       (make-term-in-const-form minus-const) arg2 arg1)))
	  (num (car x))
	  (sps1 (cadr x))
	  (nsps-list1 (caddr x))
	  (sps2 (cadddr x))
	  (nsps-list2 (car (cddddr x)))
	  (sps (stringpowers-to-joined-stringpowers
		(insertsort stringpower<? (append sps1 sps2))))
	  (non-zero-strings (union (term-to-non-zero-strings arg1)
				   (term-to-non-zero-strings arg2)))
	  (reduced-sps ;if = delete pos-exp-strings and non-zero-strings,
					;and reduce exps to 1.  Else delete
					;non-zero-strings with even exps and
					;pos-exp-strings, and red exps mod 2
	   (if 
	    op-is-=? 
	    (map (lambda (sp) (list (car sp) 1))
		 (list-transform-positive sps
		   (lambda (sp)
		     (and (not (member (car sp) non-zero-strings))
			  (not (positive-exponential-string? (car sp)))))))
	    (map (lambda (sp) (list (car sp)
				    (if (= 1 (modulo (cadr sp) 2)) 1 2)))
		 (list-transform-positive sps
		   (lambda (sp)
		     (and (not (and (member (car sp) non-zero-strings)
				    (even? (cadr sp))))
			  (not (positive-exponential-string? (car sp)))))))))
	  (pos1? (positive-num-stringpowers-list? nsps-list1 type))
	  (neg1? (negative-num-stringpowers-list? nsps-list1 type))
	  (pos2? (positive-num-stringpowers-list? nsps-list2 type))
	  (neg2? (negative-num-stringpowers-list? nsps-list2 type))
	  (all-neg1?
	   (apply and-op (map (lambda (nsps) (negative? (car nsps)))
			      nsps-list1)))
	  (all-neg2?
	   (apply and-op (map (lambda (nsps) (negative? (car nsps)))
			      nsps-list2)))
	  (negated-nsps-list1 (map (lambda (nsps)
				     (cons (- (car nsps)) (cdr nsps)))
				   nsps-list1))
	  (negated-nsps-list2 (map (lambda (nsps)
				     (cons (- (car nsps)) (cdr nsps)))
				   nsps-list2))
	  (sign-and-not-all-neg-nsps-lists ;cancel non-zero nsps-lists
	   (cond
	    ((or (and pos1? pos2?) (and neg1? neg2?)) (list #t '()))
	    ((or (and pos1? neg2?) (and neg1? pos2?)) (list #f '()))
	    (pos1? (if all-neg2?
		       (list #f (list negated-nsps-list2))
		       (list #t (list nsps-list2))))
	    (neg1? (if all-neg2?
		       (list #t (list negated-nsps-list2))
		       (list #f (list nsps-list2))))
	    (pos2? (if all-neg1?
		       (list #f (list negated-nsps-list1))
		       (list #t (list nsps-list1))))
	    (neg2? (if all-neg1?
		       (list #t (list negated-nsps-list1))
		       (list #f (list nsps-list1))))
	    ((and all-neg1? all-neg2?)
	     (list #t (list negated-nsps-list1 negated-nsps-list2)))
	    ((and all-neg1? (not all-neg2?))
	     (list #f (list negated-nsps-list1 nsps-list2)))
	    ((and (not all-neg1?) all-neg2?)
	     (list #f (list nsps-list1 negated-nsps-list2)))
	    ((and (not all-neg1?) (not all-neg2?))
	     (list #t (list nsps-list1 nsps-list2)))
	    (else (myerror "simp-comparison" "this should not happen"))))
	  (sign (car sign-and-not-all-neg-nsps-lists))
	  (not-all-neg-nsps-lists (cadr sign-and-not-all-neg-nsps-lists)))
     (cond
      ((null? nsps-list1)
       (if (or op-is-=? op-is-<=?) truth falsity))
      ((and (null? reduced-sps) (null? not-all-neg-nsps-lists))
       (if op-is-=? falsity (if sign truth falsity)))
      ((and (null? reduced-sps) (= 1 (length not-all-neg-nsps-lists)))
	 (let* ((nsps-list (car not-all-neg-nsps-lists))
		(pos-nsps-list (list-transform-positive nsps-list
				 (lambda (nsps) (positive? (car nsps)))))
		(neg-nsps-list (list-transform-positive nsps-list
				 (lambda (nsps) (negative? (car nsps)))))
		(abs-neg-nsps-list
		 (map (lambda (nsps) (cons (- (car nsps)) (cdr nsps)))
		      neg-nsps-list))
		(pos-nsps-list-term
		 (nsps-list-and-type-to-term pos-nsps-list type))
		(abs-neg-nsps-list-term
		 (nsps-list-and-type-to-term abs-neg-nsps-list type))
		(term1 (if sign
			   abs-neg-nsps-list-term
			   pos-nsps-list-term))
		(term2 (if sign
			   pos-nsps-list-term
			   abs-neg-nsps-list-term)))
	   (if (atom-form? atom-or-pred)
	       (make-atomic-formula
		(mk-term-in-app-form (term-in-app-form-to-final-op
				      (atom-form-to-kernel atom-or-pred))
				     term1 term2))
	       (make-predicate-formula
		(predicate-form-to-predicate atom-or-pred) term1 term2))))
      ((and (apply and-op (map (lambda (sp) (even? (cadr sp))) reduced-sps))
	    (null? not-all-neg-nsps-lists)
	    sign op-is-<=?)
       truth)
      ((and (apply and-op (map (lambda (sp) (even? (cadr sp))) reduced-sps))
	    (null? not-all-neg-nsps-lists)
	    (not sign) op-is-<?)
       falsity)
      (else
       (let* ((sps-terms (map (lambda (x)
				(stringpower-and-type-to-term x type))
			      reduced-sps))
	      (nsps-terms (map (lambda (nspsl)
				 (nsps-list-and-type-to-term nspsl type))
			       not-all-neg-nsps-lists))
	      (final-term (apply mk-* (append sps-terms nsps-terms)))
	      (term1 (if sign
			 (num-and-type-to-gen-numeric-term 0 type)
			 final-term))
	      (term2 (if sign
			 final-term
			 (num-and-type-to-gen-numeric-term 0 type))))
	 (if (atom-form? atom-or-pred)
	     (make-atomic-formula
	      (mk-term-in-app-form (term-in-app-form-to-final-op
				    (atom-form-to-kernel atom-or-pred))
				   term1 term2))
	     (make-predicate-formula
	      (predicate-form-to-predicate atom-or-pred) term1 term2))))))
   atom-or-pred))

; Tests
; (formula-to-string (simp-comparison (pf "a+b==b+a")))
; (formula-to-string (simp-comparison (pf "a+b<=b+a")))
; (formula-to-string (simp-comparison (pf "a+b<b+a")))

; (formula-to-string (simp-comparison (pf "0==(1+a*a)")))
; (formula-to-string (simp-comparison (pf "0<=(1+a*a)")))
; (formula-to-string (simp-comparison (pf "0<(1+a*a)")))
; (formula-to-string (simp-comparison (pf "0<((IntN 1#1)-a*a)")))

; (formula-to-string (simp-comparison (pf "0==(1-a*a)")))
; (formula-to-string (simp-comparison (pf "0<((IntN 1#1)+a*a)")))

; (formula-to-string (simp-comparison (pf "0<=b*b*(1+a*a)")))

; (formula-to-string (simp-comparison (pf "0<b*b*((IntN 1#1)-a*a)")))

; (formula-to-string (simp-comparison (pf "0<b*b*a*a")))
; (formula-to-string (simp-comparison (pf "0<=(IntN 1#1)*b*b*a*a")))

; (formula-to-string (simp-comparison (pf "j+i+1=i+j")))
; (formula-to-string (simp-comparison (pf "m+n+2=n+m")))
; (formula-to-string (simp-comparison (pf "a*a==(IntN 1#1)")))
; (formula-to-string (simp-comparison (pf "0==(1+a*a)/((IntN 1#1)-a*a)")))

; (formula-to-string (simp-comparison (pf "0<1/(a*a)")))
; (formula-to-string (simp-comparison (pf "0<1/a")))
; (formula-to-string (simp-comparison (pf "0<1/(a*a*(1+b*b+c))")))
; (formula-to-string (simp-comparison (pf "l<=S(l+l+k)")))

; (formula-to-string (simp-comparison (pf "0<exp 2 k")))

; (formula-to-string (simp-comparison (pf "x===x+1")))
; (formula-to-string (simp-comparison (pf "x<<=x+1")))
; (formula-to-string (simp-comparison (pf "0<<=y*y*(1+x*x)")))
; (formula-to-string (simp-comparison (pf "RealLe x(x+1)")))

; (formula-to-string (simp-comparison (pf "c<<=c+1/3*(d-c)")))

; Now: Integration of simp-comparison into interactive proving.

; Given an atomic goal in the form of a comparison (more precisely, an
; equality or a leq- or less-inequality in one of the types pos, int,
; rat or real e.g., a<b), (ord-field-simp-bwd) (1) simplifies the atom
; to simp-atom, using the field axioms, (2) generates a new global
; assumption ex k RealLt 0(abs x)k -> ... 0<abs r -> ...-> simp-atom
; -> atom (with additional hypotheses ex k RealLt 0(abs s)k or 0<abs
; s for every term s corresponding to one of the non-zero-strings),
; and (3) uses this new global assumption to create the new goal
; simp-atom.

; Given a goal with an atomic hypothesis in the form of a comparison,
; (ord-field-simp-fwd) (1) simplifies the hypothesis to simp-atom,
; using the field axioms, (2) generates a new global assumption ex k
; RealLt 0(abs x)k -> ... 0<abs r -> ... -> atom -> simp-atom, and
; (3) uses this new global assumption to create the new goal with the
; simplified hypothesis.

(define (comparison-to-non-zero-strings atom-or-pred)
  (if (is-comparison? atom-or-pred)
      (let* ((args (if (atom-form? atom-or-pred)
		       (term-in-app-form-to-args
			(atom-form-to-kernel atom-or-pred))
		       (predicate-form-to-args atom-or-pred)))
	     (arg1 (car args))
	     (arg2 (cadr args)))
	(union (term-to-non-zero-strings arg1)
	       (term-to-non-zero-strings arg2)))
      '()))
	  
(define (ord-field-simp-bwd)
  (let* ((num-goals (pproof-state-to-num-goals))
         (num-goal (if (null? num-goals)
		       (myerror "cut: num-goals empty")
		       (car num-goals)))
	 (goal (num-goal-to-goal num-goal))
	 (formula (goal-to-formula goal))
	 (simp-fla (if (is-comparison? formula)
		       (simp-comparison formula)
		       (myerror "ord-field-simp-bwd" "comparison expected"
				(formula-to-string formula)))))
    (if (formula=? formula simp-fla)
	(myerror "ord-field-simp-bwd" "formula cannot be simplified"
		 (formula-to-string formula)))
    (let* ((name (new-global-assumption-name "Simp-GA"))
	   (non-zero-strings (comparison-to-non-zero-strings formula))
	   (args (if (atom-form? formula)
		     (term-in-app-form-to-args
		      (atom-form-to-kernel formula))
		     (predicate-form-to-args formula)))
	   (type (term-to-type (car args)))
	   (string (cond ((equal? (py "pos") type) "Pos")
			 ((equal? (py "int") type) "Int")
			 ((equal? (py "rat") type) "Rat")
			 ((equal? (py "real") type) "Real")))
	   (abs-name (string-append string "Abs"))
	   (lt-name (string-append string "Lt"))
	   (non-zero-hyps ;list of hyps ex k RealLt 0(abs s)k or 0<abs s
	    (map (lambda (s)
		   (let ((abs-s (make-term-in-app-form
				 (make-term-in-const-form
				  (pconst-name-to-pconst abs-name))
				 (pt s))))
		     (if (string=? "Real" string)
			 (let ((var (type-to-new-var (py "pos"))))
			   (make-ex
			    var (make-atomic-formula
				 (mk-term-in-app-form
				  (make-term-in-const-form
				   (pconst-name-to-pconst lt-name))
				  (num-and-type-to-gen-numeric-term 0 type)
				  abs-s (make-term-in-var-form var)))))
			 (make-atomic-formula
			  (mk-term-in-app-form
			   (make-term-in-const-form
			    (pconst-name-to-pconst lt-name))
			   (num-and-type-to-gen-numeric-term 0 type)
			   abs-s)))))
		 non-zero-strings))
	   (real-vars (list-transform-positive (formula-to-free formula)
			(lambda (v) (equal? (py "real") (var-to-type v)))))
	   (real-hyps ;list of hypotheses Real x
	    (map (lambda (v)
		   (make-predicate-formula
		    (make-idpredconst "Real" '() '())
		    (make-term-in-var-form v)))
		 real-vars)))
      (if (formula=? truth simp-fla)
	  (let* ((imp-formula
		  (apply mk-imp (append real-hyps non-zero-hyps
					(list formula))))
		 (vars (formula-to-free imp-formula))
		 (varterms (map make-term-in-var-form vars)))
	    (add-global-assumption
	     name (apply mk-all (append vars (list imp-formula))))
	    (apply
	     use-with
	     (append (list name)
		     varterms
		     (apply
		      list (map (lambda (x) DEFAULT-GOAL-NAME)
				(append real-hyps non-zero-hyps))))))
	  (let* ((imp-formula
		  (apply mk-imp (append real-hyps non-zero-hyps
					(list simp-fla formula))))
		 (vars (formula-to-free imp-formula))
		 (varterms (map make-term-in-var-form vars)))
	    (add-global-assumption
	     name (apply mk-all (append vars (list imp-formula))))
	    (apply
	     use-with
	     (append (list name)
		     varterms
		     (apply
		      list (map (lambda (x) DEFAULT-GOAL-NAME)
				(append real-hyps non-zero-hyps)))
		     (list DEFAULT-GOAL-NAME))))))))

; (set-goal (pf "all a,b.a+b==b+a"))
; (strip)
; (ord-field-simp-bwd)

; (set-goal (pf "all a,b.0<abs a -> 0<abs b ->
;                0<=a*b*((IntN 1#1)*a+b) ->
;                1/b<=1/a"))
; (strip)
; (ord-field-simp-bwd)
; (auto)

; (display-global-assumptions "Simp-GA1")

; ord-field-simp-fwd does for forward chaining the same as
; ord-field-simp-bwd for backward chaining.  It replaces the present
; goal by a new one, with one additional hypothesis obtained by
; instantiating a previous one.  In the following definition of
; ord-field-simp-fwd x is a number or string identifying a hypothesis
; form the context.

(define (ord-field-simp-fwd x)
  (let* ((num-goals (pproof-state-to-num-goals))
         (num-goal (if (null? num-goals)
		       (myerror "cut: num-goals empty")
		       (car num-goals)))
	 (goal (num-goal-to-goal num-goal))
	 (hypname-info (num-goal-to-hypname-info num-goal))
	 (context (goal-to-context goal))
	 (avars (context-to-avars context))
	 (maxhyp (length avars))
	 (formula (goal-to-formula goal))
	 (x-formula
	  (cond
	   ((and (integer? x) (positive? x))
	    (if (<= x maxhyp)
		(avar-to-formula (list-ref avars (- x 1)))
		(myerror "ord-field-simp-fwd" "assumption number expected" x)))
	   ((and (string? x)
		 (member x (hypname-info-to-names hypname-info)))
	    (let ((i (name-and-hypname-info-to-index x hypname-info)))
	      (if (<= i maxhyp)
		  (avar-to-formula (list-ref avars (- i 1)))
		  (myerror
		   "ord-field-simp-fwd" "assumption number expected" i))))
	   (else (myerror "ord-field-simp-fwd" "illegal first argument" x))))
	 (simp-fla (if (is-comparison? x-formula)
		       (simp-comparison x-formula)
		       (myerror "ord-field-simp-fwd" "comparison expected"
				(formula-to-string x-formula)))))
    (if (formula=? x-formula simp-fla)
	(myerror "ord-field-simp-fwd" "formula cannot be simplified"
		 (formula-to-string x-formula)))
    (let* ((name (new-global-assumption-name "Simp-GA"))
	   (non-zero-strings (comparison-to-non-zero-strings x-formula))
	   (args (if (atom-form? x-formula)
		     (term-in-app-form-to-args
		      (atom-form-to-kernel x-formula))
		     (predicate-form-to-args x-formula)))
	   (type (term-to-type (car args)))
	   (string (cond ((equal? (py "pos") type) "Pos")
			 ((equal? (py "int") type) "Int")
			 ((equal? (py "rat") type) "Rat")
			 ((equal? (py "real") type) "Real")))
	   (abs-name (string-append string "Abs"))
	   (lt-name (string-append string "Lt"))
	   (non-zero-hyps ;list of hyps ex k RealLt 0(abs s)k or 0<abs s
	    (map (lambda (s)
		   (let ((abs-s (make-term-in-app-form
				 (make-term-in-const-form
				  (pconst-name-to-pconst abs-name))
				 (pt s))))
		     (if (string=? "real" string)
			 (let ((var (type-to-new-var (py "pos"))))
			   (make-ex
			    var (make-atomic-formula
				 (mk-term-in-app-form
				  (make-term-in-const-form
				   (pconst-name-to-pconst lt-name))
				  (num-and-type-to-gen-numeric-term 0 type)
				  abs-s (make-term-in-var-form var)))))
			 (make-atomic-formula
			  (mk-term-in-app-form
			   (make-term-in-const-form
			    (pconst-name-to-pconst lt-name))
			   (num-and-type-to-gen-numeric-term 0 type)
			   abs-s)))))
		 non-zero-strings))
	   (real-vars (list-transform-positive (formula-to-free x-formula)
			(lambda (v) (equal? (py "real") (var-to-type v)))))
	   (real-hyps ;list of hypotheses Real x
	    (map (lambda (v)
		   (make-predicate-formula
		    (make-idpredconst "Real" '() '())
		    (make-term-in-var-form v)))
		 real-vars))
	   (imp-formula (apply mk-imp (append real-hyps non-zero-hyps
					      (list x-formula simp-fla))))
	   (vars (formula-to-free imp-formula))
	   (varterms (map make-term-in-var-form vars)))
      (add-global-assumption
       name (apply mk-all (append vars (list imp-formula))))
      (apply inst-with
	     (append (list name)
		     varterms
		     (apply
		      list (map (lambda (x)
				  DEFAULT-GOAL-NAME)
				(append real-hyps non-zero-strings)))
		     (list x))))))