tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list tct-trs: Prelude.head: empty list WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) FROM(edge(z0,z1,z2)) -> c10() IF1(false(),z0,z1,z2,z3,z4,z5,z6) -> c19(IF2(z0,z1,z2,z3,z4,z5,z6)) IF1(true(),z0,z1,z2,z3,z4,z5,z6) -> c18() IF2(false(),z0,z1,z2,z3,z4,z5) -> c21(IF3(z0,z1,z2,z3,z4,z5)) IF2(true(),z0,z1,z2,z3,z4,z5) -> c20() IF3(false(),z0,z1,z2,z3,z4) -> c22(REACH(z1,z2,rest(z3),edge(from(z3),to(z3),z4)),REST(z3)) IF3(false(),z0,z1,z2,z3,z4) -> c23(REACH(z1,z2,rest(z3),edge(from(z3),to(z3),z4)),FROM(z3)) IF3(false(),z0,z1,z2,z3,z4) -> c24(REACH(z1,z2,rest(z3),edge(from(z3),to(z3),z4)),TO(z3)) IF3(true(),z0,z1,z2,z3,z4) -> c25(IF4(z0,z1,z2,z3,z4)) IF4(false(),z0,z1,z2,z3) -> c27(OR(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) ,REACH(z0,z1,rest(z2),z3) ,REST(z2)) IF4(false(),z0,z1,z2,z3) -> c28(OR(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) ,REACH(to(z2),z1,union(rest(z2),z3),empty()) ,TO(z2)) IF4(false(),z0,z1,z2,z3) -> c29(OR(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) ,REACH(to(z2),z1,union(rest(z2),z3),empty()) ,UNION(rest(z2),z3) ,REST(z2)) IF4(true(),z0,z1,z2,z3) -> c26() ISEMPTY(edge(z0,z1,z2)) -> c9() ISEMPTY(empty()) -> c8() OR(false(),z0) -> c5() OR(true(),z0) -> c4() REACH(z0,z1,z2,z3) -> c14(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3),EQ(z0,z1)) REACH(z0,z1,z2,z3) -> c15(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3),ISEMPTY(z2)) REACH(z0,z1,z2,z3) -> c16(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3) ,EQ(z0,from(z2)) ,FROM(z2)) REACH(z0,z1,z2,z3) -> c17(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3) ,EQ(z1,to(z2)) ,TO(z2)) REST(edge(z0,z1,z2)) -> c12() REST(empty()) -> c13() TO(edge(z0,z1,z2)) -> c11() UNION(edge(z0,z1,z2),z3) -> c7(UNION(z2,z3)) UNION(empty(),z0) -> c6() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) from(edge(z0,z1,z2)) -> z0 if1(false(),z0,z1,z2,z3,z4,z5,z6) -> if2(z0,z1,z2,z3,z4,z5,z6) if1(true(),z0,z1,z2,z3,z4,z5,z6) -> true() if2(false(),z0,z1,z2,z3,z4,z5) -> if3(z0,z1,z2,z3,z4,z5) if2(true(),z0,z1,z2,z3,z4,z5) -> false() if3(false(),z0,z1,z2,z3,z4) -> reach(z1,z2,rest(z3),edge(from(z3),to(z3),z4)) if3(true(),z0,z1,z2,z3,z4) -> if4(z0,z1,z2,z3,z4) if4(false(),z0,z1,z2,z3) -> or(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) if4(true(),z0,z1,z2,z3) -> true() isEmpty(edge(z0,z1,z2)) -> false() isEmpty(empty()) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,z2,z3) -> if1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3) rest(edge(z0,z1,z2)) -> z2 rest(empty()) -> empty() to(edge(z0,z1,z2)) -> z1 union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,FROM/1,IF1/8,IF2/7,IF3/6,IF4/5,ISEMPTY/1,OR/2,REACH/4,REST/1,TO/1,UNION/2,eq/2,from/1,if1/8,if2/7 ,if3/6,if4/5,isEmpty/1,or/2,reach/4,rest/1,to/1,union/2} / {0/0,c/0,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2 ,c16/3,c17/3,c18/0,c19/1,c2/0,c20/0,c21/1,c22/2,c23/2,c24/2,c25/1,c26/0,c27/3,c28/3,c29/4,c3/1,c4/0,c5/0 ,c6/0,c7/1,c8/0,c9/0,edge/3,empty/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ,FROM,IF1,IF2,IF3,IF4,ISEMPTY,OR,REACH,REST,TO,UNION,eq ,from,if1,if2,if3,if4,isEmpty,or,reach,rest,to,union} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16 ,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c4,c5,c6,c7,c8,c9,edge,empty,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) FROM(edge(z0,z1,z2)) -> c10() IF1(false(),z0,z1,z2,z3,z4,z5,z6) -> c19(IF2(z0,z1,z2,z3,z4,z5,z6)) IF1(true(),z0,z1,z2,z3,z4,z5,z6) -> c18() IF2(false(),z0,z1,z2,z3,z4,z5) -> c21(IF3(z0,z1,z2,z3,z4,z5)) IF2(true(),z0,z1,z2,z3,z4,z5) -> c20() IF3(false(),z0,z1,z2,z3,z4) -> c22(REACH(z1,z2,rest(z3),edge(from(z3),to(z3),z4)),REST(z3)) IF3(false(),z0,z1,z2,z3,z4) -> c23(REACH(z1,z2,rest(z3),edge(from(z3),to(z3),z4)),FROM(z3)) IF3(false(),z0,z1,z2,z3,z4) -> c24(REACH(z1,z2,rest(z3),edge(from(z3),to(z3),z4)),TO(z3)) IF3(true(),z0,z1,z2,z3,z4) -> c25(IF4(z0,z1,z2,z3,z4)) IF4(false(),z0,z1,z2,z3) -> c27(OR(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) ,REACH(z0,z1,rest(z2),z3) ,REST(z2)) IF4(false(),z0,z1,z2,z3) -> c28(OR(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) ,REACH(to(z2),z1,union(rest(z2),z3),empty()) ,TO(z2)) IF4(false(),z0,z1,z2,z3) -> c29(OR(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) ,REACH(to(z2),z1,union(rest(z2),z3),empty()) ,UNION(rest(z2),z3) ,REST(z2)) IF4(true(),z0,z1,z2,z3) -> c26() ISEMPTY(edge(z0,z1,z2)) -> c9() ISEMPTY(empty()) -> c8() OR(false(),z0) -> c5() OR(true(),z0) -> c4() REACH(z0,z1,z2,z3) -> c14(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3),EQ(z0,z1)) REACH(z0,z1,z2,z3) -> c15(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3),ISEMPTY(z2)) REACH(z0,z1,z2,z3) -> c16(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3) ,EQ(z0,from(z2)) ,FROM(z2)) REACH(z0,z1,z2,z3) -> c17(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3) ,EQ(z1,to(z2)) ,TO(z2)) REST(edge(z0,z1,z2)) -> c12() REST(empty()) -> c13() TO(edge(z0,z1,z2)) -> c11() UNION(edge(z0,z1,z2),z3) -> c7(UNION(z2,z3)) UNION(empty(),z0) -> c6() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) from(edge(z0,z1,z2)) -> z0 if1(false(),z0,z1,z2,z3,z4,z5,z6) -> if2(z0,z1,z2,z3,z4,z5,z6) if1(true(),z0,z1,z2,z3,z4,z5,z6) -> true() if2(false(),z0,z1,z2,z3,z4,z5) -> if3(z0,z1,z2,z3,z4,z5) if2(true(),z0,z1,z2,z3,z4,z5) -> false() if3(false(),z0,z1,z2,z3,z4) -> reach(z1,z2,rest(z3),edge(from(z3),to(z3),z4)) if3(true(),z0,z1,z2,z3,z4) -> if4(z0,z1,z2,z3,z4) if4(false(),z0,z1,z2,z3) -> or(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) if4(true(),z0,z1,z2,z3) -> true() isEmpty(edge(z0,z1,z2)) -> false() isEmpty(empty()) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,z2,z3) -> if1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3) rest(edge(z0,z1,z2)) -> z2 rest(empty()) -> empty() to(edge(z0,z1,z2)) -> z1 union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,FROM/1,IF1/8,IF2/7,IF3/6,IF4/5,ISEMPTY/1,OR/2,REACH/4,REST/1,TO/1,UNION/2,eq/2,from/1,if1/8,if2/7 ,if3/6,if4/5,isEmpty/1,or/2,reach/4,rest/1,to/1,union/2} / {0/0,c/0,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2 ,c16/3,c17/3,c18/0,c19/1,c2/0,c20/0,c21/1,c22/2,c23/2,c24/2,c25/1,c26/0,c27/3,c28/3,c29/4,c3/1,c4/0,c5/0 ,c6/0,c7/1,c8/0,c9/0,edge/3,empty/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ,FROM,IF1,IF2,IF3,IF4,ISEMPTY,OR,REACH,REST,TO,UNION,eq ,from,if1,if2,if3,if4,isEmpty,or,reach,rest,to,union} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16 ,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c4,c5,c6,c7,c8,c9,edge,empty,false,s,true} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: EQ(0(),0()) -> c() EQ(0(),s(z0)) -> c1() EQ(s(z0),0()) -> c2() EQ(s(z0),s(z1)) -> c3(EQ(z0,z1)) FROM(edge(z0,z1,z2)) -> c10() IF1(false(),z0,z1,z2,z3,z4,z5,z6) -> c19(IF2(z0,z1,z2,z3,z4,z5,z6)) IF1(true(),z0,z1,z2,z3,z4,z5,z6) -> c18() IF2(false(),z0,z1,z2,z3,z4,z5) -> c21(IF3(z0,z1,z2,z3,z4,z5)) IF2(true(),z0,z1,z2,z3,z4,z5) -> c20() IF3(false(),z0,z1,z2,z3,z4) -> c22(REACH(z1,z2,rest(z3),edge(from(z3),to(z3),z4)),REST(z3)) IF3(false(),z0,z1,z2,z3,z4) -> c23(REACH(z1,z2,rest(z3),edge(from(z3),to(z3),z4)),FROM(z3)) IF3(false(),z0,z1,z2,z3,z4) -> c24(REACH(z1,z2,rest(z3),edge(from(z3),to(z3),z4)),TO(z3)) IF3(true(),z0,z1,z2,z3,z4) -> c25(IF4(z0,z1,z2,z3,z4)) IF4(false(),z0,z1,z2,z3) -> c27(OR(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) ,REACH(z0,z1,rest(z2),z3) ,REST(z2)) IF4(false(),z0,z1,z2,z3) -> c28(OR(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) ,REACH(to(z2),z1,union(rest(z2),z3),empty()) ,TO(z2)) IF4(false(),z0,z1,z2,z3) -> c29(OR(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) ,REACH(to(z2),z1,union(rest(z2),z3),empty()) ,UNION(rest(z2),z3) ,REST(z2)) IF4(true(),z0,z1,z2,z3) -> c26() ISEMPTY(edge(z0,z1,z2)) -> c9() ISEMPTY(empty()) -> c8() OR(false(),z0) -> c5() OR(true(),z0) -> c4() REACH(z0,z1,z2,z3) -> c14(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3),EQ(z0,z1)) REACH(z0,z1,z2,z3) -> c15(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3),ISEMPTY(z2)) REACH(z0,z1,z2,z3) -> c16(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3) ,EQ(z0,from(z2)) ,FROM(z2)) REACH(z0,z1,z2,z3) -> c17(IF1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3) ,EQ(z1,to(z2)) ,TO(z2)) REST(edge(z0,z1,z2)) -> c12() REST(empty()) -> c13() TO(edge(z0,z1,z2)) -> c11() UNION(edge(z0,z1,z2),z3) -> c7(UNION(z2,z3)) UNION(empty(),z0) -> c6() - Weak TRS: eq(0(),0()) -> true() eq(0(),s(z0)) -> false() eq(s(z0),0()) -> false() eq(s(z0),s(z1)) -> eq(z0,z1) from(edge(z0,z1,z2)) -> z0 if1(false(),z0,z1,z2,z3,z4,z5,z6) -> if2(z0,z1,z2,z3,z4,z5,z6) if1(true(),z0,z1,z2,z3,z4,z5,z6) -> true() if2(false(),z0,z1,z2,z3,z4,z5) -> if3(z0,z1,z2,z3,z4,z5) if2(true(),z0,z1,z2,z3,z4,z5) -> false() if3(false(),z0,z1,z2,z3,z4) -> reach(z1,z2,rest(z3),edge(from(z3),to(z3),z4)) if3(true(),z0,z1,z2,z3,z4) -> if4(z0,z1,z2,z3,z4) if4(false(),z0,z1,z2,z3) -> or(reach(z0,z1,rest(z2),z3),reach(to(z2),z1,union(rest(z2),z3),empty())) if4(true(),z0,z1,z2,z3) -> true() isEmpty(edge(z0,z1,z2)) -> false() isEmpty(empty()) -> true() or(false(),z0) -> z0 or(true(),z0) -> true() reach(z0,z1,z2,z3) -> if1(eq(z0,z1),isEmpty(z2),eq(z0,from(z2)),eq(z1,to(z2)),z0,z1,z2,z3) rest(edge(z0,z1,z2)) -> z2 rest(empty()) -> empty() to(edge(z0,z1,z2)) -> z1 union(edge(z0,z1,z2),z3) -> edge(z0,z1,union(z2,z3)) union(empty(),z0) -> z0 - Signature: {EQ/2,FROM/1,IF1/8,IF2/7,IF3/6,IF4/5,ISEMPTY/1,OR/2,REACH/4,REST/1,TO/1,UNION/2,eq/2,from/1,if1/8,if2/7 ,if3/6,if4/5,isEmpty/1,or/2,reach/4,rest/1,to/1,union/2} / {0/0,c/0,c1/0,c10/0,c11/0,c12/0,c13/0,c14/2,c15/2 ,c16/3,c17/3,c18/0,c19/1,c2/0,c20/0,c21/1,c22/2,c23/2,c24/2,c25/1,c26/0,c27/3,c28/3,c29/4,c3/1,c4/0,c5/0 ,c6/0,c7/1,c8/0,c9/0,edge/3,empty/0,false/0,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {EQ,FROM,IF1,IF2,IF3,IF4,ISEMPTY,OR,REACH,REST,TO,UNION,eq ,from,if1,if2,if3,if4,isEmpty,or,reach,rest,to,union} and constructors {0,c,c1,c10,c11,c12,c13,c14,c15,c16 ,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c4,c5,c6,c7,c8,c9,edge,empty,false,s,true} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: EQ(x,y){x -> s(x),y -> s(y)} = EQ(s(x),s(y)) ->^+ c3(EQ(x,y)) = C[EQ(x,y) = EQ(x,y){}] WORST_CASE(Omega(n^1),?)