:: GATE_5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for a, b being set holds
( ( $ XOR3 a,b,{} implies $ XOR2 a,b ) & ( $ XOR2 a,b implies $ XOR3 a,b,{} ) & ( $ XOR3 a,{} ,b implies $ XOR2 a,b ) & ( $ XOR2 a,b implies $ XOR3 a,{} ,b ) & ( $ XOR3 {} ,a,b implies $ XOR2 a,b ) & ( $ XOR2 a,b implies $ XOR3 {} ,a,b ) )
proof end;

Lm2: for a, b being set holds
( ( $ MAJ3 a,b,{} implies $ AND2 a,b ) & ( $ AND2 a,b implies $ MAJ3 a,b,{} ) & ( $ MAJ3 a,{} ,b implies $ AND2 a,b ) & ( $ AND2 a,b implies $ MAJ3 a,{} ,b ) & ( $ MAJ3 {} ,a,b implies $ AND2 a,b ) & ( $ AND2 a,b implies $ MAJ3 {} ,a,b ) )
proof end;

definition
let x0, x1, y0, y1 be set ;
func MULT210 x1,y1,x0,y0 -> set equals :: GATE_5:def 1
 AND2 x0,y0;
correctness
coherence
AND2 x0,y0 is set ;
;
func MULT211 x1,y1,x0,y0 -> set equals :: GATE_5:def 2
 ADD1 (AND2 x1,y0),(AND2 x0,y1),{} ;
correctness
coherence
ADD1 (AND2 x1,y0),(AND2 x0,y1),{} is set ;
;
func MULT212 x1,y1,x0,y0 -> set equals :: GATE_5:def 3
 ADD2 {} ,(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} ;
correctness
coherence
ADD2 {} ,(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} is set ;
;
func MULT213 x1,y1,x0,y0 -> set equals :: GATE_5:def 4
 CARR2 {} ,(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} ;
correctness
coherence
CARR2 {} ,(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} is set ;
;
end;

:: deftheorem defines MULT210 GATE_5:def 1 :
for x0, x1, y0, y1 being set holds MULT210 x1,y1,x0,y0 = AND2 x0,y0;

:: deftheorem defines MULT211 GATE_5:def 2 :
for x0, x1, y0, y1 being set holds MULT211 x1,y1,x0,y0 = ADD1 (AND2 x1,y0),(AND2 x0,y1),{} ;

:: deftheorem defines MULT212 GATE_5:def 3 :
for x0, x1, y0, y1 being set holds MULT212 x1,y1,x0,y0 = ADD2 {} ,(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} ;

:: deftheorem defines MULT213 GATE_5:def 4 :
for x0, x1, y0, y1 being set holds MULT213 x1,y1,x0,y0 = CARR2 {} ,(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} ;

theorem :: GATE_5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x0, x1, y0, y1, z0, z1, z2, z3, q00, q01, c01, q11, c11 being set holds
not ( ( $ q00 implies $ AND2 x0,y0 ) & ( $ AND2 x0,y0 implies $ q00 ) & ( $ q01 implies $ XOR3 (AND2 x1,y0),(AND2 x0,y1),{} ) & ( $ XOR3 (AND2 x1,y0),(AND2 x0,y1),{} implies $ q01 ) & ( $ c01 implies $ MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} ) & ( $ MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} implies $ c01 ) & ( $ q11 implies $ XOR3 (AND2 x1,y1),{} ,c01 ) & ( $ XOR3 (AND2 x1,y1),{} ,c01 implies $ q11 ) & ( $ c11 implies $ MAJ3 (AND2 x1,y1),{} ,c01 ) & ( $ MAJ3 (AND2 x1,y1),{} ,c01 implies $ c11 ) & ( $ z0 implies $ q00 ) & ( $ q00 implies $ z0 ) & ( $ z1 implies $ q01 ) & ( $ q01 implies $ z1 ) & ( $ z2 implies $ q11 ) & ( $ q11 implies $ z2 ) & ( $ z3 implies $ c11 ) & ( $ c11 implies $ z3 ) & not ( ( $ z0 implies $ MULT210 x1,y1,x0,y0 ) & ( $ MULT210 x1,y1,x0,y0 implies $ z0 ) & ( $ z1 implies $ MULT211 x1,y1,x0,y0 ) & ( $ MULT211 x1,y1,x0,y0 implies $ z1 ) & ( $ z2 implies $ MULT212 x1,y1,x0,y0 ) & ( $ MULT212 x1,y1,x0,y0 implies $ z2 ) & ( $ z3 implies $ MULT213 x1,y1,x0,y0 ) & ( $ MULT213 x1,y1,x0,y0 implies $ z3 ) ) )
proof end;

definition
let x0, x1, x2, y0, y1 be set ;
func MULT310 x2,x1,y1,x0,y0 -> set equals :: GATE_5:def 5
 AND2 x0,y0;
correctness
coherence
AND2 x0,y0 is set ;
;
func MULT311 x2,x1,y1,x0,y0 -> set equals :: GATE_5:def 6
 ADD1 (AND2 x1,y0),(AND2 x0,y1),{} ;
correctness
coherence
ADD1 (AND2 x1,y0),(AND2 x0,y1),{} is set ;
;
func MULT312 x2,x1,y1,x0,y0 -> set equals :: GATE_5:def 7
 ADD2 (AND2 x2,y0),(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} ;
correctness
coherence
ADD2 (AND2 x2,y0),(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} is set ;
;
func MULT313 x2,x1,y1,x0,y0 -> set equals :: GATE_5:def 8
 ADD3 {} ,(AND2 x2,y1),(AND2 x2,y0),(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} ;
correctness
coherence
ADD3 {} ,(AND2 x2,y1),(AND2 x2,y0),(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} is set ;
;
func MULT314 x2,x1,y1,x0,y0 -> set equals :: GATE_5:def 9
 CARR3 {} ,(AND2 x2,y1),(AND2 x2,y0),(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} ;
correctness
coherence
CARR3 {} ,(AND2 x2,y1),(AND2 x2,y0),(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} is set ;
;
end;

:: deftheorem defines MULT310 GATE_5:def 5 :
for x0, x1, x2, y0, y1 being set holds MULT310 x2,x1,y1,x0,y0 = AND2 x0,y0;

:: deftheorem defines MULT311 GATE_5:def 6 :
for x0, x1, x2, y0, y1 being set holds MULT311 x2,x1,y1,x0,y0 = ADD1 (AND2 x1,y0),(AND2 x0,y1),{} ;

:: deftheorem defines MULT312 GATE_5:def 7 :
for x0, x1, x2, y0, y1 being set holds MULT312 x2,x1,y1,x0,y0 = ADD2 (AND2 x2,y0),(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} ;

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

:: deftheorem defines MULT314 GATE_5:def 9 :
for x0, x1, x2, y0, y1 being set holds MULT314 x2,x1,y1,x0,y0 = CARR3 {} ,(AND2 x2,y1),(AND2 x2,y0),(AND2 x1,y1),(AND2 x1,y0),(AND2 x0,y1),{} ;

definition
let x0, x1, x2, y0, y1, y2 be set ;
func MULT321 x2,y2,x1,y1,x0,y0 -> set equals :: GATE_5:def 10
 ADD1 (MULT312 x2,x1,y1,x0,y0),(AND2 x0,y2),{} ;
correctness
coherence
ADD1 (MULT312 x2,x1,y1,x0,y0),(AND2 x0,y2),{} is set ;
;
func MULT322 x2,y2,x1,y1,x0,y0 -> set equals :: GATE_5:def 11
 ADD2 (MULT313 x2,x1,y1,x0,y0),(AND2 x1,y2),(MULT312 x2,x1,y1,x0,y0),(AND2 x0,y2),{} ;
correctness
coherence
ADD2 (MULT313 x2,x1,y1,x0,y0),(AND2 x1,y2),(MULT312 x2,x1,y1,x0,y0),(AND2 x0,y2),{} is set ;
;
func MULT323 x2,y2,x1,y1,x0,y0 -> set equals :: GATE_5:def 12
 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),{} ;
correctness
coherence
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),{} is set ;
;
func MULT324 x2,y2,x1,y1,x0,y0 -> set equals :: GATE_5:def 13
 CARR3 (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),{} ;
correctness
coherence
CARR3 (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),{} is set ;
;
end;

:: deftheorem defines MULT321 GATE_5:def 10 :
for x0, x1, x2, y0, y1, y2 being set holds MULT321 x2,y2,x1,y1,x0,y0 = ADD1 (MULT312 x2,x1,y1,x0,y0),(AND2 x0,y2),{} ;

:: deftheorem defines MULT322 GATE_5:def 11 :
for x0, x1, x2, y0, y1, y2 being set holds MULT322 x2,y2,x1,y1,x0,y0 = ADD2 (MULT313 x2,x1,y1,x0,y0),(AND2 x1,y2),(MULT312 x2,x1,y1,x0,y0),(AND2 x0,y2),{} ;

:: 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),{} ;

:: deftheorem defines MULT324 GATE_5:def 13 :
for x0, x1, x2, y0, y1, y2 being set holds MULT324 x2,y2,x1,y1,x0,y0 = CARR3 (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),{} ;

theorem :: GATE_5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x0, x1, x2, y0, y1, y2, z0, z1, z2, z3, z4, z5, q00, q01, q02, c01, c02, q11, q12, c11, c12, q21, q22, c21, c22 being set holds
not ( ( $ q00 implies $ AND2 x0,y0 ) & ( $ AND2 x0,y0 implies $ q00 ) & ( $ q01 implies $ XOR3 (AND2 x1,y0),(AND2 x0,y1),{} ) & ( $ XOR3 (AND2 x1,y0),(AND2 x0,y1),{} implies $ q01 ) & ( $ c01 implies $ MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} ) & ( $ MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} implies $ c01 ) & ( $ q02 implies $ XOR3 (AND2 x2,y0),(AND2 x1,y1),{} ) & ( $ XOR3 (AND2 x2,y0),(AND2 x1,y1),{} implies $ q02 ) & ( $ c02 implies $ MAJ3 (AND2 x2,y0),(AND2 x1,y1),{} ) & ( $ MAJ3 (AND2 x2,y0),(AND2 x1,y1),{} implies $ c02 ) & ( $ q11 implies $ XOR3 q02,(AND2 x0,y2),c01 ) & ( $ XOR3 q02,(AND2 x0,y2),c01 implies $ q11 ) & ( $ c11 implies $ MAJ3 q02,(AND2 x0,y2),c01 ) & ( $ MAJ3 q02,(AND2 x0,y2),c01 implies $ c11 ) & ( $ q12 implies $ XOR3 (AND2 x2,y1),(AND2 x1,y2),c02 ) & ( $ XOR3 (AND2 x2,y1),(AND2 x1,y2),c02 implies $ q12 ) & ( $ c12 implies $ MAJ3 (AND2 x2,y1),(AND2 x1,y2),c02 ) & ( $ MAJ3 (AND2 x2,y1),(AND2 x1,y2),c02 implies $ c12 ) & ( $ q21 implies $ XOR3 q12,{} ,c11 ) & ( $ XOR3 q12,{} ,c11 implies $ q21 ) & ( $ c21 implies $ MAJ3 q12,{} ,c11 ) & ( $ MAJ3 q12,{} ,c11 implies $ c21 ) & ( $ q22 implies $ XOR3 (AND2 x2,y2),c21,c12 ) & ( $ XOR3 (AND2 x2,y2),c21,c12 implies $ q22 ) & ( $ c22 implies $ MAJ3 (AND2 x2,y2),c21,c12 ) & ( $ MAJ3 (AND2 x2,y2),c21,c12 implies $ c22 ) & ( $ z0 implies $ q00 ) & ( $ q00 implies $ z0 ) & ( $ z1 implies $ q01 ) & ( $ q01 implies $ z1 ) & ( $ z2 implies $ q11 ) & ( $ q11 implies $ z2 ) & ( $ z3 implies $ q21 ) & ( $ q21 implies $ z3 ) & ( $ z4 implies $ q22 ) & ( $ q22 implies $ z4 ) & ( $ z5 implies $ c22 ) & ( $ c22 implies $ z5 ) & not ( ( $ z0 implies $ MULT310 x2,x1,y1,x0,y0 ) & ( $ MULT310 x2,x1,y1,x0,y0 implies $ z0 ) & ( $ z1 implies $ MULT311 x2,x1,y1,x0,y0 ) & ( $ MULT311 x2,x1,y1,x0,y0 implies $ z1 ) & ( $ z2 implies $ MULT321 x2,y2,x1,y1,x0,y0 ) & ( $ MULT321 x2,y2,x1,y1,x0,y0 implies $ z2 ) & ( $ z3 implies $ MULT322 x2,y2,x1,y1,x0,y0 ) & ( $ MULT322 x2,y2,x1,y1,x0,y0 implies $ z3 ) & ( $ z4 implies $ MULT323 x2,y2,x1,y1,x0,y0 ) & ( $ MULT323 x2,y2,x1,y1,x0,y0 implies $ z4 ) & ( $ z5 implies $ MULT324 x2,y2,x1,y1,x0,y0 ) & ( $ MULT324 x2,y2,x1,y1,x0,y0 implies $ z5 ) ) )
proof end;

theorem :: GATE_5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x0, x1, x2, y0, y1, y2, z0, z1, z2, z3, z4, z5, q00, q01, q02, q03, c01, c02, c03, q11, q12, q13, c11, c12, c13 being set holds
not ( ( $ q00 implies $ AND2 x0,y0 ) & ( $ AND2 x0,y0 implies $ q00 ) & ( $ q01 implies $ XOR3 (AND2 x1,y0),(AND2 x0,y1),{} ) & ( $ XOR3 (AND2 x1,y0),(AND2 x0,y1),{} implies $ q01 ) & ( $ c01 implies $ MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} ) & ( $ MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} implies $ c01 ) & ( $ q02 implies $ XOR3 (AND2 x2,y0),(AND2 x1,y1),(AND2 x0,y2) ) & ( $ XOR3 (AND2 x2,y0),(AND2 x1,y1),(AND2 x0,y2) implies $ q02 ) & ( $ c02 implies $ MAJ3 (AND2 x2,y0),(AND2 x1,y1),(AND2 x0,y2) ) & ( $ MAJ3 (AND2 x2,y0),(AND2 x1,y1),(AND2 x0,y2) implies $ c02 ) & ( $ q03 implies $ XOR3 (AND2 x2,y1),(AND2 x1,y2),{} ) & ( $ XOR3 (AND2 x2,y1),(AND2 x1,y2),{} implies $ q03 ) & ( $ c03 implies $ MAJ3 (AND2 x2,y1),(AND2 x1,y2),{} ) & ( $ MAJ3 (AND2 x2,y1),(AND2 x1,y2),{} implies $ c03 ) & ( $ q11 implies $ XOR3 q02,c01,{} ) & ( $ XOR3 q02,c01,{} implies $ q11 ) & ( $ c11 implies $ MAJ3 q02,c01,{} ) & ( $ MAJ3 q02,c01,{} implies $ c11 ) & ( $ q12 implies $ XOR3 q03,c02,c11 ) & ( $ XOR3 q03,c02,c11 implies $ q12 ) & ( $ c12 implies $ MAJ3 q03,c02,c11 ) & ( $ MAJ3 q03,c02,c11 implies $ c12 ) & ( $ q13 implies $ XOR3 (AND2 x2,y2),c03,c12 ) & ( $ XOR3 (AND2 x2,y2),c03,c12 implies $ q13 ) & ( $ c13 implies $ MAJ3 (AND2 x2,y2),c03,c12 ) & ( $ MAJ3 (AND2 x2,y2),c03,c12 implies $ c13 ) & ( $ z0 implies $ q00 ) & ( $ q00 implies $ z0 ) & ( $ z1 implies $ q01 ) & ( $ q01 implies $ z1 ) & ( $ z2 implies $ q11 ) & ( $ q11 implies $ z2 ) & ( $ z3 implies $ q12 ) & ( $ q12 implies $ z3 ) & ( $ z4 implies $ q13 ) & ( $ q13 implies $ z4 ) & ( $ z5 implies $ c13 ) & ( $ c13 implies $ z5 ) & not ( ( $ z0 implies $ MULT310 x2,x1,y1,x0,y0 ) & ( $ MULT310 x2,x1,y1,x0,y0 implies $ z0 ) & ( $ z1 implies $ MULT311 x2,x1,y1,x0,y0 ) & ( $ MULT311 x2,x1,y1,x0,y0 implies $ z1 ) & ( $ z2 implies $ MULT321 x2,y2,x1,y1,x0,y0 ) & ( $ MULT321 x2,y2,x1,y1,x0,y0 implies $ z2 ) & ( $ z3 implies $ MULT322 x2,y2,x1,y1,x0,y0 ) & ( $ MULT322 x2,y2,x1,y1,x0,y0 implies $ z3 ) & ( $ z4 implies $ MULT323 x2,y2,x1,y1,x0,y0 ) & ( $ MULT323 x2,y2,x1,y1,x0,y0 implies $ z4 ) & ( $ z5 implies $ MULT324 x2,y2,x1,y1,x0,y0 ) & ( $ MULT324 x2,y2,x1,y1,x0,y0 implies $ z5 ) ) )
proof end;

notation
let a1, b1, c be set ;
synonym CLAADD1 a1,b1,c for XOR3 a1,b1,c;
synonym CLACARR1 a1,b1,c for MAJ3 a1,b1,c;
end;

definition
let a1, b1, a2, b2, c be set ;
canceled;
canceled;
func CLAADD2 a2,b2,a1,b1,c -> set equals :: GATE_5:def 16
 XOR3 a2,b2,(MAJ3 a1,b1,c);
correctness
coherence
XOR3 a2,b2,(MAJ3 a1,b1,c) is set ;
;
func CLACARR2 a2,b2,a1,b1,c -> set equals :: GATE_5:def 17
 OR2 (AND2 a2,b2),(AND2 (OR2 a2,b2),(MAJ3 a1,b1,c));
correctness
coherence
OR2 (AND2 a2,b2),(AND2 (OR2 a2,b2),(MAJ3 a1,b1,c)) is set ;
;
end;

:: deftheorem GATE_5:def 14 :
canceled;

:: deftheorem GATE_5:def 15 :
canceled;

:: deftheorem defines CLAADD2 GATE_5:def 16 :
for a1, b1, a2, b2, c being set holds CLAADD2 a2,b2,a1,b1,c = XOR3 a2,b2,(MAJ3 a1,b1,c);

:: deftheorem defines CLACARR2 GATE_5:def 17 :
for a1, b1, a2, b2, c being set holds CLACARR2 a2,b2,a1,b1,c = OR2 (AND2 a2,b2),(AND2 (OR2 a2,b2),(MAJ3 a1,b1,c));

definition
let a1, b1, a2, b2, a3, b3, c be set ;
func CLAADD3 a3,b3,a2,b2,a1,b1,c -> set equals :: GATE_5:def 18
 XOR3 a3,b3,(CLACARR2 a2,b2,a1,b1,c);
correctness
coherence
XOR3 a3,b3,(CLACARR2 a2,b2,a1,b1,c) is set ;
;
func CLACARR3 a3,b3,a2,b2,a1,b1,c -> set equals :: GATE_5:def 19
 OR3 (AND2 a3,b3),(AND2 (OR2 a3,b3),(AND2 a2,b2)),(AND3 (OR2 a3,b3),(OR2 a2,b2),(MAJ3 a1,b1,c));
correctness
coherence
OR3 (AND2 a3,b3),(AND2 (OR2 a3,b3),(AND2 a2,b2)),(AND3 (OR2 a3,b3),(OR2 a2,b2),(MAJ3 a1,b1,c)) is set ;
;
end;

:: deftheorem defines CLAADD3 GATE_5:def 18 :
for a1, b1, a2, b2, a3, b3, c being set holds CLAADD3 a3,b3,a2,b2,a1,b1,c = XOR3 a3,b3,(CLACARR2 a2,b2,a1,b1,c);

:: deftheorem defines CLACARR3 GATE_5:def 19 :
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));

definition
let a1, b1, a2, b2, a3, b3, a4, b4, c be set ;
func CLAADD4 a4,b4,a3,b3,a2,b2,a1,b1,c -> set equals :: GATE_5:def 20
 XOR3 a4,b4,(CLACARR3 a3,b3,a2,b2,a1,b1,c);
correctness
coherence
XOR3 a4,b4,(CLACARR3 a3,b3,a2,b2,a1,b1,c) is set ;
;
func CLACARR4 a4,b4,a3,b3,a2,b2,a1,b1,c -> set equals :: GATE_5:def 21
 OR4 (AND2 a4,b4),(AND2 (OR2 a4,b4),(AND2 a3,b3)),(AND3 (OR2 a4,b4),(OR2 a3,b3),(AND2 a2,b2)),(AND4 (OR2 a4,b4),(OR2 a3,b3),(OR2 a2,b2),(MAJ3 a1,b1,c));
correctness
coherence
OR4 (AND2 a4,b4),(AND2 (OR2 a4,b4),(AND2 a3,b3)),(AND3 (OR2 a4,b4),(OR2 a3,b3),(AND2 a2,b2)),(AND4 (OR2 a4,b4),(OR2 a3,b3),(OR2 a2,b2),(MAJ3 a1,b1,c)) is set ;
;
end;

:: deftheorem defines CLAADD4 GATE_5:def 20 :
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);

:: deftheorem defines CLACARR4 GATE_5:def 21 :
for a1, b1, a2, b2, a3, b3, a4, b4, c being set holds CLACARR4 a4,b4,a3,b3,a2,b2,a1,b1,c = OR4 (AND2 a4,b4),(AND2 (OR2 a4,b4),(AND2 a3,b3)),(AND3 (OR2 a4,b4),(OR2 a3,b3),(AND2 a2,b2)),(AND4 (OR2 a4,b4),(OR2 a3,b3),(OR2 a2,b2),(MAJ3 a1,b1,c));

theorem :: GATE_5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x0, x1, x2, y0, y1, y2, z0, z1, z2, z3, z4, z5, q00, q01, q02, q03, c01, c02, c03 being set holds
not ( ( $ q00 implies $ AND2 x0,y0 ) & ( $ AND2 x0,y0 implies $ q00 ) & ( $ q01 implies $ XOR3 (AND2 x1,y0),(AND2 x0,y1),{} ) & ( $ XOR3 (AND2 x1,y0),(AND2 x0,y1),{} implies $ q01 ) & ( $ c01 implies $ MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} ) & ( $ MAJ3 (AND2 x1,y0),(AND2 x0,y1),{} implies $ c01 ) & ( $ q02 implies $ XOR3 (AND2 x2,y0),(AND2 x1,y1),(AND2 x0,y2) ) & ( $ XOR3 (AND2 x2,y0),(AND2 x1,y1),(AND2 x0,y2) implies $ q02 ) & ( $ c02 implies $ MAJ3 (AND2 x2,y0),(AND2 x1,y1),(AND2 x0,y2) ) & ( $ MAJ3 (AND2 x2,y0),(AND2 x1,y1),(AND2 x0,y2) implies $ c02 ) & ( $ q03 implies $ XOR3 (AND2 x2,y1),(AND2 x1,y2),{} ) & ( $ XOR3 (AND2 x2,y1),(AND2 x1,y2),{} implies $ q03 ) & ( $ c03 implies $ MAJ3 (AND2 x2,y1),(AND2 x1,y2),{} ) & ( $ MAJ3 (AND2 x2,y1),(AND2 x1,y2),{} implies $ c03 ) & ( $ z0 implies $ q00 ) & ( $ q00 implies $ z0 ) & ( $ z1 implies $ q01 ) & ( $ q01 implies $ z1 ) & ( $ z2 implies $ CLAADD1 q02,c01,{} ) & ( $ CLAADD1 q02,c01,{} implies $ z2 ) & ( $ z3 implies $ CLAADD2 q03,c02,q02,c01,{} ) & ( $ CLAADD2 q03,c02,q02,c01,{} implies $ z3 ) & ( $ z4 implies $ CLAADD3 (AND2 x2,y2),c03,q03,c02,q02,c01,{} ) & ( $ CLAADD3 (AND2 x2,y2),c03,q03,c02,q02,c01,{} implies $ z4 ) & ( $ z5 implies $ CLACARR3 (AND2 x2,y2),c03,q03,c02,q02,c01,{} ) & ( $ CLACARR3 (AND2 x2,y2),c03,q03,c02,q02,c01,{} implies $ z5 ) & not ( ( $ z0 implies $ MULT310 x2,x1,y1,x0,y0 ) & ( $ MULT310 x2,x1,y1,x0,y0 implies $ z0 ) & ( $ z1 implies $ MULT311 x2,x1,y1,x0,y0 ) & ( $ MULT311 x2,x1,y1,x0,y0 implies $ z1 ) & ( $ z2 implies $ MULT321 x2,y2,x1,y1,x0,y0 ) & ( $ MULT321 x2,y2,x1,y1,x0,y0 implies $ z2 ) & ( $ z3 implies $ MULT322 x2,y2,x1,y1,x0,y0 ) & ( $ MULT322 x2,y2,x1,y1,x0,y0 implies $ z3 ) & ( $ z4 implies $ MULT323 x2,y2,x1,y1,x0,y0 ) & ( $ MULT323 x2,y2,x1,y1,x0,y0 implies $ z4 ) & ( $ z5 implies $ MULT324 x2,y2,x1,y1,x0,y0 ) & ( $ MULT324 x2,y2,x1,y1,x0,y0 implies $ z5 ) ) )
proof end;