YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(s(x0))	→	s(s(s(p(s(b(p(p(s(s(x0))))))))))
b(s(x0))	→	s(s(s(p(p(s(s(c(p(s(p(s(x0))))))))))))
c(s(x0))	→	p(s(p(s(a(p(s(p(s(x0)))))))))
p(p(s(x0)))	→	p(x0)
p(s(x0))	→	x0

Proof

1 Bounds

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

final states:

{2, 28, 23, 12, 1}

transitions:

23 → 20

23 → 30

23 → 16

3 → 35

3 → 5

1 → 23

1 → 26

1 → 24

13 → 15

26 → 23

36 → 6

2 → 13

2 → 6

2 → 36

2 → 28

16 → 30

12 → 9

12 → 7

7 → 9

30 → 20

17 → 29

17 → 19

24 → 26

c₀(15) → 16

a₀(15) → 24

b₀(6) → 7

p₁(29) → 30

p₁(35) → 36

s₀(9) → 10

s₀(11) → 1

s₀(22) → 12

s₀(3) → 4

s₀(7) → 8

s₀(24) → 25

s₀(26) → 27

s₀(16) → 17

s₀(10) → 11

s₀(2) → 3

s₀(20) → 21

s₀(13) → 14

s₀(17) → 18

s₀(21) → 22

p₀(2) → 28

p₀(18) → 19

p₀(19) → 20

p₀(25) → 26

p₀(4) → 5

p₀(8) → 9

p₀(3) → 13

p₀(14) → 15

p₀(27) → 23

p₀(5) → 6

f5₀ → 2

23	→	20
23	→	30
23	→	16
3	→	35
3	→	5
1	→	23
1	→	26
1	→	24
13	→	15
26	→	23
36	→	6
2	→	13
2	→	6
2	→	36
2	→	28
16	→	30
12	→	9
12	→	7
7	→	9
30	→	20
17	→	29
17	→	19
24	→	26
c₀(15)	→	16
a₀(15)	→	24
b₀(6)	→	7
p₁(29)	→	30
p₁(35)	→	36
s₀(9)	→	10
s₀(11)	→	1
s₀(22)	→	12
s₀(3)	→	4
s₀(7)	→	8
s₀(24)	→	25
s₀(26)	→	27
s₀(16)	→	17
s₀(10)	→	11
s₀(2)	→	3
s₀(20)	→	21
s₀(13)	→	14
s₀(17)	→	18
s₀(21)	→	22
p₀(2)	→	28
p₀(18)	→	19
p₀(19)	→	20
p₀(25)	→	26
p₀(4)	→	5
p₀(8)	→	9
p₀(3)	→	13
p₀(14)	→	15
p₀(27)	→	23
p₀(5)	→	6
f5₀	→	2