~/bend-docscommunity

proofs/containers/balanced_search_tree/setters.bend source

proofs/containers/balanced_search_tree/setters.bend on the hub · documented module

import Baseimport ../../lib/logic.bend as Limport ../../lib/nat.bend as Nimport ../../lib/order.bend as Oimport ../../../spec/lib/common.bend as SCimport ../../../src/containers/balanced_search_tree.bend as Mimport ./state.bend as STimport ./prim.bend as PRimport ./mirror.bend as MIimport ./frame.bend as FRimport ./agree.bend as AGimport ../../../spec/containers/balanced_search_tree/main.bend as Simport ./ends.bend as ENimport ./path.bend as Pimport ../../lib/nat_list.bend as NL# The mirror's node setters as functions of the node list: each rewrites one# field of an id's node (nothing for a free or absent node). The written# node, the length, and agreement off the id.# (source: tools/generators/tm_hand/setters.src)# ---- left ----def setl_n(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, x: M.Node<K>) -> List<&2, M.Node<K>>:  match x:    case M.Free{f}:      nl    case M.N{+c, +a, +b, +q, +k}:      PR.wr_nl(K, nl, id, M.N{c, v, b, q, k})def setl(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> List<&2, M.Node<K>>:  setl_n(K, nl, id, v, ST.nd(K, nl, id))def set_left_node_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {MI.set_left_node(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v, x) == ST.SH{n, root, lo, hi, free, l, d, setl_n(K, nl, id, v, x), pl, tg, fl} : ST.Sh<K, V>}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q, k}:      {==}def set_left_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat) -> {MI.set_left(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v) == ST.SH{n, root, lo, hi, free, l, d, setl(K, nl, id, v), pl, tg, fl} : ST.Sh<K, V>}:  set_left_node_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, id, v, ST.nd(K, nl, id))def setl_same(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == True{} : Bool}) -> {ST.nd(K, setl(K, nl, 1n+i, v), 1n+i) == M.N{c, v, b, q, k} : M.Node<K>}:  %Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+i), M.N{c, a, b, q, k}, hx) : {ST.nd(K, setl_n(K, nl, 1n+i, v, _), 1n+i) == M.N{c, v, b, q, k} : M.Node<K>}  FR.nd_wr_same(K, nl, i, M.N{c, v, b, q, k}, hi)def setl_n_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {SC.length(M.Node<K>, setl_n(K, nl, id, v, x)) == SC.length(M.Node<K>, nl) : Nat}:  match x:    case M.Free{f}:      {==}    case M.N{+c, +a, +b, +q, +k}:      FR.len_wr(K, nl, id, M.N{c, v, b, q, k})def setl_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {SC.length(M.Node<K>, setl(K, nl, id, v)) == SC.length(M.Node<K>, nl) : Nat}:  setl_n_len(K, nl, id, v, ST.nd(K, nl, id))def setl_n_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setl_n(K, nl, id, v, x)) == True{} : Bool}:  match x:    case M.Free{f}:      AG.agr_refl(~K, ~cmp, ~o, xs, nl)    case M.N{+c, +a, +b, +q, +k}:      AG.agr_wr(~K, ~cmp, ~o, xs, nl, id, M.N{c, v, b, q, k}, hn)# agreement off the written iddef setl_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setl(K, nl, id, v)) == True{} : Bool}:  setl_n_agr(~K, ~cmp, ~o, xs, nl, id, v, ST.nd(K, nl, id), hn)# ---- right ----def setr_n(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, x: M.Node<K>) -> List<&2, M.Node<K>>:  match x:    case M.Free{f}:      nl    case M.N{+c, +a, +b, +q, +k}:      PR.wr_nl(K, nl, id, M.N{c, a, v, q, k})def setr(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> List<&2, M.Node<K>>:  setr_n(K, nl, id, v, ST.nd(K, nl, id))def set_right_node_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {MI.set_right_node(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v, x) == ST.SH{n, root, lo, hi, free, l, d, setr_n(K, nl, id, v, x), pl, tg, fl} : ST.Sh<K, V>}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q, k}:      {==}def set_right_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat) -> {MI.set_right(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v) == ST.SH{n, root, lo, hi, free, l, d, setr(K, nl, id, v), pl, tg, fl} : ST.Sh<K, V>}:  set_right_node_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, id, v, ST.nd(K, nl, id))def setr_same(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == True{} : Bool}) -> {ST.nd(K, setr(K, nl, 1n+i, v), 1n+i) == M.N{c, a, v, q, k} : M.Node<K>}:  %Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+i), M.N{c, a, b, q, k}, hx) : {ST.nd(K, setr_n(K, nl, 1n+i, v, _), 1n+i) == M.N{c, a, v, q, k} : M.Node<K>}  FR.nd_wr_same(K, nl, i, M.N{c, a, v, q, k}, hi)def setr_n_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {SC.length(M.Node<K>, setr_n(K, nl, id, v, x)) == SC.length(M.Node<K>, nl) : Nat}:  match x:    case M.Free{f}:      {==}    case M.N{+c, +a, +b, +q, +k}:      FR.len_wr(K, nl, id, M.N{c, a, v, q, k})def setr_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {SC.length(M.Node<K>, setr(K, nl, id, v)) == SC.length(M.Node<K>, nl) : Nat}:  setr_n_len(K, nl, id, v, ST.nd(K, nl, id))def setr_n_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setr_n(K, nl, id, v, x)) == True{} : Bool}:  match x:    case M.Free{f}:      AG.agr_refl(~K, ~cmp, ~o, xs, nl)    case M.N{+c, +a, +b, +q, +k}:      AG.agr_wr(~K, ~cmp, ~o, xs, nl, id, M.N{c, a, v, q, k}, hn)# agreement off the written iddef setr_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setr(K, nl, id, v)) == True{} : Bool}:  setr_n_agr(~K, ~cmp, ~o, xs, nl, id, v, ST.nd(K, nl, id), hn)# ---- parent ----def setp_n(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, x: M.Node<K>) -> List<&2, M.Node<K>>:  match x:    case M.Free{f}:      nl    case M.N{+c, +a, +b, +q, +k}:      PR.wr_nl(K, nl, id, M.N{c, a, b, v, k})def setp(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> List<&2, M.Node<K>>:  setp_n(K, nl, id, v, ST.nd(K, nl, id))def set_parent_node_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {MI.set_parent_node(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v, x) == ST.SH{n, root, lo, hi, free, l, d, setp_n(K, nl, id, v, x), pl, tg, fl} : ST.Sh<K, V>}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q, k}:      {==}def set_parent_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Nat) -> {MI.set_parent(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v) == ST.SH{n, root, lo, hi, free, l, d, setp(K, nl, id, v), pl, tg, fl} : ST.Sh<K, V>}:  set_parent_node_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, id, v, ST.nd(K, nl, id))def setp_same(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == True{} : Bool}) -> {ST.nd(K, setp(K, nl, 1n+i, v), 1n+i) == M.N{c, a, b, v, k} : M.Node<K>}:  %Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+i), M.N{c, a, b, q, k}, hx) : {ST.nd(K, setp_n(K, nl, 1n+i, v, _), 1n+i) == M.N{c, a, b, v, k} : M.Node<K>}  FR.nd_wr_same(K, nl, i, M.N{c, a, b, v, k}, hi)def setp_n_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>) -> {SC.length(M.Node<K>, setp_n(K, nl, id, v, x)) == SC.length(M.Node<K>, nl) : Nat}:  match x:    case M.Free{f}:      {==}    case M.N{+c, +a, +b, +q, +k}:      FR.len_wr(K, nl, id, M.N{c, a, b, v, k})def setp_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {SC.length(M.Node<K>, setp(K, nl, id, v)) == SC.length(M.Node<K>, nl) : Nat}:  setp_n_len(K, nl, id, v, ST.nd(K, nl, id))def setp_n_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +x: M.Node<K>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setp_n(K, nl, id, v, x)) == True{} : Bool}:  match x:    case M.Free{f}:      AG.agr_refl(~K, ~cmp, ~o, xs, nl)    case M.N{+c, +a, +b, +q, +k}:      AG.agr_wr(~K, ~cmp, ~o, xs, nl, id, M.N{c, a, b, v, k}, hn)# agreement off the written iddef setp_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setp(K, nl, id, v)) == True{} : Bool}:  setp_n_agr(~K, ~cmp, ~o, xs, nl, id, v, ST.nd(K, nl, id), hn)# ---- red ----def setc_n(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, x: M.Node<K>) -> List<&2, M.Node<K>>:  match x:    case M.Free{f}:      nl    case M.N{+c, +a, +b, +q, +k}:      PR.wr_nl(K, nl, id, M.N{v, a, b, q, k})def setc(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool) -> List<&2, M.Node<K>>:  setc_n(K, nl, id, v, ST.nd(K, nl, id))def set_red_node_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Bool, +x: M.Node<K>) -> {MI.set_red_node(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v, x) == ST.SH{n, root, lo, hi, free, l, d, setc_n(K, nl, id, v, x), pl, tg, fl} : ST.Sh<K, V>}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q, k}:      {==}def set_red_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +n: Nat, +root: Nat, +lo: Nat, +hi: Nat, +free: Nat, +l: Nat, +d: Nat, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +tg: ST.Tr, +fl: List<&2, Nat>, +id: Nat, +v: Bool) -> {MI.set_red(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, id, v) == ST.SH{n, root, lo, hi, free, l, d, setc(K, nl, id, v), pl, tg, fl} : ST.Sh<K, V>}:  set_red_node_m(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, id, v, ST.nd(K, nl, id))def setc_same(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +v: Bool, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}, +hi: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == True{} : Bool}) -> {ST.nd(K, setc(K, nl, 1n+i, v), 1n+i) == M.N{v, a, b, q, k} : M.Node<K>}:  %Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+i), M.N{c, a, b, q, k}, hx) : {ST.nd(K, setc_n(K, nl, 1n+i, v, _), 1n+i) == M.N{v, a, b, q, k} : M.Node<K>}  FR.nd_wr_same(K, nl, i, M.N{v, a, b, q, k}, hi)def setc_n_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +x: M.Node<K>) -> {SC.length(M.Node<K>, setc_n(K, nl, id, v, x)) == SC.length(M.Node<K>, nl) : Nat}:  match x:    case M.Free{f}:      {==}    case M.N{+c, +a, +b, +q, +k}:      FR.len_wr(K, nl, id, M.N{v, a, b, q, k})def setc_len(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool) -> {SC.length(M.Node<K>, setc(K, nl, id, v)) == SC.length(M.Node<K>, nl) : Nat}:  setc_n_len(K, nl, id, v, ST.nd(K, nl, id))def setc_n_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +x: M.Node<K>, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setc_n(K, nl, id, v, x)) == True{} : Bool}:  match x:    case M.Free{f}:      AG.agr_refl(~K, ~cmp, ~o, xs, nl)    case M.N{+c, +a, +b, +q, +k}:      AG.agr_wr(~K, ~cmp, ~o, xs, nl, id, M.N{v, a, b, q, k}, hn)# agreement off the written iddef setc_agr(~K: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +hn: {NL.memn(id, xs) == False{} : Bool}) -> {AG.agr(~K, ~cmp, xs, nl, setc(K, nl, id, v)) == True{} : Bool}:  setc_n_agr(~K, ~cmp, ~o, xs, nl, id, v, ST.nd(K, nl, id), hn)# ---- every id's node after a setter ----def fn_c(-K: Data, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +e: {M.Free{0n} == M.N{c, a, b, q, k} : M.Node<K>}) -> Empty:  L.true_false(L.subst(M.Node<K>, z => {ST.is_free(K, M.Free{0n}, 0n) == ST.is_free(K, z, 0n) : Bool}, M.Free{0n}, M.N{c, a, b, q, k}, e, {==}))def nr_c(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}, +t: Bool, +ht: {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == t : Bool}) -> {t == True{} : Bool}:  match t:    case True{}:      {==}    case False{}:      +e = Equal.trans(M.Node<K>, M.Free{0n}, ST.nd(K, nl, 1n+i), M.N{c, a, b, q, k}, Equal.sym(M.Node<K>, ST.nd(K, nl, 1n+i), M.Free{0n}, PR.nth_hi(M.Node<K>, nl, i, M.Free{0n}, ht)), hx)      Empty.absurd({False{} == True{} : Bool}, fn_c(K, c, a, b, q, k, e))def nd_n_range(-K: Data, +nl: List<&2, M.Node<K>>, +i: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, 1n+i) == M.N{c, a, b, q, k} : M.Node<K>}) -> {Nat.is_lt(i, SC.length(M.Node<K>, nl)) == True{} : Bool}:  nr_c(K, nl, i, c, a, b, q, k, hx, Nat.is_lt(i, SC.length(M.Node<K>, nl)), {==})def modl(-K: Data, x: M.Node<K>, +v: Nat) -> M.Node<K>:  match x:    case M.Free{+f}:      M.Free{f}    case M.N{+c, +a, +b, +q, +k}:      M.N{c, v, b, q, k}def wsame_l(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, id) == M.N{c, a, b, q, k} : M.Node<K>}) -> {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, v, b, q, k}), id) == M.N{c, v, b, q, k} : M.Node<K>}:  match id:    case 0n:      Empty.absurd({ST.nd(K, PR.wr_nl(K, nl, 0n, M.N{c, v, b, q, k}), 0n) == M.N{c, v, b, q, k} : M.Node<K>}, fn_c(K, c, a, b, q, k, hx))    case 1n+i:      FR.nd_wr_same(K, nl, i, M.N{c, v, b, q, k}, nd_n_range(K, nl, i, c, a, b, q, k, hx))def ndl_c(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +x: M.Node<K>, +hx: {ST.nd(K, nl, id) == x : M.Node<K>}, +e: Bool, +he: {Nat.is_eq(id, j) == e : Bool}) -> {ST.nd(K, setl_n(K, nl, id, v, x), j) == ST.pk(M.Node<K>, e, modl(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:  match x e:    case M.Free{f} True{}:      +ej = N.eq_from_is_eq(id, j, he)      %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, nl, _) == modl(K, ST.nd(K, nl, _), v) : M.Node<K>}      %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.Free{f}, hx) : {_ == modl(K, _, v) : M.Node<K>}      {==}    case M.Free{f} False{}:      {==}    case M.N{+c, +a, +b, +q, +k} True{}:      +ej = N.eq_from_is_eq(id, j, he)      %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, v, b, q, k}), _) == modl(K, ST.nd(K, nl, _), v) : M.Node<K>}      %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.N{c, a, b, q, k}, hx) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, v, b, q, k}), id) == modl(K, _, v) : M.Node<K>}      wsame_l(K, nl, id, v, c, a, b, q, k, hx)    case M.N{+c, +a, +b, +q, +k} False{}:      FR.nd_wr_other(K, nl, id, M.N{c, v, b, q, k}, j, he)# the node at j after setting id: modified when j is iddef ndl(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.nd(K, setl(K, nl, id, v), j) == ST.pk(M.Node<K>, Nat.is_eq(id, j), modl(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:  ndl_c(K, nl, id, v, j, ST.nd(K, nl, id), {==}, Nat.is_eq(id, j), {==})def modr(-K: Data, x: M.Node<K>, +v: Nat) -> M.Node<K>:  match x:    case M.Free{+f}:      M.Free{f}    case M.N{+c, +a, +b, +q, +k}:      M.N{c, a, v, q, k}def wsame_r(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, id) == M.N{c, a, b, q, k} : M.Node<K>}) -> {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, v, q, k}), id) == M.N{c, a, v, q, k} : M.Node<K>}:  match id:    case 0n:      Empty.absurd({ST.nd(K, PR.wr_nl(K, nl, 0n, M.N{c, a, v, q, k}), 0n) == M.N{c, a, v, q, k} : M.Node<K>}, fn_c(K, c, a, b, q, k, hx))    case 1n+i:      FR.nd_wr_same(K, nl, i, M.N{c, a, v, q, k}, nd_n_range(K, nl, i, c, a, b, q, k, hx))def ndr_c(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +x: M.Node<K>, +hx: {ST.nd(K, nl, id) == x : M.Node<K>}, +e: Bool, +he: {Nat.is_eq(id, j) == e : Bool}) -> {ST.nd(K, setr_n(K, nl, id, v, x), j) == ST.pk(M.Node<K>, e, modr(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:  match x e:    case M.Free{f} True{}:      +ej = N.eq_from_is_eq(id, j, he)      %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, nl, _) == modr(K, ST.nd(K, nl, _), v) : M.Node<K>}      %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.Free{f}, hx) : {_ == modr(K, _, v) : M.Node<K>}      {==}    case M.Free{f} False{}:      {==}    case M.N{+c, +a, +b, +q, +k} True{}:      +ej = N.eq_from_is_eq(id, j, he)      %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, v, q, k}), _) == modr(K, ST.nd(K, nl, _), v) : M.Node<K>}      %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.N{c, a, b, q, k}, hx) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, v, q, k}), id) == modr(K, _, v) : M.Node<K>}      wsame_r(K, nl, id, v, c, a, b, q, k, hx)    case M.N{+c, +a, +b, +q, +k} False{}:      FR.nd_wr_other(K, nl, id, M.N{c, a, v, q, k}, j, he)# the node at j after setting id: modified when j is iddef ndr(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.nd(K, setr(K, nl, id, v), j) == ST.pk(M.Node<K>, Nat.is_eq(id, j), modr(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:  ndr_c(K, nl, id, v, j, ST.nd(K, nl, id), {==}, Nat.is_eq(id, j), {==})def modp(-K: Data, x: M.Node<K>, +v: Nat) -> M.Node<K>:  match x:    case M.Free{+f}:      M.Free{f}    case M.N{+c, +a, +b, +q, +k}:      M.N{c, a, b, v, k}def wsame_p(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, id) == M.N{c, a, b, q, k} : M.Node<K>}) -> {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, b, v, k}), id) == M.N{c, a, b, v, k} : M.Node<K>}:  match id:    case 0n:      Empty.absurd({ST.nd(K, PR.wr_nl(K, nl, 0n, M.N{c, a, b, v, k}), 0n) == M.N{c, a, b, v, k} : M.Node<K>}, fn_c(K, c, a, b, q, k, hx))    case 1n+i:      FR.nd_wr_same(K, nl, i, M.N{c, a, b, v, k}, nd_n_range(K, nl, i, c, a, b, q, k, hx))def ndp_c(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +x: M.Node<K>, +hx: {ST.nd(K, nl, id) == x : M.Node<K>}, +e: Bool, +he: {Nat.is_eq(id, j) == e : Bool}) -> {ST.nd(K, setp_n(K, nl, id, v, x), j) == ST.pk(M.Node<K>, e, modp(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:  match x e:    case M.Free{f} True{}:      +ej = N.eq_from_is_eq(id, j, he)      %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, nl, _) == modp(K, ST.nd(K, nl, _), v) : M.Node<K>}      %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.Free{f}, hx) : {_ == modp(K, _, v) : M.Node<K>}      {==}    case M.Free{f} False{}:      {==}    case M.N{+c, +a, +b, +q, +k} True{}:      +ej = N.eq_from_is_eq(id, j, he)      %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, b, v, k}), _) == modp(K, ST.nd(K, nl, _), v) : M.Node<K>}      %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.N{c, a, b, q, k}, hx) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{c, a, b, v, k}), id) == modp(K, _, v) : M.Node<K>}      wsame_p(K, nl, id, v, c, a, b, q, k, hx)    case M.N{+c, +a, +b, +q, +k} False{}:      FR.nd_wr_other(K, nl, id, M.N{c, a, b, v, k}, j, he)# the node at j after setting id: modified when j is iddef ndp(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.nd(K, setp(K, nl, id, v), j) == ST.pk(M.Node<K>, Nat.is_eq(id, j), modp(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:  ndp_c(K, nl, id, v, j, ST.nd(K, nl, id), {==}, Nat.is_eq(id, j), {==})def modc(-K: Data, x: M.Node<K>, +v: Bool) -> M.Node<K>:  match x:    case M.Free{+f}:      M.Free{f}    case M.N{+c, +a, +b, +q, +k}:      M.N{v, a, b, q, k}def wsame_c(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +c: Bool, +a: Nat, +b: Nat, +q: Nat, +k: K, +hx: {ST.nd(K, nl, id) == M.N{c, a, b, q, k} : M.Node<K>}) -> {ST.nd(K, PR.wr_nl(K, nl, id, M.N{v, a, b, q, k}), id) == M.N{v, a, b, q, k} : M.Node<K>}:  match id:    case 0n:      Empty.absurd({ST.nd(K, PR.wr_nl(K, nl, 0n, M.N{v, a, b, q, k}), 0n) == M.N{v, a, b, q, k} : M.Node<K>}, fn_c(K, c, a, b, q, k, hx))    case 1n+i:      FR.nd_wr_same(K, nl, i, M.N{v, a, b, q, k}, nd_n_range(K, nl, i, c, a, b, q, k, hx))def ndc_c(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +j: Nat, +x: M.Node<K>, +hx: {ST.nd(K, nl, id) == x : M.Node<K>}, +e: Bool, +he: {Nat.is_eq(id, j) == e : Bool}) -> {ST.nd(K, setc_n(K, nl, id, v, x), j) == ST.pk(M.Node<K>, e, modc(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:  match x e:    case M.Free{f} True{}:      +ej = N.eq_from_is_eq(id, j, he)      %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, nl, _) == modc(K, ST.nd(K, nl, _), v) : M.Node<K>}      %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.Free{f}, hx) : {_ == modc(K, _, v) : M.Node<K>}      {==}    case M.Free{f} False{}:      {==}    case M.N{+c, +a, +b, +q, +k} True{}:      +ej = N.eq_from_is_eq(id, j, he)      %Equal.sym(Nat, j, id, Equal.sym(Nat, id, j, ej)) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{v, a, b, q, k}), _) == modc(K, ST.nd(K, nl, _), v) : M.Node<K>}      %Equal.sym(M.Node<K>, ST.nd(K, nl, id), M.N{c, a, b, q, k}, hx) : {ST.nd(K, PR.wr_nl(K, nl, id, M.N{v, a, b, q, k}), id) == modc(K, _, v) : M.Node<K>}      wsame_c(K, nl, id, v, c, a, b, q, k, hx)    case M.N{+c, +a, +b, +q, +k} False{}:      FR.nd_wr_other(K, nl, id, M.N{v, a, b, q, k}, j, he)# the node at j after setting id: modified when j is iddef ndc(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +j: Nat) -> {ST.nd(K, setc(K, nl, id, v), j) == ST.pk(M.Node<K>, Nat.is_eq(id, j), modc(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)) : M.Node<K>}:  ndc_c(K, nl, id, v, j, ST.nd(K, nl, id), {==}, Nat.is_eq(id, j), {==})# ---- what setters keep everywhere ----def ent_modl(-K: Data, -V: Data, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, modl(K, x, v), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:  match x m:    case M.Free{f} +m:      {==}    case M.N{c, a, b, q, k} None{}:      {==}    case M.N{c, a, b, q, k} Some{w}:      {==}def free_modl(-K: Data, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, modl(K, x, v), q) == ST.is_free(K, x, q) : Bool}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q2, k}:      {==}def ent_pkl(-K: Data, -V: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.pk(M.Node<K>, e, modl(K, x, v), x), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:  match e:    case True{}:      ent_modl(K, V, x, v, m)    case False{}:      {==}def free_pkl(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, ST.pk(M.Node<K>, e, modl(K, x, v), x), q) == ST.is_free(K, x, q) : Bool}:  match e:    case True{}:      free_modl(K, x, v, q)    case False{}:      {==}def ent_setl(-K: Data, -V: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.nd(K, setl(K, nl, id, v), j), m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}:  %Equal.sym(M.Node<K>, ST.nd(K, setl(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modl(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndl(K, nl, id, v, j)) : {ST.ent(K, V, _, m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}  ent_pkl(K, V, Nat.is_eq(id, j), ST.nd(K, nl, j), v, m)# a setter keeps every entrydef ents_setl(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {ST.ents(~K, ~V, xs, setl(K, nl, id, v), pl) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:  match xs:    case Nil{}:      {==}    case Con{+j, +t}:      %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setl(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setl(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {ST.cons_m(M.Entry<K, V>, _, ST.ents(~K, ~V, t, setl(K, nl, id, v), pl)) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}      %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, t, setl(K, nl, id, v), pl), ST.ents(~K, ~V, t, nl, pl), ents_setl(~K, ~V, t, nl, pl, id, v)) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}      {==}def oks_setl(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {EN.oks(~K, ~V, xs, setl(K, nl, id, v), pl) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:  match xs:    case Nil{}:      {==}    case Con{+j, +t}:      %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setl(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setl(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {Bool.and(S.is_some(M.Entry<K, V>, _), EN.oks(~K, ~V, t, setl(K, nl, id, v), pl)) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}      %Equal.sym(Bool, EN.oks(~K, ~V, t, setl(K, nl, id, v), pl), EN.oks(~K, ~V, t, nl, pl), oks_setl(~K, ~V, t, nl, pl, id, v)) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}      {==}# a setter keeps the free chaindef fll_setl(~K: Data, +fl: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {ST.fll(~K, setl(K, nl, id, v), fl) == ST.fll(~K, nl, fl) : Bool}:  match fl:    case Nil{}:      {==}    case Con{+f, +t}:      %Equal.sym(M.Node<K>, ST.nd(K, setl(K, nl, id, v), f), ST.pk(M.Node<K>, Nat.is_eq(id, f), modl(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ndl(K, nl, id, v, f)) : {Bool.and(ST.is_free(K, _, ST.fst0(t)), ST.fll(~K, setl(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}      %Equal.sym(Bool, ST.is_free(K, ST.pk(M.Node<K>, Nat.is_eq(id, f), modl(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ST.fst0(t)), ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), free_pkl(K, Nat.is_eq(id, f), ST.nd(K, nl, f), v, ST.fst0(t))) : {Bool.and(_, ST.fll(~K, setl(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}      %Equal.sym(Bool, ST.fll(~K, setl(K, nl, id, v), t), ST.fll(~K, nl, t), fll_setl(~K, t, nl, id, v)) : {Bool.and(ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), _) == ST.fll(~K, nl, Con{f, t}) : Bool}      {==}def ent_modr(-K: Data, -V: Data, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, modr(K, x, v), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:  match x m:    case M.Free{f} +m:      {==}    case M.N{c, a, b, q, k} None{}:      {==}    case M.N{c, a, b, q, k} Some{w}:      {==}def free_modr(-K: Data, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, modr(K, x, v), q) == ST.is_free(K, x, q) : Bool}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q2, k}:      {==}def ent_pkr(-K: Data, -V: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.pk(M.Node<K>, e, modr(K, x, v), x), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:  match e:    case True{}:      ent_modr(K, V, x, v, m)    case False{}:      {==}def free_pkr(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, ST.pk(M.Node<K>, e, modr(K, x, v), x), q) == ST.is_free(K, x, q) : Bool}:  match e:    case True{}:      free_modr(K, x, v, q)    case False{}:      {==}def ent_setr(-K: Data, -V: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.nd(K, setr(K, nl, id, v), j), m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}:  %Equal.sym(M.Node<K>, ST.nd(K, setr(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modr(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndr(K, nl, id, v, j)) : {ST.ent(K, V, _, m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}  ent_pkr(K, V, Nat.is_eq(id, j), ST.nd(K, nl, j), v, m)# a setter keeps every entrydef ents_setr(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {ST.ents(~K, ~V, xs, setr(K, nl, id, v), pl) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:  match xs:    case Nil{}:      {==}    case Con{+j, +t}:      %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setr(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setr(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {ST.cons_m(M.Entry<K, V>, _, ST.ents(~K, ~V, t, setr(K, nl, id, v), pl)) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}      %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, t, setr(K, nl, id, v), pl), ST.ents(~K, ~V, t, nl, pl), ents_setr(~K, ~V, t, nl, pl, id, v)) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}      {==}def oks_setr(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {EN.oks(~K, ~V, xs, setr(K, nl, id, v), pl) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:  match xs:    case Nil{}:      {==}    case Con{+j, +t}:      %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setr(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setr(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {Bool.and(S.is_some(M.Entry<K, V>, _), EN.oks(~K, ~V, t, setr(K, nl, id, v), pl)) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}      %Equal.sym(Bool, EN.oks(~K, ~V, t, setr(K, nl, id, v), pl), EN.oks(~K, ~V, t, nl, pl), oks_setr(~K, ~V, t, nl, pl, id, v)) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}      {==}# a setter keeps the free chaindef fll_setr(~K: Data, +fl: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {ST.fll(~K, setr(K, nl, id, v), fl) == ST.fll(~K, nl, fl) : Bool}:  match fl:    case Nil{}:      {==}    case Con{+f, +t}:      %Equal.sym(M.Node<K>, ST.nd(K, setr(K, nl, id, v), f), ST.pk(M.Node<K>, Nat.is_eq(id, f), modr(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ndr(K, nl, id, v, f)) : {Bool.and(ST.is_free(K, _, ST.fst0(t)), ST.fll(~K, setr(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}      %Equal.sym(Bool, ST.is_free(K, ST.pk(M.Node<K>, Nat.is_eq(id, f), modr(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ST.fst0(t)), ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), free_pkr(K, Nat.is_eq(id, f), ST.nd(K, nl, f), v, ST.fst0(t))) : {Bool.and(_, ST.fll(~K, setr(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}      %Equal.sym(Bool, ST.fll(~K, setr(K, nl, id, v), t), ST.fll(~K, nl, t), fll_setr(~K, t, nl, id, v)) : {Bool.and(ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), _) == ST.fll(~K, nl, Con{f, t}) : Bool}      {==}def ent_modp(-K: Data, -V: Data, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, modp(K, x, v), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:  match x m:    case M.Free{f} +m:      {==}    case M.N{c, a, b, q, k} None{}:      {==}    case M.N{c, a, b, q, k} Some{w}:      {==}def free_modp(-K: Data, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, modp(K, x, v), q) == ST.is_free(K, x, q) : Bool}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q2, k}:      {==}def ent_pkp(-K: Data, -V: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.pk(M.Node<K>, e, modp(K, x, v), x), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:  match e:    case True{}:      ent_modp(K, V, x, v, m)    case False{}:      {==}def free_pkp(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat, +q: Nat) -> {ST.is_free(K, ST.pk(M.Node<K>, e, modp(K, x, v), x), q) == ST.is_free(K, x, q) : Bool}:  match e:    case True{}:      free_modp(K, x, v, q)    case False{}:      {==}def ent_setp(-K: Data, -V: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.nd(K, setp(K, nl, id, v), j), m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}:  %Equal.sym(M.Node<K>, ST.nd(K, setp(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modp(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndp(K, nl, id, v, j)) : {ST.ent(K, V, _, m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}  ent_pkp(K, V, Nat.is_eq(id, j), ST.nd(K, nl, j), v, m)# a setter keeps every entrydef ents_setp(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {ST.ents(~K, ~V, xs, setp(K, nl, id, v), pl) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:  match xs:    case Nil{}:      {==}    case Con{+j, +t}:      %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setp(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setp(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {ST.cons_m(M.Entry<K, V>, _, ST.ents(~K, ~V, t, setp(K, nl, id, v), pl)) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}      %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, t, setp(K, nl, id, v), pl), ST.ents(~K, ~V, t, nl, pl), ents_setp(~K, ~V, t, nl, pl, id, v)) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}      {==}def oks_setp(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Nat) -> {EN.oks(~K, ~V, xs, setp(K, nl, id, v), pl) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:  match xs:    case Nil{}:      {==}    case Con{+j, +t}:      %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setp(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setp(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {Bool.and(S.is_some(M.Entry<K, V>, _), EN.oks(~K, ~V, t, setp(K, nl, id, v), pl)) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}      %Equal.sym(Bool, EN.oks(~K, ~V, t, setp(K, nl, id, v), pl), EN.oks(~K, ~V, t, nl, pl), oks_setp(~K, ~V, t, nl, pl, id, v)) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}      {==}# a setter keeps the free chaindef fll_setp(~K: Data, +fl: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat) -> {ST.fll(~K, setp(K, nl, id, v), fl) == ST.fll(~K, nl, fl) : Bool}:  match fl:    case Nil{}:      {==}    case Con{+f, +t}:      %Equal.sym(M.Node<K>, ST.nd(K, setp(K, nl, id, v), f), ST.pk(M.Node<K>, Nat.is_eq(id, f), modp(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ndp(K, nl, id, v, f)) : {Bool.and(ST.is_free(K, _, ST.fst0(t)), ST.fll(~K, setp(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}      %Equal.sym(Bool, ST.is_free(K, ST.pk(M.Node<K>, Nat.is_eq(id, f), modp(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ST.fst0(t)), ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), free_pkp(K, Nat.is_eq(id, f), ST.nd(K, nl, f), v, ST.fst0(t))) : {Bool.and(_, ST.fll(~K, setp(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}      %Equal.sym(Bool, ST.fll(~K, setp(K, nl, id, v), t), ST.fll(~K, nl, t), fll_setp(~K, t, nl, id, v)) : {Bool.and(ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), _) == ST.fll(~K, nl, Con{f, t}) : Bool}      {==}def ent_modc(-K: Data, -V: Data, +x: M.Node<K>, +v: Bool, +m: Maybe<&2, V>) -> {ST.ent(K, V, modc(K, x, v), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:  match x m:    case M.Free{f} +m:      {==}    case M.N{c, a, b, q, k} None{}:      {==}    case M.N{c, a, b, q, k} Some{w}:      {==}def free_modc(-K: Data, +x: M.Node<K>, +v: Bool, +q: Nat) -> {ST.is_free(K, modc(K, x, v), q) == ST.is_free(K, x, q) : Bool}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q2, k}:      {==}def ent_pkc(-K: Data, -V: Data, +e: Bool, +x: M.Node<K>, +v: Bool, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.pk(M.Node<K>, e, modc(K, x, v), x), m) == ST.ent(K, V, x, m) : Maybe<&2, M.Entry<K, V>>}:  match e:    case True{}:      ent_modc(K, V, x, v, m)    case False{}:      {==}def free_pkc(-K: Data, +e: Bool, +x: M.Node<K>, +v: Bool, +q: Nat) -> {ST.is_free(K, ST.pk(M.Node<K>, e, modc(K, x, v), x), q) == ST.is_free(K, x, q) : Bool}:  match e:    case True{}:      free_modc(K, x, v, q)    case False{}:      {==}def ent_setc(-K: Data, -V: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +j: Nat, +m: Maybe<&2, V>) -> {ST.ent(K, V, ST.nd(K, setc(K, nl, id, v), j), m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}:  %Equal.sym(M.Node<K>, ST.nd(K, setc(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modc(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndc(K, nl, id, v, j)) : {ST.ent(K, V, _, m) == ST.ent(K, V, ST.nd(K, nl, j), m) : Maybe<&2, M.Entry<K, V>>}  ent_pkc(K, V, Nat.is_eq(id, j), ST.nd(K, nl, j), v, m)# a setter keeps every entrydef ents_setc(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Bool) -> {ST.ents(~K, ~V, xs, setc(K, nl, id, v), pl) == ST.ents(~K, ~V, xs, nl, pl) : List<&2, M.Entry<K, V>>}:  match xs:    case Nil{}:      {==}    case Con{+j, +t}:      %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setc(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setc(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {ST.cons_m(M.Entry<K, V>, _, ST.ents(~K, ~V, t, setc(K, nl, id, v), pl)) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}      %Equal.sym(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, t, setc(K, nl, id, v), pl), ST.ents(~K, ~V, t, nl, pl), ents_setc(~K, ~V, t, nl, pl, id, v)) : {ST.cons_m(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), _) == ST.ents(~K, ~V, Con{j, t}, nl, pl) : List<&2, M.Entry<K, V>>}      {==}def oks_setc(~K: Data, ~V: Data, +xs: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +pl: List<&2, Maybe<&2, V>>, +id: Nat, +v: Bool) -> {EN.oks(~K, ~V, xs, setc(K, nl, id, v), pl) == EN.oks(~K, ~V, xs, nl, pl) : Bool}:  match xs:    case Nil{}:      {==}    case Con{+j, +t}:      %Equal.sym(Maybe<&2, M.Entry<K, V>>, ST.ent(K, V, ST.nd(K, setc(K, nl, id, v), j), ST.pv(V, pl, j)), ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j)), ent_setc(K, V, nl, id, v, j, ST.pv(V, pl, j))) : {Bool.and(S.is_some(M.Entry<K, V>, _), EN.oks(~K, ~V, t, setc(K, nl, id, v), pl)) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}      %Equal.sym(Bool, EN.oks(~K, ~V, t, setc(K, nl, id, v), pl), EN.oks(~K, ~V, t, nl, pl), oks_setc(~K, ~V, t, nl, pl, id, v)) : {Bool.and(S.is_some(M.Entry<K, V>, ST.ent(K, V, ST.nd(K, nl, j), ST.pv(V, pl, j))), _) == EN.oks(~K, ~V, Con{j, t}, nl, pl) : Bool}      {==}# a setter keeps the free chaindef fll_setc(~K: Data, +fl: List<&2, Nat>, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool) -> {ST.fll(~K, setc(K, nl, id, v), fl) == ST.fll(~K, nl, fl) : Bool}:  match fl:    case Nil{}:      {==}    case Con{+f, +t}:      %Equal.sym(M.Node<K>, ST.nd(K, setc(K, nl, id, v), f), ST.pk(M.Node<K>, Nat.is_eq(id, f), modc(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ndc(K, nl, id, v, f)) : {Bool.and(ST.is_free(K, _, ST.fst0(t)), ST.fll(~K, setc(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}      %Equal.sym(Bool, ST.is_free(K, ST.pk(M.Node<K>, Nat.is_eq(id, f), modc(K, ST.nd(K, nl, f), v), ST.nd(K, nl, f)), ST.fst0(t)), ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), free_pkc(K, Nat.is_eq(id, f), ST.nd(K, nl, f), v, ST.fst0(t))) : {Bool.and(_, ST.fll(~K, setc(K, nl, id, v), t)) == ST.fll(~K, nl, Con{f, t}) : Bool}      %Equal.sym(Bool, ST.fll(~K, setc(K, nl, id, v), t), ST.fll(~K, nl, t), fll_setc(~K, t, nl, id, v)) : {Bool.and(ST.is_free(K, ST.nd(K, nl, f), ST.fst0(t)), _) == ST.fll(~K, nl, Con{f, t}) : Bool}      {==}# ---- recolouring keeps every link ----def isn_modc(-K: Data, +x: M.Node<K>, +v: Bool, +a: Nat, +b: Nat, +q: Nat) -> {ST.is_node(K, modc(K, x, v), a, b, q) == ST.is_node(K, x, a, b, q) : Bool}:  match x:    case M.Free{f}:      {==}    case M.N{c, x1, x2, x3, k}:      {==}def isn_pkc(-K: Data, +e: Bool, +x: M.Node<K>, +v: Bool, +a: Nat, +b: Nat, +q: Nat) -> {ST.is_node(K, ST.pk(M.Node<K>, e, modc(K, x, v), x), a, b, q) == ST.is_node(K, x, a, b, q) : Bool}:  match e:    case True{}:      isn_modc(K, x, v, a, b, q)    case False{}:      {==}def isn_setc(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool, +j: Nat, +a: Nat, +b: Nat, +q: Nat) -> {ST.is_node(K, ST.nd(K, setc(K, nl, id, v), j), a, b, q) == ST.is_node(K, ST.nd(K, nl, j), a, b, q) : Bool}:  %Equal.sym(M.Node<K>, ST.nd(K, setc(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modc(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndc(K, nl, id, v, j)) : {ST.is_node(K, _, a, b, q) == ST.is_node(K, ST.nd(K, nl, j), a, b, q) : Bool}  isn_pkc(K, Nat.is_eq(id, j), ST.nd(K, nl, j), v, a, b, q)def rep_setc(~K: Data, +t: ST.Tr, +p: Nat, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool) -> {ST.rep(~K, t, p, setc(K, nl, id, v)) == ST.rep(~K, t, p, nl) : Bool}:  match t:    case ST.TE{}:      {==}    case ST.TN{+i, +l, +r}:      %Equal.sym(Bool, ST.is_node(K, ST.nd(K, setc(K, nl, id, v), i), ST.rid(l), ST.rid(r), p), ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), p), isn_setc(K, nl, id, v, i, ST.rid(l), ST.rid(r), p)) : {Bool.and(Nat.is_lt(0n, i), Bool.and(_, Bool.and(ST.rep(~K, l, i, setc(K, nl, id, v)), ST.rep(~K, r, i, setc(K, nl, id, v))))) == ST.rep(~K, ST.TN{i, l, r}, p, nl) : Bool}      %Equal.sym(Bool, ST.rep(~K, l, i, setc(K, nl, id, v)), ST.rep(~K, l, i, nl), rep_setc(~K, l, i, nl, id, v)) : {Bool.and(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), p), Bool.and(_, ST.rep(~K, r, i, setc(K, nl, id, v))))) == ST.rep(~K, ST.TN{i, l, r}, p, nl) : Bool}      %Equal.sym(Bool, ST.rep(~K, r, i, setc(K, nl, id, v)), ST.rep(~K, r, i, nl), rep_setc(~K, r, i, nl, id, v)) : {Bool.and(Nat.is_lt(0n, i), Bool.and(ST.is_node(K, ST.nd(K, nl, i), ST.rid(l), ST.rid(r), p), Bool.and(ST.rep(~K, l, i, nl), _))) == ST.rep(~K, ST.TN{i, l, r}, p, nl) : Bool}      {==}def ctx_setc(~K: Data, +c: List<&2, P.Fr>, +x: Nat, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Bool) -> {P.ctxok(~K, c, x, setc(K, nl, id, v)) == P.ctxok(~K, c, x, nl) : Bool}:  match c:    case Nil{}:      {==}    case Con{P.FR{+p, +lft, +s}, +u}:      %Equal.sym(Bool, ST.is_node(K, ST.nd(K, setc(K, nl, id, v), p), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), isn_setc(K, nl, id, v, p, ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u))) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(_, ST.rep(~K, s, p, setc(K, nl, id, v)))), P.ctxok(~K, u, p, setc(K, nl, id, v))) == P.ctxok(~K, Con{P.FR{p, lft, s}, u}, x, nl) : Bool}      %Equal.sym(Bool, ST.rep(~K, s, p, setc(K, nl, id, v)), ST.rep(~K, s, p, nl), rep_setc(~K, s, p, nl, id, v)) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), _)), P.ctxok(~K, u, p, setc(K, nl, id, v))) == P.ctxok(~K, Con{P.FR{p, lft, s}, u}, x, nl) : Bool}      %Equal.sym(Bool, P.ctxok(~K, u, p, setc(K, nl, id, v)), P.ctxok(~K, u, p, nl), ctx_setc(~K, u, p, nl, id, v)) : {Bool.and(Bool.and(Nat.is_lt(0n, p), Bool.and(ST.is_node(K, ST.nd(K, nl, p), ST.pk(Nat, lft, x, ST.rid(s)), ST.pk(Nat, lft, ST.rid(s), x), P.top(u)), ST.rep(~K, s, p, nl))), _) == P.ctxok(~K, Con{P.FR{p, lft, s}, u}, x, nl) : Bool}      {==}# the recoloured node's colourdef red_modc(-K: Data, +x: M.Node<K>, +v: Bool, +h: {ST.is_red(K, x) == ST.is_red(K, x) : Bool}) -> {ST.is_red(K, modc(K, x, False{})) == False{} : Bool}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q, k}:      {==}# ---- link setters keep every colour ----def red_modl(-K: Data, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, modl(K, x, v)) == ST.is_red(K, x) : Bool}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q, k}:      {==}def red_pkl(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, ST.pk(M.Node<K>, e, modl(K, x, v), x)) == ST.is_red(K, x) : Bool}:  match e:    case True{}:      red_modl(K, x, v)    case False{}:      {==}def red_setl(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.is_red(K, ST.nd(K, setl(K, nl, id, v), j)) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}:  %Equal.sym(M.Node<K>, ST.nd(K, setl(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modl(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndl(K, nl, id, v, j)) : {ST.is_red(K, _) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}  red_pkl(K, Nat.is_eq(id, j), ST.nd(K, nl, j), v)def red_modr(-K: Data, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, modr(K, x, v)) == ST.is_red(K, x) : Bool}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q, k}:      {==}def red_pkr(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, ST.pk(M.Node<K>, e, modr(K, x, v), x)) == ST.is_red(K, x) : Bool}:  match e:    case True{}:      red_modr(K, x, v)    case False{}:      {==}def red_setr(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.is_red(K, ST.nd(K, setr(K, nl, id, v), j)) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}:  %Equal.sym(M.Node<K>, ST.nd(K, setr(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modr(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndr(K, nl, id, v, j)) : {ST.is_red(K, _) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}  red_pkr(K, Nat.is_eq(id, j), ST.nd(K, nl, j), v)def red_modp(-K: Data, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, modp(K, x, v)) == ST.is_red(K, x) : Bool}:  match x:    case M.Free{f}:      {==}    case M.N{c, a, b, q, k}:      {==}def red_pkp(-K: Data, +e: Bool, +x: M.Node<K>, +v: Nat) -> {ST.is_red(K, ST.pk(M.Node<K>, e, modp(K, x, v), x)) == ST.is_red(K, x) : Bool}:  match e:    case True{}:      red_modp(K, x, v)    case False{}:      {==}def red_setp(-K: Data, +nl: List<&2, M.Node<K>>, +id: Nat, +v: Nat, +j: Nat) -> {ST.is_red(K, ST.nd(K, setp(K, nl, id, v), j)) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}:  %Equal.sym(M.Node<K>, ST.nd(K, setp(K, nl, id, v), j), ST.pk(M.Node<K>, Nat.is_eq(id, j), modp(K, ST.nd(K, nl, j), v), ST.nd(K, nl, j)), ndp(K, nl, id, v, j)) : {ST.is_red(K, _) == ST.is_red(K, ST.nd(K, nl, j)) : Bool}  red_pkp(K, Nat.is_eq(id, j), ST.nd(K, nl, j), v)