The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

0 CpxRelTRS
↳1 DecreasingLoopProof (⇔, 4247 ms)
↳2 BOUNDS(n^1, INF)
↳3 RenamingProof (⇔, 0 ms)
↳4 CpxRelTRS
    ↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 typed CpxTrs
    ↳7 OrderProof (LOWER BOUND(ID), 0 ms)
    ↳8 typed CpxTrs
    ↳9 RewriteLemmaProof (LOWER BOUND(ID), 12.1 s)
    ↳10 BEST
        ↳11 typed CpxTrs
            ↳12 RewriteLemmaProof (LOWER BOUND(ID), 818 ms)
            ↳13 BEST
                ↳14 typed CpxTrs
                    ↳15 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)
                    ↳16 typed CpxTrs
                    ↳17 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)
                    ↳18 typed CpxTrs
                    ↳19 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)
                    ↳20 typed CpxTrs
                    ↳21 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)
                    ↳22 typed CpxTrs
                    ↳23 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)
                    ↳24 typed CpxTrs
                    ↳25 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)
                    ↳26 typed CpxTrs
                    ↳27 NoRewriteLemmaProof (LOWER BOUND(ID), 0 ms)
                    ↳28 typed CpxTrs
                    ↳29 LowerBoundsProof (⇔, 0 ms)
                    ↳30 BOUNDS(1, INF)
                ↳31 typed CpxTrs
                    ↳32 LowerBoundsProof (⇔, 0 ms)
                    ↳33 BOUNDS(1, INF)
        ↳34 typed CpxTrs
            ↳35 LowerBoundsProof (⇔, 0 ms)
            ↳36 BOUNDS(1, INF)

(0) Obligation:

Runtime Complexity Relative TRS:
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: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
firstline(::(@x311179_8, @xs311180_8)) →+ ::(#abs(#0), firstline(@xs311180_8))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@xs311180_8 / ::(@x311179_8, @xs311180_8)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
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: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
#eq, #compare, #add, firstline, firstline#1, lcstable, lcstable#1, newline, newline#1

They will be analysed ascendingly in the following order:
firstline = firstline#1
firstline < lcstable#1
lcstable = lcstable#1
newline = newline#1

(8) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

The following defined symbols remain to be analysed:
#eq, #compare, #add, firstline, firstline#1, lcstable, lcstable#1, newline, newline#1

They will be analysed ascendingly in the following order:
firstline = firstline#1
firstline < lcstable#1
lcstable = lcstable#1
newline = newline#1

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)

Induction Base:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(0), gen_#0:#neg:#pos:#s::::nil4_8(0)) →RΩ(0)
#true

Induction Step:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(+(n6_8, 1)), gen_#0:#neg:#pos:#s::::nil4_8(+(n6_8, 1))) →RΩ(0)
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) →IH
#true

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).

(10) Complex Obligation (BEST)

(11) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Lemmas:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

The following defined symbols remain to be analysed:
#compare, #add, firstline, firstline#1, lcstable, lcstable#1, newline, newline#1

They will be analysed ascendingly in the following order:
firstline = firstline#1
firstline < lcstable#1
lcstable = lcstable#1
newline = newline#1

(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
#compare(gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8), gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8)) → #EQ, rt ∈ Ω(0)

Induction Base:
#compare(gen_#0:#neg:#pos:#s::::nil4_8(0), gen_#0:#neg:#pos:#s::::nil4_8(0)) →RΩ(0)
#EQ

Induction Step:
#compare(gen_#0:#neg:#pos:#s::::nil4_8(+(n4227307_8, 1)), gen_#0:#neg:#pos:#s::::nil4_8(+(n4227307_8, 1))) →RΩ(0)
#compare(gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8), gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8)) →IH
#EQ

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n0).

(13) Complex Obligation (BEST)

(14) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Lemmas:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)
#compare(gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8), gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

The following defined symbols remain to be analysed:
#add, firstline, firstline#1, lcstable, lcstable#1, newline, newline#1

They will be analysed ascendingly in the following order:
firstline = firstline#1
firstline < lcstable#1
lcstable = lcstable#1
newline = newline#1

(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol #add.

(16) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Lemmas:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)
#compare(gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8), gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

The following defined symbols remain to be analysed:
newline#1, firstline, firstline#1, lcstable, lcstable#1, newline

They will be analysed ascendingly in the following order:
firstline = firstline#1
firstline < lcstable#1
lcstable = lcstable#1
newline = newline#1

(17) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol newline#1.

(18) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Lemmas:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)
#compare(gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8), gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

The following defined symbols remain to be analysed:
newline, firstline, firstline#1, lcstable, lcstable#1

They will be analysed ascendingly in the following order:
firstline = firstline#1
firstline < lcstable#1
lcstable = lcstable#1
newline = newline#1

(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol newline.

(20) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Lemmas:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)
#compare(gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8), gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

The following defined symbols remain to be analysed:
firstline#1, firstline, lcstable, lcstable#1

They will be analysed ascendingly in the following order:
firstline = firstline#1
firstline < lcstable#1
lcstable = lcstable#1

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol firstline#1.

(22) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Lemmas:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)
#compare(gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8), gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

The following defined symbols remain to be analysed:
firstline, lcstable, lcstable#1

They will be analysed ascendingly in the following order:
firstline = firstline#1
firstline < lcstable#1
lcstable = lcstable#1

(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol firstline.

(24) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Lemmas:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)
#compare(gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8), gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

The following defined symbols remain to be analysed:
lcstable#1, lcstable

They will be analysed ascendingly in the following order:
lcstable = lcstable#1

(25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol lcstable#1.

(26) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Lemmas:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)
#compare(gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8), gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

The following defined symbols remain to be analysed:
lcstable

They will be analysed ascendingly in the following order:
lcstable = lcstable#1

(27) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol lcstable.

(28) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Lemmas:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)
#compare(gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8), gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

No more defined symbols left to analyse.

(29) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)

(30) BOUNDS(1, INF)

(31) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Lemmas:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)
#compare(gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8), gen_#0:#neg:#pos:#s::::nil4_8(n4227307_8)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

No more defined symbols left to analyse.

(32) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)

(33) BOUNDS(1, INF)

(34) Obligation:

Innermost TRS:
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)
#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)))

Types:
#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
+' :: #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
hole_#0:#neg:#pos:#s::::nil1_8 :: #0:#neg:#pos:#s::::nil
hole_#false:#true2_8 :: #false:#true
hole_#EQ:#GT:#LT3_8 :: #EQ:#GT:#LT
gen_#0:#neg:#pos:#s::::nil4_8 :: Nat → #0:#neg:#pos:#s::::nil

Lemmas:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s::::nil4_8(0) ⇔ #0
gen_#0:#neg:#pos:#s::::nil4_8(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s::::nil4_8(x))

No more defined symbols left to analyse.

(35) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
#eq(gen_#0:#neg:#pos:#s::::nil4_8(n6_8), gen_#0:#neg:#pos:#s::::nil4_8(n6_8)) → #true, rt ∈ Ω(0)

(36) BOUNDS(1, INF)