YES Time: 0.000774 TRS: { admit(x, nil()) -> nil(), admit(x, .(u, .(v, .(w(), z)))) -> cond(=(sum(x, u, v), w()), .(u, .(v, .(w(), admit(carry(x, u, v), z))))), cond(true(), y) -> y} DP: DP: {admit#(x, .(u, .(v, .(w(), z)))) -> admit#(carry(x, u, v), z), admit#(x, .(u, .(v, .(w(), z)))) -> cond#(=(sum(x, u, v), w()), .(u, .(v, .(w(), admit(carry(x, u, v), z)))))} TRS: { admit(x, nil()) -> nil(), admit(x, .(u, .(v, .(w(), z)))) -> cond(=(sum(x, u, v), w()), .(u, .(v, .(w(), admit(carry(x, u, v), z))))), cond(true(), y) -> y} EDG: {(admit#(x, .(u, .(v, .(w(), z)))) -> admit#(carry(x, u, v), z), admit#(x, .(u, .(v, .(w(), z)))) -> admit#(carry(x, u, v), z)) (admit#(x, .(u, .(v, .(w(), z)))) -> admit#(carry(x, u, v), z), admit#(x, .(u, .(v, .(w(), z)))) -> cond#(=(sum(x, u, v), w()), .(u, .(v, .(w(), admit(carry(x, u, v), z))))))} SCCS (1): Scc: {admit#(x, .(u, .(v, .(w(), z)))) -> admit#(carry(x, u, v), z)} SCC (1): Strict: {admit#(x, .(u, .(v, .(w(), z)))) -> admit#(carry(x, u, v), z)} Weak: { admit(x, nil()) -> nil(), admit(x, .(u, .(v, .(w(), z)))) -> cond(=(sum(x, u, v), w()), .(u, .(v, .(w(), admit(carry(x, u, v), z))))), cond(true(), y) -> y} SPSC: Simple Projection: pi(admit#) = 1 Strict: {} Qed