law pick_below

bend-ml-llama@0.2.1.0 · main.bend:1362

import Base
import bend-ml-tensor-array@0.1.19.0/main.bend as TA

1362# PROOF: by induction on cs: the draw returns a candidate of cs, whose id is below n, or id 0 < n when cs is empty.
1363law pick_below:
1364  for +cs: List<&2, Cand>
1365  for +s: Bool
1366  for +q: Nat
1367  for +temp: F32
1368  for +top: F32
1369  for +target: F32
1370  for +acc: F32
1371  for +n: Nat
1372  for +e: {True{} == below(cs, n) : Bool}
1373  for pos: {True{} == TA.leb(1n, n) : Bool}
1374  {True{} == TA.leb(1n+Cand.i(pick.go(cs, s, q, temp, top, target, acc)), n) : Bool}