:: Binary Arithmetics. Addition :: by Takaya Nishiyama and Yasuho Mizuhara :: :: Received October 8, 1993 :: Copyright (c) 1993 Association of Mizar Users environ vocabularies MONOID_0, FUNCT_1, RELAT_1, MIDSP_3, FINSEQ_1, MARGREL1, ZF_LANG, ORDINAL2, ARYTM_1, CQC_LANG, POWER, SETWISEO, BOOLE, FINSEQ_2, BINARITH, FINSEQ_4, ARYTM, RFINSEQ; notations XBOOLE_0, SUBSET_1, ORDINAL1, 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, RFINSEQ, SEQ_1, NAT_1, XXREAL_0; constructors BINOP_1, SETWISEO, XXREAL_0, NAT_1, INT_1, BINOP_2, MARGREL1, PARTFUN1, FINSOP_1, SERIES_1, RFINSEQ, SEQ_1; registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, XBOOLEAN, MARGREL1, FINSEQ_2, XBOOLE_0, REAL_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, REAL_2, XREAL_1, XXREAL_0, XBOOLEAN, RFINSEQ, FUNCOP_1, PARTFUN1, FINSEQ_3; schemes FINSEQ_1, FINSEQ_2, NAT_1; begin definition let i be Nat, D be non empty set; mode Tuple of i,D is Element of i-tuples_on D; end; canceled; theorem Th2: 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 FINSEQ_2:109; then i in dom z by A1,FINSEQ_1:def 3; hence thesis by FINSEQ_4:83; end; theorem Th3: 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:56; then 0+1 in Seg len <*d*>; then A1: 0+1 in dom <*d*> by FINSEQ_1:def 3; len(z) = n by FINSEQ_2:109; hence (z^<*d*>)/.(n+1) = <*d*>/.1 by A1,FINSEQ_4:84 .= d by FINSEQ_4:25; end; registration let x, y be boolean set; cluster x 'xor' y -> boolean; correctness; 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; 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; canceled 3; theorem x 'or' FALSE = x; canceled; theorem 'not' (x '&' y) = 'not' x 'or' 'not' y; theorem 'not' (x 'or' y) = 'not' x '&' 'not' y; canceled; theorem x '&' y = 'not' ('not' x 'or' 'not' y); theorem TRUE 'xor' x = 'not' x; theorem FALSE 'xor' x = x; canceled; theorem x '&' x = x; canceled 2; theorem x 'or' TRUE = TRUE; theorem (x 'or' y) 'or' z = x 'or' (y 'or' z); theorem x 'or' x = x; canceled 11; theorem TRUE 'xor' FALSE = TRUE; definition let i,j be natural number; canceled 2; func i -' j -> Element of NAT equals :Def3: i - j if i - j >= 0 otherwise 0; coherence by INT_1:16; correctness; end; canceled 5; theorem Th39: for i,j being natural number holds i + j -' j = i proof let i, j be natural number; i + j - j >= 0; hence i + j -' j = i by Def3; end; reserve i,j,k for Nat; reserve n for non empty 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,FINSEQ_2:110; 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 8 .= 'not' (x/.i) by A2,A4,A3; 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 & len z = n by FINSEQ_2:109; then X: dom y = Seg n by FINSEQ_1:def 3; now let j be Nat; assume A8: j in dom y; then A9: j in dom y & j in dom z by A7,FINSEQ_1:def 3,X; thus y.j = y/.j by PARTFUN1:def 8,A8 .= 'not' (x/.j) by A5,A8,X .= z/.j by A6,A8,X .= z.j by A9,PARTFUN1:def 8; end; hence y = z by A7,FINSEQ_2:10; 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 :Def5: 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 & a = z.b by FUNCT_1:def 5; A6: b in Seg n by A3,A5,FINSEQ_1:def 3; reconsider b as Element of NAT by A5; b>=1 by A6,FINSEQ_1:3; then reconsider c = b-1 as Element of NAT by INT_1:18; z.b = f.c by A4,A5; hence a in BOOLEAN by A5; end; then reconsider z as Tuple of n, BOOLEAN by A3,FINSEQ_2:110; take z; 0+1 <= n by NAT_1:13; then 1 in Seg n; then A7: 1 in dom z by A3,FINSEQ_1:def 3; hence z/.1 = z.1 by PARTFUN1:def 8 .= f.(1-1) by A4,A7 .= FALSE by A1; let i be Nat; assume A8: 1 <= i & i < n; then consider j be Nat such that A9: j+1 = i by NAT_1:6; A10: j+1 in Seg n by A8,A9; A11: i+1-1=i; A12:j+1 in dom z by A3,A10,FINSEQ_1:def 3; then A13: z/.(j+1) = z.(j+1) by PARTFUN1:def 8 .= f.(j+1-1) by A4,A12 .= f.j; 1 <= i+1 & i+1 <= n by A8,NAT_1:13; then A14: i + 1 in dom z by A3,FINSEQ_3:27; hence z/.(i+1) = z.(i+1) by PARTFUN1:def 8 .= f.(j+1) by A4,A9,A11,A14 .= (x/.i) '&' (y/.i) 'or' (x/.i) '&' (z/.i) 'or' (y/.i) '&' (z/.i) by A2,A9,A13; end; uniqueness proof let z1, z2 be Tuple of n, BOOLEAN such that A15: z1/.1 = FALSE and A16: 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 A17: z2/.1 = FALSE and A18: 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); A19: len z1 = n & len z2 = n by FINSEQ_2:109; then X: dom z1 = Seg n by FINSEQ_1:def 3; now let j be Nat such that A20: j in dom z1; defpred P[Nat] means $1 in Seg n implies z1/.$1 = z2/.$1; A21: P[0] by FINSEQ_1:3; A22: now let k such that A23: P[k]; thus P[k+1] proof assume A24: k+1 in Seg n; per cases; suppose k = 0; hence z1/.(k+1) = z2/.(k+1) by A15,A17; end; suppose k <> 0; then k > 0; then A25: k >= 0+1 by NAT_1:13; A26: k+1 <= n by A24,FINSEQ_1:3; k < k+1 by XREAL_1:31; then A27: k < n by A26,XXREAL_0:2; thus z1/.(k+1) = (x/.k) '&' (y/.k) 'or' (x/.k) '&' (z1/.k) 'or' (y/.k) '&' (z1/.k) by A16,A25,A27 .= z2/.(k+1) by A18,A23,A25,A27,FINSEQ_1:3; end; end; end; A28: for k holds P[k] from NAT_1:sch 2 (A21,A22); A29: dom z1 = Seg n & dom z2 = Seg n by A19,FINSEQ_1:def 3; thus z1.j = z1/.j by A20,PARTFUN1:def 8 .= z2/.j by A20,A28,X .= z2.j by A20,A29,PARTFUN1:def 8; end; hence z1 = z2 by A19,FINSEQ_2:10; end; end; definition let n be Nat, x be Tuple of n, BOOLEAN; func Binary(x) -> Tuple of n, NAT means :Def6: 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,FINSEQ_2:110; 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 8 .= IFEQ(x/.j,FALSE,0,2 to_power(j-'1)) by A2,A4,A3; 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 & len z2 = n by FINSEQ_2:109; then A8: dom z1 = Seg n & dom z2 = Seg n by FINSEQ_1:def 3; now let j be Nat; assume A9: j in dom z1; hence z1.j = z1/.j by PARTFUN1:def 8 .= IFEQ( x/.j,FALSE,0,2 to_power(j-'1)) by A5,A9,A8 .= z2/.j by A6,A9,A8 .= z2.j by A8,A9,PARTFUN1:def 8; end; hence z1 = z2 by A7,FINSEQ_2:10; 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 :Def8: 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,FINSEQ_2:110; 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 8 .= (x/.i) 'xor' (y/.i) 'xor' (carry(x,y)/.i) by A2,A4,A3; 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 & len z2 = n by FINSEQ_2:109; then A8: dom z1 = Seg n & dom z2 = Seg n by FINSEQ_1:def 3; now let j be Nat; assume A9: j in dom z1; hence z1.j = z1/.j by PARTFUN1:def 8 .= (x/.j) 'xor' (y/.j) 'xor' (carry(x,y)/.j) by A5,A9,A8 .= z2/.j by A6,A9,A8 .= z2.j by A8,A9,PARTFUN1:def 8; end; hence z1 = z2 by A7,FINSEQ_2:10; 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 :Def10: add_ovfl(z1,z2) = FALSE; end; theorem Th40: for z1 being Tuple of 1,BOOLEAN holds z1= <*FALSE*> or z1=<*TRUE*> proof let z1 be Tuple of 1,BOOLEAN; consider B being Element of BOOLEAN such that A1: z1=<*B*> by FINSEQ_2:117; per cases by XBOOLEAN:def 3; suppose z1/.1 = FALSE; hence thesis by A1,FINSEQ_4:25; end; suppose z1/.1 = TRUE; hence thesis by A1,FINSEQ_4:25; end; end; theorem Th41: for z1 being Tuple of 1,BOOLEAN holds z1=<*FALSE*> implies Absval(z1) = 0 proof let z1 be Tuple of 1,BOOLEAN; assume A1: z1=<*FALSE*>; consider k being Element of NAT such that A2: Binary( z1 ) = <* k *> by FINSEQ_2:117; A3: z1/.1 = FALSE by A1,FINSEQ_4:25; 1 in Seg 1; then (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1)) by Def6 .= 0 by A3,FUNCOP_1:def 8; hence Absval(z1) = addnat $$ <* 0 *> by A2,FINSEQ_4:25 .= 0 by FINSOP_1:12; end; theorem Th42: for z1 being Tuple of 1,BOOLEAN st z1=<*TRUE*> holds Absval(z1)=1 proof let z1 be Tuple of 1,BOOLEAN; assume A1: z1=<*TRUE*>; consider k being Element of NAT such that A2: Binary( z1 ) = <* k *> by FINSEQ_2:117; A3: z1/.1 <> FALSE by A1,FINSEQ_4:25; 1 in Seg 1; then A4: (Binary(z1))/.1 = IFEQ(z1/.1,FALSE,0,2 to_power(1-'1)) by Def6 .= 2 to_power(1-'1) by A3,FUNCOP_1:def 8; A5: 1 - 1 = 0; thus Absval(z1) = addnat $$ <* 2 to_power(1-'1) *> by A2,A4,FINSEQ_4:25 .= 2 to_power(1-'1) by FINSOP_1:12 .= 2 to_power(0) by A5,Def3 .= 1 by POWER:29; 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:127; end; definition let D be non empty set; let d be Element of D; redefine func <* d *> -> Tuple of 1,D; coherence by FINSEQ_2:118; end; theorem Th43: 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; A1: P[1] proof assume 1 in Seg n; thus carry(z1^<*d1*>,z2^<*d2*>)/.1 = FALSE by Def5 .= carry(z1,z2)/.1 by Def5; end; A2: for i being non empty Nat st P[i] holds P[i+1] proof let i be non empty Nat; assume A3: P[i]; A4: i+1 > i by XREAL_1:31; assume i+1 in Seg n; then i+1 >= 1 & i+1 <= n by FINSEQ_1:3; then A5: 1 <= i & i < n by A4,NAT_1:14,XXREAL_0:2; then A6: i in Seg n by FINSEQ_1:3; then A7: (z1^<*d1*>)/.i = z1/.i by Th2; A8: (z2^<*d2*>)/.i = z2/.i by A6,Th2; n <= n+1 by NAT_1:11; then 1 <= i & i < n+1 by A5,XXREAL_0:2; 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 A3,A7,A8,Def5,A5,FINSEQ_1:3 .= carry(z1,z2)/.(i+1) by A5,Def5; end; let i be Nat; assume A9: i in Seg n; then A10: i is non empty by FINSEQ_1:3; for i being non empty Nat holds P[i] from NAT_1:sch 10(A1,A2); hence thesis by A9,A10; end; theorem Th44: 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: n in Seg n by FINSEQ_1:5; then A2: carry(z1^<*d1*>,z2^<*d2*>)/.n = carry(z1,z2)/.n by Th43; A3: z1/.n = (z1^<*d1*>)/.n by A1,Th2; A4: z2/.n = (z2^<*d2*>)/.n by A1,Th2; 1 <= n & n < n+1 by NAT_1:14,XREAL_1:31; hence add_ovfl(z1,z2) = carry(z1^<*d1*>,z2^<*d2*>)/.(n+1) by A2,A3,A4,Def5; end; theorem Th45: 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 let i such that A1: i in Seg (n+1); A2: Seg (n+1) = Seg (n) \/ {. n+1 .} by FINSEQ_1:11; per cases by A1,A2,XBOOLE_0:def 2; suppose A3: i in Seg n; hence ((z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,z2)*>)/.i = (z1+z2)/.i by Th2 .= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A3,Def8 .= ((z1^<*d1*>)/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A3,Th2 .= ((z1^<*d1*>)/.i) 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1,z2)/.i) by A3,Th2 .= ((z1^<*d1*>)/.i) 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1^<*d1*>,z2^<*d2*>)/.i) by A3,Th43; 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 Th3 .= d1 'xor' d2 'xor' (carry(z1^<*d1*>,z2^<*d2*>)/.i) by A4,Th44 .= d1 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1^<*d1*>,z2^<*d2*>)/.i) by A4,Th3 .= ((z1^<*d1*>)/.i) 'xor' ((z2^<*d2*>)/.i) 'xor' (carry(z1^<*d1*>,z2^<*d2*>)/.i) by A4,Th3; end; end; hence z1^<*d1*> + z2^<*d2*> = (z1+z2)^<*d1 'xor' d2 'xor' add_ovfl(z1,z2)*> by Def8; end; theorem Th46: 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 let i such that A1: i in Seg (n+1); A2: Seg (n+1) = Seg (n) \/ {. n+1 .} by FINSEQ_1:11; per cases by A1,A2,XBOOLE_0:def 2; suppose A3: i in Seg n; hence (Binary(z)^<*IFEQ(d,FALSE,0,2 to_power(n))*>)/.i = (Binary(z))/.i by Th2 .= IFEQ(z/.i,FALSE,0,2 to_power(i-'1)) by A3,Def6 .= IFEQ((z^<*d*>)/.i,FALSE,0,2 to_power(i-'1)) by A3,Th2; 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 Th3 .= IFEQ((z^<*d*>)/.i,FALSE,0,2 to_power(n)) by A4,Th3 .= IFEQ((z^<*d*>)/.i,FALSE,0,2 to_power(i-'1)) by A4,Th39; end; end; hence Absval(z^<*d*>) = addnat $$ (Binary(z)^<*IFEQ(d,FALSE,0,2 to_power(n))*>) by Def6 .= addnat.(addnat$$Binary(z),IFEQ(d,FALSE,0,2 to_power(n))) by FINSOP_1:5 .= Absval(z)+IFEQ(d,FALSE,0,2 to_power n) by BINOP_2:def 23; end; theorem Th47: 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 set f = FALSE, t = TRUE; defpred P[ non empty 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); A1: P[1] proof let z1,z2 be Tuple of 1, BOOLEAN; A2: carry(z1,z2)/.1 = f by Def5; reconsider T= <*t*>,F= <*f*> as Tuple of 1,BOOLEAN; A3: Absval(T)=1 & Absval(F)=0 by Th41,Th42; per cases by Th40; suppose A4: z1=<*f*> & z2=<*f*>; A5: IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 proof add_ovfl(z1,z2) = f by A2,A4,FINSEQ_4:25; hence IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 by FUNCOP_1:def 8; end; now let i; assume A6: i in Seg 1; then A7: i=1 by FINSEQ_1:4,TARSKI:def 1; thus F/.i = (z1/.1) 'xor' f 'xor' f by A4,A6,FINSEQ_1:4 ,TARSKI:def 1 .= (z1/.1) 'xor' (z2/.1) 'xor' f by A4,FINSEQ_4:25 .= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A7, Def5; end; hence thesis by A3,A4,A5,Def8; end; suppose A8: z1=<*t*> & z2=<*f*>; A9: IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 proof add_ovfl(z1,z2) = f by A2,A8,FINSEQ_4:25; hence IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 by FUNCOP_1:def 8; end; now let i; assume A10: i in Seg 1; then A11: i=1 by FINSEQ_1:4,TARSKI:def 1; thus T/.i = (z1/.1) 'xor' f 'xor' f by A8,A10,FINSEQ_1:4 ,TARSKI:def 1 .= (z1/.1) 'xor' (z2/.1) 'xor' f by A8,FINSEQ_4:25 .= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A11,Def5; end; hence thesis by A3,A8,A9,Def8; end; suppose A12: z1=<*f*> & z2=<*t*>; A13: IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 proof add_ovfl(z1,z2) = f by A2,A12,FINSEQ_4:25; hence IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 0 by FUNCOP_1:def 8; end; now let i; assume i in Seg 1; then A14: i=1 by FINSEQ_1:4,TARSKI:def 1; hence T/.i = 'not' t 'xor' t 'xor' f by FINSEQ_4:25 .= (z1/.1) 'xor' t 'xor' f by A12,FINSEQ_4:25 .= (z1/.1) 'xor' (z2/.1) 'xor' f by A12,FINSEQ_4:25 .= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A14,Def5; end; hence thesis by A3,A12,A13,Def8; end; suppose A15: z1=<*t*> & z2=<*t*>; A16: IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power 1) = 2 proof add_ovfl(z1,z2) = t by A2,A15,FINSEQ_4:25; hence IFEQ(add_ovfl(z1,z2),FALSE,0,2 to_power (1)) = 2 to_power 1 by FUNCOP_1:def 8 .= 2 by POWER:30; end; now let i; assume i in Seg 1; then A17: i=1 by FINSEQ_1:4,TARSKI:def 1; hence F/.i = t 'xor' t 'xor' 'not' t by FINSEQ_4:25 .= (z1/.1) 'xor' t 'xor' f by A15,FINSEQ_4:25 .= (z1/.1) 'xor' (z2/.1) 'xor' f by A15,FINSEQ_4:25 .= (z1/.i) 'xor' (z2/.i) 'xor' (carry(z1,z2)/.i) by A17,Def5; end; then z1+z2=<*f*> by Def8; hence thesis by A3,A15,A16; end; end; A18: for n being non empty Nat st P[n] holds P[n+1] proof let n; assume A19: 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 A20: z1 = t1^<*d1*> by FINSEQ_2:137; consider t2 being (Element of n-tuples_on BOOLEAN), d2 being Element of BOOLEAN such that A21: z2 = t2^<*d2*> by FINSEQ_2:137; 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 & 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(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; A22: 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 A20,A21,Th3 .= 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 Th3 .= d1 '&' d2 'or' d1 '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) 'or' ((t2^<*d2*>)/.(n+1)) '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) by Th3 .= d1 '&' d2 'or' d1 '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) 'or' d2 '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) by Th3 .= d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' (carry(t1^<*d1*>,t2^<*d2*>)/.(n+1)) by Th44 .= d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,t2) by Th44; A23: C2 + C1 = C5 + C3 + C4 proof now per cases; suppose A24: d1=f; then A25: C3=0 by FUNCOP_1:def 8; now per cases; suppose A26: d2=f; then C4=0 by FUNCOP_1:def 8; hence C2 + C1 = C5 + C3 + C4 by A22,A24,A26,FUNCOP_1:def 8; end; suppose A27: d2 <> f; then A28: C4=2 to_power n by FUNCOP_1:def 8; now per cases; suppose A29: add_ovfl(t1,t2)=f; then C5=0 by FUNCOP_1:def 8; hence C2 + C1 = C5 + C3 + C4 by A22,A24,A29,FUNCOP_1:def 8; end; suppose A30: add_ovfl(t1,t2)<>f; then A31: C5=2 to_power(n) by FUNCOP_1:def 8; A32: d1 '&' d2 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,t2) = f 'or' f 'or' t '&' add_ovfl(t1,t2) by A24,A27,XBOOLEAN:def 3 .= t by A30,XBOOLEAN:def 3; d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' add_ovfl(t1,t2) by A24,A27,XBOOLEAN:def 3 .= f by A30,XBOOLEAN:def 3; then C2=0 & C1=2 to_power(n+1) by A22,A32,FUNCOP_1:def 8; hence C2 + C1 = 2 to_power n * 2 to_power 1 by POWER:32 .= 2 * 2 to_power n by POWER:30 .= C5 + C3 + C4 by A25,A28,A31; end; end; hence C2 + C1 = C5 + C3 +C4; end; end; hence C2 + C1 = C5 + C3 +C4; end; suppose A33: d1 <>f; then A34: C3=2 to_power n by FUNCOP_1:def 8; now per cases; suppose A35: d2=f; then A36: C4=0 by FUNCOP_1:def 8; now per cases; suppose add_ovfl(t1,t2)=f; hence C2 + C1 = C5 + C3 + C4 by A22,A35,A36,FUNCOP_1:def 8; end; suppose A37: add_ovfl(t1,t2)<>f; then A38: C5=2 to_power(n) by FUNCOP_1:def 8; A39: 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 A33,A35,XBOOLEAN:def 3 .= f 'or' t '&' t 'or' d2 '&' add_ovfl(t1,t2) by A37,XBOOLEAN:def 3 .= t; d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' add_ovfl(t1,t2) by A33,A35,XBOOLEAN:def 3 .= f by A37,XBOOLEAN:def 3; then C2=0 & C1=2 to_power (n+1) by A22,A39,FUNCOP_1:def 8; hence C2 + C1 = 2 to_power n * 2 to_power 1 by POWER:32 .= 2 * 2 to_power n by POWER:30 .= C5 + C3 + C4 by A34,A36,A38; end; end; hence C2 + C1 = C5 + C3 +C4; end; suppose A40: d2<>f; then A41: C4=2 to_power n by FUNCOP_1:def 8; now per cases; suppose A42: add_ovfl(t1,t2)=f; then A43: C5=0 by FUNCOP_1:def 8; A44: 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 A33,XBOOLEAN:def 3 .= t '&' t 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,t2) by A40,XBOOLEAN:def 3 .= t; d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' d2 'xor' add_ovfl(t1,t2) by A33,XBOOLEAN:def 3 .= f by A40,A42,XBOOLEAN:def 3; then C2=0 & C1=2 to_power (n+1) by A22,A44,FUNCOP_1:def 8; hence C2 + C1 = 2 to_power n * 2 to_power 1 by POWER:32 .= 2 * 2 to_power n by POWER:30 .= C5 + C3 + C4 by A34,A41,A43; end; suppose A45: add_ovfl(t1,t2)<>f; A46: 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 A33,XBOOLEAN:def 3 .= t '&' t 'or' d1 '&' add_ovfl(t1,t2) 'or' d2 '&' add_ovfl(t1,t2) by A40,XBOOLEAN:def 3 .= t; d1 'xor' d2 'xor' add_ovfl(t1,t2) = t 'xor' d2 'xor' add_ovfl(t1,t2) by A33,XBOOLEAN:def 3 .= f 'xor' add_ovfl(t1,t2) by A40,XBOOLEAN:def 3 .= t by A45,XBOOLEAN:def 3; then C2=2 to_power n & C1=2 to_power (n+1) by A22,A46,FUNCOP_1:def 8; hence C2 + C1 = 2 to_power n + 2 to_power n * 2 to_power 1 by POWER:32 .= 2 to_power n + 2 * 2 to_power n by POWER:30 .= 2 to_power n + 2 to_power n + 2 to_power n .= C5 + C3 + C4 by A34,A41,A45,FUNCOP_1:def 8; end; end; hence C2 + C1 = C5 + C3 +C4; end; end; hence C2 + C1 = C5 + C3 +C4; end; end; hence C2 + C1 = C5 + C3 +C4; 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 A20,A21,Th45 .=Absval(t1+t2) + C2 + C1 by Th46 .= Absval(t1+t2) + C5 + C3 + C4 by A23 .= Absval(t1) + Absval(t2) + C3 + C4 by A19 .= Absval(t1) + C3 + (Absval(t2) + C4 ) .= Absval(t1)+IFEQ(d1,FALSE,0,2 to_power n) + Absval(t2^<*d2*>) by Th46 .= Absval(z1) + Absval(z2) by A20,A21,Th46; end; thus for n being non empty Nat holds P[n] from NAT_1:sch 10(A1,A18); 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 Def10; 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 Th47; end; begin :: Addenda reserve a,b,c for natural number; :: from SCMFSA_7, 2005.02.05, A.T. theorem c <= a & c <= b & a -' c = b -' c implies a = b proof assume A1: a >= c & b >= c & a -' c = b -' c; then a - c >= 0 by XREAL_1:50; then A2: a -' c = a - c by Def3; b - c >= 0 by A1,XREAL_1:50; then a + (-c) = b + (-c) by A1,A2,Def3; hence thesis; end; theorem Th50: b <= a implies a -' b = a - b proof assume a >= b; then a - b >= 0 by XREAL_1:50; hence thesis by Def3; end; :: from GOBOARD9, 2005.02.05, A.T. theorem Th51: a -' a = 0 proof a-a = 0; hence thesis by Def3; end; theorem Th52: a -' b <= a proof a-b <= a-0 by REAL_2:106; hence thesis by Def3; end; :: from AMI_5, 2005.11.16, A.T. theorem Th53: for i,j being natural number st i >= j holds i -' j + j = i proof let i,j be natural number; assume i >= j; then ex m being Nat st i = j + m by NAT_1:10; hence i -' j + j = i by Th39; end; :: from JORDAN4:1, AK, 21.06,2006 reserve n,i,j,k for Nat; theorem Th54: n-'i=0 implies n<=i proof assume A1: n-'i=0; assume i=1 or i-i1>=1 implies i-'i1=i-i1 proof assume A1: i-'i1>=1 or i-i1>=1; per cases by A1; suppose i-'i1>=1; hence thesis by Def3; end; suppose i-i1>=1; hence thesis by Def3; end; end; theorem n-'0=n proof n-'0=n-0 by Def3 .=n; hence thesis; end; theorem i1<=i2 implies n-'i2<=n-'i1 proof assume A1: i1<=i2; per cases; suppose A2: i2<=n; then A3: n-'i1=n-i1 by A1,Th50,XXREAL_0:2; n-'i2=n-i2 by A2,Th50; hence n-'i2<=n-'i1 by A1,A3,REAL_2:106; end; suppose i2>n; then n-i2<0 by REAL_2:105; hence n-'i2<=n-'i1 by Def3; end; end; theorem Th60: i1<=i2 implies i1-'n<=i2-'n proof assume A1: i1<=i2; per cases; suppose i1-n>=0; then A2: i1-'n=i1-n by Def3; i1-n<=i2-n by A1,XREAL_1:11; hence thesis by A2,Def3; end; suppose i1-n<0; hence thesis by Def3; end; end; theorem Th61: i-'i1>=1 or i-i1>=1 implies i-'i1+i1=i proof assume i-'i1>=1 or i-i1>=1; then i-'i1+i1=i-i1+i1 by Th57 .=i; hence thesis; end; theorem i1<=i2 implies i1-'1<=i2 proof assume A1: i1<=i2; per cases; suppose i1-1>=0; then i1-'1=i1-1 by Def3; then i1-'1<=i1-1+1 by NAT_1:12; hence i1-'1<=i2 by A1,XXREAL_0:2; end; suppose i1-1<0; hence i1-'1<=i2 by Def3; end; end; theorem Th63: i-'2=i-'1-'1 proof per cases; suppose A1: i>=2; then 1<=i by XXREAL_0:2; then i-1>=0 by XREAL_1:50; then A2: i-'1=i-1 by Def3; i-1>=1+1-1 by A1,XREAL_1:11; then i-1-1>=1-1 by XREAL_1:11; then i-'1-'1 =i-2 by A2,Def3; hence thesis by Def3; end; suppose A3: i<2; then i-2<2-2 by XREAL_1:11; then A4: i-'2=0 by Def3; A5: i+1-1<=1+1-1 by A3,NAT_1:13; now per cases; case 1<=i; then i=1 by A5,XXREAL_0:1; then A6: i-'1-'1=0-'1 by Th51; thus thesis by A4,A6,Th52; end; case i<1; then i-1<1-1 by XREAL_1:11; then A7: i-'1-'1=0-'1 by Def3; thus thesis by A4,A7,Th52; end; end; hence thesis; end; end; theorem Th64: i1+1<=i2 implies i1-'1=i1 implies i>=i1-'i2 proof assume A1: i>=i1; i1>=i1-'i2 by Th52; hence thesis by A1,XXREAL_0:2; end; theorem 1<=i & 1<=i1-'i implies i1-'i= k; i-'k +k <= j + k by A1,XREAL_1:8; hence i <= j + k by A2,Th53; end; suppose A3: i <= k; k <= j + k by NAT_1:11; hence i <= j + k by A3,XXREAL_0:2; end; end; theorem :: SPRECT_3:6 i <= j + k implies i-'k <= j proof assume i <= j + k; then i -' k <= j + k -' k by Th60; hence i-'k <= j by Th39; end; theorem :: SPRECT_3:7 i <= j -' k & k <= j implies i + k <= j proof assume that A1: i <= j -' k and A2: j >= k; i + k <= j -' k + k by A1,XREAL_1:8; hence i + k <= j by A2,Th53; end; theorem :: SPRECT_3:8 j + k <= i implies k <= i -' j proof assume A1: j + k <= i; per cases by A1,XXREAL_0:1; suppose j + k = i; hence k <= i -' j by Th39; end; suppose j + k < i; hence k <= i -' j by Th70; end; end; theorem :: SPRECT_3:9 k <= i & i < j implies i -' k < j -' k proof assume that A1: k <= i and A2: i < j; i -' k + k = i by A1,Th53; then i -' k + k < j -' k + k by A1,A2,Th53,XXREAL_0:2; hence i -' k < j -' k by XREAL_1:8; end; theorem :: SPRECT_3:10 i < j & k < j implies i -' k < j -' k proof assume that A1: i < j and A2: k < j; per cases; suppose k <= i; then A3: i -' k = i - k by Th50; j -' k = j - k by A2,Th50; hence thesis by A1,A3,XREAL_1:11; end; suppose k > i; then i - k < 0 by REAL_2:105; then A4: i -' k = 0 by Def3; j -' k <> 0 by A2,Th54; hence thesis by A4; end; end; :: from JORDAN3, 2007.03.09, A.T theorem for D being non empty set, f being FinSequence of D, k being Nat holds len (f/^k)=len f-'k proof let D be non empty set, f be FinSequence of D,k be Nat; per cases; suppose A1: k<=len f; then len f-'k=len f-k by Th50; hence len (f/^k)=len f-'k by A1,RFINSEQ:def 2; end; suppose A2: k>len f; then (f/^k)=<*>D by RFINSEQ:def 2; then A3: len (f/^k)=0 by FINSEQ_1:32; len f-k<0 by A2,REAL_2:105; hence len (f/^k)=len f-'k by A3,Def3; end; end;