let x, y, c be non pair set ; :: thesis: ( InputVertices (BorrowStr x,y,c) = {x,y,c} & InnerVertices (BorrowStr x,y,c) = {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \/ {(BorrowOutput x,y,c)} )
set xy = <*x,y*>;
set yc = <*y,c*>;
set xc = <*x,c*>;
set xy1 = [<*x,y*>,and2a ];
set yc1 = [<*y,c*>,and2 ];
set xc1 = [<*x,c*>,and2a ];
set MI = BorrowIStr x,y,c;
set S = 1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ;
set M = BorrowStr x,y,c;
A1: ( InputVertices (1GateCircStr <*x,y*>,and2a ) = {x,y} & InputVertices (1GateCircStr <*x,c*>,and2a ) = {x,c} ) by FACIRC_1:40;
A2: InputVertices (1GateCircStr <*y,c*>,and2 ) = {y,c} by FACIRC_1:40;
A3: ( InnerVertices (1GateCircStr <*x,y*>,and2a ) = {[<*x,y*>,and2a ]} & InnerVertices (1GateCircStr <*y,c*>,and2 ) = {[<*y,c*>,and2 ]} ) by CIRCCOMB:49;
A4: InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ) is Relation by FACIRC_1:38;
A5: ( not InputVertices (1GateCircStr <*x,y*>,and2a ) is with_pair & not InputVertices (1GateCircStr <*y,c*>,and2 ) is with_pair ) by FACIRC_1:41;
then A6: ( not InputVertices (1GateCircStr <*x,c*>,and2a ) is with_pair & not InputVertices ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 )) is with_pair ) by FACIRC_1:9, FACIRC_1:41;
then not InputVertices (BorrowIStr x,y,c) is with_pair by FACIRC_1:9;
then A7: InputVertices (BorrowStr x,y,c) = (InputVertices (BorrowIStr x,y,c)) \/ ((InputVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) \ (InnerVertices (BorrowIStr x,y,c))) by A4, FACIRC_1:6;
A8: InnerVertices (1GateCircStr <*x,c*>,and2a ) = {[<*x,c*>,and2a ]} by CIRCCOMB:49;
1GateCircStr <*x,y*>,and2a tolerates 1GateCircStr <*y,c*>,and2 by CIRCCOMB:55;
then A9: InnerVertices ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 )) = {[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]} by A3, CIRCCOMB:15;
(1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 ) tolerates 1GateCircStr <*x,c*>,and2a by CIRCCOMB:55;
then A10: InnerVertices (BorrowIStr x,y,c) = ({[<*x,y*>,and2a ]} \/ {[<*y,c*>,and2 ]}) \/ {[<*x,c*>,and2a ]} by A8, A9, CIRCCOMB:15
.= {[<*x,y*>,and2a ],[<*y,c*>,and2 ]} \/ {[<*x,c*>,and2a ]} by ENUMSET1:41
.= {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} by ENUMSET1:43 ;
InputVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 ) = {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} by FACIRC_1:42;
then A11: (InputVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) \ (InnerVertices (BorrowIStr x,y,c)) = {} by A10, XBOOLE_1:37;
InnerVertices ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 )) = {[<*x,y*>,and2a ],[<*y,c*>,and2 ]} by A9, ENUMSET1:41;
hence InputVertices (BorrowStr x,y,c) = (InputVertices ((1GateCircStr <*x,y*>,and2a ) +* (1GateCircStr <*y,c*>,and2 ))) \/ (InputVertices (1GateCircStr <*x,c*>,and2a )) by A6, A7, A8, A11, FACIRC_1:7
.= ((InputVertices (1GateCircStr <*x,y*>,and2a )) \/ (InputVertices (1GateCircStr <*y,c*>,and2 ))) \/ (InputVertices (1GateCircStr <*x,c*>,and2a )) by A5, A3, FACIRC_1:7
.= {x,y,y,c} \/ {c,x} by A1, A2, 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 (BorrowStr x,y,c) = {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \/ {(BorrowOutput x,y,c)}
BorrowIStr x,y,c tolerates 1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 by CIRCCOMB:55;
hence InnerVertices (BorrowStr x,y,c) = (InnerVertices (BorrowIStr x,y,c)) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]*>,or3 )) by CIRCCOMB:15
.= {[<*x,y*>,and2a ],[<*y,c*>,and2 ],[<*x,c*>,and2a ]} \/ {(BorrowOutput x,y,c)} by A10, CIRCCOMB:49 ;
:: thesis: verum