TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60057 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (399ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (1ms), PolynomialOrderingProcessor (0ms), DependencyGraph (1ms), PolynomialLinearRange4 (254ms), DependencyGraph (1ms), PolynomialLinearRange4 (131ms), DependencyGraph (9ms), PolynomialLinearRange4 (108ms), DependencyGraph (2ms), PolynomialLinearRange4 (115ms), DependencyGraph (1ms), ReductionPairSAT (374ms), DependencyGraph (1ms), SizeChangePrinciple (timeout)].
| – Problem 3 was processed with processor PolynomialLinearRange4 (102ms).
| | – Problem 5 was processed with processor PolynomialLinearRange4 (64ms).
| | | – Problem 6 was processed with processor DependencyGraph (1ms).
| | | | – Problem 7 was processed with processor PolynomialLinearRange4 (54ms).
| | | | | – Problem 8 was processed with processor DependencyGraph (0ms).
| – Problem 4 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (2ms), PolynomialOrderingProcessor (0ms), DependencyGraph (1ms), PolynomialLinearRange4 (234ms), DependencyGraph (23ms), PolynomialLinearRange4 (119ms), DependencyGraph (1ms), PolynomialLinearRange4 (142ms), DependencyGraph (1ms), PolynomialLinearRange4 (136ms), DependencyGraph (1ms), ReductionPairSAT (636ms), DependencyGraph (1ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| x#(N, s(M)) | → | U71#(isNat(M), M, N) | | U71#(tt, M, N) | → | U72#(isNat(N), M, N) |
| U72#(tt, M, N) | → | x#(N, M) |
Rewrite Rules
| U11(tt, V2) | → | U12(isNat(V2)) | | U12(tt) | → | tt |
| U21(tt) | → | tt | | U31(tt, V2) | → | U32(isNat(V2)) |
| U32(tt) | → | tt | | U41(tt, N) | → | N |
| U51(tt, M, N) | → | U52(isNat(N), M, N) | | U52(tt, M, N) | → | s(plus(N, M)) |
| U61(tt) | → | 0 | | U71(tt, M, N) | → | U72(isNat(N), M, N) |
| U72(tt, M, N) | → | plus(x(N, M), N) | | isNat(0) | → | tt |
| isNat(plus(V1, V2)) | → | U11(isNat(V1), V2) | | isNat(s(V1)) | → | U21(isNat(V1)) |
| isNat(x(V1, V2)) | → | U31(isNat(V1), V2) | | plus(N, 0) | → | U41(isNat(N), N) |
| plus(N, s(M)) | → | U51(isNat(M), M, N) | | x(N, 0) | → | U61(isNat(N)) |
| x(N, s(M)) | → | U71(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, U71, isNat, U72, U61, 0, U51, s, tt, U41, U52, U11, U12, U31, U32, U21, x
Open Dependency Pair Problem 4
Dependency Pairs
| plus#(N, s(M)) | → | U51#(isNat(M), M, N) | | U52#(tt, M, N) | → | plus#(N, M) |
| U51#(tt, M, N) | → | U52#(isNat(N), M, N) |
Rewrite Rules
| U11(tt, V2) | → | U12(isNat(V2)) | | U12(tt) | → | tt |
| U21(tt) | → | tt | | U31(tt, V2) | → | U32(isNat(V2)) |
| U32(tt) | → | tt | | U41(tt, N) | → | N |
| U51(tt, M, N) | → | U52(isNat(N), M, N) | | U52(tt, M, N) | → | s(plus(N, M)) |
| U61(tt) | → | 0 | | U71(tt, M, N) | → | U72(isNat(N), M, N) |
| U72(tt, M, N) | → | plus(x(N, M), N) | | isNat(0) | → | tt |
| isNat(plus(V1, V2)) | → | U11(isNat(V1), V2) | | isNat(s(V1)) | → | U21(isNat(V1)) |
| isNat(x(V1, V2)) | → | U31(isNat(V1), V2) | | plus(N, 0) | → | U41(isNat(N), N) |
| plus(N, s(M)) | → | U51(isNat(M), M, N) | | x(N, 0) | → | U61(isNat(N)) |
| x(N, s(M)) | → | U71(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, U71, isNat, U72, U61, 0, U51, s, tt, U41, U52, U11, U12, U31, U32, U21, x
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNat#(x(V1, V2)) | → | U31#(isNat(V1), V2) | | plus#(N, s(M)) | → | U51#(isNat(M), M, N) |
| plus#(N, 0) | → | isNat#(N) | | isNat#(s(V1)) | → | isNat#(V1) |
| isNat#(plus(V1, V2)) | → | U11#(isNat(V1), V2) | | U51#(tt, M, N) | → | isNat#(N) |
| U72#(tt, M, N) | → | plus#(x(N, M), N) | | U72#(tt, M, N) | → | x#(N, M) |
| U51#(tt, M, N) | → | U52#(isNat(N), M, N) | | plus#(N, s(M)) | → | isNat#(M) |
| U11#(tt, V2) | → | isNat#(V2) | | x#(N, s(M)) | → | U71#(isNat(M), M, N) |
| x#(N, 0) | → | U61#(isNat(N)) | | U71#(tt, M, N) | → | U72#(isNat(N), M, N) |
| isNat#(x(V1, V2)) | → | isNat#(V1) | | x#(N, 0) | → | isNat#(N) |
| isNat#(s(V1)) | → | U21#(isNat(V1)) | | U31#(tt, V2) | → | isNat#(V2) |
| isNat#(plus(V1, V2)) | → | isNat#(V1) | | plus#(N, 0) | → | U41#(isNat(N), N) |
| U71#(tt, M, N) | → | isNat#(N) | | U72#(tt, M, N) | → | T(M) |
| U52#(tt, M, N) | → | T(N) | | U11#(tt, V2) | → | U12#(isNat(V2)) |
| U52#(tt, M, N) | → | T(M) | | U31#(tt, V2) | → | U32#(isNat(V2)) |
| x#(N, s(M)) | → | isNat#(M) | | U72#(tt, M, N) | → | T(N) |
| U41#(tt, N) | → | T(N) | | U52#(tt, M, N) | → | plus#(N, M) |
Rewrite Rules
| U11(tt, V2) | → | U12(isNat(V2)) | | U12(tt) | → | tt |
| U21(tt) | → | tt | | U31(tt, V2) | → | U32(isNat(V2)) |
| U32(tt) | → | tt | | U41(tt, N) | → | N |
| U51(tt, M, N) | → | U52(isNat(N), M, N) | | U52(tt, M, N) | → | s(plus(N, M)) |
| U61(tt) | → | 0 | | U71(tt, M, N) | → | U72(isNat(N), M, N) |
| U72(tt, M, N) | → | plus(x(N, M), N) | | isNat(0) | → | tt |
| isNat(plus(V1, V2)) | → | U11(isNat(V1), V2) | | isNat(s(V1)) | → | U21(isNat(V1)) |
| isNat(x(V1, V2)) | → | U31(isNat(V1), V2) | | plus(N, 0) | → | U41(isNat(N), N) |
| plus(N, s(M)) | → | U51(isNat(M), M, N) | | x(N, 0) | → | U61(isNat(N)) |
| x(N, s(M)) | → | U71(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, U71, isNat, U72, U61, 0, U51, s, tt, U41, U52, U11, U12, U31, U32, U21, x
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(0) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U41) = μ(U72#) = μ(U21) = μ(U12#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U72) = μ(U71#) = μ(U51) = μ(s) = μ(U52) = μ(U32#) = μ(U11) = μ(U12) = μ(U31) = μ(U32) = {1}
μ(x#) = μ(plus) = μ(plus#) = μ(x) = {1, 2}
The following SCCs where found
| plus#(N, s(M)) → U51#(isNat(M), M, N) | U52#(tt, M, N) → plus#(N, M) |
| U51#(tt, M, N) → U52#(isNat(N), M, N) |
| isNat#(x(V1, V2)) → U31#(isNat(V1), V2) | isNat#(s(V1)) → isNat#(V1) |
| isNat#(plus(V1, V2)) → U11#(isNat(V1), V2) | U31#(tt, V2) → isNat#(V2) |
| isNat#(plus(V1, V2)) → isNat#(V1) | isNat#(x(V1, V2)) → isNat#(V1) |
| U11#(tt, V2) → isNat#(V2) |
| x#(N, s(M)) → U71#(isNat(M), M, N) | U71#(tt, M, N) → U72#(isNat(N), M, N) |
| U72#(tt, M, N) → x#(N, M) |
Problem 3: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNat#(x(V1, V2)) | → | U31#(isNat(V1), V2) | | isNat#(s(V1)) | → | isNat#(V1) |
| isNat#(plus(V1, V2)) | → | U11#(isNat(V1), V2) | | U31#(tt, V2) | → | isNat#(V2) |
| isNat#(plus(V1, V2)) | → | isNat#(V1) | | isNat#(x(V1, V2)) | → | isNat#(V1) |
| U11#(tt, V2) | → | isNat#(V2) |
Rewrite Rules
| U11(tt, V2) | → | U12(isNat(V2)) | | U12(tt) | → | tt |
| U21(tt) | → | tt | | U31(tt, V2) | → | U32(isNat(V2)) |
| U32(tt) | → | tt | | U41(tt, N) | → | N |
| U51(tt, M, N) | → | U52(isNat(N), M, N) | | U52(tt, M, N) | → | s(plus(N, M)) |
| U61(tt) | → | 0 | | U71(tt, M, N) | → | U72(isNat(N), M, N) |
| U72(tt, M, N) | → | plus(x(N, M), N) | | isNat(0) | → | tt |
| isNat(plus(V1, V2)) | → | U11(isNat(V1), V2) | | isNat(s(V1)) | → | U21(isNat(V1)) |
| isNat(x(V1, V2)) | → | U31(isNat(V1), V2) | | plus(N, 0) | → | U41(isNat(N), N) |
| plus(N, s(M)) | → | U51(isNat(M), M, N) | | x(N, 0) | → | U61(isNat(N)) |
| x(N, s(M)) | → | U71(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, U71, isNat, U72, U61, 0, U51, s, tt, U41, U52, U11, U12, U31, U32, U21, x
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(0) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U41) = μ(U72#) = μ(U21) = μ(U12#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U72) = μ(U71#) = μ(U51) = μ(s) = μ(U52) = μ(U32#) = μ(U11) = μ(U12) = μ(U31) = μ(U32) = {1}
μ(x#) = μ(plus) = μ(plus#) = μ(x) = {1, 2}
Polynomial Interpretation
- 0: 2
- U11(x,y): 0
- U11#(x,y): y
- U12(x): 0
- U21(x): 0
- U31(x,y): 0
- U31#(x,y): y
- U32(x): 0
- U41(x,y): 0
- U51(x,y,z): 0
- U52(x,y,z): 0
- U61(x): 0
- U71(x,y,z): 0
- U72(x,y,z): 0
- isNat(x): 0
- isNat#(x): x
- plus(x,y): y + 2x
- s(x): x + 1
- tt: 0
- x(x,y): 2y + 2x
Standard Usable rules
| U11(tt, V2) | → | U12(isNat(V2)) | | isNat(0) | → | tt |
| U21(tt) | → | tt | | U32(tt) | → | tt |
| U12(tt) | → | tt | | U31(tt, V2) | → | U32(isNat(V2)) |
| isNat(x(V1, V2)) | → | U31(isNat(V1), V2) | | isNat(plus(V1, V2)) | → | U11(isNat(V1), V2) |
| isNat(s(V1)) | → | U21(isNat(V1)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNat#(s(V1)) | → | isNat#(V1) |
Problem 5: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNat#(x(V1, V2)) | → | U31#(isNat(V1), V2) | | isNat#(plus(V1, V2)) | → | U11#(isNat(V1), V2) |
| U31#(tt, V2) | → | isNat#(V2) | | isNat#(plus(V1, V2)) | → | isNat#(V1) |
| isNat#(x(V1, V2)) | → | isNat#(V1) | | U11#(tt, V2) | → | isNat#(V2) |
Rewrite Rules
| U11(tt, V2) | → | U12(isNat(V2)) | | U12(tt) | → | tt |
| U21(tt) | → | tt | | U31(tt, V2) | → | U32(isNat(V2)) |
| U32(tt) | → | tt | | U41(tt, N) | → | N |
| U51(tt, M, N) | → | U52(isNat(N), M, N) | | U52(tt, M, N) | → | s(plus(N, M)) |
| U61(tt) | → | 0 | | U71(tt, M, N) | → | U72(isNat(N), M, N) |
| U72(tt, M, N) | → | plus(x(N, M), N) | | isNat(0) | → | tt |
| isNat(plus(V1, V2)) | → | U11(isNat(V1), V2) | | isNat(s(V1)) | → | U21(isNat(V1)) |
| isNat(x(V1, V2)) | → | U31(isNat(V1), V2) | | plus(N, 0) | → | U41(isNat(N), N) |
| plus(N, s(M)) | → | U51(isNat(M), M, N) | | x(N, 0) | → | U61(isNat(N)) |
| x(N, s(M)) | → | U71(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, U71, isNat, U72, U61, 0, U51, s, tt, U41, U52, U11, U12, U31, U32, U21, x
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(0) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U41) = μ(U72#) = μ(U21) = μ(U12#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U72) = μ(U71#) = μ(U51) = μ(s) = μ(U52) = μ(U32#) = μ(U11) = μ(U12) = μ(U31) = μ(U32) = {1}
μ(x#) = μ(plus) = μ(plus#) = μ(x) = {1, 2}
Polynomial Interpretation
- 0: 2
- U11(x,y): 0
- U11#(x,y): 2y
- U12(x): 0
- U21(x): 0
- U31(x,y): 0
- U31#(x,y): 3y
- U32(x): 0
- U41(x,y): 0
- U51(x,y,z): 0
- U52(x,y,z): 0
- U61(x): 0
- U71(x,y,z): 0
- U72(x,y,z): 0
- isNat(x): 0
- isNat#(x): 2x
- plus(x,y): y + 2x
- s(x): 3x + 3
- tt: 0
- x(x,y): 2y + 2x + 1
Standard Usable rules
| U11(tt, V2) | → | U12(isNat(V2)) | | isNat(0) | → | tt |
| U21(tt) | → | tt | | U32(tt) | → | tt |
| U12(tt) | → | tt | | U31(tt, V2) | → | U32(isNat(V2)) |
| isNat(x(V1, V2)) | → | U31(isNat(V1), V2) | | isNat(plus(V1, V2)) | → | U11(isNat(V1), V2) |
| isNat(s(V1)) | → | U21(isNat(V1)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNat#(x(V1, V2)) | → | U31#(isNat(V1), V2) | | isNat#(x(V1, V2)) | → | isNat#(V1) |
Problem 6: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNat#(plus(V1, V2)) | → | U11#(isNat(V1), V2) | | U31#(tt, V2) | → | isNat#(V2) |
| isNat#(plus(V1, V2)) | → | isNat#(V1) | | U11#(tt, V2) | → | isNat#(V2) |
Rewrite Rules
| U11(tt, V2) | → | U12(isNat(V2)) | | U12(tt) | → | tt |
| U21(tt) | → | tt | | U31(tt, V2) | → | U32(isNat(V2)) |
| U32(tt) | → | tt | | U41(tt, N) | → | N |
| U51(tt, M, N) | → | U52(isNat(N), M, N) | | U52(tt, M, N) | → | s(plus(N, M)) |
| U61(tt) | → | 0 | | U71(tt, M, N) | → | U72(isNat(N), M, N) |
| U72(tt, M, N) | → | plus(x(N, M), N) | | isNat(0) | → | tt |
| isNat(plus(V1, V2)) | → | U11(isNat(V1), V2) | | isNat(s(V1)) | → | U21(isNat(V1)) |
| isNat(x(V1, V2)) | → | U31(isNat(V1), V2) | | plus(N, 0) | → | U41(isNat(N), N) |
| plus(N, s(M)) | → | U51(isNat(M), M, N) | | x(N, 0) | → | U61(isNat(N)) |
| x(N, s(M)) | → | U71(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, U71, isNat, U72, U61, 0, U51, s, tt, U41, U52, U11, U12, U31, U32, U21, x
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(0) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U41) = μ(U72#) = μ(U21) = μ(U12#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U72) = μ(U71#) = μ(U51) = μ(s) = μ(U52) = μ(U32#) = μ(U11) = μ(U12) = μ(U31) = μ(U32) = {1}
μ(x#) = μ(plus) = μ(plus#) = μ(x) = {1, 2}
The following SCCs where found
| isNat#(plus(V1, V2)) → U11#(isNat(V1), V2) | isNat#(plus(V1, V2)) → isNat#(V1) |
| U11#(tt, V2) → isNat#(V2) |
Problem 7: PolynomialLinearRange4
Dependency Pair Problem
Dependency Pairs
| isNat#(plus(V1, V2)) | → | U11#(isNat(V1), V2) | | isNat#(plus(V1, V2)) | → | isNat#(V1) |
| U11#(tt, V2) | → | isNat#(V2) |
Rewrite Rules
| U11(tt, V2) | → | U12(isNat(V2)) | | U12(tt) | → | tt |
| U21(tt) | → | tt | | U31(tt, V2) | → | U32(isNat(V2)) |
| U32(tt) | → | tt | | U41(tt, N) | → | N |
| U51(tt, M, N) | → | U52(isNat(N), M, N) | | U52(tt, M, N) | → | s(plus(N, M)) |
| U61(tt) | → | 0 | | U71(tt, M, N) | → | U72(isNat(N), M, N) |
| U72(tt, M, N) | → | plus(x(N, M), N) | | isNat(0) | → | tt |
| isNat(plus(V1, V2)) | → | U11(isNat(V1), V2) | | isNat(s(V1)) | → | U21(isNat(V1)) |
| isNat(x(V1, V2)) | → | U31(isNat(V1), V2) | | plus(N, 0) | → | U41(isNat(N), N) |
| plus(N, s(M)) | → | U51(isNat(M), M, N) | | x(N, 0) | → | U61(isNat(N)) |
| x(N, s(M)) | → | U71(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, U71, isNat, U72, U61, 0, U51, s, tt, U41, U52, U11, U12, U31, U32, U21, x
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(0) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U41) = μ(U72#) = μ(U21) = μ(U12#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U72) = μ(U71#) = μ(U51) = μ(s) = μ(U52) = μ(U32#) = μ(U11) = μ(U12) = μ(U31) = μ(U32) = {1}
μ(x#) = μ(plus) = μ(plus#) = μ(x) = {1, 2}
Polynomial Interpretation
- 0: 0
- U11(x,y): x + 2
- U11#(x,y): 2y + x + 3
- U12(x): 0
- U21(x): 0
- U31(x,y): 3
- U32(x): 2
- U41(x,y): 0
- U51(x,y,z): 0
- U52(x,y,z): 0
- U61(x): 0
- U71(x,y,z): 0
- U72(x,y,z): 0
- isNat(x): x
- isNat#(x): x + 1
- plus(x,y): 2y + x + 2
- s(x): 0
- tt: 0
- x(x,y): 3
Standard Usable rules
| U11(tt, V2) | → | U12(isNat(V2)) | | isNat(0) | → | tt |
| U21(tt) | → | tt | | U32(tt) | → | tt |
| U12(tt) | → | tt | | U31(tt, V2) | → | U32(isNat(V2)) |
| isNat(x(V1, V2)) | → | U31(isNat(V1), V2) | | isNat(plus(V1, V2)) | → | U11(isNat(V1), V2) |
| isNat(s(V1)) | → | U21(isNat(V1)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| isNat#(plus(V1, V2)) | → | isNat#(V1) | | U11#(tt, V2) | → | isNat#(V2) |
Problem 8: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| isNat#(plus(V1, V2)) | → | U11#(isNat(V1), V2) |
Rewrite Rules
| U11(tt, V2) | → | U12(isNat(V2)) | | U12(tt) | → | tt |
| U21(tt) | → | tt | | U31(tt, V2) | → | U32(isNat(V2)) |
| U32(tt) | → | tt | | U41(tt, N) | → | N |
| U51(tt, M, N) | → | U52(isNat(N), M, N) | | U52(tt, M, N) | → | s(plus(N, M)) |
| U61(tt) | → | 0 | | U71(tt, M, N) | → | U72(isNat(N), M, N) |
| U72(tt, M, N) | → | plus(x(N, M), N) | | isNat(0) | → | tt |
| isNat(plus(V1, V2)) | → | U11(isNat(V1), V2) | | isNat(s(V1)) | → | U21(isNat(V1)) |
| isNat(x(V1, V2)) | → | U31(isNat(V1), V2) | | plus(N, 0) | → | U41(isNat(N), N) |
| plus(N, s(M)) | → | U51(isNat(M), M, N) | | x(N, 0) | → | U61(isNat(N)) |
| x(N, s(M)) | → | U71(isNat(M), M, N) |
Original Signature
Termination of terms over the following signature is verified: plus, U71, isNat, U72, U61, 0, U51, s, tt, U41, U52, U11, U12, U31, U32, U21, x
Strategy
Context-sensitive strategy:
μ(isNat) = μ(T) = μ(0) = μ(tt) = μ(isNat#) = ∅
μ(U11#) = μ(U31#) = μ(U21#) = μ(U52#) = μ(U41#) = μ(U61) = μ(U41) = μ(U72#) = μ(U21) = μ(U12#) = μ(U61#) = μ(U51#) = μ(U71) = μ(U72) = μ(U71#) = μ(U51) = μ(s) = μ(U52) = μ(U32#) = μ(U11) = μ(U12) = μ(U31) = μ(U32) = {1}
μ(x#) = μ(plus) = μ(plus#) = μ(x) = {1, 2}
There are no SCCs!