let am, bp, cm, dp, cin be set ; ( [<*am,bp*>,xor2c ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & GFA2AdderOutput am,bp,cm in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*am,bp*>,and2a ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*bp,cm*>,and2c ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*cm,am*>,and2b ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & GFA2CarryOutput am,bp,cm in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*cin,dp*>,and2a ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) )
set S = BitFTA2Str am,bp,cm,dp,cin;
set S1 = BitGFA2Str am,bp,cm;
set A1 = GFA2AdderOutput am,bp,cm;
set C1 = GFA2CarryOutput am,bp,cm;
set S2 = BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp;
set A2 = GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp;
set C2 = GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp;
set ambp0 = [<*am,bp*>,xor2c ];
set ambp = [<*am,bp*>,and2a ];
set bpcm = [<*bp,cm*>,and2c ];
set cmam = [<*cm,am*>,and2b ];
set A1cin0 = [<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ];
set A1cin = [<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ];
set cindp = [<*cin,dp*>,and2a ];
set dpA1 = [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ];
set p1 = {[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm),[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)};
set p2 = {[<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ],(GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp),[<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ],[<*cin,dp*>,and2a ],[<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ],(GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp)};
A1:
( [<*am,bp*>,xor2c ] in {[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm),[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} & GFA2AdderOutput am,bp,cm in {[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm),[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} )
by ENUMSET1:def 4;
A2:
( [<*am,bp*>,and2a ] in {[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm),[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} & [<*bp,cm*>,and2c ] in {[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm),[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} )
by ENUMSET1:def 4;
A3:
( [<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ] in {[<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ],(GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp),[<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ],[<*cin,dp*>,and2a ],[<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ],(GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp)} & GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp in {[<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ],(GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp),[<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ],[<*cin,dp*>,and2a ],[<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ],(GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp)} )
by ENUMSET1:def 4;
A4:
( [<*cm,am*>,and2b ] in {[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm),[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} & GFA2CarryOutput am,bp,cm in {[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm),[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} )
by ENUMSET1:def 4;
A5:
( [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] in {[<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ],(GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp),[<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ],[<*cin,dp*>,and2a ],[<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ],(GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp)} & GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp in {[<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ],(GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp),[<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ],[<*cin,dp*>,and2a ],[<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ],(GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp)} )
by ENUMSET1:def 4;
A6:
( [<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ] in {[<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ],(GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp),[<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ],[<*cin,dp*>,and2a ],[<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ],(GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp)} & [<*cin,dp*>,and2a ] in {[<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ],(GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp),[<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ],[<*cin,dp*>,and2a ],[<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ],(GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp)} )
by ENUMSET1:def 4;
InnerVertices (BitFTA2Str am,bp,cm,dp,cin) =
(({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)}) \/ {[<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ],(GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp)}) \/ {[<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ],[<*cin,dp*>,and2a ],[<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ],(GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp)}
by Th21
.=
({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm),[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} \/ {[<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ],(GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp)}) \/ {[<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ],[<*cin,dp*>,and2a ],[<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ],(GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp)}
by ENUMSET1:52
.=
{[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm),[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} \/ ({[<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ],(GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp)} \/ {[<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ],[<*cin,dp*>,and2a ],[<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ],(GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp)})
by XBOOLE_1:4
.=
{[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm),[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ],(GFA2CarryOutput am,bp,cm)} \/ {[<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ],(GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp),[<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ],[<*cin,dp*>,and2a ],[<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ],(GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp)}
by ENUMSET1:52
;
hence
( [<*am,bp*>,xor2c ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & GFA2AdderOutput am,bp,cm in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*am,bp*>,and2a ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*bp,cm*>,and2c ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*cm,am*>,and2b ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & GFA2CarryOutput am,bp,cm in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*(GFA2AdderOutput am,bp,cm),cin*>,xor2c ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & GFA1AdderOutput (GFA2AdderOutput am,bp,cm),cin,dp in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*(GFA2AdderOutput am,bp,cm),cin*>,and2c ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*cin,dp*>,and2a ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & [<*dp,(GFA2AdderOutput am,bp,cm)*>,and2 ] in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) & GFA1CarryOutput (GFA2AdderOutput am,bp,cm),cin,dp in InnerVertices (BitFTA2Str am,bp,cm,dp,cin) )
by A1, A2, A4, A3, A6, A5, XBOOLE_0:def 3; verum