Proof step 2 from proof ebm-cons-write (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  m < # avols[v], v ∈ avols, ∀ v0. v0 ∈ avols → (∀ m0. m0 < # avols[v0] → avols[v0][m0].mapped? → # avols[v0][m0].data = LEB_SIZE ∧ avols[v0][m0].fill ≤ LEB_SIZE ∧ is-aligned(avols[v0][m0].fill, EB_PAGE_SIZE) ∧ range=(avols[v0][m0].data, avols[v0][m0].fill, emptyleb, 0, LEB_SIZE - avols[v0][m0].fill)) ⊦ (∀ v0. v0 ∈ avols[v, avols[v][m, leb]] → (∀ m0. m0 < # avols[v, avols[v][m, leb]][v0] → avols[v, avols[v][m, leb]][v0][m0].mapped? → # avols[v, avols[v][m, leb]][v0][m0].data = LEB_SIZE ∧ avols[v, avols[v][m, leb]][v0][m0].fill ≤ LEB_SIZE ∧ is-aligned(avols[v, avols[v][m, leb]][v0][m0].fill, EB_PAGE_SIZE) ∧ range= (avols[v, avols[v][m, leb]][v0][m0].data, avols[v, avols[v][m, leb]][v0][m0].fill, emptyleb, 0, LEB_SIZE - avols[v, avols[v][m, leb]][v0][m0].fill))) ↔ ( avols[v][m].mapped? → # avols[v][m].data = LEB_SIZE ∧ avols[v][m].fill ≤ LEB_SIZE ∧ is-aligned(avols[v][m].fill, EB_PAGE_SIZE) ∧ range=(avols[v][m].data, avols[v][m].fill, emptyleb, 0, LEB_SIZE - avols[v][m].fill)) → leb.mapped? → # leb.data = LEB_SIZE ∧ leb.fill ≤ LEB_SIZE ∧ is-aligned(leb.fill, EB_PAGE_SIZE) ∧ range=(leb.data, leb.fill, emptyleb, 0, LEB_SIZE - leb.fill)

Rule argument

Additional information

Used simplifier rules: ebm-cons-def: ⊦ ebm-cons(avols) ↔ (∀ v. v ∈ avols → ebm-cons(avols[v]));%ebm-cons: ⊦ ebm-cons(evol) ↔ (∀ m. m < # evol → valid-leb(evol[m]));%valid-leb-def: ⊦ valid-leb(leb) ↔ leb.mapped? → # leb.data = LEB_SIZE ∧ leb.fill ≤ LEB_SIZE ∧ is-aligned(leb.fill, EB_PAGE_SIZE) ∧ range=(leb.data, leb.fill, emptyleb, 0, LEB_SIZE - leb.fill);% ⊦ m < n → n ≠ 0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic