Proof step 5 from proof refine-store (previous step)

User applied rule insert program lemma

And obtained the following new goals

• Proof step 6:

  jro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), ¬ adr ∈ fi, adr ∈ gstore, key-cons(key, gstore[adr].nd), gstore1 = gstore, fi1 = fi ⊦ ⟪gjournal_index_store#(key, adr, fi0, jro0, gstore0, nx, pmaxino, p_os, jvalid0; jmaxino, fi, gstore)⟫ ( jro < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi.inos < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro0) ∧ ri-inj(fi) ∧ gstore =○refsize gstore1 ∧ fi = fi1[key, adr])

• Proof step 7:

  gstore ↓[adr] = mkgnode(nd, m, boolvar, boolvar0), fi = ri, fs = nodes(gstore ↓, jro0), log = abs-log(nx, gstore ↓), remove-refsize0(gstore0) = gstore0, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ jro0, p_os.keys.inodes?, jro.keys.inodes?, fi1.inos < pmaxino, ri.inos < jmaxino, p_os < pmaxino, jro < jmaxino, inv(gstore0), inv(gstore \ jro0), key-cons(key, nd), log-cons(abs-log(nx, gstore ↓), nodes(gstore ↓, jro0)), refsize-cons(gstore0, range fi1), refsize-cons(gstore, range ri), ri-inj(fi1), ri-inj(ri), adr ∈ nodes(gstore ↓, jro0), pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore0, ri.lebs ⊆ dom gstore, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), jvalid → jvalid0 ⊦ jmaxino = 0, pmaxino = 0, dups(nx), adr ∈ ri, jro < jmaxino ∧ p_os < pmaxino ∧ pmaxino ≤ jmaxino ∧ fi.inos < jmaxino ∧ fi1.inos < pmaxino ∧ jmaxino ≠ 0 ∧ pmaxino ≠ 0 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi.lebs ⊆ dom gstore ∧ fi1.lebs ⊆ dom gstore0 ∧ refsize-cons(gstore, range fi) ∧ refsize-cons(gstore0, range fi1) ∧ inv-journal(nx, gstore, gstore0, jro0) ∧ ri-inj(fi) ∧ ri-inj(fi1) ∧ ¬ adr ∈ fi ∧ adr ∈ gstore ∧ key-cons(key, gstore[adr].nd) ∧ gstore = gstore ∧ fi = fi

• Proof step 9:

  jvalid2 ↔ jvalid1, jvalid3 ↔ jvalid0, gstore ↓[adr] = mkgnode(nd, m, boolvar, boolvar0), adr0 = adr, fi = ri, fi = fi, fi2 = fi1, fi3 = fi, fs = nodes(gstore ↓, jro0), gstore = gstore, gstore2 = gstore0, gstore3 = gstore, jro1 = jro, jro2 = jro0, key0 = key, log = abs-log(nx, gstore ↓), nx0 = nx, p_os0 = p_os, pmaxino0 = pmaxino, remove-refsize0(gstore0) = gstore0, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ jro0, p_os.keys.inodes?, jro.keys.inodes?, ri.inos < jmaxino, jro < jmaxino, p_os < pmaxino, fi.inos < jmaxino, fi1.inos < pmaxino, inv(gstore0), inv(gstore \ jro0), inv-journal(nx, gstore, gstore0, jro0), key-cons(key, nd), key-cons(key, gstore[adr].nd), log-cons(abs-log(nx, gstore ↓), nodes(gstore ↓, jro0)), refsize-cons(gstore, range ri), refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi1), ri-inj(ri), ri-inj(fi), ri-inj(fi1), adr ∈ nodes(gstore ↓, jro0), adr ∈ gstore, pmaxino ≤ jmaxino, ri.lebs ⊆ dom gstore, fi.lebs ⊆ dom gstore, fi1.lebs ⊆ dom gstore0, jvalid → jvalid0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0) ⊦ [gjournal_index_store#(key, adr, fi1, jro0, gstore0, nx, pmaxino, p_os, jvalid0; jmaxino, fi, gstore)] ( jro1 < jmaxino ∧ pmaxino0 ≤ jmaxino ∧ fi.inos < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid2 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore, jro2)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx0, gstore, gstore2, jro2) ∧ ri-inj(fi) ∧ gstore =○refsize gstore3 ∧ fi = fi3[key0, adr0] → ⟨aubifs_core_index_store#(key, adr, fi1, jro.keys, p_os.keys, fs, log, jvalid; ri)⟩ (fi = ri ∧ log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid0))), jmaxino = 0, pmaxino = 0, dups(nx), adr ∈ fi, adr ∈ ri

Rule argument

Additional information