~/bend-docscommunity

proofs/END_TO_END.bend checks

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

48 imports
import Base
import ./lib/array.bend as AR
import ./lib/logic.bend as L
import ../spec/lib/common.bend as SC
import ../src/containers/dynamic_array.bend as DA
import ../spec/containers/dynamic_array.bend as DAS
import ../src/containers/types/dynamic_array.bend as DAT
import ./containers/dynamic_array/proof.bend as DAP
import ./containers/dynamic_array/state.bend as DAST
import ../src/containers/deque.bend as DQ
import ../spec/containers/deque.bend as DQS
import ../src/containers/types/deque.bend as DQT
import ./containers/deque/proof.bend as DQP
import ./containers/deque/state.bend as DQSH
import ./containers/deque/stepok.bend as DQK
import ./containers/deque/trace.bend as DQTR
import ../src/containers/queue.bend as QU
import ../spec/containers/queue.bend as QUS
import ../src/containers/types/queue.bend as QUT
import ./containers/queue/proof.bend as QUP
import ./containers/queue/state.bend as QUSH
import ./containers/queue/steps.bend as QUST
import ./containers/queue/trace.bend as QUTR
import ./lib/order.bend as O
import ../src/containers/binary_heap.bend as BH
import ../spec/containers/binary_heap.bend as BHS
import ../src/containers/types/binary_heap.bend as BHT
import ./containers/binary_heap/proof.bend as BHP
import ./containers/binary_heap/state.bend as BHSH
import ./containers/binary_heap/steps.bend as BHST
import ./containers/binary_heap/trace.bend as BHTR
import ../src/containers/bitset.bend as BI
import ../spec/lib/common.bend as SCOM
import ../spec/containers/bitset.bend as BIS
import ../src/containers/types/bitset.bend as BIT
import ./containers/bitset/proof.bend as BIP
import ./containers/bitset/state.bend as BIST
import ./containers/bitset/steps.bend as BISP
import ./containers/bitset/trace.bend as BITR
import ../src/containers/bitlist.bend as BLI
import ../src/containers/types/bitlist.bend as BLT
import ../spec/containers/bitlist.bend as BLS
import ./containers/bitlist/state.bend as BLST
import ./containers/bitlist/steps.bend as BLSP
import ./containers/bitlist/trace.bend as BLTR
import ./containers/bitlist/proof.bend as BLP
import ../spec/containers/balanced_search_tree/recursive.bend as BTS
import ../src/containers/types/balanced_search_tree.bend as BTT

Laws

law array_get_after_set_same provedsource · line 56 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T> -> @+i:U32 -> @+v:T -> @+x:T -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(U32.to_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(T, d, t) == True{} : Bool} -> {Array.get(T, Array.set(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(T, t), i, v), i) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(T, d, t, U32.to_nat(i), v)), v) : Pair(Array<T>, T)}

law array_get_after_set_other provedsource · line 71 · raw

@-T:Data -> @+d:Nat -> @+t:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.Tree<T> -> @+i:U32 -> @+j:U32 -> @+v:T -> @+x:T -> @+y:T -> @+hd:{Nat.is_lt(d, 32n) == True{} : Bool} -> @+hi:{Nat.is_lt(U32.to_nat(i), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+hj:{Nat.is_lt(U32.to_nat(j), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(d)) == True{} : Bool} -> @+ne:{Nat.is_eq(U32.to_nat(i), U32.to_nat(j)) == False{} : Bool} -> @+hx:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(T, t), U32.to_nat(i)) == Some{x} : Maybe<&2, T>} -> @+hy:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.nth(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.slots(T, t), U32.to_nat(j)) == Some{y} : Maybe<&2, T>} -> @+pf:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.perfect(T, d, t) == True{} : Bool} -> {Array.get(T, Array.set(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(T, t), i, v), j) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.upd(T, d, t, U32.to_nat(i), v)), y) : Pair(Array<T>, T)}

law array_new provedsource · line 91 · raw

@-T:Data -> @+d:Nat -> @+v:T -> {Array.new(T, d, v) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.thaw(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/array.trep(T, d, v)) : Array<T>}

law dynamic_array_new provedsource · line 101 · raw

@-T:Data -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new(T)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(T) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>}

law dynamic_array_new_invariant provedsource · line 107 · raw

@-T:Data -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new(T))

law dynamic_array_with_limit provedsource · line 113 · raw

@-T:Data -> @+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit(T, k)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(T, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>}

law dynamic_array_step provedsource · line 120 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, sh) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view1(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh), op)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh)), op) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)}

law dynamic_array_step_invariant provedsource · line 129 · raw

@-T:Data -> @+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<T> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(T, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(T, sh), op)))

law dynamic_array_trace provedsource · line 138 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new(T))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(T)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)}

law dynamic_array_trace_invariant provedsource · line 145 · raw

@-T:Data -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new(T))))

law dynamic_array_trace_limited provedsource · line 152 · raw

@-T:Data -> @+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit(T, k))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(T, k)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)}

law dynamic_array_trace_limited_invariant provedsource · line 160 · raw

@-T:Data -> @+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run(T, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit(T, k))))

law dynamic_array_new_at_u32 provedsource · line 174 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(U32)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(U32) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>}

law dynamic_array_new_at_invariant_u32 provedsource · line 179 · raw

0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(U32))

law dynamic_array_with_limit_at_u32 provedsource · line 184 · raw

@+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(U32, k)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(U32, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>}

law dynamic_array_step_at_u32 provedsource · line 190 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, sh) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view1(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, sh), op)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.step(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, sh)), op) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>)}

law dynamic_array_step_at_invariant_u32 provedsource · line 198 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<U32> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(U32, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(U32, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(U32, sh), op)))

law dynamic_array_trace_at_u32 provedsource · line 206 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<U32>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(U32, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(U32))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(U32, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(U32)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>>)}

law dynamic_array_trace_at_invariant_u32 provedsource · line 212 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<U32>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(U32, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(U32, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(U32))))

law dynamic_array_trace_limited_at_u32 provedsource · line 218 · raw

@+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<U32>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(U32, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(U32, k))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(U32, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(U32, k)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<U32>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>>)}

law dynamic_array_trace_limited_at_invariant_u32 provedsource · line 225 · raw

@+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<U32>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(U32, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<U32>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(U32, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(U32, k))))

law dynamic_array_new_at_nat provedsource · line 232 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(Nat)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(Nat) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<Nat>}

law dynamic_array_new_at_invariant_nat provedsource · line 237 · raw

0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(Nat))

law dynamic_array_with_limit_at_nat provedsource · line 242 · raw

@+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(Nat, k)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(Nat, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<Nat>}

law dynamic_array_step_at_nat provedsource · line 248 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<Nat> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<Nat> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(Nat, sh) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view1(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(Nat, sh), op)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.step(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(Nat, sh)), op) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<Nat>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<Nat>)}

law dynamic_array_step_at_invariant_nat provedsource · line 256 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<Nat> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<Nat> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(Nat, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(Nat, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Nat>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<Nat>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(Nat, sh), op)))

law dynamic_array_trace_at_nat provedsource · line 264 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<Nat>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(Nat, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(Nat))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(Nat, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(Nat)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<Nat>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<Nat>>)}

law dynamic_array_trace_at_invariant_nat provedsource · line 270 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<Nat>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(Nat, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Nat>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<Nat>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(Nat, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(Nat))))

law dynamic_array_trace_limited_at_nat provedsource · line 276 · raw

@+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<Nat>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view(Nat, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(Nat, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(Nat, k))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(Nat, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(Nat, k)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<Nat>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<Nat>>)}

law dynamic_array_trace_limited_at_invariant_nat provedsource · line 283 · raw

@+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<Nat>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(Nat, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, Nat>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<Nat>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(Nat, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(Nat, k))))

law dynamic_array_new_at_string provedsource · line 290 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(String)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(String) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<String>}

law dynamic_array_new_at_invariant_string provedsource · line 295 · raw

0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(String))

law dynamic_array_with_limit_at_string provedsource · line 300 · raw

@+k:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(String, k)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(String, k) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<String>}

law dynamic_array_step_at_string provedsource · line 306 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<String> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<String> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(String, sh) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view1(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(String, sh), op)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.step(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.abs(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(String, sh)), op) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<String>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<String>)}

law dynamic_array_step_at_invariant_string provedsource · line 314 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Shadow<String> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<String> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.good(String, sh) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(String, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, String>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<String>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.step_at(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.real(String, sh), op)))

law dynamic_array_trace_at_string provedsource · line 322 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<String>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(String, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(String))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(String, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.new(String)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<String>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<String>>)}

law dynamic_array_trace_at_invariant_string provedsource · line 328 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<String>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(String, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, String>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<String>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(String, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_at(String))))

law dynamic_array_trace_limited_at_string provedsource · line 334 · raw

@+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<String>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/proof.view(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(String, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(String, k))) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.run(String, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.with_limit(String, k)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/dynamic_array.Model<String>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<String>>)}

law dynamic_array_trace_limited_at_invariant_string provedsource · line 341 · raw

@+k:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<String>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/dynamic_array/state.Inv(String, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, String>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<String>>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.run_at(String, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.with_limit_at(String, k))))

law deque_u32_new provedsource · line 353 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.initial(U32)) == [] : List<&2, U32>}

law deque_u32_new_is_the_constructor provedsource · line 358 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.new(U32) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.initial(U32)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<U32>}

law deque_u32_step provedsource · line 363 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<U32> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<U32> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(U32, sh, op)

law deque_u32_shadow_unique provedsource · line 370 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<U32> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<U32> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(U32, a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(U32, b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<U32>} -> {a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<U32>}

law deque_u32_trace provedsource · line 378 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<U32>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/trace.TraceOK(U32, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.initial(U32))

law deque_string_new provedsource · line 384 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.model(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.initial(String)) == [] : List<&2, String>}

law deque_string_new_is_the_constructor provedsource · line 389 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.new(String) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.initial(String)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<String>}

law deque_string_step provedsource · line 394 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<String> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<String> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/stepok.StepOK(String, sh, op)

law deque_string_shadow_unique provedsource · line 401 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<String> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<String> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(String, a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.real(String, b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/deque.Deque<String>} -> {a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.Shadow<String>}

law deque_string_trace provedsource · line 409 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/deque.Op<String>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/trace.TraceOK(String, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/deque/state.initial(String))

law queue_u32_new provedsource · line 419 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.initial(U32)) == [] : List<&2, U32>}

law queue_u32_new_is_the_constructor provedsource · line 424 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.new(U32) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.initial(U32)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<U32>}

law queue_u32_step provedsource · line 429 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<U32> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Op<U32> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/steps.StepOK(U32, sh, op)

law queue_u32_shadow_unique provedsource · line 436 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<U32> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<U32> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(U32, a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(U32, b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<U32>} -> {a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<U32>}

law queue_u32_trace provedsource · line 444 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Op<U32>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/trace.TraceOK(U32, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.initial(U32))

law queue_string_new provedsource · line 450 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.model(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.initial(String)) == [] : List<&2, String>}

law queue_string_new_is_the_constructor provedsource · line 455 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.new(String) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.initial(String)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<String>}

law queue_string_step provedsource · line 460 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<String> -> @+op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Op<String> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/steps.StepOK(String, sh, op)

law queue_string_shadow_unique provedsource · line 467 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<String> -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<String> -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(String, a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.real(String, b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/queue.Queue<String>} -> {a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.Shadow<String>}

law queue_string_trace provedsource · line 475 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/queue.Op<String>> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/trace.TraceOK(String, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/queue/state.initial(String))

law binary_heap_u32_new provedsource · line 489 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(U32)) == [] : List<&2, U32>}

law binary_heap_u32_new_good provedsource · line 494 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(U32)) == True{} : Bool}

law binary_heap_u32_new_is_the_constructor provedsource · line 499 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.new(U32) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(U32)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<U32>}

law binary_heap_u32_abstraction_of_a_real_heap provedsource · line 504 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.abs(U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(U32, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(U32, U32.cmp, sh) : List<&2, U32>}

law binary_heap_string_new provedsource · line 510 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(String, String.order, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(String)) == [] : List<&2, String>}

law binary_heap_string_new_is_the_constructor provedsource · line 515 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.new(String) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(String, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(String)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.Heap<String>}

law binary_heap_string_abstraction_of_a_real_heap provedsource · line 520 · raw

@+sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<String> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.abs(String, String.order, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.real(String, sh)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.model(String, String.order, sh) : List<&2, String>}

law binary_heap_u32_step provedsource · line 526 · raw

@sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<U32> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<U32> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(U32, U32.cmp, sh) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(U32, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.pushcost(U32, op)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(U32, U32.cmp, sh, op)

law binary_heap_u32_trace provedsource · line 537 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<U32>> -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.pushes(U32, ops), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.TraceOK(U32, U32.cmp, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(U32))

law binary_heap_u32_new_invariant provedsource · line 546 · raw

0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Inv(U32, U32.cmp, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.new(U32))

law binary_heap_string_step provedsource · line 551 · raw

@sh:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Shadow<String> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<String> -> @+g:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.good(String, String.order, sh) == True{} : Bool} -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(Nat.add(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.sh_size(String, sh), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.pushcost(String, op)), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/steps.StepOK(String, String.order, sh, op)

law binary_heap_string_trace provedsource · line 562 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/binary_heap.Op<String>> -> @+q:Nat -> @+hq:{Nat.is_le(q, 31n) == True{} : Bool} -> @+room:{Nat.is_lt(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.pushes(String, ops), 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(q)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/trace.TraceOK(String, String.order, ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.initial(String))

law binary_heap_string_new_invariant provedsource · line 571 · raw

0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/binary_heap/state.Inv(String, String.order, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/binary_heap.new(String))

law bitset_new provedsource · line 578 · raw

@+n:Nat -> @+h:{Nat.is_le(n, Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)), 32n)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.model(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/trace.initial(n)) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitset.new(n) : List<&2, Bool>}

law bitset_new_invariant provedsource · line 585 · raw

@+n:Nat -> @+h:{Nat.is_le(n, Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)), 32n)) == True{} : Bool} -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.good(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/trace.initial(n)) == True{} : Bool}

law bitset_new_is_the_constructor provedsource · line 592 · raw

@+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.new(n) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/trace.initial(n)) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset}

law bitset_from_bools provedsource · line 598 · 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} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/steps.FromOK(ys)

law bitset_step provedsource · line 605 · 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} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/steps.StepOK(sh, op)

law bitset_shadow_unique provedsource · line 613 · raw

@+a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @+b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh -> @+e:{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(a) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.real(b) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.Bitset} -> {a == b : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/state.Sh}

law bitset_trace provedsource · line 621 · raw

@+n:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitset.Op> -> @+h:{Nat.is_le(n, Nat.mul(0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/lib/common.pow2(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.depth_for(n)), 32n)) == True{} : Bool} -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/trace.TraceOK(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitset/trace.initial(n))

law bitlist_new_is_the_constructor provedsource · line 641 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.new == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.real(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(None{})) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitlist.Bitlist}

law bitlist_new provedsource · line 646 · raw

{0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(None{})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.new : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model}

law bitlist_with_limit provedsource · line 651 · raw

@+n:Nat -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/state.model(0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(Some{n})) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.with_limit(n) : 0x5c489f5d9646d7cc9aa3dd8137e9dc07/spec/containers/bitlist.Model}

law bitlist_step provedsource · line 657 · raw

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

law bitlist_trace provedsource · line 665 · raw

@+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.TraceOK(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(None{}))

law bitlist_trace_limited provedsource · line 671 · raw

@+n:Nat -> @+ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/bitlist.Op> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.TraceOK(ops, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(Some{n}))

law bitlist_from_bools provedsource · line 678 · raw

@+bs:List<&2, Bool> -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.FromOK(bs, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/containers/bitlist/trace.initial(None{}))