theorem Th127: :: GFACIRC1:127

for x, y, z being set holds InnerVertices (BitGFA3Str (x,y,z)) = (({[<*x,y*>,xor2]} \/ {(GFA3AdderOutput (x,y,z))}) \/ {[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]}) \/ {(GFA3CarryOutput (x,y,z))}