anchor.diff:              (* ------------------------------------------------------------------------- *)
   
               let MONOMIAL_ADD_CONV tm = 
  -                let l, r = dest_add tm
  -                if is_semiring_constant l && is_semiring_constant r
  -                then SEMIRING_ADD_CONV tm
  +                choice {
  +                    let! l, r = dest_add tm
  +                    if is_semiring_constant l && is_semiring_constant r then 
  +                        return! SEMIRING_ADD_CONV tm
  +                    else 
  +                        let th1 = 
  +                            choice {
  +                                let! l' = lhand l
  +                                if is_mul l && is_semiring_constant l' then 
  +                                    let! r' = lhand r
  +                                    if is_mul r && is_semiring_constant r' then
  +                                        let! tm1 = rand r
  +                                        return! INST [l', a_tm; r', b_tm; tm1, m_tm] pthm_02
  +                                    else 
  +                                        return! INST [l', a_tm; r, m_tm] pthm_03
  +                                else
  +                                    let! r' = lhand r
  +                                    if is_mul r && is_semiring_constant r' then 
  +                                        return! INST [r', a_tm; l, m_tm] pthm_04
  +                                    else 
  +                                        return! INST [r, m_tm] pthm_05
  +                            }
  +
  +                        let! tm1' = Choice.bind (rand << concl) th1
  +                        let! tm1, tm2 = dest_comb tm1'
  +                        let! tm3, tm4 = dest_comb tm1
  +                        let th2 = AP_TERM tm3 (SEMIRING_ADD_CONV tm4)
  +                        let th3 = TRANS th1 (AP_THM th2 tm2)
  +                        let! tm5 = Choice.bind (rand << concl) th3
  +                        let! tm2' = lhand tm5
  +                        if tm2' = zero_tm then 
  +                            let! tm3' = rand tm5
  +                            return! TRANS th3 (INST [tm3', m_tm] pthm_06)
  +                        else 
  +                            return! MONOMIAL_DEONE th3
  +                }
  +
  +            (* ------------------------------------------------------------------------- *)
  +            (* Ordering on monomials.                                                    *)
  +            (* ------------------------------------------------------------------------- *)
  +
  +            let powervars tm = 
  +                let ptms = striplist (Choice.toOption << dest_mul) tm
  +                
  +                if is_semiring_constant(hd ptms) then 
  +                    tl ptms
                   else 
  -                    let th1 = 
  -                        if is_mul l && is_semiring_constant(Choice.get <| lhand l)
  -                        then 
  -                            if is_mul r 
  -                                && is_semiring_constant(Choice.get <| lhand r)
  -                            then 
  -                                INST [Choice.get <| lhand l, a_tm;
  -                                        Choice.get <| lhand r, b_tm;
  -                                        Choice.get <| rand r, m_tm] pthm_02
  -                            else 
  -                                INST [Choice.get <| lhand l, a_tm;
  -                                        r, m_tm] pthm_03
  -                        elif is_mul r 
  -                                && is_semiring_constant(Choice.get <| lhand r)
  -                        then 
  -                            INST [Choice.get <| lhand r, a_tm;
  -                                    l, m_tm] pthm_04
  -                        else INST [r, m_tm] pthm_05
  -                    let tm1, tm2 = Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th1))
  -                    let tm3, tm4 = Choice.get <| dest_comb tm1
  -                    let th2 = AP_TERM tm3 (SEMIRING_ADD_CONV tm4)
  -                    let th3 = TRANS th1 (AP_THM th2 tm2)
  -                    let tm5 = Choice.get <| rand(concl <| Choice.get th3)
  -                    if Choice.get <| lhand tm5 = zero_tm
  -                    then TRANS th3 (INST [Choice.get <| rand tm5, m_tm] pthm_06)
  -                    else MONOMIAL_DEONE th3
  -
  -            (* ------------------------------------------------------------------------- *)
  -            (* Ordering on monomials.                                                    *)
  -            (* ------------------------------------------------------------------------- *)
  -
  -            let powervars tm = 
  -                let ptms = striplist (Some << dest_mul) tm
  -                if is_semiring_constant(hd ptms)
  -                then tl ptms
  -                else ptms
  +                    ptms
  +
               let dest_varpow tm = 
                   try 
  -                    let x, n = dest_pow tm
  +                    let x, n = Choice.get <| dest_pow tm
                       (x, Choice.get <| dest_numeral n)
                   with
                   | Failure _ -> 
  -                    (tm, (if is_semiring_constant tm
  -                            then num_0
  -                            else num_1))
  +                    (tm, if is_semiring_constant tm then num_0 else num_1)
  +
               let morder = 
                   let rec lexorder l1 l2 = 
                       match (l1, l2) with
  
positive.code: 
              let POLYNOMIAL_MUL_CONV = 
                  let rec PMUL tm = 
                      let l, r = dest_mul tm
                      if not(is_add l)
                      then POLYNOMIAL_MONOMIAL_MUL_CONV tm
                      elif not(is_add r)
                      then 
                          let th1 = INST [l, a_tm; r, b_tm] pthm_09
                          TRANS th1 
                              (POLYNOMIAL_MONOMIAL_MUL_CONV
                                      (Choice.get <| rand(concl <| Choice.get th1)))
                      else 
                          let a, b = dest_add l
                          let th1 = 
                              INST [a, a_tm; b, b_tm; r, c_tm] pthm_10
                          let tm1, tm2 = Choice.get <| dest_comb(Choice.get <| rand(concl <| Choice.get th1))
                          let tm3, tm4 = Choice.get <| dest_comb tm1
                          let th2 = 
                              AP_TERM tm3 
                                  (POLYNOMIAL_MONOMIAL_MUL_CONV tm4)
                          let th3 = TRANS th1 (MK_COMB(th2, PMUL tm2))
                          TRANS th3 
                              (POLYNOMIAL_ADD_CONV(Choice.get <| rand(concl <| Choice.get th3)))
                  fun tm -> 
                      let l, r = dest_mul tm
                      if l = zero_tm
                      then INST [r, a_tm] pthm_11
                      elif r = zero_tm
                      then INST [l, a_tm] pthm_12
                      elif l = one_tm
                      then INST [r, a_tm] pthm_13
                      elif r = one_tm
                      then INST [l, a_tm] pthm_14
                      else PMUL tm
  
              (* ------------------------------------------------------------------------- *)
              (* Power of polynomial (optimized for the monomial and trivial cases).       *)
  
negative.code: 
              let POLYNOMIAL_ADD_CONV = 
                  let DEZERO_RULE th = 
                      choice {
                          let! tm = Choice.bind (rand << concl) th
                          if not(is_add tm) then 
                              return! th
                          else 
                              let! lop, r = dest_comb tm
                              let! l = rand lop
                              if l = zero_tm then 
                                  return! TRANS th (INST [r, a_tm] pthm_07)
                              elif r = zero_tm then 
                                  return! TRANS th (INST [l, a_tm] pthm_08)
                              else 
                                  return! th
                      }
  
                  let rec PADD tm = 
                      choice {
                          let! l, r = dest_add tm
                          if l = zero_tm then 
                              return! INST [r, a_tm] pthm_07
                          elif r = zero_tm then 
                              return! INST [l, a_tm] pthm_08
                          elif is_add l then 
                              let! a, b = dest_add l
                              if is_add r then 
                                  let! c, d = dest_add r
                                  let ord = morder a c
                                  if ord = 0 then 
                                      let th1 = 
                                          INST [a, a_tm;
                                                b, b_tm;
                                                c, c_tm;
                                                d, d_tm] pthm_23
                                      let! tm1' = Choice.bind (rand << concl) th1
                                      let! tm1, tm2 = dest_comb tm1'
                                      let! tm3, tm4 = dest_comb tm1
                                      let th2 = AP_TERM tm3 (MONOMIAL_ADD_CONV tm4)
                                      return! DEZERO_RULE(TRANS th1 (MK_COMB(th2, PADD tm2)))
                                  else 
                                      let th1 = 
                                          if ord > 0 then 
                                              INST [a, a_tm;
                                                    b, b_tm;
                                                    r, c_tm] pthm_24
                                          else 
                                              INST [l, a_tm;
                                                    c, c_tm;
                                                    d, d_tm] pthm_25
                                      let! tm1' = Choice.bind (rand << concl) th1
                                      let! tm1, tm2 = dest_comb tm1'
                                      return! DEZERO_RULE(TRANS th1 (AP_TERM tm1 (PADD tm2)))
                              else 
                                  let ord = morder a r
                                  if ord = 0 then 
                                      let th1 = 
                                          INST [a, a_tm;
                                                b, b_tm;
                                                r, c_tm] pthm_26
                                      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 (MONOMIAL_ADD_CONV tm4)) tm2
                                      return! DEZERO_RULE(TRANS th1 th2)
                                  elif ord > 0 then 
                                      let th1 = 
                                          INST [a, a_tm;
                                                b, b_tm;
                                                r, c_tm] pthm_24
                                      let! tm1' = Choice.bind (rand << concl) th1
                                      let! tm1, tm2 = dest_comb tm1'
                                      return! DEZERO_RULE(TRANS th1 (AP_TERM tm1 (PADD tm2)))
                                  else 
                                      return! DEZERO_RULE(INST [l, a_tm; r, c_tm] pthm_27)
                          elif is_add r then 
                              let! c, d = dest_add r
                              let ord = morder l c
                              if ord = 0 then 
                                  let th1 = 
                                      INST [l, a_tm;
                                            c, c_tm;
                                            d, d_tm] pthm_28
                                  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 (MONOMIAL_ADD_CONV tm4)) tm2
                                  return! DEZERO_RULE(TRANS th1 th2)
                              elif ord > 0 then 
                                  return! REFL tm
                              else 
                                  let th1 = 
                                      INST [l, a_tm;
                                            c, c_tm;
                                            d, d_tm] pthm_25
                                  let! tm1' = Choice.bind (rand << concl) th1
                                  let! tm1, tm2 = dest_comb tm1'
                                  return! DEZERO_RULE(TRANS th1 (AP_TERM tm1 (PADD tm2)))
                          else 
                              let ord = morder l r
                              if ord = 0 then 
                                  return! MONOMIAL_ADD_CONV tm
                              elif ord > 0 then 
                                  return! DEZERO_RULE(REFL tm)
                              else 
                                  return! DEZERO_RULE(INST [l, a_tm; r, c_tm] pthm_27)
                      }
  
                  PADD
  
              (* ------------------------------------------------------------------------- *)
  