ProofNum.nvt2: law of lawful-fields@0.1.1.0 Import: import lawful-fields@0.1.1.0/proof_num.bend as ProofNum Lines 589-605 of lawful-fields@0.1.1.0/proof_num.bend: https://jend.leeeet.dev/read.txt?path=lawful-fields@0.1.1.0/proof_num.bend&start_line=589&end_line=605 import Base import lawful-bytes@0.1.1.0/defs.bend as D import lawful-fields@0.1.1.0/defs.bend as F import lawful-fields@0.1.1.0/fields.bend as C import lawful-bytes@0.1.1.0/proof_core.bend as K import lawful-arrays@0.1.0.0/proof_tree.bend as P law nvt2: for +n: Nat for +len: U32 for +t: P.Tree for +d: Nat for +from: U32 for +to: U32 for +M: Nat for +q: Nat for +hm: {Nat.pow(2n, 32n) == M : Nat} for +hcq: {U32.to_nat(429496729) == q : Nat} for +hq: {Nat.add(Nat.mul(q, 10n), 6n) == M : Nat} for +h: {D.ok(K.BT(len, t), d) == True{} : Bool} for +hft: {U32.is_le(from, to) == True{} : Bool} for +ht: {Nat.is_le(U32.to_nat(to), D.size(K.BT(len, t))) == True{} : Bool} for +hn: {Nat.sub(U32.to_nat(to), U32.to_nat(from)) == n : Nat} {F.nat_of(Pair.snd(D.Bytes, Maybe<&2, U32>, C.num(K.BT(len, t), from, to))) == F.decb(D.slice(D.view(K.BT(len, t)), U32.to_nat(from), Nat.sub(U32.to_nat(to), U32.to_nat(from))), M) : Maybe<&2, Nat>} Uses (53): 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.get https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe 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.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.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=Pair https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 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.to_nat 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/bytes.bend&name=at https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=Bytes 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=size 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/proof_append.bend&name=slice_zero https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=AT 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=at_pair_t https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=at_view_t 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_full 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-fields@0.1.1.0/defs.bend&name=dec.go https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=decb https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=decb.of https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=nat_of https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=num https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=num.fin https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/fields.bend&name=num.go https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_num.bend&name=decs https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_num.bend&name=nv https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_num.bend&name=posM https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_num.bend&name=sub0_nlt https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_num.bend&name=subs_lt 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=lt_le_trans 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=is_lt_to_nat