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