Proof step 6 from proof at-write-at (previous step)

User applied rule structural induction

And obtained the following new goals

• Proof step 7:

  # [] + # ax0 + 1 = # ndx ⊦ fs[[] + adr ' + ax0, ndx][adr] = ndx[# []], dups(ax0), dups([]), dups([] + ax0), adr ∈ ax0, adr ∈ []

• Proof step 9:

  #(adr0 + ax) + # ax0 + 1 = # ndx, ∀ ax0, ndx, fs, adr. # ax + # ax0 + 1 = # ndx → fs[ax + adr ' + ax0, ndx][adr] = ndx[# ax] ∨ dups(ax + ax0) ∨ dups(ax) ∨ dups(ax0) ∨ adr ∈ ax ∨ adr ∈ ax0 ⊦ fs[(adr0 + ax) + adr ' + ax0, ndx][adr] = ndx[#(adr0 + ax)], dups(ax0), dups(adr0 + ax), dups((adr0 + ax) + ax0), adr ∈ ax0, adr ∈ adr0 + ax

Rule argument

Additional information

Used simplifier rules: address-list freely generated by [], +;;