PROOF.AP.set_leaves: def of bend-osdev-array@0.1.0.1 Import: import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF Lines 1108-1146 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=1108&end_line=1146 import Base import bend-osdev-array@0.1.0.1/array.bend as A def AP.set_leaves(-T: Data, +d: Nat, +t: AP.Tree, +i: U32, +v: T, 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}) -> {A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, t, U32.shln(1, d), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, t)), U32.to_nat(i), v) : List<&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)) : {Con{v, Nil{}} == List.set(&2, T, Con{x, Nil{}}, _, v) : List<&2, T>} {==} case 0n APNode{xs, ys} _: Empty.absurd({A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, APNode{xs, ys}, U32.shln(1, 0n), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, APNode{xs, ys})), U32.to_nat(i), v) : List<&2, T>}, AP.ft(hp)) case 1n+p APLeaf{x} _: Empty.absurd({A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, APLeaf{x}, U32.shln(1, 1n+p), i, v, b))) == List.set(&2, T, A.Arrays.leaves(T, AP.build(T, APLeaf{x})), U32.to_nat(i), v) : List<&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)) +k = U32.to_nat(i) +z1 = U32.is_lt(i, U32.shr(sh)) +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(k, 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.append(&2, T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, _, i, v, U32.is_lt(i, U32.shr(_))))), ly) == List.set(&2, T, List.append(&2, T, lx, ly), k, v) : List<&2, T>} Equal.trans(List<&2, T>, List.append(&2, T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, sh, i, v, z1))), ly), List.append(&2, T, List.set(&2, T, lx, k, v), ly), List.set(&2, T, List.append(&2, T, lx, ly), k, v), AP.app_cong_l(T, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, xs, sh, i, v, z1))), List.set(&2, T, lx, k, v), ly, AP.set_leaves(T, p, xs, i, v, z1, {==}, hd1, hpx, hi1)), Equal.sym(List<&2, T>, List.set(&2, T, List.append(&2, T, lx, ly), k, v), List.append(&2, T, List.set(&2, T, lx, k, v), ly), AP.set_app_l(T, lx, ly, k, v, hl))) 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) +z1 = U32.is_lt(j, U32.shr(sh)) +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.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, _, U32.sub(i, _), v, U32.is_lt(U32.sub(i, _), U32.shr(_)))))) == List.set(&2, T, List.append(&2, T, lx, ly), U32.to_nat(i), v) : List<&2, T>} %hs : {List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))) == List.set(&2, T, List.append(&2, T, lx, ly), _, v) : List<&2, T>} %AP.len_perf(T, p, xs, hpx) : {List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))) == List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(_, w), v) : List<&2, T>} Equal.trans(List<&2, T>, List.append(&2, T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1)))), List.append(&2, T, lx, List.set(&2, T, ly, w, v)), List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w), v), AP.app_cong_r(T, lx, A.Arrays.leaves(T, AP.build(T, AP.swap_t(T, ys, sh, j, v, z1))), List.set(&2, T, ly, w, v), AP.set_leaves(T, p, ys, j, v, z1, {==}, hd1, hpy, hj)), Equal.sym(List<&2, T>, List.set(&2, T, List.append(&2, T, lx, ly), Nat.add(List.length(&2, T, lx), w), v), List.append(&2, T, lx, List.set(&2, T, ly, w, v)), AP.set_app_r(T, lx, ly, w, v))) Uses (41): 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.length https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.set 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.app_cong_l https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.app_cong_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.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.set_app_l https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.set_app_r 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/PROOF.bend&name=AP.swap_t 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