Proof step 78 from proof inv-format (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 79:

  err = ESUCCESS, err = err0, ginval = ∅, ginval0 = ∅, gstore = ∅, gstore0 = ∅, ind = indexnode(mkbrarray(BRANCH_SIZE), true, 0), istore = istore2[n, indexblock([], [], 0)], istore0 = ∅, istore2 = ∅, maxino = maxino4, nx = [], pstate = index(n), pstate0 = unbuffered, inv(istore), indexnode(mkbrarray(BRANCH_SIZE), true, 0).flashsize ≤ LEB_SIZE, pstate.index? → pstate.lnum ∈ istore, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪syn := true; err1 := err, istore1 := istore; if err1 = ESUCCESS then apersistence_add_ind#(ind, adr, istore0, ginval0, gstore0, gstore, nx, maxino, ginval; adr0, istore1, pstate, syn; err1); if err1 = ESUCCESS then apersistence_set_iblock_refsize# (adr0.lnum, ind.flashsize, adr, istore0, ginval0, gstore0, gstore, nx, maxino, ginval, pstate, syn; istore1); if err1 = ESUCCESS then apersistence_sync#(adr, istore1, istore0, ginval0, gstore0, gstore, nx, maxino, ginval; pstate, syn; err1); if err1 = ESUCCESS then let ns = ∅ in apersistence_commit#(adr0, maxino4, syn; ns, istore1, ginval0, gstore0, adr, istore0, gstore, nx, maxino, ginval; pstate, err1)⟫ ( ( err1 = ESUCCESS → syn ∧ (∃ ri, fi. btree-inv(null, adr, istore1, istore0, zh, ri, fi)) ∧ inv(gstore0 \ ginval0) ∧ inv(gstore) ∧ elems nx ∩ ginval0 = ∅ ∧ ¬ dups(nx) ∧ dom gstore ∪ elems nx = dom gstore0 ∪ ginval0 ∧ remove-refsize0(gstore) = gstore ∧ inv(istore1) ∧ inv(istore0) ∧ istore0 ⊑ istore1 ∧ remove-refsize0(istore0) = istore0 ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore0) ∧ (pstate.index? → pstate.lnum ∈ istore1)) ∧ (err1 = ESUCCESS ∨ ⌊err1⌋ ) ∧ (err1 = ESUCCESS → btree-inv(null, adr, istore1, istore0, zh, ∅, ∅) ∧ gstore0 = ∅ ∧ ginval0 = ∅ ∧ maxino = maxino4 ∧ nx = [] ∧ ginval = ∅)), pstate.journal?, n ∈ istore2

Rule argument

Additional information