gfacirc1.miz



    begin

    scheme :: GFACIRC1:sch1

    1AryBooleEx { F( set) -> Element of BOOLEAN } :

ex f be Function of (1 -tuples_on BOOLEAN ), BOOLEAN st for x be Element of BOOLEAN holds (f . <*x*>) = F(x);

      deffunc G( Tuple of 1, BOOLEAN ) = F(.);

      consider f be Function of (1 -tuples_on BOOLEAN ), BOOLEAN such that

       A1: for a be Element of (1 -tuples_on BOOLEAN ) holds (f . a) = G(a) from FUNCT_2:sch 4;

      hereby

        take f;

        let x be Element of BOOLEAN ;

        reconsider a = <*x*> as Element of (1 -tuples_on BOOLEAN ) by FINSEQ_2: 98;

        

        thus (f . <*x*>) = F(.) by A1

        .= F(x) by FINSEQ_1:def 8;

      end;

    end;

    scheme :: GFACIRC1:sch2

    1AryBooleUniq { F( set) -> Element of BOOLEAN } :

for f1,f2 be Function of (1 -tuples_on BOOLEAN ), BOOLEAN st (for x be Element of BOOLEAN holds (f1 . <*x*>) = F(x)) & (for x be Element of BOOLEAN holds (f2 . <*x*>) = F(x)) holds f1 = f2;

      let f1,f2 be Function of (1 -tuples_on BOOLEAN ), BOOLEAN such that

       A1: for x be Element of BOOLEAN holds (f1 . <*x*>) = F(x) and

       A2: for x be Element of BOOLEAN holds (f2 . <*x*>) = F(x);

      now

        let a be Tuple of 1, BOOLEAN ;

        consider x be Element of BOOLEAN such that

         A3: a = <*x*> by FINSEQ_2: 97;

        

        thus (f1 . a) = F(x) by A1, A3

        .= (f2 . a) by A2, A3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: GFACIRC1:sch3

    1AryBooleDef { F( set) -> Element of BOOLEAN } :

(ex f be Function of (1 -tuples_on BOOLEAN ), BOOLEAN st for x be Element of BOOLEAN holds (f . <*x*>) = F(x)) & for f1,f2 be Function of (1 -tuples_on BOOLEAN ), BOOLEAN st (for x be Element of BOOLEAN holds (f1 . <*x*>) = F(x)) & (for x be Element of BOOLEAN holds (f2 . <*x*>) = F(x)) holds f1 = f2;

      deffunc G( Tuple of 1, BOOLEAN ) = F(.);

      consider f be Function of (1 -tuples_on BOOLEAN ), BOOLEAN such that

       A1: for a be Tuple of 1, BOOLEAN holds (f . a) = G(a) from FUNCT_2:sch 4;

      hereby

        take f;

        let x be Element of BOOLEAN ;

        reconsider a = <*x*> as Element of (1 -tuples_on BOOLEAN ) by FINSEQ_2: 98;

        

        thus (f . <*x*>) = F(.) by A1

        .= F(x) by FINSEQ_1:def 8;

      end;

      let f1,f2 be Function of (1 -tuples_on BOOLEAN ), BOOLEAN such that

       A2: for x be Element of BOOLEAN holds (f1 . <*x*>) = F(x) and

       A3: for x be Element of BOOLEAN holds (f2 . <*x*>) = F(x);

      now

        let a be Tuple of 1, BOOLEAN ;

        consider x be Element of BOOLEAN such that

         A4: a = <*x*> by FINSEQ_2: 97;

        

        thus (f1 . a) = F(x) by A2, A4

        .= (f2 . a) by A3, A4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      :: GFACIRC1:def1

      func inv1 -> Function of (1 -tuples_on BOOLEAN ), BOOLEAN means

      : Def1: for x be Element of BOOLEAN holds (it . <*x*>) = ( 'not' x);

      existence

      proof

        deffunc U( Element of BOOLEAN ) = ( 'not' $1);

        thus ex t be Function of (1 -tuples_on BOOLEAN ), BOOLEAN st for x be Element of BOOLEAN holds (t . <*x*>) = U(x) from 1AryBooleEx;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN ) = ( 'not' $1);

        thus for t1,t2 be Function of (1 -tuples_on BOOLEAN ), BOOLEAN st (for x be Element of BOOLEAN holds (t1 . <*x*>) = U(x)) & (for x be Element of BOOLEAN holds (t2 . <*x*>) = U(x)) holds t1 = t2 from 1AryBooleUniq;

      end;

    end

    theorem :: GFACIRC1:1

    

     Th1: for x be Element of BOOLEAN holds ( inv1 . <*x*>) = ( 'not' x) & ( inv1 . <*x*>) = ( nand2 . <*x, x*>) & ( inv1 . <* 0 *>) = 1 & ( inv1 . <*1*>) = 0

    proof

      let x be Element of BOOLEAN ;

      thus ( inv1 . <*x*>) = ( 'not' x) by Def1;

      

      thus ( inv1 . <*x*>) = ( 'not' (x '&' x)) by Def1

      .= ( nand2 . <*x, x*>) by TWOSCOMP:def 4;

      

      thus ( inv1 . <* 0 *>) = ( 'not' FALSE ) by Def1

      .= 1;

      

      thus ( inv1 . <*1*>) = ( 'not' TRUE ) by Def1

      .= 0 ;

    end;

    definition

      :: GFACIRC1:def2

      func buf1 -> Function of (1 -tuples_on BOOLEAN ), BOOLEAN means

      : Def2: for x be Element of BOOLEAN holds (it . <*x*>) = x;

      existence

      proof

        deffunc U( Element of BOOLEAN ) = $1;

        thus ex t be Function of (1 -tuples_on BOOLEAN ), BOOLEAN st for x be Element of BOOLEAN holds (t . <*x*>) = U(x) from 1AryBooleEx;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN ) = $1;

        thus for t1,t2 be Function of (1 -tuples_on BOOLEAN ), BOOLEAN st (for x be Element of BOOLEAN holds (t1 . <*x*>) = U(x)) & (for x be Element of BOOLEAN holds (t2 . <*x*>) = U(x)) holds t1 = t2 from 1AryBooleUniq;

      end;

    end

    theorem :: GFACIRC1:2

    for x be Element of BOOLEAN holds ( buf1 . <*x*>) = x & ( buf1 . <*x*>) = ( and2 . <*x, x*>) & ( buf1 . <* 0 *>) = 0 & ( buf1 . <*1*>) = 1

    proof

      let x be Element of BOOLEAN ;

      thus ( buf1 . <*x*>) = x by Def2;

      

      thus ( buf1 . <*x*>) = (x '&' x) by Def2

      .= ( and2 . <*x, x*>) by FACIRC_1:def 6;

      

      thus ( buf1 . <* 0 *>) = FALSE by Def2

      .= 0 ;

      

      thus ( buf1 . <*1*>) = TRUE by Def2

      .= 1;

    end;

    definition

      :: GFACIRC1:def3

      func and2c -> Function of (2 -tuples_on BOOLEAN ), BOOLEAN means

      : Def3: for x,y be Element of BOOLEAN holds (it . <*x, y*>) = (x '&' ( 'not' y));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ($1 '&' ( 'not' $2));

        thus ex t be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st for x,y be Element of BOOLEAN holds (t . <*x, y*>) = U(x,y) from FACIRC_1:sch 1;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ($1 '&' ( 'not' $2));

        thus for t1,t2 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st (for x,y be Element of BOOLEAN holds (t1 . <*x, y*>) = U(x,y)) & (for x,y be Element of BOOLEAN holds (t2 . <*x, y*>) = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;

      end;

    end

    theorem :: GFACIRC1:3

    for x,y be Element of BOOLEAN holds ( and2c . <*x, y*>) = (x '&' ( 'not' y)) & ( and2c . <*x, y*>) = ( and2a . <*y, x*>) & ( and2c . <*x, y*>) = ( nor2a . <*x, y*>) & ( and2c . <* 0 , 0 *>) = 0 & ( and2c . <* 0 , 1*>) = 0 & ( and2c . <*1, 0 *>) = 1 & ( and2c . <*1, 1*>) = 0

    proof

      let x,y be Element of BOOLEAN ;

      thus ( and2c . <*x, y*>) = (x '&' ( 'not' y)) by Def3;

      

      thus ( and2c . <*x, y*>) = (x '&' ( 'not' y)) by Def3

      .= ( and2a . <*y, x*>) by TWOSCOMP:def 2;

      

      thus ( and2c . <*x, y*>) = ( 'not' (( 'not' x) 'or' ( 'not' ( 'not' y)))) by Def3

      .= ( nor2a . <*x, y*>) by TWOSCOMP:def 11;

      

      thus ( and2c . <* 0 , 0 *>) = ( FALSE '&' ( 'not' FALSE )) by Def3

      .= 0 ;

      

      thus ( and2c . <* 0 , 1*>) = ( FALSE '&' ( 'not' TRUE )) by Def3

      .= 0 ;

      

      thus ( and2c . <*1, 0 *>) = ( TRUE '&' ( 'not' FALSE )) by Def3

      .= 1;

      

      thus ( and2c . <*1, 1*>) = ( TRUE '&' ( 'not' TRUE )) by Def3

      .= 0 ;

    end;

    definition

      :: GFACIRC1:def4

      func xor2c -> Function of (2 -tuples_on BOOLEAN ), BOOLEAN means

      : Def4: for x,y be Element of BOOLEAN holds (it . <*x, y*>) = (x 'xor' ( 'not' y));

      existence

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ($1 'xor' ( 'not' $2));

        thus ex t be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st for x,y be Element of BOOLEAN holds (t . <*x, y*>) = U(x,y) from FACIRC_1:sch 1;

      end;

      uniqueness

      proof

        deffunc U( Element of BOOLEAN , Element of BOOLEAN ) = ($1 'xor' ( 'not' $2));

        thus for t1,t2 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN st (for x,y be Element of BOOLEAN holds (t1 . <*x, y*>) = U(x,y)) & (for x,y be Element of BOOLEAN holds (t2 . <*x, y*>) = U(x,y)) holds t1 = t2 from FACIRC_1:sch 2;

      end;

    end

    theorem :: GFACIRC1:4

    

     Th4: for x,y be Element of BOOLEAN holds ( xor2c . <*x, y*>) = (x 'xor' ( 'not' y)) & ( xor2c . <*x, y*>) = ( xor2a . <*x, y*>) & ( xor2c . <*x, y*>) = ( or2 . <*( nor2 . <*x, y*>), ( and2 . <*x, y*>)*>) & ( xor2c . <* 0 , 0 *>) = 1 & ( xor2c . <* 0 , 1*>) = 0 & ( xor2c . <*1, 0 *>) = 0 & ( xor2c . <*1, 1*>) = 1

    proof

      let x,y be Element of BOOLEAN ;

      thus ( xor2c . <*x, y*>) = (x 'xor' ( 'not' y)) by Def4;

      

      thus ( xor2c . <*x, y*>) = (x 'xor' ( 'not' y)) by Def4

      .= (( 'not' x) 'xor' y)

      .= ( xor2a . <*x, y*>) by TWOSCOMP:def 14;

      

      thus ( xor2c . <*x, y*>) = (x 'xor' ( 'not' y)) by Def4

      .= ((( 'not' x) '&' ( 'not' y)) 'or' (x '&' ( 'not' ( 'not' y))))

      .= ( or2 . <*(( 'not' x) '&' ( 'not' y)), (x '&' y)*>) by FACIRC_1:def 5

      .= ( or2 . <*( nor2 . <*x, y*>), (x '&' y)*>) by TWOSCOMP: 54

      .= ( or2 . <*( nor2 . <*x, y*>), ( and2 . <*x, y*>)*>) by FACIRC_1:def 6;

      

      thus ( xor2c . <* 0 , 0 *>) = ( FALSE 'xor' ( 'not' FALSE )) by Def4

      .= 1 by XBOOLEAN: 102;

      

      thus ( xor2c . <* 0 , 1*>) = ( FALSE 'xor' ( 'not' TRUE )) by Def4

      .= 0 ;

      

      thus ( xor2c . <*1, 0 *>) = ( TRUE 'xor' ( 'not' FALSE )) by Def4

      .= 0 ;

      

      thus ( xor2c . <*1, 1*>) = ( TRUE 'xor' ( 'not' TRUE )) by Def4

      .= 1 by BINARITH: 7;

    end;

    theorem :: GFACIRC1:5

    for x,y be Element of BOOLEAN holds ( inv1 . <*( xor2 . <*x, y*>)*>) = ( xor2a . <*x, y*>) & ( inv1 . <*( xor2 . <*x, y*>)*>) = ( xor2c . <*x, y*>) & ( xor2 . <*( inv1 . <*x*>), ( inv1 . <*y*>)*>) = ( xor2 . <*x, y*>)

    proof

      let x,y be Element of BOOLEAN ;

      

      thus ( inv1 . <*( xor2 . <*x, y*>)*>) = ( inv1 . <*(x 'xor' y)*>) by FACIRC_1:def 4

      .= ( 'not' (x 'xor' y)) by Def1

      .= (( 'not' x) 'xor' y) by XBOOLEAN: 74

      .= ( xor2a . <*x, y*>) by TWOSCOMP:def 14;

      hence ( inv1 . <*( xor2 . <*x, y*>)*>) = ( xor2c . <*x, y*>) by Th4;

      

      thus ( xor2 . <*( inv1 . <*x*>), ( inv1 . <*y*>)*>) = ( xor2 . <*( 'not' x), ( inv1 . <*y*>)*>) by Th1

      .= ( xor2 . <*( 'not' x), ( 'not' y)*>) by Th1

      .= (( 'not' x) 'xor' ( 'not' y)) by FACIRC_1:def 4

      .= (x 'xor' y)

      .= ( xor2 . <*x, y*>) by FACIRC_1:def 4;

    end;

    theorem :: GFACIRC1:6

    for x,y,z be Element of BOOLEAN holds ( inv1 . <*( xor2 . <*( xor2c . <*x, y*>), z*>)*>) = ( xor2c . <*( xor2c . <*x, y*>), z*>)

    proof

      let x,y,z be Element of BOOLEAN ;

      

      thus ( inv1 . <*( xor2 . <*( xor2c . <*x, y*>), z*>)*>) = ( inv1 . <*( xor2 . <*(x 'xor' ( 'not' y)), z*>)*>) by Def4

      .= ( inv1 . <*((x 'xor' ( 'not' y)) 'xor' z)*>) by FACIRC_1:def 4

      .= ( 'not' ((x 'xor' ( 'not' y)) 'xor' z)) by Def1

      .= ((x 'xor' ( 'not' y)) 'xor' ( 'not' z)) by XBOOLEAN: 74

      .= ( xor2c . <*(x 'xor' ( 'not' y)), z*>) by Def4

      .= ( xor2c . <*( xor2c . <*x, y*>), z*>) by Def4;

    end;

    theorem :: GFACIRC1:7

    for x,y,z be Element of BOOLEAN holds ((( 'not' x) 'xor' y) 'xor' ( 'not' z)) = ((x 'xor' ( 'not' y)) 'xor' ( 'not' z));

    theorem :: GFACIRC1:8

    for x,y,z be Element of BOOLEAN holds ( xor2c . <*( xor2a . <*x, y*>), z*>) = ( xor2c . <*( xor2c . <*x, y*>), z*>) by Th4;

    theorem :: GFACIRC1:9

    for x,y,z be Element of BOOLEAN holds ( inv1 . <*( xor2c . <*( xor2b . <*x, y*>), z*>)*>) = ( xor2 . <*( xor2 . <*x, y*>), z*>)

    proof

      let x,y,z be Element of BOOLEAN ;

      

      thus ( inv1 . <*( xor2c . <*( xor2b . <*x, y*>), z*>)*>) = ( inv1 . <*( xor2c . <*(( 'not' x) 'xor' ( 'not' y)), z*>)*>) by TWOSCOMP:def 15

      .= ( inv1 . <*((( 'not' x) 'xor' ( 'not' y)) 'xor' ( 'not' z))*>) by Def4

      .= ( 'not' ((( 'not' x) 'xor' ( 'not' y)) 'xor' ( 'not' z))) by Def1

      .= ((x 'xor' y) 'xor' z) by XBOOLEAN: 74

      .= ( xor2 . <*(x 'xor' y), z*>) by FACIRC_1:def 4

      .= ( xor2 . <*( xor2 . <*x, y*>), z*>) by FACIRC_1:def 4;

    end;

    

     Lm1: for f1,f2,f3 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN holds for x,y,z be set st x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1] holds not [ <*x, y*>, f1] in {y, z} & not z in { [ <*x, y*>, f1], [ <*y, z*>, f2]} & not x in { [ <*x, y*>, f1], [ <*y, z*>, f2]} & not [ <*z, x*>, f3] in {x, y, z}

    proof

      let f1,f2,f3 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN ;

      let x,y,z be set;

      set xy = { { <*x, y*>}, { <*x, y*>, f1}}, yz = { { <*y, z*>}, { <*y, z*>, f2}}, zx = { { <*z, x*>}, { <*z, x*>, f3}};

      assume that

       A1: x <> [ <*y, z*>, f2] and

       A2: y <> [ <*z, x*>, f3] and

       A3: z <> [ <*x, y*>, f1];

      

       A4: <*x, y*> in { <*x, y*>} & { <*x, y*>} in xy by TARSKI:def 1, TARSKI:def 2;

      ( dom <*x, y*>) = ( Seg 2) by FINSEQ_1: 89;

      then

       A5: 2 in ( dom <*x, y*>) by FINSEQ_1: 1;

      ( <*x, y*> . 2) = y by FINSEQ_1: 44;

      then

       A6: [2, y] in <*x, y*> by A5, FUNCT_1: 1;

      y in {2, y} & {2, y} in { {2}, {2, y}} by TARSKI:def 2;

      then y <> xy by A6, A4, XREGULAR: 9;

      hence not [ <*x, y*>, f1] in {y, z} by A3, TARSKI:def 2;

      

       A7: z in {2, z} & {2, z} in { {2}, {2, z}} by TARSKI:def 2;

      

       A8: <*x, y*> in { <*x, y*>} & { <*x, y*>} in xy by TARSKI:def 1, TARSKI:def 2;

       <*z*> = { [1, z]} by FINSEQ_1:def 5;

      then

       A9: [1, z] in <*z*> by TARSKI:def 1;

       <*x*> = { [1, x]} by FINSEQ_1:def 5;

      then

       A10: [1, x] in <*x*> by TARSKI:def 1;

      ( dom <*z, x*>) = ( Seg 2) by FINSEQ_1: 89;

      then

       A11: 2 in ( dom <*z, x*>) by FINSEQ_1: 1;

      ( <*z, x*> . 2) = x by FINSEQ_1: 44;

      then

       A12: [2, x] in <*z, x*> by A11, FUNCT_1: 1;

       <*z, x*> = ( <*z*> ^ <*x*>) by FINSEQ_1:def 9;

      then

       A13: <*z*> c= <*z, x*> by FINSEQ_6: 10;

      ( dom <*y, z*>) = ( Seg 2) by FINSEQ_1: 89;

      then

       A14: 2 in ( dom <*y, z*>) by FINSEQ_1: 1;

      ( <*y, z*> . 2) = z by FINSEQ_1: 44;

      then

       A15: [2, z] in <*y, z*> by A14, FUNCT_1: 1;

       <*x, y*> = ( <*x*> ^ <*y*>) by FINSEQ_1:def 9;

      then

       A16: <*x*> c= <*x, y*> by FINSEQ_6: 10;

       <*y, z*> in { <*y, z*>} & { <*y, z*>} in yz by TARSKI:def 1, TARSKI:def 2;

      then

       A17: z <> yz by A7, A15, XREGULAR: 9;

      x in {1, x} & {1, x} in { {1}, {1, x}} by TARSKI:def 2;

      then x <> xy by A16, A10, A8, XREGULAR: 9;

      hence not z in { [ <*x, y*>, f1], [ <*y, z*>, f2]} & not x in { [ <*x, y*>, f1], [ <*y, z*>, f2]} by A1, A3, A17, TARSKI:def 2;

      

       A18: <*z, x*> in { <*z, x*>} & { <*z, x*>} in zx by TARSKI:def 1, TARSKI:def 2;

      

       A19: <*z, x*> in { <*z, x*>} & { <*z, x*>} in zx by TARSKI:def 1, TARSKI:def 2;

      x in {2, x} & {2, x} in { {2}, {2, x}} by TARSKI:def 2;

      then

       A20: x <> zx by A12, A18, XREGULAR: 9;

      z in {1, z} & {1, z} in { {1}, {1, z}} by TARSKI:def 2;

      then z <> zx by A13, A9, A19, XREGULAR: 9;

      hence thesis by A2, A20, ENUMSET1:def 1;

    end;

    

     Lm2: for f1,f2,f3 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN holds for f4 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN holds for x,y,z be set holds ( {x, y, z} \ { [ <* [ <*x, y*>, f1], [ <*y, z*>, f2], [ <*z, x*>, f3]*>, f4]}) = {x, y, z}

    proof

      let f1,f2,f3 be Function of (2 -tuples_on BOOLEAN ), BOOLEAN ;

      let f4 be Function of (3 -tuples_on BOOLEAN ), BOOLEAN ;

      let x,y,z be set;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      

       A1: ( <*xy, yz, zx*> . 3) = zx by FINSEQ_1: 45;

      ( len <*xy, yz, zx*>) = 3 by FINSEQ_1: 45;

      then

       A2: ( Seg 3) = ( dom <*xy, yz, zx*>) by FINSEQ_1:def 3;

      then 3 in ( dom <*xy, yz, zx*>) by FINSEQ_1: 1;

      then [3, zx] in <*xy, yz, zx*> by A1, FUNCT_1: 1;

      then zx in ( rng <*xy, yz, zx*>) by XTUPLE_0:def 13;

      then

       A3: ( the_rank_of zx) in ( the_rank_of xyz) by CLASSES1: 82;

      ( rng <*y, z*>) = {y, z} by FINSEQ_2: 127;

      then

       A4: z in ( rng <*y, z*>) by TARSKI:def 2;

      thus ( {x, y, z} \ {xyz}) c= {x, y, z};

      

       A5: ( <*xy, yz, zx*> . 2) = yz by FINSEQ_1: 45;

      let a be object;

      

       A6: ( <*xy, yz, zx*> . 1) = xy by FINSEQ_1: 45;

      1 in ( dom <*xy, yz, zx*>) by A2, FINSEQ_1: 1;

      then [1, xy] in <*xy, yz, zx*> by A6, FUNCT_1: 1;

      then xy in ( rng <*xy, yz, zx*>) by XTUPLE_0:def 13;

      then

       A7: ( the_rank_of xy) in ( the_rank_of xyz) by CLASSES1: 82;

      ( rng <*z, x*>) = {z, x} by FINSEQ_2: 127;

      then

       A8: x in ( rng <*z, x*>) by TARSKI:def 2;

      2 in ( dom <*xy, yz, zx*>) by A2, FINSEQ_1: 1;

      then [2, yz] in <*xy, yz, zx*> by A5, FUNCT_1: 1;

      then yz in ( rng <*xy, yz, zx*>) by XTUPLE_0:def 13;

      then

       A9: ( the_rank_of yz) in ( the_rank_of xyz) by CLASSES1: 82;

      ( rng <*x, y*>) = {x, y} by FINSEQ_2: 127;

      then

       A10: y in ( rng <*x, y*>) by TARSKI:def 2;

      assume

       A11: a in {x, y, z};

      then a = x or a = y or a = z by ENUMSET1:def 1;

      then a <> xyz by A8, A3, A10, A7, A4, A9, CLASSES1: 82;

      then not a in {xyz} by TARSKI:def 1;

      hence thesis by A11, XBOOLE_0:def 5;

    end;

    

     Lm3: for f be Function of (2 -tuples_on BOOLEAN ), BOOLEAN holds for x,y,c be set st c <> [ <*x, y*>, f] holds for s be State of ( 2GatesCircuit (x,y,c,f)) holds (( Following s) . ( 2GatesCircOutput (x,y,c,f))) = (f . <*(s . [ <*x, y*>, f]), (s . c)*>) & (( Following s) . [ <*x, y*>, f]) = (f . <*(s . x), (s . y)*>) & (( Following s) . x) = (s . x) & (( Following s) . y) = (s . y) & (( Following s) . c) = (s . c)

    proof

      let f be Function of (2 -tuples_on BOOLEAN ), BOOLEAN ;

      let x,y,c be set such that

       A1: c <> [ <*x, y*>, f];

      set S = ( 2GatesCircStr (x,y,c,f));

      

       A2: ( InputVertices S) = {x, y, c} by A1, FACIRC_1: 57;

      then

       A3: c in ( InputVertices S) by ENUMSET1:def 1;

      set xyf = [ <*x, y*>, f];

      set p = <*xyf, c*>;

      set S2 = ( 1GateCircStr (p,f)), A2 = ( 1GateCircuit (xyf,c,f));

      ( InnerVertices S) = {xyf, ( 2GatesCircOutput (x,y,c,f))} by FACIRC_1: 56;

      then

      reconsider xyf as Element of ( InnerVertices S) by TARSKI:def 2;

      set A = ( 2GatesCircuit (x,y,c,f));

      let s be State of A;

      set S1 = ( 1GateCircStr ( <*x, y*>,f)), A1 = ( 1GateCircuit (x,y,f));

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

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      

       A4: ( dom s2) = the carrier of S2 by CIRCUIT1: 3;

      

       A5: ( rng p) = {xyf, c} by FINSEQ_2: 127;

      then c in ( rng p) by TARSKI:def 2;

      then

       A6: c in ( InputVertices S2) by CIRCCOMB: 42;

      xyf in ( rng p) by A5, TARSKI:def 2;

      then xyf in ( InputVertices S2) by CIRCCOMB: 42;

      then

      reconsider xyf9 = xyf, c9 = c as Vertex of S2 by A6;

      reconsider v2 = [p, f] as Element of ( InnerVertices S2) by FACIRC_1: 47;

      reconsider xyf1 = xyf as Element of ( InnerVertices S1) by FACIRC_1: 47;

      reconsider vx = x, vy = y as Vertex of S1 by FACIRC_1: 43;

      

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

      

      thus (( Following s) . ( 2GatesCircOutput (x,y,c,f))) = (( Following s2) . v2) by CIRCCOMB: 64

      .= (f . <*(s2 . xyf9), (s2 . c9)*>) by FACIRC_1: 50

      .= (f . <*(s . [ <*x, y*>, f]), (s2 . c9)*>) by A4, FUNCT_1: 47

      .= (f . <*(s . [ <*x, y*>, f]), (s . c)*>) by A4, FUNCT_1: 47;

      

      thus (( Following s) . [ <*x, y*>, f]) = (( Following s1) . xyf1) by CIRCCOMB: 64

      .= (f . <*(s1 . vx), (s1 . vy)*>) by FACIRC_1: 50

      .= (f . <*(s . x), (s1 . vy)*>) by A7, FUNCT_1: 47

      .= (f . <*(s . x), (s . y)*>) by A7, FUNCT_1: 47;

      x in ( InputVertices S) & y in ( InputVertices S) by A2, ENUMSET1:def 1;

      hence thesis by A3, CIRCUIT2:def 5;

    end;

    begin

    definition

      let x,y,z be set;

      :: GFACIRC1:def5

      func GFA0CarryIStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ((( 1GateCircStr ( <*x, y*>, and2 )) +* ( 1GateCircStr ( <*y, z*>, and2 ))) +* ( 1GateCircStr ( <*z, x*>, and2 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def6

      func GFA0CarryICirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA0CarryIStr (x,y,z)) equals ((( 1GateCircuit (x,y, and2 )) +* ( 1GateCircuit (y,z, and2 ))) +* ( 1GateCircuit (z,x, and2 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def7

      func GFA0CarryStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( GFA0CarryIStr (x,y,z)) +* ( 1GateCircStr ( <* [ <*x, y*>, and2 ], [ <*y, z*>, and2 ], [ <*z, x*>, and2 ]*>, or3 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def8

      func GFA0CarryCirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA0CarryStr (x,y,z)) equals (( GFA0CarryICirc (x,y,z)) +* ( 1GateCircuit ( [ <*x, y*>, and2 ], [ <*y, z*>, and2 ], [ <*z, x*>, and2 ], or3 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def9

      func GFA0CarryOutput (x,y,z) -> Element of ( InnerVertices ( GFA0CarryStr (x,y,z))) equals [ <* [ <*x, y*>, and2 ], [ <*y, z*>, and2 ], [ <*z, x*>, and2 ]*>, or3 ];

      coherence

      proof

         [ <* [ <*x, y*>, and2 ], [ <*y, z*>, and2 ], [ <*z, x*>, and2 ]*>, or3 ] in ( InnerVertices ( 1GateCircStr ( <* [ <*x, y*>, and2 ], [ <*y, z*>, and2 ], [ <*z, x*>, and2 ]*>, or3 ))) by FACIRC_1: 47;

        hence thesis by FACIRC_1: 21;

      end;

    end

    theorem :: GFACIRC1:10

    

     Th10: for x,y,z be set holds ( InnerVertices ( GFA0CarryIStr (x,y,z))) = { [ <*x, y*>, and2 ], [ <*y, z*>, and2 ], [ <*z, x*>, and2 ]}

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      

       A1: Cxy tolerates Cyz by CIRCCOMB: 47;

      (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 47;

      

      then ( InnerVertices ( GFA0CarryIStr (x,y,z))) = (( InnerVertices (Cxy +* Cyz)) \/ ( InnerVertices Czx)) by CIRCCOMB: 11

      .= ((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) by A1, CIRCCOMB: 11

      .= (( {xy} \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) by CIRCCOMB: 42

      .= (( {xy} \/ {yz}) \/ ( InnerVertices Czx)) by CIRCCOMB: 42

      .= (( {xy} \/ {yz}) \/ {zx}) by CIRCCOMB: 42

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      hence thesis;

    end;

    theorem :: GFACIRC1:11

    

     Th11: for x,y,z be set holds ( InnerVertices ( GFA0CarryStr (x,y,z))) = ( { [ <*x, y*>, and2 ], [ <*y, z*>, and2 ], [ <*z, x*>, and2 ]} \/ {( GFA0CarryOutput (x,y,z))})

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      

       A1: Cxy tolerates ((Cyz +* Czx) +* Cxyz) by CIRCCOMB: 47;

      Cyz tolerates (Czx +* Cxyz) by CIRCCOMB: 47;

      then

       A2: ( InnerVertices (Cyz +* (Czx +* Cxyz))) = (( InnerVertices Cyz) \/ ( InnerVertices (Czx +* Cxyz))) by CIRCCOMB: 11;

      Czx tolerates Cxyz by CIRCCOMB: 47;

      then

       A3: ( InnerVertices (Czx +* Cxyz)) = (( InnerVertices Czx) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 11;

      

      thus ( InnerVertices ( GFA0CarryStr (x,y,z))) = ( InnerVertices ((Cxy +* (Cyz +* Czx)) +* Cxyz)) by CIRCCOMB: 6

      .= ( InnerVertices (Cxy +* ((Cyz +* Czx) +* Cxyz))) by CIRCCOMB: 6

      .= (( InnerVertices Cxy) \/ ( InnerVertices ((Cyz +* Czx) +* Cxyz))) by A1, CIRCCOMB: 11

      .= (( InnerVertices Cxy) \/ ( InnerVertices (Cyz +* (Czx +* Cxyz)))) by CIRCCOMB: 6

      .= ((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ (( InnerVertices Czx) \/ ( InnerVertices Cxyz))) by A2, A3, XBOOLE_1: 4

      .= (((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by XBOOLE_1: 4

      .= ((( {xy} \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= ((( {xy} \/ {yz}) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= ((( {xy} \/ {yz}) \/ {zx}) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= (( {xy, yz} \/ {zx}) \/ ( InnerVertices Cxyz)) by ENUMSET1: 1

      .= ( {xy, yz, zx} \/ ( InnerVertices Cxyz)) by ENUMSET1: 3

      .= ( {xy, yz, zx} \/ {( GFA0CarryOutput (x,y,z))}) by CIRCCOMB: 42;

    end;

    theorem :: GFACIRC1:12

    

     Th12: for x,y,z be set holds ( InnerVertices ( GFA0CarryStr (x,y,z))) is Relation

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      ( InnerVertices Cxy) is Relation & ( InnerVertices Cyz) is Relation by FACIRC_1: 38;

      then ( InnerVertices Czx) is Relation & ( InnerVertices (Cxy +* Cyz)) is Relation by FACIRC_1: 3, FACIRC_1: 38;

      then ( InnerVertices Cxyz) is Relation & ( InnerVertices ( GFA0CarryIStr (x,y,z))) is Relation by FACIRC_1: 3, FACIRC_1: 38;

      hence thesis by FACIRC_1: 3;

    end;

    theorem :: GFACIRC1:13

    

     Th13: for x,y,z be set st x <> [ <*y, z*>, and2 ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2 ] holds ( InputVertices ( GFA0CarryIStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      assume that

       A1: x <> yz and

       A2: y <> zx & z <> xy;

      

       A3: not xy in {y, z} by A1, A2, Lm1;

      

       A4: not zx in {x, y, z} by A1, A2, Lm1;

      

       A5: y <> [ <*y, z*>, f2] by FACIRC_2: 2;

      

       A6: ( not z in {xy, yz}) & not x in {xy, yz} by A1, A2, Lm1;

      

       A7: Cxy tolerates Cyz by CIRCCOMB: 47;

      ( InputVertices ( GFA0CarryIStr (x,y,z))) = ((( InputVertices (Cxy +* Cyz)) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ ( InnerVertices (Cxy +* Cyz)))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((((( InputVertices Cxy) \ ( InnerVertices Cyz)) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ ( InnerVertices (Cxy +* Cyz)))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((((( InputVertices Cxy) \ ( InnerVertices Cyz)) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by A7, CIRCCOMB: 11

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by CIRCCOMB: 42

      .= (((( {x, y} \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ {xy, yz})) by ENUMSET1: 1

      .= ((( {x, y} \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ {xy, yz})) by A1, A5, FACIRC_2: 1

      .= ((( {x, y} \/ {y, z}) \ {zx}) \/ ( {z, x} \ {xy, yz})) by A3, ZFMISC_1: 57

      .= ((( {x, y} \/ {y, z}) \ {zx}) \/ {z, x}) by A6, ZFMISC_1: 63

      .= (( {x, y, y, z} \ {zx}) \/ {z, x}) by ENUMSET1: 5

      .= (( {y, y, x, z} \ {zx}) \/ {z, x}) by ENUMSET1: 67

      .= (( {y, x, z} \ {zx}) \/ {z, x}) by ENUMSET1: 31

      .= (( {x, y, z} \ {zx}) \/ {z, x}) by ENUMSET1: 58

      .= ( {x, y, z} \/ {z, x}) by A4, ZFMISC_1: 57

      .= {x, y, z, z, x} by ENUMSET1: 9

      .= ( {x, y, z, z} \/ {x}) by ENUMSET1: 10

      .= ( {z, z, x, y} \/ {x}) by ENUMSET1: 73

      .= ( {z, x, y} \/ {x}) by ENUMSET1: 31

      .= {z, x, y, x} by ENUMSET1: 6

      .= {x, x, y, z} by ENUMSET1: 70

      .= {x, y, z} by ENUMSET1: 31;

      hence thesis;

    end;

    theorem :: GFACIRC1:14

    

     Th14: for x,y,z be set st x <> [ <*y, z*>, and2 ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2 ] holds ( InputVertices ( GFA0CarryStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set MI = ( GFA0CarryIStr (x,y,z));

      assume

       A1: x <> yz & y <> zx & z <> xy;

      

       A2: ( InputVertices S) = ( rng <*xy, yz, zx*>) by CIRCCOMB: 42

      .= {xy, yz, zx} by FINSEQ_2: 128;

      

       A3: ( InnerVertices S) = {xyz} & ( {x, y, z} \ {xyz}) = {x, y, z} by Lm2, CIRCCOMB: 42;

      

       A4: ( {xy, yz, zx} \ {xy, yz, zx}) = {} by XBOOLE_1: 37;

      

      thus ( InputVertices ( GFA0CarryStr (x,y,z))) = ((( InputVertices MI) \ ( InnerVertices S)) \/ (( InputVertices S) \ ( InnerVertices MI))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ( {x, y, z} \/ ( {xy, yz, zx} \ ( InnerVertices MI))) by A1, A2, A3, Th13

      .= ( {x, y, z} \/ {} ) by A4, Th10

      .= {x, y, z};

    end;

    theorem :: GFACIRC1:15

    for x,y,z be non pair set holds ( InputVertices ( GFA0CarryStr (x,y,z))) is without_pairs

    proof

      let x,y,z be non pair set;

      set f1 = and2 , f2 = and2 , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set M = ( GFA0CarryStr (x,y,z));

      set MI = ( GFA0CarryIStr (x,y,z));

      given xx be pair object such that

       A1: xx in ( InputVertices M);

      

       A2: Cxy tolerates Cyz by CIRCCOMB: 47;

      

       A3: ( InnerVertices Czx) = {zx} & (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 42, CIRCCOMB: 47;

      ( InnerVertices Cxy) = {xy} & ( InnerVertices Cyz) = {yz} by CIRCCOMB: 42;

      then ( InnerVertices (Cxy +* Cyz)) = ( {xy} \/ {yz}) by A2, CIRCCOMB: 11;

      

      then

       A4: ( InnerVertices MI) = (( {xy} \/ {yz}) \/ {zx}) by A3, CIRCCOMB: 11

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      ( InputVertices S) = {xy, yz, zx} by FACIRC_1: 42;

      then

       A5: (( InputVertices S) \ ( InnerVertices MI)) = {} by A4, XBOOLE_1: 37;

      ( InputVertices Cxy) is without_pairs & ( InputVertices Cyz) is without_pairs by FACIRC_1: 41;

      then ( InputVertices Czx) is without_pairs & ( InputVertices (Cxy +* Cyz)) is without_pairs by FACIRC_1: 9, FACIRC_1: 41;

      then

       A6: ( InputVertices MI) is without_pairs by FACIRC_1: 9;

      ( InnerVertices S) is Relation by FACIRC_1: 38;

      then ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) by A6, FACIRC_1: 6;

      hence thesis by A6, A1, A5;

    end;

    theorem :: GFACIRC1:16

    

     Th16: for x,y,z be set holds x in the carrier of ( GFA0CarryStr (x,y,z)) & y in the carrier of ( GFA0CarryStr (x,y,z)) & z in the carrier of ( GFA0CarryStr (x,y,z)) & [ <*x, y*>, and2 ] in the carrier of ( GFA0CarryStr (x,y,z)) & [ <*y, z*>, and2 ] in the carrier of ( GFA0CarryStr (x,y,z)) & [ <*z, x*>, and2 ] in the carrier of ( GFA0CarryStr (x,y,z)) & [ <* [ <*x, y*>, and2 ], [ <*y, z*>, and2 ], [ <*z, x*>, and2 ]*>, or3 ] in the carrier of ( GFA0CarryStr (x,y,z))

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set p = <*xy, yz, zx*>;

      z in the carrier of Czx by FACIRC_1: 43;

      then

       A1: z in the carrier of ( GFA0CarryIStr (x,y,z)) by FACIRC_1: 20;

      zx in the carrier of Czx by FACIRC_1: 43;

      then

       A2: zx in the carrier of ( GFA0CarryIStr (x,y,z)) by FACIRC_1: 20;

      y in the carrier of Cxy by FACIRC_1: 43;

      then y in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A3: y in the carrier of ( GFA0CarryIStr (x,y,z)) by FACIRC_1: 20;

      the carrier of Cxyz = (( rng p) \/ {xyz}) & [p, f4] in { [p, f4]} by CIRCCOMB:def 6, TARSKI:def 1;

      then

       A4: xyz in the carrier of Cxyz by XBOOLE_0:def 3;

      yz in the carrier of Cyz by FACIRC_1: 43;

      then yz in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A5: yz in the carrier of ( GFA0CarryIStr (x,y,z)) by FACIRC_1: 20;

      xy in the carrier of Cxy by FACIRC_1: 43;

      then xy in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A6: xy in the carrier of ( GFA0CarryIStr (x,y,z)) by FACIRC_1: 20;

      x in the carrier of Czx by FACIRC_1: 43;

      then x in the carrier of ( GFA0CarryIStr (x,y,z)) by FACIRC_1: 20;

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

    end;

    theorem :: GFACIRC1:17

    

     Th17: for x,y,z be set holds [ <*x, y*>, and2 ] in ( InnerVertices ( GFA0CarryStr (x,y,z))) & [ <*y, z*>, and2 ] in ( InnerVertices ( GFA0CarryStr (x,y,z))) & [ <*z, x*>, and2 ] in ( InnerVertices ( GFA0CarryStr (x,y,z))) & ( GFA0CarryOutput (x,y,z)) in ( InnerVertices ( GFA0CarryStr (x,y,z)))

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      ( InnerVertices ( GFA0CarryStr (x,y,z))) = ( {xy, yz, zx} \/ {( GFA0CarryOutput (x,y,z))}) by Th11

      .= {xy, yz, zx, ( GFA0CarryOutput (x,y,z))} by ENUMSET1: 6;

      hence thesis by ENUMSET1:def 2;

    end;

    theorem :: GFACIRC1:18

    

     Th18: for x,y,z be set st x <> [ <*y, z*>, and2 ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2 ] holds x in ( InputVertices ( GFA0CarryStr (x,y,z))) & y in ( InputVertices ( GFA0CarryStr (x,y,z))) & z in ( InputVertices ( GFA0CarryStr (x,y,z)))

    proof

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      let x,y,z be set;

      assume x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      then ( InputVertices ( GFA0CarryStr (x,y,z))) = {x, y, z} by Th14;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: GFACIRC1:19

    

     Th19: for x,y,z be non pair set holds ( InputVertices ( GFA0CarryStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be non pair set;

      set f1 = and2 , f2 = and2 , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set M = ( GFA0CarryStr (x,y,z));

      set MI = ( GFA0CarryIStr (x,y,z));

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      

       A1: ( InputVertices Cxy) = {x, y} & ( InputVertices Cyz) = {y, z} by FACIRC_1: 40;

      

       A2: ( InputVertices Czx) = {z, x} by FACIRC_1: 40;

      

       A3: ( InputVertices S) = {xy, yz, zx} by FACIRC_1: 42;

      

       A4: ( InnerVertices S) is Relation by FACIRC_1: 38;

      

       A5: ( InnerVertices Cxy) = {xy} & ( InnerVertices Cyz) = {yz} by CIRCCOMB: 42;

      Cxy tolerates Cyz by CIRCCOMB: 47;

      then

       A6: ( InnerVertices Czx) = {zx} & ( InnerVertices (Cxy +* Cyz)) = ( {xy} \/ {yz}) by A5, CIRCCOMB: 11, CIRCCOMB: 42;

      (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 47;

      

      then ( InnerVertices MI) = (( {xy} \/ {yz}) \/ {zx}) by A6, CIRCCOMB: 11

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      then

       A7: (( InputVertices S) \ ( InnerVertices MI)) = {} by A3, XBOOLE_1: 37;

      

       A8: ( InputVertices Cxy) is without_pairs & ( InputVertices Cyz) is without_pairs by FACIRC_1: 41;

      then

       A9: ( InputVertices Czx) is without_pairs & ( InputVertices (Cxy +* Cyz)) is without_pairs by FACIRC_1: 9, FACIRC_1: 41;

      then ( InputVertices MI) is without_pairs by FACIRC_1: 9;

      then ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) by A4, FACIRC_1: 6;

      

      hence ( InputVertices M) = (( InputVertices (Cxy +* Cyz)) \/ ( InputVertices Czx)) by A9, A6, A7, FACIRC_1: 7

      .= ((( InputVertices Cxy) \/ ( InputVertices Cyz)) \/ ( InputVertices Czx)) by A8, A5, FACIRC_1: 7

      .= ( {x, y, y, z} \/ {z, x}) by A1, A2, ENUMSET1: 5

      .= ( {y, y, x, z} \/ {z, x}) by ENUMSET1: 67

      .= ( {y, x, z} \/ {z, x}) by ENUMSET1: 31

      .= ( {x, y, z} \/ {z, x}) by ENUMSET1: 58

      .= ( {x, y, z} \/ ( {z} \/ {x})) by ENUMSET1: 1

      .= (( {x, y, z} \/ {z}) \/ {x}) by XBOOLE_1: 4

      .= (( {z, x, y} \/ {z}) \/ {x}) by ENUMSET1: 59

      .= ( {z, z, x, y} \/ {x}) by ENUMSET1: 4

      .= ( {z, x, y} \/ {x}) by ENUMSET1: 31

      .= ( {x, y, z} \/ {x}) by ENUMSET1: 59

      .= {x, x, y, z} by ENUMSET1: 4

      .= {x, y, z} by ENUMSET1: 31;

    end;

    theorem :: GFACIRC1:20

    

     Th20: for x,y,z be set holds for s be State of ( GFA0CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following s) . [ <*x, y*>, and2 ]) = (a1 '&' a2) & (( Following s) . [ <*y, z*>, and2 ]) = (a2 '&' a3) & (( Following s) . [ <*z, x*>, and2 ]) = (a3 '&' a1)

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      let s be State of ( GFA0CarryCirc (x,y,z));

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

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

       A1: a1 = (s . x) and

       A2: a2 = (s . y) and

       A3: a3 = (s . z);

      set S = ( GFA0CarryStr (x,y,z));

      

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

      

       A5: y in the carrier of S by Th16;

      

       A6: x in the carrier of S by Th16;

      

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

      xy in ( InnerVertices ( GFA0CarryStr (x,y,z))) by Th17;

      

      hence (( Following s) . [ <*x, y*>, f1]) = (f1 . (s * <*x, y*>)) by A4, FACIRC_1: 35

      .= (f1 . <*a1, a2*>) by A1, A2, A7, A6, A5, FINSEQ_2: 125

      .= (a1 '&' a2) by FACIRC_1:def 6;

      

       A8: z in the carrier of S by Th16;

      yz in ( InnerVertices ( GFA0CarryStr (x,y,z))) by Th17;

      

      hence (( Following s) . [ <*y, z*>, f2]) = (f2 . (s * <*y, z*>)) by A4, FACIRC_1: 35

      .= (f2 . <*a2, a3*>) by A2, A3, A7, A5, A8, FINSEQ_2: 125

      .= (a2 '&' a3) by FACIRC_1:def 6;

      zx in ( InnerVertices ( GFA0CarryStr (x,y,z))) by Th17;

      

      hence (( Following s) . [ <*z, x*>, f3]) = (f3 . (s * <*z, x*>)) by A4, FACIRC_1: 35

      .= (f3 . <*a3, a1*>) by A1, A3, A7, A6, A8, FINSEQ_2: 125

      .= (a3 '&' a1) by FACIRC_1:def 6;

    end;

    theorem :: GFACIRC1:21

    

     Th21: for x,y,z be set holds for s be State of ( GFA0CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . [ <*x, y*>, and2 ]) & a2 = (s . [ <*y, z*>, and2 ]) & a3 = (s . [ <*z, x*>, and2 ]) holds (( Following s) . ( GFA0CarryOutput (x,y,z))) = ((a1 'or' a2) 'or' a3)

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 , f4 = or3 ;

      let s be State of ( GFA0CarryCirc (x,y,z));

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

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

       A1: a1 = (s . xy) & a2 = (s . yz) & a3 = (s . zx);

      set S = ( GFA0CarryStr (x,y,z));

      reconsider xy, yz, zx as Element of ( InnerVertices S) by Th17;

      

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

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

      

      hence (( Following s) . ( GFA0CarryOutput (x,y,z))) = (f4 . (s * <*xy, yz, zx*>)) by FACIRC_1: 35

      .= (f4 . <*a1, a2, a3*>) by A1, A2, FINSEQ_2: 126

      .= ((a1 'or' a2) 'or' a3) by TWOSCOMP: 14;

    end;

    theorem :: GFACIRC1:22

    

     Th22: for x,y,z be set st x <> [ <*y, z*>, and2 ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2 ] holds for s be State of ( GFA0CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA0CarryOutput (x,y,z))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) & (( Following (s,2)) . [ <*x, y*>, and2 ]) = (a1 '&' a2) & (( Following (s,2)) . [ <*y, z*>, and2 ]) = (a2 '&' a3) & (( Following (s,2)) . [ <*z, x*>, and2 ]) = (a3 '&' a1)

    proof

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      let x,y,z be set such that

       A1: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( GFA0CarryStr (x,y,z));

      reconsider x9 = x, y9 = y, z9 = z as Vertex of S by Th16;

      let s be State of ( GFA0CarryCirc (x,y,z));

      y in ( InputVertices S) by A1, Th18;

      then

       A2: (( Following s) . y9) = (s . y) by CIRCUIT2:def 5;

      z in ( InputVertices S) by A1, Th18;

      then

       A3: (( Following s) . z9) = (s . z) by CIRCUIT2:def 5;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      

       A4: ( Following (s,2)) = ( Following ( Following s)) by FACIRC_1: 15;

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

       A5: a1 = (s . x) & a2 = (s . y) & a3 = (s . z);

      

       A6: (( Following s) . zx) = (a3 '&' a1) by A5, Th20;

      (( Following s) . xy) = (a1 '&' a2) & (( Following s) . yz) = (a2 '&' a3) by A5, Th20;

      hence (( Following (s,2)) . ( GFA0CarryOutput (x,y,z))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) by A4, A6, Th21;

      x in ( InputVertices S) by A1, Th18;

      then (( Following s) . x9) = (s . x) by CIRCUIT2:def 5;

      hence thesis by A5, A2, A3, A4, Th20;

    end;

    theorem :: GFACIRC1:23

    

     Th23: for x,y,z be set st x <> [ <*y, z*>, and2 ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2 ] holds for s be State of ( GFA0CarryCirc (x,y,z)) holds ( Following (s,2)) is stable

    proof

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      let x,y,z be set such that

       A1: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( GFA0CarryStr (x,y,z));

      reconsider xx = x, yy = y, zz = z as Vertex of S by Th16;

      let s be State of ( GFA0CarryCirc (x,y,z));

      set a1 = (s . xx), a2 = (s . yy), a3 = (s . zz);

      set ffs = ( Following (s,2)), fffs = ( Following ffs);

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      

       A2: ffs = ( Following ( Following s)) by FACIRC_1: 15;

      

       A3: z in ( InputVertices S) by A1, Th18;

      then (( Following s) . z) = a3 by CIRCUIT2:def 5;

      then

       A4: (ffs . z) = a3 by A2, A3, CIRCUIT2:def 5;

      

       A5: y in ( InputVertices S) by A1, Th18;

      then (( Following s) . y) = a2 by CIRCUIT2:def 5;

      then

       A6: (ffs . y) = a2 by A2, A5, CIRCUIT2:def 5;

      

       A7: x in ( InputVertices S) by A1, Th18;

      then (( Following s) . x) = a1 by CIRCUIT2:def 5;

      then

       A8: (ffs . x) = a1 by A2, A7, CIRCUIT2:def 5;

      a3 = (s . z);

      then

       A9: (ffs . xy) = (a1 '&' a2) by A1, Th22;

      a2 = (s . y);

      then

       A10: (ffs . zx) = (a1 '&' a3) by A1, Th22;

      a1 = (s . x);

      then

       A11: (ffs . yz) = (a2 '&' a3) by A1, Th22;

      

       A12: (ffs . ( GFA0CarryOutput (x,y,z))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) by A1, Th22;

       A13:

      now

        let a be object;

        assume

         A14: a in the carrier of S;

        then

        reconsider v = a as Vertex of S;

        

         A15: v in (( InputVertices S) \/ ( InnerVertices S)) by A14, XBOOLE_1: 45;

        thus (ffs . a) = (fffs . a)

        proof

          per cases by A15, XBOOLE_0:def 3;

            suppose v in ( InputVertices S);

            hence thesis by CIRCUIT2:def 5;

          end;

            suppose v in ( InnerVertices S);

            then v in ( {xy, yz, zx} \/ {( GFA0CarryOutput (x,y,z))}) by Th11;

            then v in {xy, yz, zx} or v in {( GFA0CarryOutput (x,y,z))} by XBOOLE_0:def 3;

            then v = xy or v = yz or v = zx or v = ( GFA0CarryOutput (x,y,z)) by ENUMSET1:def 1, TARSKI:def 1;

            hence thesis by A12, A9, A11, A10, A8, A6, A4, Th20, Th21;

          end;

        end;

      end;

      ( dom ( Following ( Following (s,2)))) = the carrier of S & ( dom ( Following (s,2))) = the carrier of S by CIRCUIT1: 3;

      hence ffs = fffs by A13, FUNCT_1: 2;

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def10

      func GFA0AdderStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ( 2GatesCircStr (x,y,z, xor2 ));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def11

      func GFA0AdderCirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA0AdderStr (x,y,z)) equals ( 2GatesCircuit (x,y,z, xor2 ));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def12

      func GFA0AdderOutput (x,y,z) -> Element of ( InnerVertices ( GFA0AdderStr (x,y,z))) equals ( 2GatesCircOutput (x,y,z, xor2 ));

      coherence ;

    end

    theorem :: GFACIRC1:24

    

     Th24: for x,y,z be set holds ( InnerVertices ( GFA0AdderStr (x,y,z))) = ( { [ <*x, y*>, xor2 ]} \/ {( GFA0AdderOutput (x,y,z))})

    proof

      let x,y,z be set;

      set f = xor2 ;

      set xy = [ <*x, y*>, f];

      set S = ( GFA0AdderStr (x,y,z));

      

      thus ( InnerVertices S) = {xy, ( GFA0AdderOutput (x,y,z))} by FACIRC_1: 56

      .= ( {xy} \/ {( GFA0AdderOutput (x,y,z))}) by ENUMSET1: 1;

    end;

    theorem :: GFACIRC1:25

    for x,y,z be set holds x in the carrier of ( GFA0AdderStr (x,y,z)) & y in the carrier of ( GFA0AdderStr (x,y,z)) & z in the carrier of ( GFA0AdderStr (x,y,z)) & [ <*x, y*>, xor2 ] in the carrier of ( GFA0AdderStr (x,y,z)) & [ <* [ <*x, y*>, xor2 ], z*>, xor2 ] in the carrier of ( GFA0AdderStr (x,y,z)) by FACIRC_1: 60, FACIRC_1: 61;

    theorem :: GFACIRC1:26

    

     Th26: for x,y,z be set holds [ <*x, y*>, xor2 ] in ( InnerVertices ( GFA0AdderStr (x,y,z))) & ( GFA0AdderOutput (x,y,z)) in ( InnerVertices ( GFA0AdderStr (x,y,z)))

    proof

      let x,y,z be set;

      set f = xor2 ;

      set S = ( GFA0AdderStr (x,y,z));

      ( InnerVertices S) = ( { [ <*x, y*>, f]} \/ {( GFA0AdderOutput (x,y,z))}) by Th24

      .= { [ <*x, y*>, f], ( GFA0AdderOutput (x,y,z))} by ENUMSET1: 1;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: GFACIRC1:27

    

     Th27: for x,y,z be set st z <> [ <*x, y*>, xor2 ] holds x in ( InputVertices ( GFA0AdderStr (x,y,z))) & y in ( InputVertices ( GFA0AdderStr (x,y,z))) & z in ( InputVertices ( GFA0AdderStr (x,y,z)))

    proof

      set f = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set S = ( GFA0AdderStr (x,y,z));

      ( InputVertices S) = {x, y, z} by A1, FACIRC_1: 57;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: GFACIRC1:28

    

     Th28: for x,y,z be set st z <> [ <*x, y*>, xor2 ] holds for s be State of ( GFA0AdderCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following s) . [ <*x, y*>, xor2 ]) = (a1 'xor' a2) & (( Following s) . x) = a1 & (( Following s) . y) = a2 & (( Following s) . z) = a3

    proof

      set f = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set A = ( GFA0AdderCirc (x,y,z));

      set xy = [ <*x, y*>, f];

      let s be State of A;

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

       A2: a1 = (s . x) & a2 = (s . y) and

       A3: a3 = (s . z);

      (( Following s) . xy) = (f . <*a1, a2*>) by A1, A2, Lm3;

      hence (( Following s) . xy) = (a1 'xor' a2) by FACIRC_1:def 4;

      thus thesis by A1, A2, A3, Lm3;

    end;

    theorem :: GFACIRC1:29

    

     Th29: for x,y,z be set st z <> [ <*x, y*>, xor2 ] holds for s be State of ( GFA0AdderCirc (x,y,z)) holds for a1a2,a1,a2,a3 be Element of BOOLEAN st a1a2 = (s . [ <*x, y*>, xor2 ]) & a3 = (s . z) holds (( Following s) . ( GFA0AdderOutput (x,y,z))) = (a1a2 'xor' a3)

    proof

      set f = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set A = ( GFA0AdderCirc (x,y,z));

      set xy = [ <*x, y*>, f];

      let s be State of A;

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

       A2: a1a2 = (s . xy) & a3 = (s . z);

      

      thus (( Following s) . ( GFA0AdderOutput (x,y,z))) = (f . <*(s . xy), (s . z)*>) by A1, Lm3

      .= (a1a2 'xor' a3) by A2, FACIRC_1:def 4;

    end;

    theorem :: GFACIRC1:30

    

     Th30: for x,y,z be set st z <> [ <*x, y*>, xor2 ] holds for s be State of ( GFA0AdderCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA0AdderOutput (x,y,z))) = ((a1 'xor' a2) 'xor' a3) & (( Following (s,2)) . [ <*x, y*>, xor2 ]) = (a1 'xor' a2) & (( Following (s,2)) . x) = a1 & (( Following (s,2)) . y) = a2 & (( Following (s,2)) . z) = a3

    proof

      set f = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set xy = [ <*x, y*>, f];

      set A = ( GFA0AdderCirc (x,y,z));

      let s be State of A;

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

       A2: a1 = (s . x) & a2 = (s . y) and

       A3: a3 = (s . z);

      

      thus (( Following (s,2)) . ( GFA0AdderOutput (x,y,z))) = (f . <*(f . <*a1, a2*>), a3*>) by A1, A2, A3, FACIRC_1: 62

      .= (f . <*(a1 'xor' a2), a3*>) by FACIRC_1:def 4

      .= ((a1 'xor' a2) 'xor' a3) by FACIRC_1:def 4;

      (( Following (s,2)) . xy) = (f . <*a1, a2*>) by A1, A2, FACIRC_1: 62;

      hence (( Following (s,2)) . xy) = (a1 'xor' a2) by FACIRC_1:def 4;

      thus thesis by A1, A2, A3, FACIRC_1: 62;

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def13

      func BitGFA0Str (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( GFA0AdderStr (x,y,z)) +* ( GFA0CarryStr (x,y,z)));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def14

      func BitGFA0Circ (x,y,z) -> strict Boolean gate`2=den Circuit of ( BitGFA0Str (x,y,z)) equals (( GFA0AdderCirc (x,y,z)) +* ( GFA0CarryCirc (x,y,z)));

      coherence ;

    end

    theorem :: GFACIRC1:31

    

     Th31: for x,y,z be set holds ( InnerVertices ( BitGFA0Str (x,y,z))) = ((( { [ <*x, y*>, xor2 ]} \/ {( GFA0AdderOutput (x,y,z))}) \/ { [ <*x, y*>, and2 ], [ <*y, z*>, and2 ], [ <*z, x*>, and2 ]}) \/ {( GFA0CarryOutput (x,y,z))})

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      set f0 = xor2 ;

      set xyf0 = [ <*x, y*>, f0];

      set xyf1 = [ <*x, y*>, f1], yzf2 = [ <*y, z*>, f2], zxf3 = [ <*z, x*>, f3];

      set S = ( BitGFA0Str (x,y,z));

      set S1 = ( GFA0AdderStr (x,y,z));

      set S2 = ( GFA0CarryStr (x,y,z));

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

      set A2 = ( GFA0CarryOutput (x,y,z));

      

      thus ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by FACIRC_1: 27

      .= (( {xyf0} \/ {A1}) \/ ( InnerVertices S2)) by Th24

      .= (( {xyf0} \/ {A1}) \/ ( {xyf1, yzf2, zxf3} \/ {A2})) by Th11

      .= ((( {xyf0} \/ {A1}) \/ {xyf1, yzf2, zxf3}) \/ {A2}) by XBOOLE_1: 4;

    end;

    theorem :: GFACIRC1:32

    for x,y,z be set holds ( InnerVertices ( BitGFA0Str (x,y,z))) is Relation

    proof

      let x,y,z be set;

      set S1 = ( GFA0AdderStr (x,y,z));

      set S2 = ( GFA0CarryStr (x,y,z));

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by Th12, FACIRC_1: 58;

      hence thesis by FACIRC_1: 3;

    end;

    theorem :: GFACIRC1:33

    

     Th33: for x,y,z be set st z <> [ <*x, y*>, xor2 ] & x <> [ <*y, z*>, and2 ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2 ] holds ( InputVertices ( BitGFA0Str (x,y,z))) = {x, y, z}

    proof

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      set f0 = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] & x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S2 = ( GFA0CarryStr (x,y,z));

      set S1 = ( GFA0AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} & ( InputVertices S2) = {x, y, z} by A1, Th14, FACIRC_1: 57;

      hence thesis by CIRCCOMB: 47, FACIRC_2: 21;

    end;

    theorem :: GFACIRC1:34

    

     Th34: for x,y,z be non pair set holds ( InputVertices ( BitGFA0Str (x,y,z))) = {x, y, z}

    proof

      let x,y,z be non pair set;

      set S = ( BitGFA0Str (x,y,z));

      set S1 = ( GFA0AdderStr (x,y,z));

      set S2 = ( GFA0CarryStr (x,y,z));

      

       A1: ( InputVertices S1) = {x, y, z} & ( InputVertices S2) = {x, y, z} by Th19, FACIRC_1: 57;

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by Th12, FACIRC_1: 58;

      

      hence ( InputVertices S) = ( {x, y, z} \/ {x, y, z}) by A1, FACIRC_1: 7

      .= {x, y, z};

    end;

    theorem :: GFACIRC1:35

    for x,y,z be non pair set holds ( InputVertices ( BitGFA0Str (x,y,z))) is without_pairs

    proof

      let x,y,z be non pair set;

      ( InputVertices ( BitGFA0Str (x,y,z))) = {x, y, z} by Th34;

      hence thesis;

    end;

    theorem :: GFACIRC1:36

    for x,y,z be set holds x in the carrier of ( BitGFA0Str (x,y,z)) & y in the carrier of ( BitGFA0Str (x,y,z)) & z in the carrier of ( BitGFA0Str (x,y,z)) & [ <*x, y*>, xor2 ] in the carrier of ( BitGFA0Str (x,y,z)) & [ <* [ <*x, y*>, xor2 ], z*>, xor2 ] in the carrier of ( BitGFA0Str (x,y,z)) & [ <*x, y*>, and2 ] in the carrier of ( BitGFA0Str (x,y,z)) & [ <*y, z*>, and2 ] in the carrier of ( BitGFA0Str (x,y,z)) & [ <*z, x*>, and2 ] in the carrier of ( BitGFA0Str (x,y,z)) & [ <* [ <*x, y*>, and2 ], [ <*y, z*>, and2 ], [ <*z, x*>, and2 ]*>, or3 ] in the carrier of ( BitGFA0Str (x,y,z))

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 , f4 = or3 ;

      set f0 = xor2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set S1 = ( GFA0AdderStr (x,y,z));

      set S2 = ( GFA0CarryStr (x,y,z));

      

       A1: x in the carrier of S1 & y in the carrier of S1 by FACIRC_1: 60;

      

       A2: z in the carrier of S1 & [ <*x, y*>, f0] in the carrier of S1 by FACIRC_1: 60, FACIRC_1: 61;

      

       A3: xyz in the carrier of S2 by Th16;

      

       A4: yz in the carrier of S2 & zx in the carrier of S2 by Th16;

       [ <* [ <*x, y*>, f0], z*>, f0] in the carrier of S1 & xy in the carrier of S2 by Th16, FACIRC_1: 61;

      hence thesis by A1, A2, A4, A3, FACIRC_1: 20;

    end;

    theorem :: GFACIRC1:37

    

     Th37: for x,y,z be set holds [ <*x, y*>, xor2 ] in ( InnerVertices ( BitGFA0Str (x,y,z))) & ( GFA0AdderOutput (x,y,z)) in ( InnerVertices ( BitGFA0Str (x,y,z))) & [ <*x, y*>, and2 ] in ( InnerVertices ( BitGFA0Str (x,y,z))) & [ <*y, z*>, and2 ] in ( InnerVertices ( BitGFA0Str (x,y,z))) & [ <*z, x*>, and2 ] in ( InnerVertices ( BitGFA0Str (x,y,z))) & ( GFA0CarryOutput (x,y,z)) in ( InnerVertices ( BitGFA0Str (x,y,z)))

    proof

      let x,y,z be set;

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      set f0 = xor2 ;

      set xyf0 = [ <*x, y*>, f0];

      set xyf1 = [ <*x, y*>, f1], yzf2 = [ <*y, z*>, f2], zxf3 = [ <*z, x*>, f3];

      set S = ( BitGFA0Str (x,y,z));

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

      set A2 = ( GFA0CarryOutput (x,y,z));

      ( InnerVertices S) = ((( {xyf0} \/ {A1}) \/ {xyf1, yzf2, zxf3}) \/ {A2}) by Th31

      .= (( {xyf0, A1} \/ {xyf1, yzf2, zxf3}) \/ {A2}) by ENUMSET1: 1

      .= ( {xyf0, A1, xyf1, yzf2, zxf3} \/ {A2}) by ENUMSET1: 8

      .= {xyf0, A1, xyf1, yzf2, zxf3, A2} by ENUMSET1: 15;

      hence thesis by ENUMSET1:def 4;

    end;

    theorem :: GFACIRC1:38

    for x,y,z be set st z <> [ <*x, y*>, xor2 ] & x <> [ <*y, z*>, and2 ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2 ] holds x in ( InputVertices ( BitGFA0Str (x,y,z))) & y in ( InputVertices ( BitGFA0Str (x,y,z))) & z in ( InputVertices ( BitGFA0Str (x,y,z)))

    proof

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      set f0 = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] & x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( BitGFA0Str (x,y,z));

      ( InputVertices S) = {x, y, z} by A1, Th33;

      hence thesis by ENUMSET1:def 1;

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def15

      func BitGFA0CarryOutput (x,y,z) -> Element of ( InnerVertices ( BitGFA0Str (x,y,z))) equals [ <* [ <*x, y*>, and2 ], [ <*y, z*>, and2 ], [ <*z, x*>, and2 ]*>, or3 ];

      coherence

      proof

        ( GFA0CarryOutput (x,y,z)) in ( InnerVertices ( BitGFA0Str (x,y,z))) by Th37;

        hence thesis;

      end;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def16

      func BitGFA0AdderOutput (x,y,z) -> Element of ( InnerVertices ( BitGFA0Str (x,y,z))) equals ( 2GatesCircOutput (x,y,z, xor2 ));

      coherence

      proof

        ( GFA0AdderOutput (x,y,z)) in ( InnerVertices ( BitGFA0Str (x,y,z))) by Th37;

        hence thesis;

      end;

    end

    theorem :: GFACIRC1:39

    for x,y,z be set st z <> [ <*x, y*>, xor2 ] & x <> [ <*y, z*>, and2 ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2 ] holds for s be State of ( BitGFA0Circ (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA0AdderOutput (x,y,z))) = ((a1 'xor' a2) 'xor' a3) & (( Following (s,2)) . ( GFA0CarryOutput (x,y,z))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1))

    proof

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      set f0 = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] and

       A2: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S2 = ( GFA0CarryStr (x,y,z));

      set S1 = ( GFA0AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} by A1, FACIRC_1: 57;

      then

       A3: ( InputVertices S1) = ( InputVertices S2) by A2, Th14;

      set A2 = ( GFA0CarryCirc (x,y,z));

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

      set A = ( BitGFA0Circ (x,y,z));

      let s be State of A;

      let a1,a2,a3 be Element of BOOLEAN ;

      assume that

       A4: a1 = (s . x) and

       A5: a2 = (s . y) and

       A6: a3 = (s . z);

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

      

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

      z in the carrier of S1 by FACIRC_1: 60;

      then

       A8: a3 = (s1 . z) by A6, A7, FUNCT_1: 47;

      y in the carrier of S1 by FACIRC_1: 60;

      then

       A9: a2 = (s1 . y) by A5, A7, FUNCT_1: 47;

      reconsider t = s as State of (A1 +* A2);

      ( InnerVertices S2) misses ( InputVertices S2) by XBOOLE_1: 79;

      then

       A10: (( Following (t,2)) . ( GFA0AdderOutput (x,y,z))) = (( Following (s1,2)) . ( GFA0AdderOutput (x,y,z))) by A3, FACIRC_1: 32;

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      

       A11: ( dom s2) = the carrier of S2 by CIRCUIT1: 3;

      x in the carrier of S1 by FACIRC_1: 60;

      then a1 = (s1 . x) by A4, A7, FUNCT_1: 47;

      hence (( Following (s,2)) . ( GFA0AdderOutput (x,y,z))) = ((a1 'xor' a2) 'xor' a3) by A1, A9, A8, A10, Th30;

      ( InnerVertices S1) misses ( InputVertices S1) by XBOOLE_1: 79;

      then

       A12: (( Following (t,2)) . ( GFA0CarryOutput (x,y,z))) = (( Following (s2,2)) . ( GFA0CarryOutput (x,y,z))) by A3, FACIRC_1: 33;

      z in the carrier of S2 by Th16;

      then

       A13: a3 = (s2 . z) by A6, A11, FUNCT_1: 47;

      y in the carrier of S2 by Th16;

      then

       A14: a2 = (s2 . y) by A5, A11, FUNCT_1: 47;

      x in the carrier of S2 by Th16;

      then a1 = (s2 . x) by A4, A11, FUNCT_1: 47;

      hence thesis by A2, A14, A13, A12, Th22;

    end;

    theorem :: GFACIRC1:40

    for x,y,z be set st z <> [ <*x, y*>, xor2 ] & x <> [ <*y, z*>, and2 ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2 ] holds for s be State of ( BitGFA0Circ (x,y,z)) holds ( Following (s,2)) is stable

    proof

      set f1 = and2 , f2 = and2 , f3 = and2 ;

      set f0 = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] and

       A2: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set A = ( BitGFA0Circ (x,y,z));

      let s be State of A;

      set S2 = ( GFA0CarryStr (x,y,z));

      set S1 = ( GFA0AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} by A1, FACIRC_1: 57;

      then

       A3: ( InputVertices S1) = ( InputVertices S2) by A2, Th14;

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

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

      ( Following (s1,2)) is stable by A1, FACIRC_1: 63;

      

      then

       A4: ( Following (s1,2)) = ( Following ( Following (s1,2)))

      .= ( Following (s1,(2 + 1))) by FACIRC_1: 12;

      set A2 = ( GFA0CarryCirc (x,y,z));

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      ( Following (s2,2)) is stable by A2, Th23;

      

      then

       A5: ( Following (s2,2)) = ( Following ( Following (s2,2)))

      .= ( Following (s2,(2 + 1))) by FACIRC_1: 12;

      reconsider t = s as State of (A1 +* A2);

      set S = ( BitGFA0Str (x,y,z));

      

       A6: ( dom ( Following (s,3))) = the carrier of S by CIRCUIT1: 3;

      ( InnerVertices S2) misses ( InputVertices S2) by XBOOLE_1: 79;

      then

       A7: ( Following (s1,2)) = (( Following (t,2)) | the carrier of S1) & ( Following (s1,3)) = (( Following (t,3)) | the carrier of S1) by A3, FACIRC_1: 30;

      ( InnerVertices S1) misses ( InputVertices S1) by XBOOLE_1: 79;

      then

       A8: ( Following (s2,2)) = (( Following (t,2)) | the carrier of S2) & ( Following (s2,3)) = (( Following (t,3)) | the carrier of S2) by A3, FACIRC_1: 31;

      

       A9: the carrier of S = (the carrier of S1 \/ the carrier of S2) by CIRCCOMB:def 2;

      

       A10: ( dom ( Following (s1,2))) = the carrier of S1 & ( dom ( Following (s2,2))) = the carrier of S2 by CIRCUIT1: 3;

       A11:

      now

        let a be object;

        assume a in the carrier of S;

        then a in the carrier of S1 or a in the carrier of S2 by A9, XBOOLE_0:def 3;

        then (( Following (s,2)) . a) = (( Following (s1,2)) . a) & (( Following (s,3)) . a) = (( Following (s1,3)) . a) or (( Following (s,2)) . a) = (( Following (s2,2)) . a) & (( Following (s,3)) . a) = (( Following (s2,3)) . a) by A7, A8, A4, A5, A10, FUNCT_1: 47;

        hence (( Following (s,2)) . a) = (( Following ( Following (s,2))) . a) by A4, A5, FACIRC_1: 12;

      end;

      ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) & ( dom ( Following (s,2))) = the carrier of S by CIRCUIT1: 3, FACIRC_1: 12;

      hence ( Following (s,2)) = ( Following ( Following (s,2))) by A6, A11, FUNCT_1: 2;

    end;

    begin

    definition

      let x,y,z be set;

      :: GFACIRC1:def17

      func GFA1CarryIStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ((( 1GateCircStr ( <*x, y*>, and2c )) +* ( 1GateCircStr ( <*y, z*>, and2a ))) +* ( 1GateCircStr ( <*z, x*>, and2 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def18

      func GFA1CarryICirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA1CarryIStr (x,y,z)) equals ((( 1GateCircuit (x,y, and2c )) +* ( 1GateCircuit (y,z, and2a ))) +* ( 1GateCircuit (z,x, and2 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def19

      func GFA1CarryStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( GFA1CarryIStr (x,y,z)) +* ( 1GateCircStr ( <* [ <*x, y*>, and2c ], [ <*y, z*>, and2a ], [ <*z, x*>, and2 ]*>, or3 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def20

      func GFA1CarryCirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA1CarryStr (x,y,z)) equals (( GFA1CarryICirc (x,y,z)) +* ( 1GateCircuit ( [ <*x, y*>, and2c ], [ <*y, z*>, and2a ], [ <*z, x*>, and2 ], or3 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def21

      func GFA1CarryOutput (x,y,z) -> Element of ( InnerVertices ( GFA1CarryStr (x,y,z))) equals [ <* [ <*x, y*>, and2c ], [ <*y, z*>, and2a ], [ <*z, x*>, and2 ]*>, or3 ];

      coherence

      proof

         [ <* [ <*x, y*>, and2c ], [ <*y, z*>, and2a ], [ <*z, x*>, and2 ]*>, or3 ] in ( InnerVertices ( 1GateCircStr ( <* [ <*x, y*>, and2c ], [ <*y, z*>, and2a ], [ <*z, x*>, and2 ]*>, or3 ))) by FACIRC_1: 47;

        hence thesis by FACIRC_1: 21;

      end;

    end

    theorem :: GFACIRC1:41

    

     Th41: for x,y,z be set holds ( InnerVertices ( GFA1CarryIStr (x,y,z))) = { [ <*x, y*>, and2c ], [ <*y, z*>, and2a ], [ <*z, x*>, and2 ]}

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      

       A1: Cxy tolerates Cyz by CIRCCOMB: 47;

      (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 47;

      

      then ( InnerVertices ( GFA1CarryIStr (x,y,z))) = (( InnerVertices (Cxy +* Cyz)) \/ ( InnerVertices Czx)) by CIRCCOMB: 11

      .= ((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) by A1, CIRCCOMB: 11

      .= (( {xy} \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) by CIRCCOMB: 42

      .= (( {xy} \/ {yz}) \/ ( InnerVertices Czx)) by CIRCCOMB: 42

      .= (( {xy} \/ {yz}) \/ {zx}) by CIRCCOMB: 42

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      hence thesis;

    end;

    theorem :: GFACIRC1:42

    

     Th42: for x,y,z be set holds ( InnerVertices ( GFA1CarryStr (x,y,z))) = ( { [ <*x, y*>, and2c ], [ <*y, z*>, and2a ], [ <*z, x*>, and2 ]} \/ {( GFA1CarryOutput (x,y,z))})

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      

       A1: Cxy tolerates ((Cyz +* Czx) +* Cxyz) by CIRCCOMB: 47;

      Cyz tolerates (Czx +* Cxyz) by CIRCCOMB: 47;

      then

       A2: ( InnerVertices (Cyz +* (Czx +* Cxyz))) = (( InnerVertices Cyz) \/ ( InnerVertices (Czx +* Cxyz))) by CIRCCOMB: 11;

      Czx tolerates Cxyz by CIRCCOMB: 47;

      then

       A3: ( InnerVertices (Czx +* Cxyz)) = (( InnerVertices Czx) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 11;

      

      thus ( InnerVertices ( GFA1CarryStr (x,y,z))) = ( InnerVertices ((Cxy +* (Cyz +* Czx)) +* Cxyz)) by CIRCCOMB: 6

      .= ( InnerVertices (Cxy +* ((Cyz +* Czx) +* Cxyz))) by CIRCCOMB: 6

      .= (( InnerVertices Cxy) \/ ( InnerVertices ((Cyz +* Czx) +* Cxyz))) by A1, CIRCCOMB: 11

      .= (( InnerVertices Cxy) \/ ( InnerVertices (Cyz +* (Czx +* Cxyz)))) by CIRCCOMB: 6

      .= ((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ (( InnerVertices Czx) \/ ( InnerVertices Cxyz))) by A2, A3, XBOOLE_1: 4

      .= (((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by XBOOLE_1: 4

      .= ((( {xy} \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= ((( {xy} \/ {yz}) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= ((( {xy} \/ {yz}) \/ {zx}) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= (( {xy, yz} \/ {zx}) \/ ( InnerVertices Cxyz)) by ENUMSET1: 1

      .= ( {xy, yz, zx} \/ ( InnerVertices Cxyz)) by ENUMSET1: 3

      .= ( {xy, yz, zx} \/ {( GFA1CarryOutput (x,y,z))}) by CIRCCOMB: 42;

    end;

    theorem :: GFACIRC1:43

    

     Th43: for x,y,z be set holds ( InnerVertices ( GFA1CarryStr (x,y,z))) is Relation

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      ( InnerVertices Cxy) is Relation & ( InnerVertices Cyz) is Relation by FACIRC_1: 38;

      then ( InnerVertices Czx) is Relation & ( InnerVertices (Cxy +* Cyz)) is Relation by FACIRC_1: 3, FACIRC_1: 38;

      then ( InnerVertices Cxyz) is Relation & ( InnerVertices ( GFA1CarryIStr (x,y,z))) is Relation by FACIRC_1: 3, FACIRC_1: 38;

      hence thesis by FACIRC_1: 3;

    end;

    theorem :: GFACIRC1:44

    

     Th44: for x,y,z be set st x <> [ <*y, z*>, and2a ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2c ] holds ( InputVertices ( GFA1CarryIStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      assume that

       A1: x <> yz and

       A2: y <> zx & z <> xy;

      

       A3: not xy in {y, z} by A1, A2, Lm1;

      

       A4: not zx in {x, y, z} by A1, A2, Lm1;

      

       A5: y <> yz by FACIRC_2: 2;

      

       A6: ( not z in {xy, yz}) & not x in {xy, yz} by A1, A2, Lm1;

      

       A7: Cxy tolerates Cyz by CIRCCOMB: 47;

      ( InputVertices ( GFA1CarryIStr (x,y,z))) = ((( InputVertices (Cxy +* Cyz)) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ ( InnerVertices (Cxy +* Cyz)))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((((( InputVertices Cxy) \ ( InnerVertices Cyz)) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ ( InnerVertices (Cxy +* Cyz)))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((((( InputVertices Cxy) \ ( InnerVertices Cyz)) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by A7, CIRCCOMB: 11

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by CIRCCOMB: 42

      .= (((( {x, y} \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ {xy, yz})) by ENUMSET1: 1

      .= ((( {x, y} \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ {xy, yz})) by A1, A5, FACIRC_2: 1

      .= ((( {x, y} \/ {y, z}) \ {zx}) \/ ( {z, x} \ {xy, yz})) by A3, ZFMISC_1: 57

      .= ((( {x, y} \/ {y, z}) \ {zx}) \/ {z, x}) by A6, ZFMISC_1: 63

      .= (( {x, y, y, z} \ {zx}) \/ {z, x}) by ENUMSET1: 5

      .= (( {y, y, x, z} \ {zx}) \/ {z, x}) by ENUMSET1: 67

      .= (( {y, x, z} \ {zx}) \/ {z, x}) by ENUMSET1: 31

      .= (( {x, y, z} \ {zx}) \/ {z, x}) by ENUMSET1: 58

      .= ( {x, y, z} \/ {z, x}) by A4, ZFMISC_1: 57

      .= {x, y, z, z, x} by ENUMSET1: 9

      .= ( {x, y, z, z} \/ {x}) by ENUMSET1: 10

      .= ( {z, z, x, y} \/ {x}) by ENUMSET1: 73

      .= ( {z, x, y} \/ {x}) by ENUMSET1: 31

      .= {z, x, y, x} by ENUMSET1: 6

      .= {x, x, y, z} by ENUMSET1: 70

      .= {x, y, z} by ENUMSET1: 31;

      hence thesis;

    end;

    theorem :: GFACIRC1:45

    

     Th45: for x,y,z be set st x <> [ <*y, z*>, and2a ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2c ] holds ( InputVertices ( GFA1CarryStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set MI = ( GFA1CarryIStr (x,y,z));

      

       A1: ( InputVertices S) = ( rng <*xy, yz, zx*>) by CIRCCOMB: 42

      .= {xy, yz, zx} by FINSEQ_2: 128;

      assume

       A2: x <> yz & y <> zx & z <> xy;

      

       A3: ( InnerVertices S) = {xyz} & ( {x, y, z} \ {xyz}) = {x, y, z} by Lm2, CIRCCOMB: 42;

      

       A4: ( {xy, yz, zx} \ {xy, yz, zx}) = {} by XBOOLE_1: 37;

      

      thus ( InputVertices ( GFA1CarryStr (x,y,z))) = ((( InputVertices MI) \ ( InnerVertices S)) \/ (( InputVertices S) \ ( InnerVertices MI))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ( {x, y, z} \/ ( {xy, yz, zx} \ ( InnerVertices MI))) by A1, A2, A3, Th44

      .= ( {x, y, z} \/ {} ) by A4, Th41

      .= {x, y, z};

    end;

    theorem :: GFACIRC1:46

    for x,y,z be non pair set holds ( InputVertices ( GFA1CarryStr (x,y,z))) is without_pairs

    proof

      let x,y,z be non pair set;

      set f1 = and2c , f2 = and2a , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set M = ( GFA1CarryStr (x,y,z));

      set MI = ( GFA1CarryIStr (x,y,z));

      given xx be pair object such that

       A1: xx in ( InputVertices M);

      

       A2: Cxy tolerates Cyz by CIRCCOMB: 47;

      

       A3: ( InnerVertices Czx) = {zx} & (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 42, CIRCCOMB: 47;

      ( InnerVertices Cxy) = {xy} & ( InnerVertices Cyz) = {yz} by CIRCCOMB: 42;

      then ( InnerVertices (Cxy +* Cyz)) = ( {xy} \/ {yz}) by A2, CIRCCOMB: 11;

      

      then

       A4: ( InnerVertices MI) = (( {xy} \/ {yz}) \/ {zx}) by A3, CIRCCOMB: 11

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      ( InputVertices S) = {xy, yz, zx} by FACIRC_1: 42;

      then

       A5: (( InputVertices S) \ ( InnerVertices MI)) = {} by A4, XBOOLE_1: 37;

      ( InputVertices Cxy) is without_pairs & ( InputVertices Cyz) is without_pairs by FACIRC_1: 41;

      then ( InputVertices Czx) is without_pairs & ( InputVertices (Cxy +* Cyz)) is without_pairs by FACIRC_1: 9, FACIRC_1: 41;

      then

       A6: ( InputVertices MI) is without_pairs by FACIRC_1: 9;

      ( InnerVertices S) is Relation by FACIRC_1: 38;

      then ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) by A6, FACIRC_1: 6;

      hence thesis by A6, A1, A5;

    end;

    theorem :: GFACIRC1:47

    

     Th47: for x,y,z be set holds x in the carrier of ( GFA1CarryStr (x,y,z)) & y in the carrier of ( GFA1CarryStr (x,y,z)) & z in the carrier of ( GFA1CarryStr (x,y,z)) & [ <*x, y*>, and2c ] in the carrier of ( GFA1CarryStr (x,y,z)) & [ <*y, z*>, and2a ] in the carrier of ( GFA1CarryStr (x,y,z)) & [ <*z, x*>, and2 ] in the carrier of ( GFA1CarryStr (x,y,z)) & [ <* [ <*x, y*>, and2c ], [ <*y, z*>, and2a ], [ <*z, x*>, and2 ]*>, or3 ] in the carrier of ( GFA1CarryStr (x,y,z))

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set p = <*xy, yz, zx*>;

      z in the carrier of Czx by FACIRC_1: 43;

      then

       A1: z in the carrier of ( GFA1CarryIStr (x,y,z)) by FACIRC_1: 20;

      zx in the carrier of Czx by FACIRC_1: 43;

      then

       A2: zx in the carrier of ( GFA1CarryIStr (x,y,z)) by FACIRC_1: 20;

      y in the carrier of Cxy by FACIRC_1: 43;

      then y in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A3: y in the carrier of ( GFA1CarryIStr (x,y,z)) by FACIRC_1: 20;

      the carrier of Cxyz = (( rng p) \/ {xyz}) & [p, f4] in { [p, f4]} by CIRCCOMB:def 6, TARSKI:def 1;

      then

       A4: xyz in the carrier of Cxyz by XBOOLE_0:def 3;

      yz in the carrier of Cyz by FACIRC_1: 43;

      then yz in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A5: yz in the carrier of ( GFA1CarryIStr (x,y,z)) by FACIRC_1: 20;

      xy in the carrier of Cxy by FACIRC_1: 43;

      then xy in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A6: xy in the carrier of ( GFA1CarryIStr (x,y,z)) by FACIRC_1: 20;

      x in the carrier of Czx by FACIRC_1: 43;

      then x in the carrier of ( GFA1CarryIStr (x,y,z)) by FACIRC_1: 20;

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

    end;

    theorem :: GFACIRC1:48

    

     Th48: for x,y,z be set holds [ <*x, y*>, and2c ] in ( InnerVertices ( GFA1CarryStr (x,y,z))) & [ <*y, z*>, and2a ] in ( InnerVertices ( GFA1CarryStr (x,y,z))) & [ <*z, x*>, and2 ] in ( InnerVertices ( GFA1CarryStr (x,y,z))) & ( GFA1CarryOutput (x,y,z)) in ( InnerVertices ( GFA1CarryStr (x,y,z)))

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      ( InnerVertices ( GFA1CarryStr (x,y,z))) = ( {xy, yz, zx} \/ {( GFA1CarryOutput (x,y,z))}) by Th42

      .= {xy, yz, zx, ( GFA1CarryOutput (x,y,z))} by ENUMSET1: 6;

      hence thesis by ENUMSET1:def 2;

    end;

    theorem :: GFACIRC1:49

    

     Th49: for x,y,z be set st x <> [ <*y, z*>, and2a ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2c ] holds x in ( InputVertices ( GFA1CarryStr (x,y,z))) & y in ( InputVertices ( GFA1CarryStr (x,y,z))) & z in ( InputVertices ( GFA1CarryStr (x,y,z)))

    proof

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      let x,y,z be set;

      assume x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      then ( InputVertices ( GFA1CarryStr (x,y,z))) = {x, y, z} by Th45;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: GFACIRC1:50

    

     Th50: for x,y,z be non pair set holds ( InputVertices ( GFA1CarryStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be non pair set;

      set f1 = and2c , f2 = and2a , f3 = and2 , f4 = or3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set M = ( GFA1CarryStr (x,y,z));

      set MI = ( GFA1CarryIStr (x,y,z));

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      

       A1: ( InputVertices Cxy) = {x, y} & ( InputVertices Cyz) = {y, z} by FACIRC_1: 40;

      

       A2: ( InputVertices Czx) = {z, x} by FACIRC_1: 40;

      

       A3: ( InputVertices S) = {xy, yz, zx} by FACIRC_1: 42;

      

       A4: ( InnerVertices S) is Relation by FACIRC_1: 38;

      

       A5: ( InnerVertices Cxy) = {xy} & ( InnerVertices Cyz) = {yz} by CIRCCOMB: 42;

      Cxy tolerates Cyz by CIRCCOMB: 47;

      then

       A6: ( InnerVertices Czx) = {zx} & ( InnerVertices (Cxy +* Cyz)) = ( {xy} \/ {yz}) by A5, CIRCCOMB: 11, CIRCCOMB: 42;

      (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 47;

      

      then ( InnerVertices MI) = (( {xy} \/ {yz}) \/ {zx}) by A6, CIRCCOMB: 11

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      then

       A7: (( InputVertices S) \ ( InnerVertices MI)) = {} by A3, XBOOLE_1: 37;

      

       A8: ( InputVertices Cxy) is without_pairs & ( InputVertices Cyz) is without_pairs by FACIRC_1: 41;

      then

       A9: ( InputVertices Czx) is without_pairs & ( InputVertices (Cxy +* Cyz)) is without_pairs by FACIRC_1: 9, FACIRC_1: 41;

      then ( InputVertices MI) is without_pairs by FACIRC_1: 9;

      then ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) by A4, FACIRC_1: 6;

      

      hence ( InputVertices M) = (( InputVertices (Cxy +* Cyz)) \/ ( InputVertices Czx)) by A9, A6, A7, FACIRC_1: 7

      .= ((( InputVertices Cxy) \/ ( InputVertices Cyz)) \/ ( InputVertices Czx)) by A8, A5, FACIRC_1: 7

      .= ( {x, y, y, z} \/ {z, x}) by A1, A2, ENUMSET1: 5

      .= ( {y, y, x, z} \/ {z, x}) by ENUMSET1: 67

      .= ( {y, x, z} \/ {z, x}) by ENUMSET1: 31

      .= ( {x, y, z} \/ {z, x}) by ENUMSET1: 58

      .= ( {x, y, z} \/ ( {z} \/ {x})) by ENUMSET1: 1

      .= (( {x, y, z} \/ {z}) \/ {x}) by XBOOLE_1: 4

      .= (( {z, x, y} \/ {z}) \/ {x}) by ENUMSET1: 59

      .= ( {z, z, x, y} \/ {x}) by ENUMSET1: 4

      .= ( {z, x, y} \/ {x}) by ENUMSET1: 31

      .= ( {x, y, z} \/ {x}) by ENUMSET1: 59

      .= {x, x, y, z} by ENUMSET1: 4

      .= {x, y, z} by ENUMSET1: 31;

    end;

    theorem :: GFACIRC1:51

    

     Th51: for x,y,z be set holds for s be State of ( GFA1CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following s) . [ <*x, y*>, and2c ]) = (a1 '&' ( 'not' a2)) & (( Following s) . [ <*y, z*>, and2a ]) = (( 'not' a2) '&' a3) & (( Following s) . [ <*z, x*>, and2 ]) = (a3 '&' a1)

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      let s be State of ( GFA1CarryCirc (x,y,z));

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

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

       A1: a1 = (s . x) and

       A2: a2 = (s . y) and

       A3: a3 = (s . z);

      set S = ( GFA1CarryStr (x,y,z));

      

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

      

       A5: y in the carrier of S by Th47;

      

       A6: x in the carrier of S by Th47;

      

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

      xy in ( InnerVertices ( GFA1CarryStr (x,y,z))) by Th48;

      

      hence (( Following s) . [ <*x, y*>, f1]) = (f1 . (s * <*x, y*>)) by A4, FACIRC_1: 35

      .= (f1 . <*a1, a2*>) by A1, A2, A7, A6, A5, FINSEQ_2: 125

      .= (a1 '&' ( 'not' a2)) by Def3;

      

       A8: z in the carrier of S by Th47;

      yz in ( InnerVertices ( GFA1CarryStr (x,y,z))) by Th48;

      

      hence (( Following s) . [ <*y, z*>, f2]) = (f2 . (s * <*y, z*>)) by A4, FACIRC_1: 35

      .= (f2 . <*a2, a3*>) by A2, A3, A7, A5, A8, FINSEQ_2: 125

      .= (( 'not' a2) '&' a3) by TWOSCOMP:def 2;

      zx in ( InnerVertices ( GFA1CarryStr (x,y,z))) by Th48;

      

      hence (( Following s) . [ <*z, x*>, f3]) = (f3 . (s * <*z, x*>)) by A4, FACIRC_1: 35

      .= (f3 . <*a3, a1*>) by A1, A3, A7, A6, A8, FINSEQ_2: 125

      .= (a3 '&' a1) by FACIRC_1:def 6;

    end;

    theorem :: GFACIRC1:52

    

     Th52: for x,y,z be set holds for s be State of ( GFA1CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . [ <*x, y*>, and2c ]) & a2 = (s . [ <*y, z*>, and2a ]) & a3 = (s . [ <*z, x*>, and2 ]) holds (( Following s) . ( GFA1CarryOutput (x,y,z))) = ((a1 'or' a2) 'or' a3)

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 , f4 = or3 ;

      let s be State of ( GFA1CarryCirc (x,y,z));

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

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

       A1: a1 = (s . xy) & a2 = (s . yz) & a3 = (s . zx);

      set S = ( GFA1CarryStr (x,y,z));

      reconsider xy, yz, zx as Element of ( InnerVertices S) by Th48;

      

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

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

      

      hence (( Following s) . ( GFA1CarryOutput (x,y,z))) = (f4 . (s * <*xy, yz, zx*>)) by FACIRC_1: 35

      .= (f4 . <*a1, a2, a3*>) by A1, A2, FINSEQ_2: 126

      .= ((a1 'or' a2) 'or' a3) by TWOSCOMP: 14;

    end;

    theorem :: GFACIRC1:53

    

     Th53: for x,y,z be set st x <> [ <*y, z*>, and2a ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2c ] holds for s be State of ( GFA1CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA1CarryOutput (x,y,z))) = (((a1 '&' ( 'not' a2)) 'or' (( 'not' a2) '&' a3)) 'or' (a3 '&' a1)) & (( Following (s,2)) . [ <*x, y*>, and2c ]) = (a1 '&' ( 'not' a2)) & (( Following (s,2)) . [ <*y, z*>, and2a ]) = (( 'not' a2) '&' a3) & (( Following (s,2)) . [ <*z, x*>, and2 ]) = (a3 '&' a1)

    proof

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      let x,y,z be set such that

       A1: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( GFA1CarryStr (x,y,z));

      reconsider x9 = x, y9 = y, z9 = z as Vertex of S by Th47;

      let s be State of ( GFA1CarryCirc (x,y,z));

      y in ( InputVertices S) by A1, Th49;

      then

       A2: (( Following s) . y9) = (s . y) by CIRCUIT2:def 5;

      z in ( InputVertices S) by A1, Th49;

      then

       A3: (( Following s) . z9) = (s . z) by CIRCUIT2:def 5;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      

       A4: ( Following (s,2)) = ( Following ( Following s)) by FACIRC_1: 15;

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

       A5: a1 = (s . x) & a2 = (s . y) & a3 = (s . z);

      

       A6: (( Following s) . zx) = (a3 '&' a1) by A5, Th51;

      (( Following s) . xy) = (a1 '&' ( 'not' a2)) & (( Following s) . yz) = (( 'not' a2) '&' a3) by A5, Th51;

      hence (( Following (s,2)) . ( GFA1CarryOutput (x,y,z))) = (((a1 '&' ( 'not' a2)) 'or' (( 'not' a2) '&' a3)) 'or' (a3 '&' a1)) by A4, A6, Th52;

      x in ( InputVertices S) by A1, Th49;

      then (( Following s) . x9) = (s . x) by CIRCUIT2:def 5;

      hence thesis by A5, A2, A3, A4, Th51;

    end;

    theorem :: GFACIRC1:54

    

     Th54: for x,y,z be set st x <> [ <*y, z*>, and2a ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2c ] holds for s be State of ( GFA1CarryCirc (x,y,z)) holds ( Following (s,2)) is stable

    proof

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      let x,y,z be set such that

       A1: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( GFA1CarryStr (x,y,z));

      reconsider xx = x, yy = y, zz = z as Vertex of S by Th47;

      let s be State of ( GFA1CarryCirc (x,y,z));

      set a1 = (s . xx), a2 = (s . yy), a3 = (s . zz);

      set ffs = ( Following (s,2)), fffs = ( Following ffs);

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      

       A2: ffs = ( Following ( Following s)) by FACIRC_1: 15;

      

       A3: z in ( InputVertices S) by A1, Th49;

      then (( Following s) . z) = a3 by CIRCUIT2:def 5;

      then

       A4: (ffs . z) = a3 by A2, A3, CIRCUIT2:def 5;

      

       A5: y in ( InputVertices S) by A1, Th49;

      then (( Following s) . y) = a2 by CIRCUIT2:def 5;

      then

       A6: (ffs . y) = a2 by A2, A5, CIRCUIT2:def 5;

      

       A7: x in ( InputVertices S) by A1, Th49;

      then (( Following s) . x) = a1 by CIRCUIT2:def 5;

      then

       A8: (ffs . x) = a1 by A2, A7, CIRCUIT2:def 5;

      a3 = (s . z);

      then

       A9: (ffs . xy) = (a1 '&' ( 'not' a2)) by A1, Th53;

      a2 = (s . y);

      then

       A10: (ffs . zx) = (a1 '&' a3) by A1, Th53;

      a1 = (s . x);

      then

       A11: (ffs . yz) = (( 'not' a2) '&' a3) by A1, Th53;

      

       A12: (ffs . ( GFA1CarryOutput (x,y,z))) = (((a1 '&' ( 'not' a2)) 'or' (( 'not' a2) '&' a3)) 'or' (a3 '&' a1)) by A1, Th53;

       A13:

      now

        let a be object;

        assume

         A14: a in the carrier of S;

        then

        reconsider v = a as Vertex of S;

        

         A15: v in (( InputVertices S) \/ ( InnerVertices S)) by A14, XBOOLE_1: 45;

        thus (ffs . a) = (fffs . a)

        proof

          per cases by A15, XBOOLE_0:def 3;

            suppose v in ( InputVertices S);

            hence thesis by CIRCUIT2:def 5;

          end;

            suppose v in ( InnerVertices S);

            then v in ( {xy, yz, zx} \/ {( GFA1CarryOutput (x,y,z))}) by Th42;

            then v in {xy, yz, zx} or v in {( GFA1CarryOutput (x,y,z))} by XBOOLE_0:def 3;

            then v = xy or v = yz or v = zx or v = ( GFA1CarryOutput (x,y,z)) by ENUMSET1:def 1, TARSKI:def 1;

            hence thesis by A12, A9, A11, A10, A8, A6, A4, Th51, Th52;

          end;

        end;

      end;

      ( dom ( Following ( Following (s,2)))) = the carrier of S & ( dom ( Following (s,2))) = the carrier of S by CIRCUIT1: 3;

      hence ffs = fffs by A13, FUNCT_1: 2;

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def22

      func GFA1AdderStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ( 2GatesCircStr (x,y,z, xor2c ));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def23

      func GFA1AdderCirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA1AdderStr (x,y,z)) equals ( 2GatesCircuit (x,y,z, xor2c ));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def24

      func GFA1AdderOutput (x,y,z) -> Element of ( InnerVertices ( GFA1AdderStr (x,y,z))) equals ( 2GatesCircOutput (x,y,z, xor2c ));

      coherence ;

    end

    theorem :: GFACIRC1:55

    

     Th55: for x,y,z be set holds ( InnerVertices ( GFA1AdderStr (x,y,z))) = ( { [ <*x, y*>, xor2c ]} \/ {( GFA1AdderOutput (x,y,z))})

    proof

      let x,y,z be set;

      set f = xor2c ;

      set xy = [ <*x, y*>, f];

      set S = ( GFA1AdderStr (x,y,z));

      

      thus ( InnerVertices S) = {xy, ( GFA1AdderOutput (x,y,z))} by FACIRC_1: 56

      .= ( {xy} \/ {( GFA1AdderOutput (x,y,z))}) by ENUMSET1: 1;

    end;

    theorem :: GFACIRC1:56

    for x,y,z be set holds x in the carrier of ( GFA1AdderStr (x,y,z)) & y in the carrier of ( GFA1AdderStr (x,y,z)) & z in the carrier of ( GFA1AdderStr (x,y,z)) & [ <*x, y*>, xor2c ] in the carrier of ( GFA1AdderStr (x,y,z)) & [ <* [ <*x, y*>, xor2c ], z*>, xor2c ] in the carrier of ( GFA1AdderStr (x,y,z)) by FACIRC_1: 60, FACIRC_1: 61;

    theorem :: GFACIRC1:57

    

     Th57: for x,y,z be set holds [ <*x, y*>, xor2c ] in ( InnerVertices ( GFA1AdderStr (x,y,z))) & ( GFA1AdderOutput (x,y,z)) in ( InnerVertices ( GFA1AdderStr (x,y,z)))

    proof

      let x,y,z be set;

      set f = xor2c ;

      set S = ( GFA1AdderStr (x,y,z));

      ( InnerVertices S) = ( { [ <*x, y*>, f]} \/ {( GFA1AdderOutput (x,y,z))}) by Th55

      .= { [ <*x, y*>, f], ( GFA1AdderOutput (x,y,z))} by ENUMSET1: 1;

      hence thesis by TARSKI:def 2;

    end;

    theorem :: GFACIRC1:58

    

     Th58: for x,y,z be set st z <> [ <*x, y*>, xor2c ] holds x in ( InputVertices ( GFA1AdderStr (x,y,z))) & y in ( InputVertices ( GFA1AdderStr (x,y,z))) & z in ( InputVertices ( GFA1AdderStr (x,y,z)))

    proof

      set f = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set S = ( GFA1AdderStr (x,y,z));

      ( InputVertices S) = {x, y, z} by A1, FACIRC_1: 57;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: GFACIRC1:59

    

     Th59: for x,y,z be set st z <> [ <*x, y*>, xor2c ] holds for s be State of ( GFA1AdderCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following s) . [ <*x, y*>, xor2c ]) = (a1 'xor' ( 'not' a2)) & (( Following s) . x) = a1 & (( Following s) . y) = a2 & (( Following s) . z) = a3

    proof

      set f = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set A = ( GFA1AdderCirc (x,y,z));

      set xy = [ <*x, y*>, f];

      let s be State of A;

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

       A2: a1 = (s . x) & a2 = (s . y) and

       A3: a3 = (s . z);

      (( Following s) . xy) = (f . <*a1, a2*>) by A1, A2, Lm3;

      hence (( Following s) . xy) = (a1 'xor' ( 'not' a2)) by Def4;

      thus thesis by A1, A2, A3, Lm3;

    end;

    theorem :: GFACIRC1:60

    

     Th60: for x,y,z be set st z <> [ <*x, y*>, xor2c ] holds for s be State of ( GFA1AdderCirc (x,y,z)) holds for a1a2,a1,a2,a3 be Element of BOOLEAN st a1a2 = (s . [ <*x, y*>, xor2c ]) & a3 = (s . z) holds (( Following s) . ( GFA1AdderOutput (x,y,z))) = (a1a2 'xor' ( 'not' a3))

    proof

      set f = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set A = ( GFA1AdderCirc (x,y,z));

      set xy = [ <*x, y*>, f];

      let s be State of A;

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

       A2: a1a2 = (s . xy) & a3 = (s . z);

      

      thus (( Following s) . ( GFA1AdderOutput (x,y,z))) = (f . <*(s . xy), (s . z)*>) by A1, Lm3

      .= (a1a2 'xor' ( 'not' a3)) by A2, Def4;

    end;

    theorem :: GFACIRC1:61

    

     Th61: for x,y,z be set st z <> [ <*x, y*>, xor2c ] holds for s be State of ( GFA1AdderCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA1AdderOutput (x,y,z))) = ((a1 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) & (( Following (s,2)) . [ <*x, y*>, xor2c ]) = (a1 'xor' ( 'not' a2)) & (( Following (s,2)) . x) = a1 & (( Following (s,2)) . y) = a2 & (( Following (s,2)) . z) = a3

    proof

      set f = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set xy = [ <*x, y*>, f];

      set A = ( GFA1AdderCirc (x,y,z));

      let s be State of A;

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

       A2: a1 = (s . x) & a2 = (s . y) and

       A3: a3 = (s . z);

      

      thus (( Following (s,2)) . ( GFA1AdderOutput (x,y,z))) = (f . <*(f . <*a1, a2*>), a3*>) by A1, A2, A3, FACIRC_1: 62

      .= (f . <*(a1 'xor' ( 'not' a2)), a3*>) by Def4

      .= ((a1 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) by Def4;

      (( Following (s,2)) . xy) = (f . <*a1, a2*>) by A1, A2, FACIRC_1: 62;

      hence (( Following (s,2)) . xy) = (a1 'xor' ( 'not' a2)) by Def4;

      thus thesis by A1, A2, A3, FACIRC_1: 62;

    end;

    theorem :: GFACIRC1:62

    

     Th62: for x,y,z be set st z <> [ <*x, y*>, xor2c ] holds for s be State of ( GFA1AdderCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA1AdderOutput (x,y,z))) = ( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3))

    proof

      set f = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set A = ( GFA1AdderCirc (x,y,z));

      let s be State of A;

      let a1,a2,a3 be Element of BOOLEAN ;

      assume a1 = (s . x) & a2 = (s . y) & a3 = (s . z);

      

      hence (( Following (s,2)) . ( GFA1AdderOutput (x,y,z))) = ((a1 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) by A1, Th61

      .= ( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3)) by XBOOLEAN: 74;

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def25

      func BitGFA1Str (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( GFA1AdderStr (x,y,z)) +* ( GFA1CarryStr (x,y,z)));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def26

      func BitGFA1Circ (x,y,z) -> strict Boolean gate`2=den Circuit of ( BitGFA1Str (x,y,z)) equals (( GFA1AdderCirc (x,y,z)) +* ( GFA1CarryCirc (x,y,z)));

      coherence ;

    end

    theorem :: GFACIRC1:63

    

     Th63: for x,y,z be set holds ( InnerVertices ( BitGFA1Str (x,y,z))) = ((( { [ <*x, y*>, xor2c ]} \/ {( GFA1AdderOutput (x,y,z))}) \/ { [ <*x, y*>, and2c ], [ <*y, z*>, and2a ], [ <*z, x*>, and2 ]}) \/ {( GFA1CarryOutput (x,y,z))})

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      set f0 = xor2c ;

      set xyf0 = [ <*x, y*>, f0];

      set xyf1 = [ <*x, y*>, f1], yzf2 = [ <*y, z*>, f2], zxf3 = [ <*z, x*>, f3];

      set S = ( BitGFA1Str (x,y,z));

      set S1 = ( GFA1AdderStr (x,y,z));

      set S2 = ( GFA1CarryStr (x,y,z));

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

      set A2 = ( GFA1CarryOutput (x,y,z));

      

      thus ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by FACIRC_1: 27

      .= (( {xyf0} \/ {A1}) \/ ( InnerVertices S2)) by Th55

      .= (( {xyf0} \/ {A1}) \/ ( {xyf1, yzf2, zxf3} \/ {A2})) by Th42

      .= ((( {xyf0} \/ {A1}) \/ {xyf1, yzf2, zxf3}) \/ {A2}) by XBOOLE_1: 4;

    end;

    theorem :: GFACIRC1:64

    for x,y,z be set holds ( InnerVertices ( BitGFA1Str (x,y,z))) is Relation

    proof

      let x,y,z be set;

      set S1 = ( GFA1AdderStr (x,y,z));

      set S2 = ( GFA1CarryStr (x,y,z));

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by Th43, FACIRC_1: 58;

      hence thesis by FACIRC_1: 3;

    end;

    theorem :: GFACIRC1:65

    

     Th65: for x,y,z be set st z <> [ <*x, y*>, xor2c ] & x <> [ <*y, z*>, and2a ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2c ] holds ( InputVertices ( BitGFA1Str (x,y,z))) = {x, y, z}

    proof

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      set f0 = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] & x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S2 = ( GFA1CarryStr (x,y,z));

      set S1 = ( GFA1AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} & ( InputVertices S2) = {x, y, z} by A1, Th45, FACIRC_1: 57;

      hence thesis by CIRCCOMB: 47, FACIRC_2: 21;

    end;

    theorem :: GFACIRC1:66

    

     Th66: for x,y,z be non pair set holds ( InputVertices ( BitGFA1Str (x,y,z))) = {x, y, z}

    proof

      let x,y,z be non pair set;

      set S = ( BitGFA1Str (x,y,z));

      set S1 = ( GFA1AdderStr (x,y,z));

      set S2 = ( GFA1CarryStr (x,y,z));

      

       A1: ( InputVertices S1) = {x, y, z} & ( InputVertices S2) = {x, y, z} by Th50, FACIRC_1: 57;

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by Th43, FACIRC_1: 58;

      

      hence ( InputVertices S) = ( {x, y, z} \/ {x, y, z}) by A1, FACIRC_1: 7

      .= {x, y, z};

    end;

    theorem :: GFACIRC1:67

    for x,y,z be non pair set holds ( InputVertices ( BitGFA1Str (x,y,z))) is without_pairs

    proof

      let x,y,z be non pair set;

      ( InputVertices ( BitGFA1Str (x,y,z))) = {x, y, z} by Th66;

      hence thesis;

    end;

    theorem :: GFACIRC1:68

    for x,y,z be set holds x in the carrier of ( BitGFA1Str (x,y,z)) & y in the carrier of ( BitGFA1Str (x,y,z)) & z in the carrier of ( BitGFA1Str (x,y,z)) & [ <*x, y*>, xor2c ] in the carrier of ( BitGFA1Str (x,y,z)) & [ <* [ <*x, y*>, xor2c ], z*>, xor2c ] in the carrier of ( BitGFA1Str (x,y,z)) & [ <*x, y*>, and2c ] in the carrier of ( BitGFA1Str (x,y,z)) & [ <*y, z*>, and2a ] in the carrier of ( BitGFA1Str (x,y,z)) & [ <*z, x*>, and2 ] in the carrier of ( BitGFA1Str (x,y,z)) & [ <* [ <*x, y*>, and2c ], [ <*y, z*>, and2a ], [ <*z, x*>, and2 ]*>, or3 ] in the carrier of ( BitGFA1Str (x,y,z))

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 , f4 = or3 ;

      set f0 = xor2c ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set S1 = ( GFA1AdderStr (x,y,z));

      set S2 = ( GFA1CarryStr (x,y,z));

      

       A1: x in the carrier of S1 & y in the carrier of S1 by FACIRC_1: 60;

      

       A2: z in the carrier of S1 & [ <*x, y*>, f0] in the carrier of S1 by FACIRC_1: 60, FACIRC_1: 61;

      

       A3: xyz in the carrier of S2 by Th47;

      

       A4: yz in the carrier of S2 & zx in the carrier of S2 by Th47;

       [ <* [ <*x, y*>, f0], z*>, f0] in the carrier of S1 & xy in the carrier of S2 by Th47, FACIRC_1: 61;

      hence thesis by A1, A2, A4, A3, FACIRC_1: 20;

    end;

    theorem :: GFACIRC1:69

    

     Th69: for x,y,z be set holds [ <*x, y*>, xor2c ] in ( InnerVertices ( BitGFA1Str (x,y,z))) & ( GFA1AdderOutput (x,y,z)) in ( InnerVertices ( BitGFA1Str (x,y,z))) & [ <*x, y*>, and2c ] in ( InnerVertices ( BitGFA1Str (x,y,z))) & [ <*y, z*>, and2a ] in ( InnerVertices ( BitGFA1Str (x,y,z))) & [ <*z, x*>, and2 ] in ( InnerVertices ( BitGFA1Str (x,y,z))) & ( GFA1CarryOutput (x,y,z)) in ( InnerVertices ( BitGFA1Str (x,y,z)))

    proof

      let x,y,z be set;

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      set f0 = xor2c ;

      set xyf0 = [ <*x, y*>, f0];

      set xyf1 = [ <*x, y*>, f1], yzf2 = [ <*y, z*>, f2], zxf3 = [ <*z, x*>, f3];

      set S = ( BitGFA1Str (x,y,z));

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

      set A2 = ( GFA1CarryOutput (x,y,z));

      ( InnerVertices S) = ((( {xyf0} \/ {A1}) \/ {xyf1, yzf2, zxf3}) \/ {A2}) by Th63

      .= (( {xyf0, A1} \/ {xyf1, yzf2, zxf3}) \/ {A2}) by ENUMSET1: 1

      .= ( {xyf0, A1, xyf1, yzf2, zxf3} \/ {A2}) by ENUMSET1: 8

      .= {xyf0, A1, xyf1, yzf2, zxf3, A2} by ENUMSET1: 15;

      hence thesis by ENUMSET1:def 4;

    end;

    theorem :: GFACIRC1:70

    for x,y,z be set st z <> [ <*x, y*>, xor2c ] & x <> [ <*y, z*>, and2a ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2c ] holds x in ( InputVertices ( BitGFA1Str (x,y,z))) & y in ( InputVertices ( BitGFA1Str (x,y,z))) & z in ( InputVertices ( BitGFA1Str (x,y,z)))

    proof

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      set f0 = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] & x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( BitGFA1Str (x,y,z));

      ( InputVertices S) = {x, y, z} by A1, Th65;

      hence thesis by ENUMSET1:def 1;

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def27

      func BitGFA1CarryOutput (x,y,z) -> Element of ( InnerVertices ( BitGFA1Str (x,y,z))) equals [ <* [ <*x, y*>, and2c ], [ <*y, z*>, and2a ], [ <*z, x*>, and2 ]*>, or3 ];

      coherence

      proof

        ( GFA1CarryOutput (x,y,z)) in ( InnerVertices ( BitGFA1Str (x,y,z))) by Th69;

        hence thesis;

      end;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def28

      func BitGFA1AdderOutput (x,y,z) -> Element of ( InnerVertices ( BitGFA1Str (x,y,z))) equals ( 2GatesCircOutput (x,y,z, xor2c ));

      coherence

      proof

        ( GFA1AdderOutput (x,y,z)) in ( InnerVertices ( BitGFA1Str (x,y,z))) by Th69;

        hence thesis;

      end;

    end

    theorem :: GFACIRC1:71

    for x,y,z be set st z <> [ <*x, y*>, xor2c ] & x <> [ <*y, z*>, and2a ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2c ] holds for s be State of ( BitGFA1Circ (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA1AdderOutput (x,y,z))) = ( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3)) & (( Following (s,2)) . ( GFA1CarryOutput (x,y,z))) = (((a1 '&' ( 'not' a2)) 'or' (( 'not' a2) '&' a3)) 'or' (a3 '&' a1))

    proof

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      set f0 = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] and

       A2: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S2 = ( GFA1CarryStr (x,y,z));

      set S1 = ( GFA1AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} by A1, FACIRC_1: 57;

      then

       A3: ( InputVertices S1) = ( InputVertices S2) by A2, Th45;

      set A2 = ( GFA1CarryCirc (x,y,z));

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

      set A = ( BitGFA1Circ (x,y,z));

      let s be State of A;

      let a1,a2,a3 be Element of BOOLEAN ;

      assume that

       A4: a1 = (s . x) and

       A5: a2 = (s . y) and

       A6: a3 = (s . z);

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

      

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

      z in the carrier of S1 by FACIRC_1: 60;

      then

       A8: a3 = (s1 . z) by A6, A7, FUNCT_1: 47;

      y in the carrier of S1 by FACIRC_1: 60;

      then

       A9: a2 = (s1 . y) by A5, A7, FUNCT_1: 47;

      reconsider t = s as State of (A1 +* A2);

      ( InnerVertices S2) misses ( InputVertices S2) by XBOOLE_1: 79;

      then

       A10: (( Following (t,2)) . ( GFA1AdderOutput (x,y,z))) = (( Following (s1,2)) . ( GFA1AdderOutput (x,y,z))) by A3, FACIRC_1: 32;

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      

       A11: ( dom s2) = the carrier of S2 by CIRCUIT1: 3;

      x in the carrier of S1 by FACIRC_1: 60;

      then a1 = (s1 . x) by A4, A7, FUNCT_1: 47;

      hence (( Following (s,2)) . ( GFA1AdderOutput (x,y,z))) = ( 'not' ((a1 'xor' ( 'not' a2)) 'xor' a3)) by A1, A9, A8, A10, Th62;

      ( InnerVertices S1) misses ( InputVertices S1) by XBOOLE_1: 79;

      then

       A12: (( Following (t,2)) . ( GFA1CarryOutput (x,y,z))) = (( Following (s2,2)) . ( GFA1CarryOutput (x,y,z))) by A3, FACIRC_1: 33;

      z in the carrier of S2 by Th47;

      then

       A13: a3 = (s2 . z) by A6, A11, FUNCT_1: 47;

      y in the carrier of S2 by Th47;

      then

       A14: a2 = (s2 . y) by A5, A11, FUNCT_1: 47;

      x in the carrier of S2 by Th47;

      then a1 = (s2 . x) by A4, A11, FUNCT_1: 47;

      hence thesis by A2, A14, A13, A12, Th53;

    end;

    theorem :: GFACIRC1:72

    for x,y,z be set st z <> [ <*x, y*>, xor2c ] & x <> [ <*y, z*>, and2a ] & y <> [ <*z, x*>, and2 ] & z <> [ <*x, y*>, and2c ] holds for s be State of ( BitGFA1Circ (x,y,z)) holds ( Following (s,2)) is stable

    proof

      set f1 = and2c , f2 = and2a , f3 = and2 ;

      set f0 = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] and

       A2: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set A = ( BitGFA1Circ (x,y,z));

      let s be State of A;

      set S2 = ( GFA1CarryStr (x,y,z));

      set S1 = ( GFA1AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} by A1, FACIRC_1: 57;

      then

       A3: ( InputVertices S1) = ( InputVertices S2) by A2, Th45;

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

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

      ( Following (s1,2)) is stable by A1, FACIRC_1: 63;

      

      then

       A4: ( Following (s1,2)) = ( Following ( Following (s1,2)))

      .= ( Following (s1,(2 + 1))) by FACIRC_1: 12;

      set A2 = ( GFA1CarryCirc (x,y,z));

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      ( Following (s2,2)) is stable by A2, Th54;

      

      then

       A5: ( Following (s2,2)) = ( Following ( Following (s2,2)))

      .= ( Following (s2,(2 + 1))) by FACIRC_1: 12;

      reconsider t = s as State of (A1 +* A2);

      set S = ( BitGFA1Str (x,y,z));

      

       A6: ( dom ( Following (s,3))) = the carrier of S by CIRCUIT1: 3;

      ( InnerVertices S2) misses ( InputVertices S2) by XBOOLE_1: 79;

      then

       A7: ( Following (s1,2)) = (( Following (t,2)) | the carrier of S1) & ( Following (s1,3)) = (( Following (t,3)) | the carrier of S1) by A3, FACIRC_1: 30;

      ( InnerVertices S1) misses ( InputVertices S1) by XBOOLE_1: 79;

      then

       A8: ( Following (s2,2)) = (( Following (t,2)) | the carrier of S2) & ( Following (s2,3)) = (( Following (t,3)) | the carrier of S2) by A3, FACIRC_1: 31;

      

       A9: the carrier of S = (the carrier of S1 \/ the carrier of S2) by CIRCCOMB:def 2;

      

       A10: ( dom ( Following (s1,2))) = the carrier of S1 & ( dom ( Following (s2,2))) = the carrier of S2 by CIRCUIT1: 3;

       A11:

      now

        let a be object;

        assume a in the carrier of S;

        then a in the carrier of S1 or a in the carrier of S2 by A9, XBOOLE_0:def 3;

        then (( Following (s,2)) . a) = (( Following (s1,2)) . a) & (( Following (s,3)) . a) = (( Following (s1,3)) . a) or (( Following (s,2)) . a) = (( Following (s2,2)) . a) & (( Following (s,3)) . a) = (( Following (s2,3)) . a) by A7, A8, A4, A5, A10, FUNCT_1: 47;

        hence (( Following (s,2)) . a) = (( Following ( Following (s,2))) . a) by A4, A5, FACIRC_1: 12;

      end;

      ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) & ( dom ( Following (s,2))) = the carrier of S by CIRCUIT1: 3, FACIRC_1: 12;

      hence ( Following (s,2)) = ( Following ( Following (s,2))) by A6, A11, FUNCT_1: 2;

    end;

    begin

    definition

      let x,y,z be set;

      :: GFACIRC1:def29

      func GFA2CarryIStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ((( 1GateCircStr ( <*x, y*>, and2a )) +* ( 1GateCircStr ( <*y, z*>, and2c ))) +* ( 1GateCircStr ( <*z, x*>, nor2 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def30

      func GFA2CarryICirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA2CarryIStr (x,y,z)) equals ((( 1GateCircuit (x,y, and2a )) +* ( 1GateCircuit (y,z, and2c ))) +* ( 1GateCircuit (z,x, nor2 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def31

      func GFA2CarryStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( GFA2CarryIStr (x,y,z)) +* ( 1GateCircStr ( <* [ <*x, y*>, and2a ], [ <*y, z*>, and2c ], [ <*z, x*>, nor2 ]*>, nor3 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def32

      func GFA2CarryCirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA2CarryStr (x,y,z)) equals (( GFA2CarryICirc (x,y,z)) +* ( 1GateCircuit ( [ <*x, y*>, and2a ], [ <*y, z*>, and2c ], [ <*z, x*>, nor2 ], nor3 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def33

      func GFA2CarryOutput (x,y,z) -> Element of ( InnerVertices ( GFA2CarryStr (x,y,z))) equals [ <* [ <*x, y*>, and2a ], [ <*y, z*>, and2c ], [ <*z, x*>, nor2 ]*>, nor3 ];

      coherence

      proof

         [ <* [ <*x, y*>, and2a ], [ <*y, z*>, and2c ], [ <*z, x*>, nor2 ]*>, nor3 ] in ( InnerVertices ( 1GateCircStr ( <* [ <*x, y*>, and2a ], [ <*y, z*>, and2c ], [ <*z, x*>, nor2 ]*>, nor3 ))) by FACIRC_1: 47;

        hence thesis by FACIRC_1: 21;

      end;

    end

    theorem :: GFACIRC1:73

    

     Th73: for x,y,z be set holds ( InnerVertices ( GFA2CarryIStr (x,y,z))) = { [ <*x, y*>, and2a ], [ <*y, z*>, and2c ], [ <*z, x*>, nor2 ]}

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      

       A1: Cxy tolerates Cyz by CIRCCOMB: 47;

      (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 47;

      

      then ( InnerVertices ( GFA2CarryIStr (x,y,z))) = (( InnerVertices (Cxy +* Cyz)) \/ ( InnerVertices Czx)) by CIRCCOMB: 11

      .= ((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) by A1, CIRCCOMB: 11

      .= (( {xy} \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) by CIRCCOMB: 42

      .= (( {xy} \/ {yz}) \/ ( InnerVertices Czx)) by CIRCCOMB: 42

      .= (( {xy} \/ {yz}) \/ {zx}) by CIRCCOMB: 42

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      hence thesis;

    end;

    theorem :: GFACIRC1:74

    

     Th74: for x,y,z be set holds ( InnerVertices ( GFA2CarryStr (x,y,z))) = ( { [ <*x, y*>, and2a ], [ <*y, z*>, and2c ], [ <*z, x*>, nor2 ]} \/ {( GFA2CarryOutput (x,y,z))})

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      

       A1: Cxy tolerates ((Cyz +* Czx) +* Cxyz) by CIRCCOMB: 47;

      Cyz tolerates (Czx +* Cxyz) by CIRCCOMB: 47;

      then

       A2: ( InnerVertices (Cyz +* (Czx +* Cxyz))) = (( InnerVertices Cyz) \/ ( InnerVertices (Czx +* Cxyz))) by CIRCCOMB: 11;

      Czx tolerates Cxyz by CIRCCOMB: 47;

      then

       A3: ( InnerVertices (Czx +* Cxyz)) = (( InnerVertices Czx) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 11;

      

      thus ( InnerVertices ( GFA2CarryStr (x,y,z))) = ( InnerVertices ((Cxy +* (Cyz +* Czx)) +* Cxyz)) by CIRCCOMB: 6

      .= ( InnerVertices (Cxy +* ((Cyz +* Czx) +* Cxyz))) by CIRCCOMB: 6

      .= (( InnerVertices Cxy) \/ ( InnerVertices ((Cyz +* Czx) +* Cxyz))) by A1, CIRCCOMB: 11

      .= (( InnerVertices Cxy) \/ ( InnerVertices (Cyz +* (Czx +* Cxyz)))) by CIRCCOMB: 6

      .= ((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ (( InnerVertices Czx) \/ ( InnerVertices Cxyz))) by A2, A3, XBOOLE_1: 4

      .= (((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by XBOOLE_1: 4

      .= ((( {xy} \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= ((( {xy} \/ {yz}) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= ((( {xy} \/ {yz}) \/ {zx}) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= (( {xy, yz} \/ {zx}) \/ ( InnerVertices Cxyz)) by ENUMSET1: 1

      .= ( {xy, yz, zx} \/ ( InnerVertices Cxyz)) by ENUMSET1: 3

      .= ( {xy, yz, zx} \/ {( GFA2CarryOutput (x,y,z))}) by CIRCCOMB: 42;

    end;

    theorem :: GFACIRC1:75

    

     Th75: for x,y,z be set holds ( InnerVertices ( GFA2CarryStr (x,y,z))) is Relation

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      ( InnerVertices Cxy) is Relation & ( InnerVertices Cyz) is Relation by FACIRC_1: 38;

      then ( InnerVertices Czx) is Relation & ( InnerVertices (Cxy +* Cyz)) is Relation by FACIRC_1: 3, FACIRC_1: 38;

      then ( InnerVertices Cxyz) is Relation & ( InnerVertices ( GFA2CarryIStr (x,y,z))) is Relation by FACIRC_1: 3, FACIRC_1: 38;

      hence thesis by FACIRC_1: 3;

    end;

    theorem :: GFACIRC1:76

    

     Th76: for x,y,z be set st x <> [ <*y, z*>, and2c ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, and2a ] holds ( InputVertices ( GFA2CarryIStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      assume that

       A1: x <> yz and

       A2: y <> zx & z <> xy;

      

       A3: not xy in {y, z} by A1, A2, Lm1;

      

       A4: not zx in {x, y, z} by A1, A2, Lm1;

      

       A5: y <> yz by FACIRC_2: 2;

      

       A6: ( not z in {xy, yz}) & not x in {xy, yz} by A1, A2, Lm1;

      

       A7: Cxy tolerates Cyz by CIRCCOMB: 47;

      ( InputVertices ( GFA2CarryIStr (x,y,z))) = ((( InputVertices (Cxy +* Cyz)) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ ( InnerVertices (Cxy +* Cyz)))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((((( InputVertices Cxy) \ ( InnerVertices Cyz)) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ ( InnerVertices (Cxy +* Cyz)))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((((( InputVertices Cxy) \ ( InnerVertices Cyz)) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by A7, CIRCCOMB: 11

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by CIRCCOMB: 42

      .= (((( {x, y} \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ {xy, yz})) by ENUMSET1: 1

      .= ((( {x, y} \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ {xy, yz})) by A1, A5, FACIRC_2: 1

      .= ((( {x, y} \/ {y, z}) \ {zx}) \/ ( {z, x} \ {xy, yz})) by A3, ZFMISC_1: 57

      .= ((( {x, y} \/ {y, z}) \ {zx}) \/ {z, x}) by A6, ZFMISC_1: 63

      .= (( {x, y, y, z} \ {zx}) \/ {z, x}) by ENUMSET1: 5

      .= (( {y, y, x, z} \ {zx}) \/ {z, x}) by ENUMSET1: 67

      .= (( {y, x, z} \ {zx}) \/ {z, x}) by ENUMSET1: 31

      .= (( {x, y, z} \ {zx}) \/ {z, x}) by ENUMSET1: 58

      .= ( {x, y, z} \/ {z, x}) by A4, ZFMISC_1: 57

      .= {x, y, z, z, x} by ENUMSET1: 9

      .= ( {x, y, z, z} \/ {x}) by ENUMSET1: 10

      .= ( {z, z, x, y} \/ {x}) by ENUMSET1: 73

      .= ( {z, x, y} \/ {x}) by ENUMSET1: 31

      .= {z, x, y, x} by ENUMSET1: 6

      .= {x, x, y, z} by ENUMSET1: 70

      .= {x, y, z} by ENUMSET1: 31;

      hence thesis;

    end;

    theorem :: GFACIRC1:77

    

     Th77: for x,y,z be set st x <> [ <*y, z*>, and2c ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, and2a ] holds ( InputVertices ( GFA2CarryStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set MI = ( GFA2CarryIStr (x,y,z));

      

       A1: ( InputVertices S) = ( rng <*xy, yz, zx*>) by CIRCCOMB: 42

      .= {xy, yz, zx} by FINSEQ_2: 128;

      assume

       A2: x <> yz & y <> zx & z <> xy;

      

       A3: ( InnerVertices S) = {xyz} & ( {x, y, z} \ {xyz}) = {x, y, z} by Lm2, CIRCCOMB: 42;

      

       A4: ( {xy, yz, zx} \ {xy, yz, zx}) = {} by XBOOLE_1: 37;

      

      thus ( InputVertices ( GFA2CarryStr (x,y,z))) = ((( InputVertices MI) \ ( InnerVertices S)) \/ (( InputVertices S) \ ( InnerVertices MI))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ( {x, y, z} \/ ( {xy, yz, zx} \ ( InnerVertices MI))) by A1, A2, A3, Th76

      .= ( {x, y, z} \/ {} ) by A4, Th73

      .= {x, y, z};

    end;

    theorem :: GFACIRC1:78

    for x,y,z be non pair set holds ( InputVertices ( GFA2CarryStr (x,y,z))) is without_pairs

    proof

      let x,y,z be non pair set;

      set f1 = and2a , f2 = and2c , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set M = ( GFA2CarryStr (x,y,z));

      set MI = ( GFA2CarryIStr (x,y,z));

      given xx be pair object such that

       A1: xx in ( InputVertices M);

      

       A2: Cxy tolerates Cyz by CIRCCOMB: 47;

      

       A3: ( InnerVertices Czx) = {zx} & (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 42, CIRCCOMB: 47;

      ( InnerVertices Cxy) = {xy} & ( InnerVertices Cyz) = {yz} by CIRCCOMB: 42;

      then ( InnerVertices (Cxy +* Cyz)) = ( {xy} \/ {yz}) by A2, CIRCCOMB: 11;

      

      then

       A4: ( InnerVertices MI) = (( {xy} \/ {yz}) \/ {zx}) by A3, CIRCCOMB: 11

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      ( InputVertices S) = {xy, yz, zx} by FACIRC_1: 42;

      then

       A5: (( InputVertices S) \ ( InnerVertices MI)) = {} by A4, XBOOLE_1: 37;

      ( InputVertices Cxy) is without_pairs & ( InputVertices Cyz) is without_pairs by FACIRC_1: 41;

      then ( InputVertices Czx) is without_pairs & ( InputVertices (Cxy +* Cyz)) is without_pairs by FACIRC_1: 9, FACIRC_1: 41;

      then

       A6: ( InputVertices MI) is without_pairs by FACIRC_1: 9;

      ( InnerVertices S) is Relation by FACIRC_1: 38;

      then ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) by A6, FACIRC_1: 6;

      hence thesis by A6, A1, A5;

    end;

    theorem :: GFACIRC1:79

    

     Th79: for x,y,z be set holds x in the carrier of ( GFA2CarryStr (x,y,z)) & y in the carrier of ( GFA2CarryStr (x,y,z)) & z in the carrier of ( GFA2CarryStr (x,y,z)) & [ <*x, y*>, and2a ] in the carrier of ( GFA2CarryStr (x,y,z)) & [ <*y, z*>, and2c ] in the carrier of ( GFA2CarryStr (x,y,z)) & [ <*z, x*>, nor2 ] in the carrier of ( GFA2CarryStr (x,y,z)) & [ <* [ <*x, y*>, and2a ], [ <*y, z*>, and2c ], [ <*z, x*>, nor2 ]*>, nor3 ] in the carrier of ( GFA2CarryStr (x,y,z))

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set p = <*xy, yz, zx*>;

      z in the carrier of Czx by FACIRC_1: 43;

      then

       A1: z in the carrier of ( GFA2CarryIStr (x,y,z)) by FACIRC_1: 20;

      zx in the carrier of Czx by FACIRC_1: 43;

      then

       A2: zx in the carrier of ( GFA2CarryIStr (x,y,z)) by FACIRC_1: 20;

      y in the carrier of Cxy by FACIRC_1: 43;

      then y in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A3: y in the carrier of ( GFA2CarryIStr (x,y,z)) by FACIRC_1: 20;

      the carrier of Cxyz = (( rng p) \/ {xyz}) & [p, f4] in { [p, f4]} by CIRCCOMB:def 6, TARSKI:def 1;

      then

       A4: xyz in the carrier of Cxyz by XBOOLE_0:def 3;

      yz in the carrier of Cyz by FACIRC_1: 43;

      then yz in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A5: yz in the carrier of ( GFA2CarryIStr (x,y,z)) by FACIRC_1: 20;

      xy in the carrier of Cxy by FACIRC_1: 43;

      then xy in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A6: xy in the carrier of ( GFA2CarryIStr (x,y,z)) by FACIRC_1: 20;

      x in the carrier of Czx by FACIRC_1: 43;

      then x in the carrier of ( GFA2CarryIStr (x,y,z)) by FACIRC_1: 20;

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

    end;

    theorem :: GFACIRC1:80

    

     Th80: for x,y,z be set holds [ <*x, y*>, and2a ] in ( InnerVertices ( GFA2CarryStr (x,y,z))) & [ <*y, z*>, and2c ] in ( InnerVertices ( GFA2CarryStr (x,y,z))) & [ <*z, x*>, nor2 ] in ( InnerVertices ( GFA2CarryStr (x,y,z))) & ( GFA2CarryOutput (x,y,z)) in ( InnerVertices ( GFA2CarryStr (x,y,z)))

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      ( InnerVertices ( GFA2CarryStr (x,y,z))) = ( {xy, yz, zx} \/ {( GFA2CarryOutput (x,y,z))}) by Th74

      .= {xy, yz, zx, ( GFA2CarryOutput (x,y,z))} by ENUMSET1: 6;

      hence thesis by ENUMSET1:def 2;

    end;

    theorem :: GFACIRC1:81

    

     Th81: for x,y,z be set st x <> [ <*y, z*>, and2c ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, and2a ] holds x in ( InputVertices ( GFA2CarryStr (x,y,z))) & y in ( InputVertices ( GFA2CarryStr (x,y,z))) & z in ( InputVertices ( GFA2CarryStr (x,y,z)))

    proof

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      let x,y,z be set;

      assume x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      then ( InputVertices ( GFA2CarryStr (x,y,z))) = {x, y, z} by Th77;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: GFACIRC1:82

    

     Th82: for x,y,z be non pair set holds ( InputVertices ( GFA2CarryStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be non pair set;

      set f1 = and2a , f2 = and2c , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set M = ( GFA2CarryStr (x,y,z));

      set MI = ( GFA2CarryIStr (x,y,z));

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      

       A1: ( InputVertices Cxy) = {x, y} & ( InputVertices Cyz) = {y, z} by FACIRC_1: 40;

      

       A2: ( InputVertices Czx) = {z, x} by FACIRC_1: 40;

      

       A3: ( InputVertices S) = {xy, yz, zx} by FACIRC_1: 42;

      

       A4: ( InnerVertices S) is Relation by FACIRC_1: 38;

      

       A5: ( InnerVertices Cxy) = {xy} & ( InnerVertices Cyz) = {yz} by CIRCCOMB: 42;

      Cxy tolerates Cyz by CIRCCOMB: 47;

      then

       A6: ( InnerVertices Czx) = {zx} & ( InnerVertices (Cxy +* Cyz)) = ( {xy} \/ {yz}) by A5, CIRCCOMB: 11, CIRCCOMB: 42;

      (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 47;

      

      then ( InnerVertices MI) = (( {xy} \/ {yz}) \/ {zx}) by A6, CIRCCOMB: 11

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      then

       A7: (( InputVertices S) \ ( InnerVertices MI)) = {} by A3, XBOOLE_1: 37;

      

       A8: ( InputVertices Cxy) is without_pairs & ( InputVertices Cyz) is without_pairs by FACIRC_1: 41;

      then

       A9: ( InputVertices Czx) is without_pairs & ( InputVertices (Cxy +* Cyz)) is without_pairs by FACIRC_1: 9, FACIRC_1: 41;

      then ( InputVertices MI) is without_pairs by FACIRC_1: 9;

      then ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) by A4, FACIRC_1: 6;

      

      hence ( InputVertices M) = (( InputVertices (Cxy +* Cyz)) \/ ( InputVertices Czx)) by A9, A6, A7, FACIRC_1: 7

      .= ((( InputVertices Cxy) \/ ( InputVertices Cyz)) \/ ( InputVertices Czx)) by A8, A5, FACIRC_1: 7

      .= ( {x, y, y, z} \/ {z, x}) by A1, A2, ENUMSET1: 5

      .= ( {y, y, x, z} \/ {z, x}) by ENUMSET1: 67

      .= ( {y, x, z} \/ {z, x}) by ENUMSET1: 31

      .= ( {x, y, z} \/ {z, x}) by ENUMSET1: 58

      .= ( {x, y, z} \/ ( {z} \/ {x})) by ENUMSET1: 1

      .= (( {x, y, z} \/ {z}) \/ {x}) by XBOOLE_1: 4

      .= (( {z, x, y} \/ {z}) \/ {x}) by ENUMSET1: 59

      .= ( {z, z, x, y} \/ {x}) by ENUMSET1: 4

      .= ( {z, x, y} \/ {x}) by ENUMSET1: 31

      .= ( {x, y, z} \/ {x}) by ENUMSET1: 59

      .= {x, x, y, z} by ENUMSET1: 4

      .= {x, y, z} by ENUMSET1: 31;

    end;

    theorem :: GFACIRC1:83

    

     Th83: for x,y,z be set holds for s be State of ( GFA2CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following s) . [ <*x, y*>, and2a ]) = (( 'not' a1) '&' a2) & (( Following s) . [ <*y, z*>, and2c ]) = (a2 '&' ( 'not' a3)) & (( Following s) . [ <*z, x*>, nor2 ]) = (( 'not' a3) '&' ( 'not' a1))

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      let s be State of ( GFA2CarryCirc (x,y,z));

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

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

       A1: a1 = (s . x) and

       A2: a2 = (s . y) and

       A3: a3 = (s . z);

      set S = ( GFA2CarryStr (x,y,z));

      

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

      

       A5: y in the carrier of S by Th79;

      

       A6: x in the carrier of S by Th79;

      

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

      xy in ( InnerVertices ( GFA2CarryStr (x,y,z))) by Th80;

      

      hence (( Following s) . [ <*x, y*>, f1]) = (f1 . (s * <*x, y*>)) by A4, FACIRC_1: 35

      .= (f1 . <*a1, a2*>) by A1, A2, A7, A6, A5, FINSEQ_2: 125

      .= (( 'not' a1) '&' a2) by TWOSCOMP:def 2;

      

       A8: z in the carrier of S by Th79;

      yz in ( InnerVertices ( GFA2CarryStr (x,y,z))) by Th80;

      

      hence (( Following s) . [ <*y, z*>, f2]) = (f2 . (s * <*y, z*>)) by A4, FACIRC_1: 35

      .= (f2 . <*a2, a3*>) by A2, A3, A7, A5, A8, FINSEQ_2: 125

      .= (a2 '&' ( 'not' a3)) by Def3;

      zx in ( InnerVertices ( GFA2CarryStr (x,y,z))) by Th80;

      

      hence (( Following s) . [ <*z, x*>, f3]) = (f3 . (s * <*z, x*>)) by A4, FACIRC_1: 35

      .= (f3 . <*a3, a1*>) by A1, A3, A7, A6, A8, FINSEQ_2: 125

      .= (( 'not' a3) '&' ( 'not' a1)) by TWOSCOMP: 54;

    end;

    theorem :: GFACIRC1:84

    

     Th84: for x,y,z be set holds for s be State of ( GFA2CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . [ <*x, y*>, and2a ]) & a2 = (s . [ <*y, z*>, and2c ]) & a3 = (s . [ <*z, x*>, nor2 ]) holds (( Following s) . ( GFA2CarryOutput (x,y,z))) = ( 'not' ((a1 'or' a2) 'or' a3))

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 , f4 = nor3 ;

      let s be State of ( GFA2CarryCirc (x,y,z));

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

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

       A1: a1 = (s . xy) & a2 = (s . yz) & a3 = (s . zx);

      set S = ( GFA2CarryStr (x,y,z));

      reconsider xy, yz, zx as Element of ( InnerVertices S) by Th80;

      

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

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

      

      hence (( Following s) . ( GFA2CarryOutput (x,y,z))) = (f4 . (s * <*xy, yz, zx*>)) by FACIRC_1: 35

      .= (f4 . <*a1, a2, a3*>) by A1, A2, FINSEQ_2: 126

      .= ( 'not' ((a1 'or' a2) 'or' a3)) by TWOSCOMP:def 28;

    end;

    theorem :: GFACIRC1:85

    

     Th85: for x,y,z be set st x <> [ <*y, z*>, and2c ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, and2a ] holds for s be State of ( GFA2CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA2CarryOutput (x,y,z))) = ( 'not' (((( 'not' a1) '&' a2) 'or' (a2 '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1)))) & (( Following (s,2)) . [ <*x, y*>, and2a ]) = (( 'not' a1) '&' a2) & (( Following (s,2)) . [ <*y, z*>, and2c ]) = (a2 '&' ( 'not' a3)) & (( Following (s,2)) . [ <*z, x*>, nor2 ]) = (( 'not' a3) '&' ( 'not' a1))

    proof

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      let x,y,z be set such that

       A1: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( GFA2CarryStr (x,y,z));

      reconsider x9 = x, y9 = y, z9 = z as Vertex of S by Th79;

      let s be State of ( GFA2CarryCirc (x,y,z));

      y in ( InputVertices S) by A1, Th81;

      then

       A2: (( Following s) . y9) = (s . y) by CIRCUIT2:def 5;

      z in ( InputVertices S) by A1, Th81;

      then

       A3: (( Following s) . z9) = (s . z) by CIRCUIT2:def 5;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      

       A4: ( Following (s,2)) = ( Following ( Following s)) by FACIRC_1: 15;

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

       A5: a1 = (s . x) & a2 = (s . y) & a3 = (s . z);

      

       A6: (( Following s) . zx) = (( 'not' a3) '&' ( 'not' a1)) by A5, Th83;

      (( Following s) . xy) = (( 'not' a1) '&' a2) & (( Following s) . yz) = (a2 '&' ( 'not' a3)) by A5, Th83;

      hence (( Following (s,2)) . ( GFA2CarryOutput (x,y,z))) = ( 'not' (((( 'not' a1) '&' a2) 'or' (a2 '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1)))) by A4, A6, Th84;

      x in ( InputVertices S) by A1, Th81;

      then (( Following s) . x9) = (s . x) by CIRCUIT2:def 5;

      hence thesis by A5, A2, A3, A4, Th83;

    end;

    theorem :: GFACIRC1:86

    

     Th86: for x,y,z be set st x <> [ <*y, z*>, and2c ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, and2a ] holds for s be State of ( GFA2CarryCirc (x,y,z)) holds ( Following (s,2)) is stable

    proof

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      let x,y,z be set such that

       A1: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( GFA2CarryStr (x,y,z));

      reconsider xx = x, yy = y, zz = z as Vertex of S by Th79;

      let s be State of ( GFA2CarryCirc (x,y,z));

      set a1 = (s . xx), a2 = (s . yy), a3 = (s . zz);

      set ffs = ( Following (s,2)), fffs = ( Following ffs);

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      

       A2: ffs = ( Following ( Following s)) by FACIRC_1: 15;

      

       A3: z in ( InputVertices S) by A1, Th81;

      then (( Following s) . z) = a3 by CIRCUIT2:def 5;

      then

       A4: (ffs . z) = a3 by A2, A3, CIRCUIT2:def 5;

      

       A5: y in ( InputVertices S) by A1, Th81;

      then (( Following s) . y) = a2 by CIRCUIT2:def 5;

      then

       A6: (ffs . y) = a2 by A2, A5, CIRCUIT2:def 5;

      

       A7: x in ( InputVertices S) by A1, Th81;

      then (( Following s) . x) = a1 by CIRCUIT2:def 5;

      then

       A8: (ffs . x) = a1 by A2, A7, CIRCUIT2:def 5;

      a3 = (s . z);

      then

       A9: (ffs . xy) = (( 'not' a1) '&' a2) by A1, Th85;

      a2 = (s . y);

      then

       A10: (ffs . zx) = (( 'not' a1) '&' ( 'not' a3)) by A1, Th85;

      a1 = (s . x);

      then

       A11: (ffs . yz) = (a2 '&' ( 'not' a3)) by A1, Th85;

      

       A12: (ffs . ( GFA2CarryOutput (x,y,z))) = ( 'not' (((( 'not' a1) '&' a2) 'or' (a2 '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1)))) by A1, Th85;

       A13:

      now

        let a be object;

        assume

         A14: a in the carrier of S;

        then

        reconsider v = a as Vertex of S;

        

         A15: v in (( InputVertices S) \/ ( InnerVertices S)) by A14, XBOOLE_1: 45;

        thus (ffs . a) = (fffs . a)

        proof

          per cases by A15, XBOOLE_0:def 3;

            suppose v in ( InputVertices S);

            hence thesis by CIRCUIT2:def 5;

          end;

            suppose v in ( InnerVertices S);

            then v in ( {xy, yz, zx} \/ {( GFA2CarryOutput (x,y,z))}) by Th74;

            then v in {xy, yz, zx} or v in {( GFA2CarryOutput (x,y,z))} by XBOOLE_0:def 3;

            then v = xy or v = yz or v = zx or v = ( GFA2CarryOutput (x,y,z)) by ENUMSET1:def 1, TARSKI:def 1;

            hence thesis by A12, A9, A11, A10, A8, A6, A4, Th83, Th84;

          end;

        end;

      end;

      ( dom ( Following ( Following (s,2)))) = the carrier of S & ( dom ( Following (s,2))) = the carrier of S by CIRCUIT1: 3;

      hence ffs = fffs by A13, FUNCT_1: 2;

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def34

      func GFA2AdderStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ( 2GatesCircStr (x,y,z, xor2c ));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def35

      func GFA2AdderCirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA2AdderStr (x,y,z)) equals ( 2GatesCircuit (x,y,z, xor2c ));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def36

      func GFA2AdderOutput (x,y,z) -> Element of ( InnerVertices ( GFA2AdderStr (x,y,z))) equals ( 2GatesCircOutput (x,y,z, xor2c ));

      coherence ;

    end

    theorem :: GFACIRC1:87

    

     Th87: for x,y,z be set holds ( InnerVertices ( GFA2AdderStr (x,y,z))) = ( { [ <*x, y*>, xor2c ]} \/ {( GFA2AdderOutput (x,y,z))})

    proof

      let x,y,z be set;

      ( GFA2AdderOutput (x,y,z)) = ( GFA1AdderOutput (x,y,z));

      hence thesis by Th55;

    end;

    theorem :: GFACIRC1:88

    for x,y,z be set holds x in the carrier of ( GFA2AdderStr (x,y,z)) & y in the carrier of ( GFA2AdderStr (x,y,z)) & z in the carrier of ( GFA2AdderStr (x,y,z)) & [ <*x, y*>, xor2c ] in the carrier of ( GFA2AdderStr (x,y,z)) & [ <* [ <*x, y*>, xor2c ], z*>, xor2c ] in the carrier of ( GFA2AdderStr (x,y,z)) by FACIRC_1: 60, FACIRC_1: 61;

    theorem :: GFACIRC1:89

    for x,y,z be set holds [ <*x, y*>, xor2c ] in ( InnerVertices ( GFA2AdderStr (x,y,z))) & ( GFA2AdderOutput (x,y,z)) in ( InnerVertices ( GFA2AdderStr (x,y,z)))

    proof

      let x,y,z be set;

      set S1 = ( GFA1AdderStr (x,y,z));

      ( GFA2AdderStr (x,y,z)) = S1;

      hence thesis by Th57;

    end;

    theorem :: GFACIRC1:90

    for x,y,z be set st z <> [ <*x, y*>, xor2c ] holds x in ( InputVertices ( GFA2AdderStr (x,y,z))) & y in ( InputVertices ( GFA2AdderStr (x,y,z))) & z in ( InputVertices ( GFA2AdderStr (x,y,z)))

    proof

      set f = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set S1 = ( GFA1AdderStr (x,y,z));

      ( GFA2AdderStr (x,y,z)) = S1;

      hence thesis by A1, Th58;

    end;

    theorem :: GFACIRC1:91

    for x,y,z be set st z <> [ <*x, y*>, xor2c ] holds for s be State of ( GFA2AdderCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following s) . [ <*x, y*>, xor2c ]) = (a1 'xor' ( 'not' a2)) & (( Following s) . x) = a1 & (( Following s) . y) = a2 & (( Following s) . z) = a3

    proof

      set f = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

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

      ( GFA2AdderCirc (x,y,z)) = A1;

      hence thesis by A1, Th59;

    end;

    theorem :: GFACIRC1:92

    for x,y,z be set st z <> [ <*x, y*>, xor2c ] holds for s be State of ( GFA2AdderCirc (x,y,z)) holds for a1a2,a1,a2,a3 be Element of BOOLEAN st a1a2 = (s . [ <*x, y*>, xor2c ]) & a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following s) . ( GFA2AdderOutput (x,y,z))) = (a1a2 'xor' ( 'not' a3))

    proof

      set f = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

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

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

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

      set A2 = ( GFA2AdderCirc (x,y,z));

      A2 = A1 & O2 = O1;

      hence thesis by A1, Th60;

    end;

    theorem :: GFACIRC1:93

    

     Th93: for x,y,z be set st z <> [ <*x, y*>, xor2c ] holds for s be State of ( GFA2AdderCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA2AdderOutput (x,y,z))) = ((a1 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) & (( Following (s,2)) . [ <*x, y*>, xor2c ]) = (a1 'xor' ( 'not' a2)) & (( Following (s,2)) . x) = a1 & (( Following (s,2)) . y) = a2 & (( Following (s,2)) . z) = a3

    proof

      set f = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

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

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

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

      set A2 = ( GFA2AdderCirc (x,y,z));

      A2 = A1 & O2 = O1;

      hence thesis by A1, Th61;

    end;

    theorem :: GFACIRC1:94

    

     Th94: for x,y,z be set st z <> [ <*x, y*>, xor2c ] holds for s be State of ( GFA2AdderCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA2AdderOutput (x,y,z))) = ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3))

    proof

      set f = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set A = ( GFA2AdderCirc (x,y,z));

      let s be State of A;

      let a1,a2,a3 be Element of BOOLEAN ;

      assume a1 = (s . x) & a2 = (s . y) & a3 = (s . z);

      

      hence (( Following (s,2)) . ( GFA2AdderOutput (x,y,z))) = ((a1 'xor' ( 'not' a2)) 'xor' ( 'not' a3)) by A1, Th93

      .= ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3));

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def37

      func BitGFA2Str (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( GFA2AdderStr (x,y,z)) +* ( GFA2CarryStr (x,y,z)));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def38

      func BitGFA2Circ (x,y,z) -> strict Boolean gate`2=den Circuit of ( BitGFA2Str (x,y,z)) equals (( GFA2AdderCirc (x,y,z)) +* ( GFA2CarryCirc (x,y,z)));

      coherence ;

    end

    theorem :: GFACIRC1:95

    

     Th95: for x,y,z be set holds ( InnerVertices ( BitGFA2Str (x,y,z))) = ((( { [ <*x, y*>, xor2c ]} \/ {( GFA2AdderOutput (x,y,z))}) \/ { [ <*x, y*>, and2a ], [ <*y, z*>, and2c ], [ <*z, x*>, nor2 ]}) \/ {( GFA2CarryOutput (x,y,z))})

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      set f0 = xor2c ;

      set xyf0 = [ <*x, y*>, f0];

      set xyf1 = [ <*x, y*>, f1], yzf2 = [ <*y, z*>, f2], zxf3 = [ <*z, x*>, f3];

      set S = ( BitGFA2Str (x,y,z));

      set S1 = ( GFA2AdderStr (x,y,z));

      set S2 = ( GFA2CarryStr (x,y,z));

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

      set A2 = ( GFA2CarryOutput (x,y,z));

      

      thus ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by FACIRC_1: 27

      .= (( {xyf0} \/ {A1}) \/ ( InnerVertices S2)) by Th87

      .= (( {xyf0} \/ {A1}) \/ ( {xyf1, yzf2, zxf3} \/ {A2})) by Th74

      .= ((( {xyf0} \/ {A1}) \/ {xyf1, yzf2, zxf3}) \/ {A2}) by XBOOLE_1: 4;

    end;

    theorem :: GFACIRC1:96

    for x,y,z be set holds ( InnerVertices ( BitGFA2Str (x,y,z))) is Relation

    proof

      let x,y,z be set;

      set S1 = ( GFA2AdderStr (x,y,z));

      set S2 = ( GFA2CarryStr (x,y,z));

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by Th75, FACIRC_1: 58;

      hence thesis by FACIRC_1: 3;

    end;

    theorem :: GFACIRC1:97

    

     Th97: for x,y,z be set st z <> [ <*x, y*>, xor2c ] & x <> [ <*y, z*>, and2c ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, and2a ] holds ( InputVertices ( BitGFA2Str (x,y,z))) = {x, y, z}

    proof

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      set f0 = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] & x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S2 = ( GFA2CarryStr (x,y,z));

      set S1 = ( GFA2AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} & ( InputVertices S2) = {x, y, z} by A1, Th77, FACIRC_1: 57;

      hence thesis by CIRCCOMB: 47, FACIRC_2: 21;

    end;

    theorem :: GFACIRC1:98

    

     Th98: for x,y,z be non pair set holds ( InputVertices ( BitGFA2Str (x,y,z))) = {x, y, z}

    proof

      let x,y,z be non pair set;

      set S = ( BitGFA2Str (x,y,z));

      set S1 = ( GFA2AdderStr (x,y,z));

      set S2 = ( GFA2CarryStr (x,y,z));

      

       A1: ( InputVertices S1) = {x, y, z} & ( InputVertices S2) = {x, y, z} by Th82, FACIRC_1: 57;

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by Th75, FACIRC_1: 58;

      

      hence ( InputVertices S) = ( {x, y, z} \/ {x, y, z}) by A1, FACIRC_1: 7

      .= {x, y, z};

    end;

    theorem :: GFACIRC1:99

    for x,y,z be non pair set holds ( InputVertices ( BitGFA2Str (x,y,z))) is without_pairs

    proof

      let x,y,z be non pair set;

      ( InputVertices ( BitGFA2Str (x,y,z))) = {x, y, z} by Th98;

      hence thesis;

    end;

    theorem :: GFACIRC1:100

    for x,y,z be set holds x in the carrier of ( BitGFA2Str (x,y,z)) & y in the carrier of ( BitGFA2Str (x,y,z)) & z in the carrier of ( BitGFA2Str (x,y,z)) & [ <*x, y*>, xor2c ] in the carrier of ( BitGFA2Str (x,y,z)) & [ <* [ <*x, y*>, xor2c ], z*>, xor2c ] in the carrier of ( BitGFA2Str (x,y,z)) & [ <*x, y*>, and2a ] in the carrier of ( BitGFA2Str (x,y,z)) & [ <*y, z*>, and2c ] in the carrier of ( BitGFA2Str (x,y,z)) & [ <*z, x*>, nor2 ] in the carrier of ( BitGFA2Str (x,y,z)) & [ <* [ <*x, y*>, and2a ], [ <*y, z*>, and2c ], [ <*z, x*>, nor2 ]*>, nor3 ] in the carrier of ( BitGFA2Str (x,y,z))

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 , f4 = nor3 ;

      set f0 = xor2c ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set S1 = ( GFA2AdderStr (x,y,z));

      set S2 = ( GFA2CarryStr (x,y,z));

      

       A1: x in the carrier of S1 & y in the carrier of S1 by FACIRC_1: 60;

      

       A2: z in the carrier of S1 & [ <*x, y*>, f0] in the carrier of S1 by FACIRC_1: 60, FACIRC_1: 61;

      

       A3: xyz in the carrier of S2 by Th79;

      

       A4: yz in the carrier of S2 & zx in the carrier of S2 by Th79;

       [ <* [ <*x, y*>, f0], z*>, f0] in the carrier of S1 & xy in the carrier of S2 by Th79, FACIRC_1: 61;

      hence thesis by A1, A2, A4, A3, FACIRC_1: 20;

    end;

    theorem :: GFACIRC1:101

    

     Th101: for x,y,z be set holds [ <*x, y*>, xor2c ] in ( InnerVertices ( BitGFA2Str (x,y,z))) & ( GFA2AdderOutput (x,y,z)) in ( InnerVertices ( BitGFA2Str (x,y,z))) & [ <*x, y*>, and2a ] in ( InnerVertices ( BitGFA2Str (x,y,z))) & [ <*y, z*>, and2c ] in ( InnerVertices ( BitGFA2Str (x,y,z))) & [ <*z, x*>, nor2 ] in ( InnerVertices ( BitGFA2Str (x,y,z))) & ( GFA2CarryOutput (x,y,z)) in ( InnerVertices ( BitGFA2Str (x,y,z)))

    proof

      let x,y,z be set;

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      set f0 = xor2c ;

      set xyf0 = [ <*x, y*>, f0];

      set xyf1 = [ <*x, y*>, f1], yzf2 = [ <*y, z*>, f2], zxf3 = [ <*z, x*>, f3];

      set S = ( BitGFA2Str (x,y,z));

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

      set A2 = ( GFA2CarryOutput (x,y,z));

      ( InnerVertices S) = ((( {xyf0} \/ {A1}) \/ {xyf1, yzf2, zxf3}) \/ {A2}) by Th95

      .= (( {xyf0, A1} \/ {xyf1, yzf2, zxf3}) \/ {A2}) by ENUMSET1: 1

      .= ( {xyf0, A1, xyf1, yzf2, zxf3} \/ {A2}) by ENUMSET1: 8

      .= {xyf0, A1, xyf1, yzf2, zxf3, A2} by ENUMSET1: 15;

      hence thesis by ENUMSET1:def 4;

    end;

    theorem :: GFACIRC1:102

    for x,y,z be set st z <> [ <*x, y*>, xor2c ] & x <> [ <*y, z*>, and2c ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, and2a ] holds x in ( InputVertices ( BitGFA2Str (x,y,z))) & y in ( InputVertices ( BitGFA2Str (x,y,z))) & z in ( InputVertices ( BitGFA2Str (x,y,z)))

    proof

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      set f0 = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] & x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( BitGFA2Str (x,y,z));

      ( InputVertices S) = {x, y, z} by A1, Th97;

      hence thesis by ENUMSET1:def 1;

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def39

      func BitGFA2CarryOutput (x,y,z) -> Element of ( InnerVertices ( BitGFA2Str (x,y,z))) equals [ <* [ <*x, y*>, and2a ], [ <*y, z*>, and2c ], [ <*z, x*>, nor2 ]*>, nor3 ];

      coherence

      proof

        ( GFA2CarryOutput (x,y,z)) in ( InnerVertices ( BitGFA2Str (x,y,z))) by Th101;

        hence thesis;

      end;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def40

      func BitGFA2AdderOutput (x,y,z) -> Element of ( InnerVertices ( BitGFA2Str (x,y,z))) equals ( 2GatesCircOutput (x,y,z, xor2c ));

      coherence

      proof

        ( GFA2AdderOutput (x,y,z)) in ( InnerVertices ( BitGFA2Str (x,y,z))) by Th101;

        hence thesis;

      end;

    end

    theorem :: GFACIRC1:103

    for x,y,z be set st z <> [ <*x, y*>, xor2c ] & x <> [ <*y, z*>, and2c ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, and2a ] holds for s be State of ( BitGFA2Circ (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA2AdderOutput (x,y,z))) = ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) & (( Following (s,2)) . ( GFA2CarryOutput (x,y,z))) = ( 'not' (((( 'not' a1) '&' a2) 'or' (a2 '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1))))

    proof

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      set f0 = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] and

       A2: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S2 = ( GFA2CarryStr (x,y,z));

      set S1 = ( GFA2AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} by A1, FACIRC_1: 57;

      then

       A3: ( InputVertices S1) = ( InputVertices S2) by A2, Th77;

      set A2 = ( GFA2CarryCirc (x,y,z));

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

      set A = ( BitGFA2Circ (x,y,z));

      let s be State of A;

      let a1,a2,a3 be Element of BOOLEAN ;

      assume that

       A4: a1 = (s . x) and

       A5: a2 = (s . y) and

       A6: a3 = (s . z);

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

      

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

      z in the carrier of S1 by FACIRC_1: 60;

      then

       A8: a3 = (s1 . z) by A6, A7, FUNCT_1: 47;

      y in the carrier of S1 by FACIRC_1: 60;

      then

       A9: a2 = (s1 . y) by A5, A7, FUNCT_1: 47;

      reconsider t = s as State of (A1 +* A2);

      ( InnerVertices S2) misses ( InputVertices S2) by XBOOLE_1: 79;

      then

       A10: (( Following (t,2)) . ( GFA2AdderOutput (x,y,z))) = (( Following (s1,2)) . ( GFA2AdderOutput (x,y,z))) by A3, FACIRC_1: 32;

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      

       A11: ( dom s2) = the carrier of S2 by CIRCUIT1: 3;

      x in the carrier of S1 by FACIRC_1: 60;

      then a1 = (s1 . x) by A4, A7, FUNCT_1: 47;

      hence (( Following (s,2)) . ( GFA2AdderOutput (x,y,z))) = ((( 'not' a1) 'xor' a2) 'xor' ( 'not' a3)) by A1, A9, A8, A10, Th94;

      ( InnerVertices S1) misses ( InputVertices S1) by XBOOLE_1: 79;

      then

       A12: (( Following (t,2)) . ( GFA2CarryOutput (x,y,z))) = (( Following (s2,2)) . ( GFA2CarryOutput (x,y,z))) by A3, FACIRC_1: 33;

      z in the carrier of S2 by Th79;

      then

       A13: a3 = (s2 . z) by A6, A11, FUNCT_1: 47;

      y in the carrier of S2 by Th79;

      then

       A14: a2 = (s2 . y) by A5, A11, FUNCT_1: 47;

      x in the carrier of S2 by Th79;

      then a1 = (s2 . x) by A4, A11, FUNCT_1: 47;

      hence thesis by A2, A14, A13, A12, Th85;

    end;

    theorem :: GFACIRC1:104

    for x,y,z be set st z <> [ <*x, y*>, xor2c ] & x <> [ <*y, z*>, and2c ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, and2a ] holds for s be State of ( BitGFA2Circ (x,y,z)) holds ( Following (s,2)) is stable

    proof

      set f1 = and2a , f2 = and2c , f3 = nor2 ;

      set f0 = xor2c ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] and

       A2: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set A = ( BitGFA2Circ (x,y,z));

      let s be State of A;

      set S2 = ( GFA2CarryStr (x,y,z));

      set S1 = ( GFA2AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} by A1, FACIRC_1: 57;

      then

       A3: ( InputVertices S1) = ( InputVertices S2) by A2, Th77;

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

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

      ( Following (s1,2)) is stable by A1, FACIRC_1: 63;

      

      then

       A4: ( Following (s1,2)) = ( Following ( Following (s1,2)))

      .= ( Following (s1,(2 + 1))) by FACIRC_1: 12;

      set A2 = ( GFA2CarryCirc (x,y,z));

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      ( Following (s2,2)) is stable by A2, Th86;

      

      then

       A5: ( Following (s2,2)) = ( Following ( Following (s2,2)))

      .= ( Following (s2,(2 + 1))) by FACIRC_1: 12;

      reconsider t = s as State of (A1 +* A2);

      set S = ( BitGFA2Str (x,y,z));

      

       A6: ( dom ( Following (s,3))) = the carrier of S by CIRCUIT1: 3;

      ( InnerVertices S2) misses ( InputVertices S2) by XBOOLE_1: 79;

      then

       A7: ( Following (s1,2)) = (( Following (t,2)) | the carrier of S1) & ( Following (s1,3)) = (( Following (t,3)) | the carrier of S1) by A3, FACIRC_1: 30;

      ( InnerVertices S1) misses ( InputVertices S1) by XBOOLE_1: 79;

      then

       A8: ( Following (s2,2)) = (( Following (t,2)) | the carrier of S2) & ( Following (s2,3)) = (( Following (t,3)) | the carrier of S2) by A3, FACIRC_1: 31;

      

       A9: the carrier of S = (the carrier of S1 \/ the carrier of S2) by CIRCCOMB:def 2;

      

       A10: ( dom ( Following (s1,2))) = the carrier of S1 & ( dom ( Following (s2,2))) = the carrier of S2 by CIRCUIT1: 3;

       A11:

      now

        let a be object;

        assume a in the carrier of S;

        then a in the carrier of S1 or a in the carrier of S2 by A9, XBOOLE_0:def 3;

        then (( Following (s,2)) . a) = (( Following (s1,2)) . a) & (( Following (s,3)) . a) = (( Following (s1,3)) . a) or (( Following (s,2)) . a) = (( Following (s2,2)) . a) & (( Following (s,3)) . a) = (( Following (s2,3)) . a) by A7, A8, A4, A5, A10, FUNCT_1: 47;

        hence (( Following (s,2)) . a) = (( Following ( Following (s,2))) . a) by A4, A5, FACIRC_1: 12;

      end;

      ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) & ( dom ( Following (s,2))) = the carrier of S by CIRCUIT1: 3, FACIRC_1: 12;

      hence ( Following (s,2)) = ( Following ( Following (s,2))) by A6, A11, FUNCT_1: 2;

    end;

    begin

    definition

      let x,y,z be set;

      :: GFACIRC1:def41

      func GFA3CarryIStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ((( 1GateCircStr ( <*x, y*>, nor2 )) +* ( 1GateCircStr ( <*y, z*>, nor2 ))) +* ( 1GateCircStr ( <*z, x*>, nor2 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def42

      func GFA3CarryICirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA3CarryIStr (x,y,z)) equals ((( 1GateCircuit (x,y, nor2 )) +* ( 1GateCircuit (y,z, nor2 ))) +* ( 1GateCircuit (z,x, nor2 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def43

      func GFA3CarryStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( GFA3CarryIStr (x,y,z)) +* ( 1GateCircStr ( <* [ <*x, y*>, nor2 ], [ <*y, z*>, nor2 ], [ <*z, x*>, nor2 ]*>, nor3 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def44

      func GFA3CarryCirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA3CarryStr (x,y,z)) equals (( GFA3CarryICirc (x,y,z)) +* ( 1GateCircuit ( [ <*x, y*>, nor2 ], [ <*y, z*>, nor2 ], [ <*z, x*>, nor2 ], nor3 )));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def45

      func GFA3CarryOutput (x,y,z) -> Element of ( InnerVertices ( GFA3CarryStr (x,y,z))) equals [ <* [ <*x, y*>, nor2 ], [ <*y, z*>, nor2 ], [ <*z, x*>, nor2 ]*>, nor3 ];

      coherence

      proof

         [ <* [ <*x, y*>, nor2 ], [ <*y, z*>, nor2 ], [ <*z, x*>, nor2 ]*>, nor3 ] in ( InnerVertices ( 1GateCircStr ( <* [ <*x, y*>, nor2 ], [ <*y, z*>, nor2 ], [ <*z, x*>, nor2 ]*>, nor3 ))) by FACIRC_1: 47;

        hence thesis by FACIRC_1: 21;

      end;

    end

    theorem :: GFACIRC1:105

    

     Th105: for x,y,z be set holds ( InnerVertices ( GFA3CarryIStr (x,y,z))) = { [ <*x, y*>, nor2 ], [ <*y, z*>, nor2 ], [ <*z, x*>, nor2 ]}

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      

       A1: Cxy tolerates Cyz by CIRCCOMB: 47;

      (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 47;

      

      then ( InnerVertices ( GFA3CarryIStr (x,y,z))) = (( InnerVertices (Cxy +* Cyz)) \/ ( InnerVertices Czx)) by CIRCCOMB: 11

      .= ((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) by A1, CIRCCOMB: 11

      .= (( {xy} \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) by CIRCCOMB: 42

      .= (( {xy} \/ {yz}) \/ ( InnerVertices Czx)) by CIRCCOMB: 42

      .= (( {xy} \/ {yz}) \/ {zx}) by CIRCCOMB: 42

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      hence thesis;

    end;

    theorem :: GFACIRC1:106

    

     Th106: for x,y,z be set holds ( InnerVertices ( GFA3CarryStr (x,y,z))) = ( { [ <*x, y*>, nor2 ], [ <*y, z*>, nor2 ], [ <*z, x*>, nor2 ]} \/ {( GFA3CarryOutput (x,y,z))})

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      

       A1: Cxy tolerates ((Cyz +* Czx) +* Cxyz) by CIRCCOMB: 47;

      Cyz tolerates (Czx +* Cxyz) by CIRCCOMB: 47;

      then

       A2: ( InnerVertices (Cyz +* (Czx +* Cxyz))) = (( InnerVertices Cyz) \/ ( InnerVertices (Czx +* Cxyz))) by CIRCCOMB: 11;

      Czx tolerates Cxyz by CIRCCOMB: 47;

      then

       A3: ( InnerVertices (Czx +* Cxyz)) = (( InnerVertices Czx) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 11;

      

      thus ( InnerVertices ( GFA3CarryStr (x,y,z))) = ( InnerVertices ((Cxy +* (Cyz +* Czx)) +* Cxyz)) by CIRCCOMB: 6

      .= ( InnerVertices (Cxy +* ((Cyz +* Czx) +* Cxyz))) by CIRCCOMB: 6

      .= (( InnerVertices Cxy) \/ ( InnerVertices ((Cyz +* Czx) +* Cxyz))) by A1, CIRCCOMB: 11

      .= (( InnerVertices Cxy) \/ ( InnerVertices (Cyz +* (Czx +* Cxyz)))) by CIRCCOMB: 6

      .= ((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ (( InnerVertices Czx) \/ ( InnerVertices Cxyz))) by A2, A3, XBOOLE_1: 4

      .= (((( InnerVertices Cxy) \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by XBOOLE_1: 4

      .= ((( {xy} \/ ( InnerVertices Cyz)) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= ((( {xy} \/ {yz}) \/ ( InnerVertices Czx)) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= ((( {xy} \/ {yz}) \/ {zx}) \/ ( InnerVertices Cxyz)) by CIRCCOMB: 42

      .= (( {xy, yz} \/ {zx}) \/ ( InnerVertices Cxyz)) by ENUMSET1: 1

      .= ( {xy, yz, zx} \/ ( InnerVertices Cxyz)) by ENUMSET1: 3

      .= ( {xy, yz, zx} \/ {( GFA3CarryOutput (x,y,z))}) by CIRCCOMB: 42;

    end;

    theorem :: GFACIRC1:107

    

     Th107: for x,y,z be set holds ( InnerVertices ( GFA3CarryStr (x,y,z))) is Relation

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      ( InnerVertices Cxy) is Relation & ( InnerVertices Cyz) is Relation by FACIRC_1: 38;

      then ( InnerVertices Czx) is Relation & ( InnerVertices (Cxy +* Cyz)) is Relation by FACIRC_1: 3, FACIRC_1: 38;

      then ( InnerVertices Cxyz) is Relation & ( InnerVertices ( GFA3CarryIStr (x,y,z))) is Relation by FACIRC_1: 3, FACIRC_1: 38;

      hence thesis by FACIRC_1: 3;

    end;

    theorem :: GFACIRC1:108

    

     Th108: for x,y,z be set st x <> [ <*y, z*>, nor2 ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, nor2 ] holds ( InputVertices ( GFA3CarryIStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      assume that

       A1: x <> yz and

       A2: y <> zx & z <> xy;

      

       A3: not xy in {y, z} by A1, A2, Lm1;

      

       A4: not zx in {x, y, z} by A1, A2, Lm1;

      

       A5: y <> yz by FACIRC_2: 2;

      

       A6: ( not z in {xy, yz}) & not x in {xy, yz} by A1, A2, Lm1;

      

       A7: Cxy tolerates Cyz by CIRCCOMB: 47;

      ( InputVertices ( GFA3CarryIStr (x,y,z))) = ((( InputVertices (Cxy +* Cyz)) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ ( InnerVertices (Cxy +* Cyz)))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((((( InputVertices Cxy) \ ( InnerVertices Cyz)) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ ( InnerVertices (Cxy +* Cyz)))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((((( InputVertices Cxy) \ ( InnerVertices Cyz)) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by A7, CIRCCOMB: 11

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ ( InnerVertices Cxy))) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ ( InnerVertices Czx)) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ (( InnerVertices Cxy) \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ ( InnerVertices Cyz)))) by CIRCCOMB: 42

      .= ((((( InputVertices Cxy) \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by CIRCCOMB: 42

      .= (((( {x, y} \ {yz}) \/ (( InputVertices Cyz) \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ (( InputVertices Czx) \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ ( {xy} \/ {yz}))) by FACIRC_1: 40

      .= (((( {x, y} \ {yz}) \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ {xy, yz})) by ENUMSET1: 1

      .= ((( {x, y} \/ ( {y, z} \ {xy})) \ {zx}) \/ ( {z, x} \ {xy, yz})) by A1, A5, FACIRC_2: 1

      .= ((( {x, y} \/ {y, z}) \ {zx}) \/ ( {z, x} \ {xy, yz})) by A3, ZFMISC_1: 57

      .= ((( {x, y} \/ {y, z}) \ {zx}) \/ {z, x}) by A6, ZFMISC_1: 63

      .= (( {x, y, y, z} \ {zx}) \/ {z, x}) by ENUMSET1: 5

      .= (( {y, y, x, z} \ {zx}) \/ {z, x}) by ENUMSET1: 67

      .= (( {y, x, z} \ {zx}) \/ {z, x}) by ENUMSET1: 31

      .= (( {x, y, z} \ {zx}) \/ {z, x}) by ENUMSET1: 58

      .= ( {x, y, z} \/ {z, x}) by A4, ZFMISC_1: 57

      .= {x, y, z, z, x} by ENUMSET1: 9

      .= ( {x, y, z, z} \/ {x}) by ENUMSET1: 10

      .= ( {z, z, x, y} \/ {x}) by ENUMSET1: 73

      .= ( {z, x, y} \/ {x}) by ENUMSET1: 31

      .= {z, x, y, x} by ENUMSET1: 6

      .= {x, x, y, z} by ENUMSET1: 70

      .= {x, y, z} by ENUMSET1: 31;

      hence thesis;

    end;

    theorem :: GFACIRC1:109

    

     Th109: for x,y,z be set st x <> [ <*y, z*>, nor2 ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, nor2 ] holds ( InputVertices ( GFA3CarryStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set MI = ( GFA3CarryIStr (x,y,z));

      

       A1: ( InputVertices S) = ( rng <*xy, yz, zx*>) by CIRCCOMB: 42

      .= {xy, yz, zx} by FINSEQ_2: 128;

      assume

       A2: x <> yz & y <> zx & z <> xy;

      

       A3: ( InnerVertices S) = {xyz} & ( {x, y, z} \ {xyz}) = {x, y, z} by Lm2, CIRCCOMB: 42;

      

       A4: ( {xy, yz, zx} \ {xy, yz, zx}) = {} by XBOOLE_1: 37;

      

      thus ( InputVertices ( GFA3CarryStr (x,y,z))) = ((( InputVertices MI) \ ( InnerVertices S)) \/ (( InputVertices S) \ ( InnerVertices MI))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ( {x, y, z} \/ ( {xy, yz, zx} \ ( InnerVertices MI))) by A1, A2, A3, Th108

      .= ( {x, y, z} \/ {} ) by A4, Th105

      .= {x, y, z};

    end;

    theorem :: GFACIRC1:110

    for x,y,z be non pair set holds ( InputVertices ( GFA3CarryStr (x,y,z))) is without_pairs

    proof

      let x,y,z be non pair set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set M = ( GFA3CarryStr (x,y,z));

      set MI = ( GFA3CarryIStr (x,y,z));

      given xx be pair object such that

       A1: xx in ( InputVertices M);

      

       A2: Cxy tolerates Cyz by CIRCCOMB: 47;

      

       A3: ( InnerVertices Czx) = {zx} & (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 42, CIRCCOMB: 47;

      ( InnerVertices Cxy) = {xy} & ( InnerVertices Cyz) = {yz} by CIRCCOMB: 42;

      then ( InnerVertices (Cxy +* Cyz)) = ( {xy} \/ {yz}) by A2, CIRCCOMB: 11;

      

      then

       A4: ( InnerVertices MI) = (( {xy} \/ {yz}) \/ {zx}) by A3, CIRCCOMB: 11

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      ( InputVertices S) = {xy, yz, zx} by FACIRC_1: 42;

      then

       A5: (( InputVertices S) \ ( InnerVertices MI)) = {} by A4, XBOOLE_1: 37;

      ( InputVertices Cxy) is without_pairs & ( InputVertices Cyz) is without_pairs by FACIRC_1: 41;

      then ( InputVertices Czx) is without_pairs & ( InputVertices (Cxy +* Cyz)) is without_pairs by FACIRC_1: 9, FACIRC_1: 41;

      then

       A6: ( InputVertices MI) is without_pairs by FACIRC_1: 9;

      ( InnerVertices S) is Relation by FACIRC_1: 38;

      then ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) by A6, FACIRC_1: 6;

      hence thesis by A6, A1, A5;

    end;

    theorem :: GFACIRC1:111

    

     Th111: for x,y,z be set holds x in the carrier of ( GFA3CarryStr (x,y,z)) & y in the carrier of ( GFA3CarryStr (x,y,z)) & z in the carrier of ( GFA3CarryStr (x,y,z)) & [ <*x, y*>, nor2 ] in the carrier of ( GFA3CarryStr (x,y,z)) & [ <*y, z*>, nor2 ] in the carrier of ( GFA3CarryStr (x,y,z)) & [ <*z, x*>, nor2 ] in the carrier of ( GFA3CarryStr (x,y,z)) & [ <* [ <*x, y*>, nor2 ], [ <*y, z*>, nor2 ], [ <*z, x*>, nor2 ]*>, nor3 ] in the carrier of ( GFA3CarryStr (x,y,z))

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set Cxyz = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      set p = <*xy, yz, zx*>;

      z in the carrier of Czx by FACIRC_1: 43;

      then

       A1: z in the carrier of ( GFA3CarryIStr (x,y,z)) by FACIRC_1: 20;

      zx in the carrier of Czx by FACIRC_1: 43;

      then

       A2: zx in the carrier of ( GFA3CarryIStr (x,y,z)) by FACIRC_1: 20;

      y in the carrier of Cxy by FACIRC_1: 43;

      then y in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A3: y in the carrier of ( GFA3CarryIStr (x,y,z)) by FACIRC_1: 20;

      the carrier of Cxyz = (( rng p) \/ {xyz}) & [p, f4] in { [p, f4]} by CIRCCOMB:def 6, TARSKI:def 1;

      then

       A4: xyz in the carrier of Cxyz by XBOOLE_0:def 3;

      yz in the carrier of Cyz by FACIRC_1: 43;

      then yz in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A5: yz in the carrier of ( GFA3CarryIStr (x,y,z)) by FACIRC_1: 20;

      xy in the carrier of Cxy by FACIRC_1: 43;

      then xy in the carrier of (Cxy +* Cyz) by FACIRC_1: 20;

      then

       A6: xy in the carrier of ( GFA3CarryIStr (x,y,z)) by FACIRC_1: 20;

      x in the carrier of Czx by FACIRC_1: 43;

      then x in the carrier of ( GFA3CarryIStr (x,y,z)) by FACIRC_1: 20;

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

    end;

    theorem :: GFACIRC1:112

    

     Th112: for x,y,z be set holds [ <*x, y*>, nor2 ] in ( InnerVertices ( GFA3CarryStr (x,y,z))) & [ <*y, z*>, nor2 ] in ( InnerVertices ( GFA3CarryStr (x,y,z))) & [ <*z, x*>, nor2 ] in ( InnerVertices ( GFA3CarryStr (x,y,z))) & ( GFA3CarryOutput (x,y,z)) in ( InnerVertices ( GFA3CarryStr (x,y,z)))

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      ( InnerVertices ( GFA3CarryStr (x,y,z))) = ( {xy, yz, zx} \/ {( GFA3CarryOutput (x,y,z))}) by Th106

      .= {xy, yz, zx, ( GFA3CarryOutput (x,y,z))} by ENUMSET1: 6;

      hence thesis by ENUMSET1:def 2;

    end;

    theorem :: GFACIRC1:113

    

     Th113: for x,y,z be set st x <> [ <*y, z*>, nor2 ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, nor2 ] holds x in ( InputVertices ( GFA3CarryStr (x,y,z))) & y in ( InputVertices ( GFA3CarryStr (x,y,z))) & z in ( InputVertices ( GFA3CarryStr (x,y,z)))

    proof

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      let x,y,z be set;

      assume x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      then ( InputVertices ( GFA3CarryStr (x,y,z))) = {x, y, z} by Th109;

      hence thesis by ENUMSET1:def 1;

    end;

    theorem :: GFACIRC1:114

    

     Th114: for x,y,z be non pair set holds ( InputVertices ( GFA3CarryStr (x,y,z))) = {x, y, z}

    proof

      let x,y,z be non pair set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 , f4 = nor3 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set Cxy = ( 1GateCircStr ( <*x, y*>,f1));

      set Cyz = ( 1GateCircStr ( <*y, z*>,f2));

      set Czx = ( 1GateCircStr ( <*z, x*>,f3));

      set M = ( GFA3CarryStr (x,y,z));

      set MI = ( GFA3CarryIStr (x,y,z));

      set S = ( 1GateCircStr ( <*xy, yz, zx*>,f4));

      

       A1: ( InputVertices Cxy) = {x, y} & ( InputVertices Cyz) = {y, z} by FACIRC_1: 40;

      

       A2: ( InputVertices Czx) = {z, x} by FACIRC_1: 40;

      

       A3: ( InputVertices S) = {xy, yz, zx} by FACIRC_1: 42;

      

       A4: ( InnerVertices S) is Relation by FACIRC_1: 38;

      

       A5: ( InnerVertices Cxy) = {xy} & ( InnerVertices Cyz) = {yz} by CIRCCOMB: 42;

      Cxy tolerates Cyz by CIRCCOMB: 47;

      then

       A6: ( InnerVertices Czx) = {zx} & ( InnerVertices (Cxy +* Cyz)) = ( {xy} \/ {yz}) by A5, CIRCCOMB: 11, CIRCCOMB: 42;

      (Cxy +* Cyz) tolerates Czx by CIRCCOMB: 47;

      

      then ( InnerVertices MI) = (( {xy} \/ {yz}) \/ {zx}) by A6, CIRCCOMB: 11

      .= ( {xy, yz} \/ {zx}) by ENUMSET1: 1

      .= {xy, yz, zx} by ENUMSET1: 3;

      then

       A7: (( InputVertices S) \ ( InnerVertices MI)) = {} by A3, XBOOLE_1: 37;

      

       A8: ( InputVertices Cxy) is without_pairs & ( InputVertices Cyz) is without_pairs by FACIRC_1: 41;

      then

       A9: ( InputVertices Czx) is without_pairs & ( InputVertices (Cxy +* Cyz)) is without_pairs by FACIRC_1: 9, FACIRC_1: 41;

      then ( InputVertices MI) is without_pairs by FACIRC_1: 9;

      then ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) by A4, FACIRC_1: 6;

      

      hence ( InputVertices M) = (( InputVertices (Cxy +* Cyz)) \/ ( InputVertices Czx)) by A9, A6, A7, FACIRC_1: 7

      .= ((( InputVertices Cxy) \/ ( InputVertices Cyz)) \/ ( InputVertices Czx)) by A8, A5, FACIRC_1: 7

      .= ( {x, y, y, z} \/ {z, x}) by A1, A2, ENUMSET1: 5

      .= ( {y, y, x, z} \/ {z, x}) by ENUMSET1: 67

      .= ( {y, x, z} \/ {z, x}) by ENUMSET1: 31

      .= ( {x, y, z} \/ {z, x}) by ENUMSET1: 58

      .= ( {x, y, z} \/ ( {z} \/ {x})) by ENUMSET1: 1

      .= (( {x, y, z} \/ {z}) \/ {x}) by XBOOLE_1: 4

      .= (( {z, x, y} \/ {z}) \/ {x}) by ENUMSET1: 59

      .= ( {z, z, x, y} \/ {x}) by ENUMSET1: 4

      .= ( {z, x, y} \/ {x}) by ENUMSET1: 31

      .= ( {x, y, z} \/ {x}) by ENUMSET1: 59

      .= {x, x, y, z} by ENUMSET1: 4

      .= {x, y, z} by ENUMSET1: 31;

    end;

    theorem :: GFACIRC1:115

    

     Th115: for x,y,z be set holds for s be State of ( GFA3CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following s) . [ <*x, y*>, nor2 ]) = (( 'not' a1) '&' ( 'not' a2)) & (( Following s) . [ <*y, z*>, nor2 ]) = (( 'not' a2) '&' ( 'not' a3)) & (( Following s) . [ <*z, x*>, nor2 ]) = (( 'not' a3) '&' ( 'not' a1))

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      let s be State of ( GFA3CarryCirc (x,y,z));

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

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

       A1: a1 = (s . x) and

       A2: a2 = (s . y) and

       A3: a3 = (s . z);

      set S = ( GFA3CarryStr (x,y,z));

      

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

      

       A5: y in the carrier of S by Th111;

      

       A6: x in the carrier of S by Th111;

      

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

      xy in ( InnerVertices ( GFA3CarryStr (x,y,z))) by Th112;

      

      hence (( Following s) . [ <*x, y*>, f1]) = (f1 . (s * <*x, y*>)) by A4, FACIRC_1: 35

      .= (f1 . <*a1, a2*>) by A1, A2, A7, A6, A5, FINSEQ_2: 125

      .= (( 'not' a1) '&' ( 'not' a2)) by TWOSCOMP: 54;

      

       A8: z in the carrier of S by Th111;

      yz in ( InnerVertices ( GFA3CarryStr (x,y,z))) by Th112;

      

      hence (( Following s) . [ <*y, z*>, f2]) = (f2 . (s * <*y, z*>)) by A4, FACIRC_1: 35

      .= (f2 . <*a2, a3*>) by A2, A3, A7, A5, A8, FINSEQ_2: 125

      .= (( 'not' a2) '&' ( 'not' a3)) by TWOSCOMP: 54;

      zx in ( InnerVertices ( GFA3CarryStr (x,y,z))) by Th112;

      

      hence (( Following s) . [ <*z, x*>, f3]) = (f3 . (s * <*z, x*>)) by A4, FACIRC_1: 35

      .= (f3 . <*a3, a1*>) by A1, A3, A7, A6, A8, FINSEQ_2: 125

      .= (( 'not' a3) '&' ( 'not' a1)) by TWOSCOMP: 54;

    end;

    theorem :: GFACIRC1:116

    

     Th116: for x,y,z be set holds for s be State of ( GFA3CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . [ <*x, y*>, nor2 ]) & a2 = (s . [ <*y, z*>, nor2 ]) & a3 = (s . [ <*z, x*>, nor2 ]) holds (( Following s) . ( GFA3CarryOutput (x,y,z))) = ( 'not' ((a1 'or' a2) 'or' a3))

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 , f4 = nor3 ;

      let s be State of ( GFA3CarryCirc (x,y,z));

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

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

       A1: a1 = (s . xy) & a2 = (s . yz) & a3 = (s . zx);

      set S = ( GFA3CarryStr (x,y,z));

      reconsider xy, yz, zx as Element of ( InnerVertices S) by Th112;

      

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

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

      

      hence (( Following s) . ( GFA3CarryOutput (x,y,z))) = (f4 . (s * <*xy, yz, zx*>)) by FACIRC_1: 35

      .= (f4 . <*a1, a2, a3*>) by A1, A2, FINSEQ_2: 126

      .= ( 'not' ((a1 'or' a2) 'or' a3)) by TWOSCOMP:def 28;

    end;

    theorem :: GFACIRC1:117

    

     Th117: for x,y,z be set st x <> [ <*y, z*>, nor2 ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, nor2 ] holds for s be State of ( GFA3CarryCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA3CarryOutput (x,y,z))) = ( 'not' (((( 'not' a1) '&' ( 'not' a2)) 'or' (( 'not' a2) '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1)))) & (( Following (s,2)) . [ <*x, y*>, nor2 ]) = (( 'not' a1) '&' ( 'not' a2)) & (( Following (s,2)) . [ <*y, z*>, nor2 ]) = (( 'not' a2) '&' ( 'not' a3)) & (( Following (s,2)) . [ <*z, x*>, nor2 ]) = (( 'not' a3) '&' ( 'not' a1))

    proof

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      let x,y,z be set such that

       A1: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( GFA3CarryStr (x,y,z));

      reconsider x9 = x, y9 = y, z9 = z as Vertex of S by Th111;

      let s be State of ( GFA3CarryCirc (x,y,z));

      y in ( InputVertices S) by A1, Th113;

      then

       A2: (( Following s) . y9) = (s . y) by CIRCUIT2:def 5;

      z in ( InputVertices S) by A1, Th113;

      then

       A3: (( Following s) . z9) = (s . z) by CIRCUIT2:def 5;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      

       A4: ( Following (s,2)) = ( Following ( Following s)) by FACIRC_1: 15;

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

       A5: a1 = (s . x) & a2 = (s . y) & a3 = (s . z);

      

       A6: (( Following s) . zx) = (( 'not' a3) '&' ( 'not' a1)) by A5, Th115;

      (( Following s) . xy) = (( 'not' a1) '&' ( 'not' a2)) & (( Following s) . yz) = (( 'not' a2) '&' ( 'not' a3)) by A5, Th115;

      hence (( Following (s,2)) . ( GFA3CarryOutput (x,y,z))) = ( 'not' (((( 'not' a1) '&' ( 'not' a2)) 'or' (( 'not' a2) '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1)))) by A4, A6, Th116;

      x in ( InputVertices S) by A1, Th113;

      then (( Following s) . x9) = (s . x) by CIRCUIT2:def 5;

      hence thesis by A5, A2, A3, A4, Th115;

    end;

    theorem :: GFACIRC1:118

    

     Th118: for x,y,z be set st x <> [ <*y, z*>, nor2 ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, nor2 ] holds for s be State of ( GFA3CarryCirc (x,y,z)) holds ( Following (s,2)) is stable

    proof

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      let x,y,z be set such that

       A1: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( GFA3CarryStr (x,y,z));

      reconsider xx = x, yy = y, zz = z as Vertex of S by Th111;

      let s be State of ( GFA3CarryCirc (x,y,z));

      set a1 = (s . xx), a2 = (s . yy), a3 = (s . zz);

      set ffs = ( Following (s,2)), fffs = ( Following ffs);

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      

       A2: ffs = ( Following ( Following s)) by FACIRC_1: 15;

      

       A3: z in ( InputVertices S) by A1, Th113;

      then (( Following s) . z) = a3 by CIRCUIT2:def 5;

      then

       A4: (ffs . z) = a3 by A2, A3, CIRCUIT2:def 5;

      

       A5: y in ( InputVertices S) by A1, Th113;

      then (( Following s) . y) = a2 by CIRCUIT2:def 5;

      then

       A6: (ffs . y) = a2 by A2, A5, CIRCUIT2:def 5;

      

       A7: x in ( InputVertices S) by A1, Th113;

      then (( Following s) . x) = a1 by CIRCUIT2:def 5;

      then

       A8: (ffs . x) = a1 by A2, A7, CIRCUIT2:def 5;

      a3 = (s . z);

      then

       A9: (ffs . xy) = (( 'not' a1) '&' ( 'not' a2)) by A1, Th117;

      a2 = (s . y);

      then

       A10: (ffs . zx) = (( 'not' a1) '&' ( 'not' a3)) by A1, Th117;

      a1 = (s . x);

      then

       A11: (ffs . yz) = (( 'not' a2) '&' ( 'not' a3)) by A1, Th117;

      

       A12: (ffs . ( GFA3CarryOutput (x,y,z))) = ( 'not' (((( 'not' a1) '&' ( 'not' a2)) 'or' (( 'not' a2) '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1)))) by A1, Th117;

       A13:

      now

        let a be object;

        assume

         A14: a in the carrier of S;

        then

        reconsider v = a as Vertex of S;

        

         A15: v in (( InputVertices S) \/ ( InnerVertices S)) by A14, XBOOLE_1: 45;

        thus (ffs . a) = (fffs . a)

        proof

          per cases by A15, XBOOLE_0:def 3;

            suppose v in ( InputVertices S);

            hence thesis by CIRCUIT2:def 5;

          end;

            suppose v in ( InnerVertices S);

            then v in ( {xy, yz, zx} \/ {( GFA3CarryOutput (x,y,z))}) by Th106;

            then v in {xy, yz, zx} or v in {( GFA3CarryOutput (x,y,z))} by XBOOLE_0:def 3;

            then v = xy or v = yz or v = zx or v = ( GFA3CarryOutput (x,y,z)) by ENUMSET1:def 1, TARSKI:def 1;

            hence thesis by A12, A9, A11, A10, A8, A6, A4, Th115, Th116;

          end;

        end;

      end;

      ( dom ( Following ( Following (s,2)))) = the carrier of S & ( dom ( Following (s,2))) = the carrier of S by CIRCUIT1: 3;

      hence ffs = fffs by A13, FUNCT_1: 2;

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def46

      func GFA3AdderStr (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ( 2GatesCircStr (x,y,z, xor2 ));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def47

      func GFA3AdderCirc (x,y,z) -> strict Boolean gate`2=den Circuit of ( GFA3AdderStr (x,y,z)) equals ( 2GatesCircuit (x,y,z, xor2 ));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def48

      func GFA3AdderOutput (x,y,z) -> Element of ( InnerVertices ( GFA3AdderStr (x,y,z))) equals ( 2GatesCircOutput (x,y,z, xor2 ));

      coherence ;

    end

    theorem :: GFACIRC1:119

    

     Th119: for x,y,z be set holds ( InnerVertices ( GFA3AdderStr (x,y,z))) = ( { [ <*x, y*>, xor2 ]} \/ {( GFA3AdderOutput (x,y,z))})

    proof

      let x,y,z be set;

      ( GFA3AdderOutput (x,y,z)) = ( GFA0AdderOutput (x,y,z));

      hence thesis by Th24;

    end;

    theorem :: GFACIRC1:120

    for x,y,z be set holds x in the carrier of ( GFA3AdderStr (x,y,z)) & y in the carrier of ( GFA3AdderStr (x,y,z)) & z in the carrier of ( GFA3AdderStr (x,y,z)) & [ <*x, y*>, xor2 ] in the carrier of ( GFA3AdderStr (x,y,z)) & [ <* [ <*x, y*>, xor2 ], z*>, xor2 ] in the carrier of ( GFA3AdderStr (x,y,z)) by FACIRC_1: 60, FACIRC_1: 61;

    theorem :: GFACIRC1:121

    for x,y,z be set holds [ <*x, y*>, xor2 ] in ( InnerVertices ( GFA3AdderStr (x,y,z))) & ( GFA3AdderOutput (x,y,z)) in ( InnerVertices ( GFA3AdderStr (x,y,z)))

    proof

      let x,y,z be set;

      set S0 = ( GFA0AdderStr (x,y,z));

      ( GFA3AdderStr (x,y,z)) = S0;

      hence thesis by Th26;

    end;

    theorem :: GFACIRC1:122

    for x,y,z be set st z <> [ <*x, y*>, xor2 ] holds x in ( InputVertices ( GFA3AdderStr (x,y,z))) & y in ( InputVertices ( GFA3AdderStr (x,y,z))) & z in ( InputVertices ( GFA3AdderStr (x,y,z)))

    proof

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, xor2 ];

      set S0 = ( GFA0AdderStr (x,y,z));

      ( GFA3AdderStr (x,y,z)) = S0;

      hence thesis by A1, Th27;

    end;

    theorem :: GFACIRC1:123

    for x,y,z be set st z <> [ <*x, y*>, xor2 ] holds for s be State of ( GFA3AdderCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following s) . [ <*x, y*>, xor2 ]) = (a1 'xor' a2) & (( Following s) . x) = a1 & (( Following s) . y) = a2 & (( Following s) . z) = a3

    proof

      set f = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set A0 = ( GFA0AdderCirc (x,y,z));

      set A3 = ( GFA3AdderCirc (x,y,z));

      A3 = A0;

      hence thesis by A1, Th28;

    end;

    theorem :: GFACIRC1:124

    for x,y,z be set st z <> [ <*x, y*>, xor2 ] holds for s be State of ( GFA3AdderCirc (x,y,z)) holds for a1a2,a1,a2,a3 be Element of BOOLEAN st a1a2 = (s . [ <*x, y*>, xor2 ]) & a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following s) . ( GFA3AdderOutput (x,y,z))) = (a1a2 'xor' a3)

    proof

      set f = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

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

      set O3 = ( GFA3AdderOutput (x,y,z));

      set A0 = ( GFA0AdderCirc (x,y,z));

      set A3 = ( GFA3AdderCirc (x,y,z));

      A3 = A0 & O3 = O0;

      hence thesis by A1, Th29;

    end;

    theorem :: GFACIRC1:125

    

     Th125: for x,y,z be set st z <> [ <*x, y*>, xor2 ] holds for s be State of ( GFA3AdderCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA3AdderOutput (x,y,z))) = ((a1 'xor' a2) 'xor' a3) & (( Following (s,2)) . [ <*x, y*>, xor2 ]) = (a1 'xor' a2) & (( Following (s,2)) . x) = a1 & (( Following (s,2)) . y) = a2 & (( Following (s,2)) . z) = a3

    proof

      set f = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

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

      set O3 = ( GFA3AdderOutput (x,y,z));

      set A0 = ( GFA0AdderCirc (x,y,z));

      set A3 = ( GFA3AdderCirc (x,y,z));

      A3 = A0 & O3 = O0;

      hence thesis by A1, Th30;

    end;

    theorem :: GFACIRC1:126

    

     Th126: for x,y,z be set st z <> [ <*x, y*>, xor2 ] holds for s be State of ( GFA3AdderCirc (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA3AdderOutput (x,y,z))) = ( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3)))

    proof

      set f = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f];

      set A = ( GFA3AdderCirc (x,y,z));

      let s be State of A;

      let a1,a2,a3 be Element of BOOLEAN ;

      assume a1 = (s . x) & a2 = (s . y) & a3 = (s . z);

      

      hence (( Following (s,2)) . ( GFA3AdderOutput (x,y,z))) = ((a1 'xor' a2) 'xor' a3) by A1, Th125

      .= ( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) by XBOOLEAN: 74;

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def49

      func BitGFA3Str (x,y,z) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( GFA3AdderStr (x,y,z)) +* ( GFA3CarryStr (x,y,z)));

      coherence ;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def50

      func BitGFA3Circ (x,y,z) -> strict Boolean gate`2=den Circuit of ( BitGFA3Str (x,y,z)) equals (( GFA3AdderCirc (x,y,z)) +* ( GFA3CarryCirc (x,y,z)));

      coherence ;

    end

    theorem :: GFACIRC1:127

    

     Th127: for x,y,z be set holds ( InnerVertices ( BitGFA3Str (x,y,z))) = ((( { [ <*x, y*>, xor2 ]} \/ {( GFA3AdderOutput (x,y,z))}) \/ { [ <*x, y*>, nor2 ], [ <*y, z*>, nor2 ], [ <*z, x*>, nor2 ]}) \/ {( GFA3CarryOutput (x,y,z))})

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      set f0 = xor2 ;

      set xyf0 = [ <*x, y*>, f0];

      set xyf1 = [ <*x, y*>, f1], yzf2 = [ <*y, z*>, f2], zxf3 = [ <*z, x*>, f3];

      set S = ( BitGFA3Str (x,y,z));

      set S1 = ( GFA3AdderStr (x,y,z));

      set S2 = ( GFA3CarryStr (x,y,z));

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

      set A2 = ( GFA3CarryOutput (x,y,z));

      

      thus ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by FACIRC_1: 27

      .= (( {xyf0} \/ {A1}) \/ ( InnerVertices S2)) by Th119

      .= (( {xyf0} \/ {A1}) \/ ( {xyf1, yzf2, zxf3} \/ {A2})) by Th106

      .= ((( {xyf0} \/ {A1}) \/ {xyf1, yzf2, zxf3}) \/ {A2}) by XBOOLE_1: 4;

    end;

    theorem :: GFACIRC1:128

    for x,y,z be set holds ( InnerVertices ( BitGFA3Str (x,y,z))) is Relation

    proof

      let x,y,z be set;

      set S1 = ( GFA3AdderStr (x,y,z));

      set S2 = ( GFA3CarryStr (x,y,z));

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by Th107, FACIRC_1: 58;

      hence thesis by FACIRC_1: 3;

    end;

    theorem :: GFACIRC1:129

    

     Th129: for x,y,z be set st z <> [ <*x, y*>, xor2 ] & x <> [ <*y, z*>, nor2 ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, nor2 ] holds ( InputVertices ( BitGFA3Str (x,y,z))) = {x, y, z}

    proof

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      set f0 = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] & x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S2 = ( GFA3CarryStr (x,y,z));

      set S1 = ( GFA3AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} & ( InputVertices S2) = {x, y, z} by A1, Th109, FACIRC_1: 57;

      hence thesis by CIRCCOMB: 47, FACIRC_2: 21;

    end;

    theorem :: GFACIRC1:130

    

     Th130: for x,y,z be non pair set holds ( InputVertices ( BitGFA3Str (x,y,z))) = {x, y, z}

    proof

      let x,y,z be non pair set;

      set S = ( BitGFA3Str (x,y,z));

      set S1 = ( GFA3AdderStr (x,y,z));

      set S2 = ( GFA3CarryStr (x,y,z));

      

       A1: ( InputVertices S1) = {x, y, z} & ( InputVertices S2) = {x, y, z} by Th114, FACIRC_1: 57;

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by Th107, FACIRC_1: 58;

      

      hence ( InputVertices S) = ( {x, y, z} \/ {x, y, z}) by A1, FACIRC_1: 7

      .= {x, y, z};

    end;

    theorem :: GFACIRC1:131

    for x,y,z be non pair set holds ( InputVertices ( BitGFA3Str (x,y,z))) is without_pairs

    proof

      let x,y,z be non pair set;

      ( InputVertices ( BitGFA3Str (x,y,z))) = {x, y, z} by Th130;

      hence thesis;

    end;

    theorem :: GFACIRC1:132

    for x,y,z be set holds x in the carrier of ( BitGFA3Str (x,y,z)) & y in the carrier of ( BitGFA3Str (x,y,z)) & z in the carrier of ( BitGFA3Str (x,y,z)) & [ <*x, y*>, xor2 ] in the carrier of ( BitGFA3Str (x,y,z)) & [ <* [ <*x, y*>, xor2 ], z*>, xor2 ] in the carrier of ( BitGFA3Str (x,y,z)) & [ <*x, y*>, nor2 ] in the carrier of ( BitGFA3Str (x,y,z)) & [ <*y, z*>, nor2 ] in the carrier of ( BitGFA3Str (x,y,z)) & [ <*z, x*>, nor2 ] in the carrier of ( BitGFA3Str (x,y,z)) & [ <* [ <*x, y*>, nor2 ], [ <*y, z*>, nor2 ], [ <*z, x*>, nor2 ]*>, nor3 ] in the carrier of ( BitGFA3Str (x,y,z))

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 , f4 = nor3 ;

      set f0 = xor2 ;

      set xy = [ <*x, y*>, f1], yz = [ <*y, z*>, f2], zx = [ <*z, x*>, f3];

      set xyz = [ <*xy, yz, zx*>, f4];

      set S1 = ( GFA3AdderStr (x,y,z));

      set S2 = ( GFA3CarryStr (x,y,z));

      

       A1: x in the carrier of S1 & y in the carrier of S1 by FACIRC_1: 60;

      

       A2: z in the carrier of S1 & [ <*x, y*>, f0] in the carrier of S1 by FACIRC_1: 60, FACIRC_1: 61;

      

       A3: xyz in the carrier of S2 by Th111;

      

       A4: yz in the carrier of S2 & zx in the carrier of S2 by Th111;

       [ <* [ <*x, y*>, f0], z*>, f0] in the carrier of S1 & xy in the carrier of S2 by Th111, FACIRC_1: 61;

      hence thesis by A1, A2, A4, A3, FACIRC_1: 20;

    end;

    theorem :: GFACIRC1:133

    

     Th133: for x,y,z be set holds [ <*x, y*>, xor2 ] in ( InnerVertices ( BitGFA3Str (x,y,z))) & ( GFA3AdderOutput (x,y,z)) in ( InnerVertices ( BitGFA3Str (x,y,z))) & [ <*x, y*>, nor2 ] in ( InnerVertices ( BitGFA3Str (x,y,z))) & [ <*y, z*>, nor2 ] in ( InnerVertices ( BitGFA3Str (x,y,z))) & [ <*z, x*>, nor2 ] in ( InnerVertices ( BitGFA3Str (x,y,z))) & ( GFA3CarryOutput (x,y,z)) in ( InnerVertices ( BitGFA3Str (x,y,z)))

    proof

      let x,y,z be set;

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      set f0 = xor2 ;

      set xyf0 = [ <*x, y*>, f0];

      set xyf1 = [ <*x, y*>, f1], yzf2 = [ <*y, z*>, f2], zxf3 = [ <*z, x*>, f3];

      set S = ( BitGFA3Str (x,y,z));

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

      set A2 = ( GFA3CarryOutput (x,y,z));

      ( InnerVertices S) = ((( {xyf0} \/ {A1}) \/ {xyf1, yzf2, zxf3}) \/ {A2}) by Th127

      .= (( {xyf0, A1} \/ {xyf1, yzf2, zxf3}) \/ {A2}) by ENUMSET1: 1

      .= ( {xyf0, A1, xyf1, yzf2, zxf3} \/ {A2}) by ENUMSET1: 8

      .= {xyf0, A1, xyf1, yzf2, zxf3, A2} by ENUMSET1: 15;

      hence thesis by ENUMSET1:def 4;

    end;

    theorem :: GFACIRC1:134

    for x,y,z be set st z <> [ <*x, y*>, xor2 ] & x <> [ <*y, z*>, nor2 ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, nor2 ] holds x in ( InputVertices ( BitGFA3Str (x,y,z))) & y in ( InputVertices ( BitGFA3Str (x,y,z))) & z in ( InputVertices ( BitGFA3Str (x,y,z)))

    proof

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      set f0 = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] & x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S = ( BitGFA3Str (x,y,z));

      ( InputVertices S) = {x, y, z} by A1, Th129;

      hence thesis by ENUMSET1:def 1;

    end;

    definition

      let x,y,z be set;

      :: GFACIRC1:def51

      func BitGFA3CarryOutput (x,y,z) -> Element of ( InnerVertices ( BitGFA3Str (x,y,z))) equals [ <* [ <*x, y*>, nor2 ], [ <*y, z*>, nor2 ], [ <*z, x*>, nor2 ]*>, nor3 ];

      coherence

      proof

        ( GFA3CarryOutput (x,y,z)) in ( InnerVertices ( BitGFA3Str (x,y,z))) by Th133;

        hence thesis;

      end;

    end

    definition

      let x,y,z be set;

      :: GFACIRC1:def52

      func BitGFA3AdderOutput (x,y,z) -> Element of ( InnerVertices ( BitGFA3Str (x,y,z))) equals ( 2GatesCircOutput (x,y,z, xor2 ));

      coherence

      proof

        ( GFA3AdderOutput (x,y,z)) in ( InnerVertices ( BitGFA3Str (x,y,z))) by Th133;

        hence thesis;

      end;

    end

    theorem :: GFACIRC1:135

    for x,y,z be set st z <> [ <*x, y*>, xor2 ] & x <> [ <*y, z*>, nor2 ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, nor2 ] holds for s be State of ( BitGFA3Circ (x,y,z)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . z) holds (( Following (s,2)) . ( GFA3AdderOutput (x,y,z))) = ( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) & (( Following (s,2)) . ( GFA3CarryOutput (x,y,z))) = ( 'not' (((( 'not' a1) '&' ( 'not' a2)) 'or' (( 'not' a2) '&' ( 'not' a3))) 'or' (( 'not' a3) '&' ( 'not' a1))))

    proof

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      set f0 = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] and

       A2: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set S2 = ( GFA3CarryStr (x,y,z));

      set S1 = ( GFA3AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} by A1, FACIRC_1: 57;

      then

       A3: ( InputVertices S1) = ( InputVertices S2) by A2, Th109;

      set A2 = ( GFA3CarryCirc (x,y,z));

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

      set A = ( BitGFA3Circ (x,y,z));

      let s be State of A;

      let a1,a2,a3 be Element of BOOLEAN ;

      assume that

       A4: a1 = (s . x) and

       A5: a2 = (s . y) and

       A6: a3 = (s . z);

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

      

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

      z in the carrier of S1 by FACIRC_1: 60;

      then

       A8: a3 = (s1 . z) by A6, A7, FUNCT_1: 47;

      y in the carrier of S1 by FACIRC_1: 60;

      then

       A9: a2 = (s1 . y) by A5, A7, FUNCT_1: 47;

      reconsider t = s as State of (A1 +* A2);

      ( InnerVertices S2) misses ( InputVertices S2) by XBOOLE_1: 79;

      then

       A10: (( Following (t,2)) . ( GFA3AdderOutput (x,y,z))) = (( Following (s1,2)) . ( GFA3AdderOutput (x,y,z))) by A3, FACIRC_1: 32;

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      

       A11: ( dom s2) = the carrier of S2 by CIRCUIT1: 3;

      x in the carrier of S1 by FACIRC_1: 60;

      then a1 = (s1 . x) by A4, A7, FUNCT_1: 47;

      hence (( Following (s,2)) . ( GFA3AdderOutput (x,y,z))) = ( 'not' ((( 'not' a1) 'xor' ( 'not' a2)) 'xor' ( 'not' a3))) by A1, A9, A8, A10, Th126;

      ( InnerVertices S1) misses ( InputVertices S1) by XBOOLE_1: 79;

      then

       A12: (( Following (t,2)) . ( GFA3CarryOutput (x,y,z))) = (( Following (s2,2)) . ( GFA3CarryOutput (x,y,z))) by A3, FACIRC_1: 33;

      z in the carrier of S2 by Th111;

      then

       A13: a3 = (s2 . z) by A6, A11, FUNCT_1: 47;

      y in the carrier of S2 by Th111;

      then

       A14: a2 = (s2 . y) by A5, A11, FUNCT_1: 47;

      x in the carrier of S2 by Th111;

      then a1 = (s2 . x) by A4, A11, FUNCT_1: 47;

      hence thesis by A2, A14, A13, A12, Th117;

    end;

    theorem :: GFACIRC1:136

    for x,y,z be set st z <> [ <*x, y*>, xor2 ] & x <> [ <*y, z*>, nor2 ] & y <> [ <*z, x*>, nor2 ] & z <> [ <*x, y*>, nor2 ] holds for s be State of ( BitGFA3Circ (x,y,z)) holds ( Following (s,2)) is stable

    proof

      set f1 = nor2 , f2 = nor2 , f3 = nor2 ;

      set f0 = xor2 ;

      let x,y,z be set such that

       A1: z <> [ <*x, y*>, f0] and

       A2: x <> [ <*y, z*>, f2] & y <> [ <*z, x*>, f3] & z <> [ <*x, y*>, f1];

      set A = ( BitGFA3Circ (x,y,z));

      let s be State of A;

      set S2 = ( GFA3CarryStr (x,y,z));

      set S1 = ( GFA3AdderStr (x,y,z));

      ( InputVertices S1) = {x, y, z} by A1, FACIRC_1: 57;

      then

       A3: ( InputVertices S1) = ( InputVertices S2) by A2, Th109;

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

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

      ( Following (s1,2)) is stable by A1, FACIRC_1: 63;

      

      then

       A4: ( Following (s1,2)) = ( Following ( Following (s1,2)))

      .= ( Following (s1,(2 + 1))) by FACIRC_1: 12;

      set A2 = ( GFA3CarryCirc (x,y,z));

      reconsider s2 = (s | the carrier of S2) as State of A2 by FACIRC_1: 26;

      ( Following (s2,2)) is stable by A2, Th118;

      

      then

       A5: ( Following (s2,2)) = ( Following ( Following (s2,2)))

      .= ( Following (s2,(2 + 1))) by FACIRC_1: 12;

      reconsider t = s as State of (A1 +* A2);

      set S = ( BitGFA3Str (x,y,z));

      

       A6: ( dom ( Following (s,3))) = the carrier of S by CIRCUIT1: 3;

      ( InnerVertices S2) misses ( InputVertices S2) by XBOOLE_1: 79;

      then

       A7: ( Following (s1,2)) = (( Following (t,2)) | the carrier of S1) & ( Following (s1,3)) = (( Following (t,3)) | the carrier of S1) by A3, FACIRC_1: 30;

      ( InnerVertices S1) misses ( InputVertices S1) by XBOOLE_1: 79;

      then

       A8: ( Following (s2,2)) = (( Following (t,2)) | the carrier of S2) & ( Following (s2,3)) = (( Following (t,3)) | the carrier of S2) by A3, FACIRC_1: 31;

      

       A9: the carrier of S = (the carrier of S1 \/ the carrier of S2) by CIRCCOMB:def 2;

      

       A10: ( dom ( Following (s1,2))) = the carrier of S1 & ( dom ( Following (s2,2))) = the carrier of S2 by CIRCUIT1: 3;

       A11:

      now

        let a be object;

        assume a in the carrier of S;

        then a in the carrier of S1 or a in the carrier of S2 by A9, XBOOLE_0:def 3;

        then (( Following (s,2)) . a) = (( Following (s1,2)) . a) & (( Following (s,3)) . a) = (( Following (s1,3)) . a) or (( Following (s,2)) . a) = (( Following (s2,2)) . a) & (( Following (s,3)) . a) = (( Following (s2,3)) . a) by A7, A8, A4, A5, A10, FUNCT_1: 47;

        hence (( Following (s,2)) . a) = (( Following ( Following (s,2))) . a) by A4, A5, FACIRC_1: 12;

      end;

      ( Following (s,(2 + 1))) = ( Following ( Following (s,2))) & ( dom ( Following (s,2))) = the carrier of S by CIRCUIT1: 3, FACIRC_1: 12;

      hence ( Following (s,2)) = ( Following ( Following (s,2))) by A6, A11, FUNCT_1: 2;

    end;