(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 = < #false, #true >
   b = µX. < #0, #neg(X), #pos(X), #s(X), dd(X,X), nil >
   c = < #EQ, #GT, #LT >
 )

(SIGNATURES
   #abs :: b -> b
   #equal :: b x b -> a
   #eq :: b x b -> a
   #greater :: b x b -> a
   #compare :: b x b -> c
   #ckgt :: c -> a
   add :: b x b -> b
   #add :: b x b -> b
   firstline :: b -> b
   firstline#1 :: b -> b
   lcs :: b x b -> b
   lcstable :: b x b -> b
   lcs#1 :: b -> b
   lcs#2 :: b -> b
   lcs#3 :: b -> b
   lcstable#1 :: b x b -> b
   lcstable#2 :: b x b x b -> b
   lcstable#3 :: b x b x b -> b
   newline :: b x b x b -> b
   max :: b x b -> b
   max#1 :: a x b x b -> b
   newline#1 :: b x b x b -> b
   newline#2 :: b x b x b x b -> b
   newline#3 :: b x b x b x b x b -> b
   right :: b -> b
   newline#4 :: b x b x b x b x b x b -> b
   newline#5 :: b x b x b x b x b x b -> b
   newline#7 :: a x b x b x b -> b
   newline#6 :: b x b -> b
   right#1 :: b -> b
   #pred :: b -> b
   #succ :: b -> b
   #and :: a x 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))
    add(@x,@y) -> #add(@x,@y)
    firstline(@l) -> firstline#1(@l)
    firstline#1(dd(@x,@xs)) -> dd(#abs(#0),firstline(@xs))
    firstline#1(nil) -> nil
    lcs(@l1,@l2) -> lcs#1(lcstable(@l1,@l2))
    lcs#1(@m) -> lcs#2(@m)
    lcs#2(dd(@l1,@'@2)) -> lcs#3(@l1)
    lcs#2(nil) -> #abs(#0)
    lcs#3(dd(@len,@'@1)) -> @len
    lcs#3(nil) -> #abs(#0)
    lcstable(@l1,@l2) -> lcstable#1(@l1,@l2)
    lcstable#1(dd(@x,@xs),@l2) -> lcstable#2(lcstable(@xs,@l2),@l2,@x)
    lcstable#1(nil,@l2) -> dd(firstline(@l2),nil)
    lcstable#2(@m,@l2,@x) -> lcstable#3(@m,@l2,@x)
    lcstable#3(dd(@l,@ls),@l2,@x) -> dd(newline(@x,@l,@l2),dd(@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(dd(@x,@xs),@lastline,@y) -> newline#2(@lastline,@x,@xs,@y)
    newline#1(nil,@lastline,@y) -> nil
    newline#2(dd(@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) -> dd(@elem,@nl)
    newline#7(#false,@belowVal,@diagVal,@rightVal) -> max(@belowVal,@rightVal)
    newline#7(#true,@belowVal,@diagVal,@rightVal) -> add(@diagVal,#pos(#s(#0)))
    right(@l) -> right#1(@l)
    right#1(dd(@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(dd(@x'1,@x'2),dd(@y'1,@y'2)) -> #and(#eq(@x'1,@y'1),#eq(@x'2,@y'2))
    #eq(dd(@x'1,@x'2),nil) -> #false
    #eq(nil,dd(@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))))