let x1, x2, x3, x4, x5, x6, x7 be set ; :: thesis:
set S = STC0Str (x1,x2,x3,x4,x5,x6,x7);
set S1 = STC0IStr (x1,x2,x3,x4,x5,x6,x7);
set C1 = STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7);
set C2 = STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7);
set C3 = STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7);
set S2 = BitGFA0Str ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)));
set C1C2x = [<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,xor2];
set C1C2a = [<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,and2];
set C2C3a = [<*(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))*>,and2];
set C3C1a = [<*(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7))*>,and2];
set Aout = GFA0AdderOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)));
set Cout = GFA0CarryOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)));
STC0IStr (x1,x2,x3,x4,x5,x6,x7) tolerates BitGFA0Str ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))) by CIRCCOMB:47;
hence InnerVertices (STC0Str (x1,x2,x3,x4,x5,x6,x7)) = (InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7))) \/ (InnerVertices (BitGFA0Str ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))) by CIRCCOMB:11
.= (InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7))) \/ ((({[<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,xor2]} \/ {(GFA0AdderOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))}) \/ {[<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,and2],[<*(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))*>,and2],[<*(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7))*>,and2]}) \/ {(GFA0CarryOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))}) by GFACIRC1:31
.= (InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7))) \/ (({[<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,xor2],(GFA0AdderOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))} \/ {[<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,and2],[<*(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))*>,and2],[<*(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7))*>,and2]}) \/ {(GFA0CarryOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))}) by ENUMSET1:1
.= (InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7))) \/ ({[<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,xor2],(GFA0AdderOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))} \/ ({[<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,and2],[<*(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))*>,and2],[<*(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7))*>,and2]} \/ {(GFA0CarryOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))})) by XBOOLE_1:4
.= (InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7))) \/ ({[<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,xor2],(GFA0AdderOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))} \/ {[<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,and2],[<*(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))*>,and2],[<*(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7))*>,and2],(GFA0CarryOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))}) by ENUMSET1:6
.= ((InnerVertices (STC0IStr (x1,x2,x3,x4,x5,x6,x7))) \/ {[<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,xor2],(GFA0AdderOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))}) \/ {[<*(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7))*>,and2],[<*(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))*>,and2],[<*(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7))*>,and2],(GFA0CarryOutput ((STC0ICarryOutputC1 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC2 (x1,x2,x3,x4,x5,x6,x7)),(STC0ICarryOutputC3 (x1,x2,x3,x4,x5,x6,x7))))} by XBOOLE_1:4 ;
:: thesis: