let x, y, z be set ; InnerVertices (GFA2CarryStr (x,y,z)) = {[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]} \/ {(GFA2CarryOutput (x,y,z))}
set f1 = and2a ;
set f2 = and2c ;
set f3 = and2b ;
set f4 = nor3 ;
set xy = [<*x,y*>,and2a];
set yz = [<*y,z*>,and2c];
set zx = [<*z,x*>,and2b];
set Cxy = 1GateCircStr (<*x,y*>,and2a);
set Cyz = 1GateCircStr (<*y,z*>,and2c);
set Czx = 1GateCircStr (<*z,x*>,and2b);
set Cxyz = 1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3);
A1:
1GateCircStr (<*x,y*>,and2a) tolerates ((1GateCircStr (<*y,z*>,and2c)) +* (1GateCircStr (<*z,x*>,and2b))) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3))
by CIRCCOMB:55;
1GateCircStr (<*y,z*>,and2c) tolerates (1GateCircStr (<*z,x*>,and2b)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3))
by CIRCCOMB:55;
then A2:
InnerVertices ((1GateCircStr (<*y,z*>,and2c)) +* ((1GateCircStr (<*z,x*>,and2b)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3)))) = (InnerVertices (1GateCircStr (<*y,z*>,and2c))) \/ (InnerVertices ((1GateCircStr (<*z,x*>,and2b)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3))))
by CIRCCOMB:15;
1GateCircStr (<*z,x*>,and2b) tolerates 1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3)
by CIRCCOMB:55;
then A3:
InnerVertices ((1GateCircStr (<*z,x*>,and2b)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3))) = (InnerVertices (1GateCircStr (<*z,x*>,and2b))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3)))
by CIRCCOMB:15;
thus InnerVertices (GFA2CarryStr (x,y,z)) =
InnerVertices (((1GateCircStr (<*x,y*>,and2a)) +* ((1GateCircStr (<*y,z*>,and2c)) +* (1GateCircStr (<*z,x*>,and2b)))) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3)))
by CIRCCOMB:10
.=
InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (((1GateCircStr (<*y,z*>,and2c)) +* (1GateCircStr (<*z,x*>,and2b))) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3))))
by CIRCCOMB:10
.=
(InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (((1GateCircStr (<*y,z*>,and2c)) +* (1GateCircStr (<*z,x*>,and2b))) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3))))
by A1, CIRCCOMB:15
.=
(InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices ((1GateCircStr (<*y,z*>,and2c)) +* ((1GateCircStr (<*z,x*>,and2b)) +* (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3)))))
by CIRCCOMB:10
.=
((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))) \/ ((InnerVertices (1GateCircStr (<*z,x*>,and2b))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3))))
by A2, A3, XBOOLE_1:4
.=
(((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2b)))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3)))
by XBOOLE_1:4
.=
(({[<*x,y*>,and2a]} \/ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2b)))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3)))
by CIRCCOMB:49
.=
(({[<*x,y*>,and2a]} \/ {[<*y,z*>,and2c]}) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2b)))) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3)))
by CIRCCOMB:49
.=
(({[<*x,y*>,and2a]} \/ {[<*y,z*>,and2c]}) \/ {[<*z,x*>,and2b]}) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3)))
by CIRCCOMB:49
.=
({[<*x,y*>,and2a],[<*y,z*>,and2c]} \/ {[<*z,x*>,and2b]}) \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3)))
by ENUMSET1:41
.=
{[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]} \/ (InnerVertices (1GateCircStr (<*[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]*>,nor3)))
by ENUMSET1:43
.=
{[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]} \/ {(GFA2CarryOutput (x,y,z))}
by CIRCCOMB:49
; verum