YES Proof: This system is quasi-decreasing. By \cite{O02}, p. 214, Proposition 7.2.50. This system is of type 3 or smaller. This system is deterministic. System R transformed to U(R). Call external tool: ttt2 - trs 30 Input: ?1(pair(z1, z2), x, y, rest) -> cons(z1, cons(z2, rest)) cons(x, cons(y, rest)) -> ?1(orient(x, y), x, y, rest) cons(x, cons(x, rest)) -> cons(x, rest) ?2(pair(z1, z2), x, y) -> pair(s(z1), s(z2)) orient(s(x), s(y)) -> ?2(orient(x, y), x, y) orient(s(x), 0) -> pair(0, s(x)) DP Processor: DPs: ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest) ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) cons#(x,cons(y,rest)) -> orient#(x,y) cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) orient#(s(x),s(y)) -> orient#(x,y) orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y) TRS: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) TDG Processor: DPs: ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest) ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) cons#(x,cons(y,rest)) -> orient#(x,y) cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) orient#(s(x),s(y)) -> orient#(x,y) orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y) TRS: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) graph: orient#(s(x),s(y)) -> orient#(x,y) -> orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y) orient#(s(x),s(y)) -> orient#(x,y) -> orient#(s(x),s(y)) -> orient#(x,y) cons#(x,cons(y,rest)) -> orient#(x,y) -> orient#(s(x),s(y)) -> ?2#(orient(x,y),x,y) cons#(x,cons(y,rest)) -> orient#(x,y) -> orient#(s(x),s(y)) -> orient#(x,y) cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) -> ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) -> ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest) ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) -> cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) -> cons#(x,cons(y,rest)) -> orient#(x,y) ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest) -> cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest) -> cons#(x,cons(y,rest)) -> orient#(x,y) SCC Processor: #sccs: 2 #rules: 4 #arcs: 10/36 DPs: cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) ?1#(pair(z1,z2),x,y,rest) -> cons#(z2,rest) ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) TRS: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) Matrix Interpretation Processor: dim=2 usable rules: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) interpretation: [0] [?2](x0, x1, x2) = [0], [cons#](x0, x1) = [0 2]x1, [0 0] [0] [?1](x0, x1, x2, x3) = [0 1]x3 + [2], [0 0] [2] [orient](x0, x1) = [0 3]x1 + [0], [0] [s](x0) = [0], [0 0] [pair](x0, x1) = [1 1]x0, [?1#](x0, x1, x2, x3) = [0 2]x3 + [2], [1] [0] = [1], [0 0] [0] [cons](x0, x1) = [0 1]x1 + [1] orientation: cons#(x,cons(y,rest)) = [0 2]rest + [2] >= [0 2]rest + [2] = ?1#(orient(x,y),x,y,rest) ?1#(pair(z1,z2),x,y,rest) = [0 2]rest + [2] >= [0 2]rest = cons#(z2,rest) ?1#(pair(z1,z2),x,y,rest) = [0 2]rest + [2] >= [0 2]rest + [2] = cons#(z1,cons(z2,rest)) [0 0] [0] [0 0] [0] ?1(pair(z1,z2),x,y,rest) = [0 1]rest + [2] >= [0 1]rest + [2] = cons(z1,cons(z2,rest)) [0 0] [0] [0 0] [0] cons(x,cons(y,rest)) = [0 1]rest + [2] >= [0 1]rest + [2] = ?1(orient(x,y),x,y,rest) [0 0] [0] [0 0] [0] cons(x,cons(x,rest)) = [0 1]rest + [2] >= [0 1]rest + [1] = cons(x,rest) [0] [0] ?2(pair(z1,z2),x,y) = [0] >= [0] = pair(s(z1),s(z2)) [2] [0] orient(s(x),s(y)) = [0] >= [0] = ?2(orient(x,y),x,y) [2] [0] orient(s(x),0()) = [3] >= [2] = pair(0(),s(x)) problem: DPs: cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) TRS: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) Restore Modifier: DPs: cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) TRS: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) EDG Processor: DPs: cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) TRS: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) graph: cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) -> ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) ?1#(pair(z1,z2),x,y,rest) -> cons#(z1,cons(z2,rest)) -> cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) Matrix Interpretation Processor: dim=2 usable rules: ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) interpretation: [0 0] [1 1] [?2](x0, x1, x2) = [0 3]x0 + [0 0]x1, [cons#](x0, x1) = [0 2]x0, [0 0] [0 0] [0] [?1](x0, x1, x2, x3) = [0 2]x0 + [1 0]x1 + [1], [2 0] [2 0] [orient](x0, x1) = [0 1]x0 + [0 0]x1, [1 1] [0] [s](x0) = [0 3]x0 + [1], [0 0] [0] [pair](x0, x1) = [0 1]x0 + [1], [?1#](x0, x1, x2, x3) = [0 2]x0, [1] [0] = [0], [0] [cons](x0, x1) = [0] orientation: cons#(x,cons(y,rest)) = [0 2]x >= [0 2]x = ?1#(orient(x,y),x,y,rest) ?1#(pair(z1,z2),x,y,rest) = [0 2]z1 + [2] >= [0 2]z1 = cons#(z1,cons(z2,rest)) [0 0] [0 0] [0] [0] ?1(pair(z1,z2),x,y,rest) = [1 0]x + [0 2]z1 + [3] >= [0] = cons(z1,cons(z2,rest)) [0] [0 0] [0] cons(x,cons(y,rest)) = [0] >= [1 2]x + [1] = ?1(orient(x,y),x,y,rest) [0] [0] cons(x,cons(x,rest)) = [0] >= [0] = cons(x,rest) [1 1] [0 0] [0] [0 0] [0] ?2(pair(z1,z2),x,y) = [0 0]x + [0 3]z1 + [3] >= [0 3]z1 + [2] = pair(s(z1),s(z2)) [2 2] [2 2] [0] [1 1] orient(s(x),s(y)) = [0 3]x + [0 0]y + [1] >= [0 3]x = ?2(orient(x,y),x,y) [2 2] [2] [0] orient(s(x),0()) = [0 3]x + [1] >= [1] = pair(0(),s(x)) problem: DPs: cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) TRS: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) Restore Modifier: DPs: cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) TRS: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) EDG Processor: DPs: cons#(x,cons(y,rest)) -> ?1#(orient(x,y),x,y,rest) TRS: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) graph: Qed DPs: orient#(s(x),s(y)) -> orient#(x,y) TRS: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) Subterm Criterion Processor: simple projection: pi(orient#) = 0 problem: DPs: TRS: ?1(pair(z1,z2),x,y,rest) -> cons(z1,cons(z2,rest)) cons(x,cons(y,rest)) -> ?1(orient(x,y),x,y,rest) cons(x,cons(x,rest)) -> cons(x,rest) ?2(pair(z1,z2),x,y) -> pair(s(z1),s(z2)) orient(s(x),s(y)) -> ?2(orient(x,y),x,y) orient(s(x),0()) -> pair(0(),s(x)) Qed