| # ax = # ndx, jvalid ↔ jvalid1, jvalid0 ↔ jvalid2, ax0 = ax, fi1 = fi, gstore1 = gstore, jmaxino0 = jmaxino, jro = jro0, ndx0 = ndx, remove-refsize0(gstore0) = gstore0, ax.toSet ∩ range fi = ∅, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ jro0, jro1 < jmaxino, p_os < pmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, inv(gstore \ jro0), inv(gstore0), key-cons(ndx), nodes-cons(ax, ndx, gstore, jro0), refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), ri-inj(fi), ri-inj(fi0), pmaxino ≤ jmaxino, fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, ndx.keys.toSet ⊆ dom fi, jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0) ⊦ ⟪while ax ≠ [] do {/* (inv-gc-update-index : invariant # ax` = # ndx` ∧ (∃ ax0, ndx0. # ax0 = # ndx0 ∧ ax` = ax0 + ax ∧ ndx` = ndx0 + ndx ∧ fi = (fi`)[ndx0.keys, ax0]) ∧ dom fi = dom fi` ∧ inv-journal(nx, gstore, gstore0, jro) ∧ jmaxino` ≤ jmaxino ∧ fi.inos < jmaxino ∧ refsize-cons(gstore, range fi) ∧ ri-inj(fi) ∧ fi.lebs ⊆ dom gstore ∧ dom gstore = dom gstore` ∧ nodes-cons(ax, ndx, gstore, jro) ∧ nodes(gstore ↓, jro) = nodes(gstore` ↓, jro`) ∧ abs-log(nx, gstore ↓) = abs-log(nx`, gstore` ↓) ∧ (jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) wfbound # ax) */; gjournal_index_store#(ndx.head.key, ax.head, fi0, jro, gstore0, nx, pmaxino, p_os, jvalid; jmaxino, fi, gstore); ax := ax.tail; ndx := ndx.tail}⟫ ( jro1 < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi1[ndx0.keys, ax0].inos < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi1[ndx0.keys, ax0].lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi1[ndx0.keys, ax0]) ∧ inv(gstore \ jro0) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ jro0 ∧ ri-inj(fi1[ndx0.keys, ax0]) ∧ fi = fi1[ndx0.keys, ax0] ∧ dom gstore = dom gstore1 ∧ nodes(gstore ↓, jro0) = nodes(gstore1 ↓, jro0) ∧ abs-log(nx, gstore ↓) = abs-log(nx, gstore1 ↓) ∧ jmaxino0 ≤ jmaxino), jmaxino = 0, pmaxino = 0, dups(nx), dups(ax) |
# ax2 = # ndx1, jvalid0 ↔ jvalid2, jvalid ↔ jvalid1, abs-log(nx, gstore ↓) = abs-log(nx, gstore2 ↓), ax = ax1, ax0 = ax2, dom fi = dom fi2, dom gstore = dom gstore2, fi1 = fi2, gstore1 = gstore2, jmaxino0 = jmaxino1, jro = jro0, ndx0 = ndx1, nodes(gstore ↓, jro) = nodes(gstore2 ↓, jro), remove-refsize0(gstore0) = gstore0, elems nx ∩ jro0 = ∅, ax2.toSet ∩ range fi2 = ∅, dom gstore0 ∪ elems nx = dom gstore2 ∪ jro0, fi0.inos < pmaxino, fi2.inos < jmaxino1, p_os < pmaxino, jro1 < jmaxino1, fi.inos < jmaxino, inv(gstore0), inv(gstore2 \ jro0), inv-journal(nx, gstore, gstore0, jro), key-cons(ndx1), nodes-cons(ax2, ndx1, gstore2, jro0), nodes-cons(ax, ndx, gstore, jro), refsize-cons(gstore0, range fi0), refsize-cons(gstore2, range fi2), refsize-cons(gstore, range fi), ri-inj(fi0), ri-inj(fi2), ri-inj(fi), pmaxino ≤ jmaxino1, jmaxino1 ≤ jmaxino, ndx1.keys.toSet ⊆ dom fi2, fi0.lebs ⊆ dom gstore0, fi2.lebs ⊆ dom gstore2, fi.lebs ⊆ dom gstore, jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), ∃ ax0, ndx0. # ax0 = # ndx0 ∧ ax2 = ax0 + ax ∧ ndx1 = ndx0 + ndx ∧ fi = fi2[ndx0.keys, ax0] ⊦ ⟪gjournal_index_store#(ndx.head.key, ax.head, fi0, jro, gstore0, nx, pmaxino, p_os, jvalid; jmaxino, fi, gstore); ax := ax.tail; ndx := ndx.tail⟫ ( ( # ax2 = # ndx1 ∧ (∃ ax0, ndx0. # ax0 = # ndx0 ∧ ax2 = ax0 + ax ∧ ndx1 = ndx0 + ndx ∧ fi = fi2[ndx0.keys, ax0]) ∧ dom fi = dom fi2 ∧ inv-journal(nx, gstore, gstore0, jro) ∧ jmaxino1 ≤ jmaxino ∧ fi.inos < jmaxino ∧ refsize-cons(gstore, range fi) ∧ ri-inj(fi) ∧ fi.lebs ⊆ dom gstore ∧ dom gstore = dom gstore2 ∧ nodes-cons(ax, ndx, gstore, jro) ∧ nodes(gstore ↓, jro) = nodes(gstore2 ↓, jro) ∧ abs-log(nx, gstore ↓) = abs-log(nx, gstore2 ↓) ∧ (jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro))) ∧ # ax < # ax1), ax = [], jmaxino1 = 0, pmaxino = 0, dups(ax2), dups(nx)
Used simplifier rules: ⊦ ax + [] = ax; (s)%a: ⊦ (ax + ax0) + ax1 = ax + ax0 + ax1; from specification list[address-list-set]% ⊦ # ndx.keys = # ndx; (s)%# kx = # ax ⊦ dom ri[kx, ax] = dom ri ∪ kx.toSet; (s)% ⊦ ks ∪ ks0 = ks0 ↔ ks ⊆ ks0; (s)%una: ⊦ (ks ∪ ks0) ∪ ks1 = ks ∪ ks0 ∪ ks1; from specification set-union[node-index]%unc: ⊦ ks ∪ ks0 = ks0 ∪ ks; from specification set-union[node-index]% ⊦ #(ndx + ndx0) = # ndx + # ndx0; (s)%a: ⊦ (ndx + ndx0) + ndx1 = ndx + ndx0 + ndx1; from specification list[node-list]% ⊦ (ndx0 + ndx1).keys = ndx0.keys + ndx1.keys; (s)% ⊦ (kx + kx0).toSet = kx.toSet ∪ kx0.toSet; (s)%a: ⊦ (kx + kx0) + kx1 = kx + kx0 + kx1; from specification list[key-list-set]% ⊦ ks ∪ ks0 ⊆ ks1 ↔ ks ⊆ ks1 ∧ ks0 ⊆ ks1; (ws)% ⊦ key-cons(ndx0 + ndx1) ↔ key-cons(ndx0) ∧ key-cons(ndx1); (s)%⊦ inv-journal(nx, gstore, gstore0, ginval) ↔ inv(gstore \ ginval) ∧ inv(gstore0) ∧ elems nx ∩ ginval = ∅ ∧ ¬ dups(nx) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ remove-refsize0(gstore0) = gstore0; (s)%int-a: ⊦ (as ∩ as0) ∩ as1 = as ∩ as0 ∩ as1; from specification set-union[node-store]%int-c: ⊦ as ∩ as0 = as0 ∩ as; from specification set-union[node-store]%# ax = # kx ⊦ ri-inj(ri) ∧ ¬ dups(ax) ∧ ax.toSet ∩ range ri = ∅ → ri-inj(ri[kx, ax]); (s)% ⊦ ns < n ∧ n ≤ m → (ns < m ↔ true); (ss)%let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat% ⊦ m = m + n ↔ n = 0; (s)% ⊦ # ndx = 0 ↔ ndx = []; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ [].keys = []; (s)% ⊦ kx + [] = kx; (s)% ⊦ m ≤ 0 ↔ m = 0; (s)% ⊦ [].toSet = ∅; (s)% ⊦ ∅ ⊆ ks; (s)% ⊦ ndx + [] = ndx; (s)% ⊦ key-cons([]); (s)% ⊦ ax = ax0 + ax ↔ ax0 = []; (s)% ⊦ ndx = ndx0 + ndx ↔ ndx0 = []; (s)% ⊦ ri[[], []] = ri; (s)% ⊦ # [] = 0; (s)% ⊦ # [] = 0; (s)% ⊦ m ≤ m; (s) Used formulas: # ax` = # ndx` ∧ (∃ ax0, ndx0. # ax0 = # ndx0 ∧ ax` = ax0 + ax ∧ ndx` = ndx0 + ndx ∧ fi = (fi`)[ndx0.keys, ax0]) ∧ dom fi = dom fi` ∧ inv-journal(nx, gstore, gstore0, jro) ∧ jmaxino` ≤ jmaxino ∧ fi.inos < jmaxino ∧ refsize-cons(gstore, range fi) ∧ ri-inj(fi) ∧ fi.lebs ⊆ dom gstore ∧ dom gstore = dom gstore` ∧ nodes-cons(ax, ndx, gstore, jro) ∧ nodes(gstore ↓, jro) = nodes(gstore` ↓, jro`) ∧ abs-log(nx, gstore ↓) = abs-log(nx`, gstore` ↓) ∧ (jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)), # ax = # ax