WORST_CASE(?, O(n^1)) Initial complexity problem: 1: T: (Comp: ?, Cost: 1) evalwisestart(Ar_0, Ar_1) -> Com_1(evalwiseentryin(Ar_0, Ar_1)) (Comp: ?, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_0 + 1 ] (Comp: ?, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_1 + 1 ] (Comp: ?, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_1, Ar_0)) [ Ar_0 >= 0 /\ Ar_1 >= 0 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 + 3 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_0 >= Ar_1 + 3 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_0 + 2 >= Ar_1 /\ Ar_1 + 2 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_0 >= Ar_1 + 1 ] (Comp: ?, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) (Comp: ?, Cost: 1) evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) (Comp: ?, Cost: 1) evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1) -> Com_1(evalwisestart(Ar_0, Ar_1)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 1 produces the following problem: 2: T: (Comp: 1, Cost: 1) evalwisestart(Ar_0, Ar_1) -> Com_1(evalwiseentryin(Ar_0, Ar_1)) (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_0 + 1 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_1 + 1 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_1, Ar_0)) [ Ar_0 >= 0 /\ Ar_1 >= 0 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 + 3 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_0 >= Ar_1 + 3 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_0 + 2 >= Ar_1 /\ Ar_1 + 2 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_0 >= Ar_1 + 1 ] (Comp: ?, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) (Comp: ?, Cost: 1) evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) (Comp: ?, Cost: 1) evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1) -> Com_1(evalwisestart(Ar_0, Ar_1)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(evalwisestart) = 2 Pol(evalwiseentryin) = 2 Pol(evalwisereturnin) = 1 Pol(evalwisebb6in) = 2 Pol(evalwisebb3in) = 2 Pol(evalwisebb4in) = 2 Pol(evalwisebb5in) = 2 Pol(evalwisestop) = 0 Pol(koat_start) = 2 orients all transitions weakly and the transition evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1)) strictly and produces the following problem: 3: T: (Comp: 1, Cost: 1) evalwisestart(Ar_0, Ar_1) -> Com_1(evalwiseentryin(Ar_0, Ar_1)) (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_0 + 1 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_1 + 1 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_1, Ar_0)) [ Ar_0 >= 0 /\ Ar_1 >= 0 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 + 3 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_0 >= Ar_1 + 3 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_0 + 2 >= Ar_1 /\ Ar_1 + 2 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_0 >= Ar_1 + 1 ] (Comp: ?, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) (Comp: ?, Cost: 1) evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) (Comp: 2, Cost: 1) evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1) -> Com_1(evalwisestart(Ar_0, Ar_1)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(evalwisestart) = 1 Pol(evalwiseentryin) = 1 Pol(evalwisereturnin) = 0 Pol(evalwisebb6in) = 1 Pol(evalwisebb3in) = 1 Pol(evalwisebb4in) = 1 Pol(evalwisebb5in) = 1 Pol(evalwisestop) = 0 Pol(koat_start) = 1 orients all transitions weakly and the transition evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_0 + 2 >= Ar_1 /\ Ar_1 + 2 >= Ar_0 ] strictly and produces the following problem: 4: T: (Comp: 1, Cost: 1) evalwisestart(Ar_0, Ar_1) -> Com_1(evalwiseentryin(Ar_0, Ar_1)) (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_0 + 1 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_1 + 1 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_1, Ar_0)) [ Ar_0 >= 0 /\ Ar_1 >= 0 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 + 3 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_0 >= Ar_1 + 3 ] (Comp: 1, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_0 + 2 >= Ar_1 /\ Ar_1 + 2 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_0 >= Ar_1 + 1 ] (Comp: ?, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) (Comp: ?, Cost: 1) evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) (Comp: 2, Cost: 1) evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1) -> Com_1(evalwisestart(Ar_0, Ar_1)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Applied AI with 'oct' on problem 4 to obtain the following invariants: For symbol evalwisebb3in: X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 >= 0 For symbol evalwisebb4in: X_1 - X_2 - 1 >= 0 /\ X_2 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 2 >= 0 For symbol evalwisebb5in: X_2 - 1 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ -X_1 + X_2 >= 0 /\ X_1 >= 0 For symbol evalwisebb6in: X_2 >= 0 /\ X_1 + X_2 >= 0 /\ X_1 >= 0 This yielded the following problem: 5: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1) -> Com_1(evalwisestart(Ar_0, Ar_1)) [ 0 <= 0 ] (Comp: 2, Cost: 1) evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1)) (Comp: ?, Cost: 1) evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) [ Ar_1 - 1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ -Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 ] (Comp: ?, Cost: 1) evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) [ Ar_0 - Ar_1 - 1 >= 0 /\ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 - 2 >= 0 ] (Comp: ?, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 >= 0 /\ Ar_1 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 >= 0 /\ Ar_0 >= Ar_1 + 1 ] (Comp: 1, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_0 + 2 >= Ar_1 /\ Ar_1 + 2 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_0 >= Ar_1 + 3 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_1 >= Ar_0 + 3 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_1, Ar_0)) [ Ar_0 >= 0 /\ Ar_1 >= 0 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_1 + 1 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_0 + 1 ] (Comp: 1, Cost: 1) evalwisestart(Ar_0, Ar_1) -> Com_1(evalwiseentryin(Ar_0, Ar_1)) start location: koat_start leaf cost: 0 A polynomial rank function with Pol(evalwisebb5in) = -3*V_1 + 3*V_2 + 1 Pol(evalwisebb6in) = -3*V_1 + 3*V_2 + 3 Pol(evalwisebb3in) = -3*V_1 + 3*V_2 + 2 and size complexities S("evalwisestart(Ar_0, Ar_1) -> Com_1(evalwiseentryin(Ar_0, Ar_1))", 0-0) = Ar_0 S("evalwisestart(Ar_0, Ar_1) -> Com_1(evalwiseentryin(Ar_0, Ar_1))", 0-1) = Ar_1 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_0 + 1 ]", 0-0) = Ar_0 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_0 + 1 ]", 0-1) = Ar_1 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_1 + 1 ]", 0-0) = Ar_0 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_1 + 1 ]", 0-1) = Ar_1 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_1, Ar_0)) [ Ar_0 >= 0 /\\ Ar_1 >= 0 ]", 0-0) = Ar_1 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_1, Ar_0)) [ Ar_0 >= 0 /\\ Ar_1 >= 0 ]", 0-1) = Ar_0 S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_1 >= Ar_0 + 3 ]", 0-0) = ? S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_1 >= Ar_0 + 3 ]", 0-1) = Ar_0 S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 >= Ar_1 + 3 ]", 0-0) = Ar_1 S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 >= Ar_1 + 3 ]", 0-1) = Ar_0 + Ar_1 S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 + 2 >= Ar_1 /\\ Ar_1 + 2 >= Ar_0 ]", 0-0) = ? S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 + 2 >= Ar_1 /\\ Ar_1 + 2 >= Ar_0 ]", 0-1) = Ar_0 + Ar_1 S("evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 >= Ar_1 + 1 ]", 0-0) = Ar_1 S("evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 >= Ar_1 + 1 ]", 0-1) = Ar_0 + Ar_1 S("evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 >= 0 /\\ Ar_1 >= Ar_0 ]", 0-0) = ? S("evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 >= 0 /\\ Ar_1 >= Ar_0 ]", 0-1) = Ar_0 S("evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) [ Ar_0 - Ar_1 - 1 >= 0 /\\ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 - 2 >= 0 ]", 0-0) = Ar_1 S("evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) [ Ar_0 - Ar_1 - 1 >= 0 /\\ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 - 2 >= 0 ]", 0-1) = Ar_1 S("evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) [ Ar_1 - 1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ -Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 ]", 0-0) = ? S("evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) [ Ar_1 - 1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ -Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 ]", 0-1) = Ar_0 S("evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1))", 0-0) = ? S("evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1))", 0-1) = Ar_0 + Ar_1 S("koat_start(Ar_0, Ar_1) -> Com_1(evalwisestart(Ar_0, Ar_1)) [ 0 <= 0 ]", 0-0) = Ar_0 S("koat_start(Ar_0, Ar_1) -> Com_1(evalwisestart(Ar_0, Ar_1)) [ 0 <= 0 ]", 0-1) = Ar_1 orients the transitions evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) [ Ar_1 - 1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ -Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 ] evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 >= 0 /\ Ar_1 >= Ar_0 ] evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_1 >= Ar_0 + 3 ] weakly and the transitions evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_1 >= Ar_0 + 3 ] evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) [ Ar_1 - 1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ -Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 ] evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 >= 0 /\ Ar_1 >= Ar_0 ] strictly and produces the following problem: 6: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1) -> Com_1(evalwisestart(Ar_0, Ar_1)) [ 0 <= 0 ] (Comp: 2, Cost: 1) evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1)) (Comp: 3*Ar_1 + 3*Ar_0 + 3, Cost: 1) evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) [ Ar_1 - 1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ -Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 ] (Comp: ?, Cost: 1) evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) [ Ar_0 - Ar_1 - 1 >= 0 /\ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 - 2 >= 0 ] (Comp: 3*Ar_1 + 3*Ar_0 + 3, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 >= 0 /\ Ar_1 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 >= 0 /\ Ar_0 >= Ar_1 + 1 ] (Comp: 1, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_0 + 2 >= Ar_1 /\ Ar_1 + 2 >= Ar_0 ] (Comp: ?, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_0 >= Ar_1 + 3 ] (Comp: 3*Ar_1 + 3*Ar_0 + 3, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_1 >= Ar_0 + 3 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_1, Ar_0)) [ Ar_0 >= 0 /\ Ar_1 >= 0 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_1 + 1 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_0 + 1 ] (Comp: 1, Cost: 1) evalwisestart(Ar_0, Ar_1) -> Com_1(evalwiseentryin(Ar_0, Ar_1)) start location: koat_start leaf cost: 0 A polynomial rank function with Pol(evalwisebb6in) = 3*V_1 - 3*V_2 Pol(evalwisebb3in) = 3*V_1 - 3*V_2 - 1 Pol(evalwisebb4in) = 3*V_1 - 3*V_2 - 2 and size complexities S("evalwisestart(Ar_0, Ar_1) -> Com_1(evalwiseentryin(Ar_0, Ar_1))", 0-0) = Ar_0 S("evalwisestart(Ar_0, Ar_1) -> Com_1(evalwiseentryin(Ar_0, Ar_1))", 0-1) = Ar_1 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_0 + 1 ]", 0-0) = Ar_0 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_0 + 1 ]", 0-1) = Ar_1 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_1 + 1 ]", 0-0) = Ar_0 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_1 + 1 ]", 0-1) = Ar_1 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_1, Ar_0)) [ Ar_0 >= 0 /\\ Ar_1 >= 0 ]", 0-0) = Ar_1 S("evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_1, Ar_0)) [ Ar_0 >= 0 /\\ Ar_1 >= 0 ]", 0-1) = Ar_0 S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_1 >= Ar_0 + 3 ]", 0-0) = 4*Ar_0 + 4*Ar_1 + 48 S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_1 >= Ar_0 + 3 ]", 0-1) = Ar_0 S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 >= Ar_1 + 3 ]", 0-0) = Ar_1 S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 >= Ar_1 + 3 ]", 0-1) = Ar_0 + Ar_1 S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 + 2 >= Ar_1 /\\ Ar_1 + 2 >= Ar_0 ]", 0-0) = 4*Ar_0 + 4*Ar_1 + 192 S("evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 + 2 >= Ar_1 /\\ Ar_1 + 2 >= Ar_0 ]", 0-1) = Ar_0 + Ar_1 S("evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 >= Ar_1 + 1 ]", 0-0) = Ar_1 S("evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 >= 0 /\\ Ar_0 >= Ar_1 + 1 ]", 0-1) = Ar_0 + Ar_1 S("evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 >= 0 /\\ Ar_1 >= Ar_0 ]", 0-0) = 4*Ar_0 + 4*Ar_1 + 48 S("evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 >= 0 /\\ Ar_1 >= Ar_0 ]", 0-1) = Ar_0 S("evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) [ Ar_0 - Ar_1 - 1 >= 0 /\\ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 - 2 >= 0 ]", 0-0) = Ar_1 S("evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) [ Ar_0 - Ar_1 - 1 >= 0 /\\ Ar_1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ Ar_0 - 2 >= 0 ]", 0-1) = Ar_1 S("evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) [ Ar_1 - 1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ -Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 ]", 0-0) = 4*Ar_0 + 4*Ar_1 + 48 S("evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) [ Ar_1 - 1 >= 0 /\\ Ar_0 + Ar_1 - 3 >= 0 /\\ -Ar_0 + Ar_1 >= 0 /\\ Ar_0 >= 0 ]", 0-1) = Ar_0 S("evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1))", 0-0) = 4*Ar_0 + 4*Ar_1 + 768 S("evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1))", 0-1) = Ar_0 + Ar_1 S("koat_start(Ar_0, Ar_1) -> Com_1(evalwisestart(Ar_0, Ar_1)) [ 0 <= 0 ]", 0-0) = Ar_0 S("koat_start(Ar_0, Ar_1) -> Com_1(evalwisestart(Ar_0, Ar_1)) [ 0 <= 0 ]", 0-1) = Ar_1 orients the transitions evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_0 >= Ar_1 + 3 ] evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) [ Ar_0 - Ar_1 - 1 >= 0 /\ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 - 2 >= 0 ] evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 >= 0 /\ Ar_0 >= Ar_1 + 1 ] weakly and the transitions evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_0 >= Ar_1 + 3 ] evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) [ Ar_0 - Ar_1 - 1 >= 0 /\ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 - 2 >= 0 ] evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 >= 0 /\ Ar_0 >= Ar_1 + 1 ] strictly and produces the following problem: 7: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1) -> Com_1(evalwisestart(Ar_0, Ar_1)) [ 0 <= 0 ] (Comp: 2, Cost: 1) evalwisereturnin(Ar_0, Ar_1) -> Com_1(evalwisestop(Ar_0, Ar_1)) (Comp: 3*Ar_1 + 3*Ar_0 + 3, Cost: 1) evalwisebb5in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0 + 1, Ar_1)) [ Ar_1 - 1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ -Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 ] (Comp: 3*Ar_1 + 3*Ar_0, Cost: 1) evalwisebb4in(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_0, Ar_1 + 1)) [ Ar_0 - Ar_1 - 1 >= 0 /\ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 - 2 >= 0 ] (Comp: 3*Ar_1 + 3*Ar_0 + 3, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb5in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 >= 0 /\ Ar_1 >= Ar_0 ] (Comp: 3*Ar_1 + 3*Ar_0, Cost: 1) evalwisebb3in(Ar_0, Ar_1) -> Com_1(evalwisebb4in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 - 3 >= 0 /\ Ar_0 >= 0 /\ Ar_0 >= Ar_1 + 1 ] (Comp: 1, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_0 + 2 >= Ar_1 /\ Ar_1 + 2 >= Ar_0 ] (Comp: 3*Ar_1 + 3*Ar_0, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_0 >= Ar_1 + 3 ] (Comp: 3*Ar_1 + 3*Ar_0 + 3, Cost: 1) evalwisebb6in(Ar_0, Ar_1) -> Com_1(evalwisebb3in(Ar_0, Ar_1)) [ Ar_1 >= 0 /\ Ar_0 + Ar_1 >= 0 /\ Ar_0 >= 0 /\ Ar_1 >= Ar_0 + 3 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisebb6in(Ar_1, Ar_0)) [ Ar_0 >= 0 /\ Ar_1 >= 0 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_1 + 1 ] (Comp: 1, Cost: 1) evalwiseentryin(Ar_0, Ar_1) -> Com_1(evalwisereturnin(Ar_0, Ar_1)) [ 0 >= Ar_0 + 1 ] (Comp: 1, Cost: 1) evalwisestart(Ar_0, Ar_1) -> Com_1(evalwiseentryin(Ar_0, Ar_1)) start location: koat_start leaf cost: 0 Complexity upper bound 18*Ar_1 + 18*Ar_0 + 16 Time: 1.907 sec (SMT: 1.837 sec)