proof - 次のアルゴリズムの正しさを証明するにはどうすればよいですか?

Question

リスト x,y をパラメーターとして取り、x と y の結合で z 番目に小さい要素を返す次のアルゴリズム min を考えてみましょう。前提条件: X と Y は昇順で並べ替えられた int のリストであり、互いに素です。

疑似コードであるため、インデックス付けは 0 ではなく 1 で始まることに注意してください。

Min(x,y,z):
    if z = 1:
        return(min(x[1]; y[1]))
    if z = 2:
        if x[1] < y[1]:
            return(min(x[2],y[1]))
        else:
            return(min(x[1], y[2]))

q = Ceiling(z/2) //round up z/2

if x[q] < y[z-q + 1]:
    return(Min(x[q:z], y[1:(z - q + 1)], (z-q +1)))
else:
    return(Min(x[1:q], B[(z -q + 1):z], q))

z が 2 ずつ減少し続け、最終的に基本ケースの 1 つに到達するため、終了することを証明できますが、部分的な正確性を証明することはできません。