YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

tower(0(x0))	→	s(0(p(s(p(s(x0))))))
tower(s(x0))	→	p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x0))))))))))))))
twoto(0(x0))	→	s(0(x0))
twoto(s(x0))	→	p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x0))))))))))))))))))))))))))))))))
twice(0(x0))	→	0(x0)
twice(s(x0))	→	p(p(p(s(s(s(s(s(twice(p(p(p(s(s(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 Rule Removal

Using the linear polynomial interpretation over the arctic semiring over the integers

[twoto(x₁)]	=	0 · x₁ + -∞
[tower(x₁)]	=	1 · x₁ + -∞
[p(x₁)]	=	0 · x₁ + -∞
[twice(x₁)]	=	0 · x₁ + -∞
[0(x₁)]	=	0 · x₁ + -∞
[s(x₁)]	=	0 · x₁ + -∞

the rules

tower(s(x0))	→	p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x0))))))))))))))
twoto(0(x0))	→	s(0(x0))
twoto(s(x0))	→	p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x0))))))))))))))))))))))))))))))))
twice(0(x0))	→	0(x0)
twice(s(x0))	→	p(p(p(s(s(s(s(s(twice(p(p(p(s(s(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)))))))))

remain.

1.1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals

[twoto(x₁)]

1	2
0	1

· x₁ +

0	0
0	0

[tower(x₁)]

2	2
0	0

· x₁ +

2	0
0	0

[p(x₁)]

1	0
0	1

· x₁ +

0	0
0	0

[twice(x₁)]

1	0
0	1

· x₁ +

0	0
0	0

[0(x₁)]

2	2
0	0

· x₁ +

0	0
1	0

[s(x₁)]

1	0
0	1

· x₁ +

0	0
0	0

the rules

tower(s(x0))	→	p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x0))))))))))))))
twoto(s(x0))	→	p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x0))))))))))))))))))))))))))))))))
twice(0(x0))	→	0(x0)
twice(s(x0))	→	p(p(p(s(s(s(s(s(twice(p(p(p(s(s(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)))))))))

remain.

1.1.1 Bounds

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

final states:

{60, 2, 59, 45, 44, 16, 1}

transitions:

33 → 104

33 → 89

23 → 25

25 → 27

89 → 41

81 → 22

97 → 50

18 → 90

18 → 22

18 → 81

41 → 72

41 → 43

3 → 96

3 → 75

9 → 11

37 → 66

37 → 39

34 → 36

55 → 82

55 → 57

99 → 45

31 → 33

1 → 11

1 → 9

1 → 7

60 → 59

44 → 51

73 → 16

91 → 27

91 → 25

91 → 23

36 → 88

36 → 40

36 → 67

54 → 98

54 → 83

75 → 49

105 → 73

67 → 40

53 → 99

2 → 4

2 → 97

2 → 59

4 → 6

28 → 30

45 → 51

16 → 25

16 → 91

16 → 17

14 → 1

12 → 14

7 → 9

30 → 73

30 → 105

46 → 74

46 → 48

83 → 58

17 → 23

17 → 91

19 → 80

19 → 21

twoto₀(11) → 12

twoto₀(6) → 17

tower₀(6) → 7

s₀(33) → 34

s₀(23) → 24

s₀(41) → 42

s₀(14) → 15

s₀(63) → 64

s₀(30) → 31

s₀(37) → 38

s₀(19) → 20

s₀(7) → 8

s₀(51) → 52

s₀(34) → 35

s₀(55) → 56

s₀(46) → 47

s₀(36) → 37

s₀(18) → 19

s₀(28) → 29

s₀(3) → 46

s₀(47) → 61

s₀(64) → 65

s₀(9) → 10

s₀(25) → 26

s₀(54) → 55

s₀(12) → 13

s₀(61) → 62

s₀(53) → 54

s₀(31) → 32

s₀(62) → 63

s₀(17) → 18

s₀(2) → 3

s₀(4) → 5

s₀(52) → 53

twice₀(50) → 51

twice₀(27) → 28

0₀(65) → 60

0₀(2) → 44

f6₀ → 2

p₀(2) → 59

p₀(56) → 57

p₀(10) → 11

p₀(49) → 50

p₀(48) → 49

p₀(24) → 25

p₀(43) → 16

p₀(8) → 9

p₀(21) → 22

p₀(26) → 27

p₀(38) → 39

p₀(3) → 4

p₀(32) → 33

p₀(29) → 30

p₀(15) → 1

p₀(35) → 36

p₀(22) → 23

p₀(42) → 43

p₀(20) → 21

p₀(39) → 40

p₀(40) → 41

p₀(57) → 58

p₀(58) → 45

p₀(5) → 6

p₀(13) → 14

p₀(47) → 48

p₁(72) → 73

p₁(82) → 83

p₁(98) → 99

p₁(80) → 81

p₁(88) → 89

p₁(74) → 75

p₁(66) → 67

p₁(96) → 97

p₁(90) → 91

p₁(104) → 105

33	→	104
33	→	89
23	→	25
25	→	27
89	→	41
81	→	22
97	→	50
18	→	90
18	→	22
18	→	81
41	→	72
41	→	43
3	→	96
3	→	75
9	→	11
37	→	66
37	→	39
34	→	36
55	→	82
55	→	57
99	→	45
31	→	33
1	→	11
1	→	9
1	→	7
60	→	59
44	→	51
73	→	16
91	→	27
91	→	25
91	→	23
36	→	88
36	→	40
36	→	67
54	→	98
54	→	83
75	→	49
105	→	73
67	→	40
53	→	99
2	→	4
2	→	97
2	→	59
4	→	6
28	→	30
45	→	51
16	→	25
16	→	91
16	→	17
14	→	1
12	→	14
7	→	9
30	→	73
30	→	105
46	→	74
46	→	48
83	→	58
17	→	23
17	→	91
19	→	80
19	→	21
twoto₀(11)	→	12
twoto₀(6)	→	17
tower₀(6)	→	7
s₀(33)	→	34
s₀(23)	→	24
s₀(41)	→	42
s₀(14)	→	15
s₀(63)	→	64
s₀(30)	→	31
s₀(37)	→	38
s₀(19)	→	20
s₀(7)	→	8
s₀(51)	→	52
s₀(34)	→	35
s₀(55)	→	56
s₀(46)	→	47
s₀(36)	→	37
s₀(18)	→	19
s₀(28)	→	29
s₀(3)	→	46
s₀(47)	→	61
s₀(64)	→	65
s₀(9)	→	10
s₀(25)	→	26
s₀(54)	→	55
s₀(12)	→	13
s₀(61)	→	62
s₀(53)	→	54
s₀(31)	→	32
s₀(62)	→	63
s₀(17)	→	18
s₀(2)	→	3
s₀(4)	→	5
s₀(52)	→	53
twice₀(50)	→	51
twice₀(27)	→	28
0₀(65)	→	60
0₀(2)	→	44
f6₀	→	2
p₀(2)	→	59
p₀(56)	→	57
p₀(10)	→	11
p₀(49)	→	50
p₀(48)	→	49
p₀(24)	→	25
p₀(43)	→	16
p₀(8)	→	9
p₀(21)	→	22
p₀(26)	→	27
p₀(38)	→	39
p₀(3)	→	4
p₀(32)	→	33
p₀(29)	→	30
p₀(15)	→	1
p₀(35)	→	36
p₀(22)	→	23
p₀(42)	→	43
p₀(20)	→	21
p₀(39)	→	40
p₀(40)	→	41
p₀(57)	→	58
p₀(58)	→	45
p₀(5)	→	6
p₀(13)	→	14
p₀(47)	→	48
p₁(72)	→	73
p₁(82)	→	83
p₁(98)	→	99
p₁(80)	→	81
p₁(88)	→	89
p₁(74)	→	75
p₁(66)	→	67
p₁(96)	→	97
p₁(90)	→	91
p₁(104)	→	105