let x, y, z be set ; :: thesis: InnerVertices (GFA2CarryIStr (x,y,z)) = {[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]}
set f1 = and2a ;
set f2 = and2c ;
set f3 = nor2 ;
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);
A1: 1GateCircStr (<*x,y*>,and2a) tolerates 1GateCircStr (<*y,z*>,and2c) by CIRCCOMB:47;
(1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,z*>,and2c)) tolerates 1GateCircStr (<*z,x*>,nor2) by CIRCCOMB:47;
then InnerVertices (GFA2CarryIStr (x,y,z)) = (InnerVertices ((1GateCircStr (<*x,y*>,and2a)) +* (1GateCircStr (<*y,z*>,and2c)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,nor2))) by CIRCCOMB:11
.= ((InnerVertices (1GateCircStr (<*x,y*>,and2a))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,nor2))) by A1, CIRCCOMB:11
.= ({[<*x,y*>,and2a]} \/ (InnerVertices (1GateCircStr (<*y,z*>,and2c)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,nor2))) by CIRCCOMB:42
.= ({[<*x,y*>,and2a]} \/ {[<*y,z*>,and2c]}) \/ (InnerVertices (1GateCircStr (<*z,x*>,nor2))) by CIRCCOMB:42
.= ({[<*x,y*>,and2a]} \/ {[<*y,z*>,and2c]}) \/ {[<*z,x*>,nor2]} by CIRCCOMB:42
.= {[<*x,y*>,and2a],[<*y,z*>,and2c]} \/ {[<*z,x*>,nor2]} by ENUMSET1:1
.= {[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]} by ENUMSET1:3 ;
hence InnerVertices (GFA2CarryIStr (x,y,z)) = {[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,nor2]} ; :: thesis: verum