Proof step 21 from proof refine-add1 (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  # ax = 1, abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓) + ax, fs = nodes(gstore ↓, jro0), log = abs-log(nx, gstore ↓), nodes(gstore1 ↓, jro) = nodes(gstore ↓, jro0)[ax, nd '], 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, ax ≠ [], jmaxino1 ≠ 0, pmaxino ≠ 0, 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)), new(ax, nodes(gstore ↓, jro0)), node-cons(nd.key, nd), nodes-cons(ax, nd ', 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), pmaxino ≤ jmaxino1, ri.lebs ⊆ dom gstore1, ri.lebs ⊆ dom gstore, fi1.lebs ⊆ dom gstore0, dom gstore ⊆ dom gstore1, ¬ dups(ax), ¬ dups(nx), ¬ dups(nx0), jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore1, jro), jvalid5 → jvalid4, jvalid3 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0) ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; adr := ?; jvalid := ?⟩ ( abs-log(nx, gstore ↓) = abs-log(nx0, gstore1 ↓) ∧ nodes(gstore ↓, jro0) = nodes(gstore1 ↓, jro) ∧ (jvalid → jvalid1) ∧ ax.head = adr ∧ ESUCCESS = err), ⟨choose adr1 with new(adr1 ', fs) ∧ ¬ dups(adr1 ') in {adr := adr1; fs[adr] := nd, log := log + adr, err := ESUCCESS} ifnone err := ENOSPC; jvalid := ?⟩ (log = abs-log(nx0, gstore1 ↓) ∧ fs = nodes(gstore1 ↓, jro) ∧ (jvalid → jvalid1) ∧ ax.head = adr ∧ ESUCCESS = err)

Rule argument

Additional information