WORST_CASE(?,O(n^2)) proof of input_pnsrsWuKPP.trs # AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 935 ms] (2) CpxRelTRS (3) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (4) CpxWeightedTrs (5) CpxWeightedTrsRenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CpxWeightedTrs (7) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxTypedWeightedTrs (9) CompletionProof [UPPER BOUND(ID), 13 ms] (10) CpxTypedWeightedCompleteTrs (11) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 18 ms] (12) CpxRNTS (13) CompleteCoflocoProof [FINISHED, 4432 ms] (14) BOUNDS(1, n^2) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #equal(@x, @y) -> #eq(@x, @y) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) +(@x, @y) -> #add(@x, @y) firstline(@l) -> firstline#1(@l) firstline#1(::(@x, @xs)) -> ::(#abs(#0), firstline(@xs)) firstline#1(nil) -> nil lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) lcs#1(@m) -> lcs#2(@m) lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) lcs#2(nil) -> #abs(#0) lcs#3(::(@len, @_@1)) -> @len lcs#3(nil) -> #abs(#0) lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) lcstable#1(nil, @l2) -> ::(firstline(@l2), nil) lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) lcstable#3(nil, @l2, @x) -> nil max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) max#1(#false, @a, @b) -> @b max#1(#true, @a, @b) -> @a newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) newline#1(nil, @lastline, @y) -> nil newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) newline#2(nil, @x, @xs, @y) -> nil newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) newline#6(@elem, @nl) -> ::(@elem, @nl) newline#7(#false, @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) newline#7(#true, @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0))) right(@l) -> right#1(@l) right#1(::(@x, @xs)) -> @x right#1(nil) -> #abs(#0) The (relative) TRS S consists of the following rules: #add(#0, @y) -> @y #add(#neg(#s(#0)), @y) -> #pred(@y) #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) #add(#pos(#s(#0)), @y) -> #succ(@y) #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) #eq(#0, #0) -> #true #eq(#0, #neg(@y)) -> #false #eq(#0, #pos(@y)) -> #false #eq(#0, #s(@y)) -> #false #eq(#neg(@x), #0) -> #false #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) #eq(#neg(@x), #pos(@y)) -> #false #eq(#pos(@x), #0) -> #false #eq(#pos(@x), #neg(@y)) -> #false #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) #eq(#s(@x), #0) -> #false #eq(#s(@x), #s(@y)) -> #eq(@x, @y) #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) #eq(::(@x_1, @x_2), nil) -> #false #eq(nil, ::(@y_1, @y_2)) -> #false #eq(nil, nil) -> #true #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) 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, n^2). The TRS R consists of the following rules: #abs(#0) -> #0 #abs(#neg(@x)) -> #pos(@x) #abs(#pos(@x)) -> #pos(@x) #abs(#s(@x)) -> #pos(#s(@x)) #equal(@x, @y) -> #eq(@x, @y) #greater(@x, @y) -> #ckgt(#compare(@x, @y)) +(@x, @y) -> #add(@x, @y) firstline(@l) -> firstline#1(@l) firstline#1(::(@x, @xs)) -> ::(#abs(#0), firstline(@xs)) firstline#1(nil) -> nil lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) lcs#1(@m) -> lcs#2(@m) lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) lcs#2(nil) -> #abs(#0) lcs#3(::(@len, @_@1)) -> @len lcs#3(nil) -> #abs(#0) lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) lcstable#1(nil, @l2) -> ::(firstline(@l2), nil) lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) lcstable#3(nil, @l2, @x) -> nil max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) max#1(#false, @a, @b) -> @b max#1(#true, @a, @b) -> @a newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) newline#1(nil, @lastline, @y) -> nil newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) newline#2(nil, @x, @xs, @y) -> nil newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) newline#6(@elem, @nl) -> ::(@elem, @nl) newline#7(#false, @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) newline#7(#true, @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0))) right(@l) -> right#1(@l) right#1(::(@x, @xs)) -> @x right#1(nil) -> #abs(#0) The (relative) TRS S consists of the following rules: #add(#0, @y) -> @y #add(#neg(#s(#0)), @y) -> #pred(@y) #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) #add(#pos(#s(#0)), @y) -> #succ(@y) #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(@y)) -> #GT #compare(#0, #pos(@y)) -> #LT #compare(#0, #s(@y)) -> #LT #compare(#neg(@x), #0) -> #LT #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) #compare(#neg(@x), #pos(@y)) -> #LT #compare(#pos(@x), #0) -> #GT #compare(#pos(@x), #neg(@y)) -> #GT #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) #compare(#s(@x), #0) -> #GT #compare(#s(@x), #s(@y)) -> #compare(@x, @y) #eq(#0, #0) -> #true #eq(#0, #neg(@y)) -> #false #eq(#0, #pos(@y)) -> #false #eq(#0, #s(@y)) -> #false #eq(#neg(@x), #0) -> #false #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) #eq(#neg(@x), #pos(@y)) -> #false #eq(#pos(@x), #0) -> #false #eq(#pos(@x), #neg(@y)) -> #false #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) #eq(#s(@x), #0) -> #false #eq(#s(@x), #s(@y)) -> #eq(@x, @y) #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) #eq(::(@x_1, @x_2), nil) -> #false #eq(nil, ::(@y_1, @y_2)) -> #false #eq(nil, nil) -> #true #pred(#0) -> #neg(#s(#0)) #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) #pred(#pos(#s(#0))) -> #0 #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) #succ(#0) -> #pos(#s(#0)) #succ(#neg(#s(#0))) -> #0 #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (4) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: #abs(#0) -> #0 [1] #abs(#neg(@x)) -> #pos(@x) [1] #abs(#pos(@x)) -> #pos(@x) [1] #abs(#s(@x)) -> #pos(#s(@x)) [1] #equal(@x, @y) -> #eq(@x, @y) [1] #greater(@x, @y) -> #ckgt(#compare(@x, @y)) [1] +(@x, @y) -> #add(@x, @y) [1] firstline(@l) -> firstline#1(@l) [1] firstline#1(::(@x, @xs)) -> ::(#abs(#0), firstline(@xs)) [1] firstline#1(nil) -> nil [1] lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) [1] lcs#1(@m) -> lcs#2(@m) [1] lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) [1] lcs#2(nil) -> #abs(#0) [1] lcs#3(::(@len, @_@1)) -> @len [1] lcs#3(nil) -> #abs(#0) [1] lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) [1] lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) [1] lcstable#1(nil, @l2) -> ::(firstline(@l2), nil) [1] lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) [1] lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) [1] lcstable#3(nil, @l2, @x) -> nil [1] max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) [1] max#1(#false, @a, @b) -> @b [1] max#1(#true, @a, @b) -> @a [1] newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) [1] newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) [1] newline#1(nil, @lastline, @y) -> nil [1] newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) [1] newline#2(nil, @x, @xs, @y) -> nil [1] newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) [1] newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) [1] newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) [1] newline#6(@elem, @nl) -> ::(@elem, @nl) [1] newline#7(#false, @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) [1] newline#7(#true, @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0))) [1] right(@l) -> right#1(@l) [1] right#1(::(@x, @xs)) -> @x [1] right#1(nil) -> #abs(#0) [1] #add(#0, @y) -> @y [0] #add(#neg(#s(#0)), @y) -> #pred(@y) [0] #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) [0] #add(#pos(#s(#0)), @y) -> #succ(@y) [0] #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) [0] #and(#false, #false) -> #false [0] #and(#false, #true) -> #false [0] #and(#true, #false) -> #false [0] #and(#true, #true) -> #true [0] #ckgt(#EQ) -> #false [0] #ckgt(#GT) -> #true [0] #ckgt(#LT) -> #false [0] #compare(#0, #0) -> #EQ [0] #compare(#0, #neg(@y)) -> #GT [0] #compare(#0, #pos(@y)) -> #LT [0] #compare(#0, #s(@y)) -> #LT [0] #compare(#neg(@x), #0) -> #LT [0] #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) [0] #compare(#neg(@x), #pos(@y)) -> #LT [0] #compare(#pos(@x), #0) -> #GT [0] #compare(#pos(@x), #neg(@y)) -> #GT [0] #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) [0] #compare(#s(@x), #0) -> #GT [0] #compare(#s(@x), #s(@y)) -> #compare(@x, @y) [0] #eq(#0, #0) -> #true [0] #eq(#0, #neg(@y)) -> #false [0] #eq(#0, #pos(@y)) -> #false [0] #eq(#0, #s(@y)) -> #false [0] #eq(#neg(@x), #0) -> #false [0] #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) [0] #eq(#neg(@x), #pos(@y)) -> #false [0] #eq(#pos(@x), #0) -> #false [0] #eq(#pos(@x), #neg(@y)) -> #false [0] #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) [0] #eq(#s(@x), #0) -> #false [0] #eq(#s(@x), #s(@y)) -> #eq(@x, @y) [0] #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) [0] #eq(::(@x_1, @x_2), nil) -> #false [0] #eq(nil, ::(@y_1, @y_2)) -> #false [0] #eq(nil, nil) -> #true [0] #pred(#0) -> #neg(#s(#0)) [0] #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) [0] #pred(#pos(#s(#0))) -> #0 [0] #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) [0] #succ(#0) -> #pos(#s(#0)) [0] #succ(#neg(#s(#0))) -> #0 [0] #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) [0] #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (5) CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID)) Renamed defined symbols to avoid conflicts with arithmetic symbols: + => plus ---------------------------------------- (6) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: #abs(#0) -> #0 [1] #abs(#neg(@x)) -> #pos(@x) [1] #abs(#pos(@x)) -> #pos(@x) [1] #abs(#s(@x)) -> #pos(#s(@x)) [1] #equal(@x, @y) -> #eq(@x, @y) [1] #greater(@x, @y) -> #ckgt(#compare(@x, @y)) [1] plus(@x, @y) -> #add(@x, @y) [1] firstline(@l) -> firstline#1(@l) [1] firstline#1(::(@x, @xs)) -> ::(#abs(#0), firstline(@xs)) [1] firstline#1(nil) -> nil [1] lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) [1] lcs#1(@m) -> lcs#2(@m) [1] lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) [1] lcs#2(nil) -> #abs(#0) [1] lcs#3(::(@len, @_@1)) -> @len [1] lcs#3(nil) -> #abs(#0) [1] lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) [1] lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) [1] lcstable#1(nil, @l2) -> ::(firstline(@l2), nil) [1] lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) [1] lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) [1] lcstable#3(nil, @l2, @x) -> nil [1] max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) [1] max#1(#false, @a, @b) -> @b [1] max#1(#true, @a, @b) -> @a [1] newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) [1] newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) [1] newline#1(nil, @lastline, @y) -> nil [1] newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) [1] newline#2(nil, @x, @xs, @y) -> nil [1] newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) [1] newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) [1] newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) [1] newline#6(@elem, @nl) -> ::(@elem, @nl) [1] newline#7(#false, @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) [1] newline#7(#true, @belowVal, @diagVal, @rightVal) -> plus(@diagVal, #pos(#s(#0))) [1] right(@l) -> right#1(@l) [1] right#1(::(@x, @xs)) -> @x [1] right#1(nil) -> #abs(#0) [1] #add(#0, @y) -> @y [0] #add(#neg(#s(#0)), @y) -> #pred(@y) [0] #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) [0] #add(#pos(#s(#0)), @y) -> #succ(@y) [0] #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) [0] #and(#false, #false) -> #false [0] #and(#false, #true) -> #false [0] #and(#true, #false) -> #false [0] #and(#true, #true) -> #true [0] #ckgt(#EQ) -> #false [0] #ckgt(#GT) -> #true [0] #ckgt(#LT) -> #false [0] #compare(#0, #0) -> #EQ [0] #compare(#0, #neg(@y)) -> #GT [0] #compare(#0, #pos(@y)) -> #LT [0] #compare(#0, #s(@y)) -> #LT [0] #compare(#neg(@x), #0) -> #LT [0] #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) [0] #compare(#neg(@x), #pos(@y)) -> #LT [0] #compare(#pos(@x), #0) -> #GT [0] #compare(#pos(@x), #neg(@y)) -> #GT [0] #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) [0] #compare(#s(@x), #0) -> #GT [0] #compare(#s(@x), #s(@y)) -> #compare(@x, @y) [0] #eq(#0, #0) -> #true [0] #eq(#0, #neg(@y)) -> #false [0] #eq(#0, #pos(@y)) -> #false [0] #eq(#0, #s(@y)) -> #false [0] #eq(#neg(@x), #0) -> #false [0] #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) [0] #eq(#neg(@x), #pos(@y)) -> #false [0] #eq(#pos(@x), #0) -> #false [0] #eq(#pos(@x), #neg(@y)) -> #false [0] #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) [0] #eq(#s(@x), #0) -> #false [0] #eq(#s(@x), #s(@y)) -> #eq(@x, @y) [0] #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) [0] #eq(::(@x_1, @x_2), nil) -> #false [0] #eq(nil, ::(@y_1, @y_2)) -> #false [0] #eq(nil, nil) -> #true [0] #pred(#0) -> #neg(#s(#0)) [0] #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) [0] #pred(#pos(#s(#0))) -> #0 [0] #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) [0] #succ(#0) -> #pos(#s(#0)) [0] #succ(#neg(#s(#0))) -> #0 [0] #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) [0] #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (7) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (8) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: #abs(#0) -> #0 [1] #abs(#neg(@x)) -> #pos(@x) [1] #abs(#pos(@x)) -> #pos(@x) [1] #abs(#s(@x)) -> #pos(#s(@x)) [1] #equal(@x, @y) -> #eq(@x, @y) [1] #greater(@x, @y) -> #ckgt(#compare(@x, @y)) [1] plus(@x, @y) -> #add(@x, @y) [1] firstline(@l) -> firstline#1(@l) [1] firstline#1(::(@x, @xs)) -> ::(#abs(#0), firstline(@xs)) [1] firstline#1(nil) -> nil [1] lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) [1] lcs#1(@m) -> lcs#2(@m) [1] lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) [1] lcs#2(nil) -> #abs(#0) [1] lcs#3(::(@len, @_@1)) -> @len [1] lcs#3(nil) -> #abs(#0) [1] lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) [1] lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) [1] lcstable#1(nil, @l2) -> ::(firstline(@l2), nil) [1] lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) [1] lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) [1] lcstable#3(nil, @l2, @x) -> nil [1] max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) [1] max#1(#false, @a, @b) -> @b [1] max#1(#true, @a, @b) -> @a [1] newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) [1] newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) [1] newline#1(nil, @lastline, @y) -> nil [1] newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) [1] newline#2(nil, @x, @xs, @y) -> nil [1] newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) [1] newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) [1] newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) [1] newline#6(@elem, @nl) -> ::(@elem, @nl) [1] newline#7(#false, @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) [1] newline#7(#true, @belowVal, @diagVal, @rightVal) -> plus(@diagVal, #pos(#s(#0))) [1] right(@l) -> right#1(@l) [1] right#1(::(@x, @xs)) -> @x [1] right#1(nil) -> #abs(#0) [1] #add(#0, @y) -> @y [0] #add(#neg(#s(#0)), @y) -> #pred(@y) [0] #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) [0] #add(#pos(#s(#0)), @y) -> #succ(@y) [0] #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) [0] #and(#false, #false) -> #false [0] #and(#false, #true) -> #false [0] #and(#true, #false) -> #false [0] #and(#true, #true) -> #true [0] #ckgt(#EQ) -> #false [0] #ckgt(#GT) -> #true [0] #ckgt(#LT) -> #false [0] #compare(#0, #0) -> #EQ [0] #compare(#0, #neg(@y)) -> #GT [0] #compare(#0, #pos(@y)) -> #LT [0] #compare(#0, #s(@y)) -> #LT [0] #compare(#neg(@x), #0) -> #LT [0] #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) [0] #compare(#neg(@x), #pos(@y)) -> #LT [0] #compare(#pos(@x), #0) -> #GT [0] #compare(#pos(@x), #neg(@y)) -> #GT [0] #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) [0] #compare(#s(@x), #0) -> #GT [0] #compare(#s(@x), #s(@y)) -> #compare(@x, @y) [0] #eq(#0, #0) -> #true [0] #eq(#0, #neg(@y)) -> #false [0] #eq(#0, #pos(@y)) -> #false [0] #eq(#0, #s(@y)) -> #false [0] #eq(#neg(@x), #0) -> #false [0] #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) [0] #eq(#neg(@x), #pos(@y)) -> #false [0] #eq(#pos(@x), #0) -> #false [0] #eq(#pos(@x), #neg(@y)) -> #false [0] #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) [0] #eq(#s(@x), #0) -> #false [0] #eq(#s(@x), #s(@y)) -> #eq(@x, @y) [0] #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) [0] #eq(::(@x_1, @x_2), nil) -> #false [0] #eq(nil, ::(@y_1, @y_2)) -> #false [0] #eq(nil, nil) -> #true [0] #pred(#0) -> #neg(#s(#0)) [0] #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) [0] #pred(#pos(#s(#0))) -> #0 [0] #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) [0] #succ(#0) -> #pos(#s(#0)) [0] #succ(#neg(#s(#0))) -> #0 [0] #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) [0] #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) [0] The TRS has the following type information: #abs :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil #0 :: #0:#neg:#pos:#s::::nil #neg :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil #pos :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil #s :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil #equal :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #false:#true #eq :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #false:#true #greater :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #false:#true #ckgt :: #EQ:#GT:#LT -> #false:#true #compare :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #EQ:#GT:#LT plus :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil #add :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil firstline :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil firstline#1 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil :: :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil nil :: #0:#neg:#pos:#s::::nil lcs :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil lcs#1 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil lcstable :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil lcs#2 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil lcs#3 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil lcstable#1 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil lcstable#2 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil lcstable#3 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil newline :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil max :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil max#1 :: #false:#true -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil #false :: #false:#true #true :: #false:#true newline#1 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil newline#2 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil newline#3 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil newline#4 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil right :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil newline#5 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil newline#6 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil newline#7 :: #false:#true -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil right#1 :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil #pred :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil #succ :: #0:#neg:#pos:#s::::nil -> #0:#neg:#pos:#s::::nil #and :: #false:#true -> #false:#true -> #false:#true #EQ :: #EQ:#GT:#LT #GT :: #EQ:#GT:#LT #LT :: #EQ:#GT:#LT Rewrite Strategy: INNERMOST ---------------------------------------- (9) 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: #add(v0, v1) -> null_#add [0] #and(v0, v1) -> null_#and [0] #ckgt(v0) -> null_#ckgt [0] #compare(v0, v1) -> null_#compare [0] #eq(v0, v1) -> null_#eq [0] #pred(v0) -> null_#pred [0] #succ(v0) -> null_#succ [0] #abs(v0) -> null_#abs [0] firstline#1(v0) -> null_firstline#1 [0] lcs#2(v0) -> null_lcs#2 [0] lcs#3(v0) -> null_lcs#3 [0] lcstable#1(v0, v1) -> null_lcstable#1 [0] lcstable#3(v0, v1, v2) -> null_lcstable#3 [0] max#1(v0, v1, v2) -> null_max#1 [0] newline#1(v0, v1, v2) -> null_newline#1 [0] newline#2(v0, v1, v2, v3) -> null_newline#2 [0] newline#7(v0, v1, v2, v3) -> null_newline#7 [0] right#1(v0) -> null_right#1 [0] And the following fresh constants: null_#add, null_#and, null_#ckgt, null_#compare, null_#eq, null_#pred, null_#succ, null_#abs, null_firstline#1, null_lcs#2, null_lcs#3, null_lcstable#1, null_lcstable#3, null_max#1, null_newline#1, null_newline#2, null_newline#7, null_right#1 ---------------------------------------- (10) 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: #abs(#0) -> #0 [1] #abs(#neg(@x)) -> #pos(@x) [1] #abs(#pos(@x)) -> #pos(@x) [1] #abs(#s(@x)) -> #pos(#s(@x)) [1] #equal(@x, @y) -> #eq(@x, @y) [1] #greater(@x, @y) -> #ckgt(#compare(@x, @y)) [1] plus(@x, @y) -> #add(@x, @y) [1] firstline(@l) -> firstline#1(@l) [1] firstline#1(::(@x, @xs)) -> ::(#abs(#0), firstline(@xs)) [1] firstline#1(nil) -> nil [1] lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) [1] lcs#1(@m) -> lcs#2(@m) [1] lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) [1] lcs#2(nil) -> #abs(#0) [1] lcs#3(::(@len, @_@1)) -> @len [1] lcs#3(nil) -> #abs(#0) [1] lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) [1] lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) [1] lcstable#1(nil, @l2) -> ::(firstline(@l2), nil) [1] lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) [1] lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) [1] lcstable#3(nil, @l2, @x) -> nil [1] max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) [1] max#1(#false, @a, @b) -> @b [1] max#1(#true, @a, @b) -> @a [1] newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) [1] newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) [1] newline#1(nil, @lastline, @y) -> nil [1] newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) [1] newline#2(nil, @x, @xs, @y) -> nil [1] newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) [1] newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) [1] newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) [1] newline#6(@elem, @nl) -> ::(@elem, @nl) [1] newline#7(#false, @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) [1] newline#7(#true, @belowVal, @diagVal, @rightVal) -> plus(@diagVal, #pos(#s(#0))) [1] right(@l) -> right#1(@l) [1] right#1(::(@x, @xs)) -> @x [1] right#1(nil) -> #abs(#0) [1] #add(#0, @y) -> @y [0] #add(#neg(#s(#0)), @y) -> #pred(@y) [0] #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) [0] #add(#pos(#s(#0)), @y) -> #succ(@y) [0] #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) [0] #and(#false, #false) -> #false [0] #and(#false, #true) -> #false [0] #and(#true, #false) -> #false [0] #and(#true, #true) -> #true [0] #ckgt(#EQ) -> #false [0] #ckgt(#GT) -> #true [0] #ckgt(#LT) -> #false [0] #compare(#0, #0) -> #EQ [0] #compare(#0, #neg(@y)) -> #GT [0] #compare(#0, #pos(@y)) -> #LT [0] #compare(#0, #s(@y)) -> #LT [0] #compare(#neg(@x), #0) -> #LT [0] #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) [0] #compare(#neg(@x), #pos(@y)) -> #LT [0] #compare(#pos(@x), #0) -> #GT [0] #compare(#pos(@x), #neg(@y)) -> #GT [0] #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) [0] #compare(#s(@x), #0) -> #GT [0] #compare(#s(@x), #s(@y)) -> #compare(@x, @y) [0] #eq(#0, #0) -> #true [0] #eq(#0, #neg(@y)) -> #false [0] #eq(#0, #pos(@y)) -> #false [0] #eq(#0, #s(@y)) -> #false [0] #eq(#neg(@x), #0) -> #false [0] #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) [0] #eq(#neg(@x), #pos(@y)) -> #false [0] #eq(#pos(@x), #0) -> #false [0] #eq(#pos(@x), #neg(@y)) -> #false [0] #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) [0] #eq(#s(@x), #0) -> #false [0] #eq(#s(@x), #s(@y)) -> #eq(@x, @y) [0] #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) [0] #eq(::(@x_1, @x_2), nil) -> #false [0] #eq(nil, ::(@y_1, @y_2)) -> #false [0] #eq(nil, nil) -> #true [0] #pred(#0) -> #neg(#s(#0)) [0] #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) [0] #pred(#pos(#s(#0))) -> #0 [0] #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) [0] #succ(#0) -> #pos(#s(#0)) [0] #succ(#neg(#s(#0))) -> #0 [0] #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) [0] #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) [0] #add(v0, v1) -> null_#add [0] #and(v0, v1) -> null_#and [0] #ckgt(v0) -> null_#ckgt [0] #compare(v0, v1) -> null_#compare [0] #eq(v0, v1) -> null_#eq [0] #pred(v0) -> null_#pred [0] #succ(v0) -> null_#succ [0] #abs(v0) -> null_#abs [0] firstline#1(v0) -> null_firstline#1 [0] lcs#2(v0) -> null_lcs#2 [0] lcs#3(v0) -> null_lcs#3 [0] lcstable#1(v0, v1) -> null_lcstable#1 [0] lcstable#3(v0, v1, v2) -> null_lcstable#3 [0] max#1(v0, v1, v2) -> null_max#1 [0] newline#1(v0, v1, v2) -> null_newline#1 [0] newline#2(v0, v1, v2, v3) -> null_newline#2 [0] newline#7(v0, v1, v2, v3) -> null_newline#7 [0] right#1(v0) -> null_right#1 [0] The TRS has the following type information: #abs :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 #0 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 #neg :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 #pos :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 #s :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 #equal :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #false:#true:null_#and:null_#ckgt:null_#eq #eq :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #false:#true:null_#and:null_#ckgt:null_#eq #greater :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #false:#true:null_#and:null_#ckgt:null_#eq #ckgt :: #EQ:#GT:#LT:null_#compare -> #false:#true:null_#and:null_#ckgt:null_#eq #compare :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #EQ:#GT:#LT:null_#compare plus :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 #add :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 firstline :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 firstline#1 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 :: :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 nil :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 lcs :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 lcs#1 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 lcstable :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 lcs#2 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 lcs#3 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 lcstable#1 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 lcstable#2 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 lcstable#3 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 newline :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 max :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 max#1 :: #false:#true:null_#and:null_#ckgt:null_#eq -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 #false :: #false:#true:null_#and:null_#ckgt:null_#eq #true :: #false:#true:null_#and:null_#ckgt:null_#eq newline#1 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 newline#2 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 newline#3 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 newline#4 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 right :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 newline#5 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 newline#6 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 newline#7 :: #false:#true:null_#and:null_#ckgt:null_#eq -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 right#1 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 #pred :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 #succ :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 -> #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 #and :: #false:#true:null_#and:null_#ckgt:null_#eq -> #false:#true:null_#and:null_#ckgt:null_#eq -> #false:#true:null_#and:null_#ckgt:null_#eq #EQ :: #EQ:#GT:#LT:null_#compare #GT :: #EQ:#GT:#LT:null_#compare #LT :: #EQ:#GT:#LT:null_#compare null_#add :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_#and :: #false:#true:null_#and:null_#ckgt:null_#eq null_#ckgt :: #false:#true:null_#and:null_#ckgt:null_#eq null_#compare :: #EQ:#GT:#LT:null_#compare null_#eq :: #false:#true:null_#and:null_#ckgt:null_#eq null_#pred :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_#succ :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_#abs :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_firstline#1 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_lcs#2 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_lcs#3 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_lcstable#1 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_lcstable#3 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_max#1 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_newline#1 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_newline#2 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_newline#7 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 null_right#1 :: #0:#neg:#pos:#s::::nil:null_#add:null_#pred:null_#succ:null_#abs:null_firstline#1:null_lcs#2:null_lcs#3:null_lcstable#1:null_lcstable#3:null_max#1:null_newline#1:null_newline#2:null_newline#7:null_right#1 Rewrite Strategy: INNERMOST ---------------------------------------- (11) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: #0 => 0 nil => 1 #false => 1 #true => 2 #EQ => 1 #GT => 2 #LT => 3 null_#add => 0 null_#and => 0 null_#ckgt => 0 null_#compare => 0 null_#eq => 0 null_#pred => 0 null_#succ => 0 null_#abs => 0 null_firstline#1 => 0 null_lcs#2 => 0 null_lcs#3 => 0 null_lcstable#1 => 0 null_lcstable#3 => 0 null_max#1 => 0 null_newline#1 => 0 null_newline#2 => 0 null_newline#7 => 0 null_right#1 => 0 ---------------------------------------- (12) Obligation: Complexity RNTS consisting of the following rules: #abs(z) -{ 1 }-> 0 :|: z = 0 #abs(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 #abs(z) -{ 1 }-> 1 + @x :|: @x >= 0, z = 1 + @x #abs(z) -{ 1 }-> 1 + (1 + @x) :|: @x >= 0, z = 1 + @x #add(z, z') -{ 0 }-> @y :|: z' = @y, z = 0, @y >= 0 #add(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 #add(z, z') -{ 0 }-> #succ(@y) :|: z = 1 + (1 + 0), z' = @y, @y >= 0 #add(z, z') -{ 0 }-> #succ(#add(1 + (1 + @x), @y)) :|: @x >= 0, z' = @y, z = 1 + (1 + (1 + @x)), @y >= 0 #add(z, z') -{ 0 }-> #pred(@y) :|: z = 1 + (1 + 0), z' = @y, @y >= 0 #add(z, z') -{ 0 }-> #pred(#add(1 + (1 + @x), @y)) :|: @x >= 0, z' = @y, z = 1 + (1 + (1 + @x)), @y >= 0 #and(z, z') -{ 0 }-> 2 :|: z = 2, z' = 2 #and(z, z') -{ 0 }-> 1 :|: z = 1, z' = 1 #and(z, z') -{ 0 }-> 1 :|: z' = 2, z = 1 #and(z, z') -{ 0 }-> 1 :|: z = 2, z' = 1 #and(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 #ckgt(z) -{ 0 }-> 2 :|: z = 2 #ckgt(z) -{ 0 }-> 1 :|: z = 1 #ckgt(z) -{ 0 }-> 1 :|: z = 3 #ckgt(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 #compare(z, z') -{ 0 }-> 3 :|: z = 0, z' = 1 + @y, @y >= 0 #compare(z, z') -{ 0 }-> 3 :|: @x >= 0, z = 1 + @x, z' = 0 #compare(z, z') -{ 0 }-> 3 :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0 #compare(z, z') -{ 0 }-> 2 :|: z = 0, z' = 1 + @y, @y >= 0 #compare(z, z') -{ 0 }-> 2 :|: @x >= 0, z = 1 + @x, z' = 0 #compare(z, z') -{ 0 }-> 2 :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0 #compare(z, z') -{ 0 }-> 1 :|: z = 0, z' = 0 #compare(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 #compare(z, z') -{ 0 }-> #compare(@x, @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0 #compare(z, z') -{ 0 }-> #compare(@y, @x) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0 #eq(z, z') -{ 0 }-> 2 :|: z = 0, z' = 0 #eq(z, z') -{ 0 }-> 2 :|: z = 1, z' = 1 #eq(z, z') -{ 0 }-> 1 :|: z = 0, z' = 1 + @y, @y >= 0 #eq(z, z') -{ 0 }-> 1 :|: @x >= 0, z = 1 + @x, z' = 0 #eq(z, z') -{ 0 }-> 1 :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0 #eq(z, z') -{ 0 }-> 1 :|: @x_1 >= 0, z = 1 + @x_1 + @x_2, @x_2 >= 0, z' = 1 #eq(z, z') -{ 0 }-> 1 :|: z = 1, @y_1 >= 0, @y_2 >= 0, z' = 1 + @y_1 + @y_2 #eq(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 #eq(z, z') -{ 0 }-> #eq(@x, @y) :|: @x >= 0, z = 1 + @x, z' = 1 + @y, @y >= 0 #eq(z, z') -{ 0 }-> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) :|: @x_1 >= 0, z = 1 + @x_1 + @x_2, @y_1 >= 0, @x_2 >= 0, @y_2 >= 0, z' = 1 + @y_1 + @y_2 #equal(z, z') -{ 1 }-> #eq(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0 #greater(z, z') -{ 1 }-> #ckgt(#compare(@x, @y)) :|: z = @x, @x >= 0, z' = @y, @y >= 0 #pred(z) -{ 0 }-> 0 :|: z = 1 + (1 + 0) #pred(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 #pred(z) -{ 0 }-> 1 + (1 + @x) :|: @x >= 0, z = 1 + (1 + (1 + @x)) #pred(z) -{ 0 }-> 1 + (1 + 0) :|: z = 0 #pred(z) -{ 0 }-> 1 + (1 + (1 + @x)) :|: @x >= 0, z = 1 + (1 + @x) #succ(z) -{ 0 }-> 0 :|: z = 1 + (1 + 0) #succ(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 #succ(z) -{ 0 }-> 1 + (1 + @x) :|: @x >= 0, z = 1 + (1 + (1 + @x)) #succ(z) -{ 0 }-> 1 + (1 + 0) :|: z = 0 #succ(z) -{ 0 }-> 1 + (1 + (1 + @x)) :|: @x >= 0, z = 1 + (1 + @x) firstline(z) -{ 1 }-> firstline#1(@l) :|: z = @l, @l >= 0 firstline#1(z) -{ 1 }-> 1 :|: z = 1 firstline#1(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 firstline#1(z) -{ 1 }-> 1 + #abs(0) + firstline(@xs) :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0 lcs(z, z') -{ 1 }-> lcs#1(lcstable(@l1, @l2)) :|: @l1 >= 0, z' = @l2, @l2 >= 0, z = @l1 lcs#1(z) -{ 1 }-> lcs#2(@m) :|: @m >= 0, z = @m lcs#2(z) -{ 1 }-> lcs#3(@l1) :|: z = 1 + @l1 + @_@2, @l1 >= 0, @_@2 >= 0 lcs#2(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 lcs#2(z) -{ 1 }-> #abs(0) :|: z = 1 lcs#3(z) -{ 1 }-> @len :|: @_@1 >= 0, z = 1 + @len + @_@1, @len >= 0 lcs#3(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 lcs#3(z) -{ 1 }-> #abs(0) :|: z = 1 lcstable(z, z') -{ 1 }-> lcstable#1(@l1, @l2) :|: @l1 >= 0, z' = @l2, @l2 >= 0, z = @l1 lcstable#1(z, z') -{ 1 }-> lcstable#2(lcstable(@xs, @l2), @l2, @x) :|: z' = @l2, @x >= 0, z = 1 + @x + @xs, @l2 >= 0, @xs >= 0 lcstable#1(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 lcstable#1(z, z') -{ 1 }-> 1 + firstline(@l2) + 1 :|: z' = @l2, z = 1, @l2 >= 0 lcstable#2(z, z', z'') -{ 1 }-> lcstable#3(@m, @l2, @x) :|: @m >= 0, z' = @l2, @x >= 0, @l2 >= 0, z = @m, z'' = @x lcstable#3(z, z', z'') -{ 1 }-> 1 :|: z' = @l2, @x >= 0, z = 1, @l2 >= 0, z'' = @x lcstable#3(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 lcstable#3(z, z', z'') -{ 1 }-> 1 + newline(@x, @l, @l2) + (1 + @l + @ls) :|: z = 1 + @l + @ls, @ls >= 0, @l >= 0, z' = @l2, @x >= 0, @l2 >= 0, z'' = @x max(z, z') -{ 1 }-> max#1(#greater(@a, @b), @a, @b) :|: @a >= 0, z = @a, z' = @b, @b >= 0 max#1(z, z', z'') -{ 1 }-> @a :|: z = 2, @a >= 0, z' = @a, @b >= 0, z'' = @b max#1(z, z', z'') -{ 1 }-> @b :|: @a >= 0, z = 1, z' = @a, @b >= 0, z'' = @b max#1(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 newline(z, z', z'') -{ 1 }-> newline#1(@l, @lastline, @y) :|: @l >= 0, z'' = @l, @lastline >= 0, z' = @lastline, z = @y, @y >= 0 newline#1(z, z', z'') -{ 1 }-> newline#2(@lastline, @x, @xs, @y) :|: @x >= 0, z = 1 + @x + @xs, @lastline >= 0, z' = @lastline, @xs >= 0, @y >= 0, z'' = @y newline#1(z, z', z'') -{ 1 }-> 1 :|: @lastline >= 0, z = 1, z' = @lastline, @y >= 0, z'' = @y newline#1(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 newline#2(z, z', z'', z1) -{ 1 }-> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) :|: @lastline' >= 0, @x >= 0, z1 = @y, z = 1 + @belowVal + @lastline', @xs >= 0, @y >= 0, z' = @x, z'' = @xs, @belowVal >= 0 newline#2(z, z', z'', z1) -{ 1 }-> 1 :|: @x >= 0, z = 1, z1 = @y, @xs >= 0, @y >= 0, z' = @x, z'' = @xs newline#2(z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0 newline#3(z, z', z'', z1, z2) -{ 1 }-> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) :|: z'' = @lastline', z1 = @x, @lastline' >= 0, @x >= 0, z = @nl, z2 = @y, z' = @belowVal, @y >= 0, @nl >= 0, @belowVal >= 0 newline#4(z, z', z'', z1, z2, z3) -{ 1 }-> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) :|: z'' = @lastline', @lastline' >= 0, @x >= 0, @rightVal >= 0, z1 = @nl, z2 = @x, z = @rightVal, z' = @belowVal, z3 = @y, @y >= 0, @belowVal >= 0, @nl >= 0 newline#5(z, z', z'', z1, z2, z3) -{ 1 }-> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) :|: z = @diagVal, @x >= 0, @rightVal >= 0, z2 = @x, z' = @belowVal, z3 = @y, z'' = @nl, z1 = @rightVal, @diagVal >= 0, @y >= 0, @belowVal >= 0, @nl >= 0 newline#6(z, z') -{ 1 }-> 1 + @elem + @nl :|: @elem >= 0, z' = @nl, @nl >= 0, z = @elem newline#7(z, z', z'', z1) -{ 1 }-> plus(@diagVal, 1 + (1 + 0)) :|: z = 2, @rightVal >= 0, z' = @belowVal, z1 = @rightVal, @diagVal >= 0, z'' = @diagVal, @belowVal >= 0 newline#7(z, z', z'', z1) -{ 1 }-> max(@belowVal, @rightVal) :|: @rightVal >= 0, z = 1, z' = @belowVal, z1 = @rightVal, @diagVal >= 0, z'' = @diagVal, @belowVal >= 0 newline#7(z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0 plus(z, z') -{ 1 }-> #add(@x, @y) :|: z = @x, @x >= 0, z' = @y, @y >= 0 right(z) -{ 1 }-> right#1(@l) :|: z = @l, @l >= 0 right#1(z) -{ 1 }-> @x :|: @x >= 0, z = 1 + @x + @xs, @xs >= 0 right#1(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 right#1(z) -{ 1 }-> #abs(0) :|: z = 1 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (13) CompleteCoflocoProof (FINISHED) Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo: eq(start(V, V3, V26, V55, V65, V71),0,[fun(V, Out)],[V >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun1(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun3(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[plus(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[firstline(V, Out)],[V >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun7(V, Out)],[V >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[lcs(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun8(V, Out)],[V >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun9(V, Out)],[V >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun10(V, Out)],[V >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[lcstable(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun11(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun12(V, V3, V26, Out)],[V >= 0,V3 >= 0,V26 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun13(V, V3, V26, Out)],[V >= 0,V3 >= 0,V26 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[max(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun14(V, V3, V26, Out)],[V >= 0,V3 >= 0,V26 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[newline(V, V3, V26, Out)],[V >= 0,V3 >= 0,V26 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun15(V, V3, V26, Out)],[V >= 0,V3 >= 0,V26 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun16(V, V3, V26, V55, Out)],[V >= 0,V3 >= 0,V26 >= 0,V55 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun17(V, V3, V26, V55, V65, Out)],[V >= 0,V3 >= 0,V26 >= 0,V55 >= 0,V65 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun18(V, V3, V26, V55, V65, V71, Out)],[V >= 0,V3 >= 0,V26 >= 0,V55 >= 0,V65 >= 0,V71 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun19(V, V3, V26, V55, V65, V71, Out)],[V >= 0,V3 >= 0,V26 >= 0,V55 >= 0,V65 >= 0,V71 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun20(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun21(V, V3, V26, V55, Out)],[V >= 0,V3 >= 0,V26 >= 0,V55 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[right(V, Out)],[V >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun22(V, Out)],[V >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun6(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun25(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun4(V, Out)],[V >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun5(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun2(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun23(V, Out)],[V >= 0]). eq(start(V, V3, V26, V55, V65, V71),0,[fun24(V, Out)],[V >= 0]). eq(fun(V, Out),1,[],[Out = 0,V = 0]). eq(fun(V, Out),1,[],[Out = 1 + V1,V1 >= 0,V = 1 + V1]). eq(fun(V, Out),1,[],[Out = 2 + V2,V2 >= 0,V = 1 + V2]). eq(fun1(V, V3, Out),1,[fun2(V4, V5, Ret)],[Out = Ret,V = V4,V4 >= 0,V3 = V5,V5 >= 0]). eq(fun3(V, V3, Out),1,[fun5(V6, V7, Ret0),fun4(Ret0, Ret1)],[Out = Ret1,V = V6,V6 >= 0,V3 = V7,V7 >= 0]). eq(plus(V, V3, Out),1,[fun6(V8, V9, Ret2)],[Out = Ret2,V = V8,V8 >= 0,V3 = V9,V9 >= 0]). eq(firstline(V, Out),1,[fun7(V10, Ret3)],[Out = Ret3,V = V10,V10 >= 0]). eq(fun7(V, Out),1,[fun(0, Ret01),firstline(V12, Ret11)],[Out = 1 + Ret01 + Ret11,V11 >= 0,V = 1 + V11 + V12,V12 >= 0]). eq(fun7(V, Out),1,[],[Out = 1,V = 1]). eq(lcs(V, V3, Out),1,[lcstable(V14, V13, Ret02),fun8(Ret02, Ret4)],[Out = Ret4,V14 >= 0,V3 = V13,V13 >= 0,V = V14]). eq(fun8(V, Out),1,[fun9(V15, Ret5)],[Out = Ret5,V15 >= 0,V = V15]). eq(fun9(V, Out),1,[fun10(V16, Ret6)],[Out = Ret6,V = 1 + V16 + V17,V16 >= 0,V17 >= 0]). eq(fun9(V, Out),1,[fun(0, Ret7)],[Out = Ret7,V = 1]). eq(fun10(V, Out),1,[],[Out = V19,V18 >= 0,V = 1 + V18 + V19,V19 >= 0]). eq(fun10(V, Out),1,[fun(0, Ret8)],[Out = Ret8,V = 1]). eq(lcstable(V, V3, Out),1,[fun11(V21, V20, Ret9)],[Out = Ret9,V21 >= 0,V3 = V20,V20 >= 0,V = V21]). eq(fun11(V, V3, Out),1,[lcstable(V24, V22, Ret03),fun12(Ret03, V22, V23, Ret10)],[Out = Ret10,V3 = V22,V23 >= 0,V = 1 + V23 + V24,V22 >= 0,V24 >= 0]). eq(fun11(V, V3, Out),1,[firstline(V25, Ret011)],[Out = 2 + Ret011,V3 = V25,V = 1,V25 >= 0]). eq(fun12(V, V3, V26, Out),1,[fun13(V29, V27, V28, Ret12)],[Out = Ret12,V29 >= 0,V3 = V27,V28 >= 0,V27 >= 0,V = V29,V26 = V28]). eq(fun13(V, V3, V26, Out),1,[newline(V31, V33, V32, Ret012)],[Out = 2 + Ret012 + V30 + V33,V = 1 + V30 + V33,V30 >= 0,V33 >= 0,V3 = V32,V31 >= 0,V32 >= 0,V26 = V31]). eq(fun13(V, V3, V26, Out),1,[],[Out = 1,V3 = V34,V35 >= 0,V = 1,V34 >= 0,V26 = V35]). eq(max(V, V3, Out),1,[fun3(V36, V37, Ret04),fun14(Ret04, V36, V37, Ret13)],[Out = Ret13,V36 >= 0,V = V36,V3 = V37,V37 >= 0]). eq(fun14(V, V3, V26, Out),1,[],[Out = V39,V38 >= 0,V = 1,V3 = V38,V39 >= 0,V26 = V39]). eq(fun14(V, V3, V26, Out),1,[],[Out = V41,V = 2,V41 >= 0,V3 = V41,V40 >= 0,V26 = V40]). eq(newline(V, V3, V26, Out),1,[fun15(V43, V44, V42, Ret14)],[Out = Ret14,V43 >= 0,V26 = V43,V44 >= 0,V3 = V44,V = V42,V42 >= 0]). eq(fun15(V, V3, V26, Out),1,[fun16(V46, V47, V48, V45, Ret15)],[Out = Ret15,V47 >= 0,V = 1 + V47 + V48,V46 >= 0,V3 = V46,V48 >= 0,V45 >= 0,V26 = V45]). eq(fun15(V, V3, V26, Out),1,[],[Out = 1,V50 >= 0,V = 1,V3 = V50,V49 >= 0,V26 = V49]). eq(fun16(V, V3, V26, V55, Out),1,[newline(V52, V51, V53, Ret05),fun17(Ret05, V56, V51, V54, V52, Ret16)],[Out = Ret16,V51 >= 0,V54 >= 0,V55 = V52,V = 1 + V51 + V56,V53 >= 0,V52 >= 0,V3 = V54,V26 = V53,V56 >= 0]). eq(fun16(V, V3, V26, V55, Out),1,[],[Out = 1,V57 >= 0,V = 1,V55 = V59,V58 >= 0,V59 >= 0,V3 = V57,V26 = V58]). eq(fun17(V, V3, V26, V55, V65, Out),1,[right(V64, Ret06),fun18(Ret06, V60, V62, V64, V61, V63, Ret17)],[Out = Ret17,V26 = V62,V55 = V61,V62 >= 0,V61 >= 0,V = V64,V65 = V63,V3 = V60,V63 >= 0,V64 >= 0,V60 >= 0]). eq(fun18(V, V3, V26, V55, V65, V71, Out),1,[right(V68, Ret07),fun19(Ret07, V66, V70, V69, V67, V72, Ret18)],[Out = Ret18,V26 = V68,V68 >= 0,V67 >= 0,V69 >= 0,V55 = V70,V65 = V67,V = V69,V3 = V66,V71 = V72,V72 >= 0,V66 >= 0,V70 >= 0]). eq(fun19(V, V3, V26, V55, V65, V71, Out),1,[fun1(V73, V78, Ret00),fun21(Ret00, V74, V77, V76, Ret08),fun20(Ret08, V75, Ret19)],[Out = Ret19,V = V77,V73 >= 0,V76 >= 0,V65 = V73,V3 = V74,V71 = V78,V26 = V75,V55 = V76,V77 >= 0,V78 >= 0,V74 >= 0,V75 >= 0]). eq(fun20(V, V3, Out),1,[],[Out = 1 + V79 + V80,V79 >= 0,V3 = V80,V80 >= 0,V = V79]). eq(fun21(V, V3, V26, V55, Out),1,[max(V81, V82, Ret20)],[Out = Ret20,V82 >= 0,V = 1,V3 = V81,V55 = V82,V83 >= 0,V26 = V83,V81 >= 0]). eq(fun21(V, V3, V26, V55, Out),1,[plus(V86, 1 + (1 + 0), Ret21)],[Out = Ret21,V = 2,V85 >= 0,V3 = V84,V55 = V85,V86 >= 0,V26 = V86,V84 >= 0]). eq(right(V, Out),1,[fun22(V87, Ret22)],[Out = Ret22,V = V87,V87 >= 0]). eq(fun22(V, Out),1,[],[Out = V89,V89 >= 0,V = 1 + V88 + V89,V88 >= 0]). eq(fun22(V, Out),1,[fun(0, Ret23)],[Out = Ret23,V = 1]). eq(fun6(V, V3, Out),0,[],[Out = V90,V3 = V90,V = 0,V90 >= 0]). eq(fun6(V, V3, Out),0,[fun23(V91, Ret24)],[Out = Ret24,V = 2,V3 = V91,V91 >= 0]). eq(fun6(V, V3, Out),0,[fun6(1 + (1 + V93), V92, Ret09),fun23(Ret09, Ret25)],[Out = Ret25,V93 >= 0,V3 = V92,V = 3 + V93,V92 >= 0]). eq(fun6(V, V3, Out),0,[fun24(V94, Ret26)],[Out = Ret26,V = 2,V3 = V94,V94 >= 0]). eq(fun6(V, V3, Out),0,[fun6(1 + (1 + V96), V95, Ret010),fun24(Ret010, Ret27)],[Out = Ret27,V96 >= 0,V3 = V95,V = 3 + V96,V95 >= 0]). eq(fun25(V, V3, Out),0,[],[Out = 1,V = 1,V3 = 1]). eq(fun25(V, V3, Out),0,[],[Out = 1,V3 = 2,V = 1]). eq(fun25(V, V3, Out),0,[],[Out = 1,V = 2,V3 = 1]). eq(fun25(V, V3, Out),0,[],[Out = 2,V = 2,V3 = 2]). eq(fun4(V, Out),0,[],[Out = 1,V = 1]). eq(fun4(V, Out),0,[],[Out = 2,V = 2]). eq(fun4(V, Out),0,[],[Out = 1,V = 3]). eq(fun5(V, V3, Out),0,[],[Out = 1,V = 0,V3 = 0]). eq(fun5(V, V3, Out),0,[],[Out = 2,V = 0,V3 = 1 + V97,V97 >= 0]). eq(fun5(V, V3, Out),0,[],[Out = 3,V = 0,V3 = 1 + V98,V98 >= 0]). eq(fun5(V, V3, Out),0,[],[Out = 3,V99 >= 0,V = 1 + V99,V3 = 0]). eq(fun5(V, V3, Out),0,[fun5(V100, V101, Ret28)],[Out = Ret28,V101 >= 0,V = 1 + V101,V3 = 1 + V100,V100 >= 0]). eq(fun5(V, V3, Out),0,[],[Out = 3,V103 >= 0,V = 1 + V103,V3 = 1 + V102,V102 >= 0]). eq(fun5(V, V3, Out),0,[],[Out = 2,V104 >= 0,V = 1 + V104,V3 = 0]). eq(fun5(V, V3, Out),0,[],[Out = 2,V105 >= 0,V = 1 + V105,V3 = 1 + V106,V106 >= 0]). eq(fun5(V, V3, Out),0,[fun5(V107, V108, Ret29)],[Out = Ret29,V107 >= 0,V = 1 + V107,V3 = 1 + V108,V108 >= 0]). eq(fun2(V, V3, Out),0,[],[Out = 2,V = 0,V3 = 0]). eq(fun2(V, V3, Out),0,[],[Out = 1,V = 0,V3 = 1 + V109,V109 >= 0]). eq(fun2(V, V3, Out),0,[],[Out = 1,V110 >= 0,V = 1 + V110,V3 = 0]). eq(fun2(V, V3, Out),0,[fun2(V112, V111, Ret30)],[Out = Ret30,V112 >= 0,V = 1 + V112,V3 = 1 + V111,V111 >= 0]). eq(fun2(V, V3, Out),0,[],[Out = 1,V114 >= 0,V = 1 + V114,V3 = 1 + V113,V113 >= 0]). eq(fun2(V, V3, Out),0,[fun2(V118, V116, Ret013),fun2(V117, V115, Ret110),fun25(Ret013, Ret110, Ret31)],[Out = Ret31,V118 >= 0,V = 1 + V117 + V118,V116 >= 0,V117 >= 0,V115 >= 0,V3 = 1 + V115 + V116]). eq(fun2(V, V3, Out),0,[],[Out = 1,V120 >= 0,V = 1 + V119 + V120,V119 >= 0,V3 = 1]). eq(fun2(V, V3, Out),0,[],[Out = 1,V = 1,V122 >= 0,V121 >= 0,V3 = 1 + V121 + V122]). eq(fun2(V, V3, Out),0,[],[Out = 2,V = 1,V3 = 1]). eq(fun23(V, Out),0,[],[Out = 2,V = 0]). eq(fun23(V, Out),0,[],[Out = 3 + V123,V123 >= 0,V = 2 + V123]). eq(fun23(V, Out),0,[],[Out = 0,V = 2]). eq(fun23(V, Out),0,[],[Out = 2 + V124,V124 >= 0,V = 3 + V124]). eq(fun24(V, Out),0,[],[Out = 2,V = 0]). eq(fun24(V, Out),0,[],[Out = 0,V = 2]). eq(fun24(V, Out),0,[],[Out = 2 + V125,V125 >= 0,V = 3 + V125]). eq(fun24(V, Out),0,[],[Out = 3 + V126,V126 >= 0,V = 2 + V126]). eq(fun6(V, V3, Out),0,[],[Out = 0,V128 >= 0,V127 >= 0,V = V128,V3 = V127]). eq(fun25(V, V3, Out),0,[],[Out = 0,V130 >= 0,V129 >= 0,V = V130,V3 = V129]). eq(fun4(V, Out),0,[],[Out = 0,V131 >= 0,V = V131]). eq(fun5(V, V3, Out),0,[],[Out = 0,V132 >= 0,V133 >= 0,V = V132,V3 = V133]). eq(fun2(V, V3, Out),0,[],[Out = 0,V134 >= 0,V135 >= 0,V = V134,V3 = V135]). eq(fun23(V, Out),0,[],[Out = 0,V136 >= 0,V = V136]). eq(fun24(V, Out),0,[],[Out = 0,V137 >= 0,V = V137]). eq(fun(V, Out),0,[],[Out = 0,V138 >= 0,V = V138]). eq(fun7(V, Out),0,[],[Out = 0,V139 >= 0,V = V139]). eq(fun9(V, Out),0,[],[Out = 0,V140 >= 0,V = V140]). eq(fun10(V, Out),0,[],[Out = 0,V141 >= 0,V = V141]). eq(fun11(V, V3, Out),0,[],[Out = 0,V143 >= 0,V142 >= 0,V = V143,V3 = V142]). eq(fun13(V, V3, V26, Out),0,[],[Out = 0,V145 >= 0,V26 = V146,V144 >= 0,V = V145,V3 = V144,V146 >= 0]). eq(fun14(V, V3, V26, Out),0,[],[Out = 0,V149 >= 0,V26 = V148,V147 >= 0,V = V149,V3 = V147,V148 >= 0]). eq(fun15(V, V3, V26, Out),0,[],[Out = 0,V152 >= 0,V26 = V151,V150 >= 0,V = V152,V3 = V150,V151 >= 0]). eq(fun16(V, V3, V26, V55, Out),0,[],[Out = 0,V55 = V156,V155 >= 0,V26 = V154,V153 >= 0,V = V155,V3 = V153,V154 >= 0,V156 >= 0]). eq(fun21(V, V3, V26, V55, Out),0,[],[Out = 0,V55 = V160,V159 >= 0,V26 = V158,V157 >= 0,V = V159,V3 = V157,V158 >= 0,V160 >= 0]). eq(fun22(V, Out),0,[],[Out = 0,V161 >= 0,V = V161]). input_output_vars(fun(V,Out),[V],[Out]). input_output_vars(fun1(V,V3,Out),[V,V3],[Out]). input_output_vars(fun3(V,V3,Out),[V,V3],[Out]). input_output_vars(plus(V,V3,Out),[V,V3],[Out]). input_output_vars(firstline(V,Out),[V],[Out]). input_output_vars(fun7(V,Out),[V],[Out]). input_output_vars(lcs(V,V3,Out),[V,V3],[Out]). input_output_vars(fun8(V,Out),[V],[Out]). input_output_vars(fun9(V,Out),[V],[Out]). input_output_vars(fun10(V,Out),[V],[Out]). input_output_vars(lcstable(V,V3,Out),[V,V3],[Out]). input_output_vars(fun11(V,V3,Out),[V,V3],[Out]). input_output_vars(fun12(V,V3,V26,Out),[V,V3,V26],[Out]). input_output_vars(fun13(V,V3,V26,Out),[V,V3,V26],[Out]). input_output_vars(max(V,V3,Out),[V,V3],[Out]). input_output_vars(fun14(V,V3,V26,Out),[V,V3,V26],[Out]). input_output_vars(newline(V,V3,V26,Out),[V,V3,V26],[Out]). input_output_vars(fun15(V,V3,V26,Out),[V,V3,V26],[Out]). input_output_vars(fun16(V,V3,V26,V55,Out),[V,V3,V26,V55],[Out]). input_output_vars(fun17(V,V3,V26,V55,V65,Out),[V,V3,V26,V55,V65],[Out]). input_output_vars(fun18(V,V3,V26,V55,V65,V71,Out),[V,V3,V26,V55,V65,V71],[Out]). input_output_vars(fun19(V,V3,V26,V55,V65,V71,Out),[V,V3,V26,V55,V65,V71],[Out]). input_output_vars(fun20(V,V3,Out),[V,V3],[Out]). input_output_vars(fun21(V,V3,V26,V55,Out),[V,V3,V26,V55],[Out]). input_output_vars(right(V,Out),[V],[Out]). input_output_vars(fun22(V,Out),[V],[Out]). input_output_vars(fun6(V,V3,Out),[V,V3],[Out]). input_output_vars(fun25(V,V3,Out),[V,V3],[Out]). input_output_vars(fun4(V,Out),[V],[Out]). input_output_vars(fun5(V,V3,Out),[V,V3],[Out]). input_output_vars(fun2(V,V3,Out),[V,V3],[Out]). input_output_vars(fun23(V,Out),[V],[Out]). input_output_vars(fun24(V,Out),[V],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. non_recursive : [fun/2] 1. recursive : [firstline/2,fun7/2] 2. non_recursive : [fun25/3] 3. recursive [non_tail,multiple] : [fun2/3] 4. non_recursive : [fun1/3] 5. non_recursive : [fun10/2] 6. non_recursive : [fun20/3] 7. non_recursive : [fun14/4] 8. non_recursive : [fun4/2] 9. recursive : [fun5/3] 10. non_recursive : [fun3/3] 11. non_recursive : [max/3] 12. non_recursive : [fun23/2] 13. non_recursive : [fun24/2] 14. recursive [non_tail] : [fun6/3] 15. non_recursive : [plus/3] 16. non_recursive : [fun21/5] 17. non_recursive : [fun19/7] 18. non_recursive : [fun22/2] 19. non_recursive : [right/2] 20. non_recursive : [fun18/7] 21. non_recursive : [fun17/6] 22. recursive [non_tail] : [fun15/4,fun16/5,newline/4] 23. non_recursive : [fun13/4] 24. non_recursive : [fun12/4] 25. recursive [non_tail] : [fun11/3,lcstable/3] 26. non_recursive : [fun9/2] 27. non_recursive : [fun8/2] 28. non_recursive : [lcs/3] 29. non_recursive : [start/6] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into fun/2 1. SCC is partially evaluated into firstline/2 2. SCC is partially evaluated into fun25/3 3. SCC is partially evaluated into fun2/3 4. SCC is completely evaluated into other SCCs 5. SCC is partially evaluated into fun10/2 6. SCC is completely evaluated into other SCCs 7. SCC is partially evaluated into fun14/4 8. SCC is partially evaluated into fun4/2 9. SCC is partially evaluated into fun5/3 10. SCC is partially evaluated into fun3/3 11. SCC is partially evaluated into max/3 12. SCC is partially evaluated into fun23/2 13. SCC is partially evaluated into fun24/2 14. SCC is partially evaluated into fun6/3 15. SCC is completely evaluated into other SCCs 16. SCC is partially evaluated into fun21/5 17. SCC is partially evaluated into fun19/7 18. SCC is partially evaluated into fun22/2 19. SCC is completely evaluated into other SCCs 20. SCC is partially evaluated into fun18/7 21. SCC is partially evaluated into fun17/6 22. SCC is partially evaluated into newline/4 23. SCC is partially evaluated into fun13/4 24. SCC is completely evaluated into other SCCs 25. SCC is partially evaluated into lcstable/3 26. SCC is partially evaluated into fun9/2 27. SCC is completely evaluated into other SCCs 28. SCC is partially evaluated into lcs/3 29. SCC is partially evaluated into start/6 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations fun/2 * CE 54 is refined into CE [118] * CE 55 is refined into CE [119] * CE 53 is refined into CE [120] * CE 56 is refined into CE [121] ### Cost equations --> "Loop" of fun/2 * CEs [118] --> Loop 77 * CEs [119] --> Loop 78 * CEs [120,121] --> Loop 79 ### Ranking functions of CR fun(V,Out) #### Partial ranking functions of CR fun(V,Out) ### Specialization of cost equations firstline/2 * CE 40 is refined into CE [122] * CE 38 is refined into CE [123] * CE 39 is refined into CE [124] ### Cost equations --> "Loop" of firstline/2 * CEs [123] --> Loop 80 * CEs [124] --> Loop 81 * CEs [122] --> Loop 82 ### Ranking functions of CR firstline(V,Out) * RF of phase [82]: [V] #### Partial ranking functions of CR firstline(V,Out) * Partial RF of phase [82]: - RF of loop [82:1]: V ### Specialization of cost equations fun25/3 * CE 95 is refined into CE [125] * CE 94 is refined into CE [126] * CE 93 is refined into CE [127] * CE 92 is refined into CE [128] * CE 91 is refined into CE [129] ### Cost equations --> "Loop" of fun25/3 * CEs [125] --> Loop 83 * CEs [126] --> Loop 84 * CEs [127] --> Loop 85 * CEs [128] --> Loop 86 * CEs [129] --> Loop 87 ### Ranking functions of CR fun25(V,V3,Out) #### Partial ranking functions of CR fun25(V,V3,Out) ### Specialization of cost equations fun2/3 * CE 61 is refined into CE [130] * CE 64 is refined into CE [131] * CE 59 is refined into CE [132] * CE 63 is refined into CE [133] * CE 58 is refined into CE [134] * CE 57 is refined into CE [135] * CE 62 is refined into CE [136,137,138,139,140] * CE 60 is refined into CE [141] ### Cost equations --> "Loop" of fun2/3 * CEs [141] --> Loop 88 * CEs [139] --> Loop 89 * CEs [138] --> Loop 90 * CEs [137] --> Loop 91 * CEs [136] --> Loop 92 * CEs [140] --> Loop 93 * CEs [130] --> Loop 94 * CEs [131] --> Loop 95 * CEs [132] --> Loop 96 * CEs [133] --> Loop 97 * CEs [134] --> Loop 98 * CEs [135] --> Loop 99 ### Ranking functions of CR fun2(V,V3,Out) * RF of phase [88,89,90,91,92,93]: [V,V3] #### Partial ranking functions of CR fun2(V,V3,Out) * Partial RF of phase [88,89,90,91,92,93]: - RF of loop [88:1,89:1,89:2,90:1,90:2,91:1,91:2,92:1,92:2,93:1,93:2]: V V3 ### Specialization of cost equations fun10/2 * CE 76 is refined into CE [142] * CE 78 is refined into CE [143] * CE 77 is refined into CE [144] ### Cost equations --> "Loop" of fun10/2 * CEs [142] --> Loop 100 * CEs [143,144] --> Loop 101 ### Ranking functions of CR fun10(V,Out) #### Partial ranking functions of CR fun10(V,Out) ### Specialization of cost equations fun14/4 * CE 82 is refined into CE [145] * CE 81 is refined into CE [146] * CE 80 is refined into CE [147] ### Cost equations --> "Loop" of fun14/4 * CEs [145] --> Loop 102 * CEs [146] --> Loop 103 * CEs [147] --> Loop 104 ### Ranking functions of CR fun14(V,V3,V26,Out) #### Partial ranking functions of CR fun14(V,V3,V26,Out) ### Specialization of cost equations fun4/2 * CE 99 is refined into CE [148] * CE 98 is refined into CE [149] * CE 97 is refined into CE [150] * CE 96 is refined into CE [151] ### Cost equations --> "Loop" of fun4/2 * CEs [148] --> Loop 105 * CEs [149] --> Loop 106 * CEs [150] --> Loop 107 * CEs [151] --> Loop 108 ### Ranking functions of CR fun4(V,Out) #### Partial ranking functions of CR fun4(V,Out) ### Specialization of cost equations fun5/3 * CE 105 is refined into CE [152] * CE 107 is refined into CE [153] * CE 109 is refined into CE [154] * CE 103 is refined into CE [155] * CE 106 is refined into CE [156] * CE 102 is refined into CE [157] * CE 101 is refined into CE [158] * CE 100 is refined into CE [159] * CE 104 is refined into CE [160] * CE 108 is refined into CE [161] ### Cost equations --> "Loop" of fun5/3 * CEs [160] --> Loop 109 * CEs [161] --> Loop 110 * CEs [152] --> Loop 111 * CEs [153] --> Loop 112 * CEs [154] --> Loop 113 * CEs [155] --> Loop 114 * CEs [156] --> Loop 115 * CEs [157] --> Loop 116 * CEs [158] --> Loop 117 * CEs [159] --> Loop 118 ### Ranking functions of CR fun5(V,V3,Out) * RF of phase [109,110]: [V/2+V3/2-1/2] #### Partial ranking functions of CR fun5(V,V3,Out) * Partial RF of phase [109,110]: - RF of loop [109:1]: V/2+V3/2-1/2 - RF of loop [110:1]: V depends on loops [109:1] V3 depends on loops [109:1] ### Specialization of cost equations fun3/3 * CE 65 is refined into CE [162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178] ### Cost equations --> "Loop" of fun3/3 * CEs [175] --> Loop 119 * CEs [173,177] --> Loop 120 * CEs [174] --> Loop 121 * CEs [168] --> Loop 122 * CEs [170] --> Loop 123 * CEs [169,171] --> Loop 124 * CEs [164] --> Loop 125 * CEs [166] --> Loop 126 * CEs [165,167] --> Loop 127 * CEs [162] --> Loop 128 * CEs [163,172,176,178] --> Loop 129 ### Ranking functions of CR fun3(V,V3,Out) #### Partial ranking functions of CR fun3(V,V3,Out) ### Specialization of cost equations max/3 * CE 79 is refined into CE [179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195] ### Cost equations --> "Loop" of max/3 * CEs [192] --> Loop 130 * CEs [194] --> Loop 131 * CEs [191] --> Loop 132 * CEs [189] --> Loop 133 * CEs [186,187,188,190] --> Loop 134 * CEs [182] --> Loop 135 * CEs [183,184,185] --> Loop 136 * CEs [179,180,181,193,195] --> Loop 137 ### Ranking functions of CR max(V,V3,Out) #### Partial ranking functions of CR max(V,V3,Out) ### Specialization of cost equations fun23/2 * CE 113 is refined into CE [196] * CE 111 is refined into CE [197] * CE 112 is refined into CE [198] * CE 110 is refined into CE [199] ### Cost equations --> "Loop" of fun23/2 * CEs [196] --> Loop 138 * CEs [197] --> Loop 139 * CEs [198] --> Loop 140 * CEs [199] --> Loop 141 ### Ranking functions of CR fun23(V,Out) #### Partial ranking functions of CR fun23(V,Out) ### Specialization of cost equations fun24/2 * CE 116 is refined into CE [200] * CE 117 is refined into CE [201] * CE 115 is refined into CE [202] * CE 114 is refined into CE [203] ### Cost equations --> "Loop" of fun24/2 * CEs [200] --> Loop 142 * CEs [201] --> Loop 143 * CEs [202] --> Loop 144 * CEs [203] --> Loop 145 ### Ranking functions of CR fun24(V,Out) #### Partial ranking functions of CR fun24(V,Out) ### Specialization of cost equations fun6/3 * CE 71 is refined into CE [204] * CE 67 is refined into CE [205,206,207,208] * CE 69 is refined into CE [209,210,211,212] * CE 66 is refined into CE [213] * CE 68 is refined into CE [214,215,216,217] * CE 70 is refined into CE [218,219,220,221] ### Cost equations --> "Loop" of fun6/3 * CEs [216,220] --> Loop 146 * CEs [217,221] --> Loop 147 * CEs [214,218] --> Loop 148 * CEs [215,219] --> Loop 149 * CEs [208,212] --> Loop 150 * CEs [207,211] --> Loop 151 * CEs [204,206,210] --> Loop 152 * CEs [205,209] --> Loop 153 * CEs [213] --> Loop 154 ### Ranking functions of CR fun6(V,V3,Out) * RF of phase [146,147,148,149]: [V-2] #### Partial ranking functions of CR fun6(V,V3,Out) * Partial RF of phase [146,147,148,149]: - RF of loop [146:1,147:1,148:1,149:1]: V-2 ### Specialization of cost equations fun21/5 * CE 87 is refined into CE [222] * CE 86 is refined into CE [223,224,225,226,227] * CE 85 is refined into CE [228,229,230,231,232,233,234] ### Cost equations --> "Loop" of fun21/5 * CEs [226,227] --> Loop 155 * CEs [225] --> Loop 156 * CEs [224] --> Loop 157 * CEs [223] --> Loop 158 * CEs [234] --> Loop 159 * CEs [233] --> Loop 160 * CEs [232] --> Loop 161 * CEs [231] --> Loop 162 * CEs [222,228,230] --> Loop 163 * CEs [229] --> Loop 164 ### Ranking functions of CR fun21(V,V3,V26,V55,Out) #### Partial ranking functions of CR fun21(V,V3,V26,V55,Out) ### Specialization of cost equations fun19/7 * CE 84 is refined into CE [235,236,237,238,239,240,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264] ### Cost equations --> "Loop" of fun19/7 * CEs [253] --> Loop 165 * CEs [249,264] --> Loop 166 * CEs [248,263] --> Loop 167 * CEs [258] --> Loop 168 * CEs [257] --> Loop 169 * CEs [256] --> Loop 170 * CEs [244] --> Loop 171 * CEs [243] --> Loop 172 * CEs [242] --> Loop 173 * CEs [239] --> Loop 174 * CEs [235,238,247,252,259,262] --> Loop 175 * CEs [246,261] --> Loop 176 * CEs [255] --> Loop 177 * CEs [241] --> Loop 178 * CEs [245,260] --> Loop 179 * CEs [254] --> Loop 180 * CEs [240] --> Loop 181 * CEs [251] --> Loop 182 * CEs [237] --> Loop 183 * CEs [250] --> Loop 184 * CEs [236] --> Loop 185 ### Ranking functions of CR fun19(V,V3,V26,V55,V65,V71,Out) #### Partial ranking functions of CR fun19(V,V3,V26,V55,V65,V71,Out) ### Specialization of cost equations fun22/2 * CE 88 is refined into CE [265] * CE 90 is refined into CE [266] * CE 89 is refined into CE [267] ### Cost equations --> "Loop" of fun22/2 * CEs [265] --> Loop 186 * CEs [266,267] --> Loop 187 ### Ranking functions of CR fun22(V,Out) #### Partial ranking functions of CR fun22(V,Out) ### Specialization of cost equations fun18/7 * CE 83 is refined into CE [268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290,291,292,293,294,295,296,297,298,299,300,301,302,303] ### Cost equations --> "Loop" of fun18/7 * CEs [303] --> Loop 188 * CEs [282,301] --> Loop 189 * CEs [283,302] --> Loop 190 * CEs [287] --> Loop 191 * CEs [269,285] --> Loop 192 * CEs [280,299] --> Loop 193 * CEs [281,300] --> Loop 194 * CEs [276,279,295,298] --> Loop 195 * CEs [277,296] --> Loop 196 * CEs [278,297] --> Loop 197 * CEs [294] --> Loop 198 * CEs [286] --> Loop 199 * CEs [268,284] --> Loop 200 * CEs [272,290] --> Loop 201 * CEs [271,289] --> Loop 202 * CEs [270,288] --> Loop 203 * CEs [275,293] --> Loop 204 * CEs [274,292] --> Loop 205 * CEs [273,291] --> Loop 206 ### Ranking functions of CR fun18(V,V3,V26,V55,V65,V71,Out) #### Partial ranking functions of CR fun18(V,V3,V26,V55,V65,V71,Out) ### Specialization of cost equations fun17/6 * CE 52 is refined into CE [304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322,323,324,325,326,327,328,329,330,331,332] ### Cost equations --> "Loop" of fun17/6 * CEs [330] --> Loop 207 * CEs [313,332] --> Loop 208 * CEs [306,316,331] --> Loop 209 * CEs [310,327] --> Loop 210 * CEs [311,328] --> Loop 211 * CEs [312,329] --> Loop 212 * CEs [325] --> Loop 213 * CEs [305,315,326] --> Loop 214 * CEs [323] --> Loop 215 * CEs [304,314,324] --> Loop 216 * CEs [309,322] --> Loop 217 * CEs [307,320] --> Loop 218 * CEs [308,321] --> Loop 219 * CEs [319] --> Loop 220 * CEs [318] --> Loop 221 * CEs [317] --> Loop 222 ### Ranking functions of CR fun17(V,V3,V26,V55,V65,Out) #### Partial ranking functions of CR fun17(V,V3,V26,V55,V65,Out) ### Specialization of cost equations newline/4 * CE 47 is refined into CE [333] * CE 50 is refined into CE [334] * CE 51 is refined into CE [335] * CE 48 is refined into CE [336] * CE 49 is refined into CE [337,338,339,340,341,342,343,344,345,346,347,348,349,350,351,352] ### Cost equations --> "Loop" of newline/4 * CEs [351] --> Loop 223 * CEs [352] --> Loop 224 * CEs [350] --> Loop 225 * CEs [347] --> Loop 226 * CEs [348] --> Loop 227 * CEs [349] --> Loop 228 * CEs [344] --> Loop 229 * CEs [343] --> Loop 230 * CEs [339] --> Loop 231 * CEs [337] --> Loop 232 * CEs [346] --> Loop 233 * CEs [345] --> Loop 234 * CEs [342] --> Loop 235 * CEs [340] --> Loop 236 * CEs [341] --> Loop 237 * CEs [338] --> Loop 238 * CEs [333,334] --> Loop 239 * CEs [335] --> Loop 240 * CEs [336] --> Loop 241 ### Ranking functions of CR newline(V,V3,V26,Out) * RF of phase [223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238]: [V3,V26] #### Partial ranking functions of CR newline(V,V3,V26,Out) * Partial RF of phase [223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238]: - RF of loop [223:1,224:1,225:1,226:1,227:1,231:1,238:1]: V26/2-1/2 - RF of loop [223:1,235:1]: V3-4 - RF of loop [224:1,225:1,229:1,230:1]: V3/2-1/2 - RF of loop [226:1,236:1]: V3-3 - RF of loop [227:1,228:1,231:1,232:1,237:1,238:1]: V3 - RF of loop [228:1,229:1,230:1,232:1,235:1,236:1,237:1]: V26 - RF of loop [233:1,234:1]: V3-1 V26-1 ### Specialization of cost equations fun13/4 * CE 46 is refined into CE [353] * CE 44 is refined into CE [354,355,356] * CE 45 is refined into CE [357] ### Cost equations --> "Loop" of fun13/4 * CEs [354] --> Loop 242 * CEs [356] --> Loop 243 * CEs [353] --> Loop 244 * CEs [355] --> Loop 245 * CEs [357] --> Loop 246 ### Ranking functions of CR fun13(V,V3,V26,Out) #### Partial ranking functions of CR fun13(V,V3,V26,Out) ### Specialization of cost equations lcstable/3 * CE 43 is refined into CE [358,359,360,361,362] * CE 41 is refined into CE [363] * CE 42 is refined into CE [364,365] ### Cost equations --> "Loop" of lcstable/3 * CEs [363] --> Loop 247 * CEs [364] --> Loop 248 * CEs [365] --> Loop 249 * CEs [362] --> Loop 250 * CEs [361] --> Loop 251 * CEs [358] --> Loop 252 * CEs [360] --> Loop 253 * CEs [359] --> Loop 254 ### Ranking functions of CR lcstable(V,V3,Out) * RF of phase [250,251,254]: [V] * RF of phase [252]: [V] * RF of phase [253]: [V] #### Partial ranking functions of CR lcstable(V,V3,Out) * Partial RF of phase [250,251,254]: - RF of loop [250:1,251:1,254:1]: V * Partial RF of phase [252]: - RF of loop [252:1]: V * Partial RF of phase [253]: - RF of loop [253:1]: V ### Specialization of cost equations fun9/2 * CE 75 is refined into CE [366] * CE 73 is refined into CE [367,368] * CE 74 is refined into CE [369] ### Cost equations --> "Loop" of fun9/2 * CEs [368] --> Loop 255 * CEs [366,367,369] --> Loop 256 ### Ranking functions of CR fun9(V,Out) #### Partial ranking functions of CR fun9(V,Out) ### Specialization of cost equations lcs/3 * CE 72 is refined into CE [370,371,372,373,374,375,376] ### Cost equations --> "Loop" of lcs/3 * CEs [376] --> Loop 257 * CEs [373] --> Loop 258 * CEs [370,371,372,374,375] --> Loop 259 ### Ranking functions of CR lcs(V,V3,Out) #### Partial ranking functions of CR lcs(V,V3,Out) ### Specialization of cost equations start/6 * CE 5 is refined into CE [377] * CE 1 is refined into CE [378] * CE 2 is refined into CE [379,380] * CE 3 is refined into CE [381,382,383,384,385,386,387,388,389,390,391,392,393] * CE 4 is refined into CE [394] * CE 6 is refined into CE [395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430] * CE 7 is refined into CE [431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466] * CE 8 is refined into CE [467] * CE 9 is refined into CE [468,469] * CE 10 is refined into CE [470,471,472] * CE 11 is refined into CE [473,474,475,476,477,478] * CE 12 is refined into CE [479,480,481,482,483,484,485,486,487,488] * CE 13 is refined into CE [489,490,491,492,493,494,495,496] * CE 14 is refined into CE [497,498] * CE 15 is refined into CE [499,500,501] * CE 16 is refined into CE [502,503] * CE 17 is refined into CE [504,505] * CE 18 is refined into CE [506,507] * CE 19 is refined into CE [508,509,510,511] * CE 20 is refined into CE [512,513,514,515,516] * CE 21 is refined into CE [517,518,519,520,521] * CE 22 is refined into CE [522,523,524,525,526,527,528] * CE 23 is refined into CE [529,530,531] * CE 24 is refined into CE [532,533,534] * CE 25 is refined into CE [535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550] * CE 26 is refined into CE [551,552,553,554,555,556,557,558,559,560,561,562,563,564,565,566,567,568,569] * CE 27 is refined into CE [570,571,572,573,574,575,576,577,578,579,580,581,582,583,584,585,586,587,588,589] * CE 28 is refined into CE [590,591,592,593,594,595,596,597,598] * CE 29 is refined into CE [599,600] * CE 30 is refined into CE [601,602] * CE 31 is refined into CE [603,604,605,606,607,608,609,610] * CE 32 is refined into CE [611,612,613,614,615] * CE 33 is refined into CE [616,617,618,619] * CE 34 is refined into CE [620,621,622,623,624,625,626,627,628] * CE 35 is refined into CE [629,630,631,632,633,634] * CE 36 is refined into CE [635,636,637,638] * CE 37 is refined into CE [639,640,641,642] ### Cost equations --> "Loop" of start/6 * CEs [486,526,626] --> Loop 260 * CEs [560,561] --> Loop 261 * CEs [543,544,582,583] --> Loop 262 * CEs [557,558,559,580] --> Loop 263 * CEs [541,578,579] --> Loop 264 * CEs [538,539,540,577] --> Loop 265 * CEs [432,439,440,451,461,542] --> Loop 266 * CEs [396,398,399,400,403,404,415,421,422,423,425] --> Loop 267 * CEs [381,385,390] --> Loop 268 * CEs [377,513,518] --> Loop 269 * CEs [576] --> Loop 270 * CEs [555] --> Loop 271 * CEs [562,563,575,584,585,586] --> Loop 272 * CEs [536] --> Loop 273 * CEs [554] --> Loop 274 * CEs [574] --> Loop 275 * CEs [450,452,453,454,455,456,533] --> Loop 276 * CEs [431,434,435,436,437,438,447,448,449,457,458,459,460,476,483,484,485,493,524,525,535,537,556,607,623,624,632] --> Loop 277 * CEs [618] --> Loop 278 * CEs [411,412,413,414,490,491,492,530,572,573,595,596,597,598,604,605,606,613,614,617] --> Loop 279 * CEs [379,380,467,499,508,509,512,517,529,590,591,593,594,611,612,616] --> Loop 280 * CEs [378,382,383,384,386,387,388,389,391,392,393,394,395,397,401,402,405,406,407,408,409,410,416,417,418,419,420,424,426,427,428,429,430,433,441,442,443,444,445,446,462,463,464,465,466,468,469,470,471,472,473,474,475,477,478,479,480,481,482,487,488,489,494,495,496,497,498,500,501,502,503,504,505,506,507,510,511,514,515,516,519,520,521,522,523,527,528,531,532,534,545,546,547,548,549,550,551,552,553,564,565,566,567,568,569,570,571,581,587,588,589,592,599,600,601,602,603,608,609,610,615,619,620,621,622,625,627,628,629,630,631,633,634,635,636,637,638,639,640,641,642] --> Loop 281 ### Ranking functions of CR start(V,V3,V26,V55,V65,V71) #### Partial ranking functions of CR start(V,V3,V26,V55,V65,V71) Computing Bounds ===================================== #### Cost of chains of fun(V,Out): * Chain [79]: 1 with precondition: [Out=0,V>=0] * Chain [78]: 1 with precondition: [V+1=Out,V>=1] * Chain [77]: 1 with precondition: [V=Out,V>=1] #### Cost of chains of firstline(V,Out): * Chain [[82],81]: 3*it(82)+2 Such that:it(82) =< V with precondition: [Out>=2,V>=Out] * Chain [[82],80]: 3*it(82)+1 Such that:it(82) =< V with precondition: [Out>=1,V>=Out] * Chain [81]: 2 with precondition: [V=1,Out=1] * Chain [80]: 1 with precondition: [Out=0,V>=0] #### Cost of chains of fun25(V,V3,Out): * Chain [87]: 0 with precondition: [V=1,V3=1,Out=1] * Chain [86]: 0 with precondition: [V=1,V3=2,Out=1] * Chain [85]: 0 with precondition: [V=2,V3=1,Out=1] * Chain [84]: 0 with precondition: [V=2,V3=2,Out=2] * Chain [83]: 0 with precondition: [Out=0,V>=0,V3>=0] #### Cost of chains of fun2(V,V3,Out): * Chain [99]: 0 with precondition: [V=0,V3=0,Out=2] * Chain [98]: 0 with precondition: [V=0,Out=1,V3>=1] * Chain [97]: 0 with precondition: [V=1,V3=1,Out=2] * Chain [96]: 0 with precondition: [V3=0,Out=1,V>=1] * Chain [95]: 0 with precondition: [Out=0,V>=0,V3>=0] * Chain [94]: 0 with precondition: [Out=1,V>=1,V3>=1] * Chain [multiple([88,89,90,91,92,93],[[99],[98],[97],[96],[95],[94]])]: 0 with precondition: [2>=Out,V>=1,V3>=1,Out>=0] #### Cost of chains of fun10(V,Out): * Chain [101]: 2 with precondition: [Out=0,V>=0] * Chain [100]: 1 with precondition: [Out>=0,V>=Out+1] #### Cost of chains of fun14(V,V3,V26,Out): * Chain [104]: 1 with precondition: [V=1,V26=Out,V3>=0,V26>=0] * Chain [103]: 1 with precondition: [V=2,V3=Out,V3>=0,V26>=0] * Chain [102]: 0 with precondition: [Out=0,V>=0,V3>=0,V26>=0] #### Cost of chains of fun4(V,Out): * Chain [108]: 0 with precondition: [V=1,Out=1] * Chain [107]: 0 with precondition: [V=2,Out=2] * Chain [106]: 0 with precondition: [V=3,Out=1] * Chain [105]: 0 with precondition: [Out=0,V>=0] #### Cost of chains of fun5(V,V3,Out): * Chain [[109,110],118]: 0 with precondition: [Out=1,V3=V,V3>=1] * Chain [[109,110],117]: 0 with precondition: [Out=2,V>=1,V3>=1,V+V3>=3] * Chain [[109,110],116]: 0 with precondition: [Out=3,V>=1,V3>=1,V+V3>=3] * Chain [[109,110],115]: 0 with precondition: [Out=2,V>=1,V3>=1,V+V3>=3] * Chain [[109,110],114]: 0 with precondition: [Out=3,V>=1,V3>=1,V+V3>=3] * Chain [[109,110],113]: 0 with precondition: [Out=0,V>=1,V3>=1] * Chain [[109,110],112]: 0 with precondition: [Out=2,V>=2,V3>=2] * Chain [[109,110],111]: 0 with precondition: [Out=3,V>=2,V3>=2] * Chain [118]: 0 with precondition: [V=0,V3=0,Out=1] * Chain [117]: 0 with precondition: [V=0,Out=2,V3>=1] * Chain [116]: 0 with precondition: [V=0,Out=3,V3>=1] * Chain [115]: 0 with precondition: [V3=0,Out=2,V>=1] * Chain [114]: 0 with precondition: [V3=0,Out=3,V>=1] * Chain [113]: 0 with precondition: [Out=0,V>=0,V3>=0] * Chain [112]: 0 with precondition: [Out=2,V>=1,V3>=1] * Chain [111]: 0 with precondition: [Out=3,V>=1,V3>=1] #### Cost of chains of fun3(V,V3,Out): * Chain [129]: 1 with precondition: [Out=0,V>=0,V3>=0] * Chain [128]: 1 with precondition: [V=0,V3=0,Out=1] * Chain [127]: 1 with precondition: [V=0,Out=0,V3>=1] * Chain [126]: 1 with precondition: [V=0,Out=1,V3>=1] * Chain [125]: 1 with precondition: [V=0,Out=2,V3>=1] * Chain [124]: 1 with precondition: [V3=0,Out=0,V>=1] * Chain [123]: 1 with precondition: [V3=0,Out=1,V>=1] * Chain [122]: 1 with precondition: [V3=0,Out=2,V>=1] * Chain [121]: 1 with precondition: [Out=0,V=V3,V>=1] * Chain [120]: 1 with precondition: [Out=1,V>=1,V3>=1] * Chain [119]: 1 with precondition: [Out=2,V>=1,V3>=1] #### Cost of chains of max(V,V3,Out): * Chain [137]: 3 with precondition: [Out=0,V>=0,V3>=0] * Chain [136]: 3 with precondition: [V=0,Out=0,V3>=1] * Chain [135]: 3 with precondition: [V=0,V3=Out,V3>=1] * Chain [134]: 3 with precondition: [V3=0,Out=0,V>=1] * Chain [133]: 3 with precondition: [V3=0,V=Out,V>=1] * Chain [132]: 2 with precondition: [Out=0,V=V3,V>=1] * Chain [131]: 3 with precondition: [V=Out,V>=1,V3>=1] * Chain [130]: 3 with precondition: [V3=Out,V>=1,V3>=1] #### Cost of chains of fun23(V,Out): * Chain [141]: 0 with precondition: [V=0,Out=2] * Chain [140]: 0 with precondition: [Out=0,V>=0] * Chain [139]: 0 with precondition: [V+1=Out,V>=2] * Chain [138]: 0 with precondition: [V=Out+1,V>=3] #### Cost of chains of fun24(V,Out): * Chain [145]: 0 with precondition: [V=0,Out=2] * Chain [144]: 0 with precondition: [Out=0,V>=0] * Chain [143]: 0 with precondition: [V+1=Out,V>=2] * Chain [142]: 0 with precondition: [V=Out+1,V>=3] #### Cost of chains of fun6(V,V3,Out): * Chain [[146,147,148,149],153]: 0 with precondition: [V3=0,V>=3,Out>=0,V>=Out] * Chain [[146,147,148,149],152]: 0 with precondition: [V>=3,V3>=0,Out>=0,V>=Out+1] * Chain [[146,147,148,149],151]: 0 with precondition: [V>=3,V3>=2,Out>=0,V+V3>=Out+1] * Chain [[146,147,148,149],150]: 0 with precondition: [V>=3,V3>=3,Out>=0,V+V3>=Out+3] * Chain [154]: 0 with precondition: [V=0,V3=Out,V3>=0] * Chain [153]: 0 with precondition: [V=2,V3=0,Out=2] * Chain [152]: 0 with precondition: [Out=0,V>=0,V3>=0] * Chain [151]: 0 with precondition: [V=2,V3+1=Out,V3>=2] * Chain [150]: 0 with precondition: [V=2,V3=Out+1,V3>=3] #### Cost of chains of fun21(V,V3,V26,V55,Out): * Chain [164]: 4 with precondition: [V=1,V3=0,V55=Out,V26>=0,V55>=1] * Chain [163]: 4 with precondition: [Out=0,V>=0,V3>=0,V26>=0,V55>=0] * Chain [162]: 4 with precondition: [V=1,V55=0,V3=Out,V3>=1,V26>=0] * Chain [161]: 3 with precondition: [V=1,Out=0,V3=V55,V3>=1,V26>=0] * Chain [160]: 4 with precondition: [V=1,V3=Out,V3>=1,V26>=0,V55>=1] * Chain [159]: 4 with precondition: [V=1,V55=Out,V3>=1,V26>=0,V55>=1] * Chain [158]: 2 with precondition: [V=2,V26=0,Out=2,V3>=0,V55>=0] * Chain [157]: 2 with precondition: [V=2,V26=2,Out=3,V3>=0,V55>=0] * Chain [156]: 2 with precondition: [V=2,Out=0,V3>=0,V26>=0,V55>=0] * Chain [155]: 2 with precondition: [V=2,V3>=0,V26>=3,V55>=0,Out>=0,V26+1>=Out] #### Cost of chains of fun19(V,V3,V26,V55,V65,V71,Out): * Chain [185]: 5 with precondition: [V=0,V65=0,V71=0,V26+3=Out,V3>=0,V26>=0,V55>=0] * Chain [184]: 5 with precondition: [V=0,V26+3=Out,V3>=0,V26>=0,V55>=0,V65>=1,V71>=1] * Chain [183]: 5 with precondition: [V=2,V65=0,V71=0,V26+4=Out,V3>=0,V26>=0,V55>=0] * Chain [182]: 5 with precondition: [V=2,V26+4=Out,V3>=0,V26>=0,V55>=0,V65>=1,V71>=1] * Chain [181]: 7 with precondition: [V3=0,V65=0,V26+V55+1=Out,V>=0,V26>=0,V55>=1,V71>=1] * Chain [180]: 7 with precondition: [V3=0,V71=0,V26+V55+1=Out,V>=0,V26>=0,V55>=1,V65>=1] * Chain [179]: 7 with precondition: [V3=0,V26+V55+1=Out,V>=0,V26>=0,V55>=1,V65>=1,V71>=1] * Chain [178]: 7 with precondition: [V55=0,V65=0,V3+V26+1=Out,V>=0,V3>=1,V26>=0,V71>=1] * Chain [177]: 7 with precondition: [V55=0,V71=0,V3+V26+1=Out,V>=0,V3>=1,V26>=0,V65>=1] * Chain [176]: 7 with precondition: [V55=0,V3+V26+1=Out,V>=0,V3>=1,V26>=0,V65>=1,V71>=1] * Chain [175]: 7 with precondition: [V26+1=Out,V>=0,V3>=0,V26>=0,V55>=0,V65>=0,V71>=0] * Chain [174]: 5 with precondition: [V65=0,V71=0,V>=3,V3>=0,V26>=0,V55>=0,Out>=V26+1,V+V26+2>=Out] * Chain [173]: 7 with precondition: [V65=0,V26+1=Out,V>=0,V3>=0,V26>=0,V55>=0,V71>=1] * Chain [172]: 7 with precondition: [V65=0,V3+V26+1=Out,V>=0,V3>=1,V26>=0,V55>=1,V71>=1] * Chain [171]: 7 with precondition: [V65=0,V26+V55+1=Out,V>=0,V3>=1,V26>=0,V55>=1,V71>=1] * Chain [170]: 7 with precondition: [V71=0,V26+1=Out,V>=0,V3>=0,V26>=0,V55>=0,V65>=1] * Chain [169]: 7 with precondition: [V71=0,V3+V26+1=Out,V>=0,V3>=1,V26>=0,V55>=1,V65>=1] * Chain [168]: 7 with precondition: [V71=0,V26+V55+1=Out,V>=0,V3>=1,V26>=0,V55>=1,V65>=1] * Chain [167]: 7 with precondition: [V3+V26+1=Out,V>=0,V3>=1,V26>=0,V55>=1,V65>=1,V71>=1] * Chain [166]: 7 with precondition: [V26+V55+1=Out,V>=0,V3>=1,V26>=0,V55>=1,V65>=1,V71>=1] * Chain [165]: 5 with precondition: [V>=3,V3>=0,V26>=0,V55>=0,V65>=1,V71>=1,Out>=V26+1,V+V26+2>=Out] #### Cost of chains of fun22(V,Out): * Chain [187]: 2 with precondition: [Out=0,V>=0] * Chain [186]: 1 with precondition: [Out>=0,V>=Out+1] #### Cost of chains of fun18(V,V3,V26,V55,V65,V71,Out): * Chain [206]: 11 with precondition: [V=0,V65=0,V3+V55+1=Out,V3>=1,V26>=0,V55>=0,V71>=1] * Chain [205]: 11 with precondition: [V=0,V71=0,V3+V55+1=Out,V3>=1,V26>=0,V55>=0,V65>=1] * Chain [204]: 11 with precondition: [V=0,V3+V55+1=Out,V3>=1,V26>=0,V55>=0,V65>=1,V71>=1] * Chain [203]: 11 with precondition: [V3=0,V65=0,V+V55+1=Out,V>=1,V26>=0,V55>=0,V71>=1] * Chain [202]: 11 with precondition: [V3=0,V71=0,V+V55+1=Out,V>=1,V26>=0,V55>=0,V65>=1] * Chain [201]: 11 with precondition: [V3=0,V+V55+1=Out,V>=1,V26>=0,V55>=0,V65>=1,V71>=1] * Chain [200]: 9 with precondition: [V65=0,V71=0,V55+3=Out,V>=0,V3>=0,V26>=0,V55>=0] * Chain [199]: 8 with precondition: [V65=0,V71=0,V55+4=Out,V>=0,V3>=0,V26>=3,V55>=0] * Chain [198]: 8 with precondition: [V65=0,V71=0,V>=0,V3>=0,V26>=4,V55>=0,Out>=V55+1,V26+V55+1>=Out] * Chain [197]: 11 with precondition: [V65=0,V+V55+1=Out,V>=1,V3>=1,V26>=0,V55>=0,V71>=1] * Chain [196]: 11 with precondition: [V65=0,V3+V55+1=Out,V>=1,V3>=1,V26>=0,V55>=0,V71>=1] * Chain [195]: 11 with precondition: [V55+1=Out,V>=0,V3>=0,V26>=0,V55>=0,V65>=0,V71>=0] * Chain [194]: 11 with precondition: [V71=0,V+V55+1=Out,V>=1,V3>=1,V26>=0,V55>=0,V65>=1] * Chain [193]: 11 with precondition: [V71=0,V3+V55+1=Out,V>=1,V3>=1,V26>=0,V55>=0,V65>=1] * Chain [192]: 9 with precondition: [V55+3=Out,V>=0,V3>=0,V26>=0,V55>=0,V65>=1,V71>=1] * Chain [191]: 8 with precondition: [V55+4=Out,V>=0,V3>=0,V26>=3,V55>=0,V65>=1,V71>=1] * Chain [190]: 11 with precondition: [V+V55+1=Out,V>=1,V3>=1,V26>=0,V55>=0,V65>=1,V71>=1] * Chain [189]: 11 with precondition: [V3+V55+1=Out,V>=1,V3>=1,V26>=0,V55>=0,V65>=1,V71>=1] * Chain [188]: 8 with precondition: [V>=0,V3>=0,V26>=4,V55>=0,V65>=1,V71>=1,Out>=V55+1,V26+V55+1>=Out] #### Cost of chains of fun17(V,V3,V26,V55,V65,Out): * Chain [222]: 14 with precondition: [V3=0,V55=0,V26>=0,V65>=1,Out>=V+2,2*V>=Out] * Chain [221]: 14 with precondition: [V3=0,V65=0,V26>=0,V55>=1,Out>=V+2,2*V>=Out] * Chain [220]: 14 with precondition: [V3=0,V26>=0,V55>=1,V65>=1,Out>=V+2,2*V>=Out] * Chain [219]: 13 with precondition: [V55=0,V65=0,V+3=Out,V>=0,V3>=0,V26>=0] * Chain [218]: 12 with precondition: [V55=0,V65=0,V+4=Out,V>=0,V3>=0,V26>=3] * Chain [217]: 12 with precondition: [V55=0,V65=0,V>=0,V3>=0,V26>=4,Out>=V+1,V+V26+1>=Out] * Chain [216]: 15 with precondition: [V55=0,V+V3+1=Out,V>=0,V3>=1,V26>=0,V65>=1] * Chain [215]: 14 with precondition: [V55=0,V3>=1,V26>=0,V65>=1,Out>=V+2,2*V>=Out] * Chain [214]: 15 with precondition: [V65=0,V+V3+1=Out,V>=0,V3>=1,V26>=0,V55>=1] * Chain [213]: 14 with precondition: [V65=0,V3>=1,V26>=0,V55>=1,Out>=V+2,2*V>=Out] * Chain [212]: 15 with precondition: [V+1=Out,V>=0,V3>=0,V26>=0,V55>=0,V65>=0] * Chain [211]: 13 with precondition: [V+3=Out,V>=0,V3>=0,V26>=0,V55>=1,V65>=1] * Chain [210]: 12 with precondition: [V+4=Out,V>=0,V3>=0,V26>=3,V55>=1,V65>=1] * Chain [209]: 15 with precondition: [V+V3+1=Out,V>=0,V3>=1,V26>=0,V55>=1,V65>=1] * Chain [208]: 12 with precondition: [V>=0,V3>=0,V26>=4,V55>=1,V65>=1,Out>=V+1,V+V26+1>=Out] * Chain [207]: 14 with precondition: [V3>=1,V26>=0,V55>=1,V65>=1,Out>=V+2,2*V>=Out] #### Cost of chains of newline(V,V3,V26,Out): * Chain [[223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238],241]: 80*it(223)+70*it(224)+81*it(228)+35*it(229)+3 Such that:aux(42) =< V3 aux(43) =< V3/2 aux(44) =< V26 aux(45) =< V26/2 it(223) =< aux(42) it(224) =< aux(42) it(228) =< aux(42) it(229) =< aux(42) it(224) =< aux(43) it(229) =< aux(43) it(223) =< aux(44) it(224) =< aux(44) it(228) =< aux(44) it(229) =< aux(44) it(223) =< aux(45) it(224) =< aux(45) with precondition: [V>=0,V3>=2,V26>=2,Out>=2] * Chain [[223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238],240]: 80*it(223)+70*it(224)+81*it(228)+35*it(229)+2 Such that:aux(46) =< V3 aux(47) =< V3/2 aux(48) =< V26 aux(49) =< V26/2 it(223) =< aux(46) it(224) =< aux(46) it(228) =< aux(46) it(229) =< aux(46) it(224) =< aux(47) it(229) =< aux(47) it(223) =< aux(48) it(224) =< aux(48) it(228) =< aux(48) it(229) =< aux(48) it(223) =< aux(49) it(224) =< aux(49) with precondition: [V>=0,V3>=1,V26>=2,Out>=2] * Chain [[223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238],239]: 80*it(223)+70*it(224)+81*it(228)+35*it(229)+2 Such that:aux(50) =< V3 aux(51) =< V3/2 aux(52) =< V26 aux(53) =< V26/2 it(223) =< aux(50) it(224) =< aux(50) it(228) =< aux(50) it(229) =< aux(50) it(224) =< aux(51) it(229) =< aux(51) it(223) =< aux(52) it(224) =< aux(52) it(228) =< aux(52) it(229) =< aux(52) it(223) =< aux(53) it(224) =< aux(53) with precondition: [V>=0,V3>=1,V26>=1,Out>=1] * Chain [241]: 3 with precondition: [V3=1,Out=1,V>=0,V26>=1] * Chain [240]: 2 with precondition: [V26=1,Out=1,V>=0,V3>=0] * Chain [239]: 2 with precondition: [Out=0,V>=0,V3>=0,V26>=0] #### Cost of chains of fun13(V,V3,V26,Out): * Chain [246]: 1 with precondition: [V=1,Out=1,V3>=0,V26>=0] * Chain [245]: 3 with precondition: [V3=1,V+2=Out,V>=1,V26>=0] * Chain [244]: 0 with precondition: [Out=0,V>=0,V3>=0,V26>=0] * Chain [243]: 3 with precondition: [V+1=Out,V>=1,V3>=0,V26>=0] * Chain [242]: 240*s(31)+210*s(32)+243*s(33)+105*s(34)+4 Such that:s(27) =< V s(28) =< V/2 s(29) =< V3 s(30) =< V3/2 s(31) =< s(27) s(32) =< s(27) s(33) =< s(27) s(34) =< s(27) s(32) =< s(28) s(34) =< s(28) s(31) =< s(29) s(32) =< s(29) s(33) =< s(29) s(34) =< s(29) s(31) =< s(30) s(32) =< s(30) with precondition: [V>=2,V3>=1,V26>=0,Out>=V+2] #### Cost of chains of lcstable(V,V3,Out): * Chain [[253],[250,251,254],249]: 22*it(250)+450*s(49)+348*s(51)+3 Such that:aux(58) =< V3 aux(63) =< V it(250) =< aux(63) aux(59) =< it(250)*aux(58) s(53) =< aux(59)*(1/2) s(49) =< aux(59) s(51) =< aux(59) s(49) =< s(53) with precondition: [Out=0,V>=3,V3>=0] * Chain [[253],[250,251,254],248]: 22*it(250)+450*s(49)+348*s(51)+6*s(56)+4 Such that:aux(65) =< V3 aux(66) =< V it(250) =< aux(66) s(56) =< aux(65) aux(59) =< it(250)*aux(65) s(53) =< aux(59)*(1/2) s(49) =< aux(59) s(51) =< aux(59) s(49) =< s(53) with precondition: [Out=0,V>=3,V3>=1] * Chain [[253],249]: 3*it(253)+3 Such that:it(253) =< V with precondition: [Out=0,V>=2,V3>=0] * Chain [[253],248]: 3*it(253)+6*s(56)+4 Such that:it(253) =< V s(55) =< V3 s(56) =< s(55) with precondition: [Out=0,V>=2,V3>=1] * Chain [[253],247]: 3*it(253)+1 Such that:it(253) =< V with precondition: [Out=0,V>=1,V3>=0] * Chain [[250,251,254],249]: 19*it(250)+450*s(49)+348*s(51)+3 Such that:aux(58) =< V3 aux(62) =< V it(250) =< aux(62) aux(59) =< it(250)*aux(58) s(53) =< aux(59)*(1/2) s(49) =< aux(59) s(51) =< aux(59) s(49) =< s(53) with precondition: [V>=2,V3>=0,Out>=3] * Chain [[250,251,254],248]: 19*it(250)+450*s(49)+348*s(51)+6*s(56)+4 Such that:aux(64) =< V aux(65) =< V3 s(56) =< aux(65) it(250) =< aux(64) aux(59) =< it(250)*aux(65) s(53) =< aux(59)*(1/2) s(49) =< aux(59) s(51) =< aux(59) s(49) =< s(53) with precondition: [V>=2,V3>=1,Out>=4] * Chain [249]: 3 with precondition: [V=1,Out=2,V3>=0] * Chain [248]: 6*s(56)+4 Such that:s(55) =< V3 s(56) =< s(55) with precondition: [V=1,Out>=3,V3+2>=Out] * Chain [247]: 1 with precondition: [Out=0,V>=0,V3>=0] #### Cost of chains of fun9(V,Out): * Chain [256]: 3 with precondition: [Out=0,V>=0] * Chain [255]: 2 with precondition: [Out>=0,V>=Out+2] #### Cost of chains of lcs(V,V3,Out): * Chain [259]: 24*s(93)+91*s(96)+1800*s(100)+1392*s(101)+9 Such that:aux(71) =< V aux(72) =< V3 s(96) =< aux(71) s(93) =< aux(72) s(98) =< s(96)*aux(72) s(99) =< s(98)*(1/2) s(100) =< s(98) s(101) =< s(98) s(100) =< s(99) with precondition: [Out=0,V>=0,V3>=0] * Chain [258]: 6*s(111)+8 Such that:s(110) =< V3 s(111) =< s(110) with precondition: [V=1,V3>=1,Out>=0,V3>=Out] * Chain [257]: 6*s(114)+38*s(115)+900*s(118)+696*s(119)+8 Such that:s(112) =< V s(113) =< V3 s(114) =< s(113) s(115) =< s(112) s(116) =< s(115)*s(113) s(117) =< s(116)*(1/2) s(118) =< s(116) s(119) =< s(116) s(118) =< s(117) with precondition: [V>=2,V3>=0,Out>=0] #### Cost of chains of start(V,V3,V26,V55,V65,V71): * Chain [281]: 240*s(124)+210*s(125)+243*s(126)+105*s(127)+444*s(129)+240*s(138)+210*s(139)+243*s(140)+105*s(141)+399*s(144)+8100*s(148)+6264*s(149)+450*s(178)+2610*s(186)+2520*s(187)+2916*s(188)+1530*s(189)+1680*s(266)+1470*s(267)+1701*s(268)+735*s(269)+240*s(374)+210*s(375)+243*s(376)+105*s(377)+20 Such that:s(121) =< 1 s(120) =< 2 s(134) =< V3+2 s(135) =< V3/2+1 aux(75) =< V aux(76) =< V/2 aux(77) =< V3 aux(78) =< V3/2 aux(79) =< V26 aux(80) =< V26/2 s(124) =< s(120) s(125) =< s(120) s(126) =< s(120) s(127) =< s(120) s(125) =< s(121) s(127) =< s(121) s(124) =< aux(77) s(125) =< aux(77) s(126) =< aux(77) s(127) =< aux(77) s(124) =< aux(78) s(125) =< aux(78) s(144) =< aux(75) s(129) =< aux(77) s(146) =< s(144)*aux(77) s(147) =< s(146)*(1/2) s(148) =< s(146) s(149) =< s(146) s(148) =< s(147) s(178) =< aux(77) s(178) =< aux(78) s(186) =< aux(77) s(187) =< aux(77) s(188) =< aux(77) s(189) =< aux(77) s(187) =< aux(78) s(189) =< aux(78) s(186) =< aux(75) s(187) =< aux(75) s(188) =< aux(75) s(189) =< aux(75) s(186) =< aux(76) s(187) =< aux(76) s(266) =< aux(75) s(267) =< aux(75) s(268) =< aux(75) s(269) =< aux(75) s(267) =< aux(76) s(269) =< aux(76) s(266) =< aux(79) s(267) =< aux(79) s(268) =< aux(79) s(269) =< aux(79) s(266) =< aux(80) s(267) =< aux(80) s(374) =< aux(77) s(375) =< aux(77) s(376) =< aux(77) s(377) =< aux(77) s(375) =< aux(78) s(377) =< aux(78) s(374) =< aux(79) s(375) =< aux(79) s(376) =< aux(79) s(377) =< aux(79) s(374) =< aux(80) s(375) =< aux(80) s(138) =< s(134) s(139) =< s(134) s(140) =< s(134) s(141) =< s(134) s(139) =< s(135) s(141) =< s(135) s(138) =< aux(77) s(139) =< aux(77) s(140) =< aux(77) s(141) =< aux(77) s(138) =< aux(78) s(139) =< aux(78) with precondition: [V>=0] * Chain [280]: 18*s(379)+8 Such that:aux(81) =< V3 s(379) =< aux(81) with precondition: [V=1] * Chain [279]: 19 with precondition: [V=2] * Chain [278]: 0 with precondition: [V=3] * Chain [277]: 1440*s(388)+1260*s(389)+1458*s(390)+630*s(391)+19 Such that:aux(82) =< V aux(83) =< V/2 aux(84) =< V26 aux(85) =< V26/2 s(388) =< aux(82) s(389) =< aux(82) s(390) =< aux(82) s(391) =< aux(82) s(389) =< aux(83) s(391) =< aux(83) s(388) =< aux(84) s(389) =< aux(84) s(390) =< aux(84) s(391) =< aux(84) s(388) =< aux(85) s(389) =< aux(85) with precondition: [V3=0,V>=1] * Chain [276]: 18 with precondition: [V26=1,V>=0,V3>=0] * Chain [275]: 7 with precondition: [V3=0,V65=0,V>=0,V26>=0,V55>=1,V71>=1] * Chain [274]: 11 with precondition: [V3=0,V65=0,V>=1,V26>=0,V55>=0,V71>=1] * Chain [273]: 14 with precondition: [V3=0,V65=0,V>=2,V26>=0,V55>=1] * Chain [272]: 11 with precondition: [V71=0,V>=0,V3>=0,V26>=0,V55>=0,V65>=1] * Chain [271]: 11 with precondition: [V3=0,V71=0,V>=1,V26>=0,V55>=0,V65>=1] * Chain [270]: 7 with precondition: [V3=0,V>=0,V26>=0,V55>=1,V65>=1,V71>=1] * Chain [269]: 4 with precondition: [V3=1,V>=1,V26>=0] * Chain [268]: 12*s(433)+38*s(437)+900*s(440)+696*s(441)+9 Such that:s(434) =< V aux(86) =< 1 s(433) =< aux(86) s(437) =< s(434) s(438) =< s(437)*aux(86) s(439) =< s(438)*(1/2) s(440) =< s(438) s(441) =< s(438) s(440) =< s(439) with precondition: [V3=1,V>=2] * Chain [267]: 1440*s(446)+1260*s(447)+1458*s(448)+630*s(449)+20 Such that:aux(87) =< V aux(88) =< V/2 aux(89) =< V3 aux(90) =< V3/2 s(446) =< aux(89) s(447) =< aux(89) s(448) =< aux(89) s(449) =< aux(89) s(447) =< aux(90) s(449) =< aux(90) s(446) =< aux(87) s(447) =< aux(87) s(448) =< aux(87) s(449) =< aux(87) s(446) =< aux(88) s(447) =< aux(88) with precondition: [V26=0,V>=1,V3>=1] * Chain [266]: 720*s(494)+630*s(495)+729*s(496)+315*s(497)+19 Such that:aux(91) =< V aux(92) =< V/2 aux(93) =< V26 aux(94) =< V26/2 s(494) =< aux(91) s(495) =< aux(91) s(496) =< aux(91) s(497) =< aux(91) s(495) =< aux(92) s(497) =< aux(92) s(494) =< aux(93) s(495) =< aux(93) s(496) =< aux(93) s(497) =< aux(93) s(494) =< aux(94) s(495) =< aux(94) with precondition: [V55=0,V>=2,V3>=1,V26>=0] * Chain [265]: 13 with precondition: [V55=0,V65=0,V>=0,V3>=0,V26>=0] * Chain [264]: 15 with precondition: [V55=0,V>=0,V3>=1,V26>=0,V65>=1] * Chain [263]: 9 with precondition: [V65=0,V71=0,V>=0,V3>=0,V26>=0,V55>=0] * Chain [262]: 15 with precondition: [V65=0,V>=0,V3>=1,V26>=0,V55>=1] * Chain [261]: 11 with precondition: [V65=0,V>=1,V3>=1,V26>=0,V55>=0,V71>=1] * Chain [260]: 2 with precondition: [V=V3,V>=1] Closed-form bounds of start(V,V3,V26,V55,V65,V71): ------------------------------------- * Chain [281] with precondition: [V>=0] - Upper bound: 5985*V+1616+14364*V*nat(V3)+nat(V3)*11268+nat(V3+2)*798 - Complexity: n^2 * Chain [280] with precondition: [V=1] - Upper bound: nat(V3)*18+8 - Complexity: n * Chain [279] with precondition: [V=2] - Upper bound: 19 - Complexity: constant * Chain [278] with precondition: [V=3] - Upper bound: 0 - Complexity: constant * Chain [277] with precondition: [V3=0,V>=1] - Upper bound: 4788*V+19 - Complexity: n * Chain [276] with precondition: [V26=1,V>=0,V3>=0] - Upper bound: 18 - Complexity: constant * Chain [275] with precondition: [V3=0,V65=0,V>=0,V26>=0,V55>=1,V71>=1] - Upper bound: 7 - Complexity: constant * Chain [274] with precondition: [V3=0,V65=0,V>=1,V26>=0,V55>=0,V71>=1] - Upper bound: 11 - Complexity: constant * Chain [273] with precondition: [V3=0,V65=0,V>=2,V26>=0,V55>=1] - Upper bound: 14 - Complexity: constant * Chain [272] with precondition: [V71=0,V>=0,V3>=0,V26>=0,V55>=0,V65>=1] - Upper bound: 11 - Complexity: constant * Chain [271] with precondition: [V3=0,V71=0,V>=1,V26>=0,V55>=0,V65>=1] - Upper bound: 11 - Complexity: constant * Chain [270] with precondition: [V3=0,V>=0,V26>=0,V55>=1,V65>=1,V71>=1] - Upper bound: 7 - Complexity: constant * Chain [269] with precondition: [V3=1,V>=1,V26>=0] - Upper bound: 4 - Complexity: constant * Chain [268] with precondition: [V3=1,V>=2] - Upper bound: 1634*V+21 - Complexity: n * Chain [267] with precondition: [V26=0,V>=1,V3>=1] - Upper bound: 4788*V3+20 - Complexity: n * Chain [266] with precondition: [V55=0,V>=2,V3>=1,V26>=0] - Upper bound: 2394*V+19 - Complexity: n * Chain [265] with precondition: [V55=0,V65=0,V>=0,V3>=0,V26>=0] - Upper bound: 13 - Complexity: constant * Chain [264] with precondition: [V55=0,V>=0,V3>=1,V26>=0,V65>=1] - Upper bound: 15 - Complexity: constant * Chain [263] with precondition: [V65=0,V71=0,V>=0,V3>=0,V26>=0,V55>=0] - Upper bound: 9 - Complexity: constant * Chain [262] with precondition: [V65=0,V>=0,V3>=1,V26>=0,V55>=1] - Upper bound: 15 - Complexity: constant * Chain [261] with precondition: [V65=0,V>=1,V3>=1,V26>=0,V55>=0,V71>=1] - Upper bound: 11 - Complexity: constant * Chain [260] with precondition: [V=V3,V>=1] - Upper bound: 2 - Complexity: constant ### Maximum cost of start(V,V3,V26,V55,V65,V71): max([max([19,nat(V3)*4770+12+(nat(V3)*18+8)]),1634*V+19+max([2,1197*V+1597+14364*V*nat(V3)+nat(V3)*11268+nat(V3+2)*798+2394*V+760*V])]) Asymptotic class: n^2 * Total analysis performed in 4147 ms. ---------------------------------------- (14) BOUNDS(1, n^2)