def octets_of_append

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:8499

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

8499# Octets.of_list of an append is the append of the Octets (from bytes' laws)
8500def 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}:
8501  %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}
8502  %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}
8503  %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}
8504  %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}
8505  %mask_append(p, q) : {B.Octets.of_list(B.append(p, q)) == B.Octets.of_list(_) : B.Octets}
8506  %BL.octets_to_of(B.append(p, q)) : {B.Octets.of_list(B.append(p, q)) == B.Octets.of_list(_) : B.Octets}
8507  %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}
8508  {==}