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