Term Rewriting System R:
[x]
f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
Innermost Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(b, f(a, f(a, f(a, f(b, x))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(b, f(a, f(a, f(a, f(b, x)))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(a, f(b, x))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(b, x)))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(b, x))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(b, x)
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳A-Transformation
Dependency Pairs:
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(b, x)))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(a, f(b, x))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))
Rule:
f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
Strategy:
innermost
We have an applicative DP problem with proper arity. Thus we can use the A-Transformation to obtain one new DP problem which consists of the A-transformed TRSs.
R
↳DPs
→DP Problem 1
↳ATrans
→DP Problem 2
↳RFC Match Bounds
Dependency Pairs:
A(a(b(a(a(b(a(x))))))) -> A(a(b(x)))
A(a(b(a(a(b(a(x))))))) -> A(a(a(b(x))))
A(a(b(a(a(b(a(x))))))) -> A(a(b(a(a(a(b(x)))))))
Rule:
a(a(b(a(a(b(a(x))))))) -> a(b(a(a(b(a(a(a(b(x)))))))))
Strategy:
innermost
Using RFC Match Bounds, the DP problem could be solved. The Match Bound was 3.
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90
Node 22 is start node and node 23 is final node.
Those nodes are connect through the following edges:
- 23 to 23 labelled #(0)
- 22 to 24 labelled A(0)
- 24 to 25 labelled a(0)
- 25 to 23 labelled b(0)
- 22 to 26 labelled A(0)
- 26 to 27 labelled a(0)
- 27 to 28 labelled b(0)
- 28 to 29 labelled a(0)
- 29 to 30 labelled a(0)
- 30 to 31 labelled a(0)
- 31 to 23 labelled b(0)
- 22 to 29 labelled A(0)
- 22 to 32 labelled A(1)
- 32 to 33 labelled a(1)
- 33 to 23 labelled b(1)
- 22 to 34 labelled A(1)
- 34 to 35 labelled a(1)
- 35 to 36 labelled a(1)
- 36 to 23 labelled b(1)
- 22 to 37 labelled A(1)
- 37 to 38 labelled a(1)
- 38 to 39 labelled b(1)
- 39 to 40 labelled a(1)
- 40 to 41 labelled a(1)
- 41 to 42 labelled a(1)
- 42 to 23 labelled b(1)
- 29 to 43 labelled a(1)
- 43 to 44 labelled b(1)
- 44 to 45 labelled a(1)
- 45 to 46 labelled a(1)
- 46 to 47 labelled b(1)
- 47 to 48 labelled a(1)
- 48 to 49 labelled a(1)
- 49 to 50 labelled a(1)
- 50 to 23 labelled b(1)
- 48 to 43 labelled a(1)
- 34 to 43 labelled a(1)
- 40 to 43 labelled a(1)
- 33 to 45 labelled b(1)
- 42 to 45 labelled b(1)
- 22 to 40 labelled A(1)
- 28 to 51 labelled a(1)
- 51 to 52 labelled b(1)
- 52 to 53 labelled a(1)
- 53 to 54 labelled a(1)
- 54 to 55 labelled b(1)
- 55 to 56 labelled a(1)
- 56 to 57 labelled a(1)
- 57 to 58 labelled a(1)
- 58 to 48 labelled b(1)
- 22 to 57 labelled A(1)
- 22 to 53 labelled A(1)
- 22 to 56 labelled A(1)
- 56 to 43 labelled a(1)
- 44 to 59 labelled a(2)
- 59 to 60 labelled b(2)
- 60 to 61 labelled a(2)
- 61 to 62 labelled a(2)
- 62 to 63 labelled b(2)
- 63 to 64 labelled a(2)
- 64 to 65 labelled a(2)
- 65 to 66 labelled a(2)
- 66 to 45 labelled b(2)
- 22 to 65 labelled A(2)
- 22 to 61 labelled A(2)
- 22 to 64 labelled A(2)
- 62 to 48 labelled b(2)
- 66 to 48 labelled b(2)
- 22 to 60 labelled A(2)
- 39 to 59 labelled a(2)
- 47 to 59 labelled a(2)
- 66 to 59 labelled b(2)
- 33 to 59 labelled b(1)
- 42 to 59 labelled b(1)
- 52 to 59 labelled a(2)
- 55 to 59 labelled a(2)
- 58 to 59 labelled b(1)
- 60 to 43 labelled a(1)
- 64 to 43 labelled a(1)
- 60 to 59 labelled a(2)
- 63 to 59 labelled a(2)
- 61 to 43 labelled b(2)
- 66 to 43 labelled b(2)
- 61 to 49 labelled b(2)
- 66 to 49 labelled b(2)
- 22 to 67 labelled A(3)
- 67 to 68 labelled a(3)
- 68 to 59 labelled b(3)
- 22 to 69 labelled A(3)
- 69 to 70 labelled a(3)
- 70 to 71 labelled b(3)
- 71 to 72 labelled a(3)
- 72 to 73 labelled a(3)
- 73 to 74 labelled a(3)
- 74 to 59 labelled b(3)
- 22 to 72 labelled A(3)
- 68 to 64 labelled b(3)
- 74 to 64 labelled b(3)
- 72 to 59 labelled a(2)
- 61 to 50 labelled b(2)
- 66 to 50 labelled b(2)
- 61 to 46 labelled b(2)
- 66 to 46 labelled b(2)
- 71 to 59 labelled a(2)
- 68 to 61 labelled b(3)
- 74 to 61 labelled b(3)
- 71 to 75 labelled a(3)
- 75 to 76 labelled b(3)
- 76 to 77 labelled a(3)
- 77 to 78 labelled a(3)
- 78 to 79 labelled b(3)
- 79 to 80 labelled a(3)
- 80 to 81 labelled a(3)
- 81 to 82 labelled a(3)
- 82 to 59 labelled b(3)
- 82 to 64 labelled b(3)
- 80 to 59 labelled a(2)
- 79 to 59 labelled a(2)
- 76 to 83 labelled a(3)
- 83 to 84 labelled b(3)
- 84 to 85 labelled a(3)
- 85 to 86 labelled a(3)
- 86 to 87 labelled b(3)
- 87 to 88 labelled a(3)
- 88 to 89 labelled a(3)
- 89 to 90 labelled a(3)
- 90 to 61 labelled b(3)
- 76 to 75 labelled a(3)
- 79 to 75 labelled a(3)
- 76 to 59 labelled a(2)
Innermost Termination of R successfully shown.
Duration:
0:01 minutes