begin
theorem Th1:
theorem Th2:
theorem
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem
theorem
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
begin
definition
let n,
k be
Nat;
func n -BinarySequence k -> Tuple of
n,
BOOLEAN means :
Def1:
for
i being
Nat st
i in Seg n holds
it /. i = IFEQ ((k div (2 to_power (i -' 1))) mod 2),
0 ,
FALSE ,
TRUE ;
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;
:: deftheorem Def1 defines -BinarySequence BINARI_3:def 1 :
theorem Th26:
theorem Th27:
theorem Th28:
Lm1:
for n being non empty Nat holds (n + 1) -BinarySequence (2 to_power n) = (0* n) ^ <*TRUE *>
Lm2:
for n being non empty 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 empty 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 empty 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 )
theorem Th29:
theorem
theorem
theorem
theorem Th33:
theorem Th34:
theorem
theorem Th36:
theorem