let am, bm, cm, dm, cin be set ; :: thesis: ( [<*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: 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 ThFTA3S1
.= ({[<*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 ;
( [<*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)} & [<*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)} & [<*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)} & [<*(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)} & [<*(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)} & [<*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;
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, XBOOLE_0:def 3; :: thesis: verum