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:42;
A4: InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]*>,or3)) is Relation by FACIRC_1:38;
A5: ( InputVertices (1GateCircStr (<*x,y*>,and2a)) is without_pairs & InputVertices (1GateCircStr (<*y,c*>,and2)) is without_pairs ) by FACIRC_1:41;
then A6: ( InputVertices (1GateCircStr (<*x,c*>,and2a)) is without_pairs & InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) is without_pairs ) by FACIRC_1:9, FACIRC_1:41;
then InputVertices (BorrowIStr (x,y,c)) is without_pairs 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:42;
1GateCircStr (<*x,y*>,and2a) tolerates 1GateCircStr (<*y,c*>,and2) by CIRCCOMB:47;
then A9: InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))) = {[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]} by A3, CIRCCOMB:11;
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)) tolerates 1GateCircStr (<*x,c*>,and2a) by CIRCCOMB:47;
then A10: InnerVertices (BorrowIStr (x,y,c)) = ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]}) \/ {[<*x,c*>,and2a]} by A8, A9, CIRCCOMB:11
.= {[<*x,y*>,and2a],[<*y,c*>,and2]} \/ {[<*x,c*>,and2a]} by ENUMSET1:1
.= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} by ENUMSET1:3 ;
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:1;
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:5
.= {y,y,x,c} \/ {c,x} by ENUMSET1:67
.= {y,x,c} \/ {c,x} by ENUMSET1:31
.= {x,y,c} \/ {c,x} by ENUMSET1:58
.= {x,y,c} \/ ({c} \/ {x}) by ENUMSET1:1
.= ({x,y,c} \/ {c}) \/ {x} by XBOOLE_1:4
.= ({c,x,y} \/ {c}) \/ {x} by ENUMSET1:59
.= {c,c,x,y} \/ {x} by ENUMSET1:4
.= {c,x,y} \/ {x} by ENUMSET1:31
.= {x,y,c} \/ {x} by ENUMSET1:59
.= {x,x,y,c} by ENUMSET1:4
.= {x,y,c} by ENUMSET1:31 ;
:: 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:47;
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:11
.= {[<*x,y*>,and2a],[<*y,c*>,and2],[<*x,c*>,and2a]} \/ {(BorrowOutput (x,y,c))} by A10, CIRCCOMB:42 ;
:: thesis: verum