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