environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, NAT_1, INT_1, XXREAL_0, CARD_1, RELAT_1, ARYTM_3, POWER, EUCLID, FINSEQ_1, BINOP_2, ZFMISC_1, TARSKI, FUNCT_1, FINSEQ_2, MARGREL1, BINARITH, ARYTM_1, SUBSET_1, PARTFUN1, XBOOLEAN, BINARI_2, BINARI_3, FUNCOP_1, ORDINAL4, COMPLEX1, NEWTON, BINARI_4, XCMPLX_0;
notations HIDDEN, INT_1, SUBSET_1, XBOOLEAN, MARGREL1, FUNCOP_1, XCMPLX_0, POWER, BINARITH, BINARI_2, BINARI_3, SERIES_1, ORDINAL1, NUMBERS, XXREAL_0, XBOOLE_0, NAT_D, BINOP_2, EUCLID, TARSKI, PARTFUN1, FUNCT_1, RELAT_1, ZFMISC_1, INT_2, FINSEQOP, NEWTON, FINSEQ_1, FINSEQ_2;
definitions ;
theorems POWER, NAT_1, PRE_FF, ABSVALUE, BINARI_3, INT_1, BINARITH, NAT_2, BINARI_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCOP_1, RVSUM_1, FUNCT_2, ZFMISC_1, EULER_2, PEPIN, PREPOWER, XREAL_1, XXREAL_0, XBOOLEAN, NAT_D, VALUED_1, XREAL_0, CARD_1;
schemes NAT_1;
registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, XBOOLEAN, MARGREL1, VALUED_0, FINSEQ_1, FINSEQ_2, RELAT_1, FUNCT_1, CARD_1, XCMPLX_0, ORDINAL1;
constructors HIDDEN, REAL_1, NAT_D, FINSEQOP, NEWTON, SERIES_1, BINARITH, BINARI_2, EUCLID, BINARI_3, RVSUM_1, RELSET_1, BINOP_2, TREES_3;
requirements HIDDEN, REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
equalities FINSEQ_2, XBOOLEAN, EUCLID;
expansions ;
theorem Th1:
for
m being
Nat st
m > 0 holds
m * 2
>= m + 1
theorem Th4:
for
k,
m,
l being
Nat st
k <= l &
l <= m & not
k = l holds
(
k + 1
<= l &
l <= m )
theorem Th8:
for
k,
l,
m being
Nat st
l + m <= k - 1 holds
(
l < k &
m < k )
Lm1:
for n being non zero 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 zero 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 zero 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 zero 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,|.h.|))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,|.i.|))) + i) mod (2 to_power n)
Lm5:
for n being non zero 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 zero 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)