1.15/1.22 YES 1.15/1.22 1.15/1.22 Problem: 1.15/1.22 b() -> a() 1.15/1.22 b() -> c() 1.15/1.22 c() -> h(b()) 1.15/1.22 c() -> d() 1.15/1.22 a() -> h(a()) 1.15/1.22 d() -> h(d()) 1.15/1.22 1.15/1.22 Proof: 1.15/1.22 Uncurry Processor: 1.15/1.22 b() -> a() 1.15/1.22 b() -> c() 1.15/1.22 c() -> f5(h(),b()) 1.15/1.22 c() -> d() 1.15/1.22 a() -> f5(h(),a()) 1.15/1.22 d() -> f5(h(),d()) 1.15/1.22 Ground Confluence Processor: 1.15/1.22 UNC by decision procedure. 1.23/1.23 EOF