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