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

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

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