law topk_below
import bend-ml-llama@0.2.1.0/main.bend as BendMlLlamaimport Base
1335# PROOF: by induction on xs, with i + length(xs) = n: the head of xs has id i < n (step_room), and after it
1336# 1 + i + length(tail) = n still holds (step_inv); ins_below and take_below keep the candidates' ids below n.
1337law topk_below:
1338 for +xs: List<&2, F32>
1339 for +g: Bool
1340 for +k: Nat
1341 for +i: Nat
1342 for +m: Nat
1343 for +lo: F32
1344 for +cs: List<&2, Cand>
1345 for +n: Nat
1346 for +inv: {Nat.add(i, List.length(&2, F32, xs)) == n : Nat}
1347 for +e: {True{} == below(cs, n) : Bool}
1348 {True{} == below(topk.go(xs, g, k, i, m, lo, cs), n) : Bool}