YES
Termination Proof using AProVETerm Rewriting System R:
[N, M, X, V1, V2]
U11(tt, N) -> N
U21(tt, M, N) -> s(plus(N, M))
U31(tt) -> 0
U41(tt, M, N) -> plus(x(N, M), N)
and(tt, X) -> X
isNat(0) -> tt
isNat(plus(V1, V2)) -> and(isNat(V1), isNat(V2))
isNat(s(V1)) -> isNat(V1)
isNat(x(V1, V2)) -> and(isNat(V1), isNat(V2))
plus(N, 0) -> U11(isNat(N), N)
plus(N, s(M)) -> U21(and(isNat(M), isNat(N)), M, N)
x(N, 0) -> U31(isNat(N))
x(N, s(M)) -> U41(and(isNat(M), isNat(N)), M, N)
Termination of R to be shown.
TRS
↳CSR to TRS Transformation
Trivial-Transformation successful.
Replacement map:
and(1, 2)
plus(1, 2)
U41(1, 2, 3)
U31(1)
x(1, 2)
U21(1, 2, 3)
s(1)
U11(1, 2)
isNat(1)
Old CSR:
U11(tt, N) -> N
U21(tt, M, N) -> s(plus(N, M))
U31(tt) -> 0
U41(tt, M, N) -> plus(x(N, M), N)
and(tt, X) -> X
isNat(0) -> tt
isNat(plus(V1, V2)) -> and(isNat(V1), isNat(V2))
isNat(s(V1)) -> isNat(V1)
isNat(x(V1, V2)) -> and(isNat(V1), isNat(V2))
plus(N, 0) -> U11(isNat(N), N)
plus(N, s(M)) -> U21(and(isNat(M), isNat(N)), M, N)
x(N, 0) -> U31(isNat(N))
x(N, s(M)) -> U41(and(isNat(M), isNat(N)), M, N)
new TRS:
U11(tt, N) -> N
U21(tt, M, N) -> s(plus(N, M))
plus(N, 0) -> U11(isNat(N), N)
plus(N, s(M)) -> U21(and(isNat(M), isNat(N)), M, N)
U31(tt) -> 0
U41(tt, M, N) -> plus(x(N, M), N)
x(N, 0) -> U31(isNat(N))
x(N, s(M)) -> U41(and(isNat(M), isNat(N)), M, N)
and(tt, X) -> X
isNat(0) -> tt
isNat(plus(V1, V2)) -> and(isNat(V1), isNat(V2))
isNat(s(V1)) -> isNat(V1)
isNat(x(V1, V2)) -> and(isNat(V1), isNat(V2))
TRS
↳CSRtoTRS
→TRS1
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
U21'(tt, M, N) -> PLUS(N, M)
PLUS(N, 0) -> U11'(isNat(N), N)
PLUS(N, 0) -> ISNAT(N)
PLUS(N, s(M)) -> U21'(and(isNat(M), isNat(N)), M, N)
PLUS(N, s(M)) -> AND(isNat(M), isNat(N))
PLUS(N, s(M)) -> ISNAT(M)
PLUS(N, s(M)) -> ISNAT(N)
U41'(tt, M, N) -> PLUS(x(N, M), N)
U41'(tt, M, N) -> X(N, M)
X(N, 0) -> U31'(isNat(N))
X(N, 0) -> ISNAT(N)
X(N, s(M)) -> U41'(and(isNat(M), isNat(N)), M, N)
X(N, s(M)) -> AND(isNat(M), isNat(N))
X(N, s(M)) -> ISNAT(M)
X(N, s(M)) -> ISNAT(N)
ISNAT(plus(V1, V2)) -> AND(isNat(V1), isNat(V2))
ISNAT(plus(V1, V2)) -> ISNAT(V1)
ISNAT(plus(V1, V2)) -> ISNAT(V2)
ISNAT(s(V1)) -> ISNAT(V1)
ISNAT(x(V1, V2)) -> AND(isNat(V1), isNat(V2))
ISNAT(x(V1, V2)) -> ISNAT(V1)
ISNAT(x(V1, V2)) -> ISNAT(V2)
Furthermore, R contains three SCCs.
TRS
↳CSRtoTRS
→TRS1
↳DPs
→DP Problem 1
↳Size-Change Principle
→DP Problem 2
↳SCP
→DP Problem 3
↳SCP
Dependency Pairs:
ISNAT(x(V1, V2)) -> ISNAT(V2)
ISNAT(x(V1, V2)) -> ISNAT(V1)
ISNAT(s(V1)) -> ISNAT(V1)
ISNAT(plus(V1, V2)) -> ISNAT(V2)
ISNAT(plus(V1, V2)) -> ISNAT(V1)
Rules:
U11(tt, N) -> N
U21(tt, M, N) -> s(plus(N, M))
plus(N, 0) -> U11(isNat(N), N)
plus(N, s(M)) -> U21(and(isNat(M), isNat(N)), M, N)
U31(tt) -> 0
U41(tt, M, N) -> plus(x(N, M), N)
x(N, 0) -> U31(isNat(N))
x(N, s(M)) -> U41(and(isNat(M), isNat(N)), M, N)
and(tt, X) -> X
isNat(0) -> tt
isNat(plus(V1, V2)) -> and(isNat(V1), isNat(V2))
isNat(s(V1)) -> isNat(V1)
isNat(x(V1, V2)) -> and(isNat(V1), isNat(V2))
We number the DPs as follows:
- ISNAT(x(V1, V2)) -> ISNAT(V2)
- ISNAT(x(V1, V2)) -> ISNAT(V1)
- ISNAT(s(V1)) -> ISNAT(V1)
- ISNAT(plus(V1, V2)) -> ISNAT(V2)
- ISNAT(plus(V1, V2)) -> ISNAT(V1)
and get the following Size-Change Graph(s): | {5, 4, 3, 2, 1} | , | {5, 4, 3, 2, 1} |
|---|
| 1 | > | 1 |
|
which lead(s) to this/these maximal multigraph(s): | {5, 4, 3, 2, 1} | , | {5, 4, 3, 2, 1} |
|---|
| 1 | > | 1 |
|
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
plus(x1, x2) -> plus(x1, x2)
x(x1, x2) -> x(x1, x2)
s(x1) -> s(x1)
We obtain no new DP problems.
TRS
↳CSRtoTRS
→TRS1
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳Size-Change Principle
→DP Problem 3
↳SCP
Dependency Pairs:
PLUS(N, s(M)) -> U21'(and(isNat(M), isNat(N)), M, N)
U21'(tt, M, N) -> PLUS(N, M)
Rules:
U11(tt, N) -> N
U21(tt, M, N) -> s(plus(N, M))
plus(N, 0) -> U11(isNat(N), N)
plus(N, s(M)) -> U21(and(isNat(M), isNat(N)), M, N)
U31(tt) -> 0
U41(tt, M, N) -> plus(x(N, M), N)
x(N, 0) -> U31(isNat(N))
x(N, s(M)) -> U41(and(isNat(M), isNat(N)), M, N)
and(tt, X) -> X
isNat(0) -> tt
isNat(plus(V1, V2)) -> and(isNat(V1), isNat(V2))
isNat(s(V1)) -> isNat(V1)
isNat(x(V1, V2)) -> and(isNat(V1), isNat(V2))
We number the DPs as follows:
- PLUS(N, s(M)) -> U21'(and(isNat(M), isNat(N)), M, N)
- U21'(tt, M, N) -> PLUS(N, M)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
s(x1) -> s(x1)
We obtain no new DP problems.
TRS
↳CSRtoTRS
→TRS1
↳DPs
→DP Problem 1
↳SCP
→DP Problem 2
↳SCP
→DP Problem 3
↳Size-Change Principle
Dependency Pairs:
X(N, s(M)) -> U41'(and(isNat(M), isNat(N)), M, N)
U41'(tt, M, N) -> X(N, M)
Rules:
U11(tt, N) -> N
U21(tt, M, N) -> s(plus(N, M))
plus(N, 0) -> U11(isNat(N), N)
plus(N, s(M)) -> U21(and(isNat(M), isNat(N)), M, N)
U31(tt) -> 0
U41(tt, M, N) -> plus(x(N, M), N)
x(N, 0) -> U31(isNat(N))
x(N, s(M)) -> U41(and(isNat(M), isNat(N)), M, N)
and(tt, X) -> X
isNat(0) -> tt
isNat(plus(V1, V2)) -> and(isNat(V1), isNat(V2))
isNat(s(V1)) -> isNat(V1)
isNat(x(V1, V2)) -> and(isNat(V1), isNat(V2))
We number the DPs as follows:
- X(N, s(M)) -> U41'(and(isNat(M), isNat(N)), M, N)
- U41'(tt, M, N) -> X(N, M)
and get the following Size-Change Graph(s):
which lead(s) to this/these maximal multigraph(s):
DP: empty set
Oriented Rules: none
We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial
with Argument Filtering System:
s(x1) -> s(x1)
We obtain no new DP problems.
Termination of R successfully shown.
Duration:
0:15 minutes