MAYBE Time: 0.003939 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: DP: {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)} 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)} 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 (2): Scc: {gr#(s x, s y) -> gr#(x, y)} Scc: {cond#(true(), x, y) -> cond#(gr(x, y), y, x)} SCC (1): 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#) = 1 Strict: {} Qed SCC (1): 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