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

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 184:

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

• Proof step 200:

  abs-log(nx1, gstore2 ↓) = [], dom gstore1 = dom gstore3 ∪ jro, fi = fi2, nodes(gstore3 ↓, jro) = nodes(gstore2 ↓, jro0), remove-refsize0(gstore1) = gstore1, elems nx1 ∩ jro0 = ∅, nx0.toSet ∩ dom gstore3 = ∅, elems nx0 ∩ jro3 = ∅, dom gstore1 ∪ elems nx1 = dom gstore2 ∪ jro0, dom gstore1 ∪ elems nx0 = dom gstore ∪ jro3, fi1.inos < pmaxino, fi2.inos < jmaxino3, p_os < pmaxino, fi2.inos < jmaxino0, jro2 < jmaxino3, inv(gstore2 \ jro0), inv(gstore1), inv(gstore3 \ jro), inv(gstore \ jro3), key-cons(ndx1), key-cons(nd.key, nd), key-cons(ndx), refsize-cons(gstore1, range fi1), refsize-cons(gstore3, range fi2), refsize-cons(gstore2, range fi2), refsize-cons(gstore, range fi2), ri-inj(fi1), ri-inj(fi2), nd.key ∈ fi2, pmaxino ≤ jmaxino3, jmaxino3 ≤ jmaxino0, pmaxino ≤ jmaxino0, nd.flashsize + ndx.flashsize ≤ LEB_SIZE, fi2.lebs ⊆ dom gstore, dom gstore2 ⊆ dom gstore, fi1.lebs ⊆ dom gstore1, fi2.lebs ⊆ dom gstore3, fi2.lebs ⊆ dom gstore2, ndx1.keys.toSet ⊆ dom fi2, ndx.keys.toSet ⊆ dom fi2, range fi2 ⊆ dom nodes(gstore2 ↓, jro0), dom gstore2 ⊆ dom gstore3, dom gstore3 ⊆ dom gstore, jvalid7 ∧ nx1 ≠ [] → valid-journal-head(nx1, gstore2, jro0), err ≠ ESUCCESS → abs-log(nx0, gstore ↓) = [] ∧ nodes(gstore ↓, jro3) = nodes(gstore2 ↓, jro0), err = ESUCCESS → # abs-log(nx0, gstore ↓) = # ndx + 1 ∧ ¬ dups(abs-log(nx0, gstore ↓)) ∧ nodes-cons(abs-log(nx0, gstore ↓), nd ' + ndx, gstore, jro3) ∧ abs-log(nx0, gstore ↓) = ax ∧ nodes(gstore ↓, jro3) = nodes(gstore2 ↓, jro0)[abs-log(nx0, gstore ↓), nd ' + ndx] ∧ new(abs-log(nx0, gstore ↓), nodes(gstore2 ↓, jro0)), jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore, jro3), ndx1 = [] ∨ LEB_SIZE < (nd.flashsize + ndx.flashsize) + ndx1.head.flashsize, err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪skip⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (∃ ndx0. (nd ' + ndx) + ndx1 = ndx0 + ndx1) ∧ jmaxino3 ≤ jmaxino0 ∧ (jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore, jro3)) ∧ fi.inos < jmaxino0 ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv(gstore \ jro3) ∧ dom gstore1 ∪ elems nx0 = dom gstore ∪ jro3 ∧ ri-inj(fi) ∧ ndx1.keys.toSet ⊆ dom fi ∧ range fi ⊆ dom nodes(gstore ↓, jro3) ∧ dom gstore2 ⊆ dom gstore ∧ (∃ ndx3, ndx0. (nd ' + ndx) + ndx1 = ndx3 + ndx0 ∧ (err = ESUCCESS → ndx0 = ndx1) ∧ new(abs-log(nx0, gstore ↓), nodes(gstore2 ↓, jro0)) ∧ ¬ dups(abs-log(nx0, gstore ↓)) ∧ # abs-log(nx0, gstore ↓) = # ndx3 ∧ fi = fi2[ndx3.keys, abs-log(nx0, gstore ↓)] ∧ nodes(gstore ↓, jro3) = nodes(gstore2 ↓, jro0)[abs-log(nx0, gstore ↓), ndx3]) ∧ (err = ESUCCESS ⊃ # ndx1;0) < #((nd ' + ndx) + ndx1)), err = ESUCCESS, jmaxino3 = 0, pmaxino = 0, dups(ndx1.keys), dups(ndx.keys), dups(ndx.keys + ndx1.keys), dups(nx1), dups(nx0), nd.key ∈ ndx1.keys, nd.key ∈ ndx.keys

Rule argument

Additional information