(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)
(DATATYPES
    A = µX.< #0, #neg(X), #pos(X), #s(X), ::(X, X), nil, #false, #true, #EQ, #GT, #LT >)
(SIGNATURES
    #abs :: [A] -> A
    #equal :: [A x A] -> A
    #greater :: [A x A] -> A
    + :: [A x A] -> A
    firstline :: [A] -> A
    firstline#1 :: [A] -> A
    lcs :: [A x A] -> A
    lcs#1 :: [A] -> A
    lcs#2 :: [A] -> A
    lcs#3 :: [A] -> A
    lcstable :: [A x A] -> A
    lcstable#1 :: [A x A] -> A
    lcstable#2 :: [A x A x A] -> A
    lcstable#3 :: [A x A x A] -> A
    max :: [A x A] -> A
    max#1 :: [A x A x A] -> A
    newline :: [A x A x A] -> A
    newline#1 :: [A x A x A] -> A
    newline#2 :: [A x A x A x A] -> A
    newline#3 :: [A x A x A x A x A] -> A
    newline#4 :: [A x A x A x A x A x A] -> A
    newline#5 :: [A x A x A x A x A x A] -> A
    newline#6 :: [A x A] -> A
    newline#7 :: [A x A x A x A] -> A
    right :: [A] -> A
    right#1 :: [A] -> A
    #add :: [A x A] -> A
    #and :: [A x A] -> A
    #ckgt :: [A] -> A
    #compare :: [A x A] -> A
    #eq :: [A x A] -> A
    #pred :: [A] -> A
    #succ :: [A] -> A)
(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))))