begin
theorem Th1:
for
m being
Nat st
m > 0 holds
m * 2
>= m + 1
theorem Th2:
theorem
theorem Th4:
for
k,
m,
l being
Nat st
k <= l &
l <= m & not
k = l holds
(
k + 1
<= l &
l <= m )
theorem Th5:
theorem
theorem
theorem Th8:
for
l,
m,
k being
Nat st
l + m <= k - 1 holds
(
l < k &
m < k )
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem
theorem
theorem
theorem Th20:
begin
:: deftheorem Def1 defines MajP BINARI_4:def 1 :
for m, j, b3 being Nat holds
( b3 = MajP m,j iff ( 2 to_power b3 >= j & b3 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b3 ) ) );
theorem
theorem Th22:
theorem
theorem Th24:
theorem
begin
:: deftheorem Def2 defines 2sComplement BINARI_4:def 2 :
for m being Nat
for i being Integer holds
( ( i < 0 implies 2sComplement m,i = m -BinarySequence (abs ((2 to_power (MajP m,(abs i))) + i)) ) & ( not i < 0 implies 2sComplement m,i = m -BinarySequence (abs i) ) );
theorem
theorem
Lm1:
for n being non empty Nat
for k, l being Nat st k mod n = l mod n & k > l holds
ex s being Integer st k = l + (s * n)
Lm2:
for n being non empty Nat
for k, l being Nat st k mod n = l mod n holds
ex s being Integer st k = l + (s * n)
Lm3:
for n being non empty Nat
for k, l, m being Nat st m < n & k mod (2 to_power n) = l mod (2 to_power n) holds
(k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2
Lm4:
for n being non empty Nat
for h, i being Integer st h mod (2 to_power n) = i mod (2 to_power n) holds
((2 to_power (MajP n,(abs h))) + h) mod (2 to_power n) = ((2 to_power (MajP n,(abs i))) + i) mod (2 to_power n)
Lm5:
for n being non empty Nat
for h, i being Integer st h >= 0 & i >= 0 & h mod (2 to_power n) = i mod (2 to_power n) holds
2sComplement n,h = 2sComplement n,i
Lm6:
for n being non empty Nat
for h, i being Integer st h < 0 & i < 0 & h mod (2 to_power n) = i mod (2 to_power n) holds
2sComplement n,h = 2sComplement n,i
theorem
theorem
theorem Th30:
theorem
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem
theorem
theorem