| gstore2[n1] = groupblock(gndx0, lax, m), remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, jmaxino ≠ 0, m ≠ 0, pmaxino ≠ 0, p_os.keys.inodes?, jro1.keys.inodes?, ri.inos < jmaxino, jro1 < jmaxino, p_os < pmaxino, fi1.inos < pmaxino, inv(gstore1), inv(gstore2 \ jro0), inv(groupblock(gndx0, lax, m)), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro0)), refsize-cons(gstore2, range ri), refsize-cons(gstore1, range fi1), ri-cons(ri, nodes(gstore2 ↓, jro0)), ri-inj(ri), ri-inj(fi1), n1 ∈ gstore2, n1 ∈ gstore1, pmaxino ≤ jmaxino, ri.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, ⌊err0⌋ , ¬ dups(nx), ¬ n1 ∈ nx, ¬ n1 ∈ jro0, jvalid5 → jvalid4, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0) ⊦ ⟨fs := nodes(gstore2 ↓, jro0); jvalid := ?⟩ (fs = nodes(gstore2 ↓, jro0) ∧ (jvalid → jvalid4)) |
gstore2[n1] = groupblock(gndx0, lax, m), remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, jro1.keys.inodes?, p_os.keys.inodes?, fi1.inos < pmaxino, p_os < pmaxino, jro1 < jmaxino, ri.inos < jmaxino, inv(groupblock(gndx0, lax, m)), inv(gstore2 \ jro0), inv(gstore1), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro0)), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range ri), ri-cons(ri, nodes(gstore2 ↓, jro0)), ri-inj(fi1), ri-inj(ri), n1 ∈ gstore1, n1 ∈ gstore2, pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore2, ⌊err0⌋ , jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), jvalid5 → jvalid4 ⊦ ⟨jvalid := ?⟩ (nodes(gstore2 ↓, jro0) = nodes(gstore2 ↓, jro0) ∧ (jvalid → jvalid4)), jmaxino = 0, m = 0, pmaxino = 0, dups(nx), n1 ∈ nx, n1 ∈ jro0