MAYBE
proof of input_I6JXLOwTnT.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 338 ms]
(2) CpxRelTRS
(3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(4) CpxRelTRS
(5) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(6) CpxTRS
(7) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms]
(8) CpxWeightedTrs
    (9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxTypedWeightedTrs
    (11) CompletionProof [UPPER BOUND(ID), 0 ms]
    (12) CpxTypedWeightedCompleteTrs
        (13) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
        (14) CpxTypedWeightedCompleteTrs
        (15) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (16) CpxRNTS
        (17) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
        (18) CpxRNTS
    (19) CompletionProof [UPPER BOUND(ID), 0 ms]
    (20) CpxTypedWeightedCompleteTrs
        (21) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
        (22) CpxRNTS
(23) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(24) CdtProblem
    (25) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (26) CdtProblem
    (27) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (28) CdtProblem
    (29) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (30) CdtProblem
    (31) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (32) CdtProblem
    (33) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (34) CdtProblem
    (35) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (36) CdtProblem
    (37) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (38) CdtProblem


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n))
   rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x))
   rewrite(Val(n)) -> Val(n)
   second(Op(x, y)) -> y
   isOp(Val(n)) -> False
   isOp(Op(x, y)) -> True
   first(Val(n)) -> Val(n)
   first(Op(x, y)) -> x
   assrewrite(exp) -> rewrite(exp)

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

   rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y))
   rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y))
   rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1))))

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n))
   rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x))
   rewrite(Val(n)) -> Val(n)
   second(Op(x, y)) -> y
   isOp(Val(n)) -> False
   isOp(Op(x, y)) -> True
   first(Val(n)) -> Val(n)
   first(Op(x, y)) -> x
   assrewrite(exp) -> rewrite(exp)

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

   rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y))
   rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y))
   rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1))))

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(3) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(4)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n))
   rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x))
   rewrite(Val(n)) -> Val(n)
   second(Op(x, y)) -> y
   isOp(Val(n)) -> False
   isOp(Op(x, y)) -> True
   first(Val(n)) -> Val(n)
   first(Op(x, y)) -> x
   assrewrite(exp) -> rewrite(exp)

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

   rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y))
   rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y))
   rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1))))

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(5) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

(6)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n))
   rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x))
   rewrite(Val(n)) -> Val(n)
   second(Op(x, y)) -> y
   isOp(Val(n)) -> False
   isOp(Op(x, y)) -> True
   first(Val(n)) -> Val(n)
   first(Op(x, y)) -> x
   assrewrite(exp) -> rewrite(exp)
   rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y))
   rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y))
   rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1))))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(7) RelTrsToWeightedTrsProof (UPPER BOUND(ID))
Transformed relative TRS to weighted TRS
----------------------------------------

(8)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) [1]
   rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) [1]
   rewrite(Val(n)) -> Val(n) [1]
   second(Op(x, y)) -> y [1]
   isOp(Val(n)) -> False [1]
   isOp(Op(x, y)) -> True [1]
   first(Val(n)) -> Val(n) [1]
   first(Op(x, y)) -> x [1]
   assrewrite(exp) -> rewrite(exp) [1]
   rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) [0]
   rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) [0]
   rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) [0]

Rewrite Strategy: INNERMOST
----------------------------------------

(9) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(10)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) [1]
   rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) [1]
   rewrite(Val(n)) -> Val(n) [1]
   second(Op(x, y)) -> y [1]
   isOp(Val(n)) -> False [1]
   isOp(Op(x, y)) -> True [1]
   first(Val(n)) -> Val(n) [1]
   first(Op(x, y)) -> x [1]
   assrewrite(exp) -> rewrite(exp) [1]
   rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) [0]
   rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) [0]
   rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) [0]

The TRS has the following type information:
rewrite :: Val:Op -> Val:Op
Op :: Val:Op -> Val:Op -> Val:Op
Val :: a -> Val:Op
rewrite[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op
second :: Val:Op -> Val:Op
isOp :: Val:Op -> False:True
False :: False:True
True :: False:True
first :: Val:Op -> Val:Op
assrewrite :: Val:Op -> Val:Op
rewrite[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rewrite[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op

Rewrite Strategy: INNERMOST
----------------------------------------

(11) CompletionProof (UPPER BOUND(ID))
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:

   second_1
   isOp_1
   first_1
   assrewrite_1

(c) The following functions are completely defined:

   rewrite_1
   rewrite[Let]_3
   rewrite[Let][Let]_4
   rewrite[Let][Let][Let]_4

Due to the following rules being added:

   rewrite[Let](v0, v1, v2) -> const [0]
   rewrite[Let][Let](v0, v1, v2, v3) -> const [0]
   rewrite[Let][Let][Let](v0, v1, v2, v3) -> const [0]
   rewrite(v0) -> const [0]

And the following fresh constants:    const, const1

----------------------------------------

(12)
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:

   rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) [1]
   rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) [1]
   rewrite(Val(n)) -> Val(n) [1]
   second(Op(x, y)) -> y [1]
   isOp(Val(n)) -> False [1]
   isOp(Op(x, y)) -> True [1]
   first(Val(n)) -> Val(n) [1]
   first(Op(x, y)) -> x [1]
   assrewrite(exp) -> rewrite(exp) [1]
   rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) [0]
   rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) [0]
   rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) [0]
   rewrite[Let](v0, v1, v2) -> const [0]
   rewrite[Let][Let](v0, v1, v2, v3) -> const [0]
   rewrite[Let][Let][Let](v0, v1, v2, v3) -> const [0]
   rewrite(v0) -> const [0]

The TRS has the following type information:
rewrite :: Val:Op:const -> Val:Op:const
Op :: Val:Op:const -> Val:Op:const -> Val:Op:const
Val :: a -> Val:Op:const
rewrite[Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const
second :: Val:Op:const -> Val:Op:const
isOp :: Val:Op:const -> False:True
False :: False:True
True :: False:True
first :: Val:Op:const -> Val:Op:const
assrewrite :: Val:Op:const -> Val:Op:const
rewrite[Let][Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const
rewrite[Let][Let][Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const
const :: Val:Op:const
const1 :: a

Rewrite Strategy: INNERMOST
----------------------------------------

(13) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

(14)
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:

   rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) [1]
   rewrite(Op(Op(Op(Val(n'), y''), y), y')) -> rewrite[Let](Op(Op(Op(Val(n'), y''), y), y'), Op(Op(Val(n'), y''), y), Op(rewrite(y''), Val(n'))) [2]
   rewrite(Op(Op(Op(Op(x', y1), y'''), y), y')) -> rewrite[Let](Op(Op(Op(Op(x', y1), y'''), y), y'), Op(Op(Op(x', y1), y'''), y), rewrite[Let](Op(Op(x', y1), y'''), Op(x', y1), rewrite(x'))) [2]
   rewrite(Op(Op(Val(n''), y), y')) -> rewrite[Let](Op(Op(Val(n''), y), y'), Op(Val(n''), y), Val(n'')) [2]
   rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), const) [1]
   rewrite(Val(n)) -> Val(n) [1]
   second(Op(x, y)) -> y [1]
   isOp(Val(n)) -> False [1]
   isOp(Op(x, y)) -> True [1]
   first(Val(n)) -> Val(n) [1]
   first(Op(x, y)) -> x [1]
   assrewrite(exp) -> rewrite(exp) [1]
   rewrite[Let](exp, Op(x, Op(Val(n1), y2)), a1) -> rewrite[Let][Let](exp, Op(x, Op(Val(n1), y2)), a1, Op(rewrite(y2), Val(n1))) [1]
   rewrite[Let](exp, Op(x, Op(Op(x'', y3), y'1)), a1) -> rewrite[Let][Let](exp, Op(x, Op(Op(x'', y3), y'1)), a1, rewrite[Let](Op(Op(x'', y3), y'1), Op(x'', y3), rewrite(x''))) [1]
   rewrite[Let](exp, Op(x, Val(n2)), a1) -> rewrite[Let][Let](exp, Op(x, Val(n2)), a1, Val(n2)) [1]
   rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, const) [0]
   rewrite[Let][Let](Op(x, Op(Val(n3), y4)), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, Op(Val(n3), y4)), a1, b1, Op(rewrite(y4), Val(n3))) [1]
   rewrite[Let][Let](Op(x, Op(Op(x1, y5), y'2)), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, Op(Op(x1, y5), y'2)), a1, b1, rewrite[Let](Op(Op(x1, y5), y'2), Op(x1, y5), rewrite(x1))) [1]
   rewrite[Let][Let](Op(x, Val(n4)), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, Val(n4)), a1, b1, Val(n4)) [1]
   rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, const) [0]
   rewrite[Let][Let][Let](exp, a1, b1, Op(Val(n5), y6)) -> rewrite(Op(a1, Op(b1, Op(rewrite(y6), Val(n5))))) [1]
   rewrite[Let][Let][Let](exp, a1, b1, Op(Op(x2, y7), y'3)) -> rewrite(Op(a1, Op(b1, rewrite[Let](Op(Op(x2, y7), y'3), Op(x2, y7), rewrite(x2))))) [1]
   rewrite[Let][Let][Let](exp, a1, b1, Val(n6)) -> rewrite(Op(a1, Op(b1, Val(n6)))) [1]
   rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, const))) [0]
   rewrite[Let](v0, v1, v2) -> const [0]
   rewrite[Let][Let](v0, v1, v2, v3) -> const [0]
   rewrite[Let][Let][Let](v0, v1, v2, v3) -> const [0]
   rewrite(v0) -> const [0]

The TRS has the following type information:
rewrite :: Val:Op:const -> Val:Op:const
Op :: Val:Op:const -> Val:Op:const -> Val:Op:const
Val :: a -> Val:Op:const
rewrite[Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const
second :: Val:Op:const -> Val:Op:const
isOp :: Val:Op:const -> False:True
False :: False:True
True :: False:True
first :: Val:Op:const -> Val:Op:const
assrewrite :: Val:Op:const -> Val:Op:const
rewrite[Let][Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const
rewrite[Let][Let][Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const
const :: Val:Op:const
const1 :: a

Rewrite Strategy: INNERMOST
----------------------------------------

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

   False => 0
   True => 1
   const => 0
   const1 => 0

----------------------------------------

(16)
Obligation:
Complexity RNTS consisting of the following rules:

   assrewrite(z) -{ 1 }-> rewrite(exp) :|: z = exp, exp >= 0
   first(z) -{ 1 }-> x :|: z = 1 + x + y, x >= 0, y >= 0
   first(z) -{ 1 }-> 1 + n :|: n >= 0, z = 1 + n
   isOp(z) -{ 1 }-> 1 :|: z = 1 + x + y, x >= 0, y >= 0
   isOp(z) -{ 1 }-> 0 :|: n >= 0, z = 1 + n
   rewrite(z) -{ 1 }-> rewrite[Let](1 + (1 + x + y) + y', 1 + x + y, 0) :|: x >= 0, y >= 0, y' >= 0, z = 1 + (1 + x + y) + y'
   rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + n'') + y) + y', 1 + (1 + n'') + y, 1 + n'') :|: y >= 0, n'' >= 0, y' >= 0, z = 1 + (1 + (1 + n'') + y) + y'
   rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + (1 + n') + y'') + y) + y', 1 + (1 + (1 + n') + y'') + y, 1 + rewrite(y'') + (1 + n')) :|: y >= 0, n' >= 0, y'' >= 0, y' >= 0, z = 1 + (1 + (1 + (1 + n') + y'') + y) + y'
   rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + (1 + x' + y1) + y''') + y) + y', 1 + (1 + (1 + x' + y1) + y''') + y, rewrite[Let](1 + (1 + x' + y1) + y''', 1 + x' + y1, rewrite(x'))) :|: y1 >= 0, x' >= 0, y >= 0, y' >= 0, z = 1 + (1 + (1 + (1 + x' + y1) + y''') + y) + y', y''' >= 0
   rewrite(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   rewrite(z) -{ 1 }-> 1 + n :|: n >= 0, z = 1 + n
   rewrite(z) -{ 1 }-> 1 + rewrite(y) + (1 + n) :|: n >= 0, y >= 0, z = 1 + (1 + n) + y
   rewrite[Let](z, z', z'') -{ 0 }-> rewrite[Let][Let](exp, 1 + x + y, a1, 0) :|: a1 >= 0, z' = 1 + x + y, x >= 0, y >= 0, z = exp, z'' = a1, exp >= 0
   rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](exp, 1 + x + (1 + n2), a1, 1 + n2) :|: a1 >= 0, x >= 0, z = exp, n2 >= 0, z' = 1 + x + (1 + n2), z'' = a1, exp >= 0
   rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](exp, 1 + x + (1 + (1 + n1) + y2), a1, 1 + rewrite(y2) + (1 + n1)) :|: a1 >= 0, x >= 0, z = exp, z' = 1 + x + (1 + (1 + n1) + y2), n1 >= 0, y2 >= 0, z'' = a1, exp >= 0
   rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](exp, 1 + x + (1 + (1 + x'' + y3) + y'1), a1, rewrite[Let](1 + (1 + x'' + y3) + y'1, 1 + x'' + y3, rewrite(x''))) :|: a1 >= 0, x >= 0, z = exp, y'1 >= 0, y3 >= 0, z' = 1 + x + (1 + (1 + x'' + y3) + y'1), x'' >= 0, z'' = a1, exp >= 0
   rewrite[Let](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> rewrite[Let][Let][Let](1 + x + y, a1, b1, 0) :|: a1 >= 0, z = 1 + x + y, z1 = b1, b1 >= 0, opab >= 0, x >= 0, y >= 0, z' = opab, z'' = a1
   rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + n4), a1, b1, 1 + n4) :|: z = 1 + x + (1 + n4), n4 >= 0, a1 >= 0, z1 = b1, b1 >= 0, opab >= 0, x >= 0, z' = opab, z'' = a1
   rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + (1 + n3) + y4), a1, b1, 1 + rewrite(y4) + (1 + n3)) :|: a1 >= 0, z1 = b1, b1 >= 0, opab >= 0, x >= 0, z' = opab, y4 >= 0, z'' = a1, z = 1 + x + (1 + (1 + n3) + y4), n3 >= 0
   rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + (1 + x1 + y5) + y'2), a1, b1, rewrite[Let](1 + (1 + x1 + y5) + y'2, 1 + x1 + y5, rewrite(x1))) :|: y5 >= 0, x1 >= 0, a1 >= 0, z1 = b1, b1 >= 0, y'2 >= 0, opab >= 0, x >= 0, z' = opab, z'' = a1, z = 1 + x + (1 + (1 + x1 + y5) + y'2)
   rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + a1 + (1 + b1 + rewrite[Let](1 + (1 + x2 + y7) + y'3, 1 + x2 + y7, rewrite(x2)))) :|: a1 >= 0, b1 >= 0, z = exp, y7 >= 0, y'3 >= 0, z'' = b1, z' = a1, z1 = 1 + (1 + x2 + y7) + y'3, exp >= 0, x2 >= 0
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> rewrite(1 + a1 + (1 + b1 + 0)) :|: a1 >= 0, b1 >= 0, z1 = c1, z = exp, c1 >= 0, z'' = b1, z' = a1, exp >= 0
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + a1 + (1 + b1 + (1 + n6))) :|: a1 >= 0, b1 >= 0, n6 >= 0, z = exp, z'' = b1, z' = a1, exp >= 0, z1 = 1 + n6
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + a1 + (1 + b1 + (1 + rewrite(y6) + (1 + n5)))) :|: a1 >= 0, b1 >= 0, z = exp, y6 >= 0, n5 >= 0, z'' = b1, z1 = 1 + (1 + n5) + y6, z' = a1, exp >= 0
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   second(z) -{ 1 }-> y :|: z = 1 + x + y, x >= 0, y >= 0


----------------------------------------

(17) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

(18)
Obligation:
Complexity RNTS consisting of the following rules:

   assrewrite(z) -{ 1 }-> rewrite(z) :|: z >= 0
   first(z) -{ 1 }-> x :|: z = 1 + x + y, x >= 0, y >= 0
   first(z) -{ 1 }-> 1 + (z - 1) :|: z - 1 >= 0
   isOp(z) -{ 1 }-> 1 :|: z = 1 + x + y, x >= 0, y >= 0
   isOp(z) -{ 1 }-> 0 :|: z - 1 >= 0
   rewrite(z) -{ 1 }-> rewrite[Let](1 + (1 + x + y) + y', 1 + x + y, 0) :|: x >= 0, y >= 0, y' >= 0, z = 1 + (1 + x + y) + y'
   rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + n'') + y) + y', 1 + (1 + n'') + y, 1 + n'') :|: y >= 0, n'' >= 0, y' >= 0, z = 1 + (1 + (1 + n'') + y) + y'
   rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + (1 + n') + y'') + y) + y', 1 + (1 + (1 + n') + y'') + y, 1 + rewrite(y'') + (1 + n')) :|: y >= 0, n' >= 0, y'' >= 0, y' >= 0, z = 1 + (1 + (1 + (1 + n') + y'') + y) + y'
   rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + (1 + x' + y1) + y''') + y) + y', 1 + (1 + (1 + x' + y1) + y''') + y, rewrite[Let](1 + (1 + x' + y1) + y''', 1 + x' + y1, rewrite(x'))) :|: y1 >= 0, x' >= 0, y >= 0, y' >= 0, z = 1 + (1 + (1 + (1 + x' + y1) + y''') + y) + y', y''' >= 0
   rewrite(z) -{ 0 }-> 0 :|: z >= 0
   rewrite(z) -{ 1 }-> 1 + (z - 1) :|: z - 1 >= 0
   rewrite(z) -{ 1 }-> 1 + rewrite(y) + (1 + n) :|: n >= 0, y >= 0, z = 1 + (1 + n) + y
   rewrite[Let](z, z', z'') -{ 0 }-> rewrite[Let][Let](z, 1 + x + y, z'', 0) :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0, z >= 0
   rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](z, 1 + x + (1 + n2), z'', 1 + n2) :|: z'' >= 0, x >= 0, n2 >= 0, z' = 1 + x + (1 + n2), z >= 0
   rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](z, 1 + x + (1 + (1 + n1) + y2), z'', 1 + rewrite(y2) + (1 + n1)) :|: z'' >= 0, x >= 0, z' = 1 + x + (1 + (1 + n1) + y2), n1 >= 0, y2 >= 0, z >= 0
   rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](z, 1 + x + (1 + (1 + x'' + y3) + y'1), z'', rewrite[Let](1 + (1 + x'' + y3) + y'1, 1 + x'' + y3, rewrite(x''))) :|: z'' >= 0, x >= 0, y'1 >= 0, y3 >= 0, z' = 1 + x + (1 + (1 + x'' + y3) + y'1), x'' >= 0, z >= 0
   rewrite[Let](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> rewrite[Let][Let][Let](1 + x + y, z'', z1, 0) :|: z'' >= 0, z = 1 + x + y, z1 >= 0, z' >= 0, x >= 0, y >= 0
   rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + n4), z'', z1, 1 + n4) :|: z = 1 + x + (1 + n4), n4 >= 0, z'' >= 0, z1 >= 0, z' >= 0, x >= 0
   rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + (1 + n3) + y4), z'', z1, 1 + rewrite(y4) + (1 + n3)) :|: z'' >= 0, z1 >= 0, z' >= 0, x >= 0, y4 >= 0, z = 1 + x + (1 + (1 + n3) + y4), n3 >= 0
   rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + (1 + x1 + y5) + y'2), z'', z1, rewrite[Let](1 + (1 + x1 + y5) + y'2, 1 + x1 + y5, rewrite(x1))) :|: y5 >= 0, x1 >= 0, z'' >= 0, z1 >= 0, y'2 >= 0, z' >= 0, x >= 0, z = 1 + x + (1 + (1 + x1 + y5) + y'2)
   rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + z' + (1 + z'' + rewrite[Let](1 + (1 + x2 + y7) + y'3, 1 + x2 + y7, rewrite(x2)))) :|: z' >= 0, z'' >= 0, y7 >= 0, y'3 >= 0, z1 = 1 + (1 + x2 + y7) + y'3, z >= 0, x2 >= 0
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> rewrite(1 + z' + (1 + z'' + 0)) :|: z' >= 0, z'' >= 0, z1 >= 0, z >= 0
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + z' + (1 + z'' + (1 + (z1 - 1)))) :|: z' >= 0, z'' >= 0, z1 - 1 >= 0, z >= 0
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + z' + (1 + z'' + (1 + rewrite(y6) + (1 + n5)))) :|: z' >= 0, z'' >= 0, y6 >= 0, n5 >= 0, z1 = 1 + (1 + n5) + y6, z >= 0
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
   second(z) -{ 1 }-> y :|: z = 1 + x + y, x >= 0, y >= 0


----------------------------------------

(19) CompletionProof (UPPER BOUND(ID))
The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

   rewrite[Let](v0, v1, v2) -> null_rewrite[Let] [0]
   rewrite[Let][Let](v0, v1, v2, v3) -> null_rewrite[Let][Let] [0]
   rewrite[Let][Let][Let](v0, v1, v2, v3) -> null_rewrite[Let][Let][Let] [0]
   rewrite(v0) -> null_rewrite [0]
   second(v0) -> null_second [0]
   isOp(v0) -> null_isOp [0]
   first(v0) -> null_first [0]

And the following fresh constants:    null_rewrite[Let], null_rewrite[Let][Let], null_rewrite[Let][Let][Let], null_rewrite, null_second, null_isOp, null_first, const

----------------------------------------

(20)
Obligation:
Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

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

   rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) [1]
   rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) [1]
   rewrite(Val(n)) -> Val(n) [1]
   second(Op(x, y)) -> y [1]
   isOp(Val(n)) -> False [1]
   isOp(Op(x, y)) -> True [1]
   first(Val(n)) -> Val(n) [1]
   first(Op(x, y)) -> x [1]
   assrewrite(exp) -> rewrite(exp) [1]
   rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) [0]
   rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) [0]
   rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) [0]
   rewrite[Let](v0, v1, v2) -> null_rewrite[Let] [0]
   rewrite[Let][Let](v0, v1, v2, v3) -> null_rewrite[Let][Let] [0]
   rewrite[Let][Let][Let](v0, v1, v2, v3) -> null_rewrite[Let][Let][Let] [0]
   rewrite(v0) -> null_rewrite [0]
   second(v0) -> null_second [0]
   isOp(v0) -> null_isOp [0]
   first(v0) -> null_first [0]

The TRS has the following type information:
rewrite :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
Op :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
Val :: a -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
rewrite[Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
second :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
isOp :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> False:True:null_isOp
False :: False:True:null_isOp
True :: False:True:null_isOp
first :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
assrewrite :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
rewrite[Let][Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
rewrite[Let][Let][Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
null_rewrite[Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
null_rewrite[Let][Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
null_rewrite[Let][Let][Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
null_rewrite :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
null_second :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
null_isOp :: False:True:null_isOp
null_first :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first
const :: a

Rewrite Strategy: INNERMOST
----------------------------------------

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

   False => 1
   True => 2
   null_rewrite[Let] => 0
   null_rewrite[Let][Let] => 0
   null_rewrite[Let][Let][Let] => 0
   null_rewrite => 0
   null_second => 0
   null_isOp => 0
   null_first => 0
   const => 0

----------------------------------------

(22)
Obligation:
Complexity RNTS consisting of the following rules:

   assrewrite(z) -{ 1 }-> rewrite(exp) :|: z = exp, exp >= 0
   first(z) -{ 1 }-> x :|: z = 1 + x + y, x >= 0, y >= 0
   first(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   first(z) -{ 1 }-> 1 + n :|: n >= 0, z = 1 + n
   isOp(z) -{ 1 }-> 2 :|: z = 1 + x + y, x >= 0, y >= 0
   isOp(z) -{ 1 }-> 1 :|: n >= 0, z = 1 + n
   isOp(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   rewrite(z) -{ 1 }-> rewrite[Let](1 + (1 + x + y) + y', 1 + x + y, rewrite(x)) :|: x >= 0, y >= 0, y' >= 0, z = 1 + (1 + x + y) + y'
   rewrite(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   rewrite(z) -{ 1 }-> 1 + n :|: n >= 0, z = 1 + n
   rewrite(z) -{ 1 }-> 1 + rewrite(y) + (1 + n) :|: n >= 0, y >= 0, z = 1 + (1 + n) + y
   rewrite[Let](z, z', z'') -{ 0 }-> rewrite[Let][Let](exp, 1 + x + y, a1, rewrite(y)) :|: a1 >= 0, z' = 1 + x + y, x >= 0, y >= 0, z = exp, z'' = a1, exp >= 0
   rewrite[Let](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> rewrite[Let][Let][Let](1 + x + y, a1, b1, rewrite(y)) :|: a1 >= 0, z = 1 + x + y, z1 = b1, b1 >= 0, opab >= 0, x >= 0, y >= 0, z' = opab, z'' = a1
   rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> rewrite(1 + a1 + (1 + b1 + rewrite(c1))) :|: a1 >= 0, b1 >= 0, z1 = c1, z = exp, c1 >= 0, z'' = b1, z' = a1, exp >= 0
   rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   second(z) -{ 1 }-> y :|: z = 1 + x + y, x >= 0, y >= 0
   second(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0

Only complete derivations are relevant for the runtime complexity.

----------------------------------------

(23) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(24)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
   rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
   rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
   rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
   rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
   rewrite(Val(z0)) -> Val(z0)
   second(Op(z0, z1)) -> z1
   isOp(Val(z0)) -> False
   isOp(Op(z0, z1)) -> True
   first(Val(z0)) -> Val(z0)
   first(Op(z0, z1)) -> z0
   assrewrite(z0) -> rewrite(z0)
Tuples:
   REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2))
   REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1))
   REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
   SECOND(Op(z0, z1)) -> c6
   ISOP(Val(z0)) -> c7
   ISOP(Op(z0, z1)) -> c8
   FIRST(Val(z0)) -> c9
   FIRST(Op(z0, z1)) -> c10
   ASSREWRITE(z0) -> c11(REWRITE(z0))
S tuples:
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
   SECOND(Op(z0, z1)) -> c6
   ISOP(Val(z0)) -> c7
   ISOP(Op(z0, z1)) -> c8
   FIRST(Val(z0)) -> c9
   FIRST(Op(z0, z1)) -> c10
   ASSREWRITE(z0) -> c11(REWRITE(z0))
K tuples:none
Defined Rule Symbols:   rewrite_1, second_1, isOp_1, first_1, assrewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4

Defined Pair Symbols:   REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4, REWRITE_1, SECOND_1, ISOP_1, FIRST_1, ASSREWRITE_1

Compound Symbols:   c_2, c1_2, c2_2, c3_1, c4_2, c5, c6, c7, c8, c9, c10, c11_1


----------------------------------------

(25) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   ASSREWRITE(z0) -> c11(REWRITE(z0))
Removed 5 trailing nodes:
   ISOP(Op(z0, z1)) -> c8
   FIRST(Val(z0)) -> c9
   FIRST(Op(z0, z1)) -> c10
   SECOND(Op(z0, z1)) -> c6
   ISOP(Val(z0)) -> c7

----------------------------------------

(26)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
   rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
   rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
   rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
   rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
   rewrite(Val(z0)) -> Val(z0)
   second(Op(z0, z1)) -> z1
   isOp(Val(z0)) -> False
   isOp(Op(z0, z1)) -> True
   first(Val(z0)) -> Val(z0)
   first(Op(z0, z1)) -> z0
   assrewrite(z0) -> rewrite(z0)
Tuples:
   REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2))
   REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1))
   REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
S tuples:
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
K tuples:none
Defined Rule Symbols:   rewrite_1, second_1, isOp_1, first_1, assrewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4

Defined Pair Symbols:   REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4, REWRITE_1

Compound Symbols:   c_2, c1_2, c2_2, c3_1, c4_2, c5


----------------------------------------

(27) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   second(Op(z0, z1)) -> z1
   isOp(Val(z0)) -> False
   isOp(Op(z0, z1)) -> True
   first(Val(z0)) -> Val(z0)
   first(Op(z0, z1)) -> z0
   assrewrite(z0) -> rewrite(z0)

----------------------------------------

(28)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
   rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
   rewrite(Val(z0)) -> Val(z0)
   rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
   rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
   rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
Tuples:
   REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2))
   REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1))
   REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
S tuples:
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
K tuples:none
Defined Rule Symbols:   rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4

Defined Pair Symbols:   REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4, REWRITE_1

Compound Symbols:   c_2, c1_2, c2_2, c3_1, c4_2, c5


----------------------------------------

(29) CdtInstantiationProof (BOTH BOUNDS(ID, ID))
Use instantiation to replace REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2)) by 
   REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1))

----------------------------------------

(30)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
   rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
   rewrite(Val(z0)) -> Val(z0)
   rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
   rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
   rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
Tuples:
   REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1))
   REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
   REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1))
S tuples:
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
K tuples:none
Defined Rule Symbols:   rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4

Defined Pair Symbols:   REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4, REWRITE_1, REWRITE[LET]_3

Compound Symbols:   c1_2, c2_2, c3_1, c4_2, c5, c_2


----------------------------------------

(31) CdtInstantiationProof (BOTH BOUNDS(ID, ID))
Use instantiation to replace REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1)) by 
   REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), x3, y0) -> c1(REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, y0, rewrite(x2)), REWRITE(x2))

----------------------------------------

(32)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
   rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
   rewrite(Val(z0)) -> Val(z0)
   rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
   rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
   rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
Tuples:
   REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3))
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
   REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1))
   REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), x3, y0) -> c1(REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, y0, rewrite(x2)), REWRITE(x2))
S tuples:
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
K tuples:none
Defined Rule Symbols:   rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4

Defined Pair Symbols:   REWRITE[LET][LET][LET]_4, REWRITE_1, REWRITE[LET]_3, REWRITE[LET][LET]_4

Compound Symbols:   c2_2, c3_1, c4_2, c5, c_2, c1_2


----------------------------------------

(33) CdtInstantiationProof (BOTH BOUNDS(ID, ID))
Use instantiation to replace REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3)) by 
   REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, x4, y0) -> c2(REWRITE(Op(x3, Op(x4, rewrite(y0)))), REWRITE(y0))

----------------------------------------

(34)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
   rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
   rewrite(Val(z0)) -> Val(z0)
   rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
   rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
   rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
Tuples:
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
   REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1))
   REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), x3, y0) -> c1(REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, y0, rewrite(x2)), REWRITE(x2))
   REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, x4, y0) -> c2(REWRITE(Op(x3, Op(x4, rewrite(y0)))), REWRITE(y0))
S tuples:
   REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1))
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
K tuples:none
Defined Rule Symbols:   rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4

Defined Pair Symbols:   REWRITE_1, REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4

Compound Symbols:   c3_1, c4_2, c5, c_2, c1_2, c2_2


----------------------------------------

(35) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) by 
   REWRITE(Op(Val(z0), Op(Val(y0), y1))) -> c3(REWRITE(Op(Val(y0), y1)))
   REWRITE(Op(Val(z0), Op(Op(y0, y1), y2))) -> c3(REWRITE(Op(Op(y0, y1), y2)))
   REWRITE(Op(Val(z0), Val(y0))) -> c3(REWRITE(Val(y0)))

----------------------------------------

(36)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
   rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
   rewrite(Val(z0)) -> Val(z0)
   rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
   rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
   rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
Tuples:
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
   REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1))
   REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), x3, y0) -> c1(REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, y0, rewrite(x2)), REWRITE(x2))
   REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, x4, y0) -> c2(REWRITE(Op(x3, Op(x4, rewrite(y0)))), REWRITE(y0))
   REWRITE(Op(Val(z0), Op(Val(y0), y1))) -> c3(REWRITE(Op(Val(y0), y1)))
   REWRITE(Op(Val(z0), Op(Op(y0, y1), y2))) -> c3(REWRITE(Op(Op(y0, y1), y2)))
   REWRITE(Op(Val(z0), Val(y0))) -> c3(REWRITE(Val(y0)))
S tuples:
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
   REWRITE(Op(Val(z0), Op(Val(y0), y1))) -> c3(REWRITE(Op(Val(y0), y1)))
   REWRITE(Op(Val(z0), Op(Op(y0, y1), y2))) -> c3(REWRITE(Op(Op(y0, y1), y2)))
   REWRITE(Op(Val(z0), Val(y0))) -> c3(REWRITE(Val(y0)))
K tuples:none
Defined Rule Symbols:   rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4

Defined Pair Symbols:   REWRITE_1, REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4

Compound Symbols:   c4_2, c5, c_2, c1_2, c2_2, c3_1


----------------------------------------

(37) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace REWRITE(Op(Val(z0), Op(Val(y0), y1))) -> c3(REWRITE(Op(Val(y0), y1))) by 
   REWRITE(Op(Val(z0), Op(Val(z1), Op(Val(y1), y2)))) -> c3(REWRITE(Op(Val(z1), Op(Val(y1), y2))))
   REWRITE(Op(Val(z0), Op(Val(z1), Op(Op(y1, y2), y3)))) -> c3(REWRITE(Op(Val(z1), Op(Op(y1, y2), y3))))
   REWRITE(Op(Val(z0), Op(Val(z1), Val(y1)))) -> c3(REWRITE(Op(Val(z1), Val(y1))))

----------------------------------------

(38)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0))
   rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0))
   rewrite(Val(z0)) -> Val(z0)
   rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2))
   rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1))
   rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3))))
Tuples:
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
   REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1))
   REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), x3, y0) -> c1(REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, y0, rewrite(x2)), REWRITE(x2))
   REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, x4, y0) -> c2(REWRITE(Op(x3, Op(x4, rewrite(y0)))), REWRITE(y0))
   REWRITE(Op(Val(z0), Op(Op(y0, y1), y2))) -> c3(REWRITE(Op(Op(y0, y1), y2)))
   REWRITE(Op(Val(z0), Val(y0))) -> c3(REWRITE(Val(y0)))
   REWRITE(Op(Val(z0), Op(Val(z1), Op(Val(y1), y2)))) -> c3(REWRITE(Op(Val(z1), Op(Val(y1), y2))))
   REWRITE(Op(Val(z0), Op(Val(z1), Op(Op(y1, y2), y3)))) -> c3(REWRITE(Op(Val(z1), Op(Op(y1, y2), y3))))
   REWRITE(Op(Val(z0), Op(Val(z1), Val(y1)))) -> c3(REWRITE(Op(Val(z1), Val(y1))))
S tuples:
   REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0))
   REWRITE(Val(z0)) -> c5
   REWRITE(Op(Val(z0), Op(Op(y0, y1), y2))) -> c3(REWRITE(Op(Op(y0, y1), y2)))
   REWRITE(Op(Val(z0), Val(y0))) -> c3(REWRITE(Val(y0)))
   REWRITE(Op(Val(z0), Op(Val(z1), Op(Val(y1), y2)))) -> c3(REWRITE(Op(Val(z1), Op(Val(y1), y2))))
   REWRITE(Op(Val(z0), Op(Val(z1), Op(Op(y1, y2), y3)))) -> c3(REWRITE(Op(Val(z1), Op(Op(y1, y2), y3))))
   REWRITE(Op(Val(z0), Op(Val(z1), Val(y1)))) -> c3(REWRITE(Op(Val(z1), Val(y1))))
K tuples:none
Defined Rule Symbols:   rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4

Defined Pair Symbols:   REWRITE_1, REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4

Compound Symbols:   c4_2, c5, c_2, c1_2, c2_2, c3_1