| p_os0.keys = jro1.keys, ESUCCESS = err1, [] = abs-log(nx0, gstore0 ↓), nodes(gstore2 ↓, jro2) \ as = nodes(gstore0 ↓, jro), fs = nodes(gstore2 ↓, jro2), remove-refsize0(gstore1) = gstore1, ri = fi0, ro = jro1.keys, elems nx ∩ jro2 = ∅, dom remove-refsize0(gstore2) ∩ jro2 = ∅, as ∩ range fi0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro2, jmaxino ≠ 0, pmaxino ≠ 0, jro1.keys.inodes?, p_os.keys.inodes?, fi0.inos < jmaxino, p_os < pmaxino, jro1 < jmaxino, fi1.inos < pmaxino, inv(gstore1), inv(gstore2 \ jro2), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro2)), refsize-cons(gstore2, range fi0), refsize-cons(gstore1, range fi1), ri-cons(fi0, nodes(gstore2 ↓, jro2)), ri-inj(fi0), ri-inj(fi1), pmaxino ≤ jmaxino, fi0.lebs ⊆ dom gstore2, fi1.lebs ⊆ dom gstore1, ¬ dups(nx), jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro2), jvalid2 → jvalid0 ⊦ ⟨choose as with as ∩ range ri = ∅ in fi1 := ri, fo := ro, fs := fs \ as, log := [], err := ESUCCESS; jvalid := true⟩ (jro1.keys = fo ∧ fi0 = fi1 ∧ log = [] ∧ fs = nodes(gstore0 ↓, jro) ∧ err1 = err), ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; jvalid := ?⟩ (jro1.keys = p_os.keys ∧ fi0 = fi1 ∧ abs-log(nx, gstore2 ↓) = [] ∧ nodes(gstore2 ↓, jro2) = nodes(gstore0 ↓, jro) ∧ ESUCCESS = err), jro1.keys = p_os.keys ∧ fi0 = fi1 ∧ abs-log(nx, gstore2 ↓) = [] ∧ nodes(gstore2 ↓, jro2) = nodes(gstore0 ↓, jro) |
p_os0.keys = jro1.keys, ESUCCESS = err1, [] = abs-log(nx0, gstore0 ↓), nodes(gstore2 ↓, jro2) \ as0 = nodes(gstore0 ↓, jro), fs = nodes(gstore2 ↓, jro2), remove-refsize0(gstore1) = gstore1, ri = fi0, ro = jro1.keys, as0 ∩ range fi0 = ∅, dom remove-refsize0(gstore2) ∩ jro2 = ∅, elems nx ∩ jro2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ jro2, p_os.keys.inodes?, jro1.keys.inodes?, fi1.inos < pmaxino, jro1 < jmaxino, p_os < pmaxino, fi0.inos < jmaxino, inv(gstore2 \ jro2), inv(gstore1), log-cons(abs-log(nx, gstore2 ↓), nodes(gstore2 ↓, jro2)), refsize-cons(gstore1, range fi1), refsize-cons(gstore2, range fi0), ri-cons(fi0, nodes(gstore2 ↓, jro2)), ri-inj(fi1), ri-inj(fi0), pmaxino ≤ jmaxino, fi1.lebs ⊆ dom gstore1, fi0.lebs ⊆ dom gstore2, jvalid2 → jvalid0, jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore2, jro2) ⊦ ∃ as. as ∩ range ri = ∅ ∧ ⟨fi1 := ri, fo := ro, fs := fs \ as, log := [], err := ESUCCESS; jvalid := true⟩ (jro1.keys = fo ∧ fi0 = fi1 ∧ log = [] ∧ fs = nodes(gstore0 ↓, jro) ∧ err1 = err), ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; jvalid := ?⟩ (jro1.keys = p_os.keys ∧ fi0 = fi1 ∧ abs-log(nx, gstore2 ↓) = [] ∧ nodes(gstore2 ↓, jro2) = nodes(gstore0 ↓, jro) ∧ ESUCCESS = err), jmaxino = 0, pmaxino = 0, dups(nx), jro1.keys = p_os.keys ∧ fi0 = fi1 ∧ abs-log(nx, gstore2 ↓) = [] ∧ nodes(gstore2 ↓, jro2) = nodes(gstore0 ↓, jro)