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
   [0>1, 0>8, 1>5, 2>3, 2>4, 5>6, 6>7]
 sort attachment (non-strict)
   f : 8 -> 0
   g : 5 -> 1
   a : 6
   h : 4 x 4 -> 2
   0 : 3
   1 : 7
 -----
 0:f(x) -> g(a())
   g(x) -> x
   a() -> 1()
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed
 
 
 1:h(x,x) -> 0()
   Qed (ToyamaOyamaguchi95Cor22)