let x, y, c be set ; :: thesis: 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:55;
A2: 1GateCircStr <*y,c*>,'&' tolerates (1GateCircStr <*c,x*>,'&' ) +* (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ) by CIRCCOMB:55;
A3: 1GateCircStr <*c,x*>,'&' tolerates 1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 by CIRCCOMB:55;
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:15;
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:15;
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:10
.= InnerVertices ((1GateCircStr <*x,y*>,'&' ) +* (((1GateCircStr <*y,c*>,'&' ) +* (1GateCircStr <*c,x*>,'&' )) +* (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ))) by CIRCCOMB:10
.= (InnerVertices (1GateCircStr <*x,y*>,'&' )) \/ (InnerVertices (((1GateCircStr <*y,c*>,'&' ) +* (1GateCircStr <*c,x*>,'&' )) +* (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 ))) by A1, CIRCCOMB:15
.= (InnerVertices (1GateCircStr <*x,y*>,'&' )) \/ (InnerVertices ((1GateCircStr <*y,c*>,'&' ) +* ((1GateCircStr <*c,x*>,'&' ) +* (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 )))) by CIRCCOMB:10
.= ((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:49
.= (({[<*x,y*>,'&' ]} \/ {[<*y,c*>,'&' ]}) \/ (InnerVertices (1GateCircStr <*c,x*>,'&' ))) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 )) by CIRCCOMB:49
.= (({[<*x,y*>,'&' ]} \/ {[<*y,c*>,'&' ]}) \/ {[<*c,x*>,'&' ]}) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 )) by CIRCCOMB:49
.= ({[<*x,y*>,'&' ],[<*y,c*>,'&' ]} \/ {[<*c,x*>,'&' ]}) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 )) by ENUMSET1:41
.= {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]} \/ (InnerVertices (1GateCircStr <*[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]*>,or3 )) by ENUMSET1:43
.= {[<*x,y*>,'&' ],[<*y,c*>,'&' ],[<*c,x*>,'&' ]} \/ {(MajorityOutput x,y,c)} by CIRCCOMB:49 ; :: thesis: verum