Syntax | Terms | Equations | Horn formulas | Universal formulas | First-order formulas | Theories
Here we list distinct terms with no constant subterms other than $0, 1$.
Any variables, constant symbols or operation symbols can be substituted instead of $x$ $y$ $z$ $w$ $1$ $f$ $g$ $*$ $+$ $-$ respectively.
Terms of depth 0
$x$
Terms of depth 1
$f(x) \qquad x*y \qquad x*x \qquad 1*x \qquad x*1$
Terms of depth 2
$f(g(x)) \qquad f(f(x)) \qquad f(x*y) \qquad f(x*x) \qquad f(1*x) \qquad f(x*1) \qquad f(x)*y \qquad f(x)*x \qquad$ $f(x)*1 \qquad x*f(y) \qquad x*f(x) \qquad 1*f(x) \qquad f(x)*g(y) \qquad f(x)*g(x) \qquad f(x)*f(y) \qquad f(x)*f(x) \qquad$ 16 terms
$x*(y+z) \qquad x*(x+y) \qquad x*(y+x) \qquad y*(x+x) \qquad x*(x+x) \qquad x*(y+1) \qquad x*(1+y) \qquad 1*(x+y) \qquad x*(x+1) \qquad x*(1+x) \qquad$ $1*(x+x) \qquad 0*(x+1) \qquad 0*(1+x) \qquad 1*(x+1) \qquad 1*(1+x) \qquad$ 15 terms
$(x*y)+z \qquad (x*x)+y \qquad (x*y)+x \qquad (y*x)+x \qquad (x*x)+x \qquad (x*y)+1 \qquad (x*1)+y \qquad (1*x)+y \qquad (x*x)+1 \qquad (x*1)+x \qquad$ $(1*x)+x \qquad (x*0)+1 \qquad (0*x)+1 \qquad (x*1)+1 \qquad (1*x)+1 \qquad$ 15 terms
$x*(y*z) \qquad x*(x*y) \qquad x*(y*x) \qquad y*(x*x) \qquad x*(x*x) \qquad x*(y*1) \qquad x*(1*y) \qquad 1*(x*y) \qquad x*(x*1) \qquad x*(1*x) \qquad$ $1*(x*x) \qquad 0*(x*1) \qquad 0*(1*x) \qquad 1*(x*1) \qquad 1*(1*x) \qquad$ 15 terms
$(x*y)*z \qquad (x*x)*y \qquad (x*y)*x \qquad (y*x)*x \qquad (x*x)*x \qquad (x*y)*1 \qquad (x*1)*y \qquad (1*x)*y \qquad (x*x)*1 \qquad (x*1)*x \qquad$ $(1*x)*x \qquad (x*0)*1 \qquad (0*x)*1 \qquad (x*1)*1 \qquad (1*x)*1 \qquad$ 15 terms
$f(x)*(y+z) \qquad f(x)*(x+y) \qquad f(x)*(y+x) \qquad f(y)*(x+x) \qquad f(x)*(x+x) \qquad f(x)*(y+1) \qquad f(x)*(1+y) \qquad f(x)*(x+1) \qquad f(x)*(1+x) \qquad$ 9 terms
$(x*y)+f(z) \qquad (x*x)+f(y) \qquad (x*y)+f(x) \qquad (y*x)+f(x) \qquad (x*x)+f(x) \qquad (x*1)+f(y) \qquad (1*x)+f(y) \qquad (x*1)+f(x) \qquad (1*x)+f(x) \qquad$ 9 terms
$f(x)*(y*z) \qquad f(x)*(x*y) \qquad f(x)*(y*x) \qquad f(y)*(x*x) \qquad f(x)*(x*x) \qquad f(x)*(y*1) \qquad f(x)*(1*y) \qquad f(x)*(x*1) \qquad f(x)*(1*x) \qquad$ 9 terms
$(x*y)*f(z) \qquad (x*x)*f(y) \qquad (x*y)*f(x) \qquad (y*x)*f(x) \qquad (x*x)*f(x) \qquad (x*1)*f(y) \qquad (1*x)*f(y) \qquad (x*1)*f(x) \qquad (1*x)*f(x) \qquad$ 9 terms
$(x*y)+(z-w)$ and all substitution instances with $x$ $y$ $z$ $1$ $*$ $+$
Terms of depth 3
Only terms of the form that actually occur in practice are listed below.
$f(f(x)*y) \qquad f(x*f(y)) \qquad f(f(x)*f(y))$
$f(f(x)*x) \qquad f(x*f(x)) \qquad f(f(x)*f(x))$
$(x*f(x))*x \qquad x*(f(x)*x)$
$((x*y)*x)*f((x*y)*x) \qquad (x*(y*x))*f(x*(y*x))$
$(x*f(x))*(y*f(y))$
