The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, EXP).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, EXP).


The TRS R consists of the following rules:

merge(nil, y) → y
merge(x, nil) → x
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) → y
++(.(x, y), z) → .(x, ++(y, z))
if(true, x, y) → x
if(false, x, y) → x

Rewrite Strategy: INNERMOST

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

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, EXP).


The TRS R consists of the following rules:

merge(nil, y) → y [1]
merge(x, nil) → x [1]
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))) [1]
++(nil, y) → y [1]
++(.(x, y), z) → .(x, ++(y, z)) [1]
if(true, x, y) → x [1]
if(false, x, y) → x [1]

Rewrite Strategy: INNERMOST

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

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

merge(nil, y) → y [1]
merge(x, nil) → x [1]
merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))) [1]
++(nil, y) → y [1]
++(.(x, y), z) → .(x, ++(y, z)) [1]
if(true, x, y) → x [1]
if(false, x, y) → x [1]

The TRS has the following type information:

merge :: nil:. → nil:. → nil:. nil :: nil:. . :: a → nil:. → nil:. if :: <:true:false → nil:. → nil:. → nil:. < :: a → a → <:true:false ++ :: nil:. → nil:. → nil:. true :: <:true:false false :: <:true:false

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

++

(c) The following functions are completely defined:

merge
if

Due to the following rules being added:

if(v0, v1, v2) → nil [0]

And the following fresh constants:

const

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: merge(nil, y) → y [1] merge(x, nil) → x [1] merge(.(x, y), .(u, v)) → if(<(x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v))) [1] ++(nil, y) → y [1] ++(.(x, y), z) → .(x, ++(y, z)) [1] if(true, x, y) → x [1] if(false, x, y) → x [1] if(v0, v1, v2) → nil [0] The TRS has the following type information: merge :: nil:. → nil:. → nil:. nil :: nil:. . :: a → nil:. → nil:. if :: <:true:false → nil:. → nil:. → nil:. < :: a → a → <:true:false ++ :: nil:. → nil:. → nil:. true :: <:true:false false :: <:true:false const :: a Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: merge(nil, y) → y [1] merge(x, nil) → x [1] merge(.(x, nil), .(u, nil)) → if(<(x, u), .(x, .(u, nil)), .(u, .(x, nil))) [3] merge(.(x, nil), .(u, .(u', v'))) → if(<(x, u), .(x, .(u, .(u', v'))), .(u, if(<(x, u'), .(x, merge(nil, .(u', v'))), .(u', merge(.(x, nil), v'))))) [3] merge(.(x, .(x', y')), .(u, nil)) → if(<(x, u), .(x, if(<(x', u), .(x', merge(y', .(u, nil))), .(u, merge(.(x', y'), nil)))), .(u, .(x, .(x', y')))) [3] merge(.(x, .(x', y')), .(u, .(u'', v''))) → if(<(x, u), .(x, if(<(x', u), .(x', merge(y', .(u, .(u'', v'')))), .(u, merge(.(x', y'), .(u'', v''))))), .(u, if(<(x, u''), .(x, merge(.(x', y'), .(u'', v''))), .(u'', merge(.(x, .(x', y')), v''))))) [3] ++(nil, y) → y [1] ++(.(x, y), z) → .(x, ++(y, z)) [1] if(true, x, y) → x [1] if(false, x, y) → x [1] if(v0, v1, v2) → nil [0] The TRS has the following type information: merge :: nil:. → nil:. → nil:. nil :: nil:. . :: a → nil:. → nil:. if :: <:true:false → nil:. → nil:. → nil:. < :: a → a → <:true:false ++ :: nil:. → nil:. → nil:. true :: <:true:false false :: <:true:false const :: a Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

nil => 0
true => 1
false => 0
const => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ y :|: z'' = y, y >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z) :|: z'' = z, z >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ x :|: z1 = y, x >= 0, y >= 0, z'' = x, z' = 1
if(z', z'', z1) -{ 1 }→ x :|: z1 = y, x >= 0, y >= 0, z'' = x, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: v0 >= 0, z1 = v2, v1 >= 0, z'' = v1, v2 >= 0, z' = v0
merge(z', z'') -{ 1 }→ x :|: z'' = 0, z' = x, x >= 0
merge(z', z'') -{ 1 }→ y :|: z'' = y, y >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + 0), 1 + u + merge(1 + x' + y', 0)), 1 + u + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), z'' = 1 + u + 0, x >= 0, x' >= 0, y' >= 0, u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + (1 + u + 0), 1 + u + (1 + x + 0)) :|: z'' = 1 + u + 0, x >= 0, z' = 1 + x + 0, u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + (1 + u + (1 + u' + v')), 1 + u + if(1 + x + u', 1 + x + merge(0, 1 + u' + v'), 1 + u' + merge(1 + x + 0, v'))) :|: x >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, z' = 1 + x + 0, u >= 0

(11) InliningProof (UPPER BOUND(ID) transformation)

Inlined the following terminating rules on right-hand sides where appropriate:

if(z', z'', z1) -{ 1 }→ x :|: z1 = y, x >= 0, y >= 0, z'' = x, z' = 1
if(z', z'', z1) -{ 1 }→ x :|: z1 = y, x >= 0, y >= 0, z'' = x, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: v0 >= 0, z1 = v2, v1 >= 0, z'' = v1, v2 >= 0, z' = v0

(12) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ y :|: z'' = y, y >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z) :|: z'' = z, z >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ x :|: z1 = y, x >= 0, y >= 0, z'' = x, z' = 1
if(z', z'', z1) -{ 1 }→ x :|: z1 = y, x >= 0, y >= 0, z'' = x, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: v0 >= 0, z1 = v2, v1 >= 0, z'' = v1, v2 >= 0, z' = v0
merge(z', z'') -{ 1 }→ x :|: z'' = 0, z' = x, x >= 0
merge(z', z'') -{ 4 }→ x' :|: z'' = 1 + u + 0, x >= 0, z' = 1 + x + 0, u >= 0, 1 + u + (1 + x + 0) = y, x' >= 0, y >= 0, 1 + x + (1 + u + 0) = x', 1 + x + u = 1
merge(z', z'') -{ 1 }→ y :|: z'' = y, y >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + 0), 1 + u + merge(1 + x' + y', 0)), 1 + u + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), z'' = 1 + u + 0, x >= 0, x' >= 0, y' >= 0, u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + (1 + u + (1 + u' + v')), 1 + u + if(1 + x + u', 1 + x + merge(0, 1 + u' + v'), 1 + u' + merge(1 + x + 0, v'))) :|: x >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, z' = 1 + x + 0, u >= 0
merge(z', z'') -{ 3 }→ 0 :|: z'' = 1 + u + 0, x >= 0, z' = 1 + x + 0, u >= 0, v0 >= 0, 1 + u + (1 + x + 0) = v2, v1 >= 0, 1 + x + (1 + u + 0) = v1, v2 >= 0, 1 + x + u = v0

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

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(14) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 1
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: z' >= 0, z'' >= 0, z1 >= 0
merge(z', z'') -{ 4 }→ x' :|: z' - 1 >= 0, z'' - 1 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = y, x' >= 0, y >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = x', 1 + (z' - 1) + (z'' - 1) = 1
merge(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
merge(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + (z'' - 1), 1 + x + if(1 + x' + (z'' - 1), 1 + x' + merge(y', 1 + (z'' - 1) + 0), 1 + (z'' - 1) + merge(1 + x' + y', 0)), 1 + (z'' - 1) + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, z'' - 1 >= 0
merge(z', z'') -{ 3 }→ if(1 + (z' - 1) + u, 1 + (z' - 1) + (1 + u + (1 + u' + v')), 1 + u + if(1 + (z' - 1) + u', 1 + (z' - 1) + merge(0, 1 + u' + v'), 1 + u' + merge(1 + (z' - 1) + 0, v'))) :|: z' - 1 >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, u >= 0
merge(z', z'') -{ 3 }→ 0 :|: z' - 1 >= 0, z'' - 1 >= 0, v0 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = v2, v1 >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = v1, v2 >= 0, 1 + (z' - 1) + (z'' - 1) = v0

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

Found the following analysis order by SCC decomposition:

{ if } { ++ } { merge }

(16) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 1
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: z' >= 0, z'' >= 0, z1 >= 0
merge(z', z'') -{ 4 }→ x' :|: z' - 1 >= 0, z'' - 1 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = y, x' >= 0, y >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = x', 1 + (z' - 1) + (z'' - 1) = 1
merge(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
merge(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + (z'' - 1), 1 + x + if(1 + x' + (z'' - 1), 1 + x' + merge(y', 1 + (z'' - 1) + 0), 1 + (z'' - 1) + merge(1 + x' + y', 0)), 1 + (z'' - 1) + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, z'' - 1 >= 0
merge(z', z'') -{ 3 }→ if(1 + (z' - 1) + u, 1 + (z' - 1) + (1 + u + (1 + u' + v')), 1 + u + if(1 + (z' - 1) + u', 1 + (z' - 1) + merge(0, 1 + u' + v'), 1 + u' + merge(1 + (z' - 1) + 0, v'))) :|: z' - 1 >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, u >= 0
merge(z', z'') -{ 3 }→ 0 :|: z' - 1 >= 0, z'' - 1 >= 0, v0 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = v2, v1 >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = v1, v2 >= 0, 1 + (z' - 1) + (z'' - 1) = v0

Function symbols to be analyzed: {if}, {++}, {merge}

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: if
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z''

(18) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 1
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: z' >= 0, z'' >= 0, z1 >= 0
merge(z', z'') -{ 4 }→ x' :|: z' - 1 >= 0, z'' - 1 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = y, x' >= 0, y >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = x', 1 + (z' - 1) + (z'' - 1) = 1
merge(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
merge(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + (z'' - 1), 1 + x + if(1 + x' + (z'' - 1), 1 + x' + merge(y', 1 + (z'' - 1) + 0), 1 + (z'' - 1) + merge(1 + x' + y', 0)), 1 + (z'' - 1) + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, z'' - 1 >= 0
merge(z', z'') -{ 3 }→ if(1 + (z' - 1) + u, 1 + (z' - 1) + (1 + u + (1 + u' + v')), 1 + u + if(1 + (z' - 1) + u', 1 + (z' - 1) + merge(0, 1 + u' + v'), 1 + u' + merge(1 + (z' - 1) + 0, v'))) :|: z' - 1 >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, u >= 0
merge(z', z'') -{ 3 }→ 0 :|: z' - 1 >= 0, z'' - 1 >= 0, v0 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = v2, v1 >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = v1, v2 >= 0, 1 + (z' - 1) + (z'' - 1) = v0

Function symbols to be analyzed: {if}, {++}, {merge}
Previous analysis results are:

if: runtime: ?, size: O(n1) [z'']

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: if
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(20) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 1
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: z' >= 0, z'' >= 0, z1 >= 0
merge(z', z'') -{ 4 }→ x' :|: z' - 1 >= 0, z'' - 1 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = y, x' >= 0, y >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = x', 1 + (z' - 1) + (z'' - 1) = 1
merge(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
merge(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + (z'' - 1), 1 + x + if(1 + x' + (z'' - 1), 1 + x' + merge(y', 1 + (z'' - 1) + 0), 1 + (z'' - 1) + merge(1 + x' + y', 0)), 1 + (z'' - 1) + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, z'' - 1 >= 0
merge(z', z'') -{ 3 }→ if(1 + (z' - 1) + u, 1 + (z' - 1) + (1 + u + (1 + u' + v')), 1 + u + if(1 + (z' - 1) + u', 1 + (z' - 1) + merge(0, 1 + u' + v'), 1 + u' + merge(1 + (z' - 1) + 0, v'))) :|: z' - 1 >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, u >= 0
merge(z', z'') -{ 3 }→ 0 :|: z' - 1 >= 0, z'' - 1 >= 0, v0 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = v2, v1 >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = v1, v2 >= 0, 1 + (z' - 1) + (z'' - 1) = v0

Function symbols to be analyzed: {++}, {merge}
Previous analysis results are:

if: runtime: O(1) [1], size: O(n1) [z'']

(21) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(22) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 1
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: z' >= 0, z'' >= 0, z1 >= 0
merge(z', z'') -{ 4 }→ x' :|: z' - 1 >= 0, z'' - 1 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = y, x' >= 0, y >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = x', 1 + (z' - 1) + (z'' - 1) = 1
merge(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
merge(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + (z'' - 1), 1 + x + if(1 + x' + (z'' - 1), 1 + x' + merge(y', 1 + (z'' - 1) + 0), 1 + (z'' - 1) + merge(1 + x' + y', 0)), 1 + (z'' - 1) + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, z'' - 1 >= 0
merge(z', z'') -{ 3 }→ if(1 + (z' - 1) + u, 1 + (z' - 1) + (1 + u + (1 + u' + v')), 1 + u + if(1 + (z' - 1) + u', 1 + (z' - 1) + merge(0, 1 + u' + v'), 1 + u' + merge(1 + (z' - 1) + 0, v'))) :|: z' - 1 >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, u >= 0
merge(z', z'') -{ 3 }→ 0 :|: z' - 1 >= 0, z'' - 1 >= 0, v0 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = v2, v1 >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = v1, v2 >= 0, 1 + (z' - 1) + (z'' - 1) = v0

Function symbols to be analyzed: {++}, {merge}
Previous analysis results are:

if: runtime: O(1) [1], size: O(n1) [z'']

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: ++
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z' + z''

(24) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 1
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: z' >= 0, z'' >= 0, z1 >= 0
merge(z', z'') -{ 4 }→ x' :|: z' - 1 >= 0, z'' - 1 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = y, x' >= 0, y >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = x', 1 + (z' - 1) + (z'' - 1) = 1
merge(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
merge(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + (z'' - 1), 1 + x + if(1 + x' + (z'' - 1), 1 + x' + merge(y', 1 + (z'' - 1) + 0), 1 + (z'' - 1) + merge(1 + x' + y', 0)), 1 + (z'' - 1) + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, z'' - 1 >= 0
merge(z', z'') -{ 3 }→ if(1 + (z' - 1) + u, 1 + (z' - 1) + (1 + u + (1 + u' + v')), 1 + u + if(1 + (z' - 1) + u', 1 + (z' - 1) + merge(0, 1 + u' + v'), 1 + u' + merge(1 + (z' - 1) + 0, v'))) :|: z' - 1 >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, u >= 0
merge(z', z'') -{ 3 }→ 0 :|: z' - 1 >= 0, z'' - 1 >= 0, v0 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = v2, v1 >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = v1, v2 >= 0, 1 + (z' - 1) + (z'' - 1) = v0

Function symbols to be analyzed: {++}, {merge}
Previous analysis results are:

if: runtime: O(1) [1], size: O(n1) [z''] ++: runtime: ?, size: O(n1) [z' + z'']

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: ++
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z'

(26) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 1 }→ 1 + x + ++(y, z'') :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 1
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: z' >= 0, z'' >= 0, z1 >= 0
merge(z', z'') -{ 4 }→ x' :|: z' - 1 >= 0, z'' - 1 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = y, x' >= 0, y >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = x', 1 + (z' - 1) + (z'' - 1) = 1
merge(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
merge(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + (z'' - 1), 1 + x + if(1 + x' + (z'' - 1), 1 + x' + merge(y', 1 + (z'' - 1) + 0), 1 + (z'' - 1) + merge(1 + x' + y', 0)), 1 + (z'' - 1) + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, z'' - 1 >= 0
merge(z', z'') -{ 3 }→ if(1 + (z' - 1) + u, 1 + (z' - 1) + (1 + u + (1 + u' + v')), 1 + u + if(1 + (z' - 1) + u', 1 + (z' - 1) + merge(0, 1 + u' + v'), 1 + u' + merge(1 + (z' - 1) + 0, v'))) :|: z' - 1 >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, u >= 0
merge(z', z'') -{ 3 }→ 0 :|: z' - 1 >= 0, z'' - 1 >= 0, v0 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = v2, v1 >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = v1, v2 >= 0, 1 + (z' - 1) + (z'' - 1) = v0

Function symbols to be analyzed: {merge}
Previous analysis results are:

if: runtime: O(1) [1], size: O(n1) [z''] ++: runtime: O(n1) [1 + z'], size: O(n1) [z' + z'']

(27) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(28) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 2 + y }→ 1 + x + s :|: s >= 0, s <= 1 * y + 1 * z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 1
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: z' >= 0, z'' >= 0, z1 >= 0
merge(z', z'') -{ 4 }→ x' :|: z' - 1 >= 0, z'' - 1 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = y, x' >= 0, y >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = x', 1 + (z' - 1) + (z'' - 1) = 1
merge(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
merge(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + (z'' - 1), 1 + x + if(1 + x' + (z'' - 1), 1 + x' + merge(y', 1 + (z'' - 1) + 0), 1 + (z'' - 1) + merge(1 + x' + y', 0)), 1 + (z'' - 1) + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, z'' - 1 >= 0
merge(z', z'') -{ 3 }→ if(1 + (z' - 1) + u, 1 + (z' - 1) + (1 + u + (1 + u' + v')), 1 + u + if(1 + (z' - 1) + u', 1 + (z' - 1) + merge(0, 1 + u' + v'), 1 + u' + merge(1 + (z' - 1) + 0, v'))) :|: z' - 1 >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, u >= 0
merge(z', z'') -{ 3 }→ 0 :|: z' - 1 >= 0, z'' - 1 >= 0, v0 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = v2, v1 >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = v1, v2 >= 0, 1 + (z' - 1) + (z'' - 1) = v0

Function symbols to be analyzed: {merge}
Previous analysis results are:

if: runtime: O(1) [1], size: O(n1) [z''] ++: runtime: O(n1) [1 + z'], size: O(n1) [z' + z'']

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: merge
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z' + z''

(30) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 2 + y }→ 1 + x + s :|: s >= 0, s <= 1 * y + 1 * z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 1
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: z' >= 0, z'' >= 0, z1 >= 0
merge(z', z'') -{ 4 }→ x' :|: z' - 1 >= 0, z'' - 1 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = y, x' >= 0, y >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = x', 1 + (z' - 1) + (z'' - 1) = 1
merge(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
merge(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + (z'' - 1), 1 + x + if(1 + x' + (z'' - 1), 1 + x' + merge(y', 1 + (z'' - 1) + 0), 1 + (z'' - 1) + merge(1 + x' + y', 0)), 1 + (z'' - 1) + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, z'' - 1 >= 0
merge(z', z'') -{ 3 }→ if(1 + (z' - 1) + u, 1 + (z' - 1) + (1 + u + (1 + u' + v')), 1 + u + if(1 + (z' - 1) + u', 1 + (z' - 1) + merge(0, 1 + u' + v'), 1 + u' + merge(1 + (z' - 1) + 0, v'))) :|: z' - 1 >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, u >= 0
merge(z', z'') -{ 3 }→ 0 :|: z' - 1 >= 0, z'' - 1 >= 0, v0 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = v2, v1 >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = v1, v2 >= 0, 1 + (z' - 1) + (z'' - 1) = v0

Function symbols to be analyzed: {merge}
Previous analysis results are:

if: runtime: O(1) [1], size: O(n1) [z''] ++: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] merge: runtime: ?, size: O(n1) [z' + z'']

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: merge
after applying outer abstraction to obtain an ITS,
resulting in: EXP with polynomial bound: ?

(32) Obligation:

Complexity RNTS consisting of the following rules:

++(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
++(z', z'') -{ 2 + y }→ 1 + x + s :|: s >= 0, s <= 1 * y + 1 * z'', z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 1
if(z', z'', z1) -{ 1 }→ z'' :|: z'' >= 0, z1 >= 0, z' = 0
if(z', z'', z1) -{ 0 }→ 0 :|: z' >= 0, z'' >= 0, z1 >= 0
merge(z', z'') -{ 4 }→ x' :|: z' - 1 >= 0, z'' - 1 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = y, x' >= 0, y >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = x', 1 + (z' - 1) + (z'' - 1) = 1
merge(z', z'') -{ 1 }→ z' :|: z'' = 0, z' >= 0
merge(z', z'') -{ 1 }→ z'' :|: z'' >= 0, z' = 0
merge(z', z'') -{ 3 }→ if(1 + x + u, 1 + x + if(1 + x' + u, 1 + x' + merge(y', 1 + u + (1 + u'' + v'')), 1 + u + merge(1 + x' + y', 1 + u'' + v'')), 1 + u + if(1 + x + u'', 1 + x + merge(1 + x' + y', 1 + u'' + v''), 1 + u'' + merge(1 + x + (1 + x' + y'), v''))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, u'' >= 0, v'' >= 0, z'' = 1 + u + (1 + u'' + v''), u >= 0
merge(z', z'') -{ 3 }→ if(1 + x + (z'' - 1), 1 + x + if(1 + x' + (z'' - 1), 1 + x' + merge(y', 1 + (z'' - 1) + 0), 1 + (z'' - 1) + merge(1 + x' + y', 0)), 1 + (z'' - 1) + (1 + x + (1 + x' + y'))) :|: z' = 1 + x + (1 + x' + y'), x >= 0, x' >= 0, y' >= 0, z'' - 1 >= 0
merge(z', z'') -{ 3 }→ if(1 + (z' - 1) + u, 1 + (z' - 1) + (1 + u + (1 + u' + v')), 1 + u + if(1 + (z' - 1) + u', 1 + (z' - 1) + merge(0, 1 + u' + v'), 1 + u' + merge(1 + (z' - 1) + 0, v'))) :|: z' - 1 >= 0, z'' = 1 + u + (1 + u' + v'), u' >= 0, v' >= 0, u >= 0
merge(z', z'') -{ 3 }→ 0 :|: z' - 1 >= 0, z'' - 1 >= 0, v0 >= 0, 1 + (z'' - 1) + (1 + (z' - 1) + 0) = v2, v1 >= 0, 1 + (z' - 1) + (1 + (z'' - 1) + 0) = v1, v2 >= 0, 1 + (z' - 1) + (z'' - 1) = v0

Function symbols to be analyzed:
Previous analysis results are:

if: runtime: O(1) [1], size: O(n1) [z''] ++: runtime: O(n1) [1 + z'], size: O(n1) [z' + z''] merge: runtime: EXP, size: O(n1) [z' + z'']

(33) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(34) BOUNDS(1, EXP)