:: deftheorem defines STC0IAdderOutputA3 WALLACE1:def 12 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0IAdderOutputA3 (x1,x2,x3,x4,x5,x6,x7) = GFA0AdderOutput ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4);