proofs/u32_successor.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/u32_successor.bend as U32_successor

4 imports

import Base
import ./natural_addition.bend as Addition
import ./word_encoding.bend as WordEncoding
import ./word_width.bend as WordWidth

Laws

law pad_nat provedsource · line 6 · raw

@+n:Nat -> @+w:Word(n) -> {Word.to_nat(1n+n, Word.shr.pad(n, w)) == Word.to_nat(n, w) : Nat}

law inc_nat provedsource · line 24 · raw

@+n:Nat -> @+w:Word(n) -> {Word.to_nat(1n+n, Word.inc(1n+n, Word.shr.pad(n, w))) == 1n+Word.to_nat(n, w) : Nat}

law adc_zero provedsource · line 42 · raw

@+n:Nat -> @+w:Word(n) -> {Word.adc(n, w, Word.zero(n), False{}, False{}) == w : Word(n)}

law adc_one provedsource · line 60 · raw

@+n:Nat -> @+w:Word(n) -> {Word.adc(n, w, Word.zero(n), False{}, True{}) == Word.inc(n, w) : Word(n)}

law add_one provedsource · line 78 · raw

@+n:Nat -> @+w:Word(n) -> {Word.add(n, w, Word.inc(n, Word.zero(n))) == Word.inc(n, w) : Word(n)}

law concat_pad provedsource · line 95 · raw

@+width:Nat -> @+word:Word(width) -> {0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_width.transport(Nat.add(width, 1n), 1n+width, 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_encoding.concat(width, 1n, word, Word.zero(1n)), 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/natural_addition.successor_width(width)) == Word.shr.pad(width, word) : Word(1n+width)}

law successor provedsource · line 144 · raw

@+i:U32 -> Goal(i)

Definitions

def padded_successor source · line 121 · raw

@+low:Word(31n) -> {U32.to_nat(U32.add(U32{Word.shr.pad(31n, low)}, 1)) == 1n+U32.to_nat(U32{Word.shr.pad(31n, low)}) : Nat}

def Goal source · line 128 · raw

@+i:U32 -> Type

def parts source · line 131 · raw

@+parts:0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_encoding.Split<31n, 1n> -> Goal(U32{0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/word_encoding.join(31n, 1n, parts)})

def word source · line 140 · raw

@+w:Word(32n) -> Goal(U32{w})