let x, y, c be non pair object ; :: thesis: ( 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 ;
:: thesis: 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 ;
:: thesis: verum