let x, y, c be set ; :: thesis: ( x <> [<*y,c*>,and2] & y <> [<*x,c*>,and2a] & c <> [<*x,y*>,and2a] implies InputVertices (BorrowIStr (x,y,c)) = {x,y,c} )
assume that
A1: x <> [<*y,c*>,and2] and
A2: y <> [<*x,c*>,and2a] and
A3: c <> [<*x,y*>,and2a] ; :: thesis: InputVertices (BorrowIStr (x,y,c)) = {x,y,c}
A4: 1GateCircStr (<*x,y*>,and2a) tolerates 1GateCircStr (<*y,c*>,and2) by CIRCCOMB:47;
A5: y in {1,y} by TARSKI:def 2;
A6: y in {2,y} by TARSKI:def 2;
A7: {1,y} in {{1},{1,y}} by TARSKI:def 2;
A8: {2,y} in {{2},{2,y}} by TARSKI:def 2;
<*y,c*> = <*y*> ^ <*c*> by FINSEQ_1:def 9;
then A9: <*y*> c= <*y,c*> by FINSEQ_6:10;
<*y*> = {[1,y]} by FINSEQ_1:def 5;
then A10: [1,y] in <*y*> by TARSKI:def 1;
A11: <*y,c*> in {<*y,c*>} by TARSKI:def 1;
A12: {<*y,c*>} in {{<*y,c*>},{<*y,c*>,and2}} by TARSKI:def 2;
then A13: y <> [<*y,c*>,and2] by A5, A7, A9, A10, A11, XREGULAR:9;
A14: c in {2,c} by TARSKI:def 2;
A15: {2,c} in {{2},{2,c}} by TARSKI:def 2;
dom <*y,c*> = Seg 2 by FINSEQ_1:89;
then A16: 2 in dom <*y,c*> by FINSEQ_1:1;
<*y,c*> . 2 = c ;
then [2,c] in <*y,c*> by A16, FUNCT_1:1;
then A17: c <> [<*y,c*>,and2] by A11, A12, A14, A15, XREGULAR:9;
dom <*x,y*> = Seg 2 by FINSEQ_1:89;
then A18: 2 in dom <*x,y*> by FINSEQ_1:1;
<*x,y*> . 2 = y ;
then A19: [2,y] in <*x,y*> by A18, FUNCT_1:1;
A20: <*x,y*> in {<*x,y*>} by TARSKI:def 1;
{<*x,y*>} in {{<*x,y*>},{<*x,y*>,and2a}} by TARSKI:def 2;
then y <> [<*x,y*>,and2a] by A6, A8, A19, A20, XREGULAR:9;
then A21: not [<*x,y*>,and2a] in {y,c} by A3, TARSKI:def 2;
A22: x in {1,x} by TARSKI:def 2;
A23: {1,x} in {{1},{1,x}} by TARSKI:def 2;
<*x,y*> = <*x*> ^ <*y*> by FINSEQ_1:def 9;
then A24: <*x*> c= <*x,y*> by FINSEQ_6:10;
<*x*> = {[1,x]} by FINSEQ_1:def 5;
then A25: [1,x] in <*x*> by TARSKI:def 1;
A26: <*x,y*> in {<*x,y*>} by TARSKI:def 1;
{<*x,y*>} in {{<*x,y*>},{<*x,y*>,and2a}} by TARSKI:def 2;
then A27: x <> [<*x,y*>,and2a] by A22, A23, A24, A25, A26, XREGULAR:9;
A28: not c in {[<*x,y*>,and2a],[<*y,c*>,and2]} by A3, A17, TARSKI:def 2;
A29: not x in {[<*x,y*>,and2a],[<*y,c*>,and2]} by A1, A27, TARSKI:def 2;
A30: c in {2,c} by TARSKI:def 2;
A31: {2,c} in {{2},{2,c}} by TARSKI:def 2;
dom <*x,c*> = Seg 2 by FINSEQ_1:89;
then A32: 2 in dom <*x,c*> by FINSEQ_1:1;
<*x,c*> . 2 = c ;
then A33: [2,c] in <*x,c*> by A32, FUNCT_1:1;
A34: <*x,c*> in {<*x,c*>} by TARSKI:def 1;
{<*x,c*>} in {{<*x,c*>},{<*x,c*>,and2a}} by TARSKI:def 2;
then A35: c <> [<*x,c*>,and2a] by A30, A31, A33, A34, XREGULAR:9;
A36: x in {1,x} by TARSKI:def 2;
A37: {1,x} in {{1},{1,x}} by TARSKI:def 2;
<*x,c*> = <*x*> ^ <*c*> by FINSEQ_1:def 9;
then A38: <*x*> c= <*x,c*> by FINSEQ_6:10;
<*x*> = {[1,x]} by FINSEQ_1:def 5;
then A39: [1,x] in <*x*> by TARSKI:def 1;
A40: <*x,c*> in {<*x,c*>} by TARSKI:def 1;
{<*x,c*>} in {{<*x,c*>},{<*x,c*>,and2a}} by TARSKI:def 2;
then x <> [<*x,c*>,and2a] by A36, A37, A38, A39, A40, XREGULAR:9;
then A41: not [<*x,c*>,and2a] in {x,y,c} by A2, A35, ENUMSET1:def 1;
InputVertices (BorrowIStr (x,y,c)) = ((InputVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2)))) \ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ (InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))) by CIRCCMB2:5, CIRCCOMB:47
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ (InnerVertices (1GateCircStr (<*y,c*>,and2)))) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2a))))) \ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ (InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,c*>,and2))))) by CIRCCMB2:5, CIRCCOMB:47
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ (InnerVertices (1GateCircStr (<*y,c*>,and2)))) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2a))))) \ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2))))) by A4, CIRCCOMB:11
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ (InnerVertices (1GateCircStr (<*x,y*>,and2a))))) \ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ {[<*x,y*>,and2a]})) \ (InnerVertices (1GateCircStr (<*x,c*>,and2a)))) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,c*>,and2))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ({[<*x,y*>,and2a]} \/ (InnerVertices (1GateCircStr (<*y,c*>,and2))))) by CIRCCOMB:42
.= ((((InputVertices (1GateCircStr (<*x,y*>,and2a))) \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by CIRCCOMB:42
.= ((({x,y} \ {[<*y,c*>,and2]}) \/ ((InputVertices (1GateCircStr (<*y,c*>,and2))) \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,and2]}) \/ ({y,c} \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ((InputVertices (1GateCircStr (<*x,c*>,and2a))) \ ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,and2]}) \/ ({y,c} \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ({x,c} \ ({[<*x,y*>,and2a]} \/ {[<*y,c*>,and2]})) by FACIRC_1:40
.= ((({x,y} \ {[<*y,c*>,and2]}) \/ ({y,c} \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ({x,c} \ {[<*x,y*>,and2a],[<*y,c*>,and2]}) by ENUMSET1:1
.= (({x,y} \/ ({y,c} \ {[<*x,y*>,and2a]})) \ {[<*x,c*>,and2a]}) \/ ({x,c} \ {[<*x,y*>,and2a],[<*y,c*>,and2]}) by A1, A13, FACIRC_2:1
.= (({x,y} \/ {y,c}) \ {[<*x,c*>,and2a]}) \/ ({x,c} \ {[<*x,y*>,and2a],[<*y,c*>,and2]}) by A21, ZFMISC_1:57
.= (({x,y} \/ {y,c}) \ {[<*x,c*>,and2a]}) \/ {x,c} by A28, A29, ZFMISC_1:63
.= ({x,y,y,c} \ {[<*x,c*>,and2a]}) \/ {x,c} by ENUMSET1:5
.= ({y,y,x,c} \ {[<*x,c*>,and2a]}) \/ {x,c} by ENUMSET1:67
.= ({y,x,c} \ {[<*x,c*>,and2a]}) \/ {x,c} by ENUMSET1:31
.= ({x,y,c} \ {[<*x,c*>,and2a]}) \/ {x,c} by ENUMSET1:58
.= {x,y,c} \/ {x,c} by A41, ZFMISC_1:57
.= {x,y,c,c,x} by ENUMSET1:9
.= {x,y,c,c} \/ {x} by ENUMSET1:10
.= {c,c,x,y} \/ {x} by ENUMSET1:73
.= {c,x,y} \/ {x} by ENUMSET1:31
.= {c,x,y,x} by ENUMSET1:6
.= {x,x,y,c} by ENUMSET1:70
.= {x,y,c} by ENUMSET1:31 ;
hence InputVertices (BorrowIStr (x,y,c)) = {x,y,c} ; :: thesis: verum