YES Time: 0.065521 TRS: { eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} DP: DP: { eq#(s x, s y) -> eq#(x, y), le#(s x, s y) -> le#(x, y), app#(add(n, x), y) -> app#(x, y), min# add(n, add(m, x)) -> le#(n, m), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min# add(n, x), if_min#(false(), add(n, add(m, x))) -> min# add(m, x), rm#(n, add(m, x)) -> eq#(n, m), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x), if_rm#(false(), n, add(m, x)) -> rm#(n, x), minsort#(add(n, x), y) -> eq#(n, min add(n, x)), minsort#(add(n, x), y) -> min# add(n, x), minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y), if_minsort#(true(), add(n, x), y) -> rm#(n, x), if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))} TRS: { eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} EDG: {(if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y)) (if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> min# add(n, x)) (if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> eq#(n, min add(n, x))) (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y)) (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> min# add(n, x)) (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> eq#(n, min add(n, x))) (min# add(n, add(m, x)) -> le#(n, m), le#(s x, s y) -> le#(x, y)) (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))) (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil())) (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> rm#(n, x)) (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y)) (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y)) (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x))) (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m)) (if_minsort#(true(), add(n, x), y) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x))) (if_minsort#(true(), add(n, x), y) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m)) (if_min#(true(), add(n, add(m, x))) -> min# add(n, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x)))) (if_min#(true(), add(n, add(m, x))) -> min# add(n, x), min# add(n, add(m, x)) -> le#(n, m)) (minsort#(add(n, x), y) -> min# add(n, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x)))) (minsort#(add(n, x), y) -> min# add(n, x), min# add(n, add(m, x)) -> le#(n, m)) (if_min#(false(), add(n, add(m, x))) -> min# add(m, x), min# add(n, add(m, x)) -> le#(n, m)) (if_min#(false(), add(n, add(m, x))) -> min# add(m, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x)))) (min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min# add(n, x)) (min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(false(), add(n, add(m, x))) -> min# add(m, x)) (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m)) (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x))) (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y)) (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y)) (rm#(n, add(m, x)) -> eq#(n, m), eq#(s x, s y) -> eq#(x, y)) (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x)) (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(false(), n, add(m, x)) -> rm#(n, x)) (minsort#(add(n, x), y) -> eq#(n, min add(n, x)), eq#(s x, s y) -> eq#(x, y)) (if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y), app#(add(n, x), y) -> app#(x, y))} SCCS (6): Scc: { minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))} Scc: { rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x), if_rm#(false(), n, add(m, x)) -> rm#(n, x)} Scc: { min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min# add(n, x), if_min#(false(), add(n, add(m, x))) -> min# add(m, x)} Scc: {app#(add(n, x), y) -> app#(x, y)} Scc: {le#(s x, s y) -> le#(x, y)} Scc: {eq#(s x, s y) -> eq#(x, y)} SCC (3): Strict: { minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_rm](x0, x1, x2) = x0, [if_minsort](x0, x1, x2) = 0, [eq](x0, x1) = 0, [le](x0, x1) = 0, [app](x0, x1) = x0 + x1, [add](x0, x1) = x0 + 1, [if_min](x0, x1) = 0, [rm](x0, x1) = x0, [minsort](x0, x1) = 0, [s](x0) = 0, [min](x0) = 0, [true] = 0, [0] = 0, [false] = 0, [nil] = 0, [if_minsort#](x0, x1, x2) = x0 + x1 + 1, [minsort#](x0, x1) = x0 + x1 + 1 Strict: if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)) 2 + 1x + 1y + 0n >= 2 + 1x + 1y + 0n if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()) 2 + 1x + 1y + 0n >= 1 + 1x + 1y + 0n minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y) 2 + 1x + 1y + 0n >= 2 + 1x + 1y + 0n Weak: EDG: {(minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))) (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y))} SCCS (1): Scc: { minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))} SCC (2): Strict: { minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} SPSC: Simple Projection: pi(if_minsort#) = 1, pi(minsort#) = 0 Strict: {minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y)} EDG: {} SCCS (0): Qed SCC (3): Strict: { rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x), if_rm#(false(), n, add(m, x)) -> rm#(n, x)} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} SPSC: Simple Projection: pi(if_rm#) = 2, pi(rm#) = 1 Strict: { rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x)} EDG: {(if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x))) (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x))} SCCS (1): Scc: { rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x)} SCC (2): Strict: { rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x)} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} SPSC: Simple Projection: pi(if_rm#) = 2, pi(rm#) = 1 Strict: {rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x))} EDG: {} SCCS (0): Qed SCC (3): Strict: { min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min# add(n, x), if_min#(false(), add(n, add(m, x))) -> min# add(m, x)} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_rm](x0, x1, x2) = x0 + x1, [if_minsort](x0, x1, x2) = x0 + x1, [eq](x0, x1) = x0 + x1, [le](x0, x1) = 0, [app](x0, x1) = 0, [add](x0, x1) = x0 + 1, [if_min](x0, x1) = 0, [rm](x0, x1) = 0, [minsort](x0, x1) = x0, [s](x0) = 0, [min](x0) = x0 + 1, [true] = 0, [0] = 0, [false] = 0, [nil] = 0, [if_min#](x0, x1) = x0, [min#](x0) = x0 Strict: if_min#(false(), add(n, add(m, x))) -> min# add(m, x) 2 + 1x + 0n + 0m >= 1 + 1x + 0m if_min#(true(), add(n, add(m, x))) -> min# add(n, x) 2 + 1x + 0n + 0m >= 1 + 1x + 0n min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))) 2 + 1x + 0n + 0m >= 2 + 1x + 0n + 0m Weak: EDG: {} SCCS (0): Qed SCC (1): Strict: {app#(add(n, x), y) -> app#(x, y)} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} SPSC: Simple Projection: pi(app#) = 0 Strict: {} Qed SCC (1): Strict: {le#(s x, s y) -> le#(x, y)} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} SPSC: Simple Projection: pi(le#) = 1 Strict: {} Qed SCC (1): Strict: {eq#(s x, s y) -> eq#(x, y)} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} SPSC: Simple Projection: pi(eq#) = 1 Strict: {} Qed