YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

→

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

Proof

1 String Reversal

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

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

→

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

1.1 Bounds

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

final states:

{1}

transitions:

33 → 57

61 → 64

1 → 4

1 → 3

13 → 29

6 → 8

11 → 36

14 → 5

63 → 37

42 → 31

35 → 10

70 → 39

a₃(67) → 68

a₃(68) → 69

a₃(69) → 70

b₃(64) → 65

b₃(66) → 67

b₃(65) → 66

b₂(59) → 60

b₂(37) → 38

b₂(58) → 59

b₂(38) → 39

b₂(36) → 37

b₂(57) → 58

a₀(7) → 1

a₀(6) → 7

a₀(5) → 6

b₀(2) → 3

b₀(4) → 5

b₀(3) → 4

f2₀ → 2

b₁(9) → 10

b₁(8) → 9

b₁(29) → 30

b₁(10) → 11

b₁(31) → 32

b₁(30) → 31

a₂(61) → 62

a₂(62) → 63

a₂(39) → 40

a₂(40) → 41

a₂(60) → 61

a₂(41) → 42

a₁(13) → 14

a₁(33) → 34

a₁(12) → 13

a₁(32) → 33

a₁(11) → 12

a₁(34) → 35

33	→	57
61	→	64
1	→	4
1	→	3
13	→	29
6	→	8
11	→	36
14	→	5
63	→	37
42	→	31
35	→	10
70	→	39
a₃(67)	→	68
a₃(68)	→	69
a₃(69)	→	70
b₃(64)	→	65
b₃(66)	→	67
b₃(65)	→	66
b₂(59)	→	60
b₂(37)	→	38
b₂(58)	→	59
b₂(38)	→	39
b₂(36)	→	37
b₂(57)	→	58
a₀(7)	→	1
a₀(6)	→	7
a₀(5)	→	6
b₀(2)	→	3
b₀(4)	→	5
b₀(3)	→	4
f2₀	→	2
b₁(9)	→	10
b₁(8)	→	9
b₁(29)	→	30
b₁(10)	→	11
b₁(31)	→	32
b₁(30)	→	31
a₂(61)	→	62
a₂(62)	→	63
a₂(39)	→	40
a₂(40)	→	41
a₂(60)	→	61
a₂(41)	→	42
a₁(13)	→	14
a₁(33)	→	34
a₁(12)	→	13
a₁(32)	→	33
a₁(11)	→	12
a₁(34)	→	35