let x, y, c be set ; :: thesis: InnerVertices (BorrowStr x,y,c) = {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \/ {(BorrowOutput x,y,c)}
set xy = [<*x,y*>,and2a ];
set yc = [<*y,c*>,and2 ];
set xc = [<*x,c*>,and2a ];
set Cxy = 1GateCircStr <*x,y*>,and2a ;
set Cyc = 1GateCircStr <*y,c*>,and2 ;
set Cxc = 1GateCircStr <*x,c*>,and2a ;
set Cxyc = 1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ;
A1: 1GateCircStr <*x,y*>,and2a tolerates ((1GateCircStr <*y,c*>,and2 ) +* (1GateCircStr <*x,c*>,and2a )) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ) by CIRCCOMB:55;
A2: 1GateCircStr <*y,c*>,and2 tolerates (1GateCircStr <*x,c*>,and2a ) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ) by CIRCCOMB:55;
A3: 1GateCircStr <*x,c*>,and2a tolerates 1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 by CIRCCOMB:55;
A4: InnerVertices ((1GateCircStr <*y,c*>,and2 ) +* ((1GateCircStr <*x,c*>,and2a ) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ))) = (InnerVertices (1GateCircStr <*y,c*>,and2 )) \/ (InnerVertices ((1GateCircStr <*x,c*>,and2a ) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ))) by A2, CIRCCOMB:15;
A5: InnerVertices ((1GateCircStr <*x,c*>,and2a ) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) = (InnerVertices (1GateCircStr <*x,c*>,and2a )) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) by A3, CIRCCOMB:15;
thus InnerVertices (BorrowStr x,y,c) = InnerVertices (((1GateCircStr <*x,y*>,and2a ) +* ((1GateCircStr <*y,c*>,and2 ) +* (1GateCircStr <*x,c*>,and2a ))) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) by CIRCCOMB:10
.= InnerVertices ((1GateCircStr <*x,y*>,and2a ) +* (((1GateCircStr <*y,c*>,and2 ) +* (1GateCircStr <*x,c*>,and2a )) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ))) by CIRCCOMB:10
.= (InnerVertices (1GateCircStr <*x,y*>,and2a )) \/ (InnerVertices (((1GateCircStr <*y,c*>,and2 ) +* (1GateCircStr <*x,c*>,and2a )) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ))) by A1, CIRCCOMB:15
.= (InnerVertices (1GateCircStr <*x,y*>,and2a )) \/ (InnerVertices ((1GateCircStr <*y,c*>,and2 ) +* ((1GateCircStr <*x,c*>,and2a ) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )))) by CIRCCOMB:10
.= ((InnerVertices (1GateCircStr <*x,y*>,and2a )) \/ (InnerVertices (1GateCircStr <*y,c*>,and2 ))) \/ ((InnerVertices (1GateCircStr <*x,c*>,and2a )) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ))) by A4, A5, XBOOLE_1:4
.= (((InnerVertices (1GateCircStr <*x,y*>,and2a )) \/ (InnerVertices (1GateCircStr <*y,c*>,and2 ))) \/ (InnerVertices (1GateCircStr <*x,c*>,and2a ))) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) by XBOOLE_1:4
.= (({[<*x,y*>,and2a ]} \/ (InnerVertices (1GateCircStr <*y,c*>,and2 ))) \/ (InnerVertices (1GateCircStr <*x,c*>,and2a ))) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) by CIRCCOMB:49
.= (({[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]}) \/ (InnerVertices (1GateCircStr <*x,c*>,and2a ))) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) by CIRCCOMB:49
.= (({[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]}) \/ {[<*x,c*>,and2a ]}) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) by CIRCCOMB:49
.= ({[<*x,y*>,and2a ],[<*y,c*>,and2 ]} \/ {[<*x,c*>,and2a ]}) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) by ENUMSET1:41
.= {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) by ENUMSET1:43
.= {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \/ {(BorrowOutput x,y,c)} by CIRCCOMB:49 ; :: thesis: verum