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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 179:

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

Rule argument

Additional information

Used simplifier rules: a: ⊦ (ax + ax0) + ax1 = ax + ax0 + ax1; from specification list[address-list-set]% ⊦ [] + ax = ax; (s)% ⊦ abs-log([], gstore) = []; (s)% ⊦ ns \ ∅ = ns; (s)% ⊦ [].toSet = ∅; (s)%a: ⊦ (ndx + ndx0) + ndx1 = ndx + ndx0 + ndx1; from specification list[node-list]% ⊦ m +1 = m + 1; (s)% ⊦ #(nd ' + ndx) = (# ndx)+1; (s)%unc: ⊦ ns ∪ ns0 = ns0 ∪ ns; from specification set-union[nat-set]%una: ⊦ (ns ∪ ns0) ∪ ns1 = ns ∪ ns0 ∪ ns1; from specification set-union[nat-set]% ⊦ ns ∪ ∅ = ns; (s)% ⊦ ¬ dups([]); (s)%int-c: ⊦ ns ∩ ns0 = ns0 ∩ ns; from specification set-union[nat-set]%int-a: ⊦ (ns ∩ ns0) ∩ ns1 = ns ∩ ns0 ∩ ns1; from specification set-union[nat-set]% ⊦ ns ∩ ∅ = ∅; (s)% ⊦ elems [] = ∅; (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)