:: Binary Arithmetics. Addition
::  by Takaya Nishiyama and Yasuho Mizuhara
::
:: Received October 8, 1993
:: Copyright (c) 1993-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_2, FINSEQ_1, ORDINAL4,
      PARTFUN1, RELAT_1, ARYTM_3, CARD_1, MARGREL1, XBOOLEAN, XCMPLX_0,
      FUNCT_1, XXREAL_0, ARYTM_1, FUNCOP_1, POWER, BINOP_2, SETWISEO, REAL_1,
      BINARITH;
 notations XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, REAL_1, XBOOLEAN, MARGREL1,
      FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, BINOP_2, SETWISEO, FUNCOP_1,
      SETWOP_2, SERIES_1, FINSEQ_1, FINSEQ_2, XXREAL_0, ORDINAL1, NAT_1, NAT_D;
 constructors BINOP_1, SETWISEO, XXREAL_0, NAT_1, INT_1, BINOP_2, MARGREL1,
      PARTFUN1, FINSOP_1, SERIES_1, RFINSEQ, SEQ_1, REAL_1, NAT_D, RELSET_1,
      FINSEQ_2;
 registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
      BINOP_2, XBOOLEAN, MARGREL1, FINSEQ_2, XBOOLE_0, REAL_1, CARD_1,
      FINSEQ_1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions FINSEQ_1, TARSKI, XBOOLEAN;
 theorems NAT_1, INT_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_1, TARSKI, POWER,
      FINSOP_1, XBOOLE_0, BINOP_2, XREAL_1, XXREAL_0, XBOOLEAN, FUNCOP_1,
      PARTFUN1, FINSEQ_3, XREAL_0, NAT_D, CARD_1;
 schemes FINSEQ_1, FINSEQ_2, NAT_1;

begin

theorem Th1:
  for i,n being Nat, D being non empty set, d being Element of D, z
  being Tuple of n,D st i in Seg n holds (z^<*d*>)/.i=z/.i
proof
  let i,n be Nat, D be non empty set, d be Element of D, z be Tuple of n,D
  such that
A1: i in Seg n;
  len z = n by CARD_1:def 7;
  then i in dom z by A1,FINSEQ_1:def 3;
  hence thesis by FINSEQ_4:68;
end;

theorem Th2:
  for n being Nat, D being non empty set, d being Element of D, z
  being Tuple of n,D holds (z^<*d*>)/.(n+1)=d
proof
  let n be Nat, D be non empty set, d be Element of D, z be Tuple of n,D;
  len<*d*> = 1 by FINSEQ_1:39;
  then 0+1 in Seg len <*d*>;
  then
A1: 0+1 in dom <*d*> by FINSEQ_1:def 3;
  len(z) = n by CARD_1:def 7;
  hence (z^<*d*>)/.(n+1) = <*d*>/.1 by A1,FINSEQ_4:69
    .= d by FINSEQ_4:16;
end;

definition
  let x, y be Element of BOOLEAN;
  redefine func x 'or' y -> Element of BOOLEAN;
  correctness
  proof
    x 'or' y = FALSE or x 'or' y = TRUE by XBOOLEAN:def 3;
    hence thesis;
  end;
  redefine func x 'xor' y -> Element of BOOLEAN;
  correctness
  proof
    x 'xor' y = FALSE or x 'xor' y = TRUE by XBOOLEAN:def 3;
    hence thesis;
  end;
end;

reserve x,y,z for boolean set;

theorem
  x 'or' FALSE = x;

theorem
  'not' (x '&' y) = 'not' x 'or' 'not' y;

theorem
  'not' (x 'or' y) = 'not' x '&' 'not' y;

theorem
  x '&' y = 'not' ('not' x 'or' 'not' y);

theorem
  TRUE 'xor' x = 'not' x;

theorem
  FALSE 'xor' x = x;

theorem
  x '&' x = x;

theorem
  x 'or' TRUE = TRUE;

theorem
  (x 'or' y) 'or' z = x 'or' (y 'or' z);

theorem
  x 'or' x = x;

theorem
  TRUE 'xor' FALSE = TRUE;

reserve i,j,k for Nat;
reserve n for non zero Nat;
reserve x,y,z1,z2 for Tuple of n, BOOLEAN;

definition

  let n be Nat, x be Tuple of n, BOOLEAN;
  func 'not' x -> Tuple of n, BOOLEAN means
  for i st i in Seg n holds it/.i = 'not' (x/.i);
  existence
  proof
    deffunc F(Nat) = 'not' (x/.$1);
    consider z being FinSequence of BOOLEAN such that
A1: len z = n and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg n by A1,FINSEQ_1:def 3;
    reconsider z as Tuple of n, BOOLEAN by A1,CARD_1:def 7;
    take z;
    let i;
    assume
A4: i in Seg n;
    then i in dom z by A1,FINSEQ_1:def 3;
    hence z/.i = z.i by PARTFUN1:def 6
      .= 'not' (x/.i) by A2,A3,A4;
  end;
  uniqueness
  proof
    let y, z be Tuple of n, BOOLEAN such that
A5: for i st i in Seg n holds y/.i = 'not' (x/.i) and
A6: for i st i in Seg n holds z/.i = 'not' (x/.i);
A7: len y = n by CARD_1:def 7;
    then
A8: dom y = Seg n by FINSEQ_1:def 3;
A9: len z = n by CARD_1:def 7;
    now
      let j be Nat;
      assume
A10:  j in dom y;
      then
A11:  j in dom z by A9,A8,FINSEQ_1:def 3;
      thus y.j = y/.j by A10,PARTFUN1:def 6
        .= 'not' (x/.j) by A5,A8,A10
        .= z/.j by A6,A8,A10
        .= z.j by A11,PARTFUN1:def 6;
    end;
    hence thesis by A7,A9,FINSEQ_2:9;
  end;
end;

definition
  let n be non empty Nat, x, y be Tuple of n, BOOLEAN;
  func carry(x, y) -> Tuple of n, BOOLEAN means
  :Def2:
  it/.1 = FALSE & for i
being Nat st 1 <= i & i < n holds it/.(i+1) = (x/.i) '&' (y/.i) 'or' (x/.i) '&'
  (it/.i) 'or' (y/.i) '&' (it/.i);
  existence
  proof
    deffunc G(Nat,Element of BOOLEAN) = (x/.($1+1)) '&' (y/.($1+1)) 'or' (x/.(
    $1+1)) '&' $2 'or' (y/.($1+1)) '&' $2;
    consider f being Function of NAT, BOOLEAN such that
A1: f.0 = FALSE and
A2: for i being Nat holds f.(i+1) = G(i,f.i) from NAT_1:sch 12;
    deffunc F(Nat) = f.($1-1);
    consider z being FinSequence such that
A3: len z = n and
A4: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_1:sch 2;
    z is FinSequence of BOOLEAN
    proof
      let a be set;
      assume a in rng z;
      then consider b be set such that
A5:   b in dom z and
A6:   a = z.b by FUNCT_1:def 3;
A7:   b in Seg n by A3,A5,FINSEQ_1:def 3;
      reconsider b as Element of NAT by A5;
      b>=1 by A7,FINSEQ_1:1;
      then reconsider c = b-1 as Element of NAT by INT_1:5;
      z.b = f.c by A4,A5;
      hence thesis by A6;
    end;
    then reconsider z as Tuple of n, BOOLEAN by A3,CARD_1:def 7;
    take z;
    0+1 <= n by NAT_1:13;
    then 1 in Seg n;
    then
A8: 1 in dom z by A3,FINSEQ_1:def 3;
    hence z/.1 = z.1 by PARTFUN1:def 6
      .= f.(1-1) by A4,A8
      .= FALSE by A1;
    let i be Nat;
    assume that
A9: 1 <= i and
A10: i < n;
    consider j be Nat such that
A11: j+1 = i by A9,NAT_1:6;
    j+1 in Seg n by A9,A10,A11;
    then
A12: j+1 in dom z by A3,FINSEQ_1:def 3;
    then
A13: z/.(j+1) = z.(j+1) by PARTFUN1:def 6
      .= f.(j+1-1) by A4,A12
      .= f.j;
A14: i+1-1=i;
    1 <= i+1 & i+1 <= n by A9,A10,NAT_1:13;
    then
A15: i + 1 in dom z by A3,FINSEQ_3:25;
    hence z/.(i+1) = z.(i+1) by PARTFUN1:def 6
      .= f.(j+1) by A4,A11,A14,A15
      .= (x/.i) '&' (y/.i) 'or' (x/.i) '&' (z/.i) 'or' (y/.i) '&' (z/.i) by A2
,A11,A13;
  end;
  uniqueness
  proof
    let z1, z2 be Tuple of n, BOOLEAN such that
A16: z1/.1 = FALSE and
A17: for i being Nat st 1 <= i & i < n holds z1/.(i+1) = (x/.i) '&' (y
    /.i) 'or' (x/.i) '&' (z1/.i) 'or' (y/.i) '&' (z1/.i) and
A18: z2/.1 = FALSE and
A19: for i being Nat st 1 <= i & i < n holds z2/.(i+1) = (x/.i) '&' (y
    /.i) 'or' (x/.i) '&' (z2/.i) 'or' (y/.i) '&' (z2/.i);
A20: len z2 = n by CARD_1:def 7;
A21: len z1 = n by CARD_1:def 7;
    then
A22: dom z1 = Seg n by FINSEQ_1:def 3;
    now
      defpred P[Nat] means $1 in Seg n implies z1/.$1 = z2/.$1;
A23:  dom z1 = Seg n & dom z2 = Seg n by A21,A20,FINSEQ_1:def 3;
A24:  now
        let k such that
A25:    P[k];
        thus P[k+1]
        proof
          assume
A26:      k+1 in Seg n;
          per cases;
          suppose
            k = 0;
            hence thesis by A16,A18;
          end;
          suppose
A27:        k <> 0;
            k+1 <= n & k < k+1 by A26,FINSEQ_1:1,XREAL_1:29;
            then
A28:        k < n by XXREAL_0:2;
A29:        k >= 0+1 by A27,NAT_1:13;
            hence
            z1/.(k+1) = (x/.k) '&' (y/.k) 'or' (x/.k) '&' (z1/.k) 'or' (y
            /.k) '&' (z1/.k) by A17,A28
              .= z2/.(k+1) by A19,A25,A29,A28,FINSEQ_1:1;
          end;
        end;
      end;
A30:  P[0] by FINSEQ_1:1;
A31:  for k holds P[k] from NAT_1:sch 2 (A30,A24);
      let j be Nat such that
A32:  j in dom z1;
      thus z1.j = z1/.j by A32,PARTFUN1:def 6
        .= z2/.j by A22,A32,A31
        .= z2.j by A32,A23,PARTFUN1:def 6;
    end;
    hence thesis by A21,A20,FINSEQ_2:9;
  end;
end;

definition
  let n be Nat, x be Tuple of n, BOOLEAN;
  func Binary(x) -> Tuple of n, NAT means
  :Def3:
  for i st i in Seg n holds it /.i = IFEQ(x/.i,FALSE,0,2 to_power(i-'1));
  existence
  proof
    deffunc F(Nat) = IFEQ( x/.$1,FALSE,0,2 to_power($1-'1));
    consider z being FinSequence of NAT such that
A1: len z = n and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg n by A1,FINSEQ_1:def 3;
    reconsider z as Tuple of n, NAT by A1,CARD_1:def 7;
    take z;
    let j;
    assume
A4: j in Seg n;
    then j in dom z by A1,FINSEQ_1:def 3;
    hence z/.j = z.j by PARTFUN1:def 6
      .= IFEQ(x/.j,FALSE,0,2 to_power(j-'1)) by A2,A3,A4;
  end;
  uniqueness
  proof
    let z1, z2 be Tuple of n, NAT such that
A5: for i st i in Seg n holds z1/.i = IFEQ(x/.i,FALSE,0,2 to_power(i-' 1)) and
A6: for i st i in Seg n holds z2/.i = IFEQ(x/.i,FALSE,0,2 to_power(i-' 1));
A7: len z1 = n by CARD_1:def 7;
    then
A8: dom z1 = Seg n by FINSEQ_1:def 3;
A9: len z2 = n by CARD_1:def 7;
    then
A10: dom z2 = Seg n by FINSEQ_1:def 3;
    now
      let j be Nat;
      assume
A11:  j in dom z1;
      hence z1.j = z1/.j by PARTFUN1:def 6
        .= IFEQ( x/.j,FALSE,0,2 to_power(j-'1)) by A5,A8,A11
        .= z2/.j by A6,A8,A11
        .= z2.j by A8,A10,A11,PARTFUN1:def 6;
    end;
    hence thesis by A7,A9,FINSEQ_2:9;
  end;
end;

definition
  let n be Nat, x be Tuple of n, BOOLEAN;
  func Absval (x) -> Element of NAT equals
  addnat $$ Binary (x);
  correctness;
end;

definition
  let n, x, y;
  func x + y -> Tuple of n, BOOLEAN means
  :Def5:
  for i st i in Seg n holds it /.i = (x/.i) 'xor' (y/.i) 'xor' (carry(x,y)/.i);
  existence
  proof
    deffunc F(Nat) = (x/.$1) 'xor' (y/.$1) 'xor' (carry(x,y)/.$1);
    consider z being FinSequence of BOOLEAN such that
A1: len z = n and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg n by A1,FINSEQ_1:def 3;
    reconsider z as Tuple of n, BOOLEAN by A1,CARD_1:def 7;
    take z;
    let i;
    assume
A4: i in Seg n;
    then i in dom z by A1,FINSEQ_1:def 3;
    hence z/.i = z.i by PARTFUN1:def 6
      .= (x/.i) 'xor' (y/.i) 'xor' (carry(x,y)/.i) by A2,A3,A4;
  end;
  uniqueness
  proof
    let z1, z2 such that
A5: for i st i in Seg n holds z1/.i = (x/.i) 'xor' (y/.i) 'xor' (carry
    (x,y)/.i) and
A6: for i st i in Seg n holds z2/.i = (x/.i) 'xor' (y/.i) 'xor' (carry
    (x,y)/.i);
A7: len z1 = n by CARD_1:def 7;
    then
A8: dom z1 = Seg n by FINSEQ_1:def 3;
A9: len z2 = n by CARD_1:def 7;
    then
A10: dom z2 = Seg n by FINSEQ_1:def 3;
    now
      let j be Nat;
      assume
A11:  j in dom z1;
      hence z1.j = z1/.j by PARTFUN1:def 6
        .= (x/.j) 'xor' (y/.j) 'xor' (carry(x,y)/.j) by A5,A8,A11
        .= z2/.j by A6,A8,A11
        .= z2.j by A8,A10,A11,PARTFUN1:def 6;
    end;
    hence thesis by A7,A9,FINSEQ_2:9;
  end;
end;

definition
  let n,z1,z2;
  func add_ovfl(z1,z2) -> Element of BOOLEAN equals
  (z1/.n) '&' (z2/.n) 'or' (
  z1/.n) '&' (carry(z1,z2)/.n) 'or' (z2/.n) '&' (carry(z1,z2)/.n);
  correctness;
end;

definition
  let n,z1,z2;
  pred z1,z2 are_summable means
  :Def7:
  add_ovfl(z1,z2) = FALSE;
end;

theorem Th14:
  for z1 being Tuple of 1,BOOLEAN holds z1= <*FALSE*> or z1=<*TRUE *>
proof
  let z1 be Tuple of 1,BOOLEAN;
A1: ex B being Element of BOOLEAN st z1=<*B*> by FINSEQ_2:97;
  per cases by XBOOLEAN:def 3;
  suppose
    z1/.1 = FALSE;
    hence thesis by A1,FINSEQ_4:16;
  end;
  suppose
    z1/.1 = TRUE;
    hence thesis by A1,FINSEQ_4:16;
  end;
end;

theorem Th15:
  for z1 being Tuple of 1,BOOLEAN holds z1=<*FALSE*> implies Absval(z1) = 0
proof
  let z1 be Tuple of 1,BOOLEAN;
A1: ex k being Element of NAT st Binary( z1 ) = <* k *> by FINSEQ_2:97;
  assume z1=<*FALSE*>;
  then
A2: z1/.1 = FALSE by FINSEQ_4:16;
  1 in Seg 1;
  then (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1)) by Def3
    .= 0 by A2,FUNCOP_1:def 8;
  hence Absval(z1) = addnat $$ <* 0 *> by A1,FINSEQ_4:16
    .= 0 by FINSOP_1:11;
end;

theorem Th16:
  for z1 being Tuple of 1,BOOLEAN st z1=<*TRUE*> holds Absval(z1)= 1
proof
  let z1 be Tuple of 1,BOOLEAN;
A1: 1 - 1 = 0;
  assume z1=<*TRUE*>;
  then
A2: z1/.1 <> FALSE by FINSEQ_4:16;
  1 in Seg 1;
  then
A3: (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1)) by Def3
    .= 2 to_power(1-'1) by A2,FUNCOP_1:def 8;
  ex k being Element of NAT st Binary( z1 ) = <* k *> by FINSEQ_2:97;
  hence Absval(z1) = addnat $$ <* 2 to_power(1-'1) *> by A3,FINSEQ_4:16
    .= 2 to_power(1-'1) by FINSOP_1:11
    .= 2 to_power(0) by A1,XREAL_0:def 2
    .= 1 by POWER:24;
end;

definition
  let n1,n2 be Nat;
  let D be non empty set;
  let z1 be Tuple of n1,D;
  let z2 be Tuple of n2,D;
  redefine func z1 ^ z2 -> Tuple of n1+n2,D;
  coherence by FINSEQ_2:107;
end;

definition
  let D be non empty set;
  let d be Element of D;
  redefine func <* d *> -> Tuple of 1,D;
  coherence
   proof
     <*d*> in 1-tuples_on D by FINSEQ_2:98;
    hence thesis;
   end;
end;

theorem Th17:
  for z1,z2 being Tuple of n,BOOLEAN holds for d1,d2 being Element
of BOOLEAN holds for i being Nat holds i in Seg n implies carry(z1^<*d1*>,z2^<*
  d2*>)/.i = carry(z1,z2)/.i
proof
  let z1,z2 be Tuple of n,BOOLEAN;
  let d1,d2 be Element of BOOLEAN;
  defpred P[Nat] means $1 in Seg n implies carry(z1^<*d1*>,z2^<*d2*>)/.$1 =
  carry(z1,z2)/.$1;
  let i be Nat;
A1: for i being non empty Nat st P[i] holds P[i+1]
  proof
    let i be non empty Nat;
    assume
A2: P[i];
    assume i+1 in Seg n;
    then i+1 > i & i+1 <= n by FINSEQ_1:1,XREAL_1:29;
    then
A3: i < n by XXREAL_0:2;
    n <= n+1 by NAT_1:11;
    then
A4: i < n+1 by A3,XXREAL_0:2;
A5: 1 <= i by NAT_1:14;
    then i in Seg n by A3,FINSEQ_1:1;
    then (z1^<*d1*>)/.i = z1/.i & (z2^<*d2*>)/.i = z2/.i by Th1;
    hence
    carry(z1^<*d1*>,z2^<*d2*>)/.(i+1) = ((z1/.i) '&' (z2/.i)) 'or' (z1/.i
    ) '&' (carry(z1,z2)/.i) 'or' (z2/.i) '&' (carry(z1,z2)/.i) by A2,A5,A3,A4
,Def2,FINSEQ_1:1
      .= carry(z1,z2)/.(i+1) by A5,A3,Def2;
  end;
A6: P[1]
  proof
    assume 1 in Seg n;
    thus carry(z1^<*d1*>,z2^<*d2*>)/.1 = FALSE by Def2
      .= carry(z1,z2)/.1 by Def2;
  end;
A7: for i being non empty Nat holds P[i] from NAT_1:sch 10(A6,A1);
  assume
A8: i in Seg n;
  then i is non empty by FINSEQ_1:1;
  hence thesis by A8,A7;
end;

theorem Th18:
  for z1,z2 being Tuple of n,BOOLEAN, d1,d2 being Element of
  BOOLEAN holds add_ovfl(z1,z2) = carry(z1^<*d1*>,z2^<*d2*>)/.(n+1)
proof
  let z1,z2 be Tuple of n,BOOLEAN, d1,d2 be Element of BOOLEAN;
A1: 1 <= n & n < n+1 by NAT_1:14,XREAL_1:29;
A2: n in Seg n by FINSEQ_1:3;
  then
A3: z2/.n = (z2^<*d2*>)/.n by Th1;
  carry(z1^<*d1*>,z2^<*d2*>)/.n = carry(z1,z2)/.n & z1/.n = (z1^<*d1*>)/.n
  by A2,Th1,Th17;
  hence thesis by A3,A1,Def2;
end;

theorem Th19:
  for z1,z2 being Tuple of n,BOOLEAN, d1,d2 being Element of
BOOLEAN holds z1^<*d1*> + z2^<*d2*> = (z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,
  z2)*>
proof
  let z1,z2 be Tuple of n,BOOLEAN, d1,d2 be Element of BOOLEAN;
  for i st i in Seg (n+1) holds ((z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,
z2)*>)/.i = ((z1^<*d1*>)/.i) 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1^<*d1*>,z2^
  <*d2*>)/.i)
  proof
A1: Seg (n+1) = Seg (n) \/ {. n+1 .} by FINSEQ_1:9;
    let i such that
A2: i in Seg (n+1);
    per cases by A2,A1,XBOOLE_0:def 3;
    suppose
A3:   i in Seg n;
      hence ((z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,z2)*>)/.i = (z1+z2)/.i
       by Th1
        .= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A3,Def5
        .= ((z1^<*d1*>)/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A3,Th1
        .= ((z1^<*d1*>)/.i) 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1,z2)/.i)
      by A3,Th1
        .= ((z1^<*d1*>)/.i) 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1^<*d1*>,z2
      ^<*d2*>)/.i) by A3,Th17;
    end;
    suppose
      i in {. n+1 .};
      then
A4:   i=n+1 by TARSKI:def 1;
      hence (((z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,z2)*>)/.i) = d1 'xor' d2
      'xor' add_ovfl(z1,z2) by Th2
        .= d1 'xor' d2 'xor' (carry(z1^<*d1*>,z2^<*d2*>)/.i) by A4,Th18
        .= d1 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1^<*d1*>,z2^<*d2*>)/.i)
      by A4,Th2
        .= ((z1^<*d1*>)/.i) 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1^<*d1*>,z2
      ^<*d2*>)/.i) by A4,Th2;
    end;
  end;
  hence thesis by Def5;
end;

theorem Th20:
  for z being Tuple of n,BOOLEAN, d being Element of BOOLEAN holds
  Absval(z^<*d*>) = Absval(z)+IFEQ(d,FALSE,0,2 to_power n)
proof
  let z be Tuple of n,BOOLEAN, d be Element of BOOLEAN;
  for i st i in Seg (n+1) holds ((Binary(z)^<*IFEQ(d,FALSE,0,2 to_power(n)
  )*>)/.i) = IFEQ((z^<*d*>)/.i,FALSE,0,2 to_power(i-'1))
  proof
A1: Seg (n+1) = Seg (n) \/ {. n+1 .} by FINSEQ_1:9;
    let i such that
A2: i in Seg (n+1);
    per cases by A2,A1,XBOOLE_0:def 3;
    suppose
A3:   i in Seg n;
      hence (Binary(z)^<*IFEQ(d,FALSE,0,2 to_power(n))*>)/.i = (Binary(z))/.i
      by Th1
        .= IFEQ(z/.i,FALSE,0,2 to_power(i-'1)) by A3,Def3
        .= IFEQ((z^<*d*>)/.i,FALSE,0,2 to_power(i-'1)) by A3,Th1;
    end;
    suppose
      i in {. n+1 .};
      then
A4:   i=n+1 by TARSKI:def 1;
      hence
      (Binary(z)^<*IFEQ(d,FALSE,0,2 to_power(n))*>)/.i = IFEQ(d,FALSE,0,2
      to_power(n)) by Th2
        .= IFEQ((z^<*d*>)/.i,FALSE,0,2 to_power(n)) by A4,Th2
        .= IFEQ((z^<*d*>)/.i,FALSE,0,2 to_power(i-'1)) by A4,NAT_D:34;
    end;
  end;
  hence Absval(z^<*d*>) = addnat $$ (Binary(z)^<*IFEQ(d,FALSE,0,2 to_power(n))
  *>) by Def3
    .= addnat.(addnat$$Binary(z),IFEQ(d,FALSE,0,2 to_power(n))) by FINSOP_1:4
    .= Absval(z)+IFEQ(d,FALSE,0,2 to_power n) by BINOP_2:def 23;
end;

theorem Th21:
  for n for z1,z2 being Tuple of n,BOOLEAN holds Absval(z1+z2) +
  IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n)) = Absval(z1) + Absval(z2)
proof
  defpred P[non zero Nat] means for z1,z2 being Tuple of $1, BOOLEAN holds
  Absval(z1+z2) + IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power $1) = Absval(z1) +
  Absval(z2);
  set f = FALSE, t = TRUE;
A1: for n being non zero Nat st P[n] holds P[n+1]
  proof
    let n;
    assume
A2: P[n];
    let z1,z2 be Tuple of n+1,BOOLEAN;
    consider t1 being (Element of n-tuples_on BOOLEAN), d1 being Element of
    BOOLEAN such that
A3: z1 = t1^<*d1*> by FINSEQ_2:117;
    consider t2 being (Element of n-tuples_on BOOLEAN), d2 being Element of
    BOOLEAN such that
A4: z2 = t2^<*d2*> by FINSEQ_2:117;
A5: IFEQ(add_ovfl(t1,t2),FALSE,0,2 to_power(n)) is Element of NAT;
A6: IFEQ(d1,FALSE,0,2 to_power n) is Element of NAT & IFEQ(d2,FALSE,0,2
    to_power n) is Element of NAT;
    IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n+1)) is Element of NAT &
IFEQ(d1 'xor' d2 'xor' add_ovfl(t1,t2),FALSE,0,2 to_power n) is Element of NAT;
    then reconsider
    C1= IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n+1)), C2= IFEQ(d1
    'xor' d2 'xor' add_ovfl(t1,t2),FALSE,0,2 to_power n), C3= IFEQ(d1,FALSE,0,2
to_power n), C4= IFEQ(d2,FALSE,0,2 to_power n), C5= IFEQ(add_ovfl(t1,t2),FALSE,
    0,2 to_power(n)) as Real by A6,A5;
A7: add_ovfl(z1,z2) = d1 '&' ((t2^<*d2*>)/.(n+1)) 'or' ((t1^<*d1*>)/.(n+1
)) '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) 'or' ((t2^<*d2*>)/.(n+1)) '&' (carry
    (t1^<*d1*>,t2^<*d2*>)/.(n+1)) by A3,A4,Th2
      .= d1 '&' d2 'or' ((t1^<*d1*>)/.(n+1)) '&' (carry(t1^<*d1*>,t2^<*d2*>)
/.(n+1)) 'or' ((t2^<*d2*>)/.(n+1)) '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) by
Th2
      .= d1 '&' d2 'or' d1 '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) 'or' ((t2
    ^<*d2*>)/.(n+1)) '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) by Th2
      .= d1 '&' d2 'or' d1 '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) 'or' d2
    '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) by Th2
      .= d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' (carry(t1^<*d1*>,
    t2^<*d2*>)/.(n+1)) by Th18
      .= d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,t2)
    by Th18;
A8: C2 + C1 = C5 + C3 + C4
    proof
      now
        per cases;
        suppose
A9:       d1=f;
          then
A10:      C3=0 by FUNCOP_1:def 8;
          now
            per cases;
            suppose
A11:          d2=f;
              then C4=0 by FUNCOP_1:def 8;
              hence thesis by A7,A9,A11,FUNCOP_1:def 8;
            end;
            suppose
A12:          d2 <> f;
              then
A13:          C4=2 to_power n by FUNCOP_1:def 8;
              now
                per cases;
                suppose
A14:              add_ovfl(t1,t2)=f;
                  then C5=0 by FUNCOP_1:def 8;
                  hence thesis by A7,A9,A14,FUNCOP_1:def 8;
                end;
                suppose
A15:              add_ovfl(t1,t2)<>f;
                  d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' add_ovfl(t1
                  ,t2) by A9,A12,XBOOLEAN:def 3
                    .= f by A15,XBOOLEAN:def 3;
                  then
A16:              C2=0 by FUNCOP_1:def 8;
A17:              C5=2 to_power(n) by A15,FUNCOP_1:def 8;
                  d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
add_ovfl(t1,t2) = f 'or' f 'or' t '&' add_ovfl(t1,t2) by A9,A12,XBOOLEAN:def 3
                    .= t by A15,XBOOLEAN:def 3;
                  then C1=2 to_power(n+1) by A7,FUNCOP_1:def 8;
                  hence C2 + C1 = 2 to_power n * 2 to_power 1 by A16,POWER:27
                    .= 2 * 2 to_power n by POWER:25
                    .= C5 + C3 + C4 by A10,A13,A17;
                end;
              end;
              hence thesis;
            end;
          end;
          hence thesis;
        end;
        suppose
A18:      d1 <>f;
          then
A19:      C3=2 to_power n by FUNCOP_1:def 8;
          now
            per cases;
            suppose
A20:          d2=f;
              then
A21:          C4=0 by FUNCOP_1:def 8;
              now
                per cases;
                suppose
                  add_ovfl(t1,t2)=f;
                  hence thesis by A7,A20,A21,FUNCOP_1:def 8;
                end;
                suppose
A22:              add_ovfl(t1,t2)<>f;
                  d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' add_ovfl(t1
                  ,t2) by A18,A20,XBOOLEAN:def 3
                    .= f by A22,XBOOLEAN:def 3;
                  then
A23:              C2=0 by FUNCOP_1:def 8;
A24:              C5=2 to_power(n) by A22,FUNCOP_1:def 8;
                  d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
add_ovfl(t1,t2) = f 'or' t '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,t2) by
A18,A20,XBOOLEAN:def 3
                    .= f 'or' t '&' t 'or' d2 '&' add_ovfl(t1,t2) by A22,
XBOOLEAN:def 3
                    .= t;
                  then C1=2 to_power (n+1) by A7,FUNCOP_1:def 8;
                  hence C2 + C1 = 2 to_power n * 2 to_power 1 by A23,POWER:27
                    .= 2 * 2 to_power n by POWER:25
                    .= C5 + C3 + C4 by A19,A21,A24;
                end;
              end;
              hence thesis;
            end;
            suppose
A25:          d2<>f;
              then
A26:          C4=2 to_power n by FUNCOP_1:def 8;
              now
                per cases;
                suppose
A27:              add_ovfl(t1,t2)=f;
                  d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' d2 'xor'
                  add_ovfl(t1,t2) by A18,XBOOLEAN:def 3
                    .= f by A25,A27,XBOOLEAN:def 3;
                  then
A28:              C2=0 by FUNCOP_1:def 8;
A29:              C5=0 by A27,FUNCOP_1:def 8;
                  d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
add_ovfl(t1,t2) = t '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,
                  t2) by A18,XBOOLEAN:def 3
                    .= t '&' t 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
                  add_ovfl(t1,t2) by A25,XBOOLEAN:def 3
                    .= t;
                  then C1=2 to_power (n+1) by A7,FUNCOP_1:def 8;
                  hence C2 + C1 = 2 to_power n * 2 to_power 1 by A28,POWER:27
                    .= 2 * 2 to_power n by POWER:25
                    .= C5 + C3 + C4 by A19,A26,A29;
                end;
                suppose
A30:              add_ovfl(t1,t2)<>f;
                  d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' d2 'xor'
                  add_ovfl(t1,t2) by A18,XBOOLEAN:def 3
                    .= f 'xor' add_ovfl(t1,t2) by A25,XBOOLEAN:def 3
                    .= t by A30,XBOOLEAN:def 3;
                  then
A31:              C2=2 to_power n by FUNCOP_1:def 8;
                  d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
add_ovfl(t1,t2) = t '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,
                  t2) by A18,XBOOLEAN:def 3
                    .= t '&' t 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&'
                  add_ovfl(t1,t2) by A25,XBOOLEAN:def 3
                    .= t;
                  then C1=2 to_power (n+1) by A7,FUNCOP_1:def 8;
                  hence
                  C2 + C1 = 2 to_power n + 2 to_power n * 2 to_power 1 by A31,
POWER:27
                    .= 2 to_power n + 2 * 2 to_power n by POWER:25
                    .= 2 to_power n + 2 to_power n + 2 to_power n
                    .= C5 + C3 + C4 by A19,A26,A30,FUNCOP_1:def 8;
                end;
              end;
              hence thesis;
            end;
          end;
          hence thesis;
        end;
      end;
      hence thesis;
    end;
    thus Absval(z1+z2) + IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n+1)) =
Absval((t1+t2)^<*d1 'xor' d2 'xor' add_ovfl(t1,t2)*>) + IFEQ(add_ovfl(z1,z2),
    FALSE,0,2 to_power (n+1)) by A3,A4,Th19
      .=Absval(t1+t2) + C2 + C1 by Th20
      .= Absval(t1+t2) + C5 + C3 + C4 by A8
      .= Absval(t1) + Absval(t2) + C3 + C4 by A2
      .= Absval(t1) + C3 + (Absval(t2) + C4 )
      .= Absval(t1)+IFEQ(d1,FALSE,0,2 to_power n) + Absval(t2^<*d2*>) by Th20
      .= Absval(z1) + Absval(z2) by A3,A4,Th20;
  end;
A32: P[1]
  proof
    reconsider T= <*t*>,F= <*f*> as Tuple of 1,BOOLEAN;
    let z1,z2 be Tuple of 1, BOOLEAN;
A33: carry(z1,z2)/.1 = f by Def2;
A34: Absval(T)=1 by Th16;
A35: Absval(F)=0 by Th15;
    per cases by Th14;
    suppose
A36:  z1=<*f*> & z2=<*f*>;
A37:  now
        let i;
        assume
A38:    i in Seg 1;
        then
A39:    i=1 by FINSEQ_1:2,TARSKI:def 1;
        thus F/.i = (z1/.1) 'xor' f 'xor' f by A36,A38,FINSEQ_1:2,TARSKI:def 1
          .= (z1/.1) 'xor' (z2/.1) 'xor' f by A36,FINSEQ_4:16
          .= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A39,Def2;
      end;
      add_ovfl(z1,z2) = f by A33,A36,FINSEQ_4:16;
      then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 by FUNCOP_1:def 8;
      hence thesis by A35,A36,A37,Def5;
    end;
    suppose
A40:  z1=<*t*> & z2=<*f*>;
A41:  now
        let i;
        assume
A42:    i in Seg 1;
        then
A43:    i=1 by FINSEQ_1:2,TARSKI:def 1;
        thus T/.i = (z1/.1) 'xor' f 'xor' f by A40,A42,FINSEQ_1:2,TARSKI:def 1
          .= (z1/.1) 'xor' (z2/.1) 'xor' f by A40,FINSEQ_4:16
          .= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A43,Def2;
      end;
      add_ovfl(z1,z2) = f by A33,A40,FINSEQ_4:16;
      then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 by FUNCOP_1:def 8;
      hence thesis by A35,A40,A41,Def5;
    end;
    suppose
A44:  z1=<*f*> & z2=<*t*>;
A45:  now
        let i;
        assume i in Seg 1;
        then
A46:    i=1 by FINSEQ_1:2,TARSKI:def 1;
        hence T/.i = 'not' t 'xor' t 'xor' f by FINSEQ_4:16
          .= (z1/.1) 'xor' t 'xor' f by A44,FINSEQ_4:16
          .= (z1/.1) 'xor' (z2/.1) 'xor' f by A44,FINSEQ_4:16
          .= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A46,Def2;
      end;
      add_ovfl(z1,z2) = f by A33,A44,FINSEQ_4:16;
      then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 by FUNCOP_1:def 8;
      hence thesis by A35,A44,A45,Def5;
    end;
    suppose
A47:  z1=<*t*> & z2=<*t*>;
      now
        let i;
        assume i in Seg 1;
        then
A48:    i=1 by FINSEQ_1:2,TARSKI:def 1;
        hence F/.i = t 'xor' t 'xor' 'not' t by FINSEQ_4:16
          .= (z1/.1) 'xor' t 'xor' f by A47,FINSEQ_4:16
          .= (z1/.1) 'xor' (z2/.1) 'xor' f by A47,FINSEQ_4:16
          .= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A48,Def2;
      end;
      then
A49:  z1+z2=<*f*> by Def5;
      add_ovfl(z1,z2) = t by A33,A47,FINSEQ_4:16;
      then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 2 to_power 1 by
FUNCOP_1:def 8
        .= 2 by POWER:25;
      hence thesis by A34,A35,A47,A49;
    end;
  end;
  thus for n being non zero Nat holds P[n] from NAT_1:sch 10(A32,A1);
end;

theorem
  for z1,z2 being Tuple of n,BOOLEAN st z1,z2 are_summable holds Absval(
  z1+z2) = Absval(z1) + Absval(z2)
proof
  let z1,z2 be Tuple of n,BOOLEAN;
  assume z1,z2 are_summable;
  then add_ovfl(z1,z2) = FALSE by Def7;
  then IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n))=0 by FUNCOP_1:def 8;
  hence
  Absval(z1+z2) = Absval(z1+z2) + IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (n))
    .= Absval(z1) + Absval(z2) by Th21;
end;