let x, y, z be set ; :: thesis: InnerVertices (BitGFA3Str (x,y,z)) = (({[<*x,y*>,xor2]} \/ {(GFA3AdderOutput (x,y,z))}) \/ {[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]}) \/ {(GFA3CarryOutput (x,y,z))}
set f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
set f0 = xor2 ;
set xyf0 = [<*x,y*>,xor2];
set xyf1 = [<*x,y*>,and2b];
set yzf2 = [<*y,z*>,and2b];
set zxf3 = [<*z,x*>,and2b];
set S = BitGFA3Str (x,y,z);
set S1 = GFA3AdderStr (x,y,z);
set S2 = GFA3CarryStr (x,y,z);
set A1 = GFA3AdderOutput (x,y,z);
set A2 = GFA3CarryOutput (x,y,z);
thus InnerVertices (BitGFA3Str (x,y,z)) = (InnerVertices (GFA3AdderStr (x,y,z))) \/ (InnerVertices (GFA3CarryStr (x,y,z))) by FACIRC_1:27
.= ({[<*x,y*>,xor2]} \/ {(GFA3AdderOutput (x,y,z))}) \/ (InnerVertices (GFA3CarryStr (x,y,z))) by Th137
.= ({[<*x,y*>,xor2]} \/ {(GFA3AdderOutput (x,y,z))}) \/ ({[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]} \/ {(GFA3CarryOutput (x,y,z))}) by Th124
.= (({[<*x,y*>,xor2]} \/ {(GFA3AdderOutput (x,y,z))}) \/ {[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]}) \/ {(GFA3CarryOutput (x,y,z))} by XBOOLE_1:4 ; :: thesis: verum