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*>,nor2] 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 A1 = GFA2AdderOutput (am,bp,cm);
set C1 = GFA2CarryOutput (am,bp,cm);
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*>,nor2];
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*>,nor2],(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*>,nor2],(GFA2CarryOutput (am,bp,cm))} & GFA2AdderOutput (am,bp,cm) in {[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm)),[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(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*>,nor2],(GFA2CarryOutput (am,bp,cm))} & [<*bp,cm*>,and2c] in {[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm)),[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(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*>,nor2] in {[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm)),[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(GFA2CarryOutput (am,bp,cm))} & GFA2CarryOutput (am,bp,cm) in {[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm)),[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(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*>,nor2],(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*>,nor2],(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:12
.=
{[<*am,bp*>,xor2c],(GFA2AdderOutput (am,bp,cm)),[<*am,bp*>,and2a],[<*bp,cm*>,and2c],[<*cm,am*>,nor2],(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*>,nor2],(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:12
;
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*>,nor2] 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