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 :
for n, k being Nat
for b3 being Tuple of n, BOOLEAN holds
( b3 = n -BinarySequence k iff for i being Nat st i in Seg n holds
b3 /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) );
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