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) min(x,0) -> 0
(2) min(0,y) -> 0
(3) min(s(x),s(y)) -> s(min(x,y))
(4) max(x,0) -> x
(5) max(0,y) -> y
(6) max(s(x),s(y)) -> s(max(x,y))
(7) -(x,0) -> x
(8) -(s(x),s(y)) -> -(x,y)
(9) gcd(s(x),s(y)) -> gcd(-(s(max(x,y)),s(min(x,y))),s(min(x,y)))

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

  This interpretation is a model and yields following TRS:
(1) min{i,2}(x,0) -> 0
(2) min{2,j}(0,y) -> 0
(3<) min{i + 1,j + 1}(s{i}(x),s{j}(y)) -> s{j}(min{i,j}(x,y)) for i >= j
(3>) min{i + 1,j + 1}(s{i}(x),s{j}(y)) -> s{i}(min{i,j}(x,y)) for j >= i
(4) max{i,2}(x,0) -> x
(5) max{2,j}(0,y) -> y
(6<) max{i + 1,j + 1}(s{i}(x),s{j}(y)) -> s{i}(max{i,j}(x,y)) for i >= j
(6>) max{i + 1,j + 1}(s{i}(x),s{j}(y)) -> s{j}(max{i,j}(x,y)) for j >= i
(7) -{i,2}(x,0) -> x
(8<) -{i + 1,j + 1}(s{i}(x),s{j}(y)) -> -{i,j}(x,y) for i >= j
(8>) -{i + 1,j + 1}(s{i}(x),s{j}(y)) -> -{i,j}(x,y) for j >= i
(9<) gcd{i + 1,j + 1}(s{i}(x),s{j}(y)) -> gcd{-j + i + 2,j + 1}(-{i + 1,j + 1}(s{i}(max{i,j}(x,y)),s{j}(min{i,j}(x,y))),s{j}(min{i,j}(x,y))) for i >= j
(9>) gcd{i + 1,j + 1}(s{i}(x),s{j}(y)) -> gcd{-i + j + 2,i + 1}(-{j + 1,i + 1}(s{j}(max{i,j}(x,y)),s{i}(min{i,j}(x,y))),s{i}(min{i,j}(x,y))) for j >= i

[3]  All the rules of this TRS can be oriented with RPO with the following precedence:
Status: min: Lex-LR, max: Lex-LR, -: Lex-LR, 
Precedence:
min{i,j} = min{k,l} for all i, j, k, l
min{i,j} > s{k} for all i, j, k
gcd{i,j} > min{k,l} for all i, j, k, l
max{i,j} > s{k} for all i, j, k
gcd{i,j} > s{k} for all i, j, k
max{i,j} = max{k,l} for all i, j, k, l
gcd{i,j} > max{k,l} for all i, j, k, l
-{i,j} = -{k,l} for all i, j, k, l
gcd{i,j} > -{k,l} for all i, j, k, l
gcd{i,j} > gcd{k,l} for i+j > k+l


gcd.trs, 1.59, Y