[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 bor-2pot-plus
⊦ j0 < 2 ^ i ∧ 0 ≤ i ∧ 0 ≤ j0 ∧ 0 ≤ j → bor(j * 2 ^ i, j0) = j * 2 ^ i + j0
Type: A user defined theorem
Validity: The proof is valid.
Features:
Comment:
Used by:
bor-256-plus
,
bor-2pot-plus-02
,
bor-65536-plus
,
bor-shift-plus
,
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 23
Proof steps: 48
Used lemmas:
add-ones-grlen-01
,
and-notempty
,
add-ones-lelen-01
,
and-size-one-01
,
and-size-one
,
and-com
,
and-onel-01
,
or-invandinv
,
bor-def
,
Used spec theorems:
int2bits
/
int2bits-pos
int2bits
/
uint2bits-2pot-01
int2bits
/
bits2int-pos
int-pot
/
eq-two
int2bits
/
bits2int-split
bitopsaux
/
inv-fill
int2bits
/
int2uint-fill
bitopsaux
/
fill-length
Used simplifier rules:
int-abs
/
forward-lels
int-mult
/
zero-ge
int2bits
/
uint2bits-zero
int-mult
/
Mult-zero
int-abs
/
anti
int-abs
/
lels
bitopsaux
/
inv-mklist
list
/bitlista/
app-02-ant
int-basic2
/
add-zero
bitopsaux
/
inv-false
int2bits
/
int2bits-zero
int2bits
/
int2bits-eq
int-abs
/
lels-04
int2bits
/
int2bits-first-02
list-data
/bitlista/
lf-01
bitopsaux
/
inv-rest
nat-basic1
/
f
nat-basic1
/
lf-02
nat-basic1
/
lf-01
nat-basic1
/
ls-02
list-data
/bitlista/
size-01
intnat
/
num-i2n-le
int2bits
/
int2bits-first-04
int2bits
/
int2int-inj
int-abs
/
lels-02
intnat
/
nat2int
list
/bitlista/
len
list
/bitlista/
len-02
nat-basic2
/
eq-01
list
/bitlista/
in-append
list
/bitlista/
in-17
intnat
/
i2i-pos
bitopsaux
/
inv-append
list-data
/bitlista/
elim-list-c
list
/bitlista/
in-14
bitopsaux
/
inv-first-01
list
/bitlista/
c
int2bits
/
uint2int-01
bitopsaux
/
invert-base
list-last
/bitlista/
mk-empty
intnat
/
abs-zero
int-basic1
/
lf-03
list-last
/bitlista/
mk-zero
int-mult
/
one
int-basic2
/
eq
list
/bitlista/
app
list
/bitlista/
a
int-abs
/
bet-01
int2bits
/
uint2bits-first-02
int2bits
/
uint2bits-empty
int-basic1
/
ls-01
int-abs
/
lels-01
list-data
/bitlista/
l
int2bits
/
uint2uint-pos
bitlista
/
inmklist-01
int2bits
/
int2bits-inv-first
list-last
/bitlista/
mk-len
int2bits
/
int2bits-not-empty
bitopsaux
/
inv-empty
bitopsaux
/
inv-inv
int-basic2
/
add-c
int-basic2
/
add-a
int-mult
/
commutativity
int-mult
/
associativity
int-mult
/
eq-pos
int-basic2
/
add-in
intnat
/
i2i-pos-01
int-pot
/
eq-two
bitopsaux
/
inv-len
nat
/
lels-01
int2bits
/
int2bits-len-pos-01
nat-basic2
/
a
nat-basic2
/
c
nat
/
eq