1 import Base 2 import ./defs.bend as D 3 import ./bytes.bend as B 4 import ./fast.bend as FA 5 import ./proof_seq.bend as Q 6 import ./proof_core.bend as C 7 import ./proof_find.bend as F 8 import ./proof_append.bend as X 9 import ./proof_shift.bend as H 10 import ./proof_fast_word.bend as FW 11 import ./proof_fast_find.bend as FF 12 import lawful-words@0.1.0.0/defs.bend as W 13 import lawful-words@0.1.0.0/proof_nat.bend as N 14 import lawful-words@0.1.0.0/proof_u32.bend as U 15 import lawful-arrays@0.1.0.0/proof_base.bend as AB 16 import lawful-arrays@0.1.0.0/proof_tree.bend as P 17 import 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. 24 def 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 31 def FG2(n: Nat, z: Bool, +wi: U32, +m: U32, +r1: U32, +r2: U32, +t: P.Tree) -> 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 41 law 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 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} 50 51 def fg2_eq(n, z, wi, m, r1, r2, t): 52 match n z: 53 case 0n _: 54 %Equal.sym(Array & 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} 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, 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} 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} 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, 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} 67 {==} 68 69 def M02(+t: P.Tree, +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 72 law fast2_eq: 73 for +len: U32 74 for +t: P.Tree 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 81 def 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, 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, 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 96 law min_le_l: 97 for +a: Nat 98 for +b: Nat 99 {Nat.is_le(Nat.min(a, b), a) == True{} : Bool} 100 101 def 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 110 law 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 115 def 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 118 law 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 124 def 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. 133 law 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 143 def 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. 166 law 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 175 def 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. 189 law hv02: 190 for +t: P.Tree 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 198 def 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 211 law 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 222 def 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 245 law 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 257 def 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 279 law 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 291 def 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 312 law fhit2: 313 for +len: U32 314 for +t: P.Tree 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 332 def 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 377 law nohit2: 378 for +t: P.Tree 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 389 def 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 398 law fnone2: 399 for +len: U32 400 for +t: P.Tree 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 419 def 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 443 law fskip2: 444 for +len: U32 445 for +t: P.Tree 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 464 def 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 496 law fi2: 497 for +k: Nat 498 for +z: Bool 499 for +len: U32 500 for +t: P.Tree 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 521 def 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 561 law fview2_lt: 562 for +len: U32 563 for +t: P.Tree 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 576 def 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 640 law fview2_go: 641 for +b: Bool 642 for +len: U32 643 for +t: P.Tree 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 657 def 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 677 law fast_find2_t: 678 for +len: U32 679 for +t: P.Tree 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 692 def 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)))))