[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 byte-law-righthift-not
⊦ (i = 128 ∧ j = 1 → i2b(i i>> j) ≠ i2b(b2i(i2b(i)) i>> j)) ∧ (i = 128 ∧ j = 1 → i2b(i i>>> j) ≠ i2b(b2i(i2b(i)) i>>> j))
Type: A user defined theorem
Validity: The proof is valid.
Features:
Comment:
Used by:
Used by units in proved state:
Proof exists?: Yes
View
the proof
Infos about the proof
Proved?: Yes
Interactions: 42
Proof steps: 101
Used lemmas:
num-i2b-pos
,
notequal
,
bib-pos-high
,
Used spec theorems:
intops
/
intshiftrzero-def
bitopsaux
/
fill-length
list-del
/bitlista/
sublist-def
bitopsaux
/
fill-fill
list-del
/bitlista/
firstn-app-02
int2bits
/
bits2uint-mklist
int2bits
/
bits2uint-split
list-del
/bitlista/
firstN-rec-01
int2bits
/
bits2int-neg-03
int2bits
/
int2bits-neg-num
int2bits
/
int2bits-pos
Used simplifier rules:
int2bits
/
bits2uint-one-02
list-last
/bitlista/
last-def
list-last
/bitlista/
l-05
list-del
/bitlista/
lastn-one
list-del
/bitlista/
num-lastN
list-del
/bitlista/
firstn-one
int2bits
/
bits2uint-zeros-03
int2bits
/
int2bits-leneq-pos
int2bits
/
bits2uint-one
intnat
/
n2i-add
list-del
/bitlista/
first-length
nat
/
fle
nat
/
le-num-05
nat
/
le-num-04
nat-basic2
/
eqs
nat
/
not-zero
nat
/
let
list-last
/bitlista/
mk-len
nat-basic1
/
lf-02
nat-basic2
/
l-02
bitlista
/
mklist-num-01
list-last
/bitlista/
mk-plus
int2bits
/
int2bits-first-01
int2bits
/
int2bits-first-02
nat
/
le-ls-simp
list-del
/bitlista/
restN-zero
list-last
/bitlista/
mk-zero
bitlista
/
mklist-num
list
/bitlista/
e
list
/bitlista/
app-02-ant
list
/bitlista/
c-08
bitopsaux
/
succ-one
int2bits
/
bits2uint-zero
list
/bitlista/
app
list-del
/bitlista/
sub-zerozero
list-del
/bitlista/
sublist-num-01
nat
/
add-num-04
nat-basic2
/
one
nat
/
lels
nat-basic2
/
s
nat-basic2
/
oz
int2bits
/
int2bits-len-one
nat-basic1
/
one
int2bits
/
bits2uint-one-03
int2bits
/
bits2int-pos
intops
/
bitsand-zerol
intops
/
and-rec-07
list
/bitlista/
len-02
list
/bitlista/
len
bitopsaux
/
sgn-base-01
bitopsaux
/
sgn-rec
bitopsaux
/
succ-zero
bitopsaux
/
succ-rec
list
/bitlista/
a
list
/bitlista/
c
bitopsaux
/
inv-false
bitopsaux
/
invert-one
bitopsaux
/
invert-zero
list
/bitlista/
Last
list
/bitlista/
Two
int2bits
/
uint2bits-one
int2bits
/
uint2bits-pos-num
nat-basic2
/
c
nat-basic2
/
a
nat-basic2
/
l-01
nat-basic1
/
lf-01
nat
/
lels-03
nat-basic1
/
ls-02
nat
/
elim-sub
int2bits
/
int2bits-not-empty
list-data
/bitlista/
l
nat
/
fle-01
nat-basic1
/
f
nat
/
lels-01
intops
/
band-commutativity
intops
/
band-associativity
intops
/
band-num
intops
/
intshiftrsign-num