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;
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, 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 ;
A8: C2 + C1 = (C5 + C3) + C4
proof
now
per cases ( d1 = FALSE or d1 <> FALSE ) ;
suppose A9: d1 = FALSE ; :: thesis: C2 + C1 = (C5 + C3) + C4
then A10: C3 = 0 by FUNCOP_1:def 8;
now
per cases ( d2 = FALSE or d2 <> FALSE ) ;
suppose A11: d2 = FALSE ; :: thesis: C2 + C1 = (C5 + C3) + C4
then C4 = 0 by FUNCOP_1:def 8;
hence C2 + C1 = (C5 + C3) + C4 by A7, A9, A11, FUNCOP_1:def 8; :: thesis: verum
end;
suppose A12: d2 <> FALSE ; :: thesis: C2 + C1 = (C5 + C3) + C4
then A13: C4 = 2 to_power n by FUNCOP_1:def 8;
now
per cases ( add_ovfl (t1,t2) = FALSE or add_ovfl (t1,t2) <> FALSE ) ;
suppose A14: 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 A7, A9, A14, FUNCOP_1:def 8; :: thesis: verum
end;
suppose A15: 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 A9, A12, XBOOLEAN:def 3
.= FALSE 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))) = (FALSE 'or' FALSE) 'or' (TRUE '&' (add_ovfl (t1,t2))) by A9, A12, XBOOLEAN:def 3
.= TRUE 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 ;
:: 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 A18: d1 <> FALSE ; :: thesis: C2 + C1 = (C5 + C3) + C4
then A19: C3 = 2 to_power n by FUNCOP_1:def 8;
now
per cases ( d2 = FALSE or d2 <> FALSE ) ;
suppose A20: d2 = FALSE ; :: thesis: C2 + C1 = (C5 + C3) + C4
then A21: C4 = 0 by FUNCOP_1:def 8;
now
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 A7, A20, A21, FUNCOP_1:def 8; :: thesis: verum
end;
suppose A22: 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 A18, A20, XBOOLEAN:def 3
.= FALSE 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))) = (FALSE 'or' (TRUE '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2))) by A18, A20, XBOOLEAN:def 3
.= (FALSE 'or' (TRUE '&' TRUE)) 'or' (d2 '&' (add_ovfl (t1,t2))) by A22, XBOOLEAN:def 3
.= TRUE ;
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 ;
:: thesis: verum
end;
end;
end;
hence C2 + C1 = (C5 + C3) + C4 ; :: thesis: verum
end;
suppose A25: d2 <> FALSE ; :: thesis: C2 + C1 = (C5 + C3) + C4
then A26: C4 = 2 to_power n by FUNCOP_1:def 8;
now
per cases ( add_ovfl (t1,t2) = FALSE or add_ovfl (t1,t2) <> FALSE ) ;
suppose A27: 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 A18, XBOOLEAN:def 3
.= FALSE 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))) = ((TRUE '&' d2) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2))) by A18, XBOOLEAN:def 3
.= ((TRUE '&' TRUE) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2))) by A25, XBOOLEAN:def 3
.= TRUE ;
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 ;
:: thesis: verum
end;
suppose A30: 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 A18, XBOOLEAN:def 3
.= FALSE 'xor' (add_ovfl (t1,t2)) by A25, XBOOLEAN:def 3
.= TRUE 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))) = ((TRUE '&' d2) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2))) by A18, XBOOLEAN:def 3
.= ((TRUE '&' TRUE) 'or' (d1 '&' (add_ovfl (t1,t2)))) 'or' (d2 '&' (add_ovfl (t1,t2))) by A25, XBOOLEAN:def 3
.= TRUE ;
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 ;
:: 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, Th45
.= ((Absval (t1 + t2)) + C2) + C1 by Th46
.= (((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 Th46
.= (Absval z1) + (Absval z2) by A3, A4, Th46 ; :: thesis: verum
end;
A32: 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)
A33: (carry (z1,z2)) /. 1 = FALSE by Def5;
A34: Absval T = 1 by Th42;
A35: Absval F = 0 by Th41;
per cases ( ( z1 = <*FALSE*> & z2 = <*FALSE*> ) or ( z1 = <*TRUE*> & z2 = <*FALSE*> ) or ( z1 = <*FALSE*> & z2 = <*TRUE*> ) or ( z1 = <*TRUE*> & z2 = <*TRUE*> ) ) by Th40;
suppose A36: ( z1 = <*FALSE*> & z2 = <*FALSE*> ) ; :: thesis: (Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
A37: now
let i be Nat; :: thesis: ( i in Seg 1 implies F /. i = ((z1 /. i) 'xor' (z2 /. i)) 'xor' ((carry (z1,z2)) /. i) )
assume A38: i in Seg 1 ; :: thesis: F /. i = ((z1 /. i) 'xor' (z2 /. i)) 'xor' ((carry (z1,z2)) /. i)
then A39: i = 1 by FINSEQ_1:2, TARSKI:def 1;
thus F /. i = ((z1 /. 1) 'xor' FALSE) 'xor' FALSE by A36, A38, FINSEQ_1:2, TARSKI:def 1
.= ((z1 /. 1) 'xor' (z2 /. 1)) 'xor' FALSE by A36, FINSEQ_4:16
.= ((z1 /. i) 'xor' (z2 /. i)) 'xor' ((carry (z1,z2)) /. i) by A39, Def5 ; :: thesis: verum
end;
add_ovfl (z1,z2) = FALSE 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 (Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2) by A35, A36, A37, Def8; :: thesis: verum
end;
suppose A40: ( z1 = <*TRUE*> & z2 = <*FALSE*> ) ; :: thesis: (Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
A41: now
let i be Nat; :: thesis: ( i in Seg 1 implies T /. i = ((z1 /. i) 'xor' (z2 /. i)) 'xor' ((carry (z1,z2)) /. i) )
assume A42: i in Seg 1 ; :: thesis: T /. i = ((z1 /. i) 'xor' (z2 /. i)) 'xor' ((carry (z1,z2)) /. i)
then A43: i = 1 by FINSEQ_1:2, TARSKI:def 1;
thus T /. i = ((z1 /. 1) 'xor' FALSE) 'xor' FALSE by A40, A42, FINSEQ_1:2, TARSKI:def 1
.= ((z1 /. 1) 'xor' (z2 /. 1)) 'xor' FALSE by A40, FINSEQ_4:16
.= ((z1 /. i) 'xor' (z2 /. i)) 'xor' ((carry (z1,z2)) /. i) by A43, Def5 ; :: thesis: verum
end;
add_ovfl (z1,z2) = FALSE 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 (Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2) by A35, A40, A41, Def8; :: thesis: verum
end;
suppose A44: ( z1 = <*FALSE*> & z2 = <*TRUE*> ) ; :: thesis: (Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
A45: now
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 A46: 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 A44, FINSEQ_4:16
.= ((z1 /. 1) 'xor' (z2 /. 1)) 'xor' FALSE by A44, FINSEQ_4:16
.= ((z1 /. i) 'xor' (z2 /. i)) 'xor' ((carry (z1,z2)) /. i) by A46, Def5 ;
:: thesis: verum
end;
add_ovfl (z1,z2) = FALSE 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 (Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2) by A35, A44, A45, Def8; :: thesis: verum
end;
suppose A47: ( z1 = <*TRUE*> & z2 = <*TRUE*> ) ; :: thesis: (Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2)
now
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 A48: 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 A47, FINSEQ_4:16
.= ((z1 /. 1) 'xor' (z2 /. 1)) 'xor' FALSE by A47, FINSEQ_4:16
.= ((z1 /. i) 'xor' (z2 /. i)) 'xor' ((carry (z1,z2)) /. i) by A48, Def5 ;
:: thesis: verum
end;
then A49: z1 + z2 = <*FALSE*> by Def8;
add_ovfl (z1,z2) = TRUE 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 (Absval (z1 + z2)) + (IFEQ ((add_ovfl (z1,z2)),FALSE,0,(2 to_power 1))) = (Absval z1) + (Absval z2) by A34, A35, A47, A49; :: thesis: verum
end;
end;
end;
thus for n being non zero Nat holds S1[n] from NAT_1:sch 10(A32, A1); :: thesis: verum