| abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓) + adr7 ' + adr1 ' + adr9 ' + adr10 ', nodes(gstore1 ↓, jro) = nodes(gstore ↓, jro0)[adr7, nd6][adr1, nd5][adr9, nd4][adr10, nd3], 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), nodes-cons(adr7 ' + adr1 ' + adr9 ' + adr10 ', nd6 ' + nd5 ' + nd4 ' + nd3 ', 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), adr10 ∈ abs-log(nx0, gstore1 ↓), 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) ⊦ ¬ adr7 ∈ nodes(gstore ↓, jro0) ∧ ¬ adr1 ∈ nodes(gstore ↓, jro0) ∧ ¬ adr9 ∈ nodes(gstore ↓, jro0) ∧ ¬ adr10 ∈ nodes(gstore ↓, jro0) ∧ adr7 ≠ adr1 ∧ adr7 ≠ adr9 ∧ adr7 ≠ adr10 ∧ adr1 ≠ adr9 ∧ adr1 ≠ adr10 ∧ adr9 ≠ adr10 ∧ ⟨adr6 := adr7, adr5 := adr1, adr0 := adr9, adr := adr10; fs := nodes(gstore ↓, jro0)[adr6, nd6][adr5, nd5][adr0, nd4][adr, nd3], log := (((abs-log(nx, gstore ↓) + adr6 ') + adr5 ') + adr0 ') + adr ', err := ESUCCESS; jvalid := ?⟩ ( log = abs-log(nx0, gstore1 ↓) ∧ fs = nodes(gstore1 ↓, jro) ∧ (jvalid → jvalid1) ∧ adr7 = adr6 ∧ adr1 = adr5 ∧ adr9 = adr0 ∧ adr10 = adr ∧ ESUCCESS = err), adr1 = adr10, adr1 = adr9, adr7 = adr10, adr7 = adr1, adr7 = adr9, adr9 = adr10, jmaxino1 = 0, pmaxino = 0, dups(nx), dups(nx0), adr9 ∈ nodes(gstore ↓, jro0), adr7 ∈ nodes(gstore ↓, jro0), adr1 ∈ nodes(gstore ↓, jro0), adr10 ∈ nodes(gstore ↓, jro0) |
abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓) + adr7 ' + adr1 ' + adr9 ' + adr10 ', nodes(gstore1 ↓, jro) = nodes(gstore ↓, jro0)[adr7, nd6][adr1, nd5][adr9, nd4][adr10, nd3], 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, adr1 ≠ adr9, adr1 ≠ adr10, adr7 ≠ adr9, adr7 ≠ adr1, adr7 ≠ adr10, adr9 ≠ adr10, jmaxino1 ≠ 0, pmaxino ≠ 0, 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), nodes-cons(adr7 ' + adr1 ' + adr9 ' + adr10 ', nd6 ' + nd5 ' + nd4 ' + nd3 ', 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), adr10 ∈ abs-log(nx0, gstore1 ↓), pmaxino ≤ jmaxino1, dom gstore ⊆ dom gstore1, fi1.lebs ⊆ dom gstore0, ri.lebs ⊆ dom gstore, ri.lebs ⊆ dom gstore1, ¬ dups(nx0), ¬ dups(nx), ¬ adr10 ∈ nodes(gstore ↓, jro0), ¬ adr1 ∈ nodes(gstore ↓, jro0), ¬ adr7 ∈ nodes(gstore ↓, jro0), ¬ adr9 ∈ nodes(gstore ↓, jro0), jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), jvalid5 → jvalid4, jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore1, jro) ⊦ ⟨adr6 := adr7, adr5 := adr1, adr0 := adr9, adr := adr10; fs := nodes(gstore ↓, jro0)[adr6, nd6][adr5, nd5][adr0, nd4][adr, nd3], log := (((abs-log(nx, gstore ↓) + adr6 ') + adr5 ') + adr0 ') + adr ', err := ESUCCESS; jvalid := ?⟩ ( log = abs-log(nx0, gstore1 ↓) ∧ fs = nodes(gstore1 ↓, jro) ∧ (jvalid → jvalid1) ∧ adr7 = adr6 ∧ adr1 = adr5 ∧ adr9 = adr0 ∧ adr10 = adr ∧ ESUCCESS = err)