Proof step 10 from proof key-range-replace-branches (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 11:

  # zbrar0 = # zbrar1, n + 1 = m, n < m, n < # zbrar1, m ≤ # zbrar1, ∀ n0. n0 ≤ n ∧ n0 ≤ m → zbrar0[n0].key = zbrar1[n0].key ⊦ n = 0, ri |> zbrar0[n - 1].key = (n + 1 = m ⊃ ri |> zbrar1[n - 1].key;(ri |> zbrar1[n - 1].key) |≤ zbrar1[n].key)

• Proof step 15:

  # zbrar0 = # zbrar1, n < m, n < # zbrar1, m ≤ # zbrar1, ∀ n0. n0 ≤ n ∧ n0 ≤ m → zbrar0[n0].key = zbrar1[n0].key ⊦ n + 1 = m, n = 0, (ri |> zbrar0[n - 1].key) |≤ zbrar0[n].key = (n + 1 = m ⊃ ri |> zbrar1[n - 1].key;(ri |> zbrar1[n - 1].key) |≤ zbrar1[n].key)

Rule argument

Additional information