:: BINARI_3 semantic presentation

begin

theorem Th1: :: BINARI_3:1
for n being non empty Nat
for F being Tuple of n, BOOLEAN holds Absval F < 2 to_power n
proof
defpred S1[ non empty Nat] means  for F being Tuple of $1, BOOLEAN holds Absval F < 2 to_power $1;
A1: for n being non empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non empty Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
 n < n + 1 by NAT_1:13;
then A3: 2 to_power n < 2 to_power (n + 1) by POWER:39;
let F be Tuple of n + 1, BOOLEAN ; ::_thesis: Absval F < 2 to_power (n + 1)
consider T being Element of n -tuples_on BOOLEAN, d being Element of BOOLEAN  such that
A4: F = T ^ <*d*> by FINSEQ_2:117;
A5: Absval F = (Absval T) + (IFEQ (d,FALSE,0,(2 to_power n))) by A4, BINARITH:20;
A6: Absval T < 2 to_power n by A2;
percases ( d = FALSE or d = TRUE ) by XBOOLEAN:def_3;
suppose d = FALSE ; ::_thesis: Absval F < 2 to_power (n + 1)
then  Absval F = (Absval T) + 0 by A5, FUNCOP_1:def_8;
then  (Absval F) + (2 to_power n) < (2 to_power n) + (2 to_power (n + 1)) by A2, A3, XREAL_1:8;
hence  Absval F < 2 to_power (n + 1) by XREAL_1:6; ::_thesis: verum
end;
suppose d = TRUE ; ::_thesis: Absval F < 2 to_power (n + 1)
then  Absval F = (Absval T) + (2 to_power n) by A5, FUNCOP_1:def_8;
then  Absval F < (2 to_power n) + (2 to_power n) by A6, XREAL_1:6;
then  Absval F < (2 to_power n) * 2 ;
then  Absval F < (2 to_power n) * (2 to_power 1) by POWER:25;
hence  Absval F < 2 to_power (n + 1) by POWER:27; ::_thesis: verum
end;
end;
end;
A7: S1[1]
proof
let F be Tuple of 1, BOOLEAN ; ::_thesis: Absval F < 2 to_power 1
consider d being Element of BOOLEAN  such that
A8: F = <*d*> by FINSEQ_2:97;
 ( d = TRUE or d = FALSE ) by XBOOLEAN:def_3;
then  ( Absval F = 1 or Absval F = 0 ) by A8, BINARITH:15, BINARITH:16;
then  Absval F < 2 ;
hence  Absval F < 2 to_power 1 by POWER:25; ::_thesis: verum
end;
thus  for n being non empty Nat holds S1[n] from NAT_1:sch_10(A7, A1); ::_thesis: verum
end;

theorem Th2: :: BINARI_3:2
for n being non empty Nat
for F1, F2 being Tuple of n, BOOLEAN st Absval F1 = Absval F2 holds
F1 = F2
proof
defpred S1[ non empty Nat] means  for F1, F2 being Tuple of $1, BOOLEAN st Absval F1 = Absval F2 holds
F1 = F2;
A1: for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: for F1, F2 being Tuple of k, BOOLEAN st Absval F1 = Absval F2 holds
F1 = F2 ; ::_thesis: S1[k + 1]
let F1, F2 be Tuple of k + 1, BOOLEAN ; ::_thesis: ( Absval F1 = Absval F2 implies F1 = F2 )
consider T1 being Element of k -tuples_on BOOLEAN, d1 being Element of BOOLEAN  such that
A3: F1 = T1 ^ <*d1*> by FINSEQ_2:117;
assume A4: Absval F1 = Absval F2 ; ::_thesis: F1 = F2
consider T2 being Element of k -tuples_on BOOLEAN, d2 being Element of BOOLEAN  such that
A5: F2 = T2 ^ <*d2*> by FINSEQ_2:117;
A6: (Absval T1) + (IFEQ (d1,FALSE,0,(2 to_power k))) = Absval F1 by A3, BINARITH:20
.= (Absval T2) + (IFEQ (d2,FALSE,0,(2 to_power k))) by A5, A4, BINARITH:20 ;
 d1 = d2
proof
assume A7: d1 <> d2 ; ::_thesis: contradiction
percases ( d1 = FALSE or d1 = TRUE ) by XBOOLEAN:def_3;
supposeA8: d1 = FALSE ; ::_thesis: contradiction
then A9: IFEQ (d1,FALSE,0,(2 to_power k)) = 0 by FUNCOP_1:def_8;
 IFEQ (d2,FALSE,0,(2 to_power k)) = 2 to_power k by A7, A8, FUNCOP_1:def_8;
hence  contradiction by A6, A9, Th1, NAT_1:11; ::_thesis: verum
end;
supposeA10: d1 = TRUE ; ::_thesis: contradiction
then  d2 = FALSE by A7, XBOOLEAN:def_3;
then A11: IFEQ (d2,FALSE,0,(2 to_power k)) = 0 by FUNCOP_1:def_8;
 IFEQ (d1,FALSE,0,(2 to_power k)) = 2 to_power k by A10, FUNCOP_1:def_8;
hence  contradiction by A6, A11, Th1, NAT_1:11; ::_thesis: verum
end;
end;
end;
hence  F1 = F2 by A2, A3, A5, A6, XCMPLX_1:2; ::_thesis: verum
end;
A12: S1[1]
proof
let F1, F2 be Tuple of 1, BOOLEAN ; ::_thesis: ( Absval F1 = Absval F2 implies F1 = F2 )
consider d1 being Element of BOOLEAN  such that
A13: F1 = <*d1*> by FINSEQ_2:97;
assume A14: Absval F1 = Absval F2 ; ::_thesis: F1 = F2
assume A15: F1 <> F2 ; ::_thesis: contradiction
consider d2 being Element of BOOLEAN  such that
A16: F2 = <*d2*> by FINSEQ_2:97;
percases ( d1 = FALSE or d1 = TRUE ) by XBOOLEAN:def_3;
supposeA17: d1 = FALSE ; ::_thesis: contradiction
then A18: Absval F1 = 0 by A13, BINARITH:15;
 d2 = TRUE by A13, A16, A15, A17, XBOOLEAN:def_3;
hence  contradiction by A16, A14, A18, BINARITH:16; ::_thesis: verum
end;
supposeA19: d1 = TRUE ; ::_thesis: contradiction
then A20: Absval F1 = 1 by A13, BINARITH:16;
 d2 = FALSE by A13, A16, A15, A19, XBOOLEAN:def_3;
hence  contradiction by A16, A14, A20, BINARITH:15; ::_thesis: verum
end;
end;
end;
thus  for n being non empty Nat holds S1[n] from NAT_1:sch_10(A12, A1); ::_thesis: verum
end;

theorem :: BINARI_3:3
for t1, t2 being FinSequence st Rev t1 = Rev t2 holds
t1 = t2
proof
let t1, t2 be FinSequence; ::_thesis: ( Rev t1 = Rev t2 implies t1 = t2 )
assume A1: Rev t1 = Rev t2 ; ::_thesis: t1 = t2
thus t1 = Rev (Rev t1)
.= t2 by A1 ; ::_thesis: verum
end;

theorem Th4: :: BINARI_3:4
for n being Nat holds 0* n in BOOLEAN *
proof
let n be Nat; ::_thesis: 0* n in BOOLEAN *
 n |-> FALSE is FinSequence of BOOLEAN ;
hence  0* n in BOOLEAN * by FINSEQ_1:def_11; ::_thesis: verum
end;

theorem Th5: :: BINARI_3:5
for n being Nat
for y being Tuple of n, BOOLEAN st y = 0* n holds
'not' y = n |-> 1
proof
let n be Nat; ::_thesis: for y being Tuple of n, BOOLEAN st y = 0* n holds
'not' y = n |-> 1
let y be Tuple of n, BOOLEAN ; ::_thesis: ( y = 0* n implies 'not' y = n |-> 1 )
assume A1: y = 0* n ; ::_thesis: 'not' y = n |-> 1
A2: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_('not'_y)_holds_
('not'_y)_._i_=_(n_|->_1)_._i
A3: len y = n by CARD_1:def_7;
let i be Nat; ::_thesis: ( 1 <= i & i <= len ('not' y) implies ('not' y) . i = (n |-> 1) . i )
assume that
A4: 1 <= i and
A5: i <= len ('not' y) ; ::_thesis: ('not' y) . i = (n |-> 1) . i
A6: len ('not' y) = n by CARD_1:def_7;
then A7: i in Seg n by A4, A5, FINSEQ_1:1;
then A8: y . i = FALSE by A1, FUNCOP_1:7;
thus ('not' y) . i = ('not' y) /. i by A4, A5, FINSEQ_4:15
.= 'not' (y /. i) by A7, BINARITH:def_1
.= 'not' FALSE by A4, A5, A6, A3, A8, FINSEQ_4:15
.= (n |-> 1) . i by A7, FUNCOP_1:7 ; ::_thesis: verum
end;
len ('not' y) = n by CARD_1:def_7
.= len (n |-> 1) by CARD_1:def_7 ;
hence  'not' y = n |-> 1 by A2, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th6: :: BINARI_3:6
for n being non empty Nat
for F being Tuple of n, BOOLEAN st F = 0* n holds
Absval F = 0
proof
defpred S1[ Nat] means  for F being Tuple of $1, BOOLEAN st F = 0* $1 holds
Absval F = 0 ;
A1: for n being non empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non empty Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: for F being Tuple of n, BOOLEAN st F = 0* n holds
Absval F = 0 ; ::_thesis: S1[n + 1]
let F be Tuple of n + 1, BOOLEAN ; ::_thesis: ( F = 0* (n + 1) implies Absval F = 0 )
 0* n in BOOLEAN * by Th4;
then  0* n is FinSequence of BOOLEAN by FINSEQ_1:def_11;
then reconsider F1 = 0* n as Tuple of n, BOOLEAN ;
assume  F = 0* (n + 1) ; ::_thesis: Absval F = 0
hence  Absval F = Absval (F1 ^ <*FALSE*>) by FINSEQ_2:60
.= (Absval F1) + (IFEQ (FALSE,FALSE,0,(2 to_power n))) by BINARITH:20
.= 0 + (IFEQ (FALSE,FALSE,0,(2 to_power n))) by A2
.= 0 by FUNCOP_1:def_8 ;
::_thesis: verum
end;
A3: S1[1] by BINARITH:15, FINSEQ_2:59;
thus  for n being non empty Nat holds S1[n] from NAT_1:sch_10(A3, A1); ::_thesis: verum
end;

theorem :: BINARI_3:7
for n being non empty Nat
for F being Tuple of n, BOOLEAN st F = 0* n holds
Absval ('not' F) = (2 to_power n) - 1
proof
let n be non empty Nat; ::_thesis: for F being Tuple of n, BOOLEAN st F = 0* n holds
Absval ('not' F) = (2 to_power n) - 1
let F be Tuple of n, BOOLEAN ; ::_thesis: ( F = 0* n implies Absval ('not' F) = (2 to_power n) - 1 )
assume A1: F = 0* n ; ::_thesis: Absval ('not' F) = (2 to_power n) - 1
thus  Absval ('not' F) = ((- (Absval F)) + (2 to_power n)) - 1 by BINARI_2:13
.= ((- 0) + (2 to_power n)) - 1 by A1, Th6
.= (2 to_power n) - 1 ; ::_thesis: verum
end;

theorem :: BINARI_3:8
for n being Nat holds Rev (0* n) = 0* n
proof
let n be Nat; ::_thesis: Rev (0* n) = 0* n
A1: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(0*_n)_holds_
(Rev_(0*_n))_._k_=_(0*_n)_._k
let k be Nat; ::_thesis: ( k in dom (0* n) implies (Rev (0* n)) . k = (0* n) . k )
assume A2: k in dom (0* n) ; ::_thesis: (Rev (0* n)) . k = (0* n) . k
then  k in Seg (len (0* n)) by FINSEQ_1:def_3;
then A3: k in Seg n by CARD_1:def_7;
then  (n - k) + 1 in Seg n by FINSEQ_5:2;
then A4: ((len (0* n)) - k) + 1 in Seg n by CARD_1:def_7;
thus (Rev (0* n)) . k = (0* n) . (((len (0* n)) - k) + 1) by A2, FINSEQ_5:58
.= 0 by A4, FUNCOP_1:7
.= (0* n) . k by A3, FUNCOP_1:7 ; ::_thesis: verum
end;
dom (Rev (0* n)) = Seg (len (Rev (0* n))) by FINSEQ_1:def_3
.= Seg (len (0* n)) by FINSEQ_5:def_3
.= dom (0* n) by FINSEQ_1:def_3 ;
hence  Rev (0* n) = 0* n by A1, FINSEQ_1:13; ::_thesis: verum
end;

theorem :: BINARI_3:9
for n being Nat
for y being Tuple of n, BOOLEAN st y = 0* n holds
Rev ('not' y) = 'not' y
proof
let n be Nat; ::_thesis: for y being Tuple of n, BOOLEAN st y = 0* n holds
Rev ('not' y) = 'not' y
let y be Tuple of n, BOOLEAN ; ::_thesis: ( y = 0* n implies Rev ('not' y) = 'not' y )
assume A1: y = 0* n ; ::_thesis: Rev ('not' y) = 'not' y
A2: now__::_thesis:_for_k_being_Nat_st_k_in_dom_('not'_y)_holds_
(Rev_('not'_y))_._k_=_('not'_y)_._k
let k be Nat; ::_thesis: ( k in dom ('not' y) implies (Rev ('not' y)) . k = ('not' y) . k )
assume A3: k in dom ('not' y) ; ::_thesis: (Rev ('not' y)) . k = ('not' y) . k
then  k in Seg (len ('not' y)) by FINSEQ_1:def_3;
then A4: k in Seg n by CARD_1:def_7;
then  (n - k) + 1 in Seg n by FINSEQ_5:2;
then A5: ((len ('not' y)) - k) + 1 in Seg n by CARD_1:def_7;
thus (Rev ('not' y)) . k = ('not' y) . (((len ('not' y)) - k) + 1) by A3, FINSEQ_5:58
.= (n |-> 1) . (((len ('not' y)) - k) + 1) by A1, Th5
.= 1 by A5, FUNCOP_1:7
.= (n |-> 1) . k by A4, FUNCOP_1:7
.= ('not' y) . k by A1, Th5 ; ::_thesis: verum
end;
dom (Rev ('not' y)) = Seg (len (Rev ('not' y))) by FINSEQ_1:def_3
.= Seg (len ('not' y)) by FINSEQ_5:def_3
.= dom ('not' y) by FINSEQ_1:def_3 ;
hence  Rev ('not' y) = 'not' y by A2, FINSEQ_1:13; ::_thesis: verum
end;

theorem Th10: :: BINARI_3:10
Bin1 1 = <*TRUE*>
proof
 1 in Seg 1 by FINSEQ_1:3;
then A1: (Bin1 1) /. 1 = TRUE by BINARI_2:5;
 ex d being Element of BOOLEAN st Bin1 1 = <*d*> by FINSEQ_2:97;
hence  Bin1 1 = <*TRUE*> by A1, FINSEQ_4:16; ::_thesis: verum
end;

theorem Th11: :: BINARI_3:11
for n being non empty Nat holds Absval (Bin1 n) = 1
proof
defpred S1[ Nat] means  Absval (Bin1 $1) = 1;
A1: for n being non empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non empty Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: Absval (Bin1 n) = 1 ; ::_thesis: S1[n + 1]
thus  Absval (Bin1 (n + 1)) = Absval ((Bin1 n) ^ <*FALSE*>) by BINARI_2:7
.= (Absval (Bin1 n)) + (IFEQ (FALSE,FALSE,0,(2 to_power n))) by BINARITH:20
.= (Absval (Bin1 n)) + 0 by FUNCOP_1:def_8
.= 1 by A2 ; ::_thesis: verum
end;
A3: S1[1] by Th10, BINARITH:16;
thus  for n being non empty Nat holds S1[n] from NAT_1:sch_10(A3, A1); ::_thesis: verum
end;

theorem Th12: :: BINARI_3:12
for x, y being Element of BOOLEAN holds
( ( not x 'or' y = TRUE or x = TRUE or y = TRUE ) & ( ( x = TRUE or y = TRUE ) implies x 'or' y = TRUE ) & ( x 'or' y = FALSE implies ( x = FALSE & y = FALSE ) ) & ( x = FALSE & y = FALSE implies x 'or' y = FALSE ) )
proof
let x, y be Element of BOOLEAN ; ::_thesis: ( ( not x 'or' y = TRUE or x = TRUE or y = TRUE ) & ( ( x = TRUE or y = TRUE ) implies x 'or' y = TRUE ) & ( x 'or' y = FALSE implies ( x = FALSE & y = FALSE ) ) & ( x = FALSE & y = FALSE implies x 'or' y = FALSE ) )
thus  ( not x 'or' y = TRUE or x = TRUE or y = TRUE ) ::_thesis: ( ( ( x = TRUE or y = TRUE ) implies x 'or' y = TRUE ) & ( x 'or' y = FALSE implies ( x = FALSE & y = FALSE ) ) & ( x = FALSE & y = FALSE implies x 'or' y = FALSE ) )
proof
assume  x 'or' y = TRUE ; ::_thesis: ( x = TRUE or y = TRUE )
then  ( 'not' x = FALSE or 'not' y = FALSE ) by MARGREL1:12;
hence  ( x = TRUE or y = TRUE ) ; ::_thesis: verum
end;
thus  ( ( x = TRUE or y = TRUE ) implies x 'or' y = TRUE ) ; ::_thesis: ( x 'or' y = FALSE iff ( x = FALSE & y = FALSE ) )
thus  ( x 'or' y = FALSE implies ( x = FALSE & y = FALSE ) ) ::_thesis: ( x = FALSE & y = FALSE implies x 'or' y = FALSE )
proof
assume A1: x 'or' y = FALSE ; ::_thesis: ( x = FALSE & y = FALSE )
then  'not' x = TRUE by MARGREL1:12;
hence  ( x = FALSE & y = FALSE ) by A1; ::_thesis: verum
end;
thus  ( x = FALSE & y = FALSE implies x 'or' y = FALSE ) ; ::_thesis: verum
end;

theorem Th13: :: BINARI_3:13
for x, y being Element of BOOLEAN holds
( add_ovfl (<*x*>,<*y*>) = TRUE iff ( x = TRUE & y = TRUE ) )
proof
let x, y be Element of BOOLEAN ; ::_thesis: ( add_ovfl (<*x*>,<*y*>) = TRUE iff ( x = TRUE & y = TRUE ) )
A1: (<*TRUE*> /. 1) '&' (<*TRUE*> /. 1) = TRUE by FINSEQ_4:16;
thus  ( add_ovfl (<*x*>,<*y*>) = TRUE implies ( x = TRUE & y = TRUE ) ) ::_thesis: ( x = TRUE & y = TRUE implies add_ovfl (<*x*>,<*y*>) = TRUE )
proof
assume  add_ovfl (<*x*>,<*y*>) = TRUE ; ::_thesis: ( x = TRUE & y = TRUE )
then  (((<*x*> /. 1) '&' (<*y*> /. 1)) 'or' ((<*x*> /. 1) '&' ((carry (<*x*>,<*y*>)) /. 1))) 'or' ((<*y*> /. 1) '&' ((carry (<*x*>,<*y*>)) /. 1)) = TRUE by BINARITH:def_6;
then A2: ( ((<*x*> /. 1) '&' (<*y*> /. 1)) 'or' ((<*x*> /. 1) '&' ((carry (<*x*>,<*y*>)) /. 1)) = TRUE or (<*y*> /. 1) '&' ((carry (<*x*>,<*y*>)) /. 1) = TRUE ) by Th12;
now__::_thesis:_(_x_=_TRUE_&_y_=_TRUE_)
percases ( (<*x*> /. 1) '&' (<*y*> /. 1) = TRUE or (<*x*> /. 1) '&' ((carry (<*x*>,<*y*>)) /. 1) = TRUE or (<*y*> /. 1) '&' ((carry (<*x*>,<*y*>)) /. 1) = TRUE ) by A2, Th12;
supposeA3: (<*x*> /. 1) '&' (<*y*> /. 1) = TRUE ; ::_thesis: ( x = TRUE & y = TRUE )
then  <*x*> /. 1 = TRUE by MARGREL1:12;
hence  ( x = TRUE & y = TRUE ) by A3, FINSEQ_4:16; ::_thesis: verum
end;
suppose (<*x*> /. 1) '&' ((carry (<*x*>,<*y*>)) /. 1) = TRUE ; ::_thesis: ( x = TRUE & y = TRUE )
then  (carry (<*x*>,<*y*>)) /. 1 = TRUE by MARGREL1:12;
hence  ( x = TRUE & y = TRUE ) by BINARITH:def_2; ::_thesis: verum
end;
suppose (<*y*> /. 1) '&' ((carry (<*x*>,<*y*>)) /. 1) = TRUE ; ::_thesis: ( x = TRUE & y = TRUE )
then  (carry (<*x*>,<*y*>)) /. 1 = TRUE by MARGREL1:12;
hence  ( x = TRUE & y = TRUE ) by BINARITH:def_2; ::_thesis: verum
end;
end;
end;
hence  ( x = TRUE & y = TRUE ) ; ::_thesis: verum
end;
assume that
A4: x = TRUE and
A5: y = TRUE ; ::_thesis: add_ovfl (<*x*>,<*y*>) = TRUE
thus  add_ovfl (<*x*>,<*y*>) = (((<*TRUE*> /. 1) '&' (<*TRUE*> /. 1)) 'or' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1))) 'or' ((<*TRUE*> /. 1) '&' ((carry (<*TRUE*>,<*TRUE*>)) /. 1)) by A4, A5, BINARITH:def_6
.= TRUE by A1 ; ::_thesis: verum
end;

theorem Th14: :: BINARI_3:14
'not' <*FALSE*> = <*TRUE*>
proof
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_1_holds_
('not'_<*FALSE*>)_._i_=_<*TRUE*>_._i
let i be Nat; ::_thesis: ( i in Seg 1 implies ('not' <*FALSE*>) . i = <*TRUE*> . i )
assume A1: i in Seg 1 ; ::_thesis: ('not' <*FALSE*>) . i = <*TRUE*> . i
then A2: i = 1 by FINSEQ_1:2, TARSKI:def_1;
 len <*FALSE*> = 1 by CARD_1:def_7;
then A3: <*FALSE*> /. i = <*FALSE*> . 1 by A2, FINSEQ_4:15;
 len ('not' <*FALSE*>) = 1 by CARD_1:def_7;
hence ('not' <*FALSE*>) . i = ('not' <*FALSE*>) /. i by A2, FINSEQ_4:15
.= 'not' (<*FALSE*> /. i) by A1, BINARITH:def_1
.= 'not' FALSE by A3, FINSEQ_1:40
.= <*TRUE*> . i by A2, FINSEQ_1:40 ;
::_thesis: verum
end;
hence  'not' <*FALSE*> = <*TRUE*> by FINSEQ_2:119; ::_thesis: verum
end;

theorem :: BINARI_3:15
'not' <*TRUE*> = <*FALSE*>
proof
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_1_holds_
('not'_<*TRUE*>)_._i_=_<*FALSE*>_._i
let i be Nat; ::_thesis: ( i in Seg 1 implies ('not' <*TRUE*>) . i = <*FALSE*> . i )
assume A1: i in Seg 1 ; ::_thesis: ('not' <*TRUE*>) . i = <*FALSE*> . i
then A2: i = 1 by FINSEQ_1:2, TARSKI:def_1;
 len <*TRUE*> = 1 by CARD_1:def_7;
then A3: <*TRUE*> /. i = <*TRUE*> . 1 by A2, FINSEQ_4:15;
 len ('not' <*TRUE*>) = 1 by CARD_1:def_7;
hence ('not' <*TRUE*>) . i = ('not' <*TRUE*>) /. i by A2, FINSEQ_4:15
.= 'not' (<*TRUE*> /. i) by A1, BINARITH:def_1
.= 'not' TRUE by A3, FINSEQ_1:40
.= <*FALSE*> . i by A2, FINSEQ_1:40 ;
::_thesis: verum
end;
hence  'not' <*TRUE*> = <*FALSE*> by FINSEQ_2:119; ::_thesis: verum
end;

theorem :: BINARI_3:16
<*FALSE*> + <*FALSE*> = <*FALSE*>
proof
 add_ovfl (<*FALSE*>,<*FALSE*>) <> TRUE by Th13;
then  add_ovfl (<*FALSE*>,<*FALSE*>) = FALSE by XBOOLEAN:def_3;
then  <*FALSE*>,<*FALSE*> are_summable by BINARITH:def_7;
then  Absval (<*FALSE*> + <*FALSE*>) = (Absval <*FALSE*>) + (Absval <*FALSE*>) by BINARITH:22
.= (Absval <*FALSE*>) + 0 by BINARITH:15
.= Absval <*FALSE*> ;
hence  <*FALSE*> + <*FALSE*> = <*FALSE*> by Th2; ::_thesis: verum
end;

theorem Th17: :: BINARI_3:17
( <*FALSE*> + <*TRUE*> = <*TRUE*> & <*TRUE*> + <*FALSE*> = <*TRUE*> )
proof
 add_ovfl (<*FALSE*>,<*TRUE*>) <> TRUE by Th13;
then  add_ovfl (<*FALSE*>,<*TRUE*>) = FALSE by XBOOLEAN:def_3;
then  <*FALSE*>,<*TRUE*> are_summable by BINARITH:def_7;
then  Absval (<*FALSE*> + <*TRUE*>) = (Absval <*FALSE*>) + (Absval <*TRUE*>) by BINARITH:22
.= (Absval <*FALSE*>) + 1 by BINARITH:16
.= 0 + 1 by BINARITH:15
.= Absval <*TRUE*> by BINARITH:16 ;
hence  <*FALSE*> + <*TRUE*> = <*TRUE*> by Th2; ::_thesis: <*TRUE*> + <*FALSE*> = <*TRUE*>
 add_ovfl (<*TRUE*>,<*FALSE*>) <> TRUE by Th13;
then  add_ovfl (<*TRUE*>,<*FALSE*>) = FALSE by XBOOLEAN:def_3;
then  <*TRUE*>,<*FALSE*> are_summable by BINARITH:def_7;
then  Absval (<*TRUE*> + <*FALSE*>) = (Absval <*TRUE*>) + (Absval <*FALSE*>) by BINARITH:22
.= (Absval <*TRUE*>) + 0 by BINARITH:15
.= Absval <*TRUE*> ;
hence  <*TRUE*> + <*FALSE*> = <*TRUE*> by Th2; ::_thesis: verum
end;

theorem :: BINARI_3:18
<*TRUE*> + <*TRUE*> = <*FALSE*>
proof
A1: add_ovfl (<*TRUE*>,<*TRUE*>) = TRUE by Th13;
Absval (<*TRUE*> + <*TRUE*>) = ((Absval (<*TRUE*> + <*TRUE*>)) + 2) - 2
.= ((Absval (<*TRUE*> + <*TRUE*>)) + (2 to_power 1)) - 2 by POWER:25
.= ((Absval (<*TRUE*> + <*TRUE*>)) + (IFEQ ((add_ovfl (<*TRUE*>,<*TRUE*>)),FALSE,0,(2 to_power 1)))) - 2 by A1, FUNCOP_1:def_8
.= ((Absval <*TRUE*>) + (Absval <*TRUE*>)) - 2 by BINARITH:21
.= ((Absval <*TRUE*>) + 1) - 2 by BINARITH:16
.= (1 + 1) - 2 by BINARITH:16
.= Absval <*FALSE*> by BINARITH:15 ;
hence  <*TRUE*> + <*TRUE*> = <*FALSE*> by Th2; ::_thesis: verum
end;

theorem Th19: :: BINARI_3:19
for n being non empty Nat
for x, y being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds
for k being non empty Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )
proof
let n be non empty Nat; ::_thesis: for x, y being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds
for k being non empty Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )
let x, y be Tuple of n, BOOLEAN ; ::_thesis: ( x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE implies for k being non empty Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE ) )
assume that
A1: x /. n = TRUE and
A2: (carry (x,(Bin1 n))) /. n = TRUE ; ::_thesis: for k being non empty Nat st k <> 1 & k <= n holds
( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )
defpred S1[ Nat] means ( $1 in Seg (n -' 1) implies ( x /. ((n -' $1) + 1) = TRUE & (carry (x,(Bin1 n))) /. ((n -' $1) + 1) = TRUE ) );
let k be non empty Nat; ::_thesis: ( k <> 1 & k <= n implies ( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE ) )
assume that
A3: k <> 1 and
A4: k <= n ; ::_thesis: ( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE )
set i = (n -' k) + 1;
 1 < k by A3, NAT_2:19;
then  1 + 1 <= k by NAT_1:13;
then A5: 1 <= k - 1 by XREAL_1:19;
A6: for j being non empty Nat st S1[j] holds
S1[j + 1]
proof
let j be non empty Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
assume that
A7: S1[j] and
A8: j + 1 in Seg (n -' 1) ; ::_thesis: ( x /. ((n -' (j + 1)) + 1) = TRUE & (carry (x,(Bin1 n))) /. ((n -' (j + 1)) + 1) = TRUE )
A9: j + 1 <= n -' 1 by A8, FINSEQ_1:1;
then A10: j < n -' 1 by NAT_1:13;
then  j < n - 1 by NAT_1:14, XREAL_1:233;
then  j + 1 < n by XREAL_1:20;
then A11: j < n by NAT_1:13;
 j + 1 <= n - 1 by A9, NAT_1:14, XREAL_1:233;
then  1 <= (n - 1) - j by XREAL_1:19;
then  1 <= (n - j) - 1 ;
then  1 + 1 <= n - j by XREAL_1:19;
then  1 + 1 <= n -' j by A11, XREAL_1:233;
then A12: n -' j > 1 by NAT_1:13;
A13: 1 <= j by NAT_1:14;
A14: n -' j < n by NAT_2:9;
then  n -' j in Seg n by A12, FINSEQ_1:1;
then A15: (Bin1 n) /. (n -' j) = FALSE by A12, BINARI_2:6;
then  ((Bin1 n) /. (n -' j)) '&' ((carry (x,(Bin1 n))) /. (n -' j)) = FALSE ;
then A16: TRUE = ((x /. (n -' j)) '&' ((Bin1 n) /. (n -' j))) 'or' ((x /. (n -' j)) '&' ((carry (x,(Bin1 n))) /. (n -' j))) by A7, A13, A10, A14, A12, A15, BINARITH:def_2, FINSEQ_1:1
.= (x /. (n -' j)) '&' ((carry (x,(Bin1 n))) /. (n -' j)) by A15 ;
then  x /. (n -' j) = TRUE by MARGREL1:12;
hence  x /. ((n -' (j + 1)) + 1) = TRUE by A11, NAT_2:7; ::_thesis: (carry (x,(Bin1 n))) /. ((n -' (j + 1)) + 1) = TRUE
 (carry (x,(Bin1 n))) /. (n -' j) = TRUE by A16, MARGREL1:12;
hence  (carry (x,(Bin1 n))) /. ((n -' (j + 1)) + 1) = TRUE by A11, NAT_2:7; ::_thesis: verum
end;
A17: 1 <= (n -' k) + 1 by NAT_1:11;
(n -' k) + 1 = (n - k) + 1 by A4, XREAL_1:233
.= n - (k - 1) ;
then A18: (n -' k) + 1 <= n - 1 by A5, XREAL_1:13;
then  ((n -' k) + 1) + 1 <= n by XREAL_1:19;
then  (n -' k) + 1 < n by NAT_1:13;
then A19: k = (n -' ((n -' k) + 1)) + 1 by A4, NAT_2:5;
 (n -' k) + 1 <= n -' 1 by A18, NAT_1:14, XREAL_1:233;
then A20: (n -' k) + 1 in Seg (n -' 1) by A17, FINSEQ_1:1;
A21: S1[1] by A1, A2, NAT_1:14, XREAL_1:235;
 for j being non empty Nat holds S1[j] from NAT_1:sch_10(A21, A6);
hence  ( x /. k = TRUE & (carry (x,(Bin1 n))) /. k = TRUE ) by A19, A20; ::_thesis: verum
end;

theorem Th20: :: BINARI_3:20
for n being non empty Nat
for x being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds
carry (x,(Bin1 n)) = 'not' (Bin1 n)
proof
let n be non empty Nat; ::_thesis: for x being Tuple of n, BOOLEAN st x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds
carry (x,(Bin1 n)) = 'not' (Bin1 n)
let x be Tuple of n, BOOLEAN ; ::_thesis: ( x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE implies carry (x,(Bin1 n)) = 'not' (Bin1 n) )
assume that
A1: x /. n = TRUE and
A2: (carry (x,(Bin1 n))) /. n = TRUE ; ::_thesis: carry (x,(Bin1 n)) = 'not' (Bin1 n)
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_n_holds_
(carry_(x,(Bin1_n)))_._i_=_('not'_(Bin1_n))_._i
A3: len ('not' (Bin1 n)) = n by CARD_1:def_7;
let i be Nat; ::_thesis: ( i in Seg n implies (carry (x,(Bin1 n))) . b1 = ('not' (Bin1 n)) . b1 )
reconsider z = i as Nat ;
A4: len (carry (x,(Bin1 n))) = n by CARD_1:def_7;
assume A5: i in Seg n ; ::_thesis: (carry (x,(Bin1 n))) . b1 = ('not' (Bin1 n)) . b1
then A6: 1 <= i by FINSEQ_1:1;
A7: i <= n by A5, FINSEQ_1:1;
percases ( i = 1 or i <> 1 ) ;
supposeA8: i = 1 ; ::_thesis: (carry (x,(Bin1 n))) . b1 = ('not' (Bin1 n)) . b1
thus (carry (x,(Bin1 n))) . i = (carry (x,(Bin1 n))) /. z by A6, A7, A4, FINSEQ_4:15
.= 'not' TRUE by A8, BINARITH:def_2
.= 'not' ((Bin1 n) /. i) by A5, A8, BINARI_2:5
.= ('not' (Bin1 n)) /. z by A5, BINARITH:def_1
.= ('not' (Bin1 n)) . i by A6, A7, A3, FINSEQ_4:15 ; ::_thesis: verum
end;
supposeA9: i <> 1 ; ::_thesis: (carry (x,(Bin1 n))) . b1 = ('not' (Bin1 n)) . b1
A10: not i is empty by A5, FINSEQ_1:1;
thus (carry (x,(Bin1 n))) . i = (carry (x,(Bin1 n))) /. z by A6, A7, A4, FINSEQ_4:15
.= 'not' FALSE by A1, A2, A7, A9, A10, Th19
.= 'not' ((Bin1 n) /. i) by A5, A9, BINARI_2:6
.= ('not' (Bin1 n)) /. z by A5, BINARITH:def_1
.= ('not' (Bin1 n)) . i by A6, A7, A3, FINSEQ_4:15 ; ::_thesis: verum
end;
end;
end;
hence  carry (x,(Bin1 n)) = 'not' (Bin1 n) by FINSEQ_2:119; ::_thesis: verum
end;

theorem Th21: :: BINARI_3:21
for n being non empty Nat
for x, y being Tuple of n, BOOLEAN st y = 0* n & x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds
x = 'not' y
proof
let n be non empty Nat; ::_thesis: for x, y being Tuple of n, BOOLEAN st y = 0* n & x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE holds
x = 'not' y
let x, y be Tuple of n, BOOLEAN ; ::_thesis: ( y = 0* n & x /. n = TRUE & (carry (x,(Bin1 n))) /. n = TRUE implies x = 'not' y )
assume that
A1: y = 0* n and
A2: x /. n = TRUE and
A3: (carry (x,(Bin1 n))) /. n = TRUE ; ::_thesis: x = 'not' y
A4: len x = n by CARD_1:def_7;
A5: len ('not' y) = n by CARD_1:def_7;
A6: len y = n by CARD_1:def_7;
A7: len (carry (x,(Bin1 n))) = n by CARD_1:def_7;
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_n_holds_
x_._i_=_('not'_y)_._i
let i be Nat; ::_thesis: ( i in Seg n implies x . i = ('not' y) . i )
reconsider z = i as Nat ;
assume A8: i in Seg n ; ::_thesis: x . i = ('not' y) . i
then A9: 1 <= i by FINSEQ_1:1;
A10: i <= n by A8, FINSEQ_1:1;
A11: y . i = FALSE by A1, A8, FUNCOP_1:7;
now__::_thesis:_x_._i_=_('not'_y)_._i
percases ( i = 1 or i <> 1 ) ;
supposeA12: i = 1 ; ::_thesis: x . i = ('not' y) . i
A13: n >= 1 by NAT_1:14;
now__::_thesis:_x_._i_=_('not'_y)_._i
percases ( n = 1 or n > 1 ) by A13, XXREAL_0:1;
suppose n = 1 ; ::_thesis: x . i = ('not' y) . i
hence  x . i = ('not' y) . i by A3, BINARITH:def_2; ::_thesis: verum
end;
supposeA14: n > 1 ; ::_thesis: x . i = ('not' y) . i
A15: len ('not' (Bin1 n)) = n by CARD_1:def_7;
A16: (carry (x,(Bin1 n))) /. i = FALSE by A12, BINARITH:def_2;
then A17: ((Bin1 n) /. i) '&' ((carry (x,(Bin1 n))) /. i) = FALSE ;
A18: 1 + 1 <= n by A14, NAT_1:13;
then A19: 2 in Seg n by FINSEQ_1:1;
(carry (x,(Bin1 n))) . (i + 1) = ('not' (Bin1 n)) . 2 by A2, A3, A12, Th20
.= ('not' (Bin1 n)) /. 2 by A18, A15, FINSEQ_4:15
.= 'not' ((Bin1 n) /. 2) by A19, BINARITH:def_1
.= 'not' FALSE by A19, BINARI_2:6
.= TRUE ;
then A20: TRUE = (carry (x,(Bin1 n))) /. (i + 1) by A7, A12, A18, FINSEQ_4:15
.= ((x /. i) '&' ((Bin1 n) /. i)) 'or' ((x /. i) '&' ((carry (x,(Bin1 n))) /. i)) by A12, A14, A16, A17, BINARITH:def_2
.= (x /. i) '&' ((Bin1 n) /. i) by A16 ;
thus x . i = x /. z by A4, A9, A10, FINSEQ_4:15
.= 'not' FALSE by A20, MARGREL1:12
.= 'not' (y /. z) by A6, A9, A10, A11, FINSEQ_4:15
.= ('not' y) /. z by A8, BINARITH:def_1
.= ('not' y) . i by A5, A9, A10, FINSEQ_4:15 ; ::_thesis: verum
end;
end;
end;
hence  x . i = ('not' y) . i ; ::_thesis: verum
end;
supposeA21: i <> 1 ; ::_thesis: x . i = ('not' y) . i
A22: not i is empty by A8, FINSEQ_1:1;
thus x . i = x /. z by A4, A9, A10, FINSEQ_4:15
.= 'not' FALSE by A2, A3, A10, A21, A22, Th19
.= 'not' (y /. z) by A6, A9, A10, A11, FINSEQ_4:15
.= ('not' y) /. z by A8, BINARITH:def_1
.= ('not' y) . i by A5, A9, A10, FINSEQ_4:15 ; ::_thesis: verum
end;
end;
end;
hence  x . i = ('not' y) . i ; ::_thesis: verum
end;
hence  x = 'not' y by FINSEQ_2:119; ::_thesis: verum
end;

theorem Th22: :: BINARI_3:22
for n being non empty Nat
for y being Tuple of n, BOOLEAN st y = 0* n holds
carry (('not' y),(Bin1 n)) = 'not' (Bin1 n)
proof
let n be non empty Nat; ::_thesis: for y being Tuple of n, BOOLEAN st y = 0* n holds
carry (('not' y),(Bin1 n)) = 'not' (Bin1 n)
let y be Tuple of n, BOOLEAN ; ::_thesis: ( y = 0* n implies carry (('not' y),(Bin1 n)) = 'not' (Bin1 n) )
A1: n >= 1 by NAT_1:14;
A2: len y = n by CARD_1:def_7;
assume A3: y = 0* n ; ::_thesis: carry (('not' y),(Bin1 n)) = 'not' (Bin1 n)
then A4: y . n = 0 by FINSEQ_1:3, FUNCOP_1:7;
 n in Seg n by FINSEQ_1:3;
then A5: ('not' y) /. n = 'not' (y /. n) by BINARITH:def_1
.= 'not' FALSE by A1, A4, A2, FINSEQ_4:15
.= TRUE ;
percases ( n = 1 or n <> 1 ) ;
supposeA6: n = 1 ; ::_thesis: carry (('not' y),(Bin1 n)) = 'not' (Bin1 n)
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_n_holds_
(carry_(('not'_y),(Bin1_n)))_._i_=_('not'_(Bin1_n))_._i
let i be Nat; ::_thesis: ( i in Seg n implies (carry (('not' y),(Bin1 n))) . i = ('not' (Bin1 n)) . i )
A7: len ('not' (Bin1 n)) = n by CARD_1:def_7;
assume A8: i in Seg n ; ::_thesis: (carry (('not' y),(Bin1 n))) . i = ('not' (Bin1 n)) . i
then A9: i = 1 by A6, FINSEQ_1:2, TARSKI:def_1;
 len (carry (('not' y),(Bin1 n))) = n by CARD_1:def_7;
hence (carry (('not' y),(Bin1 n))) . i = (carry (('not' y),(Bin1 n))) /. i by A6, A9, FINSEQ_4:15
.= 'not' TRUE by A9, BINARITH:def_2
.= 'not' ((Bin1 n) /. i) by A8, A9, BINARI_2:5
.= ('not' (Bin1 n)) /. i by A8, BINARITH:def_1
.= ('not' (Bin1 n)) . i by A6, A9, A7, FINSEQ_4:15 ;
::_thesis: verum
end;
hence  carry (('not' y),(Bin1 n)) = 'not' (Bin1 n) by FINSEQ_2:119; ::_thesis: verum
end;
suppose n <> 1 ; ::_thesis: carry (('not' y),(Bin1 n)) = 'not' (Bin1 n)
then A10: not n is trivial by NAT_2:def_1;
defpred S1[ Nat] means ( $1 <= n implies (carry (('not' y),(Bin1 n))) /. $1 = TRUE );
A11: for i being non trivial Nat st S1[i] holds
S1[i + 1]
proof
let i be non trivial Nat; ::_thesis: ( S1[i] implies S1[i + 1] )
assume that
A12: ( i <= n implies (carry (('not' y),(Bin1 n))) /. i = TRUE ) and
A13: i + 1 <= n ; ::_thesis: (carry (('not' y),(Bin1 n))) /. (i + 1) = TRUE
A14: 1 <= i by NAT_1:14;
A15: i < n by A13, NAT_1:13;
then A16: i in Seg n by A14, FINSEQ_1:1;
then A17: y . i = FALSE by A3, FUNCOP_1:7;
A18: ('not' y) /. i = 'not' (y /. i) by A16, BINARITH:def_1
.= 'not' FALSE by A2, A14, A15, A17, FINSEQ_4:15
.= TRUE ;
 i <> 1 by NAT_2:def_1;
then A19: (Bin1 n) /. i = FALSE by A16, BINARI_2:6;
then  ((Bin1 n) /. i) '&' ((carry (('not' y),(Bin1 n))) /. i) = FALSE ;
hence (carry (('not' y),(Bin1 n))) /. (i + 1) = ((('not' y) /. i) '&' ((Bin1 n) /. i)) 'or' ((('not' y) /. i) '&' ((carry (('not' y),(Bin1 n))) /. i)) by A14, A15, A19, BINARITH:def_2
.= TRUE by A12, A13, A18, NAT_1:13 ;
::_thesis: verum
end;
A20: S1[2]
proof
assume  2 <= n ; ::_thesis: (carry (('not' y),(Bin1 n))) /. 2 = TRUE
then  1 + 1 <= n ;
then A21: 1 < n by NAT_1:13;
then A22: 1 in Seg n by FINSEQ_1:1;
then A23: y . 1 = FALSE by A3, FUNCOP_1:7;
('not' y) /. 1 = 'not' (y /. 1) by A22, BINARITH:def_1
.= 'not' FALSE by A2, A21, A23, FINSEQ_4:15
.= TRUE ;
then A24: (('not' y) /. 1) '&' ((Bin1 n) /. 1) = TRUE by A22, BINARI_2:5;
thus (carry (('not' y),(Bin1 n))) /. 2 = (carry (('not' y),(Bin1 n))) /. (1 + 1)
.= (((('not' y) /. 1) '&' ((Bin1 n) /. 1)) 'or' ((('not' y) /. 1) '&' ((carry (('not' y),(Bin1 n))) /. 1))) 'or' (((Bin1 n) /. 1) '&' ((carry (('not' y),(Bin1 n))) /. 1)) by A21, BINARITH:def_2
.= TRUE by A24 ; ::_thesis: verum
end;
 for i being non trivial Nat holds S1[i] from NAT_2:sch_2(A20, A11);
then  (carry (('not' y),(Bin1 n))) /. n = TRUE by A10;
hence  carry (('not' y),(Bin1 n)) = 'not' (Bin1 n) by A5, Th20; ::_thesis: verum
end;
end;
end;

theorem Th23: :: BINARI_3:23
for n being non empty Nat
for x, y being Tuple of n, BOOLEAN st y = 0* n holds
( add_ovfl (x,(Bin1 n)) = TRUE iff x = 'not' y )
proof
let n be non empty Nat; ::_thesis: for x, y being Tuple of n, BOOLEAN st y = 0* n holds
( add_ovfl (x,(Bin1 n)) = TRUE iff x = 'not' y )
let x, y be Tuple of n, BOOLEAN ; ::_thesis: ( y = 0* n implies ( add_ovfl (x,(Bin1 n)) = TRUE iff x = 'not' y ) )
assume A1: y = 0* n ; ::_thesis: ( add_ovfl (x,(Bin1 n)) = TRUE iff x = 'not' y )
A2: n in Seg n by FINSEQ_1:3;
A3: 1 in Seg 1 by FINSEQ_1:3;
thus  ( add_ovfl (x,(Bin1 n)) = TRUE implies x = 'not' y ) ::_thesis: ( x = 'not' y implies add_ovfl (x,(Bin1 n)) = TRUE )
proof
assume A4: add_ovfl (x,(Bin1 n)) = TRUE ; ::_thesis: x = 'not' y
then A5: (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) 'or' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)) = TRUE by BINARITH:def_6;
percases ( n <> 1 or n = 1 ) ;
supposeA6: n <> 1 ; ::_thesis: x = 'not' y
now__::_thesis:_x_=_'not'_y
percases ( ((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)) = TRUE or ((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n) = TRUE ) by A5, Th12;
supposeA7: ((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)) = TRUE ; ::_thesis: x = 'not' y
now__::_thesis:_not_x_<>_'not'_y
percases ( (x /. n) '&' ((Bin1 n) /. n) = TRUE or (x /. n) '&' ((carry (x,(Bin1 n))) /. n) = TRUE ) by A7, Th12;
supposeA8: (x /. n) '&' ((Bin1 n) /. n) = TRUE ; ::_thesis: not x <> 'not' y
assume  x <> 'not' y ; ::_thesis: contradiction
 (Bin1 n) /. n = TRUE by A8, MARGREL1:12;
hence  contradiction by A2, A6, BINARI_2:6; ::_thesis: verum
end;
supposeA9: (x /. n) '&' ((carry (x,(Bin1 n))) /. n) = TRUE ; ::_thesis: x = 'not' y
then  x /. n = TRUE by MARGREL1:12;
hence  x = 'not' y by A1, A9, Th21; ::_thesis: verum
end;
end;
end;
hence  x = 'not' y ; ::_thesis: verum
end;
supposeA10: ((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n) = TRUE ; ::_thesis: not x <> 'not' y
assume  x <> 'not' y ; ::_thesis: contradiction
 (Bin1 n) /. n = TRUE by A10, MARGREL1:12;
hence  contradiction by A2, A6, BINARI_2:6; ::_thesis: verum
end;
end;
end;
hence  x = 'not' y ; ::_thesis: verum
end;
supposeA11: n = 1 ; ::_thesis: x = 'not' y
then  len y = 1 by CARD_1:def_7;
then  1 in dom y by A3, FINSEQ_1:def_3;
then A12: y /. 1 = y . 1 by PARTFUN1:def_6
.= 0 by A1, A11, FINSEQ_1:3, FUNCOP_1:7 ;
consider d being Element of BOOLEAN  such that
A13: x = <*d*> by A11, FINSEQ_2:97;
A14: d = TRUE by A4, A11, A13, Th10, Th13;
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_n_holds_
x_/._i_=_'not'_(y_/._i)
let i be Nat; ::_thesis: ( i in Seg n implies x /. i = 'not' (y /. i) )
assume  i in Seg n ; ::_thesis: x /. i = 'not' (y /. i)
then  i = 1 by A11, FINSEQ_1:2, TARSKI:def_1;
hence  x /. i = 'not' (y /. i) by A13, A14, A12, FINSEQ_4:16; ::_thesis: verum
end;
hence  x = 'not' y by BINARITH:def_1; ::_thesis: verum
end;
end;
end;
assume A15: x = 'not' y ; ::_thesis: add_ovfl (x,(Bin1 n)) = TRUE
percases ( n <> 1 or n = 1 ) ;
supposeA16: n <> 1 ; ::_thesis: add_ovfl (x,(Bin1 n)) = TRUE
A17: (carry (x,(Bin1 n))) /. n = ('not' (Bin1 n)) /. n by A1, A15, Th22
.= 'not' ((Bin1 n) /. n) by A2, BINARITH:def_1
.= 'not' FALSE by A2, A16, BINARI_2:6
.= TRUE ;
 len y = n by CARD_1:def_7;
then  n in dom y by A2, FINSEQ_1:def_3;
then A18: y /. n = y . n by PARTFUN1:def_6
.= 0 by A1, FINSEQ_1:3, FUNCOP_1:7 ;
A19: x /. n = 'not' (y /. n) by A2, A15, BINARITH:def_1
.= TRUE by A18 ;
thus  add_ovfl (x,(Bin1 n)) = (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) 'or' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)) by BINARITH:def_6
.= TRUE by A19, A17 ; ::_thesis: verum
end;
supposeA20: n = 1 ; ::_thesis: add_ovfl (x,(Bin1 n)) = TRUE
then  len y = 1 by CARD_1:def_7;
then  1 in dom y by A3, FINSEQ_1:def_3;
then A21: y /. 1 = y . 1 by PARTFUN1:def_6
.= 0 by A1, A20, FINSEQ_1:3, FUNCOP_1:7 ;
consider d being Element of BOOLEAN  such that
A22: x = <*d*> by A20, FINSEQ_2:97;
d = ('not' y) /. 1 by A15, A22, FINSEQ_4:16
.= 'not' (y /. 1) by A3, A20, BINARITH:def_1
.= TRUE by A21 ;
hence  add_ovfl (x,(Bin1 n)) = TRUE by A20, A22, Th10, Th13; ::_thesis: verum
end;
end;
end;

theorem Th24: :: BINARI_3:24
for n being non empty Nat
for z being Tuple of n, BOOLEAN st z = 0* n holds
('not' z) + (Bin1 n) = z
proof
let n be non empty Nat; ::_thesis: for z being Tuple of n, BOOLEAN st z = 0* n holds
('not' z) + (Bin1 n) = z
let z be Tuple of n, BOOLEAN ; ::_thesis: ( z = 0* n implies ('not' z) + (Bin1 n) = z )
assume A1: z = 0* n ; ::_thesis: ('not' z) + (Bin1 n) = z
then A2: add_ovfl (('not' z),(Bin1 n)) = TRUE by Th23;
Absval (('not' z) + (Bin1 n)) = ((Absval (('not' z) + (Bin1 n))) + (2 to_power n)) - (2 to_power n)
.= ((Absval (('not' z) + (Bin1 n))) + (IFEQ ((add_ovfl (('not' z),(Bin1 n))),FALSE,0,(2 to_power n)))) - (2 to_power n) by A2, FUNCOP_1:def_8
.= ((Absval ('not' z)) + (Absval (Bin1 n))) - (2 to_power n) by BINARITH:21
.= ((((- (Absval z)) + (2 to_power n)) - 1) + (Absval (Bin1 n))) - (2 to_power n) by BINARI_2:13
.= ((((- (Absval z)) + (2 to_power n)) - 1) + 1) - (2 to_power n) by Th11
.= - 0 by A1, Th6
.= Absval z by A1, Th6 ;
hence  ('not' z) + (Bin1 n) = z by Th2; ::_thesis: verum
end;

begin

definition
let n, k be Nat;
funcn -BinarySequence k ->  Tuple of n, BOOLEAN  means :Def1: :: BINARI_3:def 1
 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)
proof
reconsider n9 = n as Nat ;
deffunc H1( Nat) ->  Element of BOOLEAN = IFEQ (((k div (2 to_power ($1 -' 1))) mod 2),0,FALSE,TRUE);
consider p being FinSequence of BOOLEAN  such that
A1: len p = n9 and
A2: for i being Nat st i in dom p holds
p . i = H1(i) from FINSEQ_2:sch_1();
A3: dom p = Seg n9 by A1, FINSEQ_1:def_3;
reconsider p = p as Element of n -tuples_on BOOLEAN by A1, FINSEQ_2:92;
take  p ; ::_thesis: for i being Nat st i in Seg n holds
p /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE)
let i be Nat; ::_thesis: ( i in Seg n implies p /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) )
assume A4: i in Seg n ; ::_thesis: p /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE)
then  i in dom p by A1, FINSEQ_1:def_3;
hence p /. i = p . i by PARTFUN1:def_6
.= IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A2, A3, A4 ;
::_thesis: verum
end;
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
proof
let p1, p2 be Tuple of n, BOOLEAN ; ::_thesis: ( ( for i being Nat st i in Seg n holds
p1 /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) ) & ( for i being Nat st i in Seg n holds
p2 /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) ) implies p1 = p2 )
assume that
A5: for i being Nat st i in Seg n holds
p1 /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) and
A6: for i being Nat st i in Seg n holds
p2 /. i = IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) ; ::_thesis: p1 = p2
A7: len p1 = n by CARD_1:def_7;
then A8: dom p1 = Seg n by FINSEQ_1:def_3;
A9: len p2 = n by CARD_1:def_7;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_p1_holds_
p1_._i_=_p2_._i
let i be Nat; ::_thesis: ( i in dom p1 implies p1 . i = p2 . i )
assume A10: i in dom p1 ; ::_thesis: p1 . i = p2 . i
then A11: i in dom p2 by A9, A8, FINSEQ_1:def_3;
thus p1 . i = p1 /. i by A10, PARTFUN1:def_6
.= IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A5, A8, A10
.= p2 /. i by A6, A8, A10
.= p2 . i by A11, PARTFUN1:def_6 ; ::_thesis: verum
end;
hence  p1 = p2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
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 Th25: :: BINARI_3:25
for n being Nat holds n -BinarySequence 0 = 0* n
proof
let n be Nat; ::_thesis: n -BinarySequence 0 = 0* n
 0* n in BOOLEAN * by Th4;
then  0* n is FinSequence of BOOLEAN by FINSEQ_1:def_11;
then reconsider F = 0* n as Tuple of n, BOOLEAN ;
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_n_holds_
(n_-BinarySequence_0)_._i_=_F_._i
let i be Nat; ::_thesis: ( i in Seg n implies (n -BinarySequence 0) . i = F . i )
assume A1: i in Seg n ; ::_thesis: (n -BinarySequence 0) . i = F . i
 len (n -BinarySequence 0) = n by CARD_1:def_7;
then  i in dom (n -BinarySequence 0) by A1, FINSEQ_1:def_3;
hence (n -BinarySequence 0) . i = (n -BinarySequence 0) /. i by PARTFUN1:def_6
.= IFEQ (((0 div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A1, Def1
.= IFEQ ((0 mod 2),0,FALSE,TRUE) by NAT_2:2
.= IFEQ (0,0,FALSE,TRUE) by NAT_D:26
.= 0 by FUNCOP_1:def_8
.= F . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence  n -BinarySequence 0 = 0* n by FINSEQ_2:119; ::_thesis: verum
end;

theorem Th26: :: BINARI_3:26
for n, k being Nat st k < 2 to_power n holds
((n + 1) -BinarySequence k) . (n + 1) = FALSE
proof
let n, k be Nat; ::_thesis: ( k < 2 to_power n implies ((n + 1) -BinarySequence k) . (n + 1) = FALSE )
A1: (n + 1) -' 1 = (n + 1) - 1 by NAT_D:37
.= n ;
assume  k < 2 to_power n ; ::_thesis: ((n + 1) -BinarySequence k) . (n + 1) = FALSE
then A2: (k div (2 to_power ((n + 1) -' 1))) mod 2 = 0 mod 2 by A1, NAT_D:27
.= 0 by NAT_D:26 ;
A3: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then  n + 1 in Seg (len ((n + 1) -BinarySequence k)) by CARD_1:def_7;
then  n + 1 in dom ((n + 1) -BinarySequence k) by FINSEQ_1:def_3;
hence ((n + 1) -BinarySequence k) . (n + 1) = ((n + 1) -BinarySequence k) /. (n + 1) by PARTFUN1:def_6
.= IFEQ (((k div (2 to_power ((n + 1) -' 1))) mod 2),0,FALSE,TRUE) by A3, Def1
.= FALSE by A2, FUNCOP_1:def_8 ;
::_thesis: verum
end;

theorem Th27: :: BINARI_3:27
for n being non empty Nat
for k being Nat st k < 2 to_power n holds
(n + 1) -BinarySequence k = (n -BinarySequence k) ^ <*FALSE*>
proof
let n be non empty Nat; ::_thesis: for k being Nat st k < 2 to_power n holds
(n + 1) -BinarySequence k = (n -BinarySequence k) ^ <*FALSE*>
let k be Nat; ::_thesis: ( k < 2 to_power n implies (n + 1) -BinarySequence k = (n -BinarySequence k) ^ <*FALSE*> )
assume A1: k < 2 to_power n ; ::_thesis: (n + 1) -BinarySequence k = (n -BinarySequence k) ^ <*FALSE*>
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(n_+_1)_holds_
((n_+_1)_-BinarySequence_k)_._i_=_((n_-BinarySequence_k)_^_<*FALSE*>)_._i
let i be Nat; ::_thesis: ( i in Seg (n + 1) implies ((n + 1) -BinarySequence k) . i = ((n -BinarySequence k) ^ <*FALSE*>) . i )
assume A2: i in Seg (n + 1) ; ::_thesis: ((n + 1) -BinarySequence k) . i = ((n -BinarySequence k) ^ <*FALSE*>) . i
then  i in Seg (len ((n + 1) -BinarySequence k)) by CARD_1:def_7;
then A3: i in dom ((n + 1) -BinarySequence k) by FINSEQ_1:def_3;
now__::_thesis:_((n_+_1)_-BinarySequence_k)_._i_=_((n_-BinarySequence_k)_^_<*FALSE*>)_._i
percases ( i in Seg n or i = n + 1 ) by A2, FINSEQ_2:7;
supposeA4: i in Seg n ; ::_thesis: ((n + 1) -BinarySequence k) . i = ((n -BinarySequence k) ^ <*FALSE*>) . i
then  i in Seg (len (n -BinarySequence k)) by CARD_1:def_7;
then A5: i in dom (n -BinarySequence k) by FINSEQ_1:def_3;
thus ((n + 1) -BinarySequence k) . i = ((n + 1) -BinarySequence k) /. i by A3, PARTFUN1:def_6
.= IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A2, Def1
.= (n -BinarySequence k) /. i by A4, Def1
.= (n -BinarySequence k) . i by A5, PARTFUN1:def_6
.= ((n -BinarySequence k) ^ <*FALSE*>) . i by A5, FINSEQ_1:def_7 ; ::_thesis: verum
end;
supposeA6: i = n + 1 ; ::_thesis: ((n + 1) -BinarySequence k) . i = ((n -BinarySequence k) ^ <*FALSE*>) . i
hence ((n + 1) -BinarySequence k) . i = FALSE by A1, Th26
.= ((n -BinarySequence k) ^ <*FALSE*>) . i by A6, FINSEQ_2:116 ;
::_thesis: verum
end;
end;
end;
hence  ((n + 1) -BinarySequence k) . i = ((n -BinarySequence k) ^ <*FALSE*>) . i ; ::_thesis: verum
end;
hence  (n + 1) -BinarySequence k = (n -BinarySequence k) ^ <*FALSE*> by FINSEQ_2:119; ::_thesis: verum
end;

Lm1:  for n being non empty Nat holds (n + 1) -BinarySequence (2 to_power n) = (0* n) ^ <*TRUE*>
proof
let n be non empty Nat; ::_thesis: (n + 1) -BinarySequence (2 to_power n) = (0* n) ^ <*TRUE*>
 0* n in BOOLEAN * by Th4;
then  0* n is FinSequence of BOOLEAN by FINSEQ_1:def_11;
then reconsider 0n = 0* n as Tuple of n, BOOLEAN ;
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(n_+_1)_holds_
((n_+_1)_-BinarySequence_(2_to_power_n))_._i_=_(0n_^_<*TRUE*>)_._i
let i be Nat; ::_thesis: ( i in Seg (n + 1) implies ((n + 1) -BinarySequence (2 to_power n)) . i = (0n ^ <*TRUE*>) . i )
assume A1: i in Seg (n + 1) ; ::_thesis: ((n + 1) -BinarySequence (2 to_power n)) . i = (0n ^ <*TRUE*>) . i
now__::_thesis:_((n_+_1)_-BinarySequence_(2_to_power_n))_._i_=_(0n_^_<*TRUE*>)_._i
percases ( i in Seg n or i = n + 1 ) by A1, FINSEQ_2:7;
supposeA2: i in Seg n ; ::_thesis: ((n + 1) -BinarySequence (2 to_power n)) . i = (0n ^ <*TRUE*>) . i
then A3: i >= 1 by FINSEQ_1:1;
 i <= n + 1 by A1, FINSEQ_1:1;
then  i - 1 <= (n + 1) - 1 by XREAL_1:9;
then A4: i -' 1 <= (n + 1) - 1 by A3, XREAL_1:233;
n = (n - (i -' 1)) + (i -' 1)
.= (n -' (i -' 1)) + (i -' 1) by A4, XREAL_1:233 ;
then A5: 2 to_power n = (2 to_power (n -' (i -' 1))) * (2 to_power (i -' 1)) by POWER:27;
 i in Seg (len 0n) by A2, CARD_1:def_7;
then A6: i in dom 0n by FINSEQ_1:def_3;
 n >= i by A2, FINSEQ_1:1;
then  n + 1 > i by NAT_1:13;
then  n > i - 1 by XREAL_1:19;
then  n - (i - 1) > 0 by XREAL_1:50;
then  n - (i -' 1) > 0 by A3, XREAL_1:233;
then  n -' (i -' 1) > 0 by A4, XREAL_1:233;
then consider n1 being Nat such that
A7: n -' (i -' 1) = n1 + 1 by NAT_1:6;
reconsider n1 = n1 as Nat ;
A8: 2 to_power (n -' (i -' 1)) = (2 to_power n1) * (2 to_power 1) by A7, POWER:27
.= (2 to_power n1) * 2 by POWER:25 ;
 2 to_power (i -' 1) > 0 by POWER:34;
then A9: ((2 to_power n) div (2 to_power (i -' 1))) mod 2 = (2 to_power (n -' (i -' 1))) mod 2 by A5, NAT_D:20
.= 0 by A8, NAT_D:13 ;
 i in Seg (len ((n + 1) -BinarySequence (2 to_power n))) by A1, CARD_1:def_7;
then  i in dom ((n + 1) -BinarySequence (2 to_power n)) by FINSEQ_1:def_3;
hence ((n + 1) -BinarySequence (2 to_power n)) . i = ((n + 1) -BinarySequence (2 to_power n)) /. i by PARTFUN1:def_6
.= IFEQ ((((2 to_power n) div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A1, Def1
.= 0 by A9, FUNCOP_1:def_8
.= 0n . i by A2, FUNCOP_1:7
.= (0n ^ <*TRUE*>) . i by A6, FINSEQ_1:def_7 ;
::_thesis: verum
end;
supposeA10: i = n + 1 ; ::_thesis: ((n + 1) -BinarySequence (2 to_power n)) . i = (0n ^ <*TRUE*>) . i
A11: 2 to_power n > 0 by POWER:34;
i -' 1 = (n + 1) - 1 by A10, NAT_D:37
.= n ;
then A12: ((2 to_power n) div (2 to_power (i -' 1))) mod 2 = 1 mod 2 by A11, NAT_2:3
.= 1 by NAT_D:14 ;
 n + 1 in Seg (n + 1) by FINSEQ_1:4;
then  n + 1 in Seg (len ((n + 1) -BinarySequence (2 to_power n))) by CARD_1:def_7;
then  n + 1 in dom ((n + 1) -BinarySequence (2 to_power n)) by FINSEQ_1:def_3;
hence ((n + 1) -BinarySequence (2 to_power n)) . i = ((n + 1) -BinarySequence (2 to_power n)) /. i by A10, PARTFUN1:def_6
.= IFEQ ((((2 to_power n) div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A1, Def1
.= TRUE by A12, FUNCOP_1:def_8
.= (0n ^ <*TRUE*>) . i by A10, FINSEQ_2:116 ;
::_thesis: verum
end;
end;
end;
hence  ((n + 1) -BinarySequence (2 to_power n)) . i = (0n ^ <*TRUE*>) . i ; ::_thesis: verum
end;
hence  (n + 1) -BinarySequence (2 to_power n) = (0* n) ^ <*TRUE*> by FINSEQ_2:119; ::_thesis: verum
end;

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
proof
let n be non empty Nat; ::_thesis: for k being Nat st 2 to_power n <= k & k < 2 to_power (n + 1) holds
((n + 1) -BinarySequence k) . (n + 1) = TRUE
let k be Nat; ::_thesis: ( 2 to_power n <= k & k < 2 to_power (n + 1) implies ((n + 1) -BinarySequence k) . (n + 1) = TRUE )
assume that
A1: 2 to_power n <= k and
A2: k < 2 to_power (n + 1) ; ::_thesis: ((n + 1) -BinarySequence k) . (n + 1) = TRUE
 k < (2 to_power n) * (2 to_power 1) by A2, POWER:27;
then  k < 2 * (2 to_power n) by POWER:25;
then A3: k < (2 to_power n) + (2 to_power n) ;
(n + 1) -' 1 = (n + 1) - 1 by NAT_D:37
.= n ;
then A4: (k div (2 to_power ((n + 1) -' 1))) mod 2 = 1 mod 2 by A1, A3, NAT_2:20
.= 1 by NAT_D:24 ;
A5: n + 1 in Seg (n + 1) by FINSEQ_1:4;
then  n + 1 in Seg (len ((n + 1) -BinarySequence k)) by CARD_1:def_7;
then  n + 1 in dom ((n + 1) -BinarySequence k) by FINSEQ_1:def_3;
hence ((n + 1) -BinarySequence k) . (n + 1) = ((n + 1) -BinarySequence k) /. (n + 1) by PARTFUN1:def_6
.= IFEQ (((k div (2 to_power ((n + 1) -' 1))) mod 2),0,FALSE,TRUE) by A5, Def1
.= TRUE by A4, FUNCOP_1:def_8 ;
::_thesis: verum
end;

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*>
proof
let n be non empty Nat; ::_thesis: 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*>
let k be Nat; ::_thesis: ( 2 to_power n <= k & k < 2 to_power (n + 1) implies (n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*> )
assume that
A1: 2 to_power n <= k and
A2: k < 2 to_power (n + 1) ; ::_thesis: (n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_(n_+_1)_holds_
((n_+_1)_-BinarySequence_k)_._i_=_((n_-BinarySequence_(k_-'_(2_to_power_n)))_^_<*TRUE*>)_._i
let i be Nat; ::_thesis: ( i in Seg (n + 1) implies ((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . i )
reconsider z = i as Nat ;
assume A3: i in Seg (n + 1) ; ::_thesis: ((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . i
then  i in Seg (len ((n + 1) -BinarySequence k)) by CARD_1:def_7;
then A4: i in dom ((n + 1) -BinarySequence k) by FINSEQ_1:def_3;
now__::_thesis:_((n_+_1)_-BinarySequence_k)_._i_=_((n_-BinarySequence_(k_-'_(2_to_power_n)))_^_<*TRUE*>)_._i
percases ( i in Seg n or i = n + 1 ) by A3, FINSEQ_2:7;
supposeA5: i in Seg n ; ::_thesis: ((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . i
then A6: 1 <= i by FINSEQ_1:1;
A7: 2 * (2 to_power (i -' 1)) = (2 to_power (i -' 1)) * (2 to_power 1) by POWER:25
.= 2 to_power ((i -' 1) + 1) by POWER:27
.= 2 to_power ((i - 1) + 1) by A6, XREAL_1:233
.= 2 to_power i ;
 2 to_power (i -' 1) > 0 by POWER:34;
then A8: 0 + 1 <= 2 to_power (i -' 1) by NAT_1:13;
 i <= n by A5, FINSEQ_1:1;
then A9: 2 * (2 to_power (z -' 1)) divides 2 to_power n by A7, NAT_2:11;
A10: now__::_thesis:_(k_div_(2_to_power_(i_-'_1)))_mod_2_=_((k_-'_(2_to_power_n))_div_(2_to_power_(i_-'_1)))_mod_2
percases ( k div (2 to_power (i -' 1)) is even or k div (2 to_power (i -' 1)) is odd ) ;
supposeA11: k div (2 to_power (i -' 1)) is even ; ::_thesis: (k div (2 to_power (i -' 1))) mod 2 = ((k -' (2 to_power n)) div (2 to_power (i -' 1))) mod 2
then A12: (k div (2 to_power (i -' 1))) mod 2 = 0 by NAT_2:21;
 (k -' (2 to_power n)) div (2 to_power (i -' 1)) is even by A1, A8, A9, A11, NAT_2:23;
hence  (k div (2 to_power (i -' 1))) mod 2 = ((k -' (2 to_power n)) div (2 to_power (i -' 1))) mod 2 by A12, NAT_2:21; ::_thesis: verum
end;
supposeA13: k div (2 to_power (i -' 1)) is odd ; ::_thesis: (k div (2 to_power (i -' 1))) mod 2 = ((k -' (2 to_power n)) div (2 to_power (i -' 1))) mod 2
then A14: (k div (2 to_power (i -' 1))) mod 2 = 1 by NAT_2:22;
 (k -' (2 to_power n)) div (2 to_power (i -' 1)) is odd by A1, A8, A9, A13, NAT_2:23;
hence  (k div (2 to_power (i -' 1))) mod 2 = ((k -' (2 to_power n)) div (2 to_power (i -' 1))) mod 2 by A14, NAT_2:22; ::_thesis: verum
end;
end;
end;
 i in Seg (len (n -BinarySequence (k -' (2 to_power n)))) by A5, CARD_1:def_7;
then A15: i in dom (n -BinarySequence (k -' (2 to_power n))) by FINSEQ_1:def_3;
thus ((n + 1) -BinarySequence k) . i = ((n + 1) -BinarySequence k) /. i by A4, PARTFUN1:def_6
.= IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A3, Def1
.= (n -BinarySequence (k -' (2 to_power n))) /. i by A5, A10, Def1
.= (n -BinarySequence (k -' (2 to_power n))) . i by A15, PARTFUN1:def_6
.= ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . i by A15, FINSEQ_1:def_7 ; ::_thesis: verum
end;
supposeA16: i = n + 1 ; ::_thesis: ((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . i
hence ((n + 1) -BinarySequence k) . i = TRUE by A1, A2, Lm2
.= ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . i by A16, FINSEQ_2:116 ;
::_thesis: verum
end;
end;
end;
hence  ((n + 1) -BinarySequence k) . i = ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) . i ; ::_thesis: verum
end;
hence  (n + 1) -BinarySequence k = (n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*> by FINSEQ_2:119; ::_thesis: verum
end;

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 )
proof
let n be non empty Nat; ::_thesis: 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 )
let k be Nat; ::_thesis: ( k < 2 to_power n implies for x being Tuple of n, BOOLEAN st x = 0* n holds
( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 ) )
assume A1: k < 2 to_power n ; ::_thesis: for x being Tuple of n, BOOLEAN st x = 0* n holds
( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 )
let x be Tuple of n, BOOLEAN ; ::_thesis: ( x = 0* n implies ( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 ) )
assume A2: x = 0* n ; ::_thesis: ( n -BinarySequence k = 'not' x iff k = (2 to_power n) - 1 )
thus  ( n -BinarySequence k = 'not' x implies k = (2 to_power n) - 1 ) ::_thesis: ( k = (2 to_power n) - 1 implies n -BinarySequence k = 'not' x )
proof
defpred S1[ Nat] means  for k being Nat st k < 2 to_power $1 holds
for y being Tuple of $1, BOOLEAN st y = 0* $1 & $1 -BinarySequence k = 'not' y holds
k = (2 to_power $1) - 1;
assume A3: n -BinarySequence k = 'not' x ; ::_thesis: k = (2 to_power n) - 1
A4: for m being non empty Nat st S1[m] holds
S1[m + 1]
proof
let m be non empty Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A5: S1[m] ; ::_thesis: S1[m + 1]
A6: m + 1 in Seg (m + 1) by FINSEQ_1:4;
 0 <= m by NAT_1:2;
then A7: 0 + 1 <= m + 1 by XREAL_1:6;
 0* m in BOOLEAN * by Th4;
then  0* m is FinSequence of BOOLEAN by FINSEQ_1:def_11;
then reconsider y1 = 0* m as Tuple of m, BOOLEAN ;
let k be Nat; ::_thesis: ( k < 2 to_power (m + 1) implies for y being Tuple of m + 1, BOOLEAN st y = 0* (m + 1) & (m + 1) -BinarySequence k = 'not' y holds
k = (2 to_power (m + 1)) - 1 )
assume A8: k < 2 to_power (m + 1) ; ::_thesis: for y being Tuple of m + 1, BOOLEAN st y = 0* (m + 1) & (m + 1) -BinarySequence k = 'not' y holds
k = (2 to_power (m + 1)) - 1
let y be Tuple of m + 1, BOOLEAN ; ::_thesis: ( y = 0* (m + 1) & (m + 1) -BinarySequence k = 'not' y implies k = (2 to_power (m + 1)) - 1 )
assume that
A9: y = 0* (m + 1) and
A10: (m + 1) -BinarySequence k = 'not' y ; ::_thesis: k = (2 to_power (m + 1)) - 1
A11: y . (m + 1) = FALSE by A9, FINSEQ_1:4, FUNCOP_1:7;
A12: y = y1 ^ <*0*> by A9, FINSEQ_2:60;
A13: len y = m + 1 by CARD_1:def_7;
 len ('not' y) = m + 1 by CARD_1:def_7;
then A14: ((m + 1) -BinarySequence k) . (m + 1) = ('not' y) /. (m + 1) by A10, A7, FINSEQ_4:15
.= 'not' (y /. (m + 1)) by A6, BINARITH:def_1
.= 'not' FALSE by A13, A7, A11, FINSEQ_4:15
.= TRUE ;
then  (m + 1) -BinarySequence k = (m -BinarySequence (k -' (2 to_power m))) ^ <*TRUE*> by A8, Lm3, Th26;
then  (m -BinarySequence (k -' (2 to_power m))) ^ <*TRUE*> = ('not' y1) ^ <*('not' FALSE)*> by A10, A12, BINARI_2:9;
then A15: m -BinarySequence (k -' (2 to_power m)) = 'not' y1 by FINSEQ_2:17;
 k < (2 to_power m) * (2 to_power 1) by A8, POWER:27;
then  k < 2 * (2 to_power m) by POWER:25;
then  k < (2 to_power m) + (2 to_power m) ;
then  k - (2 to_power m) < 2 to_power m by XREAL_1:19;
then  k -' (2 to_power m) < 2 to_power m by A14, Th26, XREAL_1:233;
then  k -' (2 to_power m) = (2 to_power m) - 1 by A5, A15;
then  k - (2 to_power m) = (2 to_power m) - 1 by A14, Th26, XREAL_1:233;
hence k = ((2 to_power m) * 2) - 1
.= ((2 to_power m) * (2 to_power 1)) - 1 by POWER:25
.= (2 to_power (m + 1)) - 1 by POWER:27 ;
::_thesis: verum
end;
A16: S1[1]
proof
let k be Nat; ::_thesis: ( k < 2 to_power 1 implies for y being Tuple of 1, BOOLEAN st y = 0* 1 & 1 -BinarySequence k = 'not' y holds
k = (2 to_power 1) - 1 )
A17: 1 <= len (1 -BinarySequence k) by CARD_1:def_7;
assume  k < 2 to_power 1 ; ::_thesis: for y being Tuple of 1, BOOLEAN st y = 0* 1 & 1 -BinarySequence k = 'not' y holds
k = (2 to_power 1) - 1
then A18: k < 2 by POWER:25;
let y be Tuple of 1, BOOLEAN ; ::_thesis: ( y = 0* 1 & 1 -BinarySequence k = 'not' y implies k = (2 to_power 1) - 1 )
assume  y = 0* 1 ; ::_thesis: ( not 1 -BinarySequence k = 'not' y or k = (2 to_power 1) - 1 )
then A19: y = <*FALSE*> by FINSEQ_2:59;
assume A20: 1 -BinarySequence k = 'not' y ; ::_thesis: k = (2 to_power 1) - 1
A21: 1 in Seg 1 by FINSEQ_1:3;
A22: 1 = <*1*> . 1 by FINSEQ_1:40
.= (1 -BinarySequence k) /. 1 by A19, A20, A17, Th14, FINSEQ_4:15
.= IFEQ (((k div (2 to_power (1 -' 1))) mod 2),0,FALSE,TRUE) by A21, Def1 ;
 k = 1
proof
assume  k <> 1 ; ::_thesis: contradiction
then  k = 0 by A18, NAT_1:23;
then  k div (2 to_power (1 -' 1)) = 0 by NAT_D:27, POWER:34;
then  (k div (2 to_power (1 -' 1))) mod 2 = 0 by NAT_D:26;
hence  contradiction by A22, FUNCOP_1:def_8; ::_thesis: verum
end;
hence k = (1 + 1) - 1
.= (2 to_power 1) - 1 by POWER:25 ;
::_thesis: verum
end;
 for m being non empty Nat holds S1[m] from NAT_1:sch_10(A16, A4);
hence  k = (2 to_power n) - 1 by A1, A2, A3; ::_thesis: verum
end;
assume A23: k = (2 to_power n) - 1 ; ::_thesis: n -BinarySequence k = 'not' x
now__::_thesis:_for_i_being_Nat_st_i_in_Seg_n_holds_
(n_-BinarySequence_k)_._i_=_('not'_x)_._i
let i be Nat; ::_thesis: ( i in Seg n implies (n -BinarySequence k) . i = ('not' x) . i )
A24: len x = n by CARD_1:def_7;
 2 to_power (i -' 1) > 0 by POWER:34;
then A25: 2 to_power (i -' 1) >= 0 + 1 by NAT_1:13;
A26: len ('not' x) = n by CARD_1:def_7;
A27: 2 to_power (n -' (i -' 1)) > 0 by POWER:34;
then A28: 2 to_power (n -' (i -' 1)) >= 0 + 1 by NAT_1:13;
reconsider z = i as Nat ;
assume A29: i in Seg n ; ::_thesis: (n -BinarySequence k) . i = ('not' x) . i
then A30: 1 <= i by FINSEQ_1:1;
 i <= n by A29, FINSEQ_1:1;
then  i < n + 1 by NAT_1:13;
then A31: i - 1 < (n + 1) - 1 by XREAL_1:9;
 1 <= i by A29, FINSEQ_1:1;
then A32: 0 + (i -' 1) < n by A31, XREAL_1:233;
then  n - (i -' 1) > 0 by XREAL_1:20;
then  n -' (i -' 1) > 0 by A32, XREAL_1:233;
then A33: (2 to_power (n -' (i -' 1))) mod 2 = 0 by NAT_2:17;
 2 to_power n > 0 by POWER:34;
then A34: 2 to_power n >= 0 + 1 by NAT_1:13;
then k div (2 to_power (i -' 1)) = ((2 to_power n) -' 1) div (2 to_power (i -' 1)) by A23, XREAL_1:233
.= ((2 to_power n) div (2 to_power (i -' 1))) - 1 by A25, A32, A34, NAT_2:11, NAT_2:15
.= (2 to_power (n -' (i -' 1))) - 1 by A32, NAT_2:16
.= (2 to_power (n -' (i -' 1))) -' 1 by A28, XREAL_1:233 ;
then A35: (k div (2 to_power (i -' 1))) mod 2 = 1 by A33, A27, NAT_2:18;
A36: x . i = FALSE by A2, A29, FUNCOP_1:7;
A37: i <= n by A29, FINSEQ_1:1;
 i in Seg (len (n -BinarySequence k)) by A29, CARD_1:def_7;
then  i in dom (n -BinarySequence k) by FINSEQ_1:def_3;
hence (n -BinarySequence k) . i = (n -BinarySequence k) /. i by PARTFUN1:def_6
.= IFEQ (((k div (2 to_power (i -' 1))) mod 2),0,FALSE,TRUE) by A29, Def1
.= 'not' FALSE by A35, FUNCOP_1:def_8
.= 'not' (x /. z) by A24, A30, A37, A36, FINSEQ_4:15
.= ('not' x) /. z by A29, BINARITH:def_1
.= ('not' x) . i by A26, A30, A37, FINSEQ_4:15 ;
::_thesis: verum
end;
hence  n -BinarySequence k = 'not' x by FINSEQ_2:119; ::_thesis: verum
end;

theorem Th28: :: BINARI_3:28
for i being Nat holds (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*>
proof
deffunc H1( Nat) ->  Tuple of $1 + 1, BOOLEAN = ($1 + 1) -BinarySequence (2 to_power $1);
let i be Nat; ::_thesis: (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*>
set Bi = H1(i);
percases ( i = 0 or i > 0 ) by NAT_1:3;
supposeA1: i = 0 ; ::_thesis: (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*>
then A2: 0* i = 0 ;
reconsider i1 = i + 1 as non empty Nat ;
A3: 0* i1 = <*FALSE*> by A1, FINSEQ_2:59;
then reconsider x = 0* i1 as Tuple of i1, BOOLEAN ;
 2 to_power i1 = 2 by A1, POWER:25;
then  1 = (2 to_power i1) - 1 ;
then  i1 -BinarySequence 1 = 'not' x by Lm4;
hence H1(i) = <*TRUE*> by A1, A3, Th14, POWER:24
.= (0* i) ^ <*1*> by A2, FINSEQ_1:34 ;
::_thesis: verum
end;
suppose i > 0 ; ::_thesis: (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*>
then reconsider i9 = i as non empty Nat ;
 H1(i) = (0* i9) ^ <*1*> by Lm1;
hence  (i + 1) -BinarySequence (2 to_power i) = (0* i) ^ <*1*> ; ::_thesis: verum
end;
end;
end;

theorem :: BINARI_3:29
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 by Lm2;

theorem :: BINARI_3:30
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*> by Lm3;

theorem :: BINARI_3:31
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 ) by Lm4;

theorem Th32: :: BINARI_3:32
for n being non empty Nat
for k being Nat st k + 1 < 2 to_power n holds
add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE
proof
let n be non empty Nat; ::_thesis: for k being Nat st k + 1 < 2 to_power n holds
add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE
let k be Nat; ::_thesis: ( k + 1 < 2 to_power n implies add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE )
assume A1: k + 1 < 2 to_power n ; ::_thesis: add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE
then A2: k < 2 to_power n by NAT_1:13;
 0* n in BOOLEAN * by Th4;
then  0* n is FinSequence of BOOLEAN by FINSEQ_1:def_11;
then reconsider y = 0* n as Tuple of n, BOOLEAN ;
 k < (2 to_power n) - 1 by A1, XREAL_1:20;
then  n -BinarySequence k <> 'not' y by A2, Lm4;
then  add_ovfl ((n -BinarySequence k),(Bin1 n)) <> TRUE by Th23;
hence  add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE by XBOOLEAN:def_3; ::_thesis: verum
end;

theorem Th33: :: BINARI_3:33
for n being non empty Nat
for k being Nat st k + 1 < 2 to_power n holds
n -BinarySequence (k + 1) = (n -BinarySequence k) + (Bin1 n)
proof
defpred S1[ non empty Nat] means  for k being Nat st k + 1 < 2 to_power $1 holds
$1 -BinarySequence (k + 1) = ($1 -BinarySequence k) + (Bin1 $1);
A1: for n being non empty Nat st S1[n] holds
S1[n + 1]
proof
let n be non empty Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let k be Nat; ::_thesis: ( k + 1 < 2 to_power (n + 1) implies (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) )
assume A3: k + 1 < 2 to_power (n + 1) ; ::_thesis: (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1))
then A4: k < 2 to_power (n + 1) by NAT_1:13;
now__::_thesis:_(n_+_1)_-BinarySequence_(k_+_1)_=_((n_+_1)_-BinarySequence_k)_+_(Bin1_(n_+_1))
percases ( k + 1 < 2 to_power n or k + 1 > 2 to_power n or k + 1 = 2 to_power n ) by XXREAL_0:1;
supposeA5: k + 1 < 2 to_power n ; ::_thesis: (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1))
then A6: k < 2 to_power n by NAT_1:13;
A7: add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE by A5, Th32;
thus (n + 1) -BinarySequence (k + 1) = (n -BinarySequence (k + 1)) ^ <*FALSE*> by A5, Th27
.= ((n -BinarySequence k) + (Bin1 n)) ^ <*((FALSE 'xor' FALSE) 'xor' (add_ovfl ((n -BinarySequence k),(Bin1 n))))*> by A2, A5, A7
.= ((n -BinarySequence k) ^ <*FALSE*>) + ((Bin1 n) ^ <*FALSE*>) by BINARITH:19
.= ((n -BinarySequence k) ^ <*FALSE*>) + (Bin1 (n + 1)) by BINARI_2:7
.= ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) by A6, Th27 ; ::_thesis: verum
end;
supposeA8: k + 1 > 2 to_power n ; ::_thesis: (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1))
then A9: k >= 2 to_power n by NAT_1:13;
 k + 1 < (2 to_power n) * (2 to_power 1) by A3, POWER:27;
then  k + 1 < (2 to_power n) * 2 by POWER:25;
then  k + 1 < (2 to_power n) + (2 to_power n) ;
then  (k + 1) - (2 to_power n) < 2 to_power n by XREAL_1:19;
then  (k - (2 to_power n)) + 1 < 2 to_power n ;
then A10: (k -' (2 to_power n)) + 1 < 2 to_power n by A9, XREAL_1:233;
then A11: add_ovfl ((n -BinarySequence (k -' (2 to_power n))),(Bin1 n)) = FALSE by Th32;
thus (n + 1) -BinarySequence (k + 1) = (n -BinarySequence ((k + 1) -' (2 to_power n))) ^ <*TRUE*> by A3, A8, Lm3
.= (n -BinarySequence ((k -' (2 to_power n)) + 1)) ^ <*TRUE*> by A9, NAT_D:38
.= ((n -BinarySequence (k -' (2 to_power n))) + (Bin1 n)) ^ <*((TRUE 'xor' FALSE) 'xor' (add_ovfl ((n -BinarySequence (k -' (2 to_power n))),(Bin1 n))))*> by A2, A10, A11
.= ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) + ((Bin1 n) ^ <*FALSE*>) by BINARITH:19
.= ((n -BinarySequence (k -' (2 to_power n))) ^ <*TRUE*>) + (Bin1 (n + 1)) by BINARI_2:7
.= ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) by A4, A9, Lm3 ; ::_thesis: verum
end;
supposeA12: k + 1 = 2 to_power n ; ::_thesis: (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1))
 0* n in BOOLEAN * by Th4;
then  0* n is FinSequence of BOOLEAN by FINSEQ_1:def_11;
then reconsider z = 0* n as Tuple of n, BOOLEAN ;
A13: k < 2 to_power n by A12, NAT_1:13;
 k = (2 to_power n) - 1 by A12;
then A14: n -BinarySequence k = 'not' z by A13, Lm4;
thus (n + 1) -BinarySequence (k + 1) = (0* n) ^ <*1*> by A12, Th28
.= (('not' z) + (Bin1 n)) ^ <*TRUE*> by Th24
.= ((n -BinarySequence k) + (Bin1 n)) ^ <*((FALSE 'xor' FALSE) 'xor' (add_ovfl ((n -BinarySequence k),(Bin1 n))))*> by A14, Th23
.= ((n -BinarySequence k) ^ <*FALSE*>) + ((Bin1 n) ^ <*FALSE*>) by BINARITH:19
.= ((n -BinarySequence k) ^ <*FALSE*>) + (Bin1 (n + 1)) by BINARI_2:7
.= ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) by A13, Th27 ; ::_thesis: verum
end;
end;
end;
hence  (n + 1) -BinarySequence (k + 1) = ((n + 1) -BinarySequence k) + (Bin1 (n + 1)) ; ::_thesis: verum
end;
A15: S1[1]
proof
 0* 1 in BOOLEAN * by Th4;
then  0* 1 is FinSequence of BOOLEAN by FINSEQ_1:def_11;
then reconsider x = 0* 1 as Tuple of 1, BOOLEAN ;
let k be Nat; ::_thesis: ( k + 1 < 2 to_power 1 implies 1 -BinarySequence (k + 1) = (1 -BinarySequence k) + (Bin1 1) )
A16: 0* 1 = <*FALSE*> by FINSEQ_2:59;
assume A17: k + 1 < 2 to_power 1 ; ::_thesis: 1 -BinarySequence (k + 1) = (1 -BinarySequence k) + (Bin1 1)
then  k + 1 < 1 + 1 by POWER:25;
then  k < 1 by XREAL_1:6;
then A18: k = 0 by NAT_1:14;
then k + 1 = 2 - 1
.= (2 to_power 1) - 1 by POWER:25 ;
hence 1 -BinarySequence (k + 1) = 'not' x by A17, Lm4
.= (1 -BinarySequence k) + (Bin1 1) by A18, A16, Th10, Th14, Th17, Th25 ;
::_thesis: verum
end;
thus  for n being non empty Nat holds S1[n] from NAT_1:sch_10(A15, A1); ::_thesis: verum
end;

theorem :: BINARI_3:34
for n, i being Nat holds (n + 1) -BinarySequence i = <*(i mod 2)*> ^ (n -BinarySequence (i div 2))
proof
let n, i be Nat; ::_thesis: (n + 1) -BinarySequence i = <*(i mod 2)*> ^ (n -BinarySequence (i div 2))
A1: len ((n + 1) -BinarySequence i) = n + 1 by CARD_1:def_7;
then A2: dom ((n + 1) -BinarySequence i) = Seg (n + 1) by FINSEQ_1:def_3;
A3: len (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) = 1 + (len (n -BinarySequence (i div 2))) by FINSEQ_5:8
.= n + 1 by CARD_1:def_7 ;
now__::_thesis:_for_j_being_Nat_st_j_in_dom_((n_+_1)_-BinarySequence_i)_holds_
((n_+_1)_-BinarySequence_i)_._j_=_(<*(i_mod_2)*>_^_(n_-BinarySequence_(i_div_2)))_._j
let j be Nat; ::_thesis: ( j in dom ((n + 1) -BinarySequence i) implies ((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j )
reconsider z = j as Nat ;
assume A4: j in dom ((n + 1) -BinarySequence i) ; ::_thesis: ((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j
then A5: 1 <= j by A2, FINSEQ_1:1;
A6: j <= n + 1 by A2, A4, FINSEQ_1:1;
A7: len <*(i mod 2)*> = 1 by FINSEQ_1:39;
now__::_thesis:_((n_+_1)_-BinarySequence_i)_._j_=_(<*(i_mod_2)*>_^_(n_-BinarySequence_(i_div_2)))_._j
percases ( j > 1 or j = 1 ) by A5, XXREAL_0:1;
supposeA8: j > 1 ; ::_thesis: ((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j
A9: 2 to_power (((j -' 1) -' 1) + 1) = (2 to_power ((j -' 1) -' 1)) * (2 to_power 1) by POWER:27
.= 2 * (2 to_power ((j -' 1) -' 1)) by POWER:25 ;
 j - 1 > 1 - 1 by A8, XREAL_1:9;
then  j -' 1 > 0 by A5, XREAL_1:233;
then A10: j -' 1 >= 0 + 1 by NAT_1:13;
then A11: i div (2 to_power (j -' 1)) = i div (2 to_power (((j -' 1) -' 1) + 1)) by XREAL_1:235
.= (i div 2) div (2 to_power ((j -' 1) -' 1)) by A9, NAT_2:27 ;
 j - 1 <= n by A6, XREAL_1:20;
then A12: j -' 1 <= n by A5, XREAL_1:233;
then A13: j -' 1 <= len (n -BinarySequence (i div 2)) by CARD_1:def_7;
A14: j -' 1 in Seg n by A10, A12, FINSEQ_1:1;
 j <= len ((n + 1) -BinarySequence i) by A6, CARD_1:def_7;
hence ((n + 1) -BinarySequence i) . j = ((n + 1) -BinarySequence i) /. z by A5, FINSEQ_4:15
.= IFEQ (((i div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A2, A4, Def1
.= (n -BinarySequence (i div 2)) /. (j -' 1) by A14, A11, Def1
.= (n -BinarySequence (i div 2)) . (j -' 1) by A10, A13, FINSEQ_4:15
.= (n -BinarySequence (i div 2)) . (j - 1) by A5, XREAL_1:233
.= (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j by A3, A6, A7, A8, FINSEQ_1:24 ;
::_thesis: verum
end;
supposeA15: j = 1 ; ::_thesis: ((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j
A16: now__::_thesis:_IFEQ_((i_mod_2),0,FALSE,TRUE)_=_i_mod_2
percases ( i mod 2 = 0 or i mod 2 <> 0 ) ;
suppose i mod 2 = 0 ; ::_thesis: IFEQ ((i mod 2),0,FALSE,TRUE) = i mod 2
hence  IFEQ ((i mod 2),0,FALSE,TRUE) = i mod 2 by FUNCOP_1:def_8; ::_thesis: verum
end;
supposeA17: i mod 2 <> 0 ; ::_thesis: IFEQ ((i mod 2),0,FALSE,TRUE) = i mod 2
hence  IFEQ ((i mod 2),0,FALSE,TRUE) = 1 by FUNCOP_1:def_8
.= i mod 2 by A17, NAT_D:12 ;
::_thesis: verum
end;
end;
end;
A18: 2 to_power 0 = 1 by POWER:24;
thus ((n + 1) -BinarySequence i) . j = ((n + 1) -BinarySequence i) /. z by A1, A5, A6, FINSEQ_4:15
.= IFEQ (((i div (2 to_power (1 -' 1))) mod 2),0,FALSE,TRUE) by A2, A4, A15, Def1
.= IFEQ (((i div 1) mod 2),0,FALSE,TRUE) by A18, XREAL_1:232
.= IFEQ ((i mod 2),0,FALSE,TRUE) by NAT_2:4
.= (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j by A15, A16, FINSEQ_1:41 ; ::_thesis: verum
end;
end;
end;
hence  ((n + 1) -BinarySequence i) . j = (<*(i mod 2)*> ^ (n -BinarySequence (i div 2))) . j ; ::_thesis: verum
end;
hence  (n + 1) -BinarySequence i = <*(i mod 2)*> ^ (n -BinarySequence (i div 2)) by A1, A3, FINSEQ_2:9; ::_thesis: verum
end;

theorem Th35: :: BINARI_3:35
for n being non empty Nat
for k being Nat st k < 2 to_power n holds
Absval (n -BinarySequence k) = k
proof
let n be non empty Nat; ::_thesis: for k being Nat st k < 2 to_power n holds
Absval (n -BinarySequence k) = k
defpred S1[ Nat] means ( $1 < 2 to_power n implies Absval (n -BinarySequence $1) = $1 );
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
 0* n in BOOLEAN * by Th4;
then  0* n is FinSequence of BOOLEAN by FINSEQ_1:def_11;
then reconsider 0n = 0* n as Tuple of n, BOOLEAN ;
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: ( k < 2 to_power n implies Absval (n -BinarySequence k) = k ) ; ::_thesis: S1[k + 1]
assume A3: k + 1 < 2 to_power n ; ::_thesis: Absval (n -BinarySequence (k + 1)) = k + 1
then A4: (k + 1) - 1 < (2 to_power n) - 1 by XREAL_1:9;
 k < 2 to_power n by A3, NAT_1:13;
then  n -BinarySequence k <> 'not' 0n by A4, Lm4;
then  add_ovfl ((n -BinarySequence k),(Bin1 n)) <> TRUE by Th23;
then  add_ovfl ((n -BinarySequence k),(Bin1 n)) = FALSE by XBOOLEAN:def_3;
then A5: n -BinarySequence k, Bin1 n are_summable by BINARITH:def_7;
thus  Absval (n -BinarySequence (k + 1)) = Absval ((n -BinarySequence k) + (Bin1 n)) by A3, Th33
.= (Absval (n -BinarySequence k)) + (Absval (Bin1 n)) by A5, BINARITH:22
.= k + 1 by A2, A3, Th11, NAT_1:13 ; ::_thesis: verum
end;
A6: S1[ 0 ]
proof
assume  0 < 2 to_power n ; ::_thesis: Absval (n -BinarySequence 0) = 0
 n -BinarySequence 0 = 0* n by Th25;
hence  Absval (n -BinarySequence 0) = 0 by Th6; ::_thesis: verum
end;
thus  for n being Nat holds S1[n] from NAT_1:sch_2(A6, A1); ::_thesis: verum
end;

theorem :: BINARI_3:36
for n being non empty Nat
for x being Tuple of n, BOOLEAN holds n -BinarySequence (Absval x) = x
proof
let n be non empty Nat; ::_thesis: for x being Tuple of n, BOOLEAN holds n -BinarySequence (Absval x) = x
let x be Tuple of n, BOOLEAN ; ::_thesis: n -BinarySequence (Absval x) = x
 Absval x < 2 to_power n by Th1;
then  Absval (n -BinarySequence (Absval x)) = Absval x by Th35;
hence  n -BinarySequence (Absval x) = x by Th2; ::_thesis: verum
end;