MAYBE Problem: top1(free(x),y) -> top2(check(new(x)),y) top1(free(x),y) -> top2(new(x),check(y)) top1(free(x),y) -> top2(check(x),new(y)) top1(free(x),y) -> top2(x,check(new(y))) top2(x,free(y)) -> top1(check(new(x)),y) top2(x,free(y)) -> top1(new(x),check(y)) top2(x,free(y)) -> top1(check(x),new(y)) top2(x,free(y)) -> top1(x,check(new(y))) new(free(x)) -> free(new(x)) old(free(x)) -> free(old(x)) new(serve()) -> free(serve()) old(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) Proof: DP Processor: DPs: top1#(free(x),y) -> new#(x) top1#(free(x),y) -> check#(new(x)) top1#(free(x),y) -> top2#(check(new(x)),y) top1#(free(x),y) -> check#(y) top1#(free(x),y) -> top2#(new(x),check(y)) top1#(free(x),y) -> new#(y) top1#(free(x),y) -> check#(x) top1#(free(x),y) -> top2#(check(x),new(y)) top1#(free(x),y) -> check#(new(y)) top1#(free(x),y) -> top2#(x,check(new(y))) top2#(x,free(y)) -> new#(x) top2#(x,free(y)) -> check#(new(x)) top2#(x,free(y)) -> top1#(check(new(x)),y) top2#(x,free(y)) -> check#(y) top2#(x,free(y)) -> top1#(new(x),check(y)) top2#(x,free(y)) -> new#(y) top2#(x,free(y)) -> check#(x) top2#(x,free(y)) -> top1#(check(x),new(y)) top2#(x,free(y)) -> check#(new(y)) top2#(x,free(y)) -> top1#(x,check(new(y))) new#(free(x)) -> new#(x) old#(free(x)) -> old#(x) check#(free(x)) -> check#(x) check#(new(x)) -> check#(x) check#(new(x)) -> new#(check(x)) check#(old(x)) -> check#(x) check#(old(x)) -> old#(check(x)) TRS: top1(free(x),y) -> top2(check(new(x)),y) top1(free(x),y) -> top2(new(x),check(y)) top1(free(x),y) -> top2(check(x),new(y)) top1(free(x),y) -> top2(x,check(new(y))) top2(x,free(y)) -> top1(check(new(x)),y) top2(x,free(y)) -> top1(new(x),check(y)) top2(x,free(y)) -> top1(check(x),new(y)) top2(x,free(y)) -> top1(x,check(new(y))) new(free(x)) -> free(new(x)) old(free(x)) -> free(old(x)) new(serve()) -> free(serve()) old(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) Usable Rule Processor: DPs: top1#(free(x),y) -> new#(x) top1#(free(x),y) -> check#(new(x)) top1#(free(x),y) -> top2#(check(new(x)),y) top1#(free(x),y) -> check#(y) top1#(free(x),y) -> top2#(new(x),check(y)) top1#(free(x),y) -> new#(y) top1#(free(x),y) -> check#(x) top1#(free(x),y) -> top2#(check(x),new(y)) top1#(free(x),y) -> check#(new(y)) top1#(free(x),y) -> top2#(x,check(new(y))) top2#(x,free(y)) -> new#(x) top2#(x,free(y)) -> check#(new(x)) top2#(x,free(y)) -> top1#(check(new(x)),y) top2#(x,free(y)) -> check#(y) top2#(x,free(y)) -> top1#(new(x),check(y)) top2#(x,free(y)) -> new#(y) top2#(x,free(y)) -> check#(x) top2#(x,free(y)) -> top1#(check(x),new(y)) top2#(x,free(y)) -> check#(new(y)) top2#(x,free(y)) -> top1#(x,check(new(y))) new#(free(x)) -> new#(x) old#(free(x)) -> old#(x) check#(free(x)) -> check#(x) check#(new(x)) -> check#(x) check#(new(x)) -> new#(check(x)) check#(old(x)) -> check#(x) check#(old(x)) -> old#(check(x)) TRS: new(free(x)) -> free(new(x)) new(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) old(free(x)) -> free(old(x)) old(serve()) -> free(serve()) CDG Processor: DPs: top1#(free(x),y) -> new#(x) top1#(free(x),y) -> check#(new(x)) top1#(free(x),y) -> top2#(check(new(x)),y) top1#(free(x),y) -> check#(y) top1#(free(x),y) -> top2#(new(x),check(y)) top1#(free(x),y) -> new#(y) top1#(free(x),y) -> check#(x) top1#(free(x),y) -> top2#(check(x),new(y)) top1#(free(x),y) -> check#(new(y)) top1#(free(x),y) -> top2#(x,check(new(y))) top2#(x,free(y)) -> new#(x) top2#(x,free(y)) -> check#(new(x)) top2#(x,free(y)) -> top1#(check(new(x)),y) top2#(x,free(y)) -> check#(y) top2#(x,free(y)) -> top1#(new(x),check(y)) top2#(x,free(y)) -> new#(y) top2#(x,free(y)) -> check#(x) top2#(x,free(y)) -> top1#(check(x),new(y)) top2#(x,free(y)) -> check#(new(y)) top2#(x,free(y)) -> top1#(x,check(new(y))) new#(free(x)) -> new#(x) old#(free(x)) -> old#(x) check#(free(x)) -> check#(x) check#(new(x)) -> check#(x) check#(new(x)) -> new#(check(x)) check#(old(x)) -> check#(x) check#(old(x)) -> old#(check(x)) TRS: new(free(x)) -> free(new(x)) new(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) old(free(x)) -> free(old(x)) old(serve()) -> free(serve()) graph: old#(free(x)) -> old#(x) -> old#(free(x)) -> old#(x) top2#(x,free(y)) -> check#(new(y)) -> check#(free(x)) -> check#(x) top2#(x,free(y)) -> check#(new(y)) -> check#(new(x)) -> check#(x) top2#(x,free(y)) -> check#(new(y)) -> check#(new(x)) -> new#(check(x)) top2#(x,free(y)) -> check#(new(x)) -> check#(free(x)) -> check#(x) top2#(x,free(y)) -> check#(new(x)) -> check#(new(x)) -> check#(x) top2#(x,free(y)) -> check#(new(x)) -> check#(new(x)) -> new#(check(x)) top2#(x,free(y)) -> check#(y) -> check#(free(x)) -> check#(x) top2#(x,free(y)) -> check#(y) -> check#(new(x)) -> check#(x) top2#(x,free(y)) -> check#(y) -> check#(new(x)) -> new#(check(x)) top2#(x,free(y)) -> check#(y) -> check#(old(x)) -> check#(x) top2#(x,free(y)) -> check#(y) -> check#(old(x)) -> old#(check(x)) top2#(x,free(y)) -> check#(x) -> check#(free(x)) -> check#(x) top2#(x,free(y)) -> check#(x) -> check#(new(x)) -> check#(x) top2#(x,free(y)) -> check#(x) -> check#(new(x)) -> new#(check(x)) top2#(x,free(y)) -> check#(x) -> check#(old(x)) -> check#(x) top2#(x,free(y)) -> check#(x) -> check#(old(x)) -> old#(check(x)) top2#(x,free(y)) -> new#(y) -> new#(free(x)) -> new#(x) top2#(x,free(y)) -> new#(x) -> new#(free(x)) -> new#(x) top2#(x,free(y)) -> top1#(check(new(x)),y) -> top1#(free(x),y) -> new#(x) top2#(x,free(y)) -> top1#(check(new(x)),y) -> top1#(free(x),y) -> check#(new(x)) top2#(x,free(y)) -> top1#(check(new(x)),y) -> top1#(free(x),y) -> top2#(check(new(x)),y) top2#(x,free(y)) -> top1#(check(new(x)),y) -> top1#(free(x),y) -> check#(y) top2#(x,free(y)) -> top1#(check(new(x)),y) -> top1#(free(x),y) -> top2#(new(x),check(y)) top2#(x,free(y)) -> top1#(check(new(x)),y) -> top1#(free(x),y) -> new#(y) top2#(x,free(y)) -> top1#(check(new(x)),y) -> top1#(free(x),y) -> check#(x) top2#(x,free(y)) -> top1#(check(new(x)),y) -> top1#(free(x),y) -> top2#(check(x),new(y)) top2#(x,free(y)) -> top1#(check(new(x)),y) -> top1#(free(x),y) -> check#(new(y)) top2#(x,free(y)) -> top1#(check(new(x)),y) -> top1#(free(x),y) -> top2#(x,check(new(y))) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> new#(x) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> check#(new(x)) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> top2#(check(new(x)),y) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> check#(y) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> top2#(new(x),check(y)) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> new#(y) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> check#(x) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> top2#(check(x),new(y)) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> check#(new(y)) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> top2#(x,check(new(y))) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> new#(x) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> check#(new(x)) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> top2#(check(new(x)),y) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> check#(y) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> top2#(new(x),check(y)) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> new#(y) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> check#(x) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> top2#(check(x),new(y)) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> check#(new(y)) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> top2#(x,check(new(y))) top2#(x,free(y)) -> top1#(x,check(new(y))) -> top1#(free(x),y) -> new#(x) top2#(x,free(y)) -> top1#(x,check(new(y))) -> top1#(free(x),y) -> check#(new(x)) top2#(x,free(y)) -> top1#(x,check(new(y))) -> top1#(free(x),y) -> top2#(check(new(x)),y) top2#(x,free(y)) -> top1#(x,check(new(y))) -> top1#(free(x),y) -> check#(y) top2#(x,free(y)) -> top1#(x,check(new(y))) -> top1#(free(x),y) -> top2#(new(x),check(y)) top2#(x,free(y)) -> top1#(x,check(new(y))) -> top1#(free(x),y) -> new#(y) top2#(x,free(y)) -> top1#(x,check(new(y))) -> top1#(free(x),y) -> check#(x) top2#(x,free(y)) -> top1#(x,check(new(y))) -> top1#(free(x),y) -> top2#(check(x),new(y)) top2#(x,free(y)) -> top1#(x,check(new(y))) -> top1#(free(x),y) -> check#(new(y)) top2#(x,free(y)) -> top1#(x,check(new(y))) -> top1#(free(x),y) -> top2#(x,check(new(y))) check#(old(x)) -> old#(check(x)) -> old#(free(x)) -> old#(x) check#(old(x)) -> check#(x) -> check#(free(x)) -> check#(x) check#(old(x)) -> check#(x) -> check#(new(x)) -> check#(x) check#(old(x)) -> check#(x) -> check#(new(x)) -> new#(check(x)) check#(old(x)) -> check#(x) -> check#(old(x)) -> check#(x) check#(old(x)) -> check#(x) -> check#(old(x)) -> old#(check(x)) check#(new(x)) -> check#(x) -> check#(free(x)) -> check#(x) check#(new(x)) -> check#(x) -> check#(new(x)) -> check#(x) check#(new(x)) -> check#(x) -> check#(new(x)) -> new#(check(x)) check#(new(x)) -> check#(x) -> check#(old(x)) -> check#(x) check#(new(x)) -> check#(x) -> check#(old(x)) -> old#(check(x)) check#(new(x)) -> new#(check(x)) -> new#(free(x)) -> new#(x) check#(free(x)) -> check#(x) -> check#(free(x)) -> check#(x) check#(free(x)) -> check#(x) -> check#(new(x)) -> check#(x) check#(free(x)) -> check#(x) -> check#(new(x)) -> new#(check(x)) check#(free(x)) -> check#(x) -> check#(old(x)) -> check#(x) check#(free(x)) -> check#(x) -> check#(old(x)) -> old#(check(x)) new#(free(x)) -> new#(x) -> new#(free(x)) -> new#(x) top1#(free(x),y) -> top2#(check(new(x)),y) -> top2#(x,free(y)) -> new#(x) top1#(free(x),y) -> top2#(check(new(x)),y) -> top2#(x,free(y)) -> check#(new(x)) top1#(free(x),y) -> top2#(check(new(x)),y) -> top2#(x,free(y)) -> top1#(check(new(x)),y) top1#(free(x),y) -> top2#(check(new(x)),y) -> top2#(x,free(y)) -> check#(y) top1#(free(x),y) -> top2#(check(new(x)),y) -> top2#(x,free(y)) -> top1#(new(x),check(y)) top1#(free(x),y) -> top2#(check(new(x)),y) -> top2#(x,free(y)) -> new#(y) top1#(free(x),y) -> top2#(check(new(x)),y) -> top2#(x,free(y)) -> check#(x) top1#(free(x),y) -> top2#(check(new(x)),y) -> top2#(x,free(y)) -> top1#(check(x),new(y)) top1#(free(x),y) -> top2#(check(new(x)),y) -> top2#(x,free(y)) -> check#(new(y)) top1#(free(x),y) -> top2#(check(new(x)),y) -> top2#(x,free(y)) -> top1#(x,check(new(y))) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> new#(x) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> check#(new(x)) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> top1#(check(new(x)),y) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> check#(y) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> top1#(new(x),check(y)) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> new#(y) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> check#(x) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> top1#(check(x),new(y)) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> check#(new(y)) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> top1#(x,check(new(y))) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> new#(x) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> check#(new(x)) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> top1#(check(new(x)),y) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> check#(y) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> top1#(new(x),check(y)) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> new#(y) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> check#(x) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> top1#(check(x),new(y)) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> check#(new(y)) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> top1#(x,check(new(y))) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> new#(x) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> check#(new(x)) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> top1#(check(new(x)),y) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> check#(y) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> top1#(new(x),check(y)) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> new#(y) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> check#(x) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> top1#(check(x),new(y)) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> check#(new(y)) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> top1#(x,check(new(y))) top1#(free(x),y) -> check#(new(y)) -> check#(free(x)) -> check#(x) top1#(free(x),y) -> check#(new(y)) -> check#(new(x)) -> check#(x) top1#(free(x),y) -> check#(new(y)) -> check#(new(x)) -> new#(check(x)) top1#(free(x),y) -> check#(new(x)) -> check#(free(x)) -> check#(x) top1#(free(x),y) -> check#(new(x)) -> check#(new(x)) -> check#(x) top1#(free(x),y) -> check#(new(x)) -> check#(new(x)) -> new#(check(x)) top1#(free(x),y) -> check#(y) -> check#(free(x)) -> check#(x) top1#(free(x),y) -> check#(y) -> check#(new(x)) -> check#(x) top1#(free(x),y) -> check#(y) -> check#(new(x)) -> new#(check(x)) top1#(free(x),y) -> check#(y) -> check#(old(x)) -> check#(x) top1#(free(x),y) -> check#(y) -> check#(old(x)) -> old#(check(x)) top1#(free(x),y) -> check#(x) -> check#(free(x)) -> check#(x) top1#(free(x),y) -> check#(x) -> check#(new(x)) -> check#(x) top1#(free(x),y) -> check#(x) -> check#(new(x)) -> new#(check(x)) top1#(free(x),y) -> check#(x) -> check#(old(x)) -> check#(x) top1#(free(x),y) -> check#(x) -> check#(old(x)) -> old#(check(x)) top1#(free(x),y) -> new#(y) -> new#(free(x)) -> new#(x) top1#(free(x),y) -> new#(x) -> new#(free(x)) -> new#(x) Restore Modifier: DPs: top1#(free(x),y) -> new#(x) top1#(free(x),y) -> check#(new(x)) top1#(free(x),y) -> top2#(check(new(x)),y) top1#(free(x),y) -> check#(y) top1#(free(x),y) -> top2#(new(x),check(y)) top1#(free(x),y) -> new#(y) top1#(free(x),y) -> check#(x) top1#(free(x),y) -> top2#(check(x),new(y)) top1#(free(x),y) -> check#(new(y)) top1#(free(x),y) -> top2#(x,check(new(y))) top2#(x,free(y)) -> new#(x) top2#(x,free(y)) -> check#(new(x)) top2#(x,free(y)) -> top1#(check(new(x)),y) top2#(x,free(y)) -> check#(y) top2#(x,free(y)) -> top1#(new(x),check(y)) top2#(x,free(y)) -> new#(y) top2#(x,free(y)) -> check#(x) top2#(x,free(y)) -> top1#(check(x),new(y)) top2#(x,free(y)) -> check#(new(y)) top2#(x,free(y)) -> top1#(x,check(new(y))) new#(free(x)) -> new#(x) old#(free(x)) -> old#(x) check#(free(x)) -> check#(x) check#(new(x)) -> check#(x) check#(new(x)) -> new#(check(x)) check#(old(x)) -> check#(x) check#(old(x)) -> old#(check(x)) TRS: top1(free(x),y) -> top2(check(new(x)),y) top1(free(x),y) -> top2(new(x),check(y)) top1(free(x),y) -> top2(check(x),new(y)) top1(free(x),y) -> top2(x,check(new(y))) top2(x,free(y)) -> top1(check(new(x)),y) top2(x,free(y)) -> top1(new(x),check(y)) top2(x,free(y)) -> top1(check(x),new(y)) top2(x,free(y)) -> top1(x,check(new(y))) new(free(x)) -> free(new(x)) old(free(x)) -> free(old(x)) new(serve()) -> free(serve()) old(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) SCC Processor: #sccs: 4 #rules: 13 #arcs: 135/729 DPs: top2#(x,free(y)) -> top1#(check(new(x)),y) top1#(free(x),y) -> top2#(x,check(new(y))) top2#(x,free(y)) -> top1#(x,check(new(y))) top1#(free(x),y) -> top2#(check(x),new(y)) top2#(x,free(y)) -> top1#(check(x),new(y)) top1#(free(x),y) -> top2#(new(x),check(y)) top2#(x,free(y)) -> top1#(new(x),check(y)) top1#(free(x),y) -> top2#(check(new(x)),y) TRS: top1(free(x),y) -> top2(check(new(x)),y) top1(free(x),y) -> top2(new(x),check(y)) top1(free(x),y) -> top2(check(x),new(y)) top1(free(x),y) -> top2(x,check(new(y))) top2(x,free(y)) -> top1(check(new(x)),y) top2(x,free(y)) -> top1(new(x),check(y)) top2(x,free(y)) -> top1(check(x),new(y)) top2(x,free(y)) -> top1(x,check(new(y))) new(free(x)) -> free(new(x)) old(free(x)) -> free(old(x)) new(serve()) -> free(serve()) old(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) Open DPs: check#(new(x)) -> check#(x) check#(old(x)) -> check#(x) check#(free(x)) -> check#(x) TRS: top1(free(x),y) -> top2(check(new(x)),y) top1(free(x),y) -> top2(new(x),check(y)) top1(free(x),y) -> top2(check(x),new(y)) top1(free(x),y) -> top2(x,check(new(y))) top2(x,free(y)) -> top1(check(new(x)),y) top2(x,free(y)) -> top1(new(x),check(y)) top2(x,free(y)) -> top1(check(x),new(y)) top2(x,free(y)) -> top1(x,check(new(y))) new(free(x)) -> free(new(x)) old(free(x)) -> free(old(x)) new(serve()) -> free(serve()) old(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) Matrix Interpretation Processor: dimension: 1 interpretation: [check#](x0) = x0 + 1, [serve] = 1, [old](x0) = x0 + 1, [top2](x0, x1) = 0, [check](x0) = x0, [new](x0) = x0 + 1, [top1](x0, x1) = 0, [free](x0) = x0 + 1 orientation: check#(new(x)) = x + 2 >= x + 1 = check#(x) check#(old(x)) = x + 2 >= x + 1 = check#(x) check#(free(x)) = x + 2 >= x + 1 = check#(x) top1(free(x),y) = 0 >= 0 = top2(check(new(x)),y) top1(free(x),y) = 0 >= 0 = top2(new(x),check(y)) top1(free(x),y) = 0 >= 0 = top2(check(x),new(y)) top1(free(x),y) = 0 >= 0 = top2(x,check(new(y))) top2(x,free(y)) = 0 >= 0 = top1(check(new(x)),y) top2(x,free(y)) = 0 >= 0 = top1(new(x),check(y)) top2(x,free(y)) = 0 >= 0 = top1(check(x),new(y)) top2(x,free(y)) = 0 >= 0 = top1(x,check(new(y))) new(free(x)) = x + 2 >= x + 2 = free(new(x)) old(free(x)) = x + 2 >= x + 2 = free(old(x)) new(serve()) = 2 >= 2 = free(serve()) old(serve()) = 2 >= 2 = free(serve()) check(free(x)) = x + 1 >= x + 1 = free(check(x)) check(new(x)) = x + 1 >= x + 1 = new(check(x)) check(old(x)) = x + 1 >= x + 1 = old(check(x)) check(old(x)) = x + 1 >= x + 1 = old(x) problem: DPs: TRS: top1(free(x),y) -> top2(check(new(x)),y) top1(free(x),y) -> top2(new(x),check(y)) top1(free(x),y) -> top2(check(x),new(y)) top1(free(x),y) -> top2(x,check(new(y))) top2(x,free(y)) -> top1(check(new(x)),y) top2(x,free(y)) -> top1(new(x),check(y)) top2(x,free(y)) -> top1(check(x),new(y)) top2(x,free(y)) -> top1(x,check(new(y))) new(free(x)) -> free(new(x)) old(free(x)) -> free(old(x)) new(serve()) -> free(serve()) old(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) Qed DPs: new#(free(x)) -> new#(x) TRS: top1(free(x),y) -> top2(check(new(x)),y) top1(free(x),y) -> top2(new(x),check(y)) top1(free(x),y) -> top2(check(x),new(y)) top1(free(x),y) -> top2(x,check(new(y))) top2(x,free(y)) -> top1(check(new(x)),y) top2(x,free(y)) -> top1(new(x),check(y)) top2(x,free(y)) -> top1(check(x),new(y)) top2(x,free(y)) -> top1(x,check(new(y))) new(free(x)) -> free(new(x)) old(free(x)) -> free(old(x)) new(serve()) -> free(serve()) old(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) Matrix Interpretation Processor: dimension: 1 interpretation: [new#](x0) = x0, [serve] = 0, [old](x0) = x0 + 1, [top2](x0, x1) = 0, [check](x0) = x0, [new](x0) = x0 + 1, [top1](x0, x1) = 0, [free](x0) = x0 + 1 orientation: new#(free(x)) = x + 1 >= x = new#(x) top1(free(x),y) = 0 >= 0 = top2(check(new(x)),y) top1(free(x),y) = 0 >= 0 = top2(new(x),check(y)) top1(free(x),y) = 0 >= 0 = top2(check(x),new(y)) top1(free(x),y) = 0 >= 0 = top2(x,check(new(y))) top2(x,free(y)) = 0 >= 0 = top1(check(new(x)),y) top2(x,free(y)) = 0 >= 0 = top1(new(x),check(y)) top2(x,free(y)) = 0 >= 0 = top1(check(x),new(y)) top2(x,free(y)) = 0 >= 0 = top1(x,check(new(y))) new(free(x)) = x + 2 >= x + 2 = free(new(x)) old(free(x)) = x + 2 >= x + 2 = free(old(x)) new(serve()) = 1 >= 1 = free(serve()) old(serve()) = 1 >= 1 = free(serve()) check(free(x)) = x + 1 >= x + 1 = free(check(x)) check(new(x)) = x + 1 >= x + 1 = new(check(x)) check(old(x)) = x + 1 >= x + 1 = old(check(x)) check(old(x)) = x + 1 >= x + 1 = old(x) problem: DPs: TRS: top1(free(x),y) -> top2(check(new(x)),y) top1(free(x),y) -> top2(new(x),check(y)) top1(free(x),y) -> top2(check(x),new(y)) top1(free(x),y) -> top2(x,check(new(y))) top2(x,free(y)) -> top1(check(new(x)),y) top2(x,free(y)) -> top1(new(x),check(y)) top2(x,free(y)) -> top1(check(x),new(y)) top2(x,free(y)) -> top1(x,check(new(y))) new(free(x)) -> free(new(x)) old(free(x)) -> free(old(x)) new(serve()) -> free(serve()) old(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) Qed DPs: old#(free(x)) -> old#(x) TRS: top1(free(x),y) -> top2(check(new(x)),y) top1(free(x),y) -> top2(new(x),check(y)) top1(free(x),y) -> top2(check(x),new(y)) top1(free(x),y) -> top2(x,check(new(y))) top2(x,free(y)) -> top1(check(new(x)),y) top2(x,free(y)) -> top1(new(x),check(y)) top2(x,free(y)) -> top1(check(x),new(y)) top2(x,free(y)) -> top1(x,check(new(y))) new(free(x)) -> free(new(x)) old(free(x)) -> free(old(x)) new(serve()) -> free(serve()) old(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) Matrix Interpretation Processor: dimension: 1 interpretation: [old#](x0) = x0, [serve] = 0, [old](x0) = x0 + 1, [top2](x0, x1) = 0, [check](x0) = x0, [new](x0) = x0 + 1, [top1](x0, x1) = 0, [free](x0) = x0 + 1 orientation: old#(free(x)) = x + 1 >= x = old#(x) top1(free(x),y) = 0 >= 0 = top2(check(new(x)),y) top1(free(x),y) = 0 >= 0 = top2(new(x),check(y)) top1(free(x),y) = 0 >= 0 = top2(check(x),new(y)) top1(free(x),y) = 0 >= 0 = top2(x,check(new(y))) top2(x,free(y)) = 0 >= 0 = top1(check(new(x)),y) top2(x,free(y)) = 0 >= 0 = top1(new(x),check(y)) top2(x,free(y)) = 0 >= 0 = top1(check(x),new(y)) top2(x,free(y)) = 0 >= 0 = top1(x,check(new(y))) new(free(x)) = x + 2 >= x + 2 = free(new(x)) old(free(x)) = x + 2 >= x + 2 = free(old(x)) new(serve()) = 1 >= 1 = free(serve()) old(serve()) = 1 >= 1 = free(serve()) check(free(x)) = x + 1 >= x + 1 = free(check(x)) check(new(x)) = x + 1 >= x + 1 = new(check(x)) check(old(x)) = x + 1 >= x + 1 = old(check(x)) check(old(x)) = x + 1 >= x + 1 = old(x) problem: DPs: TRS: top1(free(x),y) -> top2(check(new(x)),y) top1(free(x),y) -> top2(new(x),check(y)) top1(free(x),y) -> top2(check(x),new(y)) top1(free(x),y) -> top2(x,check(new(y))) top2(x,free(y)) -> top1(check(new(x)),y) top2(x,free(y)) -> top1(new(x),check(y)) top2(x,free(y)) -> top1(check(x),new(y)) top2(x,free(y)) -> top1(x,check(new(y))) new(free(x)) -> free(new(x)) old(free(x)) -> free(old(x)) new(serve()) -> free(serve()) old(serve()) -> free(serve()) check(free(x)) -> free(check(x)) check(new(x)) -> new(check(x)) check(old(x)) -> old(check(x)) check(old(x)) -> old(x) Qed