Proof step 2 from proof abs-fwd (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # pebs = # apebs, n < # apebs, ∀ n0. n0 < # apebs → (pebs[n0].bad ↔ apebs[n0].bad) ∧ ( ¬ pebs[n0].bad → pebs[n0].fill = (apebs[n0].echdr = empty ⊃ 0;(apebs[n0].vidhdr = empty ⊃ EB_PAGE_SIZE;apebs[n0].fill + 2 * EB_PAGE_SIZE)) ∧ (apebs[n0].echdr = empty → subarray(pebs[n0].data, 0, EB_PAGE_SIZE) = emptypage) ∧ (apebs[n0].echdr.valid? → is-encoded(echdr(apebs[n0].echdr.ec), subarray(pebs[n0].data, 0, EB_PAGE_SIZE))) ∧ (apebs[n0].echdr = garbage → is-garbage-ec(subarray(pebs[n0].data, 0, EB_PAGE_SIZE)) ∧ subarray(pebs[n0].data, 0, EB_PAGE_SIZE) ≠ emptypage) ∧ (apebs[n0].vidhdr = empty → subarray(pebs[n0].data, EB_PAGE_SIZE, EB_PAGE_SIZE) = emptypage) ∧ ( apebs[n0].vidhdr.valid? → is-encoded (vidhdr(apebs[n0].vidhdr.vol, apebs[n0].vidhdr.leb, apebs[n0].vidhdr.sqn, apebs[n0].vidhdr.size, apebs[n0].vidhdr.checksum), subarray(pebs[n0].data, EB_PAGE_SIZE, EB_PAGE_SIZE))) ∧ ( apebs[n0].vidhdr = garbage → is-garbage-vid(subarray(pebs[n0].data, EB_PAGE_SIZE, EB_PAGE_SIZE)) ∧ subarray(pebs[n0].data, EB_PAGE_SIZE, EB_PAGE_SIZE) ≠ emptypage) ∧ subarray(pebs[n0].data, 2 * EB_PAGE_SIZE, LEB_SIZE) = apebs[n0].data) ⊦ (pebs[n].bad ↔ apebs[n].bad) ∧ ( ¬ pebs[n].bad → pebs[n].fill = (apebs[n].echdr = empty ⊃ 0;(apebs[n].vidhdr = empty ⊃ EB_PAGE_SIZE;apebs[n].fill + 2 * EB_PAGE_SIZE)) ∧ (apebs[n].echdr = empty → subarray(pebs[n].data, 0, EB_PAGE_SIZE) = emptypage) ∧ (apebs[n].echdr.valid? → is-encoded(echdr(apebs[n].echdr.ec), subarray(pebs[n].data, 0, EB_PAGE_SIZE))) ∧ (apebs[n].echdr = garbage → is-garbage-ec(subarray(pebs[n].data, 0, EB_PAGE_SIZE)) ∧ subarray(pebs[n].data, 0, EB_PAGE_SIZE) ≠ emptypage) ∧ (apebs[n].vidhdr = empty → subarray(pebs[n].data, EB_PAGE_SIZE, EB_PAGE_SIZE) = emptypage) ∧ ( apebs[n].vidhdr.valid? → is-encoded (vidhdr(apebs[n].vidhdr.vol, apebs[n].vidhdr.leb, apebs[n].vidhdr.sqn, apebs[n].vidhdr.size, apebs[n].vidhdr.checksum), subarray(pebs[n].data, EB_PAGE_SIZE, EB_PAGE_SIZE))) ∧ ( apebs[n].vidhdr = garbage → is-garbage-vid(subarray(pebs[n].data, EB_PAGE_SIZE, EB_PAGE_SIZE)) ∧ subarray(pebs[n].data, EB_PAGE_SIZE, EB_PAGE_SIZE) ≠ emptypage) ∧ subarray(pebs[n].data, 2 * EB_PAGE_SIZE, LEB_SIZE) = apebs[n].data)

Rule argument

Additional information

Used simplifier rules: abs: ⊦ abs(pebs, apebs) ↔ # pebs = # apebs ∧ (∀ n. n < # pebs → abs-peb(pebs[n], apebs[n]));%abs-peb: ⊦ abs-peb(peb, apeb) ↔ (peb.bad ↔ apeb.bad) ∧ ( ¬ peb.bad → peb.fill = (apeb.echdr = empty ⊃ 0 ;(apeb.vidhdr = empty ⊃ EB_PAGE_SIZE ;apeb.fill + 2 * EB_PAGE_SIZE ) ) ∧ abs-echdr(subarray(peb.data, 0, EB_PAGE_SIZE), apeb.echdr) ∧ abs-vidhdr (subarray(peb.data, EB_PAGE_SIZE, EB_PAGE_SIZE), apeb.vidhdr) ∧ subarray(peb.data, 2 * EB_PAGE_SIZE, LEB_SIZE) = apeb.data);%abs-echdr: ⊦ abs-echdr(buf, aehdr) ↔ (aehdr = empty → buf = emptypage) ∧ (aehdr.valid? → is-encoded(echdr(aehdr.ec), buf)) ∧ (aehdr = garbage → is-garbage-ec(buf) ∧ buf ≠ emptypage);%abs-vidhdr: ⊦ abs-vidhdr(buf, avhdr) ↔ (avhdr = empty → buf = emptypage) ∧ ( avhdr.valid? → is-encoded (vidhdr (avhdr.vol, avhdr.leb, avhdr.sqn, avhdr.size, avhdr.checksum), buf)) ∧ (avhdr = garbage → is-garbage-vid(buf) ∧ buf ≠ emptypage);% ⊦ m < n → n ≠ 0; (s)%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic