let x, y, c be set ; 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 Cxy = 1GateCircStr (<*x,y*>,'&');
set Cyc = 1GateCircStr (<*y,c*>,'&');
set Ccx = 1GateCircStr (<*c,x*>,'&');
set Cxyc = 1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3);
A1:
1GateCircStr (<*x,y*>,'&') tolerates ((1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*c,x*>,'&'))) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))
by CIRCCOMB:47;
A2:
1GateCircStr (<*y,c*>,'&') tolerates (1GateCircStr (<*c,x*>,'&')) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))
by CIRCCOMB:47;
A3:
1GateCircStr (<*c,x*>,'&') tolerates 1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)
by CIRCCOMB:47;
A4:
InnerVertices ((1GateCircStr (<*y,c*>,'&')) +* ((1GateCircStr (<*c,x*>,'&')) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))) = (InnerVertices (1GateCircStr (<*y,c*>,'&'))) \/ (InnerVertices ((1GateCircStr (<*c,x*>,'&')) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))))
by A2, CIRCCOMB:11;
A5:
InnerVertices ((1GateCircStr (<*c,x*>,'&')) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) = (InnerVertices (1GateCircStr (<*c,x*>,'&'))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))
by A3, CIRCCOMB:11;
thus InnerVertices (MajorityStr (x,y,c)) =
InnerVertices (((1GateCircStr (<*x,y*>,'&')) +* ((1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*c,x*>,'&')))) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))
by CIRCCOMB:6
.=
InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (((1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*c,x*>,'&'))) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))))
by CIRCCOMB:6
.=
(InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices (((1GateCircStr (<*y,c*>,'&')) +* (1GateCircStr (<*c,x*>,'&'))) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))))
by A1, CIRCCOMB:11
.=
(InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices ((1GateCircStr (<*y,c*>,'&')) +* ((1GateCircStr (<*c,x*>,'&')) +* (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))))
by CIRCCOMB:6
.=
((InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices (1GateCircStr (<*y,c*>,'&')))) \/ ((InnerVertices (1GateCircStr (<*c,x*>,'&'))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))))
by A4, A5, XBOOLE_1:4
.=
(((InnerVertices (1GateCircStr (<*x,y*>,'&'))) \/ (InnerVertices (1GateCircStr (<*y,c*>,'&')))) \/ (InnerVertices (1GateCircStr (<*c,x*>,'&')))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))
by XBOOLE_1:4
.=
(({[<*x,y*>,'&']} \/ (InnerVertices (1GateCircStr (<*y,c*>,'&')))) \/ (InnerVertices (1GateCircStr (<*c,x*>,'&')))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))
by CIRCCOMB:42
.=
(({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']}) \/ (InnerVertices (1GateCircStr (<*c,x*>,'&')))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))
by CIRCCOMB:42
.=
(({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']}) \/ {[<*c,x*>,'&']}) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))
by CIRCCOMB:42
.=
({[<*x,y*>,'&'],[<*y,c*>,'&']} \/ {[<*c,x*>,'&']}) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))
by ENUMSET1:1
.=
{[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3)))
by ENUMSET1:3
.=
{[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))}
by CIRCCOMB:42
; verum