Problem:
 F(x,x) -> G(x)
 A() -> B()

Proof:
 sorted: (order)
 0:F(x,x) -> G(x)
 1:A() -> B()
 -----
 sorts
   [0>1, 1>4, 2>3, 4>5]
 sort attachment (non-strict)
   F : 5 x 5 -> 0
   G : 4 -> 1
   A : 2
   B : 3
 -----
 0:F(x,x) -> G(x)
   Qed (SakaiOyamaguchiOgawa14)
 
 
 1:A() -> B()
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed