let ap, bp, cp, dp, cin be set ; :: thesis: ( [<*ap,bp*>,xor2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & GFA0AdderOutput ap,bp,cp in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*ap,bp*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*bp,cp*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*cp,ap*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & GFA0CarryOutput ap,bp,cp in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*cin,dp*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) )
set S = BitFTA0Str ap,bp,cp,dp,cin;
set S1 = BitGFA0Str ap,bp,cp;
set A1 = GFA0AdderOutput ap,bp,cp;
set C1 = GFA0CarryOutput ap,bp,cp;
set S2 = BitGFA0Str (GFA0AdderOutput ap,bp,cp),cin,dp;
set A2 = GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp;
set C2 = GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp;
set apbp0 = [<*ap,bp*>,xor2 ];
set apbp = [<*ap,bp*>,and2 ];
set bpcp = [<*bp,cp*>,and2 ];
set cpap = [<*cp,ap*>,and2 ];
set A1cin0 = [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ];
set A1cin = [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ];
set cindp = [<*cin,dp*>,and2 ];
set dpA1 = [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ];
set p1 = {[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)};
set p2 = {[<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ],(GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp),[<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ],[<*cin,dp*>,and2 ],[<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ],(GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp)};
A1: InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) = (({[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp)} \/ {[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)}) \/ {[<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ],(GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp)}) \/ {[<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ],[<*cin,dp*>,and2 ],[<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ],(GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp)} by ThFTA0S1
.= ({[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} \/ {[<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ],(GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp)}) \/ {[<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ],[<*cin,dp*>,and2 ],[<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ],(GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp)} by ENUMSET1:52
.= {[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} \/ ({[<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ],(GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp)} \/ {[<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ],[<*cin,dp*>,and2 ],[<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ],(GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp)}) by XBOOLE_1:4
.= {[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} \/ {[<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ],(GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp),[<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ],[<*cin,dp*>,and2 ],[<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ],(GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp)} by ENUMSET1:52 ;
( [<*ap,bp*>,xor2 ] in {[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} & GFA0AdderOutput ap,bp,cp in {[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} & [<*ap,bp*>,and2 ] in {[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} & [<*bp,cp*>,and2 ] in {[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} & [<*cp,ap*>,and2 ] in {[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} & GFA0CarryOutput ap,bp,cp in {[<*ap,bp*>,xor2 ],(GFA0AdderOutput ap,bp,cp),[<*ap,bp*>,and2 ],[<*bp,cp*>,and2 ],[<*cp,ap*>,and2 ],(GFA0CarryOutput ap,bp,cp)} & [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ] in {[<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ],(GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp),[<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ],[<*cin,dp*>,and2 ],[<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ],(GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp)} & GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp in {[<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ],(GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp),[<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ],[<*cin,dp*>,and2 ],[<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ],(GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp)} & [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ] in {[<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ],(GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp),[<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ],[<*cin,dp*>,and2 ],[<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ],(GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp)} & [<*cin,dp*>,and2 ] in {[<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ],(GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp),[<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ],[<*cin,dp*>,and2 ],[<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ],(GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp)} & [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] in {[<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ],(GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp),[<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ],[<*cin,dp*>,and2 ],[<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ],(GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp)} & GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp in {[<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ],(GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp),[<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ],[<*cin,dp*>,and2 ],[<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ],(GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp)} ) by ENUMSET1:def 4;
hence ( [<*ap,bp*>,xor2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & GFA0AdderOutput ap,bp,cp in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*ap,bp*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*bp,cp*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*cp,ap*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & GFA0CarryOutput ap,bp,cp in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*(GFA0AdderOutput ap,bp,cp),cin*>,xor2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & GFA0AdderOutput (GFA0AdderOutput ap,bp,cp),cin,dp in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*(GFA0AdderOutput ap,bp,cp),cin*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*cin,dp*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & [<*dp,(GFA0AdderOutput ap,bp,cp)*>,and2 ] in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) & GFA0CarryOutput (GFA0AdderOutput ap,bp,cp),cin,dp in InnerVertices (BitFTA0Str ap,bp,cp,dp,cin) ) by A1, XBOOLE_0:def 3; :: thesis: verum