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)x∗yx∗x1∗xx∗1
Terms of depth 2
f(g(x))f(f(x))f(x∗y)f(x∗x)f(1∗x)f(x∗1)f(x)∗yf(x)∗x f(x)∗1x∗f(y)x∗f(x)1∗f(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
(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(x∗0)+1(0∗x)+1(x∗1)+1(1∗x)+1 15 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
(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(x∗0)∗1(0∗x)∗1(x∗1)∗1(1∗x)∗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
(x∗y)+f(z)(x∗x)+f(y)(x∗y)+f(x)(y∗x)+f(x)(x∗x)+f(x)(x∗1)+f(y)(1∗x)+f(y)(x∗1)+f(x)(1∗x)+f(x) 9 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
(x∗y)∗f(z)(x∗x)∗f(y)(x∗y)∗f(x)(y∗x)∗f(x)(x∗x)∗f(x)(x∗1)∗f(y)(1∗x)∗f(y)(x∗1)∗f(x)(1∗x)∗f(x) 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)f(x∗f(y))f(f(x)∗f(y))
f(f(x)∗x)f(x∗f(x))f(f(x)∗f(x))
(x∗f(x))∗xx∗(f(x)∗x)
((x∗y)∗x)∗f((x∗y)∗x)(x∗(y∗x))∗f(x∗(y∗x))
(x∗f(x))∗(y∗f(y))