facirc_1.miz



    begin

    registration

      cluster pair -> non empty for set;

      coherence

      proof

        let z be set;

        given x,y be object such that

         A1: z = [x, y];

        thus thesis by A1;

      end;

    end

    registration

      cluster non pair for object;

      existence

      proof

        take {} ;

        let x,y be object;

        thus thesis;

      end;

    end

    registration

      cluster -> non pair for Nat;

      coherence

      proof

        let n be Nat;

        given x,y be object such that

         A1: n = [x, y];

        n <> 0 by A1;

        then 0 < n;

        then 0 in ( Segm n) by NAT_1: 44;

        hence contradiction by A1, TARSKI:def 2;

      end;

    end

    definition

      ::$Canceled

      let IT be set;

      :: FACIRC_1:def2

      attr IT is with_pair means

      : Def1: ex x be pair object st x in IT;

    end

    notation

      let IT be set;

      antonym IT is without_pairs for IT is with_pair;

    end

    registration

      cluster empty -> without_pairs for set;

      coherence ;

      let x be non pair object;

      cluster {x} -> without_pairs;

      coherence by TARSKI:def 1;

      let y be non pair object;

      cluster {x, y} -> without_pairs;

      coherence by TARSKI:def 2;

      let z be non pair object;

      cluster {x, y, z} -> without_pairs;

      coherence by ENUMSET1:def 1;

    end

    registration

      cluster without_pairs for non empty set;

      existence

      proof

        set x = the non pair set;

        take {x};

        thus thesis;

      end;

    end

    registration

      let X,Y be without_pairs set;

      cluster (X \/ Y) -> without_pairs;

      coherence

      proof

        let a be pair object;

        assume a in (X \/ Y);

        then a in X or a in Y by XBOOLE_0:def 3;

        hence contradiction by Def1;

      end;

    end

    registration

      let X be without_pairs set, Y be set;

      cluster (X \ Y) -> without_pairs;

      coherence by Def1;

      cluster (X /\ Y) -> without_pairs;

      coherence

      proof

        let a be pair object;

        assume a in (X /\ Y);

        then a in X by XBOOLE_0:def 4;

        hence contradiction by Def1;

      end;

      cluster (Y /\ X) -> without_pairs;

      coherence ;

    end

    registration

      let x be pair object;

      cluster {x} -> Relation-like;

      coherence

      proof

        let a be object;

        assume a in {x};

        then a = x by TARSKI:def 1;

        then ex y,z be object st a = [y, z] by XTUPLE_0:def 1;

        hence thesis;

      end;

      let y be pair object;

      cluster {x, y} -> Relation-like;

      coherence

      proof

        let a be object;

        assume a in {x, y};

        then a = x or a = y by TARSKI:def 2;

        then ex y,z be object st a = [y, z] by XTUPLE_0:def 1;

        hence thesis;

      end;

      let z be pair object;

      cluster {x, y, z} -> Relation-like;

      coherence

      proof

        let a be object;

        assume a in {x, y, z};

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

        then ex y,z be object st a = [y, z] by XTUPLE_0:def 1;

        hence thesis;

      end;

    end

    registration

      cluster without_pairs Relation-like -> empty for set;

      coherence

      proof

        let x be set;

        assume

         A1: not ex a be pair object st a in x;

        assume

         A2: for a be object st a in x holds ex y,z be object st a = [y, z];

        assume x is non empty;

        then

        reconsider X = x as non empty set;

        set a = the Element of X;

        ex y,z be object st a = [y, z] by A2;

        hence contradiction by A1;

      end;

    end

    definition

      let IT be Function;

      :: FACIRC_1:def3

      attr IT is nonpair-yielding means for x be set st x in ( dom IT) holds (IT . x) is non pair;

    end

    registration

      let x be non pair object;

      cluster <*x*> -> nonpair-yielding;

      coherence

      proof

        let a be set;

        assume a in ( dom <*x*>);

        then ( <*x*> . a) in ( rng <*x*>) by FUNCT_1:def 3;

        then ( <*x*> . a) in {x} by FINSEQ_1: 39;

        hence thesis by TARSKI:def 1;

      end;

      let y be non pair object;

      cluster <*x, y*> -> nonpair-yielding;

      coherence

      proof

        let a be set;

        assume a in ( dom <*x, y*>);

        then ( <*x, y*> . a) in ( rng <*x, y*>) by FUNCT_1:def 3;

        then ( <*x, y*> . a) in {x, y} by FINSEQ_2: 127;

        hence thesis by TARSKI:def 2;

      end;

      let z be non pair object;

      cluster <*x, y, z*> -> nonpair-yielding;

      coherence

      proof

        let a be set;

        assume a in ( dom <*x, y, z*>);

        then ( <*x, y, z*> . a) in ( rng <*x, y, z*>) by FUNCT_1:def 3;

        then ( <*x, y, z*> . a) in {x, y, z} by FINSEQ_2: 128;

        hence thesis by ENUMSET1:def 1;

      end;

    end

    theorem :: FACIRC_1:1

    

     Th1: for f be Function st f is nonpair-yielding holds ( rng f) is without_pairs

    proof

      let f be Function;

      assume

       A1: for x be set st x in ( dom f) holds (f . x) is non pair;

      let y be pair object;

      assume y in ( rng f);

      then ex x be object st x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

      hence thesis by A1;

    end;

    registration

      let n be Nat;

      cluster one-to-one nonpair-yielding for FinSeqLen of n;

      existence

      proof

        reconsider p = ( id ( Seg n)) as FinSequence by FINSEQ_2: 48;

        ( len p) = ( len ( idseq n)) by FINSEQ_2:def 1

        .= n by CARD_1:def 7;

        then

        reconsider p as FinSeqLen of n by CARD_1:def 7;

        take p;

        thus p is one-to-one;

        let x be set;

        assume

         A1: x in ( dom p);

        x in ( Seg n) by A1;

        hence thesis by FUNCT_1: 17;

      end;

    end

    registration

      cluster one-to-one nonpair-yielding for FinSequence;

      existence

      proof

        set n = the Nat, p = the one-to-one nonpair-yielding FinSeqLen of n;

        take p;

        thus thesis;

      end;

    end

    registration

      let f be nonpair-yielding Function;

      cluster ( rng f) -> without_pairs;

      coherence by Th1;

    end

    theorem :: FACIRC_1:2

    

     Th2: for S1,S2 be non empty ManySortedSign st S1 tolerates S2 & ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation holds ( InnerVertices (S1 +* S2)) is Relation

    proof

      let S1,S2 be non empty ManySortedSign;

      assume

       A1: S1 tolerates S2;

      assume ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation;

      then

      reconsider R1 = ( InnerVertices S1), R2 = ( InnerVertices S2) as Relation;

      (R1 \/ R2) is Relation;

      hence thesis by A1, CIRCCOMB: 11;

    end;

    theorem :: FACIRC_1:3

    for S1,S2 be unsplit gate`1=arity non empty ManySortedSign st ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation holds ( InnerVertices (S1 +* S2)) is Relation by Th2, CIRCCOMB: 47;

    theorem :: FACIRC_1:4

    

     Th4: for S1,S2 be non empty ManySortedSign st S1 tolerates S2 & ( InnerVertices S2) misses ( InputVertices S1) holds ( InputVertices S1) c= ( InputVertices (S1 +* S2)) & ( InputVertices (S1 +* S2)) = (( InputVertices S1) \/ (( InputVertices S2) \ ( InnerVertices S1)))

    proof

      let S1,S2 be non empty ManySortedSign;

      set S = (S1 +* S2);

      set R = the ResultSort of S;

      set R1 = the ResultSort of S1;

      set R2 = the ResultSort of S2;

      assume that

       A1: S1 tolerates S2 and

       A2: ( InnerVertices S2) misses ( InputVertices S1);

      

       A3: ( InnerVertices S) = ( rng R);

      ( InnerVertices S1) = ( rng R1) & ( InnerVertices S2) = ( rng R2);

      then

       A4: ( rng R) = (( rng R1) \/ ( rng R2)) by A1, A3, CIRCCOMB: 11;

      

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

      hereby

        let x be object;

        assume

         A6: x in ( InputVertices S1);

        then ( not x in ( rng R1)) & not x in ( rng R2) by A2, XBOOLE_0: 3, XBOOLE_0:def 5;

        then

         A7: not x in ( rng R) by A4, XBOOLE_0:def 3;

        x in the carrier of S by A5, A6, XBOOLE_0:def 3;

        hence x in ( InputVertices S) by A7, XBOOLE_0:def 5;

      end;

      

       A8: ( InputVertices S) c= (( InputVertices S1) \/ ( InputVertices S2)) by A1, CIRCCOMB: 11;

      hereby

        let x be object;

        assume

         A9: x in ( InputVertices (S1 +* S2));

        then not x in ( rng R) by XBOOLE_0:def 5;

        then x in ( InputVertices S1) or x in ( InputVertices S2) & not x in ( InnerVertices S1) by A4, A8, A9, XBOOLE_0:def 3;

        then x in ( InputVertices S1) or x in (( InputVertices S2) \ ( InnerVertices S1)) by XBOOLE_0:def 5;

        hence x in (( InputVertices S1) \/ (( InputVertices S2) \ ( InnerVertices S1))) by XBOOLE_0:def 3;

      end;

      let x be object;

      assume x in (( InputVertices S1) \/ (( InputVertices S2) \ ( InnerVertices S1)));

      then

       A10: x in ( InputVertices S1) or x in (( InputVertices S2) \ ( rng R1)) by XBOOLE_0:def 3;

      then

       A11: x in the carrier of S by A5, XBOOLE_0:def 3;

      x in ( InputVertices S1) & not x in ( rng R2) or x in ( InputVertices S2) & not x in ( rng R1) by A2, A10, XBOOLE_0: 3, XBOOLE_0:def 5;

      then

       A12: not x in ( rng R2) by XBOOLE_0:def 5;

       not x in ( rng R1) by A10, XBOOLE_0:def 5;

      then not x in ( rng R) by A4, A12, XBOOLE_0:def 3;

      hence thesis by A11, XBOOLE_0:def 5;

    end;

    theorem :: FACIRC_1:5

    

     Th5: for X,R be set st X is without_pairs & R is Relation holds X misses R;

    theorem :: FACIRC_1:6

    

     Th6: for S1,S2 be unsplit gate`1=arity non empty ManySortedSign st ( InputVertices S1) is without_pairs & ( InnerVertices S2) is Relation holds ( InputVertices S1) c= ( InputVertices (S1 +* S2)) & ( InputVertices (S1 +* S2)) = (( InputVertices S1) \/ (( InputVertices S2) \ ( InnerVertices S1)))

    proof

      let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;

      assume ( InputVertices S1) is without_pairs & ( InnerVertices S2) is Relation;

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

      hence thesis by Th4;

    end;

    theorem :: FACIRC_1:7

    

     Th7: for S1,S2 be unsplit gate`1=arity non empty ManySortedSign st ( InputVertices S1) is without_pairs & ( InnerVertices S1) is Relation & ( InputVertices S2) is without_pairs & ( InnerVertices S2) is Relation holds ( InputVertices (S1 +* S2)) = (( InputVertices S1) \/ ( InputVertices S2))

    proof

      let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;

      assume ( InputVertices S1) is without_pairs & ( InnerVertices S1) is Relation & ( InputVertices S2) is without_pairs & ( InnerVertices S2) is Relation;

      then ( InputVertices (S1 +* S2)) = (( InputVertices S1) \/ (( InputVertices S2) \ ( InnerVertices S1))) & ( InnerVertices S1) misses ( InputVertices S2) by Th6;

      hence thesis by XBOOLE_1: 83;

    end;

    theorem :: FACIRC_1:8

    

     Th8: for S1,S2 be non empty ManySortedSign st S1 tolerates S2 & ( InputVertices S1) is without_pairs & ( InputVertices S2) is without_pairs holds ( InputVertices (S1 +* S2)) is without_pairs

    proof

      let S1,S2 be non empty ManySortedSign;

      assume S1 tolerates S2;

      then

       A1: ( InputVertices (S1 +* S2)) c= (( InputVertices S1) \/ ( InputVertices S2)) by CIRCCOMB: 11;

      assume

       A2: for x be pair object holds not x in ( InputVertices S1);

      assume

       A3: for x be pair object holds not x in ( InputVertices S2);

      let x be pair object;

      assume x in ( InputVertices (S1 +* S2));

      then x in ( InputVertices S1) or x in ( InputVertices S2) by A1, XBOOLE_0:def 3;

      hence contradiction by A2, A3;

    end;

    theorem :: FACIRC_1:9

    for S1,S2 be unsplit gate`1=arity non empty ManySortedSign st ( InputVertices S1) is without_pairs & ( InputVertices S2) is without_pairs holds ( InputVertices (S1 +* S2)) is without_pairs by Th8, CIRCCOMB: 47;

    begin

    definition

      let i be Nat, D be non empty set;

      mode Tuple of i,D is Element of (i -tuples_on D);

    end

    scheme :: FACIRC_1:sch1

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

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

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

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

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

      hereby

        take f;

        let x,y be Element of BOOLEAN ;

        reconsider a = <*x, y*> as Tuple of 2, BOOLEAN by FINSEQ_2: 101;

        

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

        .= F(x,.) by FINSEQ_1: 44

        .= F(x,y) by FINSEQ_1: 44;

      end;

    end;

    scheme :: FACIRC_1:sch2

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

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

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

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

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

      now

        let a be Tuple of 2, BOOLEAN ;

        consider x,y be Element of BOOLEAN such that

         A3: a = <*x, y*> by FINSEQ_2: 100;

        

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: FACIRC_1:sch3

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

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

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

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

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

      hereby

        take f;

        let x,y be Element of BOOLEAN ;

        reconsider a = <*x, y*> as Tuple of 2, BOOLEAN by FINSEQ_2: 101;

        

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

        .= F(x,.) by FINSEQ_1: 44

        .= F(x,y) by FINSEQ_1: 44;

      end;

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

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

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

      now

        let a be Tuple of 2, BOOLEAN ;

        consider x,y be Element of BOOLEAN such that

         A4: a = <*x, y*> by FINSEQ_2: 100;

        

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: FACIRC_1:sch4

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

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

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

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

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

      hereby

        take f;

        let x,y,z be Element of BOOLEAN ;

        reconsider a = <*x, y, z*> as Tuple of 3, BOOLEAN by FINSEQ_2: 104;

        

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

        .= F(x,.,.) by FINSEQ_1: 45

        .= F(x,y,.) by FINSEQ_1: 45

        .= F(x,y,z) by FINSEQ_1: 45;

      end;

    end;

    scheme :: FACIRC_1:sch5

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

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

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

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

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

      now

        let a be Tuple of 3, BOOLEAN ;

        consider x,y,z be Element of BOOLEAN such that

         A3: a = <*x, y, z*> by FINSEQ_2: 103;

        

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: FACIRC_1:sch6

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

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

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

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

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

      hereby

        take f;

        let x,y,z be Element of BOOLEAN ;

        reconsider a = <*x, y, z*> as Tuple of 3, BOOLEAN by FINSEQ_2: 104;

        

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

        .= F(x,.,.) by FINSEQ_1: 45

        .= F(x,y,.) by FINSEQ_1: 45

        .= F(x,y,z) by FINSEQ_1: 45;

      end;

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

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

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

      now

        let a be Tuple of 3, BOOLEAN ;

        consider x,y,z be Element of BOOLEAN such that

         A4: a = <*x, y, z*> by FINSEQ_2: 103;

        

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      :: FACIRC_1:def4

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

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

      correctness

      proof

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

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

        hence thesis;

      end;

      :: FACIRC_1:def5

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

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

      correctness

      proof

        deffunc F( Element of BOOLEAN , Element of BOOLEAN ) = ($1 'or' $2);

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

        hence thesis;

      end;

      :: FACIRC_1:def6

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

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

      correctness

      proof

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

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

        hence thesis;

      end;

    end

    definition

      :: FACIRC_1:def7

      func or3 -> Function of (3 -tuples_on BOOLEAN ), BOOLEAN means

      : Def6: for x,y,z be Element of BOOLEAN holds (it . <*x, y, z*>) = ((x 'or' y) 'or' z);

      correctness

      proof

        deffunc F( Element of BOOLEAN , Element of BOOLEAN , Element of BOOLEAN ) = (($1 'or' $2) 'or' $3);

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

        hence thesis;

      end;

    end

    begin

    theorem :: FACIRC_1:10

    

     Th10: for S be Circuit-like non void non empty ManySortedSign holds for A be non-empty Circuit of S holds for s be State of A, g be Gate of S holds (( Following s) . ( the_result_sort_of g)) = (( Den (g,A)) . (s * ( the_arity_of g)))

    proof

      let S be Circuit-like non void non empty ManySortedSign;

      let A be non-empty Circuit of S;

      let s be State of A, g be Gate of S;

      set v = ( the_result_sort_of g);

      ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

      then (the ResultSort of S . g) in ( rng the ResultSort of S) by FUNCT_1:def 3;

      then

       A1: v in ( InnerVertices S) by MSUALG_1:def 2;

      then (g depends_on_in s) = (s * ( the_arity_of g)) & ( action_at v) = g by CIRCUIT1:def 3, MSAFREE2:def 7;

      hence thesis by A1, CIRCUIT2:def 5;

    end;

    definition

      let S be non void Circuit-like non empty ManySortedSign;

      let A be non-empty Circuit of S;

      let s be State of A;

      let n be natural Number;

      :: FACIRC_1:def8

      func Following (s,n) -> State of A means

      : Def7: ex f be sequence of ( product the Sorts of A) st it = (f . n) & (f . 0 ) = s & for n be Nat holds (f . (n + 1)) = ( Following (f . n));

      correctness

      proof

        reconsider n as Nat by TARSKI: 1;

        set D = ( product the Sorts of A);

        deffunc R( natural Number, Element of D) = ( Following $2);

        (ex y be Element of D st ex f be sequence of D st y = (f . n) & (f . 0 ) = s & for n be Nat holds (f . (n + 1)) = R(n,.)) & for y1,y2 be Element of D st (ex f be sequence of D st y1 = (f . n) & (f . 0 ) = s & for n be Nat holds (f . (n + 1)) = R(n,.)) & (ex f be sequence of D st y2 = (f . n) & (f . 0 ) = s & for n be Nat holds (f . (n + 1)) = R(n,.)) holds y1 = y2 from RECDEF_1:sch 14;

        hence thesis;

      end;

    end

    theorem :: FACIRC_1:11

    

     Th11: for S be Circuit-like non void non empty ManySortedSign holds for A be non-empty Circuit of S, s be State of A holds ( Following (s, 0 )) = s

    proof

      let S be Circuit-like non void non empty ManySortedSign;

      let A be non-empty Circuit of S, s be State of A;

      ex f be sequence of ( product the Sorts of A) st ( Following (s, 0 )) = (f . 0 ) & (f . 0 ) = s & for n be Nat holds (f . (n + 1)) = ( Following (f . n)) by Def7;

      hence thesis;

    end;

    theorem :: FACIRC_1:12

    

     Th12: for S be Circuit-like non void non empty ManySortedSign holds for A be non-empty Circuit of S, s be State of A holds for n be Nat holds ( Following (s,(n + 1))) = ( Following ( Following (s,n)))

    proof

      let S be Circuit-like non void non empty ManySortedSign;

      let A be non-empty Circuit of S, s be State of A;

      let n be Nat;

      consider f be sequence of ( product the Sorts of A) such that

       A1: ( Following (s,n)) = (f . n) and

       A2: (f . 0 ) = s and

       A3: for n be Nat holds (f . (n + 1)) = ( Following (f . n)) by Def7;

      

      thus ( Following (s,(n + 1))) = (f . (n + 1)) by A2, A3, Def7

      .= ( Following ( Following (s,n))) by A1, A3;

    end;

    theorem :: FACIRC_1:13

    

     Th13: for S be Circuit-like non void non empty ManySortedSign holds for A be non-empty Circuit of S, s be State of A holds for n,m be Nat holds ( Following (s,(n + m))) = ( Following (( Following (s,n)),m))

    proof

      let S be Circuit-like non void non empty ManySortedSign;

      let A be non-empty Circuit of S, s be State of A;

      let n be Nat;

      defpred P[ Nat] means ( Following (s,(n + $1))) = ( Following (( Following (s,n)),$1));

      

       A1: for m be Nat st P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume

         A2: ( Following (s,(n + m))) = ( Following (( Following (s,n)),m));

        

        thus ( Following (s,(n + (m + 1)))) = ( Following (s,((n + m) + 1)))

        .= ( Following ( Following (s,(n + m)))) by Th12

        .= ( Following (( Following (s,n)),(m + 1))) by A2, Th12;

      end;

      

       A3: P[ 0 ] by Th11;

      thus for i be Nat holds P[i] from NAT_1:sch 2( A3, A1);

    end;

    theorem :: FACIRC_1:14

    

     Th14: for S be non void Circuit-like non empty ManySortedSign holds for A be non-empty Circuit of S, s be State of A holds ( Following (s,1)) = ( Following s)

    proof

      let S be non void Circuit-like non empty ManySortedSign;

      let A be non-empty Circuit of S, s be State of A;

      ( 0 + 1) = 1;

      

      hence ( Following (s,1)) = ( Following ( Following (s, 0 ))) by Th12

      .= ( Following s) by Th11;

    end;

    theorem :: FACIRC_1:15

    

     Th15: for S be non void Circuit-like non empty ManySortedSign holds for A be non-empty Circuit of S, s be State of A holds ( Following (s,2)) = ( Following ( Following s))

    proof

      let S be non void Circuit-like non empty ManySortedSign;

      let A be non-empty Circuit of S, s be State of A;

      2 = (1 + 1);

      

      hence ( Following (s,2)) = ( Following ( Following (s,( 0 + 1)))) by Th12

      .= ( Following ( Following s)) by Th14;

    end;

    theorem :: FACIRC_1:16

    

     Th16: for S be Circuit-like non void non empty ManySortedSign holds for A be non-empty Circuit of S, s be State of A holds for n be Nat holds ( Following (s,(n + 1))) = ( Following (( Following s),n))

    proof

      let S be Circuit-like non void non empty ManySortedSign;

      let A be non-empty Circuit of S, s be State of A;

      let n be Nat;

      ( Following (s,(n + 1))) = ( Following (( Following (s,1)),n)) by Th13;

      hence thesis by Th14;

    end;

    definition

      let S be non void Circuit-like non empty ManySortedSign;

      let A be non-empty Circuit of S;

      let s be State of A;

      let x be object;

      :: FACIRC_1:def9

      pred s is_stable_at x means for n be Nat holds (( Following (s,n)) . x) = (s . x);

    end

    theorem :: FACIRC_1:17

    for S be non void Circuit-like non empty ManySortedSign holds for A be non-empty Circuit of S, s be State of A holds for x be set st s is_stable_at x holds for n be Nat holds ( Following (s,n)) is_stable_at x

    proof

      let S be non void Circuit-like non empty ManySortedSign;

      let A be non-empty Circuit of S;

      let s be State of A;

      let x be set such that

       A1: for n be Nat holds (( Following (s,n)) . x) = (s . x);

      let n,m be Nat;

      

      thus (( Following (( Following (s,n)),m)) . x) = (( Following (s,(n + m))) . x) by Th13

      .= (s . x) by A1

      .= (( Following (s,n)) . x) by A1;

    end;

    theorem :: FACIRC_1:18

    for S be non void Circuit-like non empty ManySortedSign holds for A be non-empty Circuit of S, s be State of A holds for x be set st x in ( InputVertices S) holds s is_stable_at x

    proof

      let S be non void Circuit-like non empty ManySortedSign;

      let A be non-empty Circuit of S;

      let s be State of A;

      let x be set;

      defpred P[ Nat] means (( Following (s,$1)) . x) = (s . x);

      assume

       A1: x in ( InputVertices S);

       A2:

      now

        let n be Nat;

        assume

         A3: P[n];

        (( Following (s,(n + 1))) . x) = (( Following ( Following (s,n))) . x) by Th12

        .= (s . x) by A1, A3, CIRCUIT2:def 5;

        hence P[(n + 1)];

      end;

      

       A4: P[ 0 ] by Th11;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A4, A2);

    end;

    theorem :: FACIRC_1:19

    

     Th19: for S be non void Circuit-like non empty ManySortedSign holds for A be non-empty Circuit of S, s be State of A holds for g be Gate of S st for x be set st x in ( rng ( the_arity_of g)) holds s is_stable_at x holds ( Following s) is_stable_at ( the_result_sort_of g)

    proof

      let S be non void Circuit-like non empty ManySortedSign;

      let A be non-empty Circuit of S;

      let s be State of A;

      let g be Gate of S;

      set p = ( the_arity_of g);

      assume

       A1: for x be set st x in ( rng p) holds s is_stable_at x;

      let n be Nat;

       A2:

      now

        let a be object;

        assume

         A3: a in ( dom p);

        then (p . a) in ( rng p) by FUNCT_1:def 3;

        then

         A4: s is_stable_at (p . a) by A1;

        ((( Following (s,n)) * p) . a) = (( Following (s,n)) . (p . a)) & ((s * p) . a) = (s . (p . a)) by A3, FUNCT_1: 13;

        hence ((( Following (s,n)) * p) . a) = ((s * p) . a) by A4;

      end;

      

       A5: ( rng p) c= the carrier of S by FINSEQ_1:def 4;

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

      then

       A6: ( dom (( Following (s,n)) * p)) = ( dom p) by A5, RELAT_1: 27;

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

      then ( dom (s * p)) = ( dom p) by A5, RELAT_1: 27;

      then

       A7: (( Following (s,n)) * p) = (s * p) by A6, A2, FUNCT_1: 2;

      

      thus (( Following (( Following s),n)) . ( the_result_sort_of g)) = (( Following (s,(n + 1))) . ( the_result_sort_of g)) by Th16

      .= (( Following ( Following (s,n))) . ( the_result_sort_of g)) by Th12

      .= (( Den (g,A)) . (( Following (s,n)) * p)) by Th10

      .= (( Following s) . ( the_result_sort_of g)) by A7, Th10;

    end;

    begin

    theorem :: FACIRC_1:20

    

     Th20: for S1,S2 be non empty ManySortedSign, v be Vertex of S1 holds v in the carrier of (S1 +* S2) & v in the carrier of (S2 +* S1)

    proof

      let S1,S2 be non empty ManySortedSign;

      let v be Vertex of S1;

      the carrier of (S1 +* S2) = (the carrier of S1 \/ the carrier of S2) & the carrier of (S2 +* S1) = (the carrier of S2 \/ the carrier of S1) by CIRCCOMB:def 2;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: FACIRC_1:21

    

     Th21: for S1,S2 be unsplit gate`1=arity non empty ManySortedSign holds for x be set st x in ( InnerVertices S1) holds x in ( InnerVertices (S1 +* S2)) & x in ( InnerVertices (S2 +* S1))

    proof

      let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;

      S1 tolerates S2 by CIRCCOMB: 47;

      then ( InnerVertices (S1 +* S2)) = (( InnerVertices S1) \/ ( InnerVertices S2)) & ( InnerVertices (S2 +* S1)) = (( InnerVertices S2) \/ ( InnerVertices S1)) by CIRCCOMB: 11;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: FACIRC_1:22

    for S1,S2 be non empty ManySortedSign holds for x be set st x in ( InnerVertices S2) holds x in ( InnerVertices (S1 +* S2))

    proof

      let S1,S2 be non empty ManySortedSign;

      set R1 = the ResultSort of S1, R2 = the ResultSort of S2;

      ( InnerVertices (S1 +* S2)) = ( rng (R1 +* R2)) by CIRCCOMB:def 2;

      then ( InnerVertices S2) c= ( InnerVertices (S1 +* S2)) by FUNCT_4: 18;

      hence thesis;

    end;

    theorem :: FACIRC_1:23

    for S1,S2 be unsplit gate`1=arity non empty ManySortedSign holds (S1 +* S2) = (S2 +* S1) by CIRCCOMB: 5, CIRCCOMB: 47;

    theorem :: FACIRC_1:24

    for S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign holds for A1 be Boolean gate`2=den Circuit of S1 holds for A2 be Boolean gate`2=den Circuit of S2 holds (A1 +* A2) = (A2 +* A1) by CIRCCOMB: 22, CIRCCOMB: 60;

    theorem :: FACIRC_1:25

    

     Th25: for S1,S2,S3 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign holds for A1 be Boolean Circuit of S1, A2 be Boolean Circuit of S2 holds for A3 be Boolean Circuit of S3 holds ((A1 +* A2) +* A3) = (A1 +* (A2 +* A3))

    proof

      let S1,S2,S3 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign;

      let A1 be Boolean Circuit of S1;

      let A2 be Boolean Circuit of S2;

      let A3 be Boolean Circuit of S3;

      

       A1: the Sorts of A3 tolerates the Sorts of A1 by CIRCCOMB: 59;

      the Sorts of A1 tolerates the Sorts of A2 & the Sorts of A2 tolerates the Sorts of A3 by CIRCCOMB: 59;

      hence thesis by A1, CIRCCOMB: 23;

    end;

    theorem :: FACIRC_1:26

    

     Th26: for S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign holds for A1 be Boolean gate`2=den non-empty Circuit of S1 holds for A2 be Boolean gate`2=den non-empty Circuit of S2 holds for s be State of (A1 +* A2) holds (s | the carrier of S1) is State of A1 & (s | the carrier of S2) is State of A2

    proof

      let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign;

      let A1 be Boolean gate`2=den Circuit of S1;

      let A2 be Boolean gate`2=den Circuit of S2;

      let s be State of (A1 +* A2);

      the Sorts of A1 tolerates the Sorts of A2 by CIRCCOMB: 59;

      hence thesis by CIRCCOMB: 26;

    end;

    theorem :: FACIRC_1:27

    

     Th27: for S1,S2 be unsplit gate`1=arity non empty ManySortedSign holds ( InnerVertices (S1 +* S2)) = (( InnerVertices S1) \/ ( InnerVertices S2))

    proof

      let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;

      S1 tolerates S2 by CIRCCOMB: 47;

      hence thesis by CIRCCOMB: 11;

    end;

    theorem :: FACIRC_1:28

    

     Th28: for S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st ( InnerVertices S2) misses ( InputVertices S1) holds for A1 be Boolean gate`2=den Circuit of S1 holds for A2 be Boolean gate`2=den Circuit of S2 holds for s be State of (A1 +* A2), s1 be State of A1 st s1 = (s | the carrier of S1) holds (( Following s) | the carrier of S1) = ( Following s1)

    proof

      let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign such that

       A1: ( InnerVertices S2) misses ( InputVertices S1);

      let A1 be Boolean gate`2=den Circuit of S1;

      let A2 be Boolean gate`2=den Circuit of S2;

      let s be State of (A1 +* A2), s1 be State of A1 such that

       A2: s1 = (s | the carrier of S1);

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

      ( dom ( Following s1)) = the carrier of S1 & ( Following s) = (( Following s2) +* ( Following s1)) by A1, A2, CIRCCOMB: 33, CIRCCOMB: 60, CIRCUIT1: 3;

      hence thesis by FUNCT_4: 23;

    end;

    theorem :: FACIRC_1:29

    

     Th29: for S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st ( InnerVertices S1) misses ( InputVertices S2) holds for A1 be Boolean gate`2=den Circuit of S1 holds for A2 be Boolean gate`2=den Circuit of S2 holds for s be State of (A1 +* A2), s2 be State of A2 st s2 = (s | the carrier of S2) holds (( Following s) | the carrier of S2) = ( Following s2)

    proof

      let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign such that

       A1: ( InnerVertices S1) misses ( InputVertices S2);

      let A1 be Boolean gate`2=den Circuit of S1;

      let A2 be Boolean gate`2=den Circuit of S2;

      let s be State of (A1 +* A2), s2 be State of A2 such that

       A2: s2 = (s | the carrier of S2);

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

      ( dom ( Following s2)) = the carrier of S2 & ( Following s) = (( Following s1) +* ( Following s2)) by A1, A2, CIRCCOMB: 32, CIRCCOMB: 60, CIRCUIT1: 3;

      hence thesis by FUNCT_4: 23;

    end;

    theorem :: FACIRC_1:30

    

     Th30: for S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st ( InnerVertices S2) misses ( InputVertices S1) holds for A1 be Boolean gate`2=den Circuit of S1 holds for A2 be Boolean gate`2=den Circuit of S2 holds for s be State of (A1 +* A2), s1 be State of A1 st s1 = (s | the carrier of S1) holds for n be Nat holds (( Following (s,n)) | the carrier of S1) = ( Following (s1,n))

    proof

      let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign such that

       A1: ( InnerVertices S2) misses ( InputVertices S1);

      let A1 be Boolean gate`2=den Circuit of S1;

      let A2 be Boolean gate`2=den Circuit of S2;

      let s be State of (A1 +* A2), s1 be State of A1 such that

       A2: s1 = (s | the carrier of S1);

      defpred P[ Nat] means (( Following (s,$1)) | the carrier of S1) = ( Following (s1,$1));

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A4: (( Following (s,n)) | the carrier of S1) = ( Following (s1,n));

        

        thus (( Following (s,(n + 1))) | the carrier of S1) = (( Following ( Following (s,n))) | the carrier of S1) by Th12

        .= ( Following ( Following (s1,n))) by A1, A4, Th28

        .= ( Following (s1,(n + 1))) by Th12;

      end;

      ( Following (s, 0 )) = s by Th11;

      then

       A5: P[ 0 ] by A2, Th11;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A5, A3);

    end;

    theorem :: FACIRC_1:31

    

     Th31: for S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st ( InnerVertices S1) misses ( InputVertices S2) holds for A1 be Boolean gate`2=den Circuit of S1 holds for A2 be Boolean gate`2=den Circuit of S2 holds for s be State of (A1 +* A2), s2 be State of A2 st s2 = (s | the carrier of S2) holds for n be Nat holds (( Following (s,n)) | the carrier of S2) = ( Following (s2,n))

    proof

      let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign such that

       A1: ( InnerVertices S1) misses ( InputVertices S2);

      let A1 be Boolean gate`2=den Circuit of S1;

      let A2 be Boolean gate`2=den Circuit of S2;

      let s be State of (A1 +* A2), s2 be State of A2 such that

       A2: s2 = (s | the carrier of S2);

      defpred P[ Nat] means (( Following (s,$1)) | the carrier of S2) = ( Following (s2,$1));

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A4: (( Following (s,n)) | the carrier of S2) = ( Following (s2,n));

        

        thus (( Following (s,(n + 1))) | the carrier of S2) = (( Following ( Following (s,n))) | the carrier of S2) by Th12

        .= ( Following ( Following (s2,n))) by A1, A4, Th29

        .= ( Following (s2,(n + 1))) by Th12;

      end;

      ( Following (s, 0 )) = s by Th11;

      then

       A5: P[ 0 ] by A2, Th11;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A5, A3);

    end;

    theorem :: FACIRC_1:32

    

     Th32: for S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st ( InnerVertices S2) misses ( InputVertices S1) holds for A1 be Boolean gate`2=den Circuit of S1 holds for A2 be Boolean gate`2=den Circuit of S2 holds for s be State of (A1 +* A2), s1 be State of A1 st s1 = (s | the carrier of S1) holds for v be set st v in the carrier of S1 holds for n be Nat holds (( Following (s,n)) . v) = (( Following (s1,n)) . v)

    proof

      let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign such that

       A1: ( InnerVertices S2) misses ( InputVertices S1);

      let A1 be Boolean gate`2=den Circuit of S1;

      let A2 be Boolean gate`2=den Circuit of S2;

      let s be State of (A1 +* A2), s1 be State of A1 such that

       A2: s1 = (s | the carrier of S1);

      let v be set;

      assume

       A3: v in the carrier of S1;

      let n be Nat;

      

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

      (( Following (s,n)) | the carrier of S1) = ( Following (s1,n)) by A1, A2, Th30;

      hence thesis by A3, A4, FUNCT_1: 47;

    end;

    theorem :: FACIRC_1:33

    

     Th33: for S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st ( InnerVertices S1) misses ( InputVertices S2) holds for A1 be Boolean gate`2=den Circuit of S1 holds for A2 be Boolean gate`2=den Circuit of S2 holds for s be State of (A1 +* A2), s2 be State of A2 st s2 = (s | the carrier of S2) holds for v be set st v in the carrier of S2 holds for n be Nat holds (( Following (s,n)) . v) = (( Following (s2,n)) . v)

    proof

      let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign such that

       A1: ( InnerVertices S1) misses ( InputVertices S2);

      let A1 be Boolean gate`2=den Circuit of S1;

      let A2 be Boolean gate`2=den Circuit of S2;

      let s be State of (A1 +* A2), s1 be State of A2 such that

       A2: s1 = (s | the carrier of S2);

      let v be set;

      assume

       A3: v in the carrier of S2;

      let n be Nat;

      

       A4: the carrier of S2 = ( dom ( Following (s1,n))) by CIRCUIT1: 3;

      (( Following (s,n)) | the carrier of S2) = ( Following (s1,n)) by A1, A2, Th31;

      hence thesis by A3, A4, FUNCT_1: 47;

    end;

    registration

      let S be gate`2=den non void non empty ManySortedSign;

      let g be Gate of S;

      cluster (g `2 ) -> Function-like Relation-like;

      coherence

      proof

        consider A be MSAlgebra over S such that

         A1: A is gate`2=den by CIRCCOMB:def 11;

        (g `2 ) = ( [(g `1 ), (the Charact of A . g)] `2 ) by A1

        .= (the Charact of A . g)

        .= ( Den (g,A)) by MSUALG_1:def 6;

        hence thesis;

      end;

    end

    theorem :: FACIRC_1:34

    

     Th34: for S be gate`2=den Circuit-like non void non empty ManySortedSign holds for A be non-empty Circuit of S st A is gate`2=den holds for s be State of A, g be Gate of S holds (( Following s) . ( the_result_sort_of g)) = ((g `2 ) . (s * ( the_arity_of g)))

    proof

      let S be gate`2=den Circuit-like non void non empty ManySortedSign;

      let A be non-empty Circuit of S such that

       A1: for g be set st g in the carrier' of S holds g = [(g `1 ), (the Charact of A . g)];

      let s be State of A, g be Gate of S;

      

       A2: ( Den (g,A)) = (the Charact of A . g) by MSUALG_1:def 6

      .= ( [(g `1 ), (the Charact of A . g)] `2 )

      .= (g `2 ) by A1;

      set v = ( the_result_sort_of g);

      ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;

      then (the ResultSort of S . g) in ( rng the ResultSort of S) by FUNCT_1:def 3;

      then

       A3: v in ( InnerVertices S) by MSUALG_1:def 2;

      then (g depends_on_in s) = (s * ( the_arity_of g)) & ( action_at v) = g by CIRCUIT1:def 3, MSAFREE2:def 7;

      hence thesis by A2, A3, CIRCUIT2:def 5;

    end;

    theorem :: FACIRC_1:35

    

     Th35: for S be gate`1=arity gate`2isBoolean unsplit non void non empty ManySortedSign holds for A be Boolean gate`2=den non-empty Circuit of S holds for s be State of A, p be FinSequence, f be Function st [p, f] in the carrier' of S holds (( Following s) . [p, f]) = (f . (s * p))

    proof

      let S be gate`1=arity gate`2isBoolean unsplit non void non empty ManySortedSign;

      let A be Boolean gate`2=den non-empty Circuit of S;

      let s be State of A, p be FinSequence, f be Function;

      assume [p, f] in the carrier' of S;

      then

      reconsider g = [p, f] as Gate of S;

      

       A1: (g `1 ) = p & (g `2 ) = f;

      

       A2: ( the_result_sort_of g) = (the ResultSort of S . g) by MSUALG_1:def 2

      .= g by CIRCCOMB: 44;

      ( the_arity_of g) = (the Arity of S . g) by MSUALG_1:def 1

      .= ( [(the Arity of S . g), (g `2 )] `1 )

      .= (g `1 ) by CIRCCOMB:def 8;

      hence thesis by A1, A2, Th34;

    end;

    theorem :: FACIRC_1:36

    for S be gate`1=arity gate`2isBoolean unsplit non void non empty ManySortedSign holds for A be Boolean gate`2=den non-empty Circuit of S holds for s be State of A, p be FinSequence, f be Function st [p, f] in the carrier' of S & for x be set st x in ( rng p) holds s is_stable_at x holds ( Following s) is_stable_at [p, f]

    proof

      let S be gate`1=arity gate`2isBoolean unsplit non void non empty ManySortedSign;

      let A be Boolean gate`2=den non-empty Circuit of S;

      let s be State of A, p be FinSequence, f be Function;

      assume [p, f] in the carrier' of S;

      then

      reconsider g = [p, f] as Gate of S;

      

       A1: ( the_arity_of g) = (the Arity of S . g) by MSUALG_1:def 1

      .= ( [(the Arity of S . g), (g `2 )] `1 )

      .= (g `1 ) by CIRCCOMB:def 8

      .= p;

      

       A2: ( the_result_sort_of g) = (the ResultSort of S . g) by MSUALG_1:def 2

      .= g by CIRCCOMB: 44;

      assume for x be set st x in ( rng p) holds s is_stable_at x;

      hence thesis by A1, A2, Th19;

    end;

    theorem :: FACIRC_1:37

    

     Th37: for S be unsplit non empty ManySortedSign holds ( InnerVertices S) = the carrier' of S

    proof

      let S be unsplit non empty ManySortedSign;

      the ResultSort of S = ( id the carrier' of S) by CIRCCOMB:def 7;

      hence thesis;

    end;

    begin

    theorem :: FACIRC_1:38

    

     Th38: for f be set, p be FinSequence holds ( InnerVertices ( 1GateCircStr (p,f))) is Relation

    proof

      let f be set, p be FinSequence;

      ( InnerVertices ( 1GateCircStr (p,f))) = { [p, f]} by CIRCCOMB: 42;

      hence thesis;

    end;

    theorem :: FACIRC_1:39

    for f be set, p be nonpair-yielding FinSequence holds ( InputVertices ( 1GateCircStr (p,f))) is without_pairs

    proof

      let f be set, p be nonpair-yielding FinSequence;

      ( InputVertices ( 1GateCircStr (p,f))) = ( rng p) by CIRCCOMB: 42;

      hence thesis;

    end;

    theorem :: FACIRC_1:40

    

     Th40: for f,x,y be object holds ( InputVertices ( 1GateCircStr ( <*x, y*>,f))) = {x, y}

    proof

      let f,x,y be object;

      set p = <*x, y*>;

      

      thus ( InputVertices ( 1GateCircStr (p,f))) = ( rng p) by CIRCCOMB: 42

      .= {x, y} by FINSEQ_2: 127;

    end;

    theorem :: FACIRC_1:41

    

     Th41: for f be set, x,y be non pair object holds ( InputVertices ( 1GateCircStr ( <*x, y*>,f))) is without_pairs

    proof

      let f be set, x,y be non pair object;

      set p = <*x, y*>;

      let z be pair object;

      assume

       A1: z in ( InputVertices ( 1GateCircStr (p,f)));

      ( InputVertices ( 1GateCircStr (p,f))) = {x, y} by Th40;

      hence thesis by A1, TARSKI:def 2;

    end;

    theorem :: FACIRC_1:42

    

     Th42: for f,x,y,z be object holds ( InputVertices ( 1GateCircStr ( <*x, y, z*>,f))) = {x, y, z}

    proof

      let f,x,y,z be object;

      set p = <*x, y, z*>;

      

      thus ( InputVertices ( 1GateCircStr (p,f))) = ( rng p) by CIRCCOMB: 42

      .= {x, y, z} by FINSEQ_2: 128;

    end;

    theorem :: FACIRC_1:43

    

     Th43: for x,y,f be object holds x in the carrier of ( 1GateCircStr ( <*x, y*>,f)) & y in the carrier of ( 1GateCircStr ( <*x, y*>,f)) & [ <*x, y*>, f] in the carrier of ( 1GateCircStr ( <*x, y*>,f))

    proof

      let x,y,f be object;

      set p = <*x, y*>;

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

      then

       A1: x in ( rng p) by FINSEQ_2: 127;

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

      then

       A2: y in ( rng p) by FINSEQ_2: 127;

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

      hence thesis by A1, A2, XBOOLE_0:def 3;

    end;

    theorem :: FACIRC_1:44

    

     Th44: for x,y,z,f be object holds x in the carrier of ( 1GateCircStr ( <*x, y, z*>,f)) & y in the carrier of ( 1GateCircStr ( <*x, y, z*>,f)) & z in the carrier of ( 1GateCircStr ( <*x, y, z*>,f))

    proof

      let x,y,z,f be object;

      set p = <*x, y, z*>;

      set A = the carrier of ( 1GateCircStr (p,f));

      y in {x, y, z} by ENUMSET1:def 1;

      then

       A1: y in ( rng p) by FINSEQ_2: 128;

      z in {x, y, z} by ENUMSET1:def 1;

      then

       A2: z in ( rng p) by FINSEQ_2: 128;

      x in {x, y, z} by ENUMSET1:def 1;

      then A = (( rng p) \/ { [p, f]}) & x in ( rng p) by CIRCCOMB:def 6, FINSEQ_2: 128;

      hence thesis by A1, A2, XBOOLE_0:def 3;

    end;

    theorem :: FACIRC_1:45

    for f,x be set, p be FinSequence holds x in the carrier of ( 1GateCircStr (p,f,x)) & for y be set st y in ( rng p) holds y in the carrier of ( 1GateCircStr (p,f,x))

    proof

      let f,x be set;

      let p be FinSequence;

      set A = the carrier of ( 1GateCircStr (p,f,x));

      A = (( rng p) \/ {x}) & x in {x} by CIRCCOMB:def 5, TARSKI:def 1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: FACIRC_1:46

    for f,x be set, p be FinSequence holds ( 1GateCircStr (p,f,x)) is gate`1=arity Circuit-like

    proof

      let f,x be set;

      let p be FinSequence;

      set S = ( 1GateCircStr (p,f,x));

      thus S is gate`1=arity

      proof

        let g be set;

        assume g in the carrier' of S;

        then g in { [p, f]} by CIRCCOMB:def 5;

        then

         A1: g = [p, f] by TARSKI:def 1;

        thus thesis by A1, CIRCCOMB:def 5;

      end;

      thus S is Circuit-like

      proof

        let S9 be non void non empty ManySortedSign such that

         A2: S9 = S;

        let o1,o2 be OperSymbol of S9;

        o1 = [p, f] by A2, CIRCCOMB: 37;

        hence thesis by A2, CIRCCOMB: 37;

      end;

    end;

    theorem :: FACIRC_1:47

    

     Th47: for p be FinSequence, f be set holds [p, f] in ( InnerVertices ( 1GateCircStr (p,f)))

    proof

      let p be FinSequence, f be set;

      ( InnerVertices ( 1GateCircStr (p,f))) = { [p, f]} by CIRCCOMB: 42;

      hence thesis by TARSKI:def 1;

    end;

    definition

      let x,y be object;

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

      :: FACIRC_1:def10

      func 1GateCircuit (x,y,f) -> Boolean gate`2=den strict Circuit of ( 1GateCircStr ( <*x, y*>,f)) equals ( 1GateCircuit ( <*x, y*> qua FinSeqLen of 2,f));

      coherence by CIRCCOMB: 61;

    end

    reserve x,y,z,c for object,

f for Function of (2 -tuples_on BOOLEAN ), BOOLEAN ;

    theorem :: FACIRC_1:48

    

     Th48: for X be finite non empty set, f be Function of (2 -tuples_on X), X holds for s be State of ( 1GateCircuit ( <*x, y*>,f)) holds (( Following s) . [ <*x, y*>, f]) = (f . <*(s . x), (s . y)*>) & (( Following s) . x) = (s . x) & (( Following s) . y) = (s . y)

    proof

      let X be finite non empty set, f be Function of (2 -tuples_on X), X;

      let s be State of ( 1GateCircuit ( <*x, y*>,f));

      set p = <*x, y*>;

      ( dom s) = the carrier of ( 1GateCircStr (p,f)) by CIRCUIT1: 3;

      then

       A1: ( dom s) = (( rng p) \/ { [p, f]}) by CIRCCOMB:def 6;

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

      then y in ( rng p) by FINSEQ_2: 127;

      then

       A2: y in ( dom s) by A1, XBOOLE_0:def 3;

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

      then x in ( rng p) by FINSEQ_2: 127;

      then

       A3: x in ( dom s) by A1, XBOOLE_0:def 3;

      

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

      .= (f . <*(s . x), (s . y)*>) by A3, A2, FINSEQ_2: 125;

      reconsider x, y as Vertex of ( 1GateCircStr (p,f)) by Th43;

      ( InputVertices ( 1GateCircStr (p,f))) = ( rng p) by CIRCCOMB: 42

      .= {x, y} by FINSEQ_2: 127;

      then x in ( InputVertices ( 1GateCircStr (p,f))) & y in ( InputVertices ( 1GateCircStr (p,f))) by TARSKI:def 2;

      hence thesis by CIRCUIT2:def 5;

    end;

    theorem :: FACIRC_1:49

    

     Th49: for X be finite non empty set, f be Function of (2 -tuples_on X), X holds for s be State of ( 1GateCircuit ( <*x, y*>,f)) holds ( Following s) is stable

    proof

      let X be finite non empty set, f be Function of (2 -tuples_on X), X;

      set S = ( 1GateCircStr ( <*x, y*>,f));

      let s be State of ( 1GateCircuit ( <*x, y*>,f));

      set s1 = ( Following s), s2 = ( Following s1);

      set p = <*x, y*>;

      

       A1: the carrier of S = (( rng p) \/ { [p, f]}) by CIRCCOMB:def 6

      .= ( {x, y} \/ { [p, f]}) by FINSEQ_2: 127;

       A2:

      now

        let a be object;

        

         A3: (s2 . [p, f]) = (f . <*(s1 . x), (s1 . y)*>) by Th48;

        assume a in the carrier of S;

        then a in {x, y} or a in { [p, f]} by A1, XBOOLE_0:def 3;

        then

         A4: a = x or a = y or a = [p, f] by TARSKI:def 1, TARSKI:def 2;

        (s1 . x) = (s . x) & (s1 . y) = (s . y) by Th48;

        hence (s2 . a) = (s1 . a) by A4, A3, Th48;

      end;

      ( dom s1) = the carrier of S & ( dom s2) = the carrier of S by CIRCUIT1: 3;

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

    end;

    theorem :: FACIRC_1:50

    for s be State of ( 1GateCircuit (x,y,f)) holds (( Following s) . [ <*x, y*>, f]) = (f . <*(s . x), (s . y)*>) & (( Following s) . x) = (s . x) & (( Following s) . y) = (s . y) by Th48;

    theorem :: FACIRC_1:51

    for s be State of ( 1GateCircuit (x,y,f)) holds ( Following s) is stable by Th49;

    definition

      let x,y,z be object;

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

      :: FACIRC_1:def11

      func 1GateCircuit (x,y,z,f) -> Boolean gate`2=den strict Circuit of ( 1GateCircStr ( <*x, y, z*>,f)) equals ( 1GateCircuit ( <*x, y, z*>,f));

      coherence by CIRCCOMB: 61;

    end

    theorem :: FACIRC_1:52

    

     Th52: for X be finite non empty set, f be Function of (3 -tuples_on X), X holds for s be State of ( 1GateCircuit ( <*x, y, z*>,f)) holds (( Following s) . [ <*x, y, z*>, f]) = (f . <*(s . x), (s . y), (s . z)*>) & (( Following s) . x) = (s . x) & (( Following s) . y) = (s . y) & (( Following s) . z) = (s . z)

    proof

      let X be finite non empty set, f be Function of (3 -tuples_on X), X;

      let s be State of ( 1GateCircuit ( <*x, y, z*>,f));

      set p = <*x, y, z*>;

      ( dom s) = the carrier of ( 1GateCircStr (p,f)) by CIRCUIT1: 3;

      then

       A1: ( dom s) = (( rng p) \/ { [p, f]}) by CIRCCOMB:def 6;

      y in {x, y, z} by ENUMSET1:def 1;

      then y in ( rng p) by FINSEQ_2: 128;

      then

       A2: y in ( dom s) by A1, XBOOLE_0:def 3;

      x in {x, y, z} by ENUMSET1:def 1;

      then x in ( rng p) by FINSEQ_2: 128;

      then

       A3: x in ( dom s) by A1, XBOOLE_0:def 3;

      z in {x, y, z} by ENUMSET1:def 1;

      then z in ( rng p) by FINSEQ_2: 128;

      then

       A4: z in ( dom s) by A1, XBOOLE_0:def 3;

      

      thus (( Following s) . [p, f]) = (f . (s * p)) by CIRCCOMB: 56

      .= (f . <*(s . x), (s . y), (s . z)*>) by A3, A2, A4, FINSEQ_2: 126;

      reconsider x, y, z as Vertex of ( 1GateCircStr (p,f)) by Th44;

      

       A5: ( InputVertices ( 1GateCircStr (p,f))) = ( rng p) by CIRCCOMB: 42

      .= {x, y, z} by FINSEQ_2: 128;

      then

       A6: z in ( InputVertices ( 1GateCircStr (p,f))) by ENUMSET1:def 1;

      x in ( InputVertices ( 1GateCircStr (p,f))) & y in ( InputVertices ( 1GateCircStr (p,f))) by A5, ENUMSET1:def 1;

      hence thesis by A6, CIRCUIT2:def 5;

    end;

    theorem :: FACIRC_1:53

    

     Th53: for X be finite non empty set, f be Function of (3 -tuples_on X), X holds for s be State of ( 1GateCircuit ( <*x, y, z*>,f)) holds ( Following s) is stable

    proof

      let X be finite non empty set, f be Function of (3 -tuples_on X), X;

      set p = <*x, y, z*>;

      set S = ( 1GateCircStr (p,f));

      let s be State of ( 1GateCircuit (p,f));

      set s1 = ( Following s), s2 = ( Following s1);

      

       A1: the carrier of S = (( rng p) \/ { [p, f]}) by CIRCCOMB:def 6

      .= ( {x, y, z} \/ { [p, f]}) by FINSEQ_2: 128;

       A2:

      now

        let a be object;

        

         A3: (s1 . z) = (s . z) & (s2 . [p, f]) = (f . <*(s1 . x), (s1 . y), (s1 . z)*>) by Th52;

        assume a in the carrier of S;

        then a in {x, y, z} or a in { [p, f]} by A1, XBOOLE_0:def 3;

        then

         A4: a = x or a = y or a = z or a = [p, f] by ENUMSET1:def 1, TARSKI:def 1;

        (s1 . x) = (s . x) & (s1 . y) = (s . y) by Th52;

        hence (s2 . a) = (s1 . a) by A4, A3, Th52;

      end;

      ( dom s1) = the carrier of S & ( dom s2) = the carrier of S by CIRCUIT1: 3;

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

    end;

    theorem :: FACIRC_1:54

    for f be Function of (3 -tuples_on BOOLEAN ), BOOLEAN holds for s be State of ( 1GateCircuit (x,y,z,f)) holds (( Following s) . [ <*x, y, z*>, f]) = (f . <*(s . x), (s . y), (s . z)*>) & (( Following s) . x) = (s . x) & (( Following s) . y) = (s . y) & (( Following s) . z) = (s . z) by Th52;

    theorem :: FACIRC_1:55

    for f be Function of (3 -tuples_on BOOLEAN ), BOOLEAN holds for s be State of ( 1GateCircuit (x,y,z,f)) holds ( Following s) is stable by Th53;

    begin

    definition

      let x,y,c be object;

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

      :: FACIRC_1:def12

      func 2GatesCircStr (x,y,c,f) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( 1GateCircStr ( <*x, y*>,f)) +* ( 1GateCircStr ( <* [ <*x, y*>, f], c*>,f)));

      correctness ;

    end

    definition

      let x,y,c be object;

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

      :: FACIRC_1:def13

      func 2GatesCircOutput (x,y,c,f) -> Element of ( InnerVertices ( 2GatesCircStr (x,y,c,f))) equals [ <* [ <*x, y*>, f], c*>, f];

      coherence

      proof

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

        set S2 = ( 1GateCircStr (p,f));

         [p, f] in ( InnerVertices S2) by Th47;

        hence thesis by Th21;

      end;

      correctness ;

    end

    registration

      let x,y,c be object;

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

      cluster ( 2GatesCircOutput (x,y,c,f)) -> pair;

      coherence ;

    end

    theorem :: FACIRC_1:56

    

     Th56: ( InnerVertices ( 2GatesCircStr (x,y,c,f))) = { [ <*x, y*>, f], ( 2GatesCircOutput (x,y,c,f))}

    proof

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

      set S1 = ( 1GateCircStr ( <*x, y*>,f)), S2 = ( 1GateCircStr (p,f));

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

      S1 tolerates S2 by CIRCCOMB: 43;

      

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

      .= ( { [ <*x, y*>, f]} \/ ( InnerVertices S2)) by CIRCCOMB: 42

      .= ( { [ <*x, y*>, f]} \/ { [p, f]}) by CIRCCOMB: 42

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

    end;

    theorem :: FACIRC_1:57

    

     Th57: c <> [ <*x, y*>, f] implies ( InputVertices ( 2GatesCircStr (x,y,c,f))) = {x, y, c}

    proof

      assume

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

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

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

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

      set S2 = ( 1GateCircStr (p,f));

      set R = the ResultSort of S;

      

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

      

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

      then

       A4: the carrier of S1 = ( {x, y} \/ { [ <*x, y*>, f]}) by CIRCCOMB:def 6;

      

       A5: ( rng R) = { [ <*x, y*>, f], ( 2GatesCircOutput (x,y,c,f))} by Th56

      .= { [ <*x, y*>, f], [p, f]};

      

       A6: ( rng p) = { [ <*x, y*>, f], c} by FINSEQ_2: 127;

      then

       A7: the carrier of S2 = ( { [ <*x, y*>, f], c} \/ { [p, f]}) by CIRCCOMB:def 6;

      thus ( InputVertices S) c= {x, y, c}

      proof

        let z be object;

        assume

         A8: z in ( InputVertices S);

        then z in the carrier of S1 or z in the carrier of S2 by A2, XBOOLE_0:def 3;

        then z in {x, y} or z in { [ <*x, y*>, f]} or z in { [ <*x, y*>, f], c} or z in { [p, f]} by A4, A7, XBOOLE_0:def 3;

        then

         A9: z = x or z = y or z = [ <*x, y*>, f] or z = c or z = [p, f] by TARSKI:def 1, TARSKI:def 2;

         not z in ( rng R) by A8, XBOOLE_0:def 5;

        hence thesis by A5, A9, ENUMSET1:def 1, TARSKI:def 2;

      end;

      let z be object;

      reconsider zz = z as set by TARSKI: 1;

      assume z in {x, y, c};

      then

       A10: z = x or z = y or z = c by ENUMSET1:def 1;

      then z in {x, y} or z in ( rng p) by A6, TARSKI:def 2;

      then z in ( InputVertices S1) or z in ( InputVertices S2) by A3, CIRCCOMB: 42;

      then

       A11: z in the carrier of S by A2, XBOOLE_0:def 3;

      z in {x, y} & [ <*x, y*>, f] in ( rng p) or z in {c} by A6, A10, TARSKI:def 1, TARSKI:def 2;

      then

       A12: ( the_rank_of zz) in ( the_rank_of [ <*x, y*>, f]) & ( the_rank_of [ <*x, y*>, f]) in ( the_rank_of [p, f]) or z = c & c in ( rng p) by A3, A6, CLASSES1: 82, TARSKI:def 1, TARSKI:def 2;

      then ( the_rank_of zz) in ( the_rank_of [p, f]) by CLASSES1: 82, ORDINAL1: 10;

      then

       A13: z <> [p, f];

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

      then not z in ( rng R) by A5, A13, TARSKI:def 2;

      hence thesis by A11, XBOOLE_0:def 5;

    end;

    definition

      let x,y,c be object;

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

      :: FACIRC_1:def14

      func 2GatesCircuit (x,y,c,f) -> strict Boolean gate`2=den Circuit of ( 2GatesCircStr (x,y,c,f)) equals (( 1GateCircuit (x,y,f)) +* ( 1GateCircuit ( [ <*x, y*>, f],c,f)));

      coherence ;

    end

    theorem :: FACIRC_1:58

    

     Th58: ( InnerVertices ( 2GatesCircStr (x,y,c,f))) is Relation

    proof

      ( InnerVertices ( 2GatesCircStr (x,y,c,f))) = { [ <*x, y*>, f], ( 2GatesCircOutput (x,y,c,f))} by Th56;

      hence thesis;

    end;

    theorem :: FACIRC_1:59

    

     Th59: for x,y,c be non pair object holds ( InputVertices ( 2GatesCircStr (x,y,c,f))) is without_pairs

    proof

      let x,y,c be non pair object;

      ( InputVertices ( 2GatesCircStr (x,y,c,f))) = {x, y, c} by Th57;

      hence thesis;

    end;

    theorem :: FACIRC_1:60

    

     Th60: x in the carrier of ( 2GatesCircStr (x,y,c,f)) & y in the carrier of ( 2GatesCircStr (x,y,c,f)) & c in the carrier of ( 2GatesCircStr (x,y,c,f))

    proof

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

      set S2 = ( 1GateCircStr ( <* [ <*x, y*>, f], c*>,f));

      

       A1: c in the carrier of S2 by Th43;

      x in the carrier of S1 & y in the carrier of S1 by Th43;

      hence thesis by A1, Th20;

    end;

    theorem :: FACIRC_1:61

     [ <*x, y*>, f] in the carrier of ( 2GatesCircStr (x,y,c,f)) & [ <* [ <*x, y*>, f], c*>, f] in the carrier of ( 2GatesCircStr (x,y,c,f))

    proof

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

      set S2 = ( 1GateCircStr ( <* [ <*x, y*>, f], c*>,f));

       [ <*x, y*>, f] in the carrier of S1 & [ <* [ <*x, y*>, f], c*>, f] in the carrier of S2 by Th43;

      hence thesis by Th20;

    end;

    definition

      let S be unsplit non void non empty ManySortedSign;

      let A be Boolean Circuit of S;

      let s be State of A;

      let v be Vertex of S;

      :: original: .

      redefine

      func s . v -> Element of BOOLEAN ;

      coherence

      proof

        (s . v) in (the Sorts of A . v) by CIRCUIT1: 4;

        hence thesis by CIRCCOMB:def 14;

      end;

    end

    reserve s for State of ( 2GatesCircuit (x,y,c,f));

    

     Lm1: c <> [ <*x, y*>, f] implies (( 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

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

      reconsider vx = x, vy = y as Vertex of S1 by Th43;

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

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

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

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

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

      

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

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

      ( InnerVertices S) = { [ <*x, y*>, f], ( 2GatesCircOutput (x,y,c,f))} by Th56;

      then

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

      

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

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

      then

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

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

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

      then

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

      reconsider xyf1 = xyf as Element of ( InnerVertices S1) by Th47;

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

      

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

      assume c <> [ <*x, y*>, f];

      then

       A5: ( InputVertices S) = {x, y, c} by Th57;

      then

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

      

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

      .= (f . <*(s2 . xyf9), (s2 . c9)*>) by Th48

      .= (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 Th48

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

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

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

      hence thesis by A6, CIRCUIT2:def 5;

    end;

    theorem :: FACIRC_1:62

    

     Th62: c <> [ <*x, y*>, f] implies (( Following (s,2)) . ( 2GatesCircOutput (x,y,c,f))) = (f . <*(f . <*(s . x), (s . y)*>), (s . c)*>) & (( Following (s,2)) . [ <*x, y*>, f]) = (f . <*(s . x), (s . y)*>) & (( Following (s,2)) . x) = (s . x) & (( Following (s,2)) . y) = (s . y) & (( Following (s,2)) . c) = (s . c)

    proof

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

      

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

      reconsider xx = x, yy = y, cc = c as Vertex of S by Th60;

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

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

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

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

      

       A2: x in {x, y} by TARSKI:def 2;

      assume c <> [ <*x, y*>, f];

      then

       A3: ( InputVertices S) = {x, y, c} by Th57;

      then

       A4: x in ( InputVertices S) by ENUMSET1:def 1;

      then

       A5: (( Following s) . xx) = (s . x) by CIRCUIT2:def 5;

      ( InnerVertices S) = { [ <*x, y*>, f], ( 2GatesCircOutput (x,y,c,f))} by Th56;

      then

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

      

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

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

      then

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

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

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

      then

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

      reconsider vx = x, vy = y as Vertex of S1 by Th43;

      set fs = ( Following s);

      reconsider fs1 = (fs | the carrier of S1) as State of A1 by Th26;

      

       A8: y in {x, y} by TARSKI:def 2;

      reconsider fs2 = (fs | the carrier of S2) as State of A2 by Th26;

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

      

       A9: ( dom fs2) = the carrier of S2 by CIRCUIT1: 3;

      

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

      then (( Following s) . cc) = (s . c) by CIRCUIT2:def 5;

      then

       A11: (( Following ( Following s)) . cc) = (s . c) by A10, CIRCUIT2:def 5;

      reconsider xyf1 = xyf as Element of ( InnerVertices S1) by Th47;

      

       A12: ( dom fs1) = the carrier of S1 by CIRCUIT1: 3;

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

      

       A13: xyf in ( InnerVertices S1) by Th47;

      

       A14: ( dom s1) = the carrier of S1 & ( InputVertices S1) = ( rng <*x, y*>) by CIRCCOMB: 42, CIRCUIT1: 3;

      

       A15: ( Following (s,(1 + 1))) = ( Following ( Following s)) by Th15;

      

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

      .= (f . <*(fs2 . xyf9), (fs2 . c9)*>) by Th48

      .= (f . <*(( Following s) . xyf), (fs2 . c)*>) by A9, FUNCT_1: 47

      .= (f . <*(( Following s) . xyf), (( Following s) . c9)*>) by A9, FUNCT_1: 47

      .= (f . <*(( Following s) . xyf), (s . cc)*>) by A10, CIRCUIT2:def 5

      .= (f . <*(( Following s1) . xyf), (s . cc)*>) by A13, CIRCCOMB: 64

      .= (f . <*(f . <*(s1 . x), (s1 . y)*>), (s . cc)*>) by Th48

      .= (f . <*(f . <*(s . x), (s1 . y)*>), (s . cc)*>) by A2, A14, A1, FUNCT_1: 47

      .= (f . <*(f . <*(s . x), (s . y)*>), (s . c)*>) by A8, A14, A1, FUNCT_1: 47;

      

       A16: y in ( InputVertices S) by A3, ENUMSET1:def 1;

      then

       A17: (( Following s) . yy) = (s . y) by CIRCUIT2:def 5;

      then

       A18: (( Following ( Following s)) . yy) = (s . y) by A16, CIRCUIT2:def 5;

      

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

      .= (f . <*(fs1 . vx), (fs1 . vy)*>) by Th48

      .= (f . <*(s . x), (fs1 . vy)*>) by A5, A12, FUNCT_1: 47

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

      (( Following ( Following s)) . xx) = (s . x) by A4, A5, CIRCUIT2:def 5;

      hence thesis by A18, A11, Th15;

    end;

    theorem :: FACIRC_1:63

    

     Th63: c <> [ <*x, y*>, f] implies ( Following (s,2)) is stable

    proof

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

      assume

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

      now

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

        let a be object;

        

         A2: (( InputVertices S) \/ ( InnerVertices S)) = the carrier of S by XBOOLE_1: 45;

        assume a in the carrier of S;

        then

        reconsider v = a as Vertex of S;

        

         A3: ( InnerVertices S) = { [ <*x, y*>, f], ( 2GatesCircOutput (x,y,c,f))} by Th56;

        

         A4: (( Following (s,2)) . c) = (s . c) by A1, Th62;

        

         A5: (( Following (s,2)) . x) = (s . x) & (( Following (s,2)) . y) = (s . y) by A1, Th62;

        

         A6: (( Following (s,2)) . [ <*x, y*>, f]) = (f . <*(s . x), (s . y)*>) & (( Following (s,2)) . ( 2GatesCircOutput (x,y,c,f))) = (f . <*(f . <*(s . x), (s . y)*>), (s . c)*>) by A1, Th62;

        

         A7: ( InputVertices S) = {x, y, c} by A1, Th57;

        per cases by A2, XBOOLE_0:def 3;

          suppose v in ( InputVertices S);

          then v = x or v = y or v = c by A7, ENUMSET1:def 1;

          hence (( Following ( Following (s,2))) . a) = (( Following (s,2)) . a) by A1, Lm1;

        end;

          suppose v in ( InnerVertices S);

          then v = [ <*x, y*>, f] or v = ( 2GatesCircOutput (x,y,c,f)) by A3, TARSKI:def 2;

          hence (( Following ( Following (s,2))) . a) = (( Following (s,2)) . a) by A1, A6, A5, A4, Lm1;

        end;

      end;

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

    end;

    theorem :: FACIRC_1:64

    

     Th64: c <> [ <*x, y*>, 'xor' ] implies for s be State of ( 2GatesCircuit (x,y,c, 'xor' )) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . c) holds (( Following (s,2)) . ( 2GatesCircOutput (x,y,c, 'xor' ))) = ((a1 'xor' a2) 'xor' a3)

    proof

      set f = 'xor' ;

      assume

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

      let s be State of ( 2GatesCircuit (x,y,c,f));

      let a1,a2,a3 be Element of BOOLEAN ;

      assume a1 = (s . x) & a2 = (s . y) & a3 = (s . c);

      

      hence (( Following (s,2)) . ( 2GatesCircOutput (x,y,c,f))) = (f . <*(f . <*a1, a2*>), a3*>) by A1, Th62

      .= (f . <*(a1 'xor' a2), a3*>) by Def3

      .= ((a1 'xor' a2) 'xor' a3) by Def3;

    end;

    theorem :: FACIRC_1:65

    c <> [ <*x, y*>, 'or' ] implies for s be State of ( 2GatesCircuit (x,y,c, 'or' )) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . c) holds (( Following (s,2)) . ( 2GatesCircOutput (x,y,c, 'or' ))) = ((a1 'or' a2) 'or' a3)

    proof

      set f = 'or' ;

      assume

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

      let s be State of ( 2GatesCircuit (x,y,c,f));

      let a1,a2,a3 be Element of BOOLEAN ;

      assume a1 = (s . x) & a2 = (s . y) & a3 = (s . c);

      

      hence (( Following (s,2)) . ( 2GatesCircOutput (x,y,c,f))) = (f . <*(f . <*a1, a2*>), a3*>) by A1, Th62

      .= (f . <*(a1 'or' a2), a3*>) by Def4

      .= ((a1 'or' a2) 'or' a3) by Def4;

    end;

    theorem :: FACIRC_1:66

    c <> [ <*x, y*>, '&' ] implies for s be State of ( 2GatesCircuit (x,y,c, '&' )) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . c) holds (( Following (s,2)) . ( 2GatesCircOutput (x,y,c, '&' ))) = ((a1 '&' a2) '&' a3)

    proof

      set f = '&' ;

      assume

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

      let s be State of ( 2GatesCircuit (x,y,c,f));

      let a1,a2,a3 be Element of BOOLEAN ;

      assume a1 = (s . x) & a2 = (s . y) & a3 = (s . c);

      

      hence (( Following (s,2)) . ( 2GatesCircOutput (x,y,c,f))) = (f . <*(f . <*a1, a2*>), a3*>) by A1, Th62

      .= (f . <*(a1 '&' a2), a3*>) by Def5

      .= ((a1 '&' a2) '&' a3) by Def5;

    end;

    begin

    definition

      let x,y,c be object;

      :: FACIRC_1:def15

      func BitAdderOutput (x,y,c) -> Element of ( InnerVertices ( 2GatesCircStr (x,y,c, 'xor' ))) equals ( 2GatesCircOutput (x,y,c, 'xor' ));

      coherence ;

    end

    definition

      let x,y,c be object;

      :: FACIRC_1:def16

      func BitAdderCirc (x,y,c) -> strict Boolean gate`2=den Circuit of ( 2GatesCircStr (x,y,c, 'xor' )) equals ( 2GatesCircuit (x,y,c, 'xor' ));

      coherence ;

    end

    definition

      let x,y,c be object;

      :: FACIRC_1:def17

      func MajorityIStr (x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals ((( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' ))) +* ( 1GateCircStr ( <*c, x*>, '&' )));

      correctness ;

    end

    definition

      let x,y,c be object;

      :: FACIRC_1:def18

      func MajorityStr (x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( MajorityIStr (x,y,c)) +* ( 1GateCircStr ( <* [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]*>, or3 )));

      correctness ;

    end

    definition

      let x,y,c be object;

      :: FACIRC_1:def19

      func MajorityICirc (x,y,c) -> strict Boolean gate`2=den Circuit of ( MajorityIStr (x,y,c)) equals ((( 1GateCircuit (x,y, '&' )) +* ( 1GateCircuit (y,c, '&' ))) +* ( 1GateCircuit (c,x, '&' )));

      coherence ;

    end

    theorem :: FACIRC_1:67

    

     Th67: ( InnerVertices ( MajorityStr (x,y,c))) is Relation

    proof

      

       A1: ( InnerVertices ( 1GateCircStr ( <* [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]*>, or3 ))) is Relation by Th38;

      ( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))) is Relation & ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' ))) is Relation by Th38;

      then

       A2: ( InnerVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))) is Relation by Th2, CIRCCOMB: 47;

      ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' ))) is Relation by Th38;

      then ( InnerVertices ( MajorityIStr (x,y,c))) is Relation by A2, Th2, CIRCCOMB: 47;

      hence thesis by A1, Th2, CIRCCOMB: 47;

    end;

    theorem :: FACIRC_1:68

    

     Th68: for x,y,c be non pair object holds ( InputVertices ( MajorityStr (x,y,c))) is without_pairs

    proof

      let x,y,c be non pair object;

      set M = ( MajorityStr (x,y,c)), MI = ( MajorityIStr (x,y,c));

      set S = ( 1GateCircStr ( <* [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]*>, or3 ));

      given xx be pair object such that

       A1: xx in ( InputVertices M);

      

       A2: ( 1GateCircStr ( <*x, y*>, '&' )) tolerates ( 1GateCircStr ( <*y, c*>, '&' )) by CIRCCOMB: 43;

      ( 1GateCircStr ( <*x, y*>, '&' )) tolerates ( 1GateCircStr ( <*c, x*>, '&' )) & ( 1GateCircStr ( <*y, c*>, '&' )) tolerates ( 1GateCircStr ( <*c, x*>, '&' )) by CIRCCOMB: 43;

      then

       A3: (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' ))) tolerates ( 1GateCircStr ( <*c, x*>, '&' )) by A2, CIRCCOMB: 3;

      ( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))) = { [ <*x, y*>, '&' ]} & ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' ))) = { [ <*y, c*>, '&' ]} by CIRCCOMB: 42;

      then ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' ))) = { [ <*c, x*>, '&' ]} & ( InnerVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))) = ( { [ <*x, y*>, '&' ]} \/ { [ <*y, c*>, '&' ]}) by A2, CIRCCOMB: 11, CIRCCOMB: 42;

      

      then

       A4: ( InnerVertices MI) = (( { [ <*x, y*>, '&' ]} \/ { [ <*y, c*>, '&' ]}) \/ { [ <*c, x*>, '&' ]}) by A3, CIRCCOMB: 11

      .= ( { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ]} \/ { [ <*c, x*>, '&' ]}) by ENUMSET1: 1

      .= { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} by ENUMSET1: 3;

      ( InputVertices S) = { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} by Th42;

      then

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

      ( InputVertices ( 1GateCircStr ( <*x, y*>, '&' ))) is without_pairs & ( InputVertices ( 1GateCircStr ( <*y, c*>, '&' ))) is without_pairs by Th41;

      then

       A6: ( InputVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))) is without_pairs by Th8, CIRCCOMB: 47;

      ( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) is without_pairs by Th41;

      then

       A7: ( InputVertices MI) is without_pairs by A6, Th8, CIRCCOMB: 47;

      ( InnerVertices S) is Relation by Th38;

      then ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) by A7, Th6;

      hence thesis by A7, A1, A5;

    end;

    theorem :: FACIRC_1:69

    for s be State of ( MajorityICirc (x,y,c)), a,b be Element of BOOLEAN st a = (s . x) & b = (s . y) holds (( Following s) . [ <*x, y*>, '&' ]) = (a '&' b)

    proof

      set xy = <*x, y*>;

      set S1 = ( 1GateCircStr (xy, '&' )), A1 = ( 1GateCircuit (x,y, '&' ));

      reconsider xx = x, yy = y as Vertex of S1 by Th43;

      reconsider v1 = [xy, '&' ] as Element of ( InnerVertices S1) by Th47;

      set S2 = ( 1GateCircStr ( <*y, c*>, '&' )), A2 = ( 1GateCircuit (y,c, '&' ));

      set S3 = ( 1GateCircStr ( <*c, x*>, '&' )), A3 = ( 1GateCircuit (c,x, '&' ));

      set S = ( MajorityIStr (x,y,c)), A = ( MajorityICirc (x,y,c));

      let s be State of A;

      let a,b be Element of BOOLEAN such that

       A1: a = (s . x) & b = (s . y);

      

       A2: A = (A1 +* (A2 +* A3)) by Th25;

      then

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

      

       A3: S = (S1 +* (S2 +* S3)) by CIRCCOMB: 6;

      then

      reconsider v = v1 as Element of ( InnerVertices S) by Th21;

      reconsider xx, yy as Vertex of S by A3, Th20;

      

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

      

      thus (( Following s) . [xy, '&' ]) = (( Following s1) . v) by A3, A2, CIRCCOMB: 64

      .= ( '&' . <*(s1 . xx), (s1 . yy)*>) by Th48

      .= ( '&' . <*(s . xx), (s1 . yy)*>) by A4, FUNCT_1: 47

      .= ( '&' . <*(s . xx), (s . yy)*>) by A4, FUNCT_1: 47

      .= (a '&' b) by A1, Def5;

    end;

    theorem :: FACIRC_1:70

    for s be State of ( MajorityICirc (x,y,c)), a,b be Element of BOOLEAN st a = (s . y) & b = (s . c) holds (( Following s) . [ <*y, c*>, '&' ]) = (a '&' b)

    proof

      set yc = <*y, c*>;

      set S2 = ( 1GateCircStr (yc, '&' )), A2 = ( 1GateCircuit (y,c, '&' ));

      reconsider yy = y, cc = c as Vertex of S2 by Th43;

      reconsider v2 = [yc, '&' ] as Element of ( InnerVertices S2) by Th47;

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

      set S3 = ( 1GateCircStr ( <*c, x*>, '&' )), A3 = ( 1GateCircuit (c,x, '&' ));

      set S = ( MajorityIStr (x,y,c)), A = ( MajorityICirc (x,y,c));

      let s be State of A;

      let a,b be Element of BOOLEAN such that

       A1: a = (s . y) & b = (s . c);

      

       A2: (S1 +* S2) = (S2 +* S1) by CIRCCOMB: 5, CIRCCOMB: 47;

      then

       A3: S = (S2 +* (S1 +* S3)) by CIRCCOMB: 6;

      then

      reconsider v = v2 as Element of ( InnerVertices S) by Th21;

      (A1 +* A2) = (A2 +* A1) by CIRCCOMB: 22, CIRCCOMB: 60;

      then

       A4: A = (A2 +* (A1 +* A3)) by A2, Th25;

      then

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

      reconsider yy, cc as Vertex of S by A3, Th20;

      

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

      

      thus (( Following s) . [yc, '&' ]) = (( Following s2) . v) by A3, A4, CIRCCOMB: 64

      .= ( '&' . <*(s2 . yy), (s2 . cc)*>) by Th48

      .= ( '&' . <*(s . yy), (s2 . cc)*>) by A5, FUNCT_1: 47

      .= ( '&' . <*(s . yy), (s . cc)*>) by A5, FUNCT_1: 47

      .= (a '&' b) by A1, Def5;

    end;

    theorem :: FACIRC_1:71

    for s be State of ( MajorityICirc (x,y,c)), a,b be Element of BOOLEAN st a = (s . c) & b = (s . x) holds (( Following s) . [ <*c, x*>, '&' ]) = (a '&' b)

    proof

      set cx = <*c, x*>;

      set S3 = ( 1GateCircStr (cx, '&' )), A3 = ( 1GateCircuit (c,x, '&' ));

      reconsider cc = c, xx = x as Vertex of S3 by Th43;

      reconsider v3 = [cx, '&' ] as Element of ( InnerVertices S3) by Th47;

      set S = ( MajorityIStr (x,y,c)), A = ( MajorityICirc (x,y,c));

      let s be State of A;

      let a,b be Element of BOOLEAN such that

       A1: a = (s . c) & b = (s . x);

      reconsider cc, xx as Vertex of S by Th20;

      reconsider s3 = (s | the carrier of S3) as State of A3 by Th26;

      reconsider v = v3 as Element of ( InnerVertices S) by Th21;

      

       A2: ( dom s3) = the carrier of S3 by CIRCUIT1: 3;

      

      thus (( Following s) . [cx, '&' ]) = (( Following s3) . v) by CIRCCOMB: 64

      .= ( '&' . <*(s3 . cc), (s3 . xx)*>) by Th48

      .= ( '&' . <*(s . cc), (s3 . xx)*>) by A2, FUNCT_1: 47

      .= ( '&' . <*(s . cc), (s . xx)*>) by A2, FUNCT_1: 47

      .= (a '&' b) by A1, Def5;

    end;

    definition

      let x,y,c be object;

      :: FACIRC_1:def20

      func MajorityOutput (x,y,c) -> Element of ( InnerVertices ( MajorityStr (x,y,c))) equals [ <* [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]*>, or3 ];

      coherence

      proof

         [ <* [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]*>, or3 ] in ( InnerVertices ( 1GateCircStr ( <* [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]*>, or3 ))) by Th47;

        hence thesis by Th21;

      end;

      correctness ;

    end

    definition

      let x,y,c be object;

      :: FACIRC_1:def21

      func MajorityCirc (x,y,c) -> strict Boolean gate`2=den Circuit of ( MajorityStr (x,y,c)) equals (( MajorityICirc (x,y,c)) +* ( 1GateCircuit ( [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ], or3 )));

      coherence ;

    end

    theorem :: FACIRC_1:72

    

     Th72: x in the carrier of ( MajorityStr (x,y,c)) & y in the carrier of ( MajorityStr (x,y,c)) & c in the carrier of ( MajorityStr (x,y,c))

    proof

      c in the carrier of ( 1GateCircStr ( <*c, x*>, '&' )) by Th43;

      then

       A1: c in the carrier of ( MajorityIStr (x,y,c)) by Th20;

      y in the carrier of ( 1GateCircStr ( <*x, y*>, '&' )) by Th43;

      then y in the carrier of (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' ))) by Th20;

      then

       A2: y in the carrier of ( MajorityIStr (x,y,c)) by Th20;

      x in the carrier of ( 1GateCircStr ( <*c, x*>, '&' )) by Th43;

      then x in the carrier of ( MajorityIStr (x,y,c)) by Th20;

      hence thesis by A2, A1, Th20;

    end;

    theorem :: FACIRC_1:73

    

     Th73: [ <*x, y*>, '&' ] in ( InnerVertices ( MajorityStr (x,y,c))) & [ <*y, c*>, '&' ] in ( InnerVertices ( MajorityStr (x,y,c))) & [ <*c, x*>, '&' ] in ( InnerVertices ( MajorityStr (x,y,c)))

    proof

       [ <*x, y*>, '&' ] in ( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))) by Th47;

      then [ <*x, y*>, '&' ] in ( InnerVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))) by Th21;

      then

       A1: [ <*x, y*>, '&' ] in ( InnerVertices ( MajorityIStr (x,y,c))) by Th21;

       [ <*y, c*>, '&' ] in ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' ))) by Th47;

      then [ <*y, c*>, '&' ] in ( InnerVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))) by Th21;

      then

       A2: [ <*y, c*>, '&' ] in ( InnerVertices ( MajorityIStr (x,y,c))) by Th21;

       [ <*c, x*>, '&' ] in ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' ))) by Th47;

      then [ <*c, x*>, '&' ] in ( InnerVertices ( MajorityIStr (x,y,c))) by Th21;

      hence thesis by A1, A2, Th21;

    end;

    theorem :: FACIRC_1:74

    

     Th74: for x,y,c be non pair object holds x in ( InputVertices ( MajorityStr (x,y,c))) & y in ( InputVertices ( MajorityStr (x,y,c))) & c in ( InputVertices ( MajorityStr (x,y,c)))

    proof

      let x,y,c be non pair object;

      assume

       A1: not thesis;

      

       A2: c in the carrier of ( MajorityStr (x,y,c)) by Th72;

      

       A3: ( InnerVertices ( MajorityStr (x,y,c))) is Relation by Th67;

      x in the carrier of ( MajorityStr (x,y,c)) & y in the carrier of ( MajorityStr (x,y,c)) by Th72;

      then x in ( InnerVertices ( MajorityStr (x,y,c))) or y in ( InnerVertices ( MajorityStr (x,y,c))) or c in ( InnerVertices ( MajorityStr (x,y,c))) by A2, A1, XBOOLE_0:def 5;

      then (ex a,b be object st x = [a, b]) or (ex a,b be object st y = [a, b]) or ex a,b be object st c = [a, b] by A3, RELAT_1:def 1;

      hence contradiction;

    end;

    theorem :: FACIRC_1:75

    

     Th75: for x,y,c be non pair object holds ( InputVertices ( MajorityStr (x,y,c))) = {x, y, c} & ( InnerVertices ( MajorityStr (x,y,c))) = ( { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} \/ {( MajorityOutput (x,y,c))})

    proof

      let x,y,c be non pair object;

      set xy = [ <*x, y*>, '&' ], yc = [ <*y, c*>, '&' ], cx = [ <*c, x*>, '&' ];

      set MI = ( MajorityIStr (x,y,c)), S = ( 1GateCircStr ( <*xy, yc, cx*>, or3 ));

      set M = ( MajorityStr (x,y,c));

      

       A1: ( 1GateCircStr ( <*x, y*>, '&' )) tolerates ( 1GateCircStr ( <*y, c*>, '&' )) by CIRCCOMB: 43;

      

       A2: ( InnerVertices S) is Relation by Th38;

      

       A3: ( InputVertices ( 1GateCircStr ( <*y, c*>, '&' ))) = {y, c} by Th40;

      

       A4: ( InnerVertices ( 1GateCircStr ( <*x, y*>, '&' ))) = { [ <*x, y*>, '&' ]} & ( InnerVertices ( 1GateCircStr ( <*y, c*>, '&' ))) = { [ <*y, c*>, '&' ]} by CIRCCOMB: 42;

      then

       A5: ( InnerVertices ( 1GateCircStr ( <*c, x*>, '&' ))) = { [ <*c, x*>, '&' ]} & ( InnerVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))) = ( { [ <*x, y*>, '&' ]} \/ { [ <*y, c*>, '&' ]}) by A1, CIRCCOMB: 11, CIRCCOMB: 42;

      ( 1GateCircStr ( <*x, y*>, '&' )) tolerates ( 1GateCircStr ( <*c, x*>, '&' )) & ( 1GateCircStr ( <*y, c*>, '&' )) tolerates ( 1GateCircStr ( <*c, x*>, '&' )) by CIRCCOMB: 43;

      then (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' ))) tolerates ( 1GateCircStr ( <*c, x*>, '&' )) by A1, CIRCCOMB: 3;

      

      then

       A6: ( InnerVertices MI) = (( { [ <*x, y*>, '&' ]} \/ { [ <*y, c*>, '&' ]}) \/ { [ <*c, x*>, '&' ]}) by A5, CIRCCOMB: 11

      .= ( { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ]} \/ { [ <*c, x*>, '&' ]}) by ENUMSET1: 1

      .= { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} by ENUMSET1: 3;

      ( InputVertices S) = { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} by Th42;

      then

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

      

       A8: ( InputVertices ( 1GateCircStr ( <*x, y*>, '&' ))) = {x, y} & ( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) = {c, x} by Th40;

      

       A9: ( InputVertices ( 1GateCircStr ( <*c, x*>, '&' ))) is without_pairs by Th41;

      

       A10: ( InputVertices ( 1GateCircStr ( <*x, y*>, '&' ))) is without_pairs & ( InputVertices ( 1GateCircStr ( <*y, c*>, '&' ))) is without_pairs by Th41;

      then

       A11: ( InputVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))) is without_pairs by Th8, CIRCCOMB: 47;

      then ( InputVertices MI) is without_pairs by A9, Th8, CIRCCOMB: 47;

      then ( InputVertices M) = (( InputVertices MI) \/ (( InputVertices S) \ ( InnerVertices MI))) by A2, Th6;

      

      hence ( InputVertices M) = (( InputVertices (( 1GateCircStr ( <*x, y*>, '&' )) +* ( 1GateCircStr ( <*y, c*>, '&' )))) \/ ( InputVertices ( 1GateCircStr ( <*c, x*>, '&' )))) by A9, A11, A5, A7, Th7

      .= ((( InputVertices ( 1GateCircStr ( <*x, y*>, '&' ))) \/ ( InputVertices ( 1GateCircStr ( <*y, c*>, '&' )))) \/ ( InputVertices ( 1GateCircStr ( <*c, x*>, '&' )))) by A10, A4, Th7

      .= ( {x, y, y, c} \/ {c, x}) by A8, A3, ENUMSET1: 5

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

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

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

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

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

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

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

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

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

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

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

      MI tolerates S by CIRCCOMB: 47;

      

      hence ( InnerVertices M) = (( InnerVertices MI) \/ ( InnerVertices S)) by CIRCCOMB: 11

      .= ( { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} \/ {( MajorityOutput (x,y,c))}) by A6, CIRCCOMB: 42;

    end;

    

     Lm2: for x,y,c be non pair object holds for s be State of ( MajorityCirc (x,y,c)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . c) holds (( Following s) . [ <*x, y*>, '&' ]) = (a1 '&' a2) & (( Following s) . [ <*y, c*>, '&' ]) = (a2 '&' a3) & (( Following s) . [ <*c, x*>, '&' ]) = (a3 '&' a1)

    proof

      let x,y,c be non pair object;

      let s be State of ( MajorityCirc (x,y,c));

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

       A1: a1 = (s . x) and

       A2: a2 = (s . y) and

       A3: a3 = (s . c);

      set S = ( MajorityStr (x,y,c));

      

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

      

       A5: y in the carrier of S by Th72;

      

       A6: x in the carrier of S by Th72;

      

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

       [ <*x, y*>, '&' ] in ( InnerVertices ( MajorityStr (x,y,c))) by Th73;

      

      hence (( Following s) . [ <*x, y*>, '&' ]) = ( '&' . (s * <*x, y*>)) by A7, Th35

      .= ( '&' . <*a1, a2*>) by A1, A2, A4, A6, A5, FINSEQ_2: 125

      .= (a1 '&' a2) by Def5;

      

       A8: c in the carrier of S by Th72;

       [ <*y, c*>, '&' ] in ( InnerVertices ( MajorityStr (x,y,c))) by Th73;

      

      hence (( Following s) . [ <*y, c*>, '&' ]) = ( '&' . (s * <*y, c*>)) by A7, Th35

      .= ( '&' . <*a2, a3*>) by A2, A3, A4, A5, A8, FINSEQ_2: 125

      .= (a2 '&' a3) by Def5;

       [ <*c, x*>, '&' ] in ( InnerVertices ( MajorityStr (x,y,c))) by Th73;

      

      hence (( Following s) . [ <*c, x*>, '&' ]) = ( '&' . (s * <*c, x*>)) by A7, Th35

      .= ( '&' . <*a3, a1*>) by A1, A3, A4, A6, A8, FINSEQ_2: 125

      .= (a3 '&' a1) by Def5;

    end;

    theorem :: FACIRC_1:76

    for x,y,c be non pair object holds for s be State of ( MajorityCirc (x,y,c)) holds for a1,a2 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) holds (( Following s) . [ <*x, y*>, '&' ]) = (a1 '&' a2)

    proof

      let x,y,c be non pair object;

      reconsider a = c as Vertex of ( MajorityStr (x,y,c)) by Th72;

      let s be State of ( MajorityCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm2;

    end;

    theorem :: FACIRC_1:77

    for x,y,c be non pair object holds for s be State of ( MajorityCirc (x,y,c)) holds for a2,a3 be Element of BOOLEAN st a2 = (s . y) & a3 = (s . c) holds (( Following s) . [ <*y, c*>, '&' ]) = (a2 '&' a3)

    proof

      let x,y,c be non pair object;

      reconsider a = x as Vertex of ( MajorityStr (x,y,c)) by Th72;

      let s be State of ( MajorityCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm2;

    end;

    theorem :: FACIRC_1:78

    for x,y,c be non pair object holds for s be State of ( MajorityCirc (x,y,c)) holds for a1,a3 be Element of BOOLEAN st a1 = (s . x) & a3 = (s . c) holds (( Following s) . [ <*c, x*>, '&' ]) = (a3 '&' a1)

    proof

      let x,y,c be non pair object;

      reconsider a = y as Vertex of ( MajorityStr (x,y,c)) by Th72;

      let s be State of ( MajorityCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm2;

    end;

    theorem :: FACIRC_1:79

    

     Th79: for x,y,c be non pair object holds for s be State of ( MajorityCirc (x,y,c)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . [ <*x, y*>, '&' ]) & a2 = (s . [ <*y, c*>, '&' ]) & a3 = (s . [ <*c, x*>, '&' ]) holds (( Following s) . ( MajorityOutput (x,y,c))) = ((a1 'or' a2) 'or' a3)

    proof

      let x,y,c be non pair object;

      set xy = [ <*x, y*>, '&' ], yc = [ <*y, c*>, '&' ], cx = [ <*c, x*>, '&' ];

      set S = ( MajorityStr (x,y,c));

      reconsider xy, yc, cx as Element of ( InnerVertices S) by Th73;

      let s be State of ( MajorityCirc (x,y,c));

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

       A1: a1 = (s . [ <*x, y*>, '&' ]) & a2 = (s . [ <*y, c*>, '&' ]) & a3 = (s . [ <*c, x*>, '&' ]);

      

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

      ( InnerVertices S) = the carrier' of S by Th37;

      

      hence (( Following s) . ( MajorityOutput (x,y,c))) = ( or3 . (s * <*xy, yc, cx*>)) by Th35

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

      .= ((a1 'or' a2) 'or' a3) by Def6;

    end;

    

     Lm3: for x,y,c be non pair object holds for s be State of ( MajorityCirc (x,y,c)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . c) holds (( Following (s,2)) . ( MajorityOutput (x,y,c))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) & (( Following (s,2)) . [ <*x, y*>, '&' ]) = (a1 '&' a2) & (( Following (s,2)) . [ <*y, c*>, '&' ]) = (a2 '&' a3) & (( Following (s,2)) . [ <*c, x*>, '&' ]) = (a3 '&' a1)

    proof

      let x,y,c be non pair object;

      set S = ( MajorityStr (x,y,c));

      reconsider x9 = x, y9 = y, c9 = c as Vertex of S by Th72;

      let s be State of ( MajorityCirc (x,y,c));

      set xy = [ <*x, y*>, '&' ], yc = [ <*y, c*>, '&' ], cx = [ <*c, x*>, '&' ];

      

       A1: ( Following (s,2)) = ( Following ( Following s)) by Th15;

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

       A2: a1 = (s . x) & a2 = (s . y) & a3 = (s . c);

      

       A3: (( Following s) . cx) = (a3 '&' a1) by A2, Lm2;

      (( Following s) . xy) = (a1 '&' a2) & (( Following s) . yc) = (a2 '&' a3) by A2, Lm2;

      hence (( Following (s,2)) . ( MajorityOutput (x,y,c))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) by A1, A3, Th79;

      y in ( InputVertices S) by Th74;

      then

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

      c in ( InputVertices S) by Th74;

      then

       A5: (( Following s) . c9) = (s . c) by CIRCUIT2:def 5;

      x in ( InputVertices S) by Th74;

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

      hence thesis by A2, A4, A5, A1, Lm2;

    end;

    theorem :: FACIRC_1:80

    for x,y,c be non pair object holds for s be State of ( MajorityCirc (x,y,c)) holds for a1,a2 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) holds (( Following (s,2)) . [ <*x, y*>, '&' ]) = (a1 '&' a2)

    proof

      let x,y,c be non pair object;

      reconsider a = c as Vertex of ( MajorityStr (x,y,c)) by Th72;

      let s be State of ( MajorityCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm3;

    end;

    theorem :: FACIRC_1:81

    for x,y,c be non pair object holds for s be State of ( MajorityCirc (x,y,c)) holds for a2,a3 be Element of BOOLEAN st a2 = (s . y) & a3 = (s . c) holds (( Following (s,2)) . [ <*y, c*>, '&' ]) = (a2 '&' a3)

    proof

      let x,y,c be non pair object;

      reconsider a = x as Vertex of ( MajorityStr (x,y,c)) by Th72;

      let s be State of ( MajorityCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm3;

    end;

    theorem :: FACIRC_1:82

    for x,y,c be non pair object holds for s be State of ( MajorityCirc (x,y,c)) holds for a1,a3 be Element of BOOLEAN st a1 = (s . x) & a3 = (s . c) holds (( Following (s,2)) . [ <*c, x*>, '&' ]) = (a3 '&' a1)

    proof

      let x,y,c be non pair object;

      reconsider a = y as Vertex of ( MajorityStr (x,y,c)) by Th72;

      let s be State of ( MajorityCirc (x,y,c));

      (s . a) is Element of BOOLEAN ;

      hence thesis by Lm3;

    end;

    theorem :: FACIRC_1:83

    for x,y,c be non pair object holds for s be State of ( MajorityCirc (x,y,c)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . c) holds (( Following (s,2)) . ( MajorityOutput (x,y,c))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) by Lm3;

    theorem :: FACIRC_1:84

    

     Th84: for x,y,c be non pair object holds for s be State of ( MajorityCirc (x,y,c)) holds ( Following (s,2)) is stable

    proof

      let x,y,c be non pair object;

      set S = ( MajorityStr (x,y,c));

      reconsider xx = x, yy = y, cc = c as Vertex of S by Th72;

      let s be State of ( MajorityCirc (x,y,c));

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

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

      

       A1: ffs = ( Following ( Following s)) by Th15;

      

       A2: y in ( InputVertices S) by Th74;

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

      then

       A3: (ffs . y) = a2 by A1, A2, CIRCUIT2:def 5;

      a2 = (s . y);

      then

       A4: (ffs . [ <*c, x*>, '&' ]) = (a3 '&' a1) by Lm3;

      

       A5: x in ( InputVertices S) by Th74;

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

      then

       A6: (ffs . x) = a1 by A1, A5, CIRCUIT2:def 5;

      a1 = (s . x);

      then

       A7: (ffs . [ <*y, c*>, '&' ]) = (a2 '&' a3) by Lm3;

      

       A8: c in ( InputVertices S) by Th74;

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

      then

       A9: (ffs . c) = a3 by A1, A8, CIRCUIT2:def 5;

      a3 = (s . c);

      then

       A10: (ffs . [ <*x, y*>, '&' ]) = (a1 '&' a2) by Lm3;

      

       A11: (ffs . ( MajorityOutput (x,y,c))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1)) by Lm3;

       A12:

      now

        let a be object;

        assume

         A13: a in the carrier of S;

        then

        reconsider v = a as Vertex of S;

        

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

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

        proof

          per cases by A14, XBOOLE_0:def 3;

            suppose v in ( InputVertices S);

            hence thesis by CIRCUIT2:def 5;

          end;

            suppose v in ( InnerVertices S);

            then v in ( { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} \/ {( MajorityOutput (x,y,c))}) by Th75;

            then v in { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} or v in {( MajorityOutput (x,y,c))} by XBOOLE_0:def 3;

            then v = [ <*x, y*>, '&' ] or v = [ <*y, c*>, '&' ] or v = [ <*c, x*>, '&' ] or v = ( MajorityOutput (x,y,c)) by ENUMSET1:def 1, TARSKI:def 1;

            hence thesis by A11, A10, A7, A4, A6, A3, A9, Lm2, Th79;

          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 A12, FUNCT_1: 2;

    end;

    definition

      let x,y,c be object;

      :: FACIRC_1:def22

      func BitAdderWithOverflowStr (x,y,c) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign equals (( 2GatesCircStr (x,y,c, 'xor' )) +* ( MajorityStr (x,y,c)));

      coherence ;

    end

    theorem :: FACIRC_1:85

    

     Th85: for x,y,c be non pair object holds ( InputVertices ( BitAdderWithOverflowStr (x,y,c))) = {x, y, c}

    proof

      let x,y,c be non pair object;

      set S = ( BitAdderWithOverflowStr (x,y,c));

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' )), S2 = ( MajorityStr (x,y,c));

      

       A1: ( InputVertices S1) = {x, y, c} & ( InputVertices S2) = {x, y, c} by Th57, Th75;

      ( InnerVertices S1) is Relation & ( InnerVertices S2) is Relation by Th58, Th67;

      

      hence ( InputVertices S) = ( {x, y, c} \/ {x, y, c}) by A1, Th7

      .= {x, y, c};

    end;

    theorem :: FACIRC_1:86

    for x,y,c be non pair object holds ( InnerVertices ( BitAdderWithOverflowStr (x,y,c))) = (( { [ <*x, y*>, 'xor' ], ( 2GatesCircOutput (x,y,c, 'xor' ))} \/ { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]}) \/ {( MajorityOutput (x,y,c))})

    proof

      let x,y,c be non pair object;

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' )), S2 = ( MajorityStr (x,y,c));

      

       A1: ( InnerVertices S2) = ( { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} \/ {( MajorityOutput (x,y,c))}) by Th75;

      (( { [ <*x, y*>, 'xor' ], ( 2GatesCircOutput (x,y,c, 'xor' ))} \/ { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]}) \/ {( MajorityOutput (x,y,c))}) = ( { [ <*x, y*>, 'xor' ], ( 2GatesCircOutput (x,y,c, 'xor' ))} \/ ( { [ <*x, y*>, '&' ], [ <*y, c*>, '&' ], [ <*c, x*>, '&' ]} \/ {( MajorityOutput (x,y,c))})) & ( InnerVertices S1) = { [ <*x, y*>, 'xor' ], ( 2GatesCircOutput (x,y,c, 'xor' ))} by Th56, XBOOLE_1: 4;

      hence thesis by A1, Th27;

    end;

    theorem :: FACIRC_1:87

    for S be non empty ManySortedSign st S = ( BitAdderWithOverflowStr (x,y,c)) holds x in the carrier of S & y in the carrier of S & c in the carrier of S

    proof

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' ));

      let S be non empty ManySortedSign;

      assume

       A1: S = ( BitAdderWithOverflowStr (x,y,c));

      

       A2: c in the carrier of S1 by Th60;

      x in the carrier of S1 & y in the carrier of S1 by Th60;

      hence thesis by A1, A2, Th20;

    end;

    definition

      let x,y,c be object;

      :: FACIRC_1:def23

      func BitAdderWithOverflowCirc (x,y,c) -> strict Boolean gate`2=den Circuit of ( BitAdderWithOverflowStr (x,y,c)) equals (( BitAdderCirc (x,y,c)) +* ( MajorityCirc (x,y,c)));

      coherence ;

    end

    theorem :: FACIRC_1:88

    ( InnerVertices ( BitAdderWithOverflowStr (x,y,c))) is Relation

    proof

      ( InnerVertices ( 2GatesCircStr (x,y,c, 'xor' ))) is Relation & ( InnerVertices ( MajorityStr (x,y,c))) is Relation by Th58, Th67;

      hence thesis by Th2, CIRCCOMB: 47;

    end;

    theorem :: FACIRC_1:89

    for x,y,c be non pair object holds ( InputVertices ( BitAdderWithOverflowStr (x,y,c))) is without_pairs

    proof

      let x,y,c be non pair object;

      ( InputVertices ( BitAdderWithOverflowStr (x,y,c))) = {x, y, c} by Th85;

      hence thesis;

    end;

    theorem :: FACIRC_1:90

    ( BitAdderOutput (x,y,c)) in ( InnerVertices ( BitAdderWithOverflowStr (x,y,c))) & ( MajorityOutput (x,y,c)) in ( InnerVertices ( BitAdderWithOverflowStr (x,y,c))) by Th21;

    theorem :: FACIRC_1:91

    for x,y,c be non pair object holds for s be State of ( BitAdderWithOverflowCirc (x,y,c)) holds for a1,a2,a3 be Element of BOOLEAN st a1 = (s . x) & a2 = (s . y) & a3 = (s . c) holds (( Following (s,2)) . ( BitAdderOutput (x,y,c))) = ((a1 'xor' a2) 'xor' a3) & (( Following (s,2)) . ( MajorityOutput (x,y,c))) = (((a1 '&' a2) 'or' (a2 '&' a3)) 'or' (a3 '&' a1))

    proof

      let x,y,c be non pair object;

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' )), S2 = ( MajorityStr (x,y,c));

      set A = ( BitAdderWithOverflowCirc (x,y,c));

      set A1 = ( BitAdderCirc (x,y,c)), A2 = ( MajorityCirc (x,y,c));

      let s be State of A;

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

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

      set f = 'xor' ;

      let a1,a2,a3 be Element of BOOLEAN ;

      assume that

       A1: a1 = (s . x) and

       A2: a2 = (s . y) and

       A3: a3 = (s . c);

      

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

      y in the carrier of S1 by Th60;

      then

       A5: a2 = (s1 . y) by A2, A4, FUNCT_1: 47;

      ( InputVertices S1) is without_pairs by Th59;

      then ( InnerVertices S2) misses ( InputVertices S1) by Th5, Th67;

      then

       A6: (( Following (t,2)) . ( 2GatesCircOutput (x,y,c,f))) = (( Following (s1,2)) . ( 2GatesCircOutput (x,y,c,f))) by Th32;

      c in the carrier of S1 by Th60;

      then

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

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

      

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

      x in the carrier of S1 by Th60;

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

      hence (( Following (s,2)) . ( BitAdderOutput (x,y,c))) = ((a1 'xor' a2) 'xor' a3) by A5, A7, A6, Th64;

      ( InputVertices S2) is without_pairs by Th68;

      then ( InnerVertices S1) misses ( InputVertices S2) by Th5, Th58;

      then

       A9: (( Following (t,2)) . ( MajorityOutput (x,y,c))) = (( Following (s2,2)) . ( MajorityOutput (x,y,c))) by Th33;

      c in the carrier of S2 by Th72;

      then

       A10: a3 = (s2 . c) by A3, A8, FUNCT_1: 47;

      y in the carrier of S2 by Th72;

      then

       A11: a2 = (s2 . y) by A2, A8, FUNCT_1: 47;

      x in the carrier of S2 by Th72;

      then a1 = (s2 . x) by A1, A8, FUNCT_1: 47;

      hence thesis by A11, A10, A9, Lm3;

    end;

    theorem :: FACIRC_1:92

    for x,y,c be non pair object holds for s be State of ( BitAdderWithOverflowCirc (x,y,c)) holds ( Following (s,2)) is stable

    proof

      let x,y,c be non pair object;

      set S1 = ( 2GatesCircStr (x,y,c, 'xor' )), S2 = ( MajorityStr (x,y,c));

      set A = ( BitAdderWithOverflowCirc (x,y,c));

      set A1 = ( BitAdderCirc (x,y,c)), A2 = ( MajorityCirc (x,y,c));

      let s be State of A;

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

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

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

      set S = ( BitAdderWithOverflowStr (x,y,c));

      

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

      

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

      ( InputVertices S1) is without_pairs by Th59;

      then ( InnerVertices S2) misses ( InputVertices S1) by Th5, Th67;

      then

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

      ( Following (s1,2)) is stable by Th63;

      

      then

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

      .= ( Following (s1,(2 + 1))) by Th12;

      ( InputVertices S2) is without_pairs by Th68;

      then ( InnerVertices S1) misses ( InputVertices S2) by Th5, Th58;

      then

       A5: ( Following (s2,2)) = (( Following (t,2)) | the carrier of S2) & ( Following (s2,3)) = (( Following (t,3)) | the carrier of S2) by Th31;

      ( Following (s2,2)) is stable by Th84;

      

      then

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

      .= ( Following (s2,(2 + 1))) by Th12;

      

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

       A8:

      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 A2, 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 A3, A5, A4, A6, A7, FUNCT_1: 47;

        hence (( Following (s,2)) . a) = (( Following ( Following (s,2))) . a) by A4, A6, Th12;

      end;

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

      hence ( Following (s,2)) = ( Following ( Following (s,2))) by A1, A8, FUNCT_1: 2;

    end;