circcmb3.miz



    begin

    theorem :: CIRCCMB3:1

    

     Th1: for S be non void Circuit-like non empty ManySortedSign holds for A be non-empty Circuit of S holds for s be State of A, x be set st x in ( InputVertices S) holds for n be Nat holds (( Following (s,n)) . x) = (s . 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, x be set such that

       A1: x in ( InputVertices S);

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

       A2:

      now

        let n be Nat;

        assume

         A3: P[n];

        (( Following (s,(n + 1))) . x) = (( Following ( Following (s,n))) . x) by FACIRC_1: 12

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

        hence P[(n + 1)];

      end;

      

       A4: P[ 0 ] by FACIRC_1: 11;

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

    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;

      :: CIRCCMB3:def1

      attr s is stabilizing means ex n be Element of NAT st ( Following (s,n)) is stable;

    end

    definition

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

      let A be non-empty Circuit of S;

      :: CIRCCMB3:def2

      attr A is stabilizing means

      : Def2: for s be State of A holds s is stabilizing;

      :: CIRCCMB3:def3

      attr A is with_stabilization-limit means ex n be Element of NAT st for s be State of A holds ( Following (s,n)) is stable;

    end

    registration

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

      cluster with_stabilization-limit -> stabilizing for non-empty Circuit of S;

      coherence

      proof

        let A be non-empty Circuit of S;

        given n be Element of NAT such that

         A1: for s be State of A holds ( Following (s,n)) is stable;

        let s be State of A;

        take n;

        thus thesis by A1;

      end;

    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;

      :: CIRCCMB3:def4

      func Result s -> State of A means

      : Def4: it is stable & ex n be Element of NAT st it = ( Following (s,n));

      existence by A1;

      uniqueness

      proof

        let s1,s2 be State of A;

        assume that

         A2: s1 is stable and

         A3: ex n be Element of NAT st s1 = ( Following (s,n)) and

         A4: s2 is stable and

         A5: ex n be Element of NAT st s2 = ( Following (s,n));

        consider n1 be Element of NAT such that

         A6: s1 = ( Following (s,n1)) by A3;

        consider n2 be Element of NAT such that

         A7: s2 = ( Following (s,n2)) by A5;

        per cases ;

          suppose n1 <= n2;

          hence thesis by A2, A6, A7, CIRCCMB2: 4;

        end;

          suppose n2 <= n1;

          hence thesis by A4, A6, A7, CIRCCMB2: 4;

        end;

      end;

    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;

      :: CIRCCMB3:def5

      func stabilization-time s -> Element of NAT means

      : Def5: ( Following (s,it )) is stable & for n be Element of NAT st n < it holds not ( Following (s,n)) is stable;

      existence

      proof

        defpred P[ Nat] means ( Following (s,$1)) is stable;

        ex k be Element of NAT st P[k] by A1;

        then

         A2: ex k be Nat st P[k];

        consider m be Nat such that

         A3: P[m] & for n be Nat st P[n] holds m <= n from NAT_1:sch 5( A2);

        reconsider m as Element of NAT by ORDINAL1:def 12;

        take m;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let n1,n2 be Element of NAT such that

         A4: ( Following (s,n1)) is stable and

         A5: (for n be Element of NAT st n < n1 holds not ( Following (s,n)) is stable) & ( Following (s,n2)) is stable and

         A6: for n be Element of NAT st n < n2 holds not ( Following (s,n)) is stable;

        assume

         A7: n1 <> n2;

        per cases by A7, XXREAL_0: 1;

          suppose n1 < n2;

          hence contradiction by A4, A6;

        end;

          suppose n2 < n1;

          hence contradiction by A5;

        end;

      end;

    end

    theorem :: CIRCCMB3:2

    

     Th2: for S be non void Circuit-like non empty ManySortedSign holds for A be non-empty Circuit of S holds for s be State of A st s is stabilizing holds ( Result s) = ( Following (s,( stabilization-time s)))

    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 such that

       A1: s is stabilizing;

      ( Following (s,( stabilization-time s))) is stable by A1, Def5;

      hence thesis by A1, Def4;

    end;

    theorem :: CIRCCMB3:3

    for S be non void Circuit-like non empty ManySortedSign holds for A be non-empty Circuit of S holds for s be State of A, n be Element of NAT st ( Following (s,n)) is stable holds ( stabilization-time s) <= n

    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, n be Element of NAT ;

      assume

       A1: ( Following (s,n)) is stable;

      then s is stabilizing;

      hence thesis by A1, Def5;

    end;

    theorem :: CIRCCMB3:4

    

     Th4: for S be non void Circuit-like non empty ManySortedSign holds for A be non-empty Circuit of S holds for s be State of A, n be Element of NAT st ( Following (s,n)) is stable holds ( Result s) = ( Following (s,n))

    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, n be Element of NAT ;

      assume

       A1: ( Following (s,n)) is stable;

      then s is stabilizing;

      hence thesis by A1, Def4;

    end;

    theorem :: CIRCCMB3:5

    

     Th5: for S be non void Circuit-like non empty ManySortedSign holds for A be non-empty Circuit of S holds for s be State of A, n be Element of NAT st s is stabilizing & n >= ( stabilization-time s) holds ( Result s) = ( Following (s,n))

    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, n be Element of NAT ;

      assume that

       A1: s is stabilizing and

       A2: n >= ( stabilization-time s);

      ( Result s) is stable by A1, Def4;

      then ( Following (s,( stabilization-time s))) is stable by A1, Th2;

      then ( Following (s,n)) is stable by A2, CIRCCMB2: 4;

      hence thesis by Th4;

    end;

    theorem :: CIRCCMB3:6

    for S be non void Circuit-like non empty ManySortedSign holds for A be non-empty Circuit of S holds for s be State of A st s is stabilizing holds for x be set st x in ( InputVertices S) holds (( Result s) . x) = (s . 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;

      assume s is stabilizing;

      then ( Result s) = ( Following (s,( stabilization-time s))) by Th2;

      hence thesis by Th1;

    end;

    theorem :: CIRCCMB3:7

    

     Th7: for S1,S2 be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) misses ( InnerVertices S2) & ( InputVertices S2) misses ( InnerVertices S1) holds for S be non void Circuit-like non empty ManySortedSign st S = (S1 +* S2) holds for A1 be non-empty Circuit of S1 holds for A2 be non-empty Circuit of S2 st A1 tolerates A2 holds for A be non-empty Circuit of S st A = (A1 +* A2) holds for s be State of A holds for s1 be State of A1 holds for s2 be State of A2 st s1 = (s | the carrier of S1) & s2 = (s | the carrier of S2) & s1 is stabilizing & s2 is stabilizing holds s is stabilizing

    proof

      let S1,S2 be non void Circuit-like non empty ManySortedSign such that

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

      let S be non void Circuit-like non empty ManySortedSign such that

       A2: S = (S1 +* S2);

      let A1 be non-empty Circuit of S1;

      let A2 be non-empty Circuit of S2;

      assume

       A3: A1 tolerates A2;

      let A be non-empty Circuit of S such that

       A4: A = (A1 +* A2);

      let s be State of A;

      let s1 be State of A1;

      let s2 be State of A2;

      assume that

       A5: s1 = (s | the carrier of S1) & s2 = (s | the carrier of S2) and

       A6: s1 is stabilizing and

       A7: s2 is stabilizing;

      consider n1 be Element of NAT such that

       A8: ( Following (s1,n1)) is stable by A6;

      consider n2 be Element of NAT such that

       A9: ( Following (s2,n2)) is stable by A7;

      ( Following (s,( max (n1,n2)))) is stable by A1, A2, A3, A4, A5, A8, A9, CIRCCMB2: 22;

      hence thesis;

    end;

    theorem :: CIRCCMB3:8

    for S1,S2 be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) misses ( InnerVertices S2) & ( InputVertices S2) misses ( InnerVertices S1) holds for S be non void Circuit-like non empty ManySortedSign st S = (S1 +* S2) holds for A1 be non-empty Circuit of S1 holds for A2 be non-empty Circuit of S2 st A1 tolerates A2 holds for A be non-empty Circuit of S st A = (A1 +* A2) holds for s be State of A holds for s1 be State of A1 st s1 = (s | the carrier of S1) & s1 is stabilizing holds for s2 be State of A2 st s2 = (s | the carrier of S2) & s2 is stabilizing holds ( stabilization-time s) = ( max (( stabilization-time s1),( stabilization-time s2)))

    proof

      let S1,S2 be non void Circuit-like non empty ManySortedSign such that

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

      let S be non void Circuit-like non empty ManySortedSign such that

       A2: S = (S1 +* S2);

      let A1 be non-empty Circuit of S1;

      let A2 be non-empty Circuit of S2;

      assume

       A3: A1 tolerates A2;

      let A be non-empty Circuit of S such that

       A4: A = (A1 +* A2);

      let s be State of A;

      let s1 be State of A1 such that

       A5: s1 = (s | the carrier of S1) and

       A6: s1 is stabilizing;

      set st1 = ( stabilization-time s1);

      let s2 be State of A2 such that

       A7: s2 = (s | the carrier of S2) and

       A8: s2 is stabilizing;

      set st2 = ( stabilization-time s2);

      

       A9: ( Following (s1,st1)) is stable by A6, Def5;

       A10:

      now

        let n be Element of NAT such that

         A11: n < ( max (st1,st2));

        per cases ;

          suppose st1 <= st2;

          then n < st2 by A11, XXREAL_0:def 10;

          then not ( Following (s2,n)) is stable by A8, Def5;

          hence not ( Following (s,n)) is stable by A1, A2, A3, A4, A5, A7, CIRCCMB2: 23;

        end;

          suppose st2 <= st1;

          then n < st1 by A11, XXREAL_0:def 10;

          then not ( Following (s1,n)) is stable by A6, Def5;

          hence not ( Following (s,n)) is stable by A1, A2, A3, A4, A5, A7, CIRCCMB2: 23;

        end;

      end;

      ( Following (s2,st2)) is stable by A8, Def5;

      then

       A12: ( Following (s,( max (st1,st2)))) is stable by A1, A2, A3, A4, A5, A7, A9, CIRCCMB2: 22;

      s is stabilizing by A1, A2, A3, A4, A5, A6, A7, A8, Th7;

      hence thesis by A12, A10, Def5;

    end;

    theorem :: CIRCCMB3:9

    

     Th9: for S1,S2 be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) misses ( InnerVertices S2) holds for S be non void Circuit-like non empty ManySortedSign st S = (S1 +* S2) holds for A1 be non-empty Circuit of S1 holds for A2 be non-empty Circuit of S2 st A1 tolerates A2 holds for A be non-empty Circuit of S st A = (A1 +* A2) holds for s be State of A holds for s1 be State of A1 st s1 = (s | the carrier of S1) & s1 is stabilizing holds for s2 be State of A2 st s2 = (( Following (s,( stabilization-time s1))) | the carrier of S2) & s2 is stabilizing holds s is stabilizing

    proof

      let S1,S2 be non void Circuit-like non empty ManySortedSign such that

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

      let S be non void Circuit-like non empty ManySortedSign such that

       A2: S = (S1 +* S2);

      let A1 be non-empty Circuit of S1;

      let A2 be non-empty Circuit of S2;

      assume

       A3: A1 tolerates A2;

      let A be non-empty Circuit of S such that

       A4: A = (A1 +* A2);

      let s be State of A;

      let s1 be State of A1 such that

       A5: s1 = (s | the carrier of S1) and

       A6: s1 is stabilizing;

      set n1 = ( stabilization-time s1);

      

       A7: ( Following (s1,n1)) is stable by A6, Def5;

      let s2 be State of A2 such that

       A8: s2 = (( Following (s,n1)) | the carrier of S2) and

       A9: s2 is stabilizing;

      set n2 = ( stabilization-time s2);

      ( Following (s2,n2)) is stable by A9, Def5;

      then ( Following (s,(n1 + n2))) is stable by A1, A2, A3, A4, A5, A7, A8, CIRCCMB2: 19;

      hence thesis;

    end;

    theorem :: CIRCCMB3:10

    

     Th10: for S1,S2 be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) misses ( InnerVertices S2) holds for S be non void Circuit-like non empty ManySortedSign st S = (S1 +* S2) holds for A1 be non-empty Circuit of S1 holds for A2 be non-empty Circuit of S2 st A1 tolerates A2 holds for A be non-empty Circuit of S st A = (A1 +* A2) holds for s be State of A holds for s1 be State of A1 st s1 = (s | the carrier of S1) & s1 is stabilizing holds for s2 be State of A2 st s2 = (( Following (s,( stabilization-time s1))) | the carrier of S2) & s2 is stabilizing holds ( stabilization-time s) = (( stabilization-time s1) + ( stabilization-time s2))

    proof

      let S1,S2 be non void Circuit-like non empty ManySortedSign such that

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

      let S be non void Circuit-like non empty ManySortedSign such that

       A2: S = (S1 +* S2);

      let A1 be non-empty Circuit of S1;

      let A2 be non-empty Circuit of S2;

      assume

       A3: A1 tolerates A2;

      let A be non-empty Circuit of S such that

       A4: A = (A1 +* A2);

      let s be State of A;

      let s1 be State of A1 such that

       A5: s1 = (s | the carrier of S1) and

       A6: s1 is stabilizing;

      set st1 = ( stabilization-time s1);

      let s2 be State of A2 such that

       A7: s2 = (( Following (s,st1)) | the carrier of S2) and

       A8: s2 is stabilizing;

      set st2 = ( stabilization-time s2);

      

       A9: ( Following (s1,st1)) is stable by A6, Def5;

       A10:

      now

        let n be Element of NAT such that

         A11: n < (st1 + st2);

        per cases ;

          suppose st1 <= n;

          then

          consider m be Nat such that

           A12: n = (st1 + m) by NAT_1: 10;

          reconsider m as Element of NAT by ORDINAL1:def 12;

          m < st2 by A11, A12, XREAL_1: 6;

          then

           A13: not ( Following (s2,m)) is stable by A8, Def5;

          ( Following (s1,st1)) = (( Following (s,st1)) | the carrier of S1) by A1, A2, A3, A4, A5, CIRCCMB2: 13;

          

          then ( Following (s2,m)) = (( Following (( Following (s,st1)),m)) | the carrier of S2) by A1, A2, A3, A4, A7, A9, CIRCCMB2: 18

          .= (( Following (s,n)) | the carrier of S2) by A12, FACIRC_1: 13;

          hence not ( Following (s,n)) is stable by A2, A3, A4, A13, CIRCCMB2: 17;

        end;

          suppose n < st1;

          then

           A14: not ( Following (s1,n)) is stable by A6, Def5;

          (( Following (s,n)) | the carrier of S1) = ( Following (s1,n)) by A1, A2, A3, A4, A5, CIRCCMB2: 13;

          hence not ( Following (s,n)) is stable by A2, A3, A4, A14, CIRCCMB2: 17;

        end;

      end;

      ( Following (s2,st2)) is stable by A8, Def5;

      then

       A15: ( Following (s,(st1 + st2))) is stable by A1, A2, A3, A4, A5, A7, A9, CIRCCMB2: 19;

      s is stabilizing by A1, A2, A3, A4, A5, A6, A7, A8, Th9;

      hence thesis by A15, A10, Def5;

    end;

    theorem :: CIRCCMB3:11

    for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) misses ( InnerVertices S2) & S = (S1 +* S2) holds for A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2 holds for A be non-empty Circuit of S st A1 tolerates A2 & A = (A1 +* A2) holds for s be State of A, s1 be State of A1 st s1 = (s | the carrier of S1) & s1 is stabilizing holds for s2 be State of A2 st s2 = (( Following (s,( stabilization-time s1))) | the carrier of S2) & s2 is stabilizing holds (( Result s) | the carrier of S1) = ( Result s1)

    proof

      let S1,S2,S be non void Circuit-like non empty ManySortedSign such that

       A1: ( InputVertices S1) misses ( InnerVertices S2) & S = (S1 +* S2);

      let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;

      let A be non-empty Circuit of S such that

       A2: A1 tolerates A2 & A = (A1 +* A2);

      let s be State of A, s1 be State of A1 such that

       A3: s1 = (s | the carrier of S1) and

       A4: s1 is stabilizing;

      let s2 be State of A2 such that

       A5: s2 = (( Following (s,( stabilization-time s1))) | the carrier of S2) & s2 is stabilizing;

      

       A6: ( stabilization-time s) = (( stabilization-time s1) + ( stabilization-time s2)) by A1, A2, A3, A4, A5, Th10;

      

      thus (( Result s) | the carrier of S1) = (( Following (s,( stabilization-time s))) | the carrier of S1) by A1, A2, A3, A4, A5, Th2, Th9

      .= ( Following (s1,( stabilization-time s))) by A1, A2, A3, CIRCCMB2: 13

      .= ( Result s1) by A4, A6, Th5, NAT_1: 11;

    end;

    begin

    theorem :: CIRCCMB3:12

    

     Th12: for x be set, X be non empty finite set holds for n be Element of NAT holds for p be FinSeqLen of n holds for g be Function of (n -tuples_on X), X holds for s be State of ( 1GateCircuit (p,g)) holds (s * p) is Element of (n -tuples_on X)

    proof

      let x be set, X be non empty finite set;

      let n be Element of NAT ;

      let p be FinSeqLen of n;

      let g be Function of (n -tuples_on X), X;

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

      set S = ( 1GateCircStr (p,g)), A = ( 1GateCircuit (p,g));

      

       A1: ( rng (s * p)) c= X

      proof

        let o be object;

        

         A2: ( rng s) c= X

        proof

          reconsider tc = the carrier of S as non empty set;

          let z be object;

          reconsider tS = the Sorts of A as non-empty ManySortedSet of tc;

          assume z in ( rng s);

          then

          consider a be object such that

           A3: a in ( dom s) and

           A4: z = (s . a) by FUNCT_1:def 3;

          reconsider a as Vertex of S by A3, CIRCUIT1: 3;

          ( dom s) = ( dom tS) by CARD_3: 9;

          then (s . a) in (the Sorts of A . a) by A3, CARD_3: 9;

          hence thesis by A4, CIRCCOMB: 54;

        end;

        assume o in ( rng (s * p));

        then o in ( rng s) by FUNCT_1: 14;

        hence thesis by A2;

      end;

      

       A5: ( rng p) c= ( dom s)

      proof

        let o be object;

        assume o in ( rng p);

        then o in (( rng p) \/ { [p, g]}) by XBOOLE_0:def 3;

        then o in the carrier of S by CIRCCOMB:def 6;

        hence thesis by CIRCUIT1: 3;

      end;

      then (s * p) is FinSequence by FINSEQ_1: 16;

      then

      reconsider sx = (s * p) as FinSequence of X by A1, FINSEQ_1:def 4;

      ( len sx) = ( len p) by A5, FINSEQ_2: 29

      .= n by CARD_1:def 7;

      hence thesis by FINSEQ_2: 92;

    end;

    theorem :: CIRCCMB3:13

    

     Th13: for x1,x2,x3,x4 be object holds ( rng <*x1, x2, x3, x4*>) = {x1, x2, x3, x4}

    proof

      let x1,x2,x3,x4 be object;

      for y be object holds y in {x1, x2, x3, x4} iff ex x be object st x in ( dom <*x1, x2, x3, x4*>) & y = ( <*x1, x2, x3, x4*> . x)

      proof

        let y be object;

        thus y in {x1, x2, x3, x4} implies ex x be object st x in ( dom <*x1, x2, x3, x4*>) & y = ( <*x1, x2, x3, x4*> . x)

        proof

          

           A1: ( dom <*x1, x2, x3, x4*>) = {1, 2, 3, 4} by FINSEQ_1: 89, FINSEQ_3: 2;

          assume

           A2: y in {x1, x2, x3, x4};

          per cases by A2, ENUMSET1:def 2;

            suppose

             A3: y = x1;

            take 1;

            thus 1 in ( dom <*x1, x2, x3, x4*>) by A1, ENUMSET1:def 2;

            thus thesis by A3, FINSEQ_4: 76;

          end;

            suppose

             A4: y = x2;

            take 2;

            thus 2 in ( dom <*x1, x2, x3, x4*>) by A1, ENUMSET1:def 2;

            thus thesis by A4, FINSEQ_4: 76;

          end;

            suppose

             A5: y = x3;

            take 3;

            thus 3 in ( dom <*x1, x2, x3, x4*>) by A1, ENUMSET1:def 2;

            thus thesis by A5, FINSEQ_4: 76;

          end;

            suppose

             A6: y = x4;

            take 4;

            thus 4 in ( dom <*x1, x2, x3, x4*>) by A1, ENUMSET1:def 2;

            thus thesis by A6, FINSEQ_4: 76;

          end;

        end;

        given x be object such that

         A7: x in ( dom <*x1, x2, x3, x4*>) and

         A8: y = ( <*x1, x2, x3, x4*> . x);

        x in ( Seg 4) by A7, FINSEQ_1: 89;

        then x = 1 or x = 2 or x = 3 or x = 4 by ENUMSET1:def 2, FINSEQ_3: 2;

        then ( <*x1, x2, x3, x4*> . x) = x1 or ( <*x1, x2, x3, x4*> . x) = x2 or ( <*x1, x2, x3, x4*> . x) = x3 or ( <*x1, x2, x3, x4*> . x) = x4 by FINSEQ_4: 76;

        hence thesis by A8, ENUMSET1:def 2;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    theorem :: CIRCCMB3:14

    

     Th14: for x1,x2,x3,x4,x5 be object holds ( rng <*x1, x2, x3, x4, x5*>) = {x1, x2, x3, x4, x5}

    proof

      let x1,x2,x3,x4,x5 be object;

      for y be object holds y in {x1, x2, x3, x4, x5} iff ex x be object st x in ( dom <*x1, x2, x3, x4, x5*>) & y = ( <*x1, x2, x3, x4, x5*> . x)

      proof

        let y be object;

        thus y in {x1, x2, x3, x4, x5} implies ex x be object st x in ( dom <*x1, x2, x3, x4, x5*>) & y = ( <*x1, x2, x3, x4, x5*> . x)

        proof

          

           A1: ( dom <*x1, x2, x3, x4, x5*>) = {1, 2, 3, 4, 5} by FINSEQ_1: 89, FINSEQ_3: 3;

          assume

           A2: y in {x1, x2, x3, x4, x5};

          per cases by A2, ENUMSET1:def 3;

            suppose

             A3: y = x1;

            take 1;

            thus 1 in ( dom <*x1, x2, x3, x4, x5*>) by A1, ENUMSET1:def 3;

            thus thesis by A3, FINSEQ_4: 78;

          end;

            suppose

             A4: y = x2;

            take 2;

            thus 2 in ( dom <*x1, x2, x3, x4, x5*>) by A1, ENUMSET1:def 3;

            thus thesis by A4, FINSEQ_4: 78;

          end;

            suppose

             A5: y = x3;

            take 3;

            thus 3 in ( dom <*x1, x2, x3, x4, x5*>) by A1, ENUMSET1:def 3;

            thus thesis by A5, FINSEQ_4: 78;

          end;

            suppose

             A6: y = x4;

            take 4;

            thus 4 in ( dom <*x1, x2, x3, x4, x5*>) by A1, ENUMSET1:def 3;

            thus thesis by A6, FINSEQ_4: 78;

          end;

            suppose

             A7: y = x5;

            take 5;

            thus 5 in ( dom <*x1, x2, x3, x4, x5*>) by A1, ENUMSET1:def 3;

            thus thesis by A7, FINSEQ_4: 78;

          end;

        end;

        given x be object such that

         A8: x in ( dom <*x1, x2, x3, x4, x5*>) and

         A9: y = ( <*x1, x2, x3, x4, x5*> . x);

        x in ( Seg 5) by A8, FINSEQ_1: 89;

        then x = 1 or x = 2 or x = 3 or x = 4 or x = 5 by ENUMSET1:def 3, FINSEQ_3: 3;

        then ( <*x1, x2, x3, x4, x5*> . x) = x1 or ( <*x1, x2, x3, x4, x5*> . x) = x2 or ( <*x1, x2, x3, x4, x5*> . x) = x3 or ( <*x1, x2, x3, x4, x5*> . x) = x4 or ( <*x1, x2, x3, x4, x5*> . x) = x5 by FINSEQ_4: 78;

        hence thesis by A9, ENUMSET1:def 3;

      end;

      hence thesis by FUNCT_1:def 3;

    end;

    definition

      let S be ManySortedSign;

      :: CIRCCMB3:def6

      attr S is one-gate means

      : Def6: ex X be non empty finite set, n be Element of NAT , p be FinSeqLen of n, f be Function of (n -tuples_on X), X st S = ( 1GateCircStr (p,f));

    end

    definition

      let S be non empty ManySortedSign;

      let A be MSAlgebra over S;

      :: CIRCCMB3:def7

      attr A is one-gate means

      : Def7: ex X be non empty finite set, n be Element of NAT , p be FinSeqLen of n, f be Function of (n -tuples_on X), X st S = ( 1GateCircStr (p,f)) & A = ( 1GateCircuit (p,f));

    end

    registration

      let p be FinSequence, x be set;

      cluster ( 1GateCircStr (p,x)) -> finite;

      coherence

      proof

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

        hence thesis;

      end;

    end

    registration

      cluster one-gate -> strict non void non empty unsplit gate`1=arity finite for ManySortedSign;

      coherence ;

    end

    registration

      cluster one-gate -> gate`2=den for non empty ManySortedSign;

      coherence ;

    end

    registration

      let X be non empty finite set, n be Element of NAT , p be FinSeqLen of n, f be Function of (n -tuples_on X), X;

      cluster ( 1GateCircStr (p,f)) -> one-gate;

      coherence ;

    end

    registration

      cluster one-gate for ManySortedSign;

      existence

      proof

        set X = the non empty finite set, n = the Element of NAT , p = the FinSeqLen of n, f = the Function of (n -tuples_on X), X;

        take ( 1GateCircStr (p,f));

        thus thesis;

      end;

    end

    registration

      let S be one-gate ManySortedSign;

      cluster one-gate -> strict non-empty for Circuit of S;

      coherence ;

    end

    registration

      let X be non empty finite set, n be Element of NAT , p be FinSeqLen of n, f be Function of (n -tuples_on X), X;

      cluster ( 1GateCircuit (p,f)) -> one-gate;

      coherence ;

    end

    registration

      let S be one-gate ManySortedSign;

      cluster one-gate non-empty for Circuit of S;

      existence

      proof

        consider X be non empty finite set, n be Element of NAT , p be FinSeqLen of n, f be Function of (n -tuples_on X), X such that

         A1: S = ( 1GateCircStr (p,f)) by Def6;

        reconsider A = ( 1GateCircuit (p,f)) as finite-yielding MSAlgebra over S by A1;

        take A;

        thus thesis by A1;

      end;

    end

    definition

      let S be one-gate ManySortedSign;

      :: CIRCCMB3:def8

      func Output S -> Vertex of S equals ( union the carrier' of S);

      coherence

      proof

        consider X be non empty finite set, n be Element of NAT , p be FinSeqLen of n, f be Function of (n -tuples_on X), X such that

         A1: S = ( 1GateCircStr (p,f)) by Def6;

         [p, f] in { [p, f]} by TARSKI:def 1;

        then

         A2: [p, f] in (( rng p) \/ { [p, f]}) by XBOOLE_0:def 3;

        the carrier' of S = { [p, f]} by A1, CIRCCOMB:def 6;

        then ( union the carrier' of S) = [p, f] by ZFMISC_1: 25;

        hence thesis by A1, A2, CIRCCOMB:def 6;

      end;

    end

    registration

      let S be one-gate ManySortedSign;

      cluster ( Output S) -> pair;

      coherence

      proof

        consider X be non empty finite set, n be Element of NAT , p be FinSeqLen of n, f be Function of (n -tuples_on X), X such that

         A1: S = ( 1GateCircStr (p,f)) by Def6;

        the carrier' of S = { [p, f]} by A1, CIRCCOMB:def 6;

        hence thesis by ZFMISC_1: 25;

      end;

    end

    theorem :: CIRCCMB3:15

    

     Th15: for S be one-gate ManySortedSign, p be FinSequence, x be set st S = ( 1GateCircStr (p,x)) holds ( Output S) = [p, x]

    proof

      let S be one-gate ManySortedSign, p be FinSequence, x be set;

      assume S = ( 1GateCircStr (p,x));

      

      hence ( Output S) = ( union { [p, x]}) by CIRCCOMB:def 6

      .= [p, x] by ZFMISC_1: 25;

    end;

    theorem :: CIRCCMB3:16

    

     Th16: for S be one-gate ManySortedSign holds ( InnerVertices S) = {( Output S)}

    proof

      let S be one-gate ManySortedSign;

      consider X be non empty finite set, n be Element of NAT , p be FinSeqLen of n, f be Function of (n -tuples_on X), X such that

       A1: S = ( 1GateCircStr (p,f)) by Def6;

      ( Output S) = [p, f] by A1, Th15;

      hence thesis by A1, CIRCCOMB: 42;

    end;

    theorem :: CIRCCMB3:17

    for S be one-gate ManySortedSign holds for A be one-gate Circuit of S holds for n be Element of NAT holds for X be finite non empty set holds for f be Function of (n -tuples_on X), X, p be FinSeqLen of n st A = ( 1GateCircuit (p,f)) holds S = ( 1GateCircStr (p,f))

    proof

      let S be one-gate ManySortedSign;

      let A be one-gate Circuit of S;

      let n be Element of NAT ;

      let X be finite non empty set;

      let f be Function of (n -tuples_on X), X, p be FinSeqLen of n such that

       A1: A = ( 1GateCircuit (p,f));

      consider X1 be non empty finite set, n1 be Element of NAT , p1 be FinSeqLen of n1, f1 be Function of (n1 -tuples_on X1), X1 such that

       A2: S = ( 1GateCircStr (p1,f1)) and

       A3: A = ( 1GateCircuit (p1,f1)) by Def7;

       { [p, f]} = the carrier' of ( 1GateCircStr (p,f)) by CIRCCOMB:def 6

      .= ( dom the Charact of ( 1GateCircuit (p1,f1))) by A1, A3, PARTFUN1:def 2

      .= the carrier' of ( 1GateCircStr (p1,f1)) by PARTFUN1:def 2

      .= { [p1, f1]} by CIRCCOMB:def 6;

      then

       A4: [p, f] = [p1, f1] by ZFMISC_1: 3;

      then p = p1 by XTUPLE_0: 1;

      hence thesis by A2, A4, XTUPLE_0: 1;

    end;

    theorem :: CIRCCMB3:18

    for n be Element of NAT holds for X be finite non empty set holds for f be Function of (n -tuples_on X), X, p be FinSeqLen of n holds for s be State of ( 1GateCircuit (p,f)) holds (( Following s) . ( Output ( 1GateCircStr (p,f)))) = (f . (s * p))

    proof

      let n be Element of NAT ;

      let X be finite non empty set;

      let f be Function of (n -tuples_on X), X, p be FinSeqLen of n;

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

      ( Output ( 1GateCircStr (p,f))) = [p, f] by Th15;

      hence thesis by CIRCCOMB: 56;

    end;

    theorem :: CIRCCMB3:19

    

     Th19: for S be one-gate ManySortedSign holds for A be one-gate Circuit of S holds for s be State of A holds ( Following s) is stable

    proof

      let S be one-gate ManySortedSign;

      let A be one-gate Circuit of S;

      let s be State of A;

      ex X be non empty finite set, n be Element of NAT , p be FinSeqLen of n, f be Function of (n -tuples_on X), X st S = ( 1GateCircStr (p,f)) & A = ( 1GateCircuit (p,f)) by Def7;

      hence thesis by CIRCCMB2: 2;

    end;

    registration

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

      cluster one-gate -> with_stabilization-limit for non-empty Circuit of S;

      coherence

      proof

        let A be non-empty Circuit of S;

        assume

         A1: A is one-gate;

        then ex X be non empty finite set, n be Element of NAT , p be FinSeqLen of n, f be Function of (n -tuples_on X), X st S = ( 1GateCircStr (p,f)) & A = ( 1GateCircuit (p,f));

        then

        reconsider S1 = S as one-gate ManySortedSign;

        reconsider A1 = A as one-gate Circuit of S1 by A1;

        take 1;

        let s be State of A;

        reconsider s1 = s as State of A1;

        ( Following s1) is stable by Th19;

        hence thesis by FACIRC_1: 14;

      end;

    end

    theorem :: CIRCCMB3:20

    

     Th20: for S be one-gate ManySortedSign holds for A be one-gate Circuit of S holds for s be State of A holds ( Result s) = ( Following s)

    proof

      let S be one-gate ManySortedSign;

      let A be one-gate Circuit of S;

      let s be State of A;

      

       A1: ( Following s) = ( Following (s,1)) by FACIRC_1: 14;

      s is stabilizing & ( Following s) is stable by Def2, Th19;

      hence thesis by A1, Def4;

    end;

    theorem :: CIRCCMB3:21

    

     Th21: for S be one-gate ManySortedSign holds for A be one-gate Circuit of S holds for s be State of A holds ( stabilization-time s) <= 1

    proof

      let S be one-gate ManySortedSign;

      let A be one-gate Circuit of S;

      let s be State of A;

      ( Following s) is stable by Th19;

      then

       A1: ( Following (s,1)) is stable by FACIRC_1: 14;

      s is stabilizing by Def2;

      hence thesis by A1, Def5;

    end;

    scheme :: CIRCCMB3:sch1

    OneGate1Ex { x() -> object , X() -> non empty finite set , f( object) -> Element of X() } :

ex S be one-gate ManySortedSign, A be one-gate Circuit of S st ( InputVertices S) = {x()} & for s be State of A holds (( Result s) . ( Output S)) = f(.);

      deffunc F( Element of (1 -tuples_on X())) = f(.);

      consider g be Function of (1 -tuples_on X()), X() such that

       A1: for a be Element of (1 -tuples_on X()) holds (g . a) = F(a) from FUNCT_2:sch 4;

      reconsider S = ( 1GateCircStr ( <*x()*>,g)) as one-gate ManySortedSign;

      take S;

      reconsider A = ( 1GateCircuit ( <*x()*>,g)) as one-gate Circuit of S;

      take A;

      ( rng <*x()*>) = {x()} by FINSEQ_1: 38;

      hence ( InputVertices S) = {x()} by CIRCCOMB: 42;

      let s be State of A;

      reconsider sx = (s * <*x()*>) as Element of (1 -tuples_on X()) by Th12;

      ( dom <*x()*>) = ( Seg 1) by FINSEQ_1: 38;

      then

       A2: 1 in ( dom <*x()*>) by FINSEQ_1: 1;

      

      thus (( Result s) . ( Output S)) = (( Following s) . ( Output S)) by Th20

      .= (( Following s) . [ <*x()*>, g]) by Th15

      .= (g . (s * <*x()*>)) by CIRCCOMB: 56

      .= f(.) by A1

      .= f(.) by A2, FUNCT_1: 13

      .= f(.) by FINSEQ_1:def 8;

    end;

    scheme :: CIRCCMB3:sch2

    OneGate2Ex { x1,x2() -> object , X() -> non empty finite set , f( object, object) -> Element of X() } :

ex S be one-gate ManySortedSign, A be one-gate Circuit of S st ( InputVertices S) = {x1(), x2()} & for s be State of A holds (( Result s) . ( Output S)) = f(.,.);

      deffunc F( Element of (2 -tuples_on X())) = f(.,.);

      consider g be Function of (2 -tuples_on X()), X() such that

       A1: for a be Element of (2 -tuples_on X()) holds (g . a) = F(a) from FUNCT_2:sch 4;

      reconsider S = ( 1GateCircStr ( <*x1(), x2()*>,g)) as one-gate ManySortedSign;

      take S;

      reconsider A = ( 1GateCircuit ( <*x1(), x2()*>,g)) as one-gate Circuit of S;

      take A;

      ( rng <*x1(), x2()*>) = {x1(), x2()} by FINSEQ_2: 127;

      hence ( InputVertices S) = {x1(), x2()} by CIRCCOMB: 42;

      let s be State of A;

      reconsider sx = (s * <*x1(), x2()*>) as Element of (2 -tuples_on X()) by Th12;

      

       A2: ( dom <*x1(), x2()*>) = ( Seg 2) by FINSEQ_1: 89;

      then

       A3: 1 in ( dom <*x1(), x2()*>) by FINSEQ_1: 1;

      

       A4: 2 in ( dom <*x1(), x2()*>) by A2, FINSEQ_1: 1;

      ( Result s) = ( Following s) by Th20;

      

      hence (( Result s) . ( Output S)) = (( Following s) . [ <*x1(), x2()*>, g]) by Th15

      .= (g . (s * <*x1(), x2()*>)) by CIRCCOMB: 56

      .= f(.,.) by A1

      .= f(.,.) by A3, FUNCT_1: 13

      .= f(.,.) by A4, FUNCT_1: 13

      .= f(.,.) by FINSEQ_1: 44

      .= f(.,.) by FINSEQ_1: 44;

    end;

    scheme :: CIRCCMB3:sch3

    OneGate3Ex { x1,x2,x3() -> object , X() -> non empty finite set , f( object, object, object) -> Element of X() } :

ex S be one-gate ManySortedSign, A be one-gate Circuit of S st ( InputVertices S) = {x1(), x2(), x3()} & for s be State of A holds (( Result s) . ( Output S)) = f(.,.,.);

      deffunc F( Element of (3 -tuples_on X())) = f(.,.,.);

      consider g be Function of (3 -tuples_on X()), X() such that

       A1: for a be Element of (3 -tuples_on X()) holds (g . a) = F(a) from FUNCT_2:sch 4;

      reconsider S = ( 1GateCircStr ( <*x1(), x2(), x3()*>,g)) as one-gate ManySortedSign;

      take S;

      reconsider A = ( 1GateCircuit ( <*x1(), x2(), x3()*>,g)) as one-gate Circuit of S;

      take A;

      ( rng <*x1(), x2(), x3()*>) = {x1(), x2(), x3()} by FINSEQ_2: 128;

      hence ( InputVertices S) = {x1(), x2(), x3()} by CIRCCOMB: 42;

      let s be State of A;

      reconsider sx = (s * <*x1(), x2(), x3()*>) as Element of (3 -tuples_on X()) by Th12;

      

       A2: ( dom <*x1(), x2(), x3()*>) = ( Seg 3) by FINSEQ_1: 89;

      then

       A3: 1 in ( dom <*x1(), x2(), x3()*>) by FINSEQ_1: 1;

      

       A4: 3 in ( dom <*x1(), x2(), x3()*>) by A2, FINSEQ_1: 1;

      

       A5: 2 in ( dom <*x1(), x2(), x3()*>) by A2, FINSEQ_1: 1;

      ( Result s) = ( Following s) by Th20;

      

      hence (( Result s) . ( Output S)) = (( Following s) . [ <*x1(), x2(), x3()*>, g]) by Th15

      .= (g . (s * <*x1(), x2(), x3()*>)) by CIRCCOMB: 56

      .= f(.,.,.) by A1

      .= f(.,.,.) by A3, FUNCT_1: 13

      .= f(.,.,.) by FINSEQ_1: 45

      .= f(.,.,.) by A5, FUNCT_1: 13

      .= f(.,.,.) by FINSEQ_1: 45

      .= f(.,.,.) by A4, FUNCT_1: 13

      .= f(.,.,.) by FINSEQ_1: 45;

    end;

    scheme :: CIRCCMB3:sch4

    OneGate4Ex { x1,x2,x3,x4() -> object , X() -> non empty finite set , f( object, object, object, object) -> Element of X() } :

ex S be one-gate ManySortedSign, A be one-gate Circuit of S st ( InputVertices S) = {x1(), x2(), x3(), x4()} & for s be State of A holds (( Result s) . ( Output S)) = f(.,.,.,.);

      deffunc F( Element of (4 -tuples_on X())) = f(.,.,.,.);

      consider g be Function of (4 -tuples_on X()), X() such that

       A1: for a be Element of (4 -tuples_on X()) holds (g . a) = F(a) from FUNCT_2:sch 4;

      reconsider S = ( 1GateCircStr ( <*x1(), x2(), x3(), x4()*>,g)) as one-gate ManySortedSign;

      take S;

      reconsider A = ( 1GateCircuit ( <*x1(), x2(), x3(), x4()*>,g)) as one-gate Circuit of S;

      take A;

      ( rng <*x1(), x2(), x3(), x4()*>) = {x1(), x2(), x3(), x4()} by Th13;

      hence ( InputVertices S) = {x1(), x2(), x3(), x4()} by CIRCCOMB: 42;

      let s be State of A;

      reconsider sx = (s * <*x1(), x2(), x3(), x4()*>) as Element of (4 -tuples_on X()) by Th12;

      

       A2: ( dom <*x1(), x2(), x3(), x4()*>) = ( Seg 4) by FINSEQ_1: 89;

      then

       A3: 1 in ( dom <*x1(), x2(), x3(), x4()*>) by FINSEQ_1: 1;

      

       A4: 3 in ( dom <*x1(), x2(), x3(), x4()*>) by A2, FINSEQ_1: 1;

      

       A5: 2 in ( dom <*x1(), x2(), x3(), x4()*>) by A2, FINSEQ_1: 1;

      

       A6: 4 in ( dom <*x1(), x2(), x3(), x4()*>) by A2, FINSEQ_1: 1;

      ( Result s) = ( Following s) by Th20;

      

      hence (( Result s) . ( Output S)) = (( Following s) . [ <*x1(), x2(), x3(), x4()*>, g]) by Th15

      .= (g . (s * <*x1(), x2(), x3(), x4()*>)) by CIRCCOMB: 56

      .= f(.,.,.,.) by A1

      .= f(.,.,.,.) by A3, FUNCT_1: 13

      .= f(.,.,.,.) by FINSEQ_4: 76

      .= f(.,.,.,.) by A5, FUNCT_1: 13

      .= f(.,.,.,.) by FINSEQ_4: 76

      .= f(.,.,.,.) by A4, FUNCT_1: 13

      .= f(.,.,.,.) by FINSEQ_4: 76

      .= f(.,.,.,.) by A6, FUNCT_1: 13

      .= f(.,.,.,.) by FINSEQ_4: 76;

    end;

    scheme :: CIRCCMB3:sch5

    OneGate5Ex { x1,x2,x3,x4,x5() -> object , X() -> non empty finite set , f( object, object, object, object, object) -> Element of X() } :

ex S be one-gate ManySortedSign, A be one-gate Circuit of S st ( InputVertices S) = {x1(), x2(), x3(), x4(), x5()} & for s be State of A holds (( Result s) . ( Output S)) = f(.,.,.,.,.);

      deffunc F( Element of (5 -tuples_on X())) = f(.,.,.,.,.);

      consider g be Function of (5 -tuples_on X()), X() such that

       A1: for a be Element of (5 -tuples_on X()) holds (g . a) = F(a) from FUNCT_2:sch 4;

      reconsider S = ( 1GateCircStr ( <*x1(), x2(), x3(), x4(), x5()*>,g)) as one-gate ManySortedSign;

      take S;

      reconsider A = ( 1GateCircuit ( <*x1(), x2(), x3(), x4(), x5()*>,g)) as one-gate Circuit of S;

      take A;

      ( rng <*x1(), x2(), x3(), x4(), x5()*>) = {x1(), x2(), x3(), x4(), x5()} by Th14;

      hence ( InputVertices S) = {x1(), x2(), x3(), x4(), x5()} by CIRCCOMB: 42;

      let s be State of A;

      reconsider sx = (s * <*x1(), x2(), x3(), x4(), x5()*>) as Element of (5 -tuples_on X()) by Th12;

      

       A2: ( dom <*x1(), x2(), x3(), x4(), x5()*>) = ( Seg 5) by FINSEQ_1: 89;

      then

       A3: 1 in ( dom <*x1(), x2(), x3(), x4(), x5()*>) by FINSEQ_1: 1;

      

       A4: 5 in ( dom <*x1(), x2(), x3(), x4(), x5()*>) by A2, FINSEQ_1: 1;

      

       A5: 4 in ( dom <*x1(), x2(), x3(), x4(), x5()*>) by A2, FINSEQ_1: 1;

      

       A6: 3 in ( dom <*x1(), x2(), x3(), x4(), x5()*>) by A2, FINSEQ_1: 1;

      

       A7: 2 in ( dom <*x1(), x2(), x3(), x4(), x5()*>) by A2, FINSEQ_1: 1;

      ( Result s) = ( Following s) by Th20;

      

      hence (( Result s) . ( Output S)) = (( Following s) . [ <*x1(), x2(), x3(), x4(), x5()*>, g]) by Th15

      .= (g . (s * <*x1(), x2(), x3(), x4(), x5()*>)) by CIRCCOMB: 56

      .= f(.,.,.,.,.) by A1

      .= f(.,.,.,.,.) by A3, FUNCT_1: 13

      .= f(.,.,.,.,.) by FINSEQ_4: 78

      .= f(.,.,.,.,.) by A7, FUNCT_1: 13

      .= f(.,.,.,.,.) by FINSEQ_4: 78

      .= f(.,.,.,.,.) by A6, FUNCT_1: 13

      .= f(.,.,.,.,.) by FINSEQ_4: 78

      .= f(.,.,.,.,.) by A5, FUNCT_1: 13

      .= f(.,.,.,.,.) by FINSEQ_4: 78

      .= f(.,.,.,.,.) by A4, FUNCT_1: 13

      .= f(.,.,.,.,.) by FINSEQ_4: 78;

    end;

    begin

    theorem :: CIRCCMB3:22

    

     Th22: for X,Y be non empty set, n,m be Element of NAT st n <> 0 & (n -tuples_on X) = (m -tuples_on Y) holds X = Y & n = m

    proof

      let X,Y be non empty set;

      let n,m be Element of NAT ;

      assume that

       A1: n <> 0 and

       A2: (n -tuples_on X) = (m -tuples_on Y);

      thus X = Y

      proof

        thus X c= Y

        proof

          let a be object;

          assume a in X;

          then (n |-> a) is Element of (n -tuples_on X) by FINSEQ_2: 112;

          then (n |-> a) in (m -tuples_on Y) by A2;

          then (n |-> a) in { s where s be Element of (Y * ) : ( len s) = m } by FINSEQ_2:def 4;

          then ex s be Element of (Y * ) st s = (n |-> a) & ( len s) = m;

          then

           A3: ( rng (n |-> a)) c= Y by FINSEQ_1:def 4;

          (n |-> a) = (( Seg n) --> a) by FINSEQ_2:def 2;

          then ( rng (n |-> a)) = {a} by A1, FUNCOP_1: 8;

          then a in ( rng (n |-> a)) by TARSKI:def 1;

          hence thesis by A3;

        end;

        let a be object;

        

         A4: (m |-> a) = (( Seg m) --> a) by FINSEQ_2:def 2;

        assume a in Y;

        then (m |-> a) is Element of (m -tuples_on Y) by FINSEQ_2: 112;

        then (m |-> a) in (n -tuples_on X) by A2;

        then (m |-> a) in { s where s be Element of (X * ) : ( len s) = n } by FINSEQ_2:def 4;

        then

         A5: ex s be Element of (X * ) st s = (m |-> a) & ( len s) = n;

        then m = n by CARD_1:def 7;

        then ( rng (m |-> a)) = {a} by A1, A4, FUNCOP_1: 8;

        then

         A6: a in ( rng (m |-> a)) by TARSKI:def 1;

        ( rng (m |-> a)) c= X by A5, FINSEQ_1:def 4;

        hence thesis by A6;

      end;

      thus thesis by A2, FINSEQ_2: 110;

    end;

    theorem :: CIRCCMB3:23

    for S1,S2 be non empty ManySortedSign holds for v be Vertex of S1 holds v is Vertex of (S1 +* S2)

    proof

      let S1,S2 be non empty ManySortedSign;

      let v be Vertex of S1;

      v in (the carrier of S1 \/ the carrier of S2) by XBOOLE_0:def 3;

      hence thesis by CIRCCOMB:def 2;

    end;

    theorem :: CIRCCMB3:24

    for S1,S2 be non empty ManySortedSign holds for v be Vertex of S2 holds v is Vertex of (S1 +* S2)

    proof

      let S1,S2 be non empty ManySortedSign;

      let v be Vertex of S2;

      v in (the carrier of S1 \/ the carrier of S2) by XBOOLE_0:def 3;

      hence thesis by CIRCCOMB:def 2;

    end;

    definition

      let X be non empty finite set;

      :: CIRCCMB3:def9

      mode Signature of X -> gate`2=den non void non empty unsplit gate`1=arity ManySortedSign means

      : Def9: ex A be Circuit of it st the Sorts of A is constant & ( the_value_of the Sorts of A) = X & A is gate`2=den;

      existence

      proof

        set p = the FinSeqLen of 1;

        set f = the Function of (1 -tuples_on X), X;

        take ( 1GateCircStr (p,f));

        set A = ( 1GateCircuit (p,f));

        

         A1: the Sorts of A = (the carrier of ( 1GateCircStr (p,f)) --> X) by CIRCCOMB:def 13;

        then ( the_value_of the Sorts of A) = X by FUNCOP_1: 79;

        hence thesis by A1;

      end;

    end

    theorem :: CIRCCMB3:25

    

     Th25: for n be Element of NAT , X be non empty finite set holds for f be Function of (n -tuples_on X), X holds for p be FinSeqLen of n holds ( 1GateCircStr (p,f)) is Signature of X

    proof

      let n be Element of NAT , X be non empty finite set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      take A = ( 1GateCircuit (p,f));

      the Sorts of A = (the carrier of ( 1GateCircStr (p,f)) --> X) by CIRCCOMB:def 13;

      hence thesis by FUNCOP_1: 79;

    end;

    registration

      let X be non empty finite set;

      cluster strict one-gate for Signature of X;

      existence

      proof

        set p = the FinSeqLen of 1;

        set f = the Function of (1 -tuples_on X), X;

        ( 1GateCircStr (p,f)) is Signature of X by Th25;

        hence thesis;

      end;

    end

    definition

      let n be Element of NAT ;

      let X be non empty finite set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      :: original: 1GateCircStr

      redefine

      func 1GateCircStr (p,f) -> strict Signature of X ;

      coherence by Th25;

    end

    definition

      let X be non empty finite set;

      let S be Signature of X;

      :: CIRCCMB3:def10

      mode Circuit of X,S -> Circuit of S means

      : Def10: it is gate`2=den & the Sorts of it is constant & ( the_value_of the Sorts of it ) = X;

      existence

      proof

        ex A be Circuit of S st the Sorts of A is constant & ( the_value_of the Sorts of A) = X & A is gate`2=den by Def9;

        hence thesis;

      end;

    end

    registration

      let X be non empty finite set;

      let S be Signature of X;

      cluster -> gate`2=den non-empty for Circuit of X, S;

      coherence

      proof

        let A be Circuit of X, S;

        thus A is gate`2=den by Def10;

        the Sorts of A is non empty constant & ( the_value_of the Sorts of A) = X by Def10;

        then ( dom the Sorts of A) = the carrier of S & for i be object st i in ( dom the Sorts of A) holds (the Sorts of A . i) is non empty by FUNCT_1:def 12, PARTFUN1:def 2;

        then the Sorts of A is non-empty by PBOOLE:def 13;

        hence thesis by MSUALG_1:def 3;

      end;

    end

    theorem :: CIRCCMB3:26

    

     Th26: for n be Element of NAT , X be non empty finite set holds for f be Function of (n -tuples_on X), X holds for p be FinSeqLen of n holds ( 1GateCircuit (p,f)) is Circuit of X, ( 1GateCircStr (p,f))

    proof

      let n be Element of NAT , X be non empty finite set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      set A = ( 1GateCircuit (p,f));

      thus A is gate`2=den;

      the Sorts of A = (the carrier of ( 1GateCircStr (p,f)) --> X) by CIRCCOMB:def 13;

      hence the Sorts of A is constant & ( the_value_of the Sorts of A) = X by FUNCOP_1: 79;

    end;

    registration

      let X be non empty finite set;

      let S be one-gate Signature of X;

      cluster strict one-gate for Circuit of X, S;

      existence

      proof

        consider A be Circuit of S such that

         A1: the Sorts of A is constant & ( the_value_of the Sorts of A) = X and

         A2: A is gate`2=den by Def9;

        set B = the MSAlgebra of A;

        the Sorts of A is finite-yielding by MSAFREE2:def 11;

        then

        reconsider B as Circuit of S by MSAFREE2:def 11;

        for g be set st g in the carrier' of S holds g = [(g `1 ), (the Charact of B . g)] by A2;

        then B is gate`2=den;

        then

        reconsider B as Circuit of X, S by A1, Def10;

        consider Y be non empty finite set, n be Element of NAT , p be FinSeqLen of n, f be Function of (n -tuples_on Y), Y such that

         A3: S = ( 1GateCircStr (p,f)) by Def6;

        take B;

        

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

        ( dom the Sorts of A) = the carrier of S by PARTFUN1:def 2;

        then

         A5: the Sorts of B = (the carrier of S --> X) by A1, FUNCOP_1: 80;

        set g = [p, f];

        set C = ( 1GateCircuit (p,f));

        g in {g} by TARSKI:def 1;

        then

         A6: g in the carrier' of S by A3, CIRCCOMB:def 6;

        then

         A7: g = [(g `1 ), (the Charact of C . g)] by A3, CIRCCOMB:def 10;

        (the Arity of S . g) in (the carrier of S * ) by A6, FUNCT_2: 5;

        then

        reconsider Ag = (the Arity of S . g) as FinSequence of the carrier of S by FINSEQ_1:def 11;

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

        then

         A8: ((the Sorts of B * the ResultSort of S) . g) = (the Sorts of B . (the ResultSort of S . g)) by A6, FUNCT_1: 13;

        (the ResultSort of S . g) in the carrier of S by A6, FUNCT_2: 5;

        then (the ResultSort of S . g) in ( dom the Sorts of B) by PARTFUN1:def 2;

        then

         A9: (the Sorts of B . (the ResultSort of S . g)) = X by A1, FUNCT_1:def 12;

        

         A10: g = [(g `1 ), (the Charact of B . g)] by A6, CIRCCOMB:def 10;

        then ( dom (the Charact of B . g)) = ( dom f) by XTUPLE_0: 1;

        then

         A11: ( dom (the Charact of B . g)) = (n -tuples_on Y) by FUNCT_2:def 1;

        (the Charact of B . g) is Function of (((the Sorts of B # ) * the Arity of S) . g), ((the Sorts of B * the ResultSort of S) . g) by A6, PBOOLE:def 15;

        then ( dom (the Charact of B . g)) = (((the Sorts of B # ) * the Arity of S) . g) by A6, FUNCT_2:def 1;

        

        then

         A12: ( dom (the Charact of B . g)) = ((the Sorts of B # ) . Ag) by A6, A4, FUNCT_1: 13

        .= (( len Ag) -tuples_on X) by A5, CIRCCOMB: 2;

        per cases ;

          suppose

           A13: n <> 0 ;

           A14:

          now

            let i be object;

            assume i in the carrier' of S;

            then i in {g} by A3, CIRCCOMB:def 6;

            then i = g by TARSKI:def 1;

            hence (the Charact of B . i) = (the Charact of C . i) by A10, A7, XTUPLE_0: 1;

          end;

          X = Y by A11, A12, A13, Th22;

          then the Sorts of B = the Sorts of ( 1GateCircuit (p,f)) by A3, A5, CIRCCOMB:def 13;

          hence thesis by A3, A14, PBOOLE: 3;

        end;

          suppose

           A15: n = 0 ;

          

          then (n -tuples_on X) = {( <*> X)} by FINSEQ_2: 94

          .= {( <*> Y)}

          .= (n -tuples_on Y) by A15, FINSEQ_2: 94;

          then

           A16: ( dom f) = (n -tuples_on X) by FUNCT_2:def 1;

          (the Charact of B . g) is Function of (((the Sorts of B # ) * the Arity of S) . g), ((the Sorts of B * the ResultSort of S) . g) by A6, PBOOLE:def 15;

          then

           A17: ( rng (the Charact of B . g)) c= ((the Sorts of B * the ResultSort of S) . g) by RELAT_1:def 19;

          (the Charact of B . g) = f by A10, XTUPLE_0: 1;

          then

          reconsider h = f as Function of (n -tuples_on X), X by A8, A9, A17, A16, FUNCT_2: 2;

          set D = ( 1GateCircuit (p,h));

          

           A18: g = [(g `1 ), (the Charact of D . g)] by A3, A6, CIRCCOMB:def 10;

           A19:

          now

            let i be object;

            assume i in the carrier' of S;

            then i in {g} by A3, CIRCCOMB:def 6;

            then i = g by TARSKI:def 1;

            hence (the Charact of B . i) = (the Charact of D . i) by A10, A18, XTUPLE_0: 1;

          end;

          the Sorts of B = the Sorts of D by A3, A5, CIRCCOMB:def 13;

          hence thesis by A3, A19, PBOOLE: 3;

        end;

      end;

    end

    registration

      let X be non empty finite set;

      let S be Signature of X;

      cluster strict for Circuit of X, S;

      existence

      proof

        consider A be Circuit of S such that

         A1: the Sorts of A is constant & ( the_value_of the Sorts of A) = X and

         A2: A is gate`2=den by Def9;

        set B = the MSAlgebra of A;

        the Sorts of A is finite-yielding by MSAFREE2:def 11;

        then

        reconsider B as Circuit of S by MSAFREE2:def 11;

        for g be set st g in the carrier' of S holds g = [(g `1 ), (the Charact of B . g)] by A2;

        then B is gate`2=den;

        then

        reconsider B as Circuit of X, S by A1, Def10;

        take B;

        thus thesis;

      end;

    end

    definition

      let n be Element of NAT ;

      let X be non empty finite set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      :: original: 1GateCircuit

      redefine

      func 1GateCircuit (p,f) -> strict Circuit of X, ( 1GateCircStr (p,f)) ;

      coherence by Th26;

    end

    theorem :: CIRCCMB3:27

    

     Th27: for X be non empty finite set holds for S1,S2 be Signature of X holds for A1 be Circuit of X, S1 holds for A2 be Circuit of X, S2 holds A1 tolerates A2

    proof

      let X be non empty finite set;

      let S1,S2 be Signature of X;

      let A1 be Circuit of X, S1;

      let A2 be Circuit of X, S2;

      thus S1 tolerates S2 by CIRCCOMB: 47;

      the Sorts of A2 is constant & ( the_value_of the Sorts of A2) = X by Def10;

      then

       A1: the Sorts of A2 = (( dom the Sorts of A2) --> X) by FUNCOP_1: 80;

      the Sorts of A1 is constant & ( the_value_of the Sorts of A1) = X by Def10;

      then the Sorts of A1 = (( dom the Sorts of A1) --> X) by FUNCOP_1: 80;

      hence the Sorts of A1 tolerates the Sorts of A2 by A1, FUNCOP_1: 87;

      thus thesis by CIRCCOMB: 48;

    end;

    theorem :: CIRCCMB3:28

    

     Th28: for X be non empty finite set holds for S1,S2 be Signature of X holds for A1 be Circuit of X, S1 holds for A2 be Circuit of X, S2 holds (A1 +* A2) is Circuit of (S1 +* S2)

    proof

      let X be non empty finite set;

      let S1,S2 be Signature of X;

      

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

      let A1 be Circuit of X, S1;

      let A2 be Circuit of X, S2;

      

       A2: ( dom the Sorts of A1) = the carrier of S1 & ( dom the Sorts of A2) = the carrier of S2 by PARTFUN1:def 2;

      

       A3: the Sorts of A1 is finite-yielding & the Sorts of A2 is finite-yielding by MSAFREE2:def 11;

      A1 tolerates A2 by Th27;

      then

       A4: the Sorts of A1 tolerates the Sorts of A2;

      then

       A5: the Sorts of (A1 +* A2) = (the Sorts of A1 +* the Sorts of A2) by CIRCCOMB:def 4;

      (A1 +* A2) is finite-yielding

      proof

        let i be object;

        assume i in the carrier of (S1 +* S2);

        then i in the carrier of S1 or i in the carrier of S2 by A1, XBOOLE_0:def 3;

        then i in the carrier of S1 & (the Sorts of (A1 +* A2) . i) = (the Sorts of A1 . i) or i in the carrier of S2 & (the Sorts of (A1 +* A2) . i) = (the Sorts of A2 . i) by A4, A5, A2, FUNCT_4: 13, FUNCT_4: 15;

        hence thesis by A3;

      end;

      hence thesis;

    end;

    theorem :: CIRCCMB3:29

    

     Th29: for X be non empty finite set holds for S1,S2 be Signature of X holds for A1 be Circuit of X, S1 holds for A2 be Circuit of X, S2 holds (A1 +* A2) is gate`2=den

    proof

      let X be non empty finite set;

      let S1,S2 be Signature of X;

      

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

      let A1 be Circuit of X, S1;

      let A2 be Circuit of X, S2;

      

       A2: ( dom the Charact of A1) = the carrier' of S1 & ( dom the Charact of A2) = the carrier' of S2 by PARTFUN1:def 2;

      

       A3: A1 tolerates A2 by Th27;

      then the Sorts of A1 tolerates the Sorts of A2;

      then

       A4: the Charact of (A1 +* A2) = (the Charact of A1 +* the Charact of A2) by CIRCCOMB:def 4;

      

       A5: the Charact of A1 tolerates the Charact of A2 by A3;

      (A1 +* A2) is gate`2=den

      proof

        let i be set;

        assume i in the carrier' of (S1 +* S2);

        then i in the carrier' of S1 or i in the carrier' of S2 by A1, XBOOLE_0:def 3;

        then i in the carrier' of S1 & (the Charact of (A1 +* A2) . i) = (the Charact of A1 . i) or i in the carrier' of S2 & (the Charact of (A1 +* A2) . i) = (the Charact of A2 . i) by A5, A4, A2, FUNCT_4: 13, FUNCT_4: 15;

        hence thesis by CIRCCOMB:def 10;

      end;

      hence thesis;

    end;

    theorem :: CIRCCMB3:30

    

     Th30: for X be non empty finite set holds for S1,S2 be Signature of X holds for A1 be Circuit of X, S1 holds for A2 be Circuit of X, S2 holds the Sorts of (A1 +* A2) is constant & ( the_value_of the Sorts of (A1 +* A2)) = X

    proof

      let X be non empty finite set;

      let S1,S2 be Signature of X;

      let A1 be Circuit of X, S1;

      let A2 be Circuit of X, S2;

      reconsider A = (A1 +* A2) as Circuit of (S1 +* S2) by Th28;

      

       A1: ( dom the Sorts of A1) = the carrier of S1 by PARTFUN1:def 2;

      the Sorts of A1 is constant & ( the_value_of the Sorts of A1) = X by Def10;

      then the Sorts of A1 = (( dom the Sorts of A1) --> X) by FUNCOP_1: 80;

      then

       A2: the Sorts of A1 = [:( dom the Sorts of A1), {X}:] by FUNCOP_1:def 2;

      the Sorts of A2 is constant & ( the_value_of the Sorts of A2) = X by Def10;

      then the Sorts of A2 = (( dom the Sorts of A2) --> X) by FUNCOP_1: 80;

      then

       A3: the Sorts of A2 = [:( dom the Sorts of A2), {X}:] by FUNCOP_1:def 2;

      A1 tolerates A2 by Th27;

      then

       A4: the Sorts of A1 tolerates the Sorts of A2;

      

      then the Sorts of A = (the Sorts of A1 +* the Sorts of A2) by CIRCCOMB:def 4

      .= (the Sorts of A1 \/ the Sorts of A2) by A4, FUNCT_4: 30

      .= [:(( dom the Sorts of A1) \/ ( dom the Sorts of A2)), {X}:] by A2, A3, ZFMISC_1: 97

      .= ((the carrier of S1 \/ ( dom the Sorts of A2)) --> X) by A1, FUNCOP_1:def 2;

      hence thesis by FUNCOP_1: 79;

    end;

    registration

      let S1,S2 be finite non empty ManySortedSign;

      cluster (S1 +* S2) -> finite;

      coherence

      proof

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

        hence thesis;

      end;

    end

    registration

      let X be non empty finite set;

      let S1,S2 be Signature of X;

      cluster (S1 +* S2) -> gate`2=den;

      coherence

      proof

        consider A2 be Circuit of S2 such that

         A1: the Sorts of A2 is constant & ( the_value_of the Sorts of A2) = X & A2 is gate`2=den by Def9;

        reconsider A2 as Circuit of X, S2 by A1, Def10;

        consider A1 be Circuit of S1 such that

         A2: the Sorts of A1 is constant & ( the_value_of the Sorts of A1) = X & A1 is gate`2=den by Def9;

        reconsider A1 as Circuit of X, S1 by A2, Def10;

        (A1 +* A2) is gate`2=den by Th29;

        hence thesis;

      end;

    end

    definition

      let X be non empty finite set;

      let S1,S2 be Signature of X;

      :: original: +*

      redefine

      func S1 +* S2 -> strict Signature of X ;

      coherence

      proof

        consider A2 be Circuit of S2 such that

         A1: the Sorts of A2 is constant & ( the_value_of the Sorts of A2) = X & A2 is gate`2=den by Def9;

        reconsider A2 as Circuit of X, S2 by A1, Def10;

        consider A1 be Circuit of S1 such that

         A2: the Sorts of A1 is constant & ( the_value_of the Sorts of A1) = X & A1 is gate`2=den by Def9;

        reconsider A1 as Circuit of X, S1 by A2, Def10;

        reconsider A = (A1 +* A2) as Circuit of (S1 +* S2) by Th28;

        (S1 +* S2) is Signature of X

        proof

          take A;

          thus the Sorts of A is constant & ( the_value_of the Sorts of A) = X by Th30;

          thus thesis by Th29;

        end;

        hence thesis;

      end;

    end

    definition

      let X be non empty finite set;

      let S1,S2 be Signature of X;

      let A1 be Circuit of X, S1;

      let A2 be Circuit of X, S2;

      :: original: +*

      redefine

      func A1 +* A2 -> strict Circuit of X, (S1 +* S2) ;

      coherence

      proof

        

         A1: the Sorts of (A1 +* A2) is constant & ( the_value_of the Sorts of (A1 +* A2)) = X by Th30;

        (A1 +* A2) is gate`2=den & (A1 +* A2) is Circuit of (S1 +* S2) by Th28, Th29;

        hence thesis by A1, Def10;

      end;

    end

    theorem :: CIRCCMB3:31

    

     Th31: for x,y be object holds ( the_rank_of x) in ( the_rank_of [x, y]) & ( the_rank_of y) in ( the_rank_of [x, y])

    proof

      let x,y be object;

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

      then

       A1: ( the_rank_of {x}) in ( the_rank_of { {x, y}, {x}}) by CLASSES1: 68;

      x in {x} by TARSKI:def 1;

      then ( the_rank_of x) in ( the_rank_of {x}) by CLASSES1: 68;

      hence ( the_rank_of x) in ( the_rank_of [x, y]) by A1, ORDINAL1: 10;

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

      then

       A2: ( the_rank_of {x, y}) in ( the_rank_of { {x, y}, {x}}) by CLASSES1: 68;

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

      then ( the_rank_of y) in ( the_rank_of {x, y}) by CLASSES1: 68;

      hence thesis by A2, ORDINAL1: 10;

    end;

    theorem :: CIRCCMB3:32

    

     Th32: for S be gate`2=den finite non void non empty unsplit gate`1=arity ManySortedSign holds for A be non-empty Circuit of S st A is gate`2=den holds A is with_stabilization-limit

    proof

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

      defpred P[ object, object] means $1 = $2 or $1 in the carrier' of S & $2 in ( proj2 ($1 `1 ));

      consider R be Relation such that

       A1: for a,b be object holds [a, b] in R iff a in the carrier of S & b in the carrier of S & P[a, b] from RELAT_1:sch 1;

      let A be non-empty Circuit of S such that

       A2: A is gate`2=den;

      

       A3: R is co-well_founded

      proof

        defpred P[ object, object] means ex x be set st x = $1 & $2 = ( the_rank_of x);

        let Y be set;

        assume that Y c= ( field R) and

         A4: Y <> {} ;

        set y = the Element of Y;

        

         A5: for x,y,z be object st P[x, y] & P[x, z] holds y = z;

        consider B be set such that

         A6: for x be object holds x in B iff ex y be object st y in Y & P[y, x] from TARSKI:sch 1( A5);

        ( the_rank_of y) in B by A4, A6;

        then ( inf B) in B by ORDINAL2: 17;

        then

        consider y be object such that

         A7: y in Y and

         A8: P[y, ( inf B)] by A6;

        reconsider y as set by TARSKI: 1;

        take y;

        thus y in Y by A7;

        let b be object;

        assume that

         A9: b in Y and

         A10: y <> b & [y, b] in R;

        ( the_rank_of b) in B by A6, A9;

        then

         A11: ( inf B) c= ( the_rank_of b) by ORDINAL2: 14;

        y in the carrier' of S by A1, A10;

        then y = [(y `1 ), (the Charact of A . y)] by A2;

        then

         A12: ( the_rank_of (y `1 )) in ( the_rank_of y) by Th31;

        b in ( proj2 (y `1 )) by A1, A10;

        then

        consider c be object such that

         A13: [c, b] in (y `1 ) by XTUPLE_0:def 13;

        

         A14: ( the_rank_of b) in ( the_rank_of [c, b]) by Th31;

        ( the_rank_of [c, b]) in ( the_rank_of (y `1 )) by A13, CLASSES1: 68;

        hence contradiction by A8, A14, A12, A11, ORDINAL1: 10;

      end;

      defpred A[ object, object] means ex n be Element of NAT st $2 = n & for s be State of A, m be Element of NAT st m >= n holds (( Following (s,m)) . $1) = (( Following (s,n)) . $1);

      defpred P[ object] means $1 in the carrier of S implies ex n be Element of NAT st for s be State of A, m be Element of NAT st m >= n holds (( Following (s,m)) . $1) = (( Following (s,n)) . $1);

      

       A15: ( rng R) c= the carrier of S

      proof

        let o be object;

        assume o in ( rng R);

        then ex q be object st [q, o] in R by XTUPLE_0:def 13;

        hence thesis by A1;

      end;

      

       A16: the carrier of S c= ( field R)

      proof

        let o be object;

        assume o in the carrier of S;

        then [o, o] in R by A1;

        hence thesis by RELAT_1: 15;

      end;

      ( dom R) c= the carrier of S

      proof

        let o be object;

        assume o in ( dom R);

        then ex q be object st [o, q] in R by XTUPLE_0:def 12;

        hence thesis by A1;

      end;

      then

       A17: (( dom R) \/ ( rng R)) c= (the carrier of S \/ the carrier of S) by A15, XBOOLE_1: 13;

      then

       A18: the carrier of S = ( field R) by A16, XBOOLE_0:def 10;

      

       A19: for a be object st for b be object st [a, b] in R & a <> b holds P[b] holds P[a]

      proof

        defpred P[ object, object] means ex n be Element of NAT st $2 = n & for s be State of A, m be Element of NAT st m >= n holds (( Following (s,m)) . $1) = (( Following (s,n)) . $1);

        let a be object;

        defpred S[ object] means a <> $1 & [a, $1] in R;

        consider RS be set such that

         A20: for b be object holds b in RS iff b in ( field R) & S[b] from XBOOLE_0:sch 1;

        

         A21: RS c= the carrier of S by A18, A20;

        assume

         A22: for b be object st [a, b] in R & a <> b holds P[b];

        

         A23: for b be object st b in RS holds ex z be object st P[b, z]

        proof

          let b be object;

          assume

           A24: b in RS;

          then a <> b & [a, b] in R by A20;

          then ex n be Element of NAT st for s be State of A, m be Element of NAT st m >= n holds (( Following (s,m)) . b) = (( Following (s,n)) . b) by A22, A21, A24;

          hence thesis;

        end;

        consider f be Function such that

         A25: ( dom f) = RS and

         A26: for x be object st x in RS holds P[x, (f . x)] from CLASSES1:sch 1( A23);

        assume

         A27: a in the carrier of S;

        per cases ;

          suppose

           A28: RS <> {} ;

          ( rng f) c= NAT

          proof

            let o be object;

            assume o in ( rng f);

            then

            consider l be object such that

             A29: l in ( dom f) and

             A30: o = (f . l) by FUNCT_1:def 3;

            ex n be Element of NAT st (f . l) = n & for s be State of A, m be Element of NAT st m >= n holds (( Following (s,m)) . l) = (( Following (s,n)) . l) by A25, A26, A29;

            hence thesis by A30;

          end;

          then

          reconsider C = ( rng f) as finite non empty Subset of NAT by A21, A25, A28, FINSET_1: 8, RELAT_1: 38, RELAT_1: 41;

          set b = the Element of RS;

          a <> b & [a, b] in R by A20, A28;

          then

          reconsider a1 = a as Gate of S by A1;

          reconsider mC = ( max C) as Element of NAT by ORDINAL1:def 12;

          take n = (mC + 1);

          let s be State of A;

          let m be Element of NAT ;

          assume m >= n;

          then

          consider k be Nat such that

           A31: m = (n + k) by NAT_1: 10;

          reconsider k as Element of NAT by ORDINAL1:def 12;

          

           A32: for x be set st x in ( rng ( the_arity_of a1)) holds ( Following (s,mC)) is_stable_at x

          proof

            let x be set;

            assume

             A33: x in ( rng ( the_arity_of a1));

            a1 = [(the Arity of S . a1), (a1 `2 )] by CIRCCOMB:def 8;

            then

             A34: a1 = [( the_arity_of a1), (a1 `2 )] by MSUALG_1:def 1;

            then ( the_rank_of x) in ( the_rank_of a1) by A33, CLASSES1: 82;

            then

             A35: x <> a;

            ( rng ( the_arity_of a1)) c= the carrier of S & x in ( proj2 (a `1 )) by A33, A34, FINSEQ_1:def 4;

            then

             A36: [a1, x] in R by A1, A27, A33;

            then x in ( field R) by RELAT_1: 15;

            then

             A37: x in RS by A20, A35, A36;

            then

            consider l be Element of NAT such that

             A38: (f . x) = l and

             A39: for s be State of A, m be Element of NAT st m >= l holds (( Following (s,m)) . x) = (( Following (s,l)) . x) by A26;

            l in ( rng f) by A25, A37, A38, FUNCT_1: 3;

            then

             A40: ( max C) >= l by XXREAL_2:def 8;

            now

              let k be Nat;

              

               A41: (mC + k) in NAT by ORDINAL1:def 12;

              

               A42: (mC + k) >= ( max C) by NAT_1: 11;

              

              thus (( Following (( Following (s,mC)),k)) . x) = (( Following (s,(mC + k))) . x) by FACIRC_1: 13

              .= (( Following (s,l)) . x) by A39, A40, A42, XXREAL_0: 2, A41

              .= (( Following (s,mC)) . x) by A39, A40;

            end;

            hence thesis;

          end;

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

          .= a by CIRCCOMB: 44;

          then ( Following ( Following (s,mC))) is_stable_at a by A32, FACIRC_1: 19;

          then ( Following (s,n)) is_stable_at a by FACIRC_1: 12;

          then (( Following (( Following (s,n)),k)) . a) = (( Following (s,n)) . a);

          hence thesis by A31, FACIRC_1: 13;

        end;

          suppose

           A43: RS = {} ;

          take n = 1;

          let s be State of A;

          let m be Element of NAT ;

          assume m >= n;

          then

          consider k be Nat such that

           A44: m = (n + k) by NAT_1: 10;

          reconsider k as Element of NAT by ORDINAL1:def 12;

           A45:

          now

            assume a in ( InnerVertices S);

            then a in ( rng ( id the carrier' of S)) by CIRCCOMB:def 7;

            then

            reconsider a1 = a as Gate of S;

            for x be set st x in ( rng ( the_arity_of a1)) holds s is_stable_at x

            proof

              let x be set;

              assume

               A46: x in ( rng ( the_arity_of a1));

              a1 = [(the Arity of S . a1), (a1 `2 )] by CIRCCOMB:def 8;

              then

               A47: a1 = [( the_arity_of a1), (a1 `2 )] by MSUALG_1:def 1;

              then ( the_rank_of x) in ( the_rank_of a1) by A46, CLASSES1: 82;

              then

               A48: x <> a;

              ( rng ( the_arity_of a1)) c= the carrier of S & x in ( proj2 (a `1 )) by A46, A47, FINSEQ_1:def 4;

              then

               A49: [a1, x] in R by A1, A27, A46;

              then x in ( field R) by RELAT_1: 15;

              hence thesis by A20, A43, A48, A49;

            end;

            then

             A50: ( Following s) is_stable_at ( the_result_sort_of a1) by FACIRC_1: 19;

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

            .= a1 by CIRCCOMB: 44;

            then ( Following (s,n)) is_stable_at a1 by A50, FACIRC_1: 14;

            then (( Following (( Following (s,n)),k)) . a) = (( Following (s,n)) . a);

            hence thesis by A44, FACIRC_1: 13;

          end;

           A51:

          now

            assume a in ( InputVertices S);

            then

             A52: s is_stable_at a by FACIRC_1: 18;

            

            hence (( Following (s,m)) . a) = (s . a)

            .= (( Following (s,n)) . a) by A52;

          end;

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

          hence thesis by A27, A51, A45, XBOOLE_0:def 3;

        end;

      end;

      

       A53: for a be object st a in ( field R) holds P[a] from REWRITE1:sch 2( A3, A19);

      

       A54: for a be object st a in ( field R) holds ex b be object st A[a, b]

      proof

        let a be object;

        assume a in ( field R);

        then ex n be Element of NAT st for s be State of A, m be Element of NAT st m >= n holds (( Following (s,m)) . a) = (( Following (s,n)) . a) by A17, A53;

        hence thesis;

      end;

      consider f be Function such that

       A55: ( dom f) = ( field R) and

       A56: for x be object st x in ( field R) holds A[x, (f . x)] from CLASSES1:sch 1( A54);

      ( rng f) c= NAT

      proof

        let o be object;

        assume o in ( rng f);

        then

        consider l be object such that

         A57: l in ( dom f) and

         A58: o = (f . l) by FUNCT_1:def 3;

        ex n be Element of NAT st (f . l) = n & for s be State of A, m be Element of NAT st m >= n holds (( Following (s,m)) . l) = (( Following (s,n)) . l) by A55, A56, A57;

        hence thesis by A58;

      end;

      then

      reconsider C = ( rng f) as finite non empty Subset of NAT by A18, A55, FINSET_1: 8, RELAT_1: 38, RELAT_1: 41;

      reconsider N = ( max C) as Element of NAT by ORDINAL1:def 12;

      take N;

      let s be State of A;

       A59:

      now

        let x be object;

        assume

         A60: x in the carrier of S;

        then

        consider n be Element of NAT such that

         A61: (f . x) = n and

         A62: for s be State of A, m be Element of NAT st m >= n holds (( Following (s,m)) . x) = (( Following (s,n)) . x) by A16, A56;

        n in C by A16, A55, A60, A61, FUNCT_1: 3;

        then

         A63: N >= n by XXREAL_2:def 8;

        then

         A64: (N + 1) >= n by NAT_1: 13;

        

        thus (( Following (s,N)) . x) = (( Following (s,n)) . x) by A62, A63

        .= (( Following (s,(N + 1))) . x) by A62, A64

        .= (( Following ( Following (s,N))) . x) by FACIRC_1: 12;

      end;

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

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

    end;

    registration

      let X be non empty finite set;

      let S be finite Signature of X;

      cluster -> with_stabilization-limit for Circuit of X, S;

      coherence by Th32;

    end

    scheme :: CIRCCMB3:sch6

    1AryDef { X() -> non empty set , F( object) -> Element of X() } :

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

      deffunc f( Element of (1 -tuples_on X())) = F(.);

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

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

      hereby

        take f;

        let x be Element of X();

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

        

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

        .= F(x) by FINSEQ_1: 40;

      end;

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

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

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

      now

        let a be Element of (1 -tuples_on X());

        consider x be Element of X() such that

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

        

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

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

      end;

      hence thesis by FUNCT_2: 63;

    end;

    scheme :: CIRCCMB3:sch7

    2AryDef { X() -> non empty set , F( object, object) -> Element of X() } :

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

      deffunc f( Element of (2 -tuples_on X())) = F(.,.);

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

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

      hereby

        take f;

        let x,y be Element of X();

        reconsider a = <*x, y*> as Element of (2 -tuples_on X()) 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 X()), X() such that

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

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

      now

        let a be Element of (2 -tuples_on X());

        consider x,y be Element of X() 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 :: CIRCCMB3:sch8

    3AryDef { X() -> non empty set , F( object, object, object) -> Element of X() } :

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

      deffunc f( Element of (3 -tuples_on X())) = F(.,.,.);

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

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

      hereby

        take f;

        let x,y,z be Element of X();

        reconsider a = <*x, y, z*> as Element of (3 -tuples_on X()) 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 X()), X() such that

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

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

      now

        let a be Element of (3 -tuples_on X());

        consider x,y,z be Element of X() 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;

    theorem :: CIRCCMB3:33

    

     Th33: for f be Function holds for x1,x2,x3,x4 be set st x1 in ( dom f) & x2 in ( dom f) & x3 in ( dom f) & x4 in ( dom f) holds (f * <*x1, x2, x3, x4*>) = <*(f . x1), (f . x2), (f . x3), (f . x4)*>

    proof

      let f be Function;

      let x1,x2,x3,x4 be set;

      assume that

       A1: x1 in ( dom f) and

       A2: x2 in ( dom f) & x3 in ( dom f) & x4 in ( dom f);

      reconsider D = ( dom f), E = ( rng f) as non empty set by A1, FUNCT_1: 3;

      ( rng <*x1, x2, x3, x4*>) c= D

      proof

        let a be object;

        assume a in ( rng <*x1, x2, x3, x4*>);

        then a in {x1, x2, x3, x4} by Th13;

        hence thesis by A1, A2, ENUMSET1:def 2;

      end;

      then

      reconsider p = <*x1, x2, x3, x4*> as FinSequence of D by FINSEQ_1:def 4;

      reconsider g = f as Function of D, E by FUNCT_2:def 1, RELSET_1: 4;

      

       A3: ( dom (g * p)) = ( dom p) by FINSEQ_3: 120;

       A4:

      now

        let k be Nat;

        assume

         A5: k in ( dom (g * p));

        then

         A6: k in ( Seg 4) by A3, FINSEQ_1: 89;

        per cases by A6, ENUMSET1:def 2, FINSEQ_3: 2;

          suppose

           A7: k = 1;

          then (p . k) = x1 by FINSEQ_4: 76;

          then ((g * p) . k) = (g . x1) by A5, FINSEQ_3: 120;

          hence ((g * p) . k) = ( <*(f . x1), (f . x2), (f . x3), (f . x4)*> . k) by A7, FINSEQ_4: 76;

        end;

          suppose

           A8: k = 2;

          then (p . k) = x2 by FINSEQ_4: 76;

          then ((g * p) . k) = (g . x2) by A5, FINSEQ_3: 120;

          hence ((g * p) . k) = ( <*(f . x1), (f . x2), (f . x3), (f . x4)*> . k) by A8, FINSEQ_4: 76;

        end;

          suppose

           A9: k = 3;

          then (p . k) = x3 by FINSEQ_4: 76;

          then ((g * p) . k) = (g . x3) by A5, FINSEQ_3: 120;

          hence ((g * p) . k) = ( <*(f . x1), (f . x2), (f . x3), (f . x4)*> . k) by A9, FINSEQ_4: 76;

        end;

          suppose

           A10: k = 4;

          then (p . k) = x4 by FINSEQ_4: 76;

          then ((g * p) . k) = (g . x4) by A5, FINSEQ_3: 120;

          hence ((g * p) . k) = ( <*(f . x1), (f . x2), (f . x3), (f . x4)*> . k) by A10, FINSEQ_4: 76;

        end;

      end;

      ( dom (g * p)) = ( Seg 4) by A3, FINSEQ_1: 89

      .= ( dom <*(f . x1), (f . x2), (f . x3), (f . x4)*>) by FINSEQ_1: 89;

      hence thesis by A4, FINSEQ_1: 13;

    end;

    theorem :: CIRCCMB3:34

    

     Th34: for f be Function holds for x1,x2,x3,x4,x5 be set st x1 in ( dom f) & x2 in ( dom f) & x3 in ( dom f) & x4 in ( dom f) & x5 in ( dom f) holds (f * <*x1, x2, x3, x4, x5*>) = <*(f . x1), (f . x2), (f . x3), (f . x4), (f . x5)*>

    proof

      let f be Function;

      let x1,x2,x3,x4,x5 be set;

      assume that

       A1: x1 in ( dom f) and

       A2: x2 in ( dom f) & x3 in ( dom f) & x4 in ( dom f) & x5 in ( dom f);

      reconsider D = ( dom f), E = ( rng f) as non empty set by A1, FUNCT_1: 3;

      ( rng <*x1, x2, x3, x4, x5*>) c= D

      proof

        let a be object;

        assume a in ( rng <*x1, x2, x3, x4, x5*>);

        then a in {x1, x2, x3, x4, x5} by Th14;

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

      end;

      then

      reconsider p = <*x1, x2, x3, x4, x5*> as FinSequence of D by FINSEQ_1:def 4;

      reconsider g = f as Function of D, E by FUNCT_2:def 1, RELSET_1: 4;

      

       A3: ( dom (g * p)) = ( dom p) by FINSEQ_3: 120;

       A4:

      now

        let k be Nat;

        assume

         A5: k in ( dom (g * p));

        then

         A6: k in ( Seg 5) by A3, FINSEQ_1: 89;

        per cases by A6, ENUMSET1:def 3, FINSEQ_3: 3;

          suppose

           A7: k = 1;

          then (p . k) = x1 by FINSEQ_4: 78;

          then ((g * p) . k) = (g . x1) by A5, FINSEQ_3: 120;

          hence ((g * p) . k) = ( <*(f . x1), (f . x2), (f . x3), (f . x4), (f . x5)*> . k) by A7, FINSEQ_4: 78;

        end;

          suppose

           A8: k = 2;

          then (p . k) = x2 by FINSEQ_4: 78;

          then ((g * p) . k) = (g . x2) by A5, FINSEQ_3: 120;

          hence ((g * p) . k) = ( <*(f . x1), (f . x2), (f . x3), (f . x4), (f . x5)*> . k) by A8, FINSEQ_4: 78;

        end;

          suppose

           A9: k = 3;

          then (p . k) = x3 by FINSEQ_4: 78;

          then ((g * p) . k) = (g . x3) by A5, FINSEQ_3: 120;

          hence ((g * p) . k) = ( <*(f . x1), (f . x2), (f . x3), (f . x4), (f . x5)*> . k) by A9, FINSEQ_4: 78;

        end;

          suppose

           A10: k = 4;

          then (p . k) = x4 by FINSEQ_4: 78;

          then ((g * p) . k) = (g . x4) by A5, FINSEQ_3: 120;

          hence ((g * p) . k) = ( <*(f . x1), (f . x2), (f . x3), (f . x4), (f . x5)*> . k) by A10, FINSEQ_4: 78;

        end;

          suppose

           A11: k = 5;

          then (p . k) = x5 by FINSEQ_4: 78;

          then ((g * p) . k) = (g . x5) by A5, FINSEQ_3: 120;

          hence ((g * p) . k) = ( <*(f . x1), (f . x2), (f . x3), (f . x4), (f . x5)*> . k) by A11, FINSEQ_4: 78;

        end;

      end;

      ( dom (g * p)) = ( Seg 5) by A3, FINSEQ_1: 89

      .= ( dom <*(f . x1), (f . x2), (f . x3), (f . x4), (f . x5)*>) by FINSEQ_1: 89;

      hence thesis by A4, FINSEQ_1: 13;

    end;

    scheme :: CIRCCMB3:sch9

    OneGate1Result { x1() -> object , B() -> non empty finite set , F( object) -> Element of B() , f() -> Function of (1 -tuples_on B()), B() } :

for s be State of ( 1GateCircuit ( <*x1()*>,f())) holds for a1 be Element of B() st a1 = (s . x1()) holds (( Result s) . ( Output ( 1GateCircStr ( <*x1()*>,f())))) = F(a1)

      provided

       A1: for g be Function of (1 -tuples_on B()), B() holds g = f() iff for a1 be Element of B() holds (g . <*a1*>) = F(a1);

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

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

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

      .= (( rng <*x1()*>) \/ { [ <*x1()*>, f()]}) by CIRCCOMB:def 6

      .= ( {x1()} \/ { [ <*x1()*>, f()]}) by FINSEQ_1: 38

      .= {x1(), [ <*x1()*>, f()]} by ENUMSET1: 1;

      then

       A2: x1() in ( dom s) by TARSKI:def 2;

      let a1 be Element of B();

      assume a1 = (s . x1());

      then

       A3: (s * <*x1()*>) = <*a1*> by A2, FINSEQ_2: 34;

      

      thus (( Result s) . ( Output S)) = (( Following s) . ( Output S)) by Th20

      .= (( Following s) . [ <*x1()*>, f()]) by Th15

      .= (f() . (s * <*x1()*>)) by CIRCCOMB: 56

      .= F(a1) by A1, A3;

    end;

    scheme :: CIRCCMB3:sch10

    OneGate2Result { x1,x2() -> object , B() -> non empty finite set , F( object, object) -> Element of B() , f() -> Function of (2 -tuples_on B()), B() } :

for s be State of ( 1GateCircuit ( <*x1(), x2()*>,f())) holds for a1,a2 be Element of B() st a1 = (s . x1()) & a2 = (s . x2()) holds (( Result s) . ( Output ( 1GateCircStr ( <*x1(), x2()*>,f())))) = F(a1,a2)

      provided

       A1: for g be Function of (2 -tuples_on B()), B() holds g = f() iff for a1,a2 be Element of B() holds (g . <*a1, a2*>) = F(a1,a2);

      set S = ( 1GateCircStr ( <*x1(), x2()*>,f()));

      let s be State of ( 1GateCircuit ( <*x1(), x2()*>,f()));

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

      .= (( rng <*x1(), x2()*>) \/ { [ <*x1(), x2()*>, f()]}) by CIRCCOMB:def 6

      .= ( {x1(), x2()} \/ { [ <*x1(), x2()*>, f()]}) by FINSEQ_2: 127

      .= {x1(), x2(), [ <*x1(), x2()*>, f()]} by ENUMSET1: 3;

      then

       A2: x1() in ( dom s) & x2() in ( dom s) by ENUMSET1:def 1;

      let a1,a2 be Element of B();

      assume a1 = (s . x1()) & a2 = (s . x2());

      then

       A3: (s * <*x1(), x2()*>) = <*a1, a2*> by A2, FINSEQ_2: 125;

      

      thus (( Result s) . ( Output S)) = (( Following s) . ( Output S)) by Th20

      .= (( Following s) . [ <*x1(), x2()*>, f()]) by Th15

      .= (f() . (s * <*x1(), x2()*>)) by CIRCCOMB: 56

      .= F(a1,a2) by A1, A3;

    end;

    scheme :: CIRCCMB3:sch11

    OneGate3Result { x1,x2,x3() -> object , B() -> non empty finite set , F( object, object, object) -> Element of B() , f() -> Function of (3 -tuples_on B()), B() } :

for s be State of ( 1GateCircuit ( <*x1(), x2(), x3()*>,f())) holds for a1,a2,a3 be Element of B() st a1 = (s . x1()) & a2 = (s . x2()) & a3 = (s . x3()) holds (( Result s) . ( Output ( 1GateCircStr ( <*x1(), x2(), x3()*>,f())))) = F(a1,a2,a3)

      provided

       A1: for g be Function of (3 -tuples_on B()), B() holds g = f() iff for a1,a2,a3 be Element of B() holds (g . <*a1, a2, a3*>) = F(a1,a2,a3);

      set S = ( 1GateCircStr ( <*x1(), x2(), x3()*>,f()));

      let s be State of ( 1GateCircuit ( <*x1(), x2(), x3()*>,f()));

      

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

      .= (( rng <*x1(), x2(), x3()*>) \/ { [ <*x1(), x2(), x3()*>, f()]}) by CIRCCOMB:def 6

      .= ( {x1(), x2(), x3()} \/ { [ <*x1(), x2(), x3()*>, f()]}) by FINSEQ_2: 128

      .= {x1(), x2(), x3(), [ <*x1(), x2(), x3()*>, f()]} by ENUMSET1: 6;

      then

       A3: x1() in ( dom s) & x2() in ( dom s) by ENUMSET1:def 2;

      

       A4: x3() in ( dom s) by A2, ENUMSET1:def 2;

      let a1,a2,a3 be Element of B();

      assume a1 = (s . x1()) & a2 = (s . x2()) & a3 = (s . x3());

      then

       A5: (s * <*x1(), x2(), x3()*>) = <*a1, a2, a3*> by A3, A4, FINSEQ_2: 126;

      

      thus (( Result s) . ( Output S)) = (( Following s) . ( Output S)) by Th20

      .= (( Following s) . [ <*x1(), x2(), x3()*>, f()]) by Th15

      .= (f() . (s * <*x1(), x2(), x3()*>)) by CIRCCOMB: 56

      .= F(a1,a2,a3) by A1, A5;

    end;

    scheme :: CIRCCMB3:sch12

    OneGate4Result { x1,x2,x3,x4() -> object , B() -> non empty finite set , F( object, object, object, object) -> Element of B() , f() -> Function of (4 -tuples_on B()), B() } :

for s be State of ( 1GateCircuit ( <*x1(), x2(), x3(), x4()*>,f())) holds for a1,a2,a3,a4 be Element of B() st a1 = (s . x1()) & a2 = (s . x2()) & a3 = (s . x3()) & a4 = (s . x4()) holds (( Result s) . ( Output ( 1GateCircStr ( <*x1(), x2(), x3(), x4()*>,f())))) = F(a1,a2,a3,a4)

      provided

       A1: for g be Function of (4 -tuples_on B()), B() holds g = f() iff for a1,a2,a3,a4 be Element of B() holds (g . <*a1, a2, a3, a4*>) = F(a1,a2,a3,a4);

      set S = ( 1GateCircStr ( <*x1(), x2(), x3(), x4()*>,f()));

      let s be State of ( 1GateCircuit ( <*x1(), x2(), x3(), x4()*>,f()));

      

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

      .= (( rng <*x1(), x2(), x3(), x4()*>) \/ { [ <*x1(), x2(), x3(), x4()*>, f()]}) by CIRCCOMB:def 6

      .= ( {x1(), x2(), x3(), x4()} \/ { [ <*x1(), x2(), x3(), x4()*>, f()]}) by Th13

      .= { [ <*x1(), x2(), x3(), x4()*>, f()], x1(), x2(), x3(), x4()} by ENUMSET1: 7;

      then

       A3: x1() in ( dom s) & x2() in ( dom s) by ENUMSET1:def 3;

      

       A4: x3() in ( dom s) & x4() in ( dom s) by A2, ENUMSET1:def 3;

      let a1,a2,a3,a4 be Element of B();

      assume a1 = (s . x1()) & a2 = (s . x2()) & a3 = (s . x3()) & a4 = (s . x4());

      then

       A5: (s * <*x1(), x2(), x3(), x4()*>) = <*a1, a2, a3, a4*> by A3, A4, Th33;

      

      thus (( Result s) . ( Output S)) = (( Following s) . ( Output S)) by Th20

      .= (( Following s) . [ <*x1(), x2(), x3(), x4()*>, f()]) by Th15

      .= (f() . (s * <*x1(), x2(), x3(), x4()*>)) by CIRCCOMB: 56

      .= F(a1,a2,a3,a4) by A1, A5;

    end;

    scheme :: CIRCCMB3:sch13

    OneGate5Result { x1,x2,x3,x4,x5() -> object , B() -> non empty finite set , F( object, object, object, object, object) -> Element of B() , f() -> Function of (5 -tuples_on B()), B() } :

for s be State of ( 1GateCircuit ( <*x1(), x2(), x3(), x4(), x5()*>,f())) holds for a1,a2,a3,a4,a5 be Element of B() st a1 = (s . x1()) & a2 = (s . x2()) & a3 = (s . x3()) & a4 = (s . x4()) & a5 = (s . x5()) holds (( Result s) . ( Output ( 1GateCircStr ( <*x1(), x2(), x3(), x4(), x5()*>,f())))) = F(a1,a2,a3,a4,a5)

      provided

       A1: for g be Function of (5 -tuples_on B()), B() holds g = f() iff for a1,a2,a3,a4,a5 be Element of B() holds (g . <*a1, a2, a3, a4, a5*>) = F(a1,a2,a3,a4,a5);

      set S = ( 1GateCircStr ( <*x1(), x2(), x3(), x4(), x5()*>,f()));

      let s be State of ( 1GateCircuit ( <*x1(), x2(), x3(), x4(), x5()*>,f()));

      

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

      .= (( rng <*x1(), x2(), x3(), x4(), x5()*>) \/ { [ <*x1(), x2(), x3(), x4(), x5()*>, f()]}) by CIRCCOMB:def 6

      .= ( {x1(), x2(), x3(), x4(), x5()} \/ { [ <*x1(), x2(), x3(), x4(), x5()*>, f()]}) by Th14

      .= {x1(), x2(), x3(), x4(), x5(), [ <*x1(), x2(), x3(), x4(), x5()*>, f()]} by ENUMSET1: 15;

      then

       A3: x1() in ( dom s) & x2() in ( dom s) by ENUMSET1:def 4;

      

       A4: x5() in ( dom s) by A2, ENUMSET1:def 4;

      

       A5: x3() in ( dom s) & x4() in ( dom s) by A2, ENUMSET1:def 4;

      let a1,a2,a3,a4,a5 be Element of B();

      assume a1 = (s . x1()) & a2 = (s . x2()) & a3 = (s . x3()) & a4 = (s . x4()) & a5 = (s . x5());

      then

       A6: (s * <*x1(), x2(), x3(), x4(), x5()*>) = <*a1, a2, a3, a4, a5*> by A3, A5, A4, Th34;

      

      thus (( Result s) . ( Output S)) = (( Following s) . ( Output S)) by Th20

      .= (( Following s) . [ <*x1(), x2(), x3(), x4(), x5()*>, f()]) by Th15

      .= (f() . (s * <*x1(), x2(), x3(), x4(), x5()*>)) by CIRCCOMB: 56

      .= F(a1,a2,a3,a4,a5) by A1, A6;

    end;

    begin

    theorem :: CIRCCMB3:35

    

     Th35: for n be Element of NAT , X be non empty finite set holds for f be Function of (n -tuples_on X), X holds for p be FinSeqLen of n holds for S be Signature of X st ( rng p) c= the carrier of S & not ( Output ( 1GateCircStr (p,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr (p,f)))) = ( InputVertices S)

    proof

      let n be Element of NAT , X be non empty finite set;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      let S be Signature of X such that

       A1: ( rng p) c= the carrier of S and

       A2: not ( Output ( 1GateCircStr (p,f))) in ( InputVertices S);

      

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

      

      thus ( InputVertices (S +* ( 1GateCircStr (p,f)))) = ((( InputVertices S) \ ( InnerVertices ( 1GateCircStr (p,f)))) \/ (( InputVertices ( 1GateCircStr (p,f))) \ ( InnerVertices S))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((( InputVertices S) \ ( InnerVertices ( 1GateCircStr (p,f)))) \/ (( rng p) \ ( InnerVertices S))) by CIRCCOMB: 42

      .= ((( InputVertices S) \ {( Output ( 1GateCircStr (p,f)))}) \/ (( rng p) \ ( InnerVertices S))) by Th16

      .= (( InputVertices S) \/ (( rng p) \ ( InnerVertices S))) by A2, ZFMISC_1: 57

      .= ( InputVertices S) by A1, A3, XBOOLE_1: 12, XBOOLE_1: 43;

    end;

    theorem :: CIRCCMB3:36

    

     Th36: for X1,X2 be set, X be non empty finite set, n be Element of NAT holds for f be Function of (n -tuples_on X), X holds for p be FinSeqLen of n holds for S be Signature of X st ( rng p) = (X1 \/ X2) & X1 c= the carrier of S & X2 misses ( InnerVertices S) & not ( Output ( 1GateCircStr (p,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr (p,f)))) = (( InputVertices S) \/ X2)

    proof

      let x1,x2 be set, X be non empty finite set, n be Element of NAT ;

      let f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n;

      let S be Signature of X such that

       A1: ( rng p) = (x1 \/ x2) and

       A2: x1 c= the carrier of S and

       A3: x2 misses ( InnerVertices S) and

       A4: not ( Output ( 1GateCircStr (p,f))) in ( InputVertices S);

      

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

      

      thus ( InputVertices (S +* ( 1GateCircStr (p,f)))) = ((( InputVertices S) \ ( InnerVertices ( 1GateCircStr (p,f)))) \/ (( InputVertices ( 1GateCircStr (p,f))) \ ( InnerVertices S))) by CIRCCMB2: 5, CIRCCOMB: 47

      .= ((( InputVertices S) \ ( InnerVertices ( 1GateCircStr (p,f)))) \/ (( rng p) \ ( InnerVertices S))) by CIRCCOMB: 42

      .= ((( InputVertices S) \ ( InnerVertices ( 1GateCircStr (p,f)))) \/ ((x1 \ ( InnerVertices S)) \/ x2)) by A1, A3, XBOOLE_1: 87

      .= (((( InputVertices S) \ ( InnerVertices ( 1GateCircStr (p,f)))) \/ (x1 \ ( InnerVertices S))) \/ x2) by XBOOLE_1: 4

      .= (((( InputVertices S) \ {( Output ( 1GateCircStr (p,f)))}) \/ (x1 \ ( InnerVertices S))) \/ x2) by Th16

      .= ((( InputVertices S) \/ (x1 \ ( InnerVertices S))) \/ x2) by A4, ZFMISC_1: 57

      .= (( InputVertices S) \/ x2) by A2, A5, XBOOLE_1: 12, XBOOLE_1: 43;

    end;

    theorem :: CIRCCMB3:37

    

     Th37: for x1 be set, X be non empty finite set holds for f be Function of (1 -tuples_on X), X holds for S be Signature of X st x1 in the carrier of S & not ( Output ( 1GateCircStr ( <*x1*>,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr ( <*x1*>,f)))) = ( InputVertices S)

    proof

      let x1 be set, X be non empty finite set;

      set p = <*x1*>;

      let f be Function of (1 -tuples_on X), X;

      let S be Signature of X;

      assume x1 in the carrier of S;

      then {x1} c= the carrier of S by ZFMISC_1: 31;

      then ( rng p) c= the carrier of S by FINSEQ_1: 38;

      hence thesis by Th35;

    end;

    theorem :: CIRCCMB3:38

    

     Th38: for x1,x2 be set, X be non empty finite set holds for f be Function of (2 -tuples_on X), X holds for S be Signature of X st x1 in the carrier of S & not x2 in ( InnerVertices S) & not ( Output ( 1GateCircStr ( <*x1, x2*>,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2*>,f)))) = (( InputVertices S) \/ {x2})

    proof

      let x1,x2 be set, X be non empty finite set;

      set p = <*x1, x2*>;

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

      let S be Signature of X such that

       A1: x1 in the carrier of S and

       A2: not x2 in ( InnerVertices S);

      

       A3: ( rng p) = {x1, x2} by FINSEQ_2: 127

      .= ( {x1} \/ {x2}) by ENUMSET1: 1;

       {x1} c= the carrier of S by A1, ZFMISC_1: 31;

      hence thesis by A2, A3, Th36, ZFMISC_1: 50;

    end;

    theorem :: CIRCCMB3:39

    

     Th39: for x1,x2 be set, X be non empty finite set holds for f be Function of (2 -tuples_on X), X holds for S be Signature of X st x2 in the carrier of S & not x1 in ( InnerVertices S) & not ( Output ( 1GateCircStr ( <*x1, x2*>,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2*>,f)))) = (( InputVertices S) \/ {x1})

    proof

      let x1,x2 be set, X be non empty finite set;

      set p = <*x1, x2*>;

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

      let S be Signature of X such that

       A1: x2 in the carrier of S and

       A2: not x1 in ( InnerVertices S);

      

       A3: ( rng p) = {x1, x2} by FINSEQ_2: 127

      .= ( {x1} \/ {x2}) by ENUMSET1: 1;

       {x2} c= the carrier of S by A1, ZFMISC_1: 31;

      hence thesis by A2, A3, Th36, ZFMISC_1: 50;

    end;

    theorem :: CIRCCMB3:40

    

     Th40: for x1,x2 be set, X be non empty finite set holds for f be Function of (2 -tuples_on X), X holds for S be Signature of X st x1 in the carrier of S & x2 in the carrier of S & not ( Output ( 1GateCircStr ( <*x1, x2*>,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2*>,f)))) = ( InputVertices S)

    proof

      let x1,x2 be set, X be non empty finite set;

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

      

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

      let S be Signature of X;

      assume x1 in the carrier of S & x2 in the carrier of S;

      then ( rng <*x1, x2*>) c= the carrier of S by A1, ZFMISC_1: 32;

      hence thesis by Th35;

    end;

    theorem :: CIRCCMB3:41

    

     Th41: for x1,x2,x3 be set, X be non empty finite set holds for f be Function of (3 -tuples_on X), X holds for S be Signature of X st x1 in the carrier of S & not x2 in ( InnerVertices S) & not x3 in ( InnerVertices S) & not ( Output ( 1GateCircStr ( <*x1, x2, x3*>,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = (( InputVertices S) \/ {x2, x3})

    proof

      let x1,x2,x3 be set, X be non empty finite set;

      set p = <*x1, x2, x3*>;

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

      let S be Signature of X such that

       A1: x1 in the carrier of S and

       A2: ( not x2 in ( InnerVertices S)) & not x3 in ( InnerVertices S);

      

       A3: ( rng p) = {x1, x2, x3} by FINSEQ_2: 128

      .= ( {x1} \/ {x2, x3}) by ENUMSET1: 2;

       {x1} c= the carrier of S by A1, ZFMISC_1: 31;

      hence thesis by A2, A3, Th36, ZFMISC_1: 51;

    end;

    theorem :: CIRCCMB3:42

    

     Th42: for x1,x2,x3 be set, X be non empty finite set holds for f be Function of (3 -tuples_on X), X holds for S be Signature of X st x2 in the carrier of S & not x1 in ( InnerVertices S) & not x3 in ( InnerVertices S) & not ( Output ( 1GateCircStr ( <*x1, x2, x3*>,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = (( InputVertices S) \/ {x1, x3})

    proof

      let x1,x2,x3 be set, X be non empty finite set;

      set p = <*x1, x2, x3*>;

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

      let S be Signature of X such that

       A1: x2 in the carrier of S and

       A2: ( not x1 in ( InnerVertices S)) & not x3 in ( InnerVertices S);

      

       A3: ( rng p) = {x1, x2, x3} by FINSEQ_2: 128

      .= {x2, x1, x3} by ENUMSET1: 58

      .= ( {x2} \/ {x1, x3}) by ENUMSET1: 2;

       {x2} c= the carrier of S by A1, ZFMISC_1: 31;

      hence thesis by A2, A3, Th36, ZFMISC_1: 51;

    end;

    theorem :: CIRCCMB3:43

    

     Th43: for x1,x2,x3 be set, X be non empty finite set holds for f be Function of (3 -tuples_on X), X holds for S be Signature of X st x3 in the carrier of S & not x1 in ( InnerVertices S) & not x2 in ( InnerVertices S) & not ( Output ( 1GateCircStr ( <*x1, x2, x3*>,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = (( InputVertices S) \/ {x1, x2})

    proof

      let x1,x2,x3 be set, X be non empty finite set;

      set p = <*x1, x2, x3*>;

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

      let S be Signature of X such that

       A1: x3 in the carrier of S and

       A2: ( not x1 in ( InnerVertices S)) & not x2 in ( InnerVertices S);

      

       A3: ( rng p) = {x1, x2, x3} by FINSEQ_2: 128

      .= ( {x1, x2} \/ {x3}) by ENUMSET1: 3;

       {x3} c= the carrier of S by A1, ZFMISC_1: 31;

      hence thesis by A2, A3, Th36, ZFMISC_1: 51;

    end;

    theorem :: CIRCCMB3:44

    

     Th44: for x1,x2,x3 be set, X be non empty finite set holds for f be Function of (3 -tuples_on X), X holds for S be Signature of X st x1 in the carrier of S & x2 in the carrier of S & not x3 in ( InnerVertices S) & not ( Output ( 1GateCircStr ( <*x1, x2, x3*>,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = (( InputVertices S) \/ {x3})

    proof

      let x1,x2,x3 be set, X be non empty finite set;

      set p = <*x1, x2, x3*>;

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

      let S be Signature of X such that

       A1: x1 in the carrier of S & x2 in the carrier of S and

       A2: not x3 in ( InnerVertices S);

      

       A3: ( rng p) = {x1, x2, x3} by FINSEQ_2: 128

      .= ( {x1, x2} \/ {x3}) by ENUMSET1: 3;

       {x1, x2} c= the carrier of S by A1, ZFMISC_1: 32;

      hence thesis by A2, A3, Th36, ZFMISC_1: 50;

    end;

    theorem :: CIRCCMB3:45

    

     Th45: for x1,x2,x3 be set, X be non empty finite set holds for f be Function of (3 -tuples_on X), X holds for S be Signature of X st x1 in the carrier of S & x3 in the carrier of S & not x2 in ( InnerVertices S) & not ( Output ( 1GateCircStr ( <*x1, x2, x3*>,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = (( InputVertices S) \/ {x2})

    proof

      let x1,x2,x3 be set, X be non empty finite set;

      set p = <*x1, x2, x3*>;

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

      let S be Signature of X such that

       A1: x1 in the carrier of S & x3 in the carrier of S and

       A2: not x2 in ( InnerVertices S);

      

       A3: ( rng p) = {x1, x2, x3} by FINSEQ_2: 128

      .= {x2, x1, x3} by ENUMSET1: 58

      .= ( {x2} \/ {x1, x3}) by ENUMSET1: 2;

       {x1, x3} c= the carrier of S by A1, ZFMISC_1: 32;

      hence thesis by A2, A3, Th36, ZFMISC_1: 50;

    end;

    theorem :: CIRCCMB3:46

    

     Th46: for x1,x2,x3 be set, X be non empty finite set holds for f be Function of (3 -tuples_on X), X holds for S be Signature of X st x2 in the carrier of S & x3 in the carrier of S & not x1 in ( InnerVertices S) & not ( Output ( 1GateCircStr ( <*x1, x2, x3*>,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = (( InputVertices S) \/ {x1})

    proof

      let x1,x2,x3 be set, X be non empty finite set;

      set p = <*x1, x2, x3*>;

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

      let S be Signature of X such that

       A1: x2 in the carrier of S & x3 in the carrier of S and

       A2: not x1 in ( InnerVertices S);

      

       A3: ( rng p) = {x1, x2, x3} by FINSEQ_2: 128

      .= ( {x1} \/ {x2, x3}) by ENUMSET1: 2;

       {x2, x3} c= the carrier of S by A1, ZFMISC_1: 32;

      hence thesis by A2, A3, Th36, ZFMISC_1: 50;

    end;

    theorem :: CIRCCMB3:47

    

     Th47: for x1,x2,x3 be set, X be non empty finite set holds for f be Function of (3 -tuples_on X), X holds for S be Signature of X st x1 in the carrier of S & x2 in the carrier of S & x3 in the carrier of S & not ( Output ( 1GateCircStr ( <*x1, x2, x3*>,f))) in ( InputVertices S) holds ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = ( InputVertices S)

    proof

      let x1,x2,x3 be set, X be non empty finite set;

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

      let S be Signature of X;

      assume x1 in the carrier of S & x2 in the carrier of S & x3 in the carrier of S;

      then

       A1: {x1, x2} c= the carrier of S & {x3} c= the carrier of S by ZFMISC_1: 31, ZFMISC_1: 32;

      ( rng <*x1, x2, x3*>) = {x1, x2, x3} by FINSEQ_2: 128

      .= ( {x1, x2} \/ {x3}) by ENUMSET1: 3;

      hence thesis by A1, Th35, XBOOLE_1: 8;

    end;

    begin

    theorem :: CIRCCMB3:48

    

     Th48: for X be non empty finite set holds for S be finite Signature of X holds for A be Circuit of X, S holds for n be Element of NAT , f be Function of (n -tuples_on X), X holds for p be FinSeqLen of n st not ( Output ( 1GateCircStr (p,f))) in ( InputVertices S) holds for s be State of (A +* ( 1GateCircuit (p,f))) holds for s9 be State of A st s9 = (s | the carrier of S) holds ( stabilization-time s) <= (1 + ( stabilization-time s9))

    proof

      let X be non empty finite set;

      let S be finite Signature of X;

      let A be Circuit of X, S;

      let n be Element of NAT , f be Function of (n -tuples_on X), X;

      let p be FinSeqLen of n such that

       A1: not ( Output ( 1GateCircStr (p,f))) in ( InputVertices S);

      ( InnerVertices ( 1GateCircStr (p,f))) = {( Output ( 1GateCircStr (p,f)))} by Th16;

      then

       A2: ( InputVertices S) misses ( InnerVertices ( 1GateCircStr (p,f))) by A1, ZFMISC_1: 50;

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

      let s9 be State of A such that

       A3: s9 = (s | the carrier of S);

      A tolerates ( 1GateCircuit (p,f)) by Th27;

      then the Sorts of A tolerates the Sorts of ( 1GateCircuit (p,f));

      then

      reconsider s1 = (( Following (s,( stabilization-time s9))) | the carrier of ( 1GateCircStr (p,f))) as State of ( 1GateCircuit (p,f)) by CIRCCOMB: 26;

      

       A4: ( stabilization-time s1) <= 1 by Th21;

      s9 is stabilizing & s1 is stabilizing by Def2;

      then ( stabilization-time s) = (( stabilization-time s9) + ( stabilization-time s1)) by A3, A2, Th10, Th27;

      hence thesis by A4, XREAL_1: 6;

    end;

    scheme :: CIRCCMB3:sch14

    Comb1CircResult { x1() -> object , B() -> non empty finite set , F( object) -> Element of B() , S() -> finite Signature of B() , C() -> Circuit of B(), S() , f() -> Function of (1 -tuples_on B()), B() } :

for s be State of (C() +* ( 1GateCircuit ( <*x1()*>,f()))) holds for s9 be State of C() st s9 = (s | the carrier of S()) holds for a1 be Element of B() st (x1() in ( InnerVertices S()) implies a1 = (( Result s9) . x1())) & ( not x1() in ( InnerVertices S()) implies a1 = (s . x1())) holds (( Result s) . ( Output ( 1GateCircStr ( <*x1()*>,f())))) = F(a1)

      provided

       A1: for g be Function of (1 -tuples_on B()), B() holds g = f() iff for a1 be Element of B() holds (g . <*a1*>) = F(a1)

       and

       A2: not ( Output ( 1GateCircStr ( <*x1()*>,f()))) in ( InputVertices S());

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

      let s be State of (C() +* ( 1GateCircuit ( <*x1()*>,f())));

      let s9 be State of C() such that

       A3: s9 = (s | the carrier of S());

      ( rng <*x1()*>) = {x1()} by FINSEQ_1: 38;

      then

       A4: ( InputVertices S) = ( rng <*x1()*>) & x1() in ( rng <*x1()*>) by CIRCCOMB: 42, TARSKI:def 1;

      then

       A5: x1() in ( InnerVertices S()) or x1() in (( InputVertices S) \ ( InnerVertices S())) by XBOOLE_0:def 5;

      

       A6: s9 is stabilizing by Def2;

      ( InnerVertices S) = {( Output S)} by Th16;

      then

       A7: ( InputVertices S()) misses ( InnerVertices S) by A2, ZFMISC_1: 50;

      

      then

       A8: (( Following (s,( stabilization-time s9))) | the carrier of S()) = ( Following (s9,( stabilization-time s9))) by A3, Th27, CIRCCMB2: 13

      .= ( Result s9) by A6, Th2;

      S() tolerates S by CIRCCOMB: 47;

      then ( InputVertices (S() +* S)) = (( InputVertices S()) \/ (( InputVertices S) \ ( InnerVertices S()))) by A7, FACIRC_1: 4;

      then

       A9: x1() in ( InnerVertices S()) or x1() in ( InputVertices (S() +* S)) by A5, XBOOLE_0:def 3;

      let a1 be Element of B();

      assume (x1() in ( InnerVertices S()) implies a1 = (( Result s9) . x1())) & ( not x1() in ( InnerVertices S()) implies a1 = (s . x1()));

      then

       A10: a1 = (( Following (s,( stabilization-time s9))) . x1()) by A9, A8, Th1, FUNCT_1: 49;

      

       A11: s is stabilizing by Def2;

      the carrier' of S = { [ <*x1()*>, f()]} by CIRCCOMB:def 6;

      then [ <*x1()*>, f()] in { [ <*x1()*>, f()]} & the carrier' of (S() +* S) = (the carrier' of S() \/ { [ <*x1()*>, f()]}) by CIRCCOMB:def 2, TARSKI:def 1;

      then

      reconsider g = [ <*x1()*>, f()] as Gate of (S() +* S) by XBOOLE_0:def 3;

      

       A12: ( the_result_sort_of g) = (the ResultSort of (S() +* S) . g) by MSUALG_1:def 2

      .= g by CIRCCOMB: 44;

      

       A13: (g `2 ) = f();

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

      then

       A14: x1() in the carrier of (S() +* S) by A4, XBOOLE_0:def 3;

      

       A15: [ <*x1()*>, f()] = ( Output S) by Th15;

      g = [(the Arity of (S() +* S) . g), (g `2 )] by CIRCCOMB:def 8;

      

      then

       A16: <*x1()*> = (the Arity of (S() +* S) . g) by XTUPLE_0: 1

      .= ( the_arity_of g) by MSUALG_1:def 1;

      ( dom ( Following (s,( stabilization-time s9)))) = the carrier of (S() +* S) by CIRCUIT1: 3;

      then

       A17: (( Following (s,( stabilization-time s9))) * <*x1()*>) = <*a1*> by A14, A10, FINSEQ_2: 34;

      ( stabilization-time s) <= (1 + ( stabilization-time s9)) by A2, A3, Th48;

      

      hence (( Result s) . ( Output S)) = (( Following (s,(1 + ( stabilization-time s9)))) . ( Output S)) by A11, Th5

      .= (( Following ( Following (s,( stabilization-time s9)))) . g) by A15, FACIRC_1: 12

      .= (f() . (( Following (s,( stabilization-time s9))) * <*x1()*>)) by A12, A16, A13, FACIRC_1: 34

      .= F(a1) by A1, A17;

    end;

    scheme :: CIRCCMB3:sch15

    Comb2CircResult { x1,x2() -> object , B() -> non empty finite set , F( object, object) -> Element of B() , S() -> finite Signature of B() , C() -> Circuit of B(), S() , f() -> Function of (2 -tuples_on B()), B() } :

for s be State of (C() +* ( 1GateCircuit ( <*x1(), x2()*>,f()))) holds for s9 be State of C() st s9 = (s | the carrier of S()) holds for a1,a2 be Element of B() st (x1() in ( InnerVertices S()) implies a1 = (( Result s9) . x1())) & ( not x1() in ( InnerVertices S()) implies a1 = (s . x1())) & (x2() in ( InnerVertices S()) implies a2 = (( Result s9) . x2())) & ( not x2() in ( InnerVertices S()) implies a2 = (s . x2())) holds (( Result s) . ( Output ( 1GateCircStr ( <*x1(), x2()*>,f())))) = F(a1,a2)

      provided

       A1: for g be Function of (2 -tuples_on B()), B() holds g = f() iff for a1,a2 be Element of B() holds (g . <*a1, a2*>) = F(a1,a2)

       and

       A2: not ( Output ( 1GateCircStr ( <*x1(), x2()*>,f()))) in ( InputVertices S());

      set S = ( 1GateCircStr ( <*x1(), x2()*>,f()));

      let s be State of (C() +* ( 1GateCircuit ( <*x1(), x2()*>,f())));

      let s9 be State of C() such that

       A3: s9 = (s | the carrier of S());

      

       A4: s9 is stabilizing by Def2;

      ( InnerVertices S) = {( Output S)} by Th16;

      then

       A5: ( InputVertices S()) misses ( InnerVertices S) by A2, ZFMISC_1: 50;

      

      then

       A6: (( Following (s,( stabilization-time s9))) | the carrier of S()) = ( Following (s9,( stabilization-time s9))) by A3, Th27, CIRCCMB2: 13

      .= ( Result s9) by A4, Th2;

      the carrier' of S = { [ <*x1(), x2()*>, f()]} by CIRCCOMB:def 6;

      then [ <*x1(), x2()*>, f()] in { [ <*x1(), x2()*>, f()]} & the carrier' of (S() +* S) = (the carrier' of S() \/ { [ <*x1(), x2()*>, f()]}) by CIRCCOMB:def 2, TARSKI:def 1;

      then

      reconsider g = [ <*x1(), x2()*>, f()] as Gate of (S() +* S) by XBOOLE_0:def 3;

      let a1,a2 be Element of B() such that

       A7: (x1() in ( InnerVertices S()) implies a1 = (( Result s9) . x1())) & ( not x1() in ( InnerVertices S()) implies a1 = (s . x1())) and

       A8: (x2() in ( InnerVertices S()) implies a2 = (( Result s9) . x2())) & ( not x2() in ( InnerVertices S()) implies a2 = (s . x2()));

      

       A9: ( InputVertices S) = ( rng <*x1(), x2()*>) by CIRCCOMB: 42;

      S() tolerates S by CIRCCOMB: 47;

      then

       A10: ( InputVertices (S() +* S)) = (( InputVertices S()) \/ (( InputVertices S) \ ( InnerVertices S()))) by A5, FACIRC_1: 4;

      

       A11: ( rng <*x1(), x2()*>) = {x1(), x2()} by FINSEQ_2: 127;

      then

       A12: x2() in ( rng <*x1(), x2()*>) by TARSKI:def 2;

      then x2() in ( InnerVertices S()) or x2() in (( InputVertices S) \ ( InnerVertices S())) by A9, XBOOLE_0:def 5;

      then x2() in ( InnerVertices S()) or x2() in ( InputVertices (S() +* S)) by A10, XBOOLE_0:def 3;

      then

       A13: a2 = (( Following (s,( stabilization-time s9))) . x2()) by A8, A6, Th1, FUNCT_1: 49;

      

       A14: x1() in ( rng <*x1(), x2()*>) by A11, TARSKI:def 2;

      then x1() in ( InnerVertices S()) or x1() in (( InputVertices S) \ ( InnerVertices S())) by A9, XBOOLE_0:def 5;

      then x1() in ( InnerVertices S()) or x1() in ( InputVertices (S() +* S)) by A10, XBOOLE_0:def 3;

      then

       A15: a1 = (( Following (s,( stabilization-time s9))) . x1()) by A7, A6, Th1, FUNCT_1: 49;

      g = [(the Arity of (S() +* S) . g), (g `2 )] by CIRCCOMB:def 8;

      

      then

       A16: <*x1(), x2()*> = (the Arity of (S() +* S) . g) by XTUPLE_0: 1

      .= ( the_arity_of g) by MSUALG_1:def 1;

      

       A17: (g `2 ) = f();

      

       A18: the carrier of (S() +* S) = (the carrier of S() \/ the carrier of S) by CIRCCOMB:def 2;

      then

       A19: x2() in the carrier of (S() +* S) by A9, A12, XBOOLE_0:def 3;

      

       A20: [ <*x1(), x2()*>, f()] = ( Output S) by Th15;

      

       A21: s is stabilizing by Def2;

      

       A22: ( dom ( Following (s,( stabilization-time s9)))) = the carrier of (S() +* S) by CIRCUIT1: 3;

      x1() in the carrier of (S() +* S) by A9, A14, A18, XBOOLE_0:def 3;

      then

       A23: (( Following (s,( stabilization-time s9))) * <*x1(), x2()*>) = <*a1, a2*> by A19, A15, A13, A22, FINSEQ_2: 125;

      

       A24: ( the_result_sort_of g) = (the ResultSort of (S() +* S) . g) by MSUALG_1:def 2

      .= g by CIRCCOMB: 44;

      ( stabilization-time s) <= (1 + ( stabilization-time s9)) by A2, A3, Th48;

      

      hence (( Result s) . ( Output S)) = (( Following (s,(1 + ( stabilization-time s9)))) . ( Output S)) by A21, Th5

      .= (( Following ( Following (s,( stabilization-time s9)))) . g) by A20, FACIRC_1: 12

      .= (f() . (( Following (s,( stabilization-time s9))) * <*x1(), x2()*>)) by A24, A16, A17, FACIRC_1: 34

      .= F(a1,a2) by A1, A23;

    end;

    scheme :: CIRCCMB3:sch16

    Comb3CircResult { x1,x2,x3() -> object , B() -> non empty finite set , F( object, object, object) -> Element of B() , S() -> finite Signature of B() , C() -> Circuit of B(), S() , f() -> Function of (3 -tuples_on B()), B() } :

for s be State of (C() +* ( 1GateCircuit ( <*x1(), x2(), x3()*>,f()))) holds for s9 be State of C() st s9 = (s | the carrier of S()) holds for a1,a2,a3 be Element of B() st (x1() in ( InnerVertices S()) implies a1 = (( Result s9) . x1())) & ( not x1() in ( InnerVertices S()) implies a1 = (s . x1())) & (x2() in ( InnerVertices S()) implies a2 = (( Result s9) . x2())) & ( not x2() in ( InnerVertices S()) implies a2 = (s . x2())) & (x3() in ( InnerVertices S()) implies a3 = (( Result s9) . x3())) & ( not x3() in ( InnerVertices S()) implies a3 = (s . x3())) holds (( Result s) . ( Output ( 1GateCircStr ( <*x1(), x2(), x3()*>,f())))) = F(a1,a2,a3)

      provided

       A1: for g be Function of (3 -tuples_on B()), B() holds g = f() iff for a1,a2,a3 be Element of B() holds (g . <*a1, a2, a3*>) = F(a1,a2,a3)

       and

       A2: not ( Output ( 1GateCircStr ( <*x1(), x2(), x3()*>,f()))) in ( InputVertices S());

      set S = ( 1GateCircStr ( <*x1(), x2(), x3()*>,f()));

      let s be State of (C() +* ( 1GateCircuit ( <*x1(), x2(), x3()*>,f())));

      let s9 be State of C() such that

       A3: s9 = (s | the carrier of S());

      

       A4: s9 is stabilizing by Def2;

      ( InnerVertices S) = {( Output S)} by Th16;

      then

       A5: ( InputVertices S()) misses ( InnerVertices S) by A2, ZFMISC_1: 50;

      

      then

       A6: (( Following (s,( stabilization-time s9))) | the carrier of S()) = ( Following (s9,( stabilization-time s9))) by A3, Th27, CIRCCMB2: 13

      .= ( Result s9) by A4, Th2;

      S() tolerates S by CIRCCOMB: 47;

      then

       A7: ( InputVertices (S() +* S)) = (( InputVertices S()) \/ (( InputVertices S) \ ( InnerVertices S()))) by A5, FACIRC_1: 4;

      the carrier' of S = { [ <*x1(), x2(), x3()*>, f()]} by CIRCCOMB:def 6;

      then [ <*x1(), x2(), x3()*>, f()] in { [ <*x1(), x2(), x3()*>, f()]} & the carrier' of (S() +* S) = (the carrier' of S() \/ { [ <*x1(), x2(), x3()*>, f()]}) by CIRCCOMB:def 2, TARSKI:def 1;

      then

      reconsider g = [ <*x1(), x2(), x3()*>, f()] as Gate of (S() +* S) by XBOOLE_0:def 3;

      let a1,a2,a3 be Element of B() such that

       A8: (x1() in ( InnerVertices S()) implies a1 = (( Result s9) . x1())) & ( not x1() in ( InnerVertices S()) implies a1 = (s . x1())) and

       A9: (x2() in ( InnerVertices S()) implies a2 = (( Result s9) . x2())) & ( not x2() in ( InnerVertices S()) implies a2 = (s . x2())) and

       A10: (x3() in ( InnerVertices S()) implies a3 = (( Result s9) . x3())) & ( not x3() in ( InnerVertices S()) implies a3 = (s . x3()));

      

       A11: ( InputVertices S) = ( rng <*x1(), x2(), x3()*>) by CIRCCOMB: 42;

      g = [(the Arity of (S() +* S) . g), (g `2 )] by CIRCCOMB:def 8;

      

      then

       A12: <*x1(), x2(), x3()*> = (the Arity of (S() +* S) . g) by XTUPLE_0: 1

      .= ( the_arity_of g) by MSUALG_1:def 1;

      

       A13: (g `2 ) = f();

      

       A14: s is stabilizing by Def2;

      

       A15: the carrier of (S() +* S) = (the carrier of S() \/ the carrier of S) by CIRCCOMB:def 2;

      

       A16: ( rng <*x1(), x2(), x3()*>) = {x1(), x2(), x3()} by FINSEQ_2: 128;

      then

       A17: x3() in ( rng <*x1(), x2(), x3()*>) by ENUMSET1:def 1;

      then

       A18: x3() in the carrier of (S() +* S) by A11, A15, XBOOLE_0:def 3;

      x3() in ( InnerVertices S()) or x3() in (( InputVertices S) \ ( InnerVertices S())) by A11, A17, XBOOLE_0:def 5;

      then x3() in ( InnerVertices S()) or x3() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A19: a3 = (( Following (s,( stabilization-time s9))) . x3()) by A10, A6, Th1, FUNCT_1: 49;

      

       A20: [ <*x1(), x2(), x3()*>, f()] = ( Output S) by Th15;

      

       A21: ( dom ( Following (s,( stabilization-time s9)))) = the carrier of (S() +* S) by CIRCUIT1: 3;

      

       A22: x1() in ( rng <*x1(), x2(), x3()*>) by A16, ENUMSET1:def 1;

      then x1() in ( InnerVertices S()) or x1() in (( InputVertices S) \ ( InnerVertices S())) by A11, XBOOLE_0:def 5;

      then x1() in ( InnerVertices S()) or x1() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A23: a1 = (( Following (s,( stabilization-time s9))) . x1()) by A8, A6, Th1, FUNCT_1: 49;

      

       A24: x2() in ( rng <*x1(), x2(), x3()*>) by A16, ENUMSET1:def 1;

      then

       A25: x2() in the carrier of (S() +* S) by A11, A15, XBOOLE_0:def 3;

      x2() in ( InnerVertices S()) or x2() in (( InputVertices S) \ ( InnerVertices S())) by A11, A24, XBOOLE_0:def 5;

      then x2() in ( InnerVertices S()) or x2() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A26: a2 = (( Following (s,( stabilization-time s9))) . x2()) by A9, A6, Th1, FUNCT_1: 49;

      x1() in the carrier of (S() +* S) by A11, A22, A15, XBOOLE_0:def 3;

      then

       A27: (( Following (s,( stabilization-time s9))) * <*x1(), x2(), x3()*>) = <*a1, a2, a3*> by A25, A18, A23, A26, A19, A21, FINSEQ_2: 126;

      

       A28: ( the_result_sort_of g) = (the ResultSort of (S() +* S) . g) by MSUALG_1:def 2

      .= g by CIRCCOMB: 44;

      ( stabilization-time s) <= (1 + ( stabilization-time s9)) by A2, A3, Th48;

      

      hence (( Result s) . ( Output S)) = (( Following (s,(1 + ( stabilization-time s9)))) . ( Output S)) by A14, Th5

      .= (( Following ( Following (s,( stabilization-time s9)))) . g) by A20, FACIRC_1: 12

      .= (f() . (( Following (s,( stabilization-time s9))) * <*x1(), x2(), x3()*>)) by A28, A12, A13, FACIRC_1: 34

      .= F(a1,a2,a3) by A1, A27;

    end;

    scheme :: CIRCCMB3:sch17

    Comb4CircResult { x1,x2,x3,x4() -> object , B() -> non empty finite set , F( object, object, object, object) -> Element of B() , S() -> finite Signature of B() , C() -> Circuit of B(), S() , f() -> Function of (4 -tuples_on B()), B() } :

for s be State of (C() +* ( 1GateCircuit ( <*x1(), x2(), x3(), x4()*>,f()))) holds for s9 be State of C() st s9 = (s | the carrier of S()) holds for a1,a2,a3,a4 be Element of B() st (x1() in ( InnerVertices S()) implies a1 = (( Result s9) . x1())) & ( not x1() in ( InnerVertices S()) implies a1 = (s . x1())) & (x2() in ( InnerVertices S()) implies a2 = (( Result s9) . x2())) & ( not x2() in ( InnerVertices S()) implies a2 = (s . x2())) & (x3() in ( InnerVertices S()) implies a3 = (( Result s9) . x3())) & ( not x3() in ( InnerVertices S()) implies a3 = (s . x3())) & (x4() in ( InnerVertices S()) implies a4 = (( Result s9) . x4())) & ( not x4() in ( InnerVertices S()) implies a4 = (s . x4())) holds (( Result s) . ( Output ( 1GateCircStr ( <*x1(), x2(), x3(), x4()*>,f())))) = F(a1,a2,a3,a4)

      provided

       A1: for g be Function of (4 -tuples_on B()), B() holds g = f() iff for a1,a2,a3,a4 be Element of B() holds (g . <*a1, a2, a3, a4*>) = F(a1,a2,a3,a4)

       and

       A2: not ( Output ( 1GateCircStr ( <*x1(), x2(), x3(), x4()*>,f()))) in ( InputVertices S());

      set S = ( 1GateCircStr ( <*x1(), x2(), x3(), x4()*>,f()));

      let s be State of (C() +* ( 1GateCircuit ( <*x1(), x2(), x3(), x4()*>,f())));

      let s9 be State of C() such that

       A3: s9 = (s | the carrier of S());

      

       A4: s9 is stabilizing by Def2;

      ( InnerVertices S) = {( Output S)} by Th16;

      then

       A5: ( InputVertices S()) misses ( InnerVertices S) by A2, ZFMISC_1: 50;

      

      then

       A6: (( Following (s,( stabilization-time s9))) | the carrier of S()) = ( Following (s9,( stabilization-time s9))) by A3, Th27, CIRCCMB2: 13

      .= ( Result s9) by A4, Th2;

      S() tolerates S by CIRCCOMB: 47;

      then

       A7: ( InputVertices (S() +* S)) = (( InputVertices S()) \/ (( InputVertices S) \ ( InnerVertices S()))) by A5, FACIRC_1: 4;

      

       A8: [ <*x1(), x2(), x3(), x4()*>, f()] = ( Output S) by Th15;

      

       A9: s is stabilizing by Def2;

      

       A10: the carrier of (S() +* S) = (the carrier of S() \/ the carrier of S) by CIRCCOMB:def 2;

      the carrier' of S = { [ <*x1(), x2(), x3(), x4()*>, f()]} by CIRCCOMB:def 6;

      then [ <*x1(), x2(), x3(), x4()*>, f()] in { [ <*x1(), x2(), x3(), x4()*>, f()]} & the carrier' of (S() +* S) = (the carrier' of S() \/ { [ <*x1(), x2(), x3(), x4()*>, f()]}) by CIRCCOMB:def 2, TARSKI:def 1;

      then

      reconsider g = [ <*x1(), x2(), x3(), x4()*>, f()] as Gate of (S() +* S) by XBOOLE_0:def 3;

      let a1,a2,a3,a4 be Element of B() such that

       A11: (x1() in ( InnerVertices S()) implies a1 = (( Result s9) . x1())) & ( not x1() in ( InnerVertices S()) implies a1 = (s . x1())) and

       A12: (x2() in ( InnerVertices S()) implies a2 = (( Result s9) . x2())) & ( not x2() in ( InnerVertices S()) implies a2 = (s . x2())) and

       A13: (x3() in ( InnerVertices S()) implies a3 = (( Result s9) . x3())) & ( not x3() in ( InnerVertices S()) implies a3 = (s . x3())) and

       A14: (x4() in ( InnerVertices S()) implies a4 = (( Result s9) . x4())) & ( not x4() in ( InnerVertices S()) implies a4 = (s . x4()));

      

       A15: ( InputVertices S) = ( rng <*x1(), x2(), x3(), x4()*>) by CIRCCOMB: 42;

      

       A16: ( rng <*x1(), x2(), x3(), x4()*>) = {x1(), x2(), x3(), x4()} by Th13;

      then

       A17: x3() in ( rng <*x1(), x2(), x3(), x4()*>) by ENUMSET1:def 2;

      then

       A18: x3() in the carrier of (S() +* S) by A15, A10, XBOOLE_0:def 3;

      

       A19: x4() in ( rng <*x1(), x2(), x3(), x4()*>) by A16, ENUMSET1:def 2;

      then

       A20: x4() in the carrier of (S() +* S) by A15, A10, XBOOLE_0:def 3;

      

       A21: x1() in ( rng <*x1(), x2(), x3(), x4()*>) by A16, ENUMSET1:def 2;

      then

       A22: x1() in the carrier of (S() +* S) by A15, A10, XBOOLE_0:def 3;

      x3() in ( InnerVertices S()) or x3() in (( InputVertices S) \ ( InnerVertices S())) by A15, A17, XBOOLE_0:def 5;

      then x3() in ( InnerVertices S()) or x3() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A23: a3 = (( Following (s,( stabilization-time s9))) . x3()) by A13, A6, Th1, FUNCT_1: 49;

      g = [(the Arity of (S() +* S) . g), (g `2 )] by CIRCCOMB:def 8;

      

      then

       A24: <*x1(), x2(), x3(), x4()*> = (the Arity of (S() +* S) . g) by XTUPLE_0: 1

      .= ( the_arity_of g) by MSUALG_1:def 1;

      

       A25: (g `2 ) = f();

      x1() in ( InnerVertices S()) or x1() in (( InputVertices S) \ ( InnerVertices S())) by A15, A21, XBOOLE_0:def 5;

      then x1() in ( InnerVertices S()) or x1() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A26: a1 = (( Following (s,( stabilization-time s9))) . x1()) by A11, A6, Th1, FUNCT_1: 49;

      

       A27: x2() in ( rng <*x1(), x2(), x3(), x4()*>) by A16, ENUMSET1:def 2;

      then

       A28: x2() in the carrier of (S() +* S) by A15, A10, XBOOLE_0:def 3;

      x4() in ( InnerVertices S()) or x4() in (( InputVertices S) \ ( InnerVertices S())) by A15, A19, XBOOLE_0:def 5;

      then x4() in ( InnerVertices S()) or x4() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A29: a4 = (( Following (s,( stabilization-time s9))) . x4()) by A14, A6, Th1, FUNCT_1: 49;

      x2() in ( InnerVertices S()) or x2() in (( InputVertices S) \ ( InnerVertices S())) by A15, A27, XBOOLE_0:def 5;

      then x2() in ( InnerVertices S()) or x2() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A30: a2 = (( Following (s,( stabilization-time s9))) . x2()) by A12, A6, Th1, FUNCT_1: 49;

      ( dom ( Following (s,( stabilization-time s9)))) = the carrier of (S() +* S) by CIRCUIT1: 3;

      then

       A31: (( Following (s,( stabilization-time s9))) * <*x1(), x2(), x3(), x4()*>) = <*a1, a2, a3, a4*> by A22, A28, A18, A20, A26, A30, A23, A29, Th33;

      

       A32: ( the_result_sort_of g) = (the ResultSort of (S() +* S) . g) by MSUALG_1:def 2

      .= g by CIRCCOMB: 44;

      ( stabilization-time s) <= (1 + ( stabilization-time s9)) by A2, A3, Th48;

      

      hence (( Result s) . ( Output S)) = (( Following (s,(1 + ( stabilization-time s9)))) . ( Output S)) by A9, Th5

      .= (( Following ( Following (s,( stabilization-time s9)))) . g) by A8, FACIRC_1: 12

      .= (f() . (( Following (s,( stabilization-time s9))) * <*x1(), x2(), x3(), x4()*>)) by A32, A24, A25, FACIRC_1: 34

      .= F(a1,a2,a3,a4) by A1, A31;

    end;

    scheme :: CIRCCMB3:sch18

    Comb5CircResult { x1,x2,x3,x4,x5() -> object , B() -> non empty finite set , F( object, object, object, object, object) -> Element of B() , S() -> finite Signature of B() , C() -> Circuit of B(), S() , f() -> Function of (5 -tuples_on B()), B() } :

for s be State of (C() +* ( 1GateCircuit ( <*x1(), x2(), x3(), x4(), x5()*>,f()))) holds for s9 be State of C() st s9 = (s | the carrier of S()) holds for a1,a2,a3,a4,a5 be Element of B() st (x1() in ( InnerVertices S()) implies a1 = (( Result s9) . x1())) & ( not x1() in ( InnerVertices S()) implies a1 = (s . x1())) & (x2() in ( InnerVertices S()) implies a2 = (( Result s9) . x2())) & ( not x2() in ( InnerVertices S()) implies a2 = (s . x2())) & (x3() in ( InnerVertices S()) implies a3 = (( Result s9) . x3())) & ( not x3() in ( InnerVertices S()) implies a3 = (s . x3())) & (x4() in ( InnerVertices S()) implies a4 = (( Result s9) . x4())) & ( not x4() in ( InnerVertices S()) implies a4 = (s . x4())) & (x5() in ( InnerVertices S()) implies a5 = (( Result s9) . x5())) & ( not x5() in ( InnerVertices S()) implies a5 = (s . x5())) holds (( Result s) . ( Output ( 1GateCircStr ( <*x1(), x2(), x3(), x4(), x5()*>,f())))) = F(a1,a2,a3,a4,a5)

      provided

       A1: for g be Function of (5 -tuples_on B()), B() holds g = f() iff for a1,a2,a3,a4,a5 be Element of B() holds (g . <*a1, a2, a3, a4, a5*>) = F(a1,a2,a3,a4,a5)

       and

       A2: not ( Output ( 1GateCircStr ( <*x1(), x2(), x3(), x4(), x5()*>,f()))) in ( InputVertices S());

      set S = ( 1GateCircStr ( <*x1(), x2(), x3(), x4(), x5()*>,f()));

      let s be State of (C() +* ( 1GateCircuit ( <*x1(), x2(), x3(), x4(), x5()*>,f())));

      let s9 be State of C() such that

       A3: s9 = (s | the carrier of S());

      

       A4: s9 is stabilizing by Def2;

      ( InnerVertices S) = {( Output S)} by Th16;

      then

       A5: ( InputVertices S()) misses ( InnerVertices S) by A2, ZFMISC_1: 50;

      

      then

       A6: (( Following (s,( stabilization-time s9))) | the carrier of S()) = ( Following (s9,( stabilization-time s9))) by A3, Th27, CIRCCMB2: 13

      .= ( Result s9) by A4, Th2;

      S() tolerates S by CIRCCOMB: 47;

      then

       A7: ( InputVertices (S() +* S)) = (( InputVertices S()) \/ (( InputVertices S) \ ( InnerVertices S()))) by A5, FACIRC_1: 4;

      

       A8: [ <*x1(), x2(), x3(), x4(), x5()*>, f()] = ( Output S) by Th15;

      

       A9: s is stabilizing by Def2;

      

       A10: the carrier of (S() +* S) = (the carrier of S() \/ the carrier of S) by CIRCCOMB:def 2;

      the carrier' of S = { [ <*x1(), x2(), x3(), x4(), x5()*>, f()]} by CIRCCOMB:def 6;

      then [ <*x1(), x2(), x3(), x4(), x5()*>, f()] in { [ <*x1(), x2(), x3(), x4(), x5()*>, f()]} & the carrier' of (S() +* S) = (the carrier' of S() \/ { [ <*x1(), x2(), x3(), x4(), x5()*>, f()]}) by CIRCCOMB:def 2, TARSKI:def 1;

      then

      reconsider g = [ <*x1(), x2(), x3(), x4(), x5()*>, f()] as Gate of (S() +* S) by XBOOLE_0:def 3;

      let a1,a2,a3,a4,a5 be Element of B() such that

       A11: (x1() in ( InnerVertices S()) implies a1 = (( Result s9) . x1())) & ( not x1() in ( InnerVertices S()) implies a1 = (s . x1())) and

       A12: (x2() in ( InnerVertices S()) implies a2 = (( Result s9) . x2())) & ( not x2() in ( InnerVertices S()) implies a2 = (s . x2())) and

       A13: (x3() in ( InnerVertices S()) implies a3 = (( Result s9) . x3())) & ( not x3() in ( InnerVertices S()) implies a3 = (s . x3())) and

       A14: (x4() in ( InnerVertices S()) implies a4 = (( Result s9) . x4())) & ( not x4() in ( InnerVertices S()) implies a4 = (s . x4())) and

       A15: (x5() in ( InnerVertices S()) implies a5 = (( Result s9) . x5())) & ( not x5() in ( InnerVertices S()) implies a5 = (s . x5()));

      

       A16: ( InputVertices S) = ( rng <*x1(), x2(), x3(), x4(), x5()*>) by CIRCCOMB: 42;

      

       A17: ( rng <*x1(), x2(), x3(), x4(), x5()*>) = {x1(), x2(), x3(), x4(), x5()} by Th14;

      then

       A18: x1() in ( rng <*x1(), x2(), x3(), x4(), x5()*>) by ENUMSET1:def 3;

      then

       A19: x1() in the carrier of (S() +* S) by A16, A10, XBOOLE_0:def 3;

      

       A20: x5() in ( rng <*x1(), x2(), x3(), x4(), x5()*>) by A17, ENUMSET1:def 3;

      then

       A21: x5() in the carrier of (S() +* S) by A16, A10, XBOOLE_0:def 3;

      x5() in ( InnerVertices S()) or x5() in (( InputVertices S) \ ( InnerVertices S())) by A16, A20, XBOOLE_0:def 5;

      then x5() in ( InnerVertices S()) or x5() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A22: a5 = (( Following (s,( stabilization-time s9))) . x5()) by A15, A6, Th1, FUNCT_1: 49;

      

       A23: x4() in ( rng <*x1(), x2(), x3(), x4(), x5()*>) by A17, ENUMSET1:def 3;

      then

       A24: x4() in the carrier of (S() +* S) by A16, A10, XBOOLE_0:def 3;

      

       A25: x3() in ( rng <*x1(), x2(), x3(), x4(), x5()*>) by A17, ENUMSET1:def 3;

      then

       A26: x3() in the carrier of (S() +* S) by A16, A10, XBOOLE_0:def 3;

      x3() in ( InnerVertices S()) or x3() in (( InputVertices S) \ ( InnerVertices S())) by A16, A25, XBOOLE_0:def 5;

      then x3() in ( InnerVertices S()) or x3() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A27: a3 = (( Following (s,( stabilization-time s9))) . x3()) by A13, A6, Th1, FUNCT_1: 49;

      

       A28: x2() in ( rng <*x1(), x2(), x3(), x4(), x5()*>) by A17, ENUMSET1:def 3;

      then

       A29: x2() in the carrier of (S() +* S) by A16, A10, XBOOLE_0:def 3;

      x1() in ( InnerVertices S()) or x1() in (( InputVertices S) \ ( InnerVertices S())) by A16, A18, XBOOLE_0:def 5;

      then x1() in ( InnerVertices S()) or x1() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A30: a1 = (( Following (s,( stabilization-time s9))) . x1()) by A11, A6, Th1, FUNCT_1: 49;

      g = [(the Arity of (S() +* S) . g), (g `2 )] by CIRCCOMB:def 8;

      

      then

       A31: <*x1(), x2(), x3(), x4(), x5()*> = (the Arity of (S() +* S) . g) by XTUPLE_0: 1

      .= ( the_arity_of g) by MSUALG_1:def 1;

      

       A32: (g `2 ) = f();

      x4() in ( InnerVertices S()) or x4() in (( InputVertices S) \ ( InnerVertices S())) by A16, A23, XBOOLE_0:def 5;

      then x4() in ( InnerVertices S()) or x4() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A33: a4 = (( Following (s,( stabilization-time s9))) . x4()) by A14, A6, Th1, FUNCT_1: 49;

      x2() in ( InnerVertices S()) or x2() in (( InputVertices S) \ ( InnerVertices S())) by A16, A28, XBOOLE_0:def 5;

      then x2() in ( InnerVertices S()) or x2() in ( InputVertices (S() +* S)) by A7, XBOOLE_0:def 3;

      then

       A34: a2 = (( Following (s,( stabilization-time s9))) . x2()) by A12, A6, Th1, FUNCT_1: 49;

      ( dom ( Following (s,( stabilization-time s9)))) = the carrier of (S() +* S) by CIRCUIT1: 3;

      then

       A35: (( Following (s,( stabilization-time s9))) * <*x1(), x2(), x3(), x4(), x5()*>) = <*a1, a2, a3, a4, a5*> by A19, A29, A26, A24, A21, A30, A34, A27, A33, A22, Th34;

      

       A36: ( the_result_sort_of g) = (the ResultSort of (S() +* S) . g) by MSUALG_1:def 2

      .= g by CIRCCOMB: 44;

      ( stabilization-time s) <= (1 + ( stabilization-time s9)) by A2, A3, Th48;

      

      hence (( Result s) . ( Output S)) = (( Following (s,(1 + ( stabilization-time s9)))) . ( Output S)) by A9, Th5

      .= (( Following ( Following (s,( stabilization-time s9)))) . g) by A8, FACIRC_1: 12

      .= (f() . (( Following (s,( stabilization-time s9))) * <*x1(), x2(), x3(), x4(), x5()*>)) by A36, A31, A32, FACIRC_1: 34

      .= F(a1,a2,a3,a4,a5) by A1, A35;

    end;

    begin

    definition

      let S be non empty ManySortedSign;

      :: CIRCCMB3:def11

      attr S is with_nonpair_inputs means

      : Def11: ( InputVertices S) is without_pairs;

    end

    registration

      cluster NAT -> without_pairs;

      coherence ;

      let X be without_pairs set;

      cluster -> without_pairs for Subset of X;

      coherence by FACIRC_1:def 2;

    end

    registration

      cluster natural-valued -> nonpair-yielding for Function;

      coherence

      proof

        let f be Function;

        assume f is natural-valued;

        then

         A1: ( rng f) c= NAT by VALUED_0:def 6;

        let x be set;

        assume x in ( dom f);

        then (f . x) in ( rng f) by FUNCT_1:def 3;

        hence thesis by A1;

      end;

    end

    registration

      cluster one-to-one natural-valued for FinSequence;

      existence

      proof

        set p = the one-to-one FinSequence of NAT ;

        take p;

        thus thesis;

      end;

    end

    registration

      let n be Element of NAT ;

      cluster one-to-one natural-valued for FinSeqLen of n;

      existence

      proof

        set p = ( id ( Seg n));

        

         A1: ( dom p) = ( Seg n);

        then ( rng p) = ( Seg n) & p is FinSequence by FINSEQ_1:def 2;

        then

        reconsider p as one-to-one FinSequence of NAT by FINSEQ_1:def 4;

        ( len p) = n by A1, FINSEQ_1:def 3;

        then

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

        take p;

        thus thesis;

      end;

    end

    registration

      let p be nonpair-yielding FinSequence;

      let f be set;

      cluster ( 1GateCircStr (p,f)) -> with_nonpair_inputs;

      coherence

      proof

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

        hence ( InputVertices ( 1GateCircStr (p,f))) is without_pairs;

      end;

    end

    registration

      cluster with_nonpair_inputs for one-gate ManySortedSign;

      existence

      proof

        set n = the Element of NAT , X = the non empty finite set;

        set f = the Function of (n -tuples_on X), X;

        set p = the natural-valued FinSeqLen of n;

        take ( 1GateCircStr (p,f));

        thus thesis;

      end;

      let X be non empty finite set;

      cluster with_nonpair_inputs for one-gate Signature of X;

      existence

      proof

        reconsider z = 0 as Element of NAT ;

        set p = the natural-valued FinSeqLen of z;

        set f = the Function of (z -tuples_on X), X;

        take ( 1GateCircStr (p,f));

        thus thesis;

      end;

    end

    registration

      let S be with_nonpair_inputs non empty ManySortedSign;

      cluster ( InputVertices S) -> without_pairs;

      coherence by Def11;

    end

    theorem :: CIRCCMB3:49

    for S be with_nonpair_inputs non empty ManySortedSign holds for x be Vertex of S st x is pair holds x in ( InnerVertices S)

    proof

      let S be with_nonpair_inputs non empty ManySortedSign;

      let x be Vertex of S;

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

      then x in ( InputVertices S) or x in ( InnerVertices S) by XBOOLE_0:def 3;

      hence thesis by FACIRC_1:def 2;

    end;

    registration

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

      cluster ( InnerVertices S) -> Relation-like;

      coherence

      proof

        let x be object;

        assume

         A1: x in ( InnerVertices S);

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

        then x = [(the Arity of S . x), (x `2 )] by A1, CIRCCOMB:def 8;

        hence thesis;

      end;

    end

    registration

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

      cluster ( InnerVertices S) -> Relation-like;

      coherence

      proof

        let x be object;

        consider A be MSAlgebra over S such that

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

        assume x in ( InnerVertices S);

        then

        reconsider g = x as Gate of S by FACIRC_1: 37;

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

        hence thesis;

      end;

    end

    registration

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

      cluster (S1 +* S2) -> with_nonpair_inputs;

      coherence

      proof

        S1 tolerates S2 by CIRCCOMB: 47;

        then ( InputVertices (S1 +* S2)) is Subset of (( InputVertices S1) \/ ( InputVertices S2)) by CIRCCOMB: 11;

        hence ( InputVertices (S1 +* S2)) is without_pairs;

      end;

    end

    theorem :: CIRCCMB3:50

    for x be non pair set, R be Relation holds not x in R

    proof

      let x be non pair set;

       not ex a,b be object st x = [a, b];

      hence thesis by RELAT_1:def 1;

    end;

    theorem :: CIRCCMB3:51

    

     Th51: for x1 be set, X be non empty finite set holds for f be Function of (1 -tuples_on X), X holds for S be with_nonpair_inputs Signature of X st x1 in the carrier of S or x1 is non pair holds (S +* ( 1GateCircStr ( <*x1*>,f))) is with_nonpair_inputs

    proof

      let x1 be set, X be non empty finite set;

      let f be Function of (1 -tuples_on X), X;

      let S be with_nonpair_inputs Signature of X such that

       A1: x1 in the carrier of S or x1 is non pair;

      

       A2: not ( Output ( 1GateCircStr ( <*x1*>,f))) in ( InputVertices S) by FACIRC_1:def 2;

      per cases by A1;

        suppose x1 in the carrier of S;

        hence ( InputVertices (S +* ( 1GateCircStr ( <*x1*>,f)))) is without_pairs by A2, Th37;

      end;

        suppose x1 is non pair;

        then

        reconsider a = x1 as non pair set;

        ( rng <*x1*>) = {a} by FINSEQ_1: 38;

        hence ( InputVertices (S +* ( 1GateCircStr ( <*x1*>,f)))) is without_pairs;

      end;

    end;

    registration

      let X be non empty finite set;

      let S be with_nonpair_inputs Signature of X;

      let x1 be Vertex of S;

      let f be Function of (1 -tuples_on X), X;

      cluster (S +* ( 1GateCircStr ( <*x1*>,f))) -> with_nonpair_inputs;

      coherence by Th51;

    end

    registration

      let X be non empty finite set;

      let S be with_nonpair_inputs Signature of X;

      let x1 be non pair set;

      let f be Function of (1 -tuples_on X), X;

      cluster (S +* ( 1GateCircStr ( <*x1*>,f))) -> with_nonpair_inputs;

      coherence ;

    end

    theorem :: CIRCCMB3:52

    

     Th52: for x1,x2 be set, X be non empty finite set holds for f be Function of (2 -tuples_on X), X holds for S be with_nonpair_inputs Signature of X st (x1 in the carrier of S or x1 is non pair) & (x2 in the carrier of S or x2 is non pair) holds (S +* ( 1GateCircStr ( <*x1, x2*>,f))) is with_nonpair_inputs

    proof

      let x1,x2 be set, X be non empty finite set;

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

      let S be with_nonpair_inputs Signature of X such that

       A1: (x1 in the carrier of S or x1 is non pair) & (x2 in the carrier of S or x2 is non pair);

      

       A2: not ( Output ( 1GateCircStr ( <*x1, x2*>,f))) in ( InputVertices S) by FACIRC_1:def 2;

      per cases by A1;

        suppose x1 in the carrier of S & x2 in the carrier of S or x1 in the carrier of S & not x2 in ( InnerVertices S) or x2 in the carrier of S & not x1 in ( InnerVertices S);

        then ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2*>,f)))) = ( InputVertices S) or {x2} is without_pairs & ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2*>,f)))) = ( {x2} \/ ( InputVertices S)) or {x1} is without_pairs & ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2*>,f)))) = ( {x1} \/ ( InputVertices S)) by A1, A2, Th38, Th39, Th40;

        hence ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2*>,f)))) is without_pairs;

      end;

        suppose x1 is non pair & x2 is non pair;

        then

        reconsider a = x1, b = x2 as non pair set;

        ( rng <*x1, x2*>) = {a, b} by FINSEQ_2: 127;

        hence ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2*>,f)))) is without_pairs;

      end;

    end;

    registration

      let X be non empty finite set;

      let S be with_nonpair_inputs Signature of X;

      let x1 be Vertex of S, n2 be non pair set;

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

      cluster (S +* ( 1GateCircStr ( <*x1, n2*>,f))) -> with_nonpair_inputs;

      coherence by Th52;

      cluster (S +* ( 1GateCircStr ( <*n2, x1*>,f))) -> with_nonpair_inputs;

      coherence by Th52;

    end

    registration

      let X be non empty finite set;

      let S be with_nonpair_inputs Signature of X;

      let x1,x2 be Vertex of S;

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

      cluster (S +* ( 1GateCircStr ( <*x1, x2*>,f))) -> with_nonpair_inputs;

      coherence by Th52;

    end

    theorem :: CIRCCMB3:53

    

     Th53: for x1,x2,x3 be set, X be non empty finite set holds for f be Function of (3 -tuples_on X), X holds for S be with_nonpair_inputs Signature of X st (x1 in the carrier of S or x1 is non pair) & (x2 in the carrier of S or x2 is non pair) & (x3 in the carrier of S or x3 is non pair) holds (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f))) is with_nonpair_inputs

    proof

      let x1,x2,x3 be set, X be non empty finite set;

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

      let S be with_nonpair_inputs Signature of X such that

       A1: (x1 in the carrier of S or x1 is non pair) & (x2 in the carrier of S or x2 is non pair) & (x3 in the carrier of S or x3 is non pair);

      

       A2: not ( Output ( 1GateCircStr ( <*x1, x2, x3*>,f))) in ( InputVertices S) by FACIRC_1:def 2;

      per cases by A1;

        suppose x1 in the carrier of S & x2 in the carrier of S & x3 in the carrier of S or x1 in the carrier of S & not x2 in ( InnerVertices S) & x3 in the carrier of S or x2 in the carrier of S & not x1 in ( InnerVertices S) & x3 in the carrier of S or x1 in the carrier of S & x2 in the carrier of S & not x3 in ( InnerVertices S) or x1 in the carrier of S & not x2 in ( InnerVertices S) & not x3 in ( InnerVertices S) or x2 in the carrier of S & not x1 in ( InnerVertices S) & not x3 in ( InnerVertices S) or not x1 in ( InnerVertices S) & not x2 in ( InnerVertices S) & x3 in the carrier of S;

        then ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = ( InputVertices S) or {x2} is without_pairs & ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = ( {x2} \/ ( InputVertices S)) or {x1} is without_pairs & ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = ( {x1} \/ ( InputVertices S)) or {x3} is without_pairs & ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = ( {x3} \/ ( InputVertices S)) or {x1, x2} is without_pairs & ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = ( {x1, x2} \/ ( InputVertices S)) or {x2, x3} is without_pairs & ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = ( {x2, x3} \/ ( InputVertices S)) or {x1, x3} is without_pairs & ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) = ( {x1, x3} \/ ( InputVertices S)) by A1, A2, Th41, Th42, Th43, Th44, Th45, Th46, Th47;

        hence ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) is without_pairs;

      end;

        suppose x1 is non pair & x2 is non pair & x3 is non pair;

        then

        reconsider a = x1, b = x2, c = x3 as non pair set;

        ( rng <*x1, x2, x3*>) = {a, b, c} by FINSEQ_2: 128;

        hence ( InputVertices (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f)))) is without_pairs;

      end;

    end;

    registration

      let X be non empty finite set;

      let S be with_nonpair_inputs Signature of X;

      let x1,x2 be Vertex of S, n be non pair set;

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

      cluster (S +* ( 1GateCircStr ( <*x1, x2, n*>,f))) -> with_nonpair_inputs;

      coherence by Th53;

      cluster (S +* ( 1GateCircStr ( <*x1, n, x2*>,f))) -> with_nonpair_inputs;

      coherence by Th53;

      cluster (S +* ( 1GateCircStr ( <*n, x1, x2*>,f))) -> with_nonpair_inputs;

      coherence by Th53;

    end

    registration

      let X be non empty finite set;

      let S be with_nonpair_inputs Signature of X;

      let x be Vertex of S, n1,n2 be non pair set;

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

      cluster (S +* ( 1GateCircStr ( <*x, n1, n2*>,f))) -> with_nonpair_inputs;

      coherence by Th53;

      cluster (S +* ( 1GateCircStr ( <*n1, x, n2*>,f))) -> with_nonpair_inputs;

      coherence by Th53;

      cluster (S +* ( 1GateCircStr ( <*n1, n2, x*>,f))) -> with_nonpair_inputs;

      coherence by Th53;

    end

    registration

      let X be non empty finite set;

      let S be with_nonpair_inputs Signature of X;

      let x1,x2,x3 be Vertex of S;

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

      cluster (S +* ( 1GateCircStr ( <*x1, x2, x3*>,f))) -> with_nonpair_inputs;

      coherence by Th53;

    end