Proof step 24 from proof inv-commit (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 25:

  remove-refsize0(gstore1) = gstore1, remove-refsize0(istore1) = istore1, dom remove-refsize0(gstore2) ∩ ginval4 = ∅, elems nx ∩ ginval4 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval4, inv(gstore2 \ ginval4), inv(gstore1), inv(istore2), inv(istore1), istore1 ⊑ istore2, pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2, pstate.index? → pstate.lnum ∈ istore2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪ginval1 := ?⟫ ( inv(gstore2 \ ginval4) ∧ inv(gstore1) ∧ elems nx ∩ ginval4 = ∅ ∧ ¬ dups(nx) ∧ dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval4 ∧ remove-refsize0(gstore1) = gstore1 ∧ inv(istore2) ∧ inv(istore1) ∧ istore1 ⊑ istore2 ∧ remove-refsize0(istore1) = istore1 ∧ (readonly.journal? → nx ≠ [] ∧ readonly.lnum = nx.last ∧ readonly.lnum ∈ gstore2) ∧ (readonly.index? → readonly.lnum ∈ istore2)), err0 = ESUCCESS, dups(nx)

Rule argument

Additional information