:: GATE_5 semantic presentation
Lemma1:
for b1, b2 being set holds
( ( $ XOR3 b1,b2,{} implies $ XOR2 b1,b2 ) & ( $ XOR2 b1,b2 implies $ XOR3 b1,b2,{} ) & ( $ XOR3 b1,{} ,b2 implies $ XOR2 b1,b2 ) & ( $ XOR2 b1,b2 implies $ XOR3 b1,{} ,b2 ) & ( $ XOR3 {} ,b1,b2 implies $ XOR2 b1,b2 ) & ( $ XOR2 b1,b2 implies $ XOR3 {} ,b1,b2 ) )
Lemma2:
for b1, b2 being set holds
( ( $ MAJ3 b1,b2,{} implies $ AND2 b1,b2 ) & ( $ AND2 b1,b2 implies $ MAJ3 b1,b2,{} ) & ( $ MAJ3 b1,{} ,b2 implies $ AND2 b1,b2 ) & ( $ AND2 b1,b2 implies $ MAJ3 b1,{} ,b2 ) & ( $ MAJ3 {} ,b1,b2 implies $ AND2 b1,b2 ) & ( $ AND2 b1,b2 implies $ MAJ3 {} ,b1,b2 ) )
definition
let c1,
c2,
c3,
c4 be
set ;
func MULT210 c2,
c4,
c1,
c3 -> set equals :: GATE_5:def 1
AND2 a1,
a3;
correctness
coherence
AND2 c1,c3 is set ;
;
func MULT211 c2,
c4,
c1,
c3 -> set equals :: GATE_5:def 2
ADD1 (AND2 a2,a3),
(AND2 a1,a4),
{} ;
correctness
coherence
ADD1 (AND2 c2,c3),(AND2 c1,c4),{} is set ;
;
func MULT212 c2,
c4,
c1,
c3 -> set equals :: GATE_5:def 3
ADD2 {} ,
(AND2 a2,a4),
(AND2 a2,a3),
(AND2 a1,a4),
{} ;
correctness
coherence
ADD2 {} ,(AND2 c2,c4),(AND2 c2,c3),(AND2 c1,c4),{} is set ;
;
func MULT213 c2,
c4,
c1,
c3 -> set equals :: GATE_5:def 4
CARR2 {} ,
(AND2 a2,a4),
(AND2 a2,a3),
(AND2 a1,a4),
{} ;
correctness
coherence
CARR2 {} ,(AND2 c2,c4),(AND2 c2,c3),(AND2 c1,c4),{} is set ;
;
end;
:: deftheorem Def1 defines MULT210 GATE_5:def 1 :
:: deftheorem Def2 defines MULT211 GATE_5:def 2 :
for
b1,
b2,
b3,
b4 being
set holds
MULT211 b2,
b4,
b1,
b3 = ADD1 (AND2 b2,b3),
(AND2 b1,b4),
{} ;
:: deftheorem Def3 defines MULT212 GATE_5:def 3 :
for
b1,
b2,
b3,
b4 being
set holds
MULT212 b2,
b4,
b1,
b3 = ADD2 {} ,
(AND2 b2,b4),
(AND2 b2,b3),
(AND2 b1,b4),
{} ;
:: deftheorem Def4 defines MULT213 GATE_5:def 4 :
for
b1,
b2,
b3,
b4 being
set holds
MULT213 b2,
b4,
b1,
b3 = CARR2 {} ,
(AND2 b2,b4),
(AND2 b2,b3),
(AND2 b1,b4),
{} ;
theorem Th1: :: GATE_5:1
for
b1,
b2,
b3,
b4,
b5,
b6,
b7,
b8,
b9,
b10,
b11,
b12,
b13 being
set holds
not ( (
$ b9 implies
$ AND2 b1,
b3 ) & (
$ AND2 b1,
b3 implies
$ b9 ) & (
$ b10 implies
$ XOR3 (AND2 b2,b3),
(AND2 b1,b4),
{} ) & (
$ XOR3 (AND2 b2,b3),
(AND2 b1,b4),
{} implies
$ b10 ) & (
$ b11 implies
$ MAJ3 (AND2 b2,b3),
(AND2 b1,b4),
{} ) & (
$ MAJ3 (AND2 b2,b3),
(AND2 b1,b4),
{} implies
$ b11 ) & (
$ b12 implies
$ XOR3 (AND2 b2,b4),
{} ,
b11 ) & (
$ XOR3 (AND2 b2,b4),
{} ,
b11 implies
$ b12 ) & (
$ b13 implies
$ MAJ3 (AND2 b2,b4),
{} ,
b11 ) & (
$ MAJ3 (AND2 b2,b4),
{} ,
b11 implies
$ b13 ) & (
$ b5 implies
$ b9 ) & (
$ b9 implies
$ b5 ) & (
$ b6 implies
$ b10 ) & (
$ b10 implies
$ b6 ) & (
$ b7 implies
$ b12 ) & (
$ b12 implies
$ b7 ) & (
$ b8 implies
$ b13 ) & (
$ b13 implies
$ b8 ) & not ( (
$ b5 implies
$ MULT210 b2,
b4,
b1,
b3 ) & (
$ MULT210 b2,
b4,
b1,
b3 implies
$ b5 ) & (
$ b6 implies
$ MULT211 b2,
b4,
b1,
b3 ) & (
$ MULT211 b2,
b4,
b1,
b3 implies
$ b6 ) & (
$ b7 implies
$ MULT212 b2,
b4,
b1,
b3 ) & (
$ MULT212 b2,
b4,
b1,
b3 implies
$ b7 ) & (
$ b8 implies
$ MULT213 b2,
b4,
b1,
b3 ) & (
$ MULT213 b2,
b4,
b1,
b3 implies
$ b8 ) ) )
definition
let c1,
c2,
c3,
c4,
c5 be
set ;
func MULT310 c3,
c2,
c5,
c1,
c4 -> set equals :: GATE_5:def 5
AND2 a1,
a4;
correctness
coherence
AND2 c1,c4 is set ;
;
func MULT311 c3,
c2,
c5,
c1,
c4 -> set equals :: GATE_5:def 6
ADD1 (AND2 a2,a4),
(AND2 a1,a5),
{} ;
correctness
coherence
ADD1 (AND2 c2,c4),(AND2 c1,c5),{} is set ;
;
func MULT312 c3,
c2,
c5,
c1,
c4 -> set equals :: GATE_5:def 7
ADD2 (AND2 a3,a4),
(AND2 a2,a5),
(AND2 a2,a4),
(AND2 a1,a5),
{} ;
correctness
coherence
ADD2 (AND2 c3,c4),(AND2 c2,c5),(AND2 c2,c4),(AND2 c1,c5),{} is set ;
;
func MULT313 c3,
c2,
c5,
c1,
c4 -> set equals :: GATE_5:def 8
ADD3 {} ,
(AND2 a3,a5),
(AND2 a3,a4),
(AND2 a2,a5),
(AND2 a2,a4),
(AND2 a1,a5),
{} ;
correctness
coherence
ADD3 {} ,(AND2 c3,c5),(AND2 c3,c4),(AND2 c2,c5),(AND2 c2,c4),(AND2 c1,c5),{} is set ;
;
func MULT314 c3,
c2,
c5,
c1,
c4 -> set equals :: GATE_5:def 9
CARR3 {} ,
(AND2 a3,a5),
(AND2 a3,a4),
(AND2 a2,a5),
(AND2 a2,a4),
(AND2 a1,a5),
{} ;
correctness
coherence
CARR3 {} ,(AND2 c3,c5),(AND2 c3,c4),(AND2 c2,c5),(AND2 c2,c4),(AND2 c1,c5),{} is set ;
;
end;
:: deftheorem Def5 defines MULT310 GATE_5:def 5 :
for
b1,
b2,
b3,
b4,
b5 being
set holds
MULT310 b3,
b2,
b5,
b1,
b4 = AND2 b1,
b4;
:: deftheorem Def6 defines MULT311 GATE_5:def 6 :
for
b1,
b2,
b3,
b4,
b5 being
set holds
MULT311 b3,
b2,
b5,
b1,
b4 = ADD1 (AND2 b2,b4),
(AND2 b1,b5),
{} ;
:: deftheorem Def7 defines MULT312 GATE_5:def 7 :
for
b1,
b2,
b3,
b4,
b5 being
set holds
MULT312 b3,
b2,
b5,
b1,
b4 = ADD2 (AND2 b3,b4),
(AND2 b2,b5),
(AND2 b2,b4),
(AND2 b1,b5),
{} ;
:: deftheorem Def8 defines MULT313 GATE_5:def 8 :
for
b1,
b2,
b3,
b4,
b5 being
set holds
MULT313 b3,
b2,
b5,
b1,
b4 = ADD3 {} ,
(AND2 b3,b5),
(AND2 b3,b4),
(AND2 b2,b5),
(AND2 b2,b4),
(AND2 b1,b5),
{} ;
:: deftheorem Def9 defines MULT314 GATE_5:def 9 :
for
b1,
b2,
b3,
b4,
b5 being
set holds
MULT314 b3,
b2,
b5,
b1,
b4 = CARR3 {} ,
(AND2 b3,b5),
(AND2 b3,b4),
(AND2 b2,b5),
(AND2 b2,b4),
(AND2 b1,b5),
{} ;
definition
let c1,
c2,
c3,
c4,
c5,
c6 be
set ;
func MULT321 c3,
c6,
c2,
c5,
c1,
c4 -> set equals :: GATE_5:def 10
ADD1 (MULT312 a3,a2,a5,a1,a4),
(AND2 a1,a6),
{} ;
correctness
coherence
ADD1 (MULT312 c3,c2,c5,c1,c4),(AND2 c1,c6),{} is set ;
;
func MULT322 c3,
c6,
c2,
c5,
c1,
c4 -> set equals :: GATE_5:def 11
ADD2 (MULT313 a3,a2,a5,a1,a4),
(AND2 a2,a6),
(MULT312 a3,a2,a5,a1,a4),
(AND2 a1,a6),
{} ;
correctness
coherence
ADD2 (MULT313 c3,c2,c5,c1,c4),(AND2 c2,c6),(MULT312 c3,c2,c5,c1,c4),(AND2 c1,c6),{} is set ;
;
func MULT323 c3,
c6,
c2,
c5,
c1,
c4 -> set equals :: GATE_5:def 12
ADD3 (MULT314 a3,a2,a5,a1,a4),
(AND2 a3,a6),
(MULT313 a3,a2,a5,a1,a4),
(AND2 a2,a6),
(MULT312 a3,a2,a5,a1,a4),
(AND2 a1,a6),
{} ;
correctness
coherence
ADD3 (MULT314 c3,c2,c5,c1,c4),(AND2 c3,c6),(MULT313 c3,c2,c5,c1,c4),(AND2 c2,c6),(MULT312 c3,c2,c5,c1,c4),(AND2 c1,c6),{} is set ;
;
func MULT324 c3,
c6,
c2,
c5,
c1,
c4 -> set equals :: GATE_5:def 13
CARR3 (MULT314 a3,a2,a5,a1,a4),
(AND2 a3,a6),
(MULT313 a3,a2,a5,a1,a4),
(AND2 a2,a6),
(MULT312 a3,a2,a5,a1,a4),
(AND2 a1,a6),
{} ;
correctness
coherence
CARR3 (MULT314 c3,c2,c5,c1,c4),(AND2 c3,c6),(MULT313 c3,c2,c5,c1,c4),(AND2 c2,c6),(MULT312 c3,c2,c5,c1,c4),(AND2 c1,c6),{} is set ;
;
end;
:: deftheorem Def10 defines MULT321 GATE_5:def 10 :
for
b1,
b2,
b3,
b4,
b5,
b6 being
set holds
MULT321 b3,
b6,
b2,
b5,
b1,
b4 = ADD1 (MULT312 b3,b2,b5,b1,b4),
(AND2 b1,b6),
{} ;
:: deftheorem Def11 defines MULT322 GATE_5:def 11 :
for
b1,
b2,
b3,
b4,
b5,
b6 being
set holds
MULT322 b3,
b6,
b2,
b5,
b1,
b4 = ADD2 (MULT313 b3,b2,b5,b1,b4),
(AND2 b2,b6),
(MULT312 b3,b2,b5,b1,b4),
(AND2 b1,b6),
{} ;
:: deftheorem Def12 defines MULT323 GATE_5:def 12 :
for
b1,
b2,
b3,
b4,
b5,
b6 being
set holds
MULT323 b3,
b6,
b2,
b5,
b1,
b4 = ADD3 (MULT314 b3,b2,b5,b1,b4),
(AND2 b3,b6),
(MULT313 b3,b2,b5,b1,b4),
(AND2 b2,b6),
(MULT312 b3,b2,b5,b1,b4),
(AND2 b1,b6),
{} ;
:: deftheorem Def13 defines MULT324 GATE_5:def 13 :
for
b1,
b2,
b3,
b4,
b5,
b6 being
set holds
MULT324 b3,
b6,
b2,
b5,
b1,
b4 = CARR3 (MULT314 b3,b2,b5,b1,b4),
(AND2 b3,b6),
(MULT313 b3,b2,b5,b1,b4),
(AND2 b2,b6),
(MULT312 b3,b2,b5,b1,b4),
(AND2 b1,b6),
{} ;
theorem Th2: :: GATE_5:2
for
b1,
b2,
b3,
b4,
b5,
b6,
b7,
b8,
b9,
b10,
b11,
b12,
b13,
b14,
b15,
b16,
b17,
b18,
b19,
b20,
b21,
b22,
b23,
b24,
b25 being
set holds
not ( (
$ b13 implies
$ AND2 b1,
b4 ) & (
$ AND2 b1,
b4 implies
$ b13 ) & (
$ b14 implies
$ XOR3 (AND2 b2,b4),
(AND2 b1,b5),
{} ) & (
$ XOR3 (AND2 b2,b4),
(AND2 b1,b5),
{} implies
$ b14 ) & (
$ b16 implies
$ MAJ3 (AND2 b2,b4),
(AND2 b1,b5),
{} ) & (
$ MAJ3 (AND2 b2,b4),
(AND2 b1,b5),
{} implies
$ b16 ) & (
$ b15 implies
$ XOR3 (AND2 b3,b4),
(AND2 b2,b5),
{} ) & (
$ XOR3 (AND2 b3,b4),
(AND2 b2,b5),
{} implies
$ b15 ) & (
$ b17 implies
$ MAJ3 (AND2 b3,b4),
(AND2 b2,b5),
{} ) & (
$ MAJ3 (AND2 b3,b4),
(AND2 b2,b5),
{} implies
$ b17 ) & (
$ b18 implies
$ XOR3 b15,
(AND2 b1,b6),
b16 ) & (
$ XOR3 b15,
(AND2 b1,b6),
b16 implies
$ b18 ) & (
$ b20 implies
$ MAJ3 b15,
(AND2 b1,b6),
b16 ) & (
$ MAJ3 b15,
(AND2 b1,b6),
b16 implies
$ b20 ) & (
$ b19 implies
$ XOR3 (AND2 b3,b5),
(AND2 b2,b6),
b17 ) & (
$ XOR3 (AND2 b3,b5),
(AND2 b2,b6),
b17 implies
$ b19 ) & (
$ b21 implies
$ MAJ3 (AND2 b3,b5),
(AND2 b2,b6),
b17 ) & (
$ MAJ3 (AND2 b3,b5),
(AND2 b2,b6),
b17 implies
$ b21 ) & (
$ b22 implies
$ XOR3 b19,
{} ,
b20 ) & (
$ XOR3 b19,
{} ,
b20 implies
$ b22 ) & (
$ b24 implies
$ MAJ3 b19,
{} ,
b20 ) & (
$ MAJ3 b19,
{} ,
b20 implies
$ b24 ) & (
$ b23 implies
$ XOR3 (AND2 b3,b6),
b24,
b21 ) & (
$ XOR3 (AND2 b3,b6),
b24,
b21 implies
$ b23 ) & (
$ b25 implies
$ MAJ3 (AND2 b3,b6),
b24,
b21 ) & (
$ MAJ3 (AND2 b3,b6),
b24,
b21 implies
$ b25 ) & (
$ b7 implies
$ b13 ) & (
$ b13 implies
$ b7 ) & (
$ b8 implies
$ b14 ) & (
$ b14 implies
$ b8 ) & (
$ b9 implies
$ b18 ) & (
$ b18 implies
$ b9 ) & (
$ b10 implies
$ b22 ) & (
$ b22 implies
$ b10 ) & (
$ b11 implies
$ b23 ) & (
$ b23 implies
$ b11 ) & (
$ b12 implies
$ b25 ) & (
$ b25 implies
$ b12 ) & not ( (
$ b7 implies
$ MULT310 b3,
b2,
b5,
b1,
b4 ) & (
$ MULT310 b3,
b2,
b5,
b1,
b4 implies
$ b7 ) & (
$ b8 implies
$ MULT311 b3,
b2,
b5,
b1,
b4 ) & (
$ MULT311 b3,
b2,
b5,
b1,
b4 implies
$ b8 ) & (
$ b9 implies
$ MULT321 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT321 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b9 ) & (
$ b10 implies
$ MULT322 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT322 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b10 ) & (
$ b11 implies
$ MULT323 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT323 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b11 ) & (
$ b12 implies
$ MULT324 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT324 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b12 ) ) )
theorem Th3: :: GATE_5:3
for
b1,
b2,
b3,
b4,
b5,
b6,
b7,
b8,
b9,
b10,
b11,
b12,
b13,
b14,
b15,
b16,
b17,
b18,
b19,
b20,
b21,
b22,
b23,
b24,
b25 being
set holds
not ( (
$ b13 implies
$ AND2 b1,
b4 ) & (
$ AND2 b1,
b4 implies
$ b13 ) & (
$ b14 implies
$ XOR3 (AND2 b2,b4),
(AND2 b1,b5),
{} ) & (
$ XOR3 (AND2 b2,b4),
(AND2 b1,b5),
{} implies
$ b14 ) & (
$ b17 implies
$ MAJ3 (AND2 b2,b4),
(AND2 b1,b5),
{} ) & (
$ MAJ3 (AND2 b2,b4),
(AND2 b1,b5),
{} implies
$ b17 ) & (
$ b15 implies
$ XOR3 (AND2 b3,b4),
(AND2 b2,b5),
(AND2 b1,b6) ) & (
$ XOR3 (AND2 b3,b4),
(AND2 b2,b5),
(AND2 b1,b6) implies
$ b15 ) & (
$ b18 implies
$ MAJ3 (AND2 b3,b4),
(AND2 b2,b5),
(AND2 b1,b6) ) & (
$ MAJ3 (AND2 b3,b4),
(AND2 b2,b5),
(AND2 b1,b6) implies
$ b18 ) & (
$ b16 implies
$ XOR3 (AND2 b3,b5),
(AND2 b2,b6),
{} ) & (
$ XOR3 (AND2 b3,b5),
(AND2 b2,b6),
{} implies
$ b16 ) & (
$ b19 implies
$ MAJ3 (AND2 b3,b5),
(AND2 b2,b6),
{} ) & (
$ MAJ3 (AND2 b3,b5),
(AND2 b2,b6),
{} implies
$ b19 ) & (
$ b20 implies
$ XOR3 b15,
b17,
{} ) & (
$ XOR3 b15,
b17,
{} implies
$ b20 ) & (
$ b23 implies
$ MAJ3 b15,
b17,
{} ) & (
$ MAJ3 b15,
b17,
{} implies
$ b23 ) & (
$ b21 implies
$ XOR3 b16,
b18,
b23 ) & (
$ XOR3 b16,
b18,
b23 implies
$ b21 ) & (
$ b24 implies
$ MAJ3 b16,
b18,
b23 ) & (
$ MAJ3 b16,
b18,
b23 implies
$ b24 ) & (
$ b22 implies
$ XOR3 (AND2 b3,b6),
b19,
b24 ) & (
$ XOR3 (AND2 b3,b6),
b19,
b24 implies
$ b22 ) & (
$ b25 implies
$ MAJ3 (AND2 b3,b6),
b19,
b24 ) & (
$ MAJ3 (AND2 b3,b6),
b19,
b24 implies
$ b25 ) & (
$ b7 implies
$ b13 ) & (
$ b13 implies
$ b7 ) & (
$ b8 implies
$ b14 ) & (
$ b14 implies
$ b8 ) & (
$ b9 implies
$ b20 ) & (
$ b20 implies
$ b9 ) & (
$ b10 implies
$ b21 ) & (
$ b21 implies
$ b10 ) & (
$ b11 implies
$ b22 ) & (
$ b22 implies
$ b11 ) & (
$ b12 implies
$ b25 ) & (
$ b25 implies
$ b12 ) & not ( (
$ b7 implies
$ MULT310 b3,
b2,
b5,
b1,
b4 ) & (
$ MULT310 b3,
b2,
b5,
b1,
b4 implies
$ b7 ) & (
$ b8 implies
$ MULT311 b3,
b2,
b5,
b1,
b4 ) & (
$ MULT311 b3,
b2,
b5,
b1,
b4 implies
$ b8 ) & (
$ b9 implies
$ MULT321 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT321 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b9 ) & (
$ b10 implies
$ MULT322 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT322 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b10 ) & (
$ b11 implies
$ MULT323 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT323 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b11 ) & (
$ b12 implies
$ MULT324 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT324 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b12 ) ) )
notation
let c1,
c2,
c3 be
set ;
synonym CLAADD1 c1,
c2,
c3 for XOR3 c1,
c2,
c3;
synonym CLACARR1 c1,
c2,
c3 for MAJ3 c1,
c2,
c3;
end;
definition
let c1,
c2,
c3,
c4,
c5 be
set ;
canceled;canceled;func CLAADD2 c3,
c4,
c1,
c2,
c5 -> set equals :: GATE_5:def 16
XOR3 a3,
a4,
(MAJ3 a1,a2,a5);
correctness
coherence
XOR3 c3,c4,(MAJ3 c1,c2,c5) is set ;
;
func CLACARR2 c3,
c4,
c1,
c2,
c5 -> set equals :: GATE_5:def 17
OR2 (AND2 a3,a4),
(AND2 (OR2 a3,a4),(MAJ3 a1,a2,a5));
correctness
coherence
OR2 (AND2 c3,c4),(AND2 (OR2 c3,c4),(MAJ3 c1,c2,c5)) is set ;
;
end;
:: deftheorem Def14 GATE_5:def 14 :
canceled;
:: deftheorem Def15 GATE_5:def 15 :
canceled;
:: deftheorem Def16 defines CLAADD2 GATE_5:def 16 :
for
b1,
b2,
b3,
b4,
b5 being
set holds
CLAADD2 b3,
b4,
b1,
b2,
b5 = XOR3 b3,
b4,
(MAJ3 b1,b2,b5);
:: deftheorem Def17 defines CLACARR2 GATE_5:def 17 :
for
b1,
b2,
b3,
b4,
b5 being
set holds
CLACARR2 b3,
b4,
b1,
b2,
b5 = OR2 (AND2 b3,b4),
(AND2 (OR2 b3,b4),(MAJ3 b1,b2,b5));
definition
let c1,
c2,
c3,
c4,
c5,
c6,
c7 be
set ;
func CLAADD3 c5,
c6,
c3,
c4,
c1,
c2,
c7 -> set equals :: GATE_5:def 18
XOR3 a5,
a6,
(CLACARR2 a3,a4,a1,a2,a7);
correctness
coherence
XOR3 c5,c6,(CLACARR2 c3,c4,c1,c2,c7) is set ;
;
func CLACARR3 c5,
c6,
c3,
c4,
c1,
c2,
c7 -> set equals :: GATE_5:def 19
OR3 (AND2 a5,a6),
(AND2 (OR2 a5,a6),(AND2 a3,a4)),
(AND3 (OR2 a5,a6),(OR2 a3,a4),(MAJ3 a1,a2,a7));
correctness
coherence
OR3 (AND2 c5,c6),(AND2 (OR2 c5,c6),(AND2 c3,c4)),(AND3 (OR2 c5,c6),(OR2 c3,c4),(MAJ3 c1,c2,c7)) is set ;
;
end;
:: deftheorem Def18 defines CLAADD3 GATE_5:def 18 :
for
b1,
b2,
b3,
b4,
b5,
b6,
b7 being
set holds
CLAADD3 b5,
b6,
b3,
b4,
b1,
b2,
b7 = XOR3 b5,
b6,
(CLACARR2 b3,b4,b1,b2,b7);
:: deftheorem Def19 defines CLACARR3 GATE_5:def 19 :
for
b1,
b2,
b3,
b4,
b5,
b6,
b7 being
set holds
CLACARR3 b5,
b6,
b3,
b4,
b1,
b2,
b7 = OR3 (AND2 b5,b6),
(AND2 (OR2 b5,b6),(AND2 b3,b4)),
(AND3 (OR2 b5,b6),(OR2 b3,b4),(MAJ3 b1,b2,b7));
definition
let c1,
c2,
c3,
c4,
c5,
c6,
c7,
c8,
c9 be
set ;
func CLAADD4 c7,
c8,
c5,
c6,
c3,
c4,
c1,
c2,
c9 -> set equals :: GATE_5:def 20
XOR3 a7,
a8,
(CLACARR3 a5,a6,a3,a4,a1,a2,a9);
correctness
coherence
XOR3 c7,c8,(CLACARR3 c5,c6,c3,c4,c1,c2,c9) is set ;
;
func CLACARR4 c7,
c8,
c5,
c6,
c3,
c4,
c1,
c2,
c9 -> set equals :: GATE_5:def 21
OR4 (AND2 a7,a8),
(AND2 (OR2 a7,a8),(AND2 a5,a6)),
(AND3 (OR2 a7,a8),(OR2 a5,a6),(AND2 a3,a4)),
(AND4 (OR2 a7,a8),(OR2 a5,a6),(OR2 a3,a4),(MAJ3 a1,a2,a9));
correctness
coherence
OR4 (AND2 c7,c8),(AND2 (OR2 c7,c8),(AND2 c5,c6)),(AND3 (OR2 c7,c8),(OR2 c5,c6),(AND2 c3,c4)),(AND4 (OR2 c7,c8),(OR2 c5,c6),(OR2 c3,c4),(MAJ3 c1,c2,c9)) is set ;
;
end;
:: deftheorem Def20 defines CLAADD4 GATE_5:def 20 :
for
b1,
b2,
b3,
b4,
b5,
b6,
b7,
b8,
b9 being
set holds
CLAADD4 b7,
b8,
b5,
b6,
b3,
b4,
b1,
b2,
b9 = XOR3 b7,
b8,
(CLACARR3 b5,b6,b3,b4,b1,b2,b9);
:: deftheorem Def21 defines CLACARR4 GATE_5:def 21 :
for
b1,
b2,
b3,
b4,
b5,
b6,
b7,
b8,
b9 being
set holds
CLACARR4 b7,
b8,
b5,
b6,
b3,
b4,
b1,
b2,
b9 = OR4 (AND2 b7,b8),
(AND2 (OR2 b7,b8),(AND2 b5,b6)),
(AND3 (OR2 b7,b8),(OR2 b5,b6),(AND2 b3,b4)),
(AND4 (OR2 b7,b8),(OR2 b5,b6),(OR2 b3,b4),(MAJ3 b1,b2,b9));
theorem Th4: :: GATE_5:4
for
b1,
b2,
b3,
b4,
b5,
b6,
b7,
b8,
b9,
b10,
b11,
b12,
b13,
b14,
b15,
b16,
b17,
b18,
b19 being
set holds
not ( (
$ b13 implies
$ AND2 b1,
b4 ) & (
$ AND2 b1,
b4 implies
$ b13 ) & (
$ b14 implies
$ XOR3 (AND2 b2,b4),
(AND2 b1,b5),
{} ) & (
$ XOR3 (AND2 b2,b4),
(AND2 b1,b5),
{} implies
$ b14 ) & (
$ b17 implies
$ MAJ3 (AND2 b2,b4),
(AND2 b1,b5),
{} ) & (
$ MAJ3 (AND2 b2,b4),
(AND2 b1,b5),
{} implies
$ b17 ) & (
$ b15 implies
$ XOR3 (AND2 b3,b4),
(AND2 b2,b5),
(AND2 b1,b6) ) & (
$ XOR3 (AND2 b3,b4),
(AND2 b2,b5),
(AND2 b1,b6) implies
$ b15 ) & (
$ b18 implies
$ MAJ3 (AND2 b3,b4),
(AND2 b2,b5),
(AND2 b1,b6) ) & (
$ MAJ3 (AND2 b3,b4),
(AND2 b2,b5),
(AND2 b1,b6) implies
$ b18 ) & (
$ b16 implies
$ XOR3 (AND2 b3,b5),
(AND2 b2,b6),
{} ) & (
$ XOR3 (AND2 b3,b5),
(AND2 b2,b6),
{} implies
$ b16 ) & (
$ b19 implies
$ MAJ3 (AND2 b3,b5),
(AND2 b2,b6),
{} ) & (
$ MAJ3 (AND2 b3,b5),
(AND2 b2,b6),
{} implies
$ b19 ) & (
$ b7 implies
$ b13 ) & (
$ b13 implies
$ b7 ) & (
$ b8 implies
$ b14 ) & (
$ b14 implies
$ b8 ) & (
$ b9 implies
$ CLAADD1 b15,
b17,
{} ) & (
$ CLAADD1 b15,
b17,
{} implies
$ b9 ) & (
$ b10 implies
$ CLAADD2 b16,
b18,
b15,
b17,
{} ) & (
$ CLAADD2 b16,
b18,
b15,
b17,
{} implies
$ b10 ) & (
$ b11 implies
$ CLAADD3 (AND2 b3,b6),
b19,
b16,
b18,
b15,
b17,
{} ) & (
$ CLAADD3 (AND2 b3,b6),
b19,
b16,
b18,
b15,
b17,
{} implies
$ b11 ) & (
$ b12 implies
$ CLACARR3 (AND2 b3,b6),
b19,
b16,
b18,
b15,
b17,
{} ) & (
$ CLACARR3 (AND2 b3,b6),
b19,
b16,
b18,
b15,
b17,
{} implies
$ b12 ) & not ( (
$ b7 implies
$ MULT310 b3,
b2,
b5,
b1,
b4 ) & (
$ MULT310 b3,
b2,
b5,
b1,
b4 implies
$ b7 ) & (
$ b8 implies
$ MULT311 b3,
b2,
b5,
b1,
b4 ) & (
$ MULT311 b3,
b2,
b5,
b1,
b4 implies
$ b8 ) & (
$ b9 implies
$ MULT321 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT321 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b9 ) & (
$ b10 implies
$ MULT322 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT322 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b10 ) & (
$ b11 implies
$ MULT323 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT323 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b11 ) & (
$ b12 implies
$ MULT324 b3,
b6,
b2,
b5,
b1,
b4 ) & (
$ MULT324 b3,
b6,
b2,
b5,
b1,
b4 implies
$ b12 ) ) )