| gstore[adr] = mkgnode(nd0, m0, boolvar1, boolvar2), fi = fi1, fo = p_os.keys, fs = nodes(gstore ↓, jro0), log = abs-log(nx, gstore ↓), remove-refsize0(gstore0) = gstore0, ri0 = ri, ro = jro.keys, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx = dom gstore1 ∪ jro0, dom gstore ∪ jro0 = dom gstore1 ∪ jro0, jro.keys.inodes?, p_os.keys.inodes?, fi1.inos < pmaxino, ri.inos < jmaxino, p_os < pmaxino, jro < jmaxino, ri.inos ∪ (key.inode? ⊃ ∅ ++ key.ino;∅) < jmaxino0, jro < jmaxino0, gstore1 =○refsize gstore, inv(gstore \ jro0), inv(gstore0), inv(gstore1 \ jro0), key-cons(key, nd0), log-cons(abs-log(nx, gstore ↓), nodes(gstore ↓, jro0)), refsize-cons(gstore0, range fi1), refsize-cons(gstore, range ri), refsize-cons(gstore1, range ri[key, adr]), ri-inj(fi1), ri-inj(ri), ri-inj(ri[key, adr]), adr ∈ fs, adr ∈ gstore, adr ∈ nodes(gstore ↓, jro0), pmaxino ≤ jmaxino, pmaxino ≤ jmaxino0, fi1.lebs ⊆ dom gstore0, ri.lebs ⊆ dom gstore, ri[key, adr].lebs ⊆ dom gstore1, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), jvalid → jvalid0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore1, jro0) ⊦ jmaxino = 0, jmaxino0 = 0, pmaxino = 0, dups(nx), adr ∈ fs, adr ∈ ri |