| jvalid ↔ jvalid3, jvalid0 ↔ jvalid4, ri[key] = @(m, m0, m1), fi = fi1, fo = p_os.keys, fs = nodes(gstore2 ↓, jro0), log = abs-log(nx, gstore2 ↓), nd = nd0, nd1 = nd0, remove-refsize0(gstore1) = gstore1, ro = jro1.keys, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, p_os.keys.inodes?, jro1.keys.inodes?, fi1.inos < pmaxino, ri.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, inv(gstore1), inv(gstore2 \ jro0), 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), @(m, m0, m1) ∈ gstore2, key ∈ ri, m ∈ gstore2, pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore2, ⌊err0⌋ , jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0), jvalid4 → jvalid2 ⊦ ⟨fail_or_success#(; ; err); if err = ESUCCESS then {jvalid := key ∈ ri; if jvalid then nd := fs[ri[key]] else nd := ?} else jvalid := ?, nd := ?⟩ ((jvalid4 → jvalid2) ∧ jvalid ∧ nd1 = nd ∧ err0 = err), jmaxino = 0, pmaxino = 0, dups(nx), m ∈ jro0 |
ri[key] = @(m, m0, m1), remove-refsize0(gstore1) = gstore1, elems nx ∩ jro0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro0, jmaxino ≠ 0, pmaxino ≠ 0, jro1.keys.inodes?, p_os.keys.inodes?, jro1 < jmaxino, p_os < pmaxino, ri.inos < jmaxino, fi1.inos < pmaxino, inv(gstore2 \ jro0), inv(gstore1), 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), m ∈ gstore2, key ∈ ri, @(m, m0, m1) ∈ gstore2, pmaxino ≤ jmaxino, ri.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, ⌊err0⌋ , ¬ dups(nx), ¬ m ∈ jro0, jvalid4 → jvalid2, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro0) ⊦ ⟨fail_or_success#(; ; err); if err = ESUCCESS then {jvalid := key ∈ ri; if jvalid then nd := nodes(gstore2 ↓, jro0)[ri[key]] else nd := ?} else jvalid := ?, nd := ?⟩ ((jvalid4 → jvalid2) ∧ jvalid ∧ nd0 = nd ∧ err0 = err)