YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

→

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

Proof

1 String Reversal

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

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

→

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

1.1 Bounds

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

final states:

{1}

transitions:

18 → 41

50 → 13

90 → 52

20 → 5

1 → 4

1 → 3

60 → 43

86 → 91

14 → 51

100 → 54

7 → 11

46 → 81

b₃(96) → 97

b₃(94) → 95

b₃(98) → 99

a₁(11) → 12

a₁(41) → 42

a₁(42) → 43

a₁(13) → 14

a₁(43) → 44

a₁(12) → 13

c₂(87) → 88

c₂(59) → 60

c₂(85) → 86

c₂(89) → 90

c₂(55) → 56

c₂(57) → 58

b₁(14) → 15

b₁(46) → 47

b₁(18) → 19

b₁(48) → 49

b₁(44) → 45

b₁(16) → 17

f3₀ → 2

c₀(8) → 9

c₀(10) → 1

c₀(6) → 7

b₂(58) → 59

b₂(86) → 87

b₂(88) → 89

b₂(54) → 55

b₂(84) → 85

b₂(56) → 57

a₂(53) → 54

a₂(82) → 83

a₂(83) → 84

a₂(52) → 53

a₂(51) → 52

a₂(81) → 82

a₀(3) → 4

a₀(2) → 3

a₀(4) → 5

c₁(49) → 50

c₁(19) → 20

c₁(17) → 18

c₁(15) → 16

c₁(45) → 46

c₁(47) → 48

a₃(92) → 93

a₃(93) → 94

a₃(91) → 92

c₃(99) → 100

c₃(97) → 98

c₃(95) → 96

b₀(5) → 6

b₀(9) → 10

b₀(7) → 8

18	→	41
50	→	13
90	→	52
20	→	5
1	→	4
1	→	3
60	→	43
86	→	91
14	→	51
100	→	54
7	→	11
46	→	81
b₃(96)	→	97
b₃(94)	→	95
b₃(98)	→	99
a₁(11)	→	12
a₁(41)	→	42
a₁(42)	→	43
a₁(13)	→	14
a₁(43)	→	44
a₁(12)	→	13
c₂(87)	→	88
c₂(59)	→	60
c₂(85)	→	86
c₂(89)	→	90
c₂(55)	→	56
c₂(57)	→	58
b₁(14)	→	15
b₁(46)	→	47
b₁(18)	→	19
b₁(48)	→	49
b₁(44)	→	45
b₁(16)	→	17
f3₀	→	2
c₀(8)	→	9
c₀(10)	→	1
c₀(6)	→	7
b₂(58)	→	59
b₂(86)	→	87
b₂(88)	→	89
b₂(54)	→	55
b₂(84)	→	85
b₂(56)	→	57
a₂(53)	→	54
a₂(82)	→	83
a₂(83)	→	84
a₂(52)	→	53
a₂(51)	→	52
a₂(81)	→	82
a₀(3)	→	4
a₀(2)	→	3
a₀(4)	→	5
c₁(49)	→	50
c₁(19)	→	20
c₁(17)	→	18
c₁(15)	→	16
c₁(45)	→	46
c₁(47)	→	48
a₃(92)	→	93
a₃(93)	→	94
a₃(91)	→	92
c₃(99)	→	100
c₃(97)	→	98
c₃(95)	→	96
b₀(5)	→	6
b₀(9)	→	10
b₀(7)	→	8