proofs/containers/binary_heap/push.bend
bend-collections-laws-containers@1.0.0.0 · 166 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/list.bend as LL
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/order.bend as O
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
8import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
9import bend-collections-laws-containers@1.0.0.0/spec/containers/binary_heap.bend as S
10import bend-collections-laws-containers@1.0.0.0/src/containers/binary_heap.bend as H
11import bend-collections-laws-containers@1.0.0.0/src/containers/types/binary_heap.bend as E
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/idx.bend as IX
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/u32idx.bend as UX
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/slots.bend as SL
15import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/vals.bend as V
16import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/root.bend as RT
17import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/up.bend as UPS
18import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/grow.bend as GR
19import bend-collections-laws-containers@1.0.0.0/proofs/containers/binary_heap/state.bend as ST
20
21# push: the element is written at slot `size` and sifted up. The four
22# hypotheses of the sift-up law hold at a fresh leaf:
23# ho_exc every pair except the one into the new slot holds already,
24# kids_le the new slot has no children inside the heap,
25# lay the slots below `size` are untouched and slot `size` is now full,
26# msort the multiset gains exactly x.
27# If the block is full it is doubled first (grow.bend: nothing but the
28# capacity changes).
29
30# ---- the pairs below the new leaf are untouched ----
31
32def pair_off(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, m: Nat, +hmi: {Nat.is_lt(m, i) == True{} : Bool}, +h: {SL.pair_ok(~A, ~cmp, AR.slots(Maybe<&2, A>, t), m) == True{} : Bool}) -> {SL.pair_ok(~A, ~cmp, UPS.ulog(~A, t, i, x), m) == True{} : Bool}:
33 match m:
34 case 0n:
35 {==}
36 case 1n+ +p:
37 %Equal.sym(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), 1n+p), SL.slot(~A, AR.slots(Maybe<&2, A>, t), 1n+p), UPS.ulog_off(~A, t, i, x, 1n+p, SL.ne_sym(i, 1n+p, N.is_eq_lt(1n+p, i, hmi)))) : {SL.mle(~A, ~cmp, SL.slot(~A, UPS.ulog(~A, t, i, x), IX.par(1n+p)), _) == True{} : Bool}
38 %Equal.sym(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), IX.par(1n+p)), SL.slot(~A, AR.slots(Maybe<&2, A>, t), IX.par(1n+p)), UPS.ulog_off(~A, t, i, x, IX.par(1n+p), SL.ne_sym(i, IX.par(1n+p), N.is_eq_lt(IX.par(1n+p), i, N.lt_trans(IX.par(1n+p), 1n+p, i, IX.par_lt(1n+p, {==}), hmi))))) : {SL.mle(~A, ~cmp, _, SL.slot(~A, AR.slots(Maybe<&2, A>, t), 1n+p)) == True{} : Bool}
39 h
40
41def exc_step(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +m: Nat, +hm: {Nat.is_lt(m, 1n+i) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), i) == True{} : Bool}, b: Bool, +eb: {Nat.is_eq(m, i) == b : Bool}) -> {SL.pair_skip(~A, ~cmp, UPS.ulog(~A, t, i, x), m, i) == True{} : Bool}:
42 match b:
43 case True{}:
44 SL.skip_eq(~A, ~cmp, UPS.ulog(~A, t, i, x), m, i, eb)
45 case False{}:
46 +hmi = N.lt_or_eq(m, i, N.lt_succ_le(m, i, hm), eb)
47 SL.skip_ne(~A, ~cmp, UPS.ulog(~A, t, i, x), m, i, eb,
48 pair_off(~A, ~cmp, t, i, x, m, hmi, SL.ho_at(~A, ~cmp, AR.slots(Maybe<&2, A>, t), i, m, hho, hmi)))
49
50def exc_up(~A: Data, ~cmp: A -> A -> Cmp, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, k: Nat, +hk: {Nat.is_le(k, 1n+i) == True{} : Bool}, +hho: {SL.ho_upto(~A, ~cmp, AR.slots(Maybe<&2, A>, t), i) == True{} : Bool}) -> {SL.ho_exc(~A, ~cmp, UPS.ulog(~A, t, i, x), k, i) == True{} : Bool}:
51 match k:
52 case 0n:
53 {==}
54 case 1n+ +m:
55 L.and_intro(SL.pair_skip(~A, ~cmp, UPS.ulog(~A, t, i, x), m, i), SL.ho_exc(~A, ~cmp, UPS.ulog(~A, t, i, x), m, i),
56 exc_step(~A, ~cmp, t, i, x, m, N.succ_le_lt(m, 1n+i, hk), hho, Nat.is_eq(m, i), {==}),
57 exc_up(~A, ~cmp, t, i, x, m, N.le_trans(m, 1n+m, 1n+i, N.le_succ(m), hk), hho))
58
59# ---- the new leaf has no children inside the heap ----
60
61def kids_leaf(~A: Data, ~cmp: A -> A -> Cmp, +ss: List<&2, Maybe<&2, A>>, +u: Nat, +i: Nat) -> {SL.kids_le(~A, ~cmp, ss, 1n+i, u, i) == True{} : Bool}:
62 L.and_intro(SL.kid_le(~A, ~cmp, ss, 1n+i, u, IX.kidl(i)), SL.kid_le(~A, ~cmp, ss, 1n+i, u, IX.kidr(i)),
63 SL.kid_le_out(~A, ~cmp, ss, 1n+i, u, IX.kidl(i), N.le_not_lt(IX.kidl(i), 1n+i, IX.double_le(i))),
64 SL.kid_le_out(~A, ~cmp, ss, 1n+i, u, IX.kidr(i), N.le_not_lt(IX.kidr(i), 1n+i, N.le_trans(1n+i, IX.kidl(i), IX.kidr(i), IX.double_le(i), N.le_succ(IX.kidl(i))))))
65
66# ---- the layout below the new leaf is untouched ----
67
68def lay_off(~A: Data, +ss: List<&2, Maybe<&2, A>>, +i: Nat, +v: Maybe<&2, A>, k: Nat, +hk: {Nat.is_le(k, i) == True{} : Bool}, +h: {SL.lay(~A, ss, k) == True{} : Bool}) -> {SL.lay(~A, SC.update(Maybe<&2, A>, ss, i, v), k) == True{} : Bool}:
69 match k:
70 case 0n:
71 {==}
72 case 1n+ +m:
73 %Equal.sym(Maybe<&2, A>, SL.slot(~A, SC.update(Maybe<&2, A>, ss, i, v), m), SL.slot(~A, ss, m), SL.slot_other(~A, ss, i, m, v, SL.ne_sym(i, m, N.is_eq_lt(m, i, N.succ_le_lt(m, i, hk))))) : {Bool.and(Maybe.is_some(&2, A, _), SL.lay(~A, SC.update(Maybe<&2, A>, ss, i, v), m)) == True{} : Bool}
74 L.and_intro(Maybe.is_some(&2, A, SL.slot(~A, ss, m)), SL.lay(~A, SC.update(Maybe<&2, A>, ss, i, v), m),
75 L.and_left(Maybe.is_some(&2, A, SL.slot(~A, ss, m)), SL.lay(~A, ss, m), h),
76 lay_off(~A, ss, i, v, m, N.lt_le(m, i, N.succ_le_lt(m, i, hk)), L.and_right(Maybe.is_some(&2, A, SL.slot(~A, ss, m)), SL.lay(~A, ss, m), h)))
77
78def lay_push(~A: Data, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}, +h: {SL.lay(~A, AR.slots(Maybe<&2, A>, t), i) == True{} : Bool}) -> {SL.lay(~A, UPS.ulog(~A, t, i, x), 1n+i) == True{} : Bool}:
79 L.and_intro(Maybe.is_some(&2, A, SL.slot(~A, UPS.ulog(~A, t, i, x), i)), SL.lay(~A, UPS.ulog(~A, t, i, x), i),
80 L.subst(Maybe<&2, A>, z => {Maybe.is_some(&2, A, z) == True{} : Bool}, Some{x}, SL.slot(~A, UPS.ulog(~A, t, i, x), i), Equal.sym(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), i), Some{x}, UPS.ulog_at(~A, d, t, i, x, hi, pf)), {==}),
81 lay_off(~A, AR.slots(Maybe<&2, A>, t), i, Some{x}, i, N.le_refl(i), h))
82
83# ---- the multiset gains exactly x ----
84
85def ms_push(~A: Data, ~cmp: A -> A -> Cmp, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +i: Nat, +x: A, +hi: {Nat.is_lt(i, SC.pow2(d)) == True{} : Bool}, +pf: {AR.perfect(Maybe<&2, A>, d, t) == True{} : Bool}) -> {V.msort(~A, ~cmp, V.vals(~A, UPS.ulog(~A, t, i, x), 1n+i)) == S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t), i))) : List<&2, A>}:
86 %Equal.sym(Maybe<&2, A>, SL.slot(~A, UPS.ulog(~A, t, i, x), i), Some{x}, UPS.ulog_at(~A, d, t, i, x, hi, pf)) : {V.msort(~A, ~cmp, V.cons_slot(~A, _, V.vals(~A, UPS.ulog(~A, t, i, x), i))) == S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t), i))) : List<&2, A>}
87 Equal.cong(List<&2, A>, List<&2, A>, zs => S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, zs)), V.vals(~A, UPS.ulog(~A, t, i, x), i), V.vals(~A, AR.slots(Maybe<&2, A>, t), i), V.vals_above(~A, AR.slots(Maybe<&2, A>, t), i, Some{x}, i, N.le_refl(i)))
88
89# ---- one sift-up at the fresh leaf ----
90
91def PushOK(~A: Data, ~cmp: A -> A -> Cmp, sh: ST.Shadow<A>, x: A) -> Type:
92 Sigma<&1, &1, ST.Shadow<A>, sh2 => {H.push(~A, ~cmp, ST.real(~A, sh), x) == ST.real(~A, sh2) : H.Heap<A>} & ({ST.good(~A, ~cmp, sh2) == True{} : Bool} & ({ST.model(~A, ~cmp, sh2) == S.ins(~A, ~cmp, x, ST.model(~A, ~cmp, sh)) : List<&2, A>} & {Nat.is_le(ST.sh_depth(~A, sh2), 1n+ST.sh_depth(~A, sh)) == True{} : Bool}))>
93
94# The sift-up result, packaged as the new shadow. `d` is the depth of the
95# block the element is written into (the grown depth if the block was full).
96def push_from(~A: Data, ~cmp: A -> A -> Cmp, +sh0: ST.Shadow<A>, +size: Nat, +d: Nat, +t: AR.Tree<Maybe<&2, A>>, +x: A, +tgt: List<&2, A>, +hd: {Nat.is_le(d, 31n) == True{} : Bool}, +hs: {Nat.is_le(1n+size, SC.pow2(d)) == True{} : Bool}, +hdd: {Nat.is_le(d, 1n+ST.sh_depth(~A, sh0)) == True{} : Bool}, +eq0: {H.push(~A, ~cmp, ST.real(~A, sh0), x) == H.BH{1n+size, U32.from_nat(1n+size), d, U.pow2u(d), H.sift_up(~A, ~cmp, d, U32.from_nat(size), x, AR.thaw(Maybe<&2, A>, t))} : H.Heap<A>}, r: UPS.SiftOK(~A, ~cmp, d, 1n+size, tgt, d, t, size, x)) -> Sigma<&1, &1, ST.Shadow<A>, sh2 => {H.push(~A, ~cmp, ST.real(~A, sh0), x) == ST.real(~A, sh2) : H.Heap<A>} & ({ST.good(~A, ~cmp, sh2) == True{} : Bool} & ({ST.model(~A, ~cmp, sh2) == tgt : List<&2, A>} & {Nat.is_le(ST.sh_depth(~A, sh2), 1n+ST.sh_depth(~A, sh0)) == True{} : Bool}))>:
97 match r:
98 case Tuple{+t2, Tuple{esift, Tuple{pf2, Tuple{hho2, Tuple{hlay2, hms2}}}}}:
99 (ST.Sh{1n+size, d, t2},
100 (Equal.trans(H.Heap<A>, H.push(~A, ~cmp, ST.real(~A, sh0), x), H.BH{1n+size, U32.from_nat(1n+size), d, U.pow2u(d), H.sift_up(~A, ~cmp, d, U32.from_nat(size), x, AR.thaw(Maybe<&2, A>, t))}, ST.real(~A, ST.Sh{1n+size, d, t2}), eq0,
101 Equal.cong(Array<Maybe<&2, A>>, H.Heap<A>, a => H.BH{1n+size, U32.from_nat(1n+size), d, U.pow2u(d), a}, H.sift_up(~A, ~cmp, d, U32.from_nat(size), x, AR.thaw(Maybe<&2, A>, t)), AR.thaw(Maybe<&2, A>, t2), esift)),
102 (ST.good_intro(~A, ~cmp, 1n+size, d, t2, hd, pf2, hlay2, hho2, hs),
103 (hms2, hdd))))
104
105# ---- the capacity decision, in Nat ----
106
107def room_bridge(+size: Nat, +depth: Nat, +hd: {Nat.is_le(depth, 31n) == True{} : Bool}, +hs: {Nat.is_le(size, SC.pow2(depth)) == True{} : Bool}) -> {U32.is_lt(U32.from_nat(size), U.pow2u(depth)) == Nat.is_lt(size, SC.pow2(depth)) : Bool}:
108 +hk = N.le_lt_trans(size, SC.pow2(depth), SC.pow2(1n+depth), hs, N.pow2_lt_succ(depth))
109 Equal.sym(Bool, Nat.is_lt(size, SC.pow2(depth)), U32.is_lt(U32.from_nat(size), U.pow2u(depth)),
110 %UX.nat_round(size, 1n+depth, hd, hk) : {Nat.is_lt(_, SC.pow2(depth)) == U32.is_lt(U32.from_nat(size), U.pow2u(depth)) : Bool}
111 AR.lt_bridge(U32.from_nat(size), depth, ST.depth_lt32(depth, hd), U32.is_lt(U32.from_nat(size), U.pow2u(depth)), {==}))
112
113def succ_le_double(+p: Nat, +h: {Nat.is_le(1n, p) == True{} : Bool}) -> {Nat.is_le(1n+p, Nat.double(p)) == True{} : Bool}:
114 match p:
115 case 0n:
116 Empty.absurd({Nat.is_le(1n, Nat.double(0n)) == True{} : Bool}, L.true_not_false(Nat.is_le(1n, 0n), h, {==}))
117 case 1n+ +k:
118 IX.double_le(k)
119
120# ---- push into a block with room ----
121
122def push_room_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +x: A, +g: {ST.good(~A, ~cmp, ST.Sh{size, depth, t}) == True{} : Bool}, +hlt: {Nat.is_lt(size, SC.pow2(depth)) == True{} : Bool}) -> PushOK(~A, ~cmp, ST.Sh{size, depth, t}, x):
123 +hd = ST.g_depth(~A, ~cmp, size, depth, t, g)
124 +pf = ST.g_perfect(~A, ~cmp, size, depth, t, g)
125 push_from(~A, ~cmp, ST.Sh{size, depth, t}, size, depth, t, x, S.ins(~A, ~cmp, x, ST.model(~A, ~cmp, ST.Sh{size, depth, t})), hd,
126 N.lt_succ_le_succ(size, SC.pow2(depth), hlt), N.le_succ(depth),
127 %Equal.sym(Bool, U32.is_lt(U32.from_nat(size), U.pow2u(depth)), Nat.is_lt(size, SC.pow2(depth)), room_bridge(size, depth, hd, ST.g_size(~A, ~cmp, size, depth, t, g))) : {H.push_room(~A, ~cmp, size, U32.from_nat(size), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), x, _) == H.BH{1n+size, U32.from_nat(1n+size), depth, U.pow2u(depth), H.sift_up(~A, ~cmp, depth, U32.from_nat(size), x, AR.thaw(Maybe<&2, A>, t))} : H.Heap<A>}
128 %Equal.sym(Bool, Nat.is_lt(size, SC.pow2(depth)), True{}, hlt) : {H.push_room(~A, ~cmp, size, U32.from_nat(size), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), x, _) == H.BH{1n+size, U32.from_nat(1n+size), depth, U.pow2u(depth), H.sift_up(~A, ~cmp, depth, U32.from_nat(size), x, AR.thaw(Maybe<&2, A>, t))} : H.Heap<A>}
129 {==},
130 UPS.sift_up_ok(~A, ~cmp, ~o, depth, depth, 1n+size, S.ins(~A, ~cmp, x, ST.model(~A, ~cmp, ST.Sh{size, depth, t})), t, size, x,
131 ST.depth_lt32(depth, hd), hlt, N.lt_succ(size), hlt, pf,
132 exc_up(~A, ~cmp, t, size, x, 1n+size, N.le_refl(1n+size), ST.g_ho(~A, ~cmp, size, depth, t, g)),
133 kids_leaf(~A, ~cmp, UPS.ulog(~A, t, size, x), IX.par(size), size),
134 lay_push(~A, depth, t, size, x, hlt, pf, ST.g_lay(~A, ~cmp, size, depth, t, g)),
135 ms_push(~A, ~cmp, depth, t, size, x, hlt, pf)))
136
137# ---- push into a full block: double it first ----
138
139def push_grow_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +x: A, +g: {ST.good(~A, ~cmp, ST.Sh{size, depth, t}) == True{} : Bool}, +hfull: {Nat.is_lt(size, SC.pow2(depth)) == False{} : Bool}, +hroom: {Nat.is_lt(depth, 31n) == True{} : Bool}) -> PushOK(~A, ~cmp, ST.Sh{size, depth, t}, x):
140 +hd = ST.g_depth(~A, ~cmp, size, depth, t, g)
141 +pf = ST.g_perfect(~A, ~cmp, size, depth, t, g)
142 +hs = ST.g_size(~A, ~cmp, size, depth, t, g)
143 +t2 = GR.gtree(~A, depth, t)
144 +pf2 = GR.gtree_perfect(~A, depth, t, pf)
145 +hi2 = N.le_lt_trans(size, SC.pow2(depth), SC.pow2(1n+depth), hs, N.pow2_lt_succ(depth))
146 +hs2 = N.le_trans(1n+size, 1n+SC.pow2(depth), SC.pow2(1n+depth), hs, succ_le_double(SC.pow2(depth), N.pow2_pos(depth)))
147 push_from(~A, ~cmp, ST.Sh{size, depth, t}, size, 1n+depth, t2, x, S.ins(~A, ~cmp, x, ST.model(~A, ~cmp, ST.Sh{size, depth, t})), N.lt_succ_le_succ(depth, 31n, hroom), hs2, N.le_refl(1n+depth),
148 %AR.new(Maybe<&2, A>, depth, None{}) : {H.push_room(~A, ~cmp, size, U32.from_nat(size), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), x, U32.is_lt(U32.from_nat(size), U.pow2u(depth))) == H.BH{1n+size, U32.from_nat(1n+size), 1n+depth, U.pow2u(1n+depth), H.sift_up(~A, ~cmp, 1n+depth, U32.from_nat(size), x, ANode{AR.thaw(Maybe<&2, A>, t), _})} : H.Heap<A>}
149 %Equal.sym(Bool, U32.is_lt(U32.from_nat(size), U.pow2u(depth)), Nat.is_lt(size, SC.pow2(depth)), room_bridge(size, depth, hd, hs)) : {H.push_room(~A, ~cmp, size, U32.from_nat(size), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), x, _) == H.BH{1n+size, U32.from_nat(1n+size), 1n+depth, U.pow2u(1n+depth), H.sift_up(~A, ~cmp, 1n+depth, U32.from_nat(size), x, H.grown(~A, depth, AR.thaw(Maybe<&2, A>, t)))} : H.Heap<A>}
150 %Equal.sym(Bool, Nat.is_lt(size, SC.pow2(depth)), False{}, hfull) : {H.push_room(~A, ~cmp, size, U32.from_nat(size), depth, U.pow2u(depth), AR.thaw(Maybe<&2, A>, t), x, _) == H.BH{1n+size, U32.from_nat(1n+size), 1n+depth, U.pow2u(1n+depth), H.sift_up(~A, ~cmp, 1n+depth, U32.from_nat(size), x, H.grown(~A, depth, AR.thaw(Maybe<&2, A>, t)))} : H.Heap<A>}
151 {==},
152 L.subst(List<&2, A>, zs => UPS.SiftOK(~A, ~cmp, 1n+depth, 1n+size, S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, zs)), 1n+depth, t2, size, x), V.vals(~A, AR.slots(Maybe<&2, A>, t2), size), V.vals(~A, AR.slots(Maybe<&2, A>, t), size), GR.gtree_vals(~A, depth, t, size, pf, hs),
153 UPS.sift_up_ok(~A, ~cmp, ~o, 1n+depth, 1n+depth, 1n+size, S.ins(~A, ~cmp, x, V.msort(~A, ~cmp, V.vals(~A, AR.slots(Maybe<&2, A>, t2), size))), t2, size, x,
154 ST.depth_lt32(1n+depth, N.lt_succ_le_succ(depth, 31n, hroom)), hi2, N.lt_succ(size), hi2, pf2,
155 exc_up(~A, ~cmp, t2, size, x, 1n+size, N.le_refl(1n+size), GR.gtree_ho(~A, ~cmp, depth, t, size, pf, hs, ST.g_ho(~A, ~cmp, size, depth, t, g))),
156 kids_leaf(~A, ~cmp, UPS.ulog(~A, t2, size, x), IX.par(size), size),
157 lay_push(~A, 1n+depth, t2, size, x, hi2, pf2, GR.gtree_lay(~A, depth, t, size, pf, hs, ST.g_lay(~A, ~cmp, size, depth, t, g))),
158 ms_push(~A, ~cmp, 1n+depth, t2, size, x, hi2, pf2))))
159
160def push_ok(~A: Data, ~cmp: A -> A -> Cmp, ~o: O.Order(~A, ~cmp), +size: Nat, +depth: Nat, +t: AR.Tree<Maybe<&2, A>>, +x: A, +g: {ST.good(~A, ~cmp, ST.Sh{size, depth, t}) == True{} : Bool}, +hroom: {Bool.or(Nat.is_lt(size, SC.pow2(depth)), Nat.is_lt(depth, 31n)) == True{} : Bool}, b: Bool, +eb: {Nat.is_lt(size, SC.pow2(depth)) == b : Bool}) -> PushOK(~A, ~cmp, ST.Sh{size, depth, t}, x):
161 match b:
162 case True{}:
163 push_room_ok(~A, ~cmp, ~o, size, depth, t, x, g, eb)
164 case False{}:
165 push_grow_ok(~A, ~cmp, ~o, size, depth, t, x, g, eb,
166 L.subst(Bool, c => {Bool.or(c, Nat.is_lt(depth, 31n)) == True{} : Bool}, Nat.is_lt(size, SC.pow2(depth)), False{}, eb, hroom))