[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 37 from proof refine-write (previous step)

# apebs0 = # wlar0, # apebs = # wlar, LEB_SIZE = (n0 + n) + vtblpnum5, apebs0[n3] = mkpeb(aehdr, avhdr, mkempbuf(vtblpnum5) + subarray(buf, n4, n) + mkempbuf(n0), m, boolvar), vols[v][vtblpnum3] = unmapped, vtblpnum3 < # vols[v], vtblpnum3 < # avols[v], abs(avols, apebs, vols, q), abs(avols, apebs0, vols, q), bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar), ebm-cons(avols), id(apebs0, apebs, mapped-pebs(vols)), is-aligned(n, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs0, wlar0, vols[v, vols[v][vtblpnum3, ⌜n3⌝ ]], vtblpnum4), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-eraseq(q0), valid-eraseq(wlar0, q0), valid-eraseq(apebs0, q0), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum0), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs0, vols, wlar0, vtblpnum4), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-wl(apebs0, wlar0), valid-wl(apebs, wlar), v ∈ vols, v ∈ avols, n + vtblpnum5 ≤ LEB_SIZE, vtblpnum5 ≤ LEB_SIZE, n ≤ LEB_SIZE, n + n4 ≤ # buf, n4 + n ≤ # buf, vtblpnum5 + n ≤ LEB_SIZE, q0.lebrefs ⊆ q.lebrefs ++ (v × vtblpnum3), n = 0 → q0.lebrefs ⊆ q.lebrefs, n ≠ 0 → m = vtblpnum5 + n, n = 0 → m = 0 ⊦ avols[v][vtblpnum3].mapped?, abs (avols[v, avols[v][vtblpnum3, mapped(mkempbuf(vtblpnum5) + subarray(buf, n4, n) + mkempbuf(n0), vtblpnum5 + n)]], apebs0, vols[v, vols[v][vtblpnum3, ⌜n3⌝ ]], q0), VTBL_VOLID ∈ vols

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 38:
⊦ q1.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ abs(avols, apebs, vols, q0) ∧ v ∈ avols ∧ m < # avols[v] ∧ avols[v][m] ≠ erased → abs(avols, apebs, vols, q1)
Proof step 39:
# apebs = # wlar, # apebs0 = # wlar0, LEB_SIZE = (n0 + n) + vtblpnum5, vols[v][vtblpnum3] = unmapped, apebs0[n3] = mkpeb(aehdr, avhdr, mkempbuf(vtblpnum5) + subarray(buf, n4, n) + mkempbuf(n0), m, boolvar), vtblpnum3 < # avols[v], vtblpnum3 < # vols[v], abs(avols, apebs0, vols, q), abs(avols, apebs, vols, q), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), ebm-cons(avols), id(apebs0, apebs, mapped-pebs(vols)), is-aligned(vtblpnum5, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-inv(apebs0), unique-sqns(apebs), unique-sqns(apebs0), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar0, vols[v, vols[v][vtblpnum3, ⌜n3⌝ ]], vtblpnum4), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-eraseq(apebs0, q0), valid-eraseq(wlar0, q0), valid-eraseq(q0), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs0, sqnum0), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-vtbl(apebs0, vols, wlar0, vtblpnum4), valid-wl(apebs, wlar), valid-wl(apebs0, wlar0), v ∈ avols, v ∈ vols, vtblpnum5 + n ≤ LEB_SIZE, n4 + n ≤ # buf, n + n4 ≤ # buf, n ≤ LEB_SIZE, vtblpnum5 ≤ LEB_SIZE, n + vtblpnum5 ≤ LEB_SIZE, q0.lebrefs ⊆ q.lebrefs ++ (v × vtblpnum3), n = 0 → m = 0, n ≠ 0 → m = vtblpnum5 + n, n = 0 → q0.lebrefs ⊆ q.lebrefs ⊦ avols[v][vtblpnum3].mapped?, abs (avols[v, avols[v][vtblpnum3, mapped(mkempbuf(vtblpnum5) + subarray(buf, n4, n) + mkempbuf(n0), vtblpnum5 + n)]], apebs0, vols[v, vols[v][vtblpnum3, ⌜n3⌝ ]], q0), VTBL_VOLID ∈ vols, q0.lebrefs ⊆ q.lebrefs ++ (v × vtblpnum3) ∧ abs (avols[v, avols[v][vtblpnum3, mapped(mkempbuf(vtblpnum5) + subarray(buf, n4, n) + mkempbuf(n0), vtblpnum5 + n)]], apebs0, vols[v, vols[v][vtblpnum3, ⌜n3⌝ ]], q) ∧ v ∈ avols[v, avols[v][vtblpnum3, mapped(mkempbuf(vtblpnum5) + subarray(buf, n4, n) + mkempbuf(n0), vtblpnum5 + n)]] ∧ vtblpnum3 < # avols[v, avols[v][vtblpnum3, mapped(mkempbuf(vtblpnum5) + subarray(buf, n4, n) + mkempbuf(n0), vtblpnum5 + n)]][v] ∧ avols[v, avols[v][vtblpnum3, mapped(mkempbuf(vtblpnum5) + subarray(buf, n4, n) + mkempbuf(n0), vtblpnum5 + n)]][v][vtblpnum3] ≠ erased

Rule argument

spec: ubi-abs name: abs-lebrefs-subset-noterased-some seq: ⊦ q1.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ abs(avols, apebs, vols, q0) ∧ v ∈ avols ∧ m < # avols[v] ∧ avols[v][m] ≠ erased → abs(avols, apebs, vols, q1) subst: [q0, v, m, q1, vols, apebs, avols] → [q, v, vtblpnum3, q0, vols[v, vols[v][vtblpnum3, ⌜n3⌝ ]], apebs0, avols [v, avols[v] [vtblpnum3, mapped (mkempbuf(vtblpnum5) + subarray(buf, n4, n) + mkempbuf(n0), vtblpnum5 + n) ] ]] flags: <all paths>

Additional information

Used terms: q, v, vtblpnum3, q0, vols[v, vols[v][vtblpnum3, ⌜n3⌝ ]], apebs0, avols [v, avols[v] [vtblpnum3, mapped (mkempbuf(vtblpnum5) + subarray(buf, n4, n) + mkempbuf(n0), vtblpnum5 + n) ] ]