anchor.diff:                      | vps, [] -> -1
                       | [], vps -> 1
                       | ((x1, n1) :: vs1), ((x2, n2) :: vs2) -> 
  -                        if variable_order x1 x2
  -                        then 1
  -                        elif variable_order x2 x1
  -                        then -1
  -                        elif n1 < n2
  -                        then -1
  -                        elif n2 < n1
  -                        then 1
  +                        if variable_order x1 x2 then 1
  +                        elif variable_order x2 x1 then -1
  +                        elif n1 < n2 then -1
  +                        elif n2 < n1 then 1
                           else lexorder vs1 vs2
  +
                   fun tm1 tm2 -> 
                       let vdegs1 = map dest_varpow (powervars tm1)
                       let vdegs2 = map dest_varpow (powervars tm2)
                       let deg1 = itlist ((+) << snd) vdegs1 num_0
                       let deg2 = itlist ((+) << snd) vdegs2 num_0
  -                    if deg1 < deg2
  -                    then -1
  -                    elif deg1 > deg2
  -                    then 1
  +                    
  +                    if deg1 < deg2 then -1
  +                    elif deg1 > deg2 then 1
                       else lexorder vdegs1 vdegs2
   
               (* ------------------------------------------------------------------------- *)
  
positive.code: 
              let POLYNOMIAL_MONOMIAL_MUL_CONV = 
                  let rec PMM_CONV tm = 
                      let l, r = dest_mul tm
                      try 
                          let y, z = dest_add r
                          let th1 = 
                              INST [l, x_tm; y, y_tm; z, z_tm] pthm_37
                          let tm1, tm2 = Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th1))
                          let tm3, tm4 = Choice.get <| dest_comb tm1
                          let th2 = 
                              MK_COMB
                                  (AP_TERM tm3 (MONOMIAL_MUL_CONV tm4), 
                                      PMM_CONV tm2)
                          TRANS th1 th2
                      with
                      | Failure _ -> MONOMIAL_MUL_CONV tm
                  PMM_CONV
  
              (* ------------------------------------------------------------------------- *)
  
negative.code: 
              let MONOMIAL_MUL_CONV = 
                  let powvar tm = 
                      choice {
                          if is_semiring_constant tm then 
                              return one_tm
                          else
                              return!  
                                  choice { 
                                      let! lop, r = dest_comb tm
                                      let! op, l = dest_comb lop
                                      if op = pow_tm && is_numeral r then 
                                          return l
                                      else 
                                          return! Choice.failwith ""
                                  }
                                  |> Choice.bindError (fun _ -> Choice.result tm)
                      }
  
                  let vorder x y = 
                      if x = y then 0
                      elif x = one_tm then -1
                      elif y = one_tm then 1
                      elif variable_order x y then -1
                      else 1
  
                  let rec MONOMIAL_MUL tm l r = 
                      choice { 
                        let! lx, ly = dest_mul l
                        let! vl = powvar lx
                        return!
                          choice { 
                              let! rx, ry = dest_mul r
                              let! vr = powvar rx
                              let ord = vorder vl vr
                              if ord = 0 then 
                                  let th1 = 
                                      INST [lx, lx_tm;
                                            ly, ly_tm;
                                            rx, rx_tm;
                                            ry, ry_tm] pthm_15
                                  let! tm1' = Choice.bind (rand << concl) th1
                                  let! tm1, tm2 = dest_comb tm1'
                                  let! tm3, tm4 = dest_comb tm1
                                  let th2 = AP_THM (AP_TERM tm3 (POWVAR_MUL_CONV tm4)) tm2
                                  let th3 = TRANS th1 th2
                                  let! tm2' = Choice.bind (rand << concl) th3
                                  let! tm5, tm6 = dest_comb tm2'
                                  let! tm7, tm8 = dest_comb tm6
                                  let! tm3' = rand tm7
                                  let th4 = MONOMIAL_MUL tm6 tm3' tm8
                                  return! TRANS th3 (AP_TERM tm5 th4)
                              else 
                                  let th0 = 
                                      if ord < 0 then pthm_16
                                      else pthm_17
                                  let th1 = 
                                      INST [lx, lx_tm;
                                            ly, ly_tm;
                                            rx, rx_tm;
                                            ry, ry_tm] th0
                                  let! tm1' = Choice.bind (rand << concl) th1
                                  let! tm1, tm2 = dest_comb tm1'
                                  let! tm3, tm4 = dest_comb tm2
                                  let! tm2' = rand tm3
                                  return! TRANS th1 (AP_TERM tm1 (MONOMIAL_MUL tm2 tm2' tm4))
                          }
                          |> Choice.bindError (fun _ -> 
                              choice {
                                  let! vr = powvar r
                                  let ord = vorder vl vr
                                  if ord = 0 then 
                                      let th1 = 
                                          INST [lx, lx_tm;
                                                ly, ly_tm;
                                                r, rx_tm] pthm_18
                                      let! tm1' = Choice.bind (rand << concl) th1
                                      let! tm1, tm2 = dest_comb tm1'
                                      let! tm3, tm4 = dest_comb tm1
                                      let th2 = AP_THM (AP_TERM tm3 (POWVAR_MUL_CONV tm4)) tm2
                                      return! TRANS th1 th2
                                  elif ord < 0 then 
                                      let th1 = 
                                          INST [lx, lx_tm;
                                                ly, ly_tm;
                                                r, rx_tm] pthm_19
                                      let! tm1' = Choice.bind (rand << concl) th1
                                      let! tm1, tm2 = dest_comb tm1'
                                      let! tm3, tm4 = dest_comb tm2
                                      let! tm2' = rand tm3
                                      return! TRANS th1 (AP_TERM tm1 (MONOMIAL_MUL tm2 tm2' tm4))
                                  else 
                                      return! INST [l, lx_tm; r, rx_tm] pthm_20})
                      }
                      |> Choice.bindError (fun _ -> 
                          let vl = powvar l
                          choice { 
                              let! vl = vl
                              let! rx, ry = dest_mul r
                              let! vr = powvar rx
                              let ord = vorder vl vr
                              if ord = 0 then 
                                  let th1 = 
                                      INST [l, lx_tm;
                                            rx, rx_tm;
                                            ry, ry_tm] pthm_21
                                  let! tm1' = Choice.bind (rand << concl) th1
                                  let! tm1, tm2 = dest_comb tm1'
                                  let! tm3, tm4 = dest_comb tm1
                                  return! TRANS th1 (AP_THM (AP_TERM tm3 (POWVAR_MUL_CONV tm4)) tm2)
                              elif ord > 0 then 
                                  let th1 = 
                                      INST [l, lx_tm;
                                            rx, rx_tm;
                                            ry, ry_tm] pthm_22
                                  let! tm1' = Choice.bind (rand << concl) th1
                                  let! tm1, tm2 = dest_comb tm1'
                                  let! tm3, tm4 = dest_comb tm2
                                  let! tm2' = rand tm3
                                  return! TRANS th1 (AP_TERM tm1 (MONOMIAL_MUL tm2 tm2' tm4))
                              else 
                                  return! REFL tm
                          }
                          |> Choice.bindError (fun _ -> 
                              choice {
                                  let! vl = vl
                                  let! vr = powvar r
                                  let ord = vorder vl vr
                                  if ord = 0 then 
                                      return! POWVAR_MUL_CONV tm
                                  elif ord > 0 then 
                                      return! INST [l, lx_tm; r, rx_tm] pthm_20
                                  else 
                                      return! REFL tm
                              }))
  
                  fun tm -> 
                      choice {
                          let! l, r = dest_mul tm
                          return! MONOMIAL_DEONE(MONOMIAL_MUL tm l r)
                      }
  
              (* ------------------------------------------------------------------------- *)
              (* Multiplication by monomial of a polynomial.                               *)
  