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

apebs[n] = mkpeb(aehdr0, avhdr0, buf0, m0, boolvar0), n < # apebs ∧ # buf0 = LEB_SIZE ∧ ( ¬ boolvar0 → (aehdr0 = empty → avhdr0 = empty) ∧ (aehdr0 ≠ garbage ∧ avhdr0 = empty → m0 = 0) ∧ m0 ≤ LEB_SIZE ∧ is-aligned(m0, EB_PAGE_SIZE) ∧ subarray(buf0, m0, LEB_SIZE - m0) = mkempbuf(LEB_SIZE - m0)) ∧ (¬ boolvar0 → aehdr0.valid? ∧ avhdr0 = empty) → # buf = LEB_SIZE ∧ ( ¬ boolvar → (aehdr = empty → avhdr = empty) ∧ (aehdr ≠ garbage ∧ avhdr = empty → m = 0) ∧ m ≤ LEB_SIZE ∧ is-aligned(m, EB_PAGE_SIZE) ∧ subarray(buf, m, LEB_SIZE - m) = mkempbuf(LEB_SIZE - m)) ∧ (¬ boolvar → aehdr.valid? ∧ avhdr = empty), ∀ n0. n0 < # apebs → # apebs[n0].data = LEB_SIZE ∧ ( ¬ apebs[n0].bad → (apebs[n0].echdr = empty → apebs[n0].vidhdr = empty) ∧ (apebs[n0].echdr ≠ garbage ∧ apebs[n0].vidhdr = empty → apebs[n0].fill = 0) ∧ apebs[n0].fill ≤ LEB_SIZE ∧ is-aligned(apebs[n0].fill, EB_PAGE_SIZE) ∧ subarray(apebs[n0].data, apebs[n0].fill, LEB_SIZE - apebs[n0].fill) = mkempbuf(LEB_SIZE - apebs[n0].fill)) ∧ (¬ apebs[n0].bad → apebs[n0].echdr.valid? ∧ apebs[n0].vidhdr = empty) ⊦ ∀ n0. n0 < # apebs → # apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].data = LEB_SIZE ∧ ( ¬ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].bad → (apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].echdr = empty → apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr = empty) ∧ ( apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].echdr ≠ garbage ∧ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr = empty → apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill = 0) ∧ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill ≤ LEB_SIZE ∧ is-aligned(apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill, EB_PAGE_SIZE) ∧ subarray (apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].data, apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill, LEB_SIZE - apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill) = mkempbuf(LEB_SIZE - apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill)) ∧ ( ¬ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].bad → apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].echdr.valid? ∧ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr = empty)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 12:
apebs[n] = mkpeb(aehdr0, avhdr0, buf0, m0, boolvar0), n0 < # apebs, n < # apebs ∧ # buf0 = LEB_SIZE ∧ ( ¬ boolvar0 → (aehdr0 = empty → avhdr0 = empty) ∧ (aehdr0 ≠ garbage ∧ avhdr0 = empty → m0 = 0) ∧ m0 ≤ LEB_SIZE ∧ is-aligned(m0, EB_PAGE_SIZE) ∧ subarray(buf0, m0, LEB_SIZE - m0) = mkempbuf(LEB_SIZE - m0)) ∧ (¬ boolvar0 → aehdr0.valid? ∧ avhdr0 = empty) → # buf = LEB_SIZE ∧ ( ¬ boolvar → (aehdr = empty → avhdr = empty) ∧ (aehdr ≠ garbage ∧ avhdr = empty → m = 0) ∧ m ≤ LEB_SIZE ∧ is-aligned(m, EB_PAGE_SIZE) ∧ subarray(buf, m, LEB_SIZE - m) = mkempbuf(LEB_SIZE - m)) ∧ (¬ boolvar → aehdr.valid? ∧ avhdr = empty), ∀ n0. n0 < # apebs → # apebs[n0].data = LEB_SIZE ∧ ( ¬ apebs[n0].bad → (apebs[n0].echdr = empty → apebs[n0].vidhdr = empty) ∧ (apebs[n0].echdr ≠ garbage ∧ apebs[n0].vidhdr = empty → apebs[n0].fill = 0) ∧ apebs[n0].fill ≤ LEB_SIZE ∧ is-aligned(apebs[n0].fill, EB_PAGE_SIZE) ∧ subarray(apebs[n0].data, apebs[n0].fill, LEB_SIZE - apebs[n0].fill) = mkempbuf(LEB_SIZE - apebs[n0].fill)) ∧ (¬ apebs[n0].bad → apebs[n0].echdr.valid? ∧ apebs[n0].vidhdr = empty) ⊦ # apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].data = LEB_SIZE ∧ ( ¬ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].bad → (apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].echdr = empty → apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr = empty) ∧ ( apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].echdr ≠ garbage ∧ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr = empty → apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill = 0) ∧ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill ≤ LEB_SIZE ∧ is-aligned(apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill, EB_PAGE_SIZE) ∧ subarray (apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].data, apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill, LEB_SIZE - apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill) = mkempbuf(LEB_SIZE - apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].fill)) ∧ ( ¬ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].bad → apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].echdr.valid? ∧ apebs[n, mkpeb(aehdr, avhdr, buf, m, boolvar)][n0].vidhdr = empty)

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic