let x, y, c be non pair object ; ( InputVertices (MajorityStr (x,y,c)) = {x,y,c} & InnerVertices (MajorityStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))} )
set xy = [<*x,y*>,'&'];
set yc = [<*y,c*>,'&'];
set cx = [<*c,x*>,'&'];
set MI = MajorityIStr (x,y,c);
set S = 1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3);
set M = MajorityStr (x,y,c);
A1:
1GateCircStr (<*x,y*>,'&') tolerates 1GateCircStr (<*y,c*>,'&')
by CIRCCOMB:43;
A2:
InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) is Relation
by Th38;
A3:
InputVertices (1GateCircStr (<*y,c*>,'&')) = {y,c}
by Th40;
A4:
( InnerVertices (1GateCircStr (<*x,y*>,'&')) = {[<*x,y*>,'&']} & InnerVertices (1GateCircStr (<*y,c*>,'&')) = {[<*y,c*>,'&']} )
by CIRCCOMB:42;
then A5:
( InnerVertices (1GateCircStr (<*c,x*>,'&')) = {[<*c,x*>,'&']} & InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) = {[<*x,y*>,'&']} \/ {[<*y,c*>,'&']} )
by A1, CIRCCOMB:11, CIRCCOMB:42;
( 1GateCircStr (<*x,y*>,'&') tolerates 1GateCircStr (<*c,x*>,'&') & 1GateCircStr (<*y,c*>,'&') tolerates 1GateCircStr (<*c,x*>,'&') )
by CIRCCOMB:43;
then
(1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&')) tolerates 1GateCircStr (<*c,x*>,'&')
by A1, CIRCCOMB:3;
then A6: InnerVertices (MajorityIStr (x,y,c)) =
({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']}) \/ {[<*c,x*>,'&']}
by A5, CIRCCOMB:11
.=
{[<*x,y*>,'&'],[<*y,c*>,'&']} \/ {[<*c,x*>,'&']}
by ENUMSET1:1
.=
{[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}
by ENUMSET1:3
;
InputVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']}
by Th42;
then A7:
(InputVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) \ (InnerVertices (MajorityIStr (x,y,c))) = {}
by A6, XBOOLE_1:37;
A8:
( InputVertices (1GateCircStr (<*x,y*>,'&')) = {x,y} & InputVertices (1GateCircStr (<*c,x*>,'&')) = {c,x} )
by Th40;
A9:
InputVertices (1GateCircStr (<*c,x*>,'&')) is without_pairs
by Th41;
A10:
( InputVertices (1GateCircStr (<*x,y*>,'&')) is without_pairs & InputVertices (1GateCircStr (<*y,c*>,'&')) is without_pairs )
by Th41;
then A11:
InputVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) is without_pairs
by Th8, CIRCCOMB:47;
then
InputVertices (MajorityIStr (x,y,c)) is without_pairs
by A9, Th8, CIRCCOMB:47;
then
InputVertices (MajorityStr (x,y,c)) = (InputVertices (MajorityIStr (x,y,c))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) \ (InnerVertices (MajorityIStr (x,y,c))))
by A2, Th6;
hence InputVertices (MajorityStr (x,y,c)) =
(InputVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&')))) \/ (InputVertices (1GateCircStr (<*c,x*>,'&')))
by A9, A11, A5, A7, Th7
.=
((InputVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InputVertices (1GateCircStr (<*y,c*>,'&')))) \/ (InputVertices (1GateCircStr (<*c,x*>,'&')))
by A10, A4, Th7
.=
{x,y,y,c} \/ {c,x}
by A8, A3, ENUMSET1:5
.=
{y,y,x,c} \/ {c,x}
by ENUMSET1:67
.=
{y,x,c} \/ {c,x}
by ENUMSET1:31
.=
{x,y,c} \/ {c,x}
by ENUMSET1:58
.=
{x,y,c} \/ ({c} \/ {x})
by ENUMSET1:1
.=
({x,y,c} \/ {c}) \/ {x}
by XBOOLE_1:4
.=
({c,x,y} \/ {c}) \/ {x}
by ENUMSET1:59
.=
{c,c,x,y} \/ {x}
by ENUMSET1:4
.=
{c,x,y} \/ {x}
by ENUMSET1:31
.=
{x,y,c} \/ {x}
by ENUMSET1:59
.=
{x,x,y,c}
by ENUMSET1:4
.=
{x,y,c}
by ENUMSET1:31
;
InnerVertices (MajorityStr (x,y,c)) = {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))}
MajorityIStr (x,y,c) tolerates 1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)
by CIRCCOMB:47;
hence InnerVertices (MajorityStr (x,y,c)) =
(InnerVertices (MajorityIStr (x,y,c))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))
by CIRCCOMB:11
.=
{[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))}
by A6, CIRCCOMB:42
;
verum