Proof step 5 from proof inv-add-gnds (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 6:

  err0 = ESUCCESS ↔ # lax = # gndx, fi = fi1, fi0 = fi2, ginval = ginval1, ginval0 = ginval2, remove-refsize0(gstore0) = gstore0, elems nx ∩ ginval2 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval2, inv(gstore[nx.last]), inv(gstore0), inv(gstore \ ginval2), inv-flashsize(prefixn(# lax, gndx), lax), ri-inj(fi1), ri-inj(fi2), nx.last ∈ gstore, # lax ≤ # gndx, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪ax := lax.to-adr(nx.last), err := err0; gstore[nx.last].gndlist := gstore[nx.last].gndlist + prefixn(# lax, gndx); gstore[nx.last].ladrlist := gstore[nx.last].ladrlist + lax; if err ≠ ESUCCESS then ax := ?; syn := ?⟫ (inv(gstore \ ginval2) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval2), nx = [], dups(nx), dups(gstore[nx.last].ladrlist + lax)

• Proof step 30:

  fi = fi1, fi0 = fi2, ginval = ginval1, ginval0 = ginval2, remove-refsize0(gstore0) = gstore0, elems nx ∩ ginval2 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval2, inv(gstore[nx.last]), inv(gstore0), inv(gstore \ ginval2), ri-inj(fi1), ri-inj(fi2), nx.last ∈ gstore ⊦ nx = [], dups(nx), ∃ lax, err0. (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ¬ dups(gstore[nx.last].ladrlist + lax) ∧ # lax ≤ # gndx ∧ inv-flashsize(prefixn(# lax, gndx), lax) ∧ (err0 = ESUCCESS ↔ # lax = # gndx)

• Proof step 35:

  fi = fi1, fi0 = fi2, ginval = ginval1, ginval0 = ginval2, remove-refsize0(gstore0) = gstore0, elems nx ∩ ginval2 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval2, inv(gstore[nx.last]), inv(gstore0), inv(gstore \ ginval2), ri-inj(fi1), ri-inj(fi2), nx.last ∈ gstore ⊦ nx = [], dups(nx), ∀ lax, err0. ⌊err0⌋ ∨ err0 = ESUCCESS → nx.last ∈ gstore ∧ nx ≠ []

Rule argument

Additional information