Problem:
 f(x) -> g(a())
 g(x) -> x
 h(x,x) -> 0()
 a() -> 1()

Proof:
 sorted: (order)
 0:f(x) -> g(a())
   g(x) -> x
   a() -> 1()
 1:h(x,x) -> 0()
 -----
 sorts
   [1>2, 1>9, 2>6, 3>4, 3>5, 6>7, 7>8]
 sort attachment (non-strict)
   f : 9 -> 1
   g : 6 -> 2
   a : 7
   h : 5 x 5 -> 3
   0 : 4
   1 : 8
 -----
 0:f(x) -> g(a())
   g(x) -> x
   a() -> 1()
   Church Rosser Transformation Processor:
    
    strict:
     f(x) -> g(a())
     g(x) -> x
     a() -> 1()
    weak:
     
    critical peaks: 0
    Closedness Processor (*parallel*):
     
     strict:
      
     weak:
      
     Qed
 
 
 1:h(x,x) -> 0()
   Church Rosser Transformation Processor (kb):
    h(x,x) -> 0()
    critical peaks: joinable
    Matrix Interpretation Processor: dim=3
     
     interpretation:
            [0]
      [0] = [0]
            [0],
      
                    [1 0 0]     [1 0 0]     [1]
      [h](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
                    [0 0 0]     [0 0 0]     [0]
     orientation:
               [2 0 0]    [1]    [0]      
      h(x,x) = [0 0 0]x + [0] >= [0] = 0()
               [0 0 0]    [0]    [0]      
     problem:
      
     Qed