MAYBE proof of input_I6JXLOwTnT.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 338 ms] (2) CpxRelTRS (3) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxRelTRS (5) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (6) CpxTRS (7) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (8) CpxWeightedTrs (9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CpxTypedWeightedTrs (11) CompletionProof [UPPER BOUND(ID), 0 ms] (12) CpxTypedWeightedCompleteTrs (13) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CpxTypedWeightedCompleteTrs (15) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (16) CpxRNTS (17) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CpxRNTS (19) CompletionProof [UPPER BOUND(ID), 0 ms] (20) CpxTypedWeightedCompleteTrs (21) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (22) CpxRNTS (23) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (24) CdtProblem (25) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (26) CdtProblem (27) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (28) CdtProblem (29) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (30) CdtProblem (31) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (32) CdtProblem (33) CdtInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (34) CdtProblem (35) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (36) CdtProblem (37) CdtForwardInstantiationProof [BOTH BOUNDS(ID, ID), 0 ms] (38) CdtProblem ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) rewrite(Val(n)) -> Val(n) second(Op(x, y)) -> y isOp(Val(n)) -> False isOp(Op(x, y)) -> True first(Val(n)) -> Val(n) first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) The (relative) TRS S consists of the following rules: rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) rewrite(Val(n)) -> Val(n) second(Op(x, y)) -> y isOp(Val(n)) -> False isOp(Op(x, y)) -> True first(Val(n)) -> Val(n) first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) The (relative) TRS S consists of the following rules: rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (4) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) rewrite(Val(n)) -> Val(n) second(Op(x, y)) -> y isOp(Val(n)) -> False isOp(Op(x, y)) -> True first(Val(n)) -> Val(n) first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) The (relative) TRS S consists of the following rules: rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (5) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (6) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) rewrite(Val(n)) -> Val(n) second(Op(x, y)) -> y isOp(Val(n)) -> False isOp(Op(x, y)) -> True first(Val(n)) -> Val(n) first(Op(x, y)) -> x assrewrite(exp) -> rewrite(exp) rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (7) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (8) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, INF). The TRS R consists of the following rules: rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) [1] rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) [1] rewrite(Val(n)) -> Val(n) [1] second(Op(x, y)) -> y [1] isOp(Val(n)) -> False [1] isOp(Op(x, y)) -> True [1] first(Val(n)) -> Val(n) [1] first(Op(x, y)) -> x [1] assrewrite(exp) -> rewrite(exp) [1] rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) [0] rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) [0] rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (9) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (10) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) [1] rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) [1] rewrite(Val(n)) -> Val(n) [1] second(Op(x, y)) -> y [1] isOp(Val(n)) -> False [1] isOp(Op(x, y)) -> True [1] first(Val(n)) -> Val(n) [1] first(Op(x, y)) -> x [1] assrewrite(exp) -> rewrite(exp) [1] rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) [0] rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) [0] rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) [0] The TRS has the following type information: rewrite :: Val:Op -> Val:Op Op :: Val:Op -> Val:Op -> Val:Op Val :: a -> Val:Op rewrite[Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op second :: Val:Op -> Val:Op isOp :: Val:Op -> False:True False :: False:True True :: False:True first :: Val:Op -> Val:Op assrewrite :: Val:Op -> Val:Op rewrite[Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op rewrite[Let][Let][Let] :: Val:Op -> Val:Op -> Val:Op -> Val:Op -> Val:Op Rewrite Strategy: INNERMOST ---------------------------------------- (11) CompletionProof (UPPER BOUND(ID)) The transformation into a RNTS is sound, since: (a) The obligation is a constructor system where every type has a constant constructor, (b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols: second_1 isOp_1 first_1 assrewrite_1 (c) The following functions are completely defined: rewrite_1 rewrite[Let]_3 rewrite[Let][Let]_4 rewrite[Let][Let][Let]_4 Due to the following rules being added: rewrite[Let](v0, v1, v2) -> const [0] rewrite[Let][Let](v0, v1, v2, v3) -> const [0] rewrite[Let][Let][Let](v0, v1, v2, v3) -> const [0] rewrite(v0) -> const [0] And the following fresh constants: const, const1 ---------------------------------------- (12) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) [1] rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) [1] rewrite(Val(n)) -> Val(n) [1] second(Op(x, y)) -> y [1] isOp(Val(n)) -> False [1] isOp(Op(x, y)) -> True [1] first(Val(n)) -> Val(n) [1] first(Op(x, y)) -> x [1] assrewrite(exp) -> rewrite(exp) [1] rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) [0] rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) [0] rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) [0] rewrite[Let](v0, v1, v2) -> const [0] rewrite[Let][Let](v0, v1, v2, v3) -> const [0] rewrite[Let][Let][Let](v0, v1, v2, v3) -> const [0] rewrite(v0) -> const [0] The TRS has the following type information: rewrite :: Val:Op:const -> Val:Op:const Op :: Val:Op:const -> Val:Op:const -> Val:Op:const Val :: a -> Val:Op:const rewrite[Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const second :: Val:Op:const -> Val:Op:const isOp :: Val:Op:const -> False:True False :: False:True True :: False:True first :: Val:Op:const -> Val:Op:const assrewrite :: Val:Op:const -> Val:Op:const rewrite[Let][Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const rewrite[Let][Let][Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const const :: Val:Op:const const1 :: a Rewrite Strategy: INNERMOST ---------------------------------------- (13) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (14) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) [1] rewrite(Op(Op(Op(Val(n'), y''), y), y')) -> rewrite[Let](Op(Op(Op(Val(n'), y''), y), y'), Op(Op(Val(n'), y''), y), Op(rewrite(y''), Val(n'))) [2] rewrite(Op(Op(Op(Op(x', y1), y'''), y), y')) -> rewrite[Let](Op(Op(Op(Op(x', y1), y'''), y), y'), Op(Op(Op(x', y1), y'''), y), rewrite[Let](Op(Op(x', y1), y'''), Op(x', y1), rewrite(x'))) [2] rewrite(Op(Op(Val(n''), y), y')) -> rewrite[Let](Op(Op(Val(n''), y), y'), Op(Val(n''), y), Val(n'')) [2] rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), const) [1] rewrite(Val(n)) -> Val(n) [1] second(Op(x, y)) -> y [1] isOp(Val(n)) -> False [1] isOp(Op(x, y)) -> True [1] first(Val(n)) -> Val(n) [1] first(Op(x, y)) -> x [1] assrewrite(exp) -> rewrite(exp) [1] rewrite[Let](exp, Op(x, Op(Val(n1), y2)), a1) -> rewrite[Let][Let](exp, Op(x, Op(Val(n1), y2)), a1, Op(rewrite(y2), Val(n1))) [1] rewrite[Let](exp, Op(x, Op(Op(x'', y3), y'1)), a1) -> rewrite[Let][Let](exp, Op(x, Op(Op(x'', y3), y'1)), a1, rewrite[Let](Op(Op(x'', y3), y'1), Op(x'', y3), rewrite(x''))) [1] rewrite[Let](exp, Op(x, Val(n2)), a1) -> rewrite[Let][Let](exp, Op(x, Val(n2)), a1, Val(n2)) [1] rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, const) [0] rewrite[Let][Let](Op(x, Op(Val(n3), y4)), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, Op(Val(n3), y4)), a1, b1, Op(rewrite(y4), Val(n3))) [1] rewrite[Let][Let](Op(x, Op(Op(x1, y5), y'2)), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, Op(Op(x1, y5), y'2)), a1, b1, rewrite[Let](Op(Op(x1, y5), y'2), Op(x1, y5), rewrite(x1))) [1] rewrite[Let][Let](Op(x, Val(n4)), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, Val(n4)), a1, b1, Val(n4)) [1] rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, const) [0] rewrite[Let][Let][Let](exp, a1, b1, Op(Val(n5), y6)) -> rewrite(Op(a1, Op(b1, Op(rewrite(y6), Val(n5))))) [1] rewrite[Let][Let][Let](exp, a1, b1, Op(Op(x2, y7), y'3)) -> rewrite(Op(a1, Op(b1, rewrite[Let](Op(Op(x2, y7), y'3), Op(x2, y7), rewrite(x2))))) [1] rewrite[Let][Let][Let](exp, a1, b1, Val(n6)) -> rewrite(Op(a1, Op(b1, Val(n6)))) [1] rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, const))) [0] rewrite[Let](v0, v1, v2) -> const [0] rewrite[Let][Let](v0, v1, v2, v3) -> const [0] rewrite[Let][Let][Let](v0, v1, v2, v3) -> const [0] rewrite(v0) -> const [0] The TRS has the following type information: rewrite :: Val:Op:const -> Val:Op:const Op :: Val:Op:const -> Val:Op:const -> Val:Op:const Val :: a -> Val:Op:const rewrite[Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const second :: Val:Op:const -> Val:Op:const isOp :: Val:Op:const -> False:True False :: False:True True :: False:True first :: Val:Op:const -> Val:Op:const assrewrite :: Val:Op:const -> Val:Op:const rewrite[Let][Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const rewrite[Let][Let][Let] :: Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const -> Val:Op:const const :: Val:Op:const const1 :: a Rewrite Strategy: INNERMOST ---------------------------------------- (15) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: False => 0 True => 1 const => 0 const1 => 0 ---------------------------------------- (16) Obligation: Complexity RNTS consisting of the following rules: assrewrite(z) -{ 1 }-> rewrite(exp) :|: z = exp, exp >= 0 first(z) -{ 1 }-> x :|: z = 1 + x + y, x >= 0, y >= 0 first(z) -{ 1 }-> 1 + n :|: n >= 0, z = 1 + n isOp(z) -{ 1 }-> 1 :|: z = 1 + x + y, x >= 0, y >= 0 isOp(z) -{ 1 }-> 0 :|: n >= 0, z = 1 + n rewrite(z) -{ 1 }-> rewrite[Let](1 + (1 + x + y) + y', 1 + x + y, 0) :|: x >= 0, y >= 0, y' >= 0, z = 1 + (1 + x + y) + y' rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + n'') + y) + y', 1 + (1 + n'') + y, 1 + n'') :|: y >= 0, n'' >= 0, y' >= 0, z = 1 + (1 + (1 + n'') + y) + y' rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + (1 + n') + y'') + y) + y', 1 + (1 + (1 + n') + y'') + y, 1 + rewrite(y'') + (1 + n')) :|: y >= 0, n' >= 0, y'' >= 0, y' >= 0, z = 1 + (1 + (1 + (1 + n') + y'') + y) + y' rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + (1 + x' + y1) + y''') + y) + y', 1 + (1 + (1 + x' + y1) + y''') + y, rewrite[Let](1 + (1 + x' + y1) + y''', 1 + x' + y1, rewrite(x'))) :|: y1 >= 0, x' >= 0, y >= 0, y' >= 0, z = 1 + (1 + (1 + (1 + x' + y1) + y''') + y) + y', y''' >= 0 rewrite(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 rewrite(z) -{ 1 }-> 1 + n :|: n >= 0, z = 1 + n rewrite(z) -{ 1 }-> 1 + rewrite(y) + (1 + n) :|: n >= 0, y >= 0, z = 1 + (1 + n) + y rewrite[Let](z, z', z'') -{ 0 }-> rewrite[Let][Let](exp, 1 + x + y, a1, 0) :|: a1 >= 0, z' = 1 + x + y, x >= 0, y >= 0, z = exp, z'' = a1, exp >= 0 rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](exp, 1 + x + (1 + n2), a1, 1 + n2) :|: a1 >= 0, x >= 0, z = exp, n2 >= 0, z' = 1 + x + (1 + n2), z'' = a1, exp >= 0 rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](exp, 1 + x + (1 + (1 + n1) + y2), a1, 1 + rewrite(y2) + (1 + n1)) :|: a1 >= 0, x >= 0, z = exp, z' = 1 + x + (1 + (1 + n1) + y2), n1 >= 0, y2 >= 0, z'' = a1, exp >= 0 rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](exp, 1 + x + (1 + (1 + x'' + y3) + y'1), a1, rewrite[Let](1 + (1 + x'' + y3) + y'1, 1 + x'' + y3, rewrite(x''))) :|: a1 >= 0, x >= 0, z = exp, y'1 >= 0, y3 >= 0, z' = 1 + x + (1 + (1 + x'' + y3) + y'1), x'' >= 0, z'' = a1, exp >= 0 rewrite[Let](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> rewrite[Let][Let][Let](1 + x + y, a1, b1, 0) :|: a1 >= 0, z = 1 + x + y, z1 = b1, b1 >= 0, opab >= 0, x >= 0, y >= 0, z' = opab, z'' = a1 rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + n4), a1, b1, 1 + n4) :|: z = 1 + x + (1 + n4), n4 >= 0, a1 >= 0, z1 = b1, b1 >= 0, opab >= 0, x >= 0, z' = opab, z'' = a1 rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + (1 + n3) + y4), a1, b1, 1 + rewrite(y4) + (1 + n3)) :|: a1 >= 0, z1 = b1, b1 >= 0, opab >= 0, x >= 0, z' = opab, y4 >= 0, z'' = a1, z = 1 + x + (1 + (1 + n3) + y4), n3 >= 0 rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + (1 + x1 + y5) + y'2), a1, b1, rewrite[Let](1 + (1 + x1 + y5) + y'2, 1 + x1 + y5, rewrite(x1))) :|: y5 >= 0, x1 >= 0, a1 >= 0, z1 = b1, b1 >= 0, y'2 >= 0, opab >= 0, x >= 0, z' = opab, z'' = a1, z = 1 + x + (1 + (1 + x1 + y5) + y'2) rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0 rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + a1 + (1 + b1 + rewrite[Let](1 + (1 + x2 + y7) + y'3, 1 + x2 + y7, rewrite(x2)))) :|: a1 >= 0, b1 >= 0, z = exp, y7 >= 0, y'3 >= 0, z'' = b1, z' = a1, z1 = 1 + (1 + x2 + y7) + y'3, exp >= 0, x2 >= 0 rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> rewrite(1 + a1 + (1 + b1 + 0)) :|: a1 >= 0, b1 >= 0, z1 = c1, z = exp, c1 >= 0, z'' = b1, z' = a1, exp >= 0 rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + a1 + (1 + b1 + (1 + n6))) :|: a1 >= 0, b1 >= 0, n6 >= 0, z = exp, z'' = b1, z' = a1, exp >= 0, z1 = 1 + n6 rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + a1 + (1 + b1 + (1 + rewrite(y6) + (1 + n5)))) :|: a1 >= 0, b1 >= 0, z = exp, y6 >= 0, n5 >= 0, z'' = b1, z1 = 1 + (1 + n5) + y6, z' = a1, exp >= 0 rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0 second(z) -{ 1 }-> y :|: z = 1 + x + y, x >= 0, y >= 0 ---------------------------------------- (17) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: assrewrite(z) -{ 1 }-> rewrite(z) :|: z >= 0 first(z) -{ 1 }-> x :|: z = 1 + x + y, x >= 0, y >= 0 first(z) -{ 1 }-> 1 + (z - 1) :|: z - 1 >= 0 isOp(z) -{ 1 }-> 1 :|: z = 1 + x + y, x >= 0, y >= 0 isOp(z) -{ 1 }-> 0 :|: z - 1 >= 0 rewrite(z) -{ 1 }-> rewrite[Let](1 + (1 + x + y) + y', 1 + x + y, 0) :|: x >= 0, y >= 0, y' >= 0, z = 1 + (1 + x + y) + y' rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + n'') + y) + y', 1 + (1 + n'') + y, 1 + n'') :|: y >= 0, n'' >= 0, y' >= 0, z = 1 + (1 + (1 + n'') + y) + y' rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + (1 + n') + y'') + y) + y', 1 + (1 + (1 + n') + y'') + y, 1 + rewrite(y'') + (1 + n')) :|: y >= 0, n' >= 0, y'' >= 0, y' >= 0, z = 1 + (1 + (1 + (1 + n') + y'') + y) + y' rewrite(z) -{ 2 }-> rewrite[Let](1 + (1 + (1 + (1 + x' + y1) + y''') + y) + y', 1 + (1 + (1 + x' + y1) + y''') + y, rewrite[Let](1 + (1 + x' + y1) + y''', 1 + x' + y1, rewrite(x'))) :|: y1 >= 0, x' >= 0, y >= 0, y' >= 0, z = 1 + (1 + (1 + (1 + x' + y1) + y''') + y) + y', y''' >= 0 rewrite(z) -{ 0 }-> 0 :|: z >= 0 rewrite(z) -{ 1 }-> 1 + (z - 1) :|: z - 1 >= 0 rewrite(z) -{ 1 }-> 1 + rewrite(y) + (1 + n) :|: n >= 0, y >= 0, z = 1 + (1 + n) + y rewrite[Let](z, z', z'') -{ 0 }-> rewrite[Let][Let](z, 1 + x + y, z'', 0) :|: z'' >= 0, z' = 1 + x + y, x >= 0, y >= 0, z >= 0 rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](z, 1 + x + (1 + n2), z'', 1 + n2) :|: z'' >= 0, x >= 0, n2 >= 0, z' = 1 + x + (1 + n2), z >= 0 rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](z, 1 + x + (1 + (1 + n1) + y2), z'', 1 + rewrite(y2) + (1 + n1)) :|: z'' >= 0, x >= 0, z' = 1 + x + (1 + (1 + n1) + y2), n1 >= 0, y2 >= 0, z >= 0 rewrite[Let](z, z', z'') -{ 1 }-> rewrite[Let][Let](z, 1 + x + (1 + (1 + x'' + y3) + y'1), z'', rewrite[Let](1 + (1 + x'' + y3) + y'1, 1 + x'' + y3, rewrite(x''))) :|: z'' >= 0, x >= 0, y'1 >= 0, y3 >= 0, z' = 1 + x + (1 + (1 + x'' + y3) + y'1), x'' >= 0, z >= 0 rewrite[Let](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0 rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> rewrite[Let][Let][Let](1 + x + y, z'', z1, 0) :|: z'' >= 0, z = 1 + x + y, z1 >= 0, z' >= 0, x >= 0, y >= 0 rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + n4), z'', z1, 1 + n4) :|: z = 1 + x + (1 + n4), n4 >= 0, z'' >= 0, z1 >= 0, z' >= 0, x >= 0 rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + (1 + n3) + y4), z'', z1, 1 + rewrite(y4) + (1 + n3)) :|: z'' >= 0, z1 >= 0, z' >= 0, x >= 0, y4 >= 0, z = 1 + x + (1 + (1 + n3) + y4), n3 >= 0 rewrite[Let][Let](z, z', z'', z1) -{ 1 }-> rewrite[Let][Let][Let](1 + x + (1 + (1 + x1 + y5) + y'2), z'', z1, rewrite[Let](1 + (1 + x1 + y5) + y'2, 1 + x1 + y5, rewrite(x1))) :|: y5 >= 0, x1 >= 0, z'' >= 0, z1 >= 0, y'2 >= 0, z' >= 0, x >= 0, z = 1 + x + (1 + (1 + x1 + y5) + y'2) rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + z' + (1 + z'' + rewrite[Let](1 + (1 + x2 + y7) + y'3, 1 + x2 + y7, rewrite(x2)))) :|: z' >= 0, z'' >= 0, y7 >= 0, y'3 >= 0, z1 = 1 + (1 + x2 + y7) + y'3, z >= 0, x2 >= 0 rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> rewrite(1 + z' + (1 + z'' + 0)) :|: z' >= 0, z'' >= 0, z1 >= 0, z >= 0 rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + z' + (1 + z'' + (1 + (z1 - 1)))) :|: z' >= 0, z'' >= 0, z1 - 1 >= 0, z >= 0 rewrite[Let][Let][Let](z, z', z'', z1) -{ 1 }-> rewrite(1 + z' + (1 + z'' + (1 + rewrite(y6) + (1 + n5)))) :|: z' >= 0, z'' >= 0, y6 >= 0, n5 >= 0, z1 = 1 + (1 + n5) + y6, z >= 0 rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 second(z) -{ 1 }-> y :|: z = 1 + x + y, x >= 0, y >= 0 ---------------------------------------- (19) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: rewrite[Let](v0, v1, v2) -> null_rewrite[Let] [0] rewrite[Let][Let](v0, v1, v2, v3) -> null_rewrite[Let][Let] [0] rewrite[Let][Let][Let](v0, v1, v2, v3) -> null_rewrite[Let][Let][Let] [0] rewrite(v0) -> null_rewrite [0] second(v0) -> null_second [0] isOp(v0) -> null_isOp [0] first(v0) -> null_first [0] And the following fresh constants: null_rewrite[Let], null_rewrite[Let][Let], null_rewrite[Let][Let][Let], null_rewrite, null_second, null_isOp, null_first, const ---------------------------------------- (20) Obligation: Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: rewrite(Op(Val(n), y)) -> Op(rewrite(y), Val(n)) [1] rewrite(Op(Op(x, y), y')) -> rewrite[Let](Op(Op(x, y), y'), Op(x, y), rewrite(x)) [1] rewrite(Val(n)) -> Val(n) [1] second(Op(x, y)) -> y [1] isOp(Val(n)) -> False [1] isOp(Op(x, y)) -> True [1] first(Val(n)) -> Val(n) [1] first(Op(x, y)) -> x [1] assrewrite(exp) -> rewrite(exp) [1] rewrite[Let](exp, Op(x, y), a1) -> rewrite[Let][Let](exp, Op(x, y), a1, rewrite(y)) [0] rewrite[Let][Let](Op(x, y), opab, a1, b1) -> rewrite[Let][Let][Let](Op(x, y), a1, b1, rewrite(y)) [0] rewrite[Let][Let][Let](exp, a1, b1, c1) -> rewrite(Op(a1, Op(b1, rewrite(c1)))) [0] rewrite[Let](v0, v1, v2) -> null_rewrite[Let] [0] rewrite[Let][Let](v0, v1, v2, v3) -> null_rewrite[Let][Let] [0] rewrite[Let][Let][Let](v0, v1, v2, v3) -> null_rewrite[Let][Let][Let] [0] rewrite(v0) -> null_rewrite [0] second(v0) -> null_second [0] isOp(v0) -> null_isOp [0] first(v0) -> null_first [0] The TRS has the following type information: rewrite :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first Op :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first Val :: a -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first rewrite[Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first second :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first isOp :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> False:True:null_isOp False :: False:True:null_isOp True :: False:True:null_isOp first :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first assrewrite :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first rewrite[Let][Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first rewrite[Let][Let][Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first -> Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first null_rewrite[Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first null_rewrite[Let][Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first null_rewrite[Let][Let][Let] :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first null_rewrite :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first null_second :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first null_isOp :: False:True:null_isOp null_first :: Val:Op:null_rewrite[Let]:null_rewrite[Let][Let]:null_rewrite[Let][Let][Let]:null_rewrite:null_second:null_first const :: a Rewrite Strategy: INNERMOST ---------------------------------------- (21) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: False => 1 True => 2 null_rewrite[Let] => 0 null_rewrite[Let][Let] => 0 null_rewrite[Let][Let][Let] => 0 null_rewrite => 0 null_second => 0 null_isOp => 0 null_first => 0 const => 0 ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: assrewrite(z) -{ 1 }-> rewrite(exp) :|: z = exp, exp >= 0 first(z) -{ 1 }-> x :|: z = 1 + x + y, x >= 0, y >= 0 first(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 first(z) -{ 1 }-> 1 + n :|: n >= 0, z = 1 + n isOp(z) -{ 1 }-> 2 :|: z = 1 + x + y, x >= 0, y >= 0 isOp(z) -{ 1 }-> 1 :|: n >= 0, z = 1 + n isOp(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 rewrite(z) -{ 1 }-> rewrite[Let](1 + (1 + x + y) + y', 1 + x + y, rewrite(x)) :|: x >= 0, y >= 0, y' >= 0, z = 1 + (1 + x + y) + y' rewrite(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 rewrite(z) -{ 1 }-> 1 + n :|: n >= 0, z = 1 + n rewrite(z) -{ 1 }-> 1 + rewrite(y) + (1 + n) :|: n >= 0, y >= 0, z = 1 + (1 + n) + y rewrite[Let](z, z', z'') -{ 0 }-> rewrite[Let][Let](exp, 1 + x + y, a1, rewrite(y)) :|: a1 >= 0, z' = 1 + x + y, x >= 0, y >= 0, z = exp, z'' = a1, exp >= 0 rewrite[Let](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> rewrite[Let][Let][Let](1 + x + y, a1, b1, rewrite(y)) :|: a1 >= 0, z = 1 + x + y, z1 = b1, b1 >= 0, opab >= 0, x >= 0, y >= 0, z' = opab, z'' = a1 rewrite[Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0 rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> rewrite(1 + a1 + (1 + b1 + rewrite(c1))) :|: a1 >= 0, b1 >= 0, z1 = c1, z = exp, c1 >= 0, z'' = b1, z' = a1, exp >= 0 rewrite[Let][Let][Let](z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0 second(z) -{ 1 }-> y :|: z = 1 + x + y, x >= 0, y >= 0 second(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (23) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2)) rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1)) rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3)))) rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0)) rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)) rewrite(Val(z0)) -> Val(z0) second(Op(z0, z1)) -> z1 isOp(Val(z0)) -> False isOp(Op(z0, z1)) -> True first(Val(z0)) -> Val(z0) first(Op(z0, z1)) -> z0 assrewrite(z0) -> rewrite(z0) Tuples: REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2)) REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1)) REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3)) REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 SECOND(Op(z0, z1)) -> c6 ISOP(Val(z0)) -> c7 ISOP(Op(z0, z1)) -> c8 FIRST(Val(z0)) -> c9 FIRST(Op(z0, z1)) -> c10 ASSREWRITE(z0) -> c11(REWRITE(z0)) S tuples: REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 SECOND(Op(z0, z1)) -> c6 ISOP(Val(z0)) -> c7 ISOP(Op(z0, z1)) -> c8 FIRST(Val(z0)) -> c9 FIRST(Op(z0, z1)) -> c10 ASSREWRITE(z0) -> c11(REWRITE(z0)) K tuples:none Defined Rule Symbols: rewrite_1, second_1, isOp_1, first_1, assrewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4 Defined Pair Symbols: REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4, REWRITE_1, SECOND_1, ISOP_1, FIRST_1, ASSREWRITE_1 Compound Symbols: c_2, c1_2, c2_2, c3_1, c4_2, c5, c6, c7, c8, c9, c10, c11_1 ---------------------------------------- (25) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: ASSREWRITE(z0) -> c11(REWRITE(z0)) Removed 5 trailing nodes: ISOP(Op(z0, z1)) -> c8 FIRST(Val(z0)) -> c9 FIRST(Op(z0, z1)) -> c10 SECOND(Op(z0, z1)) -> c6 ISOP(Val(z0)) -> c7 ---------------------------------------- (26) Obligation: Complexity Dependency Tuples Problem Rules: rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2)) rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1)) rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3)))) rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0)) rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)) rewrite(Val(z0)) -> Val(z0) second(Op(z0, z1)) -> z1 isOp(Val(z0)) -> False isOp(Op(z0, z1)) -> True first(Val(z0)) -> Val(z0) first(Op(z0, z1)) -> z0 assrewrite(z0) -> rewrite(z0) Tuples: REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2)) REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1)) REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3)) REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 S tuples: REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 K tuples:none Defined Rule Symbols: rewrite_1, second_1, isOp_1, first_1, assrewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4 Defined Pair Symbols: REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4, REWRITE_1 Compound Symbols: c_2, c1_2, c2_2, c3_1, c4_2, c5 ---------------------------------------- (27) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: second(Op(z0, z1)) -> z1 isOp(Val(z0)) -> False isOp(Op(z0, z1)) -> True first(Val(z0)) -> Val(z0) first(Op(z0, z1)) -> z0 assrewrite(z0) -> rewrite(z0) ---------------------------------------- (28) Obligation: Complexity Dependency Tuples Problem Rules: rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0)) rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)) rewrite(Val(z0)) -> Val(z0) rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2)) rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1)) rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3)))) Tuples: REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2)) REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1)) REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3)) REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 S tuples: REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 K tuples:none Defined Rule Symbols: rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4 Defined Pair Symbols: REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4, REWRITE_1 Compound Symbols: c_2, c1_2, c2_2, c3_1, c4_2, c5 ---------------------------------------- (29) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace REWRITE[LET](z0, Op(z1, z2), z3) -> c(REWRITE[LET][LET](z0, Op(z1, z2), z3, rewrite(z2)), REWRITE(z2)) by REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1)) ---------------------------------------- (30) Obligation: Complexity Dependency Tuples Problem Rules: rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0)) rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)) rewrite(Val(z0)) -> Val(z0) rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2)) rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1)) rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3)))) Tuples: REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1)) REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3)) REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1)) S tuples: REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 K tuples:none Defined Rule Symbols: rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4 Defined Pair Symbols: REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4, REWRITE_1, REWRITE[LET]_3 Compound Symbols: c1_2, c2_2, c3_1, c4_2, c5, c_2 ---------------------------------------- (31) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace REWRITE[LET][LET](Op(z0, z1), z2, z3, z4) -> c1(REWRITE[LET][LET][LET](Op(z0, z1), z3, z4, rewrite(z1)), REWRITE(z1)) by REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), x3, y0) -> c1(REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, y0, rewrite(x2)), REWRITE(x2)) ---------------------------------------- (32) Obligation: Complexity Dependency Tuples Problem Rules: rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0)) rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)) rewrite(Val(z0)) -> Val(z0) rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2)) rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1)) rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3)))) Tuples: REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3)) REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1)) REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), x3, y0) -> c1(REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, y0, rewrite(x2)), REWRITE(x2)) S tuples: REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 K tuples:none Defined Rule Symbols: rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4 Defined Pair Symbols: REWRITE[LET][LET][LET]_4, REWRITE_1, REWRITE[LET]_3, REWRITE[LET][LET]_4 Compound Symbols: c2_2, c3_1, c4_2, c5, c_2, c1_2 ---------------------------------------- (33) CdtInstantiationProof (BOTH BOUNDS(ID, ID)) Use instantiation to replace REWRITE[LET][LET][LET](z0, z1, z2, z3) -> c2(REWRITE(Op(z1, Op(z2, rewrite(z3)))), REWRITE(z3)) by REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, x4, y0) -> c2(REWRITE(Op(x3, Op(x4, rewrite(y0)))), REWRITE(y0)) ---------------------------------------- (34) Obligation: Complexity Dependency Tuples Problem Rules: rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0)) rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)) rewrite(Val(z0)) -> Val(z0) rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2)) rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1)) rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3)))) Tuples: REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1)) REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), x3, y0) -> c1(REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, y0, rewrite(x2)), REWRITE(x2)) REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, x4, y0) -> c2(REWRITE(Op(x3, Op(x4, rewrite(y0)))), REWRITE(y0)) S tuples: REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 K tuples:none Defined Rule Symbols: rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4 Defined Pair Symbols: REWRITE_1, REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4 Compound Symbols: c3_1, c4_2, c5, c_2, c1_2, c2_2 ---------------------------------------- (35) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace REWRITE(Op(Val(z0), z1)) -> c3(REWRITE(z1)) by REWRITE(Op(Val(z0), Op(Val(y0), y1))) -> c3(REWRITE(Op(Val(y0), y1))) REWRITE(Op(Val(z0), Op(Op(y0, y1), y2))) -> c3(REWRITE(Op(Op(y0, y1), y2))) REWRITE(Op(Val(z0), Val(y0))) -> c3(REWRITE(Val(y0))) ---------------------------------------- (36) Obligation: Complexity Dependency Tuples Problem Rules: rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0)) rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)) rewrite(Val(z0)) -> Val(z0) rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2)) rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1)) rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3)))) Tuples: REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1)) REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), x3, y0) -> c1(REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, y0, rewrite(x2)), REWRITE(x2)) REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, x4, y0) -> c2(REWRITE(Op(x3, Op(x4, rewrite(y0)))), REWRITE(y0)) REWRITE(Op(Val(z0), Op(Val(y0), y1))) -> c3(REWRITE(Op(Val(y0), y1))) REWRITE(Op(Val(z0), Op(Op(y0, y1), y2))) -> c3(REWRITE(Op(Op(y0, y1), y2))) REWRITE(Op(Val(z0), Val(y0))) -> c3(REWRITE(Val(y0))) S tuples: REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 REWRITE(Op(Val(z0), Op(Val(y0), y1))) -> c3(REWRITE(Op(Val(y0), y1))) REWRITE(Op(Val(z0), Op(Op(y0, y1), y2))) -> c3(REWRITE(Op(Op(y0, y1), y2))) REWRITE(Op(Val(z0), Val(y0))) -> c3(REWRITE(Val(y0))) K tuples:none Defined Rule Symbols: rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4 Defined Pair Symbols: REWRITE_1, REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4 Compound Symbols: c4_2, c5, c_2, c1_2, c2_2, c3_1 ---------------------------------------- (37) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID)) Use forward instantiation to replace REWRITE(Op(Val(z0), Op(Val(y0), y1))) -> c3(REWRITE(Op(Val(y0), y1))) by REWRITE(Op(Val(z0), Op(Val(z1), Op(Val(y1), y2)))) -> c3(REWRITE(Op(Val(z1), Op(Val(y1), y2)))) REWRITE(Op(Val(z0), Op(Val(z1), Op(Op(y1, y2), y3)))) -> c3(REWRITE(Op(Val(z1), Op(Op(y1, y2), y3)))) REWRITE(Op(Val(z0), Op(Val(z1), Val(y1)))) -> c3(REWRITE(Op(Val(z1), Val(y1)))) ---------------------------------------- (38) Obligation: Complexity Dependency Tuples Problem Rules: rewrite(Op(Val(z0), z1)) -> Op(rewrite(z1), Val(z0)) rewrite(Op(Op(z0, z1), z2)) -> rewrite[Let](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)) rewrite(Val(z0)) -> Val(z0) rewrite[Let](z0, Op(z1, z2), z3) -> rewrite[Let][Let](z0, Op(z1, z2), z3, rewrite(z2)) rewrite[Let][Let](Op(z0, z1), z2, z3, z4) -> rewrite[Let][Let][Let](Op(z0, z1), z3, z4, rewrite(z1)) rewrite[Let][Let][Let](z0, z1, z2, z3) -> rewrite(Op(z1, Op(z2, rewrite(z3)))) Tuples: REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 REWRITE[LET](Op(Op(x0, x1), x2), Op(x0, x1), y0) -> c(REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), y0, rewrite(x1)), REWRITE(x1)) REWRITE[LET][LET](Op(Op(x0, x1), x2), Op(x0, x1), x3, y0) -> c1(REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, y0, rewrite(x2)), REWRITE(x2)) REWRITE[LET][LET][LET](Op(Op(x0, x1), x2), x3, x4, y0) -> c2(REWRITE(Op(x3, Op(x4, rewrite(y0)))), REWRITE(y0)) REWRITE(Op(Val(z0), Op(Op(y0, y1), y2))) -> c3(REWRITE(Op(Op(y0, y1), y2))) REWRITE(Op(Val(z0), Val(y0))) -> c3(REWRITE(Val(y0))) REWRITE(Op(Val(z0), Op(Val(z1), Op(Val(y1), y2)))) -> c3(REWRITE(Op(Val(z1), Op(Val(y1), y2)))) REWRITE(Op(Val(z0), Op(Val(z1), Op(Op(y1, y2), y3)))) -> c3(REWRITE(Op(Val(z1), Op(Op(y1, y2), y3)))) REWRITE(Op(Val(z0), Op(Val(z1), Val(y1)))) -> c3(REWRITE(Op(Val(z1), Val(y1)))) S tuples: REWRITE(Op(Op(z0, z1), z2)) -> c4(REWRITE[LET](Op(Op(z0, z1), z2), Op(z0, z1), rewrite(z0)), REWRITE(z0)) REWRITE(Val(z0)) -> c5 REWRITE(Op(Val(z0), Op(Op(y0, y1), y2))) -> c3(REWRITE(Op(Op(y0, y1), y2))) REWRITE(Op(Val(z0), Val(y0))) -> c3(REWRITE(Val(y0))) REWRITE(Op(Val(z0), Op(Val(z1), Op(Val(y1), y2)))) -> c3(REWRITE(Op(Val(z1), Op(Val(y1), y2)))) REWRITE(Op(Val(z0), Op(Val(z1), Op(Op(y1, y2), y3)))) -> c3(REWRITE(Op(Val(z1), Op(Op(y1, y2), y3)))) REWRITE(Op(Val(z0), Op(Val(z1), Val(y1)))) -> c3(REWRITE(Op(Val(z1), Val(y1)))) K tuples:none Defined Rule Symbols: rewrite_1, rewrite[Let]_3, rewrite[Let][Let]_4, rewrite[Let][Let][Let]_4 Defined Pair Symbols: REWRITE_1, REWRITE[LET]_3, REWRITE[LET][LET]_4, REWRITE[LET][LET][LET]_4 Compound Symbols: c4_2, c5, c_2, c1_2, c2_2, c3_1