Problem:
 F(D(x),y) -> F(D(x),G(G(y)))
 F(x,E(y)) -> F(G(x),E(y))
 G(x) -> x
 H(I(x)) -> K(J(x))
 J(x) -> K(J(x))
 I(x) -> I(J(x))
 J(x) -> J(K(J(x)))
 S(x,T(x)) -> T(x)

Proof:
 sorted: (order)
 0:F(D(x),y) -> F(D(x),G(G(y)))
   F(x,E(y)) -> F(G(x),E(y))
   G(x) -> x
 1:H(I(x)) -> K(J(x))
   J(x) -> K(J(x))
   I(x) -> I(J(x))
   J(x) -> J(K(J(x)))
 2:S(x,T(x)) -> T(x)
 -----
 sorts
   [0>9, 1>3, 2>5, 3>4, 4>8, 5>6, 6>7, 9>10, 9>12, 10>11, 12>13]
 sort attachment (non-strict)
   F : 9 x 9 -> 0
   D : 13 -> 12
   G : 9 -> 9
   E : 11 -> 10
   H : 3 -> 1
   I : 8 -> 4
   K : 8 -> 8
   J : 8 -> 8
   S : 7 x 5 -> 2
   T : 7 -> 6
 -----
 0:F(D(x),y) -> F(D(x),G(G(y)))
   F(x,E(y)) -> F(G(x),E(y))
   G(x) -> x
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    G(D(x31)) -> D(x31)
    F(D(x33),E(x32)) -> F(D(x33),G(G(E(x32))))
    critical peaks: joinable
    Matrix Interpretation Processor: dim=2
     
     interpretation:
                [1 1]     [0]
      [E](x0) = [0 0]x0 + [2],
      
                [1 0]  
      [G](x0) = [0 0]x0,
      
                    [2 0]     [2 1]     [0]
      [F](x0, x1) = [0 0]x0 + [0 0]x1 + [2],
      
                [2 0]  
      [D](x0) = [0 0]x0
     orientation:
                  [2 0]       [2 0]            
      G(D(x31)) = [0 0]x31 >= [0 0]x31 = D(x31)
      
                         [2 2]      [4 0]      [2]    [2 2]      [4 0]      [0]                         
      F(D(x33),E(x32)) = [0 0]x32 + [0 0]x33 + [2] >= [0 0]x32 + [0 0]x33 + [2] = F(D(x33),G(G(E(x32))))
     problem:
      G(D(x31)) -> D(x31)
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [G](x0) = x0 + 1,
       
       [D](x0) = x0 + 4
      orientation:
       G(D(x31)) = x31 + 5 >= x31 + 4 = D(x31)
      problem:
       
      Qed
 
 
 1:H(I(x)) -> K(J(x))
   J(x) -> K(J(x))
   I(x) -> I(J(x))
   J(x) -> J(K(J(x)))
   Church Rosser Transformation Processor:
    strict:
     
    weak:
     
    critical peaks: 3
     K(J(x)) <-1|[]- J(x) -3|[]-> J(K(J(x)))
     H(I(J(x))) <-2|0[]- H(I(x)) -0|[]-> K(J(x))
     J(K(J(x))) <-3|[]- J(x) -1|[]-> K(J(x))
    Shift Processor lab=left (dd) (force):
     strict:
      J(x) -> K(J(x))
      J(x) -> J(K(J(x)))
      K(J(x)) -> K(J(K(J(x))))
      J(K(J(x))) -> K(J(K(J(x))))
      H(I(x)) -> H(I(J(x)))
      H(I(x)) -> K(J(x))
      H(I(J(x))) -> K(J(J(x)))
      K(J(J(x))) -> K(J(K(J(x))))
      K(J(x)) -> K(J(K(J(x))))
      H(I(J(x))) -> H(I(K(J(x))))
      H(I(K(J(x)))) -> K(J(K(J(x))))
      K(J(x)) -> K(J(K(J(x))))
      J(x) -> J(K(J(x)))
      J(x) -> K(J(x))
      J(K(J(x))) -> K(J(K(J(x))))
      K(J(x)) -> K(J(K(J(x))))
     weak:
      H(I(x)) -> K(J(x))
      J(x) -> K(J(x))
      I(x) -> I(J(x))
      J(x) -> J(K(J(x)))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [K](x0) = x0,
       
       [J](x0) = x0,
       
       [H](x0) = x0 + 4,
       
       [I](x0) = 2x0 + 5
      orientation:
       J(x) = x >= x = K(J(x))
       
       J(x) = x >= x = J(K(J(x)))
       
       K(J(x)) = x >= x = K(J(K(J(x))))
       
       J(K(J(x))) = x >= x = K(J(K(J(x))))
       
       H(I(x)) = 2x + 9 >= 2x + 9 = H(I(J(x)))
       
       H(I(x)) = 2x + 9 >= x = K(J(x))
       
       H(I(J(x))) = 2x + 9 >= x = K(J(J(x)))
       
       K(J(J(x))) = x >= x = K(J(K(J(x))))
       
       K(J(x)) = x >= x = K(J(K(J(x))))
       
       H(I(J(x))) = 2x + 9 >= 2x + 9 = H(I(K(J(x))))
       
       H(I(K(J(x)))) = 2x + 9 >= x = K(J(K(J(x))))
       
       K(J(x)) = x >= x = K(J(K(J(x))))
       
       J(x) = x >= x = J(K(J(x)))
       
       J(x) = x >= x = K(J(x))
       
       J(K(J(x))) = x >= x = K(J(K(J(x))))
       
       K(J(x)) = x >= x = K(J(K(J(x))))
       
       I(x) = 2x + 5 >= 2x + 5 = I(J(x))
      problem:
       strict:
        J(x) -> K(J(x))
        J(x) -> J(K(J(x)))
        K(J(x)) -> K(J(K(J(x))))
        J(K(J(x))) -> K(J(K(J(x))))
        H(I(x)) -> H(I(J(x)))
        K(J(J(x))) -> K(J(K(J(x))))
        K(J(x)) -> K(J(K(J(x))))
        H(I(J(x))) -> H(I(K(J(x))))
        K(J(x)) -> K(J(K(J(x))))
        J(x) -> J(K(J(x)))
        J(x) -> K(J(x))
        J(K(J(x))) -> K(J(K(J(x))))
        K(J(x)) -> K(J(K(J(x))))
       weak:
        J(x) -> K(J(x))
        I(x) -> I(J(x))
        J(x) -> J(K(J(x)))
      Shift Processor (ldh) lab=left (force):
       strict:
        
       weak:
        
       Rule Labeling Processor:
        strict:
         
        weak:
         
        rule labeling (right):
         H(I(x)) -> K(J(x)): 0
         J(x) -> K(J(x)): 0
         I(x) -> I(J(x)): 0
         J(x) -> J(K(J(x))): 0
        Rule Labeling Processor:
         strict:
          
         weak:
          
         rule labeling (left):
          H(I(x)) -> K(J(x)): 0
          J(x) -> K(J(x)): 0
          I(x) -> I(J(x)): 1
          J(x) -> J(K(J(x))): 1
         Decreasing Processor:
          The following diagrams are decreasing:
          peak:
           K(J(x)) <-1|[=>0,==1,==0]- J(x) -3|[?=1,==1,==0]-> J(K(J(x)))
          joins (1):
           K(J(x)) -3|0[?=1,==1,==0]-> K(J(K(J(x))))
           J(K(J(x))) -1|[=>0,==1,==0]-> K(J(K(J(x))))
          peak:
           H(I(J(x))) <-2|0[=?1,==1,==0]- H(I(x)) -0|[>=0,==1,==0]-> K(J(x))
          joins (1):
           H(I(J(x))) -0|[>=0,==1,==0]-> K(J(J(x))) -1|0,0[>=0,>>0,==0]-> K(J(K(J(x))))
           K(J(x)) -3|0[=?1,>>0,==0]-> K(J(K(J(x))))
          peak:
           J(K(J(x))) <-3|[=?1,==1,==0]- J(x) -1|[>=0,==1,==0]-> K(J(x))
          joins (1):
           J(K(J(x))) -1|[>=0,==1,==0]-> K(J(K(J(x))))
           K(J(x)) -3|0[=?1,==1,==0]-> K(J(K(J(x))))
          Qed


2:S(x,T(x)) -> T(x)
  Qed (SakaiOyamaguchiOgawa14)