Proof step 94 from proof inv-gc-update-index (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 95:

  # ax2 = # ndx1, # ax3 = # ndx2, gstore3[m] = groupblock(gndx, lax, m3), gstore3[@(m, m0, m1)] = mkgnode(nd, m2, boolvar, boolvar0), abs-log(nx, gstore3 ↓) = abs-log(nx, gstore2 ↓), dom gstore3 = dom gstore2, nodes(gstore3 ↓, jro0) = nodes(gstore2 ↓, jro0), remove-refsize0(gstore1) = gstore1, range fi2 ∩ ax3.toSet = ∅, range fi2 ∩ ax2.toSet = ∅, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, fi2[ndx2.keys, ax3].inos ∪ (nd.key.inode? ⊃ ∅ ++ nd.key.ino;∅) < max(nd.key.ino + 1, jmaxino), jro1 < jmaxino1, fi2.inos < jmaxino1, p_os < pmaxino, fi2[ndx2.keys, ax3].inos < jmaxino, fi1.inos < pmaxino, gstore3[m, groupblock(gndx, lax, m3 + m1)] =○refsize gstore3, inv(gstore2 \ jro0), inv(gstore1), inv(gstore3 \ jro0), inv(groupblock(gndx, lax, m3)), key-cons(ndx1), key-cons(ndx2), key-cons(nd.key, nd), nodes-cons(ax2, ndx1, gstore3, jro0), nodes-cons(ax3 + @(m, m0, m1) ' + ax2, ndx2 + nd ' + ndx1, gstore2, jro0), refsize-cons(gstore3[m, groupblock(gndx, lax, m3 + m1)], range fi2[ndx2.keys, ax3] ++ @(m, m0, m1)), refsize-cons(gstore2, range fi2), refsize-cons(gstore3, range fi2[ndx2.keys, ax3]), refsize-cons(gstore1, range fi1), ri-inj(fi2[ndx2.keys, ax3][nd.key, @(m, m0, m1)]), ri-inj(fi2), ri-inj(fi1), nd.key ∈ fi2, @(m, m0, m1) ∈ gstore3, m ∈ gstore3, jmaxino1 ≤ jmaxino, pmaxino ≤ jmaxino1, pmaxino ≤ jmaxino, jmaxino1 ≤ max(nd.key.ino + 1, jmaxino), pmaxino ≤ max(nd.key.ino + 1, jmaxino), ndx2.keys.toSet ⊆ dom fi2, fi2.lebs ⊆ dom gstore2, ndx1.keys.toSet ⊆ dom fi2, fi2[ndx2.keys, ax3].lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0), jvalid2 ∧ nx ≠ [] → valid-journal-head(nx, gstore3[m, groupblock(gndx, lax, m3 + m1)], jro0) ⊦ (dom fi2 ∪ ndx2.keys.toSet) ++ nd.key = dom fi2, jmaxino = 0, jmaxino1 = 0, max(nd.key.ino + 1, jmaxino) = 0, pmaxino = 0, dups(nx), dups(ax3 + ax2), dups(ax3), dups(ax2), m ∈ jro0, @(m, m0, m1) ∈ fi2, @(m, m0, m1) ∈ ax2, @(m, m0, m1) ∈ ax3, nd.key ∈ fi2[ndx2.keys, ax3]

Rule argument

Additional information

Used simplifier rules: let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat% ⊦ ¬ max(n, m) < m; (s)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic% ⊦ m < n → n ≠ 0; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ inv(groupblock(gndx, lax, m0)) → inv(groupblock(gndx, lax, n0)); (s)% ⊦ ¬ n < n; (s)%gblock.gndlist = gstore[n].gndlist, gblock.ladrlist = gstore[n].ladrlist ⊦ nodes-cons(ax, ndx, gstore, ginval) → nodes-cons(ax, ndx, gstore[n, gblock], ginval); (s)% ⊦ groupblock(gndx, lax, m).ladrlist = lax; (s)% ⊦ groupblock(gndx, lax, m).gndlist = gndx; (s)% ⊦ groupblock(gndx, lax, m).ref-size:= m0 = groupblock(gndx, lax, m0); (s)% ⊦ m + n = m + n0 ↔ n = n0; (s)% ⊦ # nd ' = 0 +1; (s)% ⊦ #(ndx + ndx0) = # ndx + # ndx0; (s)% ⊦ # adr ' = 0 +1; (s)% ⊦ #(ax + ax0) = # ax + # ax0; (s)%⊦ ¬ key ∈ ri ∧ ¬ key ∈ ri0 → (ri[key, adr] = ri0[key, adr] ↔ ri = ri0); (s)%a: ⊦ (kx + kx0) + kx1 = kx + kx0 + kx1; from specification list[key-list-set]%# kx = # ax ⊦ ri[kx + key ', ax + adr '] = ri[kx, ax][key, adr]; (s)% ⊦ # ndx.keys = # ndx; (s)% ⊦ nd '.keys = nd.key '; (s)% ⊦ (ndx0 + ndx1).keys = ndx0.keys + ndx1.keys; (s)%a: ⊦ (ndx + ndx0) + ndx1 = ndx + ndx0 + ndx1; from specification list[node-list]% ⊦ ndx + ndx0 = ndx1 + ndx0 ↔ ndx = ndx1; (s)%a: ⊦ (ax + ax0) + ax1 = ax + ax0 + ax1; from specification list[address-list-set]% ⊦ ax + ax0 = ax1 + ax0 ↔ ax = ax1; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ ns < n → ns < max(m + 1, n); (s)%⊦ inv(gstore \ ns) → (inv(gstore[n, gblock] \ ns) ↔ n ∈ ns ∨ inv(gblock)); (ws)% ⊦ n ∈ dom gstore ↔ n ∈ gstore; (s)% ⊦ ns ++ n ⊆ ns0 ↔ ns ⊆ ns0 ∧ n ∈ ns0; (ws)% ⊦ n ∈ gstore → dom gstore ++ n = dom gstore; (s)% ⊦ dom gstore[n, gblock] = dom gstore ++ n; (s)