(STARTTERM
    CONSTRUCTOR-BASED)
(STRATEGY
    INNERMOST)

(VAR
    @_@1 @_@2 @a @b @belowVal @diagVal @elem @l @l1 @l2 @lastline @lastline' @len @ls @m @nl @rightVal @x @x_1 @x_2 @xs @y @y_1 @y_2)
(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))))
(COMMENT
    This TRS was automatically generated from the resource aware ML program 'longestCommonSubsequence.raml', c.f. http://raml.tcs.ifi.lmu.de/)