MAYBE

Problem:
 *(x,*(y,z)) -> *(*(x,y),z)
 *(*(x,y),z) -> *(x,*(y,z))
 eq(x,y) -> eq(y,x)
 eq(a(),a()) -> T()
 eq(a(),*(x,y)) -> F()
 eq(*(a(),x),*(a(),y)) -> eq(x,y)
 rep(0(),x) -> nil()
 rep(s(x),y) -> *(x,rep(x,y))
 hd(*(c(x),y)) -> x
 lt(*(x,c(y))) -> y
 tl(*(c(x),y)) -> y
 lem1(x) -> eq(*(hd(x),tl(x)),x)
 lem2(*(x,y)) -> eq(lt(*(x,y)),lt(tl(*(x,y))))
 +(x,y) -> +(y,x)
 +(+(x,y),z) -> +(x,+(y,z))
 +(0(),x) -> x
 +(s(x),y) -> s(+(x,y))

Proof:
 sorted: (order)
 0:*(x,*(y,z)) -> *(*(x,y),z)
   *(*(x,y),z) -> *(x,*(y,z))
   eq(x,y) -> eq(y,x)
   eq(a(),a()) -> T()
   eq(a(),*(x,y)) -> F()
   eq(*(a(),x),*(a(),y)) -> eq(x,y)
   rep(0(),x) -> nil()
   rep(s(x),y) -> *(x,rep(x,y))
   hd(*(c(x),y)) -> x
   lt(*(x,c(y))) -> y
   tl(*(c(x),y)) -> y
   lem1(x) -> eq(*(hd(x),tl(x)),x)
   +(x,y) -> +(y,x)
   +(+(x,y),z) -> +(x,+(y,z))
   +(0(),x) -> x
   +(s(x),y) -> s(+(x,y))
 1:*(x,*(y,z)) -> *(*(x,y),z)
   *(*(x,y),z) -> *(x,*(y,z))
   eq(x,y) -> eq(y,x)
   eq(a(),a()) -> T()
   eq(a(),*(x,y)) -> F()
   eq(*(a(),x),*(a(),y)) -> eq(x,y)
   rep(0(),x) -> nil()
   rep(s(x),y) -> *(x,rep(x,y))
   hd(*(c(x),y)) -> x
   lt(*(x,c(y))) -> y
   tl(*(c(x),y)) -> y
   lem2(*(x,y)) -> eq(lt(*(x,y)),lt(tl(*(x,y))))
   +(x,y) -> +(y,x)
   +(+(x,y),z) -> +(x,+(y,z))
   +(0(),x) -> x
   +(s(x),y) -> s(+(x,y))
 -----
 sorts
   [0>2, 1>2, 1>5, 2>3, 2>4, 2>6, 5>9, 6>7, 7>8, 8>9, 9>10, 9>11, 9>12, 9>13, 9>14, 9>18, 12>16,
    14>15, 16>17]
 sort attachment (non-strict)
   * : 9 x 9 -> 9
   eq : 6 x 6 -> 2
   a : 18
   T : 4
   F : 3
   rep : 12 x 11 -> 9
   0 : 17
   nil : 10
   s : 16 -> 16
   hd : 9 -> 9
   c : 15 -> 14
   lt : 8 -> 7
   tl : 9 -> 9
   lem1 : 13 -> 0
   lem2 : 5 -> 1
   + : 16 x 16 -> 16
 -----
 0:*(x,*(y,z)) -> *(*(x,y),z)
   *(*(x,y),z) -> *(x,*(y,z))
   eq(x,y) -> eq(y,x)
   eq(a(),a()) -> T()
   eq(a(),*(x,y)) -> F()
   eq(*(a(),x),*(a(),y)) -> eq(x,y)
   rep(0(),x) -> nil()
   rep(s(x),y) -> *(x,rep(x,y))
   hd(*(c(x),y)) -> x
   lt(*(x,c(y))) -> y
   tl(*(c(x),y)) -> y
   lem1(x) -> eq(*(hd(x),tl(x)),x)
   +(x,y) -> +(y,x)
   +(+(x,y),z) -> +(x,+(y,z))
   +(0(),x) -> x
   +(s(x),y) -> s(+(x,y))
   sorted: (order)
   0:*(x,*(y,z)) -> *(*(x,y),z)
     *(*(x,y),z) -> *(x,*(y,z))
     rep(0(),x) -> nil()
     rep(s(x),y) -> *(x,rep(x,y))
     hd(*(c(x),y)) -> x
     lt(*(x,c(y))) -> y
     tl(*(c(x),y)) -> y
     +(x,y) -> +(y,x)
     +(+(x,y),z) -> +(x,+(y,z))
     +(0(),x) -> x
     +(s(x),y) -> s(+(x,y))
   1:*(x,*(y,z)) -> *(*(x,y),z)
     *(*(x,y),z) -> *(x,*(y,z))
     eq(x,y) -> eq(y,x)
     eq(a(),a()) -> T()
     eq(a(),*(x,y)) -> F()
     eq(*(a(),x),*(a(),y)) -> eq(x,y)
     rep(0(),x) -> nil()
     rep(s(x),y) -> *(x,rep(x,y))
     hd(*(c(x),y)) -> x
     tl(*(c(x),y)) -> y
     lem1(x) -> eq(*(hd(x),tl(x)),x)
     +(x,y) -> +(y,x)
     +(+(x,y),z) -> +(x,+(y,z))
     +(0(),x) -> x
     +(s(x),y) -> s(+(x,y))
   -----
   sorts
     [0>5, 1>2, 2>3, 2>4, 2>6, 5>7, 6>7, 7>8, 7>9, 7>10, 7>11, 7>12, 7>16, 10>14, 12>13, 14>15]
   sort attachment (non-strict)
     * : 7 x 7 -> 7
     eq : 6 x 6 -> 2
     a : 16
     T : 4
     F : 3
     rep : 10 x 9 -> 7
     0 : 15
     nil : 8
     s : 14 -> 14
     hd : 7 -> 7
     c : 13 -> 12
     lt : 5 -> 0
     tl : 7 -> 7
     lem1 : 11 -> 1
     + : 14 x 14 -> 14
   -----
   0:*(x,*(y,z)) -> *(*(x,y),z)
     *(*(x,y),z) -> *(x,*(y,z))
     rep(0(),x) -> nil()
     rep(s(x),y) -> *(x,rep(x,y))
     hd(*(c(x),y)) -> x
     lt(*(x,c(y))) -> y
     tl(*(c(x),y)) -> y
     +(x,y) -> +(y,x)
     +(+(x,y),z) -> +(x,+(y,z))
     +(0(),x) -> x
     +(s(x),y) -> s(+(x,y))
     sorted: (order)
     0:*(x,*(y,z)) -> *(*(x,y),z)
       *(*(x,y),z) -> *(x,*(y,z))
       rep(0(),x) -> nil()
       rep(s(x),y) -> *(x,rep(x,y))
       hd(*(c(x),y)) -> x
       +(x,y) -> +(y,x)
       +(+(x,y),z) -> +(x,+(y,z))
       +(0(),x) -> x
       +(s(x),y) -> s(+(x,y))
     1:*(x,*(y,z)) -> *(*(x,y),z)
       *(*(x,y),z) -> *(x,*(y,z))
       rep(0(),x) -> nil()
       rep(s(x),y) -> *(x,rep(x,y))
       lt(*(x,c(y))) -> y
       +(x,y) -> +(y,x)
       +(+(x,y),z) -> +(x,+(y,z))
       +(0(),x) -> x
       +(s(x),y) -> s(+(x,y))
     2:*(x,*(y,z)) -> *(*(x,y),z)
       *(*(x,y),z) -> *(x,*(y,z))
       rep(0(),x) -> nil()
       rep(s(x),y) -> *(x,rep(x,y))
       tl(*(c(x),y)) -> y
       +(x,y) -> +(y,x)
       +(+(x,y),z) -> +(x,+(y,z))
       +(0(),x) -> x
       +(s(x),y) -> s(+(x,y))
     -----
     sorts
       [0>3, 1>4, 2>5, 3>6, 4>6, 5>6, 6>7, 6>8, 6>9, 6>10, 9>12, 10>11, 12>13]
     sort attachment (non-strict)
       * : 6 x 6 -> 6
       rep : 9 x 8 -> 6
       0 : 13
       nil : 7
       s : 12 -> 12
       hd : 3 -> 0
       c : 11 -> 10
       lt : 4 -> 1
       tl : 5 -> 2
       + : 12 x 12 -> 12
     -----
     0:*(x,*(y,z)) -> *(*(x,y),z)
       *(*(x,y),z) -> *(x,*(y,z))
       rep(0(),x) -> nil()
       rep(s(x),y) -> *(x,rep(x,y))
       hd(*(c(x),y)) -> x
       +(x,y) -> +(y,x)
       +(+(x,y),z) -> +(x,+(y,z))
       +(0(),x) -> x
       +(s(x),y) -> s(+(x,y))
       Open
     
     
     1:*(x,*(y,z)) -> *(*(x,y),z)
       *(*(x,y),z) -> *(x,*(y,z))
       rep(0(),x) -> nil()
       rep(s(x),y) -> *(x,rep(x,y))
       lt(*(x,c(y))) -> y
       +(x,y) -> +(y,x)
       +(+(x,y),z) -> +(x,+(y,z))
       +(0(),x) -> x
       +(s(x),y) -> s(+(x,y))
       Open
     
     
     2:*(x,*(y,z)) -> *(*(x,y),z)
       *(*(x,y),z) -> *(x,*(y,z))
       rep(0(),x) -> nil()
       rep(s(x),y) -> *(x,rep(x,y))
       tl(*(c(x),y)) -> y
       +(x,y) -> +(y,x)
       +(+(x,y),z) -> +(x,+(y,z))
       +(0(),x) -> x
       +(s(x),y) -> s(+(x,y))
       Open
     
   
   
   1:*(x,*(y,z)) -> *(*(x,y),z)
     *(*(x,y),z) -> *(x,*(y,z))
     eq(x,y) -> eq(y,x)
     eq(a(),a()) -> T()
     eq(a(),*(x,y)) -> F()
     eq(*(a(),x),*(a(),y)) -> eq(x,y)
     rep(0(),x) -> nil()
     rep(s(x),y) -> *(x,rep(x,y))
     hd(*(c(x),y)) -> x
     tl(*(c(x),y)) -> y
     lem1(x) -> eq(*(hd(x),tl(x)),x)
     +(x,y) -> +(y,x)
     +(+(x,y),z) -> +(x,+(y,z))
     +(0(),x) -> x
     +(s(x),y) -> s(+(x,y))
     Open
   
 
 
 1:*(x,*(y,z)) -> *(*(x,y),z)
   *(*(x,y),z) -> *(x,*(y,z))
   eq(x,y) -> eq(y,x)
   eq(a(),a()) -> T()
   eq(a(),*(x,y)) -> F()
   eq(*(a(),x),*(a(),y)) -> eq(x,y)
   rep(0(),x) -> nil()
   rep(s(x),y) -> *(x,rep(x,y))
   hd(*(c(x),y)) -> x
   lt(*(x,c(y))) -> y
   tl(*(c(x),y)) -> y
   lem2(*(x,y)) -> eq(lt(*(x,y)),lt(tl(*(x,y))))
   +(x,y) -> +(y,x)
   +(+(x,y),z) -> +(x,+(y,z))
   +(0(),x) -> x
   +(s(x),y) -> s(+(x,y))
   sorted: (order)
   0:*(x,*(y,z)) -> *(*(x,y),z)
     *(*(x,y),z) -> *(x,*(y,z))
     rep(0(),x) -> nil()
     rep(s(x),y) -> *(x,rep(x,y))
     hd(*(c(x),y)) -> x
     +(x,y) -> +(y,x)
     +(+(x,y),z) -> +(x,+(y,z))
     +(0(),x) -> x
     +(s(x),y) -> s(+(x,y))
   1:*(x,*(y,z)) -> *(*(x,y),z)
     *(*(x,y),z) -> *(x,*(y,z))
     eq(x,y) -> eq(y,x)
     eq(a(),a()) -> T()
     eq(a(),*(x,y)) -> F()
     eq(*(a(),x),*(a(),y)) -> eq(x,y)
     rep(0(),x) -> nil()
     rep(s(x),y) -> *(x,rep(x,y))
     lt(*(x,c(y))) -> y
     tl(*(c(x),y)) -> y
     lem2(*(x,y)) -> eq(lt(*(x,y)),lt(tl(*(x,y))))
     +(x,y) -> +(y,x)
     +(+(x,y),z) -> +(x,+(y,z))
     +(0(),x) -> x
     +(s(x),y) -> s(+(x,y))
   -----
   sorts
     [0>5, 1>2, 1>6, 2>3, 2>4, 2>7, 5>12, 6>12, 7>8, 8>9, 9>10, 10>11, 11>12, 12>13, 12>14, 12>15,
      12>16, 12>20, 15>18, 16>17, 18>19]
   sort attachment (non-strict)
     * : 12 x 12 -> 12
     eq : 7 x 7 -> 2
     a : 20
     T : 4
     F : 3
     rep : 15 x 14 -> 12
     0 : 19
     nil : 13
     s : 18 -> 18
     hd : 5 -> 0
     c : 17 -> 16
     lt : 9 -> 8
     tl : 11 -> 10
     lem2 : 6 -> 1
     + : 18 x 18 -> 18
   -----
   0:*(x,*(y,z)) -> *(*(x,y),z)
     *(*(x,y),z) -> *(x,*(y,z))
     rep(0(),x) -> nil()
     rep(s(x),y) -> *(x,rep(x,y))
     hd(*(c(x),y)) -> x
     +(x,y) -> +(y,x)
     +(+(x,y),z) -> +(x,+(y,z))
     +(0(),x) -> x
     +(s(x),y) -> s(+(x,y))
     Open
   
   
   1:*(x,*(y,z)) -> *(*(x,y),z)
     *(*(x,y),z) -> *(x,*(y,z))
     eq(x,y) -> eq(y,x)
     eq(a(),a()) -> T()
     eq(a(),*(x,y)) -> F()
     eq(*(a(),x),*(a(),y)) -> eq(x,y)
     rep(0(),x) -> nil()
     rep(s(x),y) -> *(x,rep(x,y))
     lt(*(x,c(y))) -> y
     tl(*(c(x),y)) -> y
     lem2(*(x,y)) -> eq(lt(*(x,y)),lt(tl(*(x,y))))
     +(x,y) -> +(y,x)
     +(+(x,y),z) -> +(x,+(y,z))
     +(0(),x) -> x
     +(s(x),y) -> s(+(x,y))
     Open