set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set f4 = or3 ;
let x, y, z be set ; :: thesis: InnerVertices (GFA1CarryStr x,y,z) = {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]} \/ {(GFA1CarryOutput x,y,z)}
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:55;
A2: 1GateCircStr <*y,z*>,and2a tolerates (1GateCircStr <*z,x*>,and2 ) +* (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 ) by CIRCCOMB:55;
A3: 1GateCircStr <*z,x*>,and2 tolerates 1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 by CIRCCOMB:55;
A4: 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 A2, CIRCCOMB:15;
A5: 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 A3, CIRCCOMB:15;
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:10
.= 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:10
.= (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:15
.= (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:10
.= ((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 A4, A5, 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:49
.= (({[<*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:49
.= (({[<*x,y*>,and2c ]} \/ {[<*y,z*>,and2a ]}) \/ {[<*z,x*>,and2 ]}) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 )) by CIRCCOMB:49
.= ({[<*x,y*>,and2c ],[<*y,z*>,and2a ]} \/ {[<*z,x*>,and2 ]}) \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 )) by ENUMSET1:41
.= {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]} \/ (InnerVertices (1GateCircStr <*[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]*>,or3 )) by ENUMSET1:43
.= {[<*x,y*>,and2c ],[<*y,z*>,and2a ],[<*z,x*>,and2 ]} \/ {(GFA1CarryOutput x,y,z)} by CIRCCOMB:49 ; :: thesis: verum