| syn ↔ true, istore = istore1, istore0 = istore2, remove-refsize0(istore1) = istore1, remove-refsize0(gstore0) = gstore0, elems nx ∩ ginval = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval, inv(istore1), inv(istore2), inv(gstore0), inv(gstore \ ginval), n ∈ gstore0, n ∈ gstore, istore1 ⊑ istore2, pstate.index? → pstate.lnum ∈ istore2, pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore ⊦ ⟪choose err0 with ⌊err0⌋ ∨ err0 = ESUCCESS in err := err0; if err = ESUCCESS then gstore := gstore -- n, ginval := ginval ++ n⟫ ( inv(gstore \ ginval) ∧ elems nx ∩ ginval = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore2)), dups(nx), n ∈ nx |
syn ↔ true, istore = istore1, istore0 = istore2, remove-refsize0(gstore0) = gstore0, remove-refsize0(istore1) = istore1, elems nx ∩ ginval = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval, inv(gstore \ ginval), inv(gstore0), inv(istore2), inv(istore1), n ∈ gstore, n ∈ gstore0, istore1 ⊑ istore2, pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore, pstate.index? → pstate.lnum ∈ istore2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪err := err0; if err = ESUCCESS then gstore := gstore -- n, ginval := ginval ++ n⟫ ( inv(gstore \ ginval) ∧ elems nx ∩ ginval = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore2)), dups(nx), n ∈ nx
syn ↔ true, istore = istore1, istore0 = istore2, remove-refsize0(gstore0) = gstore0, remove-refsize0(istore1) = istore1, elems nx ∩ ginval = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval, inv(gstore \ ginval), inv(gstore0), inv(istore2), inv(istore1), n ∈ gstore, n ∈ gstore0, istore1 ⊑ istore2, pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore, pstate.index? → pstate.lnum ∈ istore2 ⊦ dups(nx), n ∈ nx, ∃ err0. ⌊err0⌋ ∨ err0 = ESUCCESS