Processing math: 100%

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)xyxx1xx1

Terms of depth 2

f(g(x))f(f(x))f(xy)f(xx)f(1x)f(x1)f(x)yf(x)x f(x)1xf(y)xf(x)1f(x)f(x)g(y)f(x)g(x)f(x)f(y)f(x)f(x) 16 terms

x(y+z)x(x+y)x(y+x)y(x+x)x(x+x)x(y+1)x(1+y)1(x+y)x(x+1)x(1+x) 1(x+x)0(x+1)0(1+x)1(x+1)1(1+x) 15 terms

(xy)+z(xx)+y(xy)+x(yx)+x(xx)+x(xy)+1(x1)+y(1x)+y(xx)+1(x1)+x (1x)+x(x0)+1(0x)+1(x1)+1(1x)+1 15 terms

x(yz)x(xy)x(yx)y(xx)x(xx)x(y1)x(1y)1(xy)x(x1)x(1x) 1(xx)0(x1)0(1x)1(x1)1(1x) 15 terms

(xy)z(xx)y(xy)x(yx)x(xx)x(xy)1(x1)y(1x)y(xx)1(x1)x (1x)x(x0)1(0x)1(x1)1(1x)1 15 terms

f(x)(y+z)f(x)(x+y)f(x)(y+x)f(y)(x+x)f(x)(x+x)f(x)(y+1)f(x)(1+y)f(x)(x+1)f(x)(1+x) 9 terms

(xy)+f(z)(xx)+f(y)(xy)+f(x)(yx)+f(x)(xx)+f(x)(x1)+f(y)(1x)+f(y)(x1)+f(x)(1x)+f(x) 9 terms

f(x)(yz)f(x)(xy)f(x)(yx)f(y)(xx)f(x)(xx)f(x)(y1)f(x)(1y)f(x)(x1)f(x)(1x) 9 terms

(xy)f(z)(xx)f(y)(xy)f(x)(yx)f(x)(xx)f(x)(x1)f(y)(1x)f(y)(x1)f(x)(1x)f(x) 9 terms

(xy)+(zw) 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)f(xf(y))f(f(x)f(y))

f(f(x)x)f(xf(x))f(f(x)f(x))

(xf(x))xx(f(x)x)

((xy)x)f((xy)x)(x(yx))f(x(yx))

(xf(x))(yf(y))


QR Code
QR Code terms (generated for current page)