Proof step 2 from proof abs-size-apebs0 (previous step)

Heuristic simplifier applied rule simplifier

And closed the goal!

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-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);%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);% ⊦ m < n → ¬ n < m; (s)%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)% ⊦ ¬ n < n; (s)% ⊦ m < n → n ≠ 0; (s)%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic