MAYBE
proof of input_K4uLQVgqbb.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), 334 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) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (32) CdtProblem
    (33) CdtForwardInstantiationProof [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
    (39) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms]
    (40) CdtProblem
    (41) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 1 ms]
    (42) 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:

   rw(Val(n), c) -> Op(Val(n), rewrite(c))
   rewrite(Op(x, y)) -> rw(x, y)
   rw(Op(x, y), c) -> rw[Let](Op(x, y), c, 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:

   rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y))
   rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c))
   rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, 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:

   rw(Val(n), c) -> Op(Val(n), rewrite(c))
   rewrite(Op(x, y)) -> rw(x, y)
   rw(Op(x, y), c) -> rw[Let](Op(x, y), c, 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:

   rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y))
   rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c))
   rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, 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:

   rw(Val(n), c) -> Op(Val(n), rewrite(c))
   rewrite(Op(x, y)) -> rw(x, y)
   rw(Op(x, y), c) -> rw[Let](Op(x, y), c, 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:

   rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y))
   rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c))
   rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, 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:

   rw(Val(n), c) -> Op(Val(n), rewrite(c))
   rewrite(Op(x, y)) -> rw(x, y)
   rw(Op(x, y), c) -> rw[Let](Op(x, y), c, 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)
   rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y))
   rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c))
   rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, 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:

   rw(Val(n), c) -> Op(Val(n), rewrite(c)) [1]
   rewrite(Op(x, y)) -> rw(x, y) [1]
   rw(Op(x, y), c) -> rw[Let](Op(x, y), c, 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]
   rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y)) [0]
   rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c)) [0]
   rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, 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:

   rw(Val(n), c) -> Op(Val(n), rewrite(c)) [1]
   rewrite(Op(x, y)) -> rw(x, y) [1]
   rw(Op(x, y), c) -> rw[Let](Op(x, y), c, 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]
   rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y)) [0]
   rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c)) [0]
   rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, c1)) [0]

The TRS has the following type information:
rw :: Val:Op -> Val:Op -> Val:Op
Val :: a -> Val:Op
Op :: Val:Op -> Val:Op -> Val:Op
rewrite :: Val:Op -> Val:Op
rw[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
rw[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op
rw[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
   rw_2
   rw[Let]_3
   rw[Let][Let]_4
   rw[Let][Let][Let]_4

Due to the following rules being added:

   rw[Let](v0, v1, v2) -> const [0]
   rw[Let][Let](v0, v1, v2, v3) -> const [0]
   rw[Let][Let][Let](v0, v1, v2, v3) -> const [0]
   rewrite(v0) -> const [0]
   rw(v0, v1) -> 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:

   rw(Val(n), c) -> Op(Val(n), rewrite(c)) [1]
   rewrite(Op(x, y)) -> rw(x, y) [1]
   rw(Op(x, y), c) -> rw[Let](Op(x, y), c, 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]
   rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y)) [0]
   rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c)) [0]
   rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, c1)) [0]
   rw[Let](v0, v1, v2) -> const [0]
   rw[Let][Let](v0, v1, v2, v3) -> const [0]
   rw[Let][Let][Let](v0, v1, v2, v3) -> const [0]
   rewrite(v0) -> const [0]
   rw(v0, v1) -> const [0]

The TRS has the following type information:
rw :: Val:Op:const -> Val:Op:const -> Val:Op:const
Val :: a -> Val:Op:const
Op :: Val:Op:const -> Val:Op:const -> Val:Op:const
rewrite :: Val:Op:const -> Val:Op:const
rw[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
rw[Let][Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const
rw[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:

   rw(Val(n), c) -> Op(Val(n), rewrite(c)) [1]
   rewrite(Op(x, y)) -> rw(x, y) [1]
   rw(Op(Op(x', y'), y), c) -> rw[Let](Op(Op(x', y'), y), c, rw(x', y')) [2]
   rw(Op(Val(n'), y), c) -> rw[Let](Op(Val(n'), y), c, Val(n')) [2]
   rw(Op(x, y), c) -> rw[Let](Op(x, y), c, 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]
   rw[Let](Op(x, Op(x'', y'')), c, a1) -> rw[Let][Let](Op(x, Op(x'', y'')), c, a1, rw(x'', y'')) [1]
   rw[Let](Op(x, Val(n'')), c, a1) -> rw[Let][Let](Op(x, Val(n'')), c, a1, Val(n'')) [1]
   rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, const) [0]
   rw[Let][Let](ab, Op(x1, y1), a1, b1) -> rw[Let][Let][Let](Op(x1, y1), a1, b1, rw(x1, y1)) [1]
   rw[Let][Let](ab, Val(n1), a1, b1) -> rw[Let][Let][Let](Val(n1), a1, b1, Val(n1)) [1]
   rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, const) [0]
   rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, c1)) [0]
   rw[Let](v0, v1, v2) -> const [0]
   rw[Let][Let](v0, v1, v2, v3) -> const [0]
   rw[Let][Let][Let](v0, v1, v2, v3) -> const [0]
   rewrite(v0) -> const [0]
   rw(v0, v1) -> const [0]

The TRS has the following type information:
rw :: Val:Op:const -> Val:Op:const -> Val:Op:const
Val :: a -> Val:Op:const
Op :: Val:Op:const -> Val:Op:const -> Val:Op:const
rewrite :: Val:Op:const -> Val:Op:const
rw[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
rw[Let][Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const
rw[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 }-> rw(x, y) :|: z = 1 + x + y, x >= 0, y >= 0
   rewrite(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   rewrite(z) -{ 1 }-> 1 + n :|: n >= 0, z = 1 + n
   rw(z, z') -{ 1 }-> rw[Let](1 + x + y, c, 0) :|: z = 1 + x + y, c >= 0, x >= 0, y >= 0, z' = c
   rw(z, z') -{ 2 }-> rw[Let](1 + (1 + n') + y, c, 1 + n') :|: c >= 0, y >= 0, z = 1 + (1 + n') + y, n' >= 0, z' = c
   rw(z, z') -{ 2 }-> rw[Let](1 + (1 + x' + y') + y, c, rw(x', y')) :|: c >= 0, x' >= 0, y >= 0, y' >= 0, z = 1 + (1 + x' + y') + y, z' = c
   rw(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   rw(z, z') -{ 1 }-> 1 + (1 + n) + rewrite(c) :|: n >= 0, c >= 0, z' = c, z = 1 + n
   rw[Let](z, z', z'') -{ 0 }-> rw[Let][Let](1 + x + y, c, a1, 0) :|: a1 >= 0, z = 1 + x + y, c >= 0, x >= 0, y >= 0, z' = c, z'' = a1
   rw[Let](z, z', z'') -{ 1 }-> rw[Let][Let](1 + x + (1 + n''), c, a1, 1 + n'') :|: a1 >= 0, c >= 0, x >= 0, n'' >= 0, z = 1 + x + (1 + n''), z' = c, z'' = a1
   rw[Let](z, z', z'') -{ 1 }-> rw[Let][Let](1 + x + (1 + x'' + y''), c, a1, rw(x'', y'')) :|: a1 >= 0, c >= 0, z = 1 + x + (1 + x'' + y''), x >= 0, y'' >= 0, z' = c, x'' >= 0, z'' = a1
   rw[Let](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   rw[Let][Let](z, z', z'', z1) -{ 0 }-> rw[Let][Let][Let](c, a1, b1, 0) :|: a1 >= 0, z1 = b1, c >= 0, b1 >= 0, z = ab, z' = c, z'' = a1, ab >= 0
   rw[Let][Let](z, z', z'', z1) -{ 1 }-> rw[Let][Let][Let](1 + n1, a1, b1, 1 + n1) :|: a1 >= 0, z1 = b1, b1 >= 0, z = ab, n1 >= 0, z' = 1 + n1, z'' = a1, ab >= 0
   rw[Let][Let](z, z', z'', z1) -{ 1 }-> rw[Let][Let][Let](1 + x1 + y1, a1, b1, rw(x1, y1)) :|: y1 >= 0, x1 >= 0, a1 >= 0, z1 = b1, b1 >= 0, z = ab, z' = 1 + x1 + y1, z'' = a1, ab >= 0
   rw[Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   rw[Let][Let][Let](z, z', z'', z1) -{ 0 }-> rw(a1, 1 + b1 + c1) :|: a1 >= 0, c >= 0, b1 >= 0, z1 = c1, z = c, c1 >= 0, z'' = b1, z' = a1
   rw[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 }-> rw(x, y) :|: z = 1 + x + y, x >= 0, y >= 0
   rewrite(z) -{ 0 }-> 0 :|: z >= 0
   rewrite(z) -{ 1 }-> 1 + (z - 1) :|: z - 1 >= 0
   rw(z, z') -{ 1 }-> rw[Let](1 + x + y, z', 0) :|: z = 1 + x + y, z' >= 0, x >= 0, y >= 0
   rw(z, z') -{ 2 }-> rw[Let](1 + (1 + n') + y, z', 1 + n') :|: z' >= 0, y >= 0, z = 1 + (1 + n') + y, n' >= 0
   rw(z, z') -{ 2 }-> rw[Let](1 + (1 + x' + y') + y, z', rw(x', y')) :|: z' >= 0, x' >= 0, y >= 0, y' >= 0, z = 1 + (1 + x' + y') + y
   rw(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   rw(z, z') -{ 1 }-> 1 + (1 + (z - 1)) + rewrite(z') :|: z - 1 >= 0, z' >= 0
   rw[Let](z, z', z'') -{ 0 }-> rw[Let][Let](1 + x + y, z', z'', 0) :|: z'' >= 0, z = 1 + x + y, z' >= 0, x >= 0, y >= 0
   rw[Let](z, z', z'') -{ 1 }-> rw[Let][Let](1 + x + (1 + n''), z', z'', 1 + n'') :|: z'' >= 0, z' >= 0, x >= 0, n'' >= 0, z = 1 + x + (1 + n'')
   rw[Let](z, z', z'') -{ 1 }-> rw[Let][Let](1 + x + (1 + x'' + y''), z', z'', rw(x'', y'')) :|: z'' >= 0, z' >= 0, z = 1 + x + (1 + x'' + y''), x >= 0, y'' >= 0, x'' >= 0
   rw[Let](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   rw[Let][Let](z, z', z'', z1) -{ 0 }-> rw[Let][Let][Let](z', z'', z1, 0) :|: z'' >= 0, z' >= 0, z1 >= 0, z >= 0
   rw[Let][Let](z, z', z'', z1) -{ 1 }-> rw[Let][Let][Let](1 + (z' - 1), z'', z1, 1 + (z' - 1)) :|: z'' >= 0, z1 >= 0, z' - 1 >= 0, z >= 0
   rw[Let][Let](z, z', z'', z1) -{ 1 }-> rw[Let][Let][Let](1 + x1 + y1, z'', z1, rw(x1, y1)) :|: y1 >= 0, x1 >= 0, z'' >= 0, z1 >= 0, z' = 1 + x1 + y1, z >= 0
   rw[Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
   rw[Let][Let][Let](z, z', z'', z1) -{ 0 }-> rw(z', 1 + z'' + z1) :|: z' >= 0, z >= 0, z'' >= 0, z1 >= 0
   rw[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:

   rw[Let](v0, v1, v2) -> null_rw[Let] [0]
   rw[Let][Let](v0, v1, v2, v3) -> null_rw[Let][Let] [0]
   rw[Let][Let][Let](v0, v1, v2, v3) -> null_rw[Let][Let][Let] [0]
   rw(v0, v1) -> null_rw [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_rw[Let], null_rw[Let][Let], null_rw[Let][Let][Let], null_rw, 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:

   rw(Val(n), c) -> Op(Val(n), rewrite(c)) [1]
   rewrite(Op(x, y)) -> rw(x, y) [1]
   rw(Op(x, y), c) -> rw[Let](Op(x, y), c, 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]
   rw[Let](Op(x, y), c, a1) -> rw[Let][Let](Op(x, y), c, a1, rewrite(y)) [0]
   rw[Let][Let](ab, c, a1, b1) -> rw[Let][Let][Let](c, a1, b1, rewrite(c)) [0]
   rw[Let][Let][Let](c, a1, b1, c1) -> rw(a1, Op(b1, c1)) [0]
   rw[Let](v0, v1, v2) -> null_rw[Let] [0]
   rw[Let][Let](v0, v1, v2, v3) -> null_rw[Let][Let] [0]
   rw[Let][Let][Let](v0, v1, v2, v3) -> null_rw[Let][Let][Let] [0]
   rw(v0, v1) -> null_rw [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:
rw :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
Val :: a -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
Op :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
rewrite :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
rw[Let] :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
second :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
isOp :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> False:True:null_isOp
False :: False:True:null_isOp
True :: False:True:null_isOp
first :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
assrewrite :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
rw[Let][Let] :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
rw[Let][Let][Let] :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first -> Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
null_rw[Let] :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
null_rw[Let][Let] :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
null_rw[Let][Let][Let] :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
null_rw :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
null_rewrite :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
null_second :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw:null_rewrite:null_second:null_first
null_isOp :: False:True:null_isOp
null_first :: Val:Op:null_rw[Let]:null_rw[Let][Let]:null_rw[Let][Let][Let]:null_rw: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_rw[Let] => 0
   null_rw[Let][Let] => 0
   null_rw[Let][Let][Let] => 0
   null_rw => 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 }-> rw(x, y) :|: z = 1 + x + y, x >= 0, y >= 0
   rewrite(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0
   rewrite(z) -{ 1 }-> 1 + n :|: n >= 0, z = 1 + n
   rw(z, z') -{ 1 }-> rw[Let](1 + x + y, c, rewrite(x)) :|: z = 1 + x + y, c >= 0, x >= 0, y >= 0, z' = c
   rw(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   rw(z, z') -{ 1 }-> 1 + (1 + n) + rewrite(c) :|: n >= 0, c >= 0, z' = c, z = 1 + n
   rw[Let](z, z', z'') -{ 0 }-> rw[Let][Let](1 + x + y, c, a1, rewrite(y)) :|: a1 >= 0, z = 1 + x + y, c >= 0, x >= 0, y >= 0, z' = c, z'' = a1
   rw[Let](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   rw[Let][Let](z, z', z'', z1) -{ 0 }-> rw[Let][Let][Let](c, a1, b1, rewrite(c)) :|: a1 >= 0, z1 = b1, c >= 0, b1 >= 0, z = ab, z' = c, z'' = a1, ab >= 0
   rw[Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
   rw[Let][Let][Let](z, z', z'', z1) -{ 0 }-> rw(a1, 1 + b1 + c1) :|: a1 >= 0, c >= 0, b1 >= 0, z1 = c1, z = c, c1 >= 0, z'' = b1, z' = a1
   rw[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:
   rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
   rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
   rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
   rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
   rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
   rewrite(Op(z0, z1)) -> rw(z0, z1)
   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:
   RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
   RW(Val(z0), z1) -> c3(REWRITE(z1))
   RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
   REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
   REWRITE(Val(z0)) -> c6
   SECOND(Op(z0, z1)) -> c7
   ISOP(Val(z0)) -> c8
   ISOP(Op(z0, z1)) -> c9
   FIRST(Val(z0)) -> c10
   FIRST(Op(z0, z1)) -> c11
   ASSREWRITE(z0) -> c12(REWRITE(z0))
S tuples:
   RW(Val(z0), z1) -> c3(REWRITE(z1))
   RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
   REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
   REWRITE(Val(z0)) -> c6
   SECOND(Op(z0, z1)) -> c7
   ISOP(Val(z0)) -> c8
   ISOP(Op(z0, z1)) -> c9
   FIRST(Val(z0)) -> c10
   FIRST(Op(z0, z1)) -> c11
   ASSREWRITE(z0) -> c12(REWRITE(z0))
K tuples:none
Defined Rule Symbols:   rw_2, rewrite_1, second_1, isOp_1, first_1, assrewrite_1, rw[Let]_3, rw[Let][Let]_4, rw[Let][Let][Let]_4

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

Compound Symbols:   c_2, c1_2, c2_1, c3_1, c4_2, c5_1, c6, c7, c8, c9, c10, c11, c12_1


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

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

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

(26)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
   rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
   rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
   rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
   rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
   rewrite(Op(z0, z1)) -> rw(z0, z1)
   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:
   RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
   RW(Val(z0), z1) -> c3(REWRITE(z1))
   RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
   REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
   REWRITE(Val(z0)) -> c6
S tuples:
   RW(Val(z0), z1) -> c3(REWRITE(z1))
   RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
   REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
   REWRITE(Val(z0)) -> c6
K tuples:none
Defined Rule Symbols:   rw_2, rewrite_1, second_1, isOp_1, first_1, assrewrite_1, rw[Let]_3, rw[Let][Let]_4, rw[Let][Let][Let]_4

Defined Pair Symbols:   RW[LET]_3, RW[LET][LET]_4, RW[LET][LET][LET]_4, RW_2, REWRITE_1

Compound Symbols:   c_2, c1_2, c2_1, c3_1, c4_2, c5_1, c6


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

(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(z0, z1)) -> rw(z0, z1)
   rewrite(Val(z0)) -> Val(z0)
   rw(Val(z0), z1) -> Op(Val(z0), rewrite(z1))
   rw(Op(z0, z1), z2) -> rw[Let](Op(z0, z1), z2, rewrite(z0))
   rw[Let](Op(z0, z1), z2, z3) -> rw[Let][Let](Op(z0, z1), z2, z3, rewrite(z1))
   rw[Let][Let](z0, z1, z2, z3) -> rw[Let][Let][Let](z1, z2, z3, rewrite(z1))
   rw[Let][Let][Let](z0, z1, z2, z3) -> rw(z1, Op(z2, z3))
Tuples:
   RW[LET](Op(z0, z1), z2, z3) -> c(RW[LET][LET](Op(z0, z1), z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET](z0, z1, z2, z3) -> c1(RW[LET][LET][LET](z1, z2, z3, rewrite(z1)), REWRITE(z1))
   RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3)))
   RW(Val(z0), z1) -> c3(REWRITE(z1))
   RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
   REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
   REWRITE(Val(z0)) -> c6
S tuples:
   RW(Val(z0), z1) -> c3(REWRITE(z1))
   RW(Op(z0, z1), z2) -> c4(RW[LET](Op(z0, z1), z2, rewrite(z0)), REWRITE(z0))
   REWRITE(Op(z0, z1)) -> c5(RW(z0, z1))
   REWRITE(Val(z0)) -> c6
K tuples:none
Defined Rule Symbols:   rewrite_1, rw_2, rw[Let]_3, rw[Let][Let]_4, rw[Let][Let][Let]_4

Defined Pair Symbols:   RW[LET]_3, RW[LET][LET]_4, RW[LET][LET][LET]_4, RW_2, REWRITE_1

Compound Symbols:   c_2, c1_2, c2_1, c3_1, c4_2, c5_1, c6


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

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

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

(30)
Obligation:
Complexity Dependency Tuples Problem

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

Defined Pair Symbols:   RW[LET]_3, RW[LET][LET][LET]_4, RW_2, REWRITE_1, RW[LET][LET]_4

Compound Symbols:   c_2, c2_1, c3_1, c4_2, c5_1, c6, c1_2


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

(31) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace RW[LET][LET][LET](z0, z1, z2, z3) -> c2(RW(z1, Op(z2, z3))) by 
   RW[LET][LET][LET](z0, Val(y0), z2, z3) -> c2(RW(Val(y0), Op(z2, z3)))
   RW[LET][LET][LET](z0, Op(y0, y1), z2, z3) -> c2(RW(Op(y0, y1), Op(z2, z3)))

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

(32)
Obligation:
Complexity Dependency Tuples Problem

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

Defined Pair Symbols:   RW[LET]_3, RW_2, REWRITE_1, RW[LET][LET]_4, RW[LET][LET][LET]_4

Compound Symbols:   c_2, c3_1, c4_2, c5_1, c6, c1_2, c2_1


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

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

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

(34)
Obligation:
Complexity Dependency Tuples Problem

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

Defined Pair Symbols:   RW[LET]_3, RW_2, REWRITE_1, RW[LET][LET]_4, RW[LET][LET][LET]_4

Compound Symbols:   c_2, c4_2, c5_1, c6, c1_2, c2_1, c3_1


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

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

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

(36)
Obligation:
Complexity Dependency Tuples Problem

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

Defined Pair Symbols:   RW[LET]_3, RW_2, REWRITE_1, RW[LET][LET]_4, RW[LET][LET][LET]_4

Compound Symbols:   c_2, c4_2, c6, c1_2, c2_1, c3_1, c5_1


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

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

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

(38)
Obligation:
Complexity Dependency Tuples Problem

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

Defined Pair Symbols:   RW[LET]_3, RW_2, REWRITE_1, RW[LET][LET]_4, RW[LET][LET][LET]_4

Compound Symbols:   c_2, c4_2, c6, c1_2, c2_1, c3_1, c5_1


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

(39) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace RW[LET][LET][LET](z0, Val(y0), z2, z3) -> c2(RW(Val(y0), Op(z2, z3))) by 
   RW[LET][LET][LET](z0, Val(z1), Op(y1, y2), z3) -> c2(RW(Val(z1), Op(Op(y1, y2), z3)))
   RW[LET][LET][LET](z0, Val(z1), Val(y1), Op(y2, y3)) -> c2(RW(Val(z1), Op(Val(y1), Op(y2, y3))))
   RW[LET][LET][LET](z0, Val(z1), Val(y1), Val(y2)) -> c2(RW(Val(z1), Op(Val(y1), Val(y2))))

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

(40)
Obligation:
Complexity Dependency Tuples Problem

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

Defined Pair Symbols:   RW[LET]_3, RW_2, REWRITE_1, RW[LET][LET]_4, RW[LET][LET][LET]_4

Compound Symbols:   c_2, c4_2, c6, c1_2, c2_1, c3_1, c5_1


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

(41) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
Use forward instantiation to replace REWRITE(Op(Val(y0), Op(y1, y2))) -> c5(RW(Val(y0), Op(y1, y2))) by 
   REWRITE(Op(Val(z0), Op(Op(y1, y2), z2))) -> c5(RW(Val(z0), Op(Op(y1, y2), z2)))
   REWRITE(Op(Val(z0), Op(Val(y1), Op(y2, y3)))) -> c5(RW(Val(z0), Op(Val(y1), Op(y2, y3))))
   REWRITE(Op(Val(z0), Op(Val(y1), Val(y2)))) -> c5(RW(Val(z0), Op(Val(y1), Val(y2))))

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

(42)
Obligation:
Complexity Dependency Tuples Problem

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

Defined Pair Symbols:   RW[LET]_3, RW_2, REWRITE_1, RW[LET][LET]_4, RW[LET][LET][LET]_4

Compound Symbols:   c_2, c4_2, c6, c1_2, c2_1, c3_1, c5_1