Proof step 26 from proof inv-gc (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, jmaxino ≠ 0, pmaxino ≠ 0, fi1.inos < pmaxino, fi2.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore1), inv(gstore2 \ jro0), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range fi2), ri-cons(fi2, nodes(gstore2 ↓, jro0)), ri-inj(fi1), ri-inj(fi2), n1 ∈ gstore2, n1 ∈ gstore1, pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, fi2.lebs ⊆ dom gstore2, ¬ dups(nx), ¬ n1 ∈ nx, jvalid4 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0) ⊦ ⟪index_get_gblock_refsize#(n1, fi2, fi1, jro0, gstore2, gstore1, nx, pmaxino, p_os, jvalid; ; n); err := ESUCCESS; if n ≠ 0 then let ax = [], gndx = [], ndx = [] in {index_read_gblock_nodes#(n1, fi2, fi1, jro0, gstore2, gstore1, nx, pmaxino, p_os, jvalid; ax, gndx; err); if err ≠ ESUCCESS then debug#("gjournal: failed to read LEB " + n1.toString + " during GC") else gjournal_gc_referenced_nodes#(n1, fi2, fi1, jro0, gstore2, gstore1, nx, pmaxino, p_os, jvalid; ax, gndx; ndx, err); if err = ESUCCESS then {gjournal_gc_copy#(jvalid1, fi1, gstore1, pmaxino, p_os; ndx, jvalid4, jmaxino0, jmaxino, fi2, jro0, gstore2, nx, jvalid; err); if err ≠ ESUCCESS then debug#("gjournal: failed to copy nodes of LEB " + n1.toString + " to journal head during GC")}}; if err = ESUCCESS then index_sync#(fi2, fi1, jro0, gstore2, gstore1, nx, pmaxino, p_os; ; jvalid, err); if err = ESUCCESS then index_deallocate_gnd#(n1, fi2, fi1, gstore1, nx, pmaxino, p_os, jvalid; jro0, gstore2; err)⟫ ( jro1 < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi2.inos < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid4 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0)) ∧ fi2.lebs ⊆ dom gstore2 ∧ refsize-cons(gstore2, range fi2) ∧ inv(gstore2 \ jro0) ∧ elems nx ∩ jro0 = ∅ ∧ ¬ dups(nx) ∧ dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0 ∧ ri-inj(fi2))

Rule argument

Additional information