| abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓), nodes(gstore1 ↓, jro) = nodes(gstore ↓, jro0), 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)), node-cons(nd3.key, nd3), node-cons(nd4.key, nd4), node-cons(nd5.key, nd5), node-cons(nd6.key, nd6), 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, ⌊err1⌋ , jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), jvalid5 → jvalid4, jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore1, jro) ⊦ ⟨choose err0 with ⌊err0⌋ in err := err0; adr9 := ?, adr6 := ?, adr0 := ?, adr := ?; jvalid := ?⟩ ((jvalid → jvalid1) ∧ adr7 = adr9 ∧ adr8 = adr6 ∧ adr11 = adr0 ∧ adr10 = adr ∧ err1 = err), ( adr ∈ nodes(gstore ↓, jro0) ∨ adr0 ∈ nodes(gstore ↓, jro0) ∨ adr1 ∈ nodes(gstore ↓, jro0) ∨ adr2 ∈ nodes(gstore ↓, jro0) ∨ adr = adr0 ∨ adr = adr1 ∨ adr = adr2 ∨ adr0 = adr1 ∨ adr0 = adr2 ∨ adr1 = adr2) ∧ ⟨err := ENOSPC; jvalid := ?⟩ ((jvalid → jvalid1) ∧ err1 = err), ∃ adr3, adr4, adr5, adr12. ¬ adr3 ∈ nodes(gstore ↓, jro0) ∧ ¬ adr4 ∈ nodes(gstore ↓, jro0) ∧ ¬ adr5 ∈ nodes(gstore ↓, jro0) ∧ ¬ adr12 ∈ nodes(gstore ↓, jro0) ∧ adr3 ≠ adr4 ∧ adr3 ≠ adr5 ∧ adr3 ≠ adr12 ∧ adr4 ≠ adr5 ∧ adr4 ≠ adr12 ∧ adr5 ≠ adr12 ∧ ⟨adr9 := adr3, adr6 := adr4, adr0 := adr5, adr := adr12; fs := nodes(gstore ↓, jro0)[adr9, nd6][adr6, nd5][adr0, nd4][adr, nd3], log := (((abs-log(nx, gstore ↓) + adr9 ') + adr6 ') + adr0 ') + adr ', err := ESUCCESS; jvalid := ?⟩ ( log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid1) ∧ adr7 = adr9 ∧ adr8 = adr6 ∧ adr11 = adr0 ∧ adr10 = adr ∧ err1 = err), jmaxino1 = 0, pmaxino = 0, dups(nx), dups(nx0) |
abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓), nodes(gstore1 ↓, jro) = nodes(gstore ↓, jro0), 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)), node-cons(nd6.key, nd6), node-cons(nd5.key, nd5), node-cons(nd4.key, nd4), node-cons(nd3.key, nd3), 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, ⌊err1⌋ , jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore1, jro), jvalid5 → jvalid4, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0) ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; adr9 := ?, adr6 := ?, adr0 := ?, adr := ?; jvalid := ?⟩ ((jvalid → jvalid1) ∧ adr7 = adr9 ∧ adr8 = adr6 ∧ adr11 = adr0 ∧ adr10 = adr ∧ err1 = err), ( adr ∈ nodes(gstore ↓, jro0) ∨ adr0 ∈ nodes(gstore ↓, jro0) ∨ adr1 ∈ nodes(gstore ↓, jro0) ∨ adr2 ∈ nodes(gstore ↓, jro0) ∨ adr = adr0 ∨ adr = adr1 ∨ adr = adr2 ∨ adr0 = adr1 ∨ adr0 = adr2 ∨ adr1 = adr2) ∧ ⟨err := ENOSPC; jvalid := ?⟩ ((jvalid → jvalid1) ∧ err1 = err), ∃ adr3, adr4, adr5, adr12. ¬ adr3 ∈ nodes(gstore ↓, jro0) ∧ ¬ adr4 ∈ nodes(gstore ↓, jro0) ∧ ¬ adr5 ∈ nodes(gstore ↓, jro0) ∧ ¬ adr12 ∈ nodes(gstore ↓, jro0) ∧ adr3 ≠ adr4 ∧ adr3 ≠ adr5 ∧ adr3 ≠ adr12 ∧ adr4 ≠ adr5 ∧ adr4 ≠ adr12 ∧ adr5 ≠ adr12 ∧ ⟨adr9 := adr3, adr6 := adr4, adr0 := adr5, adr := adr12; fs := nodes(gstore ↓, jro0)[adr9, nd6][adr6, nd5][adr0, nd4][adr, nd3], log := (((abs-log(nx, gstore ↓) + adr9 ') + adr6 ') + adr0 ') + adr ', err := ESUCCESS; jvalid := ?⟩ ( log = abs-log(nx, gstore ↓) ∧ fs = nodes(gstore ↓, jro0) ∧ (jvalid → jvalid1) ∧ adr7 = adr9 ∧ adr8 = adr6 ∧ adr11 = adr0 ∧ adr10 = adr ∧ err1 = err), jmaxino1 = 0, pmaxino = 0, dups(nx0), dups(nx)