environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, NAT_1, FINSEQ_2, MARGREL1, BINARITH, ARYTM_3, POWER, SUBSET_1, ORDINAL4, FINSEQ_1, FUNCOP_1, XBOOLEAN, CARD_1, RELAT_1, REAL_1, FINSEQ_5, EUCLID, XXREAL_0, FUNCT_1, PARTFUN1, ARYTM_1, BINARI_2, ZFMISC_1, INT_1, ABIAN, BINARI_3, XCMPLX_0;
notations HIDDEN, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, NAT_D, POWER, ABIAN, SERIES_1, MARGREL1, FUNCT_1, PARTFUN1, FUNCOP_1, FINSEQ_1, FINSEQ_5, ZFMISC_1, FINSEQ_2, BINARITH, BINARI_2, EUCLID;
definitions ;
theorems TARSKI, NAT_1, NAT_2, MARGREL1, POWER, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, BINARITH, BINARI_2, XREAL_1, XCMPLX_1, XBOOLEAN, NAT_D, PARTFUN1, XXREAL_0, CARD_1;
schemes NAT_1, NAT_2, FINSEQ_2;
registrations RELSET_1, XREAL_0, NAT_1, XBOOLEAN, MARGREL1, NAT_2, ORDINAL1, XBOOLE_0, FINSEQ_2, INT_1, FINSEQ_1;
constructors HIDDEN, NAT_D, FINSEQOP, SERIES_1, BINARITH, FINSEQ_5, BINARI_2, ABIAN, EUCLID, TREES_3;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FINSEQ_2, EUCLID, XBOOLEAN, ORDINAL1;
expansions ;
definition
let n,
k be
Nat;
existence
ex b1 being Tuple of n, BOOLEAN st
for i being Nat st i in Seg n holds
b1 /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE)
uniqueness
for b1, b2 being Tuple of n, BOOLEAN st ( for i being Nat st i in Seg n holds
b1 /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) ) & ( for i being Nat st i in Seg n holds
b2 /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) ) holds
b1 = b2
end;
Lm1:
for n being non zero Nat holds (n + 1) -BinarySequence (2 to_power n) = (0* n) ^ <*TRUE*>
Lm2:
for n being non zero Nat
for k being Nat st 2 to_power n <= k & k < 2 to_power (n + 1) holds
((n + 1) -BinarySequence k) . (n + 1) = TRUE
Lm3:
for n being non zero Nat
for k being Nat st 2 to_power n <= k & k < 2 to_power (n + 1) holds
(n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>
Lm4:
for n being non zero Nat
for k being Nat st k < 2 to_power n holds
for x being Tuple of n, BOOLEAN st x = 0* n holds
( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 )