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

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 18:

  jvalid ↔ key ∈ fi, gstore3[@(m0, m1, m2)] = mkgnode(nd, m, boolvar, boolvar0), adr0 = @(m0, m1, m2), fi1 = fi, gstore = gstore2, gstore0 = gstore3, jro = jro0, jvalid, remove-refsize0(gstore2) = gstore2, elems nx ∩ jro0 = ∅, dom gstore2 ∪ elems nx = dom gstore3 ∪ jro0, fi0.inos < pmaxino, fi.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore2), inv(gstore3 \ jro0), key-cons(key, nd), refsize-cons(gstore2, range fi0), refsize-cons(gstore3, range fi), ri-inj(fi), ri-inj(fi0), @(m0, m1, m2) ∈ gstore3, pmaxino ≤ jmaxino, fi0.lebs ⊆ dom gstore2, fi.lebs ⊆ dom gstore3, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0) ⊦ [adr := fi[key]; fi[key] := adr0] ( ri-inj(fi) → ⟪let n = ? in {jro := jro0; gstore1 := gstore3; if jvalid then {index_get_gblock_refsize#(adr.lnum, fi, fi0, jro, gstore3, gstore2, nx, pmaxino, p_os, jvalid0; ; n); index_set_gblock_refsize#(adr.lnum, n - adr.size, fi, fi0, jro, gstore2, nx, pmaxino, p_os, jvalid0; gstore3)}; index_get_gblock_refsize#(m0, fi, fi0, jro, gstore3, gstore2, nx, pmaxino, p_os, jvalid0; ; n); index_set_gblock_refsize#(m0, n + m2, fi, fi0, jro, gstore2, nx, pmaxino, p_os, jvalid0; gstore3)}; jmaxino := max(key.ino + 1, jmaxino)⟫ ( jro1 < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi1.inos ∪ (key.inode? ⊃ ∅ ++ key.ino;∅) < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0)) ∧ fi1[key, @(m0, m1, m2)].lebs ⊆ dom gstore3 ∧ refsize-cons(gstore3, range fi1[key, @(m0, m1, m2)]) ∧ inv(gstore3 \ jro0) ∧ dom gstore2 ∪ elems nx = dom gstore3 ∪ jro0 ∧ gstore3 =○refsize gstore1 ∧ fi = fi1[key, @(m0, m1, m2)])), jmaxino = 0, pmaxino = 0, dups(nx), @(m0, m1, m2) ∈ fi

• Proof step 100:

  jvalid ↔ key ∈ fi, gstore3[@(m0, m1, m2)] = mkgnode(nd, m, boolvar, boolvar0), adr0 = @(m0, m1, m2), fi1 = fi, gstore = gstore2, gstore0 = gstore3, jro = jro0, ¬ jvalid, remove-refsize0(gstore2) = gstore2, elems nx ∩ jro0 = ∅, dom gstore2 ∪ elems nx = dom gstore3 ∪ jro0, fi0.inos < pmaxino, fi.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore2), inv(gstore3 \ jro0), key-cons(key, nd), refsize-cons(gstore2, range fi0), refsize-cons(gstore3, range fi), ri-inj(fi), ri-inj(fi0), @(m0, m1, m2) ∈ gstore3, pmaxino ≤ jmaxino, fi0.lebs ⊆ dom gstore2, fi.lebs ⊆ dom gstore3, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0) ⊦ [adr := ?; fi[key] := adr0] ( ri-inj(fi) → ⟪let n = ? in {jro := jro0; gstore1 := gstore3; if jvalid then {index_get_gblock_refsize#(adr.lnum, fi, fi0, jro, gstore3, gstore2, nx, pmaxino, p_os, jvalid0; ; n); index_set_gblock_refsize#(adr.lnum, n - adr.size, fi, fi0, jro, gstore2, nx, pmaxino, p_os, jvalid0; gstore3)}; index_get_gblock_refsize#(m0, fi, fi0, jro, gstore3, gstore2, nx, pmaxino, p_os, jvalid0; ; n); index_set_gblock_refsize#(m0, n + m2, fi, fi0, jro, gstore2, nx, pmaxino, p_os, jvalid0; gstore3)}; jmaxino := max(key.ino + 1, jmaxino)⟫ ( jro1 < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi1.inos ∪ (key.inode? ⊃ ∅ ++ key.ino;∅) < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore3, jro0)) ∧ fi1[key, @(m0, m1, m2)].lebs ⊆ dom gstore3 ∧ refsize-cons(gstore3, range fi1[key, @(m0, m1, m2)]) ∧ inv(gstore3 \ jro0) ∧ dom gstore2 ∪ elems nx = dom gstore3 ∪ jro0 ∧ gstore3 =○refsize gstore1 ∧ fi = fi1[key, @(m0, m1, m2)])), jmaxino = 0, pmaxino = 0, dups(nx), @(m0, m1, m2) ∈ fi

Rule argument

Additional information