YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(d(x0))	→	d(b(c(b(d(x0)))))
a(x0)	→	b(b(f(b(b(x0)))))
b(d(b(x0)))	→	a(d(x0))
d(f(x0))	→	b(d(x0))

Proof

1 Bounds

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

final states:

{4, 12, 7, 1}

transitions:

39 → 27

39 → 9

39 → 26

39 → 25

39 → 3

39 → 4

39 → 21

3 → 25

37 → 40

60 → 27

60 → 39

73 → 75

26 → 67

76 → 41

38 → 55

22 → 37

2 → 19

4 → 3

4 → 20

45 → 27

45 → 39

12 → 26

12 → 4

12 → 21

12 → 8

30 → 12

68 → 22

74 → 38

24 → 12

43 → 73

d₀(2) → 3

d₀(6) → 1

f₁(27) → 28

d₂(37) → 38

d₂(73) → 74

f₃(57) → 58

c₀(4) → 5

b₃(56) → 57

b₃(58) → 59

b₃(59) → 60

b₃(43) → 44

b₃(41) → 42

b₃(55) → 56

f₀(9) → 10

d₁(23) → 24

d₁(19) → 20

a₀(3) → 12

b₀(2) → 8

b₀(10) → 11

b₀(8) → 9

b₀(3) → 4

b₀(11) → 7

b₀(5) → 6

c₁(67) → 68

c₁(21) → 22

a₂(38) → 39

c₃(42) → 43

b₁(29) → 30

b₁(25) → 26

b₁(26) → 27

b₁(28) → 29

b₁(22) → 23

b₁(20) → 21

d₃(75) → 76

d₃(44) → 45

d₃(40) → 41

f5₀ → 2

39	→	27
39	→	9
39	→	26
39	→	25
39	→	3
39	→	4
39	→	21
3	→	25
37	→	40
60	→	27
60	→	39
73	→	75
26	→	67
76	→	41
38	→	55
22	→	37
2	→	19
4	→	3
4	→	20
45	→	27
45	→	39
12	→	26
12	→	4
12	→	21
12	→	8
30	→	12
68	→	22
74	→	38
24	→	12
43	→	73
d₀(2)	→	3
d₀(6)	→	1
f₁(27)	→	28
d₂(37)	→	38
d₂(73)	→	74
f₃(57)	→	58
c₀(4)	→	5
b₃(56)	→	57
b₃(58)	→	59
b₃(59)	→	60
b₃(43)	→	44
b₃(41)	→	42
b₃(55)	→	56
f₀(9)	→	10
d₁(23)	→	24
d₁(19)	→	20
a₀(3)	→	12
b₀(2)	→	8
b₀(10)	→	11
b₀(8)	→	9
b₀(3)	→	4
b₀(11)	→	7
b₀(5)	→	6
c₁(67)	→	68
c₁(21)	→	22
a₂(38)	→	39
c₃(42)	→	43
b₁(29)	→	30
b₁(25)	→	26
b₁(26)	→	27
b₁(28)	→	29
b₁(22)	→	23
b₁(20)	→	21
d₃(75)	→	76
d₃(44)	→	45
d₃(40)	→	41
f5₀	→	2