PROOF.sp.tail_masked: def of bend-osdev-mode-core@0.1.0.0
Import: import bend-osdev-mode-core@0.1.0.0/PROOF.bend as PROOF
Lines 352-419 of bend-osdev-mode-core@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&start_line=352&end_line=419

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

# the tail of a masked split is masked
def sp.tail_masked(ys: List<&2, U32>) -> {B.mask(M.cm.split.tail(M.cm.split(B.mask(ys)))) == M.cm.split.tail(M.cm.split(B.mask(ys))) : List<&2, U32>}:
  match ys:
    case Nil{}:
      li.mask_mask(Nil{})
    case Con{+y0, +r0}:
      match r0:
        case Nil{}:
          li.mask_mask(Con{y0, Nil{}})
        case Con{+y1, +r1}:
          match r1:
            case Nil{}:
              li.mask_mask(Con{y0, Con{y1, Nil{}}})
            case Con{+y2, +r2}:
              match r2:
                case Nil{}:
                  li.mask_mask(Con{y0, Con{y1, Con{y2, Nil{}}}})
                case Con{+y3, +r3}:
                  match r3:
                    case Nil{}:
                      li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Nil{}}}}})
                    case Con{+y4, +r4}:
                      match r4:
                        case Nil{}:
                          li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Nil{}}}}}})
                        case Con{+y5, +r5}:
                          match r5:
                            case Nil{}:
                              li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Nil{}}}}}}})
                            case Con{+y6, +r6}:
                              match r6:
                                case Nil{}:
                                  li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Nil{}}}}}}}})
                                case Con{+y7, +r7}:
                                  match r7:
                                    case Nil{}:
                                      li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Nil{}}}}}}}}})
                                    case Con{+y8, +r8}:
                                      match r8:
                                        case Nil{}:
                                          li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Nil{}}}}}}}}}})
                                        case Con{+y9, +r9}:
                                          match r9:
                                            case Nil{}:
                                              li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Nil{}}}}}}}}}}})
                                            case Con{+y10, +r10}:
                                              match r10:
                                                case Nil{}:
                                                  li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Nil{}}}}}}}}}}}})
                                                case Con{+y11, +r11}:
                                                  match r11:
                                                    case Nil{}:
                                                      li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Nil{}}}}}}}}}}}}})
                                                    case Con{+y12, +r12}:
                                                      match r12:
                                                        case Nil{}:
                                                          li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Nil{}}}}}}}}}}}}}})
                                                        case Con{+y13, +r13}:
                                                          match r13:
                                                            case Nil{}:
                                                              li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Nil{}}}}}}}}}}}}}}})
                                                            case Con{+y14, +r14}:
                                                              match r14:
                                                                case Nil{}:
                                                                  li.mask_mask(Con{y0, Con{y1, Con{y2, Con{y3, Con{y4, Con{y5, Con{y6, Con{y7, Con{y8, Con{y9, Con{y10, Con{y11, Con{y12, Con{y13, Con{y14, Nil{}}}}}}}}}}}}}}}})
                                                                case Con{+y15, +t}:
                                                                  %Equal.sym(List<&2, U32>, M.cm.split.tail(M.cm.split.cons(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))), M.cm.split.tail(M.cm.split(B.mask(t))), sp.cons_tail(M.cm.block16(B.byte(y0), B.byte(y1), B.byte(y2), B.byte(y3), B.byte(y4), B.byte(y5), B.byte(y6), B.byte(y7), B.byte(y8), B.byte(y9), B.byte(y10), B.byte(y11), B.byte(y12), B.byte(y13), B.byte(y14), B.byte(y15)), M.cm.split(B.mask(t)))) : {B.mask(_) == _ : List<&2, U32>}
                                                                  sp.tail_masked(t)

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=byte
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=mask
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.mask_mask
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=sp.cons_tail
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.block16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.split
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.split.cons
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.split.tail