As carrier we take the set
{0,1}.
Symbols are labeled by the interpretation of their arguments using the interpretations
(modulo 2):
top#0(mark0(f000(x0,x1,x2))) |
→ |
top#0(f000(proper0(x0),proper0(x1),proper0(x2))) |
(30) |
top#0(ok0(f000(x0,x1,x2))) |
→ |
top#0(f000(x0,active0(x1),x2)) |
(31) |
top#0(ok0(f001(x0,x1,x2))) |
→ |
top#0(f001(x0,active0(x1),x2)) |
(32) |
top#0(ok1(f010(x0,x1,x2))) |
→ |
top#0(f000(x0,active1(x1),x2)) |
(33) |
top#0(ok1(f011(x0,x1,x2))) |
→ |
top#0(f001(x0,active1(x1),x2)) |
(34) |
top#0(ok0(f100(x0,x1,x2))) |
→ |
top#0(f100(x0,active0(x1),x2)) |
(35) |
top#0(ok0(f101(x0,x1,x2))) |
→ |
top#0(f101(x0,active0(x1),x2)) |
(36) |
top#0(ok1(f110(x0,x1,x2))) |
→ |
top#0(f100(x0,active1(x1),x2)) |
(37) |
top#0(ok1(f111(x0,x1,x2))) |
→ |
top#0(f101(x0,active1(x1),x2)) |
(38) |
top#0(mark0(f001(x0,x1,x2))) |
→ |
top#0(f000(proper0(x0),proper0(x1),proper1(x2))) |
(39) |
top#0(mark1(f010(x0,x1,x2))) |
→ |
top#0(f000(proper0(x0),proper1(x1),proper0(x2))) |
(40) |
top#0(mark1(f011(x0,x1,x2))) |
→ |
top#0(f000(proper0(x0),proper1(x1),proper1(x2))) |
(41) |
top#0(mark0(f100(x0,x1,x2))) |
→ |
top#0(f000(proper1(x0),proper0(x1),proper0(x2))) |
(42) |
top#0(mark0(f101(x0,x1,x2))) |
→ |
top#0(f000(proper1(x0),proper0(x1),proper1(x2))) |
(43) |
top#0(mark1(f110(x0,x1,x2))) |
→ |
top#0(f000(proper1(x0),proper1(x1),proper0(x2))) |
(44) |
top#0(mark1(f111(x0,x1,x2))) |
→ |
top#0(f000(proper1(x0),proper1(x1),proper1(x2))) |
(45) |
and the set of labeled rules:
proper0(f000(X1,X2,X3)) |
→ |
f000(proper0(X1),proper0(X2),proper0(X3)) |
(46) |
proper0(f001(X1,X2,X3)) |
→ |
f000(proper0(X1),proper0(X2),proper1(X3)) |
(47) |
proper1(f010(X1,X2,X3)) |
→ |
f000(proper0(X1),proper1(X2),proper0(X3)) |
(48) |
proper1(f011(X1,X2,X3)) |
→ |
f000(proper0(X1),proper1(X2),proper1(X3)) |
(49) |
proper0(f100(X1,X2,X3)) |
→ |
f000(proper1(X1),proper0(X2),proper0(X3)) |
(50) |
proper0(f101(X1,X2,X3)) |
→ |
f000(proper1(X1),proper0(X2),proper1(X3)) |
(51) |
proper1(f110(X1,X2,X3)) |
→ |
f000(proper1(X1),proper1(X2),proper0(X3)) |
(52) |
proper1(f111(X1,X2,X3)) |
→ |
f000(proper1(X1),proper1(X2),proper1(X3)) |
(53) |
proper1(b) |
→ |
ok1(b) |
(54) |
proper0(c) |
→ |
ok0(c) |
(55) |
f000(X1,mark0(X2),X3) |
→ |
mark0(f000(X1,X2,X3)) |
(56) |
f001(X1,mark0(X2),X3) |
→ |
mark0(f001(X1,X2,X3)) |
(57) |
f000(X1,mark1(X2),X3) |
→ |
mark1(f010(X1,X2,X3)) |
(58) |
f001(X1,mark1(X2),X3) |
→ |
mark1(f011(X1,X2,X3)) |
(59) |
f100(X1,mark0(X2),X3) |
→ |
mark0(f100(X1,X2,X3)) |
(60) |
f101(X1,mark0(X2),X3) |
→ |
mark0(f101(X1,X2,X3)) |
(61) |
f100(X1,mark1(X2),X3) |
→ |
mark1(f110(X1,X2,X3)) |
(62) |
f101(X1,mark1(X2),X3) |
→ |
mark1(f111(X1,X2,X3)) |
(63) |
f000(ok0(X1),ok0(X2),ok0(X3)) |
→ |
ok0(f000(X1,X2,X3)) |
(64) |
f000(ok0(X1),ok0(X2),ok1(X3)) |
→ |
ok0(f001(X1,X2,X3)) |
(65) |
f000(ok0(X1),ok1(X2),ok0(X3)) |
→ |
ok1(f010(X1,X2,X3)) |
(66) |
f000(ok0(X1),ok1(X2),ok1(X3)) |
→ |
ok1(f011(X1,X2,X3)) |
(67) |
f000(ok1(X1),ok0(X2),ok0(X3)) |
→ |
ok0(f100(X1,X2,X3)) |
(68) |
f000(ok1(X1),ok0(X2),ok1(X3)) |
→ |
ok0(f101(X1,X2,X3)) |
(69) |
f000(ok1(X1),ok1(X2),ok0(X3)) |
→ |
ok1(f110(X1,X2,X3)) |
(70) |
f000(ok1(X1),ok1(X2),ok1(X3)) |
→ |
ok1(f111(X1,X2,X3)) |
(71) |
active0(f100(b,X,c)) |
→ |
mark0(f000(X,c,X)) |
(72) |
active1(f110(b,X,c)) |
→ |
mark0(f101(X,c,X)) |
(73) |
active0(c) |
→ |
mark1(b) |
(74) |
active0(f000(X1,X2,X3)) |
→ |
f000(X1,active0(X2),X3) |
(75) |
active0(f001(X1,X2,X3)) |
→ |
f001(X1,active0(X2),X3) |
(76) |
active1(f010(X1,X2,X3)) |
→ |
f000(X1,active1(X2),X3) |
(77) |
active1(f011(X1,X2,X3)) |
→ |
f001(X1,active1(X2),X3) |
(78) |
active0(f100(X1,X2,X3)) |
→ |
f100(X1,active0(X2),X3) |
(79) |
active0(f101(X1,X2,X3)) |
→ |
f101(X1,active0(X2),X3) |
(80) |
active1(f110(X1,X2,X3)) |
→ |
f100(X1,active1(X2),X3) |
(81) |
active1(f111(X1,X2,X3)) |
→ |
f101(X1,active1(X2),X3) |
(82) |
Innermost rewriting w.r.t. the following left-hand sides is considered:
active0(c) |
active0(f000(x0,x1,x2)) |
active0(f001(x0,x1,x2)) |
active1(f010(x0,x1,x2)) |
active1(f011(x0,x1,x2)) |
active0(f100(x0,x1,x2)) |
active0(f101(x0,x1,x2)) |
active1(f110(x0,x1,x2)) |
active1(f111(x0,x1,x2)) |
f000(x0,mark0(x1),x2) |
f001(x0,mark0(x1),x2) |
f000(x0,mark1(x1),x2) |
f001(x0,mark1(x1),x2) |
f100(x0,mark0(x1),x2) |
f101(x0,mark0(x1),x2) |
f100(x0,mark1(x1),x2) |
f101(x0,mark1(x1),x2) |
proper0(f000(x0,x1,x2)) |
proper0(f001(x0,x1,x2)) |
proper1(f010(x0,x1,x2)) |
proper1(f011(x0,x1,x2)) |
proper0(f100(x0,x1,x2)) |
proper0(f101(x0,x1,x2)) |
proper1(f110(x0,x1,x2)) |
proper1(f111(x0,x1,x2)) |
proper1(b) |
proper0(c) |
f000(ok0(x0),ok0(x1),ok0(x2)) |
f000(ok0(x0),ok0(x1),ok1(x2)) |
f000(ok0(x0),ok1(x1),ok0(x2)) |
f000(ok0(x0),ok1(x1),ok1(x2)) |
f000(ok1(x0),ok0(x1),ok0(x2)) |
f000(ok1(x0),ok0(x1),ok1(x2)) |
f000(ok1(x0),ok1(x1),ok0(x2)) |
f000(ok1(x0),ok1(x1),ok1(x2)) |
top#0(mark1(f010(x0,x1,x2))) |
→ |
top#0(f000(proper0(x0),proper1(x1),proper0(x2))) |
(40) |
top#0(mark1(f011(x0,x1,x2))) |
→ |
top#0(f000(proper0(x0),proper1(x1),proper1(x2))) |
(41) |
top#0(mark1(f110(x0,x1,x2))) |
→ |
top#0(f000(proper1(x0),proper1(x1),proper0(x2))) |
(44) |
top#0(mark1(f111(x0,x1,x2))) |
→ |
top#0(f000(proper1(x0),proper1(x1),proper1(x2))) |
(45) |
could be deleted.
top#0(mark0(f000(x0,x1,x2))) |
→ |
top#0(f000(proper0(x0),proper0(x1),proper0(x2))) |
(30) |
top#0(mark0(f001(x0,x1,x2))) |
→ |
top#0(f000(proper0(x0),proper0(x1),proper1(x2))) |
(39) |
top#0(mark0(f100(x0,x1,x2))) |
→ |
top#0(f000(proper1(x0),proper0(x1),proper0(x2))) |
(42) |
top#0(mark0(f101(x0,x1,x2))) |
→ |
top#0(f000(proper1(x0),proper0(x1),proper1(x2))) |
(43) |
could be deleted.
f000(X1,mark0(X2),X3) |
→ |
mark0(f000(X1,X2,X3)) |
(56) |
f000(X1,mark1(X2),X3) |
→ |
mark1(f010(X1,X2,X3)) |
(58) |
f000(ok0(X1),ok0(X2),ok0(X3)) |
→ |
ok0(f000(X1,X2,X3)) |
(64) |
f000(ok0(X1),ok0(X2),ok1(X3)) |
→ |
ok0(f001(X1,X2,X3)) |
(65) |
f000(ok0(X1),ok1(X2),ok0(X3)) |
→ |
ok1(f010(X1,X2,X3)) |
(66) |
f000(ok0(X1),ok1(X2),ok1(X3)) |
→ |
ok1(f011(X1,X2,X3)) |
(67) |
f000(ok1(X1),ok0(X2),ok0(X3)) |
→ |
ok0(f100(X1,X2,X3)) |
(68) |
f000(ok1(X1),ok0(X2),ok1(X3)) |
→ |
ok0(f101(X1,X2,X3)) |
(69) |
f000(ok1(X1),ok1(X2),ok0(X3)) |
→ |
ok1(f110(X1,X2,X3)) |
(70) |
f000(ok1(X1),ok1(X2),ok1(X3)) |
→ |
ok1(f111(X1,X2,X3)) |
(71) |
f001(X1,mark0(X2),X3) |
→ |
mark0(f001(X1,X2,X3)) |
(57) |
f001(X1,mark1(X2),X3) |
→ |
mark1(f011(X1,X2,X3)) |
(59) |
f100(X1,mark0(X2),X3) |
→ |
mark0(f100(X1,X2,X3)) |
(60) |
f100(X1,mark1(X2),X3) |
→ |
mark1(f110(X1,X2,X3)) |
(62) |
f101(X1,mark0(X2),X3) |
→ |
mark0(f101(X1,X2,X3)) |
(61) |
f101(X1,mark1(X2),X3) |
→ |
mark1(f111(X1,X2,X3)) |
(63) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairs
top#0(ok0(f001(x0,x1,x2))) |
→ |
top#0(f001(x0,active0(x1),x2)) |
(32) |
top#0(ok1(f011(x0,x1,x2))) |
→ |
top#0(f001(x0,active1(x1),x2)) |
(34) |
top#0(ok0(f100(x0,x1,x2))) |
→ |
top#0(f100(x0,active0(x1),x2)) |
(35) |
top#0(ok0(f101(x0,x1,x2))) |
→ |
top#0(f101(x0,active0(x1),x2)) |
(36) |
top#0(ok1(f110(x0,x1,x2))) |
→ |
top#0(f100(x0,active1(x1),x2)) |
(37) |
top#0(ok1(f111(x0,x1,x2))) |
→ |
top#0(f101(x0,active1(x1),x2)) |
(38) |
could be deleted.
f000(X1,mark0(X2),X3) |
→ |
mark0(f000(X1,X2,X3)) |
(56) |
f000(X1,mark1(X2),X3) |
→ |
mark1(f010(X1,X2,X3)) |
(58) |
f000(ok0(X1),ok0(X2),ok0(X3)) |
→ |
ok0(f000(X1,X2,X3)) |
(64) |
f000(ok0(X1),ok0(X2),ok1(X3)) |
→ |
ok0(f001(X1,X2,X3)) |
(65) |
f000(ok0(X1),ok1(X2),ok0(X3)) |
→ |
ok1(f010(X1,X2,X3)) |
(66) |
f000(ok0(X1),ok1(X2),ok1(X3)) |
→ |
ok1(f011(X1,X2,X3)) |
(67) |
f000(ok1(X1),ok0(X2),ok0(X3)) |
→ |
ok0(f100(X1,X2,X3)) |
(68) |
f000(ok1(X1),ok0(X2),ok1(X3)) |
→ |
ok0(f101(X1,X2,X3)) |
(69) |
f000(ok1(X1),ok1(X2),ok0(X3)) |
→ |
ok1(f110(X1,X2,X3)) |
(70) |
f000(ok1(X1),ok1(X2),ok1(X3)) |
→ |
ok1(f111(X1,X2,X3)) |
(71) |
f001(X1,mark0(X2),X3) |
→ |
mark0(f001(X1,X2,X3)) |
(57) |
f001(X1,mark1(X2),X3) |
→ |
mark1(f011(X1,X2,X3)) |
(59) |
f100(X1,mark0(X2),X3) |
→ |
mark0(f100(X1,X2,X3)) |
(60) |
f100(X1,mark1(X2),X3) |
→ |
mark1(f110(X1,X2,X3)) |
(62) |
f101(X1,mark0(X2),X3) |
→ |
mark0(f101(X1,X2,X3)) |
(61) |
f101(X1,mark1(X2),X3) |
→ |
mark1(f111(X1,X2,X3)) |
(63) |
(w.r.t. the implicit argument filter of the reduction pair),
the
pairsThere are no pairs anymore.