let x, y, z be set ; :: thesis: InnerVertices (GFA3AdderStr x,y,z) = {[<*x,y*>,xor2 ]} \/ {(GFA3AdderOutput x,y,z)}
set S3 = GFA3AdderStr x,y,z;
set O3 = GFA3AdderOutput x,y,z;
set S0 = GFA0AdderStr x,y,z;
set O0 = GFA0AdderOutput x,y,z;
( GFA3AdderStr x,y,z = GFA0AdderStr x,y,z & GFA3AdderOutput x,y,z = GFA0AdderOutput x,y,z ) ;
hence InnerVertices (GFA3AdderStr x,y,z) = {[<*x,y*>,xor2 ]} \/ {(GFA3AdderOutput x,y,z)} by Th27; :: thesis: verum