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*>,and2b ] in InnerVertices (BitFTA3Str am,bm,cm,dm,cin) & [<*bm,cm*>,and2b ] in InnerVertices (BitFTA3Str am,bm,cm,dm,cin) & [<*cm,am*>,and2b ] 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*>,and2b ] in InnerVertices (BitFTA3Str am,bm,cm,dm,cin) & [<*cin,dm*>,and2b ] in InnerVertices (BitFTA3Str am,bm,cm,dm,cin) & [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] 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 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 ];
set p1 = {[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm),[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)};
set p2 = {[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm),[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)};
A1:
( [<*am,bm*>,xor2 ] in {[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm),[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} & GFA3AdderOutput am,bm,cm in {[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm),[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} )
by ENUMSET1:def 4;
A2:
( [<*am,bm*>,and2b ] in {[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm),[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} & [<*bm,cm*>,and2b ] in {[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm),[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(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*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(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*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)} )
by ENUMSET1:def 4;
A4:
( [<*cm,am*>,and2b ] in {[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm),[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} & GFA3CarryOutput am,bm,cm in {[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm),[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} )
by ENUMSET1:def 4;
A5:
( [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] in {[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm),[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(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*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)} )
by ENUMSET1:def 4;
A6:
( [<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ] in {[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm),[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)} & [<*cin,dm*>,and2b ] in {[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm),[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(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*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)}) \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm)}) \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)}
by Th31
.=
({[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm),[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm)}) \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)}
by ENUMSET1:52
.=
{[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm),[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} \/ ({[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm)} \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)})
by XBOOLE_1:4
.=
{[<*am,bm*>,xor2 ],(GFA3AdderOutput am,bm,cm),[<*am,bm*>,and2b ],[<*bm,cm*>,and2b ],[<*cm,am*>,and2b ],(GFA3CarryOutput am,bm,cm)} \/ {[<*(GFA3AdderOutput am,bm,cm),cin*>,xor2 ],(GFA3AdderOutput (GFA3AdderOutput am,bm,cm),cin,dm),[<*(GFA3AdderOutput am,bm,cm),cin*>,and2b ],[<*cin,dm*>,and2b ],[<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ],(GFA3CarryOutput (GFA3AdderOutput am,bm,cm),cin,dm)}
by ENUMSET1:52
;
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*>,and2b ] in InnerVertices (BitFTA3Str am,bm,cm,dm,cin) & [<*bm,cm*>,and2b ] in InnerVertices (BitFTA3Str am,bm,cm,dm,cin) & [<*cm,am*>,and2b ] 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*>,and2b ] in InnerVertices (BitFTA3Str am,bm,cm,dm,cin) & [<*cin,dm*>,and2b ] in InnerVertices (BitFTA3Str am,bm,cm,dm,cin) & [<*dm,(GFA3AdderOutput am,bm,cm)*>,and2b ] 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