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