:: deftheorem defines CLACARR3 GATE_5:def 17 :
for a1, b1, a2, b2, a3, b3, c being set holds CLACARR3 (a3,b3,a2,b2,a1,b1,c) = OR3 ((AND2 (a3,b3)),(AND2 ((OR2 (a3,b3)),(AND2 (a2,b2)))),(AND3 ((OR2 (a3,b3)),(OR2 (a2,b2)),(MAJ3 (a1,b1,c)))));