| err0 = ESUCCESS, 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), istore1 ⊑ istore2, pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore, pstate.index? → pstate.lnum ∈ istore2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪gstore[n] := groupblock([], [], 0), nx := nx + n, ginval := ginval -- n, pstate := journal(n)⟫ ( inv(gstore \ ginval) ∧ elems nx ∩ ginval = ∅ ∧ ¬ dups(nx) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore2)), pstate = readonly, dups(nx), n ∈ gstore |
Used simplifier rules: ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ nx + n = nx + n '; (s)% ⊦ elems(nx0 + n ') = elems nx0 ++ n; (s)%a: ⊦ (nx + nx0) + nx1 = nx + nx0 + nx1; from specification list[nat-list-set]% ⊦ (ns ++ n) ∩ (ns0 -- n) = (ns ∩ ns0) -- n; (s)%int-a: ⊦ (ns ∩ ns0) ∩ ns1 = ns ∩ ns0 ∩ ns1; from specification set-union[nat-set]%int-c: ⊦ ns ∩ ns0 = ns0 ∩ ns; from specification set-union[nat-set]% ⊦ dups(nx + n ') ↔ n ∈ nx ∨ dups(nx); (ws)% ⊦ (ns ++ n) ∪ ns0 = (ns ∪ ns0) ++ n; (s)%una: ⊦ (ns ∪ ns0) ∪ ns1 = ns ∪ ns0 ∪ ns1; from specification set-union[nat-set]%unc: ⊦ ns ∪ ns0 = ns0 ∪ ns; from specification set-union[nat-set]% ⊦ dom gstore[n, gblock] = dom gstore ++ n; (s)% ⊦ (ns ∪ (ns0 -- n)) ++ n = (ns ∪ ns0) ++ n; (s)% ⊦ journal(m).journal?; (s)% ⊦ nx + n ' ≠ []; (s)% ⊦ journal(m).lnum = m; (s)% ⊦ (nx + n ').last = n; (s)% ⊦ n ∈ gstore[n, gblock]; (s)% ⊦ ¬ journal(m).index?; (s)% ⊦ ∅ -- n = ∅; (s)%⊦ inv(gstore \ ns) → (inv(gstore[n, gblock] \ (ns -- n)) ↔ inv(gblock)); (ss)% ⊦ inv(groupblock([], [], m0)); (s)%elems-in-notin-ginval: ⊦ n ∈ nx ∧ elems nx ∩ ns = ∅ → ¬ n ∈ ns; (forward) from specification apersistence-base%fwd-in-log-in-gstore: ⊦ n ∈ nx ∧ ginval ∩ elems nx = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval → n ∈ gstore; (forward) from specification apersistence-base