~/jendhub

def encoded_subtract

stelliferous@0.0.2.0 · proofs/word_subtraction.bend:107

import stelliferous@0.0.2.0/proofs/word_subtraction.bend as WordSubtraction
import Base

107def encoded_subtract(+a: Nat,+b: Nat,h: {Nat.is_le(b,a) == True{} : Bool}) -> {U32.sub(U32.from_nat(a),
108    U32.from_nat(b)) == U32.from_nat(Nat.sub(a,b)) : U32}:
109  %restore(a,b,h) : {U32.sub(U32.from_nat(_),U32.from_nat(b)) == U32.from_nat(Nat.sub(a,b)) : U32}
110  encoded_subtract_add(Nat.sub(a,b),b)

Uses (9)

Used by (1)