tr':|E| List. tr' tr (x:|E|. (i:. i < ||tr'|| & x = tr'[i]) (y:|E|. (i:. i < ||tr'|| & y = tr'[i]) & is-send(E)(y) & (y =msg=(E) x)))

||tr||

y:|E|. (i@0:. i@0 < ||firstn(i+1;tr)|| & y = firstn(i+1;tr)[i@0]) & is-send(E)(y) & (y =msg=(E) tr[i])

j:||tr||. ji & is-send(E)(tr[j]) & (tr[j] =msg=(E) tr[i])

ExRepD
THEN
AllHyps (h.RWO "length_firstn" h)
THEN
AllHyps (h.RWO "select_firstn" h)

1	5. y: |E| 6. i@0: 7. i@0 < i+1 8. y = tr[i@0] 9. is-send(E)(y) 10. y =msg=(E) tr[i] j:||tr||. ji & is-send(E)(tr[j]) & (tr[j] =msg=(E) tr[i])

About: