let x, y, c be set ; ( 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]
; 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
by FINSEQ_1:44;
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
by FINSEQ_1:44;
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
by FINSEQ_1:44;
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}
; verum