let am, bp, cm, dp be non pair set ; :: thesis: for cin being set st cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] & not cin in InnerVertices (BitGFA2Str am,bp,cm) holds
InputVertices (BitFTA2Str am,bp,cm,dp,cin) = {am,bp,cm,dp,cin}
let cin be set ; :: thesis: ( cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] & not cin in InnerVertices (BitGFA2Str am,bp,cm) implies InputVertices (BitFTA2Str am,bp,cm,dp,cin) = {am,bp,cm,dp,cin} )
set S = BitFTA2Str am,bp,cm,dp,cin;
set S1 = BitGFA2Str am,bp,cm;
set A1 = GFA2AdderOutput am,bp,cm;
set C1 = GFA2CarryOutput am,bp,cm;
set S2 = BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp;
set A2 = GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp;
set C2 = GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp;
set ambp0 = [<*am,bp*>,xor2c ];
set ambp = [<*am,bp*>,and2a ];
set bpcm = [<*bp,cm*>,and2c ];
set cmam = [<*cm,am*>,and2b ];
set A1cin0 = [<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ];
set A1cin = [<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ];
set cindp = [<*cin,dp*>,and2a ];
set dpA1 = [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ];
assume A1: ( cin <> [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] & not cin in InnerVertices (BitGFA2Str am,bp,cm) ) ; :: thesis: InputVertices (BitFTA2Str am,bp,cm,dp,cin) = {am,bp,cm,dp,cin}
A3: InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp) misses InputVertices (BitGFA2Str am,bp,cm) by LemmaX32;
A4: InnerVertices (BitGFA2Str am,bp,cm) = (({[<*am,bp*>,xor2c ]} \/ {(GFA2AdderOutput am,bp,cm)}) \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]}) \/ {(GFA2CarryOutput am,bp,cm)} by GFACIRC1:113
.= ({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]}) \/ {(GFA2CarryOutput am,bp,cm)} by ENUMSET1:41
.= {[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ ({[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]} \/ {(GFA2CarryOutput am,bp,cm)}) by XBOOLE_1:4
.= {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ]} \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} by ENUMSET1:46
.= {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} by ENUMSET1:52 ;
GFA2AdderOutput am,bp,cm in {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} by ENUMSET1:def 4;
then A5: {(GFA2AdderOutput am,bp,cm)} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} = {} by ZFMISC_1:68;
A6: not dp in {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} by ENUMSET1:def 4;
A7: {(GFA2AdderOutput am,bp,cm),cin,dp} \ (InnerVertices (BitGFA2Str am,bp,cm)) = ({(GFA2AdderOutput am,bp,cm)} \/ {cin,dp}) \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} by A4, ENUMSET1:42
.= ({(GFA2AdderOutput am,bp,cm)} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}) \/ ({cin,dp} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}) by XBOOLE_1:42
.= ({cin} \/ {dp}) \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} by A5, ENUMSET1:41
.= ({cin} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}) \/ ({dp} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}) by XBOOLE_1:42
.= {cin} \/ ({dp} \ {(GFA2AdderOutput am,bp,cm),[<*am,bp*>,xor2c ],[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}) by A1, A4, ZFMISC_1:67
.= {cin} \/ {dp} by A6, ZFMISC_1:67
.= {cin,dp} by ENUMSET1:41 ;
( BitFTA2Str am,bp,cm,dp,cin = (BitGFA2Str am,bp,cm) +* (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp) & BitGFA2Str am,bp,cm tolerates BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp ) by CIRCCOMB:55;
hence InputVertices (BitFTA2Str am,bp,cm,dp,cin) = (InputVertices (BitGFA2Str am,bp,cm)) \/ ((InputVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp)) \ (InnerVertices (BitGFA2Str am,bp,cm))) by A3, FACIRC_1:4
.= {am,bp,cm} \/ ((InputVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp)) \ (InnerVertices (BitGFA2Str am,bp,cm))) by GFACIRC1:116
.= {am,bp,cm} \/ ({(GFA2AdderOutput am,bp,cm),cin,dp} \ (InnerVertices (BitGFA2Str am,bp,cm))) by A1, LemmaX31, GFACIRC1:78
.= {am,bp,cm,dp,cin} by A7, ENUMSET1:49 ;
:: thesis: verum