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