| fi = fi1, fi0 = fi2, ginval = ginval2, ginval0 = ginval1, gstore1 = crash(gstore, gstore0, ginval1, nx), maxino = maxino0, remove-refsize0(gstore0) = gstore0, elems nx ∩ ginval1 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval1, inv(gstore \ ginval1), inv(gstore0), inv(gstore[nx.last]), ri-inj(fi2), ri-inj(fi1), nx.last ∈ gstore ⊦ ⟨choose lax, err0 with (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ¬ dups(gstore[nx.last].ladrlist + lax) ∧ # lax ≤ # gndx ∧ inv-flashsize(prefixn(# lax, gndx), lax) ∧ (err0 = ESUCCESS ↔ # lax = # gndx) in {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 := ?⟩ (syn ∧ gstore1 = crash(gstore, gstore0, ginval1, nx)), nx = [], dups(nx) |
fi = fi1, fi0 = fi2, ginval = ginval2, ginval0 = ginval1, gstore1 = crash(gstore, gstore0, ginval1, nx), maxino = maxino0, remove-refsize0(gstore0) = gstore0, elems nx ∩ ginval1 = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval1, inv(gstore[nx.last]), inv(gstore0), inv(gstore \ ginval1), ri-inj(fi1), ri-inj(fi2), nx.last ∈ gstore ⊦ ∃ lax, err0. (⌊err0⌋ ∨ err0 = ESUCCESS → nx.last ∈ gstore ∧ nx ≠ []) ∧ ( (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ¬ dups(gstore[nx.last].ladrlist + lax) ∧ # lax ≤ # gndx ∧ inv-flashsize(prefixn(# lax, gndx), lax) ∧ (err0 = ESUCCESS ↔ # lax = # gndx)) ∧ ⟨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 := ?⟩ (syn ∧ gstore1 = crash(gstore, gstore0, ginval1, nx)), nx = [], dups(nx)