(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(x))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(x)))))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))))))))))))
Q is empty.
(1) QTRS Reverse (EQUIVALENT transformation)
We applied the QTRS Reverse Processor [REVERSE].
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
1(2(1(0(x)))) → 2(1(0(2(1(0(1(1(2(1(x))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(1(1(2(1(x)))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x))))))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x)))))))))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x))))))))))))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x)))))))))))))))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x))))))))))))))))))))))))))))
Q is empty.
(3) QTRSRoofMatchBoundsTAProof (EQUIVALENT transformation)
The TRS R could be shown to be Match-Bounded [TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] by 3. Therefore it terminates.
The compatible tree automaton used to show the Match-Boundedness is represented by:
final states : [0, 1, 2]
transitions:
10(0) → 0
10(1) → 0
10(2) → 0
20(0) → 1
20(1) → 1
20(2) → 1
00(0) → 2
00(1) → 2
00(2) → 2
11(0) → 10
21(10) → 9
11(9) → 8
11(8) → 7
01(7) → 6
11(6) → 3
21(3) → 5
01(5) → 4
11(4) → 3
21(3) → 0
11(1) → 10
11(2) → 10
11(7) → 10
11(5) → 10
12(7) → 18
22(18) → 17
12(17) → 16
12(16) → 15
02(15) → 14
12(14) → 11
22(11) → 13
02(13) → 12
12(12) → 11
22(11) → 10
12(5) → 18
12(15) → 18
13(15) → 26
23(26) → 25
13(25) → 24
13(24) → 23
03(23) → 22
13(22) → 19
23(19) → 21
03(21) → 20
13(20) → 19
23(19) → 18
13(13) → 26
5 → 10
5 → 8
13 → 7
13 → 18
21 → 26
(4) YES