YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

foo(0(x0))	→	0(s(p(p(p(s(s(s(p(s(x0))))))))))
foo(s(x0))	→	p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x0))))))))))))))))))))))))))
bar(0(x0))	→	0(p(s(s(s(x0)))))
bar(s(x0))	→	p(s(p(p(s(s(foo(s(p(p(s(s(x0))))))))))))
p(p(s(x0)))	→	p(x0)
p(s(x0))	→	x0
p(0(x0))	→	0(s(s(s(s(x0)))))

Proof

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

0(foo(x0))	→	s(p(s(s(s(p(p(p(s(0(x0))))))))))
s(foo(x0))	→	s(p(s(s(p(p(bar(s(p(s(s(p(p(foo(s(p(s(s(p(s(s(p(p(p(s(p(x0))))))))))))))))))))))))))
0(bar(x0))	→	s(s(s(p(0(x0)))))
s(bar(x0))	→	s(s(p(p(s(foo(s(s(p(p(s(p(x0))))))))))))
s(p(p(x0)))	→	p(x0)
s(p(x0))	→	x0
0(p(x0))	→	s(s(s(s(0(x0)))))

1.1 Bounds

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

final states:

{50, 2, 13, 42, 38, 12, 1}

transitions:

33 → 35

25 → 107

32 → 123

29 → 31

81 → 24

81 → 147

81 → 82

81 → 44

81 → 22

87 → 89

80 → 82

10 → 1

97 → 99

15 → 129

15 → 43

129 → 21

129 → 19

84 → 86

145 → 106

145 → 104

122 → 43

122 → 19

133 → 89

133 → 87

3 → 40

146 → 103

108 → 28

134 → 86

5 → 115

147 → 92

147 → 90

130 → 18

90 → 92

107 → 31

107 → 29

1 → 40

1 → 3

123 → 36

13 → 22

13 → 44

13 → 121

13 → 14

101 → 103

139 → 99

139 → 97

44 → 80

26 → 28

38 → 40

38 → 3

36 → 12

138 → 9

121 → 44

121 → 24

121 → 22

6 → 8

116 → 8

22 → 24

124 → 35

82 → 147

2 → 14

4 → 137

106 → 46

114 → 49

16 → 18

14 → 121

93 → 139

140 → 96

104 → 106

100 → 145

113 → 42

137 → 1

137 → 10

46 → 113

115 → 9

83 → 133

47 → 49

148 → 89

148 → 87

148 → 90

148 → 82

19 → 21

94 → 96

s₀(9) → 10

s₀(11) → 1

s₀(8) → 9

s₀(28) → 29

s₀(37) → 12

s₀(3) → 4

s₀(18) → 19

s₀(51) → 52

s₀(40) → 41

s₀(7) → 8

s₀(23) → 24

s₀(16) → 43

s₀(39) → 40

s₀(49) → 42

s₀(4) → 51

s₀(45) → 46

s₀(52) → 50

s₀(43) → 44

s₀(48) → 49

s₀(34) → 35

s₀(27) → 28

s₀(20) → 21

s₀(35) → 36

s₀(13) → 14

s₀(17) → 18

s₀(30) → 31

s₀(21) → 22

s₀(41) → 38

s₁(105) → 106

s₁(96) → 97

s₁(88) → 89

s₁(95) → 96

s₁(98) → 99

s₁(91) → 92

s₁(85) → 86

s₁(89) → 90

s₁(103) → 104

s₁(102) → 103

s₁(86) → 87

s₁(81) → 82

0₀(2) → 3

bar₀(31) → 32

bar₁(99) → 100

foo₀(44) → 45

foo₀(24) → 25

p₀(2) → 13

p₀(46) → 47

p₀(10) → 11

p₀(19) → 20

p₀(36) → 37

p₀(25) → 26

p₀(4) → 5

p₀(26) → 27

p₀(3) → 39

p₀(6) → 7

p₀(14) → 15

p₀(32) → 33

p₀(29) → 30

p₀(33) → 34

p₀(15) → 16

p₀(22) → 23

p₀(16) → 17

p₀(5) → 6

p₀(47) → 48

foo₁(92) → 93

p₂(133) → 134

p₂(145) → 146

p₂(147) → 148

p₂(139) → 140

p₁(87) → 88

p₁(101) → 102

p₁(100) → 101

p₁(97) → 98

p₁(82) → 83

p₁(123) → 124

p₁(129) → 130

p₁(94) → 95

p₁(84) → 85

p₁(90) → 91

p₁(93) → 94

p₁(107) → 108

p₁(83) → 84

p₁(80) → 81

p₁(137) → 138

p₁(121) → 122

p₁(115) → 116

p₁(104) → 105

p₁(113) → 114

f5₀ → 2

33	→	35
25	→	107
32	→	123
29	→	31
81	→	24
81	→	147
81	→	82
81	→	44
81	→	22
87	→	89
80	→	82
10	→	1
97	→	99
15	→	129
15	→	43
129	→	21
129	→	19
84	→	86
145	→	106
145	→	104
122	→	43
122	→	19
133	→	89
133	→	87
3	→	40
146	→	103
108	→	28
134	→	86
5	→	115
147	→	92
147	→	90
130	→	18
90	→	92
107	→	31
107	→	29
1	→	40
1	→	3
123	→	36
13	→	22
13	→	44
13	→	121
13	→	14
101	→	103
139	→	99
139	→	97
44	→	80
26	→	28
38	→	40
38	→	3
36	→	12
138	→	9
121	→	44
121	→	24
121	→	22
6	→	8
116	→	8
22	→	24
124	→	35
82	→	147
2	→	14
4	→	137
106	→	46
114	→	49
16	→	18
14	→	121
93	→	139
140	→	96
104	→	106
100	→	145
113	→	42
137	→	1
137	→	10
46	→	113
115	→	9
83	→	133
47	→	49
148	→	89
148	→	87
148	→	90
148	→	82
19	→	21
94	→	96
s₀(9)	→	10
s₀(11)	→	1
s₀(8)	→	9
s₀(28)	→	29
s₀(37)	→	12
s₀(3)	→	4
s₀(18)	→	19
s₀(51)	→	52
s₀(40)	→	41
s₀(7)	→	8
s₀(23)	→	24
s₀(16)	→	43
s₀(39)	→	40
s₀(49)	→	42
s₀(4)	→	51
s₀(45)	→	46
s₀(52)	→	50
s₀(43)	→	44
s₀(48)	→	49
s₀(34)	→	35
s₀(27)	→	28
s₀(20)	→	21
s₀(35)	→	36
s₀(13)	→	14
s₀(17)	→	18
s₀(30)	→	31
s₀(21)	→	22
s₀(41)	→	38
s₁(105)	→	106
s₁(96)	→	97
s₁(88)	→	89
s₁(95)	→	96
s₁(98)	→	99
s₁(91)	→	92
s₁(85)	→	86
s₁(89)	→	90
s₁(103)	→	104
s₁(102)	→	103
s₁(86)	→	87
s₁(81)	→	82
0₀(2)	→	3
bar₀(31)	→	32
bar₁(99)	→	100
foo₀(44)	→	45
foo₀(24)	→	25
p₀(2)	→	13
p₀(46)	→	47
p₀(10)	→	11
p₀(19)	→	20
p₀(36)	→	37
p₀(25)	→	26
p₀(4)	→	5
p₀(26)	→	27
p₀(3)	→	39
p₀(6)	→	7
p₀(14)	→	15
p₀(32)	→	33
p₀(29)	→	30
p₀(33)	→	34
p₀(15)	→	16
p₀(22)	→	23
p₀(16)	→	17
p₀(5)	→	6
p₀(47)	→	48
foo₁(92)	→	93
p₂(133)	→	134
p₂(145)	→	146
p₂(147)	→	148
p₂(139)	→	140
p₁(87)	→	88
p₁(101)	→	102
p₁(100)	→	101
p₁(97)	→	98
p₁(82)	→	83
p₁(123)	→	124
p₁(129)	→	130
p₁(94)	→	95
p₁(84)	→	85
p₁(90)	→	91
p₁(93)	→	94
p₁(107)	→	108
p₁(83)	→	84
p₁(80)	→	81
p₁(137)	→	138
p₁(121)	→	122
p₁(115)	→	116
p₁(104)	→	105
p₁(113)	→	114
f5₀	→	2