~/jendhub

def tr.len_eq

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

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

913def tr.len_eq(+bs: List<&2, M.CmBlock>) -> {List.length(&2, M.CmBlock, bs) == M.cm.blocks.len(bs) : Nat}:
914  Equal.sym(Nat, M.cm.blocks.len(bs), List.length(&2, M.CmBlock, bs), Equal.trans(Nat, M.cm.blocks.len.go(bs, 0n), Nat.add(List.length(&2, M.CmBlock, bs), 0n), List.length(&2, M.CmBlock, bs), tr.len_go(bs, 0n), tr.add_zero(List.length(&2, M.CmBlock, bs))))

Uses (11)

Used by (3)