proof_fast_find2.bend

lawful-bytes@0.1.1.0 · 704 lines · 22 definitions

1import Base
2import lawful-bytes@0.1.1.0/defs.bend as D
3import lawful-bytes@0.1.1.0/bytes.bend as B
4import lawful-bytes@0.1.1.0/fast.bend as FA
5import lawful-bytes@0.1.1.0/proof_seq.bend as Q
6import lawful-bytes@0.1.1.0/proof_core.bend as C
7import lawful-bytes@0.1.1.0/proof_find.bend as F
8import lawful-bytes@0.1.1.0/proof_append.bend as X
9import lawful-bytes@0.1.1.0/proof_shift.bend as H
10import lawful-bytes@0.1.1.0/proof_fast_word.bend as FW
11import lawful-bytes@0.1.1.0/proof_fast_find.bend as FF
12import lawful-words@0.1.0.0/defs.bend as W
13import lawful-words@0.1.0.0/proof_nat.bend as N
14import lawful-words@0.1.0.0/proof_u32.bend as U
15import lawful-arrays@0.1.0.0/proof_base.bend as AB
16import lawful-arrays@0.1.0.0/proof_tree.bend as P
17import lawful-arrays@0.1.0.0/defs.bend as A
18
19# fast.bend's find2 on the mirror, the same way as find (proof_fast_find.bend,
20# whose word and list lemmas are reused): the mask is the or of two flag
21# words, its place the min of their places, and the spec run_len2/first2.
22
23# Whether the head of a list is c1 or c2.
24def hd2(xs: List<&2, U32>, +c1: U32, +c2: U32) -> Bool:
25  match xs:
26    case Nil{}:
27      False{}
28    case Con{+x, t}:
29      U32.is_eq(x, c1) || U32.is_eq(x, c2)
30
31def FG2(n: Nat, z: Bool, +wi: U32, +m: U32, +r1: U32, +r2: U32, +t: P.Tree<U32>) -> U32:
32  match n z:
33    case 0n _:
34      4294967295
35    case 1n+k True{}:
36      +m2 = (FA.zb((C.WD(t, (wi + 1 : U32)) .^. r1 : U32)) .|. FA.zb((C.WD(t, (wi + 1 : U32)) .^. r2 : U32)) : U32)
37      FG2(k, U32.is_zero(m2), (wi + 1 : U32), m2, r1, r2, t)
38    case 1n+k False{}:
39      ((wi << 2n : U32) + FA.bidx(m) : U32)
40
41law fg2_eq:
42  for +n: Nat
43  for +z: Bool
44  for +wi: U32
45  for +m: U32
46  for +r1: U32
47  for +r2: U32
48  for +t: P.Tree<U32>
49  {FA.find2.go(n, z, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), wi, m, r1, r2) == (P.fromT(U32, t), FG2(n, z, wi, m, r1, r2, t)) : Array<U32> & U32}
50
51def fg2_eq(n, z, wi, m, r1, r2, t):
52  match n z:
53    case 0n _:
54      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), (P.fromT(U32, t), C.WD(t, (wi + 1 : U32))), P.get_pair_t(U32, t, (wi + 1 : U32))) :
55        {FA.find2.go(0n, z, _, wi, m, r1, r2) == (P.fromT(U32, t), FG2(0n, z, wi, m, r1, r2, t)) : Array<U32> & U32}
56      {==}
57    case 1n+k True{}:
58      +m2 = (FA.zb((C.WD(t, (wi + 1 : U32)) .^. r1 : U32)) .|. FA.zb((C.WD(t, (wi + 1 : U32)) .^. r2 : U32)) : U32)
59      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), (P.fromT(U32, t), C.WD(t, (wi + 1 : U32))), P.get_pair_t(U32, t, (wi + 1 : U32))) :
60        {FA.find2.go(1n+k, True{}, _, wi, m, r1, r2) == (P.fromT(U32, t), FG2(1n+k, True{}, wi, m, r1, r2, t)) : Array<U32> & U32}
61      %F.add11(wi) :
62        {FA.find2.go(k, U32.is_zero(m2), Array.get(U32, P.fromT(U32, t), _), (wi + 1 : U32), m2, r1, r2) == (P.fromT(U32, t), FG2(k, U32.is_zero(m2), (wi + 1 : U32), m2, r1, r2, t)) : Array<U32> & U32}
63      fg2_eq(k, U32.is_zero(m2), (wi + 1 : U32), m2, r1, r2, t)
64    case 1n+k False{}:
65      %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), (wi + 1 : U32)), (P.fromT(U32, t), C.WD(t, (wi + 1 : U32))), P.get_pair_t(U32, t, (wi + 1 : U32))) :
66        {FA.find2.go(1n+k, False{}, _, wi, m, r1, r2) == (P.fromT(U32, t), FG2(1n+k, False{}, wi, m, r1, r2, t)) : Array<U32> & U32}
67      {==}
68
69def M02(+t: P.Tree<U32>, +from: U32, +r1: U32, +r2: U32) -> U32:
70  (FA.zb(((C.WD(t, (from >> 2n : U32)) .^. r1 : U32) .|. U32.not(FA.low(from)) : U32)) .|. FA.zb(((C.WD(t, (from >> 2n : U32)) .^. r2 : U32) .|. U32.not(FA.low(from)) : U32)) : U32)
71
72law fast2_eq:
73  for +len: U32
74  for +t: P.Tree<U32>
75  for +from: U32
76  for +to: U32
77  for +c1: U32
78  for +c2: U32
79  {FA.find2(C.BT(len, t), from, to, c1, c2) == (C.BT(len, t), U32.min(FG2(FA.words(from, to), U32.is_zero(M02(t, from, FA.rep(c1), FA.rep(c2))), (from >> 2n : U32), M02(t, from, FA.rep(c1), FA.rep(c2)), FA.rep(c1), FA.rep(c2), t), to)) : D.Bytes & U32}
80
81def fast2_eq(len, t, from, to, c1, c2):
82  +k = (from >> 2n : U32)
83  +r1 = FA.rep(c1)
84  +r2 = FA.rep(c2)
85  +n = FA.words(from, to)
86  %Equal.sym(Array<U32> & U32, Array.get(U32, P.fromT(U32, t), k), (P.fromT(U32, t), C.WD(t, k)), P.get_pair_t(U32, t, k)) :
87    {FA.find.k(len, FA.find.fin(to, FA.find2.start(n, _, from, r1, r2))) == (C.BT(len, t), U32.min(FG2(n, U32.is_zero(M02(t, from, r1, r2)), k, M02(t, from, r1, r2), r1, r2, t), to)) : D.Bytes & U32}
88  %Equal.sym(Array<U32> & U32, FA.find2.go(n, U32.is_zero(M02(t, from, r1, r2)), Array.get(U32, P.fromT(U32, t), (k + 1 : U32)), k, M02(t, from, r1, r2), r1, r2),
89    (P.fromT(U32, t), FG2(n, U32.is_zero(M02(t, from, r1, r2)), k, M02(t, from, r1, r2), r1, r2, t)), fg2_eq(n, U32.is_zero(M02(t, from, r1, r2)), k, M02(t, from, r1, r2), r1, r2, t)) :
90    {FA.find.k(len, FA.find.fin(to, _)) == (C.BT(len, t), U32.min(FG2(n, U32.is_zero(M02(t, from, r1, r2)), k, M02(t, from, r1, r2), r1, r2, t), to)) : D.Bytes & U32}
91  {==}
92
93# Two runs and their min
94# ======================
95
96law min_le_l:
97  for +a: Nat
98  for +b: Nat
99  {Nat.is_le(Nat.min(a, b), a) == True{} : Bool}
100
101def min_le_l(a, b):
102  match a b:
103    case 0n _:
104      {==}
105    case 1n+p 0n:
106      {==}
107    case 1n+p 1n+q:
108      min_le_l(p, q)
109
110law min_le4:
111  for +v1: U32
112  for +v2: U32
113  {Nat.is_le(Nat.min(FW.P0(v1), FW.P0(v2)), 4n) == True{} : Bool}
114
115def min_le4(v1, v2):
116  N.le_trans(Nat.min(FW.P0(v1), FW.P0(v2)), FW.P0(v1), 4n, min_le_l(FW.P0(v1), FW.P0(v2)), FF.run_le(C.L4(v1), 0, FF.hd_eq(C.L4(v1), 0), {==}))
117
118law min_add:
119  for +o: Nat
120  for +a: Nat
121  for +b: Nat
122  {Nat.min(Nat.add(o, a), Nat.add(o, b)) == Nat.add(o, Nat.min(a, b)) : Nat}
123
124def min_add(o, a, b):
125  match o:
126    case 0n:
127      {==}
128    case 1n+p:
129      %min_add(p, a, b) : {1n+Nat.min(Nat.add(p, a), Nat.add(p, b)) == 1n+_ : Nat}
130      {==}
131
132# The first c1 or c2 is the earlier of the first c1 and the first c2.
133law min_run:
134  for +xs: List<&2, U32>
135  for +c1: U32
136  for +c2: U32
137  for +b1: Bool
138  for +b2: Bool
139  for +hb1: {FF.hd_eq(xs, c1) == b1 : Bool}
140  for +hb2: {FF.hd_eq(xs, c2) == b2 : Bool}
141  {Nat.min(D.run_len(xs, c1), D.run_len(xs, c2)) == D.run_len2(xs, c1, c2) : Nat}
142
143def min_run(xs, c1, c2, b1, b2, hb1, hb2):
144  match xs b1 b2:
145    case Nil{} _ _:
146      {==}
147    case Con{x, t} True{} _:
148      %Equal.sym(Bool, FF.hd_eq(x <> t, c1), True{}, hb1) :
149        {Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c1))), Bool.pick(Nat, U32.is_eq(x, c2), 0n, Nat.add(1n, D.run_len(t, c2)))) == Bool.pick(Nat, Bool.or(_, U32.is_eq(x, c2)), 0n, Nat.add(1n, D.run_len2(t, c1, c2))) : Nat}
150      {==}
151    case Con{x, t} False{} True{}:
152      %Equal.sym(Bool, FF.hd_eq(x <> t, c1), False{}, hb1) :
153        {Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c1))), Bool.pick(Nat, U32.is_eq(x, c2), 0n, Nat.add(1n, D.run_len(t, c2)))) == Bool.pick(Nat, Bool.or(_, U32.is_eq(x, c2)), 0n, Nat.add(1n, D.run_len2(t, c1, c2))) : Nat}
154      %Equal.sym(Bool, FF.hd_eq(x <> t, c2), True{}, hb2) :
155        {Nat.min(1n+D.run_len(t, c1), Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c2)))) == Bool.pick(Nat, Bool.or(False{}, _), 0n, Nat.add(1n, D.run_len2(t, c1, c2))) : Nat}
156      {==}
157    case Con{x, t} False{} False{}:
158      %Equal.sym(Bool, FF.hd_eq(x <> t, c1), False{}, hb1) :
159        {Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c1))), Bool.pick(Nat, U32.is_eq(x, c2), 0n, Nat.add(1n, D.run_len(t, c2)))) == Bool.pick(Nat, Bool.or(_, U32.is_eq(x, c2)), 0n, Nat.add(1n, D.run_len2(t, c1, c2))) : Nat}
160      %Equal.sym(Bool, FF.hd_eq(x <> t, c2), False{}, hb2) :
161        {Nat.min(1n+D.run_len(t, c1), Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len(t, c2)))) == Bool.pick(Nat, Bool.or(False{}, _), 0n, Nat.add(1n, D.run_len2(t, c1, c2))) : Nat}
162      %min_run(t, c1, c2, FF.hd_eq(t, c1), FF.hd_eq(t, c2), {==}, {==}) : {1n+Nat.min(D.run_len(t, c1), D.run_len(t, c2)) == 1n+_ : Nat}
163      {==}
164
165# The first word of a search, for two values.
166law p0_low2:
167  for +w: U32
168  for +c1: U32
169  for +c2: U32
170  for +i: U32
171  for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
172  for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
173  {Nat.min(FW.P0(U32.or(U32.xor(w, FA.rep(c1)), U32.not(FA.low(i)))), FW.P0(U32.or(U32.xor(w, FA.rep(c2)), U32.not(FA.low(i))))) == Nat.add(U32.to_nat((i .&. 3 : U32)), D.run_len2(List.drop(&2, U32, C.L4(w), U32.to_nat((i .&. 3 : U32))), c1, c2)) : Nat}
174
175def p0_low2(w, c1, c2, i, hc1, hc2):
176  +o = U32.to_nat((i .&. 3 : U32))
177  +ys = List.drop(&2, U32, C.L4(w), o)
178  %Equal.sym(Nat, FW.P0(U32.or(U32.xor(w, FA.rep(c1)), U32.not(FA.low(i)))), Nat.add(o, D.run_len(ys, c1)), FW.p0_low(w, c1, i, hc1)) :
179    {Nat.min(_, FW.P0(U32.or(U32.xor(w, FA.rep(c2)), U32.not(FA.low(i))))) == Nat.add(o, D.run_len2(ys, c1, c2)) : Nat}
180  %Equal.sym(Nat, FW.P0(U32.or(U32.xor(w, FA.rep(c2)), U32.not(FA.low(i)))), Nat.add(o, D.run_len(ys, c2)), FW.p0_low(w, c2, i, hc2)) :
181    {Nat.min(Nat.add(o, D.run_len(ys, c1)), _) == Nat.add(o, D.run_len2(ys, c1, c2)) : Nat}
182  %Equal.sym(Nat, Nat.min(Nat.add(o, D.run_len(ys, c1)), Nat.add(o, D.run_len(ys, c2))), Nat.add(o, Nat.min(D.run_len(ys, c1), D.run_len(ys, c2))), min_add(o, D.run_len(ys, c1), D.run_len(ys, c2))) :
183    {_ == Nat.add(o, D.run_len2(ys, c1, c2)) : Nat}
184  %Equal.sym(Nat, Nat.min(D.run_len(ys, c1), D.run_len(ys, c2)), D.run_len2(ys, c1, c2), min_run(ys, c1, c2, FF.hd_eq(ys, c1), FF.hd_eq(ys, c2), {==}, {==})) :
185    {Nat.add(o, _) == Nat.add(o, D.run_len2(ys, c1, c2)) : Nat}
186  {==}
187
188# The next word starts a fresh search.
189law hv02:
190  for +t: P.Tree<U32>
191  for +wi: U32
192  for +c1: U32
193  for +c2: U32
194  for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
195  for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
196  {Nat.min(FW.P0(U32.xor(C.WD(t, wi), FA.rep(c1))), FW.P0(U32.xor(C.WD(t, wi), FA.rep(c2)))) == Nat.add(0n, D.run_len2(FF.AW(t, wi, 0n), c1, c2)) : Nat}
197
198def hv02(t, wi, c1, c2, hc1, hc2):
199  +ws = C.L4(C.WD(t, wi))
200  %Equal.sym(List<&2, U32>, List.drop(&2, U32, ws, 0n), ws, X.drop_zero(ws)) :
201    {Nat.min(FW.P0(U32.xor(C.WD(t, wi), FA.rep(c1))), FW.P0(U32.xor(C.WD(t, wi), FA.rep(c2)))) == Nat.add(0n, D.run_len2(_, c1, c2)) : Nat}
202  %Equal.sym(Nat, FW.P0(U32.xor(C.WD(t, wi), FA.rep(c1))), D.run_len(ws, c1), FW.p0_xor(C.WD(t, wi), c1, hc1)) :
203    {Nat.min(_, FW.P0(U32.xor(C.WD(t, wi), FA.rep(c2)))) == D.run_len2(ws, c1, c2) : Nat}
204  %Equal.sym(Nat, FW.P0(U32.xor(C.WD(t, wi), FA.rep(c2))), D.run_len(ws, c2), FW.p0_xor(C.WD(t, wi), c2, hc2)) :
205    {Nat.min(D.run_len(ws, c1), _) == D.run_len2(ws, c1, c2) : Nat}
206  min_run(ws, c1, c2, FF.hd_eq(ws, c1), FF.hd_eq(ws, c2), {==}, {==})
207
208# The word loop (from proof_fast_find.bend, for two values)
209# =========================================================
210
211law run_hit2:
212  for +xs: List<&2, U32>
213  for +ys: List<&2, U32>
214  for +n: Nat
215  for +c1: U32
216  for +c2: U32
217  for +b: Bool
218  for +hb: {hd2(xs, c1, c2) == b : Bool}
219  for +h: {Nat.is_lt(D.run_len2(xs, c1, c2), List.length(&2, U32, xs)) == True{} : Bool}
220  {D.run_len2(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c1, c2) == Nat.min(D.run_len2(xs, c1, c2), n) : Nat}
221
222def run_hit2(xs, ys, n, c1, c2, b, hb, h):
223  match xs n b:
224    case Nil{} _ _:
225      Empty.absurd({D.run_len2(List.take(&2, U32, ys, n), c1, c2) == Nat.min(0n, n) : Nat}, AB.lt_zero_absurd(0n, h))
226    case Con{x, t} 0n True{}:
227      %Equal.sym(Bool, hd2(x <> t, c1, c2), True{}, hb) : {0n == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(t, c1, c2))), 0n) : Nat}
228      {==}
229    case Con{x, t} 0n False{}:
230      %Equal.sym(Bool, hd2(x <> t, c1, c2), False{}, hb) : {0n == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(t, c1, c2))), 0n) : Nat}
231      {==}
232    case Con{x, t} 1n+p True{}:
233      %Equal.sym(Bool, hd2(x <> t, c1, c2), True{}, hb) :
234        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2))) == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(t, c1, c2))), 1n+p) : Nat}
235      {==}
236    case Con{x, t} 1n+p False{}:
237      %Equal.sym(Bool, hd2(x <> t, c1, c2), False{}, hb) :
238        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2))) == Nat.min(Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(t, c1, c2))), 1n+p) : Nat}
239      +h2 = AB.subst(Bool, y => {Nat.is_lt(Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len2(t, c1, c2))), 1n+List.length(&2, U32, t)) == True{} : Bool},
240        hd2(x <> t, c1, c2), False{}, hb, h)
241      %run_hit2(t, ys, p, c1, c2, hd2(t, c1, c2), {==}, h2) :
242        {1n+D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2) == 1n+_ : Nat}
243      {==}
244
245law run_skip2:
246  for +xs: List<&2, U32>
247  for +ys: List<&2, U32>
248  for +n: Nat
249  for +c1: U32
250  for +c2: U32
251  for +b: Bool
252  for +hb: {hd2(xs, c1, c2) == b : Bool}
253  for +h: {D.run_len2(xs, c1, c2) == List.length(&2, U32, xs) : Nat}
254  for +hn: {Nat.is_le(List.length(&2, U32, xs), n) == True{} : Bool}
255  {D.run_len2(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c1, c2) == Nat.add(List.length(&2, U32, xs), D.run_len2(List.take(&2, U32, ys, Nat.sub(n, List.length(&2, U32, xs))), c1, c2)) : Nat}
256
257def run_skip2(xs, ys, n, c1, c2, b, hb, h, hn):
258  match xs n b:
259    case Nil{} _ _:
260      %Equal.sym(Nat, Nat.sub(n, 0n), n, N.sub_zero(n)) :
261        {D.run_len2(List.take(&2, U32, ys, n), c1, c2) == D.run_len2(List.take(&2, U32, ys, _), c1, c2) : Nat}
262      {==}
263    case Con{x, t} _ True{}:
264      Empty.absurd({D.run_len2(List.take(&2, U32, List.append(&2, U32, x <> t, ys), n), c1, c2) == Nat.add(1n+List.length(&2, U32, t), D.run_len2(List.take(&2, U32, ys, Nat.sub(n, 1n+List.length(&2, U32, t))), c1, c2)) : Nat},
265        N.zero_ne_succ(List.length(&2, U32, t), AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len2(t, c1, c2))) == 1n+List.length(&2, U32, t) : Nat},
266          hd2(x <> t, c1, c2), True{}, hb, h)))
267    case Con{x, t} 0n False{}:
268      Empty.absurd({0n == Nat.add(1n+List.length(&2, U32, t), D.run_len2(List.take(&2, U32, ys, Nat.sub(0n, 1n+List.length(&2, U32, t))), c1, c2)) : Nat},
269        AB.false_ne_true(hn))
270    case Con{x, t} 1n+p False{}:
271      %Equal.sym(Bool, hd2(x <> t, c1, c2), False{}, hb) :
272        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2))) == 1n+Nat.add(List.length(&2, U32, t), D.run_len2(List.take(&2, U32, ys, Nat.sub(p, List.length(&2, U32, t))), c1, c2)) : Nat}
273      +h2 = N.succ_inj(D.run_len2(t, c1, c2), List.length(&2, U32, t),
274        AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len2(t, c1, c2))) == 1n+List.length(&2, U32, t) : Nat}, hd2(x <> t, c1, c2), False{}, hb, h))
275      %run_skip2(t, ys, p, c1, c2, hd2(t, c1, c2), {==}, h2, hn) :
276        {1n+D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2) == 1n+_ : Nat}
277      {==}
278
279law run_none2:
280  for +xs: List<&2, U32>
281  for +ys: List<&2, U32>
282  for +n: Nat
283  for +c1: U32
284  for +c2: U32
285  for +b: Bool
286  for +hb: {hd2(xs, c1, c2) == b : Bool}
287  for +h: {D.run_len2(xs, c1, c2) == List.length(&2, U32, xs) : Nat}
288  for +hn: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}
289  {D.run_len2(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c1, c2) == n : Nat}
290
291def run_none2(xs, ys, n, c1, c2, b, hb, h, hn):
292  match xs n b:
293    case Nil{} 0n _:
294      %Equal.sym(List<&2, U32>, List.take(&2, U32, ys, 0n), Nil{}, Q.take_zero(ys)) : {D.run_len2(_, c1, c2) == 0n : Nat}
295      {==}
296    case Nil{} 1n+p _:
297      Empty.absurd({D.run_len2(List.take(&2, U32, ys, 1n+p), c1, c2) == 1n+p : Nat}, AB.false_ne_true(hn))
298    case Con{x, t} 0n _:
299      {==}
300    case Con{x, t} 1n+p True{}:
301      Empty.absurd({D.run_len2(List.take(&2, U32, List.append(&2, U32, x <> t, ys), 1n+p), c1, c2) == 1n+p : Nat},
302        N.zero_ne_succ(List.length(&2, U32, t), AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len2(t, c1, c2))) == 1n+List.length(&2, U32, t) : Nat},
303          hd2(x <> t, c1, c2), True{}, hb, h)))
304    case Con{x, t} 1n+p False{}:
305      %Equal.sym(Bool, hd2(x <> t, c1, c2), False{}, hb) :
306        {Bool.pick(Nat, _, 0n, Nat.add(1n, D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2))) == 1n+p : Nat}
307      +h2 = N.succ_inj(D.run_len2(t, c1, c2), List.length(&2, U32, t),
308        AB.subst(Bool, y => {Bool.pick(Nat, y, 0n, Nat.add(1n, D.run_len2(t, c1, c2))) == 1n+List.length(&2, U32, t) : Nat}, hd2(x <> t, c1, c2), False{}, hb, h))
309      %run_none2(t, ys, p, c1, c2, hd2(t, c1, c2), {==}, h2, hn) : {1n+D.run_len2(List.take(&2, U32, List.append(&2, U32, t, ys), p), c1, c2) == 1n+_ : Nat}
310      {==}
311
312law fhit2:
313  for +len: U32
314  for +t: P.Tree<U32>
315  for +d: Nat
316  for +to: U32
317  for +c1: U32
318  for +c2: U32
319  for +wi: U32
320  for +o: Nat
321  for +v1: U32
322  for +v2: U32
323  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
324  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
325  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
326  for +hs: {Nat.is_le(FF.SS(wi, o), U32.to_nat(to)) == True{} : Bool}
327  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
328  for +hv: {Nat.min(FW.P0(v1), FW.P0(v2)) == Nat.add(o, D.run_len2(FF.AW(t, wi, o), c1, c2)) : Nat}
329  for +hz: {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == False{} : Bool}
330  {U32.to_nat(U32.min(((wi << 2n : U32) + FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))) : U32), to)) == D.first2(FF.UB(t), FF.SS(wi, o), U32.to_nat(to), c1, c2) : Nat}
331
332def fhit2(len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, ho, hs, hk, hv, hz):
333  +W = U32.to_nat(wi)
334  +T = U32.to_nat(to)
335  +r = D.run_len2(FF.AW(t, wi, o), c1, c2)
336  +M4 = Nat.mul(4n, Nat.pow(2n, d))
337  +hd = C.ok_d(len, t, d, h)
338  +hf = C.ok_full(len, t, d, h)
339  +hp4 = min_le4(v1, v2)
340  +hne = Equal.trans(Bool, Nat.is_eq(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))), False{}, Equal.sym(Bool, U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))), Nat.is_eq(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), FW.zb2_none(v1, v2)), hz)
341  +hlt = Equal.trans(Bool, Nat.is_lt(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), Nat.is_le(1n+Nat.min(FW.P0(v1), FW.P0(v2)), 4n), True{}, Equal.sym(Bool, Nat.is_le(1n+Nat.min(FW.P0(v1), FW.P0(v2)), 4n), Nat.is_lt(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), N.le_succ_lt(Nat.min(FW.P0(v1), FW.P0(v2)), 4n)),
342    N.le_ne(Nat.min(FW.P0(v1), FW.P0(v2)), 4n, hp4, hne))
343  +hlt2 = AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, Nat.min(FW.P0(v1), FW.P0(v2)), Nat.add(o, r), hv, hlt)
344  +eo = N.le_sub_add(o, 4n, N.lt_to_le(o, 4n, ho))
345  +hrl0 = FF.lt_cancel(o, r, Nat.sub(4n, o), AB.subst(Nat, y => {Nat.is_lt(Nat.add(o, r), y) == True{} : Bool}, 4n, Nat.add(o, Nat.sub(4n, o)), Equal.sym(Nat, Nat.add(o, Nat.sub(4n, o)), 4n, eo), hlt2))
346  +hrl = AB.subst(Nat, y => {Nat.is_lt(r, y) == True{} : Bool}, Nat.sub(4n, o), List.length(&2, U32, FF.AW(t, wi, o)), Equal.sym(Nat, List.length(&2, U32, FF.AW(t, wi, o)), Nat.sub(4n, o), FF.awl(t, wi, o)), hrl0)
347  +eb = Equal.trans(Nat, U32.to_nat(FA.bidx(U32.or(FA.zb(v1), FA.zb(v2)))), Nat.min(FW.P0(v1), FW.P0(v2)), Nat.add(o, r), FW.zb2_bidx(v1, v2, hlt), hv)
348  +hw4 = FF.wb4(W, Nat.pow(2n, d), hk)
349  +esh = FF.shl2(wi, d, hd, N.le_trans(Nat.mul(W, 4n), Nat.add(Nat.mul(W, 4n), 4n), M4, N.le_add_r(Nat.mul(W, 4n), 4n), hw4))
350  +b1 = N.le_trans(Nat.add(Nat.mul(W, 4n), Nat.add(o, r)), Nat.add(Nat.mul(W, 4n), 4n), M4,
351    N.le_add_mono_l(Nat.mul(W, 4n), Nat.add(o, r), 4n, N.lt_to_le(Nat.add(o, r), 4n, hlt2)), hw4)
352  +b2 = AB.subst(Nat, y => {Nat.is_le(Nat.add(y, Nat.add(o, r)), M4) == True{} : Bool}, Nat.mul(W, 4n), U32.to_nat((wi << 2n : U32)), Equal.sym(Nat, U32.to_nat((wi << 2n : U32)), Nat.mul(W, 4n), esh), b1)
353  +b3 = AB.subst(Nat, y => {Nat.is_le(Nat.add(U32.to_nat((wi << 2n : U32)), y), M4) == True{} : Bool}, Nat.add(o, r), U32.to_nat(FA.bidx(U32.or(FA.zb(v1), FA.zb(v2)))),
354    Equal.sym(Nat, U32.to_nat(FA.bidx(U32.or(FA.zb(v1), FA.zb(v2)))), Nat.add(o, r), eb), b2)
355  +ej = C.add_fits((wi << 2n : U32), FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))), d, hd, b3)
356  +RHS = D.first2(FF.UB(t), FF.SS(wi, o), T, c1, c2)
357  %Equal.sym(Nat, U32.to_nat(U32.min(((wi << 2n : U32) + FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))) : U32), to)), Nat.min(U32.to_nat(((wi << 2n : U32) + FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))) : U32)), T),
358    U.to_nat_min(((wi << 2n : U32) + FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))) : U32), to)) :
359    {_ == RHS : Nat}
360  %Equal.sym(Nat, U32.to_nat(((wi << 2n : U32) + FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))) : U32)), Nat.add(U32.to_nat((wi << 2n : U32)), U32.to_nat(FA.bidx(U32.or(FA.zb(v1), FA.zb(v2))))), ej) :
361    {Nat.min(_, T) == RHS : Nat}
362  %Equal.sym(Nat, U32.to_nat(FA.bidx(U32.or(FA.zb(v1), FA.zb(v2)))), Nat.add(o, r), eb) :
363    {Nat.min(Nat.add(U32.to_nat((wi << 2n : U32)), _), T) == RHS : Nat}
364  %Equal.sym(Nat, U32.to_nat((wi << 2n : U32)), Nat.mul(W, 4n), esh) :
365    {Nat.min(Nat.add(_, Nat.add(o, r)), T) == RHS : Nat}
366  %N.add_assoc(Nat.mul(W, 4n), o, r) :
367    {Nat.min(_, T) == RHS : Nat}
368  %Equal.sym(Nat, Nat.min(Nat.add(FF.SS(wi, o), r), T), Nat.add(FF.SS(wi, o), Nat.min(r, Nat.sub(T, FF.SS(wi, o)))), FF.min_shift(FF.SS(wi, o), r, T, hs)) :
369    {_ == RHS : Nat}
370  %Equal.sym(List<&2, U32>, List.drop(&2, U32, FF.UB(t), FF.SS(wi, o)), List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), FF.dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
371    {Nat.add(FF.SS(wi, o), Nat.min(r, Nat.sub(T, FF.SS(wi, o)))) == Nat.add(FF.SS(wi, o), D.run_len2(List.take(&2, U32, _, Nat.sub(T, FF.SS(wi, o))), c1, c2)) : Nat}
372  %Equal.sym(Nat, D.run_len2(List.take(&2, U32, List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), Nat.sub(T, FF.SS(wi, o))), c1, c2), Nat.min(r, Nat.sub(T, FF.SS(wi, o))),
373    run_hit2(FF.AW(t, wi, o), FF.BW(t, wi), Nat.sub(T, FF.SS(wi, o)), c1, c2, hd2(FF.AW(t, wi, o), c1, c2), {==}, hrl)) :
374    {Nat.add(FF.SS(wi, o), Nat.min(r, Nat.sub(T, FF.SS(wi, o)))) == Nat.add(FF.SS(wi, o), _) : Nat}
375  {==}
376
377law nohit2:
378  for +t: P.Tree<U32>
379  for +wi: U32
380  for +o: Nat
381  for +v1: U32
382  for +v2: U32
383  for +c1: U32
384  for +c2: U32
385  for +hv: {Nat.min(FW.P0(v1), FW.P0(v2)) == Nat.add(o, D.run_len2(FF.AW(t, wi, o), c1, c2)) : Nat}
386  for +hz: {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == True{} : Bool}
387  {D.run_len2(FF.AW(t, wi, o), c1, c2) == List.length(&2, U32, FF.AW(t, wi, o)) : Nat}
388
389def nohit2(t, wi, o, v1, v2, c1, c2, hv, hz):
390  +r = D.run_len2(FF.AW(t, wi, o), c1, c2)
391  +e4 = N.eq_sound(Nat.min(FW.P0(v1), FW.P0(v2)), 4n, Equal.trans(Bool, Nat.is_eq(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))), True{},
392    Equal.sym(Bool, U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))), Nat.is_eq(Nat.min(FW.P0(v1), FW.P0(v2)), 4n), FW.zb2_none(v1, v2)), hz))
393  +e5 = Equal.trans(Nat, Nat.add(o, r), Nat.min(FW.P0(v1), FW.P0(v2)), 4n, Equal.sym(Nat, Nat.min(FW.P0(v1), FW.P0(v2)), Nat.add(o, r), hv), e4)
394  %Equal.sym(Nat, List.length(&2, U32, FF.AW(t, wi, o)), Nat.sub(4n, o), FF.awl(t, wi, o)) : {r == _ : Nat}
395  %e5 : {r == Nat.sub(_, o) : Nat}
396  Equal.sym(Nat, Nat.sub(Nat.add(o, r), o), r, N.sub_add_l(o, r))
397
398law fnone2:
399  for +len: U32
400  for +t: P.Tree<U32>
401  for +d: Nat
402  for +to: U32
403  for +c1: U32
404  for +c2: U32
405  for +wi: U32
406  for +o: Nat
407  for +v1: U32
408  for +v2: U32
409  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
410  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
411  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
412  for +hs: {Nat.is_le(FF.SS(wi, o), U32.to_nat(to)) == True{} : Bool}
413  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
414  for +hv: {Nat.min(FW.P0(v1), FW.P0(v2)) == Nat.add(o, D.run_len2(FF.AW(t, wi, o), c1, c2)) : Nat}
415  for +hz: {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == True{} : Bool}
416  for +he: {Nat.is_le(U32.to_nat(to), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n)) == True{} : Bool}
417  {U32.to_nat(U32.min(4294967295, to)) == D.first2(FF.UB(t), FF.SS(wi, o), U32.to_nat(to), c1, c2) : Nat}
418
419def fnone2(len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, ho, hs, hk, hv, hz, he):
420  +W = U32.to_nat(wi)
421  +T = U32.to_nat(to)
422  +X = Nat.sub(T, FF.SS(wi, o))
423  +hd = C.ok_d(len, t, d, h)
424  +hf = C.ok_full(len, t, d, h)
425  +a1 = AB.subst(Nat, y => {Nat.is_le(T, y) == True{} : Bool}, Nat.mul(Nat.add(W, 1n), 4n), Nat.add(Nat.mul(W, 4n), 4n), FF.mul4s(W), he)
426  +a2 = AB.subst(Nat, y => {Nat.is_le(y, Nat.add(Nat.mul(W, 4n), 4n)) == True{} : Bool}, T, Nat.add(FF.SS(wi, o), X),
427    Equal.sym(Nat, Nat.add(FF.SS(wi, o), X), T, N.le_sub_add(FF.SS(wi, o), T, hs)), a1)
428  +a3 = AB.subst(Nat, y => {Nat.is_le(y, Nat.add(Nat.mul(W, 4n), 4n)) == True{} : Bool}, Nat.add(Nat.add(Nat.mul(W, 4n), o), X), Nat.add(Nat.mul(W, 4n), Nat.add(o, X)),
429    N.add_assoc(Nat.mul(W, 4n), o, X), a2)
430  +a4 = N.le_sub_r(o, X, 4n, FF.le_cancel(Nat.mul(W, 4n), Nat.add(o, X), 4n, a3))
431  +hn = AB.subst(Nat, y => {Nat.is_le(X, y) == True{} : Bool}, Nat.sub(4n, o), List.length(&2, U32, FF.AW(t, wi, o)),
432    Equal.sym(Nat, List.length(&2, U32, FF.AW(t, wi, o)), Nat.sub(4n, o), FF.awl(t, wi, o)), a4)
433  +RHS = D.first2(FF.UB(t), FF.SS(wi, o), T, c1, c2)
434  %Equal.sym(U32, U32.min(4294967295, to), to, FF.min_top(to, d, hd, N.le_trans(T, U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), ht, C.ok_len(len, t, d, h)))) :
435    {U32.to_nat(_) == RHS : Nat}
436  %Equal.sym(List<&2, U32>, List.drop(&2, U32, FF.UB(t), FF.SS(wi, o)), List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), FF.dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
437    {T == Nat.add(FF.SS(wi, o), D.run_len2(List.take(&2, U32, _, X), c1, c2)) : Nat}
438  %Equal.sym(Nat, D.run_len2(List.take(&2, U32, List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), X), c1, c2), X,
439    run_none2(FF.AW(t, wi, o), FF.BW(t, wi), X, c1, c2, hd2(FF.AW(t, wi, o), c1, c2), {==}, nohit2(t, wi, o, v1, v2, c1, c2, hv, hz), hn)) :
440    {T == Nat.add(FF.SS(wi, o), _) : Nat}
441  Equal.sym(Nat, Nat.add(FF.SS(wi, o), X), T, N.le_sub_add(FF.SS(wi, o), T, hs))
442
443law fskip2:
444  for +len: U32
445  for +t: P.Tree<U32>
446  for +d: Nat
447  for +to: U32
448  for +c1: U32
449  for +c2: U32
450  for +wi: U32
451  for +o: Nat
452  for +v1: U32
453  for +v2: U32
454  for +k: Nat
455  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
456  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
457  for +hs: {Nat.is_le(FF.SS(wi, o), U32.to_nat(to)) == True{} : Bool}
458  for +hk: {Nat.is_lt(U32.to_nat(wi), Nat.pow(2n, d)) == True{} : Bool}
459  for +hv: {Nat.min(FW.P0(v1), FW.P0(v2)) == Nat.add(o, D.run_len2(FF.AW(t, wi, o), c1, c2)) : Nat}
460  for +hz: {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == True{} : Bool}
461  for +hs1: {Nat.is_le(Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n), U32.to_nat(to)) == True{} : Bool}
462  {D.first2(FF.UB(t), FF.SS(wi, o), U32.to_nat(to), c1, c2) == D.first2(FF.UB(t), Nat.mul(Nat.add(U32.to_nat(wi), 1n), 4n), U32.to_nat(to), c1, c2) : Nat}
463
464def fskip2(len, t, d, to, c1, c2, wi, o, v1, v2, k, h, ho, hs, hk, hv, hz, hs1):
465  +W = U32.to_nat(wi)
466  +T = U32.to_nat(to)
467  +S = FF.SS(wi, o)
468  +S1 = Nat.mul(Nat.add(W, 1n), 4n)
469  +L = Nat.sub(4n, o)
470  +hd = C.ok_d(len, t, d, h)
471  +hf = C.ok_full(len, t, d, h)
472  +eS = Equal.trans(Nat, Nat.add(S, L), Nat.add(Nat.mul(W, 4n), Nat.add(o, L)), S1, N.add_assoc(Nat.mul(W, 4n), o, L),
473    Equal.trans(Nat, Nat.add(Nat.mul(W, 4n), Nat.add(o, L)), Nat.add(Nat.mul(W, 4n), 4n), S1,
474      Equal.cong(Nat, Nat, y => Nat.add(Nat.mul(W, 4n), y), Nat.add(o, L), 4n, N.le_sub_add(o, 4n, N.lt_to_le(o, 4n, ho))),
475      Equal.sym(Nat, S1, Nat.add(Nat.mul(W, 4n), 4n), FF.mul4s(W))))
476  +hl0 = N.le_sub_r(S, L, T, AB.subst(Nat, y => {Nat.is_le(y, T) == True{} : Bool}, S1, Nat.add(S, L), Equal.sym(Nat, Nat.add(S, L), S1, eS), hs1))
477  +hn = AB.subst(Nat, y => {Nat.is_le(y, Nat.sub(T, S)) == True{} : Bool}, L, List.length(&2, U32, FF.AW(t, wi, o)),
478    Equal.sym(Nat, List.length(&2, U32, FF.AW(t, wi, o)), L, FF.awl(t, wi, o)), hl0)
479  +RHS = D.first2(FF.UB(t), S1, T, c1, c2)
480  %Equal.sym(List<&2, U32>, List.drop(&2, U32, FF.UB(t), S), List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), FF.dw(t, d, wi, o, hf, hd, hk, N.lt_to_le(o, 4n, ho))) :
481    {Nat.add(S, D.run_len2(List.take(&2, U32, _, Nat.sub(T, S)), c1, c2)) == RHS : Nat}
482  %Equal.sym(Nat, D.run_len2(List.take(&2, U32, List.append(&2, U32, FF.AW(t, wi, o), FF.BW(t, wi)), Nat.sub(T, S)), c1, c2),
483    Nat.add(List.length(&2, U32, FF.AW(t, wi, o)), D.run_len2(List.take(&2, U32, FF.BW(t, wi), Nat.sub(Nat.sub(T, S), List.length(&2, U32, FF.AW(t, wi, o)))), c1, c2)),
484    run_skip2(FF.AW(t, wi, o), FF.BW(t, wi), Nat.sub(T, S), c1, c2, hd2(FF.AW(t, wi, o), c1, c2), {==}, nohit2(t, wi, o, v1, v2, c1, c2, hv, hz), hn)) :
485    {Nat.add(S, _) == RHS : Nat}
486  %Equal.sym(Nat, List.length(&2, U32, FF.AW(t, wi, o)), L, FF.awl(t, wi, o)) :
487    {Nat.add(S, Nat.add(_, D.run_len2(List.take(&2, U32, FF.BW(t, wi), Nat.sub(Nat.sub(T, S), _)), c1, c2))) == RHS : Nat}
488  %Equal.sym(Nat, Nat.sub(Nat.sub(T, S), L), Nat.sub(T, Nat.add(S, L)), FF.sub_sub(T, S, L)) :
489    {Nat.add(S, Nat.add(L, D.run_len2(List.take(&2, U32, FF.BW(t, wi), _), c1, c2))) == RHS : Nat}
490  %N.add_assoc(S, L, D.run_len2(List.take(&2, U32, FF.BW(t, wi), Nat.sub(T, Nat.add(S, L))), c1, c2)) :
491    {_ == RHS : Nat}
492  %Equal.sym(Nat, Nat.add(S, L), S1, eS) :
493    {Nat.add(_, D.run_len2(List.take(&2, U32, FF.BW(t, wi), Nat.sub(T, _)), c1, c2)) == RHS : Nat}
494  {==}
495
496law fi2:
497  for +k: Nat
498  for +z: Bool
499  for +len: U32
500  for +t: P.Tree<U32>
501  for +d: Nat
502  for +to: U32
503  for +c1: U32
504  for +c2: U32
505  for +wi: U32
506  for +o: Nat
507  for +v1: U32
508  for +v2: U32
509  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
510  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
511  for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
512  for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
513  for +ho: {Nat.is_lt(o, 4n) == True{} : Bool}
514  for +hs: {Nat.is_le(FF.SS(wi, o), U32.to_nat(to)) == True{} : Bool}
515  for +he1: {Nat.is_le(U32.to_nat(to), Nat.mul(Nat.add(U32.to_nat(wi), 1n+k), 4n)) == True{} : Bool}
516  for +he2: {Nat.is_lt(Nat.mul(Nat.add(U32.to_nat(wi), k), 4n), U32.to_nat(to)) == True{} : Bool}
517  for +hv: {Nat.min(FW.P0(v1), FW.P0(v2)) == Nat.add(o, D.run_len2(FF.AW(t, wi, o), c1, c2)) : Nat}
518  for +hz: {U32.is_zero(U32.or(FA.zb(v1), FA.zb(v2))) == z : Bool}
519  {U32.to_nat(U32.min(FG2(1n+k, z, wi, U32.or(FA.zb(v1), FA.zb(v2)), FA.rep(c1), FA.rep(c2), t), to)) == D.first2(FF.UB(t), FF.SS(wi, o), U32.to_nat(to), c1, c2) : Nat}
520
521def fi2(k, z, len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, hc1, hc2, ho, hs, he1, he2, hv, hz):
522  match k z:
523    case 0n False{}:
524      fhit2(len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, ho, hs,
525        FF.wlt(U32.to_nat(wi), 0n, U32.to_nat(to), U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h)), hv, hz)
526    case 1n+q False{}:
527      fhit2(len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, ho, hs,
528        FF.wlt(U32.to_nat(wi), 1n+q, U32.to_nat(to), U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h)), hv, hz)
529    case 0n True{}:
530      fnone2(len, t, d, to, c1, c2, wi, o, v1, v2, h, ht, ho, hs,
531        FF.wlt(U32.to_nat(wi), 0n, U32.to_nat(to), U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h)), hv, hz, he1)
532    case 1n+q True{}:
533      +W = U32.to_nat(wi)
534      +T = U32.to_nat(to)
535      +j1 = (wi + 1 : U32)
536      +n1 = U32.xor(C.WD(t, j1), FA.rep(c1))
537      +n2 = U32.xor(C.WD(t, j1), FA.rep(c2))
538      +S1 = Nat.mul(Nat.add(W, 1n), 4n)
539      +hk = FF.wlt(W, 1n+q, T, U32.to_nat(len), Nat.pow(2n, d), he2, ht, C.ok_len(len, t, d, h))
540      +ej1 = C.inc_fits(wi, d, C.ok_d(len, t, d, h), N.lt_le_trans(W, Nat.pow(2n, d), Nat.mul(4n, Nat.pow(2n, d)), hk, FF.pow_le4(Nat.pow(2n, d))))
541      +hs1 = N.lt_to_le(S1, T, N.le_lt_trans(S1, Nat.mul(Nat.add(W, 1n+q), 4n), T,
542        N.le_mul_r(Nat.add(W, 1n), Nat.add(W, 1n+q), 4n, N.le_add_mono_l(W, 1n, 1n+q, N.le_zero_l(q))), he2))
543      +ea = Equal.trans(Nat, Nat.add(Nat.mul(U32.to_nat(j1), 4n), 0n), Nat.mul(U32.to_nat(j1), 4n), S1, N.add_zero(Nat.mul(U32.to_nat(j1), 4n)),
544        Equal.cong(Nat, Nat, y => Nat.mul(y, 4n), U32.to_nat(j1), Nat.add(W, 1n), ej1))
545      +hsi = AB.subst(Nat, y => {Nat.is_le(y, T) == True{} : Bool}, S1, FF.SS(j1, 0n), Equal.sym(Nat, FF.SS(j1, 0n), S1, ea), hs1)
546      +e1 = Equal.trans(Nat, Nat.add(U32.to_nat(j1), 1n+q), Nat.add(Nat.add(W, 1n), 1n+q), Nat.add(W, 1n+(1n+q)),
547        Equal.cong(Nat, Nat, y => Nat.add(y, 1n+q), U32.to_nat(j1), Nat.add(W, 1n), ej1), N.add_assoc(W, 1n, 1n+q))
548      +he1i = AB.subst(Nat, y => {Nat.is_le(T, Nat.mul(y, 4n)) == True{} : Bool}, Nat.add(W, 1n+(1n+q)), Nat.add(U32.to_nat(j1), 1n+q),
549        Equal.sym(Nat, Nat.add(U32.to_nat(j1), 1n+q), Nat.add(W, 1n+(1n+q)), e1), he1)
550      +e2 = Equal.trans(Nat, Nat.add(U32.to_nat(j1), q), Nat.add(Nat.add(W, 1n), q), Nat.add(W, 1n+q),
551        Equal.cong(Nat, Nat, y => Nat.add(y, q), U32.to_nat(j1), Nat.add(W, 1n), ej1), N.add_assoc(W, 1n, q))
552      +he2i = AB.subst(Nat, y => {Nat.is_lt(Nat.mul(y, 4n), T) == True{} : Bool}, Nat.add(W, 1n+q), Nat.add(U32.to_nat(j1), q),
553        Equal.sym(Nat, Nat.add(U32.to_nat(j1), q), Nat.add(W, 1n+q), e2), he2)
554      +ih = fi2(q, U32.is_zero(U32.or(FA.zb(n1), FA.zb(n2))), len, t, d, to, c1, c2, j1, 0n, n1, n2, h, ht, hc1, hc2, {==}, hsi, he1i, he2i, hv02(t, j1, c1, c2, hc1, hc2), {==})
555      +sk = fskip2(len, t, d, to, c1, c2, wi, o, v1, v2, q, h, ho, hs, hk, hv, hz, hs1)
556      Equal.trans(Nat, U32.to_nat(U32.min(FG2(1n+q, U32.is_zero(U32.or(FA.zb(n1), FA.zb(n2))), j1, U32.or(FA.zb(n1), FA.zb(n2)), FA.rep(c1), FA.rep(c2), t), to)), D.first2(FF.UB(t), FF.SS(j1, 0n), T, c1, c2), D.first2(FF.UB(t), FF.SS(wi, o), T, c1, c2),
557        ih, Equal.sym(Nat, D.first2(FF.UB(t), FF.SS(wi, o), T, c1, c2), D.first2(FF.UB(t), FF.SS(j1, 0n), T, c1, c2),
558          Equal.trans(Nat, D.first2(FF.UB(t), FF.SS(wi, o), T, c1, c2), D.first2(FF.UB(t), S1, T, c1, c2), D.first2(FF.UB(t), FF.SS(j1, 0n), T, c1, c2), sk,
559            Equal.cong(Nat, Nat, y => D.first2(FF.UB(t), y, T, c1, c2), S1, FF.SS(j1, 0n), Equal.sym(Nat, FF.SS(j1, 0n), S1, ea)))))
560
561law fview2_lt:
562  for +len: U32
563  for +t: P.Tree<U32>
564  for +d: Nat
565  for +from: U32
566  for +to: U32
567  for +c1: U32
568  for +c2: U32
569  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
570  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
571  for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
572  for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
573  for +hlt: {Nat.is_lt(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool}
574  {U32.to_nat(U32.min(FG2(U32.to_nat(((((to - 1 : U32) >> 2n : U32) - (from >> 2n : U32) : U32) + 1 : U32)), U32.is_zero(M02(t, from, FA.rep(c1), FA.rep(c2))), (from >> 2n : U32), M02(t, from, FA.rep(c1), FA.rep(c2)), FA.rep(c1), FA.rep(c2), t), to)) == D.first2(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c1, c2) : Nat}
575
576def fview2_lt(len, t, d, from, to, c1, c2, h, ht, hc1, hc2, hlt):
577  +F = U32.to_nat(from)
578  +T = U32.to_nat(to)
579  +wi0 = (from >> 2n : U32)
580  +W0 = U32.to_nat(wi0)
581  +o0 = U32.to_nat((from .&. 3 : U32))
582  +ee = ((to - 1 : U32) >> 2n : U32)
583  +E = U32.to_nat(ee)
584  +rc1 = FA.rep(c1)
585  +rc2 = FA.rep(c2)
586  +hd = C.ok_d(len, t, d, h)
587  +M4 = Nat.mul(4n, Nat.pow(2n, d))
588  +hTM = N.le_trans(T, U32.to_nat(len), M4, ht, C.ok_len(len, t, d, h))
589  +h0T = N.le_lt_trans(0n, F, T, N.le_zero_l(F), hlt)
590  +eW0 = U.to_nat_shrn(from, 2n)
591  +eo = U.to_nat_and_mask(from, 3, 2n, {==})
592  +et1 = U.to_nat_sub_le(to, 1, Equal.trans(Bool, U32.is_le(1, to), Nat.is_le(U32.to_nat(1), T), True{}, U.is_le_to_nat(1, to),
593    Equal.trans(Bool, Nat.is_le(1n, T), Nat.is_lt(0n, T), True{}, N.le_succ_lt(0n, T), h0T)))
594  +eE = Equal.trans(Nat, E, Nat.div(U32.to_nat((to - 1 : U32)), 4n), Nat.div(Nat.sub(T, 1n), 4n), U.to_nat_shrn((to - 1 : U32), 2n),
595    Equal.cong(Nat, Nat, y => Nat.div(y, 4n), U32.to_nat((to - 1 : U32)), Nat.sub(T, 1n), et1))
596  +hWE = AB.subst(Nat, y => {Nat.is_le(W0, y) == True{} : Bool}, Nat.div(Nat.sub(T, 1n), 4n), E, Equal.sym(Nat, E, Nat.div(Nat.sub(T, 1n), 4n), eE),
597    AB.subst(Nat, y => {Nat.is_le(y, Nat.div(Nat.sub(T, 1n), 4n)) == True{} : Bool}, Nat.div(F, 4n), W0, Equal.sym(Nat, W0, Nat.div(F, 4n), eW0),
598      FF.div_le4(F, Nat.sub(T, 1n), FF.lt_sub1(F, T, hlt))))
599  +k0 = Nat.sub(E, W0)
600  +esub = U.to_nat_sub_le(ee, wi0, Equal.trans(Bool, U32.is_le(wi0, ee), Nat.is_le(W0, E), True{}, U.is_le_to_nat(wi0, ee), hWE))
601  +hET = N.le_lt_trans(E, Nat.sub(T, 1n), T,
602    AB.subst(Nat, y => {Nat.is_le(y, Nat.sub(T, 1n)) == True{} : Bool}, Nat.div(Nat.sub(T, 1n), 4n), E, Equal.sym(Nat, E, Nat.div(Nat.sub(T, 1n), 4n), eE), FF.div_self_le(Nat.sub(T, 1n))),
603    FF.sub1_lt(T, h0T))
604  +ek = C.inc_fits((ee - wi0 : U32), d, hd,
605    AB.subst(Nat, y => {Nat.is_lt(y, M4) == True{} : Bool}, k0, U32.to_nat((ee - wi0 : U32)), Equal.sym(Nat, U32.to_nat((ee - wi0 : U32)), k0, esub),
606      N.le_lt_trans(k0, E, M4, H.sub_le(E, W0), N.lt_le_trans(E, T, M4, hET, hTM))))
607  +en = Equal.trans(Nat, U32.to_nat(((ee - wi0 : U32) + 1 : U32)), Nat.add(U32.to_nat((ee - wi0 : U32)), 1n), 1n+k0, ek,
608    Equal.trans(Nat, Nat.add(U32.to_nat((ee - wi0 : U32)), 1n), Nat.add(k0, 1n), 1n+k0, Equal.cong(Nat, Nat, y => Nat.add(y, 1n), U32.to_nat((ee - wi0 : U32)), k0, esub), N.add_one(k0)))
609  +eSF = Equal.trans(Nat, FF.SS(wi0, o0), Nat.add(Nat.mul(Nat.div(F, 4n), 4n), Nat.mod(F, 4n)), F,
610    Equal.trans(Nat, Nat.add(Nat.mul(W0, 4n), o0), Nat.add(Nat.mul(Nat.div(F, 4n), 4n), o0), Nat.add(Nat.mul(Nat.div(F, 4n), 4n), Nat.mod(F, 4n)),
611      Equal.cong(Nat, Nat, y => Nat.add(Nat.mul(y, 4n), o0), W0, Nat.div(F, 4n), eW0),
612      Equal.cong(Nat, Nat, y => Nat.add(Nat.mul(Nat.div(F, 4n), 4n), y), o0, Nat.mod(F, 4n), eo)),
613    N.div_mod(F, 4n))
614  +ho0 = AB.subst(Nat, y => {Nat.is_lt(y, 4n) == True{} : Bool}, Nat.mod(F, 4n), o0, Equal.sym(Nat, o0, Nat.mod(F, 4n), eo), N.mod_lt(F, 4n, {==}))
615  +hs0 = AB.subst(Nat, y => {Nat.is_le(y, T) == True{} : Bool}, F, FF.SS(wi0, o0), Equal.sym(Nat, FF.SS(wi0, o0), F, eSF), N.lt_to_le(F, T, hlt))
616  +eWk = N.le_sub_add(W0, E, hWE)
617  +eA = Equal.trans(Nat, Nat.add(W0, 1n+k0), 1n+Nat.add(W0, k0), Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), N.add_succ(W0, k0),
618    Equal.trans(Nat, 1n+Nat.add(W0, k0), 1n+E, Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), Equal.cong(Nat, Nat, y => 1n+y, Nat.add(W0, k0), E, eWk),
619      Equal.trans(Nat, 1n+E, Nat.add(E, 1n), Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), Equal.sym(Nat, Nat.add(E, 1n), 1n+E, N.add_one(E)),
620        Equal.cong(Nat, Nat, y => Nat.add(y, 1n), E, Nat.div(Nat.sub(T, 1n), 4n), eE))))
621  +he1 = AB.subst(Nat, y => {Nat.is_le(T, Nat.mul(y, 4n)) == True{} : Bool}, Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), Nat.add(W0, 1n+k0),
622    Equal.sym(Nat, Nat.add(W0, 1n+k0), Nat.add(Nat.div(Nat.sub(T, 1n), 4n), 1n), eA), FF.last_le(T, h0T))
623  +eB = Equal.trans(Nat, Nat.add(W0, k0), E, Nat.div(Nat.sub(T, 1n), 4n), eWk, eE)
624  +he2 = AB.subst(Nat, y => {Nat.is_lt(Nat.mul(y, 4n), T) == True{} : Bool}, Nat.div(Nat.sub(T, 1n), 4n), Nat.add(W0, k0),
625    Equal.sym(Nat, Nat.add(W0, k0), Nat.div(Nat.sub(T, 1n), 4n), eB), FF.last_lt(T, h0T))
626  +fiv = fi2(k0, U32.is_zero(M02(t, from, rc1, rc2)), len, t, d, to, c1, c2, wi0, o0, U32.or(U32.xor(C.WD(t, wi0), rc1), U32.not(FA.low(from))), U32.or(U32.xor(C.WD(t, wi0), rc2), U32.not(FA.low(from))),
627    h, ht, hc1, hc2, ho0, hs0, he1, he2, p0_low2(C.WD(t, wi0), c1, c2, from, hc1, hc2), {==})
628  +hh = AB.subst(Nat, y => {Nat.is_le(y, U32.to_nat(len)) == True{} : Bool}, T, Nat.add(F, Nat.sub(T, F)),
629    Equal.sym(Nat, Nat.add(F, Nat.sub(T, F)), T, N.le_sub_add(F, T, N.lt_to_le(F, T, hlt))), ht)
630  +E2 = Equal.trans(Nat, D.first2(FF.UB(t), FF.SS(wi0, o0), T, c1, c2), D.first2(FF.UB(t), F, T, c1, c2), D.first2(D.view(C.BT(len, t)), F, T, c1, c2),
631    Equal.cong(Nat, Nat, y => D.first2(FF.UB(t), y, T, c1, c2), FF.SS(wi0, o0), F, eSF),
632    Equal.sym(Nat, D.first2(D.view(C.BT(len, t)), F, T, c1, c2), D.first2(FF.UB(t), F, T, c1, c2),
633      Equal.cong(List<&2, U32>, Nat, y => Nat.add(F, D.run_len2(y, c1, c2)), D.slice(List.take(&2, U32, FF.UB(t), U32.to_nat(len)), F, Nat.sub(T, F)), D.slice(FF.UB(t), F, Nat.sub(T, F)),
634        FF.slice_take(FF.UB(t), U32.to_nat(len), F, Nat.sub(T, F), hh))))
635  %Equal.sym(Nat, U32.to_nat(((ee - wi0 : U32) + 1 : U32)), 1n+k0, en) :
636    {U32.to_nat(U32.min(FG2(_, U32.is_zero(M02(t, from, rc1, rc2)), wi0, M02(t, from, rc1, rc2), rc1, rc2, t), to)) == D.first2(D.view(C.BT(len, t)), F, T, c1, c2) : Nat}
637  Equal.trans(Nat, U32.to_nat(U32.min(FG2(1n+k0, U32.is_zero(M02(t, from, rc1, rc2)), wi0, M02(t, from, rc1, rc2), rc1, rc2, t), to)), D.first2(FF.UB(t), FF.SS(wi0, o0), T, c1, c2),
638    D.first2(D.view(C.BT(len, t)), F, T, c1, c2), fiv, E2)
639
640law fview2_go:
641  for +b: Bool
642  for +len: U32
643  for +t: P.Tree<U32>
644  for +d: Nat
645  for +from: U32
646  for +to: U32
647  for +c1: U32
648  for +c2: U32
649  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
650  for +hft: {U32.is_le(from, to) == True{} : Bool}
651  for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool}
652  for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
653  for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
654  for +hb: {U32.is_le(to, from) == b : Bool}
655  {U32.to_nat(U32.min(FG2(Bool.pick(Nat, b, 0n, U32.to_nat(((((to - 1 : U32) >> 2n : U32) - (from >> 2n : U32) : U32) + 1 : U32))), U32.is_zero(M02(t, from, FA.rep(c1), FA.rep(c2))), (from >> 2n : U32), M02(t, from, FA.rep(c1), FA.rep(c2)), FA.rep(c1), FA.rep(c2), t), to)) == D.first2(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c1, c2) : Nat}
656
657def fview2_go(b, len, t, d, from, to, c1, c2, h, hft, ht, hc1, hc2, hb):
658  match b:
659    case True{}:
660      +F = U32.to_nat(from)
661      +T = U32.to_nat(to)
662      +xs = D.view(C.BT(len, t))
663      +hd = C.ok_d(len, t, d, h)
664      +eTF = FF.le_antisym(T, F, Equal.trans(Bool, Nat.is_le(T, F), U32.is_le(to, from), True{}, Equal.sym(Bool, U32.is_le(to, from), Nat.is_le(T, F), U.is_le_to_nat(to, from)), hb),
665        Equal.trans(Bool, Nat.is_le(F, T), U32.is_le(from, to), True{}, Equal.sym(Bool, U32.is_le(from, to), Nat.is_le(F, T), U.is_le_to_nat(from, to)), hft))
666      %Equal.sym(U32, U32.min(4294967295, to), to, FF.min_top(to, d, hd, N.le_trans(T, U32.to_nat(len), Nat.mul(4n, Nat.pow(2n, d)), ht, C.ok_len(len, t, d, h)))) :
667        {U32.to_nat(_) == D.first2(xs, F, T, c1, c2) : Nat}
668      %Equal.sym(Nat, T, F, eTF) : {_ == D.first2(xs, F, _, c1, c2) : Nat}
669      %Equal.sym(Nat, Nat.sub(F, F), 0n, H.sub_self(F)) : {F == Nat.add(F, D.run_len2(D.slice(xs, F, _), c1, c2)) : Nat}
670      %Equal.sym(List<&2, U32>, D.slice(xs, F, 0n), Nil{}, X.slice_zero(xs, F)) : {F == Nat.add(F, D.run_len2(_, c1, c2)) : Nat}
671      Equal.sym(Nat, Nat.add(F, 0n), F, N.add_zero(F))
672    case False{}:
673      fview2_lt(len, t, d, from, to, c1, c2, h, ht, hc1, hc2,
674        N.not_le_lt(U32.to_nat(to), U32.to_nat(from), Equal.trans(Bool, Nat.is_le(U32.to_nat(to), U32.to_nat(from)), U32.is_le(to, from), False{},
675          Equal.sym(Bool, U32.is_le(to, from), Nat.is_le(U32.to_nat(to), U32.to_nat(from)), U.is_le_to_nat(to, from)), hb)))
676
677law fast_find2_t:
678  for +len: U32
679  for +t: P.Tree<U32>
680  for +d: Nat
681  for +from: U32
682  for +to: U32
683  for +c1: U32
684  for +c2: U32
685  for +h: {D.ok(C.BT(len, t), d) == True{} : Bool}
686  for +hft: {U32.is_le(from, to) == True{} : Bool}
687  for +ht: {Nat.is_le(U32.to_nat(to), D.size(C.BT(len, t))) == True{} : Bool}
688  for +hc1: {U32.is_lt(c1, 256) == True{} : Bool}
689  for +hc2: {U32.is_lt(c2, 256) == True{} : Bool}
690  {FA.find2(C.BT(len, t), from, to, c1, c2) == B.find2(C.BT(len, t), from, to, c1, c2) : D.Bytes & U32}
691
692def fast_find2_t(len, t, d, from, to, c1, c2, h, hft, ht, hc1, hc2):
693  +rc1 = FA.rep(c1)
694  +rc2 = FA.rep(c2)
695  +MN = U32.min(FG2(FA.words(from, to), U32.is_zero(M02(t, from, rc1, rc2)), (from >> 2n : U32), M02(t, from, rc1, rc2), rc1, rc2, t), to)
696  +SN = Pair.snd(D.Bytes, U32, B.find2(C.BT(len, t), from, to, c1, c2))
697  %Equal.sym(D.Bytes & U32, FA.find2(C.BT(len, t), from, to, c1, c2), (C.BT(len, t), MN), fast2_eq(len, t, from, to, c1, c2)) :
698    {_ == B.find2(C.BT(len, t), from, to, c1, c2) : D.Bytes & U32}
699  %Equal.sym(D.Bytes & U32, B.find2(C.BT(len, t), from, to, c1, c2), (C.BT(len, t), SN), F.find2_pair_t(len, t, from, to, c1, c2)) :
700    {(C.BT(len, t), MN) == _ : D.Bytes & U32}
701  Equal.cong(U32, D.Bytes & U32, y => (C.BT(len, t), y), MN, SN,
702    U.to_nat_inj(MN, SN, Equal.trans(Nat, U32.to_nat(MN), D.first2(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c1, c2), U32.to_nat(SN),
703      fview2_go(U32.is_le(to, from), len, t, d, from, to, c1, c2, h, hft, ht, hc1, hc2, {==}),
704      Equal.sym(Nat, U32.to_nat(SN), D.first2(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c1, c2), F.find2_view_t(len, t, d, from, to, c1, c2, h, hft, ht, hc1, hc2)))))