help links subscribe changes refresh edit

	Manipulating Expressions
	↑

SandBoxDomainOfComputation

Edit detail for SandBoxDomainOfComputation revision 4 of 7

	1 2 3 4 5 6 7
Editor: Bill Page Time: 2017/04/13 20:44:11 GMT+0
Note: multiplication

added:
-- default assumptions about constants

added:
\end{axiom}

Inference rules
\begin{axiom}

added:
  assume(assume(x,'integer),'nonZero) == assume(x,'nonZero)

added:
  assume(assume(x,'nonNegativeInteger),'nonZero) == assume(x,'positiveInteger)

added:
  assume(assume(x,'positiveInteger),'nonZero) == assume(x,'positive)
  --
  assume(assume(x,'nonZero),'integer) == assume(x,'nonZero)
  assume(assume(x,'nonZero),'nonNegativeInteger) == assume(x,'positiveInteger)
  assume(assume(x,'nonZero),'positiveInteger) == assume(x,'positiveInteger)
  assume(assume(x,'nonZero),'nonZero) == assume(x,'nonZero)

added:
  assume(x,'integer) + assume(y,'nonZero) == assume(x+y,'integer)

changed:
-  assume(x,'nonNegativeInteger) + assume(y,'positiveInteger) == assume(x+y,'nonNegativeInteger)
-  assume(x,'positiveInteger)+assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
-  assume(x,'positiveInteger)+assume(y,'nonNegativeInteger) == assume(x+y,'positiveInteger)
  assume(x,'nonNegativeInteger) + assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
  assume(x,'nonNegativeInteger) + assume(y,'nonZero) == assume(x+y, 'integer)
  assume(x,'positiveInteger) + assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
  assume(x,'positiveInteger) + assume(y,'nonNegativeInteger) == assume(x+y,'positiveInteger)
  assume(x,'positiveInteger) + assume(y,'nonZero) == assume(x+y,'integer)
  assume(x,'nonZero) + assume(y,'nonZero) == assume(x+y,'integer)
  --
  assume(x,'integer) * assume(y,'integer) == assume(x*y,'integer)
  assume(x,'integer) * assume(y,'nonNegativeInteger) == assume(x*y,'integer)
  assume(x,'integer) * assume(y,'positiveInteger) == assume(x*y,'integer)
  assume(x,'integer) * assume(y,'nonZero) == assume(x*y,'integer)
  assume(x,'nonNegativeInteger) * assume(y,'nonNegativeInteger) == assume(x*y,'nonNegativeInteger)
  assume(x,'nonNegativeInteger) * assume(y,'positiveInteger) == assume(x*y,'nonNegativeInteger)
  assume(x,'nonNegativeInteger) * assume(y,'nonZero) == assume(x*y, 'integer)
  assume(x,'positiveInteger) * assume(y,'positiveInteger) == assume(x*y,'positiveInteger)
  assume(x,'positiveInteger) * assume(y,'nonNegativeInteger) == assume(x*y,'nonNegativeInteger)
  assume(x,'positiveInteger) * assume(y,'nonZero) == assume(x*y,'nonZero)
  assume(x,'nonZero) * assume(y,'nonZero) == assume(x*y,'nonZero)
\end{axiom}

check if x is in t
\begin{axiom}

removed:
-

added:
tests

removed:
-domains

added:
dump type cache
\begin{axiom}
entries domains
--for i in members(domains)@List Record(key:Symbol,entry:BasicOperator) repeat output i
\end{axiom}

And "assume" system based on equational reasoning.

fricas

domains:=empty()$Table(Symbol,BasicOperator)

$\label{eq1} \mbox{\rm table} \left({}\right)$

(1)

Type: Table(Symbol,BasicOperator?)

fricas

assume(x:Expression Integer,t:Symbol):Expression Integer ==
  -- cache operators
  if not key?(t,domains) then domains.t := operator t
  (domains.t) x

   Function declaration assume : (Expression(Integer),Symbol) -> 
      Expression(Integer) has been added to workspace.

Type: Void

fricas

-- default assumptions about constants
markConstants(x:Expression Integer):Expression Integer ==
  if (s:=isPlus(x)) case List Expression Integer then
    return reduce(+,[markConstants i for i in s::List Expression Integer])
  if (s:=isTimes(x)) case List Expression Integer then
    return reduce(*,[markConstants i for i in s::List Expression Integer])
  if (r:=retractIfCan(x)@Union(Integer,"failed")) case Integer then
    if r<0 then return assume(x,'integer)
    if r>0 then return assume(x,'positiveInteger)
    return assume(x, 'nonNegativeInteger)
  return x

   Function declaration markConstants : Expression(Integer) -> 
      Expression(Integer) has been added to workspace.

Type: Void

Inference rules

fricas

prove := rule
  -- subtypes
  assume(assume(x,'integer),'integer) == assume(x,'integer)
  assume(assume(x,'integer),'nonNegativeInteger) == assume(x,'nonNegativeInteger)
  assume(assume(x,'integer),'positiveInteger) == assume(x,'positiveInteger)
  assume(assume(x,'integer),'nonZero) == assume(x,'nonZero)
  --
  assume(assume(x,'nonNegativeInteger),'integer) == assume(x,'nonNegativeInteger)
  assume(assume(x,'nonNegativeInteger),'nonNegativeInteger) == assume(x,'nonNegativeInteger)
  assume(assume(x,'nonNegativeInteger),'positiveInteger) == assume(x,'positiveInteger)
  assume(assume(x,'nonNegativeInteger),'nonZero) == assume(x,'positiveInteger)
  --
  assume(assume(x,'positiveInteger),'integer) == assume(x,'positiveInteger)
  assume(assume(x,'positiveInteger),'nonNegativeInteger) == assume(x,'positiveInteger)
  assume(assume(x,'positiveInteger),'positiveInteger) == assume(x,'positiveInteger)
  assume(assume(x,'positiveInteger),'nonZero) == assume(x,'positive)
  --
  assume(assume(x,'nonZero),'integer) == assume(x,'nonZero)
  assume(assume(x,'nonZero),'nonNegativeInteger) == assume(x,'positiveInteger)
  assume(assume(x,'nonZero),'positiveInteger) == assume(x,'positiveInteger)
  assume(assume(x,'nonZero),'nonZero) == assume(x,'nonZero)
  -- operations
  assume(x,'integer) + assume(y,'integer) == assume(x+y,'integer)
  assume(x,'integer) + assume(y,'nonNegativeInteger) == assume(x+y,'integer)
  assume(x,'integer) + assume(y,'positiveInteger) == assume(x+y,'integer)
  assume(x,'integer) + assume(y,'nonZero) == assume(x+y,'integer)
  assume(x,'nonNegativeInteger) + assume(y,'nonNegativeInteger) == assume(x+y,'nonNegativeInteger)
  assume(x,'nonNegativeInteger) + assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
  assume(x,'nonNegativeInteger) + assume(y,'nonZero) == assume(x+y, 'integer)
  assume(x,'positiveInteger) + assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
  assume(x,'positiveInteger) + assume(y,'nonNegativeInteger) == assume(x+y,'positiveInteger)
  assume(x,'positiveInteger) + assume(y,'nonZero) == assume(x+y,'integer)
  assume(x,'nonZero) + assume(y,'nonZero) == assume(x+y,'integer)
  --
  assume(x,'integer) * assume(y,'integer) == assume(x*y,'integer)
  assume(x,'integer) * assume(y,'nonNegativeInteger) == assume(x*y,'integer)
  assume(x,'integer) * assume(y,'positiveInteger) == assume(x*y,'integer)
  assume(x,'integer) * assume(y,'nonZero) == assume(x*y,'integer)
  assume(x,'nonNegativeInteger) * assume(y,'nonNegativeInteger) == assume(x*y,'nonNegativeInteger)
  assume(x,'nonNegativeInteger) * assume(y,'positiveInteger) == assume(x*y,'nonNegativeInteger)
  assume(x,'nonNegativeInteger) * assume(y,'nonZero) == assume(x*y, 'integer)
  assume(x,'positiveInteger) * assume(y,'positiveInteger) == assume(x*y,'positiveInteger)
  assume(x,'positiveInteger) * assume(y,'nonNegativeInteger) == assume(x*y,'nonNegativeInteger)
  assume(x,'positiveInteger) * assume(y,'nonZero) == assume(x*y,'nonZero)
  assume(x,'nonZero) * assume(y,'nonZero) == assume(x*y,'nonZero)

fricas

Compiling function assume with type (Expression(Integer),Symbol) -> 
      Expression(Integer)

$\label{eq2}\begin{array}{@{}l} \displaystyle \left\{{{integer \left({integer \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: integer}\right)}}, \: \right. \ \ \displaystyle \left.{{nonNegativeInteger \left({integer \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonNegativeInteger}\right)}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{positiveInteger \left({integer \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right. \ \ \displaystyle \left.\:{{nonZero \left({integer \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonZero}\right)}}, \: \right. \ \ \displaystyle \left.{{integer \left({nonNegativeInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonNegativeInteger}\right)}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{nonNegativeInteger \left({nonNegativeInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonNegativeInteger}\right)}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{positiveInteger \left({nonNegativeInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{nonZero \left({nonNegativeInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{integer \left({positiveInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{nonNegativeInteger \left({positiveInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{positiveInteger \left({positiveInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right. \ \ \displaystyle \left.\:{{nonZero \left({positiveInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positive}\right)}}, \: \right. \ \ \displaystyle \left.{{integer \left({nonZero \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonZero}\right)}}, \: \right. \ \ \displaystyle \left.{{nonNegativeInteger \left({nonZero \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{positiveInteger \left({nonZero \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right. \ \ \displaystyle \left.\:{{nonZero \left({nonZero \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonZero}\right)}}, \: \right. \ \ \displaystyle \left.{{{integer \left({y}\right)}+{integer \left({x}\right)}+ \%B}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%B}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{{nonNegativeInteger \left({y}\right)}+{integer \left({x}\right)}+ \%C}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%C}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{{positiveInteger \left({y}\right)}+{integer \left({x}\right)}+ \%D}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%D}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{{nonZero \left({y}\right)}+{integer \left({x}\right)}+ \%E}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%E}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{{nonNegativeInteger \left({y}\right)}+{nonNegativeInteger \left({x}\right)}+ \%F}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: nonNegativeInteger}\right)}+ \%F}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{{positiveInteger \left({y}\right)}+{nonNegativeInteger \left({x}\right)}+ \%G}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: positiveInteger}\right)}+ \%G}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{{nonZero \left({y}\right)}+{nonNegativeInteger \left({x}\right)}+ \%H}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%H}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{{positiveInteger \left({y}\right)}+{positiveInteger \left({x}\right)}+ \%I}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: positiveInteger}\right)}+ \%I}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{{positiveInteger \left({x}\right)}+{nonNegativeInteger \left({y}\right)}+ \%J}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: positiveInteger}\right)}+ \%J}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{{positiveInteger \left({x}\right)}+{nonZero \left({y}\right)}+ \%K}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%K}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{{nonZero \left({y}\right)}+{nonZero \left({x}\right)}+ \%L}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%L}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{\%M \ {integer \left({x}\right)}\ {integer \left({y}\right)}}\mbox{\rm = =}{\%M \ {{{\tt'}assume}\left({{x \ y}, \: integer}\right)}}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{\%N \ {integer \left({x}\right)}\ {nonNegativeInteger \left({y}\right)}}\mbox{\rm = =}{\%N \ {{{\tt'}assume}\left({{x \ y}, \: integer}\right)}}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{\%O \ {integer \left({x}\right)}\ {positiveInteger \left({y}\right)}}\mbox{\rm = =}{\%O \ {{{\tt'}assume}\left({{x \ y}, \: integer}\right)}}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{\%P \ {integer \left({x}\right)}\ {nonZero \left({y}\right)}}\mbox{\rm = =}{\%P \ {{{\tt'}assume}\left({{x \ y}, \: integer}\right)}}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{\%Q \ {nonNegativeInteger \left({x}\right)}\ {nonNegativeInteger \left({y}\right)}}\mbox{\rm = =}{\%Q \ {{{\tt'}assume}\left({{x \ y}, \: nonNegativeInteger}\right)}}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{\%R \ {nonNegativeInteger \left({x}\right)}\ {positiveInteger \left({y}\right)}}\mbox{\rm = =}{\%R \ {{{\tt'}assume}\left({{x \ y}, \: nonNegativeInteger}\right)}}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{\%S \ {nonNegativeInteger \left({x}\right)}\ {nonZero \left({y}\right)}}\mbox{\rm = =}{\%S \ {{{\tt'}assume}\left({{x \ y}, \: integer}\right)}}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{\%T \ {positiveInteger \left({x}\right)}\ {positiveInteger \left({y}\right)}}\mbox{\rm = =}{\%T \ {{{\tt'}assume}\left({{x \ y}, \: positiveInteger}\right)}}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{\%U \ {nonNegativeInteger \left({y}\right)}\ {positiveInteger \left({x}\right)}}\mbox{\rm = =}{\%U \ {{{\tt'}assume}\left({{x \ y}, \: nonNegativeInteger}\right)}}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{\%V \ {nonZero \left({y}\right)}\ {positiveInteger \left({x}\right)}}\mbox{\rm = =}{\%V \ {{{\tt'}assume}\left({{x \ y}, \: nonZero}\right)}}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{\%W \ {nonZero \left({x}\right)}\ {nonZero \left({y}\right)}}\mbox{\rm = =}{\%W \ {{{\tt'}assume}\left({{x \ y}, \: nonZero}\right)}}}\right\}$

(2)

Type: Ruleset(Integer,Integer,Expression(Integer))

check if x is in t

fricas

check(x:Expression Integer,t:Symbol):Boolean ==
  --k:=retractIfCan(prove markConstants x)@Union(Kernel Expression Integer,"failed")
  --if k case Kernel Expression Integer then is?(k,t) else false
  p := prove markConstants x
  e := equation(p, prove markConstants assume(p,t))
  output e
  e

   Function declaration check : (Expression(Integer),Symbol) -> Boolean
      has been added to workspace.

Type: Void

tests

fricas

assume(x,'positiveInteger)

$\label{eq3}positiveInteger \left({x}\right)$

(3)

Type: Expression(Integer)

fricas

prove %

$\label{eq4}positiveInteger \left({x}\right)$

(4)

Type: Expression(Integer)

fricas

assume(x,'positiveInteger)+1

$\label{eq5}{positiveInteger \left({x}\right)}+ 1$

(5)

Type: Expression(Integer)

fricas

prove markConstants %

fricas

Compiling function markConstants with type Expression(Integer) -> 
      Expression(Integer)

$\label{eq6}positiveInteger \left({x + 1}\right)$

(6)

Type: Expression(Integer)

fricas

assume(assume(x,'nonNegativeInteger),'positiveInteger)

$\label{eq7}positiveInteger \left({nonNegativeInteger \left({x}\right)}\right)$

(7)

Type: Expression(Integer)

fricas

prove %

$\label{eq8}positiveInteger \left({x}\right)$

(8)

Type: Expression(Integer)

fricas

check(assume(x,'positiveInteger),'positiveInteger)

fricas

Compiling function check with type (Expression(Integer),Symbol) -> 
      Boolean 
   positiveInteger(x) = positiveInteger(x)

$\label{eq9} \mbox{\rm true}$

(9)

Type: Boolean

fricas

check(assume(x,'positiveInteger)+1,'positiveInteger)

   positiveInteger(x + 1) = positiveInteger(x + 1)

$\label{eq10} \mbox{\rm true}$

(10)

Type: Boolean

fricas

check(3,'positiveInteger)

   positiveInteger(3) = positiveInteger(3)

$\label{eq11} \mbox{\rm true}$

(11)

Type: Boolean

fricas

check(-3,'positiveInteger)

   integer(- 3) = positiveInteger(- 3)

$\label{eq12} \mbox{\rm false}$

(12)

Type: Boolean

fricas

check(0,'positiveInteger)

   nonNegativeInteger(0) = positiveInteger(0)

$\label{eq13} \mbox{\rm false}$

(13)

Type: Boolean

fricas

--
assume(x,'nonNegativeInteger)

$\label{eq14}nonNegativeInteger \left({x}\right)$

(14)

Type: Expression(Integer)

fricas

prove %

$\label{eq15}nonNegativeInteger \left({x}\right)$

(15)

Type: Expression(Integer)

fricas

check(assume(x,'positiveInteger),'nonNegativeInteger)

   positiveInteger(x) = positiveInteger(x)

$\label{eq16} \mbox{\rm true}$

(16)

Type: Boolean

fricas

assume(x,'nonNegativeInteger)+1

$\label{eq17}{nonNegativeInteger \left({x}\right)}+ 1$

(17)

Type: Expression(Integer)

fricas

prove markConstants %

$\label{eq18}positiveInteger \left({x + 1}\right)$

(18)

Type: Expression(Integer)

fricas

assume(assume(x,'integer),'nonNegativeInteger)

$\label{eq19}nonNegativeInteger \left({integer \left({x}\right)}\right)$

(19)

Type: Expression(Integer)

fricas

prove %

$\label{eq20}nonNegativeInteger \left({x}\right)$

(20)

Type: Expression(Integer)

fricas

check(assume(x,'nonNegativeInteger),'nonNegativeInteger)

   nonNegativeInteger(x) = nonNegativeInteger(x)

$\label{eq21} \mbox{\rm true}$

(21)

Type: Boolean

fricas

check(assume(x,'nonNegativeInteger)+1,'nonNegativeInteger)

   positiveInteger(x + 1) = positiveInteger(x + 1)

$\label{eq22} \mbox{\rm true}$

(22)

Type: Boolean

fricas

check(3,'nonNegativeInteger)

   positiveInteger(3) = positiveInteger(3)

$\label{eq23} \mbox{\rm true}$

(23)

Type: Boolean

fricas

check(-3,'nonNegativeInteger)

   integer(- 3) = nonNegativeInteger(- 3)

$\label{eq24} \mbox{\rm false}$

(24)

Type: Boolean

fricas

check(0,'nonNegativeInteger)

   nonNegativeInteger(0) = nonNegativeInteger(0)

$\label{eq25} \mbox{\rm true}$

(25)

Type: Boolean

fricas

--
assume(x,'integer)

$\label{eq26}integer \left({x}\right)$

(26)

Type: Expression(Integer)

fricas

prove %

$\label{eq27}integer \left({x}\right)$

(27)

Type: Expression(Integer)

fricas

check(assume(x,'positiveInteger),'integer)

   positiveInteger(x) = positiveInteger(x)

$\label{eq28} \mbox{\rm true}$

(28)

Type: Boolean

fricas

assume(x,'integer)+1

$\label{eq29}{integer \left({x}\right)}+ 1$

(29)

Type: Expression(Integer)

fricas

prove markConstants %

$\label{eq30}integer \left({x + 1}\right)$

(30)

Type: Expression(Integer)

fricas

assume(assume(x,'integer),'integer)

$\label{eq31}integer \left({integer \left({x}\right)}\right)$

(31)

Type: Expression(Integer)

fricas

prove %

$\label{eq32}integer \left({x}\right)$

(32)

Type: Expression(Integer)

fricas

check(assume(x,'integer),'integer)

   integer(x) = integer(x)

$\label{eq33} \mbox{\rm true}$

(33)

Type: Boolean

fricas

check(assume(x,'integer)+1,'integer)

   integer(x + 1) = integer(x + 1)

$\label{eq34} \mbox{\rm true}$

(34)

Type: Boolean

fricas

check(3,'integer)

   positiveInteger(3) = positiveInteger(3)

$\label{eq35} \mbox{\rm true}$

(35)

Type: Boolean

fricas

check(-3,'integer)

   integer(- 3) = integer(- 3)

$\label{eq36} \mbox{\rm true}$

(36)

Type: Boolean

fricas

check(0,'integer)

   nonNegativeInteger(0) = nonNegativeInteger(0)

$\label{eq37} \mbox{\rm true}$

(37)

Type: Boolean

dump type cache

fricas

entries domains

$\label{eq38}\left[ nonZero , \: positiveInteger , \: nonNegativeInteger , \: integer \right]$

(38)

Type: List(BasicOperator?)