let x, y, c be set ; 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
; verum