YES(?,O(n^1)) 0.15/0.29 YES(?,O(n^1)) 0.57/0.30 0.57/0.30 Problem: 0.57/0.30 f(a(),a()) -> f(a(),b()) 0.57/0.30 f(a(),b()) -> f(s(a()),c()) 0.57/0.30 f(s(X),c()) -> f(X,c()) 0.57/0.30 f(c(),c()) -> f(a(),a()) 0.57/0.30 0.57/0.30 Proof: 0.57/0.30 Bounds Processor: 0.57/0.30 bound: 4 0.57/0.30 enrichment: match 0.57/0.30 automaton: 0.57/0.30 final states: {5} 0.57/0.30 transitions: 0.57/0.30 c3() -> 18* 0.57/0.30 s3(19) -> 20* 0.57/0.30 a3() -> 19* 0.57/0.30 f4(19,24) -> 5* 0.57/0.30 c4() -> 24* 0.57/0.30 f0(3,1) -> 5* 0.57/0.30 f0(3,3) -> 5* 0.57/0.30 f0(4,2) -> 5* 0.57/0.30 f0(4,4) -> 5* 0.57/0.30 f0(1,2) -> 5* 0.57/0.30 f0(1,4) -> 5* 0.57/0.30 f0(2,1) -> 5* 0.57/0.30 f0(2,3) -> 5* 0.57/0.30 f0(3,2) -> 5* 0.57/0.30 f0(3,4) -> 5* 0.57/0.30 f0(4,1) -> 5* 0.57/0.30 f0(4,3) -> 5* 0.57/0.30 f0(1,1) -> 5* 0.57/0.30 f0(1,3) -> 5* 0.57/0.30 f0(2,2) -> 5* 0.57/0.30 f0(2,4) -> 5* 0.57/0.30 a0() -> 1* 0.57/0.30 b0() -> 2* 0.57/0.30 s0(2) -> 3* 0.57/0.30 s0(4) -> 3* 0.57/0.30 s0(1) -> 3* 0.57/0.30 s0(3) -> 3* 0.57/0.30 c0() -> 4* 0.57/0.30 f1(4,10) -> 5* 0.57/0.30 f1(11,10) -> 5* 0.57/0.30 f1(1,10) -> 5* 0.57/0.30 f1(7,7) -> 5* 0.57/0.30 f1(3,10) -> 5* 0.57/0.30 f1(7,6) -> 5* 0.57/0.30 f1(2,10) -> 5* 0.57/0.30 a1() -> 7* 0.57/0.30 c1() -> 10* 0.57/0.30 s1(7) -> 11* 0.57/0.30 b1() -> 6* 0.57/0.30 f2(17,16) -> 5* 0.57/0.30 f2(7,16) -> 5* 0.57/0.30 f2(15,14) -> 5* 0.57/0.30 c2() -> 16* 0.57/0.30 s2(15) -> 17* 0.57/0.30 a2() -> 15* 0.57/0.30 b2() -> 14* 0.57/0.30 f3(20,18) -> 5* 0.57/0.30 f3(15,18) -> 5* 0.57/0.30 problem: 0.57/0.30 0.57/0.30 Qed 0.57/0.30 EOF