YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

→

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

Proof

1 String Reversal

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

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

→

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

1.1 Bounds

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

final states:

{1}

transitions:

80 → 54

80 → 55

10 → 41

50 → 13

20 → 6

20 → 52

20 → 53

1 → 5

1 → 4

1 → 3

8 → 11

60 → 43

6 → 51

17 → 71

a₁(11) → 12

a₁(44) → 45

a₁(14) → 15

a₁(18) → 19

a₁(51) → 52

a₁(16) → 17

a₁(54) → 55

a₁(58) → 59

a₁(53) → 54

a₁(52) → 53

a₁(43) → 44

a₁(48) → 49

a₁(42) → 43

a₁(56) → 57

a₁(12) → 13

a₁(46) → 47

a₁(13) → 14

a₁(41) → 42

a₀(5) → 6

a₀(7) → 8

a₀(9) → 10

a₀(2) → 3

a₀(4) → 5

a₀(3) → 4

a₂(73) → 74

a₂(78) → 79

a₂(76) → 77

a₂(72) → 73

a₂(74) → 75

a₂(71) → 72

b₂(79) → 80

b₂(75) → 76

b₂(77) → 78

b₀(8) → 9

b₀(6) → 7

b₀(10) → 1

f2₀ → 2

b₁(47) → 48

b₁(15) → 16

b₁(17) → 18

b₁(45) → 46

b₁(55) → 56

b₁(59) → 60

b₁(57) → 58

b₁(49) → 50

b₁(19) → 20

80	→	54
80	→	55
10	→	41
50	→	13
20	→	6
20	→	52
20	→	53
1	→	5
1	→	4
1	→	3
8	→	11
60	→	43
6	→	51
17	→	71
a₁(11)	→	12
a₁(44)	→	45
a₁(14)	→	15
a₁(18)	→	19
a₁(51)	→	52
a₁(16)	→	17
a₁(54)	→	55
a₁(58)	→	59
a₁(53)	→	54
a₁(52)	→	53
a₁(43)	→	44
a₁(48)	→	49
a₁(42)	→	43
a₁(56)	→	57
a₁(12)	→	13
a₁(46)	→	47
a₁(13)	→	14
a₁(41)	→	42
a₀(5)	→	6
a₀(7)	→	8
a₀(9)	→	10
a₀(2)	→	3
a₀(4)	→	5
a₀(3)	→	4
a₂(73)	→	74
a₂(78)	→	79
a₂(76)	→	77
a₂(72)	→	73
a₂(74)	→	75
a₂(71)	→	72
b₂(79)	→	80
b₂(75)	→	76
b₂(77)	→	78
b₀(8)	→	9
b₀(6)	→	7
b₀(10)	→	1
f2₀	→	2
b₁(47)	→	48
b₁(15)	→	16
b₁(17)	→	18
b₁(45)	→	46
b₁(55)	→	56
b₁(59)	→	60
b₁(57)	→	58
b₁(49)	→	50
b₁(19)	→	20