:: deftheorem defines CLAADD4 GATE_5:def 18 :
for a1, b1, a2, b2, a3, b3, a4, b4, c being set holds CLAADD4 (a4,b4,a3,b3,a2,b2,a1,b1,c) = XOR3 (a4,b4,(CLACARR3 (a3,b3,a2,b2,a1,b1,c)));