let x, y, z be set ; :: thesis: ( [<*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) )
set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f0 = xor2 ;
set xyf0 = [<*x,y*>,xor2 ];
set xyf1 = [<*x,y*>,and2 ];
set yzf2 = [<*y,z*>,and2 ];
set zxf3 = [<*z,x*>,and2 ];
set S = BitGFA0Str x,y,z;
set A1 = GFA0AdderOutput x,y,z;
set A2 = GFA0CarryOutput x,y,z;
InnerVertices (BitGFA0Str x,y,z) = (({[<*x,y*>,xor2 ]} \/ {(GFA0AdderOutput x,y,z)}) \/ {[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]}) \/ {(GFA0CarryOutput x,y,z)} by Th39
.= ({[<*x,y*>,xor2 ],(GFA0AdderOutput x,y,z)} \/ {[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]}) \/ {(GFA0CarryOutput x,y,z)} by ENUMSET1:41
.= {[<*x,y*>,xor2 ],(GFA0AdderOutput x,y,z),[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]} \/ {(GFA0CarryOutput x,y,z)} by ENUMSET1:48
.= {[<*x,y*>,xor2 ],(GFA0AdderOutput x,y,z),[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ],(GFA0CarryOutput x,y,z)} by ENUMSET1:55 ;
hence ( [<*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) ) by ENUMSET1:def 4; :: thesis: verum