let x, y, z be set ; :: thesis: ( [<*x,y*>,xor2 ] in InnerVertices (GFA3AdderStr x,y,z) & GFA3AdderOutput x,y,z in InnerVertices (GFA3AdderStr x,y,z) )
set S0 = GFA0AdderStr x,y,z;
GFA3AdderStr x,y,z = GFA0AdderStr x,y,z ;
hence ( [<*x,y*>,xor2 ] in InnerVertices (GFA3AdderStr x,y,z) & GFA3AdderOutput x,y,z in InnerVertices (GFA3AdderStr x,y,z) ) by Th32; :: thesis: verum