YES(O(1), O(1)) 0.00/0.55 YES(O(1), O(1)) 0.00/0.56 0.00/0.56 0.00/0.56 0.00/0.56 0.00/0.56 0.00/0.56 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 0.00/0.56 0.00/0.56 0.00/0.56
0.00/0.56
0.00/0.56
0.00/0.56
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(1)).

0 CpxRelTRS
0.00/0.56 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
0.00/0.56 
↳2 CdtProblem
0.00/0.56 
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)
0.00/0.56 
↳4 CdtProblem
0.00/0.56 
↳5 SIsEmptyProof (BOTH BOUNDS(ID, ID))
0.00/0.56 
↳6 BOUNDS(O(1), O(1))
0.00/0.56
0.00/0.56 0.00/0.56
0.00/0.56
0.00/0.56

(0) Obligation:

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

loop(Cons(x, xs), Nil, pp, ss) → False 0.00/0.56
loop(Cons(x', xs'), Cons(x, xs), pp, ss) → loop[Ite][False][Ite][False][Ite](!EQ(x', x), Cons(x', xs'), Cons(x, xs), pp, ss) 0.00/0.56
loop(Nil, s, pp, ss) → True 0.00/0.56
match1(p, s) → loop(p, s, p, s)

The (relative) TRS S consists of the following rules:

!EQ(S(x), S(y)) → !EQ(x, y) 0.00/0.56
!EQ(0, S(y)) → False 0.00/0.56
!EQ(S(x), 0) → False 0.00/0.56
!EQ(0, 0) → True

Rewrite Strategy: INNERMOST
0.00/0.56
0.00/0.56

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.
0.00/0.56
0.00/0.56

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 0.00/0.56
!EQ(0, S(z0)) → False 0.00/0.56
!EQ(S(z0), 0) → False 0.00/0.56
!EQ(0, 0) → True 0.00/0.56
loop(Cons(z0, z1), Nil, z2, z3) → False 0.00/0.56
loop(Cons(z0, z1), Cons(z2, z3), z4, z5) → loop[Ite][False][Ite][False][Ite](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5) 0.00/0.56
loop(Nil, z0, z1, z2) → True 0.00/0.56
match1(z0, z1) → loop(z0, z1, z0, z1)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1)) 0.00/0.56
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(!EQ'(z0, z2)) 0.00/0.56
MATCH1(z0, z1) → c7(LOOP(z0, z1, z0, z1))
S tuples:

LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(!EQ'(z0, z2)) 0.00/0.56
MATCH1(z0, z1) → c7(LOOP(z0, z1, z0, z1))
K tuples:none
Defined Rule Symbols:

loop, match1, !EQ

Defined Pair Symbols:

!EQ', LOOP, MATCH1

Compound Symbols:

c, c5, c7

0.00/0.56
0.00/0.56

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 2 leading nodes:

MATCH1(z0, z1) → c7(LOOP(z0, z1, z0, z1)) 0.00/0.56
LOOP(Cons(z0, z1), Cons(z2, z3), z4, z5) → c5(!EQ'(z0, z2))
0.00/0.56
0.00/0.56

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

!EQ(S(z0), S(z1)) → !EQ(z0, z1) 0.00/0.56
!EQ(0, S(z0)) → False 0.00/0.56
!EQ(S(z0), 0) → False 0.00/0.56
!EQ(0, 0) → True 0.00/0.56
loop(Cons(z0, z1), Nil, z2, z3) → False 0.00/0.56
loop(Cons(z0, z1), Cons(z2, z3), z4, z5) → loop[Ite][False][Ite][False][Ite](!EQ(z0, z2), Cons(z0, z1), Cons(z2, z3), z4, z5) 0.00/0.56
loop(Nil, z0, z1, z2) → True 0.00/0.56
match1(z0, z1) → loop(z0, z1, z0, z1)
Tuples:

!EQ'(S(z0), S(z1)) → c(!EQ'(z0, z1))
S tuples:none
K tuples:none
Defined Rule Symbols:

loop, match1, !EQ

Defined Pair Symbols:

!EQ'

Compound Symbols:

c

0.00/0.56
0.00/0.56

(5) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty
0.00/0.56
0.00/0.56

(6) BOUNDS(O(1), O(1))

0.00/0.56
0.00/0.56
0.00/0.58 EOF