let x, y, z be non pair set ; InputVertices (GFA1CarryStr (x,y,z)) is without_pairs
set f1 = and2c ;
set f2 = and2a ;
set f3 = and2 ;
set f4 = or3 ;
set xy = [<*x,y*>,and2c];
set yz = [<*y,z*>,and2a];
set zx = [<*z,x*>,and2];
set Cxy = 1GateCircStr (<*x,y*>,and2c);
set Cyz = 1GateCircStr (<*y,z*>,and2a);
set Czx = 1GateCircStr (<*z,x*>,and2);
set S = 1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3);
set M = GFA1CarryStr (x,y,z);
set MI = GFA1CarryIStr (x,y,z);
given xx being pair object such that A1:
xx in InputVertices (GFA1CarryStr (x,y,z))
; FACIRC_1:def 2 contradiction
A2:
1GateCircStr (<*x,y*>,and2c) tolerates 1GateCircStr (<*y,z*>,and2a)
by CIRCCOMB:47;
A3:
( InnerVertices (1GateCircStr (<*z,x*>,and2)) = {[<*z,x*>,and2]} & (1GateCircStr (<*x,y*>,and2c)) +* (1GateCircStr (<*y,z*>,and2a)) tolerates 1GateCircStr (<*z,x*>,and2) )
by CIRCCOMB:42, CIRCCOMB:47;
( InnerVertices (1GateCircStr (<*x,y*>,and2c)) = {[<*x,y*>,and2c]} & InnerVertices (1GateCircStr (<*y,z*>,and2a)) = {[<*y,z*>,and2a]} )
by CIRCCOMB:42;
then
InnerVertices ((1GateCircStr (<*x,y*>,and2c)) +* (1GateCircStr (<*y,z*>,and2a))) = {[<*x,y*>,and2c]} \/ {[<*y,z*>,and2a]}
by A2, CIRCCOMB:11;
then A4: InnerVertices (GFA1CarryIStr (x,y,z)) =
({[<*x,y*>,and2c]} \/ {[<*y,z*>,and2a]}) \/ {[<*z,x*>,and2]}
by A3, CIRCCOMB:11
.=
{[<*x,y*>,and2c],[<*y,z*>,and2a]} \/ {[<*z,x*>,and2]}
by ENUMSET1:1
.=
{[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]}
by ENUMSET1:3
;
InputVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)) = {[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]}
by FACIRC_1:42;
then A5:
(InputVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3))) \ (InnerVertices (GFA1CarryIStr (x,y,z))) = {}
by A4, XBOOLE_1:37;
( InputVertices (1GateCircStr (<*x,y*>,and2c)) is without_pairs & InputVertices (1GateCircStr (<*y,z*>,and2a)) is without_pairs )
by FACIRC_1:41;
then
( InputVertices (1GateCircStr (<*z,x*>,and2)) is without_pairs & InputVertices ((1GateCircStr (<*x,y*>,and2c)) +* (1GateCircStr (<*y,z*>,and2a))) is without_pairs )
by FACIRC_1:9, FACIRC_1:41;
then A6:
InputVertices (GFA1CarryIStr (x,y,z)) is without_pairs
by FACIRC_1:9;
InnerVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3)) is Relation
by FACIRC_1:38;
then
InputVertices (GFA1CarryStr (x,y,z)) = (InputVertices (GFA1CarryIStr (x,y,z))) \/ ((InputVertices (1GateCircStr (<*[<*x,y*>,and2c],[<*y,z*>,and2a],[<*z,x*>,and2]*>,or3))) \ (InnerVertices (GFA1CarryIStr (x,y,z))))
by A6, FACIRC_1:6;
hence
contradiction
by A6, A1, A5; verum