Proof step 54 from proof inv-gc-copy (previous step)

User applied rule skip call

And obtained the following new goals

• Proof step 55:

  # ax = # ndx1, abs-log(nx, gstore3 ↓) = abs-log(nx1, gstore2 ↓) + ax, ax0 = [], gstore5 = gstore3, jro1 = jro, nodes(gstore3 ↓, jro) = nodes(gstore2 ↓, jro0)[ax, ndx1], nx2 = nx, remove-refsize0(gstore1) = gstore1, elems nx1 ∩ jro0 = ∅, (nx.toSet \ nx1.toSet) ∩ dom gstore2 = ∅, elems nx ∩ jro = ∅, dom gstore1 ∪ elems nx1 = dom gstore2 ∪ jro0, dom gstore1 ∪ elems nx = dom gstore3 ∪ jro, jro2 < jmaxino3, fi2.inos < jmaxino3, n0 < nd0.flashsize, p_os < pmaxino, fi2[ndx1.keys, ax].inos < jmaxino0, fi1.inos < pmaxino, inv(gstore3[nx.last]), inv(gstore2 \ jro0), inv(gstore1), inv(gstore3 \ jro), key-cons(nd0.key, nd0), key-cons(ndx1), key-cons(ndx), key-cons(ndx3), new(ax, nodes(gstore2 ↓, jro0)), refsize-cons(gstore2, range fi2), refsize-cons(gstore3, range fi2[ndx1.keys, ax]), refsize-cons(gstore1, range fi1), ri-inj(fi2), ri-inj(fi2[ndx1.keys, ax]), ri-inj(fi1), nx.last ∈ gstore3, nd0.key ∈ fi2, jmaxino3 ≤ jmaxino0, pmaxino ≤ jmaxino3, n0 ≤ LEB_SIZE, nd0.flashsize + ndx.flashsize ≤ LEB_SIZE, pmaxino ≤ jmaxino0, fi2.lebs ⊆ dom gstore3, fi2.lebs ⊆ dom gstore2, ndx1.keys.toSet ⊆ dom fi2, ndx.keys.toSet ⊆ dom fi2, ndx3.keys.toSet ⊆ dom fi2, range fi2 ⊆ dom nodes(gstore2 ↓, jro0), range fi2[ndx1.keys, ax] ⊆ dom nodes(gstore3 ↓, jro), dom gstore2 ⊆ dom gstore3, fi2[ndx1.keys, ax].lebs ⊆ dom gstore3, fi1.lebs ⊆ dom gstore1, jvalid1 → valid-journal-head(nx, gstore3, jro), jvalid7 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro0), ndx3 = [] ∨ LEB_SIZE < (nd0.flashsize + ndx.flashsize) + ndx3.head.flashsize ⊦ ∀ ax0, jvalid1, jmaxino1, jro, gstore3, nx, jvalid0, err. (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro)) ∧ fi2[ndx1.keys, ax].lebs ⊆ dom gstore3 ∧ refsize-cons(gstore3, range fi2[ndx1.keys, ax]) ∧ inv(gstore3 \ jro) ∧ elems nx ∩ jro = ∅ ∧ ¬ dups(nx) ∧ dom gstore1 ∪ elems nx = dom gstore3 ∪ jro ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ dom gstore5 ⊆ dom gstore3 ∧ (nx.toSet \ nx2.toSet) ∩ dom gstore5 = ∅ ∧ ( err = ESUCCESS → # ax0 = # ndx + 1 ∧ ¬ dups(ax0) ∧ nodes-cons(ax0, nd0 ' + ndx, gstore3, jro) ∧ abs-log(nx, gstore3 ↓) = abs-log(nx2, gstore5 ↓) + ax0 ∧ nodes(gstore3 ↓, jro) = nodes(gstore5 ↓, jro1)[ax0, nd0 ' + ndx] ∧ new(ax0, nodes(gstore5 ↓, jro1))) ∧ (err ≠ ESUCCESS → abs-log(nx, gstore3 ↓) = abs-log(nx2, gstore5 ↓) ∧ nodes(gstore3 ↓, jro) = nodes(gstore5 ↓, jro1)) → ⟪fi := fi2[ndx1.keys, ax]; if err = ESUCCESS then {ndx0 := nd0 ' + ndx; gjournal_gc_update_index#(jvalid1, fi1, jro, gstore1, nx, pmaxino, p_os, jvalid0; ax0, ndx0, jmaxino0, fi, gstore3)}⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ jmaxino3 ≤ jmaxino0 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro)) ∧ fi.inos < jmaxino0 ∧ fi.lebs ⊆ dom gstore3 ∧ refsize-cons(gstore3, range fi) ∧ inv(gstore3 \ jro) ∧ dom gstore1 ∪ elems nx = dom gstore3 ∪ jro ∧ ri-inj(fi) ∧ ndx3.keys.toSet ⊆ dom fi ∧ range fi ⊆ dom nodes(gstore3 ↓, jro) ∧ dom gstore2 ⊆ dom gstore3 ∧ (nx.toSet \ nx1.toSet) ∩ dom gstore2 = ∅ ∧ (∃ ax, ndx0, ndx4. ndx1 + nd0 ' + ndx + ndx3 = ndx0 + ndx4 ∧ (err = ESUCCESS → ndx4 = ndx3) ∧ new(ax, nodes(gstore2 ↓, jro0)) ∧ ¬ dups(ax) ∧ # ax = # ndx0 ∧ fi = fi2[ndx0.keys, ax] ∧ nodes(gstore3 ↓, jro) = nodes(gstore2 ↓, jro0)[ax, ndx0] ∧ abs-log(nx, gstore3 ↓) = abs-log(nx1, gstore2 ↓) + ax) ∧ ¬ # ndx + # ndx3 < (err = ESUCCESS ⊃ # ndx3;0)), jmaxino3 = 0, nx = [], pmaxino = 0, dups(ndx.keys), dups(ndx1.keys), dups(ndx1.keys + ndx.keys + ndx3.keys), dups(nx1), dups(nx), dups(ax), dups(ndx.keys + ndx3.keys), dups(ndx1.keys + ndx.keys), dups(ndx3.keys), nd0.key ∈ ndx1.keys, nd0.key ∈ ndx.keys, nd0.key ∈ ndx3.keys

Rule argument

Additional information