42.83/20.58 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

42.83/20.58

42.83/20.58
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS

42.83/20.58

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳2 CdtProblem

42.83/20.58

↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳4 CdtProblem

42.83/20.58

↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)

42.83/20.58

↳6 CdtProblem

42.83/20.58

↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

42.83/20.58

↳8 CdtProblem

42.83/20.58

↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

42.83/20.58

↳10 CdtProblem

42.83/20.58

↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))

42.83/20.58

↳12 CdtProblem

42.83/20.58

↳13 CdtKnowledgeProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳14 CdtProblem

42.83/20.58

↳15 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳16 CdtProblem

42.83/20.58

↳17 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳18 CdtProblem

42.83/20.58

↳19 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳20 CdtProblem

42.83/20.58

↳21 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳22 CdtProblem

42.83/20.58

↳23 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳24 CdtProblem

42.83/20.58

↳25 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳26 CdtProblem

42.83/20.58

↳27 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳28 CdtProblem

42.83/20.58

↳29 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳30 CdtProblem

42.83/20.58

↳31 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳32 CdtProblem

42.83/20.58

↳33 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳34 CdtProblem

42.83/20.58

↳35 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳36 CdtProblem

42.83/20.58

↳37 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳38 CdtProblem

42.83/20.58

↳39 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳40 CdtProblem

42.83/20.58

↳41 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳42 CdtProblem

42.83/20.58

↳43 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳44 CdtProblem

42.83/20.58

↳45 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳46 CdtProblem

42.83/20.58

↳47 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳48 CdtProblem

42.83/20.58

↳49 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳50 CdtProblem

42.83/20.58

↳51 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳52 CdtProblem

42.83/20.58

↳53 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳54 CdtProblem

42.83/20.58

↳55 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳56 CdtProblem

42.83/20.58

↳57 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

42.83/20.58

↳58 CdtProblem

42.83/20.58

42.83/20.58 42.83/20.58

42.83/20.58

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f_0(x) → a 42.83/20.58
f_1(x) → g_1(x, x) 42.83/20.58
g_1(s(x), y) → b(f_0(y), g_1(x, y)) 42.83/20.58
f_2(x) → g_2(x, x) 42.83/20.59
g_2(s(x), y) → b(f_1(y), g_2(x, y)) 42.83/20.59
f_3(x) → g_3(x, x) 42.83/20.59
g_3(s(x), y) → b(f_2(y), g_3(x, y)) 42.83/20.59
f_4(x) → g_4(x, x) 42.83/20.59
g_4(s(x), y) → b(f_3(y), g_4(x, y)) 42.83/20.59
f_5(x) → g_5(x, x) 42.83/20.59
g_5(s(x), y) → b(f_4(y), g_5(x, y))

Rewrite Strategy: INNERMOST

42.83/20.59

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

42.83/20.59

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 42.83/20.59
f_1(z0) → g_1(z0, z0) 42.83/20.59
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 42.83/20.59
f_2(z0) → g_2(z0, z0) 42.83/20.59
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 42.83/20.59
f_3(z0) → g_3(z0, z0) 42.83/20.59
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 42.83/20.59
f_4(z0) → g_4(z0, z0) 42.83/20.59
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 42.83/20.59
f_5(z0) → g_5(z0, z0) 42.83/20.59
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_1(z0) → c1(G_1(z0, z0)) 42.83/20.59
G_1(s(z0), z1) → c2(F_0(z1), G_1(z0, z1)) 42.83/20.59
F_2(z0) → c3(G_2(z0, z0)) 42.83/20.59
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 42.83/20.59
F_3(z0) → c5(G_3(z0, z0)) 42.83/20.59
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 42.83/20.59
F_4(z0) → c7(G_4(z0, z0)) 42.83/20.59
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 42.83/20.59
F_5(z0) → c9(G_5(z0, z0)) 42.83/20.59
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1))

S tuples:

F_1(z0) → c1(G_1(z0, z0)) 42.83/20.59
G_1(s(z0), z1) → c2(F_0(z1), G_1(z0, z1)) 43.03/20.62
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.62
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.62
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.62
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.62
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.62
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.62
F_5(z0) → c9(G_5(z0, z0)) 43.03/20.62
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1))

K tuples:none
Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_1, G_1, F_2, G_2, F_3, G_3, F_4, G_4, F_5, G_5

Compound Symbols:

c1, c2, c3, c4, c5, c6, c7, c8, c9, c10

43.03/20.62

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

43.03/20.62

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.62
f_1(z0) → g_1(z0, z0) 43.03/20.62
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.62
f_2(z0) → g_2(z0, z0) 43.03/20.62
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.62
f_3(z0) → g_3(z0, z0) 43.03/20.62
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.62
f_4(z0) → g_4(z0, z0) 43.03/20.62
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.62
f_5(z0) → g_5(z0, z0) 43.03/20.62
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.62
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.62
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.62
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.62
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.62
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.62
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.62
F_5(z0) → c9(G_5(z0, z0)) 43.03/20.62
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.62
G_1(s(z0), z1) → c2(G_1(z0, z1))

S tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.62
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.62
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.62
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.62
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.62
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.62
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.62
F_5(z0) → c9(G_5(z0, z0)) 43.03/20.62
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.62
G_1(s(z0), z1) → c2(G_1(z0, z1))

K tuples:none
Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_1, F_2, G_2, F_3, G_3, F_4, G_4, F_5, G_5, G_1

Compound Symbols:

c1, c3, c4, c5, c6, c7, c8, c9, c10, c2

43.03/20.62

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

F_5(z0) → c9(G_5(z0, z0))

43.03/20.62

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.62
f_1(z0) → g_1(z0, z0) 43.03/20.62
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.62
f_2(z0) → g_2(z0, z0) 43.03/20.62
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.62
f_3(z0) → g_3(z0, z0) 43.03/20.62
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.62
f_4(z0) → g_4(z0, z0) 43.03/20.62
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.62
f_5(z0) → g_5(z0, z0) 43.03/20.62
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

S tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

K tuples:none
Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_1, F_2, G_2, F_3, G_3, F_4, G_4, G_5, G_1

Compound Symbols:

c1, c3, c4, c5, c6, c7, c8, c10, c2

43.03/20.64

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 43.03/20.64

POL(F_1(x₁)) = 0 43.03/20.64
POL(F_2(x₁)) = 0 43.03/20.64
POL(F_3(x₁)) = 0 43.03/20.64
POL(F_4(x₁)) = [1] 43.03/20.64
POL(G_1(x₁, x₂)) = 0 43.03/20.64
POL(G_2(x₁, x₂)) = 0 43.03/20.64
POL(G_3(x₁, x₂)) = 0 43.03/20.64
POL(G_4(x₁, x₂)) = 0 43.03/20.64
POL(G_5(x₁, x₂)) = [2]x₁ 43.03/20.64
POL(c1(x₁)) = x₁ 43.03/20.64
POL(c10(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(c2(x₁)) = x₁ 43.03/20.64
POL(c3(x₁)) = x₁ 43.03/20.64
POL(c4(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(c5(x₁)) = x₁ 43.03/20.64
POL(c6(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(c7(x₁)) = x₁ 43.03/20.64
POL(c8(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(s(x₁)) = [1] + x₁

43.03/20.64

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.64
f_1(z0) → g_1(z0, z0) 43.03/20.64
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.64
f_2(z0) → g_2(z0, z0) 43.03/20.64
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.64
f_3(z0) → g_3(z0, z0) 43.03/20.64
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.64
f_4(z0) → g_4(z0, z0) 43.03/20.64
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.64
f_5(z0) → g_5(z0, z0) 43.03/20.64
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

S tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

K tuples:

F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_1, F_2, G_2, F_3, G_3, F_4, G_4, G_5, G_1

Compound Symbols:

c1, c3, c4, c5, c6, c7, c8, c10, c2

43.03/20.64

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 43.03/20.64

POL(F_1(x₁)) = 0 43.03/20.64
POL(F_2(x₁)) = 0 43.03/20.64
POL(F_3(x₁)) = [3] 43.03/20.64
POL(F_4(x₁)) = [3]x₁ 43.03/20.64
POL(G_1(x₁, x₂)) = 0 43.03/20.64
POL(G_2(x₁, x₂)) = 0 43.03/20.64
POL(G_3(x₁, x₂)) = 0 43.03/20.64
POL(G_4(x₁, x₂)) = [3]x₁ 43.03/20.64
POL(G_5(x₁, x₂)) = [3]x₁ + [3]x₁·x₂ + [3]x₁² 43.03/20.64
POL(c1(x₁)) = x₁ 43.03/20.64
POL(c10(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(c2(x₁)) = x₁ 43.03/20.64
POL(c3(x₁)) = x₁ 43.03/20.64
POL(c4(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(c5(x₁)) = x₁ 43.03/20.64
POL(c6(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(c7(x₁)) = x₁ 43.03/20.64
POL(c8(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(s(x₁)) = [3] + x₁

43.03/20.64

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.64
f_1(z0) → g_1(z0, z0) 43.03/20.64
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.64
f_2(z0) → g_2(z0, z0) 43.03/20.64
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.64
f_3(z0) → g_3(z0, z0) 43.03/20.64
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.64
f_4(z0) → g_4(z0, z0) 43.03/20.64
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.64
f_5(z0) → g_5(z0, z0) 43.03/20.64
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

S tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

K tuples:

F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_1, F_2, G_2, F_3, G_3, F_4, G_4, G_5, G_1

Compound Symbols:

c1, c3, c4, c5, c6, c7, c8, c10, c2

43.03/20.64

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1))

We considered the (Usable) Rules:none
And the Tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

The order we found is given by the following interpretation:
Polynomial interpretation : 43.03/20.64

POL(F_1(x₁)) = 0 43.03/20.64
POL(F_2(x₁)) = 0 43.03/20.64
POL(F_3(x₁)) = x₁ 43.03/20.64
POL(F_4(x₁)) = [1] + x₁² 43.03/20.64
POL(G_1(x₁, x₂)) = 0 43.03/20.64
POL(G_2(x₁, x₂)) = 0 43.03/20.64
POL(G_3(x₁, x₂)) = x₁ 43.03/20.64
POL(G_4(x₁, x₂)) = [1] + x₁·x₂ 43.03/20.64
POL(G_5(x₁, x₂)) = x₁ + x₁·x₂ + x₁² + x₁³ + x₁²·x₂ + x₁·x₂² 43.03/20.64
POL(c1(x₁)) = x₁ 43.03/20.64
POL(c10(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(c2(x₁)) = x₁ 43.03/20.64
POL(c3(x₁)) = x₁ 43.03/20.64
POL(c4(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(c5(x₁)) = x₁ 43.03/20.64
POL(c6(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(c7(x₁)) = x₁ 43.03/20.64
POL(c8(x₁, x₂)) = x₁ + x₂ 43.03/20.64
POL(s(x₁)) = [1] + x₁

43.03/20.64

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.64
f_1(z0) → g_1(z0, z0) 43.03/20.64
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.64
f_2(z0) → g_2(z0, z0) 43.03/20.64
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.64
f_3(z0) → g_3(z0, z0) 43.03/20.64
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.64
f_4(z0) → g_4(z0, z0) 43.03/20.64
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.64
f_5(z0) → g_5(z0, z0) 43.03/20.64
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

S tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

K tuples:

F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_1, F_2, G_2, F_3, G_3, F_4, G_4, G_5, G_1

Compound Symbols:

c1, c3, c4, c5, c6, c7, c8, c10, c2

43.03/20.64

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

F_2(z0) → c3(G_2(z0, z0))

43.03/20.64

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.64
f_1(z0) → g_1(z0, z0) 43.03/20.64
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.64
f_2(z0) → g_2(z0, z0) 43.03/20.64
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.64
f_3(z0) → g_3(z0, z0) 43.03/20.64
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.64
f_4(z0) → g_4(z0, z0) 43.03/20.64
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.64
f_5(z0) → g_5(z0, z0) 43.03/20.64
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

S tuples:

F_1(z0) → c1(G_1(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1))

K tuples:

F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_1, F_2, G_2, F_3, G_3, F_4, G_4, G_5, G_1

Compound Symbols:

c1, c3, c4, c5, c6, c7, c8, c10, c2

43.03/20.64

(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F_1(z0) → c1(G_1(z0, z0)) by

F_1(s(y0)) → c1(G_1(s(y0), s(y0)))

43.03/20.64

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.64
f_1(z0) → g_1(z0, z0) 43.03/20.64
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.64
f_2(z0) → g_2(z0, z0) 43.03/20.64
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.64
f_3(z0) → g_3(z0, z0) 43.03/20.64
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.64
f_4(z0) → g_4(z0, z0) 43.03/20.64
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.64
f_5(z0) → g_5(z0, z0) 43.03/20.64
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_2(z0) → c3(G_2(z0, z0)) 43.03/20.64
G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.64
F_1(s(y0)) → c1(G_1(s(y0), s(y0)))

S tuples:

G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.64
F_1(s(y0)) → c1(G_1(s(y0), s(y0)))

K tuples:

F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_2(z0) → c3(G_2(z0, z0))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_2, G_2, F_3, G_3, F_4, G_4, G_5, G_1, F_1

Compound Symbols:

c3, c4, c5, c6, c7, c8, c10, c2, c1

43.03/20.64

(17) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F_2(z0) → c3(G_2(z0, z0)) by

F_2(s(y0)) → c3(G_2(s(y0), s(y0)))

43.03/20.64

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.64
f_1(z0) → g_1(z0, z0) 43.03/20.64
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.64
f_2(z0) → g_2(z0, z0) 43.03/20.64
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.64
f_3(z0) → g_3(z0, z0) 43.03/20.64
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.64
f_4(z0) → g_4(z0, z0) 43.03/20.64
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.64
f_5(z0) → g_5(z0, z0) 43.03/20.64
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.64
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.64
F_2(s(y0)) → c3(G_2(s(y0), s(y0)))

S tuples:

G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.64
F_1(s(y0)) → c1(G_1(s(y0), s(y0)))

K tuples:

F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_2(s(y0)) → c3(G_2(s(y0), s(y0)))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

G_2, F_3, G_3, F_4, G_4, G_5, G_1, F_1, F_2

Compound Symbols:

c4, c5, c6, c7, c8, c10, c2, c1, c3

43.03/20.64

(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_2(s(z0), z1) → c4(F_1(z1), G_2(z0, z1)) by

G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.64
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0)))

43.03/20.64

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.64
f_1(z0) → g_1(z0, z0) 43.03/20.64
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.64
f_2(z0) → g_2(z0, z0) 43.03/20.64
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.64
f_3(z0) → g_3(z0, z0) 43.03/20.64
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.64
f_4(z0) → g_4(z0, z0) 43.03/20.64
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.64
f_5(z0) → g_5(z0, z0) 43.03/20.64
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.64
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.64
F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.64
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.64
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0)))

S tuples:

G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.64
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.64
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.64
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0)))

K tuples:

F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
F_3(z0) → c5(G_3(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_2(s(y0)) → c3(G_2(s(y0), s(y0)))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_3, G_3, F_4, G_4, G_5, G_1, F_1, F_2, G_2

Compound Symbols:

c5, c6, c7, c8, c10, c2, c1, c3, c4

43.03/20.64

(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F_3(z0) → c5(G_3(z0, z0)) by

F_3(s(y0)) → c5(G_3(s(y0), s(y0)))

43.03/20.64

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.64
f_1(z0) → g_1(z0, z0) 43.03/20.64
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.64
f_2(z0) → g_2(z0, z0) 43.03/20.64
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.64
f_3(z0) → g_3(z0, z0) 43.03/20.64
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.64
f_4(z0) → g_4(z0, z0) 43.03/20.64
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.64
f_5(z0) → g_5(z0, z0) 43.03/20.64
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.64
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.64
F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.64
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.64
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) 43.03/20.64
F_3(s(y0)) → c5(G_3(s(y0), s(y0)))

S tuples:

G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.64
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.64
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.64
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0)))

K tuples:

F_4(z0) → c7(G_4(z0, z0)) 43.03/20.64
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.64
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.64
G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) 43.03/20.64
F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.64
F_3(s(y0)) → c5(G_3(s(y0), s(y0)))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

G_3, F_4, G_4, G_5, G_1, F_1, F_2, G_2, F_3

Compound Symbols:

c6, c7, c8, c10, c2, c1, c3, c4, c5

43.03/20.64

(23) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_3(s(z0), z1) → c6(F_2(z1), G_3(z0, z1)) by

G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.64
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0)))

43.03/20.64

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.64
f_1(z0) → g_1(z0, z0) 43.03/20.64
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.64
f_2(z0) → g_2(z0, z0) 43.03/20.64
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.64
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_4(z0) → c7(G_4(z0, z0)) 43.03/20.65
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.65
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.65
G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.65
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.65
F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0)))

S tuples:

G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.65
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.65
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0)))

K tuples:

F_4(z0) → c7(G_4(z0, z0)) 43.03/20.65
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.65
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.65
F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0)))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_4, G_4, G_5, G_1, F_1, F_2, G_2, F_3, G_3

Compound Symbols:

c7, c8, c10, c2, c1, c3, c4, c5, c6

43.03/20.65

(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F_4(z0) → c7(G_4(z0, z0)) by

F_4(s(y0)) → c7(G_4(s(y0), s(y0)))

43.03/20.65

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.65
G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.65
G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.65
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.65
F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0)))

S tuples:

G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.65
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.65
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0)))

K tuples:

G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.65
G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) 43.03/20.65
F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0)))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

G_4, G_5, G_1, F_1, F_2, G_2, F_3, G_3, F_4

Compound Symbols:

c8, c10, c2, c1, c3, c4, c5, c6, c7

43.03/20.65

(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_4(s(z0), z1) → c8(F_3(z1), G_4(z0, z1)) by

G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0)))

43.03/20.65

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.65
G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.65
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.65
F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0)))

S tuples:

G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.65
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.65
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0)))

K tuples:

G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) 43.03/20.65
F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0)))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

G_5, G_1, F_1, F_2, G_2, F_3, G_3, F_4, G_4

Compound Symbols:

c10, c2, c1, c3, c4, c5, c6, c7, c8

43.03/20.65

(29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_5(s(z0), z1) → c10(F_4(z1), G_5(z0, z1)) by

G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0)))

43.03/20.65

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.65
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.65
F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0)))

S tuples:

G_1(s(z0), z1) → c2(G_1(z0, z1)) 43.03/20.65
F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.65
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0)))

K tuples:

F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0)))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

G_1, F_1, F_2, G_2, F_3, G_3, F_4, G_4, G_5

Compound Symbols:

c2, c1, c3, c4, c5, c6, c7, c8, c10

43.03/20.65

(31) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_1(s(z0), z1) → c2(G_1(z0, z1)) by

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1))

43.03/20.65

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.65
F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1))

S tuples:

F_1(s(y0)) → c1(G_1(s(y0), s(y0))) 43.03/20.65
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1))

K tuples:

F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0)))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_1, F_2, G_2, F_3, G_3, F_4, G_4, G_5, G_1

Compound Symbols:

c1, c3, c4, c5, c6, c7, c8, c10, c2

43.03/20.65

(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F_1(s(y0)) → c1(G_1(s(y0), s(y0))) by

F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0))))

43.03/20.65

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0))))

S tuples:

G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0))))

K tuples:

F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0)))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_2, G_2, F_3, G_3, F_4, G_4, G_5, G_1, F_1

Compound Symbols:

c3, c4, c5, c6, c7, c8, c10, c2, c1

43.03/20.65

(35) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_2(s(s(y0)), z1) → c4(F_1(z1), G_2(s(y0), z1)) by

G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0))))

43.03/20.65

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0))))

S tuples:

G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0))))

K tuples:

F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0)))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_2, G_2, F_3, G_3, F_4, G_4, G_5, G_1, F_1

Compound Symbols:

c3, c4, c5, c6, c7, c8, c10, c2, c1

43.03/20.65

(37) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_2(s(z0), s(y0)) → c4(F_1(s(y0)), G_2(z0, s(y0))) by

G_2(s(s(y0)), s(z1)) → c4(F_1(s(z1)), G_2(s(y0), s(z1))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

43.03/20.65

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

S tuples:

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

K tuples:

F_2(s(y0)) → c3(G_2(s(y0), s(y0))) 43.03/20.65
F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0)))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_2, F_3, G_3, F_4, G_4, G_5, G_1, F_1, G_2

Compound Symbols:

c3, c5, c6, c7, c8, c10, c2, c1, c4

43.03/20.65

(39) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F_2(s(y0)) → c3(G_2(s(y0), s(y0))) by

F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0))))))

43.03/20.65

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1)))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0))))))

S tuples:

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

K tuples:

F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0))))))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_3, G_3, F_4, G_4, G_5, G_1, F_1, G_2, F_2

Compound Symbols:

c5, c6, c7, c8, c10, c2, c1, c4, c3

43.03/20.65

(41) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_3(s(s(y0)), z1) → c6(F_2(z1), G_3(s(y0), z1)) by

G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0))))))

43.03/20.65

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1)))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0))))))

S tuples:

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

K tuples:

F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0))))))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_3, G_3, F_4, G_4, G_5, G_1, F_1, G_2, F_2

Compound Symbols:

c5, c6, c7, c8, c10, c2, c1, c4, c3

43.03/20.65

(43) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_3(s(z0), s(y0)) → c6(F_2(s(y0)), G_3(z0, s(y0))) by

G_3(s(s(y0)), s(z1)) → c6(F_2(s(z1)), G_3(s(y0), s(z1))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1))))))

43.03/20.65

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1)))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1))))))

S tuples:

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

K tuples:

F_3(s(y0)) → c5(G_3(s(y0), s(y0))) 43.03/20.65
F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1))))))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_3, F_4, G_4, G_5, G_1, F_1, G_2, F_2, G_3

Compound Symbols:

c5, c7, c8, c10, c2, c1, c4, c3, c6

43.03/20.65

(45) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F_3(s(y0)) → c5(G_3(s(y0), s(y0))) by

F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1))))))

43.03/20.65

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1)))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1))))))

S tuples:

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

K tuples:

F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1))))))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_4, G_4, G_5, G_1, F_1, G_2, F_2, G_3, F_3

Compound Symbols:

c7, c8, c10, c2, c1, c4, c3, c6, c5

43.03/20.65

(47) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_4(s(s(y0)), z1) → c8(F_3(z1), G_4(s(y0), z1)) by

G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0))))))

43.03/20.65

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1)))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0))))))

S tuples:

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

K tuples:

F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0))))))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_4, G_4, G_5, G_1, F_1, G_2, F_2, G_3, F_3

Compound Symbols:

c7, c8, c10, c2, c1, c4, c3, c6, c5

43.03/20.65

(49) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_4(s(z0), s(y0)) → c8(F_3(s(y0)), G_4(z0, s(y0))) by

G_4(s(s(y0)), s(z1)) → c8(F_3(s(z1)), G_4(s(y0), s(z1))) 43.03/20.65
G_4(s(z0), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(z0, s(s(s(y0))))) 43.03/20.65
G_4(s(z0), s(s(y0))) → c8(F_3(s(s(y0))), G_4(z0, s(s(y0)))) 43.03/20.65
G_4(s(z0), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(z0, s(s(s(s(y0)))))) 43.03/20.65
G_4(s(s(s(s(y0)))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(s(y0))), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(y0)), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(y1)))) → c8(F_3(s(s(s(y1)))), G_4(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_4(s(s(s(y0))), s(s(y1))) → c8(F_3(s(s(y1))), G_4(s(s(y0)), s(s(y1)))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(s(y1))))) → c8(F_3(s(s(s(s(y1))))), G_4(s(s(y0)), s(s(s(s(y1))))))

43.03/20.65

(50) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1)))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_4(s(z0), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(z0, s(s(s(y0))))) 43.03/20.65
G_4(s(z0), s(s(y0))) → c8(F_3(s(s(y0))), G_4(z0, s(s(y0)))) 43.03/20.65
G_4(s(z0), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(z0, s(s(s(s(y0)))))) 43.03/20.65
G_4(s(s(s(s(y0)))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(s(y0))), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(y0)), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(y1)))) → c8(F_3(s(s(s(y1)))), G_4(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_4(s(s(s(y0))), s(s(y1))) → c8(F_3(s(s(y1))), G_4(s(s(y0)), s(s(y1)))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(s(y1))))) → c8(F_3(s(s(s(s(y1))))), G_4(s(s(y0)), s(s(s(s(y1))))))

S tuples:

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

K tuples:

F_4(s(y0)) → c7(G_4(s(y0), s(y0))) 43.03/20.65
G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_4(s(z0), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(z0, s(s(s(y0))))) 43.03/20.65
G_4(s(z0), s(s(y0))) → c8(F_3(s(s(y0))), G_4(z0, s(s(y0)))) 43.03/20.65
G_4(s(z0), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(z0, s(s(s(s(y0)))))) 43.03/20.65
G_4(s(s(s(s(y0)))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(s(y0))), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(y0)), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(y1)))) → c8(F_3(s(s(s(y1)))), G_4(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_4(s(s(s(y0))), s(s(y1))) → c8(F_3(s(s(y1))), G_4(s(s(y0)), s(s(y1)))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(s(y1))))) → c8(F_3(s(s(s(s(y1))))), G_4(s(s(y0)), s(s(s(s(y1))))))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_4, G_5, G_1, F_1, G_2, F_2, G_3, F_3, G_4

Compound Symbols:

c7, c10, c2, c1, c4, c3, c6, c5, c8

43.03/20.65

(51) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F_4(s(y0)) → c7(G_4(s(y0), s(y0))) by

F_4(s(s(s(y0)))) → c7(G_4(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_4(s(s(y0))) → c7(G_4(s(s(y0)), s(s(y0)))) 43.03/20.65
F_4(s(s(s(s(y1))))) → c7(G_4(s(s(s(s(y1)))), s(s(s(s(y1))))))

43.03/20.65

(52) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1)))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_4(s(z0), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(z0, s(s(s(y0))))) 43.03/20.65
G_4(s(z0), s(s(y0))) → c8(F_3(s(s(y0))), G_4(z0, s(s(y0)))) 43.03/20.65
G_4(s(z0), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(z0, s(s(s(s(y0)))))) 43.03/20.65
G_4(s(s(s(s(y0)))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(s(y0))), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(y0)), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(y1)))) → c8(F_3(s(s(s(y1)))), G_4(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_4(s(s(s(y0))), s(s(y1))) → c8(F_3(s(s(y1))), G_4(s(s(y0)), s(s(y1)))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(s(y1))))) → c8(F_3(s(s(s(s(y1))))), G_4(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_4(s(s(s(y0)))) → c7(G_4(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_4(s(s(y0))) → c7(G_4(s(s(y0)), s(s(y0)))) 43.03/20.65
F_4(s(s(s(s(y1))))) → c7(G_4(s(s(s(s(y1)))), s(s(s(s(y1))))))

S tuples:

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

K tuples:

G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) 43.03/20.65
G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_4(s(z0), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(z0, s(s(s(y0))))) 43.03/20.65
G_4(s(z0), s(s(y0))) → c8(F_3(s(s(y0))), G_4(z0, s(s(y0)))) 43.03/20.65
G_4(s(z0), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(z0, s(s(s(s(y0)))))) 43.03/20.65
G_4(s(s(s(s(y0)))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(s(y0))), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(y0)), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(y1)))) → c8(F_3(s(s(s(y1)))), G_4(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_4(s(s(s(y0))), s(s(y1))) → c8(F_3(s(s(y1))), G_4(s(s(y0)), s(s(y1)))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(s(y1))))) → c8(F_3(s(s(s(s(y1))))), G_4(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_4(s(s(s(y0)))) → c7(G_4(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_4(s(s(y0))) → c7(G_4(s(s(y0)), s(s(y0)))) 43.03/20.65
F_4(s(s(s(s(y1))))) → c7(G_4(s(s(s(s(y1)))), s(s(s(s(y1))))))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

G_5, G_1, F_1, G_2, F_2, G_3, F_3, G_4, F_4

Compound Symbols:

c10, c2, c1, c4, c3, c6, c5, c8, c7

43.03/20.65

(53) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_5(s(s(y0)), z1) → c10(F_4(z1), G_5(s(y0), z1)) by

G_5(s(s(s(y0))), z1) → c10(F_4(z1), G_5(s(s(y0)), z1)) 43.03/20.65
G_5(s(s(z0)), s(y1)) → c10(F_4(s(y1)), G_5(s(z0), s(y1))) 43.03/20.65
G_5(s(s(z0)), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(s(z0), s(s(s(y0))))) 43.03/20.65
G_5(s(s(z0)), s(s(y0))) → c10(F_4(s(s(y0))), G_5(s(z0), s(s(y0)))) 43.03/20.65
G_5(s(s(z0)), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(s(z0), s(s(s(s(y0))))))

43.03/20.65

(54) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1)))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_4(s(z0), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(z0, s(s(s(y0))))) 43.03/20.65
G_4(s(z0), s(s(y0))) → c8(F_3(s(s(y0))), G_4(z0, s(s(y0)))) 43.03/20.65
G_4(s(z0), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(z0, s(s(s(s(y0)))))) 43.03/20.65
G_4(s(s(s(s(y0)))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(s(y0))), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(y0)), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(y1)))) → c8(F_3(s(s(s(y1)))), G_4(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_4(s(s(s(y0))), s(s(y1))) → c8(F_3(s(s(y1))), G_4(s(s(y0)), s(s(y1)))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(s(y1))))) → c8(F_3(s(s(s(s(y1))))), G_4(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_4(s(s(s(y0)))) → c7(G_4(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_4(s(s(y0))) → c7(G_4(s(s(y0)), s(s(y0)))) 43.03/20.65
F_4(s(s(s(s(y1))))) → c7(G_4(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_5(s(s(s(y0))), z1) → c10(F_4(z1), G_5(s(s(y0)), z1)) 43.03/20.65
G_5(s(s(z0)), s(y1)) → c10(F_4(s(y1)), G_5(s(z0), s(y1))) 43.03/20.65
G_5(s(s(z0)), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(s(z0), s(s(s(y0))))) 43.03/20.65
G_5(s(s(z0)), s(s(y0))) → c10(F_4(s(s(y0))), G_5(s(z0), s(s(y0)))) 43.03/20.65
G_5(s(s(z0)), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(s(z0), s(s(s(s(y0))))))

S tuples:

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

K tuples:

G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_4(s(z0), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(z0, s(s(s(y0))))) 43.03/20.65
G_4(s(z0), s(s(y0))) → c8(F_3(s(s(y0))), G_4(z0, s(s(y0)))) 43.03/20.65
G_4(s(z0), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(z0, s(s(s(s(y0)))))) 43.03/20.65
G_4(s(s(s(s(y0)))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(s(y0))), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(y0)), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(y1)))) → c8(F_3(s(s(s(y1)))), G_4(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_4(s(s(s(y0))), s(s(y1))) → c8(F_3(s(s(y1))), G_4(s(s(y0)), s(s(y1)))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(s(y1))))) → c8(F_3(s(s(s(s(y1))))), G_4(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_4(s(s(s(y0)))) → c7(G_4(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_4(s(s(y0))) → c7(G_4(s(s(y0)), s(s(y0)))) 43.03/20.65
F_4(s(s(s(s(y1))))) → c7(G_4(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_5(s(s(s(y0))), z1) → c10(F_4(z1), G_5(s(s(y0)), z1)) 43.03/20.65
G_5(s(s(z0)), s(y1)) → c10(F_4(s(y1)), G_5(s(z0), s(y1))) 43.03/20.65
G_5(s(s(z0)), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(s(z0), s(s(s(y0))))) 43.03/20.65
G_5(s(s(z0)), s(s(y0))) → c10(F_4(s(s(y0))), G_5(s(z0), s(s(y0)))) 43.03/20.65
G_5(s(s(z0)), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(s(z0), s(s(s(s(y0))))))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

G_5, G_1, F_1, G_2, F_2, G_3, F_3, G_4, F_4

Compound Symbols:

c10, c2, c1, c4, c3, c6, c5, c8, c7

43.03/20.65

(55) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_5(s(z0), s(y0)) → c10(F_4(s(y0)), G_5(z0, s(y0))) by

G_5(s(s(y0)), s(z1)) → c10(F_4(s(z1)), G_5(s(y0), s(z1))) 43.03/20.65
G_5(s(z0), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(z0, s(s(s(y0))))) 43.03/20.65
G_5(s(z0), s(s(y0))) → c10(F_4(s(s(y0))), G_5(z0, s(s(y0)))) 43.03/20.65
G_5(s(z0), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(z0, s(s(s(s(y0)))))) 43.03/20.65
G_5(s(s(s(s(y0)))), s(z1)) → c10(F_4(s(z1)), G_5(s(s(s(y0))), s(z1))) 43.03/20.65
G_5(s(s(s(y0))), s(z1)) → c10(F_4(s(z1)), G_5(s(s(y0)), s(z1))) 43.03/20.65
G_5(s(s(s(y0))), s(s(s(y1)))) → c10(F_4(s(s(s(y1)))), G_5(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_5(s(s(s(y0))), s(s(y1))) → c10(F_4(s(s(y1))), G_5(s(s(y0)), s(s(y1)))) 43.03/20.65
G_5(s(s(s(y0))), s(s(s(s(y1))))) → c10(F_4(s(s(s(s(y1))))), G_5(s(s(y0)), s(s(s(s(y1))))))

43.03/20.65

(56) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1)))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_4(s(z0), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(z0, s(s(s(y0))))) 43.03/20.65
G_4(s(z0), s(s(y0))) → c8(F_3(s(s(y0))), G_4(z0, s(s(y0)))) 43.03/20.65
G_4(s(z0), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(z0, s(s(s(s(y0)))))) 43.03/20.65
G_4(s(s(s(s(y0)))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(s(y0))), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(y0)), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(y1)))) → c8(F_3(s(s(s(y1)))), G_4(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_4(s(s(s(y0))), s(s(y1))) → c8(F_3(s(s(y1))), G_4(s(s(y0)), s(s(y1)))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(s(y1))))) → c8(F_3(s(s(s(s(y1))))), G_4(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_4(s(s(s(y0)))) → c7(G_4(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_4(s(s(y0))) → c7(G_4(s(s(y0)), s(s(y0)))) 43.03/20.65
F_4(s(s(s(s(y1))))) → c7(G_4(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_5(s(s(s(y0))), z1) → c10(F_4(z1), G_5(s(s(y0)), z1)) 43.03/20.65
G_5(s(s(z0)), s(y1)) → c10(F_4(s(y1)), G_5(s(z0), s(y1))) 43.03/20.65
G_5(s(s(z0)), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(s(z0), s(s(s(y0))))) 43.03/20.65
G_5(s(s(z0)), s(s(y0))) → c10(F_4(s(s(y0))), G_5(s(z0), s(s(y0)))) 43.03/20.65
G_5(s(s(z0)), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_5(s(z0), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(z0, s(s(s(y0))))) 43.03/20.65
G_5(s(z0), s(s(y0))) → c10(F_4(s(s(y0))), G_5(z0, s(s(y0)))) 43.03/20.65
G_5(s(z0), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(z0, s(s(s(s(y0)))))) 43.03/20.65
G_5(s(s(s(s(y0)))), s(z1)) → c10(F_4(s(z1)), G_5(s(s(s(y0))), s(z1))) 43.03/20.65
G_5(s(s(s(y0))), s(z1)) → c10(F_4(s(z1)), G_5(s(s(y0)), s(z1))) 43.03/20.65
G_5(s(s(s(y0))), s(s(s(y1)))) → c10(F_4(s(s(s(y1)))), G_5(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_5(s(s(s(y0))), s(s(y1))) → c10(F_4(s(s(y1))), G_5(s(s(y0)), s(s(y1)))) 43.03/20.65
G_5(s(s(s(y0))), s(s(s(s(y1))))) → c10(F_4(s(s(s(s(y1))))), G_5(s(s(y0)), s(s(s(s(y1))))))

S tuples:

G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) 43.03/20.65
F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1))))

K tuples:

F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_4(s(z0), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(z0, s(s(s(y0))))) 43.03/20.65
G_4(s(z0), s(s(y0))) → c8(F_3(s(s(y0))), G_4(z0, s(s(y0)))) 43.03/20.65
G_4(s(z0), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(z0, s(s(s(s(y0)))))) 43.03/20.65
G_4(s(s(s(s(y0)))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(s(y0))), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(y0)), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(y1)))) → c8(F_3(s(s(s(y1)))), G_4(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_4(s(s(s(y0))), s(s(y1))) → c8(F_3(s(s(y1))), G_4(s(s(y0)), s(s(y1)))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(s(y1))))) → c8(F_3(s(s(s(s(y1))))), G_4(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_4(s(s(s(y0)))) → c7(G_4(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_4(s(s(y0))) → c7(G_4(s(s(y0)), s(s(y0)))) 43.03/20.65
F_4(s(s(s(s(y1))))) → c7(G_4(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_5(s(s(s(y0))), z1) → c10(F_4(z1), G_5(s(s(y0)), z1)) 43.03/20.65
G_5(s(s(z0)), s(y1)) → c10(F_4(s(y1)), G_5(s(z0), s(y1))) 43.03/20.65
G_5(s(s(z0)), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(s(z0), s(s(s(y0))))) 43.03/20.65
G_5(s(s(z0)), s(s(y0))) → c10(F_4(s(s(y0))), G_5(s(z0), s(s(y0)))) 43.03/20.65
G_5(s(s(z0)), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_5(s(z0), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(z0, s(s(s(y0))))) 43.03/20.65
G_5(s(z0), s(s(y0))) → c10(F_4(s(s(y0))), G_5(z0, s(s(y0)))) 43.03/20.65
G_5(s(z0), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(z0, s(s(s(s(y0)))))) 43.03/20.65
G_5(s(s(s(s(y0)))), s(z1)) → c10(F_4(s(z1)), G_5(s(s(s(y0))), s(z1))) 43.03/20.65
G_5(s(s(s(y0))), s(z1)) → c10(F_4(s(z1)), G_5(s(s(y0)), s(z1))) 43.03/20.65
G_5(s(s(s(y0))), s(s(s(y1)))) → c10(F_4(s(s(s(y1)))), G_5(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_5(s(s(s(y0))), s(s(y1))) → c10(F_4(s(s(y1))), G_5(s(s(y0)), s(s(y1)))) 43.03/20.65
G_5(s(s(s(y0))), s(s(s(s(y1))))) → c10(F_4(s(s(s(s(y1))))), G_5(s(s(y0)), s(s(s(s(y1))))))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

G_1, F_1, G_2, F_2, G_3, F_3, G_4, F_4, G_5

Compound Symbols:

c2, c1, c4, c3, c6, c5, c8, c7, c10

43.03/20.65

(57) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G_1(s(s(y0)), z1) → c2(G_1(s(y0), z1)) by

G_1(s(s(s(y0))), z1) → c2(G_1(s(s(y0)), z1))

43.03/20.65

(58) Obligation:

Complexity Dependency Tuples Problem
Rules:

f_0(z0) → a 43.03/20.65
f_1(z0) → g_1(z0, z0) 43.03/20.65
g_1(s(z0), z1) → b(f_0(z1), g_1(z0, z1)) 43.03/20.65
f_2(z0) → g_2(z0, z0) 43.03/20.65
g_2(s(z0), z1) → b(f_1(z1), g_2(z0, z1)) 43.03/20.65
f_3(z0) → g_3(z0, z0) 43.03/20.65
g_3(s(z0), z1) → b(f_2(z1), g_3(z0, z1)) 43.03/20.65
f_4(z0) → g_4(z0, z0) 43.03/20.65
g_4(s(z0), z1) → b(f_3(z1), g_4(z0, z1)) 43.03/20.65
f_5(z0) → g_5(z0, z0) 43.03/20.65
g_5(s(z0), z1) → b(f_4(z1), g_5(z0, z1))

Tuples:

F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1)))) 43.03/20.65
F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_4(s(z0), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(z0, s(s(s(y0))))) 43.03/20.65
G_4(s(z0), s(s(y0))) → c8(F_3(s(s(y0))), G_4(z0, s(s(y0)))) 43.03/20.65
G_4(s(z0), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(z0, s(s(s(s(y0)))))) 43.03/20.65
G_4(s(s(s(s(y0)))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(s(y0))), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(y0)), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(y1)))) → c8(F_3(s(s(s(y1)))), G_4(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_4(s(s(s(y0))), s(s(y1))) → c8(F_3(s(s(y1))), G_4(s(s(y0)), s(s(y1)))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(s(y1))))) → c8(F_3(s(s(s(s(y1))))), G_4(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_4(s(s(s(y0)))) → c7(G_4(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_4(s(s(y0))) → c7(G_4(s(s(y0)), s(s(y0)))) 43.03/20.65
F_4(s(s(s(s(y1))))) → c7(G_4(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_5(s(s(s(y0))), z1) → c10(F_4(z1), G_5(s(s(y0)), z1)) 43.03/20.65
G_5(s(s(z0)), s(y1)) → c10(F_4(s(y1)), G_5(s(z0), s(y1))) 43.03/20.65
G_5(s(s(z0)), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(s(z0), s(s(s(y0))))) 43.03/20.65
G_5(s(s(z0)), s(s(y0))) → c10(F_4(s(s(y0))), G_5(s(z0), s(s(y0)))) 43.03/20.65
G_5(s(s(z0)), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_5(s(z0), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(z0, s(s(s(y0))))) 43.03/20.65
G_5(s(z0), s(s(y0))) → c10(F_4(s(s(y0))), G_5(z0, s(s(y0)))) 43.03/20.65
G_5(s(z0), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(z0, s(s(s(s(y0)))))) 43.03/20.65
G_5(s(s(s(s(y0)))), s(z1)) → c10(F_4(s(z1)), G_5(s(s(s(y0))), s(z1))) 43.03/20.65
G_5(s(s(s(y0))), s(z1)) → c10(F_4(s(z1)), G_5(s(s(y0)), s(z1))) 43.03/20.65
G_5(s(s(s(y0))), s(s(s(y1)))) → c10(F_4(s(s(s(y1)))), G_5(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_5(s(s(s(y0))), s(s(y1))) → c10(F_4(s(s(y1))), G_5(s(s(y0)), s(s(y1)))) 43.03/20.65
G_5(s(s(s(y0))), s(s(s(s(y1))))) → c10(F_4(s(s(s(s(y1))))), G_5(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
G_1(s(s(s(y0))), z1) → c2(G_1(s(s(y0)), z1))

S tuples:

F_1(s(s(y0))) → c1(G_1(s(s(y0)), s(s(y0)))) 43.03/20.65
G_2(s(s(s(y0))), z1) → c4(F_1(z1), G_2(s(s(y0)), z1)) 43.03/20.65
G_2(s(s(z0)), s(y1)) → c4(F_1(s(y1)), G_2(s(z0), s(y1))) 43.03/20.65
G_2(s(s(z0)), s(s(y0))) → c4(F_1(s(s(y0))), G_2(s(z0), s(s(y0)))) 43.03/20.65
G_2(s(z0), s(s(y0))) → c4(F_1(s(s(y0))), G_2(z0, s(s(y0)))) 43.03/20.65
G_2(s(s(s(s(y0)))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(s(y0))), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(z1)) → c4(F_1(s(z1)), G_2(s(s(y0)), s(z1))) 43.03/20.65
G_2(s(s(s(y0))), s(s(y1))) → c4(F_1(s(s(y1))), G_2(s(s(y0)), s(s(y1)))) 43.03/20.65
G_1(s(s(s(y0))), z1) → c2(G_1(s(s(y0)), z1))

K tuples:

F_2(s(s(s(y0)))) → c3(G_2(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_2(s(s(y0))) → c3(G_2(s(s(y0)), s(s(y0)))) 43.03/20.65
F_2(s(s(s(s(y0))))) → c3(G_2(s(s(s(s(y0)))), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(y0))), z1) → c6(F_2(z1), G_3(s(s(y0)), z1)) 43.03/20.65
G_3(s(s(z0)), s(y1)) → c6(F_2(s(y1)), G_3(s(z0), s(y1))) 43.03/20.65
G_3(s(s(z0)), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(s(z0), s(s(s(y0))))) 43.03/20.65
G_3(s(s(z0)), s(s(y0))) → c6(F_2(s(s(y0))), G_3(s(z0), s(s(y0)))) 43.03/20.65
G_3(s(s(z0)), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_3(s(z0), s(s(s(y0)))) → c6(F_2(s(s(s(y0)))), G_3(z0, s(s(s(y0))))) 43.03/20.65
G_3(s(z0), s(s(y0))) → c6(F_2(s(s(y0))), G_3(z0, s(s(y0)))) 43.03/20.65
G_3(s(z0), s(s(s(s(y0))))) → c6(F_2(s(s(s(s(y0))))), G_3(z0, s(s(s(s(y0)))))) 43.03/20.65
G_3(s(s(s(s(y0)))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(s(y0))), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(z1)) → c6(F_2(s(z1)), G_3(s(s(y0)), s(z1))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(y1)))) → c6(F_2(s(s(s(y1)))), G_3(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_3(s(s(s(y0))), s(s(y1))) → c6(F_2(s(s(y1))), G_3(s(s(y0)), s(s(y1)))) 43.03/20.65
G_3(s(s(s(y0))), s(s(s(s(y1))))) → c6(F_2(s(s(s(s(y1))))), G_3(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_3(s(s(s(y0)))) → c5(G_3(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_3(s(s(y0))) → c5(G_3(s(s(y0)), s(s(y0)))) 43.03/20.65
F_3(s(s(s(s(y1))))) → c5(G_3(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_4(s(s(s(y0))), z1) → c8(F_3(z1), G_4(s(s(y0)), z1)) 43.03/20.65
G_4(s(s(z0)), s(y1)) → c8(F_3(s(y1)), G_4(s(z0), s(y1))) 43.03/20.65
G_4(s(s(z0)), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(s(z0), s(s(s(y0))))) 43.03/20.65
G_4(s(s(z0)), s(s(y0))) → c8(F_3(s(s(y0))), G_4(s(z0), s(s(y0)))) 43.03/20.65
G_4(s(s(z0)), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_4(s(z0), s(s(s(y0)))) → c8(F_3(s(s(s(y0)))), G_4(z0, s(s(s(y0))))) 43.03/20.65
G_4(s(z0), s(s(y0))) → c8(F_3(s(s(y0))), G_4(z0, s(s(y0)))) 43.03/20.65
G_4(s(z0), s(s(s(s(y0))))) → c8(F_3(s(s(s(s(y0))))), G_4(z0, s(s(s(s(y0)))))) 43.03/20.65
G_4(s(s(s(s(y0)))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(s(y0))), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(z1)) → c8(F_3(s(z1)), G_4(s(s(y0)), s(z1))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(y1)))) → c8(F_3(s(s(s(y1)))), G_4(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_4(s(s(s(y0))), s(s(y1))) → c8(F_3(s(s(y1))), G_4(s(s(y0)), s(s(y1)))) 43.03/20.65
G_4(s(s(s(y0))), s(s(s(s(y1))))) → c8(F_3(s(s(s(s(y1))))), G_4(s(s(y0)), s(s(s(s(y1)))))) 43.03/20.65
F_4(s(s(s(y0)))) → c7(G_4(s(s(s(y0))), s(s(s(y0))))) 43.03/20.65
F_4(s(s(y0))) → c7(G_4(s(s(y0)), s(s(y0)))) 43.03/20.65
F_4(s(s(s(s(y1))))) → c7(G_4(s(s(s(s(y1)))), s(s(s(s(y1)))))) 43.03/20.65
G_5(s(s(s(y0))), z1) → c10(F_4(z1), G_5(s(s(y0)), z1)) 43.03/20.65
G_5(s(s(z0)), s(y1)) → c10(F_4(s(y1)), G_5(s(z0), s(y1))) 43.03/20.65
G_5(s(s(z0)), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(s(z0), s(s(s(y0))))) 43.03/20.65
G_5(s(s(z0)), s(s(y0))) → c10(F_4(s(s(y0))), G_5(s(z0), s(s(y0)))) 43.03/20.65
G_5(s(s(z0)), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(s(z0), s(s(s(s(y0)))))) 43.03/20.65
G_5(s(z0), s(s(s(y0)))) → c10(F_4(s(s(s(y0)))), G_5(z0, s(s(s(y0))))) 43.03/20.65
G_5(s(z0), s(s(y0))) → c10(F_4(s(s(y0))), G_5(z0, s(s(y0)))) 43.03/20.65
G_5(s(z0), s(s(s(s(y0))))) → c10(F_4(s(s(s(s(y0))))), G_5(z0, s(s(s(s(y0)))))) 43.03/20.65
G_5(s(s(s(s(y0)))), s(z1)) → c10(F_4(s(z1)), G_5(s(s(s(y0))), s(z1))) 43.03/20.65
G_5(s(s(s(y0))), s(z1)) → c10(F_4(s(z1)), G_5(s(s(y0)), s(z1))) 43.03/20.65
G_5(s(s(s(y0))), s(s(s(y1)))) → c10(F_4(s(s(s(y1)))), G_5(s(s(y0)), s(s(s(y1))))) 43.03/20.65
G_5(s(s(s(y0))), s(s(y1))) → c10(F_4(s(s(y1))), G_5(s(s(y0)), s(s(y1)))) 43.03/20.65
G_5(s(s(s(y0))), s(s(s(s(y1))))) → c10(F_4(s(s(s(s(y1))))), G_5(s(s(y0)), s(s(s(s(y1))))))

Defined Rule Symbols:

f_0, f_1, g_1, f_2, g_2, f_3, g_3, f_4, g_4, f_5, g_5

Defined Pair Symbols:

F_1, G_2, F_2, G_3, F_3, G_4, F_4, G_5, G_1

Compound Symbols:

c1, c4, c3, c6, c5, c8, c7, c10, c2

43.03/20.65