| # ax0 = # referenced-adrs(lax1.to-adr(n1), ri0), # lax1 + # lax0 = # gndx0, gstore2[n1] = groupblock(gndx0, lax1 + lax0, m0), abs-log(nx0, gstore ↓) = abs-log(nx, gstore2 ↓) + ax0, nodes(gstore ↓, jro) = nodes(gstore2 ↓, jro0)[ax0, nodes(gstore2 ↓, jro0)[referenced-adrs(lax1.to-adr(n1), ri0)]], remove-refsize0(gstore1) = gstore1, elems nx0 ∩ jro = ∅, (nx0.toSet \ nx.toSet) ∩ dom gstore2 = ∅, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx0 = dom gstore ∪ jro, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, p_os.keys.inodes?, jro1.keys.inodes?, jro1 < jmaxino0, ri0[nodes(gstore2 ↓, jro0)[referenced-adrs(lax1.to-adr(n1), ri0)].keys, ax0].inos < jmaxino0, jro1 < jmaxino, p_os < pmaxino, ri0.inos < jmaxino, fi1.inos < pmaxino, inv(gstore \ jro), inv(gstore1), inv(gstore2 \ jro0), inv(groupblock(gndx0, lax1 + lax0, m0)), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro0)), new(ax0, nodes(gstore2 ↓, jro0)), refsize-cons(gstore2, range ri0), refsize-cons(gstore1, range fi1), refsize-cons(gstore, range ri0[nodes(gstore2 ↓, jro0)[referenced-adrs(lax1.to-adr(n1), ri0)].keys, ax0]), ri-cons(ri0, nodes(gstore2 ↓, jro0)), ri-inj(ri0[nodes(gstore2 ↓, jro0)[referenced-adrs(lax1.to-adr(n1), ri0)].keys, ax0]), ri-inj(ri0), ri-inj(fi1), n1 ∈ gstore1, n1 ∈ gstore2, pmaxino ≤ jmaxino0, jmaxino ≤ jmaxino0, pmaxino ≤ jmaxino, ri0.lebs ⊆ dom gstore, dom gstore2 ⊆ dom gstore, ri0.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, range ri0 ⊆ dom nodes(gstore2 ↓, jro0), ri0[nodes(gstore2 ↓, jro0)[referenced-adrs(lax1.to-adr(n1), ri0)].keys, ax0].lebs ⊆ dom gstore, ⌊err⌋ , jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore, jro), jvalid5 → jvalid4, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0) ⊦ ⟨jvalid := ?⟩ (nodes(gstore ↓, jro) = nodes(gstore ↓, jro) ∧ (jvalid → jvalid1)), jmaxino = 0, jmaxino0 = 0, m0 = 0, pmaxino = 0, dups(nodes(gstore2 ↓, jro0)[referenced-adrs(lax0.to-adr(n1), ri0)].keys), dups(nodes(gstore2 ↓, jro0)[referenced-adrs(lax1.to-adr(n1), ri0)].keys), dups(nx), dups(nx0), dups(ax0), dups(nodes(gstore2 ↓, jro0)[referenced-adrs(lax1.to-adr(n1), ri0)].keys + nodes(gstore2 ↓, jro0)[referenced-adrs(lax0.to-adr(n1), ri0)].keys), n1 ∈ nx, n1 ∈ jro0 |