1	import Base
2	import ../../lib/logic.bend as L
3	import ../../lib/nat.bend as N
4	import ../../lib/list.bend as LL
5	import ../../lib/order.bend as O
6	import ../../../spec/lib/common.bend as SC
7	import ../../../spec/containers/balanced_search_tree/main.bend as S
8	import ../../../src/containers/balanced_search_tree.bend as M
9	import ./state.bend as ST
10	import ./mirror.bend as MI
11	import ./ord.bend as OR
12	import ./reads.bend as RD
13	import ./cur.bend as CU
14	import ./cnx.bend as CX
15	import ./vsp.bend as VS
16	import ./vit.bend as VI
17	
18	# A view's size: the mirror counts the steps of the view's cursor, forward
19	# from the first entry above the lower bound (backward from the last below
20	# the upper), until an entry is out of range; the count is the number of
21	# entries within. (source: tools/generators/tm_hand/vsz.src)
22	
23	
24	# ---- a step whose specification is known ----
25	
26	def cnext(-K: Data, -V: Data, c: S.Cursor<K, V>) -> Maybe<&2, K>:
27	  match c:
28	    case S.CR{m, nx, cu, lo, hi, fw}:
29	      nx
30	
31	def stp3(~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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +nx: Nat, +cu: Nat, +a: Maybe<&2, K>, +bb: Maybe<&2, K>, +o0: Maybe<&2, M.Entry<K, V>>, +hsp: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +y2: Nat, +z2: Nat, +oe: Maybe<&2, M.Entry<K, V>>, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, oe) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +hs: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})) == (CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}), oe) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +hc2: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool}) -> Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, o0) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == a : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool})>>:
32	  +heq = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0), S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, oe), Equal.sym(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0), hsp), hs)
33	  +eo = L.pair_snd(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, oe, heq)
34	  +ec = L.pair_fst(S.Cursor<K, V>, Maybe<&2, M.Entry<K, V>>, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, oe, heq)
35	  +hk2 = Equal.sym(Maybe<&2, K>, a, CU.ck(~K, nl, y2), L.subst(S.Cursor<K, V>, q => {a == cnext(K, V, q) : Maybe<&2, K>}, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, y2), CU.ck(~K, nl, z2), lo2, hi2, fw}, ec, {==}))
36	  +hm2 = L.subst(Maybe<&2, M.Entry<K, V>>, q => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, q) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, oe, o0, Equal.sym(Maybe<&2, M.Entry<K, V>>, o0, oe, eo), hm)
37	  (y2, (z2, (hm2, (hk2, hc2))))
38	
39	def stp2(~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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +nx: Nat, +cu: Nat, +a: Maybe<&2, K>, +bb: Maybe<&2, K>, +o0: Maybe<&2, M.Entry<K, V>>, +hsp: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, +y2: Nat, +z2: Nat, +oe: Maybe<&2, M.Entry<K, V>>, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, oe) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, r: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})) == (CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}), oe) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool}) -> Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, o0) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == a : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool})>>:
40	  match r:
41	    case Tuple{hs, hc2}:
42	      stp3(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, cu, a, bb, o0, hsp, y2, z2, oe, hm, hs, hc2)
43	
44	def stp(~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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +fw: Bool, +nx: Nat, +cu: Nat, +a: Maybe<&2, K>, +bb: Maybe<&2, K>, +o0: Maybe<&2, M.Entry<K, V>>, +hsp: {S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, a, bb, lo2, hi2, fw}, o0) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, st: CU.CSTEP(~K, ~V, ~cmp, Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, CU.cmod(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw})), MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}), ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, fw)) -> Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, fw}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}, o0) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == a : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, fw}) == True{} : Bool})>>:
45	  match st:
46	    case Tuple{+y2, Tuple{+z2, Tuple{+oe, Tuple{+hm, r}}}}:
47	      stp2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, fw, nx, cu, a, bb, o0, hsp, y2, z2, oe, hm, r)
48	
49	# ---- the specification's step at an entry, either way ----
50	
51	
52	def find_at(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +es: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +hab: {es == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hord: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}) -> {S.find_e(~K, ~V, ~cmp, k, es) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}:
53	  L.subst(List<&2, M.Entry<K, V>>, z => {S.find_e(~K, ~V, ~cmp, k, z) == Some{M.Entry{k, v}} : Maybe<&2, M.Entry<K, V>>}, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), es, Equal.sym(List<&2, M.Entry<K, V>>, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab), OR.find_mid_eq(~K, ~V, ~cmp, ~o, k, xa, M.Entry{k, v}, t, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab, hord), O.refl(~K, ~cmp, ~o, k)))
54	
55	def sp_f(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +l: Nat, +es: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +hab: {es == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hord: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}, +cc: Maybe<&2, K>, +lo2: M.Bound<K>, +hi2: M.Bound<K>) -> {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, es}, Some{k}, cc, lo2, hi2, True{}}) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}:
56	  +efw = L.subst(List<&2, M.Entry<K, V>>, z => {S.first_where(~K, ~V, ~cmp, k, False{}, z) == S.head(M.Entry<K, V>, t) : Maybe<&2, M.Entry<K, V>>}, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), es, Equal.sym(List<&2, M.Entry<K, V>>, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab), CX.fw_mid(~K, ~V, ~cmp, ~o, xa, M.Entry{k, v}, t, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab, hord)))
57	  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), Some{M.Entry{k, v}}, find_at(~K, ~V, ~cmp, ~o, es, xa, k, v, t, hab, hord)) : {S.next_at(~K, ~V, ~cmp, l, es, cc, lo2, hi2, True{}, _) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
58	  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.first_where(~K, ~V, ~cmp, k, False{}, es), S.head(M.Entry<K, V>, t), efw) : {S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, _), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, True{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
59	  {==}
60	
61	def sp_b(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~K, ~cmp), +l: Nat, +es: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +hab: {es == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hord: {ST.ordered(~K, ~V, ~cmp, es) == True{} : Bool}, +cc: Maybe<&2, K>, +lo2: M.Bound<K>, +hi2: M.Bound<K>) -> {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, es}, Some{k}, cc, lo2, hi2, False{}}) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.last(M.Entry<K, V>, xa)), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}:
62	  +elw = L.subst(List<&2, M.Entry<K, V>>, z => {S.last_where(~K, ~V, ~cmp, k, False{}, z, None{}) == S.last(M.Entry<K, V>, xa) : Maybe<&2, M.Entry<K, V>>}, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), es, Equal.sym(List<&2, M.Entry<K, V>>, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab), CX.lw_mid(~K, ~V, ~cmp, ~o, xa, M.Entry{k, v}, t, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, es, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab, hord)))
63	  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.find_e(~K, ~V, ~cmp, k, es), Some{M.Entry{k, v}}, find_at(~K, ~V, ~cmp, ~o, es, xa, k, v, t, hab, hord)) : {S.next_at(~K, ~V, ~cmp, l, es, cc, lo2, hi2, False{}, _) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.last(M.Entry<K, V>, xa)), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
64	  %Equal.sym(Maybe<&2, M.Entry<K, V>>, S.last_where(~K, ~V, ~cmp, k, False{}, es, None{}), S.last(M.Entry<K, V>, xa), elw) : {S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, _), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) == S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, es}, S.key_m(K, V, S.last(M.Entry<K, V>, xa)), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, es}, None{}, cc, lo2, hi2, False{}}, None{})) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}
65	  {==}
66	
67	# ---- forward ----
68	
69	
70	def szn2(~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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Nil{})), c)) : MI.MView<K, V> & Nat}:
71	  %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Nil{})), c)) : MI.MView<K, V> & Nat}
72	  {==}
73	
74	def szn(~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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Nil{})), c)) : MI.MView<K, V> & Nat}:
75	  match r:
76	    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
77	      szn2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, y2, z2, hm)
78	
79	def szt2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, r: {CU.ck(~K, nl, y2) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}) == True{} : Bool}, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.it
80	  match r:
81	    case Tuple{hk2, hc2}:
82	      %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, Some{M.Entry{k, v}}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}
83	      +e2 = VS.cong(List<&2, M.Entry<K, V>>, Nat, q => Nat.add(SC.length(M.Entry<K, V>, q), c), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Con{M.Entry{k, v}, S.within(~K, ~V, ~cmp, lo2, hi2, t)}, VS.w_in(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, t, hb))
84	      +e3 = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c), 1n+Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c), N.add_succ(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), c), Equal.sym(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c), 1n+Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), c), e2))
85	      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)), kont(y2, z2, hc2, hk2), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c), e3))
86	
87	def szt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}) == True{} : Bool})>>, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.E
88	  match r:
89	    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
90	      szt2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, y2, z2, hm, r2, kont)
91	
92	def szs2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
93	  %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}
94	  +hbu = VS.bu_of(~K, ~cmp, lo2, hi2, k, L.and_left(S.above_lower(~K, ~cmp, k, lo2), VS.allal(~K, ~V, ~cmp, lo2, t), hal), hb)
95	  +ho = OR.ord_app_r(~K, ~V, ~cmp, xa, Con{M.Entry{k, v}, t}, L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))
96	  +hw = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), S.within(~K, ~V, ~cmp, lo2, hi2, t), Nil{}, VS.w_out(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, t, hb), VS.wnil(~K, ~V, ~cmp, ~o, lo2, hi2, k, t, hbu, OR.ord_gt(~K, ~V, ~cmp, ~o, t, M.Entry{k, v}, ho)))
97	  Equal.sym(MI.MView<K, V> & Nat, (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, c), VS.cong(List<&2, M.Entry<K, V>>, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, q), c)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t}), Nil{}, hw))
98	
99	def szs(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, True{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
100	  match r:
101	    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
102	      szs2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, y2, z2, hm)
103	
104	def szc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}) : List<&2, M.Entry<K, V>>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == True{} : Bool}, +hk: {CU.ck(~K, nl, nx) == Some{k} : Maybe<&2, K>}, +b: Bool, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == b : Bool}, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.head(M.Entry<K, V>, t)) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, t)), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, t})), c)) : MI.MView<K, V> & Nat}:
105	  match b:
106	    case True{}:
107	      +e2 = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, True{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), sp_f(~K, ~V, ~cmp, ~o, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), xa, k, v, t, hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), CU.ck(~K, nl, cu), lo2, hi2), VS.pk_t(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}), hb))
108	      szt(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, True{}, nx, cu, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, Some{M.Entry{k, v}}, Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, True{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}) == S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, True{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, hk, {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, True{}, hc)), kont)
109	    case False{}:
110	      +e2 = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, True{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}), sp_f(~K, ~V, ~cmp, ~o, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), xa, k, v, t, hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), CU.ck(~K, nl, cu), lo2, hi2), VS.pk_f(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.head(M.Entry<K, V>, t)), Some{k}, lo2, hi2, True{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}), hb))
111	      szs(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, True{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, True{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}), L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, True{}}) == S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, True{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, hk, {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, True{}, hc)))
112	
113	
114	# the count forward: the entries within from the cursor on
115	def szf(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +bs: List<&2, M.Entry<K, V>>, +xa: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}}) == True{} : Bool}, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, bs) : List<&2, M.Entry<K, V>>}, +hk: {CU.ck(~K, nl, nx) == S.key_m(K, V, S.head(M.Entry<K, V>, bs)) : Maybe<&2, K>}, +hal: {VS.allal(~K, ~V, ~cmp, lo2, bs) == True{} : Bool}, +c: Nat) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, bs), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, bs)), c)) : MI.MView<K, V> & Nat}:
116	  match bs:
117	    case Nil{}:
118	      szn(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, True{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, True{}}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, True{}}, None{}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, None{}, CU.ck(~K, nl, nx), Equal.sym(Maybe<&2, K>, CU.ck(~K, nl, nx), None{}, hk), {==}), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, True{}, hc)))
119	    case Con{M.Entry{+k, +v}, +t}:
120	      szc(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, xa, nx, cu, hab, hal, c, hc, hk, S.in_range(~K, ~cmp, k, lo2, hi2), {==}, ky => kz => kc => kk => szf(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, t, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}), ky, kz, kc, Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), SC.append(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}), t), hab, Equal.sym(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}), t), SC.append(M.Entry<K, V>, xa, Con{M.Entry{k, v}, t}), LL.append_assoc(M.Entry<K, V>, xa, Con{M.Entry{k, v}, Nil{}}, t))), kk, L.and_right(S.above_lower(~K, ~cmp, k, lo2), VS.allal(~K, ~V, ~cmp, lo2, t), hal), 1n+c))
121	
122	# ---- backward: the entries before the cursor, reversed ----
123	
124	
125	def sbn2(~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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{}))), c)) : MI.MView<K, V> & Nat}:
126	  %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{}))), c)) : MI.MView<K, V> & Nat}
127	  {==}
128	
129	def sbn(~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>, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +nx: Nat, +cu: Nat, +c: Nat, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Nil{}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Nil{}))), c)) : MI.MView<K, V> & Nat}:
130	  match r:
131	    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
132	      sbn2(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, y2, z2, hm)
133	
134	# the entries within the reversal of e before t: those of t's, then e's
135	def wl_snoc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +t: List<&2, M.Entry<K, V>>, +k: K, +v: V) -> {S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})) == SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})) : List<&2, M.Entry<K, V>>}:
136	  Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}}), LL.snoc_append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), VS.within_app(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, Nil{}}))
137	
138	def sbt2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}, r: {CU.ck(~K, nl, y2) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == True{} : Bool}, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c)) : MI.MView<K, V> & Nat
139	  match r:
140	    case Tuple{hk2, hc2}:
141	      %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, Some{M.Entry{k, v}}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}
142	      +ew = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}}), wl_snoc(~K, ~V, ~cmp, lo2, hi2, t, k, v), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), q), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}}), Con{M.Entry{k, v}, Nil{}}, VS.w_in(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, Nil{}, hb)))
143	      +el = Equal.trans(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}})), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}}), ew), LL.length_append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Con{M.Entry{k, v}, Nil{}}))
144	      +e3 = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c), Nat.add(Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c), Equal.sym(Nat, Nat.add(Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c), N.add_assoc(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n, c)), VS.cong(Nat, Nat, q => Nat.add(q, c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Equal.sym(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n), el)))
145	      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c)), kont(y2, z2, hc2, hk2), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c), e3))
146	
147	def sbt(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == True{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, Some{M.Entry{k, v}}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == True{} : Bool})>>, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 
148	  match r:
149	    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
150	      sbt2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, y2, z2, hm, r2, kont)
151	
152	def sbs2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, +y2: Nat, +z2: Nat, +hm: {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
153	  %Equal.sym(MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}), (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}), hm) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, _) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}
154	  +hal = VS.al_of(~K, ~cmp, lo2, hi2, k, L.and_left(S.below_upper(~K, ~cmp, k, hi2), VS.allbu(~K, ~V, ~cmp, hi2, t), hbu), hb)
155	  +ho = L.subst(List<&2, M.Entry<K, V>>, z => {ST.ordered(~K, ~V, ~cmp, z) == True{} : Bool}, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg))
156	  +hw1 = VS.wnil_lt(~K, ~V, ~cmp, ~o, lo2, hi2, k, SC.reverse(M.Entry<K, V>, t), hal, OR.ord_mid_l(~K, ~V, ~cmp, ~o, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs, ho))
157	  +hw2 = VS.w_out(~K, ~V, ~cmp, lo2, hi2, M.Entry{k, v}, Nil{}, hb)
158	  +hw = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})), Nil{}, wl_snoc(~K, ~V, ~cmp, lo2, hi2, t, k, v), L.subst(List<&2, M.Entry<K, V>>, q => {SC.append(M.Entry<K, V>, q, S.within(~K, ~V, ~cmp, lo2, hi2, Con{M.Entry{k, v}, Nil{}})) == Nil{} : List<&2, M.Entry<K, V>>}, Nil{}, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Equal.sym(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t)), Nil{}, hw1), hw2))
159	  Equal.sym(MI.MView<K, V> & Nat, (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), c)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, c), VS.cong(List<&2, M.Entry<K, V>>, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, q), c)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Nil{}, hw))
160	
161	def sbs(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == False{} : Bool}, r: Sigma<&1, &1, Nat, y2 => Sigma<&1, &1, Nat, z2 => {MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == (MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}, None{}) : MI.MCursor<K, V> & Maybe<&2, M.Entry<K, V>>} & ({CU.ck(~K, nl, y2) == None{} : Maybe<&2, K>} & {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, y2, z2, lo2, hi2, False{}}) == True{} : Bool})>>) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, Con{M.Entry{k, v}, t}))), c)) : MI.MView<K, V> & Nat}:
162	  match r:
163	    case Tuple{+y2, Tuple{+z2, Tuple{+hm, r2}}}:
164	      sbs2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, y2, z2, hm)
165	
166	
167	def sbc(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +k: K, +v: V, +t: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}) : List<&2, M.Entry<K, V>>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, Con{M.Entry{k, v}, t}) == True{} : Bool}, +c: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == True{} : Bool}, +hk: {CU.ck(~K, nl, nx) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))) : Maybe<&2, K>}, +b: Bool, +hb: {S.in_range(~K, ~cmp, k, lo2, hi2) == b : Bool}, kont: @+ky: Nat -> @+kz: Nat -> @+kc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}}) == True{} : Bool} -> @+kk: {CU.ck(~K, nl, ky) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))) : Maybe<&2, K>} -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, t), x), 1n+c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, ky, kz, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, t))), 1n+c)) : MI.MView<K, V> & Nat}) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, Con{M.Entry{k, v}, t}), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo,
168	  match b:
169	    case True{}:
170	      +e2 = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, False{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), sp_b(~K, ~V, ~cmp, ~o, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.reverse(M.Entry<K, V>, t), k, v, bs, hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), CU.ck(~K, nl, cu), lo2, hi2), VS.pk_t(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}), hb))
171	      sbt(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, False{}, nx, cu, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, Some{M.Entry{k, v}}, Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, False{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}) == S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, False{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, nx), S.key_m(K, V, S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Some{k}, hk, VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Some{M.Entry{k, v}}, LL.last_snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, False{}, hc)), kont)
172	    case False{}:
173	      +e2 = Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, False{}}), S.pick(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{})), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}), sp_b(~K, ~V, ~cmp, ~o, l, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.reverse(M.Entry<K, V>, t), k, v, bs, hab, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), CU.ck(~K, nl, cu), lo2, hi2), VS.pk_f(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.in_range(~K, ~cmp, k, lo2, hi2), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t))), Some{k}, lo2, hi2, False{}}, Some{M.Entry{k, v}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}), hb))
174	      sbs(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, hab, hbu, c, hb, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, False{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, Equal.trans(S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>, S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}), S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, Some{k}, CU.ck(~K, nl, cu), lo2, hi2, False{}}), (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}), L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, CU.ck(~K, nl, nx), CU.ck(~K, nl, cu), lo2, hi2, False{}}) == S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, False{}}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, CU.ck(~K, nl, nx), Some{k}, Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, nx), S.key_m(K, V, S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), Some{k}, hk, VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), S.last(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v})), Some{M.Entry{k, v}}, LL.last_snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}))), {==}), e2), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, False{}, hc)))
175	
176	
177	# the count backward: the entries within before the cursor
178	def szb(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +x: Nat, +rr: List<&2, M.Entry<K, V>>, +bs: List<&2, M.Entry<K, V>>, +nx: Nat, +cu: Nat, +hc: {CU.cgood(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}}) == True{} : Bool}, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr), bs) : List<&2, M.Entry<K, V>>}, +hk: {CU.ck(~K, nl, nx) == S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, rr))) : Maybe<&2, K>}, +hbu: {VS.allbu(~K, ~V, ~cmp, hi2, rr) == True{} : Bool}, +c: Nat) -> {MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, rr), x), c, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, nx, cu, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, rr))), c)) : MI.MView<K, V> & Nat}:
179	  match rr:
180	    case Nil{}:
181	      sbn(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, x, nx, cu, c, stp(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, lo2, hi2, False{}, nx, cu, None{}, CU.ck(~K, nl, cu), None{}, L.subst(Maybe<&2, K>, q => {S.iterator_next(~K, ~V, ~cmp, S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, q, CU.ck(~K, nl, cu), lo2, hi2, False{}}) == (S.CR{S.TM{l, ST.ents(~K, ~V, ST.ids(tg), nl, pl)}, None{}, CU.ck(~K, nl, cu), lo2, hi2, False{}}, None{}) : S.Cursor<K, V> & Maybe<&2, M.Entry<K, V>>}, None{}, CU.ck(~K, nl, nx), Equal.sym(Maybe<&2, K>, CU.ck(~K, nl, nx), None{}, hk), {==}), CX.next_m(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, nx, cu, lo2, hi2, False{}, hc)))
182	    case Con{M.Entry{+k, +v}, +t}:
183	      sbc(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, k, v, t, bs, nx, cu, Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), hab, LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs)), hbu, c, hc, hk, S.in_range(~K, ~cmp, k, lo2, hi2), {==}, ky => kz => kc => kk => szb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, x, t, Con{M.Entry{k, v}, bs}, ky, kz, kc, Equal.trans(List<&2, M.Entry<K, V>>, ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, SC.snoc(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}), bs), SC.append(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), Con{M.Entry{k, v}, bs}), hab, LL.snoc_append_cons(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, t), M.Entry{k, v}, bs)), kk, L.and_right(S.below_upper(~K, ~cmp, k, hi2), VS.allbu(~K, ~V, ~cmp, hi2, t), hbu), 1n+c))
184	
185	# ---- the view's size ----
186	
187	
188	def vsf2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, +xa: List<&2, M.Entry<K, V>>, +xb: List<&2, M.Entry<K, V>>, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>}, r: {VS.allal(~K, ~V, ~cmp, lo2, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>})) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
189	  match r:
190	    case Tuple{hal, Tuple{hwa, hfb}}:
191	      %Equal.sym(ST.Sh<K, V> & Nat, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j), h1) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+n, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.cursor_started(~K, ~V, ~cmp, lo2, hi2, True{}, _))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
192	      +hnt = Equal.trans(Nat, SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), LL.length_append(M.Entry<K, V>, xa, xb), N.add_comm(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb)))
193	      %Equal.sym(Nat, n, Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), Equal.trans(Nat, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), Equal.trans(Nat, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), hnt))) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+_, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
194	      +hk = Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, S.head(M.Entry<K, V>, xb)), h2, Equal.trans(Maybe<&2, K>, S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), S.key_m(K, V, S.head(M.Entry<K, V>, xb)), VS.start_fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.head(M.Entry<K, V>, xb), hfb)))
195	      +ew = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xb), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xb), VS.within_app(~K, ~V, ~cmp, lo2, hi2, xa, xb), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, q, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xa), Nil{}, hwa)))
196	      +ec = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), N.add_zero(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb))), Equal.sym(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, xb), ew)))
197	      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, xb), SC.length(M.Entry<K, V>, xa)), 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, True{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), 0n)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))), szf(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, SC.length(M.Entry<K, V>, xa), xb, xa, j, 0n, CU.cg_start(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, h3, True{}), hab, hk, hal, 0n), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xb)), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), ec))
198	
199	def vsf1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({VS.allal(~K, ~V, ~cmp, lo2, xb) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xa) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.fal(~K, ~V, ~cmp, lo2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) == S.head(M.Entry<K, V>, xb) : Maybe<&2, M.Entry<K, V>>}))>>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
200	  match sp:
201	    case Tuple{+xa, Tuple{+xb, Tuple{+hab, r}}}:
202	      vsf2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, xa, xb, hab, r)
203	
204	def vsb2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, +xa: List<&2, M.Entry<K, V>>, +xb: List<&2, M.Entry<K, V>>, +hab: {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>}, r: {VS.allbu(~K, ~V, ~cmp, hi2, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}) : Maybe<&2, M.Entry<K, V>>})) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
205	  match r:
206	    case Tuple{hbu, Tuple{hwb, hlb}}:
207	      %Equal.sym(ST.Sh<K, V> & Nat, MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}), (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j), h1) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+n, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.cursor_started(~K, ~V, ~cmp, lo2, hi2, False{}, _))) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
208	      +err = LL.spec_rev_rev(M.Entry<K, V>, xa)
209	      +hab2 = L.subst(List<&2, M.Entry<K, V>>, q => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, q, xb) : List<&2, M.Entry<K, V>>}, xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err), hab)
210	      +hnt = Equal.trans(Nat, SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, xb)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), LL.length_append(M.Entry<K, V>, xa, xb), VS.cong(Nat, Nat, q => Nat.add(q, SC.length(M.Entry<K, V>, xb)), SC.length(M.Entry<K, V>, xa), SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(Nat, SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xa), LL.length_rev(M.Entry<K, V>, xa))))
211	      %Equal.sym(Nat, n, Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), Equal.trans(Nat, n, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), RD.size_eq(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg), Equal.trans(Nat, SC.length(M.Entry<K, V>, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), SC.length(M.Entry<K, V>, SC.append(M.Entry<K, V>, xa, xb)), Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), hnt))) : {MI.view_count_loop(~K, ~V, ~cmp, 1n+_, 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}})) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}
212	      +hk0 = Equal.trans(Maybe<&2, K>, S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{})), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), VS.start_lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), VS.cong(Maybe<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, q), VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), S.last(M.Entry<K, V>, xa), Equal.trans(Maybe<&2, M.Entry<K, V>>, VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}), OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}), S.last(M.Entry<K, V>, xa), hlb, OR.orm_none(M.Entry<K, V>, S.last(M.Entry<K, V>, xa)))))
213	      +hk = Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), S.key_m(K, V, S.last(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), Equal.trans(Maybe<&2, K>, CU.ck(~K, nl, j), S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.key_m(K, V, S.last(M.Entry<K, V>, xa)), h2, hk0), VS.cong(List<&2, M.Entry<K, V>>, Maybe<&2, K>, q => S.key_m(K, V, S.last(M.Entry<K, V>, q)), xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err)))
214	      +ew = Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), ST.ents(~K, ~V, ST.ids(tg), nl, pl), SC.append(M.Entry<K, V>, xa, xb), hab), Equal.trans(List<&2, M.Entry<K, V>>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.append(M.Entry<K, V>, xa, xb)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), VS.within_app(~K, ~V, ~cmp, lo2, hi2, xa, xb), Equal.trans(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), Equal.trans(List<&2, M.Entry<K, V>>, SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), S.within(~K, ~V, ~cmp, lo2, hi2, xb)), SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), Nil{}), S.within(~K, ~V, ~cmp, lo2, hi2, xa), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => SC.append(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa), q), S.within(~K, ~V, ~cmp, lo2, hi2, xb), Nil{}, hwb), LL.append_nil(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, xa))), VS.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, q => S.within(~K, ~V, ~cmp, lo2, hi2, q), xa, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), Equal.sym(List<&2, M.Entry<K, V>>, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), xa, err)))))
215	      +ec = Equal.trans(Nat, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), N.add_zero(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))))), Equal.sym(Nat, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), VS.cong(List<&2, M.Entry<K, V>>, Nat, q => SC.length(M.Entry<K, V>, q), S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)), S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa))), ew)))
216	      Equal.trans(MI.MView<K, V> & Nat, MI.view_count_loop(~K, ~V, ~cmp, 1n+Nat.add(SC.length(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)), SC.length(M.Entry<K, V>, xb)), 0n, MI.iterator_next(~K, ~V, ~cmp, MI.MC{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j, 0n, lo2, hi2, False{}})), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), 0n)), (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))), szb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, SC.length(M.Entry<K, V>, xb), SC.reverse(M.Entry<K, V>, xa), xb, j, 0n, CU.cg_start(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, j, h3, False{}), hab2, hk, VS.allbu_rev(~K, ~V, ~cmp, hi2, xa, hbu), 0n), VS.cong(Nat, MI.MView<K, V> & Nat, q => (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, q), Nat.add(SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, SC.reverse(M.Entry<K, V>, SC.reverse(M.Entry<K, V>, xa)))), 0n), SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl))), ec))
217	
218	def vsb1(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, +h2: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>}, +h3: {CU.idok(ST.ids(tg), j) == True{} : Bool}, sp: Sigma<&1, &1, List<&2, M.Entry<K, V>>, xa => Sigma<&1, &1, List<&2, M.Entry<K, V>>, xb => {ST.ents(~K, ~V, ST.ids(tg), nl, pl) == SC.append(M.Entry<K, V>, xa, xb) : List<&2, M.Entry<K, V>>} & ({VS.allbu(~K, ~V, ~cmp, hi2, xa) == True{} : Bool} & ({S.within(~K, ~V, ~cmp, lo2, hi2, xb) == Nil{} : List<&2, M.Entry<K, V>>} & {VS.lbu(~K, ~V, ~cmp, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}) == OR.orm(M.Entry<K, V>, S.last(M.Entry<K, V>, xa), None{}) : Maybe<&2, M.Entry<K, V>>}))>>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
219	  match sp:
220	    case Tuple{+xa, Tuple{+xb, Tuple{+hab, r}}}:
221	      vsb2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, xa, xb, hab, r)
222	
223	
224	def vrf2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, r: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool}) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
225	  match r:
226	    case Tuple{h2, h3}:
227	      vsf1(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, VS.split_fal(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))
228	
229	def vrf(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, r: Sigma<&1, &1, Nat, j => {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, True{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat} & ({CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, lo2, True{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool})>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, False{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
230	  match r:
231	    case Tuple{+j, Tuple{+h1, r2}}:
232	      vrf2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, r2)
233	
234	def vrb2(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +j: Nat, +h1: {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat}, r: {CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool}) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
235	  match r:
236	    case Tuple{h2, h3}:
237	      vsb1(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, h2, h3, VS.split_lbu(~K, ~V, ~cmp, ~o, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl), None{}, ST.g_cord(~K, ~V, ~cmp, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg)))
238	
239	def vrb(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, r: Sigma<&1, &1, Nat, j => {MI.range_start(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, hi2, False{}) == (ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, j) : ST.Sh<K, V> & Nat} & ({CU.ck(~K, nl, j) == S.start(~K, ~V, ~cmp, hi2, False{}, ST.ents(~K, ~V, ST.ids(tg), nl, pl)) : Maybe<&2, K>} & {CU.idok(ST.ids(tg), j) == True{} : Bool})>) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, True{}}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
240	  match r:
241	    case Tuple{+j, Tuple{+h1, r2}}:
242	      vrb2(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, j, h1, r2)
243	
244	# the mirror's size of a view: the number of entries within
245	def view_size_m(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~o: O.Order(~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>, +hg: {ST.good(~K, ~V, ~cmp, ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}) == True{} : Bool}, +lo2: M.Bound<K>, +hi2: M.Bound<K>, +d2: Bool) -> {MI.view_size(~K, ~V, ~cmp, MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}) == (MI.MV{ST.SH{n, root, lo, hi, free, l, d, nl, pl, tg, fl}, lo2, hi2, d2}, SC.length(M.Entry<K, V>, S.within(~K, ~V, ~cmp, lo2, hi2, ST.ents(~K, ~V, ST.ids(tg), nl, pl)))) : MI.MView<K, V> & Nat}:
246	  match d2:
247	    case True{}:
248	      vrb(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, VI.rsid(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, hi2, False{}))
249	    case False{}:
250	      vrf(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, hi2, VI.rsid(~K, ~V, ~cmp, ~o, n, root, lo, hi, free, l, d, nl, pl, tg, fl, hg, lo2, True{}))