:: A Representation of Integers by Binary Arithmetics
:: and Addition of Integers
::  by Hisayoshi Kunimune and Yatsuka Nakamura
::
:: Received January 30, 2003
:: Copyright (c) 2003 Association of Mizar Users

environ

 vocabularies INT_1, MIDSP_3, MARGREL1, FINSEQ_1, CQC_LANG, POWER, ABSVALUE,
      BINARITH, BINARI_2, BINARI_3, ARYTM_1, NAT_1, BINARI_4, EUCLID, ARYTM_3,
      FINSEQ_4, FUNCT_1, BOOLE, RELAT_1, VECTSP_1, ZF_LANG, GROUP_1, ARYTM;
 notations INT_1, XBOOLEAN, MARGREL1, FINSEQ_1, FUNCOP_1, POWER, BINARITH,
      BINARI_2, BINARI_3, SERIES_1, NUMBERS, XCMPLX_0, XXREAL_0, XBOOLE_0,
      NAT_1, BINOP_2, EUCLID, TARSKI, PARTFUN1, FUNCT_1, RELAT_1, ZFMISC_1,
      INT_2, FINSEQOP, NEWTON, SUBSET_1;
 constructors PARTFUN1, XXREAL_0, REAL_1, NAT_1, NAT_D, FINSEQOP, NEWTON,
      SERIES_1, BINARITH, BINARI_2, EUCLID, BINARI_3, BINOP_2;
 registrations XBOOLE_0, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
      MEMBERED, XBOOLEAN, MARGREL1, SERIES_1, VALUED_0, FINSEQ_1;
 requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
 definitions FINSEQ_2, XBOOLEAN, EUCLID;
 theorems POWER, NAT_1, PRE_FF, ABSVALUE, REAL_1, BINARI_3, INT_1, BINARITH,
      NAT_2, BINARI_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCOP_1, RVSUM_1,
      FUNCT_2, ZFMISC_1, INT_3, EULER_2, PEPIN, PREPOWER, XREAL_1, XXREAL_0,
      ORDINAL1, XBOOLEAN, NAT_D, VALUED_1;
 schemes NAT_1;

begin :: Preliminaries

reserve n for non empty Nat,
  j,k,l,m for Nat,
  g,h,i for Integer;

theorem Th1:
  for m being Nat st m > 0 holds m * 2 >= m + 1
proof
  let m be Nat;
  assume m > 0;
  then m >= 0 + 1 by INT_1:20;
  then m >= 1 & m * 2 = m + m;
  hence thesis by XREAL_1:8;
end;

theorem Th2:
  for m being Nat holds 2 to_power m >= m
proof
  defpred P[Nat] means 2 to_power $1 >= $1;
A1: P[0];
A2: for m being Nat st P[m] holds P[m+1]
  proof
    let m be Nat such that
A3: 2 to_power m >= m;
    per cases;
    suppose
A4:   m = 0;
      then 2 to_power (m+1) = 2 by POWER:30;
      hence thesis by A4;
    end;
    suppose
A5:   m > 0;
      reconsider m2 = 2 to_power m as Nat;
A6:   m2 * 2 >= m * 2 by A3,NAT_1:4;
      2 to_power 1 = 2 by POWER:30;
      then
A7:   2 to_power (m+1) >= m * 2 by A6,POWER:32;
      m * 2 >= m + 1 by A5,Th1;
      hence thesis by A7,XXREAL_0:2;
    end;
  end;
  thus for m being Nat holds P[m] from NAT_1:sch 2(A1,A2);
end;

theorem
  for m be Nat holds 0*m + 0*m = 0*m
proof
  let m be Nat;
A1: dom addreal = [:REAL,REAL:] by FUNCT_2:def 1;
  rng 0*m c= REAL by FINSEQ_1:def 4;
  then
A2: [:rng 0*m, rng 0*m:] c= dom addreal by A1,ZFMISC_1:119;
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:84
    .= Seg m by FUNCOP_1:19;
A4: dom(0*m) = Seg m by FUNCOP_1:19;
  for k be Nat st k in dom(0*m) holds (0*m).k = (0*m+0*m).k
  proof
    let k be Nat such that
A5: k in dom(0*m);
    (0*m).k = 0 by A4,A5,FUNCOP_1:13;
    then (0*m+0*m).k = 0 + 0 by A3,A4,A5,VALUED_1:def 1;
    hence thesis by A4,A5,FUNCOP_1:13;
  end;
  hence thesis by A3,FUNCOP_1:19,FINSEQ_1:17;
end;

theorem Th4:
  for k,m,l be Nat holds
  k <= l & l <= m implies k = l or (k + 1 <= l & l <= m)
proof
  defpred P[Nat] means for m,l be Nat holds
  $1 <= l & l <= m implies $1 = l or ($1 + 1 <= l & l <= m);
A1: P[0] by NAT_1:13;
A2: for k be Nat st P[k] holds P[k+1]
  proof
    let k be Nat such that P[k];
    let m,l be Nat;
    assume that
A3: k+1 <= l and
A4: l <= m;
    k+1 = l or k+1 < l by A3,XXREAL_0:1;
    hence thesis by A4,NAT_1:13;
  end;
  thus for k being Nat holds P[k] from NAT_1:sch 2(A1,A2);
end;

theorem Th5:
  for n be non empty Nat holds
  for x,y be Tuple of n,BOOLEAN st x = 0*n & y = 0*n holds carry(x,y) = 0*n
proof
  let n be non empty Nat;
  let x,y be Tuple of n,BOOLEAN such that
A1: x = 0*n & y = 0*n;
  len carry(x,y) = n by FINSEQ_2:109;
  then 1 <= len carry(x,y) by NAT_1:14;
  then
A2: carry(x,y).1 = carry(x,y)/.1 by FINSEQ_4:24
    .= 0 by BINARITH:def 5;
A3: for j be Nat st 1 < j & j <= n holds carry(x,y).j = 0
  proof
    let j be Nat such that
A4: 1 < j & j <= n;
    reconsider k = j - 1 as Element of NAT by A4,INT_1:18;
    k + 1 = j;
    then
A5: 1 <= k & k < n & j = k + 1 by A4,NAT_1:13;
    then
A6: k in Seg n & k <= len x & k <= len y by FINSEQ_1:3,FINSEQ_2:109;
    len(0*n) = n by FINSEQ_2:69;
    then
A7: x/.k = (0*n).k by A1,A5,FINSEQ_4:24
      .= FALSE by A6,FUNCOP_1:13;
    len carry(x,y) = n by FINSEQ_2:109;
    then carry(x,y).j = carry(x,y)/.j by A4,FINSEQ_4:24
      .= FALSE '&' FALSE 'or' FALSE '&' (carry(x,y)/.k) 'or'
    FALSE '&' (carry(x,y)/.k) by A1,A5,A7,BINARITH:def 5
      .= FALSE;
    hence thesis;
  end;
  for l be Nat st l in Seg n holds carry(x,y).l = (0*n).l
  proof
    let l be Nat such that
A8: l in Seg n;
A9: 1 <= l & l <= n by A8,FINSEQ_1:3;
A10: (0*n).l = 0 by A8,FUNCOP_1:13;
    per cases by A9,Th4;
    suppose l = 1;
      hence thesis by A2,A8,FUNCOP_1:13;
    end;
    suppose 1 + 1 <= l & l <= n;
      then 1 < l & l <= n by NAT_1:13;
      hence thesis by A3,A10;
    end;
  end;
  hence thesis by A1,FINSEQ_2:139;
end;

theorem
  for n be non empty Nat holds
  for x,y be Tuple of n,BOOLEAN st x = 0*n & y = 0*n holds x + y = 0*n
proof
  let n be non empty Nat;
  let x,y be Tuple of n,BOOLEAN such that
A1: x = 0*n & y = 0*n;
  for k be Nat st k in Seg n holds (x+y).k = (0*n).k
  proof
    let k be Nat such that
A2: k in Seg n;
    reconsider k as Nat;
A3: (0*n).k = FALSE by A2,FUNCOP_1:13;
    len x = n & len y = n & len carry(x,y) = n & len(x+y) = n by FINSEQ_2:109;
    then
A4: 1 <= k & k <= len x & k <= len carry(x,y) & k <= len(x+y)
    by A2,FINSEQ_1:3;
    then
A5: y/.k = FALSE by A1,A3,FINSEQ_4:24;
A6: carry(x,y)/.k = carry(x,y).k by A4,FINSEQ_4:24
      .= FALSE by A1,A3,Th5;
    (x+y).k = (x+y)/.k by A4,FINSEQ_4:24
      .= FALSE 'xor' FALSE by A1,A2,A5,A6,BINARITH:def 8
      .= FALSE;
    hence thesis by A2,FUNCOP_1:13;
  end;
  hence thesis by A1,FINSEQ_2:139;
end;

theorem
  for n be non empty Nat
  for F be Tuple of n,BOOLEAN st F = 0*n holds Intval F = 0
proof
  let n be non empty Nat;
  let F be Tuple of n,BOOLEAN such that
A1: F = 0*n;
A2: 1 <= n & n <= len F by FINSEQ_2:109,NAT_1:14;
  then
A3: n in Seg n by FINSEQ_1:3;
  F/.n = F.n by A2,FINSEQ_4:24
    .= FALSE by A1,A3,FUNCOP_1:13;
  then Intval F = Absval F by BINARI_2:def 3;
  hence thesis by A1,BINARI_3:7;
end;

theorem Th8:
  l + m <= k - 1 implies l < k & m < k
proof
  assume
A1: l + m <= k - 1;
  k <= k + m by NAT_1:11;
  then
A2: k - m <= k + m - m by XREAL_1:11;
A3: l + m - m <= k - 1 - m by A1,XREAL_1:11;
  k - 1 - m = k - m - 1;
  then k - 1 - m < k by A2,XREAL_1:148,XXREAL_0:2;
  hence l < k by A3,XXREAL_0:2;
  k <= k + l by NAT_1:11;
  then
A4: k - l <= k + l - l by XREAL_1:11;
A5: m + l - l <= k - 1 - l by A1,XREAL_1:11;
  k - 1 - l = k - l - 1;
  then k - 1 - l < k by A4,XREAL_1:148,XXREAL_0:2;
  hence thesis by A5,XXREAL_0:2;
end;

theorem Th9:
  g <= h + i & h < 0 & i < 0 implies g < h & g < i
proof
  assume
A1: g <= h + i & h < 0 & i < 0;
  then g - i <= h + i - i by XREAL_1:11;
  then i + (g + -i) < 0 + h by A1,XREAL_1:10;
  hence g < h;
  g - h <= i + h - h by A1,XREAL_1:11;
  then h + (g + -h) < 0 + i by A1,XREAL_1:10;
  hence thesis;
end;

theorem Th10:
  l + m <= 2 to_power n - 1 implies
  add_ovfl(n-BinarySequence(l),n-BinarySequence(m)) = FALSE
proof
  assume
A1: l + m <= 2 to_power n - 1;
  set L = n-BinarySequence(l), M = n-BinarySequence(m);
  assume
A2: add_ovfl(L,M) <> FALSE;
A3: l < 2 to_power n & m < 2 to_power n by A1,Th8;
A4: IFEQ(add_ovfl(L,M),FALSE,0,2 to_power n) = 2 to_power n
  by A2,FUNCOP_1:def 8;
A5: Absval(L+M) + IFEQ(add_ovfl(L,M),FALSE,0,2 to_power n)
  = Absval(L)+Absval(M) by BINARITH:47
    .= l + Absval(M) by A3,BINARI_3:36
    .= l + m by A3,BINARI_3:36;
  Absval(L+M) + 2 to_power n >= 2 to_power n by NAT_1:11;
  hence contradiction by A1,A4,A5,XREAL_1:148,XXREAL_0:2;
end;

theorem Th11:
  for n be non empty Nat, l,m be 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, l,m be Nat such that
A1: l + m <= 2 to_power n - 1;
  set L = n-BinarySequence(l), M = n-BinarySequence(m);
A2: l < 2 to_power n & m < 2 to_power n by A1,Th8;
  add_ovfl(L,M) = FALSE by A1,Th10;
  then L,M are_summable by BINARITH:def 10;
  then Absval(L+M) = Absval(L) + Absval(M) by BINARITH:48
    .= l + Absval(M) by A2,BINARI_3:36;
  hence thesis by A2,BINARI_3:36;
end;

theorem Th12:
  for n be non empty Nat holds
  (for z be Tuple of n,BOOLEAN st z/.n = TRUE holds
  Absval(z) >= 2 to_power (n-'1))
proof
  defpred P[Nat] means
  (for z be Tuple of $1,BOOLEAN st z/.$1 = TRUE holds
  Absval(z) >= 2 to_power ($1-'1));
A1: P[1]
  proof
    let z be Tuple of 1,BOOLEAN such that
A2: z/.1 = TRUE;
A3: len z = 1 by FINSEQ_2:109;
    then z.1 = z/.1 by FINSEQ_4:24;
    then z = <*TRUE*> by A2,A3,FINSEQ_1:57;
    then
A4: Absval(z) = 1 by BINARITH:42;
    2 to_power (1-'1) = 2 to_power (1-1) by BINARITH:def 3;
    hence thesis by A4,POWER:29;
  end;
A5: for n be non empty Nat st P[n] holds P[n+1]
  proof
    let n be non empty Nat such that P[n];
    let z be Tuple of (n+1),BOOLEAN such that
A6: z/.(n+1) = TRUE;
    consider x be (Tuple of n,BOOLEAN), a be Element of BOOLEAN such that
A7: z = x^<*a*> by FINSEQ_2:137;
A8: n + 1 >= 1 by NAT_1:11;
    then n + 1 - 1 >= 1 - 1 by XREAL_1:11;
    then
A9: n + 1 -' 1 = n by BINARITH:def 3;
    len z = n+1 by FINSEQ_2:109;
    then
A10: z/.(n+1) = (x^<*a*>).(n+1) by A7,A8,FINSEQ_4:24
      .= a by FINSEQ_2:136;
    Absval(z) = Absval(x) + IFEQ(a,FALSE,0,2 to_power n) by A7,BINARITH:46
      .= Absval(x) + 2 to_power n by A6,A10,FUNCOP_1:def 8;
    hence thesis by A9,NAT_1:11;
  end;
  thus for n being non empty Nat holds P[n] from NAT_1:sch 10(A1,A5);
end;

theorem Th13:
  l + m <= 2 to_power (n-'1) - 1 implies
  carry(n-BinarySequence(l),n-BinarySequence(m))/.n = FALSE
proof
  assume
A1: l + m <= 2 to_power (n-'1) - 1;
  set L = n-BinarySequence(l), M = n-BinarySequence(m), F = FALSE, T = TRUE;
  assume not(carry(L,M)/.n = F);
  then
A2: carry(L,M)/.n = T by XBOOLEAN:def 3;
A3: l < 2 to_power (n-'1) & m < 2 to_power (n-'1) by A1,Th8;
  1 <= n by NAT_1:14;
  then
A4: n in Seg n by FINSEQ_1:3;
  then
A5: L/.n = IFEQ((l div 2 to_power (n-'1)) mod 2,0,F,T) by BINARI_3:def 1
    .= IFEQ(0 mod 2,0,F,T) by A3,NAT_D:27
    .= IFEQ(0,0,F,T) by NAT_D:26
    .= F by FUNCOP_1:def 8;
A6: M/.n = IFEQ((m div 2 to_power (n-'1)) mod 2,0,F,T) by A4,BINARI_3:def 1
    .= IFEQ(0 mod 2,0,F,T) by A3,NAT_D:27
    .= IFEQ(0,0,F,T) by NAT_D:26
    .= F by FUNCOP_1:def 8;
  n >= 1 by NAT_1:14;
  then n-1 >= 1-1 by XREAL_1:11;
  then n-'1 = n - 1 by BINARITH:def 3;
  then 2 to_power (n-'1) < 2 to_power n by POWER:44,XREAL_1:148;
  then
A7: 2 to_power (n-'1) - 1 < 2 to_power n - 1 by REAL_1:92;
  (L+M)/.n = F 'xor' F 'xor' T by A2,A4,A5,A6,BINARITH:def 8
    .= T;
  then
A8: Absval(L+M) >= 2 to_power (n-'1) by Th12;
  l + m < 2 to_power (n-'1) by A1,XREAL_1:148,XXREAL_0:2;
  hence contradiction by A1,A7,A8,Th11,XXREAL_0:2;
end;

theorem Th14:
  for n be non empty Nat st l + m <= 2 to_power (n-'1) - 1 holds
  Intval(n-BinarySequence(l) + n-BinarySequence(m)) = l + m
proof
  let n be non empty Nat such that
A1: l + m <= 2 to_power (n-'1) - 1;
  set L = n-BinarySequence(l), M = n-BinarySequence(m), F = FALSE, T = TRUE;
A2: l < 2 to_power (n-'1) & m < 2 to_power (n-'1) by A1,Th8;
  1 <= n by NAT_1:14;
  then
A3: n in Seg n by FINSEQ_1:3;
  then
A4: L/.n = IFEQ((l div 2 to_power (n-'1)) mod 2,0,F,T) by BINARI_3:def 1
    .= IFEQ(0 mod 2,0,F,T) by A2,NAT_D:27
    .= IFEQ(0,0,F,T) by NAT_D:26
    .= F by FUNCOP_1:def 8;
  M/.n = IFEQ((m div 2 to_power (n-'1)) mod 2,0,F,T) by A3,BINARI_3:def 1
    .= IFEQ(0 mod 2,0,F,T) by A2,NAT_D:27
    .= IFEQ(0,0,F,T) by NAT_D:26
    .= F by FUNCOP_1:def 8;
  then (L+M)/.n = F 'xor' F 'xor' (carry(L,M)/.n) by A3,A4,BINARITH:def 8
    .= F by A1,Th13;
  then
A5: Intval(L+M) = Absval(L+M) by BINARI_2:def 3;
  n >= 1 by NAT_1:14;
  then n-1 >= 1-1 by XREAL_1:11;
  then n-'1 = n - 1 by BINARITH:def 3;
  then 2 to_power (n-'1) < 2 to_power n by POWER:44,XREAL_1:148;
  then 2 to_power (n-'1) - 1 < 2 to_power n - 1 by REAL_1:92;
  hence thesis by A1,A5,Th11,XXREAL_0:2;
end;

theorem Th15:
  for z be Tuple of 1,BOOLEAN st z=<*TRUE*> holds Intval(z) = -1
proof
  let z be Tuple of 1,BOOLEAN such that
A1: z = <*TRUE*>;
  len z = 1 by FINSEQ_2:109;
  then z/.1 = z.1 by FINSEQ_4:24
    .= TRUE by A1,FINSEQ_1:57;
  then Intval(z) = Absval(z) - 2 to_power 1 by BINARI_2:def 3
    .= 1 - 2 to_power 1 by A1,BINARITH:42
    .= 1 - (1 + 1) by POWER:30
    .= 0 - 1;
  hence thesis;
end;

theorem
  for z be Tuple of 1,BOOLEAN st z=<*FALSE*> holds Intval(z) = 0
proof
  let z be Tuple of 1,BOOLEAN such that
A1: z = <*FALSE*>;
  len z = 1 by FINSEQ_2:109;
  then z/.1 = z.1 by FINSEQ_4:24
    .= FALSE by A1,FINSEQ_1:57;
  then Intval(z) = Absval(z) by BINARI_2:def 3;
  hence thesis by A1,BINARITH:41;
end;

theorem
  for x be boolean set holds TRUE 'or' x = TRUE;

theorem
  for n be non empty Nat holds 0 <= 2 to_power (n-'1) - 1 &
  -(2 to_power (n-'1)) <= 0
proof
  defpred P[Nat] means
  0 <= 2 to_power ($1-'1) - 1 & -(2 to_power ($1-'1)) <= 0;
  1 - 1 = 0;
  then 2 to_power (1-'1) = 2 to_power 0 by BINARITH:def 3
    .= 1 by POWER:29;
  then
A1: P[1];
A2: for k be non empty Nat st P[k] holds P[k+1]
  proof
    let k be non empty Nat such that
A3: 0 <= 2 to_power (k-'1) - 1 & -(2 to_power (k-'1)) <= 0;
    (k+1)-'1 = k by BINARITH:39;
    then 2 to_power (k-'1) < 2 to_power ((k+1)-'1) by NAT_2:11,POWER:44;
    hence thesis by A3,XREAL_1:11;
  end;
  thus for n being non empty Nat holds P[n]
  from NAT_1:sch 10(A1,A2);
end;

theorem
  for x,y be Tuple of n,BOOLEAN st x = 0*n & y = 0*n holds x,y are_summable
proof
  let x,y be Tuple of n,BOOLEAN such that
A1: x = 0*n & y = 0*n;
A2: 1 <= n & len x = n by FINSEQ_2:109,NAT_1:14;
  then
A3: n in Seg n by FINSEQ_1:3;
  x/.n = (0*n).n by A1,A2,FINSEQ_4:24
    .= FALSE by A3,FUNCOP_1:13;
  then add_ovfl(x,y) = FALSE '&' FALSE 'or' FALSE '&' (carry(x,y)/.n) 'or'
  FALSE '&' (carry(x,y)/.n) by A1,BINARITH:def 9
    .= FALSE;
  hence thesis by BINARITH:def 10;
end;

theorem Th20:
  (i*n) mod n = 0
proof
  (i*n) mod n = ((i mod n) * (n mod n)) mod n by INT_3:15
    .= ((i mod n) * 0) mod n by NAT_D:25
    .= 0 mod n;
  hence thesis by NAT_D:26;
end;

begin :: Majorant Power

definition
  let m, j be Nat;
  func MajP(m, j) -> Nat means
  :Def1:
  2 to_power it >= j & it >= m &
  for k be Nat st 2 to_power k >= j & k >= m holds k >= it;
  existence
  proof
    per cases;
    suppose
A2:   2 to_power m >= j;
      for k be Nat st 2 to_power k >= j & k >= m holds k >= m;
      hence thesis by A2;
    end;
    suppose
A3:   2 to_power m < j;
      defpred P[Nat] means 2 to_power $1 >= j & $1 >= m;
      2 to_power m >= m by Th2;
      then 2 to_power j >= j & j >= m by A3,Th2,XXREAL_0:2;
      then
A4:   ex k be Nat st P[k];
      ex k be Nat st P[k] &
      for l be Nat st P[l] holds l >= k from NAT_1:sch 5(A4);
     hence thesis;
    end;
  end;
  uniqueness
  proof
    let p, q be Nat such that
A6: 2 to_power p >= j & p >= m &
    for k be Nat st 2 to_power k >= j & k >= m holds k >= p and
A7: 2 to_power q >= j & q >= m &
    for k be Nat st 2 to_power k >= j & k >= m holds k >= q;
    p >= q & q >= p by A6,A7;
    hence thesis by XXREAL_0:1;
  end;
end;

theorem
  j >= k implies MajP(m, j) >= MajP(m, k)
proof
  assume
A1: j >= k;
  2 to_power MajP(m, j) >= j & MajP(m, j) >= m by Def1;
  then 2 to_power MajP(m, j) >= k & MajP(m, j) >= m by A1,XXREAL_0:2;
  hence thesis by Def1;
end;

theorem Th22:
  l >= m implies MajP(l,j) >= MajP(m,j)
proof
  assume
A1: l >= m;
A2: 2 to_power MajP(l,j) >= j & MajP(l,j) >= l by Def1;
  then MajP(l,j) >= m by A1,XXREAL_0:2;
  hence thesis by A2,Def1;
end;

theorem
  m >= 1 implies MajP(m, 1) = m
proof
  assume m >= 1;
  then
A1: 2 to_power m >= 1 & m >= m by POWER:40;
  for k be Nat st 2 to_power k >= 1 & k >= m holds k >= m;
  hence thesis by A1,Def1;
end;

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

theorem
  j > 2 to_power m implies MajP(m, j) > m
proof
  assume
A1: j > 2 to_power 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 thesis by PRE_FF:10;
end;

begin :: 2's Complement

definition
  let m be Nat;
  let i be Integer;
  func 2sComplement( m, i ) -> Tuple of m, BOOLEAN equals
  :Def2:
  m-BinarySequence( abs( (2 to_power MajP(m,abs(i))) + i ) ) if i < 0
  otherwise m-BinarySequence( abs(i) );
  correctness;
end;

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

theorem
  for i be Integer st i <= 2 to_power (n-'1) - 1 &
  -(2 to_power (n-'1)) <= i holds Intval( 2sComplement( n, i ) ) = i
proof
  let i such that
A1: i <= 2 to_power (n-'1) - 1 & -(2 to_power (n-'1)) <= i;
A2: n >= 1 by NAT_1:14;
  now per cases;
    suppose i >= 0;
      then reconsider i as Element of NAT by INT_1:16;
A3:   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:8;
      then
A4:   i < 2 to_power (n-'1) by NAT_1:13;
      n >= 1 by NAT_1:14;
      then n - 1 >= 1 - 1 by XREAL_1:11;
      then n-'1 = n - 1 by BINARITH:def 3;
      then 2 to_power (n-'1) < 2 to_power n by POWER:44,XREAL_1:148;
      then i < 2 to_power n by A4,XXREAL_0:2;
      then
A5:   Absval(n-BinarySequence i) = i by BINARI_3:36;
      1 <= n by NAT_1:14;
      then n in Seg n by FINSEQ_1:3;
      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 A4,NAT_D:27
        .= IFEQ(0,0,FALSE,TRUE) by NAT_D:26
        .= FALSE by FUNCOP_1:def 8;
      hence thesis by A3,A5,BINARI_2:def 3;
    end;
    suppose
A6:   i < 0;
      then abs(i) = -i by ABSVALUE:def 1;
      then
A7:   abs(i) <= --2 to_power (n-'1) by A1,XREAL_1:26;
A8:   2 to_power n >= 2 to_power (n-'1) by NAT_2:11,POWER:44;
      then -(2 to_power n) <= -(2 to_power (n-'1)) by XREAL_1:26;
      then -(2 to_power n) <= i by A1,XXREAL_0:2;
      then -(2 to_power n) - i <= i-i by XREAL_1:11;
      then -(2 to_power n + i) <= 0;
      then 2 to_power n + i >= -0 by XREAL_1:26;
      then reconsider k = 2 to_power n + i as Element of NAT by INT_1:16;
      MajP(n,abs(i)) = n by A7,A8,Th24,XXREAL_0:2;
      then
A9:   2sComplement(n,i) = n-BinarySequence(abs(k)) by A6,Def2
        .= n-BinarySequence(k) by ABSVALUE:def 1;
A10:  2 to_power n + i < 2 to_power n + 0 by A6,XREAL_1:8;
      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:12
        .= 2*(2 to_power (n-'1)) - (2 to_power (n-'1)) by POWER:30
        .= 2 to_power (n-'1);
      then
A11:  k >= 2 to_power (n-'1) by A1,XREAL_1:8;
      k < 2 to_power n + 0 by A6,XREAL_1:10;
      then k < (2 to_power 1) * (2 to_power (n-'1)) by NAT_1:14,NAT_2:12;
      then k < 2*(2 to_power (n-'1)) by POWER:30;
      then
A12:  k < 2 to_power (n-'1) + (2 to_power (n-'1));
      n in Seg n by A2,FINSEQ_1:3;
      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 A11,A12,NAT_2:22
        .= 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 A10,BINARI_3:36
        .= 0 + i;
      hence thesis;
    end;
  end;
  hence thesis;
end;

Lm1: k mod n = l mod n & k > l implies ex s be Integer st k = l + s*n
proof
  assume
A1: k mod n = l mod n & k > l;
A2: l = (l div n)*n + (l mod n) by NAT_D:2;
A3: k = (k div n)*n + (l mod n) by A1,NAT_D:2;
  consider m be Nat such that
A4: k = l + m by A1,NAT_1:10;
  m mod n = (((k div n) - (l div n))*n) mod n by A2,A3,A4
    .= 0 by Th20;
  then (l+m) div n = (l div n) + (m div n) by NAT_D:19;
  then
A5: k = ((l div n) + (m div n))*n + (l mod n) by A1,A4,NAT_D:2
    .= (m div n)*n + ((l div n)*n + (l mod n))
    .= (m div n)*n + l by NAT_D:2;
  take m div n;
  thus thesis by A5;
end;

Lm2: k mod n = l mod n implies ex s be Integer st k = l + s*n
proof
  assume
A1: k mod n = l mod n;
  now per cases by XXREAL_0:1;
    suppose
A2:   k = l;
      set s = 0;
      k = l + s*n by A2;
      hence thesis;
    end;
    suppose
A3:   k > l or l > k;
      now per cases by A3;
        suppose k > l;
          hence thesis by A1,Lm1;
        end;
        suppose k < l;
          then consider t be Integer such that
A4:       l = k + t*n by A1,Lm1;
          k = l + (-t)*n by A4;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
  end;
  hence thesis;
end;

Lm3: for k,l,m be 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 k,l,m be Nat such that
A1: m < n & k mod 2 to_power n = l mod 2 to_power n;
  2 to_power n = 2 |^ n by POWER:46;
  then 2 to_power n is non empty by PREPOWER:12;
  then consider s be Integer such that
A2: k = l + s*(2 to_power n) by A1,Lm2;
  consider j be Nat such that
A3: n = m + j by A1,NAT_1:10;
  reconsider j as Nat;
  set M = 2 to_power m, J = 2 to_power j;
  reconsider L = l as Integer;
A4: M > 0 by POWER:39;
  m + -m < n + -m by A1,XREAL_1:10;
  then 0 + 1 < j + 1 by A3,XREAL_1:10;
  then 1 <= j by NAT_1:13;
  then 2 to_power 1 divides 2 to_power j by NAT_2:13;
  then 2 divides 2 to_power j by POWER:30;
  then J mod 2 = 0 by PEPIN:6;
  then
A5: (s*J) mod 2 = ((s mod 2) * 0) mod 2 by INT_3:15
    .= 0 by NAT_D:26;
  k div M = (l + s*(J*M)) div M by A2,A3,POWER:32
    .= (l + s*J*M) div M
    .= (l div M) + s*J by A4,INT_3:8;
  then (k div M) mod 2 = ((L div M) mod 2 + 0) mod 2 by A5,INT_3:14
    .= (L div M) mod 2 by INT_3:13;
  hence thesis;
end;

Lm4: for h,i be 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 h,i be Integer such that
A1: h mod 2 to_power n = i mod 2 to_power n;
  reconsider M = 2 to_power MajP(n,abs h) as Integer;
  n <= MajP(n,abs h) by Def1;
  then consider x be Nat such that
A2: MajP(n,abs h) = n + x by NAT_1:10;
  reconsider x as Nat;
  M = (2 to_power n)*(2 to_power x) by A2,POWER:32;
  then
A3: 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:10
    .= (0 * (2 to_power x)) mod 2 to_power n by NAT_D:25
    .= 0 by NAT_D:26;
  reconsider L = 2 to_power MajP(n,abs i) as Integer;
  n <= MajP(n,abs i) by Def1;
  then consider y be Nat such that
A4: MajP(n,abs i) = n + y by NAT_1:10;
  reconsider y as Nat;
  L = (2 to_power n)*(2 to_power y) by A4,POWER:32;
  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:10
    .= (0 * (2 to_power y)) mod 2 to_power n by NAT_D:25
    .= 0 by NAT_D:26;
A6: (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 INT_3:14
    .= (h mod 2 to_power n) mod 2 to_power n by A3;
  (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 INT_3:14
    .= (i mod 2 to_power n) mod 2 to_power n by A5;
  hence thesis by A1,A6;
end;

Lm5: for h,i be 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 h,i be Integer such that
A1: h >= 0 & i >= 0 & h mod 2 to_power n = i mod 2 to_power n;
A2: 2sComplement(n,h) = n-BinarySequence(abs(h)) by A1,Def2;
A3: 2sComplement(n,i) = n-BinarySequence(abs(i)) by A1,Def2;
  for j be Nat st j in Seg n holds
  (n-BinarySequence(abs(h))).j = (n-BinarySequence(abs(i))).j
  proof
    let j be Nat such that
A4: j in Seg n;
    reconsider j as Nat;
A5: 1 <= j & j <= n by A4,FINSEQ_1:3;
    then j - 1 >= 1 - 1 by XREAL_1:11;
    then j-'1 = j - 1 by BINARITH:def 3;
    then
A6: j-'1 < n by A5,XREAL_1:148,XXREAL_0:2;
A7: abs h = h & abs i = i & 2 to_power n > 0 by A1,ABSVALUE:def 1,POWER:39;
A8: len(n-BinarySequence(abs(h))) = n &
    len(n-BinarySequence(abs(i))) = n by FINSEQ_2:109;
    then
A9: (n-BinarySequence(abs(h))).j =
    (n-BinarySequence(abs(h)))/.j by A5,FINSEQ_4:24
      .= IFEQ((abs(h) div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE)
    by A4,BINARI_3:def 1
      .= IFEQ((abs(i) div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE)
    by A1,A6,A7,Lm3;
    (n-BinarySequence(abs(i))).j =
    (n-BinarySequence(abs(i)))/.j by A5,A8,FINSEQ_4:24
      .= IFEQ((abs(i) div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE)
    by A4,BINARI_3:def 1;
    hence thesis by A9;
  end;
  hence thesis by A2,A3,FINSEQ_2:139;
end;

Lm6: for h,i be 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 h,i be Integer such that
A1: h < 0 & i < 0 & h mod 2 to_power n = i mod 2 to_power n;
A2: 2sComplement(n,h) =
  n-BinarySequence(abs((2 to_power MajP(n,abs(h)))+h)) by A1,Def2;
A3: 2sComplement(n,i) =
  n-BinarySequence(abs((2 to_power MajP(n,abs(i)))+i)) by A1,Def2;
  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:8;
  then reconsider H = 2 to_power MajP(n,abs h) + h as Element of NAT
  by INT_1:16;
  abs i = -i by A1,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:8;
  then reconsider I = 2 to_power MajP(n,abs i) + i as Element of NAT
  by INT_1:16;
A4: (H qua Nat) mod (2 to_power n)
  = (I qua Nat) mod (2 to_power n) by A1,Lm4;
  for j be Nat st j in Seg n holds
  (n-BinarySequence(abs H)).j = (n-BinarySequence(abs I)).j
  proof
    let j be Nat such that
A5: j in Seg n;
A6: 1 <= j & j <= n by A5,FINSEQ_1:3;
    reconsider j as Nat;
A7: len(n-BinarySequence(H)) = n &
    len(n-BinarySequence(I)) = n by FINSEQ_2:109;
    j - 1 >= 1 - 1 by A6,XREAL_1:11;
    then j-'1 = j - 1 by BINARITH:def 3;
    then
A8: j-'1 < n by A6,XREAL_1:148,XXREAL_0:2;
    abs H = H & abs I = I by ABSVALUE:def 1;
    then (n-BinarySequence(abs H)).j
    = (n-BinarySequence(H))/.j by A6,A7,FINSEQ_4:24
      .= IFEQ((H div (2 to_power (j-'1))) mod 2,0,FALSE,TRUE)
    by A5,BINARI_3:def 1
      .= IFEQ((I div (2 to_power (j-'1))) mod 2,0,FALSE,TRUE) by A4,A8,Lm3
      .= (n-BinarySequence(I))/.j by A5,BINARI_3:def 1
      .= (n-BinarySequence(I)).j by A6,A7,FINSEQ_4:24;
    hence thesis by ABSVALUE:def 1;
  end;
  hence thesis by A2,A3,FINSEQ_2:139;
end;

theorem
  for h,i be 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
  for h,i be 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 h,i be Integer such that
A1: ((h >= 0 & i >= 0) or (h < 0 & i < 0)) & h,i are_congruent_mod 2 to_power n
  ;
  h mod 2 to_power n = i mod 2 to_power n by A1,INT_3:12;
  hence thesis by A1,Lm5,Lm6;
end;

theorem Th30:
  for l,m be Nat st l mod 2 to_power n = m mod 2 to_power n holds
  n-BinarySequence(l) = n-BinarySequence(m)
proof
  let l,m be Nat such that
A1: l mod 2 to_power n = m mod 2 to_power n;
  abs l = l & abs m = m by ABSVALUE:def 1;
  then 2sComplement(n,l) = n-BinarySequence(l) &
  2sComplement(n,m) = n-BinarySequence(m) by Def2;
  hence thesis by A1,Lm5;
end;

theorem
  for l,m be Nat st l,m are_congruent_mod 2 to_power n holds
  n-BinarySequence(l) = n-BinarySequence(m)
proof
  let l,m be Nat such that
A1: l,m are_congruent_mod 2 to_power n;
  (l qua Integer) mod 2 to_power n
  = (m qua Integer) mod 2 to_power n by A1,INT_3:12;
  hence thesis by Th30;
end;

theorem Th32:
  for j be Nat st 1 <= j & j <= n holds
  2sComplement(n+1,i)/.j = 2sComplement(n,i)/.j
proof
  let j be Nat such that
A1: 1 <= j & j <= n;
A2: j in Seg n by A1,FINSEQ_1:3;
  n <= n+1 by NAT_1:11;
  then j <= n+1 by A1,XXREAL_0:2;
  then
A3: j in Seg (n+1) by A1,FINSEQ_1:3;
  set M = abs( (2 to_power MajP(n+1,abs(i))) + i );
  set N = abs( (2 to_power MajP(n,abs(i))) + i );
A4: i < 0 implies
  (M div 2 to_power (j-'1)) mod 2 = (N div 2 to_power (j-'1)) mod 2
  proof
    assume
A5: i < 0;
    MajP(n+1,abs(i)) >= MajP(n,abs(i)) by Th22,NAT_1:11;
    then consider m be Nat such that
A6: MajP(n+1,abs(i)) = MajP(n,abs(i)) + m by NAT_1:10;
    reconsider m as Nat;
    set P = MajP(n,abs(i));
    set Q = 2 to_power P;
    2 to_power (MajP(n+1,abs(i))) >= abs i by Def1;
    then 2 to_power (MajP(n+1,abs(i))) >= -i by A5,ABSVALUE:def 1;
    then 2 to_power (MajP(n+1,abs(i))) + i >= -i + i by XREAL_1:8;
    then
A7: M = 2 to_power (P+m) + i by A6,ABSVALUE:def 1
      .= (Q * 2 to_power m)+i by POWER:32;
A8: (Q * 2 to_power m qua Integer) mod Q = 0 by NAT_D:13;
A9: M mod Q = (((Q * 2 to_power m qua Integer) mod Q) +
    (i mod Q)) mod Q by A7,INT_3:14
      .= (i mod Q) mod Q by A8;
A10: (Q qua Integer) mod Q = 0 by NAT_D:25;
    Q >= abs i by Def1;
    then Q >= -i by A5,ABSVALUE:def 1;
    then Q + i >= -i + i by XREAL_1:8;
    then N = Q + i by ABSVALUE:def 1;
    then
A11: N mod Q = (((Q qua Integer) mod Q) + (i mod Q)) mod Q by INT_3:14
      .= (i mod Q) mod Q by A10;
A12: P >= n by Def1;
A13: j + -1 >= 1 + -1 by A1,XREAL_1:8;
    j -' 1 = j - 1 by A13,BINARITH:def 3;
    then j -' 1 < n by A1,XREAL_1:148,XXREAL_0:2;
    then j -' 1 < P by A12,XXREAL_0:2;
    hence thesis by A9,A11,Lm3;
  end;
  per cases;
  suppose i >= 0;
    then reconsider i as Element of NAT by INT_1:16;
A15: 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 A3,BINARI_3:def 1;
    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 A2,BINARI_3:def 1;
    hence thesis by A15;
  end;
  suppose
A16: i < 0;
    then
A17: 2sComplement(n+1,i)/.j = ((n+1)-BinarySequence(M))/.j by Def2

.= IFEQ((M div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A3,BINARI_3:def 1;
    2sComplement(n,i)/.j = (n-BinarySequence(N))/.j by A16,Def2

.= IFEQ((N div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A2,BINARI_3:def 1;
    hence thesis by A4,A16,A17;
  end;
end;

theorem Th33:
  ex x be Element of BOOLEAN st 2sComplement(m+1,i) = 2sComplement(m,i)^<*x*>
proof
  consider a be (Tuple of m,BOOLEAN), b be Element of BOOLEAN such that
A1: 2sComplement(m+1,i) = a^<*b*> by FINSEQ_2:137;
  now per cases;
    suppose m > 0;
      then reconsider m as non empty Nat;
      for j be Nat st j in Seg m holds 2sComplement(m,i).j = a.j
      proof
        let j be Nat such that
A2:     j in Seg m;
        reconsider j as Nat;
A3:     len 2sComplement(m+1,i) = m+1 & len 2sComplement(m,i) = m &
        len a = m by FINSEQ_2:109;
A4:     1 <= j & j <= m by A2,FINSEQ_1:3;
        m <= m + 1 by NAT_1:11;
        then j <= m + 1 by A4,XXREAL_0:2;
        then
A5:     2sComplement(m+1,i).j = 2sComplement(m+1,i)/.j by A3,A4,FINSEQ_4:24
          .= 2sComplement(m,i)/.j by A4,Th32
          .= 2sComplement(m,i).j by A3,A4,FINSEQ_4:24;
        j in dom a by A2,A3,FINSEQ_1:def 3;
        hence thesis by A1,A5,FINSEQ_1:def 7;
      end;
      then a = 2sComplement(m,i) by FINSEQ_2:139;
      hence thesis by A1;
    end;
    suppose
A6:   m = 0;
      then
A7:   2sComplement(m,i) = <*>BOOLEAN by FINSEQ_2:113
        .= {};
      reconsider E = {} as FinSequence by FINSEQ_1:14;
      consider c be Element of BOOLEAN such that
A8:   2sComplement(m+1,i) = <*c*> by A6,FINSEQ_2:117;
      2sComplement(m+1,i) = E^<*c*> by A8,FINSEQ_1:47;
      hence thesis by A7;
    end;
  end;
  hence thesis;
end;

theorem
  ex x be Element of BOOLEAN st
  (m+1)-BinarySequence(l) = (m-BinarySequence(l))^<*x*>
proof
  consider x be 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 thesis;
end;

theorem Th35:
  for n be non empty Nat holds
  -2 to_power n <= h+i & h < 0 & i < 0 &
  -2 to_power (n-'1) <= h & -2 to_power (n-'1) <= i implies
  carry(2sComplement(n+1,h),2sComplement(n+1,i))/.(n+1) = TRUE
proof
  defpred P[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: P[1]
  proof
    assume
A2: -2 to_power 1 <= h+i & h < 0 & i < 0 &
    -2 to_power (1-'1) <= h & -2 to_power (1-'1) <= i;
    then -2 to_power 1 < h & -2 to_power 1 < i by Th9;
    then
A3: -2 < h & -2 < i by POWER:30;
    -2+1 = -1;
    then
A4: -1 <= h & -1 <= i by A3,INT_1:20;
A5: h <= -1 & i <= -1 by A2,INT_1:21;
    then
A6: h = -1 & i = -1 by A4,XXREAL_0:1;
    then abs h = --1 & abs i = --1 by ABSVALUE:def 1;
    then 2 to_power 0 = abs h & 2 to_power 2 > 2 to_power 0 by POWER:29,44;
    then
A7: MajP(2,abs h) = 2 by Th24;
    2 to_power 2 = 2 |^ (1+1) by POWER:46
      .= 2 |^ 1 + 2 |^ 1 by PEPIN:30
      .= 2 to_power 1 + 2 |^ 1 by POWER:46
      .= 2 to_power 1 + 2 to_power 1 by POWER:46
      .= 2 + 2 to_power 1 by POWER:30
      .= 2 + 2 by POWER:30;
    then
A8: abs(2 to_power MajP(2,abs h) + h) = abs(4 + -1) by A4,A5,A7,XXREAL_0:1
      .= 3 by ABSVALUE:def 1;
    1-'1 = 1-1 by BINARITH:def 3;
    then 3 div 2 to_power (1-'1) = (1+2) div 1 by POWER:29
      .= 3 by NAT_2:6;
    then
A9: (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;
A10: 1 in Seg 2 by FINSEQ_1:3;
A11: (2sComplement(2,h))/.1 = (2-BinarySequence(3))/.1 by A2,A8,Def2
      .= IFEQ(1,0,FALSE,TRUE) by A9,A10,BINARI_3:def 1
      .= TRUE by FUNCOP_1:def 8;
    set H = 2sComplement(2,h), I = 2sComplement(2,i), T = TRUE;
    carry(H,I)/.(1+1)
    = T '&' T 'or' T '&' (carry(H,I)/.1) 'or' T '&' (carry(H,I)/.1)
    by A6,A11,BINARITH:def 5
      .= T 'or' (carry(H,I)/.1);
    hence thesis;
  end;
A12: for n be non empty Nat st P[n] holds P[n+1]
  proof
    let n be non empty Nat such that P[n];
    assume
A13: -2 to_power (n+1) <= h+i & h < 0 & i < 0 &
    -2 to_power (n+1-'1) <= h & -2 to_power (n+1-'1) <= i;
    set H1 = 2sComplement(n+1+1,h), I1 = 2sComplement(n+1+1,i),
    H = 2sComplement(n+1,h), I = 2sComplement(n+1,i), T = TRUE, N = n+1;
A14: N-1 = n;
A15: N-'1 = N-1 by BINARITH:def 3;
A16: N-'1 = n by A14,BINARITH:def 3;
A17: 2 to_power (N-'1) < 2 to_power N by A15,POWER:44,XREAL_1:148;
    2 to_power (N-'1) + 2 to_power (N-'1) = 2*(2 to_power (N-'1))
      .= (2 to_power 1)*(2 to_power (N-'1)) by POWER:30
      .= 2 to_power (0+N) by A15,POWER:32;
    then
A18: -2 to_power (N-'1) + 2 to_power N = 2 to_power (N-'1);
    abs h = -h & abs i = -i by A13,ABSVALUE:def 1;
    then --2 to_power (N-'1) >= abs h & --2 to_power (N-'1) >= abs i
    by A13,XREAL_1:26;
    then
A19: MajP(N,abs h) = N & MajP(N,abs i) = N by A17,Th24,XXREAL_0:2;
A20: 2 to_power (N-'1) <= 2 to_power N + h &
    2 to_power (N-'1) <= 2 to_power N + i by A13,A18,XREAL_1:8;
    0 <= 2 to_power N + h & 0 <= 2 to_power N + i by A13,A18,XREAL_1:8;
    then reconsider NH = 2 to_power N + h,
    NI = 2 to_power N + i as Element of NAT by INT_1:16;
A21: 1 <= N & len (N-BinarySequence(NH)) = N & len(N-BinarySequence(NI)) = N
    by FINSEQ_2:109,NAT_1:11;
A22: 2 to_power N + h < 0 + 2 to_power N &
    2 to_power N + i < 0 + 2 to_power N by A13,XREAL_1:10;
A23: H/.N = (N-BinarySequence(abs NH))/.N by A13,A19,Def2
      .= (N-BinarySequence(NH))/.N by ABSVALUE:def 1
      .= (N-BinarySequence(NH)).N by A21,FINSEQ_4:24
      .= T by A16,A20,A22,BINARI_3:30;
A24: I/.N = (N-BinarySequence(abs NI))/.N by A13,A19,Def2
      .= (N-BinarySequence(NI))/.N by ABSVALUE:def 1
      .= (N-BinarySequence(NI)).N by A21,FINSEQ_4:24
      .= T by A16,A20,A22,BINARI_3:30;
A25: H1/.N = H/.N & I1/.N = I/.N by A21,Th32;
    N < N+1 by NAT_1:13;
    then carry(H1,I1)/.(N+1) = T '&' T 'or' T '&' (carry(H1,I1)/.N) 'or'
    T '&' (carry(H1,I1)/.N) by A21,A23,A24,A25,BINARITH:def 5
      .= T 'or' (carry(H1,I1)/.N);
    hence thesis;
  end;
  thus for n being non empty Nat holds P[n]
  from NAT_1:sch 10(A1,A12);
end;

theorem
  for n be non empty Nat st
  -(2 to_power (n-'1)) <= h + i & h + i <= 2 to_power (n-'1) - 1 &
  h >= 0 & i >= 0 holds Intval(2sComplement(n,h) + 2sComplement(n,i)) = h+i
proof
  let n be non empty Nat such that
A1: -(2 to_power (n-'1)) <= h + i & h + i <= 2 to_power (n-'1) - 1 &
  h >= 0 & i >= 0;
  reconsider h,i as Element of NAT by A1,INT_1:16;
A2: 2sComplement(n,h) = n-BinarySequence(abs h) by Def2
    .= n-BinarySequence(h) by ABSVALUE:def 1;
  2sComplement(n,i) = n-BinarySequence(abs i) by Def2
    .= n-BinarySequence(i) by ABSVALUE:def 1;
  hence thesis by A1,A2,Th14;
end;

theorem
  for n be non empty Nat st
  -2 to_power ((n+1)-'1) <= h + i & h + i <= 2 to_power ((n+1)-'1) - 1 &
  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 n be non empty Nat such that
A1: -2 to_power ((n+1)-'1) <= h + i & h + i <= 2 to_power ((n+1)-'1) - 1 &
  h < 0 & i < 0 & -2 to_power (n-'1) <= h & -2 to_power (n-'1) <= i;
  set H = 2sComplement(n,h), I = 2sComplement(n,i),
  H1 = 2sComplement(n+1,h), I1 = 2sComplement(n+1,i), F = FALSE, T = TRUE;
  (n+1)-1 = n & n >= 0;
  then
A2: -2 to_power n <= h+i & h+i <= 2 to_power n - 1 by A1,BINARITH:def 3;
  then
A3: -2 to_power n < h & -2 to_power n < i by A1,Th9;
  then -h < --2 to_power n & -i < --2 to_power n by XREAL_1:26;
  then
A4: abs h < 2 to_power n & abs i < 2 to_power n by A1,ABSVALUE:def 1;
  n < n+1 by XREAL_1:31;
  then 2 to_power n < 2 to_power (n+1) by POWER:44;
  then
A5: MajP(n+1,abs h) = n+1 & MajP(n+1,abs i) = n+1 by A4,Th24,XXREAL_0:2;
A6: 2 to_power (n+1) + h < 2 to_power (n+1) + 0 &
  2 to_power (n+1) + i < 2 to_power (n+1) + 0 by A1,XREAL_1:10;
A7: 2 to_power (n+1) + -(2 to_power n)
  = -(2 to_power n) + ((2 to_power 1)*(2 to_power n)) by POWER:32
    .= -(2 to_power n) + 2*(2 to_power n) by POWER:30
    .= 2 to_power n;
  then
A8: 2 to_power n <= 2 to_power (n+1) + h &
  2 to_power n <= 2 to_power (n+1) + i by A3,XREAL_1:8;
  0 <= 2 to_power (n+1) + h & 0 <= 2 to_power (n+1) + i by A3,A7,XREAL_1:8;
  then reconsider NH = 2 to_power (n+1) + h,
  NI = 2 to_power (n+1) + i as Element of NAT by INT_1:16;
  consider a be Element of BOOLEAN such that
A9: H1 = H^<*a*> by Th33;
  consider a be Element of BOOLEAN such that
A10: I1 = I^<*a*> by Th33;
A11: len H1 = n + 1 & len I1 = n + 1 by FINSEQ_2:109;
A12: 1 <= n + 1 by NAT_1:11;
  then
A13: H1/.(n+1) = H1.(n+1) by A11,FINSEQ_4:24
    .= ((n+1)-BinarySequence(abs(2 to_power (n+1)+h))).(n+1) by A1,A5,Def2
    .= ((n+1)-BinarySequence(NH)).(n+1) by ABSVALUE:def 1
    .= T by A6,A8,BINARI_3:30;
A14: I1/.(n+1) = I1.(n+1) by A11,A12,FINSEQ_4:24
    .= ((n+1)-BinarySequence(abs(2 to_power (n+1)+i))).(n+1) by A1,A5,Def2
    .= ((n+1)-BinarySequence(NI)).(n+1) by ABSVALUE:def 1
    .= T by A6,A8,BINARI_3:30;
A15: H1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+h)) by A1,A5,Def2
    .= (n+1)-BinarySequence(NH) by ABSVALUE:def 1;
A16: I1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+i)) by A1,A5,Def2
    .= (n+1)-BinarySequence(NI) by ABSVALUE:def 1;
A17: Intval(H1) = Absval(H1) - 2 to_power (n+1) by A13,BINARI_2:def 3
    .= NH - 2 to_power (n+1) by A6,A15,BINARI_3:36
    .= h;
A18: Intval(I1) = Absval(I1) - 2 to_power (n+1) by A14,BINARI_2:def 3
    .= NI - 2 to_power (n+1) by A6,A16,BINARI_3:36
    .= i;
A19: carry(H1,I1)/.(n+1) = T by A1,A2,Th35;
  then
A20: Int_add_ovfl(H1,I1) = F '&' 'not' T '&' T by A13,A14,BINARI_2:def 4
    .= F;
  Int_add_udfl(H1,I1) = T '&' T '&' 'not' T by A13,A14,A19,BINARI_2:def 5
    .= F;
  then Intval(H1+I1) = h + i - IFEQ(F,F,0,2 to_power(n+1))
  + IFEQ(F,F,0,2 to_power(n+1)) by A9,A10,A17,A18,A20,BINARI_2:14
    .= h + i - 0 + 0;
  hence thesis;
end;

theorem
  for n be non empty Nat holds
  -(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
proof
  defpred P[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: P[1]
  proof
    assume
A2: -(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));
    1 -' 1 = 1 - 1 by BINARITH:def 3
      .= 0;
    then
A3: -1 <= h & h <= 1-1 & -1 <= i & i <= 1-1 &
    -1 <= h+i & h+i <= 1-1 by A2,POWER:29;
A4: 2sComplement(1,0) = 1-BinarySequence(abs 0) by Def2
      .= 1-BinarySequence(0) by ABSVALUE:def 1
      .= 0*1 by BINARI_3:26
      .= <* FALSE *> by FINSEQ_2:73;
A5: 2 to_power 1 = 2 & (for k be Nat st 2 to_power k >= 1 & k >= 1 holds
    k >= 1) by POWER:30;
    abs(-1) = --1 by ABSVALUE:def 1
      .= 1;
    then
A6: MajP(1,abs(-1)) = 1 by A5,Def1;
A7: 0*0 = {} by FINSEQ_2:72;
A8: 2sComplement(1,-1) = 1-BinarySequence(abs((2 to_power 1)+-1)) by A6,Def2
      .= 1-BinarySequence(abs(2+-1)) by POWER:30
      .= 1-BinarySequence(1) by ABSVALUE:def 1
      .= (0+1)-BinarySequence(2 to_power 0) by POWER:29
      .= (0*0)^<*1*> by BINARI_3:29
      .= <*TRUE*> by A7,FINSEQ_1:47;
    now per cases by A2;
      suppose h >= 0 & i < 0;
        then
A9:     h = 0 & i <= -1 by A3,INT_1:21;
        then i = -1 by A3,XXREAL_0:1;
        hence thesis by A4,A8,A9,Th15,BINARI_3:18;
      end;
      suppose
A10:    h < 0 & i >= 0;
        then h <= -1 by INT_1:21;
        then
A11:    h = -1 by A3,XXREAL_0:1;
        i = 0 by A3,A10;
        hence thesis by A4,A8,A11,Th15,BINARI_3:18;
      end;
    end;
    hence thesis;
  end;
A12: for n be non empty Nat st P[n] holds P[n+1]
  proof
    let n be non empty Nat such that
    -(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;
    assume
A13: -(2 to_power ((n+1)-'1)) <= h & h <= 2 to_power ((n+1)-'1) - 1 &
    -(2 to_power ((n+1)-'1)) <= i & i <= 2 to_power ((n+1)-'1) - 1 &
    -(2 to_power ((n+1)-'1)) <= h+i & h+i <= 2 to_power ((n+1)-'1) - 1 &
    ((h >= 0 & i < 0) or (h < 0 & i >= 0));
    set H = 2sComplement(n,h), I = 2sComplement(n,i),
    H1 = 2sComplement(n+1,h), I1 = 2sComplement(n+1,i),
    n2 = 2 to_power n, F = FALSE, T = TRUE;
    (n+1)-1 = n & n >= 0;
    then
A14: -n2 <= h & h <= n2 - 1 & -n2 <= i & i <= n2 - 1 &
    -n2 <= h+i & h+i <= n2 - 1 by A13,BINARITH:def 3;
    consider a be Element of BOOLEAN such that
A15: H1 = H^<*a*> by Th33;
    consider b be Element of BOOLEAN such that
A16: I1 = I^<*b*> by Th33;
    now per cases by A13;
      suppose
A17:    h >= 0 & i < 0;
        then reconsider h as Element of NAT by INT_1:16;
A18:    H1 = (n+1)-BinarySequence(abs h) by Def2
          .= (n+1)-BinarySequence(h) by ABSVALUE:def 1;
A19:    len H1 = n+1 & len I1 = n+1 & 1 <= n + 1 by FINSEQ_2:109,NAT_1:11;
A20:    h < 2 to_power n by A14,XREAL_1:148,XXREAL_0:2;
        then
A21:    H1.(n+1) = F by A18,BINARI_3:27;
        abs i = -i by A17,ABSVALUE:def 1;
        then
A22:    abs i <= --2 to_power n by A14,XREAL_1:26;
        n < n+1 by XREAL_1:31;
        then 2 to_power n < 2 to_power (n+1) by POWER:44;
        then
A23:    MajP(n+1,abs i) = n+1 by A22,Th24,XXREAL_0:2;
A24:    2 to_power (n+1) + i < 2 to_power (n+1) + 0 by A17,XREAL_1:10;
        2 to_power (n+1) + -(2 to_power n)
        = -(2 to_power n) + ((2 to_power 1)*(2 to_power n)) by POWER:32
          .= -(2 to_power n) + 2*(2 to_power n) by POWER:30
          .= 2 to_power n;
        then
A25:    2 to_power n <= 2 to_power (n+1) + i by A14,XREAL_1:8;

then reconsider NI = 2 to_power (n+1) + i as Element of NAT by INT_1:16;
A26:    I1.(n+1) = ((n+1)-BinarySequence(abs(2 to_power (n+1)+i))).(n+1)
        by A17,A23,Def2
          .= ((n+1)-BinarySequence(NI)).(n+1) by ABSVALUE:def 1
          .= T by A24,A25,BINARI_3:30;
        n + 0 < n+1 by XREAL_1:10;
        then 2 to_power n < 2 to_power (n+1) by POWER:44;
        then
A27:    h < 2 to_power (n+1) by A20,XXREAL_0:2;
A28:    H1/.(n+1) = H1.(n+1) by A19,FINSEQ_4:24;
        then
A29:    Intval(H1) = Absval(H1) by A21,BINARI_2:def 3
          .= h by A18,A27,BINARI_3:36;
A30:    I1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+i)) by A17,A23,Def2
          .= (n+1)-BinarySequence(NI) by ABSVALUE:def 1;
A31:    I1/.(n+1) = I1.(n+1) by A19,FINSEQ_4:24;
        then
A32:    Intval(I1) = Absval(I1) - 2 to_power (n+1) by A26,BINARI_2:def 3
          .= NI - 2 to_power (n+1) by A24,A30,BINARI_3:36
          .= i;
A33:    Int_add_ovfl(H1,I1) = 'not' F '&' 'not' T '&' (carry(H1,I1)/.(n+1))
        by A21,A26,A28,A31,BINARI_2:def 4
          .= F;
        Int_add_udfl(H1,I1) = F '&' T '&' 'not' (carry(H1,I1)/.(n+1))
        by A21,A26,A28,A31,BINARI_2:def 5
          .= F;
        then Intval(H1+I1) = h + i - IFEQ(F,F,0,2 to_power(n+1))
        + IFEQ(F,F,0,2 to_power(n+1)) by A15,A16,A29,A32,A33,BINARI_2:14
          .= h + i - 0 + 0;
        hence thesis;
      end;
      suppose
A34:    h < 0 & i >= 0;
        then reconsider i as Element of NAT by INT_1:16;
A35:    I1 = (n+1)-BinarySequence(abs i) by Def2
          .= (n+1)-BinarySequence(i) by ABSVALUE:def 1;
A36:    len I1 = n+1 & len H1 = n+1 & 1 <= n + 1 by FINSEQ_2:109,NAT_1:11;
A37:    i < 2 to_power n by A14,XREAL_1:148,XXREAL_0:2;
        then
A38:    I1.(n+1) = F by A35,BINARI_3:27;
        abs h = -h by A34,ABSVALUE:def 1;
        then
A39:    abs h <= --2 to_power n by A14,XREAL_1:26;
        n < n+1 by XREAL_1:31;
        then 2 to_power n < 2 to_power (n+1) by POWER:44;
        then
A40:    MajP(n+1,abs h) = n+1 by A39,Th24,XXREAL_0:2;
A41:    2 to_power (n+1) + h < 2 to_power (n+1) + 0 by A34,XREAL_1:10;
        2 to_power (n+1) + -(2 to_power n)
        = -(2 to_power n) + ((2 to_power 1)*(2 to_power n)) by POWER:32
          .= -(2 to_power n) + 2*(2 to_power n) by POWER:30
          .= 2 to_power n;
        then
A42:    2 to_power n <= 2 to_power (n+1) + h by A14,XREAL_1:8;

then reconsider NH = 2 to_power (n+1) + h as Element of NAT by INT_1:16;
A43:    H1.(n+1) = ((n+1)-BinarySequence(abs(2 to_power (n+1)+h))).(n+1)
        by A34,A40,Def2
          .= ((n+1)-BinarySequence(NH)).(n+1) by ABSVALUE:def 1
          .= T by A41,A42,BINARI_3:30;
        n + 0 < n+1 by XREAL_1:10;
        then 2 to_power n < 2 to_power (n+1) by POWER:44;
        then
A44:    i < 2 to_power (n+1) by A37,XXREAL_0:2;
A45:    I1/.(n+1) = I1.(n+1) by A36,FINSEQ_4:24;
        then
A46:    Intval(I1) = Absval(I1) by A38,BINARI_2:def 3
          .= i by A35,A44,BINARI_3:36;
A47:    H1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+h)) by A34,A40,Def2
          .= (n+1)-BinarySequence(NH) by ABSVALUE:def 1;
A48:    H1/.(n+1) = H1.(n+1) by A36,FINSEQ_4:24;
        then
A49:    Intval(H1) = Absval(H1) - 2 to_power (n+1) by A43,BINARI_2:def 3
          .= NH - 2 to_power (n+1) by A41,A47,BINARI_3:36
          .= h;
A50:    Int_add_ovfl(H1,I1) = 'not' T '&' 'not' F '&' (carry(H1,I1)/.(n+1))
        by A38,A43,A45,A48,BINARI_2:def 4
          .= F;
        Int_add_udfl(H1,I1) = T '&' F '&' 'not' (carry(H1,I1)/.(n+1))
        by A38,A43,A45,A48,BINARI_2:def 5
          .= F;
        then Intval(H1+I1) = h + i - IFEQ(F,F,0,2 to_power(n+1))
        + IFEQ(F,F,0,2 to_power(n+1)) by A15,A16,A46,A49,A50,BINARI_2:14
          .= h + i - 0 + 0;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  thus for n being non empty Nat holds P[n]
  from NAT_1:sch 10(A1,A12);
end;