Proof step 12 from proof keys-shift-left (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 13:

  nused < # zbrar, n < # zbrar, sorted(zbrar, 0, nused + 1), n ≤ nused, ∃ n0. n0 < nused ∧ (n0 < n ⊃ zbrar[n0];zbrar[n0 + 1]).key = key ⊦ key ≠ zbrar[n].key ∧ (∃ n0. ¬ nused < n0 ∧ zbrar[n0].key = key)

• Proof step 30:

  nused < # zbrar, n < # zbrar, sorted(zbrar, 0, nused + 1), n ≤ nused, ∃ n0. ¬ nused < n0 ∧ zbrar[n0].key = key ⊦ key = zbrar[n].key, ∃ n0. n0 < nused ∧ (n0 < n ⊃ zbrar[n0];zbrar[n0 + 1]).key = key

Rule argument

Additional information