let m be non empty Nat; :: thesis: 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*>))
let z1, z2 be Tuple of m, BOOLEAN ; :: thesis: 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*>))
let d1, d2 be Element of BOOLEAN ; :: thesis: ((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*>))
set f = FALSE ;
set 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);
set siki2 = IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m);
((Absval (z1 + z2)) + (IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m))) - (IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m)) = Absval (z1 + z2) ;
hence Absval (z1 + z2) = ((Absval z1) + (Absval z2)) - (IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m)) by BINARITH:47; :: thesis: verum

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 ( ( d1 = FALSE & d2 = FALSE ) or ( d1 = TRUE & d2 = FALSE ) or ( d1 = FALSE & d2 = TRUE ) or ( d1 = TRUE & d2 = TRUE ) ) by XBOOLEAN:def 3;

suppose A8: ( d1 = FALSE & d2 = FALSE ) ; :: thesis: ((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*>))

then A9: (Absval z1) - (IFEQ d1,FALSE ,0 ,(2 to_power m)) = (Absval z1) - 0 by 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))),FALSE ,0 ,(2 to_power (m + 1)) = 0 by A8, FUNCOP_1:def 8;
thus ((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*>)) :: thesis: verum

proof

per cases ( add_ovfl z1,z2 = FALSE or add_ovfl z1,z2 = TRUE ) by XBOOLEAN:def 3;

suppose add_ovfl z1,z2 = FALSE ; :: thesis: ((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*>))

hence ((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*>)) by A3, A4, A5, A7, A8, A9, Th12; :: thesis: verum

end;

suppose A13: add_ovfl z1,z2 = TRUE ; :: thesis: ((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*>))

then IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m) = 2 to_power m by FUNCOP_1:def 8;
then ((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, 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) ;
hence ((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*>)) by A7, A9, A10, Th12; :: thesis: verum

end;

end;

end;

end;

suppose A16: ( d1 = TRUE & d2 = FALSE ) ; :: thesis: ((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*>))

then A17: (Absval z2) - (IFEQ d2,FALSE ,0 ,(2 to_power m)) = (Absval z2) - 0 by FUNCOP_1:def 8
.= Absval z2 ;
thus ((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*>)) :: thesis: verum

proof

per cases ( add_ovfl z1,z2 = FALSE or add_ovfl z1,z2 = TRUE ) by XBOOLEAN:def 3;

suppose A18: add_ovfl z1,z2 = FALSE ; :: thesis: ((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*>))

then IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m) = 0 by FUNCOP_1:def 8;
hence ((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*>)) by A3, A4, A5, A6, A7, A16, A17, A18; :: thesis: verum

end;

suppose add_ovfl z1,z2 = TRUE ; :: thesis: ((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*>))

hence ((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*>)) by A3, A4, A5, A6, A7, A16; :: thesis: verum

end;

end;

end;

end;

suppose A21: ( d1 = FALSE & d2 = TRUE ) ; :: thesis: ((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*>))

then A22: (Absval z1) - (IFEQ d1,FALSE ,0 ,(2 to_power m)) = (Absval z1) - 0 by FUNCOP_1:def 8
.= Absval z1 ;
thus ((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*>)) :: thesis: verum

proof

per cases ( add_ovfl z1,z2 = FALSE or add_ovfl z1,z2 = TRUE ) by XBOOLEAN:def 3;

suppose A23: add_ovfl z1,z2 = FALSE ; :: thesis: ((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*>))

then IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m) = 0 by FUNCOP_1:def 8;
hence ((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*>)) by A3, A4, A5, A6, A7, A21, A22, A23; :: thesis: verum

end;

suppose add_ovfl z1,z2 = TRUE ; :: thesis: ((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*>))

hence ((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*>)) by A3, A4, A5, A6, A7, A21; :: thesis: verum

end;

end;

end;

end;

suppose A26: ( d1 = TRUE & d2 = TRUE ) ; :: thesis: ((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*>))

then A27: (Absval z2) - (IFEQ d2,FALSE ,0 ,(2 to_power m)) = (Absval z2) - (2 to_power m) by FUNCOP_1:def 8;
A28: (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>)) = ((Absval z1) - (IFEQ d1,FALSE ,0 ,(2 to_power m))) + (Intval (z2 ^ <*d2*>)) by A6
.= ((Absval z1) + (Absval z2)) - (2 * (2 to_power m)) by 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)),FALSE ,0 ,(2 to_power (m + 1)) = 0 by A26, FUNCOP_1:def 8;
thus ((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*>)) :: thesis: verum

proof

per cases ( add_ovfl z1,z2 = FALSE or add_ovfl z1,z2 = TRUE ) by XBOOLEAN:def 3;

suppose A30: add_ovfl z1,z2 = FALSE ; :: thesis: ((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*>))

then IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m) = 0 by FUNCOP_1:def 8;
hence ((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*>)) by A3, A4, A5, A26, A28, A29, A30, FUNCOP_1:def 8; :: thesis: verum

end;

suppose A32: add_ovfl z1,z2 = TRUE ; :: thesis: ((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*>))

then IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m) = 2 to_power m by FUNCOP_1:def 8;
then ((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
.= ((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 ;
hence ((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*>)) by A28; :: thesis: verum

end;

end;

end;

end;

end;