ftacell1.miz



    begin

    definition

      let ap,bp,cp,dp,cin be set;

      :: FTACELL1:def1

      func BitFTA0Str (ap,bp,cp,dp,cin) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( BitGFA0Str (ap,bp,cp)) +* ( BitGFA0Str (( GFA0AdderOutput (ap,bp,cp)),cin,dp)));

      coherence ;

    end

    definition

      let ap,bp,cp,dp,cin be set;

      :: FTACELL1:def2

      func BitFTA0Circ (ap,bp,cp,dp,cin) -> strict Boolean gate`2=den Circuit of ( BitFTA0Str (ap,bp,cp,dp,cin)) equals (( BitGFA0Circ (ap,bp,cp)) +* ( BitGFA0Circ (( GFA0AdderOutput (ap,bp,cp)),cin,dp)));

      coherence ;

    end

    theorem :: FTACELL1:1

    

     Th1: for ap,bp,cp,dp,cin be set holds ( 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))})

    proof

      let ap,bp,cp,dp,cin be set;

      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 (A1,cin,dp));

      set A2 = ( GFA0AdderOutput (A1,cin,dp));

      set C2 = ( GFA0CarryOutput (A1,cin,dp));

      set apbp0 = [ <*ap, bp*>, xor2 ];

      set apbp = [ <*ap, bp*>, and2 ];

      set bpcp = [ <*bp, cp*>, and2 ];

      set cpap = [ <*cp, ap*>, and2 ];

      set A1cin0 = [ <*A1, cin*>, xor2 ];

      set A1cin = [ <*A1, cin*>, and2 ];

      set cindp = [ <*cin, dp*>, and2 ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      S1 tolerates S2 by CIRCCOMB: 47;

      

      hence ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by CIRCCOMB: 11

      .= (((( {apbp0} \/ {A1}) \/ {apbp, bpcp, cpap}) \/ {C1}) \/ ( InnerVertices S2)) by GFACIRC1: 31

      .= ((( {apbp0, A1} \/ {apbp, bpcp, cpap}) \/ {C1}) \/ ( InnerVertices S2)) by ENUMSET1: 1

      .= (( {apbp0, A1} \/ ( {apbp, bpcp, cpap} \/ {C1})) \/ ( InnerVertices S2)) by XBOOLE_1: 4

      .= (( {apbp0, A1} \/ {apbp, bpcp, cpap, C1}) \/ ( InnerVertices S2)) by ENUMSET1: 6

      .= (( {apbp0, A1} \/ {apbp, bpcp, cpap, C1}) \/ ((( {A1cin0} \/ {A2}) \/ {A1cin, cindp, dpA1}) \/ {C2})) by GFACIRC1: 31

      .= (( {apbp0, A1} \/ {apbp, bpcp, cpap, C1}) \/ (( {A1cin0, A2} \/ {A1cin, cindp, dpA1}) \/ {C2})) by ENUMSET1: 1

      .= (( {apbp0, A1} \/ {apbp, bpcp, cpap, C1}) \/ ( {A1cin0, A2} \/ ( {A1cin, cindp, dpA1} \/ {C2}))) by XBOOLE_1: 4

      .= (( {apbp0, A1} \/ {apbp, bpcp, cpap, C1}) \/ ( {A1cin0, A2} \/ {A1cin, cindp, dpA1, C2})) by ENUMSET1: 6

      .= ((( {apbp0, A1} \/ {apbp, bpcp, cpap, C1}) \/ {A1cin0, A2}) \/ {A1cin, cindp, dpA1, C2}) by XBOOLE_1: 4;

    end;

    theorem :: FTACELL1:2

    for ap,bp,cp,dp,cin be set holds ( InnerVertices ( BitFTA0Str (ap,bp,cp,dp,cin))) is Relation

    proof

      let ap,bp,cp,dp,cin be set;

      set S1 = ( BitGFA0Str (ap,bp,cp));

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set S2 = ( BitGFA0Str (A1,cin,dp));

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by GFACIRC1: 32;

      hence thesis by FACIRC_1: 3;

    end;

    

     Lm1: for x,y,z be set holds for p be set holds ( GFA0AdderOutput (x,y,z)) <> [p, and2 ]

    proof

      let x,y,z be set, p be set;

      set A1 = ( GFA0AdderOutput (x,y,z));

      (A1 `2 ) = xor2 ;

      then ( [p, and2 ] `2 ) <> (A1 `2 ) by TWOSCOMP: 9, TWOSCOMP: 11;

      hence thesis;

    end;

    

     Lm2: for ap,bp,cp be non pair set holds for x,y,z be set holds ( InputVertices ( BitGFA0Str (ap,bp,cp))) misses ( InnerVertices ( BitGFA0Str (x,y,z)))

    proof

      let ap,bp,cp be non pair set;

      let x,y,z be set;

      set S1 = ( BitGFA0Str (ap,bp,cp));

      ( InputVertices S1) is without_pairs by GFACIRC1: 35;

      hence thesis by FACIRC_1: 5, GFACIRC1: 32;

    end;

    theorem :: FTACELL1:3

    

     Th3: for ap,bp,cp,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp))) holds ( InputVertices ( BitFTA0Str (ap,bp,cp,dp,cin))) = {ap, bp, cp, dp, cin}

    proof

      let ap,bp,cp,dp be non pair set;

      let cin be set;

      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 (A1,cin,dp));

      set apbp0 = [ <*ap, bp*>, xor2 ];

      set apbp = [ <*ap, bp*>, and2 ];

      set bpcp = [ <*bp, cp*>, and2 ];

      set cpap = [ <*cp, ap*>, and2 ];

      set cindp = [ <*cin, dp*>, and2 ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      assume that

       A1: cin <> dpA1 and

       A2: not cin in ( InnerVertices S1);

      

       A3: not dp in {A1, apbp0, apbp, bpcp, cpap, C1} by ENUMSET1:def 4;

      A1 in {A1, apbp0, apbp, bpcp, cpap, C1} by ENUMSET1:def 4;

      then

       A4: ( {A1} \ {A1, apbp0, apbp, bpcp, cpap, C1}) = {} by ZFMISC_1: 60;

      

       A5: ( InnerVertices S1) = ((( {apbp0} \/ {A1}) \/ {apbp, bpcp, cpap}) \/ {C1}) by GFACIRC1: 31

      .= (( {apbp0, A1} \/ {apbp, bpcp, cpap}) \/ {C1}) by ENUMSET1: 1

      .= ( {apbp0, A1} \/ ( {apbp, bpcp, cpap} \/ {C1})) by XBOOLE_1: 4

      .= ( {A1, apbp0} \/ {apbp, bpcp, cpap, C1}) by ENUMSET1: 6

      .= {A1, apbp0, apbp, bpcp, cpap, C1} by ENUMSET1: 12;

      

      then

       A6: ( {A1, cin, dp} \ ( InnerVertices S1)) = (( {A1} \/ {cin, dp}) \ {A1, apbp0, apbp, bpcp, cpap, C1}) by ENUMSET1: 2

      .= (( {A1} \ {A1, apbp0, apbp, bpcp, cpap, C1}) \/ ( {cin, dp} \ {A1, apbp0, apbp, bpcp, cpap, C1})) by XBOOLE_1: 42

      .= (( {cin} \/ {dp}) \ {A1, apbp0, apbp, bpcp, cpap, C1}) by A4, ENUMSET1: 1

      .= (( {cin} \ {A1, apbp0, apbp, bpcp, cpap, C1}) \/ ( {dp} \ {A1, apbp0, apbp, bpcp, cpap, C1})) by XBOOLE_1: 42

      .= ( {cin} \/ ( {dp} \ {A1, apbp0, apbp, bpcp, cpap, C1})) by A2, A5, ZFMISC_1: 59

      .= ( {cin} \/ {dp}) by A3, ZFMISC_1: 59

      .= {cin, dp} by ENUMSET1: 1;

      

       A7: A1 <> cindp by Lm1;

      ( InnerVertices S2) misses ( InputVertices S1) & S1 tolerates S2 by Lm2, CIRCCOMB: 47;

      

      hence ( InputVertices S) = (( InputVertices S1) \/ (( InputVertices S2) \ ( InnerVertices S1))) by FACIRC_1: 4

      .= ( {ap, bp, cp} \/ (( InputVertices S2) \ ( InnerVertices S1))) by GFACIRC1: 34

      .= ( {ap, bp, cp} \/ ( {A1, cin, dp} \ ( InnerVertices S1))) by A1, A7, GFACIRC1: 33

      .= {ap, bp, cp, dp, cin} by A6, ENUMSET1: 9;

    end;

    theorem :: FTACELL1:4

    

     Th4: for ap,bp,cp,dp,cin be set holds ap in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & bp in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & cp in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & dp in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & cin in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & [ <*ap, bp*>, xor2 ] in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & ( GFA0AdderOutput (ap,bp,cp)) in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & [ <*ap, bp*>, and2 ] in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & [ <*bp, cp*>, and2 ] in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & [ <*cp, ap*>, and2 ] in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & ( GFA0CarryOutput (ap,bp,cp)) in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & [ <*( GFA0AdderOutput (ap,bp,cp)), cin*>, xor2 ] in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & ( GFA0AdderOutput (( GFA0AdderOutput (ap,bp,cp)),cin,dp)) in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & [ <*( GFA0AdderOutput (ap,bp,cp)), cin*>, and2 ] in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & [ <*cin, dp*>, and2 ] in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin)) & ( GFA0CarryOutput (( GFA0AdderOutput (ap,bp,cp)),cin,dp)) in the carrier of ( BitFTA0Str (ap,bp,cp,dp,cin))

    proof

      let ap,bp,cp,dp,cin be set;

      set S1 = ( BitGFA0Str (ap,bp,cp));

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set C1 = ( GFA0CarryOutput (ap,bp,cp));

      set S2 = ( BitGFA0Str (A1,cin,dp));

      set A2 = ( GFA0AdderOutput (A1,cin,dp));

      set C2 = ( GFA0CarryOutput (A1,cin,dp));

      set apbp0 = [ <*ap, bp*>, xor2 ];

      set apbp = [ <*ap, bp*>, and2 ];

      set bpcp = [ <*bp, cp*>, and2 ];

      set cpap = [ <*cp, ap*>, and2 ];

      set A1cin0 = [ <*A1, cin*>, xor2 ];

      set A1cin = [ <*A1, cin*>, and2 ];

      set cindp = [ <*cin, dp*>, and2 ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      

       A1: cp in the carrier of S1 & apbp0 in the carrier of S1 by GFACIRC1: 36;

      

       A2: apbp in the carrier of S1 & bpcp in the carrier of S1 by GFACIRC1: 36;

      

       A3: A1 in the carrier of S2 & cin in the carrier of S2 by GFACIRC1: 36;

      

       A4: cpap in the carrier of S1 & C1 in the carrier of S1 by GFACIRC1: 36;

      

       A5: C2 in the carrier of S2 by GFACIRC1: 36;

      

       A6: cindp in the carrier of S2 & dpA1 in the carrier of S2 by GFACIRC1: 36;

      

       A7: A2 in the carrier of S2 & A1cin in the carrier of S2 by GFACIRC1: 36;

      

       A8: dp in the carrier of S2 & A1cin0 in the carrier of S2 by GFACIRC1: 36;

      ap in the carrier of S1 & bp in the carrier of S1 by GFACIRC1: 36;

      hence thesis by A1, A2, A4, A3, A8, A7, A6, A5, FACIRC_1: 20;

    end;

    theorem :: FTACELL1:5

    

     Th5: for ap,bp,cp,dp,cin be set holds [ <*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)))

    proof

      let ap,bp,cp,dp,cin be set;

      set S = ( BitFTA0Str (ap,bp,cp,dp,cin));

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set C1 = ( GFA0CarryOutput (ap,bp,cp));

      set A2 = ( GFA0AdderOutput (A1,cin,dp));

      set C2 = ( GFA0CarryOutput (A1,cin,dp));

      set apbp0 = [ <*ap, bp*>, xor2 ];

      set apbp = [ <*ap, bp*>, and2 ];

      set bpcp = [ <*bp, cp*>, and2 ];

      set cpap = [ <*cp, ap*>, and2 ];

      set A1cin0 = [ <*A1, cin*>, xor2 ];

      set A1cin = [ <*A1, cin*>, and2 ];

      set cindp = [ <*cin, dp*>, and2 ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      set p1 = {apbp0, A1, apbp, bpcp, cpap, C1};

      set p2 = {A1cin0, A2, A1cin, cindp, dpA1, C2};

      

       A1: apbp0 in p1 & A1 in p1 by ENUMSET1:def 4;

      

       A2: apbp in p1 & bpcp in p1 by ENUMSET1:def 4;

      

       A3: A1cin0 in p2 & A2 in p2 by ENUMSET1:def 4;

      

       A4: cpap in p1 & C1 in p1 by ENUMSET1:def 4;

      

       A5: dpA1 in p2 & C2 in p2 by ENUMSET1:def 4;

      

       A6: A1cin in p2 & cindp in p2 by ENUMSET1:def 4;

      ( InnerVertices S) = ((( {apbp0, A1} \/ {apbp, bpcp, cpap, C1}) \/ {A1cin0, A2}) \/ {A1cin, cindp, dpA1, C2}) by Th1

      .= ((p1 \/ {A1cin0, A2}) \/ {A1cin, cindp, dpA1, C2}) by ENUMSET1: 12

      .= (p1 \/ ( {A1cin0, A2} \/ {A1cin, cindp, dpA1, C2})) by XBOOLE_1: 4

      .= (p1 \/ p2) by ENUMSET1: 12;

      hence thesis by A1, A2, A4, A3, A6, A5, XBOOLE_0:def 3;

    end;

    theorem :: FTACELL1:6

    

     Th6: for ap,bp,cp,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp))) holds ap in ( InputVertices ( BitFTA0Str (ap,bp,cp,dp,cin))) & bp in ( InputVertices ( BitFTA0Str (ap,bp,cp,dp,cin))) & cp in ( InputVertices ( BitFTA0Str (ap,bp,cp,dp,cin))) & dp in ( InputVertices ( BitFTA0Str (ap,bp,cp,dp,cin))) & cin in ( InputVertices ( BitFTA0Str (ap,bp,cp,dp,cin)))

    proof

      let ap,bp,cp,dp be non pair set;

      let cin be set;

      set S = ( BitFTA0Str (ap,bp,cp,dp,cin));

      set S1 = ( BitGFA0Str (ap,bp,cp));

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set dpA1 = [ <*dp, A1*>, and2 ];

      assume cin <> dpA1 & not cin in ( InnerVertices S1);

      then ( InputVertices S) = {ap, bp, cp, dp, cin} by Th3;

      hence thesis by ENUMSET1:def 3;

    end;

    definition

      let ap,bp,cp,dp,cin be set;

      :: FTACELL1:def3

      func BitFTA0CarryOutput (ap,bp,cp,dp,cin) -> Element of ( InnerVertices ( BitFTA0Str (ap,bp,cp,dp,cin))) equals ( GFA0CarryOutput (ap,bp,cp));

      coherence by Th5;

      :: FTACELL1:def4

      func BitFTA0AdderOutputI (ap,bp,cp,dp,cin) -> Element of ( InnerVertices ( BitFTA0Str (ap,bp,cp,dp,cin))) equals ( GFA0AdderOutput (ap,bp,cp));

      coherence by Th5;

      :: FTACELL1:def5

      func BitFTA0AdderOutputP (ap,bp,cp,dp,cin) -> Element of ( InnerVertices ( BitFTA0Str (ap,bp,cp,dp,cin))) equals ( GFA0CarryOutput (( GFA0AdderOutput (ap,bp,cp)),cin,dp));

      coherence by Th5;

      :: FTACELL1:def6

      func BitFTA0AdderOutputQ (ap,bp,cp,dp,cin) -> Element of ( InnerVertices ( BitFTA0Str (ap,bp,cp,dp,cin))) equals ( GFA0AdderOutput (( GFA0AdderOutput (ap,bp,cp)),cin,dp));

      coherence by Th5;

    end

    theorem :: FTACELL1:7

    for ap,bp,cp be non pair set holds for dp,cin be set holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bp) & a3 = (s . cp) holds (( Following (s,2)) . ( BitFTA0CarryOutput (ap,bp,cp,dp,cin))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) & (( Following (s,2)) . ( BitFTA0AdderOutputI (ap,bp,cp,dp,cin))) = ((a1 'xor' a2) 'xor' a3)

    proof

      let ap,bp,cp be non pair set;

      let dp,cin be set;

      let s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin));

      set S1 = ( BitGFA0Str (ap,bp,cp));

      set C1 = ( BitGFA0Circ (ap,bp,cp));

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set A2 = ( GFA0CarryOutput (ap,bp,cp));

      set S2 = ( BitGFA0Str (A1,cin,dp));

      set C2 = ( BitGFA0Circ (A1,cin,dp));

      let a1,a2,a3 be Element of BOOLEAN such that

       A1: a1 = (s . ap) and

       A2: a2 = (s . bp) and

       A3: a3 = (s . cp);

      reconsider s1 = (s | the carrier of S1) as State of C1 by FACIRC_1: 26;

      

       A4: ( dom s1) = the carrier of S1 by CIRCUIT1: 3;

      ap in the carrier of S1 by GFACIRC1: 36;

      then

       A5: a1 = (s1 . ap) by A1, A4, FUNCT_1: 47;

      reconsider t = s as State of (C1 +* C2);

      

       A6: ( InputVertices S1) misses ( InnerVertices S2) by Lm2;

      cp in the carrier of S1 by GFACIRC1: 36;

      then

       A7: a3 = (s1 . cp) by A3, A4, FUNCT_1: 47;

      bp in the carrier of S1 by GFACIRC1: 36;

      then

       A8: a2 = (s1 . bp) by A2, A4, FUNCT_1: 47;

      A2 in the carrier of S1 by GFACIRC1: 36;

      then (( Following (t,2)) . ( GFA0CarryOutput (ap,bp,cp))) = (( Following (s1,2)) . ( GFA0CarryOutput (ap,bp,cp))) by A6, FACIRC_1: 32;

      hence (( Following (s,2)) . ( BitFTA0CarryOutput (ap,bp,cp,dp,cin))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) by A5, A8, A7, GFACIRC1: 39;

      A1 in the carrier of S1 by GFACIRC1: 36;

      then (( Following (t,2)) . ( GFA0AdderOutput (ap,bp,cp))) = (( Following (s1,2)) . ( GFA0AdderOutput (ap,bp,cp))) by A6, FACIRC_1: 32;

      hence thesis by A5, A8, A7, GFACIRC1: 39;

    end;

    theorem :: FTACELL1:8

    

     Th8: for ap,bp,cp,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp))) holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bp) & a3 = (s . cp) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,2)) . ( GFA0AdderOutput (ap,bp,cp))) = ((a1 'xor' a2) 'xor' a3) & (( Following (s,2)) . ap) = a1 & (( Following (s,2)) . bp) = a2 & (( Following (s,2)) . cp) = a3 & (( Following (s,2)) . dp) = a4 & (( Following (s,2)) . cin) = a5

    proof

      let ap,bp,cp,dp be non pair set;

      let cin be set such that

       A1: cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp)));

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set C1 = ( BitGFA0Circ (ap,bp,cp));

      set S1 = ( BitGFA0Str (ap,bp,cp));

      set S2 = ( BitGFA0Str (A1,cin,dp));

      set C2 = ( BitGFA0Circ (A1,cin,dp));

      set S = ( BitFTA0Str (ap,bp,cp,dp,cin));

      let s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A2: a1 = (s . ap) and

       A3: a2 = (s . bp) and

       A4: a3 = (s . cp) and

       A5: a4 = (s . dp) and

       A6: a5 = (s . cin);

      reconsider s1 = (s | the carrier of S1) as State of C1 by FACIRC_1: 26;

      

       A7: ( dom s1) = the carrier of S1 by CIRCUIT1: 3;

      

       A8: dp in ( InputVertices S) by A1, Th6;

      then

       A9: (( Following s) . dp) = a4 by A5, CIRCUIT2:def 5;

      

       A10: cp in ( InputVertices S) by A1, Th6;

      then

       A11: (( Following s) . cp) = a3 by A4, CIRCUIT2:def 5;

      bp in the carrier of S1 by GFACIRC1: 36;

      then

       A12: a2 = (s1 . bp) by A3, A7, FUNCT_1: 47;

      reconsider t = s as State of (C1 +* C2);

      A1 in the carrier of S1 & ( InputVertices S1) misses ( InnerVertices S2) by Lm2, GFACIRC1: 36;

      then

       A13: (( Following (t,2)) . ( GFA0AdderOutput (ap,bp,cp))) = (( Following (s1,2)) . ( GFA0AdderOutput (ap,bp,cp))) by FACIRC_1: 32;

      cp in the carrier of S1 by GFACIRC1: 36;

      then

       A14: a3 = (s1 . cp) by A4, A7, FUNCT_1: 47;

      ap in the carrier of S1 by GFACIRC1: 36;

      then a1 = (s1 . ap) by A2, A7, FUNCT_1: 47;

      hence (( Following (s,2)) . ( GFA0AdderOutput (ap,bp,cp))) = ((a1 'xor' a2) 'xor' a3) by A12, A14, A13, GFACIRC1: 39;

      

       A15: bp in ( InputVertices S) by A1, Th6;

      then

       A16: (( Following s) . bp) = a2 by A3, CIRCUIT2:def 5;

      

       A17: cin in ( InputVertices S) by A1, Th6;

      then

       A18: (( Following s) . cin) = a5 by A6, CIRCUIT2:def 5;

      

       A19: ap in ( InputVertices S) by A1, Th6;

      then ( Following (s,2)) = ( Following ( Following s)) & (( Following s) . ap) = a1 by A2, CIRCUIT2:def 5, FACIRC_1: 15;

      hence thesis by A19, A15, A10, A8, A17, A16, A11, A9, A18, CIRCUIT2:def 5;

    end;

    

     Lm3: for ap,bp,cp,dp be non pair set holds for cin be set holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds for a123,a4,a5 be Element of BOOLEAN st a123 = (s . ( GFA0AdderOutput (ap,bp,cp))) & a4 = (s . dp) & a5 = (s . cin) holds (( Following s) . [ <*( GFA0AdderOutput (ap,bp,cp)), cin*>, and2 ]) = (a123 '&' a5) & (( Following s) . [ <*cin, dp*>, and2 ]) = (a5 '&' a4) & (( Following s) . [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ]) = (a4 '&' a123)

    proof

      let ap,bp,cp,dp be non pair set;

      let cin be set;

      set S = ( BitFTA0Str (ap,bp,cp,dp,cin));

      set C = ( BitFTA0Circ (ap,bp,cp,dp,cin));

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set A1cin = [ <*A1, cin*>, and2 ];

      set cindp = [ <*cin, dp*>, and2 ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      let s be State of C;

      let a123,a4,a5 be Element of BOOLEAN such that

       A1: a123 = (s . A1) and

       A2: a4 = (s . dp) and

       A3: a5 = (s . cin);

      

       A4: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A5: cin in the carrier of S by Th4;

      

       A6: A1 in the carrier of S by Th4;

      

       A7: ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A1cin in the carrier' of S by Th5;

      

      hence (( Following s) . A1cin) = ( and2 . (s * <*A1, cin*>)) by FACIRC_1: 35

      .= ( and2 . <*a123, a5*>) by A1, A3, A6, A5, A4, FINSEQ_2: 125

      .= (a123 '&' a5) by FACIRC_1:def 6;

      

       A8: dp in the carrier of S by Th4;

      cindp in the carrier' of S by A7, Th5;

      

      hence (( Following s) . cindp) = ( and2 . (s * <*cin, dp*>)) by FACIRC_1: 35

      .= ( and2 . <*a5, a4*>) by A2, A3, A8, A5, A4, FINSEQ_2: 125

      .= (a5 '&' a4) by FACIRC_1:def 6;

      dpA1 in the carrier' of S by A7, Th5;

      

      hence (( Following s) . dpA1) = ( and2 . (s * <*dp, A1*>)) by FACIRC_1: 35

      .= ( and2 . <*a4, a123*>) by A1, A2, A6, A8, A4, FINSEQ_2: 125

      .= (a4 '&' a123) by FACIRC_1:def 6;

    end;

    

     Lm4: for ap,bp,cp,dp be non pair set holds for cin be set holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds for a123,a5 be Element of BOOLEAN st a123 = (s . ( GFA0AdderOutput (ap,bp,cp))) & a5 = (s . cin) holds (( Following s) . [ <*( GFA0AdderOutput (ap,bp,cp)), cin*>, xor2 ]) = (a123 'xor' a5)

    proof

      let ap,bp,cp,dp be non pair set;

      let cin be set;

      set S = ( BitFTA0Str (ap,bp,cp,dp,cin));

      set C = ( BitFTA0Circ (ap,bp,cp,dp,cin));

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set A1cin = [ <*A1, cin*>, xor2 ];

      let s be State of C;

      let a123,a5 be Element of BOOLEAN such that

       A1: a123 = (s . A1) & a5 = (s . cin);

      

       A2: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A3: A1 in the carrier of S & cin in the carrier of S by Th4;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A1cin in the carrier' of S by Th5;

      

      hence (( Following s) . A1cin) = ( xor2 . (s * <*A1, cin*>)) by FACIRC_1: 35

      .= ( xor2 . <*a123, a5*>) by A1, A3, A2, FINSEQ_2: 125

      .= (a123 'xor' a5) by FACIRC_1:def 4;

    end;

    

     Lm5: for ap,bp,cp,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp))) holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bp) & a3 = (s . cp) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,3)) . [ <*( GFA0AdderOutput (ap,bp,cp)), cin*>, and2 ]) = (((a1 'xor' a2) 'xor' a3) '&' a5) & (( Following (s,3)) . [ <*cin, dp*>, and2 ]) = (a5 '&' a4) & (( Following (s,3)) . [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ]) = (a4 '&' ((a1 'xor' a2) 'xor' a3)) & (( Following (s,3)) . ap) = a1 & (( Following (s,3)) . bp) = a2 & (( Following (s,3)) . cp) = a3 & (( Following (s,3)) . dp) = a4 & (( Following (s,3)) . cin) = a5

    proof

      let ap,bp,cp,dp be non pair set;

      let cin be set such that

       A1: cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp)));

      set S = ( BitFTA0Str (ap,bp,cp,dp,cin));

      

       A2: ap in ( InputVertices S) & bp in ( InputVertices S) by A1, Th6;

      

       A3: cp in ( InputVertices S) & dp in ( InputVertices S) by A1, Th6;

      let s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . ap) & a2 = (s . bp) & a3 = (s . cp) & a4 = (s . dp) & a5 = (s . cin);

      

       A5: (( Following (s,2)) . cin) = a5 by A1, A4, Th8;

      set cindp = [ <*cin, dp*>, and2 ];

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set A1cin = [ <*A1, cin*>, and2 ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      

       A6: ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) by FACIRC_1: 12;

      (( Following (s,2)) . A1) = ((a1 'xor' a2) 'xor' a3) & (( Following (s,2)) . dp) = a4 by A1, A4, Th8;

      hence (( Following (s,3)) . A1cin) = (((a1 'xor' a2) 'xor' a3) '&' a5) & (( Following (s,3)) . cindp) = (a5 '&' a4) & (( Following (s,3)) . dpA1) = (a4 '&' ((a1 'xor' a2) 'xor' a3)) by A6, A5, Lm3;

      

       A7: (( Following (s,2)) . cp) = a3 & (( Following (s,2)) . dp) = a4 by A1, A4, Th8;

      

       A8: (( Following (s,2)) . cin) = a5 by A1, A4, Th8;

      

       A9: cin in ( InputVertices S) by A1, Th6;

      (( Following (s,2)) . ap) = a1 & (( Following (s,2)) . bp) = a2 by A1, A4, Th8;

      hence thesis by A6, A2, A3, A9, A7, A8, CIRCUIT2:def 5;

    end;

    

     Lm6: for ap,bp,cp,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp))) holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bp) & a3 = (s . cp) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,3)) . [ <*( GFA0AdderOutput (ap,bp,cp)), cin*>, xor2 ]) = (((a1 'xor' a2) 'xor' a3) 'xor' a5) & (( Following (s,3)) . ap) = a1 & (( Following (s,3)) . bp) = a2 & (( Following (s,3)) . cp) = a3 & (( Following (s,3)) . dp) = a4 & (( Following (s,3)) . cin) = a5

    proof

      let ap,bp,cp,dp be non pair set;

      let cin be set such that

       A1: cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp)));

      set S = ( BitFTA0Str (ap,bp,cp,dp,cin));

      

       A2: ap in ( InputVertices S) & bp in ( InputVertices S) by A1, Th6;

      

       A3: cp in ( InputVertices S) & dp in ( InputVertices S) by A1, Th6;

      let s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . ap) & a2 = (s . bp) & a3 = (s . cp) & a4 = (s . dp) & a5 = (s . cin);

      

       A5: (( Following (s,2)) . cp) = a3 & (( Following (s,2)) . dp) = a4 by A1, A4, Th8;

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set A1cin = [ <*A1, cin*>, xor2 ];

      

       A6: ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) by FACIRC_1: 12;

      (( Following (s,2)) . A1) = ((a1 'xor' a2) 'xor' a3) & (( Following (s,2)) . cin) = a5 by A1, A4, Th8;

      hence (( Following (s,3)) . A1cin) = (((a1 'xor' a2) 'xor' a3) 'xor' a5) by A6, Lm4;

      

       A7: (( Following (s,2)) . cin) = a5 by A1, A4, Th8;

      

       A8: cin in ( InputVertices S) by A1, Th6;

      (( Following (s,2)) . ap) = a1 & (( Following (s,2)) . bp) = a2 by A1, A4, Th8;

      hence thesis by A6, A2, A3, A8, A5, A7, CIRCUIT2:def 5;

    end;

    

     Lm7: for ap,bp,cp,dp be non pair set holds for cin be set holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds for a123x,a123y,a123z be Element of BOOLEAN st a123x = (s . [ <*( GFA0AdderOutput (ap,bp,cp)), cin*>, and2 ]) & a123y = (s . [ <*cin, dp*>, and2 ]) & a123z = (s . [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ]) holds (( Following s) . ( GFA0CarryOutput (( GFA0AdderOutput (ap,bp,cp)),cin,dp))) = ((a123x 'or' a123y) 'or' a123z)

    proof

      let ap,bp,cp,dp be non pair set;

      let cin be set;

      set S = ( BitFTA0Str (ap,bp,cp,dp,cin));

      set C = ( BitFTA0Circ (ap,bp,cp,dp,cin));

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set A2 = ( GFA0CarryOutput (A1,cin,dp));

      set A1cin = [ <*A1, cin*>, and2 ];

      set cindp = [ <*cin, dp*>, and2 ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      let s be State of C;

      let a123x,a123y,a123z be Element of BOOLEAN such that

       A1: a123x = (s . A1cin) & a123y = (s . cindp) & a123z = (s . dpA1);

      

       A2: A1cin in the carrier of S & cindp in the carrier of S by Th4;

      

       A3: dpA1 in the carrier of S & ( dom s) = the carrier of S by Th4, CIRCUIT1: 3;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A2 in the carrier' of S by Th5;

      

      hence (( Following s) . A2) = ( or3 . (s * <*A1cin, cindp, dpA1*>)) by FACIRC_1: 35

      .= ( or3 . <*a123x, a123y, a123z*>) by A1, A2, A3, FINSEQ_2: 126

      .= ((a123x 'or' a123y) 'or' a123z) by FACIRC_1:def 7;

    end;

    

     Lm8: for ap,bp,cp,dp be non pair set holds for cin be set holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds for a1235,a4 be Element of BOOLEAN st a1235 = (s . [ <*( GFA0AdderOutput (ap,bp,cp)), cin*>, xor2 ]) & a4 = (s . dp) holds (( Following s) . ( GFA0AdderOutput (( GFA0AdderOutput (ap,bp,cp)),cin,dp))) = (a1235 'xor' a4)

    proof

      let ap,bp,cp,dp be non pair set;

      let cin be set;

      set S = ( BitFTA0Str (ap,bp,cp,dp,cin));

      set C = ( BitFTA0Circ (ap,bp,cp,dp,cin));

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set A2 = ( GFA0AdderOutput (A1,cin,dp));

      set A1cin = [ <*A1, cin*>, xor2 ];

      let s be State of C;

      let a1235,a4 be Element of BOOLEAN such that

       A1: a1235 = (s . A1cin) & a4 = (s . dp);

      

       A2: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A3: A1cin in the carrier of S & dp in the carrier of S by Th4;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A2 in the carrier' of S by Th5;

      

      hence (( Following s) . A2) = ( xor2 . (s * <*A1cin, dp*>)) by FACIRC_1: 35

      .= ( xor2 . <*a1235, a4*>) by A1, A3, A2, FINSEQ_2: 125

      .= (a1235 'xor' a4) by FACIRC_1:def 4;

    end;

    

     Lm9: for ap,bp,cp,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp))) holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bp) & a3 = (s . cp) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,4)) . ( GFA0CarryOutput (( GFA0AdderOutput (ap,bp,cp)),cin,dp))) = (((((a1 'xor' a2) 'xor' a3) '&' a5) 'or' (a5 '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3))) & (( Following (s,4)) . ap) = a1 & (( Following (s,4)) . bp) = a2 & (( Following (s,4)) . cp) = a3 & (( Following (s,4)) . dp) = a4 & (( Following (s,4)) . cin) = a5

    proof

      let ap,bp,cp,dp be non pair set;

      let cin be set such that

       A1: cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp)));

      set S = ( BitFTA0Str (ap,bp,cp,dp,cin));

      

       A2: ap in ( InputVertices S) & bp in ( InputVertices S) by A1, Th6;

      

       A3: cp in ( InputVertices S) & dp in ( InputVertices S) by A1, Th6;

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      let s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin));

      set dpA1 = [ <*dp, A1*>, and2 ];

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . ap) & a2 = (s . bp) & a3 = (s . cp) & a4 = (s . dp) & a5 = (s . cin);

      

       A5: (( Following (s,3)) . dpA1) = (a4 '&' ((a1 'xor' a2) 'xor' a3)) by A1, A4, Lm5;

      set cindp = [ <*cin, dp*>, and2 ];

      set A1cin = [ <*A1, cin*>, and2 ];

      set A2 = ( GFA0CarryOutput (A1,cin,dp));

      

       A6: ( Following (s,(3 + 1))) = ( Following ( Following (s,3))) by FACIRC_1: 12;

      (( Following (s,3)) . A1cin) = (((a1 'xor' a2) 'xor' a3) '&' a5) & (( Following (s,3)) . cindp) = (a5 '&' a4) by A1, A4, Lm5;

      hence (( Following (s,4)) . A2) = (((((a1 'xor' a2) 'xor' a3) '&' a5) 'or' (a5 '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3))) by A6, A5, Lm7;

      

       A7: (( Following (s,3)) . cp) = a3 & (( Following (s,3)) . dp) = a4 by A1, A4, Lm5;

      

       A8: (( Following (s,3)) . cin) = a5 by A1, A4, Lm5;

      

       A9: cin in ( InputVertices S) by A1, Th6;

      (( Following (s,3)) . ap) = a1 & (( Following (s,3)) . bp) = a2 by A1, A4, Lm5;

      hence thesis by A6, A2, A3, A9, A7, A8, CIRCUIT2:def 5;

    end;

    

     Lm10: for ap,bp,cp,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp))) holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bp) & a3 = (s . cp) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,4)) . ( GFA0AdderOutput (( GFA0AdderOutput (ap,bp,cp)),cin,dp))) = ((((a1 'xor' a2) 'xor' a3) 'xor' a4) 'xor' a5) & (( Following (s,4)) . ap) = a1 & (( Following (s,4)) . bp) = a2 & (( Following (s,4)) . cp) = a3 & (( Following (s,4)) . dp) = a4 & (( Following (s,4)) . cin) = a5

    proof

      let ap,bp,cp,dp be non pair set;

      let cin be set such that

       A1: cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp)));

      set S = ( BitFTA0Str (ap,bp,cp,dp,cin));

      

       A2: ap in ( InputVertices S) & bp in ( InputVertices S) by A1, Th6;

      

       A3: cp in ( InputVertices S) & dp in ( InputVertices S) by A1, Th6;

      let s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . ap) & a2 = (s . bp) & a3 = (s . cp) & a4 = (s . dp) & a5 = (s . cin);

      

       A5: (( Following (s,3)) . cp) = a3 & (( Following (s,3)) . dp) = a4 by A1, A4, Lm6;

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set A2 = ( GFA0AdderOutput (A1,cin,dp));

      set A1cin = [ <*A1, cin*>, xor2 ];

      

       A6: ( Following (s,(3 + 1))) = ( Following ( Following (s,3))) by FACIRC_1: 12;

      (( Following (s,3)) . A1cin) = (((a1 'xor' a2) 'xor' a3) 'xor' a5) & (( Following (s,3)) . dp) = a4 by A1, A4, Lm6;

      

      hence (( Following (s,4)) . A2) = ((((a1 'xor' a2) 'xor' a3) 'xor' a5) 'xor' a4) by A6, Lm8

      .= ((((a1 'xor' a2) 'xor' a3) 'xor' a4) 'xor' a5) by XBOOLEAN: 73;

      

       A7: (( Following (s,3)) . cin) = a5 by A1, A4, Lm6;

      

       A8: cin in ( InputVertices S) by A1, Th6;

      (( Following (s,3)) . ap) = a1 & (( Following (s,3)) . bp) = a2 by A1, A4, Lm6;

      hence thesis by A6, A2, A3, A8, A5, A7, CIRCUIT2:def 5;

    end;

    theorem :: FTACELL1:9

    for ap,bp,cp,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] & not cin in ( InnerVertices ( BitGFA0Str (ap,bp,cp))) holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bp) & a3 = (s . cp) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,4)) . ( BitFTA0AdderOutputP (ap,bp,cp,dp,cin))) = (((((a1 'xor' a2) 'xor' a3) '&' a5) 'or' (a5 '&' a4)) 'or' (a4 '&' ((a1 'xor' a2) 'xor' a3))) & (( Following (s,4)) . ( BitFTA0AdderOutputQ (ap,bp,cp,dp,cin))) = ((((a1 'xor' a2) 'xor' a3) 'xor' a4) 'xor' a5) by Lm9, Lm10;

    theorem :: FTACELL1:10

    for ap,bp,cp,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA0AdderOutput (ap,bp,cp))*>, and2 ] holds for s be State of ( BitFTA0Circ (ap,bp,cp,dp,cin)) holds ( Following (s,4)) is stable

    proof

      set n1 = 2, n2 = 2;

      let ap,bp,cp,dp be non pair set;

      let cin be set;

      set C = ( BitFTA0Circ (ap,bp,cp,dp,cin));

      set S1 = ( BitGFA0Str (ap,bp,cp));

      set C1 = ( BitGFA0Circ (ap,bp,cp));

      set A1 = ( GFA0AdderOutput (ap,bp,cp));

      set S2 = ( BitGFA0Str (A1,cin,dp));

      set C2 = ( BitGFA0Circ (A1,cin,dp));

      set cindp = [ <*cin, dp*>, and2 ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      assume

       A1: cin <> dpA1;

      let s be State of C;

      C1 tolerates C2 by CIRCCOMB: 60;

      then

       A2: the Sorts of C1 tolerates the Sorts of C2 by CIRCCOMB:def 3;

      then

      reconsider s1 = (s | the carrier of S1) as State of C1 by CIRCCOMB: 26;

      reconsider s2 = (( Following (s,n1)) | the carrier of S2) as State of C2 by A2, CIRCCOMB: 26;

      

       A3: ( InputVertices S1) misses ( InnerVertices S2) & ( Following (s1,n1)) is stable by Lm2, GFACIRC1: 40;

      A1 <> cindp by Lm1;

      then ( Following (s2,n2)) is stable by A1, GFACIRC1: 40;

      then ( Following (s,(n1 + n2))) is stable by A3, CIRCCMB2: 19, CIRCCOMB: 60;

      hence thesis;

    end;

    begin

    definition

      let ap,bm,cp,dm,cin be set;

      :: FTACELL1:def7

      func BitFTA1Str (ap,bm,cp,dm,cin) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( BitGFA1Str (ap,bm,cp)) +* ( BitGFA2Str (( GFA1AdderOutput (ap,bm,cp)),cin,dm)));

      coherence ;

    end

    definition

      let ap,bm,cp,dm,cin be set;

      :: FTACELL1:def8

      func BitFTA1Circ (ap,bm,cp,dm,cin) -> strict Boolean gate`2=den Circuit of ( BitFTA1Str (ap,bm,cp,dm,cin)) equals (( BitGFA1Circ (ap,bm,cp)) +* ( BitGFA2Circ (( GFA1AdderOutput (ap,bm,cp)),cin,dm)));

      coherence ;

    end

    theorem :: FTACELL1:11

    

     Th11: for ap,bm,cp,dm,cin be set holds ( 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))*>, nor2 ], ( GFA2CarryOutput (( GFA1AdderOutput (ap,bm,cp)),cin,dm))})

    proof

      let ap,bm,cp,dm,cin be set;

      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 (A1,cin,dm));

      set A2 = ( GFA2AdderOutput (A1,cin,dm));

      set C2 = ( GFA2CarryOutput (A1,cin,dm));

      set apbm0 = [ <*ap, bm*>, xor2c ];

      set apbm = [ <*ap, bm*>, and2c ];

      set bmcp = [ <*bm, cp*>, and2a ];

      set cpap = [ <*cp, ap*>, and2 ];

      set A1cin0 = [ <*A1, cin*>, xor2c ];

      set A1cin = [ <*A1, cin*>, and2a ];

      set cindm = [ <*cin, dm*>, and2c ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      S1 tolerates S2 by CIRCCOMB: 47;

      

      hence ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by CIRCCOMB: 11

      .= (((( {apbm0} \/ {A1}) \/ {apbm, bmcp, cpap}) \/ {C1}) \/ ( InnerVertices S2)) by GFACIRC1: 63

      .= ((( {apbm0, A1} \/ {apbm, bmcp, cpap}) \/ {C1}) \/ ( InnerVertices S2)) by ENUMSET1: 1

      .= (( {apbm0, A1} \/ ( {apbm, bmcp, cpap} \/ {C1})) \/ ( InnerVertices S2)) by XBOOLE_1: 4

      .= (( {apbm0, A1} \/ {apbm, bmcp, cpap, C1}) \/ ( InnerVertices S2)) by ENUMSET1: 6

      .= (( {apbm0, A1} \/ {apbm, bmcp, cpap, C1}) \/ ((( {A1cin0} \/ {A2}) \/ {A1cin, cindm, dmA1}) \/ {C2})) by GFACIRC1: 95

      .= (( {apbm0, A1} \/ {apbm, bmcp, cpap, C1}) \/ (( {A1cin0, A2} \/ {A1cin, cindm, dmA1}) \/ {C2})) by ENUMSET1: 1

      .= (( {apbm0, A1} \/ {apbm, bmcp, cpap, C1}) \/ ( {A1cin0, A2} \/ ( {A1cin, cindm, dmA1} \/ {C2}))) by XBOOLE_1: 4

      .= (( {apbm0, A1} \/ {apbm, bmcp, cpap, C1}) \/ ( {A1cin0, A2} \/ {A1cin, cindm, dmA1, C2})) by ENUMSET1: 6

      .= ((( {apbm0, A1} \/ {apbm, bmcp, cpap, C1}) \/ {A1cin0, A2}) \/ {A1cin, cindm, dmA1, C2}) by XBOOLE_1: 4;

    end;

    theorem :: FTACELL1:12

    for ap,bm,cp,dm,cin be set holds ( InnerVertices ( BitFTA1Str (ap,bm,cp,dm,cin))) is Relation

    proof

      let ap,bm,cp,dm,cin be set;

      set S1 = ( BitGFA1Str (ap,bm,cp));

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set S2 = ( BitGFA2Str (A1,cin,dm));

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by GFACIRC1: 64, GFACIRC1: 96;

      hence thesis by FACIRC_1: 3;

    end;

    

     Lm11: for x,y,z be set holds for p be set holds ( GFA1AdderOutput (x,y,z)) <> [p, and2c ]

    proof

      let x,y,z be set, p be set;

      set A1 = ( GFA1AdderOutput (x,y,z));

      (A1 `2 ) = xor2c ;

      then ( [p, and2c ] `2 ) <> (A1 `2 ) by GFACIRC1: 3, GFACIRC1: 4;

      hence thesis;

    end;

    

     Lm12: for ap,bm,cp be non pair set holds for x,y,z be set holds ( InputVertices ( BitGFA1Str (ap,bm,cp))) misses ( InnerVertices ( BitGFA2Str (x,y,z)))

    proof

      let ap,bm,cp be non pair set;

      let x,y,z be set;

      set S1 = ( BitGFA1Str (ap,bm,cp));

      ( InputVertices S1) is without_pairs by GFACIRC1: 67;

      hence thesis by FACIRC_1: 5, GFACIRC1: 96;

    end;

    theorem :: FTACELL1:13

    

     Th13: for ap,bm,cp,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp))) holds ( InputVertices ( BitFTA1Str (ap,bm,cp,dm,cin))) = {ap, bm, cp, dm, cin}

    proof

      let ap,bm,cp,dm be non pair set;

      let cin be set;

      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 (A1,cin,dm));

      set apbm0 = [ <*ap, bm*>, xor2c ];

      set apbm = [ <*ap, bm*>, and2c ];

      set bmcp = [ <*bm, cp*>, and2a ];

      set cpap = [ <*cp, ap*>, and2 ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      assume that

       A1: cin <> dmA1 and

       A2: not cin in ( InnerVertices S1);

      

       A3: not dm in {A1, apbm0, apbm, bmcp, cpap, C1} by ENUMSET1:def 4;

      A1 in {A1, apbm0, apbm, bmcp, cpap, C1} by ENUMSET1:def 4;

      then

       A4: ( {A1} \ {A1, apbm0, apbm, bmcp, cpap, C1}) = {} by ZFMISC_1: 60;

      

       A5: ( InnerVertices S1) = ((( {apbm0} \/ {A1}) \/ {apbm, bmcp, cpap}) \/ {C1}) by GFACIRC1: 63

      .= (( {apbm0, A1} \/ {apbm, bmcp, cpap}) \/ {C1}) by ENUMSET1: 1

      .= ( {apbm0, A1} \/ ( {apbm, bmcp, cpap} \/ {C1})) by XBOOLE_1: 4

      .= ( {A1, apbm0} \/ {apbm, bmcp, cpap, C1}) by ENUMSET1: 6

      .= {A1, apbm0, apbm, bmcp, cpap, C1} by ENUMSET1: 12;

      

      then

       A6: ( {A1, cin, dm} \ ( InnerVertices S1)) = (( {A1} \/ {cin, dm}) \ {A1, apbm0, apbm, bmcp, cpap, C1}) by ENUMSET1: 2

      .= (( {A1} \ {A1, apbm0, apbm, bmcp, cpap, C1}) \/ ( {cin, dm} \ {A1, apbm0, apbm, bmcp, cpap, C1})) by XBOOLE_1: 42

      .= (( {cin} \/ {dm}) \ {A1, apbm0, apbm, bmcp, cpap, C1}) by A4, ENUMSET1: 1

      .= (( {cin} \ {A1, apbm0, apbm, bmcp, cpap, C1}) \/ ( {dm} \ {A1, apbm0, apbm, bmcp, cpap, C1})) by XBOOLE_1: 42

      .= ( {cin} \/ ( {dm} \ {A1, apbm0, apbm, bmcp, cpap, C1})) by A2, A5, ZFMISC_1: 59

      .= ( {cin} \/ {dm}) by A3, ZFMISC_1: 59

      .= {cin, dm} by ENUMSET1: 1;

      ( InnerVertices S2) misses ( InputVertices S1) & S1 tolerates S2 by Lm12, CIRCCOMB: 47;

      

      hence ( InputVertices S) = (( InputVertices S1) \/ (( InputVertices S2) \ ( InnerVertices S1))) by FACIRC_1: 4

      .= ( {ap, bm, cp} \/ (( InputVertices S2) \ ( InnerVertices S1))) by GFACIRC1: 66

      .= ( {ap, bm, cp} \/ ( {A1, cin, dm} \ ( InnerVertices S1))) by A1, Lm11, GFACIRC1: 97

      .= {ap, bm, cp, dm, cin} by A6, ENUMSET1: 9;

    end;

    theorem :: FTACELL1:14

    

     Th14: for ap,bm,cp,dm,cin be set holds ap in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & bm in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & cp in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & dm in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & cin in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & [ <*ap, bm*>, xor2c ] in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & ( GFA1AdderOutput (ap,bm,cp)) in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & [ <*ap, bm*>, and2c ] in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & [ <*bm, cp*>, and2a ] in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & [ <*cp, ap*>, and2 ] in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & ( GFA1CarryOutput (ap,bm,cp)) in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & [ <*( GFA1AdderOutput (ap,bm,cp)), cin*>, xor2c ] in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & ( GFA2AdderOutput (( GFA1AdderOutput (ap,bm,cp)),cin,dm)) in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & [ <*( GFA1AdderOutput (ap,bm,cp)), cin*>, and2a ] in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & [ <*cin, dm*>, and2c ] in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin)) & ( GFA2CarryOutput (( GFA1AdderOutput (ap,bm,cp)),cin,dm)) in the carrier of ( BitFTA1Str (ap,bm,cp,dm,cin))

    proof

      let ap,bm,cp,dm,cin be set;

      set S1 = ( BitGFA1Str (ap,bm,cp));

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set C1 = ( GFA1CarryOutput (ap,bm,cp));

      set S2 = ( BitGFA2Str (A1,cin,dm));

      set A2 = ( GFA2AdderOutput (A1,cin,dm));

      set C2 = ( GFA2CarryOutput (A1,cin,dm));

      set apbm0 = [ <*ap, bm*>, xor2c ];

      set apbm = [ <*ap, bm*>, and2c ];

      set bmcp = [ <*bm, cp*>, and2a ];

      set cpap = [ <*cp, ap*>, and2 ];

      set A1cin0 = [ <*A1, cin*>, xor2c ];

      set A1cin = [ <*A1, cin*>, and2a ];

      set cindm = [ <*cin, dm*>, and2c ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      

       A1: cp in the carrier of S1 & apbm0 in the carrier of S1 by GFACIRC1: 68;

      

       A2: apbm in the carrier of S1 & bmcp in the carrier of S1 by GFACIRC1: 68;

      

       A3: A1 in the carrier of S2 & cin in the carrier of S2 by GFACIRC1: 100;

      

       A4: cpap in the carrier of S1 & C1 in the carrier of S1 by GFACIRC1: 68;

      

       A5: C2 in the carrier of S2 by GFACIRC1: 100;

      

       A6: cindm in the carrier of S2 & dmA1 in the carrier of S2 by GFACIRC1: 100;

      

       A7: A2 in the carrier of S2 & A1cin in the carrier of S2 by GFACIRC1: 100;

      

       A8: dm in the carrier of S2 & A1cin0 in the carrier of S2 by GFACIRC1: 100;

      ap in the carrier of S1 & bm in the carrier of S1 by GFACIRC1: 68;

      hence thesis by A1, A2, A4, A3, A8, A7, A6, A5, FACIRC_1: 20;

    end;

    theorem :: FTACELL1:15

    

     Th15: for ap,bm,cp,dm,cin be set holds [ <*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))*>, nor2 ] in ( InnerVertices ( BitFTA1Str (ap,bm,cp,dm,cin))) & ( GFA2CarryOutput (( GFA1AdderOutput (ap,bm,cp)),cin,dm)) in ( InnerVertices ( BitFTA1Str (ap,bm,cp,dm,cin)))

    proof

      let ap,bm,cp,dm,cin be set;

      set S = ( BitFTA1Str (ap,bm,cp,dm,cin));

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set C1 = ( GFA1CarryOutput (ap,bm,cp));

      set A2 = ( GFA2AdderOutput (A1,cin,dm));

      set C2 = ( GFA2CarryOutput (A1,cin,dm));

      set apbm0 = [ <*ap, bm*>, xor2c ];

      set apbm = [ <*ap, bm*>, and2c ];

      set bmcp = [ <*bm, cp*>, and2a ];

      set cpap = [ <*cp, ap*>, and2 ];

      set A1cin0 = [ <*A1, cin*>, xor2c ];

      set A1cin = [ <*A1, cin*>, and2a ];

      set cindm = [ <*cin, dm*>, and2c ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      set p1 = {apbm0, A1, apbm, bmcp, cpap, C1};

      set p2 = {A1cin0, A2, A1cin, cindm, dmA1, C2};

      

       A1: apbm0 in p1 & A1 in p1 by ENUMSET1:def 4;

      

       A2: apbm in p1 & bmcp in p1 by ENUMSET1:def 4;

      

       A3: A1cin0 in p2 & A2 in p2 by ENUMSET1:def 4;

      

       A4: cpap in p1 & C1 in p1 by ENUMSET1:def 4;

      

       A5: dmA1 in p2 & C2 in p2 by ENUMSET1:def 4;

      

       A6: A1cin in p2 & cindm in p2 by ENUMSET1:def 4;

      ( InnerVertices S) = ((( {apbm0, A1} \/ {apbm, bmcp, cpap, C1}) \/ {A1cin0, A2}) \/ {A1cin, cindm, dmA1, C2}) by Th11

      .= ((p1 \/ {A1cin0, A2}) \/ {A1cin, cindm, dmA1, C2}) by ENUMSET1: 12

      .= (p1 \/ ( {A1cin0, A2} \/ {A1cin, cindm, dmA1, C2})) by XBOOLE_1: 4

      .= (p1 \/ p2) by ENUMSET1: 12;

      hence thesis by A1, A2, A4, A3, A6, A5, XBOOLE_0:def 3;

    end;

    theorem :: FTACELL1:16

    

     Th16: for ap,bm,cp,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp))) holds ap in ( InputVertices ( BitFTA1Str (ap,bm,cp,dm,cin))) & bm in ( InputVertices ( BitFTA1Str (ap,bm,cp,dm,cin))) & cp in ( InputVertices ( BitFTA1Str (ap,bm,cp,dm,cin))) & dm in ( InputVertices ( BitFTA1Str (ap,bm,cp,dm,cin))) & cin in ( InputVertices ( BitFTA1Str (ap,bm,cp,dm,cin)))

    proof

      let ap,bm,cp,dm be non pair set;

      let cin be set;

      set S = ( BitFTA1Str (ap,bm,cp,dm,cin));

      set S1 = ( BitGFA1Str (ap,bm,cp));

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set dmA1 = [ <*dm, A1*>, nor2 ];

      assume cin <> dmA1 & not cin in ( InnerVertices S1);

      then ( InputVertices S) = {ap, bm, cp, dm, cin} by Th13;

      hence thesis by ENUMSET1:def 3;

    end;

    definition

      let ap,bm,cp,dm,cin be set;

      :: FTACELL1:def9

      func BitFTA1CarryOutput (ap,bm,cp,dm,cin) -> Element of ( InnerVertices ( BitFTA1Str (ap,bm,cp,dm,cin))) equals ( GFA1CarryOutput (ap,bm,cp));

      coherence by Th15;

      :: FTACELL1:def10

      func BitFTA1AdderOutputI (ap,bm,cp,dm,cin) -> Element of ( InnerVertices ( BitFTA1Str (ap,bm,cp,dm,cin))) equals ( GFA1AdderOutput (ap,bm,cp));

      coherence by Th15;

      :: FTACELL1:def11

      func BitFTA1AdderOutputP (ap,bm,cp,dm,cin) -> Element of ( InnerVertices ( BitFTA1Str (ap,bm,cp,dm,cin))) equals ( GFA2CarryOutput (( GFA1AdderOutput (ap,bm,cp)),cin,dm));

      coherence by Th15;

      :: FTACELL1:def12

      func BitFTA1AdderOutputQ (ap,bm,cp,dm,cin) -> Element of ( InnerVertices ( BitFTA1Str (ap,bm,cp,dm,cin))) equals ( GFA2AdderOutput (( GFA1AdderOutput (ap,bm,cp)),cin,dm));

      coherence by Th15;

    end

    theorem :: FTACELL1:17

    for ap,bm,cp be non pair set holds for dm,cin be set holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bm) & a3 = (s . cp) holds (( Following (s,2)) . ( BitFTA1CarryOutput (ap,bm,cp,dm,cin))) = (((a1 '&' ( 'not' a2)) 'or' (( 'not' a2) '&' a3)) 'or' (a3 '&' a1)) & (( Following (s,2)) . ( BitFTA1AdderOutputI (ap,bm,cp,dm,cin))) = ( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3))

    proof

      let ap,bm,cp be non pair set;

      let dm,cin be set;

      let s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin));

      set S1 = ( BitGFA1Str (ap,bm,cp));

      set C1 = ( BitGFA1Circ (ap,bm,cp));

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set A2 = ( GFA1CarryOutput (ap,bm,cp));

      set S2 = ( BitGFA2Str (A1,cin,dm));

      set C2 = ( BitGFA2Circ (A1,cin,dm));

      let a1,a2,a3 be Element of BOOLEAN such that

       A1: a1 = (s . ap) and

       A2: a2 = (s . bm) and

       A3: a3 = (s . cp);

      reconsider s1 = (s | the carrier of S1) as State of C1 by FACIRC_1: 26;

      

       A4: ( dom s1) = the carrier of S1 by CIRCUIT1: 3;

      ap in the carrier of S1 by GFACIRC1: 68;

      then

       A5: a1 = (s1 . ap) by A1, A4, FUNCT_1: 47;

      reconsider t = s as State of (C1 +* C2);

      

       A6: ( InputVertices S1) misses ( InnerVertices S2) by Lm12;

      cp in the carrier of S1 by GFACIRC1: 68;

      then

       A7: a3 = (s1 . cp) by A3, A4, FUNCT_1: 47;

      bm in the carrier of S1 by GFACIRC1: 68;

      then

       A8: a2 = (s1 . bm) by A2, A4, FUNCT_1: 47;

      A2 in the carrier of S1 by GFACIRC1: 68;

      then (( Following (t,2)) . ( GFA1CarryOutput (ap,bm,cp))) = (( Following (s1,2)) . ( GFA1CarryOutput (ap,bm,cp))) by A6, FACIRC_1: 32;

      hence (( Following (s,2)) . ( BitFTA1CarryOutput (ap,bm,cp,dm,cin))) = (((a1 '&' ( 'not' a2)) 'or' (( 'not' a2) '&' a3)) 'or' (a3 '&' a1)) by A5, A8, A7, GFACIRC1: 71;

      A1 in the carrier of S1 by GFACIRC1: 68;

      then (( Following (t,2)) . ( GFA1AdderOutput (ap,bm,cp))) = (( Following (s1,2)) . ( GFA1AdderOutput (ap,bm,cp))) by A6, FACIRC_1: 32;

      hence thesis by A5, A8, A7, GFACIRC1: 71;

    end;

    theorem :: FTACELL1:18

    

     Th18: for ap,bm,cp,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp))) holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bm) & a3 = (s . cp) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,2)) . ( GFA1AdderOutput (ap,bm,cp))) = ( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3)) & (( Following (s,2)) . ap) = a1 & (( Following (s,2)) . bm) = a2 & (( Following (s,2)) . cp) = a3 & (( Following (s,2)) . dm) = a4 & (( Following (s,2)) . cin) = a5

    proof

      let ap,bm,cp,dm be non pair set;

      let cin be set such that

       A1: cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp)));

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set C1 = ( BitGFA1Circ (ap,bm,cp));

      set S1 = ( BitGFA1Str (ap,bm,cp));

      set S2 = ( BitGFA2Str (A1,cin,dm));

      set C2 = ( BitGFA2Circ (A1,cin,dm));

      set S = ( BitFTA1Str (ap,bm,cp,dm,cin));

      let s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A2: a1 = (s . ap) and

       A3: a2 = (s . bm) and

       A4: a3 = (s . cp) and

       A5: a4 = (s . dm) and

       A6: a5 = (s . cin);

      reconsider s1 = (s | the carrier of S1) as State of C1 by FACIRC_1: 26;

      

       A7: ( dom s1) = the carrier of S1 by CIRCUIT1: 3;

      

       A8: dm in ( InputVertices S) by A1, Th16;

      then

       A9: (( Following s) . dm) = a4 by A5, CIRCUIT2:def 5;

      

       A10: cp in ( InputVertices S) by A1, Th16;

      then

       A11: (( Following s) . cp) = a3 by A4, CIRCUIT2:def 5;

      bm in the carrier of S1 by GFACIRC1: 68;

      then

       A12: a2 = (s1 . bm) by A3, A7, FUNCT_1: 47;

      reconsider t = s as State of (C1 +* C2);

      A1 in the carrier of S1 & ( InputVertices S1) misses ( InnerVertices S2) by Lm12, GFACIRC1: 68;

      then

       A13: (( Following (t,2)) . ( GFA1AdderOutput (ap,bm,cp))) = (( Following (s1,2)) . ( GFA1AdderOutput (ap,bm,cp))) by FACIRC_1: 32;

      cp in the carrier of S1 by GFACIRC1: 68;

      then

       A14: a3 = (s1 . cp) by A4, A7, FUNCT_1: 47;

      ap in the carrier of S1 by GFACIRC1: 68;

      then a1 = (s1 . ap) by A2, A7, FUNCT_1: 47;

      hence (( Following (s,2)) . ( GFA1AdderOutput (ap,bm,cp))) = ( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3)) by A12, A14, A13, GFACIRC1: 71;

      

       A15: bm in ( InputVertices S) by A1, Th16;

      then

       A16: (( Following s) . bm) = a2 by A3, CIRCUIT2:def 5;

      

       A17: cin in ( InputVertices S) by A1, Th16;

      then

       A18: (( Following s) . cin) = a5 by A6, CIRCUIT2:def 5;

      

       A19: ap in ( InputVertices S) by A1, Th16;

      then ( Following (s,2)) = ( Following ( Following s)) & (( Following s) . ap) = a1 by A2, CIRCUIT2:def 5, FACIRC_1: 15;

      hence thesis by A19, A15, A10, A8, A17, A16, A11, A9, A18, CIRCUIT2:def 5;

    end;

    

     Lm13: for ap,bm,cp,dm be non pair set holds for cin be set holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds for a123,a4,a5 be Element of BOOLEAN st a123 = (s . ( GFA1AdderOutput (ap,bm,cp))) & a4 = (s . dm) & a5 = (s . cin) holds (( Following s) . [ <*( GFA1AdderOutput (ap,bm,cp)), cin*>, and2a ]) = (( 'not' a123) '&' a5) & (( Following s) . [ <*cin, dm*>, and2c ]) = (a5 '&' ( 'not' a4)) & (( Following s) . [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ]) = (( 'not' a4) '&' ( 'not' a123))

    proof

      let ap,bm,cp,dm be non pair set;

      let cin be set;

      set S = ( BitFTA1Str (ap,bm,cp,dm,cin));

      set C = ( BitFTA1Circ (ap,bm,cp,dm,cin));

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set A1cin = [ <*A1, cin*>, and2a ];

      set cindm = [ <*cin, dm*>, and2c ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      let s be State of C;

      let a123,a4,a5 be Element of BOOLEAN such that

       A1: a123 = (s . A1) and

       A2: a4 = (s . dm) and

       A3: a5 = (s . cin);

      

       A4: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A5: cin in the carrier of S by Th14;

      

       A6: A1 in the carrier of S by Th14;

      

       A7: ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A1cin in the carrier' of S by Th15;

      

      hence (( Following s) . A1cin) = ( and2a . (s * <*A1, cin*>)) by FACIRC_1: 35

      .= ( and2a . <*a123, a5*>) by A1, A3, A6, A5, A4, FINSEQ_2: 125

      .= (( 'not' a123) '&' a5) by TWOSCOMP:def 2;

      

       A8: dm in the carrier of S by Th14;

      cindm in the carrier' of S by A7, Th15;

      

      hence (( Following s) . cindm) = ( and2c . (s * <*cin, dm*>)) by FACIRC_1: 35

      .= ( and2c . <*a5, a4*>) by A2, A3, A8, A5, A4, FINSEQ_2: 125

      .= (a5 '&' ( 'not' a4)) by GFACIRC1:def 3;

      dmA1 in the carrier' of S by A7, Th15;

      

      hence (( Following s) . dmA1) = ( nor2 . (s * <*dm, A1*>)) by FACIRC_1: 35

      .= ( nor2 . <*a4, a123*>) by A1, A2, A6, A8, A4, FINSEQ_2: 125

      .= (( 'not' a4) '&' ( 'not' a123)) by TWOSCOMP: 54;

    end;

    

     Lm14: for ap,bm,cp,dm be non pair set holds for cin be set holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds for a123,a5 be Element of BOOLEAN st a123 = (s . ( GFA1AdderOutput (ap,bm,cp))) & a5 = (s . cin) holds (( Following s) . [ <*( GFA1AdderOutput (ap,bm,cp)), cin*>, xor2c ]) = (a123 'xor' ( 'not' a5))

    proof

      let ap,bm,cp,dm be non pair set;

      let cin be set;

      set S = ( BitFTA1Str (ap,bm,cp,dm,cin));

      set C = ( BitFTA1Circ (ap,bm,cp,dm,cin));

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set A1cin = [ <*A1, cin*>, xor2c ];

      let s be State of C;

      let a123,a5 be Element of BOOLEAN such that

       A1: a123 = (s . A1) & a5 = (s . cin);

      

       A2: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A3: A1 in the carrier of S & cin in the carrier of S by Th14;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A1cin in the carrier' of S by Th15;

      

      hence (( Following s) . A1cin) = ( xor2c . (s * <*A1, cin*>)) by FACIRC_1: 35

      .= ( xor2c . <*a123, a5*>) by A1, A3, A2, FINSEQ_2: 125

      .= (a123 'xor' ( 'not' a5)) by GFACIRC1:def 4;

    end;

    

     Lm15: for ap,bm,cp,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp))) holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bm) & a3 = (s . cp) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,3)) . [ <*( GFA1AdderOutput (ap,bm,cp)), cin*>, and2a ]) = (((a1 'xor' ( 'not' a2)) 'xor' a3) '&' a5) & (( Following (s,3)) . [ <*cin, dm*>, and2c ]) = (a5 '&' ( 'not' a4)) & (( Following (s,3)) . [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ]) = (( 'not' a4) '&' ((a1 'xor' ( 'not' a2)) 'xor' a3)) & (( Following (s,3)) . ap) = a1 & (( Following (s,3)) . bm) = a2 & (( Following (s,3)) . cp) = a3 & (( Following (s,3)) . dm) = a4 & (( Following (s,3)) . cin) = a5

    proof

      let ap,bm,cp,dm be non pair set;

      let cin be set such that

       A1: cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp)));

      set S = ( BitFTA1Str (ap,bm,cp,dm,cin));

      

       A2: ap in ( InputVertices S) & bm in ( InputVertices S) by A1, Th16;

      

       A3: cp in ( InputVertices S) & dm in ( InputVertices S) by A1, Th16;

      let s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . ap) & a2 = (s . bm) & a3 = (s . cp) & a4 = (s . dm) & a5 = (s . cin);

      

       A5: (( Following (s,2)) . cin) = a5 by A1, A4, Th18;

      set cindm = [ <*cin, dm*>, and2c ];

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set A1cin = [ <*A1, cin*>, and2a ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      

       A6: ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) by FACIRC_1: 12;

      (( Following (s,2)) . A1) = ( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3)) & (( Following (s,2)) . dm) = a4 by A1, A4, Th18;

      hence (( Following (s,3)) . A1cin) = (((a1 'xor' ( 'not' a2)) 'xor' a3) '&' a5) & (( Following (s,3)) . cindm) = (a5 '&' ( 'not' a4)) & (( Following (s,3)) . dmA1) = (( 'not' a4) '&' ((a1 'xor' ( 'not' a2)) 'xor' a3)) by A6, A5, Lm13;

      

       A7: (( Following (s,2)) . cp) = a3 & (( Following (s,2)) . dm) = a4 by A1, A4, Th18;

      

       A8: (( Following (s,2)) . cin) = a5 by A1, A4, Th18;

      

       A9: cin in ( InputVertices S) by A1, Th16;

      (( Following (s,2)) . ap) = a1 & (( Following (s,2)) . bm) = a2 by A1, A4, Th18;

      hence thesis by A6, A2, A3, A9, A7, A8, CIRCUIT2:def 5;

    end;

    

     Lm16: for ap,bm,cp,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp))) holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bm) & a3 = (s . cp) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,3)) . [ <*( GFA1AdderOutput (ap,bm,cp)), cin*>, xor2c ]) = (( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3)) 'xor' ( 'not' a5)) & (( Following (s,3)) . ap) = a1 & (( Following (s,3)) . bm) = a2 & (( Following (s,3)) . cp) = a3 & (( Following (s,3)) . dm) = a4 & (( Following (s,3)) . cin) = a5

    proof

      let ap,bm,cp,dm be non pair set;

      let cin be set such that

       A1: cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp)));

      set S = ( BitFTA1Str (ap,bm,cp,dm,cin));

      

       A2: ap in ( InputVertices S) & bm in ( InputVertices S) by A1, Th16;

      

       A3: cp in ( InputVertices S) & dm in ( InputVertices S) by A1, Th16;

      let s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . ap) & a2 = (s . bm) & a3 = (s . cp) & a4 = (s . dm) & a5 = (s . cin);

      

       A5: (( Following (s,2)) . cp) = a3 & (( Following (s,2)) . dm) = a4 by A1, A4, Th18;

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set A1cin = [ <*A1, cin*>, xor2c ];

      

       A6: ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) by FACIRC_1: 12;

      (( Following (s,2)) . A1) = ( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3)) & (( Following (s,2)) . cin) = a5 by A1, A4, Th18;

      hence (( Following (s,3)) . A1cin) = (( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3)) 'xor' ( 'not' a5)) by A6, Lm14;

      

       A7: (( Following (s,2)) . cin) = a5 by A1, A4, Th18;

      

       A8: cin in ( InputVertices S) by A1, Th16;

      (( Following (s,2)) . ap) = a1 & (( Following (s,2)) . bm) = a2 by A1, A4, Th18;

      hence thesis by A6, A2, A3, A8, A5, A7, CIRCUIT2:def 5;

    end;

    

     Lm17: for ap,bm,cp,dm be non pair set holds for cin be set holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds for a123x,a123y,a123z be Element of BOOLEAN st a123x = (s . [ <*( GFA1AdderOutput (ap,bm,cp)), cin*>, and2a ]) & a123y = (s . [ <*cin, dm*>, and2c ]) & a123z = (s . [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ]) holds (( Following s) . ( GFA2CarryOutput (( GFA1AdderOutput (ap,bm,cp)),cin,dm))) = ( 'not' ((a123x 'or' a123y) 'or' a123z))

    proof

      let ap,bm,cp,dm be non pair set;

      let cin be set;

      set S = ( BitFTA1Str (ap,bm,cp,dm,cin));

      set C = ( BitFTA1Circ (ap,bm,cp,dm,cin));

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set A2 = ( GFA2CarryOutput (A1,cin,dm));

      set A1cin = [ <*A1, cin*>, and2a ];

      set cindm = [ <*cin, dm*>, and2c ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      let s be State of C;

      let a123x,a123y,a123z be Element of BOOLEAN such that

       A1: a123x = (s . A1cin) & a123y = (s . cindm) & a123z = (s . dmA1);

      

       A2: A1cin in the carrier of S & cindm in the carrier of S by Th14;

      

       A3: dmA1 in the carrier of S & ( dom s) = the carrier of S by Th14, CIRCUIT1: 3;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A2 in the carrier' of S by Th15;

      

      hence (( Following s) . A2) = ( nor3 . (s * <*A1cin, cindm, dmA1*>)) by FACIRC_1: 35

      .= ( nor3 . <*a123x, a123y, a123z*>) by A1, A2, A3, FINSEQ_2: 126

      .= ( 'not' ((a123x 'or' a123y) 'or' a123z)) by TWOSCOMP:def 28;

    end;

    

     Lm18: for ap,bm,cp,dm be non pair set holds for cin be set holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds for a1235,a4 be Element of BOOLEAN st a1235 = (s . [ <*( GFA1AdderOutput (ap,bm,cp)), cin*>, xor2c ]) & a4 = (s . dm) holds (( Following s) . ( GFA2AdderOutput (( GFA1AdderOutput (ap,bm,cp)),cin,dm))) = (a1235 'xor' ( 'not' a4))

    proof

      let ap,bm,cp,dm be non pair set;

      let cin be set;

      set S = ( BitFTA1Str (ap,bm,cp,dm,cin));

      set C = ( BitFTA1Circ (ap,bm,cp,dm,cin));

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set A2 = ( GFA2AdderOutput (A1,cin,dm));

      set A1cin = [ <*A1, cin*>, xor2c ];

      let s be State of C;

      let a1235,a4 be Element of BOOLEAN such that

       A1: a1235 = (s . A1cin) & a4 = (s . dm);

      

       A2: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A3: A1cin in the carrier of S & dm in the carrier of S by Th14;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A2 in the carrier' of S by Th15;

      

      hence (( Following s) . A2) = ( xor2c . (s * <*A1cin, dm*>)) by FACIRC_1: 35

      .= ( xor2c . <*a1235, a4*>) by A1, A3, A2, FINSEQ_2: 125

      .= (a1235 'xor' ( 'not' a4)) by GFACIRC1:def 4;

    end;

    

     Lm19: for ap,bm,cp,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp))) holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bm) & a3 = (s . cp) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,4)) . ( GFA2CarryOutput (( GFA1AdderOutput (ap,bm,cp)),cin,dm))) = ( 'not' (((((a1 'xor' ( 'not' a2)) 'xor' a3) '&' a5) 'or' (a5 '&' ( 'not' a4))) 'or' (( 'not' a4) '&' ((a1 'xor' ( 'not' a2)) 'xor' a3)))) & (( Following (s,4)) . ap) = a1 & (( Following (s,4)) . bm) = a2 & (( Following (s,4)) . cp) = a3 & (( Following (s,4)) . dm) = a4 & (( Following (s,4)) . cin) = a5

    proof

      let ap,bm,cp,dm be non pair set;

      let cin be set such that

       A1: cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp)));

      set S = ( BitFTA1Str (ap,bm,cp,dm,cin));

      

       A2: ap in ( InputVertices S) & bm in ( InputVertices S) by A1, Th16;

      

       A3: cp in ( InputVertices S) & dm in ( InputVertices S) by A1, Th16;

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      let s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin));

      set dmA1 = [ <*dm, A1*>, nor2 ];

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . ap) & a2 = (s . bm) & a3 = (s . cp) & a4 = (s . dm) & a5 = (s . cin);

      

       A5: (( Following (s,3)) . dmA1) = (( 'not' a4) '&' ((a1 'xor' ( 'not' a2)) 'xor' a3)) by A1, A4, Lm15;

      set cindm = [ <*cin, dm*>, and2c ];

      set A1cin = [ <*A1, cin*>, and2a ];

      set A2 = ( GFA2CarryOutput (A1,cin,dm));

      

       A6: ( Following (s,(3 + 1))) = ( Following ( Following (s,3))) by FACIRC_1: 12;

      (( Following (s,3)) . A1cin) = (((a1 'xor' ( 'not' a2)) 'xor' a3) '&' a5) & (( Following (s,3)) . cindm) = (a5 '&' ( 'not' a4)) by A1, A4, Lm15;

      hence (( Following (s,4)) . A2) = ( 'not' (((((a1 'xor' ( 'not' a2)) 'xor' a3) '&' a5) 'or' (a5 '&' ( 'not' a4))) 'or' (( 'not' a4) '&' ((a1 'xor' ( 'not' a2)) 'xor' a3)))) by A6, A5, Lm17;

      

       A7: (( Following (s,3)) . cp) = a3 & (( Following (s,3)) . dm) = a4 by A1, A4, Lm15;

      

       A8: (( Following (s,3)) . cin) = a5 by A1, A4, Lm15;

      

       A9: cin in ( InputVertices S) by A1, Th16;

      (( Following (s,3)) . ap) = a1 & (( Following (s,3)) . bm) = a2 by A1, A4, Lm15;

      hence thesis by A6, A2, A3, A9, A7, A8, CIRCUIT2:def 5;

    end;

    

     Lm20: for ap,bm,cp,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp))) holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bm) & a3 = (s . cp) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,4)) . ( GFA2AdderOutput (( GFA1AdderOutput (ap,bm,cp)),cin,dm))) = ((((a1 'xor' ( 'not' a2)) 'xor' a3) 'xor' ( 'not' a4)) 'xor' a5) & (( Following (s,4)) . ap) = a1 & (( Following (s,4)) . bm) = a2 & (( Following (s,4)) . cp) = a3 & (( Following (s,4)) . dm) = a4 & (( Following (s,4)) . cin) = a5

    proof

      let ap,bm,cp,dm be non pair set;

      let cin be set such that

       A1: cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp)));

      set S = ( BitFTA1Str (ap,bm,cp,dm,cin));

      

       A2: ap in ( InputVertices S) & bm in ( InputVertices S) by A1, Th16;

      

       A3: cp in ( InputVertices S) & dm in ( InputVertices S) by A1, Th16;

      let s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . ap) & a2 = (s . bm) & a3 = (s . cp) & a4 = (s . dm) & a5 = (s . cin);

      

       A5: (( Following (s,3)) . cp) = a3 & (( Following (s,3)) . dm) = a4 by A1, A4, Lm16;

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set A2 = ( GFA2AdderOutput (A1,cin,dm));

      set A1cin = [ <*A1, cin*>, xor2c ];

      

       A6: ( Following (s,(3 + 1))) = ( Following ( Following (s,3))) by FACIRC_1: 12;

      (( Following (s,3)) . A1cin) = (( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3)) 'xor' ( 'not' a5)) & (( Following (s,3)) . dm) = a4 by A1, A4, Lm16;

      

      hence (( Following (s,4)) . A2) = ((((a1 'xor' ( 'not' a2)) 'xor' a3) 'xor' a5) 'xor' ( 'not' a4)) by A6, Lm18

      .= ((((a1 'xor' ( 'not' a2)) 'xor' a3) 'xor' ( 'not' a4)) 'xor' a5) by XBOOLEAN: 73;

      

       A7: (( Following (s,3)) . cin) = a5 by A1, A4, Lm16;

      

       A8: cin in ( InputVertices S) by A1, Th16;

      (( Following (s,3)) . ap) = a1 & (( Following (s,3)) . bm) = a2 by A1, A4, Lm16;

      hence thesis by A6, A2, A3, A8, A5, A7, CIRCUIT2:def 5;

    end;

    theorem :: FTACELL1:19

    for ap,bm,cp,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA1Str (ap,bm,cp))) holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . ap) & a2 = (s . bm) & a3 = (s . cp) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,4)) . ( BitFTA1AdderOutputP (ap,bm,cp,dm,cin))) = ( 'not' (((((a1 'xor' ( 'not' a2)) 'xor' a3) '&' a5) 'or' (a5 '&' ( 'not' a4))) 'or' (( 'not' a4) '&' ((a1 'xor' ( 'not' a2)) 'xor' a3)))) & (( Following (s,4)) . ( BitFTA1AdderOutputQ (ap,bm,cp,dm,cin))) = ((((a1 'xor' ( 'not' a2)) 'xor' a3) 'xor' ( 'not' a4)) 'xor' a5) by Lm19, Lm20;

    theorem :: FTACELL1:20

    for ap,bm,cp,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA1AdderOutput (ap,bm,cp))*>, nor2 ] holds for s be State of ( BitFTA1Circ (ap,bm,cp,dm,cin)) holds ( Following (s,4)) is stable

    proof

      set n1 = 2, n2 = 2;

      let ap,bm,cp,dm be non pair set;

      let cin be set;

      set C = ( BitFTA1Circ (ap,bm,cp,dm,cin));

      set S1 = ( BitGFA1Str (ap,bm,cp));

      set C1 = ( BitGFA1Circ (ap,bm,cp));

      set A1 = ( GFA1AdderOutput (ap,bm,cp));

      set S2 = ( BitGFA2Str (A1,cin,dm));

      set C2 = ( BitGFA2Circ (A1,cin,dm));

      set dmA1 = [ <*dm, A1*>, nor2 ];

      assume

       A1: cin <> dmA1;

      let s be State of C;

      C1 tolerates C2 by CIRCCOMB: 60;

      then

       A2: the Sorts of C1 tolerates the Sorts of C2 by CIRCCOMB:def 3;

      then

      reconsider s1 = (s | the carrier of S1) as State of C1 by CIRCCOMB: 26;

      reconsider s2 = (( Following (s,n1)) | the carrier of S2) as State of C2 by A2, CIRCCOMB: 26;

      

       A3: ( InputVertices S1) misses ( InnerVertices S2) & ( Following (s1,n1)) is stable by Lm12, GFACIRC1: 72;

      ( Following (s2,n2)) is stable by A1, Lm11, GFACIRC1: 104;

      then ( Following (s,(n1 + n2))) is stable by A3, CIRCCMB2: 19, CIRCCOMB: 60;

      hence thesis;

    end;

    begin

    definition

      let am,bp,cm,dp,cin be set;

      :: FTACELL1:def13

      func BitFTA2Str (am,bp,cm,dp,cin) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( BitGFA2Str (am,bp,cm)) +* ( BitGFA1Str (( GFA2AdderOutput (am,bp,cm)),cin,dp)));

      coherence ;

    end

    definition

      let am,bp,cm,dp,cin be set;

      :: FTACELL1:def14

      func BitFTA2Circ (am,bp,cm,dp,cin) -> strict Boolean gate`2=den Circuit of ( BitFTA2Str (am,bp,cm,dp,cin)) equals (( BitGFA2Circ (am,bp,cm)) +* ( BitGFA1Circ (( GFA2AdderOutput (am,bp,cm)),cin,dp)));

      coherence ;

    end

    theorem :: FTACELL1:21

    

     Th21: for am,bp,cm,dp,cin be set holds ( 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))})

    proof

      let am,bp,cm,dp,cin be set;

      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 (A1,cin,dp));

      set A2 = ( GFA1AdderOutput (A1,cin,dp));

      set C2 = ( GFA1CarryOutput (A1,cin,dp));

      set ambp0 = [ <*am, bp*>, xor2c ];

      set ambp = [ <*am, bp*>, and2a ];

      set bpcm = [ <*bp, cm*>, and2c ];

      set cmam = [ <*cm, am*>, nor2 ];

      set A1cin0 = [ <*A1, cin*>, xor2c ];

      set A1cin = [ <*A1, cin*>, and2c ];

      set cindp = [ <*cin, dp*>, and2a ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      S1 tolerates S2 by CIRCCOMB: 47;

      

      hence ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by CIRCCOMB: 11

      .= (((( {ambp0} \/ {A1}) \/ {ambp, bpcm, cmam}) \/ {C1}) \/ ( InnerVertices S2)) by GFACIRC1: 95

      .= ((( {ambp0, A1} \/ {ambp, bpcm, cmam}) \/ {C1}) \/ ( InnerVertices S2)) by ENUMSET1: 1

      .= (( {ambp0, A1} \/ ( {ambp, bpcm, cmam} \/ {C1})) \/ ( InnerVertices S2)) by XBOOLE_1: 4

      .= (( {ambp0, A1} \/ {ambp, bpcm, cmam, C1}) \/ ( InnerVertices S2)) by ENUMSET1: 6

      .= (( {ambp0, A1} \/ {ambp, bpcm, cmam, C1}) \/ ((( {A1cin0} \/ {A2}) \/ {A1cin, cindp, dpA1}) \/ {C2})) by GFACIRC1: 63

      .= (( {ambp0, A1} \/ {ambp, bpcm, cmam, C1}) \/ (( {A1cin0, A2} \/ {A1cin, cindp, dpA1}) \/ {C2})) by ENUMSET1: 1

      .= (( {ambp0, A1} \/ {ambp, bpcm, cmam, C1}) \/ ( {A1cin0, A2} \/ ( {A1cin, cindp, dpA1} \/ {C2}))) by XBOOLE_1: 4

      .= (( {ambp0, A1} \/ {ambp, bpcm, cmam, C1}) \/ ( {A1cin0, A2} \/ {A1cin, cindp, dpA1, C2})) by ENUMSET1: 6

      .= ((( {ambp0, A1} \/ {ambp, bpcm, cmam, C1}) \/ {A1cin0, A2}) \/ {A1cin, cindp, dpA1, C2}) by XBOOLE_1: 4;

    end;

    theorem :: FTACELL1:22

    for am,bp,cm,dp,cin be set holds ( InnerVertices ( BitFTA2Str (am,bp,cm,dp,cin))) is Relation

    proof

      let am,bp,cm,dp,cin be set;

      set S1 = ( BitGFA2Str (am,bp,cm));

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set S2 = ( BitGFA1Str (A1,cin,dp));

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by GFACIRC1: 64, GFACIRC1: 96;

      hence thesis by FACIRC_1: 3;

    end;

    

     Lm21: for x,y,z be set holds for p be set holds ( GFA2AdderOutput (x,y,z)) <> [p, and2a ]

    proof

      let x,y,z be set, p be set;

      set A1 = ( GFA2AdderOutput (x,y,z));

      (A1 `2 ) = xor2c ;

      then ( [p, and2a ] `2 ) <> (A1 `2 ) by GFACIRC1: 4, TWOSCOMP: 9;

      hence thesis;

    end;

    

     Lm22: for am,bp,cm be non pair set holds for x,y,z be set holds ( InputVertices ( BitGFA2Str (am,bp,cm))) misses ( InnerVertices ( BitGFA1Str (x,y,z)))

    proof

      let am,bp,cm be non pair set;

      let x,y,z be set;

      set S1 = ( BitGFA2Str (am,bp,cm));

      ( InputVertices S1) is without_pairs by GFACIRC1: 99;

      hence thesis by FACIRC_1: 5, GFACIRC1: 64;

    end;

    theorem :: FTACELL1:23

    

     Th23: for am,bp,cm,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm))) holds ( InputVertices ( BitFTA2Str (am,bp,cm,dp,cin))) = {am, bp, cm, dp, cin}

    proof

      let am,bp,cm,dp be non pair set;

      let cin be set;

      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 (A1,cin,dp));

      set ambp0 = [ <*am, bp*>, xor2c ];

      set ambp = [ <*am, bp*>, and2a ];

      set bpcm = [ <*bp, cm*>, and2c ];

      set cmam = [ <*cm, am*>, nor2 ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      assume that

       A1: cin <> dpA1 and

       A2: not cin in ( InnerVertices S1);

      

       A3: not dp in {A1, ambp0, ambp, bpcm, cmam, C1} by ENUMSET1:def 4;

      A1 in {A1, ambp0, ambp, bpcm, cmam, C1} by ENUMSET1:def 4;

      then

       A4: ( {A1} \ {A1, ambp0, ambp, bpcm, cmam, C1}) = {} by ZFMISC_1: 60;

      

       A5: ( InnerVertices S1) = ((( {ambp0} \/ {A1}) \/ {ambp, bpcm, cmam}) \/ {C1}) by GFACIRC1: 95

      .= (( {ambp0, A1} \/ {ambp, bpcm, cmam}) \/ {C1}) by ENUMSET1: 1

      .= ( {ambp0, A1} \/ ( {ambp, bpcm, cmam} \/ {C1})) by XBOOLE_1: 4

      .= ( {A1, ambp0} \/ {ambp, bpcm, cmam, C1}) by ENUMSET1: 6

      .= {A1, ambp0, ambp, bpcm, cmam, C1} by ENUMSET1: 12;

      

      then

       A6: ( {A1, cin, dp} \ ( InnerVertices S1)) = (( {A1} \/ {cin, dp}) \ {A1, ambp0, ambp, bpcm, cmam, C1}) by ENUMSET1: 2

      .= (( {A1} \ {A1, ambp0, ambp, bpcm, cmam, C1}) \/ ( {cin, dp} \ {A1, ambp0, ambp, bpcm, cmam, C1})) by XBOOLE_1: 42

      .= (( {cin} \/ {dp}) \ {A1, ambp0, ambp, bpcm, cmam, C1}) by A4, ENUMSET1: 1

      .= (( {cin} \ {A1, ambp0, ambp, bpcm, cmam, C1}) \/ ( {dp} \ {A1, ambp0, ambp, bpcm, cmam, C1})) by XBOOLE_1: 42

      .= ( {cin} \/ ( {dp} \ {A1, ambp0, ambp, bpcm, cmam, C1})) by A2, A5, ZFMISC_1: 59

      .= ( {cin} \/ {dp}) by A3, ZFMISC_1: 59

      .= {cin, dp} by ENUMSET1: 1;

      ( InnerVertices S2) misses ( InputVertices S1) & S1 tolerates S2 by Lm22, CIRCCOMB: 47;

      

      hence ( InputVertices S) = (( InputVertices S1) \/ (( InputVertices S2) \ ( InnerVertices S1))) by FACIRC_1: 4

      .= ( {am, bp, cm} \/ (( InputVertices S2) \ ( InnerVertices S1))) by GFACIRC1: 98

      .= ( {am, bp, cm} \/ ( {A1, cin, dp} \ ( InnerVertices S1))) by A1, Lm21, GFACIRC1: 65

      .= {am, bp, cm, dp, cin} by A6, ENUMSET1: 9;

    end;

    theorem :: FTACELL1:24

    

     Th24: for am,bp,cm,dp,cin be set holds am in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & bp in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & cm in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & dp in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & cin in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & [ <*am, bp*>, xor2c ] in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & ( GFA2AdderOutput (am,bp,cm)) in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & [ <*am, bp*>, and2a ] in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & [ <*bp, cm*>, and2c ] in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & [ <*cm, am*>, nor2 ] in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & ( GFA2CarryOutput (am,bp,cm)) in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & [ <*( GFA2AdderOutput (am,bp,cm)), cin*>, xor2c ] in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & ( GFA1AdderOutput (( GFA2AdderOutput (am,bp,cm)),cin,dp)) in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & [ <*( GFA2AdderOutput (am,bp,cm)), cin*>, and2c ] in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & [ <*cin, dp*>, and2a ] in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin)) & ( GFA1CarryOutput (( GFA2AdderOutput (am,bp,cm)),cin,dp)) in the carrier of ( BitFTA2Str (am,bp,cm,dp,cin))

    proof

      let am,bp,cm,dp,cin be set;

      set S1 = ( BitGFA2Str (am,bp,cm));

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set C1 = ( GFA2CarryOutput (am,bp,cm));

      set S2 = ( BitGFA1Str (A1,cin,dp));

      set A2 = ( GFA1AdderOutput (A1,cin,dp));

      set C2 = ( GFA1CarryOutput (A1,cin,dp));

      set ambp0 = [ <*am, bp*>, xor2c ];

      set ambp = [ <*am, bp*>, and2a ];

      set bpcm = [ <*bp, cm*>, and2c ];

      set cmam = [ <*cm, am*>, nor2 ];

      set A1cin0 = [ <*A1, cin*>, xor2c ];

      set A1cin = [ <*A1, cin*>, and2c ];

      set cindp = [ <*cin, dp*>, and2a ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      

       A1: cm in the carrier of S1 & ambp0 in the carrier of S1 by GFACIRC1: 100;

      

       A2: ambp in the carrier of S1 & bpcm in the carrier of S1 by GFACIRC1: 100;

      

       A3: A1 in the carrier of S2 & cin in the carrier of S2 by GFACIRC1: 68;

      

       A4: cmam in the carrier of S1 & C1 in the carrier of S1 by GFACIRC1: 100;

      

       A5: C2 in the carrier of S2 by GFACIRC1: 68;

      

       A6: cindp in the carrier of S2 & dpA1 in the carrier of S2 by GFACIRC1: 68;

      

       A7: A2 in the carrier of S2 & A1cin in the carrier of S2 by GFACIRC1: 68;

      

       A8: dp in the carrier of S2 & A1cin0 in the carrier of S2 by GFACIRC1: 68;

      am in the carrier of S1 & bp in the carrier of S1 by GFACIRC1: 100;

      hence thesis by A1, A2, A4, A3, A8, A7, A6, A5, FACIRC_1: 20;

    end;

    theorem :: FTACELL1:25

    

     Th25: for am,bp,cm,dp,cin be set holds [ <*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)))

    proof

      let am,bp,cm,dp,cin be set;

      set S = ( BitFTA2Str (am,bp,cm,dp,cin));

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set C1 = ( GFA2CarryOutput (am,bp,cm));

      set A2 = ( GFA1AdderOutput (A1,cin,dp));

      set C2 = ( GFA1CarryOutput (A1,cin,dp));

      set ambp0 = [ <*am, bp*>, xor2c ];

      set ambp = [ <*am, bp*>, and2a ];

      set bpcm = [ <*bp, cm*>, and2c ];

      set cmam = [ <*cm, am*>, nor2 ];

      set A1cin0 = [ <*A1, cin*>, xor2c ];

      set A1cin = [ <*A1, cin*>, and2c ];

      set cindp = [ <*cin, dp*>, and2a ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      set p1 = {ambp0, A1, ambp, bpcm, cmam, C1};

      set p2 = {A1cin0, A2, A1cin, cindp, dpA1, C2};

      

       A1: ambp0 in p1 & A1 in p1 by ENUMSET1:def 4;

      

       A2: ambp in p1 & bpcm in p1 by ENUMSET1:def 4;

      

       A3: A1cin0 in p2 & A2 in p2 by ENUMSET1:def 4;

      

       A4: cmam in p1 & C1 in p1 by ENUMSET1:def 4;

      

       A5: dpA1 in p2 & C2 in p2 by ENUMSET1:def 4;

      

       A6: A1cin in p2 & cindp in p2 by ENUMSET1:def 4;

      ( InnerVertices S) = ((( {ambp0, A1} \/ {ambp, bpcm, cmam, C1}) \/ {A1cin0, A2}) \/ {A1cin, cindp, dpA1, C2}) by Th21

      .= ((p1 \/ {A1cin0, A2}) \/ {A1cin, cindp, dpA1, C2}) by ENUMSET1: 12

      .= (p1 \/ ( {A1cin0, A2} \/ {A1cin, cindp, dpA1, C2})) by XBOOLE_1: 4

      .= (p1 \/ p2) by ENUMSET1: 12;

      hence thesis by A1, A2, A4, A3, A6, A5, XBOOLE_0:def 3;

    end;

    theorem :: FTACELL1:26

    

     Th26: for am,bp,cm,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm))) holds am in ( InputVertices ( BitFTA2Str (am,bp,cm,dp,cin))) & bp in ( InputVertices ( BitFTA2Str (am,bp,cm,dp,cin))) & cm in ( InputVertices ( BitFTA2Str (am,bp,cm,dp,cin))) & dp in ( InputVertices ( BitFTA2Str (am,bp,cm,dp,cin))) & cin in ( InputVertices ( BitFTA2Str (am,bp,cm,dp,cin)))

    proof

      let am,bp,cm,dp be non pair set;

      let cin be set;

      set S = ( BitFTA2Str (am,bp,cm,dp,cin));

      set S1 = ( BitGFA2Str (am,bp,cm));

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set dpA1 = [ <*dp, A1*>, and2 ];

      assume cin <> dpA1 & not cin in ( InnerVertices S1);

      then ( InputVertices S) = {am, bp, cm, dp, cin} by Th23;

      hence thesis by ENUMSET1:def 3;

    end;

    definition

      let am,bp,cm,dp,cin be set;

      :: FTACELL1:def15

      func BitFTA2CarryOutput (am,bp,cm,dp,cin) -> Element of ( InnerVertices ( BitFTA2Str (am,bp,cm,dp,cin))) equals ( GFA2CarryOutput (am,bp,cm));

      coherence by Th25;

      :: FTACELL1:def16

      func BitFTA2AdderOutputI (am,bp,cm,dp,cin) -> Element of ( InnerVertices ( BitFTA2Str (am,bp,cm,dp,cin))) equals ( GFA2AdderOutput (am,bp,cm));

      coherence by Th25;

      :: FTACELL1:def17

      func BitFTA2AdderOutputP (am,bp,cm,dp,cin) -> Element of ( InnerVertices ( BitFTA2Str (am,bp,cm,dp,cin))) equals ( GFA1CarryOutput (( GFA2AdderOutput (am,bp,cm)),cin,dp));

      coherence by Th25;

      :: FTACELL1:def18

      func BitFTA2AdderOutputQ (am,bp,cm,dp,cin) -> Element of ( InnerVertices ( BitFTA2Str (am,bp,cm,dp,cin))) equals ( GFA1AdderOutput (( GFA2AdderOutput (am,bp,cm)),cin,dp));

      coherence by Th25;

    end

    theorem :: FTACELL1:27

    for am,bp,cm be non pair set holds for dp,cin be set holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bp) & a3 = (s . cm) holds (( Following (s,2)) . ( BitFTA2CarryOutput (am,bp,cm,dp,cin))) = ( 'not' (((( 'not' a1) '&' a2) 'or' (a2 '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1)))) & (( Following (s,2)) . ( BitFTA2AdderOutputI (am,bp,cm,dp,cin))) = ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3))

    proof

      let am,bp,cm be non pair set;

      let dp,cin be set;

      let s be State of ( BitFTA2Circ (am,bp,cm,dp,cin));

      set S1 = ( BitGFA2Str (am,bp,cm));

      set C1 = ( BitGFA2Circ (am,bp,cm));

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set A2 = ( GFA2CarryOutput (am,bp,cm));

      set S2 = ( BitGFA1Str (A1,cin,dp));

      set C2 = ( BitGFA1Circ (A1,cin,dp));

      let a1,a2,a3 be Element of BOOLEAN such that

       A1: a1 = (s . am) and

       A2: a2 = (s . bp) and

       A3: a3 = (s . cm);

      reconsider s1 = (s | the carrier of S1) as State of C1 by FACIRC_1: 26;

      

       A4: ( dom s1) = the carrier of S1 by CIRCUIT1: 3;

      am in the carrier of S1 by GFACIRC1: 100;

      then

       A5: a1 = (s1 . am) by A1, A4, FUNCT_1: 47;

      reconsider t = s as State of (C1 +* C2);

      

       A6: ( InputVertices S1) misses ( InnerVertices S2) by Lm22;

      cm in the carrier of S1 by GFACIRC1: 100;

      then

       A7: a3 = (s1 . cm) by A3, A4, FUNCT_1: 47;

      bp in the carrier of S1 by GFACIRC1: 100;

      then

       A8: a2 = (s1 . bp) by A2, A4, FUNCT_1: 47;

      A2 in the carrier of S1 by GFACIRC1: 100;

      then (( Following (t,2)) . ( GFA2CarryOutput (am,bp,cm))) = (( Following (s1,2)) . ( GFA2CarryOutput (am,bp,cm))) by A6, FACIRC_1: 32;

      hence (( Following (s,2)) . ( BitFTA2CarryOutput (am,bp,cm,dp,cin))) = ( 'not' (((( 'not' a1) '&' a2) 'or' (a2 '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1)))) by A5, A8, A7, GFACIRC1: 103;

      A1 in the carrier of S1 by GFACIRC1: 100;

      then (( Following (t,2)) . ( GFA2AdderOutput (am,bp,cm))) = (( Following (s1,2)) . ( GFA2AdderOutput (am,bp,cm))) by A6, FACIRC_1: 32;

      hence thesis by A5, A8, A7, GFACIRC1: 103;

    end;

    theorem :: FTACELL1:28

    

     Th28: for am,bp,cm,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm))) holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bp) & a3 = (s . cm) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,2)) . ( GFA2AdderOutput (am,bp,cm))) = ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) & (( Following (s,2)) . am) = a1 & (( Following (s,2)) . bp) = a2 & (( Following (s,2)) . cm) = a3 & (( Following (s,2)) . dp) = a4 & (( Following (s,2)) . cin) = a5

    proof

      let am,bp,cm,dp be non pair set;

      let cin be set such that

       A1: cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm)));

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set C1 = ( BitGFA2Circ (am,bp,cm));

      set S1 = ( BitGFA2Str (am,bp,cm));

      set S2 = ( BitGFA1Str (A1,cin,dp));

      set C2 = ( BitGFA1Circ (A1,cin,dp));

      set S = ( BitFTA2Str (am,bp,cm,dp,cin));

      let s be State of ( BitFTA2Circ (am,bp,cm,dp,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A2: a1 = (s . am) and

       A3: a2 = (s . bp) and

       A4: a3 = (s . cm) and

       A5: a4 = (s . dp) and

       A6: a5 = (s . cin);

      reconsider s1 = (s | the carrier of S1) as State of C1 by FACIRC_1: 26;

      

       A7: ( dom s1) = the carrier of S1 by CIRCUIT1: 3;

      

       A8: dp in ( InputVertices S) by A1, Th26;

      then

       A9: (( Following s) . dp) = a4 by A5, CIRCUIT2:def 5;

      

       A10: cm in ( InputVertices S) by A1, Th26;

      then

       A11: (( Following s) . cm) = a3 by A4, CIRCUIT2:def 5;

      bp in the carrier of S1 by GFACIRC1: 100;

      then

       A12: a2 = (s1 . bp) by A3, A7, FUNCT_1: 47;

      reconsider t = s as State of (C1 +* C2);

      A1 in the carrier of S1 & ( InputVertices S1) misses ( InnerVertices S2) by Lm22, GFACIRC1: 100;

      then

       A13: (( Following (t,2)) . ( GFA2AdderOutput (am,bp,cm))) = (( Following (s1,2)) . ( GFA2AdderOutput (am,bp,cm))) by FACIRC_1: 32;

      cm in the carrier of S1 by GFACIRC1: 100;

      then

       A14: a3 = (s1 . cm) by A4, A7, FUNCT_1: 47;

      am in the carrier of S1 by GFACIRC1: 100;

      then a1 = (s1 . am) by A2, A7, FUNCT_1: 47;

      hence (( Following (s,2)) . ( GFA2AdderOutput (am,bp,cm))) = ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) by A12, A14, A13, GFACIRC1: 103;

      

       A15: bp in ( InputVertices S) by A1, Th26;

      then

       A16: (( Following s) . bp) = a2 by A3, CIRCUIT2:def 5;

      

       A17: cin in ( InputVertices S) by A1, Th26;

      then

       A18: (( Following s) . cin) = a5 by A6, CIRCUIT2:def 5;

      

       A19: am in ( InputVertices S) by A1, Th26;

      then ( Following (s,2)) = ( Following ( Following s)) & (( Following s) . am) = a1 by A2, CIRCUIT2:def 5, FACIRC_1: 15;

      hence thesis by A19, A15, A10, A8, A17, A16, A11, A9, A18, CIRCUIT2:def 5;

    end;

    

     Lm23: for am,bp,cm,dp be non pair set holds for cin be set holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds for a123,a4,a5 be Element of BOOLEAN st a123 = (s . ( GFA2AdderOutput (am,bp,cm))) & a4 = (s . dp) & a5 = (s . cin) holds (( Following s) . [ <*( GFA2AdderOutput (am,bp,cm)), cin*>, and2c ]) = (a123 '&' ( 'not' a5)) & (( Following s) . [ <*cin, dp*>, and2a ]) = (( 'not' a5) '&' a4) & (( Following s) . [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ]) = (a4 '&' a123)

    proof

      let am,bp,cm,dp be non pair set;

      let cin be set;

      set S = ( BitFTA2Str (am,bp,cm,dp,cin));

      set C = ( BitFTA2Circ (am,bp,cm,dp,cin));

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set A1cin = [ <*A1, cin*>, and2c ];

      set cindp = [ <*cin, dp*>, and2a ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      let s be State of C;

      let a123,a4,a5 be Element of BOOLEAN such that

       A1: a123 = (s . A1) and

       A2: a4 = (s . dp) and

       A3: a5 = (s . cin);

      

       A4: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A5: cin in the carrier of S by Th24;

      

       A6: A1 in the carrier of S by Th24;

      

       A7: ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A1cin in the carrier' of S by Th25;

      

      hence (( Following s) . A1cin) = ( and2c . (s * <*A1, cin*>)) by FACIRC_1: 35

      .= ( and2c . <*a123, a5*>) by A1, A3, A6, A5, A4, FINSEQ_2: 125

      .= (a123 '&' ( 'not' a5)) by GFACIRC1:def 3;

      

       A8: dp in the carrier of S by Th24;

      cindp in the carrier' of S by A7, Th25;

      

      hence (( Following s) . cindp) = ( and2a . (s * <*cin, dp*>)) by FACIRC_1: 35

      .= ( and2a . <*a5, a4*>) by A2, A3, A8, A5, A4, FINSEQ_2: 125

      .= (( 'not' a5) '&' a4) by TWOSCOMP:def 2;

      dpA1 in the carrier' of S by A7, Th25;

      

      hence (( Following s) . dpA1) = ( and2 . (s * <*dp, A1*>)) by FACIRC_1: 35

      .= ( and2 . <*a4, a123*>) by A1, A2, A6, A8, A4, FINSEQ_2: 125

      .= (a4 '&' a123) by FACIRC_1:def 6;

    end;

    

     Lm24: for am,bp,cm,dp be non pair set holds for cin be set holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds for a123,a5 be Element of BOOLEAN st a123 = (s . ( GFA2AdderOutput (am,bp,cm))) & a5 = (s . cin) holds (( Following s) . [ <*( GFA2AdderOutput (am,bp,cm)), cin*>, xor2c ]) = (a123 'xor' ( 'not' a5))

    proof

      let am,bp,cm,dp be non pair set;

      let cin be set;

      set S = ( BitFTA2Str (am,bp,cm,dp,cin));

      set C = ( BitFTA2Circ (am,bp,cm,dp,cin));

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set A1cin = [ <*A1, cin*>, xor2c ];

      let s be State of C;

      let a123,a5 be Element of BOOLEAN such that

       A1: a123 = (s . A1) & a5 = (s . cin);

      

       A2: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A3: A1 in the carrier of S & cin in the carrier of S by Th24;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A1cin in the carrier' of S by Th25;

      

      hence (( Following s) . A1cin) = ( xor2c . (s * <*A1, cin*>)) by FACIRC_1: 35

      .= ( xor2c . <*a123, a5*>) by A1, A3, A2, FINSEQ_2: 125

      .= (a123 'xor' ( 'not' a5)) by GFACIRC1:def 4;

    end;

    

     Lm25: for am,bp,cm,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm))) holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bp) & a3 = (s . cm) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,3)) . [ <*( GFA2AdderOutput (am,bp,cm)), cin*>, and2c ]) = (((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) '&' ( 'not' a5)) & (( Following (s,3)) . [ <*cin, dp*>, and2a ]) = (( 'not' a5) '&' a4) & (( Following (s,3)) . [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ]) = (a4 '&' ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3))) & (( Following (s,3)) . am) = a1 & (( Following (s,3)) . bp) = a2 & (( Following (s,3)) . cm) = a3 & (( Following (s,3)) . dp) = a4 & (( Following (s,3)) . cin) = a5

    proof

      let am,bp,cm,dp be non pair set;

      let cin be set such that

       A1: cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm)));

      set S = ( BitFTA2Str (am,bp,cm,dp,cin));

      

       A2: am in ( InputVertices S) & bp in ( InputVertices S) by A1, Th26;

      

       A3: cm in ( InputVertices S) & dp in ( InputVertices S) by A1, Th26;

      let s be State of ( BitFTA2Circ (am,bp,cm,dp,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . am) & a2 = (s . bp) & a3 = (s . cm) & a4 = (s . dp) & a5 = (s . cin);

      

       A5: (( Following (s,2)) . cin) = a5 by A1, A4, Th28;

      set cindp = [ <*cin, dp*>, and2a ];

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set A1cin = [ <*A1, cin*>, and2c ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      

       A6: ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) by FACIRC_1: 12;

      (( Following (s,2)) . A1) = ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) & (( Following (s,2)) . dp) = a4 by A1, A4, Th28;

      hence (( Following (s,3)) . A1cin) = (((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) '&' ( 'not' a5)) & (( Following (s,3)) . cindp) = (( 'not' a5) '&' a4) & (( Following (s,3)) . dpA1) = (a4 '&' ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3))) by A6, A5, Lm23;

      

       A7: (( Following (s,2)) . cm) = a3 & (( Following (s,2)) . dp) = a4 by A1, A4, Th28;

      

       A8: (( Following (s,2)) . cin) = a5 by A1, A4, Th28;

      

       A9: cin in ( InputVertices S) by A1, Th26;

      (( Following (s,2)) . am) = a1 & (( Following (s,2)) . bp) = a2 by A1, A4, Th28;

      hence thesis by A6, A2, A3, A9, A7, A8, CIRCUIT2:def 5;

    end;

    

     Lm26: for am,bp,cm,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm))) holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bp) & a3 = (s . cm) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,3)) . [ <*( GFA2AdderOutput (am,bp,cm)), cin*>, xor2c ]) = (((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) 'xor' ( 'not' a5)) & (( Following (s,3)) . am) = a1 & (( Following (s,3)) . bp) = a2 & (( Following (s,3)) . cm) = a3 & (( Following (s,3)) . dp) = a4 & (( Following (s,3)) . cin) = a5

    proof

      let am,bp,cm,dp be non pair set;

      let cin be set such that

       A1: cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm)));

      set S = ( BitFTA2Str (am,bp,cm,dp,cin));

      

       A2: am in ( InputVertices S) & bp in ( InputVertices S) by A1, Th26;

      

       A3: cm in ( InputVertices S) & dp in ( InputVertices S) by A1, Th26;

      let s be State of ( BitFTA2Circ (am,bp,cm,dp,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . am) & a2 = (s . bp) & a3 = (s . cm) & a4 = (s . dp) & a5 = (s . cin);

      

       A5: (( Following (s,2)) . cm) = a3 & (( Following (s,2)) . dp) = a4 by A1, A4, Th28;

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set A1cin = [ <*A1, cin*>, xor2c ];

      

       A6: ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) by FACIRC_1: 12;

      (( Following (s,2)) . A1) = ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) & (( Following (s,2)) . cin) = a5 by A1, A4, Th28;

      hence (( Following (s,3)) . A1cin) = (((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) 'xor' ( 'not' a5)) by A6, Lm24;

      

       A7: (( Following (s,2)) . cin) = a5 by A1, A4, Th28;

      

       A8: cin in ( InputVertices S) by A1, Th26;

      (( Following (s,2)) . am) = a1 & (( Following (s,2)) . bp) = a2 by A1, A4, Th28;

      hence thesis by A6, A2, A3, A8, A5, A7, CIRCUIT2:def 5;

    end;

    

     Lm27: for am,bp,cm,dp be non pair set holds for cin be set holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds for a123x,a123y,a123z be Element of BOOLEAN st a123x = (s . [ <*( GFA2AdderOutput (am,bp,cm)), cin*>, and2c ]) & a123y = (s . [ <*cin, dp*>, and2a ]) & a123z = (s . [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ]) holds (( Following s) . ( GFA1CarryOutput (( GFA2AdderOutput (am,bp,cm)),cin,dp))) = ((a123x 'or' a123y) 'or' a123z)

    proof

      let am,bp,cm,dp be non pair set;

      let cin be set;

      set S = ( BitFTA2Str (am,bp,cm,dp,cin));

      set C = ( BitFTA2Circ (am,bp,cm,dp,cin));

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set A2 = ( GFA1CarryOutput (A1,cin,dp));

      set A1cin = [ <*A1, cin*>, and2c ];

      set cindp = [ <*cin, dp*>, and2a ];

      set dpA1 = [ <*dp, A1*>, and2 ];

      let s be State of C;

      let a123x,a123y,a123z be Element of BOOLEAN such that

       A1: a123x = (s . A1cin) & a123y = (s . cindp) & a123z = (s . dpA1);

      

       A2: A1cin in the carrier of S & cindp in the carrier of S by Th24;

      

       A3: dpA1 in the carrier of S & ( dom s) = the carrier of S by Th24, CIRCUIT1: 3;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A2 in the carrier' of S by Th25;

      

      hence (( Following s) . A2) = ( or3 . (s * <*A1cin, cindp, dpA1*>)) by FACIRC_1: 35

      .= ( or3 . <*a123x, a123y, a123z*>) by A1, A2, A3, FINSEQ_2: 126

      .= ((a123x 'or' a123y) 'or' a123z) by FACIRC_1:def 7;

    end;

    

     Lm28: for am,bp,cm,dp be non pair set holds for cin be set holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds for a1235,a4 be Element of BOOLEAN st a1235 = (s . [ <*( GFA2AdderOutput (am,bp,cm)), cin*>, xor2c ]) & a4 = (s . dp) holds (( Following s) . ( GFA1AdderOutput (( GFA2AdderOutput (am,bp,cm)),cin,dp))) = (a1235 'xor' ( 'not' a4))

    proof

      let am,bp,cm,dp be non pair set;

      let cin be set;

      set S = ( BitFTA2Str (am,bp,cm,dp,cin));

      set C = ( BitFTA2Circ (am,bp,cm,dp,cin));

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set A2 = ( GFA1AdderOutput (A1,cin,dp));

      set A1cin = [ <*A1, cin*>, xor2c ];

      let s be State of C;

      let a1235,a4 be Element of BOOLEAN such that

       A1: a1235 = (s . A1cin) & a4 = (s . dp);

      

       A2: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A3: A1cin in the carrier of S & dp in the carrier of S by Th24;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A2 in the carrier' of S by Th25;

      

      hence (( Following s) . A2) = ( xor2c . (s * <*A1cin, dp*>)) by FACIRC_1: 35

      .= ( xor2c . <*a1235, a4*>) by A1, A3, A2, FINSEQ_2: 125

      .= (a1235 'xor' ( 'not' a4)) by GFACIRC1:def 4;

    end;

    

     Lm29: for am,bp,cm,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm))) holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bp) & a3 = (s . cm) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,4)) . ( GFA1CarryOutput (( GFA2AdderOutput (am,bp,cm)),cin,dp))) = (((((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) '&' ( 'not' a5)) 'or' (( 'not' a5) '&' a4)) 'or' (a4 '&' ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)))) & (( Following (s,4)) . am) = a1 & (( Following (s,4)) . bp) = a2 & (( Following (s,4)) . cm) = a3 & (( Following (s,4)) . dp) = a4 & (( Following (s,4)) . cin) = a5

    proof

      let am,bp,cm,dp be non pair set;

      let cin be set such that

       A1: cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm)));

      set S = ( BitFTA2Str (am,bp,cm,dp,cin));

      

       A2: am in ( InputVertices S) & bp in ( InputVertices S) by A1, Th26;

      

       A3: cm in ( InputVertices S) & dp in ( InputVertices S) by A1, Th26;

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      let s be State of ( BitFTA2Circ (am,bp,cm,dp,cin));

      set dpA1 = [ <*dp, A1*>, and2 ];

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . am) & a2 = (s . bp) & a3 = (s . cm) & a4 = (s . dp) & a5 = (s . cin);

      

       A5: (( Following (s,3)) . dpA1) = (a4 '&' ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3))) by A1, A4, Lm25;

      set cindp = [ <*cin, dp*>, and2a ];

      set A1cin = [ <*A1, cin*>, and2c ];

      set A2 = ( GFA1CarryOutput (A1,cin,dp));

      

       A6: ( Following (s,(3 + 1))) = ( Following ( Following (s,3))) by FACIRC_1: 12;

      (( Following (s,3)) . A1cin) = (((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) '&' ( 'not' a5)) & (( Following (s,3)) . cindp) = (( 'not' a5) '&' a4) by A1, A4, Lm25;

      hence (( Following (s,4)) . A2) = (((((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) '&' ( 'not' a5)) 'or' (( 'not' a5) '&' a4)) 'or' (a4 '&' ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)))) by A6, A5, Lm27;

      

       A7: (( Following (s,3)) . cm) = a3 & (( Following (s,3)) . dp) = a4 by A1, A4, Lm25;

      

       A8: (( Following (s,3)) . cin) = a5 by A1, A4, Lm25;

      

       A9: cin in ( InputVertices S) by A1, Th26;

      (( Following (s,3)) . am) = a1 & (( Following (s,3)) . bp) = a2 by A1, A4, Lm25;

      hence thesis by A6, A2, A3, A9, A7, A8, CIRCUIT2:def 5;

    end;

    

     Lm30: for am,bp,cm,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm))) holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bp) & a3 = (s . cm) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,4)) . ( GFA1AdderOutput (( GFA2AdderOutput (am,bp,cm)),cin,dp))) = ( 'not' ((((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) 'xor' a4) 'xor' ( 'not' a5))) & (( Following (s,4)) . am) = a1 & (( Following (s,4)) . bp) = a2 & (( Following (s,4)) . cm) = a3 & (( Following (s,4)) . dp) = a4 & (( Following (s,4)) . cin) = a5

    proof

      let am,bp,cm,dp be non pair set;

      let cin be set such that

       A1: cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm)));

      set S = ( BitFTA2Str (am,bp,cm,dp,cin));

      

       A2: am in ( InputVertices S) & bp in ( InputVertices S) by A1, Th26;

      

       A3: cm in ( InputVertices S) & dp in ( InputVertices S) by A1, Th26;

      let s be State of ( BitFTA2Circ (am,bp,cm,dp,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . am) & a2 = (s . bp) & a3 = (s . cm) & a4 = (s . dp) & a5 = (s . cin);

      

       A5: (( Following (s,3)) . cm) = a3 & (( Following (s,3)) . dp) = a4 by A1, A4, Lm26;

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set A2 = ( GFA1AdderOutput (A1,cin,dp));

      set A1cin = [ <*A1, cin*>, xor2c ];

      

       A6: ( Following (s,(3 + 1))) = ( Following ( Following (s,3))) by FACIRC_1: 12;

      (( Following (s,3)) . A1cin) = (((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) 'xor' ( 'not' a5)) & (( Following (s,3)) . dp) = a4 by A1, A4, Lm26;

      

      hence (( Following (s,4)) . A2) = ((((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) 'xor' ( 'not' a5)) 'xor' ( 'not' a4)) by A6, Lm28

      .= ( 'not' ((((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) 'xor' ( 'not' a5)) 'xor' a4)) by XBOOLEAN: 74

      .= ( 'not' ((((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) 'xor' a4) 'xor' ( 'not' a5))) by XBOOLEAN: 73;

      

       A7: (( Following (s,3)) . cin) = a5 by A1, A4, Lm26;

      

       A8: cin in ( InputVertices S) by A1, Th26;

      (( Following (s,3)) . am) = a1 & (( Following (s,3)) . bp) = a2 by A1, A4, Lm26;

      hence thesis by A6, A2, A3, A8, A5, A7, CIRCUIT2:def 5;

    end;

    theorem :: FTACELL1:29

    for am,bp,cm,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] & not cin in ( InnerVertices ( BitGFA2Str (am,bp,cm))) holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bp) & a3 = (s . cm) & a4 = (s . dp) & a5 = (s . cin) holds (( Following (s,4)) . ( BitFTA2AdderOutputP (am,bp,cm,dp,cin))) = (((((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) '&' ( 'not' a5)) 'or' (( 'not' a5) '&' a4)) 'or' (a4 '&' ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)))) & (( Following (s,4)) . ( BitFTA2AdderOutputQ (am,bp,cm,dp,cin))) = ( 'not' ((((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) 'xor' a4) 'xor' ( 'not' a5))) by Lm29, Lm30;

    theorem :: FTACELL1:30

    for am,bp,cm,dp be non pair set holds for cin be set st cin <> [ <*dp, ( GFA2AdderOutput (am,bp,cm))*>, and2 ] holds for s be State of ( BitFTA2Circ (am,bp,cm,dp,cin)) holds ( Following (s,4)) is stable

    proof

      set n1 = 2, n2 = 2;

      let am,bp,cm,dp be non pair set;

      let cin be set;

      set C = ( BitFTA2Circ (am,bp,cm,dp,cin));

      set S1 = ( BitGFA2Str (am,bp,cm));

      set C1 = ( BitGFA2Circ (am,bp,cm));

      set A1 = ( GFA2AdderOutput (am,bp,cm));

      set S2 = ( BitGFA1Str (A1,cin,dp));

      set C2 = ( BitGFA1Circ (A1,cin,dp));

      set dpA1 = [ <*dp, A1*>, and2 ];

      assume

       A1: cin <> dpA1;

      let s be State of C;

      C1 tolerates C2 by CIRCCOMB: 60;

      then

       A2: the Sorts of C1 tolerates the Sorts of C2 by CIRCCOMB:def 3;

      then

      reconsider s1 = (s | the carrier of S1) as State of C1 by CIRCCOMB: 26;

      reconsider s2 = (( Following (s,n1)) | the carrier of S2) as State of C2 by A2, CIRCCOMB: 26;

      

       A3: ( InputVertices S1) misses ( InnerVertices S2) & ( Following (s1,n1)) is stable by Lm22, GFACIRC1: 104;

      ( Following (s2,n2)) is stable by A1, Lm21, GFACIRC1: 72;

      then ( Following (s,(n1 + n2))) is stable by A3, CIRCCMB2: 19, CIRCCOMB: 60;

      hence thesis;

    end;

    begin

    definition

      let am,bm,cm,dm,cin be set;

      :: FTACELL1:def19

      func BitFTA3Str (am,bm,cm,dm,cin) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( BitGFA3Str (am,bm,cm)) +* ( BitGFA3Str (( GFA3AdderOutput (am,bm,cm)),cin,dm)));

      coherence ;

    end

    definition

      let am,bm,cm,dm,cin be set;

      :: FTACELL1:def20

      func BitFTA3Circ (am,bm,cm,dm,cin) -> strict Boolean gate`2=den Circuit of ( BitFTA3Str (am,bm,cm,dm,cin)) equals (( BitGFA3Circ (am,bm,cm)) +* ( BitGFA3Circ (( GFA3AdderOutput (am,bm,cm)),cin,dm)));

      coherence ;

    end

    theorem :: FTACELL1:31

    

     Th31: for am,bm,cm,dm,cin be set holds ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) = ((( { [ <*am, bm*>, xor2 ], ( GFA3AdderOutput (am,bm,cm))} \/ { [ <*am, bm*>, nor2 ], [ <*bm, cm*>, nor2 ], [ <*cm, am*>, nor2 ], ( GFA3CarryOutput (am,bm,cm))}) \/ { [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, xor2 ], ( GFA3AdderOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm))}) \/ { [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, nor2 ], [ <*cin, dm*>, nor2 ], [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ], ( GFA3CarryOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm))})

    proof

      let am,bm,cm,dm,cin be set;

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      set S1 = ( BitGFA3Str (am,bm,cm));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set C1 = ( GFA3CarryOutput (am,bm,cm));

      set S2 = ( BitGFA3Str (A1,cin,dm));

      set A2 = ( GFA3AdderOutput (A1,cin,dm));

      set C2 = ( GFA3CarryOutput (A1,cin,dm));

      set ambm0 = [ <*am, bm*>, xor2 ];

      set ambm = [ <*am, bm*>, nor2 ];

      set bmcm = [ <*bm, cm*>, nor2 ];

      set cmam = [ <*cm, am*>, nor2 ];

      set A1cin0 = [ <*A1, cin*>, xor2 ];

      set A1cin = [ <*A1, cin*>, nor2 ];

      set cindm = [ <*cin, dm*>, nor2 ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      S1 tolerates S2 by CIRCCOMB: 47;

      

      hence ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by CIRCCOMB: 11

      .= (((( {ambm0} \/ {A1}) \/ {ambm, bmcm, cmam}) \/ {C1}) \/ ( InnerVertices S2)) by GFACIRC1: 127

      .= ((( {ambm0, A1} \/ {ambm, bmcm, cmam}) \/ {C1}) \/ ( InnerVertices S2)) by ENUMSET1: 1

      .= (( {ambm0, A1} \/ ( {ambm, bmcm, cmam} \/ {C1})) \/ ( InnerVertices S2)) by XBOOLE_1: 4

      .= (( {ambm0, A1} \/ {ambm, bmcm, cmam, C1}) \/ ( InnerVertices S2)) by ENUMSET1: 6

      .= (( {ambm0, A1} \/ {ambm, bmcm, cmam, C1}) \/ ((( {A1cin0} \/ {A2}) \/ {A1cin, cindm, dmA1}) \/ {C2})) by GFACIRC1: 127

      .= (( {ambm0, A1} \/ {ambm, bmcm, cmam, C1}) \/ (( {A1cin0, A2} \/ {A1cin, cindm, dmA1}) \/ {C2})) by ENUMSET1: 1

      .= (( {ambm0, A1} \/ {ambm, bmcm, cmam, C1}) \/ ( {A1cin0, A2} \/ ( {A1cin, cindm, dmA1} \/ {C2}))) by XBOOLE_1: 4

      .= (( {ambm0, A1} \/ {ambm, bmcm, cmam, C1}) \/ ( {A1cin0, A2} \/ {A1cin, cindm, dmA1, C2})) by ENUMSET1: 6

      .= ((( {ambm0, A1} \/ {ambm, bmcm, cmam, C1}) \/ {A1cin0, A2}) \/ {A1cin, cindm, dmA1, C2}) by XBOOLE_1: 4;

    end;

    theorem :: FTACELL1:32

    for am,bm,cm,dm,cin be set holds ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) is Relation

    proof

      let am,bm,cm,dm,cin be set;

      set S1 = ( BitGFA3Str (am,bm,cm));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set S2 = ( BitGFA3Str (A1,cin,dm));

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by GFACIRC1: 128;

      hence thesis by FACIRC_1: 3;

    end;

    

     Lm31: for x,y,z be set holds for p be set holds ( GFA3AdderOutput (x,y,z)) <> [p, nor2 ]

    proof

      let x,y,z be set, p be set;

      set A1 = ( GFA3AdderOutput (x,y,z));

      (A1 `2 ) = xor2 ;

      then ( [p, nor2 ] `2 ) <> (A1 `2 ) by TWOSCOMP: 9, TWOSCOMP: 11;

      hence thesis;

    end;

    

     Lm32: for am,bm,cm be non pair set holds for x,y,z be set holds ( InputVertices ( BitGFA3Str (am,bm,cm))) misses ( InnerVertices ( BitGFA3Str (x,y,z)))

    proof

      let am,bm,cm be non pair set;

      let x,y,z be set;

      set S1 = ( BitGFA3Str (am,bm,cm));

      ( InputVertices S1) is without_pairs by GFACIRC1: 131;

      hence thesis by FACIRC_1: 5, GFACIRC1: 128;

    end;

    theorem :: FTACELL1:33

    

     Th33: for am,bm,cm,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm))) holds ( InputVertices ( BitFTA3Str (am,bm,cm,dm,cin))) = {am, bm, cm, dm, cin}

    proof

      let am,bm,cm,dm be non pair set;

      let cin be set;

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      set S1 = ( BitGFA3Str (am,bm,cm));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set C1 = ( GFA3CarryOutput (am,bm,cm));

      set S2 = ( BitGFA3Str (A1,cin,dm));

      set ambm0 = [ <*am, bm*>, xor2 ];

      set ambm = [ <*am, bm*>, nor2 ];

      set bmcm = [ <*bm, cm*>, nor2 ];

      set cmam = [ <*cm, am*>, nor2 ];

      set cindm = [ <*cin, dm*>, nor2 ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      assume that

       A1: cin <> dmA1 and

       A2: not cin in ( InnerVertices S1);

      

       A3: not dm in {A1, ambm0, ambm, bmcm, cmam, C1} by ENUMSET1:def 4;

      A1 in {A1, ambm0, ambm, bmcm, cmam, C1} by ENUMSET1:def 4;

      then

       A4: ( {A1} \ {A1, ambm0, ambm, bmcm, cmam, C1}) = {} by ZFMISC_1: 60;

      

       A5: ( InnerVertices S1) = ((( {ambm0} \/ {A1}) \/ {ambm, bmcm, cmam}) \/ {C1}) by GFACIRC1: 127

      .= (( {ambm0, A1} \/ {ambm, bmcm, cmam}) \/ {C1}) by ENUMSET1: 1

      .= ( {ambm0, A1} \/ ( {ambm, bmcm, cmam} \/ {C1})) by XBOOLE_1: 4

      .= ( {A1, ambm0} \/ {ambm, bmcm, cmam, C1}) by ENUMSET1: 6

      .= {A1, ambm0, ambm, bmcm, cmam, C1} by ENUMSET1: 12;

      

      then

       A6: ( {A1, cin, dm} \ ( InnerVertices S1)) = (( {A1} \/ {cin, dm}) \ {A1, ambm0, ambm, bmcm, cmam, C1}) by ENUMSET1: 2

      .= (( {A1} \ {A1, ambm0, ambm, bmcm, cmam, C1}) \/ ( {cin, dm} \ {A1, ambm0, ambm, bmcm, cmam, C1})) by XBOOLE_1: 42

      .= (( {cin} \/ {dm}) \ {A1, ambm0, ambm, bmcm, cmam, C1}) by A4, ENUMSET1: 1

      .= (( {cin} \ {A1, ambm0, ambm, bmcm, cmam, C1}) \/ ( {dm} \ {A1, ambm0, ambm, bmcm, cmam, C1})) by XBOOLE_1: 42

      .= ( {cin} \/ ( {dm} \ {A1, ambm0, ambm, bmcm, cmam, C1})) by A2, A5, ZFMISC_1: 59

      .= ( {cin} \/ {dm}) by A3, ZFMISC_1: 59

      .= {cin, dm} by ENUMSET1: 1;

      

       A7: A1 <> cindm by Lm31;

      ( InnerVertices S2) misses ( InputVertices S1) & S1 tolerates S2 by Lm32, CIRCCOMB: 47;

      

      hence ( InputVertices S) = (( InputVertices S1) \/ (( InputVertices S2) \ ( InnerVertices S1))) by FACIRC_1: 4

      .= ( {am, bm, cm} \/ (( InputVertices S2) \ ( InnerVertices S1))) by GFACIRC1: 130

      .= ( {am, bm, cm} \/ ( {A1, cin, dm} \ ( InnerVertices S1))) by A1, A7, GFACIRC1: 129

      .= {am, bm, cm, dm, cin} by A6, ENUMSET1: 9;

    end;

    theorem :: FTACELL1:34

    

     Th34: for am,bm,cm,dm,cin be set holds am in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & bm in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & cm in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & dm in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & cin in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & [ <*am, bm*>, xor2 ] in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & ( GFA3AdderOutput (am,bm,cm)) in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & [ <*am, bm*>, nor2 ] in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & [ <*bm, cm*>, nor2 ] in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & [ <*cm, am*>, nor2 ] in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & ( GFA3CarryOutput (am,bm,cm)) in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, xor2 ] in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & ( GFA3AdderOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm)) in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, nor2 ] in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & [ <*cin, dm*>, nor2 ] in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin)) & ( GFA3CarryOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm)) in the carrier of ( BitFTA3Str (am,bm,cm,dm,cin))

    proof

      let am,bm,cm,dm,cin be set;

      set S1 = ( BitGFA3Str (am,bm,cm));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set C1 = ( GFA3CarryOutput (am,bm,cm));

      set S2 = ( BitGFA3Str (A1,cin,dm));

      set A2 = ( GFA3AdderOutput (A1,cin,dm));

      set C2 = ( GFA3CarryOutput (A1,cin,dm));

      set ambm0 = [ <*am, bm*>, xor2 ];

      set ambm = [ <*am, bm*>, nor2 ];

      set bmcm = [ <*bm, cm*>, nor2 ];

      set cmam = [ <*cm, am*>, nor2 ];

      set A1cin0 = [ <*A1, cin*>, xor2 ];

      set A1cin = [ <*A1, cin*>, nor2 ];

      set cindm = [ <*cin, dm*>, nor2 ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      

       A1: cm in the carrier of S1 & ambm0 in the carrier of S1 by GFACIRC1: 132;

      

       A2: ambm in the carrier of S1 & bmcm in the carrier of S1 by GFACIRC1: 132;

      

       A3: A1 in the carrier of S2 & cin in the carrier of S2 by GFACIRC1: 132;

      

       A4: cmam in the carrier of S1 & C1 in the carrier of S1 by GFACIRC1: 132;

      

       A5: C2 in the carrier of S2 by GFACIRC1: 132;

      

       A6: cindm in the carrier of S2 & dmA1 in the carrier of S2 by GFACIRC1: 132;

      

       A7: A2 in the carrier of S2 & A1cin in the carrier of S2 by GFACIRC1: 132;

      

       A8: dm in the carrier of S2 & A1cin0 in the carrier of S2 by GFACIRC1: 132;

      am in the carrier of S1 & bm in the carrier of S1 by GFACIRC1: 132;

      hence thesis by A1, A2, A4, A3, A8, A7, A6, A5, FACIRC_1: 20;

    end;

    theorem :: FTACELL1:35

    

     Th35: for am,bm,cm,dm,cin be set holds [ <*am, bm*>, xor2 ] in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & ( GFA3AdderOutput (am,bm,cm)) in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & [ <*am, bm*>, nor2 ] in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & [ <*bm, cm*>, nor2 ] in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & [ <*cm, am*>, nor2 ] in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & ( GFA3CarryOutput (am,bm,cm)) in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, xor2 ] in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & ( GFA3AdderOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm)) in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, nor2 ] in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & [ <*cin, dm*>, nor2 ] in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & ( GFA3CarryOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm)) in ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin)))

    proof

      let am,bm,cm,dm,cin be set;

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set C1 = ( GFA3CarryOutput (am,bm,cm));

      set A2 = ( GFA3AdderOutput (A1,cin,dm));

      set C2 = ( GFA3CarryOutput (A1,cin,dm));

      set ambm0 = [ <*am, bm*>, xor2 ];

      set ambm = [ <*am, bm*>, nor2 ];

      set bmcm = [ <*bm, cm*>, nor2 ];

      set cmam = [ <*cm, am*>, nor2 ];

      set A1cin0 = [ <*A1, cin*>, xor2 ];

      set A1cin = [ <*A1, cin*>, nor2 ];

      set cindm = [ <*cin, dm*>, nor2 ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      set p1 = {ambm0, A1, ambm, bmcm, cmam, C1};

      set p2 = {A1cin0, A2, A1cin, cindm, dmA1, C2};

      

       A1: ambm0 in p1 & A1 in p1 by ENUMSET1:def 4;

      

       A2: ambm in p1 & bmcm in p1 by ENUMSET1:def 4;

      

       A3: A1cin0 in p2 & A2 in p2 by ENUMSET1:def 4;

      

       A4: cmam in p1 & C1 in p1 by ENUMSET1:def 4;

      

       A5: dmA1 in p2 & C2 in p2 by ENUMSET1:def 4;

      

       A6: A1cin in p2 & cindm in p2 by ENUMSET1:def 4;

      ( InnerVertices S) = ((( {ambm0, A1} \/ {ambm, bmcm, cmam, C1}) \/ {A1cin0, A2}) \/ {A1cin, cindm, dmA1, C2}) by Th31

      .= ((p1 \/ {A1cin0, A2}) \/ {A1cin, cindm, dmA1, C2}) by ENUMSET1: 12

      .= (p1 \/ ( {A1cin0, A2} \/ {A1cin, cindm, dmA1, C2})) by XBOOLE_1: 4

      .= (p1 \/ p2) by ENUMSET1: 12;

      hence thesis by A1, A2, A4, A3, A6, A5, XBOOLE_0:def 3;

    end;

    theorem :: FTACELL1:36

    

     Th36: for am,bm,cm,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm))) holds am in ( InputVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & bm in ( InputVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & cm in ( InputVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & dm in ( InputVertices ( BitFTA3Str (am,bm,cm,dm,cin))) & cin in ( InputVertices ( BitFTA3Str (am,bm,cm,dm,cin)))

    proof

      let am,bm,cm,dm be non pair set;

      let cin be set;

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      set S1 = ( BitGFA3Str (am,bm,cm));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set dmA1 = [ <*dm, A1*>, nor2 ];

      assume cin <> dmA1 & not cin in ( InnerVertices S1);

      then ( InputVertices S) = {am, bm, cm, dm, cin} by Th33;

      hence thesis by ENUMSET1:def 3;

    end;

    definition

      let am,bm,cm,dm,cin be set;

      :: FTACELL1:def21

      func BitFTA3CarryOutput (am,bm,cm,dm,cin) -> Element of ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) equals ( GFA3CarryOutput (am,bm,cm));

      coherence by Th35;

      :: FTACELL1:def22

      func BitFTA3AdderOutputI (am,bm,cm,dm,cin) -> Element of ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) equals ( GFA3AdderOutput (am,bm,cm));

      coherence by Th35;

      :: FTACELL1:def23

      func BitFTA3AdderOutputP (am,bm,cm,dm,cin) -> Element of ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) equals ( GFA3CarryOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm));

      coherence by Th35;

      :: FTACELL1:def24

      func BitFTA3AdderOutputQ (am,bm,cm,dm,cin) -> Element of ( InnerVertices ( BitFTA3Str (am,bm,cm,dm,cin))) equals ( GFA3AdderOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm));

      coherence by Th35;

    end

    theorem :: FTACELL1:37

    for am,bm,cm be non pair set holds for dm,cin be set holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bm) & a3 = (s . cm) holds (( Following (s,2)) . ( BitFTA3CarryOutput (am,bm,cm,dm,cin))) = ( 'not' (((( 'not' a1) '&' ( 'not' a2)) 'or' (( 'not' a2) '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1)))) & (( Following (s,2)) . ( BitFTA3AdderOutputI (am,bm,cm,dm,cin))) = ( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)))

    proof

      let am,bm,cm be non pair set;

      let dm,cin be set;

      let s be State of ( BitFTA3Circ (am,bm,cm,dm,cin));

      set S1 = ( BitGFA3Str (am,bm,cm));

      set C1 = ( BitGFA3Circ (am,bm,cm));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set A2 = ( GFA3CarryOutput (am,bm,cm));

      set S2 = ( BitGFA3Str (A1,cin,dm));

      set C2 = ( BitGFA3Circ (A1,cin,dm));

      let a1,a2,a3 be Element of BOOLEAN such that

       A1: a1 = (s . am) and

       A2: a2 = (s . bm) and

       A3: a3 = (s . cm);

      reconsider s1 = (s | the carrier of S1) as State of C1 by FACIRC_1: 26;

      

       A4: ( dom s1) = the carrier of S1 by CIRCUIT1: 3;

      am in the carrier of S1 by GFACIRC1: 132;

      then

       A5: a1 = (s1 . am) by A1, A4, FUNCT_1: 47;

      reconsider t = s as State of (C1 +* C2);

      

       A6: ( InputVertices S1) misses ( InnerVertices S2) by Lm32;

      cm in the carrier of S1 by GFACIRC1: 132;

      then

       A7: a3 = (s1 . cm) by A3, A4, FUNCT_1: 47;

      bm in the carrier of S1 by GFACIRC1: 132;

      then

       A8: a2 = (s1 . bm) by A2, A4, FUNCT_1: 47;

      A2 in the carrier of S1 by GFACIRC1: 132;

      then (( Following (t,2)) . ( GFA3CarryOutput (am,bm,cm))) = (( Following (s1,2)) . ( GFA3CarryOutput (am,bm,cm))) by A6, FACIRC_1: 32;

      hence (( Following (s,2)) . ( BitFTA3CarryOutput (am,bm,cm,dm,cin))) = ( 'not' (((( 'not' a1) '&' ( 'not' a2)) 'or' (( 'not' a2) '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1)))) by A5, A8, A7, GFACIRC1: 135;

      A1 in the carrier of S1 by GFACIRC1: 132;

      then (( Following (t,2)) . ( GFA3AdderOutput (am,bm,cm))) = (( Following (s1,2)) . ( GFA3AdderOutput (am,bm,cm))) by A6, FACIRC_1: 32;

      hence thesis by A5, A8, A7, GFACIRC1: 135;

    end;

    theorem :: FTACELL1:38

    

     Th38: for am,bm,cm,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm))) holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bm) & a3 = (s . cm) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,2)) . ( GFA3AdderOutput (am,bm,cm))) = ( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) & (( Following (s,2)) . am) = a1 & (( Following (s,2)) . bm) = a2 & (( Following (s,2)) . cm) = a3 & (( Following (s,2)) . dm) = a4 & (( Following (s,2)) . cin) = a5

    proof

      let am,bm,cm,dm be non pair set;

      let cin be set such that

       A1: cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm)));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set C1 = ( BitGFA3Circ (am,bm,cm));

      set S1 = ( BitGFA3Str (am,bm,cm));

      set S2 = ( BitGFA3Str (A1,cin,dm));

      set C2 = ( BitGFA3Circ (A1,cin,dm));

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      let s be State of ( BitFTA3Circ (am,bm,cm,dm,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A2: a1 = (s . am) and

       A3: a2 = (s . bm) and

       A4: a3 = (s . cm) and

       A5: a4 = (s . dm) and

       A6: a5 = (s . cin);

      reconsider s1 = (s | the carrier of S1) as State of C1 by FACIRC_1: 26;

      

       A7: ( dom s1) = the carrier of S1 by CIRCUIT1: 3;

      

       A8: dm in ( InputVertices S) by A1, Th36;

      then

       A9: (( Following s) . dm) = a4 by A5, CIRCUIT2:def 5;

      

       A10: cm in ( InputVertices S) by A1, Th36;

      then

       A11: (( Following s) . cm) = a3 by A4, CIRCUIT2:def 5;

      bm in the carrier of S1 by GFACIRC1: 132;

      then

       A12: a2 = (s1 . bm) by A3, A7, FUNCT_1: 47;

      reconsider t = s as State of (C1 +* C2);

      A1 in the carrier of S1 & ( InputVertices S1) misses ( InnerVertices S2) by Lm32, GFACIRC1: 132;

      then

       A13: (( Following (t,2)) . ( GFA3AdderOutput (am,bm,cm))) = (( Following (s1,2)) . ( GFA3AdderOutput (am,bm,cm))) by FACIRC_1: 32;

      cm in the carrier of S1 by GFACIRC1: 132;

      then

       A14: a3 = (s1 . cm) by A4, A7, FUNCT_1: 47;

      am in the carrier of S1 by GFACIRC1: 132;

      then a1 = (s1 . am) by A2, A7, FUNCT_1: 47;

      hence (( Following (s,2)) . ( GFA3AdderOutput (am,bm,cm))) = ( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) by A12, A14, A13, GFACIRC1: 135;

      

       A15: bm in ( InputVertices S) by A1, Th36;

      then

       A16: (( Following s) . bm) = a2 by A3, CIRCUIT2:def 5;

      

       A17: cin in ( InputVertices S) by A1, Th36;

      then

       A18: (( Following s) . cin) = a5 by A6, CIRCUIT2:def 5;

      

       A19: am in ( InputVertices S) by A1, Th36;

      then ( Following (s,2)) = ( Following ( Following s)) & (( Following s) . am) = a1 by A2, CIRCUIT2:def 5, FACIRC_1: 15;

      hence thesis by A19, A15, A10, A8, A17, A16, A11, A9, A18, CIRCUIT2:def 5;

    end;

    

     Lm33: for am,bm,cm,dm be non pair set holds for cin be set holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds for a123,a4,a5 be Element of BOOLEAN st a123 = (s . ( GFA3AdderOutput (am,bm,cm))) & a4 = (s . dm) & a5 = (s . cin) holds (( Following s) . [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, nor2 ]) = (( 'not' a123) '&' ( 'not' a5)) & (( Following s) . [ <*cin, dm*>, nor2 ]) = (( 'not' a5) '&' ( 'not' a4)) & (( Following s) . [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ]) = (( 'not' a4) '&' ( 'not' a123))

    proof

      let am,bm,cm,dm be non pair set;

      let cin be set;

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      set C = ( BitFTA3Circ (am,bm,cm,dm,cin));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set A1cin = [ <*A1, cin*>, nor2 ];

      set cindm = [ <*cin, dm*>, nor2 ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      let s be State of C;

      let a123,a4,a5 be Element of BOOLEAN such that

       A1: a123 = (s . A1) and

       A2: a4 = (s . dm) and

       A3: a5 = (s . cin);

      

       A4: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A5: cin in the carrier of S by Th34;

      

       A6: A1 in the carrier of S by Th34;

      

       A7: ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A1cin in the carrier' of S by Th35;

      

      hence (( Following s) . A1cin) = ( nor2 . (s * <*A1, cin*>)) by FACIRC_1: 35

      .= ( nor2 . <*a123, a5*>) by A1, A3, A6, A5, A4, FINSEQ_2: 125

      .= (( 'not' a123) '&' ( 'not' a5)) by TWOSCOMP: 54;

      

       A8: dm in the carrier of S by Th34;

      cindm in the carrier' of S by A7, Th35;

      

      hence (( Following s) . cindm) = ( nor2 . (s * <*cin, dm*>)) by FACIRC_1: 35

      .= ( nor2 . <*a5, a4*>) by A2, A3, A8, A5, A4, FINSEQ_2: 125

      .= (( 'not' a5) '&' ( 'not' a4)) by TWOSCOMP: 54;

      dmA1 in the carrier' of S by A7, Th35;

      

      hence (( Following s) . dmA1) = ( nor2 . (s * <*dm, A1*>)) by FACIRC_1: 35

      .= ( nor2 . <*a4, a123*>) by A1, A2, A6, A8, A4, FINSEQ_2: 125

      .= (( 'not' a4) '&' ( 'not' a123)) by TWOSCOMP: 54;

    end;

    

     Lm34: for am,bm,cm,dm be non pair set holds for cin be set holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds for a123,a5 be Element of BOOLEAN st a123 = (s . ( GFA3AdderOutput (am,bm,cm))) & a5 = (s . cin) holds (( Following s) . [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, xor2 ]) = (a123 'xor' a5)

    proof

      let am,bm,cm,dm be non pair set;

      let cin be set;

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      set C = ( BitFTA3Circ (am,bm,cm,dm,cin));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set A1cin = [ <*A1, cin*>, xor2 ];

      let s be State of C;

      let a123,a5 be Element of BOOLEAN such that

       A1: a123 = (s . A1) & a5 = (s . cin);

      

       A2: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A3: A1 in the carrier of S & cin in the carrier of S by Th34;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A1cin in the carrier' of S by Th35;

      

      hence (( Following s) . A1cin) = ( xor2 . (s * <*A1, cin*>)) by FACIRC_1: 35

      .= ( xor2 . <*a123, a5*>) by A1, A3, A2, FINSEQ_2: 125

      .= (a123 'xor' a5) by FACIRC_1:def 4;

    end;

    

     Lm35: for am,bm,cm,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm))) holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bm) & a3 = (s . cm) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,3)) . [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, nor2 ]) = (((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) '&' ( 'not' a5)) & (( Following (s,3)) . [ <*cin, dm*>, nor2 ]) = (( 'not' a5) '&' ( 'not' a4)) & (( Following (s,3)) . [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ]) = (( 'not' a4) '&' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) & (( Following (s,3)) . am) = a1 & (( Following (s,3)) . bm) = a2 & (( Following (s,3)) . cm) = a3 & (( Following (s,3)) . dm) = a4 & (( Following (s,3)) . cin) = a5

    proof

      let am,bm,cm,dm be non pair set;

      let cin be set such that

       A1: cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm)));

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      

       A2: am in ( InputVertices S) & bm in ( InputVertices S) by A1, Th36;

      

       A3: cm in ( InputVertices S) & dm in ( InputVertices S) by A1, Th36;

      let s be State of ( BitFTA3Circ (am,bm,cm,dm,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . am) & a2 = (s . bm) & a3 = (s . cm) & a4 = (s . dm) & a5 = (s . cin);

      

       A5: (( Following (s,2)) . cin) = a5 by A1, A4, Th38;

      set cindm = [ <*cin, dm*>, nor2 ];

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set A1cin = [ <*A1, cin*>, nor2 ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      

       A6: ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) by FACIRC_1: 12;

      (( Following (s,2)) . A1) = ( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) & (( Following (s,2)) . dm) = a4 by A1, A4, Th38;

      hence (( Following (s,3)) . A1cin) = (((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) '&' ( 'not' a5)) & (( Following (s,3)) . cindm) = (( 'not' a5) '&' ( 'not' a4)) & (( Following (s,3)) . dmA1) = (( 'not' a4) '&' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) by A6, A5, Lm33;

      

       A7: (( Following (s,2)) . cm) = a3 & (( Following (s,2)) . dm) = a4 by A1, A4, Th38;

      

       A8: (( Following (s,2)) . cin) = a5 by A1, A4, Th38;

      

       A9: cin in ( InputVertices S) by A1, Th36;

      (( Following (s,2)) . am) = a1 & (( Following (s,2)) . bm) = a2 by A1, A4, Th38;

      hence thesis by A6, A2, A3, A9, A7, A8, CIRCUIT2:def 5;

    end;

    

     Lm36: for am,bm,cm,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm))) holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bm) & a3 = (s . cm) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,3)) . [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, xor2 ]) = (( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) 'xor' a5) & (( Following (s,3)) . am) = a1 & (( Following (s,3)) . bm) = a2 & (( Following (s,3)) . cm) = a3 & (( Following (s,3)) . dm) = a4 & (( Following (s,3)) . cin) = a5

    proof

      let am,bm,cm,dm be non pair set;

      let cin be set such that

       A1: cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm)));

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      

       A2: am in ( InputVertices S) & bm in ( InputVertices S) by A1, Th36;

      

       A3: cm in ( InputVertices S) & dm in ( InputVertices S) by A1, Th36;

      let s be State of ( BitFTA3Circ (am,bm,cm,dm,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . am) & a2 = (s . bm) & a3 = (s . cm) & a4 = (s . dm) & a5 = (s . cin);

      

       A5: (( Following (s,2)) . cm) = a3 & (( Following (s,2)) . dm) = a4 by A1, A4, Th38;

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set A1cin = [ <*A1, cin*>, xor2 ];

      

       A6: ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) by FACIRC_1: 12;

      (( Following (s,2)) . A1) = ( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) & (( Following (s,2)) . cin) = a5 by A1, A4, Th38;

      hence (( Following (s,3)) . A1cin) = (( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) 'xor' a5) by A6, Lm34;

      

       A7: (( Following (s,2)) . cin) = a5 by A1, A4, Th38;

      

       A8: cin in ( InputVertices S) by A1, Th36;

      (( Following (s,2)) . am) = a1 & (( Following (s,2)) . bm) = a2 by A1, A4, Th38;

      hence thesis by A6, A2, A3, A8, A5, A7, CIRCUIT2:def 5;

    end;

    

     Lm37: for am,bm,cm,dm be non pair set holds for cin be set holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds for a123x,a123y,a123z be Element of BOOLEAN st a123x = (s . [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, nor2 ]) & a123y = (s . [ <*cin, dm*>, nor2 ]) & a123z = (s . [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ]) holds (( Following s) . ( GFA3CarryOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm))) = ( 'not' ((a123x 'or' a123y) 'or' a123z))

    proof

      let am,bm,cm,dm be non pair set;

      let cin be set;

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      set C = ( BitFTA3Circ (am,bm,cm,dm,cin));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set A2 = ( GFA3CarryOutput (A1,cin,dm));

      set A1cin = [ <*A1, cin*>, nor2 ];

      set cindm = [ <*cin, dm*>, nor2 ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      let s be State of C;

      let a123x,a123y,a123z be Element of BOOLEAN such that

       A1: a123x = (s . A1cin) & a123y = (s . cindm) & a123z = (s . dmA1);

      

       A2: A1cin in the carrier of S & cindm in the carrier of S by Th34;

      

       A3: dmA1 in the carrier of S & ( dom s) = the carrier of S by Th34, CIRCUIT1: 3;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A2 in the carrier' of S by Th35;

      

      hence (( Following s) . A2) = ( nor3 . (s * <*A1cin, cindm, dmA1*>)) by FACIRC_1: 35

      .= ( nor3 . <*a123x, a123y, a123z*>) by A1, A2, A3, FINSEQ_2: 126

      .= ( 'not' ((a123x 'or' a123y) 'or' a123z)) by TWOSCOMP:def 28;

    end;

    

     Lm38: for am,bm,cm,dm be non pair set holds for cin be set holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds for a1235,a4 be Element of BOOLEAN st a1235 = (s . [ <*( GFA3AdderOutput (am,bm,cm)), cin*>, xor2 ]) & a4 = (s . dm) holds (( Following s) . ( GFA3AdderOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm))) = (a1235 'xor' a4)

    proof

      let am,bm,cm,dm be non pair set;

      let cin be set;

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      set C = ( BitFTA3Circ (am,bm,cm,dm,cin));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set A2 = ( GFA3AdderOutput (A1,cin,dm));

      set A1cin = [ <*A1, cin*>, xor2 ];

      let s be State of C;

      let a1235,a4 be Element of BOOLEAN such that

       A1: a1235 = (s . A1cin) & a4 = (s . dm);

      

       A2: ( dom s) = the carrier of S by CIRCUIT1: 3;

      

       A3: A1cin in the carrier of S & dm in the carrier of S by Th34;

      ( InnerVertices S) = the carrier' of S by FACIRC_1: 37;

      then A2 in the carrier' of S by Th35;

      

      hence (( Following s) . A2) = ( xor2 . (s * <*A1cin, dm*>)) by FACIRC_1: 35

      .= ( xor2 . <*a1235, a4*>) by A1, A3, A2, FINSEQ_2: 125

      .= (a1235 'xor' a4) by FACIRC_1:def 4;

    end;

    

     Lm39: for am,bm,cm,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm))) holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bm) & a3 = (s . cm) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,4)) . ( GFA3CarryOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm))) = ( 'not' (((((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) '&' ( 'not' a5)) 'or' (( 'not' a5) '&' ( 'not' a4))) 'or' (( 'not' a4) '&' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))))) & (( Following (s,4)) . am) = a1 & (( Following (s,4)) . bm) = a2 & (( Following (s,4)) . cm) = a3 & (( Following (s,4)) . dm) = a4 & (( Following (s,4)) . cin) = a5

    proof

      let am,bm,cm,dm be non pair set;

      let cin be set such that

       A1: cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm)));

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      

       A2: am in ( InputVertices S) & bm in ( InputVertices S) by A1, Th36;

      

       A3: cm in ( InputVertices S) & dm in ( InputVertices S) by A1, Th36;

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      let s be State of ( BitFTA3Circ (am,bm,cm,dm,cin));

      set dmA1 = [ <*dm, A1*>, nor2 ];

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . am) & a2 = (s . bm) & a3 = (s . cm) & a4 = (s . dm) & a5 = (s . cin);

      

       A5: (( Following (s,3)) . dmA1) = (( 'not' a4) '&' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) by A1, A4, Lm35;

      set cindm = [ <*cin, dm*>, nor2 ];

      set A1cin = [ <*A1, cin*>, nor2 ];

      set A2 = ( GFA3CarryOutput (A1,cin,dm));

      

       A6: ( Following (s,(3 + 1))) = ( Following ( Following (s,3))) by FACIRC_1: 12;

      (( Following (s,3)) . A1cin) = (((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) '&' ( 'not' a5)) & (( Following (s,3)) . cindm) = (( 'not' a5) '&' ( 'not' a4)) by A1, A4, Lm35;

      hence (( Following (s,4)) . A2) = ( 'not' (((((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) '&' ( 'not' a5)) 'or' (( 'not' a5) '&' ( 'not' a4))) 'or' (( 'not' a4) '&' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))))) by A6, A5, Lm37;

      

       A7: (( Following (s,3)) . cm) = a3 & (( Following (s,3)) . dm) = a4 by A1, A4, Lm35;

      

       A8: (( Following (s,3)) . cin) = a5 by A1, A4, Lm35;

      

       A9: cin in ( InputVertices S) by A1, Th36;

      (( Following (s,3)) . am) = a1 & (( Following (s,3)) . bm) = a2 by A1, A4, Lm35;

      hence thesis by A6, A2, A3, A9, A7, A8, CIRCUIT2:def 5;

    end;

    

     Lm40: for am,bm,cm,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm))) holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bm) & a3 = (s . cm) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,4)) . ( GFA3AdderOutput (( GFA3AdderOutput (am,bm,cm)),cin,dm))) = ( 'not' ((((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) 'xor' ( 'not' a4)) 'xor' ( 'not' a5))) & (( Following (s,4)) . am) = a1 & (( Following (s,4)) . bm) = a2 & (( Following (s,4)) . cm) = a3 & (( Following (s,4)) . dm) = a4 & (( Following (s,4)) . cin) = a5

    proof

      let am,bm,cm,dm be non pair set;

      let cin be set such that

       A1: cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm)));

      set S = ( BitFTA3Str (am,bm,cm,dm,cin));

      

       A2: am in ( InputVertices S) & bm in ( InputVertices S) by A1, Th36;

      

       A3: cm in ( InputVertices S) & dm in ( InputVertices S) by A1, Th36;

      let s be State of ( BitFTA3Circ (am,bm,cm,dm,cin));

      let a1,a2,a3,a4,a5 be Element of BOOLEAN such that

       A4: a1 = (s . am) & a2 = (s . bm) & a3 = (s . cm) & a4 = (s . dm) & a5 = (s . cin);

      

       A5: (( Following (s,3)) . cm) = a3 & (( Following (s,3)) . dm) = a4 by A1, A4, Lm36;

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set A2 = ( GFA3AdderOutput (A1,cin,dm));

      set A1cin = [ <*A1, cin*>, xor2 ];

      

       A6: ( Following (s,(3 + 1))) = ( Following ( Following (s,3))) by FACIRC_1: 12;

      (( Following (s,3)) . A1cin) = (( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) 'xor' a5) & (( Following (s,3)) . dm) = a4 by A1, A4, Lm36;

      

      hence (( Following (s,4)) . A2) = ((( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) 'xor' a5) 'xor' a4) by A6, Lm38

      .= ( 'not' ((((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) 'xor' ( 'not' a5)) 'xor' ( 'not' a4))) by XBOOLEAN: 74

      .= ( 'not' ((((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) 'xor' ( 'not' a4)) 'xor' ( 'not' a5))) by XBOOLEAN: 73;

      

       A7: (( Following (s,3)) . cin) = a5 by A1, A4, Lm36;

      

       A8: cin in ( InputVertices S) by A1, Th36;

      (( Following (s,3)) . am) = a1 & (( Following (s,3)) . bm) = a2 by A1, A4, Lm36;

      hence thesis by A6, A2, A3, A8, A5, A7, CIRCUIT2:def 5;

    end;

    theorem :: FTACELL1:39

    for am,bm,cm,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] & not cin in ( InnerVertices ( BitGFA3Str (am,bm,cm))) holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds for a1,a2,a3,a4,a5 be Element of BOOLEAN st a1 = (s . am) & a2 = (s . bm) & a3 = (s . cm) & a4 = (s . dm) & a5 = (s . cin) holds (( Following (s,4)) . ( BitFTA3AdderOutputP (am,bm,cm,dm,cin))) = ( 'not' (((((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) '&' ( 'not' a5)) 'or' (( 'not' a5) '&' ( 'not' a4))) 'or' (( 'not' a4) '&' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))))) & (( Following (s,4)) . ( BitFTA3AdderOutputQ (am,bm,cm,dm,cin))) = ( 'not' ((((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) 'xor' ( 'not' a4)) 'xor' ( 'not' a5))) by Lm39, Lm40;

    theorem :: FTACELL1:40

    for am,bm,cm,dm be non pair set holds for cin be set st cin <> [ <*dm, ( GFA3AdderOutput (am,bm,cm))*>, nor2 ] holds for s be State of ( BitFTA3Circ (am,bm,cm,dm,cin)) holds ( Following (s,4)) is stable

    proof

      set n1 = 2, n2 = 2;

      let am,bm,cm,dm be non pair set;

      let cin be set;

      set C = ( BitFTA3Circ (am,bm,cm,dm,cin));

      set S1 = ( BitGFA3Str (am,bm,cm));

      set C1 = ( BitGFA3Circ (am,bm,cm));

      set A1 = ( GFA3AdderOutput (am,bm,cm));

      set S2 = ( BitGFA3Str (A1,cin,dm));

      set C2 = ( BitGFA3Circ (A1,cin,dm));

      set cindm = [ <*cin, dm*>, nor2 ];

      set dmA1 = [ <*dm, A1*>, nor2 ];

      assume

       A1: cin <> dmA1;

      let s be State of C;

      C1 tolerates C2 by CIRCCOMB: 60;

      then

       A2: the Sorts of C1 tolerates the Sorts of C2 by CIRCCOMB:def 3;

      then

      reconsider s1 = (s | the carrier of S1) as State of C1 by CIRCCOMB: 26;

      reconsider s2 = (( Following (s,n1)) | the carrier of S2) as State of C2 by A2, CIRCCOMB: 26;

      

       A3: ( InputVertices S1) misses ( InnerVertices S2) & ( Following (s1,n1)) is stable by Lm32, GFACIRC1: 136;

      A1 <> cindm by Lm31;

      then ( Following (s2,n2)) is stable by A1, GFACIRC1: 136;

      then ( Following (s,(n1 + n2))) is stable by A3, CIRCCMB2: 19, CIRCCOMB: 60;

      hence thesis;

    end;