def g_count

bend-osdev-bpf@0.1.0.0 · PROOF.bend:206

import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I
import bend-osdev-bpf@0.1.0.0/validate.bend as V

206def g_count(+xs: List<&2, I.BpfOp>, +n: Nat) -> {V.bpf_count.go(xs, n) == Nat.add(List.length(&2, I.BpfOp, xs), n) : Nat}:
207  match xs:
208    case Nil{}:
209      {==}
210    case Con{h, t}:
211      Equal.trans(Nat, V.bpf_count.go(t, 1n+n), Nat.add(List.length(&2, I.BpfOp, t), 1n+n), 1n+Nat.add(List.length(&2, I.BpfOp, t), n),
212        g_count(t, 1n+n), add_succ(List.length(&2, I.BpfOp, t), n))