let am, bp, cm, dp, cin be set ; :: thesis: 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)}
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 ];
( BitFTA2Str am,bp,cm,dp,cin = (BitGFA2Str am,bp,cm) +* (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp) & BitGFA2Str am,bp,cm tolerates BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp ) by CIRCCOMB:55;
hence InnerVertices (BitFTA2Str am,bp,cm,dp,cin) = (InnerVertices (BitGFA2Str am,bp,cm)) \/ (InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp)) by CIRCCOMB:15
.= ((({[<*am,bp*>,xor2c ]} \/ {(GFA2AdderOutput am,bp,cm)}) \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]}) \/ {(GFA2CarryOutput am,bp,cm)}) \/ (InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp)) by GFACIRC1:113
.= (({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ {[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]}) \/ {(GFA2CarryOutput am,bp,cm)}) \/ (InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp)) by ENUMSET1:41
.= ({[<*am,bp*>,xor2c ],(GFA2AdderOutput am,bp,cm)} \/ ({[<*am,bp*>,and2a ],[<*bp,cm*>,and2c ],[<*cm,am*>,and2b ]} \/ {(GFA2CarryOutput am,bp,cm)})) \/ (InnerVertices (BitGFA1Str (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)}) \/ (InnerVertices (BitGFA1Str (GFA2AdderOutput am,bp,cm),cin,dp)) by ENUMSET1:46
.= ({[<*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 GFACIRC1:76
.= ({[<*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:41
.= ({[<*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:46
.= (({[<*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 ;
:: thesis: verum