let x, y, z be set ; :: thesis: ( [<*x,y*>,xor2] in InnerVertices (BitGFA3Str (x,y,z)) & GFA3AdderOutput (x,y,z) in InnerVertices (BitGFA3Str (x,y,z)) & [<*x,y*>,nor2] in InnerVertices (BitGFA3Str (x,y,z)) & [<*y,z*>,nor2] in InnerVertices (BitGFA3Str (x,y,z)) & [<*z,x*>,nor2] in InnerVertices (BitGFA3Str (x,y,z)) & GFA3CarryOutput (x,y,z) in InnerVertices (BitGFA3Str (x,y,z)) )
set f1 = nor2 ;
set f2 = nor2 ;
set f3 = nor2 ;
set f0 = xor2 ;
set xyf0 = [<*x,y*>,xor2];
set xyf1 = [<*x,y*>,nor2];
set yzf2 = [<*y,z*>,nor2];
set zxf3 = [<*z,x*>,nor2];
set S = BitGFA3Str (x,y,z);
set A1 = GFA3AdderOutput (x,y,z);
set A2 = GFA3CarryOutput (x,y,z);
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))} by Th127
.= ({[<*x,y*>,xor2],(GFA3AdderOutput (x,y,z))} \/ {[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]}) \/ {(GFA3CarryOutput (x,y,z))} by ENUMSET1:1
.= {[<*x,y*>,xor2],(GFA3AdderOutput (x,y,z)),[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2]} \/ {(GFA3CarryOutput (x,y,z))} by ENUMSET1:8
.= {[<*x,y*>,xor2],(GFA3AdderOutput (x,y,z)),[<*x,y*>,nor2],[<*y,z*>,nor2],[<*z,x*>,nor2],(GFA3CarryOutput (x,y,z))} by ENUMSET1:15 ;
hence ( [<*x,y*>,xor2] in InnerVertices (BitGFA3Str (x,y,z)) & GFA3AdderOutput (x,y,z) in InnerVertices (BitGFA3Str (x,y,z)) & [<*x,y*>,nor2] in InnerVertices (BitGFA3Str (x,y,z)) & [<*y,z*>,nor2] in InnerVertices (BitGFA3Str (x,y,z)) & [<*z,x*>,nor2] in InnerVertices (BitGFA3Str (x,y,z)) & GFA3CarryOutput (x,y,z) in InnerVertices (BitGFA3Str (x,y,z)) ) by ENUMSET1:def 4; :: thesis: verum