def AP.of_list_get.go

bend-osdev-array@0.1.0.1 · PROOF.bend:1518

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

1518def AP.of_list_get.go(-T: Data, +d: Nat, +xs: List<&2, T>, +f: T, +hl: {List.length(&2, T, xs) == A.Arrays.slots(d) : Nat}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32) -> {Array.get(T, A.Arrays.of_list(T, d, xs, f), i) == (A.Arrays.of_list(T, d, xs, f), A.Arrays.nth(T, xs, A.Arrays.index(d, i), f)) : Array<T> & T}:
1519  +t = AP.tof(T, d, xs, f)
1520  +k = A.Arrays.index(d, i)
1521  +g = AP.get_top(T, t, i)
1522  +el = AP.tof_leaves(T, d, xs, f, hl)
1523  +eg = Equal.trans(Maybe<&2, T>, List.get(&2, T, xs, k), List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), k), Some{g}, Equal.cong(List<&2, T>, Maybe<&2, T>, ys => List.get(&2, T, ys, k), xs, A.Arrays.leaves(T, AP.build(T, t)), Equal.sym(List<&2, T>, A.Arrays.leaves(T, AP.build(T, t)), xs, el)), AP.tree_get(T, d, t, AP.tof_perf(T, d, xs, f), hd, i))
1524  %AP.ol_sym(T, d, xs, f) : {Array.get(T, _, i) == (_, A.Arrays.nth(T, xs, k, f)) : Array<T> & T}
1525  %Equal.sym(Array<T> & T, Array.get(T, AP.build(T, t), i), (AP.build(T, t), g), AP.get_top_eq(T, t, i)) : {_ == (AP.build(T, t), A.Arrays.nth(T, xs, k, f)) : Array<T> & T}
1526  %AP.nth_get(T, xs, k, f, g, eg) : {(AP.build(T, t), _) == (AP.build(T, t), A.Arrays.nth(T, xs, k, f)) : Array<T> & T}
1527  {==}