def sp.split_join
bend-osdev-cbc@0.1.0.0 · PROOF.bend:195
import bend-osdev-cbc@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
195def sp.split_join(bs: List<&2, M.CmBlock>) -> {M.cm.split(M.cm.join_onto(bs, Nil{})) == M.CmSplit{bs, Nil{}} : M.CmSplit}:
196 match bs:
197 case Nil{}:
198 {==}
199 case Con{+b, +t}:
200 %Equal.sym(M.CmSplit, M.cm.split(M.cm.bytes_onto(b, M.cm.join_onto(t, Nil{}))), M.cm.split.cons(b, M.cm.split(M.cm.join_onto(t, Nil{}))), sp.blk(b, M.cm.join_onto(t, Nil{}))) : {_ == M.CmSplit{Con{b, t}, Nil{}} : M.CmSplit}
201 %Equal.sym(M.CmSplit, M.cm.split(M.cm.join_onto(t, Nil{})), M.CmSplit{t, Nil{}}, sp.split_join(t)) : {M.cm.split.cons(b, _) == M.CmSplit{Con{b, t}, Nil{}} : M.CmSplit}
202 {==}