proofs/containers/bitset/steps.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/steps.bend as Steps

19 imports

import Base
import ../../../src/math/pow2.bend as P2
import ../../math/pow2/pow2.bend as PT
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../lib/array.bend as A
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/bitset.bend as S
import ../../../src/containers/bitset.bend as B
import ../../../src/containers/types/bitset.bend as E
import ./lists.bend as BL
import ./model.bend as MD
import ./walk.bend as WK
import ./arr.bend as AR
import ./loops.bend as LP
import ./zip.bend as ZP
import ./depth.bend as DP
import ./state.bend as ST

Definitions

def StepOK source · line 29 · raw

@sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> Type

def n_le_cap source · line 34 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> {Nat.is_le(n, Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d), 32n)) == True{} : Bool}

def wix source · line 38 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+i:Nat -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.wordix(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool}

def length_ok source · line 43 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> StepOK(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh{n, d, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Length{})

def nth_in source · line 50 · raw

@+n:Nat -> @+ws:List<&2, U32> -> @+i:Nat -> @+h:{Nat.is_lt(i, n) == True{} : Bool} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws)) == True{} : Bool} -> {Some{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.get_walk(ws, i)} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws), n), i) : Maybe<&2, Bool>}

def nth_out source · line 55 · raw

@+n:Nat -> @+ws:List<&2, U32> -> @+i:Nat -> @+h:{Nat.is_lt(i, n) == False{} : Bool} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws)) == True{} : Bool} -> {None{} == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws), n), i) : Maybe<&2, Bool>}

def get_case source · line 59 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+i:Nat -> @b:Bool -> @+eb:{Nat.is_lt(i, n) == b : Bool} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> StepOK(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh{n, d, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Get{i})

def upd_tree source · line 80 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+i:Nat -> @+v:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>

def upd_ws source · line 83 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+i:Nat -> @+v:Bool -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(upd_tree(d, t, i, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.put_walk(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t), i, v) : List<&2, U32>}

def upd_rep source · line 88 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+i:Nat -> @+v:Bool -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, upd_tree(d, t, i, v)) == True{} : Bool}

def upd_abs source · line 96 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+i:Nat -> @+v:Bool -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> @+hi:{Nat.is_lt(i, n) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, upd_tree(d, t, i, v)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t), i, v) : List<&2, Bool>}

def AssignOK source · line 101 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+i:Nat -> @+v:Bool -> @b:Bool -> Type

def assign_case source · line 104 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+i:Nat -> @+v:Bool -> @b:Bool -> @+eb:{Nat.is_lt(i, n) == b : Bool} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> AssignOK(n, d, t, i, v, b)

def count_abs source · line 123 · raw

@+n:Nat -> @+xs:List<&2, Bool> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(n, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(xs) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.count(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, n)) : Nat}

def members_abs source · line 130 · raw

@+n:Nat -> @+xs:List<&2, Bool> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(n, xs) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.members(xs, 0n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.members(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, xs, n), 0n) : List<&2, Nat>}

def count_ok source · line 137 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> StepOK(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh{n, d, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Count{})

def tolist_ok source · line 147 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> StepOK(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh{n, d, t}, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.ToList{})

def ao_sh source · line 159 · raw

@-n:Nat -> @-d:Nat -> @-t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @-i:Nat -> @-v:Bool -> @-b:Bool -> @r:AssignOK(n, d, t, i, v, b) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh

def ao_res source · line 164 · raw

@-n:Nat -> @-d:Nat -> @-t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @-i:Nat -> @-v:Bool -> @-b:Bool -> @r:AssignOK(n, d, t, i, v, b) -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Error, Unit>

def ao_eq source · line 169 · raw

@-n:Nat -> @-d:Nat -> @-t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @-i:Nat -> @-v:Bool -> @-b:Bool -> @r:AssignOK(n, d, t, i, v, b) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.assign_if(b, n, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t), i, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(ao_sh(n, d, t, i, v, b, r)), ao_res(n, d, t, i, v, b, r)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Error, Unit>)}

def ao_good source · line 174 · raw

@-n:Nat -> @-d:Nat -> @-t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @-i:Nat -> @-v:Bool -> @-b:Bool -> @r:AssignOK(n, d, t, i, v, b) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(ao_sh(n, d, t, i, v, b, r)) == True{} : Bool}

def ao_spec source · line 179 · raw

@-n:Nat -> @-d:Nat -> @-t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @-i:Nat -> @-v:Bool -> @-b:Bool -> @r:AssignOK(n, d, t, i, v, b) -> {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(ao_sh(n, d, t, i, v, b, r)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.OUnit{ao_res(n, d, t, i, v, b, r)}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.assign(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t), i, v) : Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)}

def assign_some source · line 184 · raw

@+n:Nat -> @+ws:List<&2, U32> -> @+i:Nat -> @+v:Bool -> @+h:{Nat.is_lt(i, n) == True{} : Bool} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.invf(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.assign(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws), n), i, v) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.take(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(ws), n), i, v), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.OUnit{Done{Unit{}}}) : Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)}

def lt_add_succ source · line 188 · raw

@+a:Nat -> @+x:Nat -> {Nat.is_lt(a, Nat.add(a, 1n+x)) == True{} : Bool}

def upd_snoc source · line 192 · raw

@+p:List<&2, Bool> -> @+r:List<&2, Bool> -> @+xs:List<&2, Bool> -> @+ea:{xs == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, p, False{} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.rep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, r))) : List<&2, Bool>} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.update(Bool, xs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, p), True{}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, p, True{}), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.rep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, r))) : List<&2, Bool>}

def pick_lt source · line 199 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+p:List<&2, Bool> -> @+r:List<&2, Bool> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> @+ea:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, p, False{} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.rep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, r))) : List<&2, Bool>} -> {Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, p), n) == True{} : Bool}

The index the next bit goes to is inside the bitset.

def PickOK source · line 206 · raw

@b:Bool -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @+p:List<&2, Bool> -> @+r:List<&2, Bool> -> Type

def fill_drop_id source · line 209 · raw

@-s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset -> @x:Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Error, Unit> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.fill_drop(s, x) == s : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset}

def AC source · line 216 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+p:List<&2, Bool> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> AssignOK(n, d, t, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, p), True{}, Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, p), n))

def pick_ok source · line 219 · raw

@b:Bool -> @+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+p:List<&2, Bool> -> @+r:List<&2, Bool> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> @+ea:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, p, False{} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.rep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, r))) : List<&2, Bool>} -> PickOK(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh{n, d, t}, p, r)

def po_sh source · line 241 · raw

@-b:Bool -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-p:List<&2, Bool> -> @-r:List<&2, Bool> -> @z:PickOK(b, sh, p, r) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh

def po_eq source · line 246 · raw

@-b:Bool -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-p:List<&2, Bool> -> @-r:List<&2, Bool> -> @z:PickOK(b, sh, p, r) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.fill_pick(b, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, p)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(po_sh(b, sh, p, r, z)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset}

def po_good source · line 251 · raw

@-b:Bool -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-p:List<&2, Bool> -> @-r:List<&2, Bool> -> @z:PickOK(b, sh, p, r) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(po_sh(b, sh, p, r, z)) == True{} : Bool}

def po_model source · line 256 · raw

@-b:Bool -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @-p:List<&2, Bool> -> @-r:List<&2, Bool> -> @z:PickOK(b, sh, p, r) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(po_sh(b, sh, p, r, z)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.snoc(Bool, p, b), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.rep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, r))) : List<&2, Bool>}

def pick_sh source · line 261 · raw

@b:Bool -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @+p:List<&2, Bool> -> @+r:List<&2, Bool> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(sh) == True{} : Bool} -> @+ea:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(sh) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, p, False{} <> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.rep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, r))) : List<&2, Bool>} -> PickOK(b, sh, p, r)

def FillOK source · line 266 · raw

@zs:List<&2, Bool> -> @+p:List<&2, Bool> -> @sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> Type

def fo_sh source · line 269 · raw

@-zs:List<&2, Bool> -> @-p:List<&2, Bool> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @z:FillOK(zs, p, sh) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh

def fo_eq source · line 274 · raw

@-zs:List<&2, Bool> -> @-p:List<&2, Bool> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @z:FillOK(zs, p, sh) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.fill(zs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, p), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(fo_sh(zs, p, sh, z)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset}

def fo_good source · line 279 · raw

@-zs:List<&2, Bool> -> @-p:List<&2, Bool> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @z:FillOK(zs, p, sh) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(fo_sh(zs, p, sh, z)) == True{} : Bool}

def fo_model source · line 284 · raw

@-zs:List<&2, Bool> -> @-p:List<&2, Bool> -> @-sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @z:FillOK(zs, p, sh) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(fo_sh(zs, p, sh, z)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, p, zs) : List<&2, Bool>}

def fill_ok source · line 289 · raw

@zs:List<&2, Bool> -> @+p:List<&2, Bool> -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(sh) == True{} : Bool} -> @+ea:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(sh) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.append(Bool, p, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.rep(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, zs))) : List<&2, Bool>} -> FillOK(zs, p, sh)

def bool_count_len source · line 307 · raw

@+ys:List<&2, Bool> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bool_count(ys) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(Bool, ys) : Nat}

def FromOK source · line 314 · raw

@ys:List<&2, Bool> -> Type

def from_ok source · line 317 · raw

@+ys:List<&2, Bool> -> @+hf:{Nat.is_le(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bool_count(ys), Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bool_count(ys))), 32n)) == True{} : Bool} -> FromOK(ys)

def ws_len_eq source · line 330 · raw

@+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+tb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+pa:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> @+pb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, tb) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(tb)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.length(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t)) : Nat}

def ztz source · line 335 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+tb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd>

def ws_zip source · line 338 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+tb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+pa:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> @+pb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, tb) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(ztz(k, d, t, tb)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/model.zip_words(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(tb)) : List<&2, U32>}

def zip_flat source · line 345 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+tb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+pa:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> @+pb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, tb) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(ztz(k, d, t, tb))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(t)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.flat(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/arr.ws(tb))) : List<&2, Bool>}

def zip_rep source · line 350 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+tb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> @+gb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, tb) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, ztz(k, d, t, tb)) == True{} : Bool}

def zip_abs source · line 358 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+tb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+pa:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, t) == True{} : Bool} -> @+pb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, d, tb) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, ztz(k, d, t, tb)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, tb)) : List<&2, Bool>}

def CombOK source · line 363 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+ys:List<&2, Bool> -> @+z:List<&2, Bool> -> Type

def comb_at source · line 366 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+tb:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+ys:List<&2, Bool> -> @+z:List<&2, Bool> -> @+ez:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t), ys) == z : List<&2, Bool>} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> @+gb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, tb) == True{} : Bool} -> @+eab:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, tb) == ys : List<&2, Bool>} -> @+etrue:{Nat.is_eq(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bool_count(ys)) == True{} : Bool} -> @+efb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.from_bools(ys) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh{n, d, tb}) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset} -> CombOK(n, d, t, k, ys, z)

def fr_sh source · line 387 · raw

@-ys:List<&2, Bool> -> @z:FromOK(ys) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh

def fr_eq source · line 392 · raw

@-ys:List<&2, Bool> -> @z:FromOK(ys) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.from_bools(ys) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(fr_sh(ys, z)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset}

def fr_good source · line 397 · raw

@-ys:List<&2, Bool> -> @z:FromOK(ys) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(fr_sh(ys, z)) == True{} : Bool}

def fr_model source · line 402 · raw

@-ys:List<&2, Bool> -> @z:FromOK(ys) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(fr_sh(ys, z)) == ys : List<&2, Bool>}

def comb_sh source · line 407 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @shf:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @+ys:List<&2, Bool> -> @+z:List<&2, Bool> -> @+ez:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t), ys) == z : List<&2, Bool>} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> @+gf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(shf) == True{} : Bool} -> @+eaf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(shf) == ys : List<&2, Bool>} -> @+etrue:{Nat.is_eq(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bool_count(ys)) == True{} : Bool} -> @+efb:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.from_bools(ys) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(shf) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset} -> CombOK(n, d, t, k, ys, z)

def comb_false source · line 431 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+ys:List<&2, Bool> -> @+z:List<&2, Bool> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> @+efalse:{Nat.is_eq(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bool_count(ys)) == False{} : Bool} -> CombOK(n, d, t, k, ys, z)

def comb_case source · line 441 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+ys:List<&2, Bool> -> @+z:List<&2, Bool> -> @+ez:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t), ys) == z : List<&2, Bool>} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> @b:Bool -> @+eb:{Nat.is_eq(n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.bool_count(ys)) == b : Bool} -> CombOK(n, d, t, k, ys, z)

def co_sh source · line 450 · raw

@-n:Nat -> @-d:Nat -> @-t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @-k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @-ys:List<&2, Bool> -> @-z:List<&2, Bool> -> @c:CombOK(n, d, t, k, ys, z) -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh

def co_res source · line 455 · raw

@-n:Nat -> @-d:Nat -> @-t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @-k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @-ys:List<&2, Bool> -> @-z:List<&2, Bool> -> @c:CombOK(n, d, t, k, ys, z) -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Error, Unit>

def co_eq source · line 460 · raw

@-n:Nat -> @-d:Nat -> @-t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @-k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @-ys:List<&2, Bool> -> @-z:List<&2, Bool> -> @c:CombOK(n, d, t, k, ys, z) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.comb_bits(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh{n, d, t}), ys) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(co_sh(n, d, t, k, ys, z, c)), co_res(n, d, t, k, ys, z, c)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Error, Unit>)}

def co_good source · line 465 · raw

@-n:Nat -> @-d:Nat -> @-t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @-k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @-ys:List<&2, Bool> -> @-z:List<&2, Bool> -> @c:CombOK(n, d, t, k, ys, z) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(co_sh(n, d, t, k, ys, z, c)) == True{} : Bool}

def co_spec source · line 470 · raw

@-n:Nat -> @-d:Nat -> @-t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @-k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @-ys:List<&2, Bool> -> @-z:List<&2, Bool> -> @c:CombOK(n, d, t, k, ys, z) -> {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(co_sh(n, d, t, k, ys, z, c)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.OUnit{co_res(n, d, t, k, ys, z, c)}) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.combine(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t), ys, z) : Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)}

def CC source · line 475 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+ys:List<&2, Bool> -> @+z:List<&2, Bool> -> @+ez:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t), ys) == z : List<&2, Bool>} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> CombOK(n, d, t, k, ys, z)

def comb_step source · line 478 · raw

@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+ys:List<&2, Bool> -> @+z:List<&2, Bool> -> @+ez:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/lists.zipk(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t), ys) == z : List<&2, Bool>} -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh, sh2 => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs, o => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.obs_unit(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.comb_bits(k, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh{n, d, t}), ys)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(sh2), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(sh2) == True{} : Bool}, {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(sh2), o) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.combine(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t), ys, z) : Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)}))>>

def assign_step source · line 487 · raw

@+n:Nat -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd> -> @+i:Nat -> @+v:Bool -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.rep(n, d, t) == True{} : Bool} -> Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh, sh2 => Sigma<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs, o => Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.obs_unit(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.assign(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.BS{n, d, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Wd, t)}, i, v)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(sh2), o) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)}, Pair({0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(sh2) == True{} : Bool}, {(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(sh2), o) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.assign(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.abs(n, t), i, v) : Pair(List<&2, Bool>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Obs)}))>>

def step_ok source · line 499 · raw

@sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(sh) == True{} : Bool} -> StepOK(sh, op)