let am, bm, cm, dm be non pair set ; for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & 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 ; ( cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] & 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 ambm0 = [<*am,bm*>,xor2];
set ambm = [<*am,bm*>,nor2];
set bmcm = [<*bm,cm*>,nor2];
set cmam = [<*cm,am*>,nor2];
set cindm = [<*cin,dm*>,nor2];
set dmA1 = [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2];
assume that
A1:
cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2]
and
A2:
not cin in InnerVertices (BitGFA3Str (am,bm,cm))
; InputVertices (BitFTA3Str (am,bm,cm,dm,cin)) = {am,bm,cm,dm,cin}
A3:
not dm in {(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,xor2],[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}
by ENUMSET1:def 4;
GFA3AdderOutput (am,bm,cm) in {(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,xor2],[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}
by ENUMSET1:def 4;
then A4:
{(GFA3AdderOutput (am,bm,cm))} \ {(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,xor2],[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))} = {}
by ZFMISC_1:60;
A5: InnerVertices (BitGFA3Str (am,bm,cm)) =
(({[<*am,bm*>,xor2]} \/ {(GFA3AdderOutput (am,bm,cm))}) \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2]}) \/ {(GFA3CarryOutput (am,bm,cm))}
by GFACIRC1:127
.=
({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2]}) \/ {(GFA3CarryOutput (am,bm,cm))}
by ENUMSET1:1
.=
{[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ ({[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2]} \/ {(GFA3CarryOutput (am,bm,cm))})
by XBOOLE_1:4
.=
{(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,xor2]} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}
by ENUMSET1:6
.=
{(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,xor2],[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}
by ENUMSET1:12
;
then A6: {(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*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}
by ENUMSET1:2
.=
({(GFA3AdderOutput (am,bm,cm))} \ {(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,xor2],[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ ({cin,dm} \ {(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,xor2],[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))})
by XBOOLE_1:42
.=
({cin} \/ {dm}) \ {(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,xor2],[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}
by A4, ENUMSET1:1
.=
({cin} \ {(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,xor2],[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ ({dm} \ {(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,xor2],[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))})
by XBOOLE_1:42
.=
{cin} \/ ({dm} \ {(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,xor2],[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))})
by A2, A5, ZFMISC_1:59
.=
{cin} \/ {dm}
by A3, ZFMISC_1:59
.=
{cin,dm}
by ENUMSET1:1
;
A7:
GFA3AdderOutput (am,bm,cm) <> [<*cin,dm*>,nor2]
by Lm31;
( InnerVertices (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) misses InputVertices (BitGFA3Str (am,bm,cm)) & BitGFA3Str (am,bm,cm) tolerates BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm) )
by Lm32, CIRCCOMB:47;
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 FACIRC_1:4
.=
{am,bm,cm} \/ ((InputVertices (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm))) \ (InnerVertices (BitGFA3Str (am,bm,cm))))
by GFACIRC1:130
.=
{am,bm,cm} \/ ({(GFA3AdderOutput (am,bm,cm)),cin,dm} \ (InnerVertices (BitGFA3Str (am,bm,cm))))
by A1, A7, GFACIRC1:129
.=
{am,bm,cm,dm,cin}
by A6, ENUMSET1:9
;
verum