circcmb2.miz



    begin

    registration

      let n be Nat;

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

      let p be FinSeqLen of n;

      cluster ( 1GateCircuit (p,f)) -> Boolean;

      coherence by CIRCCOMB: 61;

    end

    theorem :: CIRCCMB2:1

    

     Th1: for X be finite non empty set, n be Nat holds for p be FinSeqLen of n holds for f be Function of (n -tuples_on X), X holds for o be OperSymbol of ( 1GateCircStr (p,f)) holds for s be State of ( 1GateCircuit (p,f)) holds (o depends_on_in s) = (s * p)

    proof

      let X be finite non empty set;

      let n be Nat;

      let p be FinSeqLen of n;

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

      let o be OperSymbol of ( 1GateCircStr (p,f));

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

      (o depends_on_in s) = (s * ( the_arity_of o)) by CIRCUIT1:def 3

      .= (s * p) by CIRCCOMB: 41;

      hence thesis;

    end;

    theorem :: CIRCCMB2:2

    for X be finite non empty set, n be Nat holds for p be FinSeqLen of n holds for f be Function of (n -tuples_on X), X holds for s be State of ( 1GateCircuit (p,f)) holds ( Following s) is stable

    proof

      let X be finite non empty set, n be Nat;

      let p be FinSeqLen of n;

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

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

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

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

      

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

      

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

      

       A3: ( InputVertices S) = ( rng p) by CIRCCOMB: 42;

      

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

       A5:

      now

        let a be object;

        assume a in the carrier of S;

        then

        reconsider v = a as Vertex of S;

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

        then

         A6: ( dom (s * p)) = ( dom p) by A2, RELAT_1: 27, XBOOLE_1: 7;

        

         A7: ( dom (s1 * p)) = ( dom p) by A1, A2, RELAT_1: 27, XBOOLE_1: 7;

         A8:

        now

          let i be object;

          assume

           A9: i in ( dom p);

          then

           A10: (p . i) in ( rng p) by FUNCT_1: 3;

          ((s1 * p) . i) = (s1 . (p . i)) & ((s * p) . i) = (s . (p . i)) by A7, A6, A9, FUNCT_1: 12;

          hence ((s1 * p) . i) = ((s * p) . i) by A3, A10, CIRCUIT2:def 5;

        end;

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

        then (s2 . v) = (s1 . v) or v = [p, f] & (v = [p, f] implies ( action_at v) = v) & (s2 . v) = (( Den (( action_at v),( 1GateCircuit (p,f)))) . (( action_at v) depends_on_in s1)) & (s1 . v) = (( Den (( action_at v),( 1GateCircuit (p,f)))) . (( action_at v) depends_on_in s)) & (( action_at v) = [p, f] implies (( action_at v) depends_on_in s) = (s * p) & (( action_at v) depends_on_in s1) = (s1 * p)) by A3, A4, Th1, CIRCCOMB: 41, CIRCUIT2:def 5, TARSKI:def 1;

        hence (s2 . a) = (s1 . a) by A7, A6, A8, FUNCT_1: 2;

      end;

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

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

    end;

    theorem :: CIRCCMB2:3

    

     Th3: 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 stable holds for n be natural Number holds ( Following (s,n)) = 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 stable;

      let n be natural Number;

      

       A0: n is Nat by TARSKI: 1;

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

      

       A2: for n be Nat st P[n] holds P[(n + 1)] by A1, FACIRC_1: 12;

      

       A3: P[ 0 ] by FACIRC_1: 11;

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

      hence thesis by A0;

    end;

    theorem :: CIRCCMB2: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, n1,n2 be natural Number st ( Following (s,n1)) is stable & n1 <= n2 holds ( Following (s,n2)) = ( Following (s,n1))

    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, n1,n2 be natural Number such that

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

       A2: n1 <= n2;

      consider k be Nat such that

       A3: n2 = (n1 + k) by A2, NAT_1: 10;

      reconsider k as Nat;

      n1 is Nat & n2 is Nat by TARSKI: 1;

      then ( Following (s,n2)) = ( Following (( Following (s,n1)),k)) by A3, FACIRC_1: 13;

      hence thesis by A1, Th3;

    end;

    begin

    scheme :: CIRCCMB2:sch1

    CIRCCMB29sch1 { S0() -> non empty ManySortedSign , o0() -> object , S( object, object, object) -> non empty ManySortedSign , o( object, object) -> object } :

ex f,h be ManySortedSet of NAT st (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n);

      deffunc f( object, object) = [S(`1,`2,$1), o(`2,$1)];

      consider F be Function such that

       A1: ( dom F) = NAT & (F . 0 ) = [S0(), o0()] and

       A2: for n be Nat holds (F . (n + 1)) = f(n,.) from NAT_1:sch 11;

      deffunc h( object) = ((F . $1) `2 );

      deffunc f( object) = ((F . $1) `1 );

      consider f be ManySortedSet of NAT such that

       A3: for n be object st n in NAT holds (f . n) = f(n) from PBOOLE:sch 4;

      consider h be ManySortedSet of NAT such that

       A4: for n be object st n in NAT holds (h . n) = h(n) from PBOOLE:sch 4;

      take f, h;

      ((F . 0 ) `1 ) = S0() & ((F . 0 ) `2 ) = o0() by A1;

      hence (f . 0 ) = S0() & (h . 0 ) = o0() by A3, A4;

      let n be Nat, S be non empty ManySortedSign, x be set;

      set x = (F . n);

      

       A5: n in NAT by ORDINAL1:def 12;

      then

       A6: (h . n) = (x `2 ) by A4;

      assume S = (f . n);

      then S = (x `1 ) by A3, A5;

      then (F . (n + 1)) = [S(S,.,n), o(.,n)] by A2, A6;

      then ((F . (n + 1)) `1 ) = S(S,.,n) & ((F . (n + 1)) `2 ) = o(.,n);

      hence thesis by A3, A4;

    end;

    scheme :: CIRCCMB2:sch2

    CIRCCMB29sch2 { S( object, object, object) -> non empty ManySortedSign , o( object, object) -> object , P[ object, object, object], f,h() -> ManySortedSet of NAT } :

for n be Nat holds ex S be non empty ManySortedSign st S = (f() . n) & P[S, (h() . n), n]

      provided

       A1: ex S be non empty ManySortedSign, x be set st S = (f() . 0 ) & x = (h() . 0 ) & P[S, x, 0 ]

       and

       A2: for n be Nat, S be non empty ManySortedSign, x be set st S = (f() . n) & x = (h() . n) holds (f() . (n + 1)) = S(S,x,n) & (h() . (n + 1)) = o(x,n)

       and

       A3: for n be Nat, S be non empty ManySortedSign, x be set st S = (f() . n) & x = (h() . n) & P[S, x, n] holds P[S(S,x,n), o(x,n), (n + 1)];

      defpred Q[ Nat] means ex S be non empty ManySortedSign st S = (f() . $1) & P[S, (h() . $1), $1];

      

       A4: for n be Nat st Q[n] holds Q[(n + 1)]

      proof

        let n be Nat;

        given S be non empty ManySortedSign such that

         A5: S = (f() . n) and

         A6: P[S, (h() . n), n];

        take S(S,.,n);

        (h() . (n + 1)) = o(.,n) by A2, A5;

        hence thesis by A2, A3, A5, A6;

      end;

      

       A7: Q[ 0 ] by A1;

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

    end;

    defpred Pl[ object, object, object] means not contradiction;

    scheme :: CIRCCMB2:sch3

    CIRCCMB29sch3 { S0() -> non empty ManySortedSign , S( object, object, object) -> non empty ManySortedSign , o( object, object) -> object , f,h() -> ManySortedSet of NAT } :

for n be Nat, x be set st x = (h() . n) holds (h() . (n + 1)) = o(x,n)

      provided

       A1: (f() . 0 ) = S0()

       and

       A2: for n be Nat, S be non empty ManySortedSign, x be set st S = (f() . n) & x = (h() . n) holds (f() . (n + 1)) = S(S,x,n) & (h() . (n + 1)) = o(x,n);

      

       A3: ex S be non empty ManySortedSign, x be set st S = (f() . 0 ) & x = (h() . 0 ) & Pl[S, x, 0 ] by A1;

      let n be Nat, x be set;

      

       A4: for n be Nat, S be non empty ManySortedSign, x be set st S = (f() . n) & x = (h() . n) & Pl[S, x, n] holds Pl[S(S,x,n), o(x,n), (n + 1)];

      

       A5: for n be Nat, S be non empty ManySortedSign, x be set st S = (f() . n) & x = (h() . n) holds (f() . (n + 1)) = S(S,x,n) & (h() . (n + 1)) = o(x,n) by A2;

      for n be Nat holds ex S be non empty ManySortedSign st S = (f() . n) & Pl[S, (h() . n), n] from CIRCCMB29sch2( A3, A5, A4);

      then

       A6: ex S be non empty ManySortedSign st S = (f() . n);

      assume x = (h() . n);

      hence thesis by A2, A6;

    end;

    scheme :: CIRCCMB2:sch4

    CIRCCMB29sch4 { S0() -> non empty ManySortedSign , o0() -> object , S( object, object, object) -> non empty ManySortedSign , o( object, object) -> object , n() -> Nat } :

ex S be non empty ManySortedSign, f,h be ManySortedSet of NAT st S = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n);

      consider f,h be ManySortedSet of NAT such that

       A1: (f . 0 ) = S0() & (h . 0 ) = o0() and

       A2: for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n) from CIRCCMB29sch1;

      

       A3: for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) & Pl[S, x, n] holds Pl[S(S,x,n), o(x,n), (n + 1)];

      

       A4: ex S be non empty ManySortedSign, x be set st S = (f . 0 ) & x = (h . 0 ) & Pl[S, x, 0 ] by A1;

      for n be Nat holds ex S be non empty ManySortedSign st S = (f . n) & Pl[S, (h . n), n] from CIRCCMB29sch2( A4, A2, A3);

      then

      consider S be non empty ManySortedSign such that

       A5: S = (f . n());

      take S, f, h;

      thus thesis by A1, A2, A5;

    end;

    scheme :: CIRCCMB2:sch5

    CIRCCMB29sch5 { S0() -> non empty ManySortedSign , o0() -> object , S( object, object, object) -> non empty ManySortedSign , o( object, object) -> object , n() -> Nat } :

for S1,S2 be non empty ManySortedSign st (ex f,h be ManySortedSet of NAT st S1 = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) & (ex f,h be ManySortedSet of NAT st S2 = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) holds S1 = S2;

      let S1,S2 be non empty ManySortedSign;

      given f1,h1 be ManySortedSet of NAT such that

       A1: S1 = (f1 . n()) and

       A2: (f1 . 0 ) = S0() and

       A3: (h1 . 0 ) = o0() and

       A4: for n be Nat, S be non empty ManySortedSign, x be set st S = (f1 . n) & x = (h1 . n) holds (f1 . (n + 1)) = S(S,x,n) & (h1 . (n + 1)) = o(x,n);

      

       A5: for n be Nat, S be non empty ManySortedSign, x be set st S = (f1 . n) & x = (h1 . n) holds (f1 . (n + 1)) = S(S,x,n) & (h1 . (n + 1)) = o(x,n) by A4;

      

       A6: for n be Nat, S be non empty ManySortedSign, x be set st S = (f1 . n) & x = (h1 . n) & Pl[S, x, n] holds Pl[S(S,x,n), o(x,n), (n + 1)];

      

       A7: ex S be non empty ManySortedSign, x be set st S = (f1 . 0 ) & x = (h1 . 0 ) & Pl[S, x, 0 ] by A2;

      

       A8: for n be Nat holds ex S be non empty ManySortedSign st S = (f1 . n) & Pl[S, (h1 . n), n] from CIRCCMB29sch2( A7, A5, A6);

      given f2,h2 be ManySortedSet of NAT such that

       A9: S2 = (f2 . n()) and

       A10: (f2 . 0 ) = S0() and

       A11: (h2 . 0 ) = o0() and

       A12: for n be Nat, S be non empty ManySortedSign, x be set st S = (f2 . n) & x = (h2 . n) holds (f2 . (n + 1)) = S(S,x,n) & (h2 . (n + 1)) = o(x,n);

      

       A13: for n be Nat, S be non empty ManySortedSign, x be set st S = (f2 . n) & x = (h2 . n) holds (f2 . (n + 1)) = S(S,x,n) & (h2 . (n + 1)) = o(x,n) by A12;

      defpred A[ Nat] means (h1 . $1) = (h2 . $1);

      

       A14: for n be Nat, S be non empty ManySortedSign, x be set st S = (f2 . n) & x = (h2 . n) & Pl[S, x, n] holds Pl[S(S,x,n), o(x,n), (n + 1)];

      

       A15: ex S be non empty ManySortedSign, x be set st S = (f2 . 0 ) & x = (h2 . 0 ) & Pl[S, x, 0 ] by A10;

      

       A16: for n be Nat holds ex S be non empty ManySortedSign st S = (f2 . n) & Pl[S, (h2 . n), n] from CIRCCMB29sch2( A15, A13, A14);

       A17:

      now

        let n be Nat;

        assume

         A18: A[n];

        ex S be non empty ManySortedSign st S = (f1 . n) & Pl[S, (h1 . n), n] by A8;

        then

         A19: (h1 . (n + 1)) = o(.,n) by A4;

        ex S be non empty ManySortedSign st S = (f2 . n) & Pl[S, (h2 . n), n] by A16;

        hence A[(n + 1)] by A12, A18, A19;

      end;

      defpred B[ Nat] means (f1 . $1) = (f2 . $1);

      

       A20: A[ 0 ] by A3, A11;

      for i be Nat holds A[i] from NAT_1:sch 2( A20, A17);

      then for i be object st i in NAT holds (h1 . i) = (h2 . i);

      then

       A21: h1 = h2 by PBOOLE: 3;

       A22:

      now

        let n be Nat;

        assume

         A23: B[n];

        consider S be non empty ManySortedSign such that

         A24: S = (f1 . n) and Pl[S, (h1 . n), n] by A8;

        (f1 . (n + 1)) = S(S,.,n) by A4, A24

        .= (f2 . (n + 1)) by A12, A21, A23, A24;

        hence B[(n + 1)];

      end;

      

       A25: B[ 0 ] by A2, A10;

      for i be Nat holds B[i] from NAT_1:sch 2( A25, A22);

      hence thesis by A1, A9;

    end;

    scheme :: CIRCCMB2:sch6

    CIRCCMB29sch6 { S0() -> non empty ManySortedSign , o0() -> object , S( object, object, object) -> non empty ManySortedSign , o( object, object) -> object , n() -> Nat } :

(ex S be non empty ManySortedSign, f,h be ManySortedSet of NAT st S = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) & for S1,S2 be non empty ManySortedSign st (ex f,h be ManySortedSet of NAT st S1 = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) & (ex f,h be ManySortedSet of NAT st S2 = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) holds S1 = S2;

      thus ex S be non empty ManySortedSign, f,h be ManySortedSet of NAT st S = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n) from CIRCCMB29sch4;

      thus for S1,S2 be non empty ManySortedSign st (ex f,h be ManySortedSet of NAT st S1 = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) & (ex f,h be ManySortedSet of NAT st S2 = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) holds S1 = S2 from CIRCCMB29sch5;

    end;

    scheme :: CIRCCMB2:sch7

    CIRCCMB29sch7 { S0() -> non empty ManySortedSign , S( object, object, object) -> non empty ManySortedSign , o0() -> object , o( object, object) -> object , n() -> Nat } :

ex S be unsplit gate`1=arity gate`2isBoolean non void non empty non empty strict ManySortedSign, f,h be ManySortedSet of NAT st S = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)

      provided

       A1: S0() is unsplit gate`1=arity gate`2isBoolean non void non empty strict

       and

       A2: for S be unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, x be set, n be Nat holds S(S,x,n) is unsplit gate`1=arity gate`2isBoolean non void non empty strict;

      defpred P[ non empty ManySortedSign, object] means $1 is unsplit gate`1=arity gate`2isBoolean non void strict;

      defpred Pl[ non empty ManySortedSign, object, object] means P[$1, $2];

      consider S be non empty ManySortedSign, f,h be ManySortedSet of NAT such that

       A3: S = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() and

       A4: for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n) from CIRCCMB29sch4;

      

       A5: for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) & Pl[S, x, n] holds Pl[S(S,x,n), o(x,n), (n + 1)] by A2;

      

       A6: ex S be non empty ManySortedSign, x be set st S = (f . 0 ) & x = (h . 0 ) & Pl[S, x, 0 ] by A1, A3;

      for n be Nat holds ex S be non empty ManySortedSign st S = (f . n) & Pl[S, (h . n), n] from CIRCCMB29sch2( A6, A4, A5);

      then ex S be non empty ManySortedSign st S = (f . n()) & P[S, n()];

      then

      reconsider S as unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign by A3;

      take S, f, h;

      thus thesis by A3, A4;

    end;

    scheme :: CIRCCMB2:sch8

    CIRCCMB29sch8 { S0() -> non empty ManySortedSign , S( object, object) -> unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign , o0() -> object , o( object, object) -> object , n() -> Nat } :

ex S be unsplit gate`1=arity gate`2isBoolean non void non empty non empty strict ManySortedSign, f,h be ManySortedSet of NAT st S = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = (S +* S(x,n)) & (h . (n + 1)) = o(x,n)

      provided

       A1: S0() is unsplit gate`1=arity gate`2isBoolean non void non empty strict;

      deffunc Sl( non empty ManySortedSign, set, set) = ($1 +* S($2,$3));

      

       A2: for S be unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, x be set, n be Nat holds Sl(S,x,n) is unsplit gate`1=arity gate`2isBoolean non void non empty strict;

      thus ex S be unsplit gate`1=arity gate`2isBoolean non void non empty non empty strict ManySortedSign, f,h be ManySortedSet of NAT st S = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = Sl(S,x,n) & (h . (n + 1)) = o(x,n) from CIRCCMB29sch7( A1, A2);

    end;

    scheme :: CIRCCMB2:sch9

    CIRCCMB29sch9 { S0() -> non empty ManySortedSign , o0() -> object , S( object, object, object) -> non empty ManySortedSign , o( object, object) -> object , n() -> Nat } :

for S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty strict non empty ManySortedSign st (ex f,h be ManySortedSet of NAT st S1 = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) & (ex f,h be ManySortedSet of NAT st S2 = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) holds S1 = S2;

      for S1,S2 be non empty ManySortedSign st (ex f,h be ManySortedSet of NAT st S1 = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) & (ex f,h be ManySortedSet of NAT st S2 = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)) holds S1 = S2 from CIRCCMB29sch5;

      hence thesis;

    end;

    begin

    theorem :: CIRCCMB2:5

    

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

    proof

      let S1,S2 be non empty ManySortedSign;

      

       A1: (the carrier of S1 \ (( rng the ResultSort of S1) \/ ( rng the ResultSort of S2))) = (( InputVertices S1) \ ( InnerVertices S2)) by XBOOLE_1: 41;

      assume S1 tolerates S2;

      then

       A2: the ResultSort of S1 tolerates the ResultSort of S2 by CIRCCOMB:def 1;

      ( InputVertices (S1 +* S2)) = (the carrier of (S1 +* S2) \ ( rng (the ResultSort of S1 +* the ResultSort of S2))) by CIRCCOMB:def 2

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

      .= ((the carrier of S1 \/ the carrier of S2) \ (( rng the ResultSort of S1) \/ ( rng the ResultSort of S2))) by A2, FRECHET: 35

      .= ((the carrier of S1 \ (( rng the ResultSort of S1) \/ ( rng the ResultSort of S2))) \/ (the carrier of S2 \ (( rng the ResultSort of S1) \/ ( rng the ResultSort of S2)))) by XBOOLE_1: 42;

      hence thesis by A1, XBOOLE_1: 41;

    end;

    theorem :: CIRCCMB2:6

    

     Th6: for X be without_pairs set, Y be Relation holds (X \ Y) = X

    proof

      let X be without_pairs set;

      let Y be Relation;

      (X /\ Y) = {} ;

      then X misses Y by XBOOLE_0:def 7;

      hence thesis by XBOOLE_1: 83;

    end;

    theorem :: CIRCCMB2:7

    for X be Relation, Y,Z be set st Z c= Y & (Y \ Z) is without_pairs holds (X \ Y) = (X \ Z)

    proof

      let X be Relation;

      let Y,Z be set;

      assume

       A1: Z c= Y;

      assume (Y \ Z) is without_pairs;

      then not (ex x be object st x in (X /\ (Y \ Z)));

      then (X /\ (Y \ Z)) = {} by XBOOLE_0: 7;

      then X misses (Y \ Z) by XBOOLE_0:def 7;

      then

       A2: (X \ (Y \ Z)) = X by XBOOLE_1: 83;

      (X \ Y) = (X \ ((Y \ Z) \/ Z)) by A1, XBOOLE_1: 45

      .= (X \ Z) by A2, XBOOLE_1: 41;

      hence thesis;

    end;

    theorem :: CIRCCMB2:8

    

     Th8: for X,Z be set, Y be Relation st Z c= Y & (X \ Z) is without_pairs holds (X \ Y) = (X \ Z)

    proof

      let X,Z be set;

      let Y be Relation;

      assume

       A1: Z c= Y;

      assume (X \ Z) is without_pairs;

      then not (ex x be object st x in ((Y \ Z) /\ (X \ Z)));

      then ((Y \ Z) /\ (X \ Z)) = {} by XBOOLE_0: 7;

      then (Y \ Z) misses (X \ Z) by XBOOLE_0:def 7;

      then

       A2: ((X \ Z) \ (Y \ Z)) = (X \ Z) by XBOOLE_1: 83;

      (X \ Y) = (X \ ((Y \ Z) \/ Z)) by A1, XBOOLE_1: 45

      .= (X \ Z) by A2, XBOOLE_1: 41;

      hence thesis;

    end;

    scheme :: CIRCCMB2:sch10

    CIRCCMB29sch10 { S0() -> unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign , f( object) -> object , h() -> ManySortedSet of NAT , S( object, object) -> unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign , o( object, object) -> object } :

for n be Nat holds ex S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st S1 = f(n) & S2 = f(+) & ( InputVertices S2) = (( InputVertices S1) \/ (( InputVertices S(.,n)) \ {(h() . n)})) & ( InnerVertices S1) is Relation & ( InputVertices S1) is without_pairs

      provided

       A1: ( InnerVertices S0()) is Relation

       and

       A2: ( InputVertices S0()) is without_pairs

       and

       A3: f(0) = S0() & (h() . 0 ) in ( InnerVertices S0())

       and

       A4: for n be Nat, x be set holds ( InnerVertices S(x,n)) is Relation

       and

       A5: for n be Nat, x be set st x = (h() . n) holds (( InputVertices S(x,n)) \ {x}) is without_pairs

       and

       A6: for n be Nat, S be non empty ManySortedSign, x be set st S = f(n) & x = (h() . n) holds f(+) = (S +* S(x,n)) & (h() . (n + 1)) = o(x,n) & x in ( InputVertices S(x,n)) & o(x,n) in ( InnerVertices S(x,n));

      

       A7: ( InnerVertices S(.,0)) is Relation by A4;

      defpred P[ Nat] means ex S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st S1 = f($1) & S2 = f(+) & ( InputVertices S2) = (( InputVertices S1) \/ (( InputVertices S(.,$1)) \ {(h() . $1)})) & (h() . ($1 + 1)) in ( InnerVertices S2) & ( InputVertices S2) is without_pairs & ( InnerVertices S2) is Relation;

      

       A8: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat;

        given S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign such that S1 = f(i) and

         A9: S2 = f(+) and ( InputVertices S2) = (( InputVertices S1) \/ (( InputVertices S(.,i)) \ {(h() . i)})) and

         A10: (h() . (i + 1)) in ( InnerVertices S2) and

         A11: ( InputVertices S2) is without_pairs and

         A12: ( InnerVertices S2) is Relation;

        

         A13: {(h() . (i + 1))} c= ( InnerVertices S2) by A10, ZFMISC_1: 31;

        take S2, S3 = (S2 +* S(.,+));

        thus S2 = f(+) & S3 = f(+) by A6, A9;

        

         A14: (( InputVertices S(.,+)) \ {(h() . (i + 1))}) is without_pairs by A5;

        reconsider X1 = ( InputVertices S2), X2 = (( InputVertices S(.,+)) \ {(h() . (i + 1))}) as without_pairs set by A5, A11;

        

         A15: ( InnerVertices S(.,+)) is Relation by A4;

        

        thus ( InputVertices S3) = ((( InputVertices S2) \ ( InnerVertices S(.,+))) \/ (( InputVertices S(.,+)) \ ( InnerVertices S2))) by Th5, CIRCCOMB: 47

        .= (( InputVertices S2) \/ (( InputVertices S(.,+)) \ ( InnerVertices S2))) by A11, A15, Th6

        .= (( InputVertices S2) \/ (( InputVertices S(.,+)) \ {(h() . (i + 1))})) by A12, A14, A13, Th8;

        then

         A16: ( InputVertices S3) = (X1 \/ X2);

        

         A17: (h() . ((i + 1) + 1)) = o(.,+) & o(.,+) in ( InnerVertices S(.,+)) by A6, A9;

        reconsider X1 = ( InnerVertices S2), X2 = ( InnerVertices S(.,+)) as Relation by A4, A12;

        S2 tolerates S(.,+) by CIRCCOMB: 47;

        then ( InnerVertices S3) = (X1 \/ X2) by CIRCCOMB: 11;

        hence thesis by A17, A16, XBOOLE_0:def 3;

      end;

      let n be Nat;

      

       A18: S0() tolerates S(.,0) by CIRCCOMB: 47;

      

       A19: ( InputVertices (S0() +* S(.,0))) = ((( InputVertices S0()) \ ( InnerVertices S(.,0))) \/ (( InputVertices S(.,0)) \ ( InnerVertices S0()))) by Th5, CIRCCOMB: 47

      .= (( InputVertices S0()) \/ (( InputVertices S(.,0)) \ ( InnerVertices S0()))) by A2, A7, Th6;

      

       A20: P[ 0 ]

      proof

        reconsider A = (( InputVertices S(.,0)) \ {(h() . 0 )}), B = ( InputVertices S0()) as without_pairs set by A2, A5;

        take S0 = S0(), S1 = (S0() +* S(.,0));

        thus S0 = f(0) & S1 = f(+) by A3, A6;

        reconsider R1 = ( InnerVertices S0()), R2 = ( InnerVertices S(.,0)) as Relation by A1, A4;

        for x be object st x in {(h() . 0 )} holds x in ( InnerVertices S0()) by A3, TARSKI:def 1;

        then {(h() . 0 )} c= ( InnerVertices S0()) by TARSKI:def 3;

        then

         A21: ( InputVertices S1) = (B \/ A) by A1, A19, Th8;

        (h() . ( 0 + 1)) = o(.,0) & o(.,0) in R2 by A3, A6;

        then (h() . ( 0 + 1)) in (R1 \/ R2) by XBOOLE_0:def 3;

        hence thesis by A18, A21, CIRCCOMB: 11;

      end;

      

       A22: for i be Nat holds P[i] from NAT_1:sch 2( A20, A8);

      then

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

       A23: S1 = f(n) and

       A24: S2 = f(+) & ( InputVertices S2) = (( InputVertices S1) \/ (( InputVertices S(.,n)) \ {(h() . n)})) and (h() . (n + 1)) in ( InnerVertices S2) and ( InputVertices S2) is without_pairs and ( InnerVertices S2) is Relation;

      take S1, S2;

      thus S1 = f(n) & S2 = f(+) & ( InputVertices S2) = (( InputVertices S1) \/ (( InputVertices S(.,n)) \ {(h() . n)})) by A23, A24;

      per cases by NAT_1: 6;

        suppose n = 0 ;

        hence thesis by A1, A2, A3, A23;

      end;

        suppose ex i be Nat st n = (i + 1);

        then

        consider i be Nat such that

         A25: n = (i + 1);

        reconsider i as Nat;

        ex T1,T2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st T1 = f(i) & T2 = f(+) & ( InputVertices T2) = (( InputVertices T1) \/ (( InputVertices S(.,i)) \ {(h() . i)})) & (h() . (i + 1)) in ( InnerVertices T2) & ( InputVertices T2) is without_pairs & ( InnerVertices T2) is Relation by A22;

        hence thesis by A23, A25;

      end;

    end;

    scheme :: CIRCCMB2:sch11

    CIRCCMB29sch11 { Sn( set) -> unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign , h() -> ManySortedSet of NAT , S( object, object) -> unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign , o( object, object) -> object } :

for n be Nat holds ( InputVertices Sn(+)) = (( InputVertices Sn(n)) \/ (( InputVertices S(.,n)) \ {(h() . n)})) & ( InnerVertices Sn(n)) is Relation & ( InputVertices Sn(n)) is without_pairs

      provided

       A1: ( InnerVertices Sn(0)) is Relation

       and

       A2: ( InputVertices Sn(0)) is without_pairs

       and

       A3: (h() . 0 ) in ( InnerVertices Sn(0))

       and

       A4: for n be Nat, x be set holds ( InnerVertices S(x,n)) is Relation

       and

       A5: for n be Nat, x be set st x = (h() . n) holds (( InputVertices S(x,n)) \ {x}) is without_pairs

       and

       A6: for n be Nat, S be non empty ManySortedSign, x be set st S = Sn(n) & x = (h() . n) holds Sn(+) = (S +* S(x,n)) & (h() . (n + 1)) = o(x,n) & x in ( InputVertices S(x,n)) & o(x,n) in ( InnerVertices S(x,n));

      deffunc SN( set) = Sn($1);

      

       A7: for n be Nat, S be non empty ManySortedSign, x be set st S = SN(n) & x = (h() . n) holds SN(+) = (S +* S(x,n)) & (h() . (n + 1)) = o(x,n) & x in ( InputVertices S(x,n)) & o(x,n) in ( InnerVertices S(x,n)) by A6;

      let n be Nat;

      

       A8: for n be Nat, x be set st x = (h() . n) holds (( InputVertices S(x,n)) \ {x}) is without_pairs by A5;

      

       A9: SN(0) = SN(0) & (h() . 0 ) in ( InnerVertices SN(0)) by A3;

      

       A10: for n be Nat, x be set holds ( InnerVertices S(x,n)) is Relation by A4;

      for n be Nat holds ex S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st S1 = SN(n) & S2 = SN(+) & ( InputVertices S2) = (( InputVertices S1) \/ (( InputVertices S(.,n)) \ {(h() . n)})) & ( InnerVertices S1) is Relation & ( InputVertices S1) is without_pairs from CIRCCMB29sch10( A1, A2, A9, A10, A8, A7);

      then ex S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st S1 = Sn(n) & S2 = Sn(+) & ( InputVertices S2) = (( InputVertices S1) \/ (( InputVertices S(.,n)) \ {(h() . n)})) & ( InnerVertices S1) is Relation & ( InputVertices S1) is without_pairs;

      hence thesis;

    end;

    begin

    scheme :: CIRCCMB2:sch12

    CIRCCMB29sch12 { S0() -> non empty ManySortedSign , A0() -> non-empty MSAlgebra over S0() , o0() -> object , S( object, object, object) -> non empty ManySortedSign , A( object, object, object, object) -> object , o( object, object) -> object } :

ex f,g,h be ManySortedSet of NAT st (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n);

      deffunc F( set, set) = [ [S(`11,`2,$1), A(`11,`12,`2,$1)], o(`2,$1)];

      consider F be Function such that

       A1: ( dom F) = NAT & (F . 0 ) = [ [S0(), A0()], o0()] and

       A2: for n be Nat holds (F . (n + 1)) = F(n,.) from NAT_1:sch 11;

      

       A3: ((F . 0 ) `2 ) = o0() by A1;

      deffunc h( object) = ((F . $1) `2 );

      deffunc g( object) = ((F . $1) `12 );

      deffunc f( object) = ((F . $1) `11 );

      consider f be ManySortedSet of NAT such that

       A4: for n be object st n in NAT holds (f . n) = f(n) from PBOOLE:sch 4;

      consider h be ManySortedSet of NAT such that

       A5: for n be object st n in NAT holds (h . n) = h(n) from PBOOLE:sch 4;

      consider g be ManySortedSet of NAT such that

       A6: for n be object st n in NAT holds (g . n) = g(n) from PBOOLE:sch 4;

      take f, g, h;

      ((F . 0 ) `11 ) = S0() & ((F . 0 ) `12 ) = A0() by A1, MCART_1: 85;

      hence (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() by A4, A6, A5, A3;

      let n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set;

      set x = (F . n);

      

       A7: n in NAT by ORDINAL1:def 12;

      then

       A8: (h . n) = (x `2 ) by A5;

      assume that

       A9: S = (f . n) and

       A10: A = (g . n);

      

       A11: A = (x `12 ) by A6, A7, A10;

      S = (x `11 ) by A4, A7, A9;

      then

       A12: (F . (n + 1)) = [ [S(S,.,n), A(S,A,.,n)], o(.,n)] by A2, A11, A8;

      then

       A13: ((F . (n + 1)) `2 ) = o(.,n);

      ((F . (n + 1)) `11 ) = S(S,.,n) & ((F . (n + 1)) `12 ) = A(S,A,.,n) by A12, MCART_1: 85;

      hence thesis by A4, A6, A5, A13;

    end;

    scheme :: CIRCCMB2:sch13

    CIRCCMB29sch13 { S( set, set, set) -> non empty ManySortedSign , A( object, object, object, object) -> object , o( object, object) -> object , P[ object, object, object, object], f,g,h() -> ManySortedSet of NAT } :

for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f() . n) & A = (g() . n) & P[S, A, (h() . n), n]

      provided

       A1: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f() . 0 ) & A = (g() . 0 ) & x = (h() . 0 ) & P[S, A, x, 0 ]

       and

       A2: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f() . n) & A = (g() . n) & x = (h() . n) holds (f() . (n + 1)) = S(S,x,n) & (g() . (n + 1)) = A(S,A,x,n) & (h() . (n + 1)) = o(x,n)

       and

       A3: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f() . n) & A = (g() . n) & x = (h() . n) & P[S, A, x, n] holds P[S(S,x,n), A(S,A,x,n), o(x,n), (n + 1)]

       and

       A4: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);

      defpred Q[ Nat] means ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f() . $1) & A = (g() . $1) & x = (h() . $1) & P[S, A, x, $1];

      

       A5: for n be Nat st Q[n] holds Q[(n + 1)]

      proof

        let n be Nat;

        given S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set such that

         A6: S = (f() . n) & A = (g() . n) & x = (h() . n) and

         A7: P[S, A, x, n];

        take S9 = S(S,x,n);

        reconsider A9 = A(S,A,x,n) as non-empty MSAlgebra over S9 by A4;

        take A9, y = (h() . (n + 1));

        y = o(x,n) by A2, A6;

        hence thesis by A2, A3, A6, A7;

      end;

      let n be Nat;

      

       A8: Q[ 0 ] by A1;

      for n be Nat holds Q[n] from NAT_1:sch 2( A8, A5);

      then

      consider S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set such that

       A9: S = (f() . n) & A = (g() . n) & x = (h() . n) & P[S, A, x, n];

      take S, A;

      thus thesis by A9;

    end;

    defpred R[ object, object, object, object] means not contradiction;

    scheme :: CIRCCMB2:sch14

    CIRCCMB29sch14 { S( set, set, set) -> non empty ManySortedSign , A( object, object, object, object) -> object , o( object, object) -> object , f1,f2,g1,g2,h1,h2() -> ManySortedSet of NAT } :

f1() = f2() & g1() = g2() & h1() = h2()

      provided

       A1: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f1() . 0 ) & A = (g1() . 0 )

       and

       A2: (f1() . 0 ) = (f2() . 0 ) & (g1() . 0 ) = (g2() . 0 ) & (h1() . 0 ) = (h2() . 0 )

       and

       A3: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f1() . n) & A = (g1() . n) & x = (h1() . n) holds (f1() . (n + 1)) = S(S,x,n) & (g1() . (n + 1)) = A(S,A,x,n) & (h1() . (n + 1)) = o(x,n)

       and

       A4: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f2() . n) & A = (g2() . n) & x = (h2() . n) holds (f2() . (n + 1)) = S(S,x,n) & (g2() . (n + 1)) = A(S,A,x,n) & (h2() . (n + 1)) = o(x,n)

       and

       A5: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);

      

       A6: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f1() . n) & A = (g1() . n) & x = (h1() . n) holds (f1() . (n + 1)) = S(S,x,n) & (g1() . (n + 1)) = A(S,A,x,n) & (h1() . (n + 1)) = o(x,n) by A3;

      set f1 = f1(), g1 = g1(), h1 = h1();

      

       A7: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f1 . n) & A = (g1 . n) & x = (h1 . n) & R[S, A, x, n] holds R[S(S,x,n), A(S,A,x,n), o(x,n), (n + 1)];

      

       A8: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n) by A5;

      

       A9: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f1 . 0 ) & A = (g1 . 0 ) & x = (h1 . 0 ) & R[S, A, x, 0 ] by A1;

      

       A10: for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f1 . n) & A = (g1 . n) & R[S, A, (h1 . n), n] from CIRCCMB29sch13( A9, A6, A7, A8);

      set f2 = f2(), g2 = g2(), h2 = h2();

      

       A11: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f2 . n) & A = (g2 . n) & x = (h2 . n) & R[S, A, x, n] holds R[S(S,x,n), A(S,A,x,n), o(x,n), (n + 1)];

      defpred P[ Nat] means (h1 . $1) = (h2 . $1);

      

       A12: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f2() . n) & A = (g2() . n) & x = (h2() . n) holds (f2() . (n + 1)) = S(S,x,n) & (g2() . (n + 1)) = A(S,A,x,n) & (h2() . (n + 1)) = o(x,n) by A4;

      

       A13: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f2 . 0 ) & A = (g2 . 0 ) & x = (h2 . 0 ) & R[S, A, x, 0 ] by A1, A2;

      

       A14: for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f2 . n) & A = (g2 . n) & R[S, A, (h2 . n), n] from CIRCCMB29sch13( A13, A12, A11, A8);

       A15:

      now

        let n be Nat;

        assume

         A16: P[n];

        ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f1 . n) & A = (g1 . n) by A10;

        then

         A17: (h1 . (n + 1)) = o(.,n) by A3;

        ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f2 . n) & A = (g2 . n) by A14;

        hence P[(n + 1)] by A4, A16, A17;

      end;

      

       A18: P[ 0 ] by A2;

      for i be Nat holds P[i] from NAT_1:sch 2( A18, A15);

      then

       A19: for i be object st i in NAT holds (h1 . i) = (h2 . i);

      defpred P[ Nat] means (f1 . $1) = (f2 . $1) & (g1 . $1) = (g2 . $1);

      

       A20: h1 = h2 by A19, PBOOLE: 3;

       A21:

      now

        let n be Nat;

        assume

         A22: P[n];

        consider S be non empty ManySortedSign, A be non-empty MSAlgebra over S such that

         A23: S = (f1 . n) & A = (g1 . n) by A10;

        

         A24: (g1 . (n + 1)) = A(S,A,.,n) by A3, A23

        .= (g2 . (n + 1)) by A4, A20, A22, A23;

        (f1 . (n + 1)) = S(S,.,n) by A3, A23

        .= (f2 . (n + 1)) by A4, A20, A22, A23;

        hence P[(n + 1)] by A24;

      end;

      

       A25: P[ 0 ] by A2;

      for i be Nat holds P[i] from NAT_1:sch 2( A25, A21);

      then (for i be object st i in NAT holds (f1 . i) = (f2 . i)) & for i be object st i in NAT holds (g1 . i) = (g2 . i);

      hence thesis by A19, PBOOLE: 3;

    end;

    scheme :: CIRCCMB2:sch15

    CIRCCMB29sch15 { S0() -> non empty ManySortedSign , A0() -> non-empty MSAlgebra over S0() , S( object, object, object) -> non empty ManySortedSign , A( object, object, object, object) -> object , o( object, object) -> object , f,g,h() -> ManySortedSet of NAT } :

for n be Nat, S be non empty ManySortedSign, x be set st S = (f() . n) & x = (h() . n) holds (f() . (n + 1)) = S(S,x,n) & (h() . (n + 1)) = o(x,n)

      provided

       A1: (f() . 0 ) = S0() & (g() . 0 ) = A0()

       and

       A2: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f() . n) & A = (g() . n) & x = (h() . n) holds (f() . (n + 1)) = S(S,x,n) & (g() . (n + 1)) = A(S,A,x,n) & (h() . (n + 1)) = o(x,n)

       and

       A3: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);

      

       A4: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f() . 0 ) & A = (g() . 0 ) & x = (h() . 0 ) & R[S, A, x, 0 ] by A1;

      let n be Nat, S be non empty ManySortedSign, x be set;

      

       A5: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f() . n) & A = (g() . n) & x = (h() . n) & R[S, A, x, n] holds R[S(S,x,n), A(S,A,x,n), o(x,n), (n + 1)];

      

       A6: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n) by A3;

      

       A7: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f() . n) & A = (g() . n) & x = (h() . n) holds (f() . (n + 1)) = S(S,x,n) & (g() . (n + 1)) = A(S,A,x,n) & (h() . (n + 1)) = o(x,n) by A2;

      for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f() . n) & A = (g() . n) & R[S, A, (h() . n), n] from CIRCCMB29sch13( A4, A7, A5, A6);

      then

       A8: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f() . n) & A = (g() . n);

      assume S = (f() . n) & x = (h() . n);

      hence thesis by A2, A8;

    end;

    scheme :: CIRCCMB2:sch16

    CIRCCMB29sch16 { S0() -> non empty ManySortedSign , A0() -> non-empty MSAlgebra over S0() , o0() -> object , S( object, object, object) -> non empty ManySortedSign , A( object, object, object, object) -> object , o( object, object) -> object , n() -> Nat } :

ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, f,g,h be ManySortedSet of NAT st S = (f . n()) & A = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n)

      provided

       A1: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);

      

       A2: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n) by A1;

      consider f,g,h be ManySortedSet of NAT such that

       A3: (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() and

       A4: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n) from CIRCCMB29sch12;

      

       A5: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) & R[S, A, x, n] holds R[S(S,x,n), A(S,A,x,n), o(x,n), (n + 1)];

      

       A6: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f . 0 ) & A = (g . 0 ) & x = (h . 0 ) & R[S, A, x, 0 ] by A3;

      for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n) & A = (g . n) & R[S, A, (h . n), n] from CIRCCMB29sch13( A6, A4, A5, A2);

      then

      consider S be non empty ManySortedSign, A be non-empty MSAlgebra over S such that

       A7: S = (f . n()) & A = (g . n());

      take S, A, f, g, h;

      thus thesis by A3, A4, A7;

    end;

    scheme :: CIRCCMB2:sch17

    CIRCCMB29sch17 { S0,Sn() -> non empty ManySortedSign , A0() -> non-empty MSAlgebra over S0() , o0() -> object , S( object, object, object) -> non empty ManySortedSign , A( object, object, object, object) -> object , o( object, object) -> object , n() -> Nat } :

ex A be non-empty MSAlgebra over Sn(), f,g,h be ManySortedSet of NAT st Sn() = (f . n()) & A = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n)

      provided

       A1: ex f,h be ManySortedSet of NAT st Sn() = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)

       and

       A2: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);

      

       A3: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n) by A2;

      consider f,g,h be ManySortedSet of NAT such that

       A4: (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() and

       A5: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n) from CIRCCMB29sch12;

      

       A6: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) & R[S, A, x, n] holds R[S(S,x,n), A(S,A,x,n), o(x,n), (n + 1)];

      

       A7: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) & R[S, A, x, n] holds R[S(S,x,n), A(S,A,x,n), o(x,n), (n + 1)];

      

       A8: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f . 0 ) & A = (g . 0 ) & x = (h . 0 ) & R[S, A, x, 0 ] by A4;

      

       A9: for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n) & A = (g . n) & R[S, A, (h . n), n] from CIRCCMB29sch13( A8, A5, A7, A3);

      

       A10: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f . 0 ) & A = (g . 0 ) & x = (h . 0 ) & R[S, A, x, 0 ] by A4;

      for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n) & A = (g . n) & R[S, A, (h . n), n] from CIRCCMB29sch13( A10, A5, A6, A3);

      then

      consider S be non empty ManySortedSign, A be non-empty MSAlgebra over S such that

       A11: S = (f . n()) and

       A12: A = (g . n());

      consider f1,h1 be ManySortedSet of NAT such that

       A13: Sn() = (f1 . n()) and

       A14: (f1 . 0 ) = S0() and

       A15: (h1 . 0 ) = o0() and

       A16: for n be Nat, S be non empty ManySortedSign, x be set st S = (f1 . n) & x = (h1 . n) holds (f1 . (n + 1)) = S(S,x,n) & (h1 . (n + 1)) = o(x,n) by A1;

      

       A17: for n be Nat, S be non empty ManySortedSign, x be set st S = (f1 . n) & x = (h1 . n) & Pl[S, x, n] holds Pl[S(S,x,n), o(x,n), (n + 1)];

      defpred P[ Nat] means (h1 . $1) = (h . $1);

      

       A18: ex S be non empty ManySortedSign, x be set st S = (f1 . 0 ) & x = (h1 . 0 ) & Pl[S, x, 0 ] by A14;

      

       A19: for n be Nat holds ex S be non empty ManySortedSign st S = (f1 . n) & Pl[S, (h1 . n), n] from CIRCCMB29sch2( A18, A16, A17);

       A20:

      now

        let n be Nat;

        assume

         A21: P[n];

        ex S be non empty ManySortedSign st S = (f1 . n) by A19;

        then

         A22: (h1 . (n + 1)) = o(.,n) by A16;

        ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n) & A = (g . n) by A9;

        hence P[(n + 1)] by A5, A21, A22;

      end;

      

       A23: P[ 0 ] by A4, A15;

      

       A24: for i be Nat holds P[i] from NAT_1:sch 2( A23, A20);

      defpred P[ Nat] means (f1 . $1) = (f . $1);

      for i be object st i in NAT holds (h1 . i) = (h . i) by A24;

      then

       A25: h1 = h by PBOOLE: 3;

       A26:

      now

        let n be Nat;

        consider S be non empty ManySortedSign, A be non-empty MSAlgebra over S such that

         A27: S = (f . n) and

         A28: A = (g . n) by A9;

        assume P[n];

        

        then (f1 . (n + 1)) = S(S,.,n) by A16, A27

        .= (f . (n + 1)) by A5, A25, A27, A28;

        hence P[(n + 1)];

      end;

      

       A29: P[ 0 ] by A4, A14;

      

       A30: for i be Nat holds P[i] from NAT_1:sch 2( A29, A26);

      then for i be object st i in NAT holds (f1 . i) = (f . i);

      then f1 = f by PBOOLE: 3;

      then

      reconsider A as non-empty MSAlgebra over Sn() by A13, A11;

      take A, f, g, h;

      thus thesis by A4, A5, A13, A30, A12;

    end;

    scheme :: CIRCCMB2:sch18

    CIRCCMB29sch18 { S0,Sn() -> non empty ManySortedSign , A0() -> non-empty MSAlgebra over S0() , o0() -> object , S( object, object, object) -> non empty ManySortedSign , A( object, object, object, object) -> object , o( object, object) -> object , n() -> Nat } :

for A1,A2 be non-empty MSAlgebra over Sn() st (ex f,g,h be ManySortedSet of NAT st Sn() = (f . n()) & A1 = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n)) & (ex f,g,h be ManySortedSet of NAT st Sn() = (f . n()) & A2 = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n)) holds A1 = A2

      provided

       A1: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);

      

       A2: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n) by A1;

      let A1,A2 be non-empty MSAlgebra over Sn();

      given f1,g1,h1 be ManySortedSet of NAT such that Sn() = (f1 . n()) and

       A3: A1 = (g1 . n()) and

       A4: (f1 . 0 ) = S0() & (g1 . 0 ) = A0() and

       A5: (h1 . 0 ) = o0() and

       A6: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f1 . n) & A = (g1 . n) & x = (h1 . n) holds (f1 . (n + 1)) = S(S,x,n) & (g1 . (n + 1)) = A(S,A,x,n) & (h1 . (n + 1)) = o(x,n);

      

       A7: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f1 . 0 ) & A = (g1 . 0 ) by A4;

      given f2,g2,h2 be ManySortedSet of NAT such that Sn() = (f2 . n()) and

       A8: A2 = (g2 . n()) and

       A9: (f2 . 0 ) = S0() & (g2 . 0 ) = A0() & (h2 . 0 ) = o0() and

       A10: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f2 . n) & A = (g2 . n) & x = (h2 . n) holds (f2 . (n + 1)) = S(S,x,n) & (g2 . (n + 1)) = A(S,A,x,n) & (h2 . (n + 1)) = o(x,n);

      

       A11: (f1 . 0 ) = (f2 . 0 ) & (g1 . 0 ) = (g2 . 0 ) & (h1 . 0 ) = (h2 . 0 ) by A4, A5, A9;

      f1 = f2 & g1 = g2 & h1 = h2 from CIRCCMB29sch14( A7, A11, A6, A10, A2);

      hence thesis by A3, A8;

    end;

    scheme :: CIRCCMB2:sch19

    CIRCCMB29sch19 { S0,Sn() -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign , A0() -> Boolean gate`2=den strict Circuit of S0() , S( object, object, object) -> non empty ManySortedSign , A( object, object, object, object) -> object , o0() -> object , o( object, object) -> object , n() -> Nat } :

ex A be Boolean gate`2=den strict Circuit of Sn(), f,g,h be ManySortedSet of NAT st Sn() = (f . n()) & A = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n)

      provided

       A1: for S be unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, x be set, n be Nat holds S(S,x,n) is unsplit gate`1=arity gate`2isBoolean non void strict

       and

       A2: ex f,h be ManySortedSet of NAT st Sn() = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (h . (n + 1)) = o(x,n)

       and

       A3: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n)

       and

       A4: for S,S1 be unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, A be Boolean gate`2=den strict Circuit of S holds for x be set, n be Nat st S1 = S(S,x,n) holds A(S,A,x,n) is Boolean gate`2=den strict Circuit of S1;

      

       A5: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n) by A3;

      defpred P[ object, object, Nat] means ex S be unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, A be Boolean gate`2=den strict Circuit of S st S = $1 & A = $2;

      consider f,g,h be ManySortedSet of NAT such that

       A6: (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() and

       A7: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n) from CIRCCMB29sch12;

      

       A8: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) & R[S, A, x, n] holds R[S(S,x,n), A(S,A,x,n), o(x,n), (n + 1)];

      

       A9: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f . 0 ) & A = (g . 0 ) & x = (h . 0 ) & R[S, A, x, 0 ] by A6;

      

       A10: for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n) & A = (g . n) & R[S, A, (h . n), n] from CIRCCMB29sch13( A9, A7, A8, A5);

      defpred R[ object, object, object, Nat] means P[$1, $2, $4];

      

       A11: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) & R[S, A, x, n] holds R[S(S,x,n), A(S,A,x,n), o(x,n), (n + 1)]

      proof

        let n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S;

        let x be set;

        assume that S = (f . n) and A = (g . n) and x = (h . n) and

         A12: P[S, A, n];

        reconsider S as unsplit gate`1=arity gate`2isBoolean non void non empty strict non empty ManySortedSign by A12;

        reconsider A as Boolean gate`2=den strict Circuit of S by A12;

        reconsider S1 = S(S,x,n) as unsplit gate`1=arity gate`2isBoolean non void non empty strict non empty ManySortedSign by A1;

        A(S,A,x,n) is Boolean gate`2=den strict Circuit of S1 by A4;

        hence thesis;

      end;

      

       A13: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f . 0 ) & A = (g . 0 ) & x = (h . 0 ) & R[S, A, x, 0 ] by A6;

      for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n) & A = (g . n) & R[S, A, (h . n), n] from CIRCCMB29sch13( A13, A7, A11, A5);

      then

      consider S be non empty ManySortedSign, A be non-empty MSAlgebra over S such that

       A14: S = (f . n()) and

       A15: A = (g . n()) and

       A16: P[S, A, n()];

      consider f1,h1 be ManySortedSet of NAT such that

       A17: Sn() = (f1 . n()) and

       A18: (f1 . 0 ) = S0() and

       A19: (h1 . 0 ) = o0() and

       A20: for n be Nat, S be non empty ManySortedSign, x be set st S = (f1 . n) & x = (h1 . n) holds (f1 . (n + 1)) = S(S,x,n) & (h1 . (n + 1)) = o(x,n) by A2;

      

       A21: for n be Nat, S be non empty ManySortedSign, x be set st S = (f1 . n) & x = (h1 . n) & Pl[S, x, n] holds Pl[S(S,x,n), o(x,n), (n + 1)];

      defpred P[ Nat] means (h1 . $1) = (h . $1);

      

       A22: ex S be non empty ManySortedSign, x be set st S = (f1 . 0 ) & x = (h1 . 0 ) & Pl[S, x, 0 ] by A18;

      

       A23: for n be Nat holds ex S be non empty ManySortedSign st S = (f1 . n) & Pl[S, (h1 . n), n] from CIRCCMB29sch2( A22, A20, A21);

       A24:

      now

        let n be Nat;

        assume

         A25: P[n];

        ex S be non empty ManySortedSign st S = (f1 . n) by A23;

        then

         A26: (h1 . (n + 1)) = o(.,n) by A20;

        ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n) & A = (g . n) by A10;

        hence P[(n + 1)] by A7, A25, A26;

      end;

      

       A27: P[ 0 ] by A6, A19;

      

       A28: for i be Nat holds P[i] from NAT_1:sch 2( A27, A24);

      defpred P[ Nat] means (f1 . $1) = (f . $1);

      for i be object st i in NAT holds (h1 . i) = (h . i) by A28;

      then

       A29: h1 = h by PBOOLE: 3;

       A30:

      now

        let n be Nat;

        consider S be non empty ManySortedSign, A be non-empty MSAlgebra over S such that

         A31: S = (f . n) and

         A32: A = (g . n) by A10;

        assume P[n];

        

        then (f1 . (n + 1)) = S(S,.,n) by A20, A31

        .= (f . (n + 1)) by A7, A29, A31, A32;

        hence P[(n + 1)];

      end;

      

       A33: P[ 0 ] by A6, A18;

      

       A34: for i be Nat holds P[i] from NAT_1:sch 2( A33, A30);

      then for i be object st i in NAT holds (f1 . i) = (f . i);

      then f1 = f by PBOOLE: 3;

      then

      reconsider A as Boolean gate`2=den strict Circuit of Sn() by A17, A14, A16;

      take A, f, g, h;

      thus thesis by A6, A7, A17, A34, A15;

    end;

    definition

      let S be non empty ManySortedSign;

      let A be object;

      :: CIRCCMB2:def1

      func MSAlg (A,S) -> non-empty MSAlgebra over S means

      : Def1: it = A;

      existence by A1;

      uniqueness ;

    end

    scheme :: CIRCCMB2:sch20

    CIRCCMB29sch20 { S0,Sn() -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign , A0() -> Boolean gate`2=den strict Circuit of S0() , S( object, object) -> unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign , A( object, object) -> object , o0() -> object , o( object, object) -> object , n() -> Nat } :

ex A be Boolean gate`2=den strict Circuit of Sn(), f,g,h be ManySortedSet of NAT st Sn() = (f . n()) & A = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A1 be non-empty MSAlgebra over S holds for x be set, A2 be non-empty MSAlgebra over S(x,n) st S = (f . n) & A1 = (g . n) & x = (h . n) & A2 = A(x,n) holds (f . (n + 1)) = (S +* S(x,n)) & (g . (n + 1)) = (A1 +* A2) & (h . (n + 1)) = o(x,n)

      provided

       A1: ex f,h be ManySortedSet of NAT st Sn() = (f . n()) & (f . 0 ) = S0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h . n) holds (f . (n + 1)) = (S +* S(x,n)) & (h . (n + 1)) = o(x,n)

       and

       A2: for x be set, n be Nat holds A(x,n) is Boolean gate`2=den strict Circuit of S(x,n);

      deffunc Sl( non empty ManySortedSign, set, set) = ($1 +* S($2,$3));

      consider f1,h1 be ManySortedSet of NAT such that

       A3: Sn() = (f1 . n()) and

       A4: (f1 . 0 ) = S0() and

       A5: (h1 . 0 ) = o0() and

       A6: for n be Nat, S be non empty ManySortedSign, x be set st S = (f1 . n) & x = (h1 . n) holds (f1 . (n + 1)) = Sl(S,x,n) & (h1 . (n + 1)) = o(x,n) by A1;

      defpred P[ object, object, Nat] means $3 <> 0 implies ex S be unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, A be Boolean gate`2=den strict Circuit of S st S = $1 & A = $2;

      deffunc Al( non empty ManySortedSign, non-empty MSAlgebra over $1, set, set) = ($2 +* ( MSAlg (A($3,$4),S($3,$4))));

      

       A7: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds Al(S,A,x,n) is non-empty MSAlgebra over Sl(S,x,n);

      

       A8: for n be Nat, S be non empty ManySortedSign, x be set st S = (f1 . n) & x = (h1 . n) & Pl[S, x, n] holds Pl[ Sl(S,x,n), o(x,n), (n + 1)];

      consider f,g,h be ManySortedSet of NAT such that

       A9: (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() and

       A10: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = Sl(S,x,n) & (g . (n + 1)) = Al(S,A,x,n) & (h . (n + 1)) = o(x,n) from CIRCCMB29sch12;

      

       A11: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) & R[S, A, x, n] holds R[ Sl(S,x,n), Al(S,A,x,n), o(x,n), (n + 1)];

      

       A12: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f . 0 ) & A = (g . 0 ) & x = (h . 0 ) & R[S, A, x, 0 ] by A9;

      

       A13: for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n) & A = (g . n) & R[S, A, (h . n), n] from CIRCCMB29sch13( A12, A10, A11, A7);

      defpred P[ Nat] means (h1 . $1) = (h . $1);

      

       A14: ex S be non empty ManySortedSign, x be set st S = (f1 . 0 ) & x = (h1 . 0 ) & Pl[S, x, 0 ] by A4;

      

       A15: for n be Nat holds ex S be non empty ManySortedSign st S = (f1 . n) & Pl[S, (h1 . n), n] from CIRCCMB29sch2( A14, A6, A8);

       A16:

      now

        let n be Nat;

        assume

         A17: P[n];

        ex S be non empty ManySortedSign st S = (f1 . n) by A15;

        then

         A18: (h1 . (n + 1)) = o(.,n) by A6;

        ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n) & A = (g . n) by A13;

        hence P[(n + 1)] by A10, A17, A18;

      end;

      

       A19: P[ 0 ] by A9, A5;

      

       A20: for i be Nat holds P[i] from NAT_1:sch 2( A19, A16);

      defpred P[ Nat] means (f1 . $1) = (f . $1);

      for i be object st i in NAT holds (h1 . i) = (h . i) by A20;

      then

       A21: h1 = h by PBOOLE: 3;

       A22:

      now

        let n be Nat;

        consider S be non empty ManySortedSign, A be non-empty MSAlgebra over S such that

         A23: S = (f . n) and

         A24: A = (g . n) by A13;

        assume P[n];

        

        then (f1 . (n + 1)) = (S +* S(.,n)) by A6, A23

        .= (f . (n + 1)) by A10, A21, A23, A24;

        hence P[(n + 1)];

      end;

      defpred R[ object, object, object, Nat] means P[$1, $2, $4];

      

       A25: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) & R[S, A, x, n] holds R[ Sl(S,x,n), Al(S,A,x,n), o(x,n), (n + 1)]

      proof

        let n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S;

        let x be set;

        assume that

         A26: S = (f . n) & A = (g . n) and x = (h . n) and

         A27: P[S, A, n] and (n + 1) <> 0 ;

        per cases ;

          suppose

           A28: n = 0 ;

          reconsider A2 = A(x,0) as Boolean gate`2=den strict Circuit of S(x,0) by A2;

          (A0() +* ( MSAlg (A(x,0),S(x,0)))) = (A0() +* A2) by Def1;

          hence thesis by A9, A26, A28;

        end;

          suppose

           A29: n <> 0 ;

          then

          reconsider S as unsplit gate`1=arity gate`2isBoolean non void non empty strict non empty ManySortedSign by A27;

          reconsider A as Boolean gate`2=den strict Circuit of S by A27, A29;

          reconsider A9 = A(x,n) as Boolean gate`2=den strict Circuit of S(x,n) by A2;

          (A +* ( MSAlg (A(x,n),S(x,n)))) = (A +* A9) by Def1;

          hence thesis;

        end;

      end;

      

       A30: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f . 0 ) & A = (g . 0 ) & x = (h . 0 ) & R[S, A, x, 0 ] by A9;

      for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n) & A = (g . n) & R[S, A, (h . n), n] from CIRCCMB29sch13( A30, A10, A25, A7);

      then

      consider S be non empty ManySortedSign, A be non-empty MSAlgebra over S such that

       A31: S = (f . n()) and

       A32: A = (g . n()) and

       A33: P[S, A, n()];

      

       A34: P[ 0 ] by A9, A4;

      

       A35: for i be Nat holds P[i] from NAT_1:sch 2( A34, A22);

      then for i be object st i in NAT holds (f1 . i) = (f . i);

      then f1 = f by PBOOLE: 3;

      then

      reconsider A as Boolean gate`2=den strict Circuit of Sn() by A9, A3, A31, A32, A33;

      take A, f, g, h;

      thus Sn() = (f . n()) & A = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() by A9, A3, A35, A32;

      let n be Nat, S be non empty ManySortedSign, A1 be non-empty MSAlgebra over S;

      let x be set, A2 be non-empty MSAlgebra over S(x,n);

      assume

       A36: S = (f . n) & A1 = (g . n) & x = (h . n) & A2 = A(x,n);

      A2 = ( MSAlg (A2,S(x,n))) by Def1;

      hence thesis by A10, A36;

    end;

    scheme :: CIRCCMB2:sch21

    CIRCCMB29sch21 { S0() -> non empty ManySortedSign , Sn() -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign , A0() -> non-empty MSAlgebra over S0() , o0() -> object , S( object, object, object) -> non empty ManySortedSign , A( object, object, object, object) -> object , o( object, object) -> object , n() -> Nat } :

for A1,A2 be Boolean gate`2=den strict Circuit of Sn() st (ex f,g,h be ManySortedSet of NAT st Sn() = (f . n()) & A1 = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n)) & (ex f,g,h be ManySortedSet of NAT st Sn() = (f . n()) & A2 = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n)) holds A1 = A2

      provided

       A1: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n);

      

       A2: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x,n) by A1;

      for A1,A2 be non-empty MSAlgebra over Sn() st (ex f,g,h be ManySortedSet of NAT st Sn() = (f . n()) & A1 = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n)) & (ex f,g,h be ManySortedSet of NAT st Sn() = (f . n()) & A2 = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h . n) holds (f . (n + 1)) = S(S,x,n) & (g . (n + 1)) = A(S,A,x,n) & (h . (n + 1)) = o(x,n)) holds A1 = A2 from CIRCCMB29sch18( A2);

      hence thesis;

    end;

    begin

    theorem :: CIRCCMB2:9

    for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InnerVertices S1) misses ( InputVertices S2) & S = (S1 +* S2) holds for C1 be non-empty Circuit of S1, C2 be non-empty Circuit of S2 holds for C be non-empty Circuit of S st C1 tolerates C2 & C = (C1 +* C2) holds for s2 be State of C2 holds for s be State of C st s2 = (s | the carrier of S2) holds ( Following s2) = (( Following s) | the carrier of S2)

    proof

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

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

      let C1 be non-empty Circuit of S1;

      let C2 be non-empty Circuit of S2;

      let C be non-empty Circuit of S such that

       A2: C1 tolerates C2 and

       A3: C = (C1 +* C2);

      let s2 be State of C2;

      let s be State of C such that

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

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

      then

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

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

      hence thesis by FUNCT_4: 23;

    end;

    theorem :: CIRCCMB2:10

    

     Th10: for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) misses ( InnerVertices S2) & S = (S1 +* S2) holds for C1 be non-empty Circuit of S1, C2 be non-empty Circuit of S2 holds for C be non-empty Circuit of S st C1 tolerates C2 & C = (C1 +* C2) holds for s1 be State of C1 holds for s be State of C st s1 = (s | the carrier of S1) holds ( Following s1) = (( Following s) | the carrier of 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 C1 be non-empty Circuit of S1;

      let C2 be non-empty Circuit of S2;

      let C be non-empty Circuit of S such that

       A2: C1 tolerates C2 and

       A3: C = (C1 +* C2);

      let s1 be State of C1;

      let s be State of C such that

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

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

      then

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

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

      hence thesis by FUNCT_4: 23;

    end;

    theorem :: CIRCCMB2:11

    for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InnerVertices S1) misses ( InputVertices S2) & S = (S1 +* S2) holds for C1 be non-empty Circuit of S1, C2 be non-empty Circuit of S2 holds for C be non-empty Circuit of S st C1 tolerates C2 & C = (C1 +* C2) holds for s1 be State of C1 holds for s2 be State of C2 holds for s be State of C st s1 = (s | the carrier of S1) & s2 = (s | the carrier of S2) & s1 is stable & s2 is stable holds s is stable

    proof

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

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

       A2: S = (S1 +* S2);

      let C1 be non-empty Circuit of S1;

      let C2 be non-empty Circuit of S2;

      let C be non-empty Circuit of S such that

       A3: C1 tolerates C2 & C = (C1 +* C2);

      let s1 be State of C1;

      let s2 be State of C2;

      let s be State of C such that

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

       A5: s1 is stable and

       A6: s2 is stable;

      ( dom s) = the carrier of S & the carrier of S = (the carrier of S1 \/ the carrier of S2) by A2, CIRCCOMB:def 2, CIRCUIT1: 3;

      then s = (s1 +* s2) by A4, FUNCT_4: 70;

      

      then s = (( Following s1) +* s2) by A5

      .= (( Following s1) +* ( Following s2)) by A6

      .= ( Following s) by A1, A2, A3, A4, CIRCCOMB: 32;

      hence s = ( Following s);

    end;

    theorem :: CIRCCMB2:12

    for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) misses ( InnerVertices S2) & S = (S1 +* S2) holds for C1 be non-empty Circuit of S1, C2 be non-empty Circuit of S2 holds for C be non-empty Circuit of S st C1 tolerates C2 & C = (C1 +* C2) holds for s1 be State of C1 holds for s2 be State of C2 holds for s be State of C st s1 = (s | the carrier of S1) & s2 = (s | the carrier of S2) & s1 is stable & s2 is stable holds s is stable

    proof

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

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

       A2: S = (S1 +* S2);

      let C1 be non-empty Circuit of S1;

      let C2 be non-empty Circuit of S2;

      let C be non-empty Circuit of S such that

       A3: C1 tolerates C2 & C = (C1 +* C2);

      let s1 be State of C1;

      let s2 be State of C2;

      let s be State of C such that

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

       A5: s1 is stable and

       A6: s2 is stable;

      ( dom s) = the carrier of S & the carrier of S = (the carrier of S1 \/ the carrier of S2) by A2, CIRCCOMB:def 2, CIRCUIT1: 3;

      then s = (s2 +* s1) by A4, FUNCT_4: 70;

      

      then s = (( Following s2) +* s1) by A6

      .= (( Following s2) +* ( Following s1)) by A5

      .= ( Following s) by A1, A2, A3, A4, CIRCCOMB: 33;

      hence s = ( Following s);

    end;

    theorem :: CIRCCMB2:13

    

     Th13: 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) holds for n be natural Number holds (( Following (s,n)) | the carrier of S1) = ( Following (s1,n))

    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);

      let n be natural Number;

      

       A0: n is Nat by TARSKI: 1;

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

       A4:

      now

        let n be Nat;

        

         A5: ( Following (s,(n + 1))) = ( Following ( Following (s,n))) & ( Following ( Following (s1,n))) = ( Following (s1,(n + 1))) by FACIRC_1: 12;

        assume P[n];

        hence P[(n + 1)] by A1, A2, A5, Th10;

      end;

      (( Following (s, 0 )) | the carrier of S1) = s1 by A3, FACIRC_1: 11

      .= ( Following (s1, 0 )) by FACIRC_1: 11;

      then

       A6: P[ 0 ];

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

      hence thesis by A0;

    end;

    theorem :: CIRCCMB2:14

    

     Th14: for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InputVertices S2) misses ( InnerVertices S1) & 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, s2 be State of A2 st s2 = (s | the carrier of S2) holds for n be Nat holds (( Following (s,n)) | the carrier of S2) = ( Following (s2,n))

    proof

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

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

       A2: 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

       A3: A1 tolerates A2 and

       A4: A = (A1 +* A2);

      S1 tolerates S2 by A3, CIRCCOMB:def 3;

      then

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

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

      hence thesis by A1, A3, A5, Th13, CIRCCOMB: 19;

    end;

    theorem :: CIRCCMB2:15

    

     Th15: 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 holds for s1 be State of A1 st s1 = (s | the carrier of S1) & s1 is stable holds for s2 be State of A2 st s2 = (s | the carrier of S2) holds (( Following s) | the carrier of S2) = ( Following s2)

    proof

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

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

       A2: S = (S1 +* S2);

      

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

      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

       A4: A1 tolerates A2 and

       A5: A = (A1 +* A2);

      let s be State of A;

      let s1 be State of A1 such that

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

       A7: s1 is stable;

      let s2 be State of A2 such that

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

       A9:

      now

        let a be object;

        assume a in the carrier of S2;

        then

        reconsider v = a as Vertex of S2;

        reconsider vv = v as Vertex of S by A3, XBOOLE_0:def 3;

        

         A10: v in ( InputVertices S2) & not v in ( InnerVertices S1) implies v in (( InputVertices S2) \ ( InnerVertices S1)) by XBOOLE_0:def 5;

        

         A11: S1 tolerates S2 by A4, CIRCCOMB:def 3;

         A12:

        now

          assume that

           A13: v in ( InputVertices S2) and

           A14: v in ( InnerVertices S1);

          reconsider v1 = v as Vertex of S1 by A14;

          

          thus (( Following s) . vv) = (( Following s1) . vv) by A2, A4, A5, A6, A14, CIRCCOMB: 31

          .= (s1 . v) by A7

          .= (s . v1) by A6, FUNCT_1: 49

          .= (s2 . v) by A8, FUNCT_1: 49

          .= (( Following s2) . vv) by A13, CIRCUIT2:def 5;

        end;

        the carrier of S2 = (( InnerVertices S2) \/ ( InputVertices S2)) & (( InputVertices S1) \ ( InnerVertices S2)) = ( InputVertices S1) by A1, XBOOLE_1: 45, XBOOLE_1: 83;

        then v in ( InnerVertices S2) or v in ( InputVertices S2) & (v in ( InnerVertices S1) or not v in ( InnerVertices S1)) & ( InputVertices S) = (( InputVertices S1) \/ (( InputVertices S2) \ ( InnerVertices S1))) by A2, A11, Th5, XBOOLE_0:def 3;

        then

         A15: vv in ( InnerVertices S2) or v in ( InputVertices S) or v in ( InputVertices S2) & v in ( InnerVertices S1) by A10, XBOOLE_0:def 3;

        

        thus ((( Following s) | the carrier of S2) . a) = (( Following s) . v) by FUNCT_1: 49

        .= (( Following s2) . a) by A2, A4, A5, A8, A12, A15, CIRCCOMB: 31;

      end;

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

      then ( dom ( Following s2)) = the carrier of S2 & ( dom (( Following s) | the carrier of S2)) = the carrier of S2 by A3, CIRCUIT1: 3, RELAT_1: 62, XBOOLE_1: 7;

      hence thesis by A9, FUNCT_1: 2;

    end;

    theorem :: CIRCCMB2:16

    for S1,S2,S be non void Circuit-like non empty ManySortedSign st 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 holds for s1 be State of A1 st s1 = (s | the carrier of S1) & s1 is stable holds for s2 be State of A2 st s2 = (s | the carrier of S2) & s2 is stable holds s is stable

    proof

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

       A1: 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 and

       A3: A = (A1 +* A2);

      S1 tolerates S2 by A2, CIRCCOMB:def 3;

      then

       A4: ( InnerVertices S) = (( InnerVertices S1) \/ ( InnerVertices S2)) by A1, CIRCCOMB: 11;

      let s be State of A;

      let s1 be State of A1 such that

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

       A6: s1 = ( Following s1);

      let s2 be State of A2 such that

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

       A8: s2 = ( Following s2);

      

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

       A10:

      now

        let x be object;

        assume x in the carrier of S;

        then

        reconsider v = x as Vertex of S;

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

        then v in ( InputVertices S) or v in ( InnerVertices S) by XBOOLE_0:def 3;

        then v in ( InputVertices S) & v in the carrier of S1 or v in ( InputVertices S) & v in the carrier of S2 or v in ( InnerVertices S1) or v in ( InnerVertices S2) by A4, A9, XBOOLE_0:def 3;

        then (( Following s) . v) = (s1 . v) & v in the carrier of S1 or (( Following s) . v) = (s2 . v) & v in the carrier of S2 by A1, A2, A3, A5, A6, A7, A8, CIRCCOMB: 31;

        hence (s . x) = (( Following s) . x) by A5, A7, FUNCT_1: 49;

      end;

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

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

    end;

    theorem :: CIRCCMB2:17

    

     Th17: for S1,S2,S be non void Circuit-like non empty ManySortedSign st 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 st s is stable holds (for s1 be State of A1 st s1 = (s | the carrier of S1) holds s1 is stable) & (for s2 be State of A2 st s2 = (s | the carrier of S2) holds s2 is stable)

    proof

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

       A1: S = (S1 +* S2);

      

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

      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

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

      let s be State of A such that

       A4: s = ( Following s);

      hereby

        let s1 be State of A1 such that

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

         A6:

        now

          let x be object;

          assume x in the carrier of S1;

          then

          reconsider v = x as Vertex of S1;

          reconsider v9 = v as Vertex of S by A2, XBOOLE_0:def 3;

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

          then v in ( InputVertices S1) or v9 in ( InnerVertices S1) by XBOOLE_0:def 3;

          then (s1 . v) = (( Following s1) . v) or (s . v9) = (( Following s1) . v) by A1, A3, A4, A5, CIRCCOMB: 31, CIRCUIT2:def 5;

          hence (s1 . x) = (( Following s1) . x) by A5, FUNCT_1: 49;

        end;

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

        then s1 = ( Following s1) by A6, FUNCT_1: 2;

        hence s1 is stable;

      end;

      let s2 be State of A2 such that

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

       A8:

      now

        let x be object;

        assume x in the carrier of S2;

        then

        reconsider v = x as Vertex of S2;

        reconsider v9 = v as Vertex of S by A2, XBOOLE_0:def 3;

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

        then v in ( InputVertices S2) or v9 in ( InnerVertices S2) by XBOOLE_0:def 3;

        then (s2 . v) = (( Following s2) . v) or (s . v9) = (( Following s2) . v) by A1, A3, A4, A7, CIRCCOMB: 31, CIRCUIT2:def 5;

        hence (s2 . x) = (( Following s2) . x) by A7, FUNCT_1: 49;

      end;

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

      hence s2 = ( Following s2) by A8, FUNCT_1: 2;

    end;

    theorem :: CIRCCMB2:18

    

     Th18: 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 s1 be State of A1, s2 be State of A2, s be State of A st s1 = (s | the carrier of S1) & s2 = (s | the carrier of S2) & s1 is stable holds for n be Nat holds (( Following (s,n)) | the carrier of S2) = ( Following (s2,n))

    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 and

       A3: A = (A1 +* A2);

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

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

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

       A6: s1 is stable;

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

       A7:

      now

        let n be Nat;

        

         A8: ( Following (s,(n + 1))) = ( Following ( Following (s,n))) & ( Following ( Following (s2,n))) = ( Following (s2,(n + 1))) by FACIRC_1: 12;

        the Sorts of A1 tolerates the Sorts of A2 by A2, CIRCCOMB:def 3;

        then

        reconsider Fs1 = (( Following (s,n)) | the carrier of S1) as State of A1 by A3, CIRCCOMB: 26;

        ( Following (s1,n)) = Fs1 by A1, A2, A3, A4, Th13;

        then

         A9: Fs1 is stable by A6, Th3;

        assume P[n];

        hence P[(n + 1)] by A1, A2, A3, A8, A9, Th15;

      end;

      (( Following (s, 0 )) | the carrier of S2) = s2 by A5, FACIRC_1: 11

      .= ( Following (s2, 0 )) by FACIRC_1: 11;

      then

       A10: P[ 0 ];

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

    end;

    theorem :: CIRCCMB2:19

    

     Th19: 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 n1,n2 be Nat holds for s be State of A holds for s1 be State of A1, s2 be State of A2 st s1 = (s | the carrier of S1) & ( Following (s1,n1)) is stable & s2 = (( Following (s,n1)) | the carrier of S2) & ( Following (s2,n2)) is stable holds ( Following (s,(n1 + n2))) is stable

    proof

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

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

       A2: 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

       A3: A1 tolerates A2 and

       A4: A = (A1 +* A2);

      let n1,n2 be Nat;

      let s be State of A, s9 be State of A1, s99 be State of A2 such that

       A5: s9 = (s | the carrier of S1) & ( Following (s9,n1)) is stable and

       A6: s99 = (( Following (s,n1)) | the carrier of S2) & ( Following (s99,n2)) is stable;

      

       A7: the Sorts of A1 tolerates the Sorts of A2 by A3, CIRCCOMB:def 3;

      then

      reconsider s1 = (( Following (s,n1)) | the carrier of S1), s0 = (s | the carrier of S1) as State of A1 by A4, CIRCCOMB: 26;

      

       A8: ( Following (( Following (s,n1)),n2)) = ( Following (s,(n1 + n2))) by FACIRC_1: 13;

      then

       A9: (( Following (s,(n1 + n2))) | the carrier of S1) = ( Following (s1,n2)) by A1, A2, A3, A4, Th13;

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

      

       A10: ( dom ( Following (s,(n1 + n2)))) = the carrier of S by CIRCUIT1: 3;

      

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

      

       A12: s1 = ( Following (s0,n1)) by A1, A2, A3, A4, Th13;

      then

       A13: (( Following (s,(n1 + n2))) | the carrier of S2) = ( Following (s2,n2)) by A1, A2, A3, A4, A5, A8, Th18;

      

      then ( Following ( Following (s,(n1 + n2)))) = (( Following ( Following (s2,n2))) +* ( Following ( Following (s1,n2)))) by A1, A2, A3, A4, A9, CIRCCOMB: 33

      .= (( Following (s2,n2)) +* ( Following ( Following (s1,n2)))) by A6

      .= (( Following (s2,n2)) +* ( Following (s1,(n2 + 1)))) by FACIRC_1: 12

      .= (( Following (s2,n2)) +* s1) by A5, A12, Th3

      .= (( Following (s2,n2)) +* ( Following (s1,n2))) by A5, A12, Th3

      .= ( Following (s,(n1 + n2))) by A11, A10, A9, A13, FUNCT_4: 70;

      hence thesis;

    end;

    theorem :: CIRCCMB2:20

    

     Th20: 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 n1,n2 be Nat st (for s be State of A1 holds ( Following (s,n1)) is stable) & (for s be State of A2 holds ( Following (s,n2)) is stable) holds for s be State of A holds ( Following (s,(n1 + n2))) is stable

    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 and

       A3: A = (A1 +* A2);

      let n1,n2 be Nat such that

       A4: (for s be State of A1 holds ( Following (s,n1)) is stable) & for s be State of A2 holds ( Following (s,n2)) is stable;

      let s be State of A;

      

       A5: the Sorts of A1 tolerates the Sorts of A2 by A2, CIRCCOMB:def 3;

      then

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

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

      ( Following (s1,n1)) is stable & ( Following (s2,n2)) is stable by A4;

      hence thesis by A1, A2, A3, Th19;

    end;

    theorem :: CIRCCMB2:21

    

     Th21: for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) misses ( InnerVertices S2) & ( InputVertices S2) misses ( InnerVertices S1) & 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 holds for s1 be State of A1 st s1 = (s | the carrier of S1) holds for s2 be State of A2 st s2 = (s | the carrier of S2) holds for n be natural Number holds ( Following (s,n)) = (( Following (s1,n)) +* ( Following (s2,n)))

    proof

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

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

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

       A3: 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

       A4: A1 tolerates A2 and

       A5: A = (A1 +* A2);

      let s be State of A;

      let s1 be State of A1 such that

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

      let s2 be State of A2 such that

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

      let n be natural Number;

      

       A8: (( Following (s,n)) | the carrier of S1) = ( Following (s1,n)) by A1, A3, A4, A5, A6, Th13;

      

       A9: ( dom ( Following (s,n))) = the carrier of S & the carrier of S = (the carrier of S1 \/ the carrier of S2) by A3, CIRCCOMB:def 2, CIRCUIT1: 3;

      S1 tolerates S2 by A4, CIRCCOMB:def 3;

      then

       A10: (S1 +* S2) = (S2 +* S1) by CIRCCOMB: 5;

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

      then (( Following (s,n)) | the carrier of S2) = ( Following (s2,n)) by A2, A3, A4, A5, A7, A10, Th13, CIRCCOMB: 19;

      hence thesis by A8, A9, FUNCT_4: 70;

    end;

    theorem :: CIRCCMB2:22

    

     Th22: for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) misses ( InnerVertices S2) & ( InputVertices S2) misses ( InnerVertices S1) & 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 n1,n2 be Nat, s be State of A holds for s1 be State of A1 st s1 = (s | the carrier of S1) holds for s2 be State of A2 st s2 = (s | the carrier of S2) & ( Following (s1,n1)) is stable & ( Following (s2,n2)) is stable holds ( Following (s,( max (n1,n2)))) is stable

    proof

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

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

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

       A3: 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

       A4: A1 tolerates A2 and

       A5: A = (A1 +* A2);

      let n1,n2 be Nat;

      let s be State of A;

      set n = ( max (n1,n2));

      let s0 be State of A1 such that

       A6: s0 = (s | the carrier of S1);

      

       A7: (( Following (s,n)) | the carrier of S1) = ( Following (s0,n)) by A1, A3, A4, A5, A6, Th13;

      S1 tolerates S2 by A4, CIRCCOMB:def 3;

      then

       A8: (S1 +* S2) = (S2 +* S1) by CIRCCOMB: 5;

      let s3 be State of A2 such that

       A9: s3 = (s | the carrier of S2) and

       A10: ( Following (s0,n1)) is stable and

       A11: ( Following (s3,n2)) is stable;

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

      then

       A12: (( Following (s,n)) | the carrier of S2) = ( Following (s3,n)) by A2, A3, A4, A5, A9, A8, Th13, CIRCCOMB: 19;

      

       A13: ( Following (s3,n)) is stable by A11, Th4, XXREAL_0: 25;

      

       A14: ( Following (s0,n)) is stable by A10, Th4, XXREAL_0: 25;

      

      thus ( Following (s,( max (n1,n2)))) = (( Following (s0,n)) +* ( Following (s3,n))) by A1, A2, A3, A4, A5, A6, A9, Th21

      .= (( Following ( Following (s0,n))) +* ( Following (s3,n))) by A14

      .= (( Following ( Following (s0,n))) +* ( Following ( Following (s3,n)))) by A13

      .= ( Following ( Following (s,n))) by A2, A3, A4, A5, A7, A12, CIRCCOMB: 32;

    end;

    theorem :: CIRCCMB2:23

    for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) misses ( InnerVertices S2) & ( InputVertices S2) misses ( InnerVertices S1) & 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 n be Nat, s be State of A holds for s1 be State of A1 st s1 = (s | the carrier of S1) holds for s2 be State of A2 st s2 = (s | the carrier of S2) & ( not ( Following (s1,n)) is stable or not ( Following (s2,n)) is stable) holds not ( Following (s,n)) is stable

    proof

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

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

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

       A3: 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

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

      let n be Nat;

      let s be State of A;

      let s0 be State of A1;

      assume s0 = (s | the carrier of S1);

      then

       A5: (( Following (s,n)) | the carrier of S1) = ( Following (s0,n)) by A1, A3, A4, Th13;

      let s3 be State of A2 such that

       A6: s3 = (s | the carrier of S2) and

       A7: not ( Following (s0,n)) is stable or not ( Following (s3,n)) is stable;

      (( Following (s,n)) | the carrier of S2) = ( Following (s3,n)) by A2, A3, A4, A6, Th14;

      hence thesis by A3, A4, A7, A5, Th17;

    end;

    theorem :: CIRCCMB2:24

    for S1,S2,S be non void Circuit-like non empty ManySortedSign st ( InputVertices S1) misses ( InnerVertices S2) & ( InputVertices S2) misses ( InnerVertices S1) & 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 n1,n2 be Nat st (for s be State of A1 holds ( Following (s,n1)) is stable) & (for s be State of A2 holds ( Following (s,n2)) is stable) holds for s be State of A holds ( Following (s,( max (n1,n2)))) is stable

    proof

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

       A1: ( InputVertices S1) misses ( InnerVertices S2) & ( InputVertices S2) misses ( InnerVertices S1) & 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 and

       A3: A = (A1 +* A2);

      let n1,n2 be Nat such that

       A4: (for s be State of A1 holds ( Following (s,n1)) is stable) & for s be State of A2 holds ( Following (s,n2)) is stable;

      let s be State of A;

      

       A5: the Sorts of A1 tolerates the Sorts of A2 by A2, CIRCCOMB:def 3;

      then

      reconsider s0 = (s | the carrier of S1) as State of A1 by A3, CIRCCOMB: 26;

      reconsider s3 = (s | the carrier of S2) as State of A2 by A3, A5, CIRCCOMB: 26;

      ( Following (s0,n1)) is stable & ( Following (s3,n2)) is stable by A4;

      hence thesis by A1, A2, A3, Th22;

    end;

    scheme :: CIRCCMB2:sch22

    CIRCCMB29sch22 { S0,Sn() -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign , A0() -> Boolean gate`2=den strict Circuit of S0() , An() -> Boolean gate`2=den strict Circuit of Sn() , S( object, object) -> unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign , A( object, object) -> object , h() -> ManySortedSet of NAT , o0() -> object , o( object, object) -> object , n( Nat) -> Nat } :

for s be State of An() holds ( Following (s,(n(0) + (n() * n())))) is stable

      provided

       A1: for x be set, n be Nat holds A(x,n) is Boolean gate`2=den strict Circuit of S(x,n)

       and

       A2: for s be State of A0() holds ( Following (s,n(0))) is stable

       and

       A3: for n be Nat, x be set holds for A be non-empty Circuit of S(x,n) st x = (h() . n) & A = A(x,n) holds for s be State of A holds ( Following (s,n())) is stable

       and

       A4: ex f,g be ManySortedSet of NAT st Sn() = (f . n()) & An() = (g . n()) & (f . 0 ) = S0() & (g . 0 ) = A0() & (h() . 0 ) = o0() & for n be Nat, S be non empty ManySortedSign, A1 be non-empty MSAlgebra over S holds for x be set, A2 be non-empty MSAlgebra over S(x,n) st S = (f . n) & A1 = (g . n) & x = (h() . n) & A2 = A(x,n) holds (f . (n + 1)) = (S +* S(x,n)) & (g . (n + 1)) = (A1 +* A2) & (h() . (n + 1)) = o(x,n)

       and

       A5: ( InnerVertices S0()) is Relation & ( InputVertices S0()) is without_pairs

       and

       A6: (h() . 0 ) = o0() & o0() in ( InnerVertices S0())

       and

       A7: for n be Nat, x be set holds ( InnerVertices S(x,n)) is Relation

       and

       A8: for n be Nat, x be set st x = (h() . n) holds (( InputVertices S(x,n)) \ {x}) is without_pairs

       and

       A9: for n be Nat, x be set st x = (h() . n) holds (h() . (n + 1)) = o(x,n) & x in ( InputVertices S(x,n)) & o(x,n) in ( InnerVertices S(x,n));

      deffunc Al( non empty ManySortedSign, non-empty MSAlgebra over $1, set, set) = ($2 +* ( MSAlg (A($3,$4),S($3,$4))));

      deffunc Sl( non empty ManySortedSign, set, set) = ($1 +* S($2,$3));

      defpred Q[ object, object, object, Nat] means ex S be unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, A be Boolean gate`2=den strict Circuit of S st $1 = S & $2 = A & $3 = (h() . $4) & for s be State of A holds ( Following (s,(n(0) + ($4 * n())))) is stable;

      deffunc h( set) = (h() . $1);

      consider f,g be ManySortedSet of NAT such that

       A10: Sn() = (f . n()) & An() = (g . n()) and

       A11: (f . 0 ) = S0() and

       A12: (g . 0 ) = A0() and (h() . 0 ) = o0() and

       A13: for n be Nat, S be non empty ManySortedSign, A1 be non-empty MSAlgebra over S holds for x be set, A2 be non-empty MSAlgebra over S(x,n) st S = (f . n) & A1 = (g . n) & x = (h() . n) & A2 = A(x,n) holds (f . (n + 1)) = (S +* S(x,n)) & (g . (n + 1)) = (A1 +* A2) & (h() . (n + 1)) = o(x,n) by A4;

      deffunc f( set) = (f . $1);

      

       A14: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h() . n) holds (f . (n + 1)) = Sl(S,x,n) & (g . (n + 1)) = Al(S,A,x,n) & (h() . (n + 1)) = o(x,n)

      proof

        let n be Nat, S be non empty ManySortedSign;

        let A be non-empty MSAlgebra over S, x be set;

        reconsider A2 = A(x,n) as Boolean gate`2=den strict Circuit of S(x,n) by A1;

        A2 = ( MSAlg (A(x,n),S(x,n))) by Def1;

        hence thesis by A13;

      end;

      

       A15: for n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set st S = (f . n) & A = (g . n) & x = (h() . n) & Q[S, A, x, n] holds Q[ Sl(S,x,n), Al(S,A,x,n), o(x,n), (n + 1)]

      proof

        let n be Nat, S be non empty ManySortedSign;

        let A be non-empty MSAlgebra over S, x be set such that

         A16: S = (f . n) and A = (g . n) and x = (h() . n);

        given S9 be unsplit gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, A9 be Boolean gate`2=den strict Circuit of S9 such that

         A17: S = S9 and

         A18: A = A9 and

         A19: x = (h() . n) and

         A20: for s be State of A9 holds ( Following (s,(n(0) + (n * n())))) is stable;

        thus Q[(S +* S(x,n)), (A +* ( MSAlg (A(x,n),S(x,n)))), o(x,n), (n + 1)]

        proof

          reconsider A2 = A(x,n) as Boolean gate`2=den strict Circuit of S(x,n) by A1;

          take (S9 +* S(x,n));

          

           A21: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds Al(S,A,x,n) is non-empty MSAlgebra over Sl(S,x,n);

          

           A22: (f . 0 ) = S0() & (g . 0 ) = A0() by A11, A12;

          for n be Nat, S be non empty ManySortedSign, x be set st S = (f . n) & x = (h() . n) holds (f . (n + 1)) = Sl(S,x,n) & (h() . (n + 1)) = o(x,n) from CIRCCMB29sch15( A22, A14, A21);

          then

           A23: for n be Nat, S be non empty ManySortedSign, x be set st S = f(n) & x = (h() . n) holds f(+) = (S +* S(x,n)) & (h() . (n + 1)) = o(x,n) & x in ( InputVertices S(x,n)) & o(x,n) in ( InnerVertices S(x,n)) by A9;

          (A9 +* A2) = (A +* ( MSAlg (A(x,n),S(x,n)))) by A17, A18, Def1;

          then

          reconsider AA = (A +* ( MSAlg (A(x,n),S(x,n)))) as Boolean gate`2=den strict Circuit of (S9 +* S(x,n));

          take AA;

          

           A24: (n(0) + ((n + 1) * n())) = ((n(0) + (n * n())) + n());

          thus (S9 +* S(x,n)) = (S +* S(x,n)) & (A +* ( MSAlg (A(x,n),S(x,n)))) = AA by A17;

          thus o(x,n) = h(+) by A9, A19;

          let s be State of AA;

          

           A25: ( InnerVertices S0()) is Relation by A5;

          

           A26: for n be Nat, x be set st x = (h() . n) holds (( InputVertices S(x,n)) \ {x}) is without_pairs by A8;

          

           A27: for n be Nat, x be set holds ( InnerVertices S(x,n)) is Relation by A7;

          

           A28: ( InputVertices S0()) is without_pairs by A5;

          

           A29: f(0) = S0() & (h() . 0 ) in ( InnerVertices S0()) by A6, A11;

          for n be Nat holds ex S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st S1 = f(n) & S2 = f(+) & ( InputVertices S2) = (( InputVertices S1) \/ (( InputVertices S(.,n)) \ {(h() . n)})) & ( InnerVertices S1) is Relation & ( InputVertices S1) is without_pairs from CIRCCMB29sch10( A25, A28, A29, A27, A26, A23);

          then ex S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty ManySortedSign st S1 = (f . n) & S2 = (f . (n + 1)) & ( InputVertices S2) = (( InputVertices S1) \/ (( InputVertices S(h,n)) \ { h(n)})) & ( InnerVertices S1) is Relation & ( InputVertices S1) is without_pairs;

          then

           A30: ( InputVertices S9) misses ( InnerVertices S(x,n)) by A7, A16, A17, FACIRC_1: 5;

          A2 = ( MSAlg (A(x,n),S(x,n))) & for s be State of A2 holds ( Following (s,n())) is stable by A3, A19, Def1;

          hence ( Following (s,(n(0) + ((n + 1) * n())))) is stable by A17, A18, A20, A30, A24, Th20, CIRCCOMB: 60;

        end;

      end;

      

       A31: for S be non empty ManySortedSign, A be non-empty MSAlgebra over S holds for x be set, n be Nat holds Al(S,A,x,n) is non-empty MSAlgebra over Sl(S,x,n);

      

       A32: ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S, x be set st S = (f . 0 ) & A = (g . 0 ) & x = (h() . 0 ) & Q[S, A, x, 0 ] by A2, A11, A12;

      for n be Nat holds ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n) & A = (g . n) & Q[S, A, (h() . n), n] from CIRCCMB29sch13( A32, A14, A15, A31);

      then ex S be non empty ManySortedSign, A be non-empty MSAlgebra over S st S = (f . n()) & A = (g . n()) & Q[S, A, (h() . n()), n()];

      hence thesis by A10;

    end;