[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-01
⊦ j0 < 2 ^ i ∧ 0 ≤ i ∧ 0 ≤ j0 ∧ j < 0 → bor(j * 2 ^ i, j0) = j * 2 ^ i + j0
Type: A user defined theorem
Validity: The proof is valid.
Features:
Comment:
Used by:
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: 29
Proof steps: 57
Used lemmas:
add-ones-grlen-01
,
and-notempty
,
add-ones-lelen-01
,
and-size-one-01
,
and-size-one
,
and-com
,
and-rec-01
,
or-invandinv
,
bor-def
,
Used spec theorems:
int2bits
/
int2bits-neg
int2bits
/
uint2bits-2pot-06
bitopsaux
/
succ-zeros-01
int2bits
/
uint2int-invsucc
bitopsaux
/
sgn-append-06
list-last
/bitlista/
mk-first-01
int2bits
/
int2bits-neg-01
int2bits
/
int2unit-inv-rest
list-data
/bitlista/
length-rest
int2bits
/
int2bits-pos
int2bits
/
bits2int-split-01
bitopsaux
/
fill-fill
int2bits
/
bits2uint-split
int2bits
/
bits2uint-ones
intnat
/
num-i2n-eq
int-pot
/
pot-dist-pos
Used simplifier rules:
int-abs
/
forward-lsle
int-mult
/
zero-ls
int-pot
/
abs-2pot
int-abs
/
abs-08
int-mult
/
abs-eqall
int-abs
/
lels-01
int-abs
/
lels-04
bitopsaux
/
succ-zero-01
bitopsaux
/
succ-mklist-01
bitopsaux
/
inv-false
int-abs
/
forward-lele
int-abs
/
numls-03
int-abs
/
bet-01
int-abs
/
lsone
bitopsaux
/
succ-empty-01
bitopsaux
/
sgn-empty-01
int2bits
/
bits2int-sgn
bitopsaux
/
succ-truein-01
bitopsaux
/
inv-mklist
int-abs
/
lels-03
int-abs
/
neg
list
/bitlista/
app-02-ant
bitopsaux
/
inv-rest
nat
/
ls-01
nat-basic2
/
s
list-data
/bitlista/
size-01
intnat
/
num-i2n-le
int-basic1
/
ls-01
int-abs
/
lels
int-abs
/
anti
int-basic1
/
lf-03
int-basic1
/
lf-02
int2bits
/
int2bits-zero
list
/bitlista/
len-02
nat-basic2
/
one-03
int-abs
/
numlsf-01
int-mult
/
eq-dist
nat-basic2
/
z
nat
/
add-01
nat
/
succ-01
nat
/
ls-02
nat-basic1
/
one-01
nat
/
pred-03
int-abs
/
numsub
bitopsaux
/
inv-append
int2bits
/
int2int-inj
list
/bitlista/
app
bitopsaux
/
invert-base
int2bits
/
int2bits-first-01
int-abs
/
sub-eq
bitopsaux
/
inv-inv
int-abs
/
neg-02
int-mult
/
minus-left
int-abs
/
subsub
int2bits
/
int2uint-inv-01
nat
/
eq
bitopsaux
/
inv-empty
list
/bitlista/
a
list
/bitlista/
len
int2bits
/
int2bits-inv-first
int2bits
/
int2bits-not-empty
list-data
/bitlista/
l
bitopsaux
/
inv-len
int2bits
/
int2uint-pos
nat
/
zero
int-basic2
/
add-zero
list-last
/bitlista/
mk-zero
int2bits
/
bits2uint-base
int-mult
/
one
bitlista
/
inmklist-01
nat
/
zero-02
list-last
/bitlista/
mk-empty
int-abs
/
Sub-def
list-last
/bitlista/
mk-len
nat
/
lels-01
int2bits
/
int2bits-len-pos-01
nat-basic1
/
lf-02
intnat
/
i2i-pos
nat-basic2
/
eq
nat-basic2
/
l-02
nat
/
elim-sub
nat-basic2
/
l-01
nat-basic1
/
lf-01
nat
/
lels-02
int-pot
/
grz
int-basic2
/
lst-03
int-basic2
/
succ-01
intnat
/
abs-zero
int-abs
/
forward-lels
int-basic1
/
trans
int-basic1
/
lf-01
nat-basic1
/
f
int-abs
/
lels-02
nat-basic2
/
c
nat-basic2
/
a
intnat
/
n2i-add
int-mult
/
dist-rmerge
int-mult
/
succ-rmerge
int-mult
/
associativity
int-mult
/
commutativity
int-mult
/
eq-pos
int-basic2
/
add-a
int-basic2
/
add-c
intnat
/
nat2int