let x1, x2, x3, x5, x6, x7 be set ; :: thesis: InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) = (({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3))} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7))}) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))}
set S = STC0IIStr (x1,x2,x3,x5,x6,x7);
set S1 = BitGFA0Str (x1,x2,x3);
set A1 = GFA0AdderOutput (x1,x2,x3);
set C1 = GFA0CarryOutput (x1,x2,x3);
set S2 = BitGFA0Str (x5,x6,x7);
set A2 = GFA0AdderOutput (x5,x6,x7);
set C2 = GFA0CarryOutput (x5,x6,x7);
set x1x20 = [<*x1,x2*>,xor2];
set x1x2 = [<*x1,x2*>,and2];
set x2x3 = [<*x2,x3*>,and2];
set x3x1 = [<*x3,x1*>,and2];
set x5x60 = [<*x5,x6*>,xor2];
set x5x6 = [<*x5,x6*>,and2];
set x6x7 = [<*x6,x7*>,and2];
set x7x5 = [<*x7,x5*>,and2];
BitGFA0Str (x1,x2,x3) tolerates BitGFA0Str (x5,x6,x7) by CIRCCOMB:47;
hence InnerVertices (STC0IIStr (x1,x2,x3,x5,x6,x7)) = (InnerVertices (BitGFA0Str (x1,x2,x3))) \/ (InnerVertices (BitGFA0Str (x5,x6,x7))) by CIRCCOMB:11
.= ((({[<*x1,x2*>,xor2]} \/ {(GFA0AdderOutput (x1,x2,x3))}) \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {(GFA0CarryOutput (x1,x2,x3))}) \/ (InnerVertices (BitGFA0Str (x5,x6,x7))) by GFACIRC1:31
.= (({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3))} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]}) \/ {(GFA0CarryOutput (x1,x2,x3))}) \/ (InnerVertices (BitGFA0Str (x5,x6,x7))) by ENUMSET1:1
.= ({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3))} \/ ({[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2]} \/ {(GFA0CarryOutput (x1,x2,x3))})) \/ (InnerVertices (BitGFA0Str (x5,x6,x7))) by XBOOLE_1:4
.= ({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3))} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ (InnerVertices (BitGFA0Str (x5,x6,x7))) by ENUMSET1:6
.= ({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3))} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ ((({[<*x5,x6*>,xor2]} \/ {(GFA0AdderOutput (x5,x6,x7))}) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]}) \/ {(GFA0CarryOutput (x5,x6,x7))}) by GFACIRC1:31
.= ({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3))} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ (({[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7))} \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]}) \/ {(GFA0CarryOutput (x5,x6,x7))}) by ENUMSET1:1
.= ({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3))} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ ({[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7))} \/ ({[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2]} \/ {(GFA0CarryOutput (x5,x6,x7))})) by XBOOLE_1:4
.= ({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3))} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ ({[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7))} \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))}) by ENUMSET1:6
.= (({[<*x1,x2*>,xor2],(GFA0AdderOutput (x1,x2,x3))} \/ {[<*x1,x2*>,and2],[<*x2,x3*>,and2],[<*x3,x1*>,and2],(GFA0CarryOutput (x1,x2,x3))}) \/ {[<*x5,x6*>,xor2],(GFA0AdderOutput (x5,x6,x7))}) \/ {[<*x5,x6*>,and2],[<*x6,x7*>,and2],[<*x7,x5*>,and2],(GFA0CarryOutput (x5,x6,x7))} by XBOOLE_1:4 ;
:: thesis: verum