[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 intshiftrsign-rec-pos
⊦ 0 ≤ i ∧ 0 < j ∧ j < 32 → i i>> j = i / 2 i>> (j - 1)
Type: A user defined theorem
Validity: The proof is valid.
Features:
Comment:
Used by:
intshiftrsign-2pot-pos
,
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 25
Proof steps: 52
Used lemmas:
band-commutativity
,
band-associativity
,
band-011x-pos-01
,
band-011x-pos-02
,
intshiftrsign
,
Used spec theorems:
int2bits
/
int2bits-rec-pos
int-div
/
mod-zero-05
list
/bitlista/
a
list-del
/bitlista/
sublist-append
list-del
/bitlista/
sublist-num-01
list-del
/bitlista/
sublist-lenrec-01
int2bits
/
bits2int-pos-02
list-del
/bitlista/
sublist-rec
list-del
/bitlista/
get-zero
int2bits
/
int2bits-pos
int2bits
/
uint2bits-rec-01
list
/bitlista/
first-01
list-last
/bitlista/
mk-rec
Used simplifier rules:
list
/bitlista/
c
list
/bitlista/
e-01
list
/bitlista/
rest-01
list
/bitlista/
c-08
int-div
/
div2-nle-01
int-div
/
div-div-pos
nat-basic2
/
one-03
int-div
/
pos
int2bits
/
uint2bits-empty
int-div
/
div-two-zero-01
int-abs
/
zero-gels-02
int2bits
/
bits2int-one
int2bits
/
bits2uint-one-03
list
/bitlista/
first
list
/bitlista/
Nil
intnat
/
abs-zero
list-last
/bitlista/
mk-empty
list
/bitlista/
e
list-del
/bitlista/
sublist-empty
list
/bitlista/
app-02-ant
nat
/
lep-02
nat-basic1
/
f
nat
/
eqle-one
list-del
/bitlista/
get-butlast
nat
/
lels
nat
/
lep-01
nat-basic2
/
oz
list-del
/bitlista/
get-succ
nat
/
elim-pred-c
nat
/
pred-03
list-data
/bitlista/
l
int2bits
/
int2bits-not-empty
nat
/
lep
nat-basic2
/
z
nat
/
lels-01
list-last
/bitlista/
mk-len
nat-basic2
/
s
nat-basic2
/
l-02
int-abs
/
bet-01
int-abs
/
lels-02
list-del
/bitlista/
sublist-num-01
list-del
/bitlista/
sub-zerozero
int2bits
/
bits2int-pos
int2bits
/
bits2uint-one-02
int2bits
/
int2bits-zero
int2bits
/
bits2int-zero
int-basic1
/
numlslsdel
nat-basic2
/
c
nat-basic2
/
a
list-last
/bitlista/
mk-last
list
/bitlista/
app
list-last
/bitlista/
mk-zero
bitlista
/
mklist-num
list-last
/bitlista/
mk-plus
intnat
/
rax-04
int-abs
/
abs-04
int-abs
/
absle
int-abs
/
numlelsdel
list
/bitlista/
in-06
list
/bitlista/
len-02
list
/bitlista/
len
int-abs
/
numle-02
int-abs
/
numleledel-01
int2bits
/
int2bits-pos-num
int2bits
/
uint2bits-pos-num
int2bits
/
uint2bits-one
list
/bitlista/
Two
list
/bitlista/
Last
list
/bitlista/
c-07
list
/bitlista/
a
list
/bitlista/
in-append
list
/bitlista/
in-17
int-abs
/
zero-gels-04
int-abs
/
lels
int-abs
/
numlsledel-01
int-abs
/
lels-01
int-abs
/
numle-03
int-div
/
div-ls-zero
int2bits
/
int2bits-first-02
int-abs
/
forward-lels
int-abs
/
mone-06
int-abs
/
numls-02
int-basic2
/
add-c
int-basic2
/
add-a
int-abs
/
numls-03
int-abs
/
forward-le-01
int-abs
/
forward-le-05
int-basic1
/
forward-pos
int-abs
/
elim-sub