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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 68:

  err = err0, istore = ∅, pstate = unbuffered, indexnode(mkbrarray(BRANCH_SIZE), true, 0).flashsize ≤ LEB_SIZE, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [if err = ESUCCESS then choose n with ¬ n ∈ istore in istore[n] := indexblock([], [], 0), pstate := index(n)] ( inv(istore) ∧ ¬ pstate.journal? ∧ (pstate.index? → pstate.lnum ∈ istore) → ⟪nx := []; maxino := maxino4; istore0 := ∅; ind := indexnode(mkbrarray(BRANCH_SIZE), true, 0); gstore0 := ∅; gstore := ∅; ginval0 := ∅; ginval := ∅; 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 = ∅)))

Rule argument

Additional information