ProofFastFind.fview_lt: law of lawful-bytes@0.1.1.0 Import: import lawful-bytes@0.1.1.0/proof_fast_find.bend as ProofFastFind Lines 926-938 of lawful-bytes@0.1.1.0/proof_fast_find.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&start_line=926&end_line=938 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 # from < to: the loop runs 1 + k0 words, from word from >> 2 to word (to - 1) >> 2. law fview_lt: for +len: U32 for +t: P.Tree for +d: Nat for +from: U32 for +to: U32 for +c: 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 +hc: {U32.is_lt(c, 256) == True{} : Bool} for +hlt: {Nat.is_lt(U32.to_nat(from), U32.to_nat(to)) == True{} : Bool} {U32.to_nat(U32.min(FG(U32.to_nat(((((to - 1 : U32) >> 2n : U32) - (from >> 2n : U32) : U32) + 1 : U32)), U32.is_zero(M0(t, from, FA.rep(c))), (from >> 2n : U32), M0(t, from, FA.rep(c)), FA.rep(c), t), to)) == D.first(D.view(C.BT(len, t)), U32.to_nat(from), U32.to_nat(to), c) : 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=first 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_len 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_find.bend&name=FG https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_fast_find.bend&name=M0 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=fi 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_fast_word.bend&name=p0_low 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