MAYBE
R
↳Dependency Pair Analysis
U11'(tt, M', N') -> U12'(equal(> (N', M'), true), M', N')
U11'(tt, M', N') -> EQUAL(> (N', M'), true)
U11'(tt, M', N') -> >'(N', M')
U12'(tt, M', N') -> gcd(d(N', M'), M')
U12'(tt, M', N') -> d(N', M')
U21'(tt, M', N) -> U22'(equal(> (M', N), true))
U21'(tt, M', N) -> EQUAL(> (M', N), true)
U21'(tt, M', N) -> >'(M', N)
U31'(tt, M', N) -> U32'(equal(> (N, M'), true), M', N)
U31'(tt, M', N) -> EQUAL(> (N, M'), true)
U31'(tt, M', N) -> >'(N, M')
U32'(tt, M', N) -> QUOT(d(N, M'), M')
U32'(tt, M', N) -> d(N, M')
*(s(N), s(M)) -> +(N, +(M, *(N, M)))
*(s(N), s(M)) -> +(M, *(N, M))
*(s(N), s(M)) -> *(N, M)
+(s(N), s(M)) -> +(N, M)
<'(N, M) -> >'(M, N)
>'(s(N), s(M)) -> >'(N, M)
d(s(N), s(M)) -> d(N, M)
gcd(N', M') -> U11'(tt, M', N')
QUOT(N, M') -> U21'(tt, M', N)
QUOT(N, M') -> U31'(tt, M', N)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Inst
→DP Problem 4
↳Remaining
→DP Problem 5
↳Polo
→DP Problem 6
↳Polo
>'(s(N), s(M)) -> >'(N, M)
1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)
>'(s(N), s(M)) -> >'(N, M)
POL(_>_'(x1, x2)) = x1 POL(s_(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 7
↳Dependency Graph
→DP Problem 2
↳Polo
→DP Problem 3
↳Inst
→DP Problem 4
↳Remaining
→DP Problem 5
↳Polo
→DP Problem 6
↳Polo
1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polynomial Ordering
→DP Problem 3
↳Inst
→DP Problem 4
↳Remaining
→DP Problem 5
↳Polo
→DP Problem 6
↳Polo
d(s(N), s(M)) -> d(N, M)
1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)
d(s(N), s(M)) -> d(N, M)
d(x, y) == d(y, x)
POL(d(x1, x2)) = x1 + x2 POL(s_(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Instantiation Transformation
→DP Problem 4
↳Remaining
→DP Problem 5
↳Polo
→DP Problem 6
↳Polo
gcd(N', M') -> U11'(tt, M', N')
U12'(tt, M', N') -> gcd(d(N', M'), M')
U11'(tt, M', N') -> U12'(equal(> (N', M'), true), M', N')
1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)
no new Dependency Pairs are created.
gcd(N', M') -> U11'(tt, M', N')
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Inst
→DP Problem 4
↳Remaining Obligation(s)
→DP Problem 5
↳Polo
→DP Problem 6
↳Polo
QUOT(N, M') -> U31'(tt, M', N)
U32'(tt, M', N) -> QUOT(d(N, M'), M')
U31'(tt, M', N) -> U32'(equal(> (N, M'), true), M', N)
1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Inst
→DP Problem 4
↳Remaining
→DP Problem 5
↳Polynomial Ordering
→DP Problem 6
↳Polo
+(s(N), s(M)) -> +(N, M)
1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)
+(s(N), s(M)) -> +(N, M)
+(x, y) == +(y, x)
POL(_+_(x1, x2)) = x1 + x2 POL(s_(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Inst
→DP Problem 4
↳Remaining
→DP Problem 5
↳Polo
→DP Problem 6
↳Polynomial Ordering
*(s(N), s(M)) -> *(N, M)
1 -> s(0)
2 -> s(s(0))
3 -> s(s(s(0)))
4 -> s(s(s(s(0))))
5 -> s(s(s(s(s(0)))))
6 -> s(s(s(s(s(s(0))))))
7 -> s(s(s(s(s(s(s(0)))))))
U11(tt, M', N') -> U12(equal(> (N', M'), true), M', N')
U12(tt, M', N') -> gcd(d(N', M'), M')
U21(tt, M', N) -> U22(equal(> (M', N), true))
U22(tt) -> 0
U31(tt, M', N) -> U32(equal(> (N, M'), true), M', N)
U32(tt, M', N) -> s(quot(d(N, M'), M'))
*(N, 0) -> 0
*(s(N), s(M)) -> s(+(N, +(M, *(N, M))))
+(N, 0) -> N
+(s(N), s(M)) -> s(s(+(N, M)))
< (N, M) -> > (M, N)
> (0, M) -> false
> (N', 0) -> true
> (s(N), s(M)) -> > (N, M)
and(tt, X) -> X
d(0, N) -> N
d(s(N), s(M)) -> d(N, M)
equal(X, X) -> tt
gcd(0, N) -> 0
gcd(N', M') -> U11(tt, M', N')
gcd(N', N') -> N'
p(s(N)) -> N
quot(M', M') -> s(0)
quot(N, M') -> U21(tt, M', N)
quot(N, M') -> U31(tt, M', N)
*(s(N), s(M)) -> *(N, M)
*(x, y) == *(y, x)
POL(_*_(x1, x2)) = x1 + x2 POL(s_(x1)) = 1 + x1