YES
  TPA v.1.0

Result: TRS is terminating

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(1) active(f(X)) -> mark(if`1(X,if`2(c,f(true))))
(2) active(if`1(true,if`2(X,Y))) -> mark(X)
(3) active(if`1(false,if`2(X,Y))) -> mark(Y)
(4) active(f(X)) -> f(active(X))
(5) active(if`1(X1,if`2(X2,X3))) -> if`1(active(X1),if`2(X2,X3))
(6) active(if`1(X1,if`2(X2,X3))) -> if`1(X1,if`2(active(X2),X3))
(7) f(mark(X)) -> mark(f(X))
(8) if`1(mark(X1),if`2(X2,X3)) -> mark(if`1(X1,if`2(X2,X3)))
(9) if`1(X1,if`2(mark(X2),X3)) -> mark(if`1(X1,if`2(X2,X3)))
(10) proper(f(X)) -> f(proper(X))
(11) proper(if`1(X1,if`2(X2,X3))) -> if`1(proper(X1),if`2(proper(X2),proper(X3)))
(12) proper(c) -> ok(c)
(13) proper(true) -> ok(true)
(14) proper(false) -> ok(false)
(15) f(ok(X)) -> ok(f(X))
(16) if`1(ok(X1),if`2(ok(X2),ok(X3))) -> ok(if`1(X1,if`2(X2,X3)))
(17) top(mark(X)) -> top(proper(X))
(18) top(ok(X)) -> top(active(X))

[2]  Use following polynomial interpretation:
[false] = 3
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(3)

[3]  Label this TRS using following interpretation over N\{0,1}:
[f(x)] = x + 1
[mark(x)] = x + 1
[if`2(x,y)] = x
[true] = 3
[top(x)] = 2
rest default

  This interpretation is a model and yields following TRS:
(1) active{i + 1}(f{i}(X)) -> mark{i}(if`1{i,2}(X,if`2{2,4}(c,f{3}(true))))
(2) active{i + 1}(if`1{3,i}(true,if`2{i,j}(X,Y))) -> mark{i}(X)
(4) active{i + 1}(f{i}(X)) -> f{i}(active{i}(X))
(5) active{l0 + k - 2}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) -> if`1{k,l0}(active{k}(X1),if`2{l0,l1}(X2,X3))
(6) active{l0 + k - 2}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) -> if`1{k,l0}(X1,if`2{l0,l1}(active{l0}(X2),X3))
(7) f{i + 1}(mark{i}(X)) -> mark{i + 1}(f{i}(X))
(8) if`1{k + 1,l0}(mark{k}(X1),if`2{l0,l1}(X2,X3)) -> mark{l0 + k - 2}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3)))
(9) if`1{k,l0 + 1}(X1,if`2{l0 + 1,l1}(mark{l0}(X2),X3)) -> mark{l0 + k - 2}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3)))
(10) proper{i + 1}(f{i}(X)) -> f{i}(proper{i}(X))
(11) proper{l0 + k - 2}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) -> if`1{k,l0}(proper{k}(X1),if`2{l0,l1}(proper{l0}(X2),proper{l1}(X3)))
(12) proper{2}(c) -> ok{2}(c)
(13) proper{3}(true) -> ok{3}(true)
(14) proper{2}(false) -> ok{2}(false)
(15) f{i}(ok{i}(X)) -> ok{i + 1}(f{i}(X))
(16) if`1{k,l0}(ok{k}(X1),if`2{l0,l1}(ok{l0}(X2),ok{l1}(X3))) -> ok{l0 + k - 2}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3)))
(17) top{i + 1}(mark{i}(X)) -> top{i}(proper{i}(X))
(18) top{i}(ok{i}(X)) -> top{i}(active{i}(X))

[4]  Use following polynomial interpretation:
[active_{i}(x)] = x
[f_{i}(x)] = x
[mark_{i}(x)] = x
[if`1_{i,j}(x,y)] = x + y - 2
[if`2_{i,j}(x,y)] = x + y - 2
[proper_{i}(x)] = x
[ok_{i}(x)] = x
[top_{i}(x)] = x + i
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(17)

[5]  Unlabel this TRS to obtain the one consisting of the rules:
(1)-(2), (4)-(16), (18)

[6]  Label this TRS using following interpretation over N\{0,1}:
[if`1(x,y)] = max(x, y)
[if`2(x,y)] = x
[proper(x)] = x + 1
[ok(x)] = x + 1
[top(x)] = 2
rest default

  This interpretation is a model and yields following TRS:
(1) active{i}(f{i}(X)) -> mark{i}(if`1{i,2}(X,if`2{2,2}(c,f{2}(true))))
(2) active{i}(if`1{2,i}(true,if`2{i,j}(X,Y))) -> mark{i}(X)
(4) active{i}(f{i}(X)) -> f{i}(active{i}(X))
(5<) active{k}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) -> if`1{k,l0}(active{k}(X1),if`2{l0,l1}(X2,X3)) for k >= l0
(5>) active{l0}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) -> if`1{k,l0}(active{k}(X1),if`2{l0,l1}(X2,X3)) for l0 >= k
(6<) active{k}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) -> if`1{k,l0}(X1,if`2{l0,l1}(active{l0}(X2),X3)) for k >= l0
(6>) active{l0}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) -> if`1{k,l0}(X1,if`2{l0,l1}(active{l0}(X2),X3)) for l0 >= k
(7) f{i}(mark{i}(X)) -> mark{i}(f{i}(X))
(8<) if`1{k,l0}(mark{k}(X1),if`2{l0,l1}(X2,X3)) -> mark{k}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) for k >= l0
(8>) if`1{k,l0}(mark{k}(X1),if`2{l0,l1}(X2,X3)) -> mark{l0}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) for l0 >= k
(9<) if`1{k,l0}(X1,if`2{l0,l1}(mark{l0}(X2),X3)) -> mark{k}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) for k >= l0
(9>) if`1{k,l0}(X1,if`2{l0,l1}(mark{l0}(X2),X3)) -> mark{l0}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) for l0 >= k
(10) proper{i}(f{i}(X)) -> f{i + 1}(proper{i}(X))
(11<) proper{k}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) -> if`1{k + 1,l0 + 1}(proper{k}(X1),if`2{l0 + 1,l1 + 1}(proper{l0}(X2),proper{l1}(X3))) for k >= l0
(11>) proper{l0}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) -> if`1{k + 1,l0 + 1}(proper{k}(X1),if`2{l0 + 1,l1 + 1}(proper{l0}(X2),proper{l1}(X3))) for l0 >= k
(12) proper{2}(c) -> ok{2}(c)
(13) proper{2}(true) -> ok{2}(true)
(14) proper{2}(false) -> ok{2}(false)
(15) f{i + 1}(ok{i}(X)) -> ok{i}(f{i}(X))
(16<) if`1{k + 1,l0 + 1}(ok{k}(X1),if`2{l0 + 1,l1 + 1}(ok{l0}(X2),ok{l1}(X3))) -> ok{k}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) for k >= l0
(16>) if`1{k + 1,l0 + 1}(ok{k}(X1),if`2{l0 + 1,l1 + 1}(ok{l0}(X2),ok{l1}(X3))) -> ok{l0}(if`1{k,l0}(X1,if`2{l0,l1}(X2,X3))) for l0 >= k
(18) top{i + 1}(ok{i}(X)) -> top{i}(active{i}(X))

[7]  Use following polynomial interpretation:
[active_{i}(x)] = x
[f_{i}(x)] = x
[mark_{i}(x)] = x
[if`1_{i,j}(x,y)] = x + y - 2
[if`2_{i,j}(x,y)] = x + y - 2
[proper_{i}(x)] = x
[ok_{i}(x)] = x
[top_{i}(x)] = x + i
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(18)

[8]  Use following polynomial interpretation:
[active_{i}(x)] = x + i
[f_{i}(x)] = x
[mark_{i}(x)] = x
[if`1_{i,j}(x,y)] = x + y - 2
[if`2_{i,j}(x,y)] = x + y - 2
[proper_{i}(x)] = x
[ok_{i}(x)] = x
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(1)-(2)

[9]  All the rules of this TRS can be oriented with RPO with the following precedence:
Status: if`1: Lex-LR, 
Precedence:
active{i} = active{k} for all i, k
active{i} > f{k} for all i, k
active{i} > if`1{k,l} for all i, k, l
active{i} > if`2{k,l} for all i, k, l
f{i} = f{k} for all i, k
f{i} > mark{k} for all i, k
proper{i} > f{k} for all i, k
f{i} > ok{k} for all i, k
if`1{i,j} > mark{k} for all i, j, k
if`1{i,j} = if`1{k,l} for all i, j, k, l
if`1{i,j} > if`2{k,l} for all i, j, k, l
proper{i} > if`1{k,l} for all i, k, l
if`1{i,j} > ok{k} for all i, j, k
proper{i} > if`2{k,l} for all i, k, l
proper{i} = proper{k} for all i, k
proper{i} > ok{k} for all i, k


../tpdb/TRS/TRCSR/Ex5_Zan97_C.trs, 0.02, Y
Couldn't open file <60>: 60: No such file or directory