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