let am, bm, cm, dm, cin be set ; ( [<*am,bm*>,xor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput (am,bm,cm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*bm,cm*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cm,am*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput (am,bm,cm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cin,dm*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) )
set S = BitFTA3Str (am,bm,cm,dm,cin);
set A1 = GFA3AdderOutput (am,bm,cm);
set C1 = GFA3CarryOutput (am,bm,cm);
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*>,nor2];
set bmcm = [<*bm,cm*>,nor2];
set cmam = [<*cm,am*>,nor2];
set A1cin0 = [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2];
set A1cin = [<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2];
set cindm = [<*cin,dm*>,nor2];
set dmA1 = [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2];
set p1 = {[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))};
set p2 = {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)),[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))};
A1:
( [<*am,bm*>,xor2] in {[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))} & GFA3AdderOutput (am,bm,cm) in {[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))} )
by ENUMSET1:def 4;
A2:
( [<*am,bm*>,nor2] in {[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))} & [<*bm,cm*>,nor2] in {[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))} )
by ENUMSET1:def 4;
A3:
( [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] in {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)),[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))} & GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)),[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))} )
by ENUMSET1:def 4;
A4:
( [<*cm,am*>,nor2] in {[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))} & GFA3CarryOutput (am,bm,cm) in {[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))} )
by ENUMSET1:def 4;
A5:
( [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] in {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)),[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))} & GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)),[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))} )
by ENUMSET1:def 4;
A6:
( [<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2] in {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)),[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))} & [<*cin,dm*>,nor2] in {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)),[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))} )
by ENUMSET1:def 4;
InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) =
(({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm))} \/ {[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}
by Th31
.=
({[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))} \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}) \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}
by ENUMSET1:12
.=
{[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))} \/ ({[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))} \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))})
by XBOOLE_1:4
.=
{[<*am,bm*>,xor2],(GFA3AdderOutput (am,bm,cm)),[<*am,bm*>,nor2],[<*bm,cm*>,nor2],[<*cm,am*>,nor2],(GFA3CarryOutput (am,bm,cm))} \/ {[<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2],(GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm)),[<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2],[<*cin,dm*>,nor2],[<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2],(GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm))}
by ENUMSET1:12
;
hence
( [<*am,bm*>,xor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput (am,bm,cm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*am,bm*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*bm,cm*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cm,am*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput (am,bm,cm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,xor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3AdderOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*(GFA3AdderOutput (am,bm,cm)),cin*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*cin,dm*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) & GFA3CarryOutput ((GFA3AdderOutput (am,bm,cm)),cin,dm) in InnerVertices (BitFTA3Str (am,bm,cm,dm,cin)) )
by A1, A2, A4, A3, A6, A5, XBOOLE_0:def 3; verum