YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

g(c(x0))	→	g(f(c(x0)))
g(f(c(x0)))	→	g(f(f(c(x0))))
g(g(x0))	→	g(f(g(x0)))
f(f(g(x0)))	→	g(f(x0))

Proof

1 Bounds

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

final states:

{10, 7, 5, 1}

transitions:

29 → 11

29 → 10

29 → 34

29 → 27

10 → 11

5 → 10

31 → 27

1 → 8

6 → 30

2 → 12

11 → 26

28 → 42

45 → 27

16 → 1

7 → 8

35 → 28

c₁(12) → 13

g₂(44) → 45

g₂(42) → 43

f₁(14) → 15

f₁(34) → 35

f₁(27) → 28

f₁(13) → 14

f3₀ → 2

g₀(9) → 7

g₀(2) → 8

g₀(6) → 5

g₀(4) → 1

g₀(11) → 10

f₂(43) → 44

c₀(2) → 3

g₁(28) → 29

g₁(30) → 31

g₁(26) → 27

g₁(15) → 16

f₀(8) → 9

f₀(2) → 11

f₀(3) → 4

f₀(4) → 6

29	→	11
29	→	10
29	→	34
29	→	27
10	→	11
5	→	10
31	→	27
1	→	8
6	→	30
2	→	12
11	→	26
28	→	42
45	→	27
16	→	1
7	→	8
35	→	28
c₁(12)	→	13
g₂(44)	→	45
g₂(42)	→	43
f₁(14)	→	15
f₁(34)	→	35
f₁(27)	→	28
f₁(13)	→	14
f3₀	→	2
g₀(9)	→	7
g₀(2)	→	8
g₀(6)	→	5
g₀(4)	→	1
g₀(11)	→	10
f₂(43)	→	44
c₀(2)	→	3
g₁(28)	→	29
g₁(30)	→	31
g₁(26)	→	27
g₁(15)	→	16
f₀(8)	→	9
f₀(2)	→	11
f₀(3)	→	4
f₀(4)	→	6