A1: add_ovfl <*TRUE *>,<*TRUE *> = TRUE by Th14;
Absval (<*TRUE *> + <*TRUE *>) = ((Absval (<*TRUE *> + <*TRUE *>)) + 2) - 2
.= ((Absval (<*TRUE *> + <*TRUE *>)) + (2 to_power 1)) - 2 by POWER:30
.= ((Absval (<*TRUE *> + <*TRUE *>)) + (IFEQ (add_ovfl <*TRUE *>,<*TRUE *>),FALSE ,0 ,(2 to_power 1))) - 2 by A1, FUNCOP_1:def 8
.= ((Absval <*TRUE *>) + (Absval <*TRUE *>)) - 2 by BINARITH:47
.= ((Absval <*TRUE *>) + 1) - 2 by BINARITH:42
.= (1 + 1) - 2 by BINARITH:42
.= Absval <*FALSE *> by BINARITH:41 ;
hence <*TRUE *> + <*TRUE *> = <*FALSE *> by Th2; :: thesis: verum