Error

Derivation

1. Initial program 31.6

   \[\log \left(x + \sqrt{x \cdot x - 1}\right)\]
2. Using strategy rm

3. Applied *-un-lft-identity31.6

   \[\leadsto \log \left(x + \sqrt{x \cdot x - \color{blue}{1 \cdot 1}}\right)\]

4. Applied *-commutative31.6

   \[\leadsto \log \left(x + \sqrt{\color{blue}{x \cdot x} - 1 \cdot 1}\right)\]

5. Applied difference-of-squares31.6

   \[\leadsto \log \left(x + \sqrt{\color{blue}{\left(x + 1\right) \cdot \left(x - 1\right)}}\right)\]

6. Applied sqrt-prod0.1

   \[\leadsto \log \left(x + \color{blue}{\sqrt{x + 1} \cdot \sqrt{x - 1}}\right)\]

7. Final simplification0.1

   \[\leadsto \log \left(x + \sqrt{1 + x} \cdot \sqrt{x - 1}\right)\]

Reproduce

herbie shell --seed 2019088 
(FPCore (x)
  :name "Hyperbolic arc-cosine"
  (log (+ x (sqrt (- (* x x) 1)))))