Proof step 3 from proof inv-allocate (previous step)

Heuristic nonrecursive calls applied rule call right

And obtained the following new goals

• Proof step 4:

  jvalid1 ↔ jvalid, fi = fi1, fi0 = fi2, gstore1 = gstore, jmaxino = jmaxino0, jro0 = jro, nx0 = nx, remove-refsize0(gstore0) = gstore0, elems nx ∩ jro = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ jro, fi1.inos < pmaxino, fi2.inos < jmaxino1, p_os < pmaxino, inv(gstore0), inv(gstore \ jro), refsize-cons(gstore0, range fi1), refsize-cons(gstore, range fi2), ri-inj(fi1), ri-inj(fi2), pmaxino ≤ jmaxino1, fi1.lebs ⊆ dom gstore0, fi2.lebs ⊆ dom gstore, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro) ⊦ ⟪let n = ? in {index_get_leb_size(fi0, fi, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; ; n); if jmaxino > n then err := ENOSPC else let n = ?, jvalid = ? in {index_is_log_empty#(fi0, fi, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; ; jvalid); if ¬ jvalid ∧ jvalid1 then index_get_block_free_size#(fi0, fi, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; ; n); if ¬ jvalid ∧ jvalid1 ∧ jmaxino ≤ n then err := ESUCCESS else {index_sync#(fi0, fi, jro, gstore, gstore0, nx, pmaxino, p_os; ; jvalid0, err); if err = ESUCCESS then index_allocate_gnd#(fi0, fi, gstore0, pmaxino, p_os, jvalid0; jro, gstore, nx; err); if err = ESUCCESS then jvalid1 := true}}}⟫ ( (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi2.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi2) ∧ inv(gstore \ jro) ∧ elems nx ∩ jro = ∅ ∧ ¬ dups(nx) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ jro ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ dom gstore1 ⊆ dom gstore ∧ (nx.toSet \ nx0.toSet) ∩ dom gstore1 = ∅ ∧ abs-log(nx, gstore ↓) = abs-log(nx0, gstore1 ↓) ∧ nodes(gstore ↓, jro) = nodes(gstore1 ↓, jro0) ∧ (err = ESUCCESS → jvalid1 ∧ nx ≠ [])), pmaxino = 0, dups(nx)

Rule argument

Additional information

Used simplifier rules: allocate: ⊦ ;