Proof step 20 from proof inv-addn (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 21:

  abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓), err = ESUCCESS, fi0 = fi2, nodes(gstore1 ↓, jro0) = nodes(gstore ↓, jro), remove-refsize0(gstore0) = gstore0, elems nx0 ∩ jro0 = ∅, (nx0.toSet \ nx.toSet) ∩ dom gstore = ∅, elems nx ∩ jro = ∅, dom gstore0 ∪ elems nx0 = dom gstore1 ∪ jro0, dom gstore0 ∪ elems nx = dom gstore ∪ jro, fi1.inos < pmaxino, fi2.inos < jmaxino1, p_os < pmaxino, inv(gstore1 \ jro0), inv(gstore \ jro), inv(gstore0), refsize-cons(gstore1, range fi2), refsize-cons(gstore0, range fi1), refsize-cons(gstore, range fi2), ri-inj(fi1), ri-inj(fi2), transaction(ndx, gndx), pmaxino ≤ jmaxino1, dom gstore ⊆ dom gstore1, fi1.lebs ⊆ dom gstore0, fi2.lebs ⊆ dom gstore, fi2.lebs ⊆ dom gstore1, jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore1, jro0), err = ESUCCESS → jvalid0 ∧ nx0 ≠ [], jvalid4 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪index_add_gnds#(gndx, fi0, fi1, jro0, gstore0, nx0, pmaxino, p_os; ax, gstore1; jvalid, err); if err = ESUCCESS then {jmaxino0 := jmaxino0 + # ndx; if jvalid1 then let err0 = ? in index_sync#(fi0, fi1, jro0, gstore1, gstore0, nx0, pmaxino, p_os; ; jvalid, err0)} else jvalid0 := false⟫ ( (jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore1, jro0)) ∧ fi2.lebs ⊆ dom gstore1 ∧ refsize-cons(gstore1, range fi2) ∧ inv(gstore1 \ jro0) ∧ dom gstore0 ∪ elems nx0 = dom gstore1 ∪ jro0 ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ dom gstore ⊆ dom gstore1 ∧ ( err = ESUCCESS → # ax = # ndx ∧ ¬ dups(ax) ∧ nodes-cons(ax, ndx, gstore1, jro0) ∧ abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓) + ax ∧ nodes(gstore1 ↓, jro0) = nodes(gstore ↓, jro)[ax, ndx] ∧ new(ax, nodes(gstore ↓, jro))) ∧ (err ≠ ESUCCESS → abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓) ∧ nodes(gstore1 ↓, jro0) = nodes(gstore ↓, jro))), pmaxino = 0, dups(nx0), dups(nx)

• Proof step 179:

  abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓), fi0 = fi2, nodes(gstore1 ↓, jro0) = nodes(gstore ↓, jro), remove-refsize0(gstore0) = gstore0, elems nx0 ∩ jro0 = ∅, (nx0.toSet \ nx.toSet) ∩ dom gstore = ∅, elems nx ∩ jro = ∅, dom gstore0 ∪ elems nx0 = dom gstore1 ∪ jro0, dom gstore0 ∪ elems nx = dom gstore ∪ jro, fi1.inos < pmaxino, fi2.inos < jmaxino1, p_os < pmaxino, inv(gstore1 \ jro0), inv(gstore \ jro), inv(gstore0), refsize-cons(gstore1, range fi2), refsize-cons(gstore0, range fi1), refsize-cons(gstore, range fi2), ri-inj(fi1), ri-inj(fi2), transaction(ndx, gndx), pmaxino ≤ jmaxino1, dom gstore ⊆ dom gstore1, fi1.lebs ⊆ dom gstore0, fi2.lebs ⊆ dom gstore, fi2.lebs ⊆ dom gstore1, jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore1, jro0), err = ESUCCESS → jvalid0 ∧ nx0 ≠ [], jvalid4 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪skip; if err = ESUCCESS then {jmaxino0 := jmaxino0 + # ndx; if jvalid1 then let err0 = ? in index_sync#(fi0, fi1, jro0, gstore1, gstore0, nx0, pmaxino, p_os; ; jvalid, err0)} else jvalid0 := false⟫ ( (jvalid0 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore1, jro0)) ∧ fi2.lebs ⊆ dom gstore1 ∧ refsize-cons(gstore1, range fi2) ∧ inv(gstore1 \ jro0) ∧ dom gstore0 ∪ elems nx0 = dom gstore1 ∪ jro0 ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ dom gstore ⊆ dom gstore1 ∧ ( err = ESUCCESS → # ax = # ndx ∧ ¬ dups(ax) ∧ nodes-cons(ax, ndx, gstore1, jro0) ∧ abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓) + ax ∧ nodes(gstore1 ↓, jro0) = nodes(gstore ↓, jro)[ax, ndx] ∧ new(ax, nodes(gstore ↓, jro))) ∧ (err ≠ ESUCCESS → abs-log(nx0, gstore1 ↓) = abs-log(nx, gstore ↓) ∧ nodes(gstore1 ↓, jro0) = nodes(gstore ↓, jro))), err = ESUCCESS, pmaxino = 0, dups(nx0), dups(nx)

Rule argument

Additional information