def add_one

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/word.bend:237

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as WA
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as MA

237# adding one is incrementing
238def add_one(+p: Nat, +x: Word(1n+p)) -> {Word.add(1n+p, x, one_word(p)) == Word.inc(1n+p, x) : Word(1n+p)}:
239  +ux = uw(1n+p, x)
240  +u1 = Equal.cong(Nat, Nat, z => Nat.add(1n, Nat.double(z)), uw(p, Word.zero(p)), 0n, A.uw_zero(p))
241  Equal.trans(Word(1n+p), Word.add(1n+p, x, one_word(p)), S.from_nat(1n+p, Nat.add(ux, uw(1n+p, one_word(p)))), Word.inc(1n+p, x),
242    WA.refines(1n+p, x, one_word(p)),
243    Equal.trans(Word(1n+p), S.from_nat(1n+p, Nat.add(ux, uw(1n+p, one_word(p)))), S.from_nat(1n+p, 1n+ux), Word.inc(1n+p, x),
244      Equal.cong(Nat, Word(1n+p), z => S.from_nat(1n+p, z), Nat.add(ux, uw(1n+p, one_word(p))), 1n+ux,
245        Equal.trans(Nat, Nat.add(ux, uw(1n+p, one_word(p))), Nat.add(ux, 1n), 1n+ux, Equal.cong(Nat, Nat, z => Nat.add(ux, z), uw(1n+p, one_word(p)), 1n, u1), N.add_comm(ux, 1n))),
246      Equal.sym(Word(1n+p), Word.inc(1n+p, x), S.from_nat(1n+p, 1n+ux), MA.increment_refines(1n+p, x))))