MAYBE Problem: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Proof: DP Processor: DPs: rec#(rec(x)) -> sent#(rec(x)) rec#(sent(x)) -> rec#(x) rec#(sent(x)) -> sent#(rec(x)) rec#(no(x)) -> rec#(x) rec#(no(x)) -> sent#(rec(x)) rec#(bot()) -> sent#(bot()) rec#(up(x)) -> rec#(x) sent#(up(x)) -> sent#(x) no#(up(x)) -> no#(x) top#(rec(up(x))) -> rec#(x) top#(rec(up(x))) -> check#(rec(x)) top#(rec(up(x))) -> top#(check(rec(x))) top#(sent(up(x))) -> rec#(x) top#(sent(up(x))) -> check#(rec(x)) top#(sent(up(x))) -> top#(check(rec(x))) top#(no(up(x))) -> rec#(x) top#(no(up(x))) -> check#(rec(x)) top#(no(up(x))) -> top#(check(rec(x))) check#(up(x)) -> check#(x) check#(sent(x)) -> check#(x) check#(sent(x)) -> sent#(check(x)) check#(rec(x)) -> check#(x) check#(rec(x)) -> rec#(check(x)) check#(no(x)) -> check#(x) check#(no(x)) -> no#(check(x)) TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) TDG Processor: DPs: rec#(rec(x)) -> sent#(rec(x)) rec#(sent(x)) -> rec#(x) rec#(sent(x)) -> sent#(rec(x)) rec#(no(x)) -> rec#(x) rec#(no(x)) -> sent#(rec(x)) rec#(bot()) -> sent#(bot()) rec#(up(x)) -> rec#(x) sent#(up(x)) -> sent#(x) no#(up(x)) -> no#(x) top#(rec(up(x))) -> rec#(x) top#(rec(up(x))) -> check#(rec(x)) top#(rec(up(x))) -> top#(check(rec(x))) top#(sent(up(x))) -> rec#(x) top#(sent(up(x))) -> check#(rec(x)) top#(sent(up(x))) -> top#(check(rec(x))) top#(no(up(x))) -> rec#(x) top#(no(up(x))) -> check#(rec(x)) top#(no(up(x))) -> top#(check(rec(x))) check#(up(x)) -> check#(x) check#(sent(x)) -> check#(x) check#(sent(x)) -> sent#(check(x)) check#(rec(x)) -> check#(x) check#(rec(x)) -> rec#(check(x)) check#(no(x)) -> check#(x) check#(no(x)) -> no#(check(x)) TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) graph: check#(up(x)) -> check#(x) -> check#(no(x)) -> no#(check(x)) check#(up(x)) -> check#(x) -> check#(no(x)) -> check#(x) check#(up(x)) -> check#(x) -> check#(rec(x)) -> rec#(check(x)) check#(up(x)) -> check#(x) -> check#(rec(x)) -> check#(x) check#(up(x)) -> check#(x) -> check#(sent(x)) -> sent#(check(x)) check#(up(x)) -> check#(x) -> check#(sent(x)) -> check#(x) check#(up(x)) -> check#(x) -> check#(up(x)) -> check#(x) check#(no(x)) -> check#(x) -> check#(no(x)) -> no#(check(x)) check#(no(x)) -> check#(x) -> check#(no(x)) -> check#(x) check#(no(x)) -> check#(x) -> check#(rec(x)) -> rec#(check(x)) check#(no(x)) -> check#(x) -> check#(rec(x)) -> check#(x) check#(no(x)) -> check#(x) -> check#(sent(x)) -> sent#(check(x)) check#(no(x)) -> check#(x) -> check#(sent(x)) -> check#(x) check#(no(x)) -> check#(x) -> check#(up(x)) -> check#(x) check#(no(x)) -> no#(check(x)) -> no#(up(x)) -> no#(x) check#(sent(x)) -> check#(x) -> check#(no(x)) -> no#(check(x)) check#(sent(x)) -> check#(x) -> check#(no(x)) -> check#(x) check#(sent(x)) -> check#(x) -> check#(rec(x)) -> rec#(check(x)) check#(sent(x)) -> check#(x) -> check#(rec(x)) -> check#(x) check#(sent(x)) -> check#(x) -> check#(sent(x)) -> sent#(check(x)) check#(sent(x)) -> check#(x) -> check#(sent(x)) -> check#(x) check#(sent(x)) -> check#(x) -> check#(up(x)) -> check#(x) check#(sent(x)) -> sent#(check(x)) -> sent#(up(x)) -> sent#(x) check#(rec(x)) -> check#(x) -> check#(no(x)) -> no#(check(x)) check#(rec(x)) -> check#(x) -> check#(no(x)) -> check#(x) check#(rec(x)) -> check#(x) -> check#(rec(x)) -> rec#(check(x)) check#(rec(x)) -> check#(x) -> check#(rec(x)) -> check#(x) check#(rec(x)) -> check#(x) -> check#(sent(x)) -> sent#(check(x)) check#(rec(x)) -> check#(x) -> check#(sent(x)) -> check#(x) check#(rec(x)) -> check#(x) -> check#(up(x)) -> check#(x) check#(rec(x)) -> rec#(check(x)) -> rec#(up(x)) -> rec#(x) check#(rec(x)) -> rec#(check(x)) -> rec#(bot()) -> sent#(bot()) check#(rec(x)) -> rec#(check(x)) -> rec#(no(x)) -> sent#(rec(x)) check#(rec(x)) -> rec#(check(x)) -> rec#(no(x)) -> rec#(x) check#(rec(x)) -> rec#(check(x)) -> rec#(sent(x)) -> sent#(rec(x)) check#(rec(x)) -> rec#(check(x)) -> rec#(sent(x)) -> rec#(x) check#(rec(x)) -> rec#(check(x)) -> rec#(rec(x)) -> sent#(rec(x)) top#(no(up(x))) -> check#(rec(x)) -> check#(no(x)) -> no#(check(x)) top#(no(up(x))) -> check#(rec(x)) -> check#(no(x)) -> check#(x) top#(no(up(x))) -> check#(rec(x)) -> check#(rec(x)) -> rec#(check(x)) top#(no(up(x))) -> check#(rec(x)) -> check#(rec(x)) -> check#(x) top#(no(up(x))) -> check#(rec(x)) -> check#(sent(x)) -> sent#(check(x)) top#(no(up(x))) -> check#(rec(x)) -> check#(sent(x)) -> check#(x) top#(no(up(x))) -> check#(rec(x)) -> check#(up(x)) -> check#(x) top#(no(up(x))) -> top#(check(rec(x))) -> top#(no(up(x))) -> top#(check(rec(x))) top#(no(up(x))) -> top#(check(rec(x))) -> top#(no(up(x))) -> check#(rec(x)) top#(no(up(x))) -> top#(check(rec(x))) -> top#(no(up(x))) -> rec#(x) top#(no(up(x))) -> top#(check(rec(x))) -> top#(sent(up(x))) -> top#(check(rec(x))) top#(no(up(x))) -> top#(check(rec(x))) -> top#(sent(up(x))) -> check#(rec(x)) top#(no(up(x))) -> top#(check(rec(x))) -> top#(sent(up(x))) -> rec#(x) top#(no(up(x))) -> top#(check(rec(x))) -> top#(rec(up(x))) -> top#(check(rec(x))) top#(no(up(x))) -> top#(check(rec(x))) -> top#(rec(up(x))) -> check#(rec(x)) top#(no(up(x))) -> top#(check(rec(x))) -> top#(rec(up(x))) -> rec#(x) top#(no(up(x))) -> rec#(x) -> rec#(up(x)) -> rec#(x) top#(no(up(x))) -> rec#(x) -> rec#(bot()) -> sent#(bot()) top#(no(up(x))) -> rec#(x) -> rec#(no(x)) -> sent#(rec(x)) top#(no(up(x))) -> rec#(x) -> rec#(no(x)) -> rec#(x) top#(no(up(x))) -> rec#(x) -> rec#(sent(x)) -> sent#(rec(x)) top#(no(up(x))) -> rec#(x) -> rec#(sent(x)) -> rec#(x) top#(no(up(x))) -> rec#(x) -> rec#(rec(x)) -> sent#(rec(x)) top#(sent(up(x))) -> check#(rec(x)) -> check#(no(x)) -> no#(check(x)) top#(sent(up(x))) -> check#(rec(x)) -> check#(no(x)) -> check#(x) top#(sent(up(x))) -> check#(rec(x)) -> check#(rec(x)) -> rec#(check(x)) top#(sent(up(x))) -> check#(rec(x)) -> check#(rec(x)) -> check#(x) top#(sent(up(x))) -> check#(rec(x)) -> check#(sent(x)) -> sent#(check(x)) top#(sent(up(x))) -> check#(rec(x)) -> check#(sent(x)) -> check#(x) top#(sent(up(x))) -> check#(rec(x)) -> check#(up(x)) -> check#(x) top#(sent(up(x))) -> top#(check(rec(x))) -> top#(no(up(x))) -> top#(check(rec(x))) top#(sent(up(x))) -> top#(check(rec(x))) -> top#(no(up(x))) -> check#(rec(x)) top#(sent(up(x))) -> top#(check(rec(x))) -> top#(no(up(x))) -> rec#(x) top#(sent(up(x))) -> top#(check(rec(x))) -> top#(sent(up(x))) -> top#(check(rec(x))) top#(sent(up(x))) -> top#(check(rec(x))) -> top#(sent(up(x))) -> check#(rec(x)) top#(sent(up(x))) -> top#(check(rec(x))) -> top#(sent(up(x))) -> rec#(x) top#(sent(up(x))) -> top#(check(rec(x))) -> top#(rec(up(x))) -> top#(check(rec(x))) top#(sent(up(x))) -> top#(check(rec(x))) -> top#(rec(up(x))) -> check#(rec(x)) top#(sent(up(x))) -> top#(check(rec(x))) -> top#(rec(up(x))) -> rec#(x) top#(sent(up(x))) -> rec#(x) -> rec#(up(x)) -> rec#(x) top#(sent(up(x))) -> rec#(x) -> rec#(bot()) -> sent#(bot()) top#(sent(up(x))) -> rec#(x) -> rec#(no(x)) -> sent#(rec(x)) top#(sent(up(x))) -> rec#(x) -> rec#(no(x)) -> rec#(x) top#(sent(up(x))) -> rec#(x) -> rec#(sent(x)) -> sent#(rec(x)) top#(sent(up(x))) -> rec#(x) -> rec#(sent(x)) -> rec#(x) top#(sent(up(x))) -> rec#(x) -> rec#(rec(x)) -> sent#(rec(x)) top#(rec(up(x))) -> check#(rec(x)) -> check#(no(x)) -> no#(check(x)) top#(rec(up(x))) -> check#(rec(x)) -> check#(no(x)) -> check#(x) top#(rec(up(x))) -> check#(rec(x)) -> check#(rec(x)) -> rec#(check(x)) top#(rec(up(x))) -> check#(rec(x)) -> check#(rec(x)) -> check#(x) top#(rec(up(x))) -> check#(rec(x)) -> check#(sent(x)) -> sent#(check(x)) top#(rec(up(x))) -> check#(rec(x)) -> check#(sent(x)) -> check#(x) top#(rec(up(x))) -> check#(rec(x)) -> check#(up(x)) -> check#(x) top#(rec(up(x))) -> top#(check(rec(x))) -> top#(no(up(x))) -> top#(check(rec(x))) top#(rec(up(x))) -> top#(check(rec(x))) -> top#(no(up(x))) -> check#(rec(x)) top#(rec(up(x))) -> top#(check(rec(x))) -> top#(no(up(x))) -> rec#(x) top#(rec(up(x))) -> top#(check(rec(x))) -> top#(sent(up(x))) -> top#(check(rec(x))) top#(rec(up(x))) -> top#(check(rec(x))) -> top#(sent(up(x))) -> check#(rec(x)) top#(rec(up(x))) -> top#(check(rec(x))) -> top#(sent(up(x))) -> rec#(x) top#(rec(up(x))) -> top#(check(rec(x))) -> top#(rec(up(x))) -> top#(check(rec(x))) top#(rec(up(x))) -> top#(check(rec(x))) -> top#(rec(up(x))) -> check#(rec(x)) top#(rec(up(x))) -> top#(check(rec(x))) -> top#(rec(up(x))) -> rec#(x) top#(rec(up(x))) -> rec#(x) -> rec#(up(x)) -> rec#(x) top#(rec(up(x))) -> rec#(x) -> rec#(bot()) -> sent#(bot()) top#(rec(up(x))) -> rec#(x) -> rec#(no(x)) -> sent#(rec(x)) top#(rec(up(x))) -> rec#(x) -> rec#(no(x)) -> rec#(x) top#(rec(up(x))) -> rec#(x) -> rec#(sent(x)) -> sent#(rec(x)) top#(rec(up(x))) -> rec#(x) -> rec#(sent(x)) -> rec#(x) top#(rec(up(x))) -> rec#(x) -> rec#(rec(x)) -> sent#(rec(x)) no#(up(x)) -> no#(x) -> no#(up(x)) -> no#(x) sent#(up(x)) -> sent#(x) -> sent#(up(x)) -> sent#(x) rec#(up(x)) -> rec#(x) -> rec#(up(x)) -> rec#(x) rec#(up(x)) -> rec#(x) -> rec#(bot()) -> sent#(bot()) rec#(up(x)) -> rec#(x) -> rec#(no(x)) -> sent#(rec(x)) rec#(up(x)) -> rec#(x) -> rec#(no(x)) -> rec#(x) rec#(up(x)) -> rec#(x) -> rec#(sent(x)) -> sent#(rec(x)) rec#(up(x)) -> rec#(x) -> rec#(sent(x)) -> rec#(x) rec#(up(x)) -> rec#(x) -> rec#(rec(x)) -> sent#(rec(x)) rec#(bot()) -> sent#(bot()) -> sent#(up(x)) -> sent#(x) rec#(no(x)) -> sent#(rec(x)) -> sent#(up(x)) -> sent#(x) rec#(no(x)) -> rec#(x) -> rec#(up(x)) -> rec#(x) rec#(no(x)) -> rec#(x) -> rec#(bot()) -> sent#(bot()) rec#(no(x)) -> rec#(x) -> rec#(no(x)) -> sent#(rec(x)) rec#(no(x)) -> rec#(x) -> rec#(no(x)) -> rec#(x) rec#(no(x)) -> rec#(x) -> rec#(sent(x)) -> sent#(rec(x)) rec#(no(x)) -> rec#(x) -> rec#(sent(x)) -> rec#(x) rec#(no(x)) -> rec#(x) -> rec#(rec(x)) -> sent#(rec(x)) rec#(sent(x)) -> sent#(rec(x)) -> sent#(up(x)) -> sent#(x) rec#(sent(x)) -> rec#(x) -> rec#(up(x)) -> rec#(x) rec#(sent(x)) -> rec#(x) -> rec#(bot()) -> sent#(bot()) rec#(sent(x)) -> rec#(x) -> rec#(no(x)) -> sent#(rec(x)) rec#(sent(x)) -> rec#(x) -> rec#(no(x)) -> rec#(x) rec#(sent(x)) -> rec#(x) -> rec#(sent(x)) -> sent#(rec(x)) rec#(sent(x)) -> rec#(x) -> rec#(sent(x)) -> rec#(x) rec#(sent(x)) -> rec#(x) -> rec#(rec(x)) -> sent#(rec(x)) rec#(rec(x)) -> sent#(rec(x)) -> sent#(up(x)) -> sent#(x) SCC Processor: #sccs: 5 #rules: 12 #arcs: 133/625 DPs: top#(no(up(x))) -> top#(check(rec(x))) top#(rec(up(x))) -> top#(check(rec(x))) top#(sent(up(x))) -> top#(check(rec(x))) TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) KBO Processor: argument filtering: pi(rec) = 0 pi(sent) = 0 pi(no) = [0] pi(bot) = [] pi(up) = 0 pi(top) = 0 pi(check) = 0 pi(top#) = 0 weight function: w0 = 1 w(top#) = w(top) = w(bot) = 1 w(check) = w(up) = w(no) = w(sent) = w(rec) = 0 precedence: top# ~ check ~ top ~ up ~ bot ~ no ~ sent ~ rec problem: DPs: top#(rec(up(x))) -> top#(check(rec(x))) top#(sent(up(x))) -> top#(check(rec(x))) TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Arctic Interpretation Processor: dimension: 1 interpretation: [top#](x0) = x0, [check](x0) = x0, [top](x0) = 3x0, [up](x0) = 2x0, [bot] = 0, [no](x0) = 2x0, [sent](x0) = x0, [rec](x0) = 2x0 orientation: top#(rec(up(x))) = 4x >= 2x = top#(check(rec(x))) top#(sent(up(x))) = 2x >= 2x = top#(check(rec(x))) rec(rec(x)) = 4x >= 2x = sent(rec(x)) rec(sent(x)) = 2x >= 2x = sent(rec(x)) rec(no(x)) = 4x >= 2x = sent(rec(x)) rec(bot()) = 2 >= 2 = up(sent(bot())) rec(up(x)) = 4x >= 4x = up(rec(x)) sent(up(x)) = 2x >= 2x = up(sent(x)) no(up(x)) = 4x >= 4x = up(no(x)) top(rec(up(x))) = 7x >= 5x = top(check(rec(x))) top(sent(up(x))) = 5x >= 5x = top(check(rec(x))) top(no(up(x))) = 7x >= 5x = top(check(rec(x))) check(up(x)) = 2x >= 2x = up(check(x)) check(sent(x)) = x >= x = sent(check(x)) check(rec(x)) = 2x >= 2x = rec(check(x)) check(no(x)) = 2x >= 2x = no(check(x)) check(no(x)) = 2x >= 2x = no(x) problem: DPs: top#(sent(up(x))) -> top#(check(rec(x))) TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Open DPs: check#(up(x)) -> check#(x) check#(sent(x)) -> check#(x) check#(rec(x)) -> check#(x) check#(no(x)) -> check#(x) TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Subterm Criterion Processor: simple projection: pi(check#) = 0 problem: DPs: TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Qed DPs: no#(up(x)) -> no#(x) TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Subterm Criterion Processor: simple projection: pi(no#) = 0 problem: DPs: TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Qed DPs: rec#(sent(x)) -> rec#(x) rec#(no(x)) -> rec#(x) rec#(up(x)) -> rec#(x) TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Subterm Criterion Processor: simple projection: pi(rec#) = 0 problem: DPs: TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Qed DPs: sent#(up(x)) -> sent#(x) TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Subterm Criterion Processor: simple projection: pi(sent#) = 0 problem: DPs: TRS: rec(rec(x)) -> sent(rec(x)) rec(sent(x)) -> sent(rec(x)) rec(no(x)) -> sent(rec(x)) rec(bot()) -> up(sent(bot())) rec(up(x)) -> up(rec(x)) sent(up(x)) -> up(sent(x)) no(up(x)) -> up(no(x)) top(rec(up(x))) -> top(check(rec(x))) top(sent(up(x))) -> top(check(rec(x))) top(no(up(x))) -> top(check(rec(x))) check(up(x)) -> up(check(x)) check(sent(x)) -> sent(check(x)) check(rec(x)) -> rec(check(x)) check(no(x)) -> no(check(x)) check(no(x)) -> no(x) Qed