PROOF.octets_of_append: def of bend-osdev-crypto@0.1.0.0
Import: import bend-osdev-crypto@0.1.0.0/PROOF.bend as PROOF
Lines 153-162 of bend-osdev-crypto@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-crypto@0.1.0.0/PROOF.bend&start_line=153&end_line=162

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL

# Octets.of_list of an append is the append of the Octets (from bytes' laws)
def octets_of_append(+p: List<&2, U32>, +q: List<&2, U32>) -> {B.Octets.of_list(B.append(p, q)) == B.Octets.append(B.Octets.of_list(p), B.Octets.of_list(q)) : B.Octets}:
  %BL.octets_of_to(B.Octets.append(B.Octets.of_list(p), B.Octets.of_list(q))) : {B.Octets.of_list(B.append(p, q)) == _ : B.Octets}
  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(B.Octets.of_list(p), B.Octets.of_list(q))), B.append(B.Octets.to_list(B.Octets.of_list(p)), B.Octets.to_list(B.Octets.of_list(q))), BL.octets_append_list(B.Octets.of_list(p), B.Octets.of_list(q))) : {B.Octets.of_list(B.append(p, q)) == B.Octets.of_list(_) : B.Octets}
  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(p)), B.mask(p), BL.octets_to_of(p)) : {B.Octets.of_list(B.append(p, q)) == B.Octets.of_list(B.append(_, B.Octets.to_list(B.Octets.of_list(q)))) : B.Octets}
  %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.of_list(q)), B.mask(q), BL.octets_to_of(q)) : {B.Octets.of_list(B.append(p, q)) == B.Octets.of_list(B.append(B.mask(p), _)) : B.Octets}
  %mask_append(p, q) : {B.Octets.of_list(B.append(p, q)) == B.Octets.of_list(_) : B.Octets}
  %BL.octets_to_of(B.append(p, q)) : {B.Octets.of_list(B.append(p, q)) == B.Octets.of_list(_) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.of_list(B.Octets.to_list(B.Octets.of_list(B.append(p, q)))), B.Octets.of_list(B.append(p, q)), BL.octets_of_list_idempotent(B.append(p, q))) : {B.Octets.of_list(B.append(p, q)) == _ : B.Octets}
  {==}

Uses (14):
  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/LAWS.bend&name=octets_append_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_of_list_idempotent
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_of_to
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&name=octets_to_of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.to_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=append
  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-crypto@0.1.0.0/PROOF.bend&name=mask_append