[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 18 from proof abs-reduce0 (previous step)

# pebs = # apebs, pebs[n0] = mkpeb(buf3, m3, boolvar3), apebs[n] = mkpeb(aehdr0, avhdr0, buf0, m0, boolvar0), pebs[n] = mkpeb(buf1, m1, boolvar1), n < # apebs, n0 < # apebs, ubi-io-inv(apebs), (boolvar2 ↔ boolvar0) ∧ ( ¬ boolvar0 → m2 = (aehdr0 = empty ⊃ 0;(avhdr0 = empty ⊃ EB_PAGE_SIZE;m0 + 2 * EB_PAGE_SIZE)) ∧ (aehdr0 = empty → subarray(buf2, 0, EB_PAGE_SIZE) = emptypage) ∧ (aehdr0.valid? → is-encoded(echdr(aehdr0.ec), subarray(buf2, 0, EB_PAGE_SIZE))) ∧ (aehdr0 = garbage → is-garbage-ec(subarray(buf2, 0, EB_PAGE_SIZE)) ∧ subarray(buf2, 0, EB_PAGE_SIZE) ≠ emptypage) ∧ (avhdr0 = empty → subarray(buf2, EB_PAGE_SIZE, EB_PAGE_SIZE) = emptypage) ∧ ( avhdr0.valid? → is-encoded(vidhdr(avhdr0.vol, avhdr0.leb, avhdr0.sqn, avhdr0.size, avhdr0.checksum), subarray(buf2, EB_PAGE_SIZE, EB_PAGE_SIZE))) ∧ (avhdr0 = garbage → is-garbage-vid(subarray(buf2, EB_PAGE_SIZE, EB_PAGE_SIZE)) ∧ subarray(buf2, EB_PAGE_SIZE, EB_PAGE_SIZE) ≠ emptypage) ∧ subarray(buf2, 2 * EB_PAGE_SIZE, LEB_SIZE) = buf0) → (boolvar1 ↔ boolvar) ∧ ( ¬ boolvar → m1 = (aehdr = empty ⊃ 0;(avhdr = empty ⊃ EB_PAGE_SIZE;m + 2 * EB_PAGE_SIZE)) ∧ (aehdr = empty → subarray(buf1, 0, EB_PAGE_SIZE) = emptypage) ∧ (aehdr.valid? → is-encoded(echdr(aehdr.ec), subarray(buf1, 0, EB_PAGE_SIZE))) ∧ (aehdr = garbage → is-garbage-ec(subarray(buf1, 0, EB_PAGE_SIZE)) ∧ subarray(buf1, 0, EB_PAGE_SIZE) ≠ emptypage) ∧ (avhdr = empty → subarray(buf1, EB_PAGE_SIZE, EB_PAGE_SIZE) = emptypage) ∧ (avhdr.valid? → is-encoded(vidhdr(avhdr.vol, avhdr.leb, avhdr.sqn, avhdr.size, avhdr.checksum), subarray(buf1, EB_PAGE_SIZE, EB_PAGE_SIZE))) ∧ (avhdr = garbage → is-garbage-vid(subarray(buf1, EB_PAGE_SIZE, EB_PAGE_SIZE)) ∧ subarray(buf1, EB_PAGE_SIZE, EB_PAGE_SIZE) ≠ emptypage) ∧ subarray(buf1, 2 * EB_PAGE_SIZE, LEB_SIZE) = buf), ∀ n0. n0 < # apebs → (pebs[n, mkpeb(buf2, m2, boolvar2)][n0].bad ↔ apebs[n0].bad) ∧ ( ¬ pebs[n, mkpeb(buf2, m2, boolvar2)][n0].bad → pebs[n, mkpeb(buf2, m2, boolvar2)][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[n, mkpeb(buf2, m2, boolvar2)][n0].data, 0, EB_PAGE_SIZE) = emptypage) ∧ (apebs[n0].echdr.valid? → is-encoded(echdr(apebs[n0].echdr.ec), subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, 0, EB_PAGE_SIZE))) ∧ ( apebs[n0].echdr = garbage → is-garbage-ec(subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, 0, EB_PAGE_SIZE)) ∧ subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, 0, EB_PAGE_SIZE) ≠ emptypage) ∧ (apebs[n0].vidhdr = empty → subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][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[n, mkpeb(buf2, m2, boolvar2)][n0].data, EB_PAGE_SIZE, EB_PAGE_SIZE))) ∧ ( apebs[n0].vidhdr = garbage → is-garbage-vid(subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, EB_PAGE_SIZE, EB_PAGE_SIZE)) ∧ subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, EB_PAGE_SIZE, EB_PAGE_SIZE) ≠ emptypage) ∧ subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, 2 * EB_PAGE_SIZE, LEB_SIZE) = apebs[n0].data) ⊦ (boolvar3 ↔ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].bad) ∧ ( ¬ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].bad → m3 = (apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].echdr = empty ⊃ 0 ;(apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr = empty ⊃ EB_PAGE_SIZE ;apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill + 2 * EB_PAGE_SIZE ) ) ∧ (apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].echdr = empty → subarray(buf3, 0, EB_PAGE_SIZE) = emptypage) ∧ ( apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].echdr.valid? → is-encoded(echdr(apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].echdr.ec), subarray(buf3, 0, EB_PAGE_SIZE))) ∧ ( apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].echdr = garbage → is-garbage-ec(subarray(buf3, 0, EB_PAGE_SIZE)) ∧ subarray(buf3, 0, EB_PAGE_SIZE) ≠ emptypage) ∧ (apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr = empty → subarray(buf3, EB_PAGE_SIZE, EB_PAGE_SIZE) = emptypage) ∧ ( apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr.valid? → is-encoded (vidhdr (apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr.vol, apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr.leb, apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr.sqn, apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr.size, apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr.checksum), subarray(buf3, EB_PAGE_SIZE, EB_PAGE_SIZE))) ∧ ( apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr = garbage → is-garbage-vid(subarray(buf3, EB_PAGE_SIZE, EB_PAGE_SIZE)) ∧ subarray(buf3, EB_PAGE_SIZE, EB_PAGE_SIZE) ≠ emptypage) ∧ subarray(buf3, 2 * EB_PAGE_SIZE, LEB_SIZE) = apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].data)

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 19:
# pebs = # apebs, pebs[n] = mkpeb(buf1, m1, boolvar1), apebs[n] = mkpeb(aehdr0, avhdr0, buf0, m0, boolvar0), pebs[n0] = mkpeb(buf3, m3, boolvar3), apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0] = mkpeb(aehdr1, avhdr1, buf4, m4, boolvar4), n0 < # apebs, n < # apebs, ubi-io-inv(apebs), (boolvar2 ↔ boolvar0) ∧ ( ¬ boolvar0 → m2 = (aehdr0 = empty ⊃ 0;(avhdr0 = empty ⊃ EB_PAGE_SIZE;m0 + 2 * EB_PAGE_SIZE)) ∧ (aehdr0 = empty → subarray(buf2, 0, EB_PAGE_SIZE) = emptypage) ∧ (aehdr0.valid? → is-encoded(echdr(aehdr0.ec), subarray(buf2, 0, EB_PAGE_SIZE))) ∧ (aehdr0 = garbage → is-garbage-ec(subarray(buf2, 0, EB_PAGE_SIZE)) ∧ subarray(buf2, 0, EB_PAGE_SIZE) ≠ emptypage) ∧ (avhdr0 = empty → subarray(buf2, EB_PAGE_SIZE, EB_PAGE_SIZE) = emptypage) ∧ ( avhdr0.valid? → is-encoded(vidhdr(avhdr0.vol, avhdr0.leb, avhdr0.sqn, avhdr0.size, avhdr0.checksum), subarray(buf2, EB_PAGE_SIZE, EB_PAGE_SIZE))) ∧ (avhdr0 = garbage → is-garbage-vid(subarray(buf2, EB_PAGE_SIZE, EB_PAGE_SIZE)) ∧ subarray(buf2, EB_PAGE_SIZE, EB_PAGE_SIZE) ≠ emptypage) ∧ subarray(buf2, 2 * EB_PAGE_SIZE, LEB_SIZE) = buf0) → (boolvar1 ↔ boolvar) ∧ ( ¬ boolvar → m1 = (aehdr = empty ⊃ 0;(avhdr = empty ⊃ EB_PAGE_SIZE;m + 2 * EB_PAGE_SIZE)) ∧ (aehdr = empty → subarray(buf1, 0, EB_PAGE_SIZE) = emptypage) ∧ (aehdr.valid? → is-encoded(echdr(aehdr.ec), subarray(buf1, 0, EB_PAGE_SIZE))) ∧ (aehdr = garbage → is-garbage-ec(subarray(buf1, 0, EB_PAGE_SIZE)) ∧ subarray(buf1, 0, EB_PAGE_SIZE) ≠ emptypage) ∧ (avhdr = empty → subarray(buf1, EB_PAGE_SIZE, EB_PAGE_SIZE) = emptypage) ∧ (avhdr.valid? → is-encoded(vidhdr(avhdr.vol, avhdr.leb, avhdr.sqn, avhdr.size, avhdr.checksum), subarray(buf1, EB_PAGE_SIZE, EB_PAGE_SIZE))) ∧ (avhdr = garbage → is-garbage-vid(subarray(buf1, EB_PAGE_SIZE, EB_PAGE_SIZE)) ∧ subarray(buf1, EB_PAGE_SIZE, EB_PAGE_SIZE) ≠ emptypage) ∧ subarray(buf1, 2 * EB_PAGE_SIZE, LEB_SIZE) = buf), ∀ n0. n0 < # apebs → (pebs[n, mkpeb(buf2, m2, boolvar2)][n0].bad ↔ apebs[n0].bad) ∧ ( ¬ pebs[n, mkpeb(buf2, m2, boolvar2)][n0].bad → pebs[n, mkpeb(buf2, m2, boolvar2)][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[n, mkpeb(buf2, m2, boolvar2)][n0].data, 0, EB_PAGE_SIZE) = emptypage) ∧ (apebs[n0].echdr.valid? → is-encoded(echdr(apebs[n0].echdr.ec), subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, 0, EB_PAGE_SIZE))) ∧ ( apebs[n0].echdr = garbage → is-garbage-ec(subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, 0, EB_PAGE_SIZE)) ∧ subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, 0, EB_PAGE_SIZE) ≠ emptypage) ∧ (apebs[n0].vidhdr = empty → subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][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[n, mkpeb(buf2, m2, boolvar2)][n0].data, EB_PAGE_SIZE, EB_PAGE_SIZE))) ∧ ( apebs[n0].vidhdr = garbage → is-garbage-vid(subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, EB_PAGE_SIZE, EB_PAGE_SIZE)) ∧ subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, EB_PAGE_SIZE, EB_PAGE_SIZE) ≠ emptypage) ∧ subarray(pebs[n, mkpeb(buf2, m2, boolvar2)][n0].data, 2 * EB_PAGE_SIZE, LEB_SIZE) = apebs[n0].data) ⊦ (boolvar3 ↔ boolvar4) ∧ ( ¬ boolvar4 → m3 = (aehdr1 = empty ⊃ 0;(avhdr1 = empty ⊃ EB_PAGE_SIZE;m4 + 2 * EB_PAGE_SIZE)) ∧ (aehdr1 = empty → subarray(buf3, 0, EB_PAGE_SIZE) = emptypage) ∧ (aehdr1.valid? → is-encoded(echdr(aehdr1.ec), subarray(buf3, 0, EB_PAGE_SIZE))) ∧ (aehdr1 = garbage → is-garbage-ec(subarray(buf3, 0, EB_PAGE_SIZE)) ∧ subarray(buf3, 0, EB_PAGE_SIZE) ≠ emptypage) ∧ (avhdr1 = empty → subarray(buf3, EB_PAGE_SIZE, EB_PAGE_SIZE) = emptypage) ∧ ( avhdr1.valid? → is-encoded(vidhdr(avhdr1.vol, avhdr1.leb, avhdr1.sqn, avhdr1.size, avhdr1.checksum), subarray(buf3, EB_PAGE_SIZE, EB_PAGE_SIZE))) ∧ (avhdr1 = garbage → is-garbage-vid(subarray(buf3, EB_PAGE_SIZE, EB_PAGE_SIZE)) ∧ subarray(buf3, EB_PAGE_SIZE, EB_PAGE_SIZE) ≠ emptypage) ∧ subarray(buf3, 2 * EB_PAGE_SIZE, LEB_SIZE) = buf4)

Rule argument

spec: apeb name: elim seq: ⊦ ( ( (aehdr = apeb.echdr ∧ avhdr = apeb.vidhdr) ∧ buf = apeb.data) ∧ m = apeb.fill) ∧ (boolvar ↔ apeb.bad) ↔ apeb = mkpeb(aehdr, avhdr, buf, m, boolvar) subst: [apeb, aehdr, avhdr, buf, m, boolvar] → [apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0], aehdr1, avhdr1, buf4, m4, boolvar4]

Additional information

Used simplifier rules: ⊦ ( ((aehdr = apeb.echdr ∧ avhdr = apeb.vidhdr) ∧ buf = apeb.data) ∧ m = apeb.fill) ∧ (boolvar ↔ apeb.bad) ↔ apeb = mkpeb(aehdr, avhdr, buf, m, boolvar); (elim) Used terms: apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0], aehdr1, avhdr1, buf4, m4, boolvar4