| gstore2[n1] = groupblock(gndx, lax, 0), err0 = ESUCCESS, remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, 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 ∈ gstore1, n1 ∈ gstore2, pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, fi2.lebs ⊆ dom gstore2, jvalid4 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪gstore2 := gstore2 -- n1, jro0 := jro0 ++ n1⟫ ( (jvalid4 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0)) ∧ fi2.lebs ⊆ dom gstore2 ∧ refsize-cons(gstore2, range fi2) ∧ inv(gstore2 \ jro0) ∧ elems nx ∩ jro0 = ∅ ∧ dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0), jmaxino = 0, pmaxino = 0, dups(nx), n1 ∈ nx |
gstore2[n1] = groupblock(gndx, lax, 0), err0 = ESUCCESS, remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, jro1 < jmaxino, p_os < pmaxino, fi2.inos < jmaxino, fi1.inos < pmaxino, inv(gstore2 \ jro0), inv(gstore1), refsize-cons(gstore2, range fi2), refsize-cons(gstore1, range fi1), ri-cons(fi2, nodes(gstore2 ↓, jro0)), ri-inj(fi2), ri-inj(fi1), n1 ∈ gstore2, n1 ∈ gstore1, pmaxino ≤ jmaxino, fi2.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, jvalid4 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ jmaxino = 0, pmaxino = 0, dups(nx), n1 ∈ nx, (jvalid4 ∧ nx ≠ [] → valid-journal-head(nx, gstore2 -- n1, jro0 ++ n1)) ∧ fi2.lebs ⊆ dom(gstore2 -- n1) ∧ refsize-cons(gstore2 -- n1, range fi2) ∧ inv((gstore2 -- n1) \ (jro0 ++ n1)) ∧ elems nx ∩ (jro0 ++ n1) = ∅ ∧ dom gstore1 ∪ elems nx = dom(gstore2 -- n1) ∪ (jro0 ++ n1)