| 2 = # ax0, abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓) + adr5 ' + ax0, fs = nodes(gstore ↓, jro0), log = abs-log(nx, gstore ↓), nodes(gstore1 ↓, jro) = nodes(gstore ↓, jro0)[adr5, nd3][ax0, nd0 ' + nd2 '], remove-refsize0(gstore0) = gstore0, elems nx0 ∩ jro = ∅, (nx0.toSet \ nx.toSet) ∩ dom gstore = ∅, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx0 = dom gstore1 ∪ jro, dom gstore0 ∪ elems nx = dom gstore ∪ jro0, p_os.keys.inodes?, jro1.keys.inodes?, fi1.inos < pmaxino, ri.inos < jmaxino1, p_os < pmaxino, jro1 < jmaxino1, inv(gstore1 \ jro), inv(gstore0), inv(gstore \ jro0), log-cons(abs-log(nx, gstore ↓), nodes(gstore ↓, jro0)), new(ax0, nodes(gstore ↓, jro0)), node-cons(nd2.key, nd2), node-cons(nd0.key, nd0), node-cons(nd3.key, nd3), nodes-cons(adr5 ' + ax0, nd3 ' + nd0 ' + nd2 ', gstore1, jro), refsize-cons(gstore1, range ri), refsize-cons(gstore0, range fi1), refsize-cons(gstore, range ri), ri-cons(ri, nodes(gstore ↓, jro0)), ri-inj(fi1), ri-inj(ri), pmaxino ≤ jmaxino1, dom gstore ⊆ dom gstore1, fi1.lebs ⊆ dom gstore0, ri.lebs ⊆ dom gstore, ri.lebs ⊆ dom gstore1, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), jvalid5 → jvalid4, jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore1, jro) ⊦ ⟨choose adr1, adr2, adr3 with new(adr1 ' + (adr2 ' + adr3), fs) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ') in {adr4 := adr1, adr0 := adr2, adr := adr3; fs := fs[adr4, nd3][adr0, nd0][adr, nd2], log := ((log + adr4) + adr0) + adr, err := ESUCCESS} ifnone err := ENOSPC; jvalid := ?⟩ (log = abs-log(nx0, gstore1 ↓) ∧ fs = nodes(gstore1 ↓, jro) ∧ (jvalid → jvalid1) ∧ adr5 = adr4 ∧ ax0[0] = adr0 ∧ ax0[1] = adr ∧ ESUCCESS = err), jmaxino1 = 0, pmaxino = 0, dups(nx0), dups(nx), dups(ax0), adr5 ∈ nodes(gstore ↓, jro0), adr5 ∈ ax0 |
2 = # ax0, abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓) + adr5 ' + ax0, fs = nodes(gstore ↓, jro0), log = abs-log(nx, gstore ↓), nodes(gstore1 ↓, jro) = nodes(gstore ↓, jro0)[adr5, nd3][ax0, nd0 ' + nd2 '], remove-refsize0(gstore0) = gstore0, elems nx ∩ jro0 = ∅, (nx0.toSet \ nx.toSet) ∩ dom gstore = ∅, elems nx0 ∩ jro = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ jro0, dom gstore0 ∪ elems nx0 = dom gstore1 ∪ jro, jro1.keys.inodes?, p_os.keys.inodes?, jro1 < jmaxino1, p_os < pmaxino, ri.inos < jmaxino1, fi1.inos < pmaxino, inv(gstore \ jro0), inv(gstore0), inv(gstore1 \ jro), log-cons(abs-log(nx, gstore ↓), nodes(gstore ↓, jro0)), new(ax0, nodes(gstore ↓, jro0)), node-cons(nd3.key, nd3), node-cons(nd0.key, nd0), node-cons(nd2.key, nd2), nodes-cons(adr5 ' + ax0, nd3 ' + nd0 ' + nd2 ', gstore1, jro), refsize-cons(gstore, range ri), refsize-cons(gstore0, range fi1), refsize-cons(gstore1, range ri), ri-cons(ri, nodes(gstore ↓, jro0)), ri-inj(ri), ri-inj(fi1), pmaxino ≤ jmaxino1, ri.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore, fi1.lebs ⊆ dom gstore0, dom gstore ⊆ dom gstore1, jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore1, jro), jvalid5 → jvalid4, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0) ⊦ (∀ adr1, adr2, adr3. ¬(new(adr1 ' + (adr2 ' + adr3), fs) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 '))) ∧ ⟨err := ENOSPC; jvalid := ?⟩ (log = abs-log(nx0, gstore1 ↓) ∧ fs = nodes(gstore1 ↓, jro) ∧ (jvalid → jvalid1) ∧ adr5 = adr4 ∧ ax0[0] = adr0 ∧ ax0[1] = adr ∧ ESUCCESS = err), ∃ adr1, adr2, adr3. (new(adr1 ' + (adr2 ' + adr3), fs) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ')) ∧ ⟨adr4 := adr1, adr0 := adr2, adr := adr3; fs := fs[adr4, nd3][adr0, nd0][adr, nd2], log := ((log + adr4) + adr0) + adr, err := ESUCCESS; jvalid := ?⟩ ( log = abs-log(nx0, gstore1 ↓) ∧ fs = nodes(gstore1 ↓, jro) ∧ (jvalid → jvalid1) ∧ adr5 = adr4 ∧ ax0[0] = adr0 ∧ ax0[1] = adr ∧ ESUCCESS = err), jmaxino1 = 0, pmaxino = 0, dups(ax0), dups(nx), dups(nx0), adr5 ∈ ax0, adr5 ∈ nodes(gstore ↓, jro0)