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