WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: CHOICE(cons(z0,z1)) -> c12() CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(0(z0),1(z1)) -> c7() EQ(1(z0),0(z1)) -> c8() EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) EQ(nil(),nil()) -> c5() GUESS(cons(z0,z1)) -> c15(CHOICE(z0)) GUESS(cons(z0,z1)) -> c16(GUESS(z1)) GUESS(nil()) -> c14() IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() MEMBER(z0,cons(z1,z2)) -> c3(IF(eq(z0,z1),true(),member(z0,z2)),EQ(z0,z1)) MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) MEMBER(z0,nil()) -> c2() NEGATE(0(z0)) -> c10() NEGATE(1(z0)) -> c11() SAT(z0) -> c20(SATCK(z0,guess(z0)),GUESS(z0)) SATCK(z0,z1) -> c21(IF(verify(z1),z1,unsat()),VERIFY(z1)) VERIFY(cons(z0,z1)) -> c18(IF(member(negate(z0),z1),false(),verify(z1)),MEMBER(negate(z0),z1),NEGATE(z0)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) VERIFY(nil()) -> c17() - Weak TRS: choice(cons(z0,z1)) -> z0 choice(cons(z0,z1)) -> choice(z1) eq(0(z0),1(z1)) -> false() eq(1(z0),0(z1)) -> false() eq(1(z0),1(z1)) -> eq(z0,z1) eq(O(z0),0(z1)) -> eq(z0,z1) eq(nil(),nil()) -> true() guess(cons(z0,z1)) -> cons(choice(z0),guess(z1)) guess(nil()) -> nil() if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 member(z0,cons(z1,z2)) -> if(eq(z0,z1),true(),member(z0,z2)) member(z0,nil()) -> false() negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) sat(z0) -> satck(z0,guess(z0)) satck(z0,z1) -> if(verify(z1),z1,unsat()) verify(cons(z0,z1)) -> if(member(negate(z0),z1),false(),verify(z1)) verify(nil()) -> true() - Signature: {CHOICE/1,EQ/2,GUESS/1,IF/3,MEMBER/2,NEGATE/1,SAT/1,SATCK/2,VERIFY/1,choice/1,eq/2,guess/1,if/3,member/2 ,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,c/0,c1/0,c10/0,c11/0,c12/0,c13/1,c14/0,c15/1,c16/1,c17/0 ,c18/3,c19/2,c2/0,c20/2,c21/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,true/0,unsat/0} - Obligation: innermost runtime complexity wrt. defined symbols {CHOICE,EQ,GUESS,IF,MEMBER,NEGATE,SAT,SATCK,VERIFY,choice ,eq,guess,if,member,negate,sat,satck,verify} and constructors {0,1,O,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,true,unsat} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: CHOICE(cons(z0,z1)) -> c12() CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(0(z0),1(z1)) -> c7() EQ(1(z0),0(z1)) -> c8() EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) EQ(nil(),nil()) -> c5() GUESS(cons(z0,z1)) -> c15(CHOICE(z0)) GUESS(cons(z0,z1)) -> c16(GUESS(z1)) GUESS(nil()) -> c14() IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() MEMBER(z0,cons(z1,z2)) -> c3(IF(eq(z0,z1),true(),member(z0,z2)),EQ(z0,z1)) MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) MEMBER(z0,nil()) -> c2() NEGATE(0(z0)) -> c10() NEGATE(1(z0)) -> c11() SAT(z0) -> c20(SATCK(z0,guess(z0)),GUESS(z0)) SATCK(z0,z1) -> c21(IF(verify(z1),z1,unsat()),VERIFY(z1)) VERIFY(cons(z0,z1)) -> c18(IF(member(negate(z0),z1),false(),verify(z1)),MEMBER(negate(z0),z1),NEGATE(z0)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) VERIFY(nil()) -> c17() - Weak TRS: choice(cons(z0,z1)) -> z0 choice(cons(z0,z1)) -> choice(z1) eq(0(z0),1(z1)) -> false() eq(1(z0),0(z1)) -> false() eq(1(z0),1(z1)) -> eq(z0,z1) eq(O(z0),0(z1)) -> eq(z0,z1) eq(nil(),nil()) -> true() guess(cons(z0,z1)) -> cons(choice(z0),guess(z1)) guess(nil()) -> nil() if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 member(z0,cons(z1,z2)) -> if(eq(z0,z1),true(),member(z0,z2)) member(z0,nil()) -> false() negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) sat(z0) -> satck(z0,guess(z0)) satck(z0,z1) -> if(verify(z1),z1,unsat()) verify(cons(z0,z1)) -> if(member(negate(z0),z1),false(),verify(z1)) verify(nil()) -> true() - Signature: {CHOICE/1,EQ/2,GUESS/1,IF/3,MEMBER/2,NEGATE/1,SAT/1,SATCK/2,VERIFY/1,choice/1,eq/2,guess/1,if/3,member/2 ,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,c/0,c1/0,c10/0,c11/0,c12/0,c13/1,c14/0,c15/1,c16/1,c17/0 ,c18/3,c19/2,c2/0,c20/2,c21/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,true/0,unsat/0} - Obligation: innermost runtime complexity wrt. defined symbols {CHOICE,EQ,GUESS,IF,MEMBER,NEGATE,SAT,SATCK,VERIFY,choice ,eq,guess,if,member,negate,sat,satck,verify} and constructors {0,1,O,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,true,unsat} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: CHOICE(cons(z0,z1)) -> c12() CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(0(z0),1(z1)) -> c7() EQ(1(z0),0(z1)) -> c8() EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) EQ(nil(),nil()) -> c5() GUESS(cons(z0,z1)) -> c15(CHOICE(z0)) GUESS(cons(z0,z1)) -> c16(GUESS(z1)) GUESS(nil()) -> c14() IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() MEMBER(z0,cons(z1,z2)) -> c3(IF(eq(z0,z1),true(),member(z0,z2)),EQ(z0,z1)) MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) MEMBER(z0,nil()) -> c2() NEGATE(0(z0)) -> c10() NEGATE(1(z0)) -> c11() SAT(z0) -> c20(SATCK(z0,guess(z0)),GUESS(z0)) SATCK(z0,z1) -> c21(IF(verify(z1),z1,unsat()),VERIFY(z1)) VERIFY(cons(z0,z1)) -> c18(IF(member(negate(z0),z1),false(),verify(z1)),MEMBER(negate(z0),z1),NEGATE(z0)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) VERIFY(nil()) -> c17() - Weak TRS: choice(cons(z0,z1)) -> z0 choice(cons(z0,z1)) -> choice(z1) eq(0(z0),1(z1)) -> false() eq(1(z0),0(z1)) -> false() eq(1(z0),1(z1)) -> eq(z0,z1) eq(O(z0),0(z1)) -> eq(z0,z1) eq(nil(),nil()) -> true() guess(cons(z0,z1)) -> cons(choice(z0),guess(z1)) guess(nil()) -> nil() if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 member(z0,cons(z1,z2)) -> if(eq(z0,z1),true(),member(z0,z2)) member(z0,nil()) -> false() negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) sat(z0) -> satck(z0,guess(z0)) satck(z0,z1) -> if(verify(z1),z1,unsat()) verify(cons(z0,z1)) -> if(member(negate(z0),z1),false(),verify(z1)) verify(nil()) -> true() - Signature: {CHOICE/1,EQ/2,GUESS/1,IF/3,MEMBER/2,NEGATE/1,SAT/1,SATCK/2,VERIFY/1,choice/1,eq/2,guess/1,if/3,member/2 ,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,c/0,c1/0,c10/0,c11/0,c12/0,c13/1,c14/0,c15/1,c16/1,c17/0 ,c18/3,c19/2,c2/0,c20/2,c21/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,true/0,unsat/0} - Obligation: innermost runtime complexity wrt. defined symbols {CHOICE,EQ,GUESS,IF,MEMBER,NEGATE,SAT,SATCK,VERIFY,choice ,eq,guess,if,member,negate,sat,satck,verify} and constructors {0,1,O,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,true,unsat} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: CHOICE(y){y -> cons(x,y)} = CHOICE(cons(x,y)) ->^+ c13(CHOICE(y)) = C[CHOICE(y) = CHOICE(y){}] ** Step 1.b:1: Ara. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: CHOICE(cons(z0,z1)) -> c12() CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(0(z0),1(z1)) -> c7() EQ(1(z0),0(z1)) -> c8() EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) EQ(nil(),nil()) -> c5() GUESS(cons(z0,z1)) -> c15(CHOICE(z0)) GUESS(cons(z0,z1)) -> c16(GUESS(z1)) GUESS(nil()) -> c14() IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() MEMBER(z0,cons(z1,z2)) -> c3(IF(eq(z0,z1),true(),member(z0,z2)),EQ(z0,z1)) MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) MEMBER(z0,nil()) -> c2() NEGATE(0(z0)) -> c10() NEGATE(1(z0)) -> c11() SAT(z0) -> c20(SATCK(z0,guess(z0)),GUESS(z0)) SATCK(z0,z1) -> c21(IF(verify(z1),z1,unsat()),VERIFY(z1)) VERIFY(cons(z0,z1)) -> c18(IF(member(negate(z0),z1),false(),verify(z1)),MEMBER(negate(z0),z1),NEGATE(z0)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) VERIFY(nil()) -> c17() - Weak TRS: choice(cons(z0,z1)) -> z0 choice(cons(z0,z1)) -> choice(z1) eq(0(z0),1(z1)) -> false() eq(1(z0),0(z1)) -> false() eq(1(z0),1(z1)) -> eq(z0,z1) eq(O(z0),0(z1)) -> eq(z0,z1) eq(nil(),nil()) -> true() guess(cons(z0,z1)) -> cons(choice(z0),guess(z1)) guess(nil()) -> nil() if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 member(z0,cons(z1,z2)) -> if(eq(z0,z1),true(),member(z0,z2)) member(z0,nil()) -> false() negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) sat(z0) -> satck(z0,guess(z0)) satck(z0,z1) -> if(verify(z1),z1,unsat()) verify(cons(z0,z1)) -> if(member(negate(z0),z1),false(),verify(z1)) verify(nil()) -> true() - Signature: {CHOICE/1,EQ/2,GUESS/1,IF/3,MEMBER/2,NEGATE/1,SAT/1,SATCK/2,VERIFY/1,choice/1,eq/2,guess/1,if/3,member/2 ,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,c/0,c1/0,c10/0,c11/0,c12/0,c13/1,c14/0,c15/1,c16/1,c17/0 ,c18/3,c19/2,c2/0,c20/2,c21/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,true/0,unsat/0} - Obligation: innermost runtime complexity wrt. defined symbols {CHOICE,EQ,GUESS,IF,MEMBER,NEGATE,SAT,SATCK,VERIFY,choice ,eq,guess,if,member,negate,sat,satck,verify} and constructors {0,1,O,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,true,unsat} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "0") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "1") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "CHOICE") :: ["A"(0)] -(1)-> "A"(0) F (TrsFun "EQ") :: ["A"(0) x "A"(0)] -(1)-> "A"(0) F (TrsFun "GUESS") :: ["A"(0)] -(2)-> "A"(0) F (TrsFun "IF") :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "MEMBER") :: ["A"(0) x "A"(0)] -(2)-> "A"(0) F (TrsFun "NEGATE") :: ["A"(0)] -(1)-> "A"(0) F (TrsFun "O") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "SAT") :: ["A"(0)] -(8)-> "A"(0) F (TrsFun "SATCK") :: ["A"(0) x "A"(0)] -(5)-> "A"(0) F (TrsFun "VERIFY") :: ["A"(0)] -(4)-> "A"(0) F (TrsFun "c") :: [] -(0)-> "A"(0) F (TrsFun "c1") :: [] -(0)-> "A"(0) F (TrsFun "c10") :: [] -(0)-> "A"(0) F (TrsFun "c11") :: [] -(0)-> "A"(0) F (TrsFun "c12") :: [] -(0)-> "A"(0) F (TrsFun "c13") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c14") :: [] -(0)-> "A"(0) F (TrsFun "c15") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c16") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c17") :: [] -(0)-> "A"(0) F (TrsFun "c18") :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c19") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c2") :: [] -(0)-> "A"(0) F (TrsFun "c20") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c21") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c3") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c4") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c5") :: [] -(0)-> "A"(0) F (TrsFun "c6") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c7") :: [] -(0)-> "A"(0) F (TrsFun "c8") :: [] -(0)-> "A"(0) F (TrsFun "c9") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "choice") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "eq") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "false") :: [] -(0)-> "A"(0) F (TrsFun "guess") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "if") :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "member") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "negate") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(0) F (TrsFun "sat") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "satck") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "true") :: [] -(0)-> "A"(0) F (TrsFun "unsat") :: [] -(0)-> "A"(0) F (TrsFun "verify") :: ["A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: CHOICE(cons(z0,z1)) -> c12() EQ(0(z0),1(z1)) -> c7() EQ(1(z0),0(z1)) -> c8() EQ(nil(),nil()) -> c5() GUESS(cons(z0,z1)) -> c15(CHOICE(z0)) GUESS(nil()) -> c14() MEMBER(z0,cons(z1,z2)) -> c3(IF(eq(z0,z1),true(),member(z0,z2)),EQ(z0,z1)) MEMBER(z0,nil()) -> c2() NEGATE(0(z0)) -> c10() NEGATE(1(z0)) -> c11() SAT(z0) -> c20(SATCK(z0,guess(z0)),GUESS(z0)) SATCK(z0,z1) -> c21(IF(verify(z1),z1,unsat()),VERIFY(z1)) VERIFY(cons(z0,z1)) -> c18(IF(member(negate(z0),z1),false(),verify(z1)),MEMBER(negate(z0),z1),NEGATE(z0)) VERIFY(nil()) -> c17() 2. Weak: CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) GUESS(cons(z0,z1)) -> c16(GUESS(z1)) IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) ** Step 1.b:2: Ara. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) GUESS(cons(z0,z1)) -> c16(GUESS(z1)) IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) - Weak TRS: CHOICE(cons(z0,z1)) -> c12() EQ(0(z0),1(z1)) -> c7() EQ(1(z0),0(z1)) -> c8() EQ(nil(),nil()) -> c5() GUESS(cons(z0,z1)) -> c15(CHOICE(z0)) GUESS(nil()) -> c14() MEMBER(z0,cons(z1,z2)) -> c3(IF(eq(z0,z1),true(),member(z0,z2)),EQ(z0,z1)) MEMBER(z0,nil()) -> c2() NEGATE(0(z0)) -> c10() NEGATE(1(z0)) -> c11() SAT(z0) -> c20(SATCK(z0,guess(z0)),GUESS(z0)) SATCK(z0,z1) -> c21(IF(verify(z1),z1,unsat()),VERIFY(z1)) VERIFY(cons(z0,z1)) -> c18(IF(member(negate(z0),z1),false(),verify(z1)),MEMBER(negate(z0),z1),NEGATE(z0)) VERIFY(nil()) -> c17() choice(cons(z0,z1)) -> z0 choice(cons(z0,z1)) -> choice(z1) eq(0(z0),1(z1)) -> false() eq(1(z0),0(z1)) -> false() eq(1(z0),1(z1)) -> eq(z0,z1) eq(O(z0),0(z1)) -> eq(z0,z1) eq(nil(),nil()) -> true() guess(cons(z0,z1)) -> cons(choice(z0),guess(z1)) guess(nil()) -> nil() if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 member(z0,cons(z1,z2)) -> if(eq(z0,z1),true(),member(z0,z2)) member(z0,nil()) -> false() negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) sat(z0) -> satck(z0,guess(z0)) satck(z0,z1) -> if(verify(z1),z1,unsat()) verify(cons(z0,z1)) -> if(member(negate(z0),z1),false(),verify(z1)) verify(nil()) -> true() - Signature: {CHOICE/1,EQ/2,GUESS/1,IF/3,MEMBER/2,NEGATE/1,SAT/1,SATCK/2,VERIFY/1,choice/1,eq/2,guess/1,if/3,member/2 ,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,c/0,c1/0,c10/0,c11/0,c12/0,c13/1,c14/0,c15/1,c16/1,c17/0 ,c18/3,c19/2,c2/0,c20/2,c21/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,true/0,unsat/0} - Obligation: innermost runtime complexity wrt. defined symbols {CHOICE,EQ,GUESS,IF,MEMBER,NEGATE,SAT,SATCK,VERIFY,choice ,eq,guess,if,member,negate,sat,satck,verify} and constructors {0,1,O,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,true,unsat} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "0") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "0") :: ["A"(0)] -(0)-> "A"(14) F (TrsFun "1") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "1") :: ["A"(0)] -(0)-> "A"(15) F (TrsFun "CHOICE") :: ["A"(9)] -(7)-> "A"(7) F (TrsFun "EQ") :: ["A"(0) x "A"(0)] -(7)-> "A"(14) F (TrsFun "GUESS") :: ["A"(9)] -(3)-> "A"(15) F (TrsFun "IF") :: ["A"(1) x "A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "MEMBER") :: ["A"(6) x "A"(3)] -(12)-> "A"(10) F (TrsFun "NEGATE") :: ["A"(0)] -(0)-> "A"(3) F (TrsFun "O") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "SAT") :: ["A"(15)] -(15)-> "A"(3) F (TrsFun "SATCK") :: ["A"(0) x "A"(6)] -(11)-> "A"(15) F (TrsFun "VERIFY") :: ["A"(3)] -(11)-> "A"(1) F (TrsFun "c") :: [] -(0)-> "A"(0) F (TrsFun "c1") :: [] -(0)-> "A"(0) F (TrsFun "c10") :: [] -(0)-> "A"(3) F (TrsFun "c11") :: [] -(0)-> "A"(5) F (TrsFun "c12") :: [] -(0)-> "A"(15) F (TrsFun "c13") :: ["A"(7)] -(0)-> "A"(7) F (TrsFun "c14") :: [] -(0)-> "A"(15) F (TrsFun "c15") :: ["A"(0)] -(0)-> "A"(15) F (TrsFun "c16") :: ["A"(15)] -(0)-> "A"(15) F (TrsFun "c17") :: [] -(0)-> "A"(9) F (TrsFun "c18") :: ["A"(0) x "A"(3) x "A"(3)] -(0)-> "A"(3) F (TrsFun "c19") :: ["A"(0) x "A"(0)] -(0)-> "A"(10) F (TrsFun "c2") :: [] -(0)-> "A"(12) F (TrsFun "c20") :: ["A"(15) x "A"(15)] -(0)-> "A"(15) F (TrsFun "c21") :: ["A"(0) x "A"(0)] -(0)-> "A"(15) F (TrsFun "c3") :: ["A"(0) x "A"(10)] -(0)-> "A"(10) F (TrsFun "c4") :: ["A"(0) x "A"(0)] -(0)-> "A"(15) F (TrsFun "c5") :: [] -(0)-> "A"(14) F (TrsFun "c6") :: ["A"(0)] -(0)-> "A"(14) F (TrsFun "c7") :: [] -(0)-> "A"(14) F (TrsFun "c8") :: [] -(0)-> "A"(14) F (TrsFun "c9") :: ["A"(14)] -(0)-> "A"(14) F (TrsFun "choice") :: ["A"(6)] -(0)-> "A"(6) F (TrsFun "cons") :: ["A"(9) x "A"(9)] -(9)-> "A"(9) F (TrsFun "cons") :: ["A"(3) x "A"(3)] -(3)-> "A"(3) F (TrsFun "cons") :: ["A"(6) x "A"(6)] -(6)-> "A"(6) F (TrsFun "cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "eq") :: ["A"(0) x "A"(0)] -(0)-> "A"(10) F (TrsFun "false") :: [] -(0)-> "A"(1) F (TrsFun "false") :: [] -(0)-> "A"(0) F (TrsFun "false") :: [] -(0)-> "A"(8) F (TrsFun "false") :: [] -(0)-> "A"(10) F (TrsFun "false") :: [] -(0)-> "A"(5) F (TrsFun "guess") :: ["A"(6)] -(0)-> "A"(6) F (TrsFun "if") :: ["A"(1) x "A"(1) x "A"(1)] -(0)-> "A"(1) F (TrsFun "member") :: ["A"(0) x "A"(0)] -(0)-> "A"(1) F (TrsFun "negate") :: ["A"(0)] -(0)-> "A"(9) F (TrsFun "nil") :: [] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(9) F (TrsFun "nil") :: [] -(0)-> "A"(3) F (TrsFun "nil") :: [] -(0)-> "A"(6) F (TrsFun "nil") :: [] -(0)-> "A"(8) F (TrsFun "sat") :: ["A"(15)] -(8)-> "A"(0) F (TrsFun "satck") :: ["A"(4) x "A"(2)] -(5)-> "A"(0) F (TrsFun "true") :: [] -(0)-> "A"(1) F (TrsFun "true") :: [] -(0)-> "A"(0) F (TrsFun "true") :: [] -(0)-> "A"(4) F (TrsFun "true") :: [] -(0)-> "A"(10) F (TrsFun "true") :: [] -(0)-> "A"(5) F (TrsFun "unsat") :: [] -(0)-> "A"(2) F (TrsFun "unsat") :: [] -(0)-> "A"(4) F (TrsFun "verify") :: ["A"(0)] -(0)-> "A"(1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"0\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"1\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"O\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c1\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c10\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c11\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c12\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c13\")_A" :: ["A"(1)] -(0)-> "A"(1) "F (TrsFun \"c14\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c15\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c16\")_A" :: ["A"(1)] -(0)-> "A"(1) "F (TrsFun \"c17\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c18\")_A" :: ["A"(0) x "A"(1) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c19\")_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "F (TrsFun \"c2\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c20\")_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c21\")_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "F (TrsFun \"c3\")_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c4\")_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "F (TrsFun \"c5\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c6\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c7\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c8\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c9\")_A" :: ["A"(1)] -(0)-> "A"(1) "F (TrsFun \"cons\")_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"false\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"nil\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"true\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"unsat\")_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: GUESS(cons(z0,z1)) -> c16(GUESS(z1)) 2. Weak: CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) ** Step 1.b:3: Ara. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) - Weak TRS: CHOICE(cons(z0,z1)) -> c12() EQ(0(z0),1(z1)) -> c7() EQ(1(z0),0(z1)) -> c8() EQ(nil(),nil()) -> c5() GUESS(cons(z0,z1)) -> c15(CHOICE(z0)) GUESS(cons(z0,z1)) -> c16(GUESS(z1)) GUESS(nil()) -> c14() MEMBER(z0,cons(z1,z2)) -> c3(IF(eq(z0,z1),true(),member(z0,z2)),EQ(z0,z1)) MEMBER(z0,nil()) -> c2() NEGATE(0(z0)) -> c10() NEGATE(1(z0)) -> c11() SAT(z0) -> c20(SATCK(z0,guess(z0)),GUESS(z0)) SATCK(z0,z1) -> c21(IF(verify(z1),z1,unsat()),VERIFY(z1)) VERIFY(cons(z0,z1)) -> c18(IF(member(negate(z0),z1),false(),verify(z1)),MEMBER(negate(z0),z1),NEGATE(z0)) VERIFY(nil()) -> c17() choice(cons(z0,z1)) -> z0 choice(cons(z0,z1)) -> choice(z1) eq(0(z0),1(z1)) -> false() eq(1(z0),0(z1)) -> false() eq(1(z0),1(z1)) -> eq(z0,z1) eq(O(z0),0(z1)) -> eq(z0,z1) eq(nil(),nil()) -> true() guess(cons(z0,z1)) -> cons(choice(z0),guess(z1)) guess(nil()) -> nil() if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 member(z0,cons(z1,z2)) -> if(eq(z0,z1),true(),member(z0,z2)) member(z0,nil()) -> false() negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) sat(z0) -> satck(z0,guess(z0)) satck(z0,z1) -> if(verify(z1),z1,unsat()) verify(cons(z0,z1)) -> if(member(negate(z0),z1),false(),verify(z1)) verify(nil()) -> true() - Signature: {CHOICE/1,EQ/2,GUESS/1,IF/3,MEMBER/2,NEGATE/1,SAT/1,SATCK/2,VERIFY/1,choice/1,eq/2,guess/1,if/3,member/2 ,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,c/0,c1/0,c10/0,c11/0,c12/0,c13/1,c14/0,c15/1,c16/1,c17/0 ,c18/3,c19/2,c2/0,c20/2,c21/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,true/0,unsat/0} - Obligation: innermost runtime complexity wrt. defined symbols {CHOICE,EQ,GUESS,IF,MEMBER,NEGATE,SAT,SATCK,VERIFY,choice ,eq,guess,if,member,negate,sat,satck,verify} and constructors {0,1,O,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,true,unsat} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "0") :: ["A"(9)] -(9)-> "A"(9) F (TrsFun "0") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "1") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "1") :: ["A"(9)] -(9)-> "A"(9) F (TrsFun "CHOICE") :: ["A"(1)] -(2)-> "A"(4) F (TrsFun "EQ") :: ["A"(0) x "A"(9)] -(3)-> "A"(14) F (TrsFun "GUESS") :: ["A"(2)] -(0)-> "A"(5) F (TrsFun "IF") :: ["A"(0) x "A"(0) x "A"(1)] -(1)-> "A"(14) F (TrsFun "MEMBER") :: ["A"(0) x "A"(13)] -(11)-> "A"(14) F (TrsFun "NEGATE") :: ["A"(0)] -(0)-> "A"(13) F (TrsFun "O") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "SAT") :: ["A"(15)] -(15)-> "A"(1) F (TrsFun "SATCK") :: ["A"(0) x "A"(13)] -(15)-> "A"(3) F (TrsFun "VERIFY") :: ["A"(13)] -(13)-> "A"(5) F (TrsFun "c") :: [] -(0)-> "A"(15) F (TrsFun "c1") :: [] -(0)-> "A"(14) F (TrsFun "c10") :: [] -(0)-> "A"(14) F (TrsFun "c11") :: [] -(0)-> "A"(14) F (TrsFun "c12") :: [] -(0)-> "A"(10) F (TrsFun "c13") :: ["A"(0)] -(0)-> "A"(15) F (TrsFun "c14") :: [] -(0)-> "A"(14) F (TrsFun "c15") :: ["A"(0)] -(0)-> "A"(8) F (TrsFun "c16") :: ["A"(5)] -(0)-> "A"(5) F (TrsFun "c17") :: [] -(0)-> "A"(8) F (TrsFun "c18") :: ["A"(7) x "A"(7) x "A"(7)] -(0)-> "A"(7) F (TrsFun "c19") :: ["A"(5) x "A"(5)] -(0)-> "A"(5) F (TrsFun "c2") :: [] -(0)-> "A"(15) F (TrsFun "c20") :: ["A"(3) x "A"(3)] -(0)-> "A"(3) F (TrsFun "c21") :: ["A"(3) x "A"(3)] -(0)-> "A"(3) F (TrsFun "c3") :: ["A"(0) x "A"(14)] -(0)-> "A"(14) F (TrsFun "c4") :: ["A"(0) x "A"(0)] -(0)-> "A"(15) F (TrsFun "c5") :: [] -(0)-> "A"(14) F (TrsFun "c6") :: ["A"(14)] -(0)-> "A"(14) F (TrsFun "c7") :: [] -(0)-> "A"(14) F (TrsFun "c8") :: [] -(0)-> "A"(14) F (TrsFun "c9") :: ["A"(0)] -(0)-> "A"(14) F (TrsFun "choice") :: ["A"(13)] -(0)-> "A"(13) F (TrsFun "cons") :: ["A"(1) x "A"(1)] -(1)-> "A"(1) F (TrsFun "cons") :: ["A"(13) x "A"(13)] -(13)-> "A"(13) F (TrsFun "cons") :: ["A"(2) x "A"(2)] -(2)-> "A"(2) F (TrsFun "cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "eq") :: ["A"(0) x "A"(0)] -(0)-> "A"(2) F (TrsFun "false") :: [] -(0)-> "A"(0) F (TrsFun "false") :: [] -(0)-> "A"(2) F (TrsFun "false") :: [] -(0)-> "A"(8) F (TrsFun "false") :: [] -(0)-> "A"(6) F (TrsFun "false") :: [] -(0)-> "A"(10) F (TrsFun "false") :: [] -(0)-> "A"(14) F (TrsFun "false") :: [] -(0)-> "A"(13) F (TrsFun "guess") :: ["A"(13)] -(0)-> "A"(13) F (TrsFun "if") :: ["A"(2) x "A"(13) x "A"(13)] -(0)-> "A"(13) F (TrsFun "member") :: ["A"(0) x "A"(0)] -(0)-> "A"(13) F (TrsFun "negate") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(9) F (TrsFun "nil") :: [] -(0)-> "A"(2) F (TrsFun "nil") :: [] -(0)-> "A"(13) F (TrsFun "sat") :: ["A"(15)] -(15)-> "A"(9) F (TrsFun "satck") :: ["A"(0) x "A"(13)] -(15)-> "A"(12) F (TrsFun "true") :: [] -(0)-> "A"(0) F (TrsFun "true") :: [] -(0)-> "A"(2) F (TrsFun "true") :: [] -(0)-> "A"(4) F (TrsFun "true") :: [] -(0)-> "A"(12) F (TrsFun "true") :: [] -(0)-> "A"(14) F (TrsFun "true") :: [] -(0)-> "A"(15) F (TrsFun "true") :: [] -(0)-> "A"(13) F (TrsFun "unsat") :: [] -(0)-> "A"(12) F (TrsFun "unsat") :: [] -(0)-> "A"(13) F (TrsFun "verify") :: ["A"(0)] -(0)-> "A"(13) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"0\")_A" :: ["A"(1)] -(1)-> "A"(1) "F (TrsFun \"1\")_A" :: ["A"(1)] -(1)-> "A"(1) "F (TrsFun \"O\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c1\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c10\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c11\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c12\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c13\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c14\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c15\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c16\")_A" :: ["A"(1)] -(0)-> "A"(1) "F (TrsFun \"c17\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c18\")_A" :: ["A"(1) x "A"(1) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c19\")_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c2\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c20\")_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c21\")_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c3\")_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c4\")_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "F (TrsFun \"c5\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c6\")_A" :: ["A"(1)] -(0)-> "A"(1) "F (TrsFun \"c7\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c8\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c9\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"cons\")_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"false\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"nil\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"true\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"unsat\")_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() 2. Weak: EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) ** Step 1.b:4: Ara. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) - Weak TRS: CHOICE(cons(z0,z1)) -> c12() CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(0(z0),1(z1)) -> c7() EQ(1(z0),0(z1)) -> c8() EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) EQ(nil(),nil()) -> c5() GUESS(cons(z0,z1)) -> c15(CHOICE(z0)) GUESS(cons(z0,z1)) -> c16(GUESS(z1)) GUESS(nil()) -> c14() IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() MEMBER(z0,cons(z1,z2)) -> c3(IF(eq(z0,z1),true(),member(z0,z2)),EQ(z0,z1)) MEMBER(z0,nil()) -> c2() NEGATE(0(z0)) -> c10() NEGATE(1(z0)) -> c11() SAT(z0) -> c20(SATCK(z0,guess(z0)),GUESS(z0)) SATCK(z0,z1) -> c21(IF(verify(z1),z1,unsat()),VERIFY(z1)) VERIFY(cons(z0,z1)) -> c18(IF(member(negate(z0),z1),false(),verify(z1)),MEMBER(negate(z0),z1),NEGATE(z0)) VERIFY(nil()) -> c17() choice(cons(z0,z1)) -> z0 choice(cons(z0,z1)) -> choice(z1) eq(0(z0),1(z1)) -> false() eq(1(z0),0(z1)) -> false() eq(1(z0),1(z1)) -> eq(z0,z1) eq(O(z0),0(z1)) -> eq(z0,z1) eq(nil(),nil()) -> true() guess(cons(z0,z1)) -> cons(choice(z0),guess(z1)) guess(nil()) -> nil() if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 member(z0,cons(z1,z2)) -> if(eq(z0,z1),true(),member(z0,z2)) member(z0,nil()) -> false() negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) sat(z0) -> satck(z0,guess(z0)) satck(z0,z1) -> if(verify(z1),z1,unsat()) verify(cons(z0,z1)) -> if(member(negate(z0),z1),false(),verify(z1)) verify(nil()) -> true() - Signature: {CHOICE/1,EQ/2,GUESS/1,IF/3,MEMBER/2,NEGATE/1,SAT/1,SATCK/2,VERIFY/1,choice/1,eq/2,guess/1,if/3,member/2 ,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,c/0,c1/0,c10/0,c11/0,c12/0,c13/1,c14/0,c15/1,c16/1,c17/0 ,c18/3,c19/2,c2/0,c20/2,c21/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,true/0,unsat/0} - Obligation: innermost runtime complexity wrt. defined symbols {CHOICE,EQ,GUESS,IF,MEMBER,NEGATE,SAT,SATCK,VERIFY,choice ,eq,guess,if,member,negate,sat,satck,verify} and constructors {0,1,O,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,true,unsat} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "0") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "0") :: ["A"(2)] -(2)-> "A"(2) F (TrsFun "1") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "1") :: ["A"(2)] -(2)-> "A"(2) F (TrsFun "CHOICE") :: ["A"(0)] -(1)-> "A"(1) F (TrsFun "EQ") :: ["A"(0) x "A"(2)] -(1)-> "A"(14) F (TrsFun "GUESS") :: ["A"(0)] -(1)-> "A"(2) F (TrsFun "IF") :: ["A"(0) x "A"(1) x "A"(1)] -(1)-> "A"(2) F (TrsFun "MEMBER") :: ["A"(0) x "A"(9)] -(1)-> "A"(7) F (TrsFun "NEGATE") :: ["A"(0)] -(0)-> "A"(8) F (TrsFun "O") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "SAT") :: ["A"(15)] -(15)-> "A"(1) F (TrsFun "SATCK") :: ["A"(0) x "A"(13)] -(14)-> "A"(2) F (TrsFun "VERIFY") :: ["A"(9)] -(3)-> "A"(1) F (TrsFun "c") :: [] -(0)-> "A"(14) F (TrsFun "c1") :: [] -(0)-> "A"(2) F (TrsFun "c10") :: [] -(0)-> "A"(8) F (TrsFun "c11") :: [] -(0)-> "A"(8) F (TrsFun "c12") :: [] -(0)-> "A"(1) F (TrsFun "c13") :: ["A"(0)] -(0)-> "A"(15) F (TrsFun "c14") :: [] -(0)-> "A"(8) F (TrsFun "c15") :: ["A"(0)] -(0)-> "A"(2) F (TrsFun "c16") :: ["A"(0)] -(0)-> "A"(13) F (TrsFun "c17") :: [] -(0)-> "A"(9) F (TrsFun "c18") :: ["A"(0) x "A"(4) x "A"(4)] -(0)-> "A"(4) F (TrsFun "c19") :: ["A"(0) x "A"(0)] -(0)-> "A"(4) F (TrsFun "c2") :: [] -(0)-> "A"(9) F (TrsFun "c20") :: ["A"(2) x "A"(2)] -(0)-> "A"(2) F (TrsFun "c21") :: ["A"(2) x "A"(0)] -(0)-> "A"(2) F (TrsFun "c3") :: ["A"(0) x "A"(8)] -(8)-> "A"(8) F (TrsFun "c4") :: ["A"(0) x "A"(0)] -(0)-> "A"(13) F (TrsFun "c5") :: [] -(0)-> "A"(14) F (TrsFun "c6") :: ["A"(0)] -(0)-> "A"(15) F (TrsFun "c7") :: [] -(0)-> "A"(14) F (TrsFun "c8") :: [] -(0)-> "A"(14) F (TrsFun "c9") :: ["A"(14)] -(0)-> "A"(14) F (TrsFun "choice") :: ["A"(15)] -(1)-> "A"(13) F (TrsFun "cons") :: ["A"(9) x "A"(9)] -(9)-> "A"(9) F (TrsFun "cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "cons") :: ["A"(15) x "A"(15)] -(15)-> "A"(15) F (TrsFun "cons") :: ["A"(13) x "A"(13)] -(13)-> "A"(13) F (TrsFun "eq") :: ["A"(0) x "A"(0)] -(0)-> "A"(14) F (TrsFun "false") :: [] -(0)-> "A"(0) F (TrsFun "false") :: [] -(0)-> "A"(1) F (TrsFun "false") :: [] -(0)-> "A"(8) F (TrsFun "false") :: [] -(0)-> "A"(14) F (TrsFun "false") :: [] -(0)-> "A"(12) F (TrsFun "guess") :: ["A"(15)] -(0)-> "A"(13) F (TrsFun "if") :: ["A"(0) x "A"(8) x "A"(1)] -(0)-> "A"(1) F (TrsFun "member") :: ["A"(0) x "A"(0)] -(0)-> "A"(1) F (TrsFun "negate") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(2) F (TrsFun "nil") :: [] -(0)-> "A"(9) F (TrsFun "nil") :: [] -(0)-> "A"(15) F (TrsFun "sat") :: ["A"(15)] -(12)-> "A"(1) F (TrsFun "satck") :: ["A"(0) x "A"(8)] -(5)-> "A"(1) F (TrsFun "true") :: [] -(0)-> "A"(0) F (TrsFun "true") :: [] -(0)-> "A"(2) F (TrsFun "true") :: [] -(0)-> "A"(4) F (TrsFun "true") :: [] -(0)-> "A"(14) F (TrsFun "true") :: [] -(0)-> "A"(12) F (TrsFun "true") :: [] -(0)-> "A"(9) F (TrsFun "unsat") :: [] -(0)-> "A"(4) F (TrsFun "unsat") :: [] -(0)-> "A"(12) F (TrsFun "verify") :: ["A"(0)] -(0)-> "A"(1) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"0\")_A" :: ["A"(1)] -(1)-> "A"(1) "F (TrsFun \"1\")_A" :: ["A"(1)] -(1)-> "A"(1) "F (TrsFun \"O\")_A" :: ["A"(0)] -(1)-> "A"(1) "F (TrsFun \"c\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c1\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c10\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c11\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c12\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c13\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c14\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c15\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c16\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c17\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c18\")_A" :: ["A"(0) x "A"(1) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c19\")_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "F (TrsFun \"c2\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c20\")_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c21\")_A" :: ["A"(1) x "A"(0)] -(0)-> "A"(1) "F (TrsFun \"c3\")_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"c4\")_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "F (TrsFun \"c5\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c6\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c7\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c8\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c9\")_A" :: ["A"(1)] -(0)-> "A"(1) "F (TrsFun \"cons\")_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"false\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"nil\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"true\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"unsat\")_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) 2. Weak: EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) ** Step 1.b:5: Ara. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) - Weak TRS: CHOICE(cons(z0,z1)) -> c12() CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(0(z0),1(z1)) -> c7() EQ(1(z0),0(z1)) -> c8() EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) EQ(nil(),nil()) -> c5() GUESS(cons(z0,z1)) -> c15(CHOICE(z0)) GUESS(cons(z0,z1)) -> c16(GUESS(z1)) GUESS(nil()) -> c14() IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() MEMBER(z0,cons(z1,z2)) -> c3(IF(eq(z0,z1),true(),member(z0,z2)),EQ(z0,z1)) MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) MEMBER(z0,nil()) -> c2() NEGATE(0(z0)) -> c10() NEGATE(1(z0)) -> c11() SAT(z0) -> c20(SATCK(z0,guess(z0)),GUESS(z0)) SATCK(z0,z1) -> c21(IF(verify(z1),z1,unsat()),VERIFY(z1)) VERIFY(cons(z0,z1)) -> c18(IF(member(negate(z0),z1),false(),verify(z1)),MEMBER(negate(z0),z1),NEGATE(z0)) VERIFY(nil()) -> c17() choice(cons(z0,z1)) -> z0 choice(cons(z0,z1)) -> choice(z1) eq(0(z0),1(z1)) -> false() eq(1(z0),0(z1)) -> false() eq(1(z0),1(z1)) -> eq(z0,z1) eq(O(z0),0(z1)) -> eq(z0,z1) eq(nil(),nil()) -> true() guess(cons(z0,z1)) -> cons(choice(z0),guess(z1)) guess(nil()) -> nil() if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 member(z0,cons(z1,z2)) -> if(eq(z0,z1),true(),member(z0,z2)) member(z0,nil()) -> false() negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) sat(z0) -> satck(z0,guess(z0)) satck(z0,z1) -> if(verify(z1),z1,unsat()) verify(cons(z0,z1)) -> if(member(negate(z0),z1),false(),verify(z1)) verify(nil()) -> true() - Signature: {CHOICE/1,EQ/2,GUESS/1,IF/3,MEMBER/2,NEGATE/1,SAT/1,SATCK/2,VERIFY/1,choice/1,eq/2,guess/1,if/3,member/2 ,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,c/0,c1/0,c10/0,c11/0,c12/0,c13/1,c14/0,c15/1,c16/1,c17/0 ,c18/3,c19/2,c2/0,c20/2,c21/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,true/0,unsat/0} - Obligation: innermost runtime complexity wrt. defined symbols {CHOICE,EQ,GUESS,IF,MEMBER,NEGATE,SAT,SATCK,VERIFY,choice ,eq,guess,if,member,negate,sat,satck,verify} and constructors {0,1,O,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,true,unsat} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "0") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "0") :: ["A"(9)] -(9)-> "A"(9) F (TrsFun "1") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "1") :: ["A"(9)] -(9)-> "A"(9) F (TrsFun "CHOICE") :: ["A"(1)] -(1)-> "A"(0) F (TrsFun "EQ") :: ["A"(0) x "A"(9)] -(1)-> "A"(2) F (TrsFun "GUESS") :: ["A"(1)] -(3)-> "A"(2) F (TrsFun "IF") :: ["A"(1) x "A"(0) x "A"(0)] -(0)-> "A"(5) F (TrsFun "MEMBER") :: ["A"(0) x "A"(11)] -(5)-> "A"(2) F (TrsFun "NEGATE") :: ["A"(0)] -(0)-> "A"(5) F (TrsFun "O") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "SAT") :: ["A"(15)] -(15)-> "A"(1) F (TrsFun "SATCK") :: ["A"(0) x "A"(11)] -(12)-> "A"(0) F (TrsFun "VERIFY") :: ["A"(11)] -(2)-> "A"(13) F (TrsFun "c") :: [] -(0)-> "A"(5) F (TrsFun "c1") :: [] -(0)-> "A"(6) F (TrsFun "c10") :: [] -(0)-> "A"(5) F (TrsFun "c11") :: [] -(0)-> "A"(5) F (TrsFun "c12") :: [] -(0)-> "A"(0) F (TrsFun "c13") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "c14") :: [] -(0)-> "A"(8) F (TrsFun "c15") :: ["A"(0)] -(3)-> "A"(3) F (TrsFun "c16") :: ["A"(0)] -(0)-> "A"(14) F (TrsFun "c17") :: [] -(0)-> "A"(13) F (TrsFun "c18") :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(15) F (TrsFun "c19") :: ["A"(0) x "A"(13)] -(0)-> "A"(13) F (TrsFun "c2") :: [] -(0)-> "A"(8) F (TrsFun "c20") :: ["A"(0) x "A"(2)] -(0)-> "A"(2) F (TrsFun "c21") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "c3") :: ["A"(2) x "A"(2)] -(2)-> "A"(2) F (TrsFun "c4") :: ["A"(0) x "A"(2)] -(0)-> "A"(2) F (TrsFun "c5") :: [] -(0)-> "A"(14) F (TrsFun "c6") :: ["A"(0)] -(8)-> "A"(8) F (TrsFun "c7") :: [] -(0)-> "A"(14) F (TrsFun "c8") :: [] -(0)-> "A"(12) F (TrsFun "c9") :: ["A"(2)] -(2)-> "A"(2) F (TrsFun "choice") :: ["A"(14)] -(0)-> "A"(14) F (TrsFun "cons") :: ["A"(11) x "A"(11)] -(11)-> "A"(11) F (TrsFun "cons") :: ["A"(1) x "A"(1)] -(1)-> "A"(1) F (TrsFun "cons") :: ["A"(14) x "A"(14)] -(14)-> "A"(14) F (TrsFun "cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "eq") :: ["A"(0) x "A"(0)] -(0)-> "A"(4) F (TrsFun "false") :: [] -(0)-> "A"(1) F (TrsFun "false") :: [] -(0)-> "A"(2) F (TrsFun "false") :: [] -(0)-> "A"(0) F (TrsFun "false") :: [] -(0)-> "A"(10) F (TrsFun "false") :: [] -(0)-> "A"(14) F (TrsFun "false") :: [] -(0)-> "A"(8) F (TrsFun "guess") :: ["A"(14)] -(0)-> "A"(11) F (TrsFun "if") :: ["A"(2) x "A"(2) x "A"(2)] -(0)-> "A"(2) F (TrsFun "member") :: ["A"(0) x "A"(0)] -(0)-> "A"(2) F (TrsFun "negate") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(9) F (TrsFun "nil") :: [] -(0)-> "A"(1) F (TrsFun "nil") :: [] -(0)-> "A"(11) F (TrsFun "nil") :: [] -(0)-> "A"(14) F (TrsFun "sat") :: ["A"(15)] -(12)-> "A"(1) F (TrsFun "satck") :: ["A"(0) x "A"(2)] -(3)-> "A"(2) F (TrsFun "true") :: [] -(0)-> "A"(1) F (TrsFun "true") :: [] -(0)-> "A"(2) F (TrsFun "true") :: [] -(0)-> "A"(0) F (TrsFun "true") :: [] -(0)-> "A"(4) F (TrsFun "true") :: [] -(0)-> "A"(8) F (TrsFun "unsat") :: [] -(0)-> "A"(0) F (TrsFun "unsat") :: [] -(0)-> "A"(8) F (TrsFun "verify") :: ["A"(0)] -(2)-> "A"(2) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"0\")_A" :: ["A"(1)] -(1)-> "A"(1) "F (TrsFun \"1\")_A" :: ["A"(1)] -(1)-> "A"(1) "F (TrsFun \"O\")_A" :: ["A"(0)] -(1)-> "A"(1) "F (TrsFun \"c\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c1\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c10\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c11\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c12\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c13\")_A" :: ["A"(1)] -(0)-> "A"(1) "F (TrsFun \"c14\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c15\")_A" :: ["A"(0)] -(1)-> "A"(1) "F (TrsFun \"c16\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c17\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c18\")_A" :: ["A"(0) x "A"(0) x "A"(0)] -(0)-> "A"(1) "F (TrsFun \"c19\")_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c2\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c20\")_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c21\")_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"c3\")_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"c4\")_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c5\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c6\")_A" :: ["A"(0)] -(1)-> "A"(1) "F (TrsFun \"c7\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c8\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c9\")_A" :: ["A"(1)] -(1)-> "A"(1) "F (TrsFun \"cons\")_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"false\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"nil\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"true\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"unsat\")_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) 2. Weak: EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) ** Step 1.b:6: Ara. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) - Weak TRS: CHOICE(cons(z0,z1)) -> c12() CHOICE(cons(z0,z1)) -> c13(CHOICE(z1)) EQ(0(z0),1(z1)) -> c7() EQ(1(z0),0(z1)) -> c8() EQ(O(z0),0(z1)) -> c6(EQ(z0,z1)) EQ(nil(),nil()) -> c5() GUESS(cons(z0,z1)) -> c15(CHOICE(z0)) GUESS(cons(z0,z1)) -> c16(GUESS(z1)) GUESS(nil()) -> c14() IF(false(),z0,z1) -> c1() IF(true(),z0,z1) -> c() MEMBER(z0,cons(z1,z2)) -> c3(IF(eq(z0,z1),true(),member(z0,z2)),EQ(z0,z1)) MEMBER(z0,cons(z1,z2)) -> c4(IF(eq(z0,z1),true(),member(z0,z2)),MEMBER(z0,z2)) MEMBER(z0,nil()) -> c2() NEGATE(0(z0)) -> c10() NEGATE(1(z0)) -> c11() SAT(z0) -> c20(SATCK(z0,guess(z0)),GUESS(z0)) SATCK(z0,z1) -> c21(IF(verify(z1),z1,unsat()),VERIFY(z1)) VERIFY(cons(z0,z1)) -> c18(IF(member(negate(z0),z1),false(),verify(z1)),MEMBER(negate(z0),z1),NEGATE(z0)) VERIFY(cons(z0,z1)) -> c19(IF(member(negate(z0),z1),false(),verify(z1)),VERIFY(z1)) VERIFY(nil()) -> c17() choice(cons(z0,z1)) -> z0 choice(cons(z0,z1)) -> choice(z1) eq(0(z0),1(z1)) -> false() eq(1(z0),0(z1)) -> false() eq(1(z0),1(z1)) -> eq(z0,z1) eq(O(z0),0(z1)) -> eq(z0,z1) eq(nil(),nil()) -> true() guess(cons(z0,z1)) -> cons(choice(z0),guess(z1)) guess(nil()) -> nil() if(false(),z0,z1) -> z1 if(true(),z0,z1) -> z0 member(z0,cons(z1,z2)) -> if(eq(z0,z1),true(),member(z0,z2)) member(z0,nil()) -> false() negate(0(z0)) -> 1(z0) negate(1(z0)) -> 0(z0) sat(z0) -> satck(z0,guess(z0)) satck(z0,z1) -> if(verify(z1),z1,unsat()) verify(cons(z0,z1)) -> if(member(negate(z0),z1),false(),verify(z1)) verify(nil()) -> true() - Signature: {CHOICE/1,EQ/2,GUESS/1,IF/3,MEMBER/2,NEGATE/1,SAT/1,SATCK/2,VERIFY/1,choice/1,eq/2,guess/1,if/3,member/2 ,negate/1,sat/1,satck/2,verify/1} / {0/1,1/1,O/1,c/0,c1/0,c10/0,c11/0,c12/0,c13/1,c14/0,c15/1,c16/1,c17/0 ,c18/3,c19/2,c2/0,c20/2,c21/2,c3/2,c4/2,c5/0,c6/1,c7/0,c8/0,c9/1,cons/2,false/0,nil/0,true/0,unsat/0} - Obligation: innermost runtime complexity wrt. defined symbols {CHOICE,EQ,GUESS,IF,MEMBER,NEGATE,SAT,SATCK,VERIFY,choice ,eq,guess,if,member,negate,sat,satck,verify} and constructors {0,1,O,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c3,c4,c5,c6,c7,c8,c9,cons,false,nil,true,unsat} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1, isBestCase = False, mkCompletelyDefined = False, verboseOutput = False} + Details: Signatures used: ---------------- F (TrsFun "0") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "0") :: ["A"(11)] -(0)-> "A"(11) F (TrsFun "0") :: ["A"(5)] -(0)-> "A"(5) F (TrsFun "1") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "1") :: ["A"(11)] -(11)-> "A"(11) F (TrsFun "1") :: ["A"(5)] -(5)-> "A"(5) F (TrsFun "CHOICE") :: ["A"(1)] -(3)-> "A"(1) F (TrsFun "EQ") :: ["A"(0) x "A"(11)] -(1)-> "A"(6) F (TrsFun "GUESS") :: ["A"(1)] -(3)-> "A"(6) F (TrsFun "IF") :: ["A"(0) x "A"(0) x "A"(2)] -(0)-> "A"(1) F (TrsFun "MEMBER") :: ["A"(0) x "A"(14)] -(10)-> "A"(15) F (TrsFun "NEGATE") :: ["A"(5)] -(0)-> "A"(15) F (TrsFun "O") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "SAT") :: ["A"(15)] -(15)-> "A"(3) F (TrsFun "SATCK") :: ["A"(0) x "A"(14)] -(6)-> "A"(14) F (TrsFun "VERIFY") :: ["A"(14)] -(4)-> "A"(15) F (TrsFun "c") :: [] -(0)-> "A"(1) F (TrsFun "c1") :: [] -(0)-> "A"(4) F (TrsFun "c10") :: [] -(0)-> "A"(15) F (TrsFun "c11") :: [] -(0)-> "A"(15) F (TrsFun "c12") :: [] -(0)-> "A"(1) F (TrsFun "c13") :: ["A"(0)] -(0)-> "A"(15) F (TrsFun "c14") :: [] -(0)-> "A"(14) F (TrsFun "c15") :: ["A"(0)] -(0)-> "A"(11) F (TrsFun "c16") :: ["A"(6)] -(0)-> "A"(6) F (TrsFun "c17") :: [] -(0)-> "A"(15) F (TrsFun "c18") :: ["A"(0) x "A"(15) x "A"(15)] -(0)-> "A"(15) F (TrsFun "c19") :: ["A"(0) x "A"(0)] -(0)-> "A"(15) F (TrsFun "c2") :: [] -(0)-> "A"(15) F (TrsFun "c20") :: ["A"(6) x "A"(6)] -(0)-> "A"(6) F (TrsFun "c21") :: ["A"(0) x "A"(15)] -(0)-> "A"(15) F (TrsFun "c3") :: ["A"(0) x "A"(0)] -(0)-> "A"(15) F (TrsFun "c4") :: ["A"(0) x "A"(15)] -(0)-> "A"(15) F (TrsFun "c5") :: [] -(0)-> "A"(14) F (TrsFun "c6") :: ["A"(0)] -(0)-> "A"(15) F (TrsFun "c7") :: [] -(0)-> "A"(14) F (TrsFun "c8") :: [] -(0)-> "A"(14) F (TrsFun "c9") :: ["A"(6)] -(0)-> "A"(6) F (TrsFun "choice") :: ["A"(14)] -(0)-> "A"(14) F (TrsFun "cons") :: ["A"(1) x "A"(1)] -(1)-> "A"(1) F (TrsFun "cons") :: ["A"(14) x "A"(14)] -(14)-> "A"(14) F (TrsFun "cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "eq") :: ["A"(0) x "A"(0)] -(0)-> "A"(2) F (TrsFun "false") :: [] -(0)-> "A"(0) F (TrsFun "false") :: [] -(0)-> "A"(1) F (TrsFun "false") :: [] -(0)-> "A"(4) F (TrsFun "false") :: [] -(0)-> "A"(10) F (TrsFun "false") :: [] -(0)-> "A"(14) F (TrsFun "false") :: [] -(0)-> "A"(12) F (TrsFun "guess") :: ["A"(14)] -(4)-> "A"(14) F (TrsFun "if") :: ["A"(1) x "A"(12) x "A"(12)] -(0)-> "A"(12) F (TrsFun "member") :: ["A"(0) x "A"(0)] -(0)-> "A"(12) F (TrsFun "negate") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(0) F (TrsFun "nil") :: [] -(0)-> "A"(11) F (TrsFun "nil") :: [] -(0)-> "A"(1) F (TrsFun "nil") :: [] -(0)-> "A"(14) F (TrsFun "sat") :: ["A"(15)] -(10)-> "A"(1) F (TrsFun "satck") :: ["A"(0) x "A"(12)] -(6)-> "A"(2) F (TrsFun "true") :: [] -(0)-> "A"(0) F (TrsFun "true") :: [] -(0)-> "A"(1) F (TrsFun "true") :: [] -(0)-> "A"(8) F (TrsFun "true") :: [] -(0)-> "A"(14) F (TrsFun "true") :: [] -(0)-> "A"(12) F (TrsFun "unsat") :: [] -(0)-> "A"(6) F (TrsFun "unsat") :: [] -(0)-> "A"(14) F (TrsFun "verify") :: ["A"(0)] -(2)-> "A"(12) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"0\")_A" :: ["A"(1)] -(0)-> "A"(1) "F (TrsFun \"1\")_A" :: ["A"(1)] -(1)-> "A"(1) "F (TrsFun \"O\")_A" :: ["A"(0)] -(1)-> "A"(1) "F (TrsFun \"c\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c1\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c10\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c11\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c12\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c13\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c14\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c15\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c16\")_A" :: ["A"(1)] -(0)-> "A"(1) "F (TrsFun \"c17\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c18\")_A" :: ["A"(0) x "A"(1) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c19\")_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "F (TrsFun \"c2\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c20\")_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c21\")_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c3\")_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "F (TrsFun \"c4\")_A" :: ["A"(0) x "A"(1)] -(0)-> "A"(1) "F (TrsFun \"c5\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c6\")_A" :: ["A"(0)] -(0)-> "A"(1) "F (TrsFun \"c7\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c8\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"c9\")_A" :: ["A"(1)] -(0)-> "A"(1) "F (TrsFun \"cons\")_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"false\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"nil\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"true\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"unsat\")_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: EQ(1(z0),1(z1)) -> c9(EQ(z0,z1)) 2. Weak: WORST_CASE(Omega(n^1),O(n^1))