def AP.u32_sub_add

bend-osdev-array@0.1.0.1 · PROOF.bend:1033

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF

import Base

1033def AP.u32_sub_add(a: U32, b: U32, h: {Nat.is_le(U32.to_nat(b), U32.to_nat(a)) == True{} : Bool}) -> {U32.to_nat(a) == Nat.add(U32.to_nat(U32.sub(a, b)), U32.to_nat(b)) : Nat}:
1034  match a b:
1035    case U32{x} U32{y}:
1036      AP.adc(32n, x, y, True{}, h)

Uses (8)

Used by (1)

bend-osdev-array@0.1.0.1/PROOF:AP.split