YES(?,O(n^1)) 0.16/0.36 YES(?,O(n^1)) 0.16/0.36 0.16/0.36 Problem: 0.16/0.36 norm(nil()) -> 0() 0.16/0.36 norm(g(x,y)) -> s(norm(x)) 0.16/0.36 f(x,nil()) -> g(nil(),x) 0.16/0.36 f(x,g(y,z)) -> g(f(x,y),z) 0.16/0.36 rem(nil(),y) -> nil() 0.16/0.36 rem(g(x,y),0()) -> g(x,y) 0.16/0.36 rem(g(x,y),s(z)) -> rem(x,z) 0.16/0.36 0.16/0.36 Proof: 0.16/0.36 Bounds Processor: 0.16/0.36 bound: 1 0.16/0.36 enrichment: match 0.16/0.36 automaton: 0.16/0.36 final states: {7,6,5} 0.16/0.36 transitions: 0.16/0.36 rem1(3,1) -> 7* 0.16/0.36 rem1(3,3) -> 7* 0.16/0.36 rem1(4,2) -> 7* 0.16/0.36 rem1(4,4) -> 7* 0.16/0.36 rem1(1,2) -> 7* 0.16/0.36 rem1(1,4) -> 7* 0.16/0.36 rem1(2,1) -> 7* 0.16/0.36 rem1(2,3) -> 7* 0.16/0.36 rem1(3,2) -> 7* 0.16/0.36 rem1(3,4) -> 7* 0.16/0.36 rem1(4,1) -> 7* 0.16/0.36 rem1(4,3) -> 7* 0.16/0.36 rem1(1,1) -> 7* 0.16/0.36 rem1(1,3) -> 7* 0.16/0.36 rem1(2,2) -> 7* 0.16/0.36 rem1(2,4) -> 7* 0.16/0.36 g1(3,1) -> 7* 0.16/0.36 g1(3,3) -> 7* 0.16/0.36 g1(4,2) -> 7* 0.16/0.36 g1(4,4) -> 7* 0.16/0.36 g1(10,1) -> 10,6 0.16/0.36 g1(10,3) -> 10,6 0.16/0.36 g1(1,2) -> 7* 0.16/0.36 g1(1,4) -> 7* 0.16/0.36 g1(7,1) -> 10* 0.16/0.36 g1(2,1) -> 7* 0.16/0.36 g1(7,3) -> 10* 0.16/0.36 g1(2,3) -> 7* 0.16/0.36 g1(3,2) -> 7* 0.16/0.36 g1(3,4) -> 7* 0.16/0.36 g1(4,1) -> 7* 0.16/0.36 g1(4,3) -> 7* 0.16/0.36 g1(10,2) -> 10,6 0.16/0.36 g1(10,4) -> 10,6 0.16/0.36 g1(1,1) -> 7* 0.16/0.36 g1(1,3) -> 7* 0.16/0.36 g1(7,2) -> 10* 0.16/0.36 g1(2,2) -> 7* 0.16/0.36 g1(7,4) -> 10* 0.16/0.36 g1(2,4) -> 7* 0.16/0.36 nil1() -> 7,10 0.16/0.36 f1(3,1) -> 10* 0.16/0.36 f1(3,3) -> 10* 0.16/0.36 f1(4,2) -> 10* 0.16/0.36 f1(4,4) -> 10* 0.16/0.36 f1(1,2) -> 10* 0.16/0.36 f1(1,4) -> 10* 0.16/0.36 f1(2,1) -> 10* 0.16/0.36 f1(2,3) -> 10* 0.16/0.36 f1(3,2) -> 10* 0.16/0.36 f1(3,4) -> 10* 0.16/0.36 f1(4,1) -> 10* 0.16/0.36 f1(4,3) -> 10* 0.16/0.36 f1(1,1) -> 10* 0.16/0.36 f1(1,3) -> 10* 0.16/0.36 f1(2,2) -> 10* 0.16/0.36 f1(2,4) -> 10* 0.16/0.36 s1(8) -> 8,5 0.16/0.36 norm1(2) -> 8* 0.16/0.36 norm1(4) -> 8* 0.16/0.36 norm1(1) -> 8* 0.16/0.36 norm1(3) -> 8* 0.16/0.36 01() -> 8,5 0.16/0.36 norm0(2) -> 5* 0.16/0.36 norm0(4) -> 5* 0.16/0.36 norm0(1) -> 5* 0.16/0.36 norm0(3) -> 5* 0.16/0.36 nil0() -> 1* 0.16/0.36 00() -> 2* 0.16/0.36 g0(3,1) -> 3* 0.16/0.36 g0(3,3) -> 3* 0.16/0.36 g0(4,2) -> 3* 0.16/0.36 g0(4,4) -> 3* 0.16/0.36 g0(1,2) -> 3* 0.16/0.36 g0(1,4) -> 3* 0.16/0.36 g0(2,1) -> 3* 0.16/0.36 g0(2,3) -> 3* 0.16/0.36 g0(3,2) -> 3* 0.16/0.36 g0(3,4) -> 3* 0.16/0.36 g0(4,1) -> 3* 0.16/0.36 g0(4,3) -> 3* 0.16/0.36 g0(1,1) -> 3* 0.16/0.36 g0(1,3) -> 3* 0.16/0.36 g0(2,2) -> 3* 0.16/0.36 g0(2,4) -> 3* 0.16/0.36 s0(2) -> 4* 0.16/0.36 s0(4) -> 4* 0.16/0.36 s0(1) -> 4* 0.16/0.36 s0(3) -> 4* 0.16/0.36 f0(3,1) -> 6* 0.16/0.36 f0(3,3) -> 6* 0.16/0.36 f0(4,2) -> 6* 0.16/0.36 f0(4,4) -> 6* 0.16/0.36 f0(1,2) -> 6* 0.16/0.36 f0(1,4) -> 6* 0.16/0.36 f0(2,1) -> 6* 0.16/0.36 f0(2,3) -> 6* 0.16/0.36 f0(3,2) -> 6* 0.16/0.36 f0(3,4) -> 6* 0.16/0.36 f0(4,1) -> 6* 0.16/0.36 f0(4,3) -> 6* 0.16/0.36 f0(1,1) -> 6* 0.16/0.36 f0(1,3) -> 6* 0.16/0.36 f0(2,2) -> 6* 0.16/0.36 f0(2,4) -> 6* 0.16/0.36 rem0(3,1) -> 7* 0.16/0.36 rem0(3,3) -> 7* 0.16/0.36 rem0(4,2) -> 7* 0.16/0.36 rem0(4,4) -> 7* 0.16/0.36 rem0(1,2) -> 7* 0.16/0.36 rem0(1,4) -> 7* 0.16/0.36 rem0(2,1) -> 7* 0.16/0.36 rem0(2,3) -> 7* 0.16/0.36 rem0(3,2) -> 7* 0.16/0.36 rem0(3,4) -> 7* 0.16/0.36 rem0(4,1) -> 7* 0.16/0.36 rem0(4,3) -> 7* 0.16/0.36 rem0(1,1) -> 7* 0.16/0.36 rem0(1,3) -> 7* 0.16/0.36 rem0(2,2) -> 7* 0.16/0.36 rem0(2,4) -> 7* 0.16/0.36 problem: 0.16/0.36 0.16/0.36 Qed 0.16/0.37 EOF