theorem Th37: :: GFACIRC1:37

for x, y, z being set holds
( [<*x,y*>,xor2] in InnerVertices (BitGFA0Str (x,y,z)) & GFA0AdderOutput (x,y,z) in InnerVertices (BitGFA0Str (x,y,z)) & [<*x,y*>,and2] in InnerVertices (BitGFA0Str (x,y,z)) & [<*y,z*>,and2] in InnerVertices (BitGFA0Str (x,y,z)) & [<*z,x*>,and2] in InnerVertices (BitGFA0Str (x,y,z)) & GFA0CarryOutput (x,y,z) in InnerVertices (BitGFA0Str (x,y,z)) )