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