YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(l(x0))	→	l(a(x0))
a(c(x0))	→	c(a(x0))
c(a(r(x0)))	→	r(a(x0))
l(r(a(x0)))	→	a(l(c(c(r(x0)))))

Proof

1 Bounds

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

final states:

{6, 5, 4, 1}

transitions:

33 → 3

33 → 1

25 → 21

32 → 51

51 → 70

39 → 32

50 → 1

50 → 71

9 → 11

5 → 4

37 → 58

34 → 21

34 → 25

1 → 3

1 → 33

1 → 74

8 → 20

13 → 6

60 → 49

38 → 48

36 → 61

72 → 59

72 → 63

52 → 36

22 → 12

2 → 32

2 → 35

4 → 3

4 → 33

63 → 59

7 → 23

35 → 73

74 → 71

a₂(73) → 74

a₂(61) → 62

a₂(58) → 59

a₂(70) → 71

a₂(48) → 49

r₂(71) → 72

l₁(12) → 13

l₁(38) → 39

a₁(20) → 21

a₁(32) → 33

a₁(11) → 12

a₁(23) → 24

r₀(3) → 5

r₀(2) → 7

f4₀ → 2

c₁(21) → 22

c₁(36) → 37

c₁(24) → 25

c₁(37) → 38

r₁(35) → 36

r₁(33) → 34

r₁(51) → 52

a₀(10) → 6

a₀(2) → 3

c₀(8) → 9

c₀(3) → 4

c₀(7) → 8

c₂(59) → 60

c₂(62) → 63

l₂(49) → 50

l₀(9) → 10

l₀(3) → 1

33	→	3
33	→	1
25	→	21
32	→	51
51	→	70
39	→	32
50	→	1
50	→	71
9	→	11
5	→	4
37	→	58
34	→	21
34	→	25
1	→	3
1	→	33
1	→	74
8	→	20
13	→	6
60	→	49
38	→	48
36	→	61
72	→	59
72	→	63
52	→	36
22	→	12
2	→	32
2	→	35
4	→	3
4	→	33
63	→	59
7	→	23
35	→	73
74	→	71
a₂(73)	→	74
a₂(61)	→	62
a₂(58)	→	59
a₂(70)	→	71
a₂(48)	→	49
r₂(71)	→	72
l₁(12)	→	13
l₁(38)	→	39
a₁(20)	→	21
a₁(32)	→	33
a₁(11)	→	12
a₁(23)	→	24
r₀(3)	→	5
r₀(2)	→	7
f4₀	→	2
c₁(21)	→	22
c₁(36)	→	37
c₁(24)	→	25
c₁(37)	→	38
r₁(35)	→	36
r₁(33)	→	34
r₁(51)	→	52
a₀(10)	→	6
a₀(2)	→	3
c₀(8)	→	9
c₀(3)	→	4
c₀(7)	→	8
c₂(59)	→	60
c₂(62)	→	63
l₂(49)	→	50
l₀(9)	→	10
l₀(3)	→	1