let ap, bp, cp, dp be non pair set ; :: thesis: for cin being set st cin <> [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] & not cin in InnerVertices (BitGFA0Str ap,bp,cp) holds
InputVertices (BitFTA0Str ap,bp,cp,dp,cin) = {ap,bp,cp,dp,cin}
let cin be set ; :: thesis: ( cin <> [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] & not cin in InnerVertices (BitGFA0Str ap,bp,cp) implies InputVertices (BitFTA0Str ap,bp,cp,dp,cin) = {ap,bp,cp,dp,cin} )
set S = BitFTA0Str ap,bp,cp,dp,cin;
set S1 = BitGFA0Str ap,bp,cp;
set A1 = GFA0AdderOutput ap,bp,cp;
set C1 = GFA0CarryOutput ap,bp,cp;
set S2 = BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp;
set A2 = GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp;
set C2 = GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp;
set apbp0 = [<*ap,bp*>,xor2 ];
set apbp = [<*ap,bp*>,and2 ];
set bpcp = [<*bp,cp*>,and2 ];
set cpap = [<*cp,ap*>,and2 ];
set A1cin0 = [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ];
set A1cin = [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ];
set cindp = [<*cin,dp*>,and2 ];
set dpA1 = [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ];
assume A1: ( cin <> [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] & not cin in InnerVertices (BitGFA0Str ap,bp,cp) ) ; :: thesis: InputVertices (BitFTA0Str ap,bp,cp,dp,cin) = {ap,bp,cp,dp,cin}
then A2: ( dp <> [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ] & GFA0AdderOutput ap,bp,cp <> [<*cin,dp*>,and2 ] & cin <> [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] & dp <> [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ] ) by LemmaX11;
A3: InnerVertices (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) misses InputVertices (BitGFA0Str ap,bp,cp) by LemmaX12;
A4: InnerVertices (BitGFA0Str ap,bp,cp) = (({[<*ap,bp*>,xor2 ]} \/ {(GFA0AdderOutput ap,bp,cp)}) \/ {[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ]}) \/ {(GFA0CarryOutput ap,bp,cp)} by GFACIRC1:39
.= ({[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp)} \/ {[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ]}) \/ {(GFA0CarryOutput ap,bp,cp)} by ENUMSET1:41
.= {[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp)} \/ ({[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ]} \/ {(GFA0CarryOutput ap,bp,cp)}) by XBOOLE_1:4
.= {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ]} \/ {[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} by ENUMSET1:46
.= {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} by ENUMSET1:52 ;
GFA0AdderOutput ap,bp,cp in {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} by ENUMSET1:def 4;
then A5: {(GFA0AdderOutput ap,bp,cp)} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} = {} by ZFMISC_1:68;
A6: not dp in {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} by ENUMSET1:def 4;
A7: {(GFA0AdderOutput ap,bp,cp),cin,dp} \ (InnerVertices (BitGFA0Str ap,bp,cp)) = ({(GFA0AdderOutput ap,bp,cp)} \/ {cin,dp}) \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} by A4, ENUMSET1:42
.= ({(GFA0AdderOutput ap,bp,cp)} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}) \/ ({cin,dp} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}) by XBOOLE_1:42
.= ({cin} \/ {dp}) \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} by A5, ENUMSET1:41
.= ({cin} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}) \/ ({dp} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}) by XBOOLE_1:42
.= {cin} \/ ({dp} \ {(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,xor2 ],[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}) by A1, A4, ZFMISC_1:67
.= {cin} \/ {dp} by A6, ZFMISC_1:67
.= {cin,dp} by ENUMSET1:41 ;
( BitFTA0Str ap,bp,cp,dp,cin = (BitGFA0Str ap,bp,cp) +* (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp) & BitGFA0Str ap,bp,cp tolerates BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp ) by CIRCCOMB:55;
hence InputVertices (BitFTA0Str ap,bp,cp,dp,cin) = (InputVertices (BitGFA0Str ap,bp,cp)) \/ ((InputVertices (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp)) \ (InnerVertices (BitGFA0Str ap,bp,cp))) by A3, FACIRC_1:4
.= {ap,bp,cp} \/ ((InputVertices (BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp)) \ (InnerVertices (BitGFA0Str ap,bp,cp))) by GFACIRC1:42
.= {ap,bp,cp} \/ ({(GFA0AdderOutput ap,bp,cp),cin,dp} \ (InnerVertices (BitGFA0Str ap,bp,cp))) by A2, GFACIRC1:41
.= {ap,bp,cp,dp,cin} by A7, ENUMSET1:49 ;
:: thesis: verum