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);
A2: ((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) ;
thus Absval (z1 + z2) = ((Absval z1) + (Absval z2)) - (IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m)) by A2, 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*>))

A9: (Absval z1) - (IFEQ d1,FALSE ,0 ,(2 to_power m)) = (Absval z1) - 0 by A8, 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 A12: 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*>))

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*>)) by A3, A4, A5, A7, A8, A9, A12, 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*>))

A14: IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m) = 2 to_power m by A13, FUNCOP_1:def 8;
A15: ((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, A14, 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) ;
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*>)) by A7, A9, A10, A15, 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*>))

A17: (Absval z2) - (IFEQ d2,FALSE ,0 ,(2 to_power m)) = (Absval z2) - 0 by A16, 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*>))

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

end;

suppose A20: 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*>))

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

A22: (Absval z1) - (IFEQ d1,FALSE ,0 ,(2 to_power m)) = (Absval z1) - 0 by A21, 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*>))

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

end;

suppose A25: 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*>))

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

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

A31: IFEQ (add_ovfl z1,z2),FALSE ,0 ,(2 to_power m) = 0 by A30, 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*>)) by A3, A4, A5, A26, A28, A29, A30, A31, 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*>))

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

end;

end;

end;

end;

end;