def tr.len_go

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

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

906def tr.len_go(+bs: List<&2, M.CmBlock>, +n: Nat) -> {M.cm.blocks.len.go(bs, n) == Nat.add(List.length(&2, M.CmBlock, bs), n) : Nat}:
907  match bs:
908    case Nil{}:
909      {==}
910    case Con{h, t}:
911      Equal.trans(Nat, M.cm.blocks.len.go(t, 1n+n), Nat.add(List.length(&2, M.CmBlock, t), 1n+n), 1n+Nat.add(List.length(&2, M.CmBlock, t), n), tr.len_go(t, 1n+n), tr.add_succ(List.length(&2, M.CmBlock, t), n))