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) TDG 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) graph: old#(free(x)) -> old#(x) -> old#(free(x)) -> old#(x) top2#(x,free(y)) -> check#(new(y)) -> check#(old(x)) -> old#(check(x)) top2#(x,free(y)) -> check#(new(y)) -> check#(old(x)) -> check#(x) top2#(x,free(y)) -> check#(new(y)) -> check#(new(x)) -> new#(check(x)) top2#(x,free(y)) -> check#(new(y)) -> check#(new(x)) -> check#(x) top2#(x,free(y)) -> check#(new(y)) -> check#(free(x)) -> check#(x) top2#(x,free(y)) -> check#(new(x)) -> check#(old(x)) -> old#(check(x)) top2#(x,free(y)) -> check#(new(x)) -> check#(old(x)) -> check#(x) top2#(x,free(y)) -> check#(new(x)) -> check#(new(x)) -> new#(check(x)) top2#(x,free(y)) -> check#(new(x)) -> check#(new(x)) -> check#(x) top2#(x,free(y)) -> check#(new(x)) -> check#(free(x)) -> check#(x) top2#(x,free(y)) -> check#(y) -> check#(old(x)) -> old#(check(x)) top2#(x,free(y)) -> check#(y) -> check#(old(x)) -> check#(x) top2#(x,free(y)) -> check#(y) -> check#(new(x)) -> new#(check(x)) top2#(x,free(y)) -> check#(y) -> check#(new(x)) -> check#(x) top2#(x,free(y)) -> check#(y) -> check#(free(x)) -> check#(x) top2#(x,free(y)) -> check#(x) -> check#(old(x)) -> old#(check(x)) top2#(x,free(y)) -> check#(x) -> check#(old(x)) -> check#(x) top2#(x,free(y)) -> check#(x) -> check#(new(x)) -> new#(check(x)) top2#(x,free(y)) -> check#(x) -> check#(new(x)) -> check#(x) top2#(x,free(y)) -> check#(x) -> check#(free(x)) -> 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) -> top2#(x,check(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#(check(x),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) -> new#(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) -> check#(y) 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#(new(x)) top2#(x,free(y)) -> top1#(check(new(x)),y) -> top1#(free(x),y) -> new#(x) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> top2#(x,check(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#(check(x),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) -> 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#(check(x),new(y)) -> top1#(free(x),y) -> check#(y) 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#(new(x)) top2#(x,free(y)) -> top1#(check(x),new(y)) -> top1#(free(x),y) -> new#(x) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> top2#(x,check(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#(check(x),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) -> new#(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) -> check#(y) 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#(new(x)) top2#(x,free(y)) -> top1#(new(x),check(y)) -> top1#(free(x),y) -> new#(x) top2#(x,free(y)) -> top1#(x,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)) 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#(x) 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) -> top2#(new(x),check(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#(check(new(x)),y) 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) -> new#(x) check#(old(x)) -> old#(check(x)) -> old#(free(x)) -> old#(x) check#(old(x)) -> check#(x) -> check#(old(x)) -> old#(check(x)) check#(old(x)) -> check#(x) -> check#(old(x)) -> check#(x) check#(old(x)) -> check#(x) -> check#(new(x)) -> new#(check(x)) check#(old(x)) -> check#(x) -> check#(new(x)) -> check#(x) check#(old(x)) -> check#(x) -> check#(free(x)) -> check#(x) check#(new(x)) -> check#(x) -> check#(old(x)) -> old#(check(x)) check#(new(x)) -> check#(x) -> check#(old(x)) -> check#(x) check#(new(x)) -> check#(x) -> check#(new(x)) -> new#(check(x)) check#(new(x)) -> check#(x) -> check#(new(x)) -> check#(x) check#(new(x)) -> check#(x) -> check#(free(x)) -> check#(x) check#(new(x)) -> new#(check(x)) -> new#(free(x)) -> new#(x) check#(free(x)) -> check#(x) -> check#(old(x)) -> old#(check(x)) check#(free(x)) -> check#(x) -> check#(old(x)) -> check#(x) check#(free(x)) -> check#(x) -> check#(new(x)) -> new#(check(x)) check#(free(x)) -> check#(x) -> check#(new(x)) -> check#(x) check#(free(x)) -> check#(x) -> check#(free(x)) -> 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)) -> top1#(x,check(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#(check(x),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)) -> new#(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)) -> check#(y) 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#(new(x)) top1#(free(x),y) -> top2#(check(new(x)),y) -> top2#(x,free(y)) -> new#(x) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> top1#(x,check(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#(check(x),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)) -> new#(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)) -> check#(y) 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#(new(x)) top1#(free(x),y) -> top2#(check(x),new(y)) -> top2#(x,free(y)) -> new#(x) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> top1#(x,check(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#(check(x),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)) -> 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#(new(x),check(y)) -> top2#(x,free(y)) -> check#(y) 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#(new(x)) top1#(free(x),y) -> top2#(new(x),check(y)) -> top2#(x,free(y)) -> new#(x) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> top1#(x,check(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#(check(x),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)) -> new#(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)) -> check#(y) 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#(new(x)) top1#(free(x),y) -> top2#(x,check(new(y))) -> top2#(x,free(y)) -> new#(x) top1#(free(x),y) -> check#(new(y)) -> check#(old(x)) -> old#(check(x)) top1#(free(x),y) -> check#(new(y)) -> check#(old(x)) -> check#(x) top1#(free(x),y) -> check#(new(y)) -> check#(new(x)) -> new#(check(x)) top1#(free(x),y) -> check#(new(y)) -> check#(new(x)) -> check#(x) top1#(free(x),y) -> check#(new(y)) -> check#(free(x)) -> check#(x) top1#(free(x),y) -> check#(new(x)) -> check#(old(x)) -> old#(check(x)) top1#(free(x),y) -> check#(new(x)) -> check#(old(x)) -> check#(x) top1#(free(x),y) -> check#(new(x)) -> check#(new(x)) -> new#(check(x)) top1#(free(x),y) -> check#(new(x)) -> check#(new(x)) -> check#(x) top1#(free(x),y) -> check#(new(x)) -> check#(free(x)) -> check#(x) top1#(free(x),y) -> check#(y) -> check#(old(x)) -> old#(check(x)) top1#(free(x),y) -> check#(y) -> check#(old(x)) -> check#(x) top1#(free(x),y) -> check#(y) -> check#(new(x)) -> new#(check(x)) top1#(free(x),y) -> check#(y) -> check#(new(x)) -> check#(x) top1#(free(x),y) -> check#(y) -> check#(free(x)) -> check#(x) top1#(free(x),y) -> check#(x) -> check#(old(x)) -> old#(check(x)) top1#(free(x),y) -> check#(x) -> check#(old(x)) -> check#(x) top1#(free(x),y) -> check#(x) -> check#(new(x)) -> new#(check(x)) top1#(free(x),y) -> check#(x) -> check#(new(x)) -> check#(x) top1#(free(x),y) -> check#(x) -> check#(free(x)) -> check#(x) top1#(free(x),y) -> new#(y) -> new#(free(x)) -> new#(x) top1#(free(x),y) -> new#(x) -> new#(free(x)) -> new#(x) SCC Processor: #sccs: 4 #rules: 13 #arcs: 143/729 DPs: top2#(x,free(y)) -> top1#(check(new(x)),y) top1#(free(x),y) -> top2#(check(new(x)),y) top2#(x,free(y)) -> top1#(new(x),check(y)) top1#(free(x),y) -> top2#(new(x),check(y)) top2#(x,free(y)) -> top1#(check(x),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#(x,check(new(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#(free(x)) -> check#(x) check#(new(x)) -> check#(x) check#(old(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) Subterm Criterion Processor: simple projection: pi(check#) = 0 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) Subterm Criterion Processor: simple projection: pi(new#) = 0 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) Subterm Criterion Processor: simple projection: pi(old#) = 0 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