| fs = nodes(gstore ↓, jro0), gstore3 = gstore, jro2 = jro0, log = abs-log(nx, gstore ↓), nx1 = nx, remove-refsize0(gstore0) = gstore0, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ jro0, jmaxino1 ≠ 0, pmaxino ≠ 0, p_os.keys.inodes?, jro1.keys.inodes?, fi1.inos < pmaxino, ri.inos < jmaxino1, p_os < pmaxino, jro1 < jmaxino1, inv(gstore0), inv(gstore \ jro0), log-cons(abs-log(nx, gstore ↓), nodes(gstore ↓, jro0)), node-cons(nd1.key, nd1), node-cons(nd2.key, nd2), refsize-cons(gstore0, range fi1), refsize-cons(gstore, range ri), ri-cons(ri, nodes(gstore ↓, jro0)), ri-inj(fi1), ri-inj(ri), pmaxino ≤ jmaxino1, fi1.lebs ⊆ dom gstore0, ri.lebs ⊆ dom gstore, ¬ dups(nx), jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), jvalid5 → jvalid4 ⊦ [gjournal_journal_addn#(nd2 ' + nd1 ', jvalid1, ri, fi1, gstore0, pmaxino, p_os; ax, jvalid3, jmaxino, jro0, gstore, nx, jvalid4; err)] ( (jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ ri.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range ri) ∧ inv(gstore \ jro0) ∧ elems nx ∩ jro0 = ∅ ∧ ¬ dups(nx) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ jro0 ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ dom gstore3 ⊆ dom gstore ∧ (nx.toSet \ nx1.toSet) ∩ dom gstore3 = ∅ ∧ ( err = ESUCCESS → # ax = 2 ∧ ¬ dups(ax) ∧ nodes-cons(ax, nd2 ' + nd1 ', gstore, jro0) ∧ abs-log(nx, gstore ↓) = abs-log(nx1, gstore3 ↓) + ax ∧ nodes(gstore ↓, jro0) = nodes(gstore3 ↓, jro2)[ax, nd2 ' + nd1 '] ∧ new(ax, nodes(gstore3 ↓, jro2))) ∧ (err ≠ ESUCCESS → abs-log(nx, gstore ↓) = abs-log(nx1, gstore3 ↓) ∧ nodes(gstore ↓, jro0) = nodes(gstore3 ↓, jro2)) → ⟪adr0 := adr3; adr := adr2; if err = ESUCCESS then {adr0 := ax[0]; adr := ax[1]}⟫ ⟨aubifs_core_journal_add2#(nd2, nd1, ri, fi1, jro1.keys, p_os.keys; adr3, adr2, fs, log; jvalid5, err0)⟩ (log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid5 → jvalid4) ∧ adr0 = adr3 ∧ adr = adr2 ∧ err = err0)) |
fs = nodes(gstore ↓, jro0), gstore3 = gstore, jro2 = jro0, log = abs-log(nx, gstore ↓), nx1 = nx, remove-refsize0(gstore0) = gstore0, elems nx ∩ jro0 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ jro0, jro1.keys.inodes?, p_os.keys.inodes?, jro1 < jmaxino1, p_os < pmaxino, ri.inos < jmaxino1, fi1.inos < pmaxino, inv(gstore \ jro0), inv(gstore0), log-cons(abs-log(nx, gstore ↓), nodes(gstore ↓, jro0)), node-cons(nd2.key, nd2), node-cons(nd1.key, nd1), refsize-cons(gstore, range ri), refsize-cons(gstore0, range fi1), ri-cons(ri, nodes(gstore ↓, jro0)), ri-inj(ri), ri-inj(fi1), pmaxino ≤ jmaxino1, ri.lebs ⊆ dom gstore, fi1.lebs ⊆ dom gstore0, jvalid5 → jvalid4, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0) ⊦ ∀ ax, jvalid3, jmaxino, jro0, gstore, nx, jvalid4, err. (jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ ri.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range ri) ∧ inv(gstore \ jro0) ∧ elems nx ∩ jro0 = ∅ ∧ ¬ dups(nx) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ jro0 ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ dom gstore3 ⊆ dom gstore ∧ (nx.toSet \ nx1.toSet) ∩ dom gstore3 = ∅ ∧ ( err = ESUCCESS → # ax = 2 ∧ ¬ dups(ax) ∧ nodes-cons(ax, nd2 ' + nd1 ', gstore, jro0) ∧ abs-log(nx, gstore ↓) = abs-log(nx1, gstore3 ↓) + ax ∧ nodes(gstore ↓, jro0) = nodes(gstore3 ↓, jro2)[ax, nd2 ' + nd1 '] ∧ new(ax, nodes(gstore3 ↓, jro2))) ∧ (err ≠ ESUCCESS → abs-log(nx, gstore ↓) = abs-log(nx1, gstore3 ↓) ∧ nodes(gstore ↓, jro0) = nodes(gstore3 ↓, jro2)) → ⟪adr0 := adr3; adr := adr2; if err = ESUCCESS then {adr0 := ax[0]; adr := ax[1]}⟫ ⟨aubifs_core_journal_add2#(nd2, nd1, ri, fi1, jro1.keys, p_os.keys; adr3, adr2, fs, log; jvalid5, err0)⟩ (log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid5 → jvalid4) ∧ adr0 = adr3 ∧ adr = adr2 ∧ err = err0), jmaxino1 = 0, pmaxino = 0, dups(nx)