YES Problem: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Proof: DP Processor: DPs: active#(f(X)) -> f#(true()) active#(f(X)) -> if#(X,c(),f(true())) active#(f(X)) -> mark#(if(X,c(),f(true()))) active#(if(true(),X,Y)) -> mark#(X) active#(if(false(),X,Y)) -> mark#(Y) mark#(f(X)) -> mark#(X) mark#(f(X)) -> f#(mark(X)) mark#(f(X)) -> active#(f(mark(X))) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(c()) -> active#(c()) mark#(true()) -> active#(true()) mark#(false()) -> active#(false()) f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) TDG Processor: DPs: active#(f(X)) -> f#(true()) active#(f(X)) -> if#(X,c(),f(true())) active#(f(X)) -> mark#(if(X,c(),f(true()))) active#(if(true(),X,Y)) -> mark#(X) active#(if(false(),X,Y)) -> mark#(Y) mark#(f(X)) -> mark#(X) mark#(f(X)) -> f#(mark(X)) mark#(f(X)) -> active#(f(mark(X))) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(c()) -> active#(c()) mark#(true()) -> active#(true()) mark#(false()) -> active#(false()) f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) graph: mark#(false()) -> active#(false()) -> active#(if(false(),X,Y)) -> mark#(Y) mark#(false()) -> active#(false()) -> active#(if(true(),X,Y)) -> mark#(X) mark#(false()) -> active#(false()) -> active#(f(X)) -> mark#(if(X,c(),f(true()))) mark#(false()) -> active#(false()) -> active#(f(X)) -> if#(X,c(),f(true())) mark#(false()) -> active#(false()) -> active#(f(X)) -> f#(true()) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(false()) -> active#(false()) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(true()) -> active#(true()) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(c()) -> active#(c()) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> active#(f(mark(X))) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(false()) -> active#(false()) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(true()) -> active#(true()) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(c()) -> active#(c()) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> active#(f(mark(X))) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> f#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(if(false(),X,Y)) -> mark#(Y) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(if(true(),X,Y)) -> mark#(X) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(f(X)) -> mark#(if(X,c(),f(true()))) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(f(X)) -> if#(X,c(),f(true())) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(f(X)) -> f#(true()) mark#(true()) -> active#(true()) -> active#(if(false(),X,Y)) -> mark#(Y) mark#(true()) -> active#(true()) -> active#(if(true(),X,Y)) -> mark#(X) mark#(true()) -> active#(true()) -> active#(f(X)) -> mark#(if(X,c(),f(true()))) mark#(true()) -> active#(true()) -> active#(f(X)) -> if#(X,c(),f(true())) mark#(true()) -> active#(true()) -> active#(f(X)) -> f#(true()) mark#(c()) -> active#(c()) -> active#(if(false(),X,Y)) -> mark#(Y) mark#(c()) -> active#(c()) -> active#(if(true(),X,Y)) -> mark#(X) mark#(c()) -> active#(c()) -> active#(f(X)) -> mark#(if(X,c(),f(true()))) mark#(c()) -> active#(c()) -> active#(f(X)) -> if#(X,c(),f(true())) mark#(c()) -> active#(c()) -> active#(f(X)) -> f#(true()) mark#(f(X)) -> mark#(X) -> mark#(false()) -> active#(false()) mark#(f(X)) -> mark#(X) -> mark#(true()) -> active#(true()) mark#(f(X)) -> mark#(X) -> mark#(c()) -> active#(c()) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X)) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(f(X)) -> f#(mark(X)) -> f#(active(X)) -> f#(X) mark#(f(X)) -> f#(mark(X)) -> f#(mark(X)) -> f#(X) mark#(f(X)) -> active#(f(mark(X))) -> active#(if(false(),X,Y)) -> mark#(Y) mark#(f(X)) -> active#(f(mark(X))) -> active#(if(true(),X,Y)) -> mark#(X) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(X)) -> mark#(if(X,c(),f(true()))) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(X)) -> if#(X,c(),f(true())) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(X)) -> f#(true()) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(mark(X1),X2,X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) f#(mark(X)) -> f#(X) -> f#(active(X)) -> f#(X) f#(mark(X)) -> f#(X) -> f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) -> f#(active(X)) -> f#(X) f#(active(X)) -> f#(X) -> f#(mark(X)) -> f#(X) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(false()) -> active#(false()) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(true()) -> active#(true()) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(c()) -> active#(c()) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X1) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X2) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(f(X)) -> active#(f(mark(X))) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(f(X)) -> f#(mark(X)) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(f(X)) -> mark#(X) active#(if(true(),X,Y)) -> mark#(X) -> mark#(false()) -> active#(false()) active#(if(true(),X,Y)) -> mark#(X) -> mark#(true()) -> active#(true()) active#(if(true(),X,Y)) -> mark#(X) -> mark#(c()) -> active#(c()) active#(if(true(),X,Y)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(true(),X,Y)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) active#(if(true(),X,Y)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) active#(if(true(),X,Y)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) active#(if(true(),X,Y)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) active#(if(true(),X,Y)) -> mark#(X) -> mark#(f(X)) -> f#(mark(X)) active#(if(true(),X,Y)) -> mark#(X) -> mark#(f(X)) -> mark#(X) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(false()) -> active#(false()) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(true()) -> active#(true()) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(c()) -> active#(c()) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(if(X1,X2,X3)) -> if#(mark(X1),mark(X2),X3) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(if(X1,X2,X3)) -> mark#(X1) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(if(X1,X2,X3)) -> mark#(X2) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(f(X)) -> active#(f(mark(X))) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(f(X)) -> f#(mark(X)) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(f(X)) -> mark#(X) active#(f(X)) -> if#(X,c(),f(true())) -> if#(X1,X2,active(X3)) -> if#(X1,X2,X3) active#(f(X)) -> if#(X,c(),f(true())) -> if#(X1,active(X2),X3) -> if#(X1,X2,X3) active#(f(X)) -> if#(X,c(),f(true())) -> if#(active(X1),X2,X3) -> if#(X1,X2,X3) active#(f(X)) -> if#(X,c(),f(true())) -> if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) active#(f(X)) -> if#(X,c(),f(true())) -> if#(X1,mark(X2),X3) -> if#(X1,X2,X3) active#(f(X)) -> if#(X,c(),f(true())) -> if#(mark(X1),X2,X3) -> if#(X1,X2,X3) active#(f(X)) -> f#(true()) -> f#(active(X)) -> f#(X) active#(f(X)) -> f#(true()) -> f#(mark(X)) -> f#(X) SCC Processor: #sccs: 3 #rules: 19 #arcs: 141/529 DPs: mark#(false()) -> active#(false()) active#(f(X)) -> mark#(if(X,c(),f(true()))) mark#(f(X)) -> mark#(X) mark#(f(X)) -> active#(f(mark(X))) active#(if(true(),X,Y)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) -> mark#(Y) mark#(c()) -> active#(c()) mark#(true()) -> active#(true()) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) EDG Processor: DPs: mark#(false()) -> active#(false()) active#(f(X)) -> mark#(if(X,c(),f(true()))) mark#(f(X)) -> mark#(X) mark#(f(X)) -> active#(f(mark(X))) active#(if(true(),X,Y)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) -> mark#(Y) mark#(c()) -> active#(c()) mark#(true()) -> active#(true()) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) graph: mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> active#(f(mark(X))) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(c()) -> active#(c()) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(true()) -> active#(true()) mark#(if(X1,X2,X3)) -> mark#(X2) -> mark#(false()) -> active#(false()) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> active#(f(mark(X))) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(c()) -> active#(c()) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(true()) -> active#(true()) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(false()) -> active#(false()) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(f(X)) -> mark#(if(X,c(),f(true()))) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(if(true(),X,Y)) -> mark#(X) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) -> active#(if(false(),X,Y)) -> mark#(Y) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(f(X)) -> mark#(X) -> mark#(c()) -> active#(c()) mark#(f(X)) -> mark#(X) -> mark#(true()) -> active#(true()) mark#(f(X)) -> mark#(X) -> mark#(false()) -> active#(false()) mark#(f(X)) -> active#(f(mark(X))) -> active#(f(X)) -> mark#(if(X,c(),f(true()))) mark#(f(X)) -> active#(f(mark(X))) -> active#(if(true(),X,Y)) -> mark#(X) mark#(f(X)) -> active#(f(mark(X))) -> active#(if(false(),X,Y)) -> mark#(Y) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(f(X)) -> mark#(X) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(f(X)) -> active#(f(mark(X))) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X2) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X1) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(c()) -> active#(c()) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(true()) -> active#(true()) active#(if(false(),X,Y)) -> mark#(Y) -> mark#(false()) -> active#(false()) active#(if(true(),X,Y)) -> mark#(X) -> mark#(f(X)) -> mark#(X) active#(if(true(),X,Y)) -> mark#(X) -> mark#(f(X)) -> active#(f(mark(X))) active#(if(true(),X,Y)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X2) active#(if(true(),X,Y)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) active#(if(true(),X,Y)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(true(),X,Y)) -> mark#(X) -> mark#(c()) -> active#(c()) active#(if(true(),X,Y)) -> mark#(X) -> mark#(true()) -> active#(true()) active#(if(true(),X,Y)) -> mark#(X) -> mark#(false()) -> active#(false()) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(f(X)) -> mark#(X) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(f(X)) -> active#(f(mark(X))) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(if(X1,X2,X3)) -> mark#(X2) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(if(X1,X2,X3)) -> mark#(X1) active#(f(X)) -> mark#(if(X,c(),f(true()))) -> mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) SCC Processor: #sccs: 1 #rules: 8 #arcs: 51/121 DPs: mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) -> mark#(Y) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> active#(f(mark(X))) active#(if(true(),X,Y)) -> mark#(X) mark#(f(X)) -> mark#(X) active#(f(X)) -> mark#(if(X,c(),f(true()))) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0 + 0, [active#](x0) = x0, [false] = 0, [mark](x0) = x0, [if](x0, x1, x2) = x0 + 1x1 + x2, [true] = 2, [c] = 0, [active](x0) = x0, [f](x0) = x0 + 2 orientation: mark#(if(X1,X2,X3)) = X1 + 1X2 + X3 + 0 >= X2 + 0 = mark#(X2) mark#(if(X1,X2,X3)) = X1 + 1X2 + X3 + 0 >= X1 + 1X2 + X3 = active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) = 1X + Y + 0 >= Y + 0 = mark#(Y) mark#(if(X1,X2,X3)) = X1 + 1X2 + X3 + 0 >= X1 + 0 = mark#(X1) mark#(f(X)) = X + 2 >= X + 2 = active#(f(mark(X))) active#(if(true(),X,Y)) = 1X + Y + 2 >= X + 0 = mark#(X) mark#(f(X)) = X + 2 >= X + 0 = mark#(X) active#(f(X)) = X + 2 >= X + 2 = mark#(if(X,c(),f(true()))) active(f(X)) = X + 2 >= X + 2 = mark(if(X,c(),f(true()))) active(if(true(),X,Y)) = 1X + Y + 2 >= X = mark(X) active(if(false(),X,Y)) = 1X + Y + 0 >= Y = mark(Y) mark(f(X)) = X + 2 >= X + 2 = active(f(mark(X))) mark(if(X1,X2,X3)) = X1 + 1X2 + X3 >= X1 + 1X2 + X3 = active(if(mark(X1),mark(X2),X3)) mark(c()) = 0 >= 0 = active(c()) mark(true()) = 2 >= 2 = active(true()) mark(false()) = 0 >= 0 = active(false()) f(mark(X)) = X + 2 >= X + 2 = f(X) f(active(X)) = X + 2 >= X + 2 = f(X) if(mark(X1),X2,X3) = X1 + 1X2 + X3 >= X1 + 1X2 + X3 = if(X1,X2,X3) if(X1,mark(X2),X3) = X1 + 1X2 + X3 >= X1 + 1X2 + X3 = if(X1,X2,X3) if(X1,X2,mark(X3)) = X1 + 1X2 + X3 >= X1 + 1X2 + X3 = if(X1,X2,X3) if(active(X1),X2,X3) = X1 + 1X2 + X3 >= X1 + 1X2 + X3 = if(X1,X2,X3) if(X1,active(X2),X3) = X1 + 1X2 + X3 >= X1 + 1X2 + X3 = if(X1,X2,X3) if(X1,X2,active(X3)) = X1 + 1X2 + X3 >= X1 + 1X2 + X3 = if(X1,X2,X3) problem: DPs: mark#(if(X1,X2,X3)) -> mark#(X2) mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) -> mark#(Y) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> active#(f(mark(X))) mark#(f(X)) -> mark#(X) active#(f(X)) -> mark#(if(X,c(),f(true()))) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [active#](x0) = x0 + 0, [false] = 0, [mark](x0) = x0 + 0, [if](x0, x1, x2) = x0 + 1x1 + x2 + 1, [true] = 0, [c] = 0, [active](x0) = x0 + 0, [f](x0) = x0 + 1 orientation: mark#(if(X1,X2,X3)) = X1 + 1X2 + X3 + 1 >= X2 = mark#(X2) mark#(if(X1,X2,X3)) = X1 + 1X2 + X3 + 1 >= X1 + 1X2 + X3 + 1 = active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) = 1X + Y + 1 >= Y = mark#(Y) mark#(if(X1,X2,X3)) = X1 + 1X2 + X3 + 1 >= X1 = mark#(X1) mark#(f(X)) = X + 1 >= X + 1 = active#(f(mark(X))) mark#(f(X)) = X + 1 >= X = mark#(X) active#(f(X)) = X + 1 >= X + 1 = mark#(if(X,c(),f(true()))) active(f(X)) = X + 1 >= X + 1 = mark(if(X,c(),f(true()))) active(if(true(),X,Y)) = 1X + Y + 1 >= X + 0 = mark(X) active(if(false(),X,Y)) = 1X + Y + 1 >= Y + 0 = mark(Y) mark(f(X)) = X + 1 >= X + 1 = active(f(mark(X))) mark(if(X1,X2,X3)) = X1 + 1X2 + X3 + 1 >= X1 + 1X2 + X3 + 1 = active(if(mark(X1),mark(X2),X3)) mark(c()) = 0 >= 0 = active(c()) mark(true()) = 0 >= 0 = active(true()) mark(false()) = 0 >= 0 = active(false()) f(mark(X)) = X + 1 >= X + 1 = f(X) f(active(X)) = X + 1 >= X + 1 = f(X) if(mark(X1),X2,X3) = X1 + 1X2 + X3 + 1 >= X1 + 1X2 + X3 + 1 = if(X1,X2,X3) if(X1,mark(X2),X3) = X1 + 1X2 + X3 + 1 >= X1 + 1X2 + X3 + 1 = if(X1,X2,X3) if(X1,X2,mark(X3)) = X1 + 1X2 + X3 + 1 >= X1 + 1X2 + X3 + 1 = if(X1,X2,X3) if(active(X1),X2,X3) = X1 + 1X2 + X3 + 1 >= X1 + 1X2 + X3 + 1 = if(X1,X2,X3) if(X1,active(X2),X3) = X1 + 1X2 + X3 + 1 >= X1 + 1X2 + X3 + 1 = if(X1,X2,X3) if(X1,X2,active(X3)) = X1 + 1X2 + X3 + 1 >= X1 + 1X2 + X3 + 1 = if(X1,X2,X3) problem: DPs: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) -> mark#(Y) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> active#(f(mark(X))) mark#(f(X)) -> mark#(X) active#(f(X)) -> mark#(if(X,c(),f(true()))) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0 + 1, [active#](x0) = x0 + 1, [false] = 2, [mark](x0) = x0 + 1, [if](x0, x1, x2) = x0 + x1 + 1x2 + 0, [true] = 0, [c] = 0, [active](x0) = x0 + 1, [f](x0) = x0 + 0 orientation: mark#(if(X1,X2,X3)) = X1 + X2 + 1X3 + 1 >= X1 + X2 + 1X3 + 1 = active#(if(mark(X1),mark(X2),X3)) active#(if(false(),X,Y)) = X + 1Y + 2 >= Y + 1 = mark#(Y) mark#(if(X1,X2,X3)) = X1 + X2 + 1X3 + 1 >= X1 + 1 = mark#(X1) mark#(f(X)) = X + 1 >= X + 1 = active#(f(mark(X))) mark#(f(X)) = X + 1 >= X + 1 = mark#(X) active#(f(X)) = X + 1 >= X + 1 = mark#(if(X,c(),f(true()))) active(f(X)) = X + 1 >= X + 1 = mark(if(X,c(),f(true()))) active(if(true(),X,Y)) = X + 1Y + 1 >= X + 1 = mark(X) active(if(false(),X,Y)) = X + 1Y + 2 >= Y + 1 = mark(Y) mark(f(X)) = X + 1 >= X + 1 = active(f(mark(X))) mark(if(X1,X2,X3)) = X1 + X2 + 1X3 + 1 >= X1 + X2 + 1X3 + 1 = active(if(mark(X1),mark(X2),X3)) mark(c()) = 1 >= 1 = active(c()) mark(true()) = 1 >= 1 = active(true()) mark(false()) = 2 >= 2 = active(false()) f(mark(X)) = X + 1 >= X + 0 = f(X) f(active(X)) = X + 1 >= X + 0 = f(X) if(mark(X1),X2,X3) = X1 + X2 + 1X3 + 1 >= X1 + X2 + 1X3 + 0 = if(X1,X2,X3) if(X1,mark(X2),X3) = X1 + X2 + 1X3 + 1 >= X1 + X2 + 1X3 + 0 = if(X1,X2,X3) if(X1,X2,mark(X3)) = X1 + X2 + 1X3 + 2 >= X1 + X2 + 1X3 + 0 = if(X1,X2,X3) if(active(X1),X2,X3) = X1 + X2 + 1X3 + 1 >= X1 + X2 + 1X3 + 0 = if(X1,X2,X3) if(X1,active(X2),X3) = X1 + X2 + 1X3 + 1 >= X1 + X2 + 1X3 + 0 = if(X1,X2,X3) if(X1,X2,active(X3)) = X1 + X2 + 1X3 + 2 >= X1 + X2 + 1X3 + 0 = if(X1,X2,X3) problem: DPs: mark#(if(X1,X2,X3)) -> active#(if(mark(X1),mark(X2),X3)) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> active#(f(mark(X))) mark#(f(X)) -> mark#(X) active#(f(X)) -> mark#(if(X,c(),f(true()))) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = 2, [active#](x0) = x0 + 0, [false] = 1, [mark](x0) = 3, [if](x0, x1, x2) = 0, [true] = 2, [c] = 2, [active](x0) = x0 + 3, [f](x0) = 2 orientation: mark#(if(X1,X2,X3)) = 2 >= 0 = active#(if(mark(X1),mark(X2),X3)) mark#(if(X1,X2,X3)) = 2 >= 2 = mark#(X1) mark#(f(X)) = 2 >= 2 = active#(f(mark(X))) mark#(f(X)) = 2 >= 2 = mark#(X) active#(f(X)) = 2 >= 2 = mark#(if(X,c(),f(true()))) active(f(X)) = 3 >= 3 = mark(if(X,c(),f(true()))) active(if(true(),X,Y)) = 3 >= 3 = mark(X) active(if(false(),X,Y)) = 3 >= 3 = mark(Y) mark(f(X)) = 3 >= 3 = active(f(mark(X))) mark(if(X1,X2,X3)) = 3 >= 3 = active(if(mark(X1),mark(X2),X3)) mark(c()) = 3 >= 3 = active(c()) mark(true()) = 3 >= 3 = active(true()) mark(false()) = 3 >= 3 = active(false()) f(mark(X)) = 2 >= 2 = f(X) f(active(X)) = 2 >= 2 = f(X) if(mark(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3) if(X1,mark(X2),X3) = 0 >= 0 = if(X1,X2,X3) if(X1,X2,mark(X3)) = 0 >= 0 = if(X1,X2,X3) if(active(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3) if(X1,active(X2),X3) = 0 >= 0 = if(X1,X2,X3) if(X1,X2,active(X3)) = 0 >= 0 = if(X1,X2,X3) problem: DPs: mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> active#(f(mark(X))) mark#(f(X)) -> mark#(X) active#(f(X)) -> mark#(if(X,c(),f(true()))) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0 + 3, [active#](x0) = x0 + 0, [false] = 5, [mark](x0) = x0 + 0, [if](x0, x1, x2) = x0 + x1 + x2 + 2, [true] = 0, [c] = 4, [active](x0) = x0 + 0, [f](x0) = 6x0 + 7 orientation: mark#(if(X1,X2,X3)) = X1 + X2 + X3 + 3 >= X1 + 3 = mark#(X1) mark#(f(X)) = 6X + 7 >= 6X + 7 = active#(f(mark(X))) mark#(f(X)) = 6X + 7 >= X + 3 = mark#(X) active#(f(X)) = 6X + 7 >= X + 7 = mark#(if(X,c(),f(true()))) active(f(X)) = 6X + 7 >= X + 7 = mark(if(X,c(),f(true()))) active(if(true(),X,Y)) = X + Y + 2 >= X + 0 = mark(X) active(if(false(),X,Y)) = X + Y + 5 >= Y + 0 = mark(Y) mark(f(X)) = 6X + 7 >= 6X + 7 = active(f(mark(X))) mark(if(X1,X2,X3)) = X1 + X2 + X3 + 2 >= X1 + X2 + X3 + 2 = active(if(mark(X1),mark(X2),X3)) mark(c()) = 4 >= 4 = active(c()) mark(true()) = 0 >= 0 = active(true()) mark(false()) = 5 >= 5 = active(false()) f(mark(X)) = 6X + 7 >= 6X + 7 = f(X) f(active(X)) = 6X + 7 >= 6X + 7 = f(X) if(mark(X1),X2,X3) = X1 + X2 + X3 + 2 >= X1 + X2 + X3 + 2 = if(X1,X2,X3) if(X1,mark(X2),X3) = X1 + X2 + X3 + 2 >= X1 + X2 + X3 + 2 = if(X1,X2,X3) if(X1,X2,mark(X3)) = X1 + X2 + X3 + 2 >= X1 + X2 + X3 + 2 = if(X1,X2,X3) if(active(X1),X2,X3) = X1 + X2 + X3 + 2 >= X1 + X2 + X3 + 2 = if(X1,X2,X3) if(X1,active(X2),X3) = X1 + X2 + X3 + 2 >= X1 + X2 + X3 + 2 = if(X1,X2,X3) if(X1,X2,active(X3)) = X1 + X2 + X3 + 2 >= X1 + X2 + X3 + 2 = if(X1,X2,X3) problem: DPs: mark#(if(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> active#(f(mark(X))) active#(f(X)) -> mark#(if(X,c(),f(true()))) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = 4x0 + 0, [active#](x0) = 4x0 + 0, [false] = 2, [mark](x0) = x0 + 0, [if](x0, x1, x2) = 1x0 + x1 + x2 + 1, [true] = 0, [c] = 0, [active](x0) = x0 + 0, [f](x0) = 1x0 + 1 orientation: mark#(if(X1,X2,X3)) = 5X1 + 4X2 + 4X3 + 5 >= 4X1 + 0 = mark#(X1) mark#(f(X)) = 5X + 5 >= 5X + 5 = active#(f(mark(X))) active#(f(X)) = 5X + 5 >= 5X + 5 = mark#(if(X,c(),f(true()))) active(f(X)) = 1X + 1 >= 1X + 1 = mark(if(X,c(),f(true()))) active(if(true(),X,Y)) = X + Y + 1 >= X + 0 = mark(X) active(if(false(),X,Y)) = X + Y + 3 >= Y + 0 = mark(Y) mark(f(X)) = 1X + 1 >= 1X + 1 = active(f(mark(X))) mark(if(X1,X2,X3)) = 1X1 + X2 + X3 + 1 >= 1X1 + X2 + X3 + 1 = active(if(mark(X1),mark(X2),X3)) mark(c()) = 0 >= 0 = active(c()) mark(true()) = 0 >= 0 = active(true()) mark(false()) = 2 >= 2 = active(false()) f(mark(X)) = 1X + 1 >= 1X + 1 = f(X) f(active(X)) = 1X + 1 >= 1X + 1 = f(X) if(mark(X1),X2,X3) = 1X1 + X2 + X3 + 1 >= 1X1 + X2 + X3 + 1 = if(X1,X2,X3) if(X1,mark(X2),X3) = 1X1 + X2 + X3 + 1 >= 1X1 + X2 + X3 + 1 = if(X1,X2,X3) if(X1,X2,mark(X3)) = 1X1 + X2 + X3 + 1 >= 1X1 + X2 + X3 + 1 = if(X1,X2,X3) if(active(X1),X2,X3) = 1X1 + X2 + X3 + 1 >= 1X1 + X2 + X3 + 1 = if(X1,X2,X3) if(X1,active(X2),X3) = 1X1 + X2 + X3 + 1 >= 1X1 + X2 + X3 + 1 = if(X1,X2,X3) if(X1,X2,active(X3)) = 1X1 + X2 + X3 + 1 >= 1X1 + X2 + X3 + 1 = if(X1,X2,X3) problem: DPs: mark#(f(X)) -> active#(f(mark(X))) active#(f(X)) -> mark#(if(X,c(),f(true()))) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0 + 0, [active#](x0) = x0 + 0, [false] = 0, [mark](x0) = 2, [if](x0, x1, x2) = 0, [true] = 0, [c] = 4, [active](x0) = 2, [f](x0) = 1 orientation: mark#(f(X)) = 1 >= 1 = active#(f(mark(X))) active#(f(X)) = 1 >= 0 = mark#(if(X,c(),f(true()))) active(f(X)) = 2 >= 2 = mark(if(X,c(),f(true()))) active(if(true(),X,Y)) = 2 >= 2 = mark(X) active(if(false(),X,Y)) = 2 >= 2 = mark(Y) mark(f(X)) = 2 >= 2 = active(f(mark(X))) mark(if(X1,X2,X3)) = 2 >= 2 = active(if(mark(X1),mark(X2),X3)) mark(c()) = 2 >= 2 = active(c()) mark(true()) = 2 >= 2 = active(true()) mark(false()) = 2 >= 2 = active(false()) f(mark(X)) = 1 >= 1 = f(X) f(active(X)) = 1 >= 1 = f(X) if(mark(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3) if(X1,mark(X2),X3) = 0 >= 0 = if(X1,X2,X3) if(X1,X2,mark(X3)) = 0 >= 0 = if(X1,X2,X3) if(active(X1),X2,X3) = 0 >= 0 = if(X1,X2,X3) if(X1,active(X2),X3) = 0 >= 0 = if(X1,X2,X3) if(X1,X2,active(X3)) = 0 >= 0 = if(X1,X2,X3) problem: DPs: mark#(f(X)) -> active#(f(mark(X))) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) SCC Processor: #sccs: 0 #rules: 0 #arcs: 36/1 DPs: if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,mark(X3)) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) if#(X1,X2,active(X3)) -> if#(X1,X2,X3) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Subterm Criterion Processor: simple projection: pi(if#) = 2 problem: DPs: if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,mark(X2),X3) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) if#(X1,active(X2),X3) -> if#(X1,X2,X3) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Subterm Criterion Processor: simple projection: pi(if#) = 1 problem: DPs: if#(mark(X1),X2,X3) -> if#(X1,X2,X3) if#(active(X1),X2,X3) -> if#(X1,X2,X3) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Subterm Criterion Processor: simple projection: pi(if#) = 0 problem: DPs: TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Qed DPs: f#(mark(X)) -> f#(X) f#(active(X)) -> f#(X) TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Subterm Criterion Processor: simple projection: pi(f#) = 0 problem: DPs: TRS: active(f(X)) -> mark(if(X,c(),f(true()))) active(if(true(),X,Y)) -> mark(X) active(if(false(),X,Y)) -> mark(Y) mark(f(X)) -> active(f(mark(X))) mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3)) mark(c()) -> active(c()) mark(true()) -> active(true()) mark(false()) -> active(false()) f(mark(X)) -> f(X) f(active(X)) -> f(X) if(mark(X1),X2,X3) -> if(X1,X2,X3) if(X1,mark(X2),X3) -> if(X1,X2,X3) if(X1,X2,mark(X3)) -> if(X1,X2,X3) if(active(X1),X2,X3) -> if(X1,X2,X3) if(X1,active(X2),X3) -> if(X1,X2,X3) if(X1,X2,active(X3)) -> if(X1,X2,X3) Qed