set f1 = and2a ;
set f2 = and2c ;
set f3 = and2b ;
set f4 = nor3 ;
let x, y, z be set ; :: thesis: InnerVertices (GFA2CarryStr x,y,z) = {[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]} \/ {(GFA2CarryOutput x,y,z)}
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;
A2: 1GateCircStr <*y,z*>,and2c tolerates (1GateCircStr <*z,x*>,and2b ) +* (1GateCircStr <*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 ) by CIRCCOMB:55;
A3: 1GateCircStr <*z,x*>,and2b tolerates 1GateCircStr <*[<*x,y*>,and2a ],[<*y,z*>,and2c ],[<*z,x*>,and2b ]*>,nor3 by CIRCCOMB:55;
A4: 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 A2, CIRCCOMB:15;
A5: 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 A3, 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 A4, A5, 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 ; :: thesis: verum