set f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
set f4 = nor3 ;
let x, y, z be non pair set ; :: thesis: InputVertices (GFA3CarryStr x,y,z) = {x,y,z}
set xy = [<*x,y*>,and2b ];
set yz = [<*y,z*>,and2b ];
set zx = [<*z,x*>,and2b ];
set Cxy = 1GateCircStr <*x,y*>,and2b ;
set Cyz = 1GateCircStr <*y,z*>,and2b ;
set Czx = 1GateCircStr <*z,x*>,and2b ;
set M = GFA3CarryStr x,y,z;
set MI = GFA3CarryIStr x,y,z;
set S = 1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ;
A1: ( not InputVertices (1GateCircStr <*x,y*>,and2b ) is with_pair & not InputVertices (1GateCircStr <*y,z*>,and2b ) is with_pair & not InputVertices (1GateCircStr <*z,x*>,and2b ) is with_pair ) by FACIRC_1:41;
then A2: not InputVertices ((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b )) is with_pair by FACIRC_1:9;
then A3: not InputVertices (GFA3CarryIStr x,y,z) is with_pair by A1, FACIRC_1:9;
A4: ( InputVertices (1GateCircStr <*x,y*>,and2b ) = {x,y} & InputVertices (1GateCircStr <*y,z*>,and2b ) = {y,z} & InputVertices (1GateCircStr <*z,x*>,and2b ) = {z,x} ) by FACIRC_1:40;
InnerVertices (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ) is Relation by FACIRC_1:38;
then A5: InputVertices (GFA3CarryStr x,y,z) = (InputVertices (GFA3CarryIStr x,y,z)) \/ ((InputVertices (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 )) \ (InnerVertices (GFA3CarryIStr x,y,z))) by A3, FACIRC_1:6;
A6: InputVertices (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 ) = {[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]} by FACIRC_1:42;
A7: ( InnerVertices (1GateCircStr <*x,y*>,and2b ) = {[<*x,y*>,and2b ]} & InnerVertices (1GateCircStr <*y,z*>,and2b ) = {[<*y,z*>,and2b ]} & InnerVertices (1GateCircStr <*z,x*>,and2b ) = {[<*z,x*>,and2b ]} ) by CIRCCOMB:49;
( 1GateCircStr <*x,y*>,and2b tolerates 1GateCircStr <*y,z*>,and2b & 1GateCircStr <*x,y*>,and2b tolerates 1GateCircStr <*z,x*>,and2b & 1GateCircStr <*y,z*>,and2b tolerates 1GateCircStr <*z,x*>,and2b ) by CIRCCOMB:55;
then A8: InnerVertices ((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b )) = {[<*x,y*>,and2b ]} \/ {[<*y,z*>,and2b ]} by A7, CIRCCOMB:15;
(1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b ) tolerates 1GateCircStr <*z,x*>,and2b by CIRCCOMB:55;
then InnerVertices (GFA3CarryIStr x,y,z) = ({[<*x,y*>,and2b ]} \/ {[<*y,z*>,and2b ]}) \/ {[<*z,x*>,and2b ]} by A7, A8, CIRCCOMB:15
.= {[<*x,y*>,and2b ],[<*y,z*>,and2b ]} \/ {[<*z,x*>,and2b ]} by ENUMSET1:41
.= {[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]} by ENUMSET1:43 ;
then (InputVertices (1GateCircStr <*[<*x,y*>,and2b ],[<*y,z*>,and2b ],[<*z,x*>,and2b ]*>,nor3 )) \ (InnerVertices (GFA3CarryIStr x,y,z)) = {} by A6, XBOOLE_1:37;
hence InputVertices (GFA3CarryStr x,y,z) = (InputVertices ((1GateCircStr <*x,y*>,and2b ) +* (1GateCircStr <*y,z*>,and2b ))) \/ (InputVertices (1GateCircStr <*z,x*>,and2b )) by A1, A2, A5, A7, A8, FACIRC_1:7
.= ((InputVertices (1GateCircStr <*x,y*>,and2b )) \/ (InputVertices (1GateCircStr <*y,z*>,and2b ))) \/ (InputVertices (1GateCircStr <*z,x*>,and2b )) by A1, A7, FACIRC_1:7
.= {x,y,y,z} \/ {z,x} by A4, ENUMSET1:45
.= {y,y,x,z} \/ {z,x} by ENUMSET1:110
.= {y,x,z} \/ {z,x} by ENUMSET1:71
.= {x,y,z} \/ {z,x} by ENUMSET1:99
.= {x,y,z} \/ ({z} \/ {x}) by ENUMSET1:41
.= ({x,y,z} \/ {z}) \/ {x} by XBOOLE_1:4
.= ({z,x,y} \/ {z}) \/ {x} by ENUMSET1:100
.= {z,z,x,y} \/ {x} by ENUMSET1:44
.= {z,x,y} \/ {x} by ENUMSET1:71
.= {x,y,z} \/ {x} by ENUMSET1:100
.= {x,x,y,z} by ENUMSET1:44
.= {x,y,z} by ENUMSET1:71 ;
:: thesis: verum