:: BINARI_4 semantic presentation

begin


theorem Th1: :: BINARI_4:1
for m being Nat st m > 0 holds
m * 2 >= m + 1
proof
let m be Nat; ::_thesis: ( m > 0 implies m * 2 >= m + 1 )
assume  m > 0 ; ::_thesis: m * 2 >= m + 1
then A1: m >= 0 + 1 by INT_1:7;
 m * 2 = m + m ;
hence  m * 2 >= m + 1 by A1, XREAL_1:6; ::_thesis: verum
end;

theorem Th2: :: BINARI_4:2
for m being Nat holds 2 to_power m >= m
proof
defpred S1[ Nat] means 2 to_power $1 >= $1;
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: 2 to_power m >= m ; ::_thesis: S1[m + 1]
percases ( m = 0 or m > 0 ) ;
supposeA3: m = 0 ; ::_thesis: S1[m + 1]
then  2 to_power (m + 1) = 2 by POWER:25;
hence  S1[m + 1] by A3; ::_thesis: verum
end;
supposeA4: m > 0 ; ::_thesis: S1[m + 1]
reconsider m2 = 2 to_power m as Nat ;
 ( m2 * 2 >= m * 2 & 2 to_power 1 = 2 ) by A2, NAT_1:4, POWER:25;
then A5: 2 to_power (m + 1) >= m * 2 by POWER:27;
 m * 2 >= m + 1 by A4, Th1;
hence  S1[m + 1] by A5, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
A6: S1[ 0 ] ;
thus  for m being Nat holds S1[m] from NAT_1:sch_2(A6, A1); ::_thesis: verum
end;

theorem :: BINARI_4:3
for m being Nat holds (0* m) + (0* m) = 0* m
proof
let m be Nat; ::_thesis: (0* m) + (0* m) = 0* m
A1: dom (0* m) = Seg m by FUNCOP_1:13;
 ( dom addreal = [:REAL,REAL:] & rng (0* m) c= REAL ) by FINSEQ_1:def_4, FUNCT_2:def_1;
then A2: [:(rng (0* m)),(rng (0* m)):] c= dom addreal by ZFMISC_1:96;
A3: dom ((0* m) + (0* m)) = dom (addreal .: ((0* m),(0* m))) by RVSUM_1:def_4
.= (dom (0* m)) /\ (dom (0* m)) by A2, FUNCOP_1:69
.= Seg m by FUNCOP_1:13 ;
 for k being Nat st k in dom (0* m) holds
(0* m) . k = ((0* m) + (0* m)) . k
proof
let k be Nat; ::_thesis: ( k in dom (0* m) implies (0* m) . k = ((0* m) + (0* m)) . k )
assume A4: k in dom (0* m) ; ::_thesis: (0* m) . k = ((0* m) + (0* m)) . k
 (0* m) . k = 0 ;
then  ((0* m) + (0* m)) . k = 0 + 0 by A3, A1, A4, VALUED_1:def_1;
hence  (0* m) . k = ((0* m) + (0* m)) . k ; ::_thesis: verum
end;
hence  (0* m) + (0* m) = 0* m by A3, FINSEQ_1:13, FUNCOP_1:13; ::_thesis: verum
end;

theorem Th4: :: BINARI_4:4
for k, m, l being Nat st k <= l & l <= m & not k = l holds
( k + 1 <= l & l <= m )
proof
defpred S1[ Nat] means  for m, l being Nat st $1 <= l & l <= m & not $1 = l holds
( $1 + 1 <= l & l <= m );
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  S1[k] ; ::_thesis: S1[k + 1]
let m, l be Nat; ::_thesis: ( k + 1 <= l & l <= m & not k + 1 = l implies ( (k + 1) + 1 <= l & l <= m ) )
assume that
A2: k + 1 <= l and
A3: l <= m ; ::_thesis: ( k + 1 = l or ( (k + 1) + 1 <= l & l <= m ) )
 ( k + 1 = l or k + 1 < l ) by A2, XXREAL_0:1;
hence  ( k + 1 = l or ( (k + 1) + 1 <= l & l <= m ) ) by A3, NAT_1:13; ::_thesis: verum
end;
A4: S1[ 0 ] by NAT_1:13;
thus  for k being Nat holds S1[k] from NAT_1:sch_2(A4, A1); ::_thesis: verum
end;

theorem Th5: :: BINARI_4:5
for n being non empty Nat
for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds
carry (x,y) = 0* n
proof
let n be non empty Nat; ::_thesis: for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds
carry (x,y) = 0* n
let x, y be Tuple of n, BOOLEAN ; ::_thesis: ( x = 0* n & y = 0* n implies carry (x,y) = 0* n )
assume that
A1: x = 0* n and
A2: y = 0* n ; ::_thesis: carry (x,y) = 0* n
A3: for j being Nat st 1 < j & j <= n holds
(carry (x,y)) . j = 0
proof
let j be Nat; ::_thesis: ( 1 < j & j <= n implies (carry (x,y)) . j = 0 )
assume that
A4: 1 < j and
A5: j <= n ; ::_thesis: (carry (x,y)) . j = 0
reconsider k = j - 1 as Element of NAT by A4, INT_1:5;
 k + 1 = j ;
then A6: ( 1 <= k & k < n ) by A4, A5, NAT_1:13;
 len (0* n) = n by CARD_1:def_7;
then A7: x /. k = (0* n) . k by A1, A6, FINSEQ_4:15
.= FALSE ;
A8: j = k + 1 ;
 len (carry (x,y)) = n by CARD_1:def_7;
then (carry (x,y)) . j = (carry (x,y)) /. j by A4, A5, FINSEQ_4:15
.= ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (x,y)) /. k))) 'or' (FALSE '&' ((carry (x,y)) /. k)) by A1, A2, A6, A8, A7, BINARITH:def_2
.= FALSE ;
hence  (carry (x,y)) . j = 0 ; ::_thesis: verum
end;
 len (carry (x,y)) = n by CARD_1:def_7;
then  1 <= len (carry (x,y)) by NAT_1:14;
then A9: (carry (x,y)) . 1 = (carry (x,y)) /. 1 by FINSEQ_4:15
.= 0 by BINARITH:def_2 ;
 for l being Nat st l in Seg n holds
(carry (x,y)) . l = (0* n) . l
proof
let l be Nat; ::_thesis: ( l in Seg n implies (carry (x,y)) . l = (0* n) . l )
assume A10: l in Seg n ; ::_thesis: (carry (x,y)) . l = (0* n) . l
A11: 1 <= l by A10, FINSEQ_1:1;
A12: (0* n) . l = 0 ;
percases ( l = 1 or ( 1 + 1 <= l & l <= n ) ) by A10, A11, Th4, FINSEQ_1:1;
suppose l = 1 ; ::_thesis: (carry (x,y)) . l = (0* n) . l
hence  (carry (x,y)) . l = (0* n) . l by A9; ::_thesis: verum
end;
supposeA13: ( 1 + 1 <= l & l <= n ) ; ::_thesis: (carry (x,y)) . l = (0* n) . l
then  1 < l by NAT_1:13;
hence  (carry (x,y)) . l = (0* n) . l by A3, A12, A13; ::_thesis: verum
end;
end;
end;
hence  carry (x,y) = 0* n by A1, FINSEQ_2:119; ::_thesis: verum
end;

theorem :: BINARI_4:6
for n being non empty Nat
for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds
x + y = 0* n
proof
let n be non empty Nat; ::_thesis: for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds
x + y = 0* n
let x, y be Tuple of n, BOOLEAN ; ::_thesis: ( x = 0* n & y = 0* n implies x + y = 0* n )
assume that
A1: x = 0* n and
A2: y = 0* n ; ::_thesis: x + y = 0* n
 for k being Nat st k in Seg n holds
(x + y) . k = (0* n) . k
proof
let k be Nat; ::_thesis: ( k in Seg n implies (x + y) . k = (0* n) . k )
assume A3: k in Seg n ; ::_thesis: (x + y) . k = (0* n) . k
reconsider k = k as Nat ;
A4: (0* n) . k = FALSE ;
A5: 1 <= k by A3, FINSEQ_1:1;
 len x = n by CARD_1:def_7;
then  k <= len x by A3, FINSEQ_1:1;
then A6: y /. k = FALSE by A1, A2, A4, A5, FINSEQ_4:15;
 len (carry (x,y)) = n by CARD_1:def_7;
then  k <= len (carry (x,y)) by A3, FINSEQ_1:1;
then A7: (carry (x,y)) /. k = (carry (x,y)) . k by A5, FINSEQ_4:15
.= FALSE by A1, A2, A4, Th5 ;
 len (x + y) = n by CARD_1:def_7;
then  k <= len (x + y) by A3, FINSEQ_1:1;
then (x + y) . k = (x + y) /. k by A5, FINSEQ_4:15
.= FALSE 'xor' FALSE by A1, A2, A3, A6, A7, BINARITH:def_5
.= FALSE ;
hence  (x + y) . k = (0* n) . k ; ::_thesis: verum
end;
hence  x + y = 0* n by A1, FINSEQ_2:119; ::_thesis: verum
end;

theorem :: BINARI_4:7
for n being non empty Nat
for F being Tuple of n, BOOLEAN st F = 0* n holds
Intval F = 0
proof
let n be non empty Nat; ::_thesis: for F being Tuple of n, BOOLEAN st F = 0* n holds
Intval F = 0
let F be Tuple of n, BOOLEAN ; ::_thesis: ( F = 0* n implies Intval F = 0 )
assume A1: F = 0* n ; ::_thesis: Intval F = 0
A2: 1 <= n by NAT_1:14;
 n <= len F by CARD_1:def_7;
then F /. n = F . n by A2, FINSEQ_4:15
.= FALSE by A1 ;
then  Intval F = Absval F by BINARI_2:def_3;
hence  Intval F = 0 by A1, BINARI_3:6; ::_thesis: verum
end;

theorem Th8: :: BINARI_4:8
for l, m, k being Nat st l + m <= k - 1 holds
( l < k & m < k )
proof
let l, m, k be Nat; ::_thesis: ( l + m <= k - 1 implies ( l < k & m < k ) )
assume A1: l + m <= k - 1 ; ::_thesis: ( l < k & m < k )
then A2: (l + m) - m <= (k - 1) - m by XREAL_1:9;
 k <= k + m by NAT_1:11;
then A3: k - m <= (k + m) - m by XREAL_1:9;
 (k - 1) - m = (k - m) - 1 ;
then  (k - 1) - m < k by A3, XREAL_1:146, XXREAL_0:2;
hence  l < k by A2, XXREAL_0:2; ::_thesis: m < k
 k <= k + l by NAT_1:11;
then A4: k - l <= (k + l) - l by XREAL_1:9;
A5: (m + l) - l <= (k - 1) - l by A1, XREAL_1:9;
 (k - 1) - l = (k - l) - 1 ;
then  (k - 1) - l < k by A4, XREAL_1:146, XXREAL_0:2;
hence  m < k by A5, XXREAL_0:2; ::_thesis: verum
end;

theorem Th9: :: BINARI_4:9
for g, h, i being Integer st g <= h + i & h < 0 & i < 0 holds
( g < h & g < i )
proof
let g, h, i be Integer; ::_thesis: ( g <= h + i & h < 0 & i < 0 implies ( g < h & g < i ) )
assume that
A1: g <= h + i and
A2: h < 0 and
A3: i < 0 ; ::_thesis: ( g < h & g < i )
 g - i <= (h + i) - i by A1, XREAL_1:9;
then  i + (g + (- i)) < 0 + h by A3, XREAL_1:8;
hence  g < h ; ::_thesis: g < i
 g - h <= (i + h) - h by A1, XREAL_1:9;
then  h + (g + (- h)) < 0 + i by A2, XREAL_1:8;
hence  g < i ; ::_thesis: verum
end;

theorem Th10: :: BINARI_4:10
for n being non empty Nat
for l, m being Nat st l + m <= (2 to_power n) - 1 holds
add_ovfl ((n -BinarySequence l),(n -BinarySequence m)) = FALSE
proof
let n be non empty Nat; ::_thesis: for l, m being Nat st l + m <= (2 to_power n) - 1 holds
add_ovfl ((n -BinarySequence l),(n -BinarySequence m)) = FALSE
let l, m be Nat; ::_thesis: ( l + m <= (2 to_power n) - 1 implies add_ovfl ((n -BinarySequence l),(n -BinarySequence m)) = FALSE )
set L = n -BinarySequence l;
set M = n -BinarySequence m;
A1: (Absval ((n -BinarySequence l) + (n -BinarySequence m))) + (2 to_power n) >= 2 to_power n by NAT_1:11;
assume A2: l + m <= (2 to_power n) - 1 ; ::_thesis: add_ovfl ((n -BinarySequence l),(n -BinarySequence m)) = FALSE
then A3: l < 2 to_power n by Th8;
assume  add_ovfl ((n -BinarySequence l),(n -BinarySequence m)) <> FALSE ; ::_thesis: contradiction
then A4: IFEQ ((add_ovfl ((n -BinarySequence l),(n -BinarySequence m))),FALSE,0,(2 to_power n)) = 2 to_power n by FUNCOP_1:def_8;
A5: m < 2 to_power n by A2, Th8;
(Absval ((n -BinarySequence l) + (n -BinarySequence m))) + (IFEQ ((add_ovfl ((n -BinarySequence l),(n -BinarySequence m))),FALSE,0,(2 to_power n))) = (Absval (n -BinarySequence l)) + (Absval (n -BinarySequence m)) by BINARITH:21
.= l + (Absval (n -BinarySequence m)) by A3, BINARI_3:35
.= l + m by A5, BINARI_3:35 ;
hence  contradiction by A2, A4, A1, XREAL_1:146, XXREAL_0:2; ::_thesis: verum
end;

theorem Th11: :: BINARI_4:11
for n being non empty Nat
for l, m being Nat st l + m <= (2 to_power n) - 1 holds
Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
proof
let n be non empty Nat; ::_thesis: for l, m being Nat st l + m <= (2 to_power n) - 1 holds
Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
let l, m be Nat; ::_thesis: ( l + m <= (2 to_power n) - 1 implies Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m )
assume A1: l + m <= (2 to_power n) - 1 ; ::_thesis: Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
A2: l < 2 to_power n by A1, Th8;
set L = n -BinarySequence l;
set M = n -BinarySequence m;
 add_ovfl ((n -BinarySequence l),(n -BinarySequence m)) = FALSE by A1, Th10;
then  n -BinarySequence l,n -BinarySequence m are_summable by BINARITH:def_7;
then A3: Absval ((n -BinarySequence l) + (n -BinarySequence m)) = (Absval (n -BinarySequence l)) + (Absval (n -BinarySequence m)) by BINARITH:22
.= l + (Absval (n -BinarySequence m)) by A2, BINARI_3:35 ;
 m < 2 to_power n by A1, Th8;
hence  Absval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m by A3, BINARI_3:35; ::_thesis: verum
end;

theorem Th12: :: BINARI_4:12
for n being non empty Nat
for z being Tuple of n, BOOLEAN st z /. n = TRUE holds
Absval z >= 2 to_power (n -' 1)
proof
defpred S1[ Nat] means  for z being Tuple of $1, BOOLEAN st z /. $1 = TRUE holds
Absval z >= 2 to_power ($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  S1[n] ; ::_thesis: S1[n + 1]
let z be Tuple of n + 1, BOOLEAN ; ::_thesis: ( z /. (n + 1) = TRUE implies Absval z >= 2 to_power ((n + 1) -' 1) )
assume A2: z /. (n + 1) = TRUE ; ::_thesis: Absval z >= 2 to_power ((n + 1) -' 1)
consider x being Element of n -tuples_on BOOLEAN, a being Element of BOOLEAN  such that
A3: z = x ^ <*a*> by FINSEQ_2:117;
A4: n + 1 >= 1 by NAT_1:11;
then  (n + 1) - 1 >= 1 - 1 by XREAL_1:9;
then A5: (n + 1) -' 1 = n by XREAL_0:def_2;
 len z = n + 1 by CARD_1:def_7;
then A6: z /. (n + 1) = (x ^ <*a*>) . (n + 1) by A3, A4, FINSEQ_4:15
.= a by FINSEQ_2:116 ;
Absval z = (Absval x) + (IFEQ (a,FALSE,0,(2 to_power n))) by A3, BINARITH:20
.= (Absval x) + (2 to_power n) by A2, A6, FUNCOP_1:def_8 ;
hence  Absval z >= 2 to_power ((n + 1) -' 1) by A5, NAT_1:11; ::_thesis: verum
end;
A7: S1[1]
proof
let z be Tuple of 1, BOOLEAN ; ::_thesis: ( z /. 1 = TRUE implies Absval z >= 2 to_power (1 -' 1) )
assume A8: z /. 1 = TRUE ; ::_thesis: Absval z >= 2 to_power (1 -' 1)
A9: len z = 1 by CARD_1:def_7;
then  z . 1 = z /. 1 by FINSEQ_4:15;
then  z = <*TRUE*> by A8, A9, FINSEQ_1:40;
then A10: Absval z = 1 by BINARITH:16;
 2 to_power (1 -' 1) = 2 to_power (1 - 1) by XREAL_0:def_2;
hence  Absval z >= 2 to_power (1 -' 1) by A10, POWER:24; ::_thesis: verum
end;
thus  for n being non empty Nat holds S1[n] from NAT_1:sch_10(A7, A1); ::_thesis: verum
end;

theorem Th13: :: BINARI_4:13
for n being non empty Nat
for l, m being Nat st l + m <= (2 to_power (n -' 1)) - 1 holds
(carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE
proof
let n be non empty Nat; ::_thesis: for l, m being Nat st l + m <= (2 to_power (n -' 1)) - 1 holds
(carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE
let l, m be Nat; ::_thesis: ( l + m <= (2 to_power (n -' 1)) - 1 implies (carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE )
set L = n -BinarySequence l;
set M = n -BinarySequence m;
set F = FALSE ;
set T = TRUE ;
assume A1: l + m <= (2 to_power (n -' 1)) - 1 ; ::_thesis: (carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE
then A2: l < 2 to_power (n -' 1) by Th8;
 n >= 1 by NAT_1:14;
then  n - 1 >= 1 - 1 by XREAL_1:9;
then  n -' 1 = n - 1 by XREAL_0:def_2;
then  2 to_power (n -' 1) < 2 to_power n by POWER:39, XREAL_1:146;
then A3: (2 to_power (n -' 1)) - 1 < (2 to_power n) - 1 by XREAL_1:14;
assume  not (carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = FALSE ; ::_thesis: contradiction
then A4: (carry ((n -BinarySequence l),(n -BinarySequence m))) /. n = TRUE by XBOOLEAN:def_3;
A5: m < 2 to_power (n -' 1) by A1, Th8;
 1 <= n by NAT_1:14;
then A6: n in Seg n by FINSEQ_1:1;
then A7: (n -BinarySequence m) /. n = IFEQ (((m div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) by BINARI_3:def_1
.= IFEQ ((0 mod 2),0,FALSE,TRUE) by A5, NAT_D:27
.= IFEQ (0,0,FALSE,TRUE) by NAT_D:26
.= FALSE by FUNCOP_1:def_8 ;
(n -BinarySequence l) /. n = IFEQ (((l div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) by A6, BINARI_3:def_1
.= IFEQ ((0 mod 2),0,FALSE,TRUE) by A2, NAT_D:27
.= IFEQ (0,0,FALSE,TRUE) by NAT_D:26
.= FALSE by FUNCOP_1:def_8 ;
then ((n -BinarySequence l) + (n -BinarySequence m)) /. n = (FALSE 'xor' FALSE) 'xor' TRUE by A4, A6, A7, BINARITH:def_5
.= TRUE ;
then A8: Absval ((n -BinarySequence l) + (n -BinarySequence m)) >= 2 to_power (n -' 1) by Th12;
 l + m < 2 to_power (n -' 1) by A1, XREAL_1:146, XXREAL_0:2;
hence  contradiction by A1, A3, A8, Th11, XXREAL_0:2; ::_thesis: verum
end;

theorem Th14: :: BINARI_4:14
for l, m being Nat
for n being non empty Nat st l + m <= (2 to_power (n -' 1)) - 1 holds
Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
proof
let l, m be Nat; ::_thesis: for n being non empty Nat st l + m <= (2 to_power (n -' 1)) - 1 holds
Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
let n be non empty Nat; ::_thesis: ( l + m <= (2 to_power (n -' 1)) - 1 implies Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m )
assume A1: l + m <= (2 to_power (n -' 1)) - 1 ; ::_thesis: Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m
A2: l < 2 to_power (n -' 1) by A1, Th8;
set L = n -BinarySequence l;
set M = n -BinarySequence m;
set F = FALSE ;
set T = TRUE ;
 n >= 1 by NAT_1:14;
then  n - 1 >= 1 - 1 by XREAL_1:9;
then  n -' 1 = n - 1 by XREAL_0:def_2;
then  2 to_power (n -' 1) < 2 to_power n by POWER:39, XREAL_1:146;
then A3: (2 to_power (n -' 1)) - 1 < (2 to_power n) - 1 by XREAL_1:14;
A4: m < 2 to_power (n -' 1) by A1, Th8;
 1 <= n by NAT_1:14;
then A5: n in Seg n by FINSEQ_1:1;
then A6: (n -BinarySequence m) /. n = IFEQ (((m div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) by BINARI_3:def_1
.= IFEQ ((0 mod 2),0,FALSE,TRUE) by A4, NAT_D:27
.= IFEQ (0,0,FALSE,TRUE) by NAT_D:26
.= FALSE by FUNCOP_1:def_8 ;
(n -BinarySequence l) /. n = IFEQ (((l div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) by A5, BINARI_3:def_1
.= IFEQ ((0 mod 2),0,FALSE,TRUE) by A2, NAT_D:27
.= IFEQ (0,0,FALSE,TRUE) by NAT_D:26
.= FALSE by FUNCOP_1:def_8 ;
then ((n -BinarySequence l) + (n -BinarySequence m)) /. n = (FALSE 'xor' FALSE) 'xor' ((carry ((n -BinarySequence l),(n -BinarySequence m))) /. n) by A5, A6, BINARITH:def_5
.= FALSE by A1, Th13 ;
then  Intval ((n -BinarySequence l) + (n -BinarySequence m)) = Absval ((n -BinarySequence l) + (n -BinarySequence m)) by BINARI_2:def_3;
hence  Intval ((n -BinarySequence l) + (n -BinarySequence m)) = l + m by A1, A3, Th11, XXREAL_0:2; ::_thesis: verum
end;

theorem Th15: :: BINARI_4:15
for z being Tuple of 1, BOOLEAN st z = <*TRUE*> holds
Intval z = - 1
proof
let z be Tuple of 1, BOOLEAN ; ::_thesis: ( z = <*TRUE*> implies Intval z = - 1 )
assume A1: z = <*TRUE*> ; ::_thesis: Intval z = - 1
 len z = 1 by CARD_1:def_7;
then z /. 1 = z . 1 by FINSEQ_4:15
.= TRUE by A1, FINSEQ_1:40 ;
then  Intval z = (Absval z) - (2 to_power 1) by BINARI_2:def_3
.= 1 - (2 to_power 1) by A1, BINARITH:16
.= 1 - (1 + 1) by POWER:25
.= 0 - 1 ;
hence  Intval z = - 1 ; ::_thesis: verum
end;

theorem :: BINARI_4:16
for z being Tuple of 1, BOOLEAN st z = <*FALSE*> holds
Intval z = 0
proof
let z be Tuple of 1, BOOLEAN ; ::_thesis: ( z = <*FALSE*> implies Intval z = 0 )
assume A1: z = <*FALSE*> ; ::_thesis: Intval z = 0
 len z = 1 by CARD_1:def_7;
then z /. 1 = z . 1 by FINSEQ_4:15
.= FALSE by A1, FINSEQ_1:40 ;
then  Intval z = Absval z by BINARI_2:def_3;
hence  Intval z = 0 by A1, BINARITH:15; ::_thesis: verum
end;

theorem :: BINARI_4:17
for x being boolean set holds TRUE 'or' x = TRUE ;

theorem :: BINARI_4:18
for n being non empty Nat holds
( 0 <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= 0 )
proof
defpred S1[ Nat] means ( 0 <= (2 to_power ($1 -' 1)) - 1 & - (2 to_power ($1 -' 1)) <= 0 );
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 that
A2: 0 <= (2 to_power (k -' 1)) - 1 and
 - (2 to_power (k -' 1)) <= 0 ; ::_thesis: S1[k + 1]
 (k + 1) -' 1 = k by NAT_D:34;
then  2 to_power (k -' 1) < 2 to_power ((k + 1) -' 1) by NAT_2:9, POWER:39;
hence  S1[k + 1] by A2, XREAL_1:9; ::_thesis: verum
end;
 1 - 1 = 0 ;
then 2 to_power (1 -' 1) = 2 to_power 0 by XREAL_0:def_2
.= 1 by POWER:24 ;
then A3: S1[1] ;
thus  for n being non empty Nat holds S1[n] from NAT_1:sch_10(A3, A1); ::_thesis: verum
end;

theorem :: BINARI_4:19
for n being non empty Nat
for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds
x,y are_summable
proof
let n be non empty Nat; ::_thesis: for x, y being Tuple of n, BOOLEAN st x = 0* n & y = 0* n holds
x,y are_summable
let x, y be Tuple of n, BOOLEAN ; ::_thesis: ( x = 0* n & y = 0* n implies x,y are_summable )
assume that
A1: x = 0* n and
A2: y = 0* n ; ::_thesis: x,y are_summable
A3: 1 <= n by NAT_1:14;
 len x = n by CARD_1:def_7;
then x /. n = (0* n) . n by A1, A3, FINSEQ_4:15
.= FALSE ;
then  add_ovfl (x,y) = ((FALSE '&' FALSE) 'or' (FALSE '&' ((carry (x,y)) /. n))) 'or' (FALSE '&' ((carry (x,y)) /. n)) by A1, A2, BINARITH:def_6
.= FALSE ;
hence  x,y are_summable by BINARITH:def_7; ::_thesis: verum
end;

theorem Th20: :: BINARI_4:20
for n being non empty Nat
for i being Integer holds (i * n) mod n = 0
proof
let n be non empty Nat; ::_thesis: for i being Integer holds (i * n) mod n = 0
let i be Integer; ::_thesis: (i * n) mod n = 0
(i * n) mod n = ((i mod n) * (n mod n)) mod n by NAT_D:67
.= ((i mod n) * 0) mod n by NAT_D:25
.= 0 mod n ;
hence  (i * n) mod n = 0 by NAT_D:26; ::_thesis: verum
end;

begin

definition
let m, j be Nat;
func MajP (m,j) ->  Nat means :Def1: :: BINARI_4:def 1
( 2 to_power it >= j & it >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= it ) );
existence
 ex b1 being Nat st
( 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) )
proof
percases ( 2 to_power m >= j or 2 to_power m < j ) ;
supposeA1: 2 to_power m >= j ; ::_thesis: ex b1 being Nat st
( 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) )
 for k being Nat st 2 to_power k >= j & k >= m holds
k >= m ;
hence  ex b1 being Nat st
( 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) ) by A1; ::_thesis: verum
end;
supposeA2: 2 to_power m < j ; ::_thesis: ex b1 being Nat st
( 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) )
defpred S1[ Nat] means ( 2 to_power $1 >= j & $1 >= m );
 2 to_power m >= m by Th2;
then A3: j >= m by A2, XXREAL_0:2;
 2 to_power j >= j by Th2;
then A4: ex k being Nat st S1[k] by A3;
 ex k being Nat st
( S1[k] & ( for l being Nat st S1[l] holds
l >= k ) ) from NAT_1:sch_5(A4);
hence  ex b1 being Nat st
( 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) ) ; ::_thesis: verum
end;
end;
end;
uniqueness
 for b1, b2 being Nat st 2 to_power b1 >= j & b1 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b1 ) & 2 to_power b2 >= j & b2 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b2 ) holds
b1 = b2
proof
let p, q be Nat; ::_thesis: ( 2 to_power p >= j & p >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= p ) & 2 to_power q >= j & q >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= q ) implies p = q )
assume  ( 2 to_power p >= j & p >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= p ) & 2 to_power q >= j & q >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= q ) ) ; ::_thesis: p = q
then  ( p >= q & q >= p ) ;
hence  p = q by XXREAL_0:1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines MajP BINARI_4:def_1_:_
 for m, j, b3 being Nat holds
( b3 = MajP (m,j) iff ( 2 to_power b3 >= j & b3 >= m & ( for k being Nat st 2 to_power k >= j & k >= m holds
k >= b3 ) ) );

theorem :: BINARI_4:21
for j, k, m being Nat st j >= k holds
MajP (m,j) >= MajP (m,k)
proof
let j, k, m be Nat; ::_thesis: ( j >= k implies MajP (m,j) >= MajP (m,k) )
assume A1: j >= k ; ::_thesis: MajP (m,j) >= MajP (m,k)
A2: MajP (m,j) >= m by Def1;
 2 to_power (MajP (m,j)) >= j by Def1;
then  2 to_power (MajP (m,j)) >= k by A1, XXREAL_0:2;
hence  MajP (m,j) >= MajP (m,k) by A2, Def1; ::_thesis: verum
end;

theorem Th22: :: BINARI_4:22
for l, m, j being Nat st l >= m holds
MajP (l,j) >= MajP (m,j)
proof
let l, m, j be Nat; ::_thesis: ( l >= m implies MajP (l,j) >= MajP (m,j) )
assume A1: l >= m ; ::_thesis: MajP (l,j) >= MajP (m,j)
A2: 2 to_power (MajP (l,j)) >= j by Def1;
 MajP (l,j) >= l by Def1;
then  MajP (l,j) >= m by A1, XXREAL_0:2;
hence  MajP (l,j) >= MajP (m,j) by A2, Def1; ::_thesis: verum
end;

theorem :: BINARI_4:23
for m being Nat st m >= 1 holds
MajP (m,1) = m
proof
let m be Nat; ::_thesis: ( m >= 1 implies MajP (m,1) = m )
assume  m >= 1 ; ::_thesis: MajP (m,1) = m
then A1: 2 to_power m >= 1 by POWER:35;
 for k being Nat st 2 to_power k >= 1 & k >= m holds
k >= m ;
hence  MajP (m,1) = m by A1, Def1; ::_thesis: verum
end;

theorem Th24: :: BINARI_4:24
for j, m being Nat st j <= 2 to_power m holds
MajP (m,j) = m
proof
let j, m be Nat; ::_thesis: ( j <= 2 to_power m implies MajP (m,j) = m )
A1: for k being Nat st 2 to_power k >= j & k >= m holds
k >= m ;
assume  j <= 2 to_power m ; ::_thesis: MajP (m,j) = m
hence  MajP (m,j) = m by A1, Def1; ::_thesis: verum
end;

theorem :: BINARI_4:25
for j, m being Nat st j > 2 to_power m holds
MajP (m,j) > m
proof
let j, m be Nat; ::_thesis: ( j > 2 to_power m implies MajP (m,j) > m )
assume A1: j > 2 to_power m ; ::_thesis: MajP (m,j) > m
 2 to_power (MajP (m,j)) >= j by Def1;
then  2 to_power (MajP (m,j)) > 2 to_power m by A1, XXREAL_0:2;
hence  MajP (m,j) > m by PRE_FF:8; ::_thesis: verum
end;

begin

definition
let m be Nat;
let i be Integer;
func 2sComplement (m,i) ->  Tuple of m, BOOLEAN  equals :Def2: :: BINARI_4:def 2
m -BinarySequence (abs ((2 to_power (MajP (m,(abs i)))) + i)) if i < 0
otherwise m -BinarySequence (abs i);
correctness
coherence
( ( i < 0 implies m -BinarySequence (abs ((2 to_power (MajP (m,(abs i)))) + i)) is Tuple of m, BOOLEAN ) & ( not i < 0 implies m -BinarySequence (abs i) is Tuple of m, BOOLEAN ) );
consistency
for b1 being Tuple of m, BOOLEAN holds verum;
;
end;

:: deftheorem Def2 defines 2sComplement BINARI_4:def_2_:_
 for m being Nat
for i being Integer holds
( ( i < 0 implies 2sComplement (m,i) = m -BinarySequence (abs ((2 to_power (MajP (m,(abs i)))) + i)) ) & ( not i < 0 implies 2sComplement (m,i) = m -BinarySequence (abs i) ) );

theorem :: BINARI_4:26
for m being Nat holds 2sComplement (m,0) = 0* m
proof
let m be Nat; ::_thesis: 2sComplement (m,0) = 0* m
2sComplement (m,0) = m -BinarySequence (abs 0) by Def2
.= m -BinarySequence 0 by ABSVALUE:2 ;
hence  2sComplement (m,0) = 0* m by BINARI_3:25; ::_thesis: verum
end;

theorem :: BINARI_4:27
for n being non empty Nat
for i being Integer st i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i holds
Intval (2sComplement (n,i)) = i
proof
let n be non empty Nat; ::_thesis: for i being Integer st i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i holds
Intval (2sComplement (n,i)) = i
let i be Integer; ::_thesis: ( i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i implies Intval (2sComplement (n,i)) = i )
assume that
A1: i <= (2 to_power (n -' 1)) - 1 and
A2: - (2 to_power (n -' 1)) <= i ; ::_thesis: Intval (2sComplement (n,i)) = i
A3: n >= 1 by NAT_1:14;
now__::_thesis:_Intval_(2sComplement_(n,i))_=_i
percases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; ::_thesis: Intval (2sComplement (n,i)) = i
then reconsider i = i as Element of NAT by INT_1:3;
A4: 2sComplement (n,i) = n -BinarySequence (abs i) by Def2
.= n -BinarySequence i by ABSVALUE:def_1 ;
 i + 1 <= ((2 to_power (n -' 1)) - 1) + 1 by A1, XREAL_1:6;
then A5: i < 2 to_power (n -' 1) by NAT_1:13;
 n >= 1 by NAT_1:14;
then  n - 1 >= 1 - 1 by XREAL_1:9;
then  n -' 1 = n - 1 by XREAL_0:def_2;
then  2 to_power (n -' 1) < 2 to_power n by POWER:39, XREAL_1:146;
then  i < 2 to_power n by A5, XXREAL_0:2;
then A6: Absval (n -BinarySequence i) = i by BINARI_3:35;
 1 <= n by NAT_1:14;
then  n in Seg n by FINSEQ_1:1;
then (n -BinarySequence i) /. n = IFEQ (((i div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) by BINARI_3:def_1
.= IFEQ ((0 mod 2),0,FALSE,TRUE) by A5, NAT_D:27
.= IFEQ (0,0,FALSE,TRUE) by NAT_D:26
.= FALSE by FUNCOP_1:def_8 ;
hence  Intval (2sComplement (n,i)) = i by A4, A6, BINARI_2:def_3; ::_thesis: verum
end;
supposeA7: i < 0 ; ::_thesis: Intval (2sComplement (n,i)) = i
A8: 2 to_power n >= 2 to_power (n -' 1) by NAT_2:9, POWER:39;
then  - (2 to_power n) <= - (2 to_power (n -' 1)) by XREAL_1:24;
then  - (2 to_power n) <= i by A2, XXREAL_0:2;
then  (- (2 to_power n)) - i <= i - i by XREAL_1:9;
then  - ((2 to_power n) + i) <= 0 ;
then  (2 to_power n) + i >= - 0 by XREAL_1:24;
then reconsider k = (2 to_power n) + i as Element of NAT by INT_1:3;
 abs i = - i by A7, ABSVALUE:def_1;
then  abs i <= - (- (2 to_power (n -' 1))) by A2, XREAL_1:24;
then  MajP (n,(abs i)) = n by A8, Th24, XXREAL_0:2;
then A9: 2sComplement (n,i) = n -BinarySequence (abs k) by A7, Def2
.= n -BinarySequence k by ABSVALUE:def_1 ;
 k < (2 to_power n) + 0 by A7, XREAL_1:8;
then  k < (2 to_power 1) * (2 to_power (n -' 1)) by NAT_1:14, NAT_2:10;
then  k < 2 * (2 to_power (n -' 1)) by POWER:25;
then A10: k < (2 to_power (n -' 1)) + (2 to_power (n -' 1)) ;
A11: (2 to_power n) + i < (2 to_power n) + 0 by A7, XREAL_1:6;
(2 to_power n) + (- (2 to_power (n -' 1))) = (2 to_power n) - (2 to_power (n -' 1))
.= ((2 to_power 1) * (2 to_power (n -' 1))) - (2 to_power (n -' 1)) by NAT_1:14, NAT_2:10
.= (2 * (2 to_power (n -' 1))) - (2 to_power (n -' 1)) by POWER:25
.= 2 to_power (n -' 1) ;
then A12: k >= 2 to_power (n -' 1) by A2, XREAL_1:6;
 n in Seg n by A3, FINSEQ_1:1;
then (n -BinarySequence k) /. n = IFEQ (((k div (2 to_power (n -' 1))) mod 2),0,FALSE,TRUE) by BINARI_3:def_1
.= IFEQ ((1 mod 2),0,FALSE,TRUE) by A12, A10, NAT_2:20
.= IFEQ (1,0,FALSE,TRUE) by NAT_D:14
.= TRUE by FUNCOP_1:def_8 ;
then  Intval (2sComplement (n,i)) = (Absval (n -BinarySequence k)) - (2 to_power n) by A9, BINARI_2:def_3
.= k - (2 to_power n) by A11, BINARI_3:35
.= 0 + i ;
hence  Intval (2sComplement (n,i)) = i ; ::_thesis: verum
end;
end;
end;
hence  Intval (2sComplement (n,i)) = i ; ::_thesis: verum
end;

Lm1:  for n being non empty 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)
proof
let n be non empty Nat; ::_thesis: for k, l being Nat st k mod n = l mod n & k > l holds
ex s being Integer st k = l + (s * n)
let k, l be Nat; ::_thesis: ( k mod n = l mod n & k > l implies ex s being Integer st k = l + (s * n) )
assume that
A1: k mod n = l mod n and
A2: k > l ; ::_thesis: ex s being Integer st k = l + (s * n)
consider m being Nat such that
A3: k = l + m by A2, NAT_1:10;
take  m div n ; ::_thesis: k = l + ((m div n) * n)
 ( l = ((l div n) * n) + (l mod n) & k = ((k div n) * n) + (l mod n) ) by A1, NAT_D:2;
then m mod n = (((k div n) - (l div n)) * n) mod n by A3
.= 0 by Th20 ;
then  (l + m) div n = (l div n) + (m div n) by NAT_D:19;
then k = (((l div n) + (m div n)) * n) + (l mod n) by A1, A3, NAT_D:2
.= ((m div n) * n) + (((l div n) * n) + (l mod n))
.= ((m div n) * n) + l by NAT_D:2 ;
hence  k = l + ((m div n) * n) ; ::_thesis: verum
end;

Lm2:  for n being non empty Nat
for k, l being Nat st k mod n = l mod n holds
ex s being Integer st k = l + (s * n)
proof
let n be non empty Nat; ::_thesis: for k, l being Nat st k mod n = l mod n holds
ex s being Integer st k = l + (s * n)
let k, l be Nat; ::_thesis: ( k mod n = l mod n implies ex s being Integer st k = l + (s * n) )
assume A1: k mod n = l mod n ; ::_thesis: ex s being Integer st k = l + (s * n)
now__::_thesis:_ex_s_being_Integer_st_k_=_l_+_(s_*_n)
percases ( k = l or k > l or l > k ) by XXREAL_0:1;
supposeA2: k = l ; ::_thesis: ex s being Integer st k = l + (s * n)
set s = 0 ;
 k = l + (0 * n) by A2;
hence  ex s being Integer st k = l + (s * n) ; ::_thesis: verum
end;
supposeA3: ( k > l or l > k ) ; ::_thesis: ex s being Integer st k = l + (s * n)
now__::_thesis:_ex_s_being_Integer_st_k_=_l_+_(s_*_n)
percases ( k > l or k < l ) by A3;
suppose k > l ; ::_thesis: ex s being Integer st k = l + (s * n)
hence  ex s being Integer st k = l + (s * n) by A1, Lm1; ::_thesis: verum
end;
suppose k < l ; ::_thesis: ex s being Integer st k = l + (s * n)
then consider t being Integer such that
A4: l = k + (t * n) by A1, Lm1;
 k = l + ((- t) * n) by A4;
hence  ex s being Integer st k = l + (s * n) ; ::_thesis: verum
end;
end;
end;
hence  ex s being Integer st k = l + (s * n) ; ::_thesis: verum
end;
end;
end;
hence  ex s being Integer st k = l + (s * n) ; ::_thesis: verum
end;

Lm3:  for n being non empty 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
proof
let n be non empty Nat; ::_thesis: 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
let k, l, m be Nat; ::_thesis: ( m < n & k mod (2 to_power n) = l mod (2 to_power n) implies (k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2 )
assume that
A1: m < n and
A2: k mod (2 to_power n) = l mod (2 to_power n) ; ::_thesis: (k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2
consider j being Nat such that
A3: n = m + j by A1, NAT_1:10;
 2 to_power n = 2 |^ n by POWER:41;
then  not 2 to_power n is empty by PREPOWER:5;
then consider s being Integer such that
A4: k = l + (s * (2 to_power n)) by A2, Lm2;
reconsider j = j as Nat ;
set M = 2 to_power m;
set J = 2 to_power j;
 m + (- m) < n + (- m) by A1, XREAL_1:8;
then  0 + 1 < j + 1 by A3, XREAL_1:8;
then  1 <= j by NAT_1:13;
then  2 to_power 1 divides 2 to_power j by NAT_2:11;
then  2 divides 2 to_power j by POWER:25;
then  (2 to_power j) mod 2 = 0 by PEPIN:6;
then A5: (s * (2 to_power j)) mod 2 = ((s mod 2) * 0) mod 2 by NAT_D:67
.= 0 by NAT_D:26 ;
reconsider L = l as Integer ;
A6: 2 to_power m > 0 by POWER:34;
k div (2 to_power m) = (l + (s * ((2 to_power j) * (2 to_power m)))) div (2 to_power m) by A4, A3, POWER:27
.= (l + ((s * (2 to_power j)) * (2 to_power m))) div (2 to_power m)
.= (l div (2 to_power m)) + (s * (2 to_power j)) by A6, NAT_D:61 ;
then (k div (2 to_power m)) mod 2 = (((L div (2 to_power m)) mod 2) + 0) mod 2 by A5, NAT_D:66
.= (L div (2 to_power m)) mod 2 by NAT_D:65 ;
hence  (k div (2 to_power m)) mod 2 = (l div (2 to_power m)) mod 2 ; ::_thesis: verum
end;

Lm4:  for n being non empty 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,(abs h)))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,(abs i)))) + i) mod (2 to_power n)
proof
let n be non empty Nat; ::_thesis: for h, i being Integer st h mod (2 to_power n) = i mod (2 to_power n) holds
((2 to_power (MajP (n,(abs h)))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,(abs i)))) + i) mod (2 to_power n)
let h, i be Integer; ::_thesis: ( h mod (2 to_power n) = i mod (2 to_power n) implies ((2 to_power (MajP (n,(abs h)))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,(abs i)))) + i) mod (2 to_power n) )
assume A1: h mod (2 to_power n) = i mod (2 to_power n) ; ::_thesis: ((2 to_power (MajP (n,(abs h)))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,(abs i)))) + i) mod (2 to_power n)
 n <= MajP (n,(abs i)) by Def1;
then consider y being Nat such that
A2: MajP (n,(abs i)) = n + y by NAT_1:10;
reconsider L = 2 to_power (MajP (n,(abs i))) as Integer ;
reconsider M = 2 to_power (MajP (n,(abs h))) as Integer ;
 n <= MajP (n,(abs h)) by Def1;
then consider x being Nat such that
A3: MajP (n,(abs h)) = n + x by NAT_1:10;
reconsider x = x as Nat ;
 M = (2 to_power n) * (2 to_power x) by A3, POWER:27;
then A4: M mod (2 to_power n) = (((2 to_power n) mod (2 to_power n)) * (2 to_power x)) mod (2 to_power n) by EULER_2:8
.= (0 * (2 to_power x)) mod (2 to_power n) by NAT_D:25
.= 0 by NAT_D:26 ;
reconsider y = y as Nat ;
 L = (2 to_power n) * (2 to_power y) by A2, POWER:27;
then A5: L mod (2 to_power n) = (((2 to_power n) mod (2 to_power n)) * (2 to_power y)) mod (2 to_power n) by EULER_2:8
.= (0 * (2 to_power y)) mod (2 to_power n) by NAT_D:25
.= 0 by NAT_D:26 ;
A6: (L + i) mod (2 to_power n) = ((L mod (2 to_power n)) + (i mod (2 to_power n))) mod (2 to_power n) by NAT_D:66
.= (i mod (2 to_power n)) mod (2 to_power n) by A5 ;
(M + h) mod (2 to_power n) = ((M mod (2 to_power n)) + (h mod (2 to_power n))) mod (2 to_power n) by NAT_D:66
.= (h mod (2 to_power n)) mod (2 to_power n) by A4 ;
hence  ((2 to_power (MajP (n,(abs h)))) + h) mod (2 to_power n) = ((2 to_power (MajP (n,(abs i)))) + i) mod (2 to_power n) by A1, A6; ::_thesis: verum
end;

Lm5:  for n being non empty 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)
proof
let n be non empty Nat; ::_thesis: 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)
let h, i be Integer; ::_thesis: ( h >= 0 & i >= 0 & h mod (2 to_power n) = i mod (2 to_power n) implies 2sComplement (n,h) = 2sComplement (n,i) )
assume that
A1: ( h >= 0 & i >= 0 ) and
A2: h mod (2 to_power n) = i mod (2 to_power n) ; ::_thesis: 2sComplement (n,h) = 2sComplement (n,i)
A3: for j being Nat st j in Seg n holds
(n -BinarySequence (abs h)) . j = (n -BinarySequence (abs i)) . j
proof
A4: ( abs h = h & abs i = i ) by A1, ABSVALUE:def_1;
let j be Nat; ::_thesis: ( j in Seg n implies (n -BinarySequence (abs h)) . j = (n -BinarySequence (abs i)) . j )
assume A5: j in Seg n ; ::_thesis: (n -BinarySequence (abs h)) . j = (n -BinarySequence (abs i)) . j
reconsider j = j as Nat ;
A6: j <= n by A5, FINSEQ_1:1;
A7: 1 <= j by A5, FINSEQ_1:1;
then  j - 1 >= 1 - 1 by XREAL_1:9;
then  j -' 1 = j - 1 by XREAL_0:def_2;
then A8: j -' 1 < n by A6, XREAL_1:146, XXREAL_0:2;
 len (n -BinarySequence (abs i)) = n by CARD_1:def_7;
then A9: (n -BinarySequence (abs i)) . j = (n -BinarySequence (abs i)) /. j by A7, A6, FINSEQ_4:15
.= IFEQ ((((abs i) div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A5, BINARI_3:def_1 ;
 len (n -BinarySequence (abs h)) = n by CARD_1:def_7;
then (n -BinarySequence (abs h)) . j = (n -BinarySequence (abs h)) /. j by A7, A6, FINSEQ_4:15
.= IFEQ ((((abs h) div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A5, BINARI_3:def_1
.= IFEQ ((((abs i) div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A2, A8, A4, Lm3 ;
hence  (n -BinarySequence (abs h)) . j = (n -BinarySequence (abs i)) . j by A9; ::_thesis: verum
end;
 ( 2sComplement (n,h) = n -BinarySequence (abs h) & 2sComplement (n,i) = n -BinarySequence (abs i) ) by A1, Def2;
hence  2sComplement (n,h) = 2sComplement (n,i) by A3, FINSEQ_2:119; ::_thesis: verum
end;

Lm6:  for n being non empty 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)
proof
let n be non empty Nat; ::_thesis: 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)
let h, i be Integer; ::_thesis: ( h < 0 & i < 0 & h mod (2 to_power n) = i mod (2 to_power n) implies 2sComplement (n,h) = 2sComplement (n,i) )
assume that
A1: h < 0 and
A2: i < 0 and
A3: h mod (2 to_power n) = i mod (2 to_power n) ; ::_thesis: 2sComplement (n,h) = 2sComplement (n,i)
 abs i = - i by A2, ABSVALUE:def_1;
then  2 to_power (MajP (n,(abs i))) >= - i by Def1;
then  (2 to_power (MajP (n,(abs i)))) + i >= (- i) + i by XREAL_1:6;
then reconsider I = (2 to_power (MajP (n,(abs i)))) + i as Element of NAT by INT_1:3;
 abs h = - h by A1, ABSVALUE:def_1;
then  2 to_power (MajP (n,(abs h))) >= - h by Def1;
then  (2 to_power (MajP (n,(abs h)))) + h >= (- h) + h by XREAL_1:6;
then reconsider H = (2 to_power (MajP (n,(abs h)))) + h as Element of NAT by INT_1:3;
A4: H mod (2 to_power n) = I mod (2 to_power n) by A3, Lm4;
A5: for j being Nat st j in Seg n holds
(n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j
proof
A6: len (n -BinarySequence I) = n by CARD_1:def_7;
let j be Nat; ::_thesis: ( j in Seg n implies (n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j )
assume A7: j in Seg n ; ::_thesis: (n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j
A8: 1 <= j by A7, FINSEQ_1:1;
A9: j <= n by A7, FINSEQ_1:1;
reconsider j = j as Nat ;
 j - 1 >= 1 - 1 by A8, XREAL_1:9;
then  j -' 1 = j - 1 by XREAL_0:def_2;
then A10: j -' 1 < n by A9, XREAL_1:146, XXREAL_0:2;
 ( len (n -BinarySequence H) = n & abs H = H ) by ABSVALUE:def_1, CARD_1:def_7;
then (n -BinarySequence (abs H)) . j = (n -BinarySequence H) /. j by A8, A9, FINSEQ_4:15
.= IFEQ (((H div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A7, BINARI_3:def_1
.= IFEQ (((I div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A4, A10, Lm3
.= (n -BinarySequence I) /. j by A7, BINARI_3:def_1
.= (n -BinarySequence I) . j by A8, A9, A6, FINSEQ_4:15 ;
hence  (n -BinarySequence (abs H)) . j = (n -BinarySequence (abs I)) . j by ABSVALUE:def_1; ::_thesis: verum
end;
 ( 2sComplement (n,h) = n -BinarySequence (abs ((2 to_power (MajP (n,(abs h)))) + h)) & 2sComplement (n,i) = n -BinarySequence (abs ((2 to_power (MajP (n,(abs i)))) + i)) ) by A1, A2, Def2;
hence  2sComplement (n,h) = 2sComplement (n,i) by A5, FINSEQ_2:119; ::_thesis: verum
end;

theorem :: BINARI_4:28
for n being non empty Nat
for h, i being Integer st ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h mod (2 to_power n) = i mod (2 to_power n) holds
2sComplement (n,h) = 2sComplement (n,i) by Lm5, Lm6;

theorem :: BINARI_4:29
for n being non empty Nat
for h, i being Integer st ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h,i are_congruent_mod 2 to_power n holds
2sComplement (n,h) = 2sComplement (n,i)
proof
let n be non empty Nat; ::_thesis: for h, i being Integer st ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h,i are_congruent_mod 2 to_power n holds
2sComplement (n,h) = 2sComplement (n,i)
let h, i be Integer; ::_thesis: ( ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) & h,i are_congruent_mod 2 to_power n implies 2sComplement (n,h) = 2sComplement (n,i) )
assume that
A1: ( ( h >= 0 & i >= 0 ) or ( h < 0 & i < 0 ) ) and
A2: h,i are_congruent_mod 2 to_power n ; ::_thesis: 2sComplement (n,h) = 2sComplement (n,i)
 h mod (2 to_power n) = i mod (2 to_power n) by A2, NAT_D:64;
hence  2sComplement (n,h) = 2sComplement (n,i) by A1, Lm5, Lm6; ::_thesis: verum
end;

theorem Th30: :: BINARI_4:30
for n being non empty Nat
for l, m being Nat st l mod (2 to_power n) = m mod (2 to_power n) holds
n -BinarySequence l = n -BinarySequence m
proof
let n be non empty Nat; ::_thesis: for l, m being Nat st l mod (2 to_power n) = m mod (2 to_power n) holds
n -BinarySequence l = n -BinarySequence m
let l, m be Nat; ::_thesis: ( l mod (2 to_power n) = m mod (2 to_power n) implies n -BinarySequence l = n -BinarySequence m )
assume A1: l mod (2 to_power n) = m mod (2 to_power n) ; ::_thesis: n -BinarySequence l = n -BinarySequence m
 abs m = m by ABSVALUE:def_1;
then A2: 2sComplement (n,m) = n -BinarySequence m by Def2;
 abs l = l by ABSVALUE:def_1;
then  2sComplement (n,l) = n -BinarySequence l by Def2;
hence  n -BinarySequence l = n -BinarySequence m by A1, A2, Lm5; ::_thesis: verum
end;

theorem :: BINARI_4:31
for n being non empty Nat
for l, m being Nat st l,m are_congruent_mod 2 to_power n holds
n -BinarySequence l = n -BinarySequence m
proof
let n be non empty Nat; ::_thesis: for l, m being Nat st l,m are_congruent_mod 2 to_power n holds
n -BinarySequence l = n -BinarySequence m
let l, m be Nat; ::_thesis: ( l,m are_congruent_mod 2 to_power n implies n -BinarySequence l = n -BinarySequence m )
assume  l,m are_congruent_mod 2 to_power n ; ::_thesis: n -BinarySequence l = n -BinarySequence m
then  l mod (2 to_power n) = m mod (2 to_power n) by NAT_D:64;
hence  n -BinarySequence l = n -BinarySequence m by Th30; ::_thesis: verum
end;

theorem Th32: :: BINARI_4:32
for n being non empty Nat
for i being Integer
for j being Nat st 1 <= j & j <= n holds
(2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j
proof
let n be non empty Nat; ::_thesis: for i being Integer
for j being Nat st 1 <= j & j <= n holds
(2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j
let i be Integer; ::_thesis: for j being Nat st 1 <= j & j <= n holds
(2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j
let j be Nat; ::_thesis: ( 1 <= j & j <= n implies (2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j )
assume that
A1: 1 <= j and
A2: j <= n ; ::_thesis: (2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j
A3: j in Seg n by A1, A2, FINSEQ_1:1;
 n <= n + 1 by NAT_1:11;
then  j <= n + 1 by A2, XXREAL_0:2;
then A4: j in Seg (n + 1) by A1, FINSEQ_1:1;
set N = abs ((2 to_power (MajP (n,(abs i)))) + i);
set M = abs ((2 to_power (MajP ((n + 1),(abs i)))) + i);
A5: ( i < 0 implies ((abs ((2 to_power (MajP ((n + 1),(abs i)))) + i)) div (2 to_power (j -' 1))) mod 2 = ((abs ((2 to_power (MajP (n,(abs i)))) + i)) div (2 to_power (j -' 1))) mod 2 )
proof
 MajP ((n + 1),(abs i)) >= MajP (n,(abs i)) by Th22, NAT_1:11;
then consider m being Nat such that
A6: MajP ((n + 1),(abs i)) = (MajP (n,(abs i))) + m by NAT_1:10;
reconsider m = m as Nat ;
set P = MajP (n,(abs i));
assume A7: i < 0 ; ::_thesis: ((abs ((2 to_power (MajP ((n + 1),(abs i)))) + i)) div (2 to_power (j -' 1))) mod 2 = ((abs ((2 to_power (MajP (n,(abs i)))) + i)) div (2 to_power (j -' 1))) mod 2
set Q = 2 to_power (MajP (n,(abs i)));
A8: ((2 to_power (MajP (n,(abs i)))) * (2 to_power m)) mod (2 to_power (MajP (n,(abs i)))) = 0 by NAT_D:13;
 2 to_power (MajP ((n + 1),(abs i))) >= abs i by Def1;
then  2 to_power (MajP ((n + 1),(abs i))) >= - i by A7, ABSVALUE:def_1;
then  (2 to_power (MajP ((n + 1),(abs i)))) + i >= (- i) + i by XREAL_1:6;
then  abs ((2 to_power (MajP ((n + 1),(abs i)))) + i) = (2 to_power ((MajP (n,(abs i))) + m)) + i by A6, ABSVALUE:def_1
.= ((2 to_power (MajP (n,(abs i)))) * (2 to_power m)) + i by POWER:27 ;
then A9: (abs ((2 to_power (MajP ((n + 1),(abs i)))) + i)) mod (2 to_power (MajP (n,(abs i)))) = ((((2 to_power (MajP (n,(abs i)))) * (2 to_power m)) mod (2 to_power (MajP (n,(abs i))))) + (i mod (2 to_power (MajP (n,(abs i)))))) mod (2 to_power (MajP (n,(abs i)))) by NAT_D:66
.= (i mod (2 to_power (MajP (n,(abs i))))) mod (2 to_power (MajP (n,(abs i)))) by A8 ;
A10: (2 to_power (MajP (n,(abs i)))) mod (2 to_power (MajP (n,(abs i)))) = 0 by NAT_D:25;
 j + (- 1) >= 1 + (- 1) by A1, XREAL_1:6;
then  j -' 1 = j - 1 by XREAL_0:def_2;
then A11: j -' 1 < n by A2, XREAL_1:146, XXREAL_0:2;
 MajP (n,(abs i)) >= n by Def1;
then A12: j -' 1 < MajP (n,(abs i)) by A11, XXREAL_0:2;
 2 to_power (MajP (n,(abs i))) >= abs i by Def1;
then  2 to_power (MajP (n,(abs i))) >= - i by A7, ABSVALUE:def_1;
then  (2 to_power (MajP (n,(abs i)))) + i >= (- i) + i by XREAL_1:6;
then  abs ((2 to_power (MajP (n,(abs i)))) + i) = (2 to_power (MajP (n,(abs i)))) + i by ABSVALUE:def_1;
then (abs ((2 to_power (MajP (n,(abs i)))) + i)) mod (2 to_power (MajP (n,(abs i)))) = (((2 to_power (MajP (n,(abs i)))) mod (2 to_power (MajP (n,(abs i))))) + (i mod (2 to_power (MajP (n,(abs i)))))) mod (2 to_power (MajP (n,(abs i)))) by NAT_D:66
.= (i mod (2 to_power (MajP (n,(abs i))))) mod (2 to_power (MajP (n,(abs i)))) by A10 ;
hence  ((abs ((2 to_power (MajP ((n + 1),(abs i)))) + i)) div (2 to_power (j -' 1))) mod 2 = ((abs ((2 to_power (MajP (n,(abs i)))) + i)) div (2 to_power (j -' 1))) mod 2 by A9, A12, Lm3; ::_thesis: verum
end;
percases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; ::_thesis: (2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j
then reconsider i = i as Element of NAT by INT_1:3;
A13: (2sComplement (n,i)) /. j = (n -BinarySequence (abs i)) /. j by Def2
.= (n -BinarySequence i) /. j by ABSVALUE:def_1
.= IFEQ (((i div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A3, BINARI_3:def_1 ;
(2sComplement ((n + 1),i)) /. j = ((n + 1) -BinarySequence (abs i)) /. j by Def2
.= ((n + 1) -BinarySequence i) /. j by ABSVALUE:def_1
.= IFEQ (((i div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A4, BINARI_3:def_1 ;
hence  (2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j by A13; ::_thesis: verum
end;
supposeA14: i < 0 ; ::_thesis: (2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j
then A15: (2sComplement (n,i)) /. j = (n -BinarySequence (abs ((2 to_power (MajP (n,(abs i)))) + i))) /. j by Def2
.= IFEQ ((((abs ((2 to_power (MajP (n,(abs i)))) + i)) div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A3, BINARI_3:def_1 ;
(2sComplement ((n + 1),i)) /. j = ((n + 1) -BinarySequence (abs ((2 to_power (MajP ((n + 1),(abs i)))) + i))) /. j by A14, Def2
.= IFEQ ((((abs ((2 to_power (MajP ((n + 1),(abs i)))) + i)) div (2 to_power (j -' 1))) mod 2),0,FALSE,TRUE) by A4, BINARI_3:def_1 ;
hence  (2sComplement ((n + 1),i)) /. j = (2sComplement (n,i)) /. j by A5, A14, A15; ::_thesis: verum
end;
end;
end;

theorem Th33: :: BINARI_4:33
for m being Nat
for i being Integer ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*>
proof
let m be Nat; ::_thesis: for i being Integer ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*>
let i be Integer; ::_thesis: ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*>
consider a being Element of m -tuples_on BOOLEAN, b being Element of BOOLEAN  such that
A1: 2sComplement ((m + 1),i) = a ^ <*b*> by FINSEQ_2:117;
now__::_thesis:_ex_x_being_Element_of_BOOLEAN_st_2sComplement_((m_+_1),i)_=_(2sComplement_(m,i))_^_<*x*>
percases ( m > 0 or m = 0 ) ;
suppose m > 0 ; ::_thesis: ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*>
then reconsider m = m as non empty Nat ;
 for j being Nat st j in Seg m holds
(2sComplement (m,i)) . j = a . j
proof
A2: len (2sComplement (m,i)) = m by CARD_1:def_7;
let j be Nat; ::_thesis: ( j in Seg m implies (2sComplement (m,i)) . j = a . j )
assume A3: j in Seg m ; ::_thesis: (2sComplement (m,i)) . j = a . j
reconsider j = j as Nat ;
A4: 1 <= j by A3, FINSEQ_1:1;
 len a = m by CARD_1:def_7;
then A5: j in dom a by A3, FINSEQ_1:def_3;
A6: j <= m by A3, FINSEQ_1:1;
 m <= m + 1 by NAT_1:11;
then  ( len (2sComplement ((m + 1),i)) = m + 1 & j <= m + 1 ) by A6, CARD_1:def_7, XXREAL_0:2;
then (2sComplement ((m + 1),i)) . j = (2sComplement ((m + 1),i)) /. j by A4, FINSEQ_4:15
.= (2sComplement (m,i)) /. j by A4, A6, Th32
.= (2sComplement (m,i)) . j by A2, A4, A6, FINSEQ_4:15 ;
hence  (2sComplement (m,i)) . j = a . j by A1, A5, FINSEQ_1:def_7; ::_thesis: verum
end;
then  a = 2sComplement (m,i) by FINSEQ_2:119;
hence  ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*> by A1; ::_thesis: verum
end;
supposeA7: m = 0 ; ::_thesis: ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*>
then consider c being Element of BOOLEAN  such that
A8: 2sComplement ((m + 1),i) = <*c*> by FINSEQ_2:97;
A9: 2sComplement ((m + 1),i) = {} ^ <*c*> by A8, FINSEQ_1:34;
 2sComplement (m,i) = {} by A7;
hence  ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*> by A9; ::_thesis: verum
end;
end;
end;
hence  ex x being Element of BOOLEAN st 2sComplement ((m + 1),i) = (2sComplement (m,i)) ^ <*x*> ; ::_thesis: verum
end;

theorem :: BINARI_4:34
for m, l being Nat ex x being Element of BOOLEAN st (m + 1) -BinarySequence l = (m -BinarySequence l) ^ <*x*>
proof
let m, l be Nat; ::_thesis: ex x being Element of BOOLEAN st (m + 1) -BinarySequence l = (m -BinarySequence l) ^ <*x*>
consider x being Element of BOOLEAN  such that
A1: 2sComplement ((m + 1),l) = (2sComplement (m,l)) ^ <*x*> by Th33;
A2: abs l = l by ABSVALUE:def_1;
then (m + 1) -BinarySequence l = (2sComplement (m,l)) ^ <*x*> by A1, Def2
.= (m -BinarySequence l) ^ <*x*> by A2, Def2 ;
hence  ex x being Element of BOOLEAN st (m + 1) -BinarySequence l = (m -BinarySequence l) ^ <*x*> ; ::_thesis: verum
end;

theorem Th35: :: BINARI_4:35
for h, i being Integer
for n being non empty Nat st - (2 to_power n) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds
(carry ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i)))) /. (n + 1) = TRUE
proof
let h, i be Integer; ::_thesis: for n being non empty Nat st - (2 to_power n) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds
(carry ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i)))) /. (n + 1) = TRUE
defpred S1[ Nat] means ( - (2 to_power $1) <= h + i & h < 0 & i < 0 & - (2 to_power ($1 -' 1)) <= h & - (2 to_power ($1 -' 1)) <= i implies (carry ((2sComplement (($1 + 1),h)),(2sComplement (($1 + 1),i)))) /. ($1 + 1) = TRUE );
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  S1[n] ; ::_thesis: S1[n + 1]
assume that
 - (2 to_power (n + 1)) <= h + i and
A2: h < 0 and
A3: i < 0 and
A4: - (2 to_power ((n + 1) -' 1)) <= h and
A5: - (2 to_power ((n + 1) -' 1)) <= i ; ::_thesis: (carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. ((n + 1) + 1) = TRUE
set H1 = 2sComplement (((n + 1) + 1),h);
set I1 = 2sComplement (((n + 1) + 1),i);
set H = 2sComplement ((n + 1),h);
set I = 2sComplement ((n + 1),i);
set T = TRUE ;
set N = n + 1;
A6: (n + 1) -' 1 = (n + 1) - 1 by XREAL_0:def_2;
then A7: 2 to_power ((n + 1) -' 1) < 2 to_power (n + 1) by POWER:39, XREAL_1:146;
(2 to_power ((n + 1) -' 1)) + (2 to_power ((n + 1) -' 1)) = 2 * (2 to_power ((n + 1) -' 1))
.= (2 to_power 1) * (2 to_power ((n + 1) -' 1)) by POWER:25
.= 2 to_power (0 + (n + 1)) by A6, POWER:27 ;
then A8: (- (2 to_power ((n + 1) -' 1))) + (2 to_power (n + 1)) = 2 to_power ((n + 1) -' 1) ;
then A9: 2 to_power ((n + 1) -' 1) <= (2 to_power (n + 1)) + h by A4, XREAL_1:6;
A10: 2 to_power ((n + 1) -' 1) <= (2 to_power (n + 1)) + i by A5, A8, XREAL_1:6;
A11: (2 to_power (n + 1)) + i < 0 + (2 to_power (n + 1)) by A3, XREAL_1:8;
 (n + 1) - 1 = n ;
then A12: (n + 1) -' 1 = n by XREAL_0:def_2;
 ( 0 <= (2 to_power (n + 1)) + h & 0 <= (2 to_power (n + 1)) + i ) by A4, A5, A8, XREAL_1:6;
then reconsider NH = (2 to_power (n + 1)) + h, NI = (2 to_power (n + 1)) + i as Element of NAT by INT_1:3;
A13: len ((n + 1) -BinarySequence NI) = n + 1 by CARD_1:def_7;
A14: 1 <= n + 1 by NAT_1:11;
then A15: ( (2sComplement (((n + 1) + 1),h)) /. (n + 1) = (2sComplement ((n + 1),h)) /. (n + 1) & (2sComplement (((n + 1) + 1),i)) /. (n + 1) = (2sComplement ((n + 1),i)) /. (n + 1) ) by Th32;
A16: (2 to_power (n + 1)) + h < 0 + (2 to_power (n + 1)) by A2, XREAL_1:8;
A17: n + 1 < (n + 1) + 1 by NAT_1:13;
 abs i = - i by A3, ABSVALUE:def_1;
then  - (- (2 to_power ((n + 1) -' 1))) >= abs i by A5, XREAL_1:24;
then  MajP ((n + 1),(abs i)) = n + 1 by A7, Th24, XXREAL_0:2;
then A18: (2sComplement ((n + 1),i)) /. (n + 1) = ((n + 1) -BinarySequence (abs NI)) /. (n + 1) by A3, Def2
.= ((n + 1) -BinarySequence NI) /. (n + 1) by ABSVALUE:def_1
.= ((n + 1) -BinarySequence NI) . (n + 1) by A14, A13, FINSEQ_4:15
.= TRUE by A12, A10, A11, BINARI_3:29 ;
A19: len ((n + 1) -BinarySequence NH) = n + 1 by CARD_1:def_7;
 abs h = - h by A2, ABSVALUE:def_1;
then  - (- (2 to_power ((n + 1) -' 1))) >= abs h by A4, XREAL_1:24;
then  MajP ((n + 1),(abs h)) = n + 1 by A7, Th24, XXREAL_0:2;
then (2sComplement ((n + 1),h)) /. (n + 1) = ((n + 1) -BinarySequence (abs NH)) /. (n + 1) by A2, Def2
.= ((n + 1) -BinarySequence NH) /. (n + 1) by ABSVALUE:def_1
.= ((n + 1) -BinarySequence NH) . (n + 1) by A14, A19, FINSEQ_4:15
.= TRUE by A12, A9, A16, BINARI_3:29 ;
then (carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. ((n + 1) + 1) = ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. (n + 1)))) 'or' (TRUE '&' ((carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. (n + 1))) by A14, A18, A15, A17, BINARITH:def_2
.= TRUE 'or' ((carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. (n + 1)) ;
hence  (carry ((2sComplement (((n + 1) + 1),h)),(2sComplement (((n + 1) + 1),i)))) /. ((n + 1) + 1) = TRUE ; ::_thesis: verum
end;
A20: S1[1]
proof
 1 -' 1 = 1 - 1 by XREAL_0:def_2;
then 3 div (2 to_power (1 -' 1)) = (1 + 2) div 1 by POWER:24
.= 3 by NAT_2:4 ;
then A21: (3 div (2 to_power (1 -' 1))) mod 2 = (2 + 1) mod 2
.= ((2 mod 2) + 1) mod 2 by NAT_D:22
.= (0 + 1) mod 2 by NAT_D:25
.= 1 by PEPIN:5 ;
A22: (- 2) + 1 = - 1 ;
set H = 2sComplement (2,h);
set I = 2sComplement (2,i);
set T = TRUE ;
assume that
A23: - (2 to_power 1) <= h + i and
A24: h < 0 and
A25: i < 0 and
 - (2 to_power (1 -' 1)) <= h and
 - (2 to_power (1 -' 1)) <= i ; ::_thesis: (carry ((2sComplement ((1 + 1),h)),(2sComplement ((1 + 1),i)))) /. (1 + 1) = TRUE
A26: i <= - 1 by A25, INT_1:8;
 - (2 to_power 1) < h by A23, A24, A25, Th9;
then  - 2 < h by POWER:25;
then A27: - 1 <= h by A22, INT_1:7;
 - (2 to_power 1) < i by A23, A24, A25, Th9;
then  - 2 < i by POWER:25;
then  - 1 <= i by A22, INT_1:7;
then A28: i = - 1 by A26, XXREAL_0:1;
A29: 1 in Seg 2 by FINSEQ_1:1;
A30: 2 to_power 2 = 2 |^ (1 + 1) by POWER:41
.= (2 |^ 1) + (2 |^ 1) by PEPIN:29
.= (2 to_power 1) + (2 |^ 1) by POWER:41
.= (2 to_power 1) + (2 to_power 1) by POWER:41
.= 2 + (2 to_power 1) by POWER:25
.= 2 + 2 by POWER:25 ;
A31: 2 to_power 2 > 2 to_power 0 by POWER:39;
A32: h <= - 1 by A24, INT_1:8;
then A33: h = - 1 by A27, XXREAL_0:1;
then  abs h = - (- 1) by ABSVALUE:def_1;
then  2 to_power 0 = abs h by POWER:24;
then  MajP (2,(abs h)) = 2 by A31, Th24;
then  abs ((2 to_power (MajP (2,(abs h)))) + h) = abs (4 + (- 1)) by A27, A32, A30, XXREAL_0:1
.= 3 by ABSVALUE:def_1 ;
then (2sComplement (2,h)) /. 1 = (2 -BinarySequence 3) /. 1 by A24, Def2
.= IFEQ (1,0,FALSE,TRUE) by A21, A29, BINARI_3:def_1
.= TRUE by FUNCOP_1:def_8 ;
then (carry ((2sComplement (2,h)),(2sComplement (2,i)))) /. (1 + 1) = ((TRUE '&' TRUE) 'or' (TRUE '&' ((carry ((2sComplement (2,h)),(2sComplement (2,i)))) /. 1))) 'or' (TRUE '&' ((carry ((2sComplement (2,h)),(2sComplement (2,i)))) /. 1)) by A33, A28, BINARITH:def_2
.= TRUE 'or' ((carry ((2sComplement (2,h)),(2sComplement (2,i)))) /. 1) ;
hence  (carry ((2sComplement ((1 + 1),h)),(2sComplement ((1 + 1),i)))) /. (1 + 1) = TRUE ; ::_thesis: verum
end;
thus  for n being non empty Nat holds S1[n] from NAT_1:sch_10(A20, A1); ::_thesis: verum
end;

theorem :: BINARI_4:36
for h, i being Integer
for n being non empty Nat st h + i <= (2 to_power (n -' 1)) - 1 & h >= 0 & i >= 0 holds
Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i
proof
let h, i be Integer; ::_thesis: for n being non empty Nat st h + i <= (2 to_power (n -' 1)) - 1 & h >= 0 & i >= 0 holds
Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i
let n be non empty Nat; ::_thesis: ( h + i <= (2 to_power (n -' 1)) - 1 & h >= 0 & i >= 0 implies Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i )
assume that
A1: h + i <= (2 to_power (n -' 1)) - 1 and
A2: ( h >= 0 & i >= 0 ) ; ::_thesis: Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i
reconsider h = h, i = i as Element of NAT by A2, INT_1:3;
A3: 2sComplement (n,i) = n -BinarySequence (abs i) by Def2
.= n -BinarySequence i by ABSVALUE:def_1 ;
2sComplement (n,h) = n -BinarySequence (abs h) by Def2
.= n -BinarySequence h by ABSVALUE:def_1 ;
hence  Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i by A1, A3, Th14; ::_thesis: verum
end;

theorem :: BINARI_4:37
for h, i being Integer
for n being non empty Nat st - (2 to_power ((n + 1) -' 1)) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds
Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i
proof
let h, i be Integer; ::_thesis: for n being non empty Nat st - (2 to_power ((n + 1) -' 1)) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i holds
Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i
let n be non empty Nat; ::_thesis: ( - (2 to_power ((n + 1) -' 1)) <= h + i & h < 0 & i < 0 & - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i implies Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i )
assume that
A1: - (2 to_power ((n + 1) -' 1)) <= h + i and
A2: h < 0 and
A3: i < 0 and
A4: ( - (2 to_power (n -' 1)) <= h & - (2 to_power (n -' 1)) <= i ) ; ::_thesis: Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i
A5: (2 to_power (n + 1)) + (- (2 to_power n)) = (- (2 to_power n)) + ((2 to_power 1) * (2 to_power n)) by POWER:27
.= (- (2 to_power n)) + (2 * (2 to_power n)) by POWER:25
.= 2 to_power n ;
 (n + 1) - 1 = n ;
then A6: - (2 to_power n) <= h + i by A1, XREAL_0:def_2;
then A7: - (2 to_power n) < h by A2, A3, Th9;
then A8: 2 to_power n <= (2 to_power (n + 1)) + h by A5, XREAL_1:6;
A9: - (2 to_power n) < i by A2, A3, A6, Th9;
then A10: 0 <= (2 to_power (n + 1)) + i by A5, XREAL_1:6;
 0 <= (2 to_power (n + 1)) + h by A7, A5, XREAL_1:6;
then reconsider NH = (2 to_power (n + 1)) + h, NI = (2 to_power (n + 1)) + i as Element of NAT by A10, INT_1:3;
A11: 1 <= n + 1 by NAT_1:11;
set H = 2sComplement (n,h);
set I = 2sComplement (n,i);
set H1 = 2sComplement ((n + 1),h);
set I1 = 2sComplement ((n + 1),i);
set F = FALSE ;
set T = TRUE ;
 n < n + 1 by XREAL_1:29;
then A12: 2 to_power n < 2 to_power (n + 1) by POWER:39;
A13: ( ex a being Element of BOOLEAN st 2sComplement ((n + 1),h) = (2sComplement (n,h)) ^ <*a*> & ex a being Element of BOOLEAN st 2sComplement ((n + 1),i) = (2sComplement (n,i)) ^ <*a*> ) by Th33;
A14: (2 to_power (n + 1)) + h < (2 to_power (n + 1)) + 0 by A2, XREAL_1:8;
 - h < - (- (2 to_power n)) by A7, XREAL_1:24;
then  abs h < 2 to_power n by A2, ABSVALUE:def_1;
then A15: MajP ((n + 1),(abs h)) = n + 1 by A12, Th24, XXREAL_0:2;
then A16: 2sComplement ((n + 1),h) = (n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h)) by A2, Def2
.= (n + 1) -BinarySequence NH by ABSVALUE:def_1 ;
 len (2sComplement ((n + 1),h)) = n + 1 by CARD_1:def_7;
then A17: (2sComplement ((n + 1),h)) /. (n + 1) = (2sComplement ((n + 1),h)) . (n + 1) by A11, FINSEQ_4:15
.= ((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h))) . (n + 1) by A2, A15, Def2
.= ((n + 1) -BinarySequence NH) . (n + 1) by ABSVALUE:def_1
.= TRUE by A14, A8, BINARI_3:29 ;
A18: 2 to_power n <= (2 to_power (n + 1)) + i by A9, A5, XREAL_1:6;
A19: (2 to_power (n + 1)) + i < (2 to_power (n + 1)) + 0 by A3, XREAL_1:8;
 - i < - (- (2 to_power n)) by A9, XREAL_1:24;
then  abs i < 2 to_power n by A3, ABSVALUE:def_1;
then A20: MajP ((n + 1),(abs i)) = n + 1 by A12, Th24, XXREAL_0:2;
then A21: 2sComplement ((n + 1),i) = (n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i)) by A3, Def2
.= (n + 1) -BinarySequence NI by ABSVALUE:def_1 ;
 len (2sComplement ((n + 1),i)) = n + 1 by CARD_1:def_7;
then A22: (2sComplement ((n + 1),i)) /. (n + 1) = (2sComplement ((n + 1),i)) . (n + 1) by A11, FINSEQ_4:15
.= ((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i))) . (n + 1) by A3, A20, Def2
.= ((n + 1) -BinarySequence NI) . (n + 1) by ABSVALUE:def_1
.= TRUE by A19, A18, BINARI_3:29 ;
then A23: Intval (2sComplement ((n + 1),i)) = (Absval (2sComplement ((n + 1),i))) - (2 to_power (n + 1)) by BINARI_2:def_3
.= NI - (2 to_power (n + 1)) by A19, A21, BINARI_3:35
.= i ;
A24: (carry ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i)))) /. (n + 1) = TRUE by A2, A3, A4, A6, Th35;
then A25: Int_add_ovfl ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i))) = (FALSE '&' ('not' TRUE)) '&' TRUE by A17, A22, BINARI_2:def_4
.= FALSE ;
A26: Int_add_udfl ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i))) = (TRUE '&' TRUE) '&' ('not' TRUE) by A17, A22, A24, BINARI_2:def_5
.= FALSE ;
Intval (2sComplement ((n + 1),h)) = (Absval (2sComplement ((n + 1),h))) - (2 to_power (n + 1)) by A17, BINARI_2:def_3
.= NH - (2 to_power (n + 1)) by A14, A16, BINARI_3:35
.= h ;
then  Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = ((h + i) - (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1))))) + (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1)))) by A13, A23, A25, A26, BINARI_2:12
.= ((h + i) - 0) + 0 ;
hence  Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i ; ::_thesis: verum
end;

theorem :: BINARI_4:38
for h, i being Integer
for n being non empty Nat st - (2 to_power (n -' 1)) <= h & h <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i & i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) holds
Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i
proof
let h, i be Integer; ::_thesis: for n being non empty Nat st - (2 to_power (n -' 1)) <= h & h <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i & i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) holds
Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i
defpred S1[ non empty Nat] means ( - (2 to_power ($1 -' 1)) <= h & h <= (2 to_power ($1 -' 1)) - 1 & - (2 to_power ($1 -' 1)) <= i & i <= (2 to_power ($1 -' 1)) - 1 & - (2 to_power ($1 -' 1)) <= h + i & h + i <= (2 to_power ($1 -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) implies Intval ((2sComplement ($1,h)) + (2sComplement ($1,i))) = h + i );
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  ( - (2 to_power (n -' 1)) <= h & h <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= i & i <= (2 to_power (n -' 1)) - 1 & - (2 to_power (n -' 1)) <= h + i & h + i <= (2 to_power (n -' 1)) - 1 & ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) implies Intval ((2sComplement (n,h)) + (2sComplement (n,i))) = h + i ) ; ::_thesis: S1[n + 1]
assume that
A2: - (2 to_power ((n + 1) -' 1)) <= h and
A3: h <= (2 to_power ((n + 1) -' 1)) - 1 and
A4: - (2 to_power ((n + 1) -' 1)) <= i and
A5: i <= (2 to_power ((n + 1) -' 1)) - 1 and
 - (2 to_power ((n + 1) -' 1)) <= h + i and
 h + i <= (2 to_power ((n + 1) -' 1)) - 1 and
A6: ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) ; ::_thesis: Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i
set H = 2sComplement (n,h);
set I = 2sComplement (n,i);
set H1 = 2sComplement ((n + 1),h);
set I1 = 2sComplement ((n + 1),i);
set n2 = 2 to_power n;
set F = FALSE ;
set T = TRUE ;
A7: (n + 1) - 1 = n ;
then A8: - (2 to_power n) <= h by A2, XREAL_0:def_2;
A9: i <= (2 to_power n) - 1 by A5, A7, XREAL_0:def_2;
A10: ( ex a being Element of BOOLEAN st 2sComplement ((n + 1),h) = (2sComplement (n,h)) ^ <*a*> & ex b being Element of BOOLEAN st 2sComplement ((n + 1),i) = (2sComplement (n,i)) ^ <*b*> ) by Th33;
A11: - (2 to_power n) <= i by A4, A7, XREAL_0:def_2;
A12: h <= (2 to_power n) - 1 by A3, A7, XREAL_0:def_2;
now__::_thesis:_Intval_((2sComplement_((n_+_1),h))_+_(2sComplement_((n_+_1),i)))_=_h_+_i
percases ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) by A6;
supposeA13: ( h >= 0 & i < 0 ) ; ::_thesis: Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i
(2 to_power (n + 1)) + (- (2 to_power n)) = (- (2 to_power n)) + ((2 to_power 1) * (2 to_power n)) by POWER:27
.= (- (2 to_power n)) + (2 * (2 to_power n)) by POWER:25
.= 2 to_power n ;
then A14: 2 to_power n <= (2 to_power (n + 1)) + i by A11, XREAL_1:6;
then reconsider NI = (2 to_power (n + 1)) + i as Element of NAT by INT_1:3;
 n < n + 1 by XREAL_1:29;
then A15: 2 to_power n < 2 to_power (n + 1) by POWER:39;
 abs i = - i by A13, ABSVALUE:def_1;
then  abs i <= - (- (2 to_power n)) by A11, XREAL_1:24;
then A16: MajP ((n + 1),(abs i)) = n + 1 by A15, Th24, XXREAL_0:2;
then A17: 2sComplement ((n + 1),i) = (n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i)) by A13, Def2
.= (n + 1) -BinarySequence NI by ABSVALUE:def_1 ;
A18: (2 to_power (n + 1)) + i < (2 to_power (n + 1)) + 0 by A13, XREAL_1:8;
reconsider h = h as Element of NAT by A13, INT_1:3;
A19: h < 2 to_power n by A12, XREAL_1:146, XXREAL_0:2;
A20: 2sComplement ((n + 1),h) = (n + 1) -BinarySequence (abs h) by Def2
.= (n + 1) -BinarySequence h by ABSVALUE:def_1 ;
then A21: (2sComplement ((n + 1),h)) . (n + 1) = FALSE by A19, BINARI_3:26;
 n + 0 < n + 1 by XREAL_1:8;
then  2 to_power n < 2 to_power (n + 1) by POWER:39;
then A22: h < 2 to_power (n + 1) by A19, XXREAL_0:2;
A23: 1 <= n + 1 by NAT_1:11;
 len (2sComplement ((n + 1),i)) = n + 1 by CARD_1:def_7;
then A24: (2sComplement ((n + 1),i)) /. (n + 1) = (2sComplement ((n + 1),i)) . (n + 1) by A23, FINSEQ_4:15;
A25: (2sComplement ((n + 1),i)) . (n + 1) = ((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + i))) . (n + 1) by A13, A16, Def2
.= ((n + 1) -BinarySequence NI) . (n + 1) by ABSVALUE:def_1
.= TRUE by A18, A14, BINARI_3:29 ;
then A26: Intval (2sComplement ((n + 1),i)) = (Absval (2sComplement ((n + 1),i))) - (2 to_power (n + 1)) by A24, BINARI_2:def_3
.= NI - (2 to_power (n + 1)) by A18, A17, BINARI_3:35
.= i ;
 len (2sComplement ((n + 1),h)) = n + 1 by CARD_1:def_7;
then A27: (2sComplement ((n + 1),h)) /. (n + 1) = (2sComplement ((n + 1),h)) . (n + 1) by A23, FINSEQ_4:15;
then A28: Int_add_ovfl ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i))) = (('not' FALSE) '&' ('not' TRUE)) '&' ((carry ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i)))) /. (n + 1)) by A21, A25, A24, BINARI_2:def_4
.= FALSE ;
A29: Int_add_udfl ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i))) = (FALSE '&' TRUE) '&' ('not' ((carry ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i)))) /. (n + 1))) by A21, A25, A27, A24, BINARI_2:def_5
.= FALSE ;
Intval (2sComplement ((n + 1),h)) = Absval (2sComplement ((n + 1),h)) by A21, A27, BINARI_2:def_3
.= h by A20, A22, BINARI_3:35 ;
then  Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = ((h + i) - (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1))))) + (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1)))) by A10, A26, A28, A29, BINARI_2:12
.= ((h + i) - 0) + 0 ;
hence  Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i ; ::_thesis: verum
end;
supposeA30: ( h < 0 & i >= 0 ) ; ::_thesis: Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i
(2 to_power (n + 1)) + (- (2 to_power n)) = (- (2 to_power n)) + ((2 to_power 1) * (2 to_power n)) by POWER:27
.= (- (2 to_power n)) + (2 * (2 to_power n)) by POWER:25
.= 2 to_power n ;
then A31: 2 to_power n <= (2 to_power (n + 1)) + h by A8, XREAL_1:6;
then reconsider NH = (2 to_power (n + 1)) + h as Element of NAT by INT_1:3;
 n < n + 1 by XREAL_1:29;
then A32: 2 to_power n < 2 to_power (n + 1) by POWER:39;
 abs h = - h by A30, ABSVALUE:def_1;
then  abs h <= - (- (2 to_power n)) by A8, XREAL_1:24;
then A33: MajP ((n + 1),(abs h)) = n + 1 by A32, Th24, XXREAL_0:2;
then A34: 2sComplement ((n + 1),h) = (n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h)) by A30, Def2
.= (n + 1) -BinarySequence NH by ABSVALUE:def_1 ;
A35: (2 to_power (n + 1)) + h < (2 to_power (n + 1)) + 0 by A30, XREAL_1:8;
reconsider i = i as Element of NAT by A30, INT_1:3;
A36: i < 2 to_power n by A9, XREAL_1:146, XXREAL_0:2;
A37: 2sComplement ((n + 1),i) = (n + 1) -BinarySequence (abs i) by Def2
.= (n + 1) -BinarySequence i by ABSVALUE:def_1 ;
then A38: (2sComplement ((n + 1),i)) . (n + 1) = FALSE by A36, BINARI_3:26;
 n + 0 < n + 1 by XREAL_1:8;
then  2 to_power n < 2 to_power (n + 1) by POWER:39;
then A39: i < 2 to_power (n + 1) by A36, XXREAL_0:2;
A40: 1 <= n + 1 by NAT_1:11;
 len (2sComplement ((n + 1),h)) = n + 1 by CARD_1:def_7;
then A41: (2sComplement ((n + 1),h)) /. (n + 1) = (2sComplement ((n + 1),h)) . (n + 1) by A40, FINSEQ_4:15;
A42: (2sComplement ((n + 1),h)) . (n + 1) = ((n + 1) -BinarySequence (abs ((2 to_power (n + 1)) + h))) . (n + 1) by A30, A33, Def2
.= ((n + 1) -BinarySequence NH) . (n + 1) by ABSVALUE:def_1
.= TRUE by A35, A31, BINARI_3:29 ;
then A43: Intval (2sComplement ((n + 1),h)) = (Absval (2sComplement ((n + 1),h))) - (2 to_power (n + 1)) by A41, BINARI_2:def_3
.= NH - (2 to_power (n + 1)) by A35, A34, BINARI_3:35
.= h ;
 len (2sComplement ((n + 1),i)) = n + 1 by CARD_1:def_7;
then A44: (2sComplement ((n + 1),i)) /. (n + 1) = (2sComplement ((n + 1),i)) . (n + 1) by A40, FINSEQ_4:15;
then A45: Int_add_ovfl ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i))) = (('not' TRUE) '&' ('not' FALSE)) '&' ((carry ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i)))) /. (n + 1)) by A38, A42, A41, BINARI_2:def_4
.= FALSE ;
A46: Int_add_udfl ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i))) = (TRUE '&' FALSE) '&' ('not' ((carry ((2sComplement ((n + 1),h)),(2sComplement ((n + 1),i)))) /. (n + 1))) by A38, A42, A44, A41, BINARI_2:def_5
.= FALSE ;
Intval (2sComplement ((n + 1),i)) = Absval (2sComplement ((n + 1),i)) by A38, A44, BINARI_2:def_3
.= i by A37, A39, BINARI_3:35 ;
then  Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = ((h + i) - (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1))))) + (IFEQ (FALSE,FALSE,0,(2 to_power (n + 1)))) by A10, A43, A45, A46, BINARI_2:12
.= ((h + i) - 0) + 0 ;
hence  Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i ; ::_thesis: verum
end;
end;
end;
hence  Intval ((2sComplement ((n + 1),h)) + (2sComplement ((n + 1),i))) = h + i ; ::_thesis: verum
end;
A47: S1[1]
proof
A48: abs (- 1) = - (- 1) by ABSVALUE:def_1
.= 1 ;
 ( 2 to_power 1 = 2 & ( for k being Nat st 2 to_power k >= 1 & k >= 1 holds
k >= 1 ) ) by POWER:25;
then  MajP (1,(abs (- 1))) = 1 by A48, Def1;
then A49: 2sComplement (1,(- 1)) = 1 -BinarySequence (abs ((2 to_power 1) + (- 1))) by Def2
.= 1 -BinarySequence (abs (2 + (- 1))) by POWER:25
.= 1 -BinarySequence 1 by ABSVALUE:def_1
.= (0 + 1) -BinarySequence (2 to_power 0) by POWER:24
.= (0* 0) ^ <*1*> by BINARI_3:28
.= <*TRUE*> by FINSEQ_1:34 ;
assume that
A50: - (2 to_power (1 -' 1)) <= h and
A51: h <= (2 to_power (1 -' 1)) - 1 and
A52: - (2 to_power (1 -' 1)) <= i and
A53: i <= (2 to_power (1 -' 1)) - 1 and
 - (2 to_power (1 -' 1)) <= h + i and
 h + i <= (2 to_power (1 -' 1)) - 1 and
A54: ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) ; ::_thesis: Intval ((2sComplement (1,h)) + (2sComplement (1,i))) = h + i
A55: 1 -' 1 = 1 - 1 by XREAL_0:def_2
.= 0 ;
then A56: h <= 1 - 1 by A51, POWER:24;
A57: i <= 1 - 1 by A53, A55, POWER:24;
A58: - 1 <= i by A52, A55, POWER:24;
A59: 2sComplement (1,0) = 1 -BinarySequence (abs 0) by Def2
.= 1 -BinarySequence 0 by ABSVALUE:def_1
.= 0* 1 by BINARI_3:25
.= <*FALSE*> by FINSEQ_2:59 ;
A60: - 1 <= h by A50, A55, POWER:24;
now__::_thesis:_Intval_((2sComplement_(1,h))_+_(2sComplement_(1,i)))_=_h_+_i
percases ( ( h >= 0 & i < 0 ) or ( h < 0 & i >= 0 ) ) by A54;
supposeA61: ( h >= 0 & i < 0 ) ; ::_thesis: Intval ((2sComplement (1,h)) + (2sComplement (1,i))) = h + i
then  i <= - 1 by INT_1:8;
then A62: i = - 1 by A58, XXREAL_0:1;
 h = 0 by A56, A61;
hence  Intval ((2sComplement (1,h)) + (2sComplement (1,i))) = h + i by A59, A49, A62, Th15, BINARI_3:17; ::_thesis: verum
end;
supposeA63: ( h < 0 & i >= 0 ) ; ::_thesis: Intval ((2sComplement (1,h)) + (2sComplement (1,i))) = h + i
then  h <= - 1 by INT_1:8;
then A64: h = - 1 by A60, XXREAL_0:1;
 i = 0 by A57, A63;
hence  Intval ((2sComplement (1,h)) + (2sComplement (1,i))) = h + i by A59, A49, A64, Th15, BINARI_3:17; ::_thesis: verum
end;
end;
end;
hence  Intval ((2sComplement (1,h)) + (2sComplement (1,i))) = h + i ; ::_thesis: verum
end;
thus  for n being non empty Nat holds S1[n] from NAT_1:sch_10(A47, A1); ::_thesis: verum
end;