let x, y, z be set ; InnerVertices (GFA1CarryStr (x,y,z)) = {[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]} \/ {(GFA1CarryOutput (x,y,z))}
set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set f4 = or3 ;
set xy = [<*x,y*>,and2c];
set yz = [<*y,z*>,and2a];
set zx = [<*z,x*>,and2];
set Cxy = 1GateCircStr (<*x,y*>,and2c);
set Cyz = 1GateCircStr (<*y,z*>,and2a);
set Czx = 1GateCircStr (<*z,x*>,and2);
set Cxyz = 1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3);
A1:
1GateCircStr (<*x,y*>,and2c) tolerates ((1GateCircStr (<*y,z*>,and2a)) +* (1GateCircStr (<*z,x*>,and2))) +* (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3))
by CIRCCOMB:47;
1GateCircStr (<*y,z*>,and2a) tolerates (1GateCircStr (<*z,x*>,and2)) +* (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3))
by CIRCCOMB:47;
then A2:
InnerVertices ((1GateCircStr (<*y,z*>,and2a)) +* ((1GateCircStr (<*z,x*>,and2)) +* (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)))) = (InnerVertices (1GateCircStr (<*y,z*>,and2a))) \/ (InnerVertices ((1GateCircStr (<*z,x*>,and2)) +* (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3))))
by CIRCCOMB:11;
1GateCircStr (<*z,x*>,and2) tolerates 1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)
by CIRCCOMB:47;
then A3:
InnerVertices ((1GateCircStr (<*z,x*>,and2)) +* (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3))) = (InnerVertices (1GateCircStr (<*z,x*>,and2))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)))
by CIRCCOMB:11;
thus InnerVertices (GFA1CarryStr (x,y,z)) =
InnerVertices (((1GateCircStr (<*x,y*>,and2c)) +* ((1GateCircStr (<*y,z*>,and2a)) +* (1GateCircStr (<*z,x*>,and2)))) +* (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)))
by CIRCCOMB:6
.=
InnerVertices ((1GateCircStr (<*x,y*>,and2c)) +* (((1GateCircStr (<*y,z*>,and2a)) +* (1GateCircStr (<*z,x*>,and2))) +* (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3))))
by CIRCCOMB:6
.=
(InnerVertices (1GateCircStr (<*x,y*>,and2c))) \/ (InnerVertices (((1GateCircStr (<*y,z*>,and2a)) +* (1GateCircStr (<*z,x*>,and2))) +* (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3))))
by A1, CIRCCOMB:11
.=
(InnerVertices (1GateCircStr (<*x,y*>,and2c))) \/ (InnerVertices ((1GateCircStr (<*y,z*>,and2a)) +* ((1GateCircStr (<*z,x*>,and2)) +* (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)))))
by CIRCCOMB:6
.=
((InnerVertices (1GateCircStr (<*x,y*>,and2c))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2a)))) \/ ((InnerVertices (1GateCircStr (<*z,x*>,and2))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3))))
by A2, A3, XBOOLE_1:4
.=
(((InnerVertices (1GateCircStr (<*x,y*>,and2c))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2a)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2)))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)))
by XBOOLE_1:4
.=
(({[<*x,y*>,and2c]} \/ (InnerVertices (1GateCircStr (<*y,z*>,and2a)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2)))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)))
by CIRCCOMB:42
.=
(({[<*x,y*>,and2c]} \/ {[<*y,z*>,and2a]}) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2)))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)))
by CIRCCOMB:42
.=
(({[<*x,y*>,and2c]} \/ {[<*y,z*>,and2a]}) \/ {[<*z,x*>,and2]}) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)))
by CIRCCOMB:42
.=
({[<*x,y*>,and2c],[<*y,z*>,and2a]} \/ {[<*z,x*>,and2]}) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)))
by ENUMSET1:1
.=
{[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]} \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)))
by ENUMSET1:3
.=
{[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]} \/ {(GFA1CarryOutput (x,y,z))}
by CIRCCOMB:42
; verum