def xtsp.lt_take

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1491

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M

1491def xtsp.lt_take(+n: Nat, +b: M.CmBlock, +h: {Nat.is_lt(n, 16n) == True{} : Bool}) -> {Nat.is_lt(B.len(B.take(n, M.cm.bytes_of(b))), 16n) == True{} : Bool}:
1492  %Equal.sym(Nat, B.len(B.take(n, M.cm.bytes_of(b))), n, li.len_take(n, M.cm.bytes_of(b))(na.lt_le(n, 16n)(h))) : {Nat.is_lt(_, 16n) == True{} : Bool}
1493  h