YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

c(a(b(a(x0))))

→

a(b(a(a(c(a(b(c(a(b(x0))))))))))

Proof

1 String Reversal

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

a(b(a(c(x0))))

→

b(a(c(b(a(c(a(a(b(a(x0))))))))))

1.1 Bounds

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

final states:

{1}

transitions:

9 → 12

55 → 13

99 → 57

1 → 5

1 → 3

6 → 45

22 → 6

66 → 46

16 → 89

19 → 56

c₀(9) → 10

c₀(6) → 7

c₂(93) → 94

c₂(60) → 61

c₂(96) → 97

c₂(63) → 64

b₀(8) → 9

b₀(11) → 1

b₀(3) → 4

a₁(14) → 15

a₁(45) → 46

a₁(47) → 48

a₁(12) → 13

a₁(50) → 51

a₁(15) → 16

a₁(20) → 21

a₁(53) → 54

a₁(48) → 49

a₁(17) → 18

c₁(16) → 17

c₁(19) → 20

c₁(49) → 50

c₁(52) → 53

b₂(95) → 96

b₂(98) → 99

b₂(57) → 58

b₂(62) → 63

b₂(90) → 91

b₂(65) → 66

b₁(51) → 52

b₁(18) → 19

b₁(46) → 47

b₁(54) → 55

b₁(21) → 22

b₁(13) → 14

f3₀ → 2

a₂(97) → 98

a₂(58) → 59

a₂(61) → 62

a₂(94) → 95

a₂(59) → 60

a₂(56) → 57

a₂(92) → 93

a₂(89) → 90

a₂(64) → 65

a₂(91) → 92

a₀(10) → 11

a₀(5) → 6

a₀(2) → 3

a₀(4) → 5

a₀(7) → 8

9	→	12
55	→	13
99	→	57
1	→	5
1	→	3
6	→	45
22	→	6
66	→	46
16	→	89
19	→	56
c₀(9)	→	10
c₀(6)	→	7
c₂(93)	→	94
c₂(60)	→	61
c₂(96)	→	97
c₂(63)	→	64
b₀(8)	→	9
b₀(11)	→	1
b₀(3)	→	4
a₁(14)	→	15
a₁(45)	→	46
a₁(47)	→	48
a₁(12)	→	13
a₁(50)	→	51
a₁(15)	→	16
a₁(20)	→	21
a₁(53)	→	54
a₁(48)	→	49
a₁(17)	→	18
c₁(16)	→	17
c₁(19)	→	20
c₁(49)	→	50
c₁(52)	→	53
b₂(95)	→	96
b₂(98)	→	99
b₂(57)	→	58
b₂(62)	→	63
b₂(90)	→	91
b₂(65)	→	66
b₁(51)	→	52
b₁(18)	→	19
b₁(46)	→	47
b₁(54)	→	55
b₁(21)	→	22
b₁(13)	→	14
f3₀	→	2
a₂(97)	→	98
a₂(58)	→	59
a₂(61)	→	62
a₂(94)	→	95
a₂(59)	→	60
a₂(56)	→	57
a₂(92)	→	93
a₂(89)	→	90
a₂(64)	→	65
a₂(91)	→	92
a₀(10)	→	11
a₀(5)	→	6
a₀(2)	→	3
a₀(4)	→	5
a₀(7)	→	8