MAYBE 0.00/0.85 MAYBE 0.00/0.87 0.00/0.87 0.00/0.87 0.00/0.87 0.00/0.87 0.00/0.87 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 0.00/0.87 0.00/0.87 0.00/0.87
0.00/0.87
0.00/0.87
0.00/0.87
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS
0.00/0.87 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
0.00/0.87 
↳2 CdtProblem
0.00/0.87 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
0.00/0.87 
↳4 CdtProblem
0.00/0.87 
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)
0.00/0.87 
↳6 CdtProblem
0.00/0.87
0.00/0.87 0.00/0.87
0.00/0.87
0.00/0.87

(0) Obligation:

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

equal0(Nil) → number42(Nil) 0.00/0.87
equal0(Cons(x, xs)) → equal0(Cons(x, xs)) 0.00/0.87
number42(x) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.87
goal(x) → equal0(x)

Rewrite Strategy: INNERMOST
0.00/0.87
0.00/0.87

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

Converted CpxTRS to CDT
0.00/0.87
0.00/0.87

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(Nil) → number42(Nil) 0.00/0.87
equal0(Cons(z0, z1)) → equal0(Cons(z0, z1)) 0.00/0.87
number42(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.87
goal(z0) → equal0(z0)
Tuples:

EQUAL0(Nil) → c(NUMBER42(Nil)) 0.00/0.87
EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1))) 0.00/0.87
GOAL(z0) → c3(EQUAL0(z0))
S tuples:

EQUAL0(Nil) → c(NUMBER42(Nil)) 0.00/0.87
EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1))) 0.00/0.87
GOAL(z0) → c3(EQUAL0(z0))
K tuples:none
Defined Rule Symbols:

equal0, number42, goal

Defined Pair Symbols:

EQUAL0, GOAL

Compound Symbols:

c, c1, c3

0.00/0.87
0.00/0.87

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

Removed 1 trailing tuple parts
0.00/0.87
0.00/0.87

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(Nil) → number42(Nil) 0.00/0.87
equal0(Cons(z0, z1)) → equal0(Cons(z0, z1)) 0.00/0.87
number42(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.87
goal(z0) → equal0(z0)
Tuples:

EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1))) 0.00/0.87
GOAL(z0) → c3(EQUAL0(z0)) 0.00/0.87
EQUAL0(Nil) → c
S tuples:

EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1))) 0.00/0.87
GOAL(z0) → c3(EQUAL0(z0)) 0.00/0.87
EQUAL0(Nil) → c
K tuples:none
Defined Rule Symbols:

equal0, number42, goal

Defined Pair Symbols:

EQUAL0, GOAL

Compound Symbols:

c1, c3, c

0.00/0.87
0.00/0.87

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0) → c3(EQUAL0(z0))
Removed 1 trailing nodes:

EQUAL0(Nil) → c
0.00/0.87
0.00/0.87

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

equal0(Nil) → number42(Nil) 0.00/0.87
equal0(Cons(z0, z1)) → equal0(Cons(z0, z1)) 0.00/0.87
number42(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) 0.00/0.87
goal(z0) → equal0(z0)
Tuples:

EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1)))
S tuples:

EQUAL0(Cons(z0, z1)) → c1(EQUAL0(Cons(z0, z1)))
K tuples:none
Defined Rule Symbols:

equal0, number42, goal

Defined Pair Symbols:

EQUAL0

Compound Symbols:

c1

0.00/0.87
0.00/0.87
0.00/0.94 EOF