[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Theorem uint2bits-one
⊦ uint2bits(1) = false + true
Type: An axiom
Validity: The proof is valid.
Features: simp, localsimp,
Comment:
Used by:
bits2bits-mone
,
int2bits-011x
,
int2bits-add-high
,
int2bits-add-low
,
int2bits-falsein-02
,
int2bits-fill-rest
,
int2bits-lelen-04
,
int2bits-len-2-32-1
,
int2bits-len-eq
,
int2bits-len-neg-01
,
int2bits-len-one
,
int2bits-len-pos-pred
,
int2bits-lslen-04
,
int2bits-lslen-05
,
int2bits-lslen-07
,
int2bits-lslen-08
,
int2bits-mod2
,
int2bits-mod2-len
,
int2bits-mod2-neg
,
int2bits-mone
,
int2bits-mone-01
,
int2bits-mone-02
,
int2bits-neg-03
,
int2bits-ones
,
int2bits-rec-2pot-neg-02
,
int2bits-rec-neg-01
,
int2bits-rec-neg-03
,
int2bits-rest
,
int2bits-restsgn
,
int2bits-true
,
int2int-lastn-negneg
,
int2int-neg
,
int2int-rest-01
,
ubits2ubits-def
,
uint2bits-2pot
,
uint2bits-2pot-01
,
uint2bits-2pot-02
,
uint2bits-2pot-neg-mone
,
uint2bits-2potrec
,
uint2bits-add-high
,
uint2bits-add-high-01
,
uint2bits-add-low
,
uint2bits-add-low-01
,
uint2bits-div2pot
,
uint2bits-empty
,
uint2bits-eq
,
uint2bits-expos1
,
uint2bits-falsein
,
uint2bits-falsein-01
,
uint2bits-first
,
uint2bits-inj
,
uint2bits-len
,
uint2bits-len-01
,
uint2bits-len-mon
,
uint2bits-mod2pot
,
uint2bits-not-one
,
uint2bits-pred
,
uint2bits-restsgn
,
uint2bits-second
,
uint2bits-sgn-02
,
uint2bits-succ
,
uint2bits-zero-01
,
uint2uint-inv
,
uint2uint-pos
,
Used by units in proved state:
intops
,
bytes
,
byte
,
Proof exists?: No