let x, y, c be non pair set ; :: 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:51;
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:49;
then A5: ( InnerVertices (1GateCircStr (<*c,x*>,'&')) = {[<*c,x*>,'&']} & InnerVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) = {[<*x,y*>,'&']} \/ {[<*y,c*>,'&']} ) by A1, CIRCCOMB:15, CIRCCOMB:49;
( 1GateCircStr (<*x,y*>,'&') tolerates 1GateCircStr (<*c,x*>,'&') & 1GateCircStr (<*y,c*>,'&') tolerates 1GateCircStr (<*c,x*>,'&') ) by CIRCCOMB:51;
then (1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&')) tolerates 1GateCircStr (<*c,x*>,'&') by A1, CIRCCOMB:7;
then A6: InnerVertices (MajorityIStr (x,y,c)) = ({[<*x,y*>,'&']} \/ {[<*y,c*>,'&']}) \/ {[<*c,x*>,'&']} by A5, CIRCCOMB:15
.= {[<*x,y*>,'&'],[<*y,c*>,'&']} \/ {[<*c,x*>,'&']} by ENUMSET1:41
.= {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} by ENUMSET1:43 ;
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: not InputVertices (1GateCircStr (<*c,x*>,'&')) is with_pair by Th41;
A10: ( not InputVertices (1GateCircStr (<*x,y*>,'&')) is with_pair & not InputVertices (1GateCircStr (<*y,c*>,'&')) is with_pair ) by Th41;
then A11: not InputVertices ((1GateCircStr (<*x,y*>,'&')) +* (1GateCircStr (<*y,c*>,'&'))) is with_pair by Th8, CIRCCOMB:55;
then not InputVertices (MajorityIStr (x,y,c)) is with_pair by A9, Th8, CIRCCOMB:55;
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:45
.= {y,y,x,c} \/ {c,x} by ENUMSET1:110
.= {y,x,c} \/ {c,x} by ENUMSET1:71
.= {x,y,c} \/ {c,x} by ENUMSET1:99
.= {x,y,c} \/ ({c} \/ {x}) by ENUMSET1:41
.= ({x,y,c} \/ {c}) \/ {x} by XBOOLE_1:4
.= ({c,x,y} \/ {c}) \/ {x} by ENUMSET1:100
.= {c,c,x,y} \/ {x} by ENUMSET1:44
.= {c,x,y} \/ {x} by ENUMSET1:71
.= {x,y,c} \/ {x} by ENUMSET1:100
.= {x,x,y,c} by ENUMSET1:44
.= {x,y,c} by ENUMSET1:71 ;
:: 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:55;
hence InnerVertices (MajorityStr (x,y,c)) = (InnerVertices (MajorityIStr (x,y,c))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']*>,or3))) by CIRCCOMB:15
.= {[<*x,y*>,'&'],[<*y,c*>,'&'],[<*c,x*>,'&']} \/ {(MajorityOutput (x,y,c))} by A6, CIRCCOMB:49 ;
:: thesis: verum