The theory of fractions s / t, with s, t
taken from some ring.
The theory of fractions s / t, with s, t
taken from some ring. The theory uses an encoding in which the same
(fixed, but arbitrary) denominator is used for all expressions. The
range of considered denominators is described by the
denomConstraint argument over the variable _0.
The theory of fractions
s / t
, withs, t
taken from some ring. The theory uses an encoding in which the same (fixed, but arbitrary) denominator is used for all expressions. The range of considered denominators is described by thedenomConstraint
argument over the variable_0
.