Problem:
 Ap(Ap(Ap(S(),x),y),z) -> Ap(Ap(x,z),Ap(y,z))
 Ap(Ap(K(),x),y) -> x
 Ap(I(),x) -> x
 Dh(z,z) -> z

Proof:
 sorted: (order)
 0:Dh(z,z) -> z
 1:Ap(Ap(Ap(S(),x),y),z) -> Ap(Ap(x,z),Ap(y,z))
   Ap(Ap(K(),x),y) -> x
   Ap(I(),x) -> x
 -----
 sorts
   [1>2, 1>3, 1>4]
 sort attachment (strict)
   Ap : 1 x 1 -> 1
   S : 4
   K : 3
   I : 2
   Dh : 0 x 0 -> 0
 -----
 0:Dh(z,z) -> z
   Church Rosser Transformation Processor (kb):
    Dh(z,z) -> z
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [Dh](x0, x1) = x0 + 2x1 + 2
     orientation:
      Dh(z,z) = 3z + 2 >= z = z
     problem:
      
     Qed
 
 
 1:Ap(Ap(Ap(S(),x),y),z) -> Ap(Ap(x,z),Ap(y,z))
   Ap(Ap(K(),x),y) -> x
   Ap(I(),x) -> x
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed