let x, y, z be set ; InnerVertices (GFA0CarryIStr (x,y,z)) = {[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]}
set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set xy = [<*x,y*>,and2];
set yz = [<*y,z*>,and2];
set zx = [<*z,x*>,and2];
set Cxy = 1GateCircStr (<*x,y*>,and2);
set Cyz = 1GateCircStr (<*y,z*>,and2);
set Czx = 1GateCircStr (<*z,x*>,and2);
A1:
1GateCircStr (<*x,y*>,and2) tolerates 1GateCircStr (<*y,z*>,and2)
by CIRCCOMB:47;
(1GateCircStr (<*x,y*>,and2)) +* (1GateCircStr (<*y,z*>,and2)) tolerates 1GateCircStr (<*z,x*>,and2)
by CIRCCOMB:47;
then InnerVertices (GFA0CarryIStr (x,y,z)) =
(InnerVertices ((1GateCircStr (<*x,y*>,and2)) +* (1GateCircStr (<*y,z*>,and2)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2)))
by CIRCCOMB:11
.=
((InnerVertices (1GateCircStr (<*x,y*>,and2))) \/ (InnerVertices (1GateCircStr (<*y,z*>,and2)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2)))
by A1, CIRCCOMB:11
.=
({[<*x,y*>,and2]} \/ (InnerVertices (1GateCircStr (<*y,z*>,and2)))) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2)))
by CIRCCOMB:42
.=
({[<*x,y*>,and2]} \/ {[<*y,z*>,and2]}) \/ (InnerVertices (1GateCircStr (<*z,x*>,and2)))
by CIRCCOMB:42
.=
({[<*x,y*>,and2]} \/ {[<*y,z*>,and2]}) \/ {[<*z,x*>,and2]}
by CIRCCOMB:42
.=
{[<*x,y*>,and2],[<*y,z*>,and2]} \/ {[<*z,x*>,and2]}
by ENUMSET1:1
.=
{[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]}
by ENUMSET1:3
;
hence
InnerVertices (GFA0CarryIStr (x,y,z)) = {[<*x,y*>,and2],[<*y,z*>,and2],[<*z,x*>,and2]}
; verum