law ins_below

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

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

1293# PROOF: by induction on cs. Inserting puts the new candidate (id i < n) at the front, or keeps the head and
1294# inserts into the tail, whose ids are below n by the induction hypothesis.
1295law ins_below:
1296  for +cs: List<&2, Cand>
1297  for +g: Bool
1298  for +v: F32
1299  for +i: Nat
1300  for +n: Nat
1301  for +e: {True{} == below(cs, n) : Bool}
1302  for ei: {True{} == TA.leb(1n+i, n) : Bool}
1303  {True{} == below(ins(cs, g, v, i), n) : Bool}