Proof step 3 from proof in-playload-data (previous step)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

  sorted(zbrar, 0, n + 0), n + 0 ≤ # zbrar ⊦ adr ∈ payload(zbrar, n, 0) ↔ (∃ m0. n ≤ m0 ∧ m0 < n + 0 ∧ zbrar[m0].entry? ∧ zbrar[m0].adr = adr)

• Proof step 7:

  sorted(zbrar, 0, n + m0 +1), n + m0 +1 ≤ # zbrar, ∀ zbrar, n, adr. sorted(zbrar, 0, n + m0) ∧ n + m0 ≤ # zbrar → (adr ∈ payload(zbrar, n, m0) ↔ (∃ m1. n ≤ m1 ∧ m1 < n + m0 ∧ zbrar[m1].entry? ∧ zbrar[m1].adr = adr)) ⊦ adr ∈ payload(zbrar, n, m0 +1) ↔ (∃ m1. n ≤ m1 ∧ m1 < n + m0 +1 ∧ zbrar[m1].entry? ∧ zbrar[m1].adr = adr)

Rule argument

Additional information

Used simplifier rules: nat freely generated by 0, +1;;