YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

i(0(x0))	→	p(s(p(s(0(p(s(p(s(x0)))))))))
i(s(x0))	→	p(s(p(s(s(j(p(s(p(s(p(p(p(p(s(s(s(s(x0))))))))))))))))))
j(0(x0))	→	p(s(p(p(s(s(0(p(s(p(s(x0)))))))))))
j(s(x0))	→	s(s(s(s(p(p(s(s(i(p(s(p(s(x0)))))))))))))
p(p(s(x0)))	→	p(x0)
p(s(x0))	→	x0
p(0(x0))	→	0(s(s(s(s(s(s(s(s(x0)))))))))

Proof

1 Bounds

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

final states:

{43, 2, 42, 33, 28, 11, 1}

transitions:

33 → 23

61 → 17

51 → 16

18 → 20

3 → 64

3 → 61

9 → 1

59 → 31

34 → 38

34 → 53

65 → 18

20 → 22

31 → 28

1 → 53

1 → 34

8 → 58

8 → 30

13 → 50

13 → 15

26 → 11

53 → 38

2 → 4

2 → 18

2 → 65

2 → 42

11 → 53

11 → 34

4 → 6

28 → 23

12 → 60

12 → 51

7 → 9

7 → 31

7 → 59

35 → 52

35 → 37

24 → 26

43 → 42

p₀(19) → 20

p₀(8) → 9

p₀(37) → 38

p₀(14) → 15

p₀(3) → 4

p₀(15) → 16

p₀(5) → 6

p₀(29) → 30

p₀(16) → 17

p₀(10) → 1

p₀(2) → 42

p₀(25) → 26

p₀(27) → 11

p₀(36) → 37

p₀(17) → 18

p₀(32) → 28

p₀(30) → 31

p₀(21) → 22

0₀(6) → 7

0₀(47) → 43

j₀(22) → 23

i₀(6) → 34

s₀(2) → 3

s₀(18) → 19

s₀(46) → 47

s₀(9) → 10

s₀(24) → 25

s₀(4) → 5

s₀(8) → 29

s₀(26) → 27

s₀(38) → 39

s₀(3) → 12

s₀(14) → 44

s₀(23) → 24

s₀(7) → 8

s₀(35) → 36

s₀(45) → 46

s₀(20) → 21

s₀(39) → 40

s₀(40) → 41

s₀(12) → 13

s₀(34) → 35

s₀(41) → 33

s₀(44) → 45

s₀(31) → 32

s₀(13) → 14

p₁(58) → 59

p₁(50) → 51

p₁(60) → 61

p₁(52) → 53

p₁(64) → 65

f5₀ → 2

33	→	23
61	→	17
51	→	16
18	→	20
3	→	64
3	→	61
9	→	1
59	→	31
34	→	38
34	→	53
65	→	18
20	→	22
31	→	28
1	→	53
1	→	34
8	→	58
8	→	30
13	→	50
13	→	15
26	→	11
53	→	38
2	→	4
2	→	18
2	→	65
2	→	42
11	→	53
11	→	34
4	→	6
28	→	23
12	→	60
12	→	51
7	→	9
7	→	31
7	→	59
35	→	52
35	→	37
24	→	26
43	→	42
p₀(19)	→	20
p₀(8)	→	9
p₀(37)	→	38
p₀(14)	→	15
p₀(3)	→	4
p₀(15)	→	16
p₀(5)	→	6
p₀(29)	→	30
p₀(16)	→	17
p₀(10)	→	1
p₀(2)	→	42
p₀(25)	→	26
p₀(27)	→	11
p₀(36)	→	37
p₀(17)	→	18
p₀(32)	→	28
p₀(30)	→	31
p₀(21)	→	22
0₀(6)	→	7
0₀(47)	→	43
j₀(22)	→	23
i₀(6)	→	34
s₀(2)	→	3
s₀(18)	→	19
s₀(46)	→	47
s₀(9)	→	10
s₀(24)	→	25
s₀(4)	→	5
s₀(8)	→	29
s₀(26)	→	27
s₀(38)	→	39
s₀(3)	→	12
s₀(14)	→	44
s₀(23)	→	24
s₀(7)	→	8
s₀(35)	→	36
s₀(45)	→	46
s₀(20)	→	21
s₀(39)	→	40
s₀(40)	→	41
s₀(12)	→	13
s₀(34)	→	35
s₀(41)	→	33
s₀(44)	→	45
s₀(31)	→	32
s₀(13)	→	14
p₁(58)	→	59
p₁(50)	→	51
p₁(60)	→	61
p₁(52)	→	53
p₁(64)	→	65
f5₀	→	2