PROOF.AP.get_leaves: def of bend-osdev-array@0.1.0.1 Import: import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF Lines 1070-1106 of bend-osdev-array@0.1.0.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&start_line=1070&end_line=1106 import Base import bend-osdev-array@0.1.0.1/array.bend as A def AP.get_leaves(-T: Data, +d: Nat, +t: AP.Tree, +i: U32, b: Bool, +eb: {U32.is_lt(i, U32.shr(U32.shln(1, d))) == b : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +hp: {A.Arrays.is_perfect(T, d, AP.build(T, t)) == True{} : Bool}, +hi: {Nat.is_lt(U32.to_nat(i), A.Arrays.slots(d)) == True{} : Bool}) -> {List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t)), U32.to_nat(i)) == Some{AP.get_v(T, t, U32.shln(1, d), i, b)} : Maybe<&2, T>}: match d t b: case 0n APLeaf{+x} _: %Equal.sym(Nat, U32.to_nat(i), 0n, AP.lt_one(U32.to_nat(i), hi)) : {List.get(&2, T, Con{x, Nil{}}, _) == Some{x} : Maybe<&2, T>} {==} case 0n APNode{xs, ys} _: Empty.absurd({List.get(&2, T, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys})), U32.to_nat(i)) == Some{AP.get_v(T, APNode{xs, ys}, U32.shln(1, 0n), i, b)} : Maybe<&2, T>}, AP.ft(hp)) case 1n+p APLeaf{x} _: Empty.absurd({List.get(&2, T, A.Arrays.leaves(T, AP.build(T, APLeaf{x})), U32.to_nat(i)) == Some{AP.get_v(T, APLeaf{x}, U32.shln(1, 1n+p), i, b)} : Maybe<&2, T>}, AP.ft(hp)) case 1n+ +p APNode{xs, ys} True{}: +hd1 = AP.lt_succ_l(p, 32n, hd) +s = A.Arrays.slots(p) +sh = U32.shln(1, p) +lx = A.Arrays.leaves(T, AP.build(T, xs)) +ly = A.Arrays.leaves(T, AP.build(T, ys)) +v = U32.to_nat(i) +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp) +hi1 = AP.lt_true(i, p, hd1, AP.eb_fix(i, p, True{}, hd, eb)) +hl = AP.lt_rw_r(v, List.length(&2, T, lx), s, AP.len_perf(T, p, xs, hpx), hi1) %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.get(&2, T, List.append(&2, T, lx, ly), v) == Some{AP.get_v(T, xs, _, i, U32.is_lt(i, U32.shr(_)))} : Maybe<&2, T>} Equal.trans(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, lx, ly), v), List.get(&2, T, lx, v), Some{AP.get_v(T, xs, sh, i, U32.is_lt(i, U32.shr(sh)))}, AP.get_app_l(T, lx, ly, v, hl), AP.get_leaves(T, p, xs, i, U32.is_lt(i, U32.shr(sh)), {==}, hd1, hpx, hi1)) case 1n+ +p APNode{xs, ys} False{}: +hd1 = AP.lt_succ_l(p, 32n, hd) +s = A.Arrays.slots(p) +sh = U32.shln(1, p) +lx = A.Arrays.leaves(T, AP.build(T, xs)) +ly = A.Arrays.leaves(T, AP.build(T, ys)) +j = U32.sub(i, sh) +w = U32.to_nat(j) +hpx = AP.and_l(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp) +hpy = AP.and_r(A.Arrays.is_perfect(T, p, AP.build(T, xs)), A.Arrays.is_perfect(T, p, AP.build(T, ys)), hp) +hs = AP.split(i, p, hd1, AP.eb_fix(i, p, False{}, hd, eb)) +hj = AP.lt_split2(w, s, AP.lt_rw_l(Nat.add(s, w), U32.to_nat(i), Nat.double(s), hs, hi)) %Equal.sym(U32, U32.shr(U32.shln(1, 1n+p)), sh, AP.shr_shln(p, hd)) : {List.get(&2, T, List.append(&2, T, lx, ly), U32.to_nat(i)) == Some{AP.get_v(T, ys, _, U32.sub(i, _), U32.is_lt(U32.sub(i, _), U32.shr(_)))} : Maybe<&2, T>} %hs : {List.get(&2, T, List.append(&2, T, lx, ly), _) == Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))} : Maybe<&2, T>} %AP.len_perf(T, p, xs, hpx) : {List.get(&2, T, List.append(&2, T, lx, ly), Nat.add(_, w)) == Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))} : Maybe<&2, T>} Equal.trans(Maybe<&2, T>, List.get(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w)), List.get(&2, T, ly, w), Some{AP.get_v(T, ys, sh, j, U32.is_lt(j, U32.shr(sh)))}, AP.get_app_r(T, lx, ly, w), AP.get_leaves(T, p, ys, j, U32.is_lt(j, U32.shr(sh)), {==}, hd1, hpy, hj)) Uses (40): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.get https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.Tree https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.and_l https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.and_r https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.build https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.eb_fix https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.ft https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.get_app_l https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.get_app_r https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.get_v https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.len_perf https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.lt_one https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.lt_rw_l https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.lt_rw_r https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.lt_split2 https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.lt_succ_l https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.lt_true https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.shr_shln https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.split https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.is_perfect https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.leaves https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.slots