law split_join_short

bend-osdev-mode-core@0.1.0.0 · LAWS.bend:207

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M

207# blocks joined in front of a short tail split back into those blocks and tail
208law split_join_short:
209  for bs: List<&2, M.CmBlock>
210  for +rest: List<&2, U32>
211  for h1: {M.cm.split(rest) == M.CmSplit{Nil{}, rest} : M.CmSplit}
212  {M.cm.split(M.cm.join_onto(bs, rest)) == M.CmSplit{bs, rest} : M.CmSplit}