def tr.len_go

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:506

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

506def 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}:
507  match bs:
508    case Nil{}:
509      {==}
510    case Con{h, t}:
511      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), UL.nat_add_succ(List.length(&2, M.CmBlock, t), n))