Proof step 2 from proof range-eq-validtrailer (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 3:

  is-aligned(m, NODE_HEADER_SIZE), is-aligned(# buf, NODE_HEADER_SIZE), range=(buf + mkempbuf(n), m, validtrailer, 0, NODE_HEADER_SIZE) ⊦ range=(buf, m, validtrailer, 0, NODE_HEADER_SIZE)

• Proof step 30:

  is-aligned(m, NODE_HEADER_SIZE), is-aligned(# buf, NODE_HEADER_SIZE), range=(buf, m, validtrailer, 0, NODE_HEADER_SIZE) ⊦ range=(buf + mkempbuf(n), m, validtrailer, 0, NODE_HEADER_SIZE)

Rule argument

Additional information