[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 24 from proof abs-reduce0 (previous step)

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

Heuristic weak cut applied rule cut formula

And closed the goal!

Rule argument

fma: n0 = n

Additional information

Used simplifier rules: ⊦ m ≠ n → apebs[n, apeb][m] = apebs[m]; (s)% ⊦ m ≠ n → pebs[n, peb][m] = pebs[m]; (s)%⊦ mkpeb(buf, m, boolvar) = mkpeb(buf0, m0, boolvar0) ↔ buf = buf0 ∧ m = m0 ∧ (boolvar ↔ boolvar0); (ws)%⊦ mkpeb(aehdr, avhdr, buf, m, boolvar) = mkpeb(aehdr0, avhdr0, buf0, m0, boolvar0) ↔ aehdr = aehdr0 ∧ avhdr = avhdr0 ∧ buf = buf0 ∧ m = m0 ∧ (boolvar ↔ boolvar0); (s)% ⊦ m < # apebs → apebs[m, apeb][m] = apeb; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)%m < # pebs ⊦ pebs[m, peb][m] = peb; (s) Used formulas: n0 = n