let m be non zero 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:21; :: thesis: verum

end;

A2: Intval ((z1 ^ <*d1*>) + (z2 ^ <*d2*>)) = Intval ((z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>) by BINARITH:19
.= (((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, Th10 ;
A3: Int_add_ovfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>)) = (('not' d1) '&' ('not' ((z2 ^ <*d2*>) /. (m + 1)))) '&' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) by BINARITH:2
.= (('not' d1) '&' ('not' d2)) '&' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1)) by BINARITH:2
.= (('not' d1) '&' ('not' d2)) '&' (add_ovfl (z1,z2)) by BINARITH:18 ;
A4: Int_add_udfl ((z1 ^ <*d1*>),(z2 ^ <*d2*>)) = (d1 '&' ((z2 ^ <*d2*>) /. (m + 1))) '&' ('not' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1))) by BINARITH:2
.= (d1 '&' d2) '&' ('not' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (m + 1))) by BINARITH:2
.= (d1 '&' d2) '&' ('not' (add_ovfl (z1,z2))) by BINARITH:18 ;
A5: Intval (z1 ^ <*d1*>) = (Absval z1) - (IFEQ (d1,FALSE,0,(2 to_power m))) by Th10;
A6: Intval (z2 ^ <*d2*>) = (Absval z2) - (IFEQ (d2,FALSE,0,(2 to_power m))) by Th10;

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 A7: ( 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 A8: (Absval z1) - (IFEQ (d1,FALSE,0,(2 to_power m))) = (Absval z1) - 0 by FUNCOP_1:def 8
.= Absval z1 ;
A9: (Absval z2) - (IFEQ (d2,FALSE,0,(2 to_power m))) = (Absval z2) - 0 by A7, FUNCOP_1:def 8
.= Absval z2 ;
A10: IFEQ (((d1 '&' d2) '&' ('not' (add_ovfl (z1,z2)))),FALSE,0,(2 to_power (m + 1))) = 0 by A7, 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 A2, A3, A4, A6, A7, A8, Th10; :: thesis: verum

end;

suppose A11: 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 A2, A3, A4, A7, A10, A11, FUNCOP_1:def 8
.= (((Absval z1) + (Absval z2)) - ((2 to_power 1) * (2 to_power m))) + (2 to_power (m + 1)) by POWER:25
.= (((Absval z1) + (Absval z2)) - (2 to_power (m + 1))) + (2 to_power (m + 1)) by POWER:27
.= (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 A6, A8, A9, Th10; :: thesis: verum

end;

end;

end;

end;

suppose A12: ( 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 A13: (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 A14: 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 A2, A3, A4, A5, A6, A12, A13, A14; :: 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 A2, A3, A4, A5, A6, A12; :: thesis: verum

end;

end;

end;

end;

suppose A15: ( 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 A16: (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 A17: 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 A2, A3, A4, A5, A6, A15, A16, A17; :: 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 A2, A3, A4, A5, A6, A15; :: thesis: verum

end;

end;

end;

end;

suppose A18: ( 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 A19: (Absval z2) - (IFEQ (d2,FALSE,0,(2 to_power m))) = (Absval z2) - (2 to_power m) by FUNCOP_1:def 8;
A20: (Intval (z1 ^ <*d1*>)) + (Intval (z2 ^ <*d2*>)) = ((Absval z1) - (IFEQ (d1,FALSE,0,(2 to_power m)))) + (Intval (z2 ^ <*d2*>)) by A5
.= ((Absval z1) + (Absval z2)) - (2 * (2 to_power m)) by A6, A18, A19
.= ((Absval z1) + (Absval z2)) - ((2 to_power 1) * (2 to_power m)) by POWER:25
.= ((Absval z1) + (Absval z2)) - (2 to_power (m + 1)) by POWER:27 ;
A21: IFEQ (((('not' d1) '&' ('not' d2)) '&' (add_ovfl (z1,z2))),FALSE,0,(2 to_power (m + 1))) = 0 by A18, 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 A22: 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 A2, A3, A4, A18, A20, A21, A22, FUNCOP_1:def 8; :: thesis: verum

end;

suppose A23: 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 A2, A3, A4, A18, A23
.= ((Absval z1) + (Absval z2)) - ((2 to_power 1) * (2 to_power m)) by POWER:25
.= ((Absval z1) + (Absval z2)) - (2 to_power (m + 1)) by POWER:27 ;
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 A20; :: thesis: verum

end;

end;

end;

end;

end;