:: deftheorem defines MULT323 GATE_5:def 12 :
for x0, x1, x2, y0, y1, y2 being set holds MULT323 (x2,y2,x1,y1,x0,y0) = ADD3 ((MULT314 (x2,x1,y1,x0,y0)),(AND2 (x2,y2)),(MULT313 (x2,x1,y1,x0,y0)),(AND2 (x1,y2)),(MULT312 (x2,x1,y1,x0,y0)),(AND2 (x0,y2)),{});