The Mizar article:

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

MML identifier: BINARI_4
[ MML identifier index ]


environ

 vocabulary 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_2, FINSEQ_4, FUNCT_1, BOOLE, RELAT_1, VECTSP_1, ZF_LANG, GROUP_1;
 notation INT_1, MIDSP_3, MARGREL1, FINSEQ_1, CQC_LANG, POWER, BINARITH,
      BINARI_2, BINARI_3, GROUP_1, SERIES_1, NUMBERS, XCMPLX_0, XREAL_0,
      XBOOLE_0, EUCLID, REAL_1, NAT_1, TARSKI, FINSEQ_4, FUNCT_1, RELAT_1,
      VECTSP_1, ZFMISC_1, FINSEQOP, PREPOWER, SUBSET_1;
 constructors BINARITH, BINARI_2, BINARI_3, GROUP_1, SERIES_1, REAL_1, EUCLID,
      FINSEQ_4, FINSEQOP, SEQ_1, PREPOWER, EULER_2, MEMBERED;
 clusters INT_1, BINARITH, MARGREL1, RELSET_1, NAT_1, XREAL_0, MEMBERED;
 requirements REAL, BOOLE, SUBSET, NUMERALS, ARITHM;
 theorems AXIOMS, POWER, NAT_1, PRE_FF, ABSVALUE, REAL_1, BINARI_3, INT_1,
      BINARITH, NAT_2, BINARI_2, JORDAN2B, FINSEQ_1, FINSEQ_2, FINSEQ_4,
      MARGREL1, EUCLID, FUNCOP_1, RVSUM_1, FUNCT_2, ZFMISC_1, JORDAN4, GR_CY_1,
      CQC_LANG, GROUP_4, INT_3, SCMFSA9A, EULER_2, PEPIN, PREPOWER, ARMSTRNG,
      XCMPLX_0, XCMPLX_1, RLVECT_1;
 schemes NAT_1, BINARITH;

begin :: Preliminaries

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

theorem Th1:
  m > 0 implies m * 2 >= m + 1
proof
  assume m > 0;
  then m >= 0 + 1 by INT_1:20;
  then m >= 1 & m * 2 = m + m by XCMPLX_1:11;
  hence thesis by AXIOMS:24;
end;

theorem Th2:
  for m being Nat holds 2 to_power m >= m
proof
    defpred _P[Nat] means 2 to_power $1 >= $1;
    2 to_power 0 = 1 by POWER:29;
then 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;
      now per cases by NAT_1:19;
      suppose
A4:     m = 0;
        then 2 to_power (m+1) = 2 by POWER:30;
      hence thesis by A4;
      suppose
A5:     m > 0;
A6:      (2 to_power m) * 2 >= m * 2 by A3,NAT_1:20;
          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,AXIOMS:22;
    end;
    hence thesis;
  end;
  thus for m being Nat holds _P[m] from Ind(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
    .= dom (m |-> (0 qua Real)) by EUCLID:def 4
    .= Seg m by FINSEQ_2:68;
A4:dom(0*m) = dom(m |-> (0 qua Real)) by EUCLID:def 4
   .= Seg m by FINSEQ_2:68;
    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);
A6:  (0*m).k = (m |-> (0 qua Real)).k by EUCLID:def 4
     .= 0 qua Real by A4,A5,FINSEQ_2:70;
    then (0*m+0*m).k = 0 + 0 by A3,A4,A5,RVSUM_1:26;
    hence thesis by A6;
  end;
  hence thesis by A3,A4,FINSEQ_1:17;
end;

theorem Th4:
  for k be Nat holds
   k <= l & l <= m implies k = l or (k + 1 <= l & l <= m)
proof
   defpred _P[Nat] means
     $1 <= l & l <= m implies $1 = l or ($1 + 1 <= l & l <= m);
A1: _P[0]   by NAT_1:38;
A2:for k be Nat st _P[k] holds _P[k+1]  proof
    let k be Nat such that
       k <= l & l <= m implies k = l or (k + 1 <= l & l <= m);
    assume that
A3:  k+1 <= l and
A4:  l <= m;
       k+1 = l or k+1 < l by A3,AXIOMS:21;
    hence thesis by A4,NAT_1:38;
  end;
  thus for k being Nat holds _P[k] from Ind(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 RLVECT_1:99;
then A2:carry(x,y).1 = carry(x,y)/.1 by FINSEQ_4:24
   .= 0 by BINARITH:def 5,MARGREL1:36;
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 Nat by A4,INT_1:18;
      k + 1 = j + 1 - 1 by XCMPLX_1:29
     .= j by XCMPLX_1:26;
then A5: 1 <= k & k < n & j = k + 1 by A4,NAT_1:38;
then A6: k in Seg n & k <= len x & k <= len y by FINSEQ_1:3,FINSEQ_2:109;
      len(0*n) = len(n |-> (0 qua Real)) by EUCLID:def 4
     .= n by FINSEQ_2:69;
then A7: x/.k = (0*n).k by A1,A5,FINSEQ_4:24
     .= (n |-> (0 qua Real)).k by EUCLID:def 4
     .= FALSE by A6,FINSEQ_2:70,MARGREL1:36;
      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 'or' FALSE '&' (carry(x,y)/.k) 'or'
         FALSE '&' (carry(x,y)/.k) by MARGREL1:49
     .= FALSE 'or' FALSE 'or' FALSE '&' (carry(x,y)/.k) by MARGREL1:49
     .= FALSE 'or' FALSE 'or' FALSE by MARGREL1:49
     .= FALSE 'or' FALSE by BINARITH:7
     .= FALSE by BINARITH:7;
    hence thesis by MARGREL1:36;
  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 = (n |-> (0 qua Real)).l by EUCLID:def 4
     .= 0 by A8,FINSEQ_2:70;
      now per cases by A9,Th4;
     suppose l = 1;
      hence thesis by A2,A10;
     suppose 1 + 1 <= l & l <= n;
      then 1 < l & l <= n by NAT_1:38;
      hence thesis by A3,A10;
    end;
    hence thesis;
  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;
A3:  (0*n).k = (n |-> (0 qua Real)).k by EUCLID:def 4
     .= FALSE by A2,FINSEQ_2:70,MARGREL1:36;
      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 'xor' FALSE by A1,A2,A5,A6,BINARITH:def 8
     .= FALSE 'xor' FALSE by BINARITH:14
     .= FALSE by BINARITH:14;
    hence thesis by A3;
  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,RLVECT_1:99;
then A3:n in Seg n by FINSEQ_1:3;
    F/.n = F.n by A2,FINSEQ_4:24
   .= FALSE by A1,A3,JORDAN2B:2,MARGREL1:def 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:29;
  then k - m <= k + m - m by REAL_1:49;
  then k - m <= k + m + -m by XCMPLX_0:def 8;
then A2:k - m <= k by XCMPLX_1:137;
    l + m - m <= k - 1 - m by A1,REAL_1:49;
  then l + m + -m <= k - 1 - m by XCMPLX_0:def 8;
then A3:l <= k - 1 - m by XCMPLX_1:137;
    k - 1 - m = k - m - 1 by XCMPLX_1:21;
  then k - 1 - m < k - m by INT_1:26;
  then k - 1 - m < k by A2,AXIOMS:22;
  hence l < k by A3,AXIOMS:22;
    k <= k + l by NAT_1:29;
  then k - l <= k + l - l by REAL_1:49;
  then k - l <= k + l + -l by XCMPLX_0:def 8;
then A4:k - l <= k by XCMPLX_1:137;
    m + l - l <= k - 1 - l by A1,REAL_1:49;
  then m + l + -l <= k - 1 - l by XCMPLX_0:def 8;
then A5:m <= k - 1 - l by XCMPLX_1:137;
    k - 1 - l = k - l - 1 by XCMPLX_1:21;
  then k - 1 - l < k - l by INT_1:26;
  then k - 1 - l < k by A4,AXIOMS:22;
  hence thesis by A5,AXIOMS:22;
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 REAL_1:49;
  then g - i <= h by XCMPLX_1:26;
  then i + (g - i) < 0 + h by A1,REAL_1:67;
  then i + (g + -i) < 0 + h by XCMPLX_0:def 8;
  then i + -i + g < h by XCMPLX_1:1;
  then i - i + g < h by XCMPLX_0:def 8;
  then 0 + g < h by XCMPLX_1:14;
  hence g < h;
    g - h <= i + h - h by A1,REAL_1:49;
  then g - h <= i by XCMPLX_1:26;
  then h + (g - h) < 0 + i by A1,REAL_1:67;
  then h + (g + -h) < 0 + i by XCMPLX_0:def 8;
  then h + -h + g < i by XCMPLX_1:1;
  then h - h + g < i by XCMPLX_0:def 8;
  then 0 + g < i by XCMPLX_1:14;
  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,CQC_LANG:def 1;
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;
A6:2 to_power n > 2 to_power n - 1 by INT_1:26;
    Absval(L+M) + 2 to_power n >= 2 to_power n by NAT_1:29;
  hence contradiction by A1,A4,A5,A6,AXIOMS:22;
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:29;
    then n + 1 - 1 >= 1 - 1 by REAL_1:49;
then A9: n + 1 -' 1 = n + 1 - 1 by BINARITH:def 3
     .= n by XCMPLX_1:26;
      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,CQC_LANG:def 1,MARGREL1:38;
    hence thesis by A9,NAT_1:29;
  end;
  thus for n being non empty Nat holds _P[n] from Ind_from_1(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 MARGREL1:39;
A3:l < 2 to_power (n-'1) & m < 2 to_power (n-'1) by A1,Th8;
    1 <= n by RLVECT_1:99;
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,JORDAN4:5
   .= IFEQ(0,0,F,T) by GR_CY_1:6
   .= F by CQC_LANG:def 1;
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,JORDAN4:5
   .= IFEQ(0,0,F,T) by GR_CY_1:6
   .= F by CQC_LANG:def 1;
    n >= 1 by RLVECT_1:99;
  then n-1 >= 1-1 by REAL_1:49;
  then n-'1 = n - 1 by BINARITH:def 3;
  then n-'1 < n by INT_1:26;
  then 2 to_power (n-'1) < 2 to_power n by POWER:44;
  then 2 to_power (n-'1) - 1 < 2 to_power n - 1 by REAL_1:92;
then A7:l + m <= 2 to_power n - 1 by A1,AXIOMS:22;
    (L+M)/.n = F 'xor' F 'xor' T by A2,A4,A5,A6,BINARITH:def 8
   .= F 'xor' T by BINARITH:14
   .= T by BINARITH:14;
then A8:Absval(L+M) >= 2 to_power (n-'1) by Th12;
    2 to_power (n-'1) - 1 < 2 to_power (n-'1) by INT_1:26;
  then l + m < 2 to_power (n-'1) by A1,AXIOMS:22;
  hence contradiction by A7,A8,Th11;
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 RLVECT_1:99;
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,JORDAN4:5
   .= IFEQ(0,0,F,T) by GR_CY_1:6
   .= F by CQC_LANG:def 1;
 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,JORDAN4:5
   .= IFEQ(0,0,F,T) by GR_CY_1:6
   .= F by CQC_LANG:def 1;
  then (L+M)/.n = F 'xor' F 'xor' (carry(L,M)/.n) by A3,A4,BINARITH:def 8
   .= F 'xor' (carry(L,M)/.n) by BINARITH:14
   .= carry(L,M)/.n by BINARITH:14
   .= F by A1,Th13;
then A5:Intval(L+M) = Absval(L+M) by BINARI_2:def 3;
    n >= 1 by RLVECT_1:99;
  then n-1 >= 1-1 by REAL_1:49;
  then n-'1 = n - 1 by BINARITH:def 3;
  then n-'1 < n by INT_1:26;
  then 2 to_power (n-'1) < 2 to_power n by POWER:44;
  then 2 to_power (n-'1) - 1 < 2 to_power n - 1 by REAL_1:92;
  then l + m <= 2 to_power n - 1 by A1,AXIOMS:22;
  hence thesis by A5,Th11;
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,MARGREL1:38
   .= 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 Th17:
  for x be boolean set holds
   TRUE 'or' x = TRUE
proof
  let x be boolean set;
    TRUE 'or' x = 'not'('not' TRUE '&' 'not' x) by BINARITH:def 1
   .= 'not'(FALSE '&' 'not' x) by MARGREL1:41
   .= 'not' FALSE by MARGREL1:49;
  hence thesis by MARGREL1:41;
end;

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 > 1 & k-'1 < (k+1)-'1 by NAT_2:11;
then 2 to_power (k-'1) < 2 to_power ((k+1)-'1) by POWER:44;
    hence thesis by A3,REAL_1:49,50;
  end;
  thus for n being non empty Nat holds _P[n] from Ind_from_1(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,RLVECT_1:99;
then A3:n in Seg n by FINSEQ_1:3;
 x/.n = (0*n).n by A1,A2,FINSEQ_4:24
   .= (n |-> (0 qua Real)).n by EUCLID:def 4
   .= FALSE by A3,FINSEQ_2:70,MARGREL1:36;
  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 'or' FALSE '&' (carry(x,y)/.n) 'or' FALSE '&' (carry(x,y)/.n)
    by MARGREL1:49
   .= FALSE 'or' FALSE 'or' FALSE '&' (carry(x,y)/.n) by MARGREL1:49
   .= FALSE 'or' FALSE 'or' FALSE by MARGREL1:49
   .= FALSE 'or' FALSE by BINARITH:7
   .= FALSE by BINARITH:7;
  hence thesis by BINARITH:def 10;
end;

theorem Th20:
  (i*n) mod n = 0
proof
    n >= 0 + 1 by RLVECT_1:99;
  then n > 0 by NAT_1:38;
  then (i*n) mod n = ((i mod n) * ((n qua Integer) mod n)) mod n by INT_3:15
   .= ((i mod n) * (n mod n)) mod n by SCMFSA9A:5
   .= ((i mod n) * 0) mod n by GR_CY_1:5
   .= 0 mod n by SCMFSA9A:5;
  hence thesis by GR_CY_1:6;
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
A1:     2 to_power m >= j;
          for k be Nat st 2 to_power k >= j & k >= m holds k >= m;
        hence thesis by A1;
      suppose
A2:     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 A2,Th2,AXIOMS:22;
then A3: 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 Min(A3);
        hence thesis;
  end;
  uniqueness
  proof
    let p, q be Nat such that
A4:    2 to_power p >= j & p >= m &
        for k be Nat st 2 to_power k >= j & k >= m holds k >= p and
A5:    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 A4,A5;
    hence thesis by AXIOMS:21;
  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,AXIOMS:22;
  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,AXIOMS:22;
  hence thesis by A2,Def1;
end;

theorem
    m >= 1 implies MajP(m, 1) = m
proof
  assume m >= 1;
  then m >= 0 + 1;
  then 2 > 1 & m > 0 by NAT_1:38;
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,AXIOMS:22;
  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 RLVECT_1:99;
    now per cases;
   suppose
A3:   i >= 0;
     then reconsider i as Nat by INT_1:16;
A4:  2sComplement(n,i) = n-BinarySequence(abs(i)) by A3,Def2
      .= n-BinarySequence(i) by A3,ABSVALUE:def 1;
       i + 1 <= 2 to_power (n-'1) - 1 + 1 by A1,AXIOMS:24;
     then i + 1 <= 2 to_power (n-'1) + 1 - 1 by XCMPLX_1:29;
     then i + 1 <= 2 to_power (n-'1) by XCMPLX_1:26;
then A5:  i < 2 to_power (n-'1) by NAT_1:38;
       n >= 1 by RLVECT_1:99;
     then n - 1 >= 1 - 1 by REAL_1:49;
     then n-'1 = n - 1 by BINARITH:def 3;
     then n-'1 < n by INT_1:26;
     then 2 to_power (n-'1) < 2 to_power n by POWER:44;
  then i < 2 to_power n by A5,AXIOMS:22;
then A6:  Absval(n-BinarySequence i) = i by BINARI_3:36;
       1 <= n by RLVECT_1:99;
     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 A5,JORDAN4:5
      .= IFEQ(0,0,FALSE,TRUE) by GR_CY_1:6
      .= FALSE by CQC_LANG:def 1;
     hence thesis by A4,A6,BINARI_2:def 3;
   suppose
A7:   i < 0;
     then abs(i) = -i by ABSVALUE:def 1;
then A8:  abs(i) <= --2 to_power (n-'1) by A1,REAL_1:50;
       n > n-'1 by NAT_2:11;
then A9:  2 to_power n >= 2 to_power (n-'1) by POWER:44;
     then -(2 to_power n) <= -(2 to_power (n-'1)) by REAL_1:50;
     then -(2 to_power n) <= i by A1,AXIOMS:22;
     then -(2 to_power n) - i <= i-i by REAL_1:49;
     then -(2 to_power n) - i <= 0 by XCMPLX_1:14;
     then -(2 to_power n + i) <= 0 by XCMPLX_1:161;
then A10:  2 to_power n + i >= 0 by REAL_1:26,50;
     then reconsider k = 2 to_power n + i as Nat by INT_1:16;
       abs(i) <= 2 to_power n by A8,A9,AXIOMS:22;
then MajP(n,abs(i)) = n by Th24;
then A11:  2sComplement(n,i) = n-BinarySequence(abs(k)) by A7,Def2
      .= n-BinarySequence(k) by A10,ABSVALUE:def 1;
A12:  2 to_power n + i < 2 to_power n + 0 by A7,REAL_1:53;
   2 to_power n + -(2 to_power (n-'1)) =
      2 to_power n - (2 to_power (n-'1)) by XCMPLX_0:def 8
      .= (2 to_power 1) * (2 to_power (n-'1)) - (2 to_power (n-'1))
       by A2,NAT_2:12
      .= 2*(2 to_power (n-'1)) - (2 to_power (n-'1)) by POWER:30
      .= 2 to_power (n-'1)+(2 to_power (n-'1))-(2 to_power (n-'1))
       by XCMPLX_1:11
      .= 2 to_power (n-'1) by XCMPLX_1:26;
then A13:  k >= 2 to_power (n-'1) by A1,AXIOMS:24;
       k < 2 to_power n + 0 by A7,REAL_1:67;
     then k < (2 to_power 1) * (2 to_power (n-'1)) by A2,NAT_2:12;
     then k < 2*(2 to_power (n-'1)) by POWER:30;
then A14:  k < 2 to_power (n-'1) + (2 to_power (n-'1)) by XCMPLX_1:11;
       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 A13,A14,NAT_2:22
      .= IFEQ(1,0,FALSE,TRUE) by GROUP_4:102
      .= TRUE by CQC_LANG:def 1;
     then Intval(2sComplement(n,i)) = Absval(n-BinarySequence(k)) - 2 to_power
n
       by A11,BINARI_2:def 3,MARGREL1:38
      .= k - 2 to_power n by A12,BINARI_3:36
      .= 2 to_power n - 2 to_power n + i by XCMPLX_1:29
      .= 0 + i by XCMPLX_1:14;
     hence thesis;
  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;
    n >= 0 + 1 by RLVECT_1:99;
then A2:n > 0 & n <> 0 by NAT_1:38;
then A3: l = (l div n)*n + (l mod n) by NAT_1:47;
A4: k = (k div n)*n + (l mod n) by A1,A2,NAT_1:47;
    consider m be Nat such that
A5:  k = l + m by A1,NAT_1:28;
      l + m - l = k + -l by A5,XCMPLX_0:def 8;
    then l - l + m = k + -l by XCMPLX_1:29;
    then 0 + m = k + -l by XCMPLX_1:14;
    then m = (k div n)*n + (l mod n) - ((l div n)*n + (l mod n))
     by A3,A4,XCMPLX_0:def 8
     .= (k div n)*n - (l div n)*n by XCMPLX_1:32
     .= ((k div n) - (l div n))*n by XCMPLX_1:40;
    then m mod n = (((k div n) - (l div n))*n) mod n by SCMFSA9A:5
     .= 0 by Th20;
then (l+m) div n = (l div n) + (m div n) by GROUP_4:106;
then A6: k = ((l div n) + (m div n))*n + (l mod n) by A1,A2,A5,NAT_1:47
     .= (m div n)*n + (l div n)*n + (l mod n) by XCMPLX_1:8
     .= (m div n)*n + ((l div n)*n + (l mod n)) by XCMPLX_1:1
     .= (m div n)*n + l by A2,NAT_1:47;
    take m div n;
    thus thesis by A6;
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 AXIOMS:21;
   suppose
A2:  k = l;
    set s = 0;
      k = l + s*n by A2;
    hence thesis;
   suppose
A3:  k > l or l > k;
      now per cases by A3;
     suppose
        k > l;
      hence thesis by A1,Lm1;
     suppose
        k < l;
      then consider t be Integer such that
A4:     l = k + t*n by A1,Lm1;
        k = l + -(t*n) by A4,XCMPLX_1:137;
      then k = l + (-t)*n by XCMPLX_1:175;
      hence thesis;
    end;
    hence thesis;
  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:28;
  set M = 2 to_power m, J = 2 to_power j;
  reconsider L = l as Integer;
A4:M > 0 by POWER:39;
A5:L div M = l div M by SCMFSA9A:5;
A6:n - m = m - m + j by A3,XCMPLX_1:29
   .= 0 + j by XCMPLX_1:14;
    m + -m < n + -m by A1,REAL_1:67;
  then m - m < n + -m by XCMPLX_0:def 8;
  then m - m < n - m by XCMPLX_0:def 8;
  then 0 < j by A6,XCMPLX_1:14;
  then 0 + 1 < j + 1 by REAL_1:67;
  then 1 <= j by NAT_1:38;
  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 A7:J mod 2 = 0 by PEPIN:6;
A8:(s*J) mod 2 = ((s mod 2) * ((J qua Integer) mod 2)) mod 2 by INT_3:15
   .= ((s mod 2) * 0) mod 2 by A7,SCMFSA9A:5
   .= 0 mod 2 by SCMFSA9A:5
   .= 0 by GR_CY_1:6;
    k div M
   = (l + s*(2 to_power (j+m))) div M by A2,A3,SCMFSA9A:5
   .= (l + s*(J*M)) div M by POWER:32
   .= (l + s*J*M) div M by XCMPLX_1:4
   .= (L div M) + s*J by A4,INT_3:8
   .= (l div M) + s*J by SCMFSA9A:5;
  then (k div M) mod 2 = ((l div M) + s*J) mod 2 by SCMFSA9A:5
   .= ((L div M) + s*J) mod 2 by SCMFSA9A:5
   .= ((L div M) mod 2 + 0) mod 2 by A8,INT_3:14
   .= (L div M) mod 2 by INT_3:13;
  hence thesis by A5,SCMFSA9A:5;
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;
A2:2 to_power n > 0 & 2 to_power n is Nat by POWER:39;
  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
A3: MajP(n,abs h) = n + x by NAT_1:28;
    M = (2 to_power n)*(2 to_power x) by A3,POWER:32;
then A4:M mod 2 to_power n =
   ((2 to_power n)*(2 to_power x)) mod 2 to_power n by SCMFSA9A:5
   .= (((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 GR_CY_1:5
   .= 0 by GR_CY_1:6;
  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
A5: MajP(n,abs i) = n + y by NAT_1:28;
    L = (2 to_power n)*(2 to_power y) by A5,POWER:32;
then A6:L mod 2 to_power n =
   ((2 to_power n)*(2 to_power y)) mod 2 to_power n by SCMFSA9A:5
   .= (((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 GR_CY_1:5
   .= 0 by GR_CY_1:6;
A7:(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 A2,INT_3:14
   .= (h mod 2 to_power n) mod 2 to_power n by A4;
    (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 A2,INT_3:14
   .= (i mod 2 to_power n) mod 2 to_power n by A6;
  hence thesis by A1,A7;
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;
A5:  1 <= j & j <= n by A4,FINSEQ_1:3;
     then j - 1 >= 1 - 1 by REAL_1:49;
     then j-'1 = j - 1 by BINARITH:def 3;
     then j-'1 < j by INT_1:26;
then A6:  j-'1 < n by A5,AXIOMS:22;
       abs h = h & abs i = i &
      2 to_power n > 0 by A1,ABSVALUE:def 1,POWER:39;
then A7:  abs(h) mod 2 to_power n = h mod 2 to_power n &
      abs(i) mod 2 to_power n = i mod 2 to_power n &
      h mod 2 to_power n >= 0 & i mod 2 to_power n >= 0
      by INT_3:9,SCMFSA9A:5;
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 AXIOMS:24;
then A4:2 to_power MajP(n,abs h) + h >= 0 by XCMPLX_0:def 6;
  then reconsider H = 2 to_power MajP(n,abs h) + h as 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 AXIOMS:24;
then A5:2 to_power MajP(n,abs i) + i >= 0 by XCMPLX_0:def 6;
  then reconsider I = 2 to_power MajP(n,abs i) + i as Nat by INT_1:16;
    H mod (2 to_power n) = (H qua Integer) mod (2 to_power n) &
  I mod (2 to_power n) = (I qua Integer) mod (2 to_power n) by SCMFSA9A:5;
then A6:(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
A7:   j in Seg n;
A8: 1 <= j & j <= n by A7,FINSEQ_1:3;
A9: len(n-BinarySequence(H)) = n &
     len(n-BinarySequence(I)) = n by FINSEQ_2:109;
      j - 1 >= 1 - 1 by A8,REAL_1:49;
    then j-'1 = j - 1 by BINARITH:def 3;
    then j-'1 < j by INT_1:26;
then A10: j-'1 < n by A8,AXIOMS:22;
      abs H = H & abs I = I by A4,A5,ABSVALUE:def 1;
    then (n-BinarySequence(abs H)).j
     = (n-BinarySequence(H))/.j by A8,A9,FINSEQ_4:24
     .= 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 A6,A10,Lm3
     .= (n-BinarySequence(I))/.j by A7,BINARI_3:def 1
     .= (n-BinarySequence(I)).j by A8,A9,FINSEQ_4:24;
    hence thesis by A5,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
;
    2 to_power n > 0 by POWER:39;
  then 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;
A2:(l qua Integer) mod 2 to_power n
    = l mod 2 to_power n by SCMFSA9A:5
   .= (m qua Integer) mod 2 to_power n by A1,SCMFSA9A:5;
A3:l >= 0 & m >= 0 by NAT_1:18;
  then abs l = l & abs m = m by ABSVALUE:def 1;
  then 2sComplement(n,l) = n-BinarySequence(l) &
   2sComplement(n,m) = n-BinarySequence(m) by A3,Def2;
  hence thesis by A2,A3,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;
    2 to_power n > 0 by POWER:39;
then (l qua Integer) mod 2 to_power n
   = (m qua Integer) mod 2 to_power n by A1,INT_3:12;
  then l mod 2 to_power n
   = (m qua Integer) mod 2 to_power n by SCMFSA9A:5
   .= m mod 2 to_power n by SCMFSA9A:5;
  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:29;
  then j <= n+1 by A1,AXIOMS:22;
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;
      n + 1 >= n by NAT_1:29;
    then MajP(n+1,abs(i)) >= MajP(n,abs(i)) by Th22;
    then consider m be Nat such that
A6:  MajP(n+1,abs(i)) = MajP(n,abs(i)) + m by NAT_1:28;
    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 AXIOMS:24;
    then 2 to_power (MajP(n+1,abs(i))) + i >= i - i by XCMPLX_0:def 8;
    then 2 to_power (MajP(n+1,abs(i))) + i >= 0 by XCMPLX_1:14;
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 > 0 by POWER:39;
A9: (Q * 2 to_power m qua Integer) mod Q
      = (Q * 2 to_power m) mod Q by SCMFSA9A:5
     .= 0 by GROUP_4:101;
A10: M mod Q = ((Q * 2 to_power m)+i) mod Q by A7,SCMFSA9A:5
     .= (((Q * 2 to_power m qua Integer) mod Q) +
      (i mod Q)) mod Q by A8,INT_3:14
     .= (i mod Q) mod Q by A9;
A11: (Q qua Integer) mod Q = Q mod Q by SCMFSA9A:5
     .= 0 by GR_CY_1:5;
      Q >= abs i by Def1;
    then Q >= -i by A5,ABSVALUE:def 1;
    then Q + i >= -i + i by AXIOMS:24;
    then Q + i >= i - i by XCMPLX_0:def 8;
    then Q + i >= 0 by XCMPLX_1:14;
then N = Q + i by ABSVALUE:def 1;
then A12: N mod Q =(Q + i) mod Q by SCMFSA9A:5
     .= (((Q qua Integer) mod Q) + (i mod Q)) mod Q by A8,INT_3:14
     .= (i mod Q) mod Q by A11;
A13:P >= n by Def1;
      j + -1 >= 1 + -1 by A1,AXIOMS:24;
then A14:j - 1 >= 0 by XCMPLX_0:def 8;
then A15:j -' 1 = j - 1 by BINARITH:def 3;
    then j -' 1 < j by INT_1:26;
    then j -' 1 < n by A1,AXIOMS:22;
    then j -' 1 < P by A13,AXIOMS:22;
    hence thesis by A10,A12,A14,A15,Lm3;
  end;
  per cases;
   suppose
A16:  i >= 0;
    then reconsider i as Nat by INT_1:16;
A17: 2sComplement(n+1,i)/.j = ((n+1)-BinarySequence(abs i))/.j by A16,Def2
     .= ((n+1)-BinarySequence(i))/.j by A16,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 A16,Def2
     .= (n-BinarySequence(i))/.j by A16,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 A17;
   suppose
A18:  i < 0;
then A19: 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 A18,Def2
     .= IFEQ((N div 2 to_power (j-'1)) mod 2,0,FALSE,TRUE) by A2,BINARI_3:def 1
;
    hence thesis by A4,A18,A19;
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 by NAT_1:19;
  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;
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:29;
      then j <= m + 1 by A4,AXIOMS:22;
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;
  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;
  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:l >= 0 by NAT_1:18;
then A3:abs l = l by ABSVALUE:def 1;
  then (m+1)-BinarySequence(l)
   = 2sComplement(m,l)^<*x*> by A1,A2,Def2
   .= (m-BinarySequence(l))^<*x*> by A2,A3,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;
      h <= -1 & i <= -1 by A2,INT_1:21;
then A5: h = -1 & i = -1 by A4,AXIOMS:21;
    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 A6: 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 A7: abs(2 to_power MajP(2,abs h) + h)
     = 3 by A5,A6,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 A8:(3 div 2 to_power (1-'1)) mod 2 = (2+1) mod 2
     .= ((2 mod 2) + 1) mod 2 by GR_CY_1:2
     .= (0 + 1) mod 2 by GR_CY_1:5
     .= (1 qua Integer) mod 2 by SCMFSA9A:5
     .= 1 by PEPIN:5;
A9:1 in Seg 2 by FINSEQ_1:3;
A10:(2sComplement(2,h))/.1 = (2-BinarySequence(3))/.1 by A2,A7,Def2
     .= IFEQ(1,0,FALSE,TRUE) by A8,A9,BINARI_3:def 1
     .= TRUE by CQC_LANG:def 1;
    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 A5,A10,BINARITH:def 5
     .= T 'or' T '&' (carry(H,I)/.1) 'or' T '&' (carry(H,I)/.1) by MARGREL1:45
     .= T 'or' (carry(H,I)/.1) 'or' T '&' (carry(H,I)/.1) by MARGREL1:50
     .= T 'or' (carry(H,I)/.1) 'or' (carry(H,I)/.1) by MARGREL1:50
     .= T 'or' (carry(H,I)/.1) by Th17;
    hence thesis by Th17;
  end;
A11: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
A12:  -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;
A13: N-1 = n by XCMPLX_1:26;
A14:0 <= n by NAT_1:18;
then A15: N-'1 = N-1 by A13,BINARITH:def 3;
A16:N-'1 = n by A13,A14,BINARITH:def 3;
      N-1 < N by INT_1:26;
then A17: 2 to_power (N-'1) < 2 to_power N by A15,POWER:44;
      2 to_power (N-'1) + 2 to_power (N-'1) = 2*(2 to_power (N-'1)) by XCMPLX_1
:11
     .= (2 to_power 1)*(2 to_power (N-'1)) by POWER:30
     .= 2 to_power (1+(N-1)) by A15,POWER:32
     .= 2 to_power (1+(N+-1)) by XCMPLX_0:def 8
     .= 2 to_power (1+N+-1) by XCMPLX_1:1
     .= 2 to_power (1+N-1) by XCMPLX_0:def 8
     .= 2 to_power (1-1+N) by XCMPLX_1:29
     .= 2 to_power (0+N);
then A18: -2 to_power (N-'1) + 2 to_power N
     = (-2 to_power (N-'1) + 2 to_power (N-'1)) + 2 to_power (N-'1)
      by XCMPLX_1:1
     .= -(2 to_power (N-'1) - 2 to_power (N-'1)) + 2 to_power (N-'1)
      by XCMPLX_1:162
     .= -0 + 2 to_power (N-'1) by XCMPLX_1:14
     .= 2 to_power (N-'1);
  abs h = -h & abs i = -i by A12,ABSVALUE:def 1;
    then --2 to_power (N-'1) >= abs h & --2 to_power (N-'1) >= abs i
       by A12,REAL_1:50;
    then abs h < 2 to_power N & abs i < 2 to_power N by A17,AXIOMS:22;
then A19:   MajP(N,abs h) = N & MajP(N,abs i) = N by Th24;
A20:   2 to_power (N-'1) <= 2 to_power N + h &
       2 to_power (N-'1) <= 2 to_power N + i
       by A12,A18,AXIOMS:24;
        2 to_power n > 0 by POWER:39;
then A21:   0 <= 2 to_power N + h & 0 <= 2 to_power N + i by A16,A20,AXIOMS:22;
      then reconsider NH = 2 to_power N + h,
       NI = 2 to_power N + i as Nat by INT_1:16;
A22:   1 <= N & len (N-BinarySequence(NH)) = N & len(N-BinarySequence(NI)) = N
       by FINSEQ_2:109,NAT_1:29;
A23:   2 to_power N + h < 0 + 2 to_power N &
       2 to_power N + i < 0 + 2 to_power N by A12,REAL_1:67;
A24:   H/.N = (N-BinarySequence(abs NH))/.N by A12,A19,Def2
       .= (N-BinarySequence(NH))/.N by A21,ABSVALUE:def 1
       .= (N-BinarySequence(NH)).N by A22,FINSEQ_4:24
       .= T by A16,A20,A23,BINARI_3:30;
A25:   I/.N = (N-BinarySequence(abs NI))/.N by A12,A19,Def2
       .= (N-BinarySequence(NI))/.N by A21,ABSVALUE:def 1
       .= (N-BinarySequence(NI)).N by A22,FINSEQ_4:24
       .= T by A16,A20,A23,BINARI_3:30;
A26:  H1/.N = H/.N & I1/.N = I/.N by A22,Th32;
        N < N+1 by NAT_1:38;
      then carry(H1,I1)/.(N+1) = T '&' T 'or' T '&' (carry(H1,I1)/.N) 'or'
       T '&' (carry(H1,I1)/.N) by A22,A24,A25,A26,BINARITH:def 5
       .= T 'or' T '&' (carry(H1,I1)/.N) 'or' T '&' (carry(H1,I1)/.N)
        by MARGREL1:45
       .= T 'or' (carry(H1,I1)/.N) 'or' T '&' (carry(H1,I1)/.N) by MARGREL1:50
       .= T 'or' (carry(H1,I1)/.N) 'or' (carry(H1,I1)/.N) by MARGREL1:50
       .= T 'or' (carry(H1,I1)/.N) by Th17;
      hence thesis by Th17;
  end;
  thus for n being non empty Nat holds _P[n] from Ind_from_1(A1,A11);
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 Nat by A1,INT_1:16;
A2: 2sComplement(n,h) = n-BinarySequence(abs h) by A1,Def2
   .= n-BinarySequence(h) by A1,ABSVALUE:def 1;
     2sComplement(n,i) = n-BinarySequence(abs i) by A1,Def2
   .= n-BinarySequence(i) by A1,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 by NAT_1:18,XCMPLX_1:26;
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 REAL_1:50;
then A4:abs h < 2 to_power n & abs i < 2 to_power n by A1,ABSVALUE:def 1;
    n < n+1 by REAL_1:69;
  then 2 to_power n < 2 to_power (n+1) by POWER:44;
  then abs h < 2 to_power (n+1) & abs i < 2 to_power (n+1) by A4,AXIOMS:22;
then A5:MajP(n+1,abs h) = n+1 & MajP(n+1,abs i) = n+1 by Th24;
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,REAL_1:67;
 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 by XCMPLX_1:184;
then A7:2 to_power n <= 2 to_power (n+1) + h &
   2 to_power n <= 2 to_power (n+1) + i by A3,AXIOMS:24;
    2 to_power n > 0 by POWER:39;
then A8:0 <= 2 to_power (n+1) + h &
   0 <= 2 to_power (n+1) + i by A7,AXIOMS:22;
  then reconsider NH = 2 to_power (n+1) + h,
   NI = 2 to_power (n+1) + i as 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:29;
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 A8,ABSVALUE:def 1
       .= T by A6,A7,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 A8,ABSVALUE:def 1
       .= T by A6,A7,BINARI_3:30;
A15:  H1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+h)) by A1,A5,Def2
       .= (n+1)-BinarySequence(NH) by A8,ABSVALUE:def 1;
A16:  I1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+i)) by A1,A5,Def2
       .= (n+1)-BinarySequence(NI) by A8,ABSVALUE:def 1;
A17:  Intval(H1) = Absval(H1) - 2 to_power (n+1)
       by A13,BINARI_2:def 3,MARGREL1:38
       .= NH - 2 to_power (n+1) by A6,A15,BINARI_3:36
       .= h by XCMPLX_1:26;
A18:  Intval(I1) = Absval(I1) - 2 to_power (n+1)
       by A14,BINARI_2:def 3,MARGREL1:38
       .= NI - 2 to_power (n+1) by A6,A16,BINARI_3:36
       .= i by XCMPLX_1:26;
A19:  carry(H1,I1)/.(n+1) = T by A1,A2,Th35;
then A20:  Int_add_ovfl(H1,I1)
       = 'not' T '&' 'not' T '&' T by A13,A14,BINARI_2:def 4
       .= F '&' 'not' T '&' T by MARGREL1:41
       .= F '&' T by MARGREL1:45
       .= F by MARGREL1:45;
   Int_add_udfl(H1,I1)
       = T '&' T '&' 'not' T by A13,A14,A19,BINARI_2:def 5
       .= T '&' 'not' T by MARGREL1:45
       .= F by MARGREL1:46;
      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 + IFEQ(F,F,0,2 to_power(n+1)) by CQC_LANG:def 1
       .= h + i - 0 + 0 by CQC_LANG:def 1;
      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
     .= 1 |-> (0 qua Real) by EUCLID:def 4
     .= <* FALSE *> by FINSEQ_2:73,MARGREL1:36;
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 = 0 |-> (0 qua Real) by EUCLID:def 4
     .= {} 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 ARMSTRNG:7
     .= <*TRUE*> by A7,FINSEQ_1:47,MARGREL1:36;
      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,AXIOMS:21;
      hence thesis by A4,A8,A9,Th15,BINARI_3:18;
     suppose
A10:  h < 0 & i >= 0;
      then h <= -1 by INT_1:21;
then A11:  h = -1 by A3,AXIOMS:21;
        i = 0 by A3,A10;
      hence thesis by A4,A8,A11,Th15,BINARI_3:18;
    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 by NAT_1:18,XCMPLX_1:26;
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 Nat by INT_1:16;
A18:   H1 = (n+1)-BinarySequence(abs h) by A17,Def2
       .= (n+1)-BinarySequence(h) by A17,ABSVALUE:def 1;
A19:   len H1 = n+1 & len I1 = n+1 & 1 <= n + 1 by FINSEQ_2:109,NAT_1:29;
        2 to_power n - 1 < 2 to_power n by INT_1:26;
then A20:   h < 2 to_power n by A14,AXIOMS:22;
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,REAL_1:50;
        n < n+1 by REAL_1:69;
      then 2 to_power n < 2 to_power (n+1) by POWER:44;
      then abs i < 2 to_power (n+1) by A22,AXIOMS:22;
then A23:   MajP(n+1,abs i) = n+1 by Th24;
A24:   2 to_power (n+1) + i < 2 to_power (n+1) + 0 by A17,REAL_1:67;
    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 by XCMPLX_1:184;
then A25:  2 to_power n <= 2 to_power (n+1) + i by A14,AXIOMS:24;
then A26:  0 < 2 to_power (n+1) + i by POWER:39;
      then reconsider NI = 2 to_power (n+1) + i as Nat by INT_1:16;
A27:  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 A26,ABSVALUE:def 1
       .= T by A24,A25,BINARI_3:30;
        n + 0 < n+1 by REAL_1:67;
      then 2 to_power n < 2 to_power (n+1) by POWER:44;
then A28:  h < 2 to_power (n+1) by A20,AXIOMS:22;
A29: H1/.(n+1) = H1.(n+1) by A19,FINSEQ_4:24;
then A30:  Intval(H1) = Absval(H1) by A21,BINARI_2:def 3
       .= h by A18,A28,BINARI_3:36;
A31:  I1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+i)) by A17,A23,Def2
       .= (n+1)-BinarySequence(NI) by A26,ABSVALUE:def 1;
A32:  I1/.(n+1) = I1.(n+1) by A19,FINSEQ_4:24;
then A33:  Intval(I1) = Absval(I1) - 2 to_power (n+1)
       by A27,BINARI_2:def 3,MARGREL1:38
       .= NI - 2 to_power (n+1) by A24,A31,BINARI_3:36
       .= i by XCMPLX_1:26;
A34:  Int_add_ovfl(H1,I1) = 'not' F '&' 'not' T '&' (carry(H1,I1)/.(n+1))
        by A21,A27,A29,A32,BINARI_2:def 4
       .= T '&' 'not' T '&' (carry(H1,I1)/.(n+1)) by MARGREL1:41
       .= F '&' (carry(H1,I1)/.(n+1)) by MARGREL1:46
       .= F by MARGREL1:45;
   Int_add_udfl(H1,I1)
       = F '&' T '&' 'not' (carry(H1,I1)/.(n+1))
        by A21,A27,A29,A32,BINARI_2:def 5
       .= F '&' 'not' (carry(H1,I1)/.(n+1)) by MARGREL1:45
       .= F by MARGREL1:45;
      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,A30,A33,A34,BINARI_2:14
       .= h + i - 0 + IFEQ(F,F,0,2 to_power(n+1)) by CQC_LANG:def 1
       .= h + i - 0 + 0 by CQC_LANG:def 1;
      hence thesis;
     suppose
A35:    h < 0 & i >= 0;
      then reconsider i as Nat by INT_1:16;
A36:   I1 = (n+1)-BinarySequence(abs i) by A35,Def2
       .= (n+1)-BinarySequence(i) by A35,ABSVALUE:def 1;
A37:   len I1 = n+1 & len H1 = n+1 & 1 <= n + 1 by FINSEQ_2:109,NAT_1:29;
        2 to_power n - 1 < 2 to_power n by INT_1:26;
then A38:   i < 2 to_power n by A14,AXIOMS:22;
then A39:   I1.(n+1) = F by A36,BINARI_3:27;
        abs h = -h by A35,ABSVALUE:def 1;
then A40:   abs h <= --2 to_power n by A14,REAL_1:50;
        n < n+1 by REAL_1:69;
      then 2 to_power n < 2 to_power (n+1) by POWER:44;
      then abs h < 2 to_power (n+1) by A40,AXIOMS:22;
then A41:   MajP(n+1,abs h) = n+1 by Th24;
A42:   2 to_power (n+1) + h < 2 to_power (n+1) + 0 by A35,REAL_1:67;
    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 by XCMPLX_1:184;
then A43:  2 to_power n <= 2 to_power (n+1) + h by A14,AXIOMS:24;
then A44:  0 < 2 to_power (n+1) + h by POWER:39;
      then reconsider NH = 2 to_power (n+1) + h as Nat by INT_1:16;
A45:  H1.(n+1) = ((n+1)-BinarySequence(abs(2 to_power (n+1)+h))).(n+1)
       by A35,A41,Def2
       .= ((n+1)-BinarySequence(NH)).(n+1) by A44,ABSVALUE:def 1
       .= T by A42,A43,BINARI_3:30;
        n + 0 < n+1 by REAL_1:67;
      then 2 to_power n < 2 to_power (n+1) by POWER:44;
then A46:  i < 2 to_power (n+1) by A38,AXIOMS:22;
A47: I1/.(n+1) = I1.(n+1) by A37,FINSEQ_4:24;
then A48:  Intval(I1) = Absval(I1) by A39,BINARI_2:def 3
       .= i by A36,A46,BINARI_3:36;
A49:  H1 = (n+1)-BinarySequence(abs(2 to_power (n+1)+h)) by A35,A41,Def2
       .= (n+1)-BinarySequence(NH) by A44,ABSVALUE:def 1;
A50:  H1/.(n+1) = H1.(n+1) by A37,FINSEQ_4:24;
then A51:  Intval(H1) = Absval(H1) - 2 to_power (n+1)
       by A45,BINARI_2:def 3,MARGREL1:38
       .= NH - 2 to_power (n+1) by A42,A49,BINARI_3:36
       .= h by XCMPLX_1:26;
A52:  Int_add_ovfl(H1,I1) = 'not' T '&' 'not' F '&' (carry(H1,I1)/.(n+1))
        by A39,A45,A47,A50,BINARI_2:def 4
       .= F '&' 'not' F '&' (carry(H1,I1)/.(n+1)) by MARGREL1:41
       .= F '&' (carry(H1,I1)/.(n+1)) by MARGREL1:46
       .= F by MARGREL1:45;
   Int_add_udfl(H1,I1) = T '&' F '&' 'not' (carry(H1,I1)/.(n+1))
        by A39,A45,A47,A50,BINARI_2:def 5
       .= F '&' 'not' (carry(H1,I1)/.(n+1)) by MARGREL1:45
       .= F by MARGREL1:45;
      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,A48,A51,A52,BINARI_2:14
       .= h + i - 0 + IFEQ(F,F,0,2 to_power(n+1)) by CQC_LANG:def 1
       .= h + i - 0 + 0 by CQC_LANG:def 1;
      hence thesis;
    end;
    hence thesis;
  end;
  thus for n being non empty Nat holds _P[n] from Ind_from_1(A1,A12);
end;

Back to top