Proof step 127 from proof inv-store (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 128:

  gstore3[m0] = groupblock(gndx, lax, m3), gstore3[@(m0, m1, m2)] = mkgnode(nd, m, boolvar, boolvar0), remove-refsize0(gstore2) = gstore2, elems nx ∩ jro0 = ∅, dom gstore2 ∪ elems nx = dom gstore3 ∪ jro0, fi1.inos < pmaxino, fi2.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore2), inv(gstore3 \ jro0), inv(gstore3[m0, groupblock(gndx, lax, m3 + m2)] \ jro0), key-cons(key, nd), refsize-cons(gstore2, range fi1), refsize-cons(gstore3, range fi2), ri-inj(fi1), ri-inj(fi2[key, @(m0, m1, m2)]), ri-inj(fi2), @(m0, m1, m2) ∈ gstore3, m0 ∈ gstore3, pmaxino ≤ jmaxino, pmaxino ≤ max(key.ino + 1, jmaxino), fi1.lebs ⊆ dom gstore2, fi2.lebs ⊆ dom gstore3, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0) ⊦ jmaxino = 0, max(key.ino + 1, jmaxino) = 0, pmaxino = 0, dups(nx), refsize-cons(gstore3[m0, groupblock(gndx, lax, m3 + m2)], range fi2 ++ @(m0, m1, m2)), key ∈ fi2, @(m0, m1, m2) ∈ fi2

• Proof step 138:

  gstore3[m0] = groupblock(gndx, lax, m3), gstore3[@(m0, m1, m2)] = mkgnode(nd, m, boolvar, boolvar0), jvalid1, remove-refsize0(gstore2) = gstore2, elems nx ∩ jro0 = ∅, dom gstore2 ∪ elems nx = dom gstore3 ∪ jro0, fi1.inos < pmaxino, fi2.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore2), inv(gstore3 \ jro0), inv(gstore3[m0, groupblock(gndx, lax, m3 + m2)] \ jro0), key-cons(key, nd), refsize-cons(gstore2, range fi1), refsize-cons(gstore3, range fi2), ri-inj(fi1), ri-inj(fi2[key, @(m0, m1, m2)]), ri-inj(fi2), @(m0, m1, m2) ∈ gstore3, m0 ∈ gstore3, pmaxino ≤ jmaxino, pmaxino ≤ max(key.ino + 1, jmaxino), fi1.lebs ⊆ dom gstore2, fi2.lebs ⊆ dom gstore3, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0) ⊦ jmaxino = 0, max(key.ino + 1, jmaxino) = 0, nx = [], pmaxino = 0, dups(nx), valid-journal-head(nx, gstore3[m0, groupblock(gndx, lax, m3 + m2)], jro0), key ∈ fi2, @(m0, m1, m2) ∈ fi2

• Proof step 152:

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

Rule argument

Additional information