YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(a(b(x0)))	→	b(b(a(a(x0))))
b(a(x0))	→	a(c(b(x0)))

Proof

1 Bounds

The given TRS is match-bounded by 2. This is shown by the following automaton.

final states:

{6, 1}

transitions:

32 → 14

15 → 17

3 → 13

20 → 1

1 → 4

1 → 13

1 → 3

44 → 14

36 → 14

6 → 7

6 → 30

2 → 29

16 → 5

19 → 35

19 → 41

c₀(7) → 8

b₂(41) → 42

b₀(5) → 1

b₀(2) → 7

b₀(4) → 5

c₁(14) → 15

c₁(30) → 31

c₁(18) → 19

b₁(35) → 36

b₁(29) → 30

b₁(13) → 14

b₁(17) → 18

a₂(43) → 44

a₁(19) → 20

a₁(15) → 16

a₁(31) → 32

f3₀ → 2

c₂(42) → 43

a₀(8) → 6

a₀(2) → 3

a₀(3) → 4

32	→	14
15	→	17
3	→	13
20	→	1
1	→	4
1	→	13
1	→	3
44	→	14
36	→	14
6	→	7
6	→	30
2	→	29
16	→	5
19	→	35
19	→	41
c₀(7)	→	8
b₂(41)	→	42
b₀(5)	→	1
b₀(2)	→	7
b₀(4)	→	5
c₁(14)	→	15
c₁(30)	→	31
c₁(18)	→	19
b₁(35)	→	36
b₁(29)	→	30
b₁(13)	→	14
b₁(17)	→	18
a₂(43)	→	44
a₁(19)	→	20
a₁(15)	→	16
a₁(31)	→	32
f3₀	→	2
c₂(42)	→	43
a₀(8)	→	6
a₀(2)	→	3
a₀(3)	→	4