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