:: Binary Arithmetics. Addition and Subtraction of Integers
::  by Yasuho Mizuhara and Takaya Nishiyama
::
:: Received March 18, 1994
:: Copyright (c) 1994 Association of Mizar Users

environ

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

begin

reserve i,j,n for Nat;
reserve m for non empty Nat;
reserve p,q for Tuple of n, BOOLEAN;
reserve d,d1,d2 for Element of BOOLEAN;

Lm1: len p = n & len q = n & (for i st i in Seg n holds p/.i = q/.i)
implies p = q
proof
  assume that
A1: len p = n and
A2: len q = n and
A3: for i st i in Seg n holds p/.i = q/.i;
A4: dom p = Seg n by A1,FINSEQ_1:def 3;
A5: for i being Nat st i in dom p holds p.i = q.i
  proof
    let i be Nat;
    assume
A6: i in dom p;
A7: i in dom q by A2,A4,A6,FINSEQ_1:def 3;
A8: p/.i=p.i by A6,PARTFUN1:def 8;
A9: q/.i = q.i by A7,PARTFUN1:def 8;
    thus thesis by A3,A4,A6,A8,A9;
  end;
  thus thesis by A1,A2,A5,FINSEQ_2:10;
end;

definition
  let n be Nat;
  func Bin1 (n) -> Tuple of n, BOOLEAN means
  :Def1:
  for i st i in Seg n holds it/.i = IFEQ(i,1,TRUE,FALSE);
  existence
  proof
    deffunc F(set) = IFEQ($1,1,TRUE,FALSE);
    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;
    z is Element of n-tuples_on BOOLEAN by A1,FINSEQ_2:110;
    then reconsider z as Tuple of n, BOOLEAN;
    take z;
    let i;
    assume
A4: i in Seg n;
A5: i in dom z by A1,A4,FINSEQ_1:def 3;
    thus z/.i = z.i by A5,PARTFUN1:def 8
      .= IFEQ(i,1,TRUE,FALSE) by A2,A3,A4;
  end;
  uniqueness
  proof
    let z1, z2 be Tuple of n, BOOLEAN such that
A6: for i st i in Seg n holds z1/.i = IFEQ(i,1,TRUE,FALSE) and
A7: for i st i in Seg n holds z2/.i = IFEQ(i,1,TRUE,FALSE);
A8: len z1 = n by FINSEQ_1:def 18;
A9: len z2 = n by FINSEQ_1:def 18;
A10: dom z1 = Seg n by A8,FINSEQ_1:def 3;
A11: now
      let j be Nat;
      assume
A12:  j in dom z1;
A13:  j in dom z2 by A9,A10,A12,FINSEQ_1:def 3;
      thus z1.j = z1/.j by A12,PARTFUN1:def 8
        .= IFEQ(j,1,TRUE,FALSE) by A6,A10,A12
        .= z2/.j by A7,A10,A12
        .= z2.j by A13,PARTFUN1:def 8;
    end;
    thus thesis by A8,A9,A11,FINSEQ_2:10;
  end;
end;

definition
  let n be non empty Nat, x be Tuple of n, BOOLEAN;
  func Neg2 (x) -> Tuple of n,BOOLEAN equals
  'not' x + Bin1 (n);
  correctness;
end;

definition
  let n be Nat, x be Tuple of n, BOOLEAN;
  func Intval (x) -> Integer equals
  :Def3:
  Absval (x) if x/.n = FALSE
  otherwise Absval (x) - 2 to_power n;
  correctness;
end;

definition
  let n be non empty Nat, z1,z2 be Tuple of n, BOOLEAN;
  func Int_add_ovfl(z1,z2) -> Element of BOOLEAN equals
  'not' (z1/.n) '&' 'not' (z2/.n) '&' (carry(z1,z2)/.n);
  correctness;
end;

definition
  let n be non empty Nat, z1,z2 be Tuple of n, BOOLEAN;
  func Int_add_udfl(z1,z2) -> Element of BOOLEAN equals
  (z1/.n) '&' (z2/.n) '&' 'not' (carry(z1,z2)/.n);
  correctness;
end;

canceled 2;

theorem
  for z1 being Tuple of 2, BOOLEAN holds
  z1=<*FALSE*>^<*FALSE*> implies Intval(z1) = 0
proof
  let z1 be Tuple of 2,BOOLEAN;
  assume
A1: z1 = <*FALSE*>^<*FALSE*>;
  consider k1,k2 being Element of NAT such that
A2: Binary (z1) = <* k1,k2 *> by FINSEQ_2:120;
A3: z1 = <*FALSE,FALSE*> by A1,FINSEQ_1:def 9;
A4: z1/.1 = FALSE by A3,FINSEQ_4:26;
A5: z1/.2 = FALSE by A3,FINSEQ_4:26;
A6: 1 in Seg 1 & Seg 1 c= Seg 2 by FINSEQ_1:5,7;
A7: (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1))
  by A6,BINARITH:def 6
    .= 0 by A4,FUNCOP_1:def 8;
A8: 2 in Seg 2 by FINSEQ_1:5;
A9: (Binary(z1))/.2 = IFEQ(z1/.2,FALSE,0,2 to_power(2-'1)) by A8,
  BINARITH:def 6
    .= 0 by A5,FUNCOP_1:def 8;
  A10: (Binary(z1))/.1 = k1 & (Binary(z1))/.2 = k2 by A2,FINSEQ_4:26;
A11: Absval(z1) = addnat $$ (<* 0,0 *>) by A2,A7,A9,A10,BINARITH:def 7
    .= addnat $$ (<* 0 *>^<* 0 *>) by FINSEQ_1:def 9
    .= addnat.(addnat$$<* 0 *>,addnat$$<* 0 *>) by FINSOP_1:6
    .= addnat.(0,addnat$$<* 0 *>) by FINSOP_1:12
    .= addnat.(0,0) by FINSOP_1:12
    .= 0 + 0 by BINOP_2:def 23
    .= 0;
  thus thesis by A5,A11,Def3;
end;

theorem Th4:
  for z1 being Tuple of 2, BOOLEAN holds
  z1=<*TRUE*>^<*FALSE*> implies Intval(z1) = 1
proof
  let z1 be Tuple of 2,BOOLEAN;
  assume
A1: z1 = <*TRUE*>^<*FALSE*>;
  consider k1,k2 being Element of NAT such that
A2: Binary (z1) = <* k1,k2 *> by FINSEQ_2:120;
A3: z1 = <*TRUE,FALSE*> by A1,FINSEQ_1:def 9;
A4: z1/.1 = TRUE by A3,FINSEQ_4:26;
A5: z1/.2 = FALSE by A3,FINSEQ_4:26;
A6: 1 in Seg 1 & Seg 1 c= Seg 2 by FINSEQ_1:5,7;
A7: (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1))
  by A6,BINARITH:def 6
    .= 2 to_power(1-'1) by A4,FUNCOP_1:def 8;
A8: 1 - 1 = 0;
A9: 1 -' 1 = 0 by A8,XREAL_0:def 2;
A10: (Binary(z1))/.1 = 1 by A7,A9,POWER:29;
A11: 2 in Seg 2 by FINSEQ_1:5;
A12: (Binary(z1))/.2 = IFEQ(z1/.2,FALSE,0,2 to_power(2-'1)) by A11,
  BINARITH:def 6
    .= 0 by A5,FUNCOP_1:def 8;
  A13: (Binary(z1))/.1 = k1 & (Binary(z1))/.2 = k2 by A2,FINSEQ_4:26;
A14: Absval(z1) = addnat $$ (<* 1,0 *>) by A2,A10,A12,A13,BINARITH:def 7
    .= addnat $$ (<* 1 *>^<* 0 *>) by FINSEQ_1:def 9
    .= addnat.(addnat$$<* 1 *>,addnat$$<* 0 *>) by FINSOP_1:6
    .= addnat.(1,addnat$$<* 0 *>) by FINSOP_1:12
    .= addnat.(1,0) by FINSOP_1:12
    .= 1 + 0 by BINOP_2:def 23
    .= 1;
  thus thesis by A5,A14,Def3;
end;

theorem
  for z1 being Tuple of 2, BOOLEAN holds
  z1=<*FALSE*>^<*TRUE*> implies Intval(z1) = -2
proof
  let z1 be Tuple of 2,BOOLEAN;
  assume
A1: z1 = <*FALSE*>^<*TRUE*>;
  consider k1,k2 being Element of NAT such that
A2: Binary (z1) = <* k1,k2 *> by FINSEQ_2:120;
A3: z1 = <*FALSE,TRUE*> by A1,FINSEQ_1:def 9;
A4: z1/.1 = FALSE by A3,FINSEQ_4:26;
A5: z1/.2 = TRUE by A3,FINSEQ_4:26;
A6: Intval(z1) = Absval(z1) - 2 to_power (1 + 1) by A5,Def3
    .= Absval(z1) - (2 to_power 1 * 2 to_power 1) by POWER:32
    .= Absval(z1) - (2 * 2 to_power 1) by POWER:30
    .= Absval(z1) - (2 * 2) by POWER:30
    .= Absval(z1) - 4;
A7: 1 in Seg 1 & Seg 1 c= Seg 2 by FINSEQ_1:5,7;
A8: (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1))
  by A7,BINARITH:def 6
    .= 0 by A4,FUNCOP_1:def 8;
A9: 2 in Seg 2 by FINSEQ_1:5;
A10: (Binary(z1))/.2 = IFEQ(z1/.2,FALSE,0,2 to_power(2-'1)) by A9,
  BINARITH:def 6
    .= 2 to_power(2-'1) by A5,FUNCOP_1:def 8;
A11: 2 - 1 = 1;
A12: 2 -' 1 = 1 by A11,XREAL_0:def 2;
A13: (Binary(z1))/.2 = 2 by A10,A12,POWER:30;
  A14: (Binary(z1))/.1 = k1 & (Binary(z1))/.2 = k2 by A2,FINSEQ_4:26;
A15: Absval(z1) = addnat $$ (<* 0,2 *>) by A2,A8,A13,A14,BINARITH:def 7
    .= addnat $$ (<* 0 *>^<* 2 *>) by FINSEQ_1:def 9
    .= addnat.(addnat$$<* 0 *>,addnat$$<* 2 *>) by FINSOP_1:6
    .= addnat.(0,addnat$$<* 2 *>) by FINSOP_1:12
    .= addnat.(0,2) by FINSOP_1:12
    .= 0 + 2 by BINOP_2:def 23
    .= 2;
  thus thesis by A6,A15;
end;

theorem
  for z1 being Tuple of 2, BOOLEAN holds
  z1=<*TRUE*>^<*TRUE*> implies Intval(z1) = -1
proof
  let z1 be Tuple of 2,BOOLEAN;
  assume
A1: z1 = <*TRUE*>^<*TRUE*>;
  consider k1,k2 being Element of NAT such that
A2: Binary (z1) = <* k1,k2 *> by FINSEQ_2:120;
A3: z1 = <*TRUE,TRUE*> by A1,FINSEQ_1:def 9;
A4: z1/.1 <> FALSE by A3,FINSEQ_4:26;
A5: z1/.2 <> FALSE by A3,FINSEQ_4:26;
A6: Intval(z1) = Absval(z1) - 2 to_power (1 + 1) by A5,Def3
    .= Absval(z1) - (2 to_power 1 * 2 to_power 1) by POWER:32
    .= Absval(z1) - (2 * 2 to_power 1) by POWER:30
    .= Absval(z1) - (2 * 2) by POWER:30
    .= Absval(z1) - 4;
A7: 1 in Seg 1 & Seg 1 c= Seg 2 by FINSEQ_1:5,7;
A8: (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1))
  by A7,BINARITH:def 6
    .= 2 to_power(1-'1) by A4,FUNCOP_1:def 8;
A9: 1 - 1 = 0;
A10: 1 -' 1 = 0 by A9,XREAL_0:def 2;
A11: (Binary(z1))/.1 = 1 by A8,A10,POWER:29;
A12: 2 in Seg 2 by FINSEQ_1:5;
A13: (Binary(z1))/.2 = IFEQ(z1/.2,FALSE,0,2 to_power(2-'1)) by A12,
  BINARITH:def 6
    .= 2 to_power(2-'1) by A5,FUNCOP_1:def 8;
A14: 2 - 1 = 1;
A15: 2 -' 1 = 1 by A14,XREAL_0:def 2;
A16: (Binary(z1))/.2 = 2 by A13,A15,POWER:30;
  A17: (Binary(z1))/.1 = k1 & (Binary(z1))/.2 = k2 by A2,FINSEQ_4:26;
A18: Absval(z1) = addnat $$ (<* 1,2 *>) by A2,A11,A16,A17,BINARITH:def 7
    .= addnat $$ (<* 1 *>^<* 2 *>) by FINSEQ_1:def 9
    .= addnat.(addnat$$<* 1 *>,addnat$$<* 2 *>) by FINSOP_1:6
    .= addnat.(1,addnat$$<* 2 *>) by FINSOP_1:12
    .= addnat.(1,2) by FINSOP_1:12
    .= 1 + 2 by BINOP_2:def 23
    .= 3;
  thus thesis by A6,A18;
end;

theorem Th7:
  for i st i in Seg n & i = 1 holds (Bin1(n))/.i = TRUE
proof
  let i be Nat such that
A1: i in Seg n and
A2: i = 1;
  thus (Bin1(n))/.i = IFEQ(i,1,TRUE,FALSE) by A1,Def1
    .= TRUE by A2,FUNCOP_1:def 8;
end;

theorem Th8:
  for i st i in Seg n & i <> 1 holds (Bin1(n))/.i = FALSE
proof
  let i be Nat such that
A1: i in Seg n and
A2: i <> 1;
  thus (Bin1(n))/.i = IFEQ(i,1,TRUE,FALSE) by A1,Def1
    .= FALSE by A2,FUNCOP_1:def 8;
end;

theorem Th9:
  Bin1 (m+1) = Bin1 (m)^<*FALSE*>
proof
  A1: len(Bin1(m+1)) = m+1 & len(Bin1(m)^<*FALSE*>) = m+1 by FINSEQ_1:def 18;
A2: for i st i in Seg (m+1) holds (Bin1(m+1))/.i = (Bin1(m)^<*FALSE*>)/.i
  proof
    let i such that
A3: i in Seg (m+1);
    per cases by A3,FINSEQ_2:8;
    suppose
A4:   i in Seg m;
      thus (Bin1(m+1))/.i = (Bin1(m)^<*FALSE*>)/.i
      proof
        per cases;
        suppose
A5:       i = 1;
A6:       (Bin1(m)^<*FALSE*>)/.i = (Bin1(m))/.i by A4,BINARITH:2
            .= TRUE by A4,A5,Th7;
          thus thesis by A3,A5,A6,Th7;
        end;
        suppose
A7:       i <> 1;
A8:       (Bin1(m)^<*FALSE*>)/.i = (Bin1(m))/.i by A4,BINARITH:2
            .= FALSE by A4,A7,Th8;
          thus thesis by A3,A7,A8,Th8;
        end;
      end;
    end;
    suppose
A9:   i = m+1;
A10:  1 <> m + 1 by NAT_1:14;
A11:  (Bin1(m+1))/.i = FALSE by A3,A9,A10,Th8;
      thus thesis by A9,A11,BINARITH:3;
    end;
  end;
  thus thesis by A1,A2,Lm1;
end;

theorem Th10:
  for m holds Intval (Bin1(m)^<*FALSE*>) = 1
proof
  defpred P[non empty Nat] means Intval (Bin1($1)^<*FALSE*>) = 1;
A1: P[1]
  proof
    consider k being Element of BOOLEAN such that
A2: Bin1(1) = <* k *> by FINSEQ_2:117;
A3: (Bin1(1))/.1 = k by A2,FINSEQ_4:25;
A4: 1 in Seg 1 by FINSEQ_1:5;
A5: Bin1(1) = <*TRUE*> by A2,A3,A4,Th7;
    thus thesis by A5,Th4;
  end;
A6: now
    let m be non empty Nat such that
A7: P[m];
A8: (Bin1(m)^<*FALSE*>)/.(m+1) = FALSE by BINARITH:3;
A9: Absval(Bin1(m)^<*FALSE*>) = 1 by A7,A8,Def3;
A10: (Bin1(m+1)^<*FALSE*>)/.(m+1+1) = FALSE by BINARITH:3;
A11: Intval(Bin1(m+1)^<*FALSE*>) = Absval(Bin1(m+1)^<*FALSE*>) by A10,Def3
      .= Absval(Bin1(m)^<*FALSE*>^<*FALSE*>) by Th9
      .= Absval(Bin1(m)^<*FALSE*>)
    + IFEQ(FALSE,FALSE,0,2 to_power(m+1)) by BINARITH:46
      .= 1 + 0 by A9,FUNCOP_1:def 8
      .= 1;
    thus P[m+1] by A11;
  end;
  thus for m holds P[m] from NAT_1:sch 10(A1,A6);
end;

theorem Th11:
  for z being Tuple of m, BOOLEAN for d being Element of BOOLEAN holds
  'not' (z^<* d *>) = 'not' z^<* 'not' d *>
proof
  let z be Tuple of m,BOOLEAN;
  let d;
  A1: len('not' (z^<*d*>))= m+1 & len('not' z^<*'not' d*>) = m+1 by
  FINSEQ_1:def 18;
A2: for i st i in Seg (m+1) holds
  ('not' (z^<*d*>))/.i = ('not' z^<*'not' d*>)/.i
  proof
    let i such that
A3: i in Seg (m+1);
    per cases by A3,FINSEQ_2:8;
    suppose
A4:   i in Seg m;
A5:   ('not' (z^<*d*>))/.i = 'not' ((z^<*d*>)/.i) by A3,BINARITH:def 4
        .= 'not' (z/.i) by A4,BINARITH:2;
A6:   ('not' z^<*'not' d*>)/.i = ('not' z)/.i by A4,BINARITH:2
        .= 'not' (z/.i) by A4,BINARITH:def 4;
      thus thesis by A5,A6;
    end;
    suppose
A7:   i = m + 1;
A8:   ('not' (z^<*d*>))/.i = 'not' ((z^<*d*>)/.i) by A3,BINARITH:def 4
        .= 'not' d by A7,BINARITH:3;
      thus thesis by A7,A8,BINARITH:3;
    end;
  end;
  thus thesis by A1,A2,Lm1;
end;

theorem Th12:
  for z being Tuple of m, BOOLEAN for d being Element of BOOLEAN holds
  Intval(z^<*d*>) =
  Absval(z)-(IFEQ(d,FALSE,0,2 to_power(m)) qua Nat)
proof
  let z be Tuple of m, BOOLEAN;
  let d;
  per cases by XBOOLEAN:def 3;
  suppose
A1: d = FALSE;
A2: (z^<*d*>)/.(m+1) = FALSE by A1,BINARITH:3;
A3: Intval(z^<*d*>) = Absval(z^<*d*>) by A2,Def3
      .= Absval(z)+IFEQ(d,FALSE,0,2 to_power(m)) by BINARITH:46
      .= Absval(z)+0 by A1,FUNCOP_1:def 8
      .= Absval(z);
A4: Absval(z)-(IFEQ(d,FALSE,0,2 to_power(m)) qua Nat)
    = Absval(z) - 0 by A1,FUNCOP_1:def 8
      .= Absval(z);
    thus thesis by A3,A4;
  end;
  suppose
A5: d = TRUE;
A6: (z^<*d*>)/.(m+1) <> FALSE by A5,BINARITH:3;
A7: Intval(z^<*d*>) = Absval(z^<*d*>) - 2 to_power(m+1) by A6,Def3
      .= Absval(z) + IFEQ(d,FALSE,0,2 to_power m)-2 to_power(m+1)
    by BINARITH:46
      .= Absval(z) + 2 to_power m - 2 to_power(m+1)
    by A5,FUNCOP_1:def 8
      .= Absval(z) + 2 to_power m - (2 to_power m * 2 to_power 1) by POWER:32
      .= Absval(z) + 2 to_power m - 2*2 to_power m by POWER:30
      .= Absval(z) - 2 to_power m;
    thus thesis by A5,A7,FUNCOP_1:def 8;
  end;
end;

theorem Th13:
  for z1,z2 being Tuple of m, BOOLEAN for d1,d2 being Element of BOOLEAN holds
  Intval(z1^<*d1*>+z2^<*d2*>)
  + IFEQ(Int_add_ovfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1))
  - IFEQ(Int_add_udfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1))
  = Intval(z1^<*d1*>) + Intval(z2^<*d2*>)
proof
  let z1,z2 be Tuple of m,BOOLEAN;
  let d1,d2 be Element of BOOLEAN;
  set f = FALSE, t = TRUE;
A1: Absval(z1+z2) = Absval(z1) + Absval(z2)
  - IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m)
  proof
    set siki1 = Absval(z1+z2),
    siki2 = IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m);
A2: siki1 + siki2 - siki2 = siki1;
    thus thesis by A2,BINARITH:47;
  end;
A3: Intval(z1^<*d1*> + z2^<*d2*>)
  = Intval((z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,z2)*>) by BINARITH:45
    .= Absval(z1) + Absval(z2) - IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m)
  - IFEQ(d1 'xor' d2 'xor' add_ovfl(z1,z2),FALSE,0, 2 to_power m) by A1,Th12;
A4: Int_add_ovfl(z1^<*d1*>,z2^<*d2*>)
  = 'not' d1 '&' 'not' ((z2^<*d2*>)/.(m+1)) '&'
  ((carry(z1^<*d1*>,z2^<*d2*>))/.(m+1)) by BINARITH:3
    .= 'not' d1 '&' 'not' d2 '&' ((carry(z1^<*d1*>,z2^<*d2*>))/.(m+1))
  by BINARITH:3
    .= 'not' d1 '&' 'not' d2 '&' add_ovfl(z1,z2) by BINARITH:44;
A5: Int_add_udfl(z1^<*d1*>,z2^<*d2*>) = d1 '&' ((z2^<*d2*>)/.(m+1)) '&'
  'not' ((carry(z1^<*d1*>,z2^<*d2*>))/.(m+1)) by BINARITH:3
    .= d1 '&' d2 '&' 'not' ((carry(z1^<*d1*>,z2^<*d2*>))/.(m+1)) by BINARITH:3
    .= d1 '&' d2 '&' 'not' add_ovfl(z1,z2) by BINARITH:44;
A6: Intval(z1^<*d1*>) = Absval(z1)-IFEQ(d1,FALSE,0,2 to_power m) by Th12;
A7: Intval(z2^<*d2*>) = Absval(z2)-IFEQ(d2,FALSE,0,2 to_power m) by Th12;
  per cases by XBOOLEAN:def 3;
  suppose
A8: d1 = f & d2 = f;
A9: Absval(z1) - IFEQ(d1,FALSE,0,2 to_power m)
    = Absval(z1) - 0 by A8,FUNCOP_1:def 8
      .= Absval(z1);
A10: Absval(z2) - IFEQ(d2,FALSE,0,2 to_power m)
    = Absval(z2) - 0 by A8,FUNCOP_1:def 8
      .= Absval(z2);
A11: IFEQ((d1 '&' d2 '&' 'not' add_ovfl(z1,z2)),f,0,2 to_power(m+1))
    = 0 by A8,FUNCOP_1:def 8;
    thus thesis
    proof
      per cases by XBOOLEAN:def 3;
      suppose
A12:    add_ovfl(z1,z2) = f;
        thus thesis by A3,A4,A5,A7,A8,A9,A12,Th12;
      end;
      suppose
A13:    add_ovfl(z1,z2) = t;
A14:    IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m)
        = 2 to_power m by A13,FUNCOP_1:def 8;
A15:    Intval(z1^<*d1*>+z2^<*d2*>)
        + IFEQ(Int_add_ovfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1))
        - IFEQ(Int_add_udfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1))
        = (Absval(z1) + Absval(z2))
        - (2*2 to_power m) + 2 to_power(m+1) by A3,A4,A5,A8,A11,A13,A14,
        FUNCOP_1:def 8
          .= (Absval(z1) + Absval(z2))
        - (2 to_power 1*2 to_power m) + 2 to_power(m+1) by POWER:30
          .= (Absval(z1) + Absval(z2))
        - 2 to_power (m+1) + 2 to_power(m+1) by POWER:32
          .= Absval(z1) + Absval(z2);
        thus thesis by A7,A9,A10,A15,Th12;
      end;
    end;
  end;
  suppose
A16: d1 = t & d2 = f;
A17: Absval(z2) - IFEQ(d2,FALSE,0,2 to_power m)
    = Absval(z2) - 0 by A16,FUNCOP_1:def 8
      .= Absval(z2);
    thus thesis
    proof
      per cases by XBOOLEAN:def 3;
      suppose
A18:    add_ovfl(z1,z2) = f;
A19:    IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m) = 0 by A18,
        FUNCOP_1:def 8;
        thus thesis by A3,A4,A5,A6,A7,A16,A17,A18,A19;
      end;
      suppose
A20:    add_ovfl(z1,z2) = t;
        thus thesis by A3,A4,A5,A6,A7,A16,A20;
      end;
    end;
  end;
  suppose
A21: d1 = f & d2 = t;
A22: Absval(z1) - IFEQ(d1,FALSE,0,2 to_power m)
    = Absval(z1) - 0 by A21,FUNCOP_1:def 8
      .= Absval(z1);
    thus thesis
    proof
      per cases by XBOOLEAN:def 3;
      suppose
A23:    add_ovfl(z1,z2) = f;
A24:    IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m) = 0 by A23,
        FUNCOP_1:def 8;
        thus thesis by A3,A4,A5,A6,A7,A21,A22,A23,A24;
      end;
      suppose
A25:    add_ovfl(z1,z2) = t;
        thus thesis by A3,A4,A5,A6,A7,A21,A25;
      end;
    end;
  end;
  suppose
A26: d1 = t & d2 = t;
A27: Absval(z2) - IFEQ(d2,FALSE,0,2 to_power m)
    = Absval(z2) - 2 to_power m by A26,FUNCOP_1:def 8;
A28: Intval(z1^<*d1*>) + Intval(z2^<*d2*>)
    = (Absval(z1) + Absval(z2)) - (2*2 to_power m) by A6,A7,A26,A27
      .= (Absval(z1) + Absval(z2)) - (2 to_power 1*2 to_power m) by POWER:30
      .= (Absval(z1) + Absval(z2)) - 2 to_power(m+1) by POWER:32;
A29: IFEQ(('not' d1 '&' 'not' d2 '&' add_ovfl(z1,z2)),f,0,2 to_power(m+1 ))
    = 0 by A26,FUNCOP_1:def 8;
    thus thesis
    proof
      per cases by XBOOLEAN:def 3;
      suppose
A30:    add_ovfl(z1,z2) = f;
A31:    IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m) = 0 by A30,
        FUNCOP_1:def 8;
        thus thesis by A3,A4,A5,A26,A28,A29,A30,A31,FUNCOP_1:def 8;
      end;
      suppose
A32:    add_ovfl(z1,z2) = t;
A33:    IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power m)
        = 2 to_power m by A32,FUNCOP_1:def 8;
A34:    Intval(z1^<*d1*>+z2^<*d2*>)
        + IFEQ(Int_add_ovfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1))
        - IFEQ(Int_add_udfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1))
        = (Absval(z1) + Absval(z2)) - (2*2 to_power m) by A3,A4,A5,A26,A32,A33
          .= (Absval(z1) + Absval(z2)) - (2 to_power 1*2 to_power m)
        by POWER:30
          .= (Absval(z1) + Absval(z2)) - 2 to_power(m+1) by POWER:32;
        thus thesis by A28,A34;
      end;
    end;
  end;
end;

theorem Th14:
  for z1,z2 being Tuple of m, BOOLEAN for d1,d2 being Element of BOOLEAN holds
  Intval(z1^<*d1*>+z2^<*d2*>) = Intval(z1^<*d1*>) + Intval(z2^<*d2*>)
  - IFEQ(Int_add_ovfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1))
  + IFEQ(Int_add_udfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1))
proof
  let z1,z2 be Tuple of m,BOOLEAN;
  let d1,d2;
  set A = Intval(z1^<*d1*>+z2^<*d2*>),
  B = IFEQ(Int_add_ovfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1)),
  C = IFEQ(Int_add_udfl(z1^<*d1*>,z2^<*d2*>),FALSE,0,2 to_power(m+1)),
  D = Intval(z1^<*d1*>) + Intval(z2^<*d2*>);
A1: A + B - C = D by Th13;
  thus thesis by A1;
end;

theorem Th15:
  for m for x being Tuple of m, BOOLEAN holds
  Absval('not' x) = - Absval(x) + 2 to_power m - 1
proof
  defpred P[Nat] means for x being Tuple of $1, BOOLEAN holds
  Absval('not' x) = - Absval(x) + 2 to_power $1 - 1;
A1: P[1]
  proof
    let x be Tuple of 1, BOOLEAN;
    per cases by BINARITH:40;
    suppose
A2:   x = <*FALSE*>;
A3:   x/.1 = FALSE by A2,FINSEQ_4:25;
      consider k being Element of BOOLEAN such that
A4:   'not' x = <* k *> by FINSEQ_2:117;
A5:   ('not' x)/.1 = k by A4,FINSEQ_4:25;
A6:   1 in Seg 1 by FINSEQ_1:5;
A7:   ('not' x)/.1 = 'not' FALSE by A3,A6,BINARITH:def 4
        .= TRUE;
A8:   - Absval(x) + 2 to_power 1 - 1
      = - 0 + 2 to_power 1 - 1 by A2,BINARITH:41
        .= 0 + 2 - 1 by POWER:30
        .= 1;
      thus thesis by A4,A5,A7,A8,BINARITH:42;
    end;
    suppose
A9:   x = <*TRUE*>;
A10:  x/.1 = TRUE by A9,FINSEQ_4:25;
      consider k being Element of BOOLEAN such that
A11:  'not' x = <* k *> by FINSEQ_2:117;
A12:  ('not' x)/.1 = k by A11,FINSEQ_4:25;
A13:  1 in Seg 1 by FINSEQ_1:5;
A14:  ('not' x)/.1 = 'not' TRUE by A10,A13,BINARITH:def 4
        .= FALSE;
A15:  - Absval(x) + 2 to_power 1 - 1
      = - 1 + 2 to_power 1 - 1 by A9,BINARITH:42
        .= - 1 + 2 - 1 by POWER:30
        .= 0;
      thus thesis by A11,A12,A14,A15,BINARITH:41;
    end;
  end;
A16: now
    let m;
    assume
A17: P[m];
A18: now
      let x be Tuple of m+1, BOOLEAN;
      consider t being (Element of m-tuples_on BOOLEAN),
      d being Element of BOOLEAN such that
A19:  x = t^<*d*> by FINSEQ_2:137;
A20:  Absval('not' x) = Absval('not' t^<*'not' d*>) by A19,Th11
        .= Absval('not' t) + IFEQ('not' d,FALSE,0,2 to_power m) by BINARITH:46
        .= - Absval(t) + 2 to_power m - 1
      + IFEQ('not' d,FALSE,0,2 to_power m) by A17;
A21:  - Absval(x) + 2 to_power(m+1) - 1
      = - (Absval(t) + IFEQ(d,FALSE,0,2 to_power m))
      + 2 to_power(m+1) - 1 by A19,BINARITH:46;
      thus Absval('not' x) = - Absval(x) + 2 to_power (m+1) - 1
      proof
        per cases by XBOOLEAN:def 3;
        suppose
A22:      d = FALSE;
          A23:      Absval
('not' x) = - Absval(t) + 2 to_power m - 1 + 2 to_power m
          by A20,A22,FUNCOP_1:def 8
            .= - Absval(t) + 2*2 to_power m - 1
            .= - Absval(t) + 2 to_power 1*2 to_power m - 1 by POWER:30
            .= - Absval(t) + 2 to_power(m+1) - 1 by POWER:32;
A24:      - Absval(x) + 2 to_power(m+1) - 1
          = -(Absval(t) + 0) + 2 to_power(m+1) - 1 by A21,A22,FUNCOP_1:def 8
            .= - Absval(t) + 2 to_power(m+1) - 1;
          thus thesis by A23,A24;
        end;
        suppose
A25:      d = TRUE;
A26:      Absval('not' x)
          = - Absval(t) + 2 to_power m - 1 + 0 by A20,A25,FUNCOP_1:def 8
            .= - Absval(t) + 2 to_power m - 1;
A27:      - Absval(x) + 2 to_power(m+1) - 1
          = -(Absval(t) + 2 to_power m) + 2 to_power(m+1) - 1
          by A21,A25,FUNCOP_1:def 8
            .= - Absval(t) - 2 to_power m + 2 to_power 1*2 to_power m - 1
          by POWER:32
            .= - Absval(t) - 2 to_power m + 2*2 to_power m - 1
          by POWER:30
            .= - Absval(t) + 2 to_power m - 1;
          thus thesis by A26,A27;
        end;
      end;
    end;
    thus P[m+1] by A18;
  end;
  thus for m holds P[m] from NAT_1:sch 10(A1,A16);
end;

theorem Th16:
  for z being Tuple of m, BOOLEAN for d being Element of BOOLEAN holds
  Neg2(z^<*d*>) = Neg2(z)^<*'not' d 'xor' add_ovfl('not' z,Bin1(m))*>
proof
  let z be Tuple of m, BOOLEAN;
  let d;
  thus Neg2(z^<*d*>) = 'not' z^<*'not' d*> + Bin1(m+1) by Th11
    .= 'not' z^<*'not' d*> + Bin1(m)^<*FALSE*> by Th9
    .= ('not' z + Bin1(m))^<*'not' d 'xor' FALSE 'xor' add_ovfl('not'
  z,Bin1(m))*> by BINARITH:45
    .= Neg2(z)^<*'not' d 'xor' add_ovfl('not' z,Bin1(m))*>;
end;

theorem Th17:
  for z being Tuple of m, BOOLEAN for d being Element of BOOLEAN holds
  Intval(Neg2(z^<*d*>))
  + IFEQ(Int_add_ovfl('not' (z^<*d*>),Bin1(m+1)),FALSE,0,2 to_power(m+1))
  = - Intval(z^<*d*>)
proof
  let z be Tuple of m, BOOLEAN;
  let d;
  set OV = IFEQ(Int_add_ovfl('not' z^<*'not' d*>,Bin1(m)^<*FALSE*>),FALSE,0,
  2 to_power(m+1)),
  UD = IFEQ(Int_add_udfl('not' z^<*'not' d*>,Bin1(m)^<*FALSE*>),FALSE,0,
  2 to_power(m+1));
A1: Int_add_udfl('not' z^<*'not' d*>,Bin1(m)^<*FALSE*>)
  = (('not' z^<*'not' d*>)/.(m+1)) '&' FALSE '&' 'not' ((carry('not'
  z^<*'not' d*>,Bin1(m)^<*FALSE*>))/.(m+1)) by BINARITH:3
    .= FALSE;
A2: Intval(Neg2(z^<*d*>))
  + IFEQ(Int_add_ovfl('not' (z^<*d*>),Bin1(m+1)),FALSE,0, 2 to_power(m+1))
  = Intval('not' z^<*'not' d*> + Bin1(m+1))
  + IFEQ(Int_add_ovfl('not' (z^<*d*>),Bin1(m+1)),FALSE,0,
  2 to_power(m+1)) by Th11
    .= Intval('not' z^<*'not' d*> + Bin1(m+1))
  + IFEQ(Int_add_ovfl('not' z^<*'not' d*>,Bin1(m+1)),FALSE,0,
  2 to_power(m+1)) by Th11
    .= Intval('not' z^<*'not' d*> + Bin1(m)^<*FALSE*>)
  + IFEQ(Int_add_ovfl('not' z^<*'not' d*>,Bin1(m+1)),FALSE,0,
  2 to_power(m+1)) by Th9
    .= Intval('not' z^<*'not' d*> + Bin1(m)^<*FALSE*>) + OV by Th9
    .= Intval('not' z^<*'not'
  d*>) + Intval(Bin1(m)^<*FALSE*>) - OV + UD + OV by Th14
    .= (Intval('not' z^<*'not' d*>) + 1) - OV + UD + OV by Th10
    .= (Intval('not' z^<*'not' d*>) + 1 + UD) - (OV - OV)
    .= Intval('not' z^<*'not' d*>) + 1 + 0 by A1,FUNCOP_1:def 8
    .= Absval('not' z) - IFEQ('not' d,FALSE,0,2 to_power m) + 1 by Th12
    .= (- Absval(z) + 2 to_power m) - 1
  - IFEQ('not' d,FALSE,0,2 to_power m) + 1 by Th15
    .= - Absval(z) + 2 to_power m - IFEQ('not' d,FALSE,0,2 to_power m);
A3: - Intval(z^<*d*>) = - (Absval(z) - IFEQ(d,FALSE,0,2 to_power m)) by Th12
    .= - Absval(z) + IFEQ(d,FALSE,0,2 to_power m);
  per cases by XBOOLEAN:def 3;
  suppose
A4: d = FALSE;
A5: Intval(Neg2(z^<*d*>))
    + IFEQ(Int_add_ovfl('not' (z^<*d*>),Bin1(m+1)),FALSE,0, 2 to_power(m+1))
    = - Absval(z) + 2 to_power m - 2 to_power m by A2,A4,FUNCOP_1:def 8
      .= - Absval(z) + 0;
    thus thesis by A3,A4,A5,FUNCOP_1:def 8;
  end;
  suppose
A6: d = TRUE;
A7: Intval(Neg2(z^<*d*>))
    + IFEQ(Int_add_ovfl('not' (z^<*d*>),Bin1(m+1)),FALSE,0, 2 to_power(m+1))
    = (- Absval(z) + 2 to_power m) - 0 by A2,A6,FUNCOP_1:def 8
      .= - Absval(z) + 2 to_power m;
    thus thesis by A3,A6,A7,FUNCOP_1:def 8;
  end;
end;

theorem
  for m for z being Tuple of m, BOOLEAN for d being Element of BOOLEAN holds
  Neg2(Neg2(z^<*d*>)) = z^<*d*>
proof
  defpred P[non empty Nat] means for z being Tuple of $1, BOOLEAN
  for d being Element of BOOLEAN holds Neg2(Neg2(z^<*d*>)) = z^<*d*>;
A1: P[1]
  proof
    let z be Tuple of 1, BOOLEAN;
    let d be Element of BOOLEAN;
    set NZD = 'not' d 'xor' 'not' (z/.1);
    set DPI = d '&' (z/.1), NZ1 = ('not' z)/.1;
    set B1 = (Bin1(1))/.1;
A2: 1 in Seg 1 by FINSEQ_1:5;
A3: 'not' d 'xor' FALSE 'xor' add_ovfl('not' z,Bin1(1))
    = 'not' d 'xor' ((NZ1 '&' B1) 'or'
    (NZ1 '&' ((carry('not' z,Bin1(1)))/.1)) 'or'
    (B1 '&' ((carry('not' z,Bin1(1)))/.1))) by BINARITH:def 9
      .= 'not' d 'xor' ((NZ1 '&' B1) 'or' (NZ1 '&' FALSE) 'or'
    (B1 '&' ((carry('not' z,Bin1(1)))/.1))) by BINARITH:def 5
      .= 'not' d 'xor' ((NZ1 '&' B1) 'or'
    FALSE 'or' (B1 '&' FALSE)) by BINARITH:def 5
      .= 'not' d 'xor' (TRUE '&' NZ1) by A2,Th7
      .= 'not' d 'xor' 'not' (z/.1) by A2,BINARITH:def 4;
A4: 'not' NZD 'xor' FALSE 'xor' add_ovfl('not' ('not' z + Bin1(1)),Bin1(1))
    = 'not' NZD 'xor' (((('not' ('not' z + Bin1(1)))/.1) '&' B1) 'or'
    ((('not' ('not' z + Bin1(1)))/.1) '&'
    ((carry('not' ('not' z + Bin1(1)),Bin1(1)))/.1)) 'or'
    (B1 '&' ((carry('not' ('not' z + Bin1(1)),Bin1(1)))/.1))) by BINARITH:def 9
      .= 'not' NZD 'xor'
    (((('not' ('not' z + Bin1(1)))/.1) '&' ((Bin1(1))/.1)) 'or'
    ((('not' ('not' z + Bin1(1)))/.1) '&' FALSE) 'or'
    (((Bin1(1))/.1) '&' ((carry('not' ('not' z + Bin1(1)),Bin1(1)))/.1)))
    by BINARITH:def 5
      .= 'not' NZD 'xor'
    (((('not' ('not' z + Bin1(1)))/.1) '&' ((Bin1(1))/.1)) 'or'
    FALSE 'or' (B1 '&' FALSE)) by BINARITH:def 5
      .=
    'not' NZD 'xor' (TRUE '&' (('not' ('not' z + Bin1(1)))/.1)) by A2,Th7
      .= 'not' NZD 'xor' 'not' ((('not' z + Bin1(1)))/.1) by A2,BINARITH:def 4
      .= 'not' NZD 'xor' 'not' ((('not' z)/.1) 'xor' ((Bin1(1))/.1)
    'xor' ((carry('not' z,Bin1(1)))/.1)) by A2,BINARITH:def 8
      .= 'not' NZD 'xor' 'not' ((('not' z)/.1) 'xor' ((Bin1(1))/.1)
    'xor' FALSE) by BINARITH:def 5
      .= 'not' NZD 'xor' 'not' (NZ1 'xor' TRUE) by A2,Th7
      .= 'not' NZD 'xor' 'not' (z/.1) by A2,BINARITH:def 4;
A5: Neg2(Neg2(z^<*d*>)) =
    'not' ('not' z^<*'not' d*> + Bin1(1 + 1)) + Bin1(1 + 1) by Th11
      .= 'not' ('not' z^<*'not' d*> + Bin1(1)^<*FALSE*>) + Bin1(1 + 1) by Th9
      .= 'not' (('not' z + Bin1(1))
    ^<*'not' d 'xor' FALSE 'xor' add_ovfl('not' z,Bin1(1))*>)
    + Bin1(1 + 1) by BINARITH:45
      .= 'not' ('not' z + Bin1(1))^<*'not' NZD*> + Bin1(1 + 1) by A3,Th11
      .= 'not' ('not' z + Bin1(1))^<*'not' NZD*> + Bin1(1)^<*FALSE*> by Th9
      .= ('not' ('not' z + Bin1(1))+ Bin1(1)) ^<*'not' NZD 'xor' 'not' (z/.1)*>
    by A4,BINARITH:45;
A6: (Neg2(Neg2(z^<*d*>)))/.1
    = ('not' ('not' z + Bin1(1))+ Bin1(1))/.1 by A2,A5,BINARITH:2
      .= (('not' ('not' z + Bin1(1)))/.1) 'xor' ((Bin1(1))/.1) 'xor'
    ((carry('not' ('not' z + Bin1(1)),Bin1(1)))/.1) by A2,BINARITH:def 8
      .= (('not' ('not' z + Bin1(1)))/.1) 'xor' ((Bin1(1))/.1) 'xor' FALSE
    by BINARITH:def 5
      .= (('not' ('not' z + Bin1(1)))/.1) 'xor' TRUE by A2,Th7
      .= 'not' 'not' ((('not' z + Bin1(1)))/.1) by A2,BINARITH:def 4
      .= (('not' z)/.1) 'xor' ((Bin1(1))/.1) 'xor' ((carry('not'
    z,Bin1(1)))/.1) by A2,BINARITH:def 8
      .= NZ1 'xor' ((Bin1(1))/.1) 'xor' FALSE by BINARITH:def 5
      .= NZ1 'xor' TRUE by A2,Th7
      .= 'not' 'not' (z/.1) by A2,BINARITH:def 4
      .= z/.1;
    reconsider p = d, q = z/.1 as boolean set;
A7: (Neg2(Neg2(z^<*d*>)))/.2 =
    ('not' d 'or' 'not' 'not' (z/.1)) '&' ('not' 'not' d
    'or' 'not' (z/.1)) 'xor' 'not' (z/.1) by A5,BINARITH:3
      .= ('not' p 'or' q) '&' p 'or' ('not' p 'or' q) '&'
    'not' q 'xor' 'not' (z/.1) by XBOOLEAN:8
      .= (p '&' 'not' p) 'or' p '&' q 'or' ('not' q '&' ('not' p 'or' q))
    'xor' 'not' (z/.1) by XBOOLEAN:8
      .= (d '&' 'not' d) 'or' (d '&' (z/.1)) 'or'
    (('not' (z/.1) '&' 'not' d) 'or' ('not' (z/.1) '&'
    (z/.1))) 'xor' 'not' (z/.1) by XBOOLEAN:8
      .= FALSE 'or' (d '&' (z/.1)) 'or'
    (('not' (z/.1) '&' 'not' d) 'or' ('not' (z/.1) '&'
    (z/.1))) 'xor' 'not' (z/.1) by XBOOLEAN:138
      .= DPI 'or' (('not' (z/.1) '&' 'not' d) 'or' FALSE)
    'xor' 'not' (z/.1) by XBOOLEAN:138
      .= (('not' d 'or' 'not' (z/.1)) '&' ('not' (z/.1) '&' ((z/.1) 'or' d)))
    'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&' 'not' 'not' (z/.1))
      .= (('not' d 'or' 'not' (z/.1)) '&' (('not' (z/.1) '&' (z/.1)) 'or'
    ('not' (z/.1) '&' d))) 'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&'
    'not' 'not' (z/.1)) by XBOOLEAN:8
      .= (('not' d 'or' 'not' (z/.1)) '&' (FALSE 'or' ('not'
    (z/.1) '&' d))) 'or' (((d '&' (z/.1)) 'or' ('not' (z/.1) '&' 'not' d)) '&'
    'not' 'not' (z/.1)) by XBOOLEAN:138
      .= ((('not' (z/.1) '&' d) '&' 'not' d) 'or' (('not'
    (z/.1) '&' d) '&' 'not' (z/.1)))
    'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&'
    'not' 'not' (z/.1)) by XBOOLEAN:8
      .= (('not' (z/.1) '&' (d '&' 'not' d)) 'or' (('not'
    (z/.1) '&' d) '&' 'not' (z/.1)))
    'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&' 'not' 'not' (z/.1))
      .= (('not' (z/.1) '&' FALSE) 'or' (('not'
    (z/.1) '&' d) '&' 'not' (z/.1)))
    'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&'
    'not' 'not' (z/.1)) by XBOOLEAN:138
      .= (d '&' ('not' (z/.1) '&' 'not' (z/.1)))
    'or' ((DPI 'or' ('not' (z/.1) '&' 'not' d)) '&' 'not' 'not' (z/.1))
      .= (d '&' 'not' (z/.1)) 'or' (((z/.1) '&' ((z/.1) '&' d)) 'or'
    ((z/.1) '&' ('not' (z/.1) '&' 'not' d))) by XBOOLEAN:8
      .= (d '&' 'not' (z/.1)) 'or' (((z/.1) '&' (z/.1) '&' d) 'or'
    ((z/.1) '&' ('not' (z/.1) '&' 'not' d)))
      .= (d '&' 'not' (z/.1))
    'or' (((z/.1) '&' d) 'or' ((z/.1) '&' 'not' (z/.1) '&' 'not' d))
      .= (d '&' 'not' (z/.1)) 'or' (((z/.1) '&' d) 'or' (FALSE '&' 'not' d))
    by XBOOLEAN:138
      .= d '&' ('not' (z/.1) 'or' (z/.1)) by XBOOLEAN:8
      .= TRUE '&' d by XBOOLEAN:102
      .= d;
    consider k1,k2 being Element of BOOLEAN such that
A8: Neg2(Neg2(z^<*d*>)) = <* k1,k2 *> by FINSEQ_2:120;
    A9: (Neg2(Neg2(z^<*d*>)))/.1 = k1 & (Neg2(Neg2(z^<*d*>)))/.2 = k2 by A8,
    FINSEQ_4:26;
    consider k being Element of BOOLEAN such that
A10: z = <*k*> by FINSEQ_2:117;
A11: Neg2(Neg2(z^<*d*>)) = <* k,d *> by A6,A7,A8,A9,A10,FINSEQ_4:25;
    thus thesis by A10,A11,FINSEQ_1:def 9;
  end;
A12: now
    let m;
    assume
A13: P[m];
A14: now
      let z be Tuple of m+1, BOOLEAN;
      let d be Element of BOOLEAN;
      consider t being (Element of m-tuples_on BOOLEAN),
      k being Element of BOOLEAN such that
A15:  z = t^<*k*> by FINSEQ_2:137;
      set A = add_ovfl('not' t,Bin1(m)), B = add_ovfl('not' Neg2(t),Bin1(m));
A16:  Neg2(Neg2(t^<*k*>))
      = Neg2(Neg2(t)^<*'not' k 'xor' add_ovfl('not' t,Bin1(m))*>) by Th16
        .= Neg2(Neg2(t))^<*'not' ('not' k 'xor' add_ovfl('not'
      t,Bin1(m))) 'xor' add_ovfl('not' Neg2(t),Bin1(m))*> by Th16;
A17:  (Neg2(Neg2(t^<*k*>)))/.(m+1)
      = 'not' ('not' k 'xor' add_ovfl('not' t,Bin1(m))) 'xor'
      add_ovfl('not' Neg2(t),Bin1(m)) by A16,BINARITH:3;
A18:  (t^<*k*>)/.(m+1) = k by BINARITH:3;
      reconsider p = k, q = A as boolean set;
A19:  'not' ('not' k 'xor' A) 'xor' B
      = (p '&' ('not' p 'or' 'not' q) 'or' ('not' p 'or' 'not'
      q) '&' q) 'xor' B by XBOOLEAN:8
        .= (k '&' 'not' A 'or' A '&' ('not' k 'or' 'not'
      A)) 'xor' B by XBOOLEAN:11
        .= (A 'xor' k) 'xor' B by XBOOLEAN:11
        .= k 'xor' (A 'xor' B) by XBOOLEAN:73;
A20:  k 'xor' (A 'xor' B) = k 'xor' FALSE by A13,A17,A18,A19;
A21:  k 'xor' (k 'xor' (A 'xor' B))
      = (k 'xor' k) 'xor' (A 'xor' B) by XBOOLEAN:73
        .= FALSE 'xor' (A 'xor' B) by XBOOLEAN:138
        .= A 'xor' B;
A22:  k 'xor' (k 'xor' FALSE) = FALSE by XBOOLEAN:138;
A23:  A 'xor' (A 'xor' B) = (A 'xor' A) 'xor' B by XBOOLEAN:73
        .= FALSE 'xor' B by XBOOLEAN:138
        .= B;
A24:  m + 1 in Seg(m+1) by FINSEQ_1:5;
A25:  add_ovfl('not' z,Bin1(m+1))
      = add_ovfl('not' t^<*'not' k*>,Bin1(m+1)) by A15,Th11
        .= add_ovfl('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>) by Th9
        .= ((('not' t^<*'not' k*>)/.(m+1)) '&'
      ((Bin1(m)^<*FALSE*>)/.(m+1))) 'or' ((('not' t^<*'not' k*>)/.(m+1)) '&'
      ((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) 'or'
      (((Bin1(m)^<*FALSE*>)/.(m+1)) '&'
((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) by BINARITH:def 9
        .= ((('not' t^<*'not' k*>)/.(m+1)) '&' FALSE) 'or'
      ((('not' t^<*'not' k*>)/.(m+1)) '&'
      ((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) 'or'
      (((Bin1(m)^<*FALSE*>)/.(m+1)) '&'
      ((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) by BINARITH:3
.= FALSE 'or' ((('not' t^<*'not' k*>)/.(m+1)) '&' ((carry('not' t^<*'not'
      k*>,Bin1(m)^<*FALSE*>))/.(m+1))) 'or' (FALSE '&' ((carry('not' t^<*'not'
      k*>,Bin1(m)^<*FALSE*>))/.(m+1))) by BINARITH:3
        .= 'not' k '&'
      ((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1)) by BINARITH:3
        .= 'not' k '&' A by BINARITH:44;
A26:  add_ovfl('not' (Neg2(z)),Bin1(m+1))
      = add_ovfl('not' (Neg2(z)),Bin1(m)^<*FALSE*>) by Th9
        .= ((('not' (Neg2(z)))/.(m+1)) '&' ((Bin1(m)^<*FALSE*>)/.(m+1))) 'or'
      ((('not' (Neg2(z)))/.(m+1)) '&'
      ((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1))) 'or'
      (((Bin1(m)^<*FALSE*>)/.(m+1)) '&'
      ((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1))) by BINARITH:def 9
        .= ((('not' (Neg2(z)))/.(m+1)) '&' FALSE) 'or'
      ((('not' (Neg2(z)))/.(m+1)) '&'
      ((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1))) 'or'
      (((Bin1(m)^<*FALSE*>)/.(m+1)) '&'
      ((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1))) by BINARITH:3
        .= FALSE 'or' ((('not' (Neg2(z)))/.(m+1)) '&'
      ((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1))) 'or'
      (FALSE '&' ((carry('not' (Neg2(z)),Bin1(m)^<*FALSE*>))/.(m+1)))
      by BINARITH:3
        .= (('not' ('not' t^<*'not' k*> + Bin1(m+1)))/.(m+1)) '&'
      ((carry('not' ('not' (t^<*k*>) + Bin1(m+1)),Bin1(m)^<*FALSE*>))/.(m+1))
      by A15,Th11
        .= (('not' ('not' t^<*'not' k*> + Bin1(m+1)))/.(m+1)) '&'
((carry('not' ('not' t^<*'not' k*> + Bin1(m+1)),Bin1(m)^<*FALSE*>))/.(m+1))
      by Th11
        .= (('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>))/.(m+1)) '&'
      ((carry('not' ('not' t^<*'not' k*> + Bin1(m+1)),Bin1(m)^<*FALSE*>))/.
      (m+1)) by Th9
        .= (('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>))/.(m+1)) '&'
      ((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
      Bin1(m)^<*FALSE*>))/.(m+1)) by Th9
        .= 'not' ((('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>))/.(m+1)) '&'
      ((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
      Bin1(m)^<*FALSE*>))/.(m+1)) by A24,BINARITH:def 4
.= 'not' ((('not' t^<*'not' k*>)/.(m+1)) 'xor' ((Bin1(m)^<*FALSE*>)/.(m+1))
      'xor' ((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) '&'
      ((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
      Bin1(m)^<*FALSE*>))/.(m+1)) by A24,BINARITH:def 8
        .= 'not' ('not' k 'xor' ((Bin1(m)^<*FALSE*>)/.(m+1)) 'xor'
      ((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) '&'
      ((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
      Bin1(m)^<*FALSE*>))/.(m+1)) by BINARITH:3
        .= 'not' ('not' k 'xor' FALSE 'xor'
      ((carry('not' t^<*'not' k*>,Bin1(m)^<*FALSE*>))/.(m+1))) '&'
      ((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
      Bin1(m)^<*FALSE*>))/.(m+1)) by BINARITH:3
        .= 'not' ('not' k 'xor' FALSE 'xor' add_ovfl('not' t,Bin1(m))) '&'
      ((carry('not' ('not' t^<*'not' k*> + Bin1(m)^<*FALSE*>),
      Bin1(m)^<*FALSE*>))/.(m+1)) by BINARITH:44
        .= 'not' ('not' k 'xor' add_ovfl('not' t,Bin1(m))) '&'
      ((carry('not' (('not' t + Bin1(m))
      ^<*'not' k 'xor' FALSE 'xor' add_ovfl('not' t,Bin1(m))*>),
      Bin1(m)^<*FALSE*>))/.(m+1)) by BINARITH:45
        .= 'not' ('not' k 'xor' add_ovfl('not' t,Bin1(m))) '&'
      ((carry(('not' ('not' t + Bin1(m))
      ^<*'not' ('not' k 'xor' FALSE 'xor' add_ovfl('not' t,Bin1(m)))*>),
      Bin1(m)^<*FALSE*>))/.(m+1)) by Th11
        .= (('not' k 'or' 'not' A) '&' (k 'or' 'not' 'not'
      A)) '&' A by A20,A21,A22,A23,BINARITH:44
        .= ('not' k 'or' 'not' A) '&' (A '&' (k 'or' A))
        .= A '&' ('not' A 'or' 'not' k) by XBOOLEAN:6
        .= A '&' 'not' k by XBOOLEAN:11;
      set C = 'not' k '&' A;
      reconsider p = d, q = C as boolean set;
A27:  'not' ('not' d 'xor' C) 'xor' C
      = ((p '&' ('not' p 'or' 'not' q)) 'or' (('not' p 'or' 'not'
      q) '&' q)) 'xor' C by XBOOLEAN:8
        .= ((d '&' 'not' C) 'or' (C '&' ('not' d 'or' 'not'
      C))) 'xor' C by XBOOLEAN:11
        .= C 'xor' d 'xor' C by XBOOLEAN:11
        .= d 'xor' (C 'xor' C) by XBOOLEAN:73
        .= d 'xor' FALSE by XBOOLEAN:138
        .= d;
      thus Neg2(Neg2(z^<*d*>))
      = Neg2(Neg2(z)^<*'not' d 'xor' add_ovfl('not' z,Bin1(m+1))*>) by Th16
        .= Neg2(Neg2(z))^<*'not' ('not' d 'xor' add_ovfl('not'
      z,Bin1(m+1))) 'xor' add_ovfl('not' Neg2(z),Bin1(m+1))*> by Th16
        .= z^<*d*> by A13,A15,A25,A26,A27;
    end;
    thus P[m+1] by A14;
  end;
  thus for m holds P[m] from NAT_1:sch 10(A1,A12);
end;

definition
  let n be non empty Nat, x, y be Tuple of n, BOOLEAN;
  func x - y -> Tuple of n, BOOLEAN means
  :Def6:
  for i st i in Seg n holds
  it/.i = (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i);
  existence
  proof
    deffunc F(Nat) = (x/.$1) 'xor' ((Neg2(y))/.$1)
    'xor' ((carry(x,Neg2(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;
    z is Element of n-tuples_on BOOLEAN by A1,FINSEQ_2:110;
    then reconsider z as Tuple of n, BOOLEAN;
    take z;
    let i;
    assume
A4: i in Seg n;
A5: i in dom z by A1,A4,FINSEQ_1:def 3;
    thus z/.i = z.i by A5,PARTFUN1:def 8
      .= (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i) by A2,A3,A4;
  end;
  uniqueness
  proof
    let z1, z2 be Tuple of n, BOOLEAN such that
A6: for i st i in Seg n holds
    z1/.i = (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i) and
A7: for i st i in Seg n holds
    z2/.i = (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i);
A8: len z1 = n by FINSEQ_1:def 18;
A9: len z2 = n by FINSEQ_1:def 18;
A10: dom z1 = Seg n by A8,FINSEQ_1:def 3;
A11: now
      let j be Nat;
      assume
A12:  j in dom z1;
A13:  Seg n = Seg len z2 by FINSEQ_1:def 18;
A14:  j in dom z2 by A10,A12,A13,FINSEQ_1:def 3;
      thus z1.j = z1/.j by A12,PARTFUN1:def 8
        .= (x/.j) 'xor' ((Neg2(y))/.j) 'xor' ((carry(x,Neg2(y)))/.j) by A6,A10
      ,A12
        .= z2/.j by A7,A10,A12
        .= z2.j by A14,PARTFUN1:def 8;
    end;
    thus thesis by A8,A9,A11,FINSEQ_2:10;
  end;
end;

theorem Th19:
  for x,y being Tuple of m, BOOLEAN holds x - y = x + Neg2(y)
proof
  let x,y be Tuple of m, BOOLEAN;
A1: for i st i in Seg m holds (x - y)/.i
  = (x/.i) 'xor' ((Neg2(y))/.i) 'xor' ((carry(x,Neg2(y)))/.i) by Def6;
  thus thesis by A1,BINARITH:def 8;
end;

theorem
  for z1,z2 being Tuple of m, BOOLEAN for d1,d2 being Element of BOOLEAN holds
  z1^<*d1*> - z2^<*d2*>
  = (z1 + Neg2(z2))^<*d1 'xor' 'not' d2 'xor' add_ovfl('not'
  z2,Bin1(m)) 'xor' add_ovfl(z1,Neg2(z2))*>
proof
  let z1,z2 be Tuple of m, BOOLEAN;
  let d1,d2;
  thus z1^<*d1*> - z2^<*d2*> = z1^<*d1*> + Neg2(z2^<*d2*>) by Th19
    .= z1^<*d1*> + Neg2(z2)^<*'not' d2 'xor' add_ovfl('not'
  z2,Bin1(m))*> by Th16
    .= (z1 + Neg2(z2))
  ^<*d1 'xor' ('not' d2 'xor' add_ovfl('not' z2,Bin1(m))) 'xor'
  add_ovfl(z1,Neg2(z2))*> by BINARITH:45
    .= (z1 + Neg2(z2))
  ^<*d1 'xor' 'not' d2 'xor' add_ovfl('not' z2,Bin1(m)) 'xor'
  add_ovfl(z1,Neg2(z2))*> by XBOOLEAN:73;
end;

theorem
  for z1,z2 being Tuple of m, BOOLEAN for d1,d2 being Element of BOOLEAN holds
  Intval(z1^<*d1*>-z2^<*d2*>)
  + IFEQ(Int_add_ovfl(z1^<*d1*>,Neg2(z2^<*d2*>)),FALSE,0,2 to_power(m+1))
  - IFEQ(Int_add_udfl(z1^<*d1*>,Neg2(z2^<*d2*>)),FALSE,0,2 to_power(m+1))
  + IFEQ(Int_add_ovfl('not' (z2^<*d2*>),Bin1(m+1)),FALSE,0,2 to_power(m+1))
  = Intval(z1^<*d1*>) - Intval(z2^<*d2*>)
proof
  let z1,z2 be Tuple of m, BOOLEAN;
  let d1,d2;
  set OV1 = IFEQ(Int_add_ovfl(z1^<*d1*>,Neg2(z2^<*d2*>)),FALSE,0,
  2 to_power(m+1)),
  UD1 = IFEQ(Int_add_udfl(z1^<*d1*>,Neg2(z2^<*d2*>)),FALSE,0,
  2 to_power(m+1)),
  OV2 = IFEQ(Int_add_ovfl('not' (z2^<*d2*>),Bin1(m+1)),FALSE,0,
  2 to_power(m+1)),
  NEG = Neg2(z2)^<*'not' d2 'xor' add_ovfl('not' z2,Bin1(m))*>;
  thus Intval(z1^<*d1*>-z2^<*d2*>) + OV1 - UD1 + OV2
  = Intval(z1^<*d1*>+Neg2(z2^<*d2*>)) + OV1 - UD1 + OV2 by Th19
    .= Intval(z1^<*d1*>+NEG) + OV1 - UD1 + OV2 by Th16
    .= Intval(z1^<*d1*>+NEG)
  + IFEQ(Int_add_ovfl(z1^<*d1*>,NEG),FALSE,0,2 to_power(m+1))
  - UD1 + OV2 by Th16
    .= Intval(z1^<*d1*>+NEG)
  + IFEQ(Int_add_ovfl(z1^<*d1*>,NEG),FALSE,0,2 to_power(m+1))
  - IFEQ(Int_add_udfl(z1^<*d1*>,NEG),FALSE,0,2 to_power(m+1)) + OV2 by Th16
    .= Intval(z1^<*d1*>) + Intval(NEG) + OV2 by Th13
    .= Intval(z1^<*d1*>) + (Intval(NEG) + OV2)
    .= Intval(z1^<*d1*>) + (Intval(Neg2(z2^<*d2*>)) + OV2) by Th16
    .= Intval(z1^<*d1*>) + (- Intval(z2^<*d2*>)) by Th17
    .= Intval(z1^<*d1*>) - Intval(z2^<*d2*>);
end;