Connect semantics in realPolyScript to HOL4 polynomial semantics
We do not yet have a proof that relates our polynomial semantics in realPolyScript
to the polynomial semantics in HOL4's $HOLDIR/src/real/polyScript
(https://github.com/HOL-Theorem-Prover/HOL/blob/develop/src/real/polyScript.sml) semantics.
Ideally the proof would be done in realPolyProofsScript
.