ProofFastFind2.fview2_lt: law of lawful-bytes@0.1.1.0 Import: import lawful-bytes@0.1.1.0/proof_fast_find2.bend as ProofFastFind2 Lines 561-574 of lawful-bytes@0.1.1.0/proof_fast_find2.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_find2.bend&start_line=561&end_line=574 import Base import lawful-bytes@0.1.1.0/defs.bend as D import lawful-bytes@0.1.1.0/fast.bend as FA import lawful-bytes@0.1.1.0/proof_core.bend as C import lawful-arrays@0.1.0.0/proof_tree.bend as P law fview2_lt: for +len: U32 for +t: P.Tree for +d: Nat for +from: U32 for +to: U32 for +c1: U32 for +c2: U32 for +h: {D.ok(C.BT(len, t), d) == True{} : Bool} for +ht: {Nat.is_le(U32.to_nat(to), U32.to_nat(len)) == True{} : Bool} for +hc1: {U32.is_lt(c1, 256) == True{} : Bool} for +hc2: {U32.is_lt(c2, 256) == True{} : Bool} for +hlt: {Nat.is_lt(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool} {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} Uses (71): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.min https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.or https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shrn https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=subst https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=Tree https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=first2 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=ok https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=run_len2 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=slice https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=view https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/fast.bend&name=low https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/fast.bend&name=rep https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=BT https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=WD https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=inc_fits https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=ok_d https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=ok_len https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find2.bend&name=FG2 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find2.bend&name=M02 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find2.bend&name=fi2 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find2.bend&name=p0_low2 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&name=SS https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&name=UB https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&name=div_le4 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&name=div_self_le https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&name=last_le https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&name=last_lt https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&name=lt_sub1 https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&name=slice_take https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&name=sub1_lt https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_shift.bend&name=sub_le https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=add_one https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=add_succ https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=div_mod https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_lt_trans https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_sub_add https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_succ_lt https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_trans https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=le_zero_l https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_le_trans https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=lt_to_le https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=mod_lt https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=is_le_to_nat https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=to_nat_and_mask https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=to_nat_shrn https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_u32.bend&name=to_nat_sub_le