Proof step 2 from proof referenced-adrs-split (previous step)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  referenced-adrs([], ri) = ax0 + ax1 ⊦ ∃ ax2, ax3. [] = ax2 + ax3 ∧ referenced-adrs(ax2, ri) = ax0 ∧ referenced-adrs(ax3, ri) = ax1

• Proof step 5:

  referenced-adrs(adr + ax2, ri) = ax0 + ax1, ∀ ri, ax0, ax1. referenced-adrs(ax2, ri) = ax0 + ax1 → (∃ ax4, ax3. ax2 = ax4 + ax3 ∧ referenced-adrs(ax4, ri) = ax0 ∧ referenced-adrs(ax3, ri) = ax1) ⊦ ∃ ax4, ax3. adr + ax2 = ax4 + ax3 ∧ referenced-adrs(ax4, ri) = ax0 ∧ referenced-adrs(ax3, ri) = ax1

Rule argument

Additional information

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