let x, y, z be set ; :: thesis: ( [<*x,y*>,xor2c] in InnerVertices (BitGFA2Str (x,y,z)) & GFA2AdderOutput (x,y,z) in InnerVertices (BitGFA2Str (x,y,z)) & [<*x,y*>,and2a] in InnerVertices (BitGFA2Str (x,y,z)) & [<*y,z*>,and2c] in InnerVertices (BitGFA2Str (x,y,z)) & [<*z,x*>,and2b] in InnerVertices (BitGFA2Str (x,y,z)) & GFA2CarryOutput (x,y,z) in InnerVertices (BitGFA2Str (x,y,z)) )
set f1 = and2a ;
set f2 = and2c ;
set f3 = and2b ;
set f0 = xor2c ;
set xyf0 = [<*x,y*>,xor2c];
set xyf1 = [<*x,y*>,and2a];
set yzf2 = [<*y,z*>,and2c];
set zxf3 = [<*z,x*>,and2b];
set S = BitGFA2Str (x,y,z);
set A1 = GFA2AdderOutput (x,y,z);
set A2 = GFA2CarryOutput (x,y,z);
InnerVertices (BitGFA2Str (x,y,z)) = (({[<*x,y*>,xor2c]} \/ {(GFA2AdderOutput (x,y,z))}) \/ {[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]}) \/ {(GFA2CarryOutput (x,y,z))} by Th113
.= ({[<*x,y*>,xor2c],(GFA2AdderOutput (x,y,z))} \/ {[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]}) \/ {(GFA2CarryOutput (x,y,z))} by ENUMSET1:41
.= {[<*x,y*>,xor2c],(GFA2AdderOutput (x,y,z)),[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b]} \/ {(GFA2CarryOutput (x,y,z))} by ENUMSET1:48
.= {[<*x,y*>,xor2c],(GFA2AdderOutput (x,y,z)),[<*x,y*>,and2a],[<*y,z*>,and2c],[<*z,x*>,and2b],(GFA2CarryOutput (x,y,z))} by ENUMSET1:55 ;
hence ( [<*x,y*>,xor2c] in InnerVertices (BitGFA2Str (x,y,z)) & GFA2AdderOutput (x,y,z) in InnerVertices (BitGFA2Str (x,y,z)) & [<*x,y*>,and2a] in InnerVertices (BitGFA2Str (x,y,z)) & [<*y,z*>,and2c] in InnerVertices (BitGFA2Str (x,y,z)) & [<*z,x*>,and2b] in InnerVertices (BitGFA2Str (x,y,z)) & GFA2CarryOutput (x,y,z) in InnerVertices (BitGFA2Str (x,y,z)) ) by ENUMSET1:def 4; :: thesis: verum