let ap, bm, cp, dm, cin be set ; :: thesis: ( [<*ap,bm*>,xor2c ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & GFA1AdderOutput ap,bm,cp in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*ap,bm*>,and2c ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*bm,cp*>,and2a ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*cp,ap*>,and2 ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & GFA1CarryOutput ap,bm,cp in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*cin,dm*>,and2c ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) )
set S = BitFTA1Str ap,bm,cp,dm,cin;
set S1 = BitGFA1Str ap,bm,cp;
set A1 = GFA1AdderOutput ap,bm,cp;
set C1 = GFA1CarryOutput ap,bm,cp;
set S2 = BitGFA2Str (GFA1AdderOutput ap,bm,cp),cin,dm;
set A2 = GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm;
set C2 = GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm;
set apbm0 = [<*ap,bm*>,xor2c ];
set apbm = [<*ap,bm*>,and2c ];
set bmcp = [<*bm,cp*>,and2a ];
set cpap = [<*cp,ap*>,and2 ];
set A1cin0 = [<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ];
set A1cin = [<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ];
set cindm = [<*cin,dm*>,and2c ];
set dmA1 = [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ];
set p1 = {[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)};
set p2 = {[<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ],(GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm),[<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ],[<*cin,dm*>,and2c ],[<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)};
A1: InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) = (({[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp)} \/ {[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)}) \/ {[<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ],(GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm)}) \/ {[<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ],[<*cin,dm*>,and2c ],[<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)} by ThFTA1S1
.= ({[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} \/ {[<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ],(GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm)}) \/ {[<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ],[<*cin,dm*>,and2c ],[<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)} by ENUMSET1:52
.= {[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} \/ ({[<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ],(GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm)} \/ {[<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ],[<*cin,dm*>,and2c ],[<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)}) by XBOOLE_1:4
.= {[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} \/ {[<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ],(GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm),[<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ],[<*cin,dm*>,and2c ],[<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)} by ENUMSET1:52 ;
( [<*ap,bm*>,xor2c ] in {[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} & GFA1AdderOutput ap,bm,cp in {[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} & [<*ap,bm*>,and2c ] in {[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} & [<*bm,cp*>,and2a ] in {[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} & [<*cp,ap*>,and2 ] in {[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} & GFA1CarryOutput ap,bm,cp in {[<*ap,bm*>,xor2c ],(GFA1AdderOutput ap,bm,cp),[<*ap,bm*>,and2c ],[<*bm,cp*>,and2a ],[<*cp,ap*>,and2 ],(GFA1CarryOutput ap,bm,cp)} & [<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ] in {[<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ],(GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm),[<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ],[<*cin,dm*>,and2c ],[<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)} & GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm in {[<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ],(GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm),[<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ],[<*cin,dm*>,and2c ],[<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)} & [<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ] in {[<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ],(GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm),[<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ],[<*cin,dm*>,and2c ],[<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)} & [<*cin,dm*>,and2c ] in {[<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ],(GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm),[<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ],[<*cin,dm*>,and2c ],[<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)} & [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ] in {[<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ],(GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm),[<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ],[<*cin,dm*>,and2c ],[<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)} & GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm in {[<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ],(GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm),[<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ],[<*cin,dm*>,and2c ],[<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ],(GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm)} ) by ENUMSET1:def 4;
hence ( [<*ap,bm*>,xor2c ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & GFA1AdderOutput ap,bm,cp in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*ap,bm*>,and2c ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*bm,cp*>,and2a ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*cp,ap*>,and2 ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & GFA1CarryOutput ap,bm,cp in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*(GFA1AdderOutput ap,bm,cp),cin*>,xor2c ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & GFA2AdderOutput (GFA1AdderOutput ap,bm,cp),cin,dm in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*(GFA1AdderOutput ap,bm,cp),cin*>,and2a ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*cin,dm*>,and2c ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & [<*dm,(GFA1AdderOutput ap,bm,cp)*>,and2b ] in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) & GFA2CarryOutput (GFA1AdderOutput ap,bm,cp),cin,dm in InnerVertices (BitFTA1Str ap,bm,cp,dm,cin) ) by A1, XBOOLE_0:def 3; :: thesis: verum