def pow_le32

bend-collections-laws-math@1.0.0.0 · proofs/lib/words32.bend:93

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AT

93def pow_le32(+one: Nat, +h1: {one == 1n : Nat}, +d: Nat, +hd: {Nat.is_lt(d, 32n) == True{} : Bool}) -> {Nat.is_le(SC.pow2(d), WD.sc(32n, one)) == True{} : Bool}:
94  +j = Nat.sub(32n, d)
95  +e = Equal.trans(Nat, WD.sc(32n, one), WD.sc(Nat.add(d, j), one), WD.sc(d, WD.sc(j, one)), Equal.cong(Nat, Nat, z => WD.sc(z, one), 32n, Nat.add(d, j), Equal.sym(Nat, Nat.add(d, j), 32n, N.sub_add(32n, d, N.lt_le(d, 32n, hd)))), AT.sc_idx(d, j, one))
96  L.subst(Nat, z => {Nat.is_le(SC.pow2(d), z) == True{} : Bool}, WD.sc(d, WD.sc(j, one)), WD.sc(32n, one), Equal.sym(Nat, WD.sc(32n, one), WD.sc(d, WD.sc(j, one)), e), L.subst(Nat, z => {Nat.is_le(z, WD.sc(d, WD.sc(j, one))) == True{} : Bool}, WD.sc(d, one), SC.pow2(d), Equal.sym(Nat, SC.pow2(d), WD.sc(d, one), pow_one(one, h1, d)), AT.sc_le(d, one, WD.sc(j, one), AT.le_sc(j, one))))