let am, bm, cm, dm be non pair set ; :: thesis: for cin being set st cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] & not cin in InnerVertices (BitGFA3Str am,bm,cm) holds
InputVertices (BitFTA3Str am,bm,cm,dm,cin) = {am,bm,cm,dm,cin}
let cin be set ; :: thesis: ( cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] & not cin in InnerVertices (BitGFA3Str am,bm,cm) implies InputVertices (BitFTA3Str am,bm,cm,dm,cin) = {am,bm,cm,dm,cin} )
set S = BitFTA3Str am,bm,cm,dm,cin;
set S1 = BitGFA3Str am,bm,cm;
set A1 = GFA3AdderOutput am,bm,cm;
set C1 = GFA3CarryOutput am,bm,cm;
set S2 = BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm;
set A2 = GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm;
set C2 = GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm;
set ambm0 = [<*am,bm*>,xor2 ];
set ambm = [<*am,bm*>,and2b ];
set bmcm = [<*bm,cm*>,and2b ];
set cmam = [<*cm,am*>,and2b ];
set A1cin0 = [<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ];
set A1cin = [<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ];
set cindm = [<*cin,dm*>,and2b ];
set dmA1 = [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ];
assume A1: ( cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] & not cin in InnerVertices (BitGFA3Str am,bm,cm) ) ; :: thesis: InputVertices (BitFTA3Str am,bm,cm,dm,cin) = {am,bm,cm,dm,cin}
then A2: ( dm <> [<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ] & GFA3AdderOutput am,bm,cm <> [<*cin,dm*>,and2b ] & cin <> [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] & dm <> [<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ] ) by LemmaX41;
A3: InnerVertices (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm) misses InputVertices (BitGFA3Str am,bm,cm) by LemmaX42;
A4: InnerVertices (BitGFA3Str am,bm,cm) = (({[<*am,bm*>,xor2 ]} \/ {(GFA3AdderOutput am,bm,cm)}) \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ]}) \/ {(GFA3CarryOutput am,bm,cm)} by GFACIRC1:150
.= ({[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ]}) \/ {(GFA3CarryOutput am,bm,cm)} by ENUMSET1:41
.= {[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm)} \/ ({[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ]} \/ {(GFA3CarryOutput am,bm,cm)}) by XBOOLE_1:4
.= {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ]} \/ {[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} by ENUMSET1:46
.= {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} by ENUMSET1:52 ;
GFA3AdderOutput am,bm,cm in {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} by ENUMSET1:def 4;
then A5: {(GFA3AdderOutput am,bm,cm)} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} = {} by ZFMISC_1:68;
A6: not dm in {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} by ENUMSET1:def 4;
A7: {(GFA3AdderOutput am,bm,cm),cin,dm} \ (InnerVertices (BitGFA3Str am,bm,cm)) = ({(GFA3AdderOutput am,bm,cm)} \/ {cin,dm}) \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} by A4, ENUMSET1:42
.= ({(GFA3AdderOutput am,bm,cm)} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ ({cin,dm} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) by XBOOLE_1:42
.= ({cin} \/ {dm}) \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} by A5, ENUMSET1:41
.= ({cin} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ ({dm} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) by XBOOLE_1:42
.= {cin} \/ ({dm} \ {(GFA3AdderOutput am,bm,cm),[<*am,bm*>,xor2 ],[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) by A1, A4, ZFMISC_1:67
.= {cin} \/ {dm} by A6, ZFMISC_1:67
.= {cin,dm} by ENUMSET1:41 ;
( BitFTA3Str am,bm,cm,dm,cin = (BitGFA3Str am,bm,cm) +* (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm) & BitGFA3Str am,bm,cm tolerates BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm ) by CIRCCOMB:55;
hence InputVertices (BitFTA3Str am,bm,cm,dm,cin) = (InputVertices (BitGFA3Str am,bm,cm)) \/ ((InputVertices (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm)) \ (InnerVertices (BitGFA3Str am,bm,cm))) by A3, FACIRC_1:4
.= {am,bm,cm} \/ ((InputVertices (BitGFA3Str (GFA3AdderOutput am,bm,cm),cin,dm)) \ (InnerVertices (BitGFA3Str am,bm,cm))) by GFACIRC1:153
.= {am,bm,cm} \/ ({(GFA3AdderOutput am,bm,cm),cin,dm} \ (InnerVertices (BitGFA3Str am,bm,cm))) by A2, GFACIRC1:152
.= {am,bm,cm,dm,cin} by A7, ENUMSET1:49 ;
:: thesis: verum