:: deftheorem defines STC0ICirc WALLACE1:def 8 :
for x1, x2, x3, x4, x5, x6, x7 being set holds STC0ICirc (x1,x2,x3,x4,x5,x6,x7) = (STC0IICirc (x1,x2,x3,x5,x6,x7)) +* (BitGFA0Circ ((GFA0AdderOutput (x1,x2,x3)),(GFA0AdderOutput (x5,x6,x7)),x4));