def bs.head_le

bend-osdev-algo@0.1.0.0 · PROOF.bend:1069

import Base
import bend-osdev-algo@0.1.0.0/bsearch.bend as S

1069# the head of a sorted list is at most each of its elements
1070def bs.head_le(t: List<&2, U32>, +x0: U32, s: {S.bsearch.sorted.pair(t, x0) == True{} : Bool}, i: Nat, +x: U32, e: {List.get(&2, U32, t, i) == Some{x} : Maybe<&2, U32>}) -> {U32.is_le(x0, x) == True{} : Bool}:
1071  match t i:
1072    case Nil{} _:
1073      Empty.absurd({U32.is_le(x0, x) == True{} : Bool}, absurd.ns32(x, e))
1074    case Con{+y, tt} 0n:
1075      %some_inj32(y, x, e) : {U32.is_le(x0, _) == True{} : Bool}
1076      bool.and_l(U32.is_le(x0, y), S.bsearch.sorted.pair(tt, y), s)
1077    case Con{+y, +tt} 1n+ip:
1078      +s2 = s
1079      u32.le_trans(x0, y, x, bool.and_l(U32.is_le(x0, y), S.bsearch.sorted.pair(tt, y), s2), bs.head_le(tt, y, bool.and_r(U32.is_le(x0, y), S.bsearch.sorted.pair(tt, y), s2), ip, x, e))