def from_nat_step

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32.bend:80

import Base

80# the U32 step over abstract words a (for p) and b (for p + 1)
81def from_nat_step(+p: Nat, +a: Word(32n), +b: Word(32n), +rec: {U32.from_nat(p) == U32{a} : U32}, +hinc: {Word.inc(32n, a) == b : Word(32n)}) -> {U32.from_nat(1n+p) == U32{b} : U32}:
82  %Equal.sym(U32, U32.from_nat(p), U32{a}, rec) : {U32.inc(_) == U32{b} : U32}
83  Equal.cong(Word(32n), U32, w => U32{w}, Word.inc(32n, a), b, hinc)