WORST_CASE(?,O(n^1)) proof of input_fT3CzJFhSE.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). (0) CpxTRS (1) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms] (2) CpxTRS (3) CpxTrsMatchBoundsTAProof [FINISHED, 58 ms] (4) BOUNDS(1, n^1) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: group3(@l) -> group3#1(@l) group3#1(::(@x, @xs)) -> group3#2(@xs, @x) group3#1(nil) -> nil group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) group3#2(nil, @x) -> nil group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) group3#3(nil, @x, @y) -> nil zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) zip3#1(nil, @l2, @l3) -> nil zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) zip3#2(nil, @l3, @x, @xs) -> nil zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) zip3#3(nil, @x, @xs, @y, @ys) -> nil S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) RelTrsToTrsProof (UPPER BOUND(ID)) transformed relative TRS to TRS ---------------------------------------- (2) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: group3(@l) -> group3#1(@l) group3#1(::(@x, @xs)) -> group3#2(@xs, @x) group3#1(nil) -> nil group3#2(::(@y, @ys), @x) -> group3#3(@ys, @x, @y) group3#2(nil, @x) -> nil group3#3(::(@z, @zs), @x, @y) -> ::(tuple#3(@x, @y, @z), group3(@zs)) group3#3(nil, @x, @y) -> nil zip3(@l1, @l2, @l3) -> zip3#1(@l1, @l2, @l3) zip3#1(::(@x, @xs), @l2, @l3) -> zip3#2(@l2, @l3, @x, @xs) zip3#1(nil, @l2, @l3) -> nil zip3#2(::(@y, @ys), @l3, @x, @xs) -> zip3#3(@l3, @x, @xs, @y, @ys) zip3#2(nil, @l3, @x, @xs) -> nil zip3#3(::(@z, @zs), @x, @xs, @y, @ys) -> ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs)) zip3#3(nil, @x, @xs, @y, @ys) -> nil S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) CpxTrsMatchBoundsTAProof (FINISHED) A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 2. The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: final states : [1, 2, 3, 4, 5, 6, 7, 8] transitions: ::0(0, 0) -> 0 nil0() -> 0 tuple#30(0, 0, 0) -> 0 group30(0) -> 1 group3#10(0) -> 2 group3#20(0, 0) -> 3 group3#30(0, 0, 0) -> 4 zip30(0, 0, 0) -> 5 zip3#10(0, 0, 0) -> 6 zip3#20(0, 0, 0, 0) -> 7 zip3#30(0, 0, 0, 0, 0) -> 8 group3#11(0) -> 1 group3#21(0, 0) -> 2 nil1() -> 2 group3#31(0, 0, 0) -> 3 nil1() -> 3 tuple#31(0, 0, 0) -> 9 group31(0) -> 10 ::1(9, 10) -> 4 nil1() -> 4 zip3#11(0, 0, 0) -> 5 zip3#21(0, 0, 0, 0) -> 6 nil1() -> 6 zip3#31(0, 0, 0, 0, 0) -> 7 nil1() -> 7 zip31(0, 0, 0) -> 11 ::1(9, 11) -> 8 nil1() -> 8 group3#12(0) -> 10 group3#21(0, 0) -> 1 nil1() -> 1 group3#31(0, 0, 0) -> 2 ::1(9, 10) -> 3 zip3#12(0, 0, 0) -> 11 zip3#21(0, 0, 0, 0) -> 5 nil1() -> 5 zip3#31(0, 0, 0, 0, 0) -> 6 ::1(9, 11) -> 7 group3#31(0, 0, 0) -> 1 ::1(9, 10) -> 2 zip3#31(0, 0, 0, 0, 0) -> 5 ::1(9, 11) -> 6 group3#21(0, 0) -> 10 nil1() -> 10 zip3#21(0, 0, 0, 0) -> 11 nil1() -> 11 group3#31(0, 0, 0) -> 10 ::1(9, 10) -> 1 zip3#31(0, 0, 0, 0, 0) -> 11 ::1(9, 11) -> 5 ::1(9, 10) -> 10 ::1(9, 11) -> 11 ---------------------------------------- (4) BOUNDS(1, n^1)