let x, y, z be non pair set ; :: thesis: not InputVertices (GFA3CarryStr (x,y,z)) is with_pair
set f1 = and2b ;
set f2 = and2b ;
set f3 = and2b ;
set f4 = nor3 ;
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 S = 1GateCircStr (<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3);
set M = GFA3CarryStr (x,y,z);
set MI = GFA3CarryIStr (x,y,z);
given xx being pair set such that A1: xx in InputVertices (GFA3CarryStr (x,y,z)) ; :: according to FACIRC_1:def 2 :: thesis: contradiction
A2: 1GateCircStr (<*x,y*>,and2b) tolerates 1GateCircStr (<*y,z*>,and2b) by CIRCCOMB:47;
A3: ( InnerVertices (1GateCircStr (<*z,x*>,and2b)) = {[<*z,x*>,and2b]} & (1GateCircStr (<*x,y*>,and2b)) +* (1GateCircStr (<*y,z*>,and2b)) tolerates 1GateCircStr (<*z,x*>,and2b) ) by CIRCCOMB:42, CIRCCOMB:47;
( InnerVertices (1GateCircStr (<*x,y*>,and2b)) = {[<*x,y*>,and2b]} & InnerVertices (1GateCircStr (<*y,z*>,and2b)) = {[<*y,z*>,and2b]} ) by CIRCCOMB:42;
then InnerVertices ((1GateCircStr (<*x,y*>,and2b)) +* (1GateCircStr (<*y,z*>,and2b))) = {[<*x,y*>,and2b]} \/ {[<*y,z*>,and2b]} by A2, CIRCCOMB:11;
then A4: InnerVertices (GFA3CarryIStr (x,y,z)) = ({[<*x,y*>,and2b]} \/ {[<*y,z*>,and2b]}) \/ {[<*z,x*>,and2b]} by A3, CIRCCOMB:11
.= {[<*x,y*>,and2b],[<*y,z*>,and2b]} \/ {[<*z,x*>,and2b]} by ENUMSET1:1
.= {[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]} by ENUMSET1:3 ;
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;
then A5: (InputVertices (1GateCircStr (<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3))) \ (InnerVertices (GFA3CarryIStr (x,y,z))) = {} by A4, XBOOLE_1:37;
( not InputVertices (1GateCircStr (<*x,y*>,and2b)) is with_pair & not InputVertices (1GateCircStr (<*y,z*>,and2b)) is with_pair ) by FACIRC_1:41;
then ( not InputVertices (1GateCircStr (<*z,x*>,and2b)) is with_pair & not InputVertices ((1GateCircStr (<*x,y*>,and2b)) +* (1GateCircStr (<*y,z*>,and2b))) is with_pair ) by FACIRC_1:9, FACIRC_1:41;
then A6: not InputVertices (GFA3CarryIStr (x,y,z)) is with_pair by FACIRC_1:9;
InnerVertices (1GateCircStr (<*[<*x,y*>,and2b],[<*y,z*>,and2b],[<*z,x*>,and2b]*>,nor3)) is Relation by FACIRC_1:38;
then 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 A6, FACIRC_1:6;
hence contradiction by A6, A1, A5, FACIRC_1:def 2; :: thesis: verum