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