Problem:
 I(x) -> I(B(x))
 F(E(x),x) -> G(x)
 E(x) -> x

Proof:
 sorted: (order)
 0:I(x) -> I(B(x))
 1:F(E(x),x) -> G(x)
   E(x) -> x
 -----
 sorts
   [0>7, 1>2, 1>3, 2>5, 3>4, 4>6, 5>6]
 sort attachment (non-strict)
   I : 7 -> 0
   B : 7 -> 7
   F : 3 x 6 -> 1
   E : 6 -> 4
   G : 5 -> 2
 -----
 0:I(x) -> I(B(x))
   Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
    
    critical peaks: joinable
    Qed
 
 
 1:F(E(x),x) -> G(x)
   E(x) -> x
   Nonconfluence Processor:
    terms: F(x,x) *<- F(E(x),x) ->* G(x)
    Qed