| 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(nd2.key, nd2), node-cons(nd0.key, nd0), node-cons(nd3.key, nd3), 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#(nd3 ' + nd0 ' + nd2 ', 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 = 3 ∧ ¬ dups(ax) ∧ nodes-cons(ax, nd3 ' + nd0 ' + nd2 ', gstore, jro0) ∧ abs-log(nx, gstore ↓) = abs-log(nx1, gstore3 ↓) + ax ∧ nodes(gstore ↓, jro0) = nodes(gstore3 ↓, jro2)[ax, nd3 ' + nd0 ' + nd2 '] ∧ new(ax, nodes(gstore3 ↓, jro2))) ∧ (err ≠ ESUCCESS → abs-log(nx, gstore ↓) = abs-log(nx1, gstore3 ↓) ∧ nodes(gstore ↓, jro0) = nodes(gstore3 ↓, jro2)) → ⟪adr1 := adr5; adr0 := adr2; adr := adr4; if err = ESUCCESS then {adr1 := ax[0]; adr0 := ax[1]; adr := ax[2]}⟫ ⟨aubifs_core_journal_add3#(nd3, nd0, nd2, ri, fi1, jro1.keys, p_os.keys; adr5, adr2, adr4, fs, log; jvalid5, err0)⟩ (log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid5 → jvalid4) ∧ adr1 = adr5 ∧ adr0 = adr2 ∧ adr = adr4 ∧ 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(nd3.key, nd3), node-cons(nd0.key, nd0), node-cons(nd2.key, nd2), 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 = 3 ∧ ¬ dups(ax) ∧ nodes-cons(ax, nd3 ' + nd0 ' + nd2 ', gstore, jro0) ∧ abs-log(nx, gstore ↓) = abs-log(nx1, gstore3 ↓) + ax ∧ nodes(gstore ↓, jro0) = nodes(gstore3 ↓, jro2)[ax, nd3 ' + nd0 ' + nd2 '] ∧ new(ax, nodes(gstore3 ↓, jro2))) ∧ (err ≠ ESUCCESS → abs-log(nx, gstore ↓) = abs-log(nx1, gstore3 ↓) ∧ nodes(gstore ↓, jro0) = nodes(gstore3 ↓, jro2)) → ⟪adr1 := adr5; adr0 := adr2; adr := adr4; if err = ESUCCESS then {adr1 := ax[0]; adr0 := ax[1]; adr := ax[2]}⟫ ⟨aubifs_core_journal_add3#(nd3, nd0, nd2, ri, fi1, jro1.keys, p_os.keys; adr5, adr2, adr4, fs, log; jvalid5, err0)⟩ (log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid5 → jvalid4) ∧ adr1 = adr5 ∧ adr0 = adr2 ∧ adr = adr4 ∧ err = err0), jmaxino1 = 0, pmaxino = 0, dups(nx)