MAYBE TRS: {cond(true(), x, y) -> cond(gr(x, y), y, x), gr(0(), x) -> false(), gr(s(x), 0()) -> true(), gr(s(x), s(y)) -> gr(x, y)} DP: Strict: {cond#(true(), x, y) -> cond#(gr(x, y), y, x), cond#(true(), x, y) -> gr#(x, y), gr#(s(x), s(y)) -> gr#(x, y)} Weak: {cond(true(), x, y) -> cond(gr(x, y), y, x), gr(0(), x) -> false(), gr(s(x), 0()) -> true(), gr(s(x), s(y)) -> gr(x, y)} EDG: {(gr#(s(x), s(y)) -> gr#(x, y), gr#(s(x), s(y)) -> gr#(x, y)) (cond#(true(), x, y) -> cond#(gr(x, y), y, x), cond#(true(), x, y) -> cond#(gr(x, y), y, x)) (cond#(true(), x, y) -> cond#(gr(x, y), y, x), cond#(true(), x, y) -> gr#(x, y)) (cond#(true(), x, y) -> gr#(x, y), gr#(s(x), s(y)) -> gr#(x, y))} SCCS: Scc: {gr#(s(x), s(y)) -> gr#(x, y)} Scc: {cond#(true(), x, y) -> cond#(gr(x, y), y, x)} SCC: Strict: {gr#(s(x), s(y)) -> gr#(x, y)} Weak: {cond(true(), x, y) -> cond(gr(x, y), y, x), gr(0(), x) -> false(), gr(s(x), 0()) -> true(), gr(s(x), s(y)) -> gr(x, y)} SPSC: Simple Projection: pi(gr#) = 0 Strict: {} Qed SCC: Strict: {cond#(true(), x, y) -> cond#(gr(x, y), y, x)} Weak: {cond(true(), x, y) -> cond(gr(x, y), y, x), gr(0(), x) -> false(), gr(s(x), 0()) -> true(), gr(s(x), s(y)) -> gr(x, y)} Fail