let x, y, z be non pair set ; :: thesis: not InputVertices (GFA0CarryStr x,y,z) is with_pair
set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f4 = or3 ;
set xy = [<*x,y*>,and2 ];
set yz = [<*y,z*>,and2 ];
set zx = [<*z,x*>,and2 ];
set Cxy = 1GateCircStr <*x,y*>,and2 ;
set Cyz = 1GateCircStr <*y,z*>,and2 ;
set Czx = 1GateCircStr <*z,x*>,and2 ;
set S = 1GateCircStr <*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ;
set M = GFA0CarryStr x,y,z;
set MI = GFA0CarryIStr x,y,z;
given xx being pair set such that A1: xx in InputVertices (GFA0CarryStr x,y,z) ; :: according to FACIRC_1:def 2 :: thesis: contradiction
A2: 1GateCircStr <*x,y*>,and2 tolerates 1GateCircStr <*y,z*>,and2 by CIRCCOMB:55;
A3: ( InnerVertices (1GateCircStr <*z,x*>,and2 ) = {[<*z,x*>,and2 ]} & (1GateCircStr <*x,y*>,and2 ) +* (1GateCircStr <*y,z*>,and2 ) tolerates 1GateCircStr <*z,x*>,and2 ) by CIRCCOMB:49, CIRCCOMB:55;
( InnerVertices (1GateCircStr <*x,y*>,and2 ) = {[<*x,y*>,and2 ]} & InnerVertices (1GateCircStr <*y,z*>,and2 ) = {[<*y,z*>,and2 ]} ) by CIRCCOMB:49;
then InnerVertices ((1GateCircStr <*x,y*>,and2 ) +* (1GateCircStr <*y,z*>,and2 )) = {[<*x,y*>,and2 ]} \/ {[<*y,z*>,and2 ]} by A2, CIRCCOMB:15;
then A4: InnerVertices (GFA0CarryIStr x,y,z) = ({[<*x,y*>,and2 ]} \/ {[<*y,z*>,and2 ]}) \/ {[<*z,x*>,and2 ]} by A3, CIRCCOMB:15
.= {[<*x,y*>,and2 ],[<*y,z*>,and2 ]} \/ {[<*z,x*>,and2 ]} by ENUMSET1:41
.= {[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]} by ENUMSET1:43 ;
InputVertices (1GateCircStr <*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ) = {[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]} by FACIRC_1:42;
then A5: (InputVertices (1GateCircStr <*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 )) \ (InnerVertices (GFA0CarryIStr x,y,z)) = {} by A4, XBOOLE_1:37;
( not InputVertices (1GateCircStr <*x,y*>,and2 ) is with_pair & not InputVertices (1GateCircStr <*y,z*>,and2 ) is with_pair ) by FACIRC_1:41;
then ( not InputVertices (1GateCircStr <*z,x*>,and2 ) is with_pair & not InputVertices ((1GateCircStr <*x,y*>,and2 ) +* (1GateCircStr <*y,z*>,and2 )) is with_pair ) by FACIRC_1:9, FACIRC_1:41;
then A6: not InputVertices (GFA0CarryIStr x,y,z) is with_pair by FACIRC_1:9;
InnerVertices (1GateCircStr <*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 ) is Relation by FACIRC_1:38;
then InputVertices (GFA0CarryStr x,y,z) = (InputVertices (GFA0CarryIStr x,y,z)) \/ ((InputVertices (1GateCircStr <*[<*x,y*>,and2 ],[<*y,z*>,and2 ],[<*z,x*>,and2 ]*>,or3 )) \ (InnerVertices (GFA0CarryIStr x,y,z))) by A6, FACIRC_1:6;
hence contradiction by A6, A1, A5, FACIRC_1:def 2; :: thesis: verum