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) a(lambda(x),y) -> lambda(a(x,p(1,a(y,t))))
(2) a(p(x,y),z) -> p(a(x,z),a(y,z))
(3) a(a(x,y),z) -> a(x,a(y,z))
(4) lambda(x) -> x
(5) a(x,y) -> x
(6) a(x,y) -> y
(7) p(x,y) -> x
(8) p(x,y) -> y

[2]  Label this TRS using following interpretation over N\{0,1}:
[lambda(x)] = x + 1
[p(x,y)] = max(x, y)
rest default

  This interpretation is a quasi-model and yields following TRS:
(D1) lambda{i + 1}(x) ->= lambda{i}(x)
(D2) a{i + 1,j}(x,y) ->= a{i,j}(x,y)
(D3) a{i,j + 1}(x,y) ->= a{i,j}(x,y)
(D4) p{i + 1,j}(x,y) ->= p{i,j}(x,y)
(D5) p{i,j + 1}(x,y) ->= p{i,j}(x,y)
(4) lambda{i}(x) -> x
(5) a{i,j}(x,y) -> x
(6) a{i,j}(x,y) -> y
(7>) p{i,j}(x,y) -> x for j >= i
(8<) p{i,j}(x,y) -> y for i >= j
(1) a{i + 1,j}(lambda{i}(x),y) -> lambda{j + i - 2}(a{i,j}(x,p{2,j}(1,a{j,2}(y,t))))
(2<) a{i,k}(p{i,j}(x,y),z) -> p{k + i - 2,k + j - 2}(a{i,k}(x,z),a{j,k}(y,z)) for i >= j
(2>) a{j,k}(p{i,j}(x,y),z) -> p{k + i - 2,k + j - 2}(a{i,k}(x,z),a{j,k}(y,z)) for j >= i
(3) a{j + i - 2,k}(a{i,j}(x,y),z) -> a{i,k + j - 2}(x,a{j,k}(y,z))
(7<) p{i,j}(x,y) -> x for i >= j
(8>) p{i,j}(x,y) -> y for j >= i

[3]  All the rules of this TRS can be oriented with RPO with the following precedence:
Status: a: Lex-LR, 
Precedence:
a{i,j} > a{k,l} for i+j > k+l
a{i,j} > lambda{k} for all i, j, k
a{i,j} > p{k,l} for all i, j, k, l
a{i,j} > 1 for all i, j
a{i,j} > t for all i, j
lambda{i} > lambda{k} for i > k
p{i,j} > p{k,l} for i+j > k+l


subst.trs, 0.3, Y