MAYBE

Problem:
 from(x) -> :(x,from(s(x)))
 +(+(x,y),z) -> +(x,+(y,z))
 +(x,+(y,z)) -> +(+(x,y),z)
 +(0(),x) -> x
 +(x,0()) -> x
 f(c(x)) -> x
 f(+(c(x),y)) -> x
 *(0(),y) -> 0()
 *(s(x),y) -> +(y,*(x,y))

Proof:
 sorted: (order)
 0:+(+(x,y),z) -> +(x,+(y,z))
   +(x,+(y,z)) -> +(+(x,y),z)
   +(0(),x) -> x
   +(x,0()) -> x
   f(c(x)) -> x
   f(+(c(x),y)) -> x
   *(0(),y) -> 0()
   *(s(x),y) -> +(y,*(x,y))
 1:from(x) -> :(x,from(s(x)))
 -----
 sorts
   [0>3, 1>2, 2>6, 3>4, 4>5, 4>7, 4>8, 5>6, 5>10, 8>9]
 sort attachment (non-strict)
   from : 6 -> 1
   : : 2 x 1 -> 1
   s : 6 -> 6
   + : 4 x 4 -> 4
   0 : 10
   f : 3 -> 0
   c : 9 -> 8
   * : 5 x 7 -> 4
 -----
 0:+(+(x,y),z) -> +(x,+(y,z))
   +(x,+(y,z)) -> +(+(x,y),z)
   +(0(),x) -> x
   +(x,0()) -> x
   f(c(x)) -> x
   f(+(c(x),y)) -> x
   *(0(),y) -> 0()
   *(s(x),y) -> +(y,*(x,y))
   Open
 
 
 1:from(x) -> :(x,from(s(x)))
   Church Rosser Transformation Processor:
    strict:
     from(x) -> :(x,from(s(x)))
    weak:
     
    critical peaks: 0
    Closedness Processor (*parallel*):
     strict:
      
     weak:
      
     Qed