steps.txt

(FPCore (a b c) (/ (* c -2.0) (+ b (sqrt (+ (pow b 2.0) (* c (* a -4.0)))))))
+-commutative
[ 2, 2, 1 ]
ltr
=========================
(FPCore (a b c) (/ (* c -2.0) (+ b (sqrt (+ (* c (* a -4.0)) (pow b 2.0))))))
*-commutative
[ 1 ]
ltr
=========================
(FPCore (a b c) (/ (* -2.0 c) (+ b (sqrt (+ (* c (* a -4.0)) (pow b 2.0))))))
*-rgt-identity
[ 1, 2 ]
ltr
=========================
(FPCore (a b c)
 (/ (* -2.0 (* c 1.0)) (+ b (sqrt (+ (* c (* a -4.0)) (pow b 2.0))))))
*-inverses
[ 1, 2, 2 ]
ltr
=========================
(FPCore (a b c)
 (/ (* -2.0 (* c (/ a a))) (+ b (sqrt (+ (* c (* a -4.0)) (pow b 2.0))))))
associate-/l*
[ 1, 2 ]
ltr
=========================
(FPCore (a b c)
 (/ (* -2.0 (/ (* c a) a)) (+ b (sqrt (+ (* c (* a -4.0)) (pow b 2.0))))))
*-rgt-identity
[ 1 ]
ltr
=========================
(FPCore (a b c)
 (/
  (* (* -2.0 (/ (* c a) a)) 1.0)
  (+ b (sqrt (+ (* c (* a -4.0)) (pow b 2.0))))))
associate-*r/
[]
ltr
=========================
(FPCore (a b c)
 (*
  (* -2.0 (/ (* c a) a))
  (/ 1.0 (+ b (sqrt (+ (* c (* a -4.0)) (pow b 2.0)))))))
#f
[]
goal
=========================

test.mjs

import { strict as assert } from 'node:assert'; 

const frmla = '(FPCore (a b c):name "quadp (p42, positive)"' +
 "(let ([d (sqrt (- (* b b) (* 4 (* a c))))])" +
   "(/ (+ (- b) d) (* 2 a))))"

const sample = (await(await fetch('http://127.0.0.1:8000/api/sample', { method: 'POST', body: JSON.stringify({ 
    formula: frmla, seed: 5 }) })).json())

const SAMPLE_SIZE = 8000
assert.ok(sample.points)
const points = sample.points

const alternatives = (await (await fetch('http://127.0.0.1:8000/api/alternatives', { method: 'POST', body: JSON.stringify({ 
    formula: frmla, 
    sample: points }) })).json()) 

var proof = alternatives.derivations[0].prev.prev.prevs[2].proof

proof.reverse()

for(var step in proof) {
    console.log(proof[step].program)
    console.log(proof[step].rule)
    console.log(proof[step].loc)
    console.log(proof[step].direction)
    console.log("=========================")
}