YES
We show the termination of the TRS R:
active(f(x)) -> mark(f(f(x)))
chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
mat(f(x),f(y())) -> f(mat(x,y()))
chk(no(c())) -> active(c())
mat(f(x),c()) -> no(c())
f(active(x)) -> active(f(x))
f(no(x)) -> no(f(x))
f(mark(x)) -> mark(f(x))
tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
-- SCC decomposition.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(f(x)) -> f#(f(x))
p2: chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
p3: chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))
p4: chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)
p5: chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X()))))))))))
p6: chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X())))))))))
p7: chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X()))))))))
p8: chk#(no(f(x))) -> f#(f(f(f(f(f(f(X())))))))
p9: chk#(no(f(x))) -> f#(f(f(f(f(f(X()))))))
p10: chk#(no(f(x))) -> f#(f(f(f(f(X())))))
p11: chk#(no(f(x))) -> f#(f(f(f(X()))))
p12: chk#(no(f(x))) -> f#(f(f(X())))
p13: chk#(no(f(x))) -> f#(f(X()))
p14: chk#(no(f(x))) -> f#(X())
p15: mat#(f(x),f(y())) -> f#(mat(x,y()))
p16: mat#(f(x),f(y())) -> mat#(x,y())
p17: chk#(no(c())) -> active#(c())
p18: f#(active(x)) -> active#(f(x))
p19: f#(active(x)) -> f#(x)
p20: f#(no(x)) -> f#(x)
p21: f#(mark(x)) -> f#(x)
p22: tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
p23: tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))
p24: tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)
p25: tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X()))))))))))
p26: tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X())))))))))
p27: tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X()))))))))
p28: tp#(mark(x)) -> f#(f(f(f(f(f(f(X())))))))
p29: tp#(mark(x)) -> f#(f(f(f(f(f(X()))))))
p30: tp#(mark(x)) -> f#(f(f(f(f(X())))))
p31: tp#(mark(x)) -> f#(f(f(f(X()))))
p32: tp#(mark(x)) -> f#(f(f(X())))
p33: tp#(mark(x)) -> f#(f(X()))
p34: tp#(mark(x)) -> f#(X())
and R consists of:
r1: active(f(x)) -> mark(f(f(x)))
r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
r3: mat(f(x),f(y())) -> f(mat(x,y()))
r4: chk(no(c())) -> active(c())
r5: mat(f(x),c()) -> no(c())
r6: f(active(x)) -> active(f(x))
r7: f(no(x)) -> no(f(x))
r8: f(mark(x)) -> mark(f(x))
r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
The estimated dependency graph contains the following SCCs:
{p22}
{p3}
{p1, p18, p19, p20, p21}
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
and R consists of:
r1: active(f(x)) -> mark(f(f(x)))
r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
r3: mat(f(x),f(y())) -> f(mat(x,y()))
r4: chk(no(c())) -> active(c())
r5: mat(f(x),c()) -> no(c())
r6: f(active(x)) -> active(f(x))
r7: f(no(x)) -> no(f(x))
r8: f(mark(x)) -> mark(f(x))
r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
The set of usable rules consists of
r1, r2, r3, r4, r5, r6, r7, r8
Take the reduction pair:
lexicographic combination of reduction pairs:
1. matrix interpretations:
carrier: N^2
order: standard order
interpretations:
tp#_A(x1) = ((1,1),(0,0)) x1
mark_A(x1) = ((0,1),(0,1)) x1 + (73,0)
chk_A(x1) = ((1,1),(1,1)) x1 + (22,0)
mat_A(x1,x2) = ((0,1),(0,1)) x1 + ((0,1),(0,0)) x2 + (0,3)
f_A(x1) = ((0,1),(0,1)) x1 + (75,1)
X_A() = (1,1)
active_A(x1) = x1 + (1,1)
no_A(x1) = x1 + (1,2)
y_A() = (1,77)
c_A() = (1,2)
2. matrix interpretations:
carrier: N^2
order: standard order
interpretations:
tp#_A(x1) = x1
mark_A(x1) = (4,3)
chk_A(x1) = (3,1)
mat_A(x1,x2) = (3,1)
f_A(x1) = (2,2)
X_A() = (1,1)
active_A(x1) = (1,2)
no_A(x1) = (4,3)
y_A() = (1,1)
c_A() = (1,1)
The next rules are strictly ordered:
p1
We remove them from the problem. Then no dependency pair remains.
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))
and R consists of:
r1: active(f(x)) -> mark(f(f(x)))
r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
r3: mat(f(x),f(y())) -> f(mat(x,y()))
r4: chk(no(c())) -> active(c())
r5: mat(f(x),c()) -> no(c())
r6: f(active(x)) -> active(f(x))
r7: f(no(x)) -> no(f(x))
r8: f(mark(x)) -> mark(f(x))
r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
The set of usable rules consists of
r3, r5
Take the reduction pair:
lexicographic combination of reduction pairs:
1. matrix interpretations:
carrier: N^2
order: standard order
interpretations:
chk#_A(x1) = x1
no_A(x1) = ((0,1),(0,0)) x1 + (3,1)
f_A(x1) = ((0,1),(0,0)) x1 + (1,3)
mat_A(x1,x2) = ((0,1),(0,0)) x1 + (2,3)
X_A() = (1,1)
y_A() = (1,1)
c_A() = (1,1)
2. matrix interpretations:
carrier: N^2
order: standard order
interpretations:
chk#_A(x1) = (0,0)
no_A(x1) = (2,2)
f_A(x1) = (2,0)
mat_A(x1,x2) = (1,1)
X_A() = (1,1)
y_A() = (1,1)
c_A() = (1,1)
The next rules are strictly ordered:
p1
We remove them from the problem. Then no dependency pair remains.
-- Reduction pair.
Consider the dependency pair problem (P, R), where P consists of
p1: active#(f(x)) -> f#(f(x))
p2: f#(mark(x)) -> f#(x)
p3: f#(no(x)) -> f#(x)
p4: f#(active(x)) -> f#(x)
p5: f#(active(x)) -> active#(f(x))
and R consists of:
r1: active(f(x)) -> mark(f(f(x)))
r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
r3: mat(f(x),f(y())) -> f(mat(x,y()))
r4: chk(no(c())) -> active(c())
r5: mat(f(x),c()) -> no(c())
r6: f(active(x)) -> active(f(x))
r7: f(no(x)) -> no(f(x))
r8: f(mark(x)) -> mark(f(x))
r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)))
The set of usable rules consists of
r1, r6, r7, r8
Take the reduction pair:
lexicographic combination of reduction pairs:
1. matrix interpretations:
carrier: N^2
order: standard order
interpretations:
active#_A(x1) = ((1,0),(1,0)) x1 + (1,2)
f_A(x1) = ((1,1),(1,0)) x1 + (1,1)
f#_A(x1) = ((1,0),(1,0)) x1
mark_A(x1) = x1 + (1,1)
no_A(x1) = ((1,1),(1,0)) x1 + (2,2)
active_A(x1) = ((1,1),(1,0)) x1 + (3,2)
2. matrix interpretations:
carrier: N^2
order: standard order
interpretations:
active#_A(x1) = (2,1)
f_A(x1) = (1,1)
f#_A(x1) = ((1,0),(1,0)) x1
mark_A(x1) = x1 + (5,3)
no_A(x1) = x1 + (1,2)
active_A(x1) = ((1,1),(1,0)) x1 + (3,1)
The next rules are strictly ordered:
p1, p2, p3, p4, p5
We remove them from the problem. Then no dependency pair remains.