PROOF.AP.get_set_other.go.body: def of bend-osdev-array@0.1.0.1 Import: import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF Lines 1297-1313 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=1297&end_line=1313 import Base import bend-osdev-array@0.1.0.1/array.bend as A import bend-osdev-u32@0.1.0.0/LAWS.bend as UL def AP.get_set_other.go.body(-T: Data, +d: Nat, -a: Array, h: {A.Arrays.is_perfect(T, d, a) == True{} : Bool}, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}, +i: U32, +j: U32, +v: T, hij: {U32.is_eq(U32.and(i, U32.sub(U32.shln(1, d), 1)), U32.and(j, U32.sub(U32.shln(1, d), 1))) == False{} : Bool}, +t: AP.Tree, +e: {AP.build(T, t) == a : Array}) -> {Pair.snd(Array, T, Array.get(T, Array.set(T, a, i, v), j)) == Pair.snd(Array, T, Array.get(T, a, j)) : T}: +hp = AP.perf_rw(T, d, a, t, e, h) +t2 = AP.set_top(T, t, i, v) +l = A.Arrays.leaves(T, AP.build(T, t)) +ki = A.Arrays.index(d, i) +kj = A.Arrays.index(d, j) +m = U32.sub(U32.shln(1, d), 1) +hk = Equal.trans(Bool, Nat.is_eq(ki, kj), U32.is_eq(U32.and(i, m), U32.and(j, m)), False{}, Equal.sym(Bool, U32.is_eq(U32.and(i, m), U32.and(j, m)), Nat.is_eq(ki, kj), UL.u32_eq_value(U32.and(i, m), U32.and(j, m))), hij) %e : {Pair.snd(Array, T, Array.get(T, Array.set(T, _, i, v), j)) == Pair.snd(Array, T, Array.get(T, _, j)) : T} %Equal.sym(Array, Array.set(T, AP.build(T, t), i, v), AP.build(T, t2), AP.set_top_eq(T, t, i, v)) : {Pair.snd(Array, T, Array.get(T, _, j)) == Pair.snd(Array, T, Array.get(T, AP.build(T, t), j)) : T} %Equal.sym(Array & T, Array.get(T, AP.build(T, t2), j), (AP.build(T, t2), AP.get_top(T, t2, j)), AP.get_top_eq(T, t2, j)) : {Pair.snd(Array, T, _) == Pair.snd(Array, T, Array.get(T, AP.build(T, t), j)) : T} %Equal.sym(Array & T, Array.get(T, AP.build(T, t), j), (AP.build(T, t), AP.get_top(T, t, j)), AP.get_top_eq(T, t, j)) : {AP.get_top(T, t2, j) == Pair.snd(Array, T, _) : T} +e1 = Equal.sym(Maybe<&2, T>, List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t2)), kj), Some{AP.get_top(T, t2, j)}, AP.tree_get(T, d, t2, AP.tree_perf(T, d, t, i, v, hp), hd, j)) +e2 = Equal.cong(List<&2, T>, Maybe<&2, T>, xs => List.get(&2, T, xs, kj), A.Arrays.leaves(T, AP.build(T, t2)), List.set(&2, T, l, ki, v), AP.tree_set(T, d, t, hp, hd, i, v)) +e3 = AP.get_set_other(T, l, ki, kj, v, hk) +e4 = AP.tree_get(T, d, t, hp, hd, j) AP.some_inj(T, AP.get_top(T, t2, j), AP.get_top(T, t, j), Equal.trans(Maybe<&2, T>, Some{AP.get_top(T, t2, j)}, List.get(&2, T, l, kj), Some{AP.get_top(T, t, j)}, Equal.trans(Maybe<&2, T>, Some{AP.get_top(T, t2, j)}, List.get(&2, T, List.set(&2, T, l, ki, v), kj), List.get(&2, T, l, kj), Equal.trans(Maybe<&2, T>, Some{AP.get_top(T, t2, j)}, List.get(&2, T, A.Arrays.leaves(T, AP.build(T, t2)), kj), List.get(&2, T, List.set(&2, T, l, ki, v), kj), e1, e2), e3), e4)) Uses (38): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.set https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong 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.get https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.set 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.is_eq 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=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq 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.sub 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.build https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.get_set_other https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.get_top https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.get_top_eq https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.perf_rw https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.set_top https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.set_top_eq https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.some_inj https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.tree_get https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.tree_perf https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/PROOF.bend&name=AP.tree_set https://jend.leeeet.dev/definition.txt?path=bend-osdev-array@0.1.0.1/array.bend&name=Arrays.index 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-u32@0.1.0.0/LAWS.bend&name=u32_eq_value