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