PROOF.get_put_other: def of bend-kit-collections@0.1.4.1 Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF Lines 974-1037 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=974&end_line=1037 import Base import bend-kit-collections@0.1.4.1/LAWS.bend as Laws import bend-kit-collections@0.1.4.1/omap.bend as O def get_put_other( ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), t: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k2: K, +k: K, +v: V, +bt: {Laws.bounded(~K, ~V, ~cmp, t, lb, ub) == True{} : Bool}, +ea: {Laws.above(~K, ~cmp, lb, k2) == True{} : Bool}, +eb: {Laws.below(~K, ~cmp, ub, k2) == True{} : Bool}, +nef: {Cmp.is_eq(cmp(k2, k)) == False{} : Bool} ) -> {g(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, t, k2, v), k) == g(~K, ~V, ~cmp, t, k) : Maybe<&2, V>}: match t: case O.OTip{}: split(c => {getc(~K, ~V, ~cmp, c, k, v, O.OTip{}, O.OTip{}) == None{} : Maybe<&2, V>}, cmp(k, k2), e => {==}, e => ne_absurd({Some{v} == None{} : Maybe<&2, V>}, cmp(k2, k), nef, eq_flip(~K, ~cmp, ~flip, k, k2, e)), e => {==}) case O.OBin{+s, +key, +val, +lo, +hi}: +b_l = bn.l(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) +b_h = bn.h(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) +plo = O.OMap.put(~K, ~V, ~cmp, lo, k2, v) +phi = O.OMap.put(~K, ~V, ~cmp, hi, k2, v) +old = {O.OBin{s, key, val, lo, hi} : O.OMap} cmp.split(O.OMap, Maybe<&2, V>, y => g(~K, ~V, ~cmp, y, k), g(~K, ~V, ~cmp, old, k), cmp(k2, key), u => O.OMap.balance(K, V, key, val, O.OMap.put(~K, ~V, ~cmp, lo, k2, v), hi), u => O.OBin{s, key, v, lo, hi}, u => O.OMap.balance(K, V, key, val, lo, O.OMap.put(~K, ~V, ~cmp, hi, k2, v)), +e => mtr(V, g(~K, ~V, ~cmp, O.OMap.balance(K, V, key, val, plo, hi), k), g(~K, ~V, ~cmp, O.OBin{0, key, val, plo, hi}, k), g(~K, ~V, ~cmp, old, k), balance.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lb, ub, k, key, val, plo, hi, put.bnd(~K, ~V, ~cmp, ~flip, ~trans, lo, lb, Some{key}, k2, v, b_l, ea, lt_true(cmp(k2, key), e)), b_h), split(c => {getc(~K, ~V, ~cmp, c, k, val, plo, hi) == getc(~K, ~V, ~cmp, c, k, val, lo, hi) : Maybe<&2, V>}, cmp(k, key), e2 => get_put_other(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lo, lb, Some{key}, k2, k, v, b_l, ea, lt_true(cmp(k2, key), e), nef), e2 => {==}, e2 => {==})), +e => split(c => {getc(~K, ~V, ~cmp, c, k, v, lo, hi) == getc(~K, ~V, ~cmp, c, k, val, lo, hi) : Maybe<&2, V>}, cmp(k, key), e2 => {==}, e2 => ne_absurd({Some{v} == Some{val} : Maybe<&2, V>}, cmp(k2, k), nef, rw(K, y => {cmp(y, k) == EQ{} : Cmp}, k2, key, eq(k2, key, e), eq_flip(~K, ~cmp, ~flip, k, key, e2))), e2 => {==}), +e => mtr(V, g(~K, ~V, ~cmp, O.OMap.balance(K, V, key, val, lo, phi), k), g(~K, ~V, ~cmp, O.OBin{0, key, val, lo, phi}, k), g(~K, ~V, ~cmp, old, k), balance.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lb, ub, k, key, val, lo, phi, b_l, put.bnd(~K, ~V, ~cmp, ~flip, ~trans, hi, Some{key}, ub, k2, v, b_h, lt_true(cmp(key, k2), gt_flip(~K, ~cmp, ~flip, k2, key, e)), eb)), split(c => {getc(~K, ~V, ~cmp, c, k, val, lo, phi) == getc(~K, ~V, ~cmp, c, k, val, lo, hi) : Maybe<&2, V>}, cmp(k, key), e2 => {==}, e2 => {==}, e2 => get_put_other(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, hi, Some{key}, ub, k2, k, v, b_h, lt_true(cmp(key, k2), gt_flip(~K, ~cmp, ~flip, k2, key, e)), eb, nef)))) Uses (28): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=above https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=below https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&name=bounded https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=Eq https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=Flip https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=Refl https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=Trans https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=balance.get https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=bn.h https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=bn.l https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=cmp.split https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=eq_flip https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=g https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=getc https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=gt_flip https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=lt_true https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=mtr https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=ne_absurd https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=put.bnd https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=rw https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=split https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap.balance https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap.put