Problem: if(true(),a(),x) -> a() if(true(),b(),x) -> b() if(true(),g(a()),x) -> g(a()) if(true(),g(b()),x) -> g(b()) if(false(),x,a()) -> a() if(false(),x,b()) -> b() if(false(),x,g(a())) -> g(a()) if(false(),x,g(b())) -> g(b()) g(a()) -> g(g(a())) g(b()) -> a() f(a(),b()) -> b() f(g(g(a())),x) -> b() Proof: sorted: (order-sorted) 0:if(true(),a(),x) -> a() if(true(),b(),x) -> b() if(true(),g(a()),x) -> g(a()) if(true(),g(b()),x) -> g(b()) if(false(),x,a()) -> a() if(false(),x,b()) -> b() if(false(),x,g(a())) -> g(a()) if(false(),x,g(b())) -> g(b()) g(a()) -> g(g(a())) g(b()) -> a() 1:g(a()) -> g(g(a())) g(b()) -> a() f(a(),b()) -> b() f(g(g(a())),x) -> b() ----- sorts [0>2, 0>7, 0>8, 1>5, 1>6, 2>3, 2>4, 5>9, 6>10, 7>9, 8>9, 9>10, 9>11] sort attachment (non-strict) if : 2 x 7 x 8 -> 0 true : 4 a : 11 b : 10 g : 9 -> 9 false : 3 f : 5 x 6 -> 1 ----- 0:if(true(),a(),x) -> a() if(true(),b(),x) -> b() if(true(),g(a()),x) -> g(a()) if(true(),g(b()),x) -> g(b()) if(false(),x,a()) -> a() if(false(),x,b()) -> b() if(false(),x,g(a())) -> g(a()) if(false(),x,g(b())) -> g(b()) g(a()) -> g(g(a())) g(b()) -> a() Nonconfluence Processor: terms: if(true(),g(g(a())),f7()) *<- if(true(),g(a()),f7()) ->* g(a()) Qed first automaton: final states: {19} transitions: true() -> 24* a() -> 21* g(21) -> 22* g(22) -> 22,23 if(24,23,20) -> 19* f7() -> 20* second automaton: final states: {17} transitions: a() -> 18* g(18) -> 17* g(17) -> 17* 1:g(a()) -> g(g(a())) g(b()) -> a() f(a(),b()) -> b() f(g(g(a())),x) -> b() Open