~/bend-docscommunity

proofs/word_subtraction.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/word_subtraction.bend as Word_subtraction

4 imports
import Base
import ./natural_addition.bend as Addition
import ./word_arithmetic.bend as WordArithmetic
import ./word_encoding.bend as WordEncoding

Laws

law undo provedsource · line 6 · raw

@+n:Nat -> @+a:Word(n) -> @+b:Word(n) -> @+f:Bool -> @+c:Bool -> {Word.adc(n, Word.adc(n, a, b, f, c), b, Bool.not(f), Bool.not(c)) == a : Word(n)}

Definitions

def subtract_add source · line 78 · raw

@+a:U32 -> @+b:U32 -> {U32.sub(U32.add(a, b), b) == a : U32}

def add_subtract source · line 84 · raw

@+a:U32 -> @+b:U32 -> {U32.add(U32.sub(a, b), b) == a : U32}

def encoded_subtract_add source · line 90 · raw

@+a:Nat -> @+b:Nat -> {U32.sub(U32.from_nat(Nat.add(a, b)), U32.from_nat(b)) == U32.from_nat(a) : U32}

def restore source · line 94 · raw

@+a:Nat -> @+b:Nat -> @h:{Nat.is_le(b, a) == True{} : Bool} -> {Nat.add(Nat.sub(a, b), b) == a : Nat}

def encoded_subtract source · line 107 · raw

@+a:Nat -> @+b:Nat -> @h:{Nat.is_le(b, a) == True{} : Bool} -> {U32.sub(U32.from_nat(a), U32.from_nat(b)) == U32.from_nat(Nat.sub(a, b)) : U32}