let ap, bm, cp, dm be non pair set ; :: thesis: for cin being set st cin <> [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ] & not cin in InnerVertices (BitGFA1Str ap,bm,cp) holds
InputVertices (BitFTA1Str ap,bm,cp,dm,cin) = {ap,bm,cp,dm,cin}
let cin be set ; :: thesis: ( cin <> [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ] & not cin in InnerVertices (BitGFA1Str ap,bm,cp) implies InputVertices (BitFTA1Str ap,bm,cp,dm,cin) = {ap,bm,cp,dm,cin} )
set S = BitFTA1Str ap,bm,cp,dm,cin;
set S1 = BitGFA1Str ap,bm,cp;
set A1 = GFA1AdderOutput ap,bm,cp;
set C1 = GFA1CarryOutput ap,bm,cp;
set S2 = BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm;
set A2 = GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm;
set C2 = GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm;
set apbm0 = [<*ap,bm*>,xor2c ];
set apbm = [<*ap,bm*>,and2c ];
set bmcp = [<*bm,cp*>,and2a ];
set cpap = [<*cp,ap*>,and2 ];
set A1cin0 = [<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ];
set A1cin = [<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ];
set cindm = [<*cin,dm*>,and2c ];
set dmA1 = [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ];
assume A1: ( cin <> [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ] & not cin in InnerVertices (BitGFA1Str ap,bm,cp) ) ; :: thesis: InputVertices (BitFTA1Str ap,bm,cp,dm,cin) = {ap,bm,cp,dm,cin}
A3: InnerVertices (BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm) misses InputVertices (BitGFA1Str ap,bm,cp) by LemmaX22;
A4: InnerVertices (BitGFA1Str ap,bm,cp) = (({[<*ap,bm*>,xor2c ]} \/ {(GFA1AdderOutput ap,bm,cp)}) \/ {[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ]}) \/ {(GFA1CarryOutput ap,bm,cp)} by GFACIRC1:76
.= ({[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp)} \/ {[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ]}) \/ {(GFA1CarryOutput ap,bm,cp)} by ENUMSET1:41
.= {[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp)} \/ ({[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ]} \/ {(GFA1CarryOutput ap,bm,cp)}) by XBOOLE_1:4
.= {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ]} \/ {[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} by ENUMSET1:46
.= {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} by ENUMSET1:52 ;
GFA1AdderOutput ap,bm,cp in {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} by ENUMSET1:def 4;
then A5: {(GFA1AdderOutput ap,bm,cp)} \ {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} = {} by ZFMISC_1:68;
A6: not dm in {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} by ENUMSET1:def 4;
A7: {(GFA1AdderOutput ap,bm,cp),cin,dm} \ (InnerVertices (BitGFA1Str ap,bm,cp)) = ({(GFA1AdderOutput ap,bm,cp)} \/ {cin,dm}) \ {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} by A4, ENUMSET1:42
.= ({(GFA1AdderOutput ap,bm,cp)} \ {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)}) \/ ({cin,dm} \ {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)}) by XBOOLE_1:42
.= ({cin} \/ {dm}) \ {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} by A5, ENUMSET1:41
.= ({cin} \ {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)}) \/ ({dm} \ {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)}) by XBOOLE_1:42
.= {cin} \/ ({dm} \ {(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,xor2c ],[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)}) by A1, A4, ZFMISC_1:67
.= {cin} \/ {dm} by A6, ZFMISC_1:67
.= {cin,dm} by ENUMSET1:41 ;
( BitFTA1Str ap,bm,cp,dm,cin = (BitGFA1Str ap,bm,cp) +* (BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm) & BitGFA1Str ap,bm,cp tolerates BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm ) by CIRCCOMB:55;
hence InputVertices (BitFTA1Str ap,bm,cp,dm,cin) = (InputVertices (BitGFA1Str ap,bm,cp)) \/ ((InputVertices (BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm)) \ (InnerVertices (BitGFA1Str ap,bm,cp))) by A3, FACIRC_1:4
.= {ap,bm,cp} \/ ((InputVertices (BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm)) \ (InnerVertices (BitGFA1Str ap,bm,cp))) by GFACIRC1:79
.= {ap,bm,cp} \/ ({(GFA1AdderOutput ap,bm,cp),cin,dm} \ (InnerVertices (BitGFA1Str ap,bm,cp))) by A1, LemmaX21, GFACIRC1:115
.= {ap,bm,cp,dm,cin} by A7, ENUMSET1:49 ;
:: thesis: verum