:: CIRCCMB2 semantic presentation

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
 1GateCircuit (p,f) is Boolean by CIRCCOMB:61;
end;

theorem Th1: :: CIRCCMB2:1
for X being non empty finite set
for n being Nat
for p being FinSeqLen of n
for f being Function of (n -tuples_on X),X
for o being OperSymbol of (1GateCircStr (p,f))
for s being State of (1GateCircuit (p,f)) holds o depends_on_in s = s * p
proof
let X be non empty finite set ; ::_thesis: for n being Nat
for p being FinSeqLen of n
for f being Function of (n -tuples_on X),X
for o being OperSymbol of (1GateCircStr (p,f))
for s being State of (1GateCircuit (p,f)) holds o depends_on_in s = s * p
let n be Nat; ::_thesis: for p being FinSeqLen of n
for f being Function of (n -tuples_on X),X
for o being OperSymbol of (1GateCircStr (p,f))
for s being State of (1GateCircuit (p,f)) holds o depends_on_in s = s * p
let p be FinSeqLen of n; ::_thesis: for f being Function of (n -tuples_on X),X
for o being OperSymbol of (1GateCircStr (p,f))
for s being State of (1GateCircuit (p,f)) holds o depends_on_in s = s * p
let f be Function of (n -tuples_on X),X; ::_thesis: for o being OperSymbol of (1GateCircStr (p,f))
for s being State of (1GateCircuit (p,f)) holds o depends_on_in s = s * p
let o be OperSymbol of (1GateCircStr (p,f)); ::_thesis: for s being State of (1GateCircuit (p,f)) holds o depends_on_in s = s * p
let s be State of (1GateCircuit (p,f)); ::_thesis: o depends_on_in s = s * p
o depends_on_in s = s * (the_arity_of o) by CIRCUIT1:def_3
.= s * p by CIRCCOMB:41 ;
hence  o depends_on_in s = s * p ; ::_thesis: verum
end;

theorem :: CIRCCMB2:2
for X being non empty finite set
for n being Nat
for p being FinSeqLen of n
for f being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,f)) holds Following s is stable
proof
let X be non empty finite set ; ::_thesis: for n being Nat
for p being FinSeqLen of n
for f being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,f)) holds Following s is stable
let n be Nat; ::_thesis: for p being FinSeqLen of n
for f being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,f)) holds Following s is stable
let p be FinSeqLen of n; ::_thesis: for f being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,f)) holds Following s is stable
let f be Function of (n -tuples_on X),X; ::_thesis: for s being State of (1GateCircuit (p,f)) holds Following s is stable
set S = 1GateCircStr (p,f);
let s be State of (1GateCircuit (p,f)); ::_thesis: Following s is stable
set s1 = Following s;
set s2 = Following (Following s);
A1: dom (Following s) = the carrier of (1GateCircStr (p,f)) by CIRCUIT1:3;
A2: the carrier of (1GateCircStr (p,f)) = (rng p) \/ {[p,f]} by CIRCCOMB:def_6;
A3: InputVertices (1GateCircStr (p,f)) = rng p by CIRCCOMB:42;
A4: InnerVertices (1GateCircStr (p,f)) = {[p,f]} by CIRCCOMB:42;
A5: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_(1GateCircStr_(p,f))_holds_
(Following_(Following_s))_._a_=_(Following_s)_._a
let a be set ; ::_thesis: ( a in the carrier of (1GateCircStr (p,f)) implies (Following (Following s)) . a = (Following s) . a )
assume  a in the carrier of (1GateCircStr (p,f)) ; ::_thesis: (Following (Following s)) . a = (Following s) . a
then reconsider v = a as Vertex of (1GateCircStr (p,f)) ;
 dom s = the carrier of (1GateCircStr (p,f)) by CIRCUIT1:3;
then A6: dom (s * p) = dom p by A2, RELAT_1:27, XBOOLE_1:7;
A7: dom ((Following s) * p) = dom p by A1, A2, RELAT_1:27, XBOOLE_1:7;
A8: now__::_thesis:_for_i_being_set_st_i_in_dom_p_holds_
((Following_s)_*_p)_._i_=_(s_*_p)_._i
let i be set ; ::_thesis: ( i in dom p implies ((Following s) * p) . i = (s * p) . i )
assume A9: i in dom p ; ::_thesis: ((Following s) * p) . i = (s * p) . i
then A10: p . i in rng p by FUNCT_1:3;
 ( ((Following s) * p) . i = (Following s) . (p . i) & (s * p) . i = s . (p . i) ) by A7, A6, A9, FUNCT_1:12;
hence  ((Following s) * p) . i = (s * p) . i by A3, A10, CIRCUIT2:def_5; ::_thesis: verum
end;
 ( v in rng p or v in {[p,f]} ) by A2, XBOOLE_0:def_3;
then  ( (Following (Following s)) . v = (Following s) . v or ( v = [p,f] & ( v = [p,f] implies action_at v = v ) & (Following (Following s)) . v = (Den ((action_at v),(1GateCircuit (p,f)))) . ((action_at v) depends_on_in (Following s)) & (Following s) . 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 (Following s) = (Following s) * p ) ) ) ) by A3, A4, Th1, CIRCCOMB:41, CIRCUIT2:def_5, TARSKI:def_1;
hence  (Following (Following s)) . a = (Following s) . a by A7, A6, A8, FUNCT_1:2; ::_thesis: verum
end;
 dom (Following (Following s)) = the carrier of (1GateCircStr (p,f)) by CIRCUIT1:3;
hence  Following s = Following (Following s) by A1, A5, FUNCT_1:2; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem Th3: :: CIRCCMB2:3
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A st s is stable holds
for n being Nat holds Following (s,n) = s
proof
let S be non empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for s being State of A st s is stable holds
for n being Nat holds Following (s,n) = s
let A be non-empty Circuit of S; ::_thesis: for s being State of A st s is stable holds
for n being Nat holds Following (s,n) = s
let s be State of A; ::_thesis: ( s is stable implies for n being Nat holds Following (s,n) = s )
assume A1: s is stable ; ::_thesis: for n being Nat holds Following (s,n) = s
defpred S1[ Nat] means  Following (s,$1) = s;
A2: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume  S1[n] ; ::_thesis: S1[n + 1]
then  Following (Following (s,n)) = s by A1, CIRCUIT2:def_6;
hence  S1[n + 1] by FACIRC_1:12; ::_thesis: verum
end;
A3: S1[ 0 ] by FACIRC_1:11;
thus  for n being Nat holds S1[n] from NAT_1:sch_2(A3, A2); ::_thesis: verum
end;

theorem Th4: :: CIRCCMB2:4
for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A
for n1, n2 being Nat st Following (s,n1) is stable & n1 <= n2 holds
Following (s,n2) = Following (s,n1)
proof
let S be non empty non void Circuit-like ManySortedSign ; ::_thesis: for A being non-empty Circuit of S
for s being State of A
for n1, n2 being Nat st Following (s,n1) is stable & n1 <= n2 holds
Following (s,n2) = Following (s,n1)
let A be non-empty Circuit of S; ::_thesis: for s being State of A
for n1, n2 being Nat st Following (s,n1) is stable & n1 <= n2 holds
Following (s,n2) = Following (s,n1)
let s be State of A; ::_thesis: for n1, n2 being Nat st Following (s,n1) is stable & n1 <= n2 holds
Following (s,n2) = Following (s,n1)
let n1, n2 be Nat; ::_thesis: ( Following (s,n1) is stable & n1 <= n2 implies Following (s,n2) = Following (s,n1) )
assume that
A1: Following (s,n1) is stable and
A2: n1 <= n2 ; ::_thesis: Following (s,n2) = Following (s,n1)
consider k being Nat such that
A3: n2 = n1 + k by A2, NAT_1:10;
reconsider k = k as Nat ;
 Following (s,n2) = Following ((Following (s,n1)),k) by A3, FACIRC_1:13;
hence  Following (s,n2) = Following (s,n1) by A1, Th3; ::_thesis: verum
end;

begin

scheme :: CIRCCMB2:sch 1
CIRCCMB29sch1{ F1() ->  non empty ManySortedSign , F2() ->  set , F3( set , set , set ) ->  non empty ManySortedSign , F4( set , set ) ->  set } :
 ex f, h being ManySortedSet of NAT st
( f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
proof
deffunc H1( set , set ) ->  set = [F3(($2 `1),($2 `2),$1),F4(($2 `2),$1)];
consider F being Function such that
A1: ( dom F = NAT & F . 0 = [F1(),F2()] ) and
A2: for n being Nat holds F . (n + 1) = H1(n,F . n) from NAT_1:sch_11();
deffunc H2( set ) ->  set = (F . $1) `2 ;
deffunc H3( set ) ->  set = (F . $1) `1 ;
consider f being ManySortedSet of NAT  such that
A3: for n being set st n in NAT holds
f . n = H3(n) from PBOOLE:sch_4();
consider h being ManySortedSet of NAT  such that
A4: for n being set st n in NAT holds
h . n = H2(n) from PBOOLE:sch_4();
take  f ; ::_thesis: ex h being ManySortedSet of NAT st
( f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
take  h ; ::_thesis: ( f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
 ( (F . 0) `1 = F1() & (F . 0) `2 = F2() ) by A1, MCART_1:7;
hence  ( f . 0 = F1() & h . 0 = F2() ) by A3, A4; ::_thesis: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) )
let n be Nat; ::_thesis: for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) )
let S be non empty ManySortedSign ; ::_thesis: for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) )
let x be set ; ::_thesis: ( S = f . n & x = h . n implies ( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) )
set x = F . n;
A5: n in NAT by ORDINAL1:def_12;
then A6: h . n = (F . n) `2 by A4;
assume  S = f . n ; ::_thesis: ( not x = h . n or ( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) )
then  S = (F . n) `1 by A3, A5;
then  F . (n + 1) = [F3(S,(h . n),n),F4((h . n),n)] by A2, A6;
then  ( (F . (n + 1)) `1 = F3(S,(h . n),n) & (F . (n + 1)) `2 = F4((h . n),n) ) by MCART_1:7;
hence  ( not x = h . n or ( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) by A3, A4; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 2
CIRCCMB29sch2{ F1( set , set , set ) ->  non empty ManySortedSign , F2( set , set ) ->  set , P1[ set , set , set ], F3() ->  ManySortedSet of NAT , F4() ->  ManySortedSet of NAT } :
 for n being Nat ex S being non empty ManySortedSign st
( S = F3() . n & P1[S,F4() . n,n] )
provided
A1: ex S being non empty ManySortedSign ex x being set st
( S = F3() . 0 & x = F4() . 0 & P1[S,x, 0 ] ) and
A2: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F3() . n & x = F4() . n holds
( F3() . (n + 1) = F1(S,x,n) & F4() . (n + 1) = F2(x,n) ) and
A3: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F3() . n & x = F4() . n & P1[S,x,n] holds
P1[F1(S,x,n),F2(x,n),n + 1]
proof
defpred S1[ Nat] means  ex S being non empty ManySortedSign st
( S = F3() . $1 & P1[S,F4() . $1,$1] );
A4: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
given S being non empty ManySortedSign  such that A5: S = F3() . n and
A6: P1[S,F4() . n,n] ; ::_thesis: S1[n + 1]
take  F1(S,(F4() . n),n) ; ::_thesis: ( F1(S,(F4() . n),n) = F3() . (n + 1) & P1[F1(S,(F4() . n),n),F4() . (n + 1),n + 1] )
 F4() . (n + 1) = F2((F4() . n),n) by A2, A5;
hence  ( F1(S,(F4() . n),n) = F3() . (n + 1) & P1[F1(S,(F4() . n),n),F4() . (n + 1),n + 1] ) by A2, A3, A5, A6; ::_thesis: verum
end;
A7: S1[ 0 ] by A1;
thus  for n being Nat holds S1[n] from NAT_1:sch_2(A7, A4); ::_thesis: verum
end;

defpred S1[ set , set , set ] means verum;

scheme :: CIRCCMB2:sch 3
CIRCCMB29sch3{ F1() ->  non empty ManySortedSign , F2( set , set , set ) ->  non empty ManySortedSign , F3( set , set ) ->  set , F4() ->  ManySortedSet of NAT , F5() ->  ManySortedSet of NAT } :
 for n being Nat
for x being set st x = F5() . n holds
F5() . (n + 1) = F3(x,n)
provided
A1: F4() . 0 = F1() and
A2: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F4() . n & x = F5() . n holds
( F4() . (n + 1) = F2(S,x,n) & F5() . (n + 1) = F3(x,n) )
proof
A3: ex S being non empty ManySortedSign ex x being set st
( S = F4() . 0 & x = F5() . 0 & S1[S,x, 0 ] ) by A1;
let n be Nat; ::_thesis: for x being set st x = F5() . n holds
F5() . (n + 1) = F3(x,n)
let x be set ; ::_thesis: ( x = F5() . n implies F5() . (n + 1) = F3(x,n) )
A4: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F4() . n & x = F5() . n & S1[S,x,n] holds
S1[F2(S,x,n),F3(x,n),n + 1] ;
A5: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F4() . n & x = F5() . n holds
( F4() . (n + 1) = F2(S,x,n) & F5() . (n + 1) = F3(x,n) ) by A2;
 for n being Nat ex S being non empty ManySortedSign st
( S = F4() . n & S1[S,F5() . n,n] ) from CIRCCMB2:sch_2(A3, A5, A4);
then A6: ex S being non empty ManySortedSign st S = F4() . n ;
assume  x = F5() . n ; ::_thesis: F5() . (n + 1) = F3(x,n)
hence  F5() . (n + 1) = F3(x,n) by A2, A6; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 4
CIRCCMB29sch4{ F1() ->  non empty ManySortedSign , F2() ->  set , F3( set , set , set ) ->  non empty ManySortedSign , F4( set , set ) ->  set , F5() ->  Nat } :
 ex S being non empty ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
proof
consider f, h being ManySortedSet of NAT  such that
A1: ( f . 0 = F1() & h . 0 = F2() ) and
A2: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) from CIRCCMB2:sch_1();
A3: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n & S1[S,x,n] holds
S1[F3(S,x,n),F4(x,n),n + 1] ;
A4: ex S being non empty ManySortedSign ex x being set st
( S = f . 0 & x = h . 0 & S1[S,x, 0 ] ) by A1;
 for n being Nat ex S being non empty ManySortedSign st
( S = f . n & S1[S,h . n,n] ) from CIRCCMB2:sch_2(A4, A2, A3);
then consider S being non empty ManySortedSign  such that
A5: S = f . F5() ;
take  S ; ::_thesis: ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
take  f ; ::_thesis: ex h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
take  h ; ::_thesis: ( S = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
thus  ( S = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) by A1, A2, A5; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 5
CIRCCMB29sch5{ F1() ->  non empty ManySortedSign , F2() ->  set , F3( set , set , set ) ->  non empty ManySortedSign , F4( set , set ) ->  set , F5() ->  Nat } :
 for S1, S2 being non empty ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2
proof
let S1, S2 be non empty ManySortedSign ; ::_thesis: ( ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) implies S1 = S2 )
given f1, h1 being ManySortedSet of NAT  such that A1: S1 = f1 . F5() and
A2: f1 . 0 = F1() and
A3: h1 . 0 = F2() and
A4: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n holds
( f1 . (n + 1) = F3(S,x,n) & h1 . (n + 1) = F4(x,n) ) ; ::_thesis: ( for f, h being ManySortedSet of NAT holds
( not S2 = f . F5() or not f . 0 = F1() or not h . 0 = F2() or ex n being Nat ex S being non empty ManySortedSign ex x being set st
( S = f . n & x = h . n & not ( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) or S1 = S2 )
A5: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n holds
( f1 . (n + 1) = F3(S,x,n) & h1 . (n + 1) = F4(x,n) ) by A4;
A6: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n & S1[S,x,n] holds
S1[F3(S,x,n),F4(x,n),n + 1] ;
A7: ex S being non empty ManySortedSign ex x being set st
( S = f1 . 0 & x = h1 . 0 & S1[S,x, 0 ] ) by A2;
A8: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S1[S,h1 . n,n] ) from CIRCCMB2:sch_2(A7, A5, A6);
given f2, h2 being ManySortedSet of NAT  such that A9: S2 = f2 . F5() and
A10: f2 . 0 = F1() and
A11: h2 . 0 = F2() and
A12: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f2 . n & x = h2 . n holds
( f2 . (n + 1) = F3(S,x,n) & h2 . (n + 1) = F4(x,n) ) ; ::_thesis: S1 = S2
A13: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f2 . n & x = h2 . n holds
( f2 . (n + 1) = F3(S,x,n) & h2 . (n + 1) = F4(x,n) ) by A12;
defpred S2[ Nat] means h1 . $1 = h2 . $1;
A14: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f2 . n & x = h2 . n & S1[S,x,n] holds
S1[F3(S,x,n),F4(x,n),n + 1] ;
A15: ex S being non empty ManySortedSign ex x being set st
( S = f2 . 0 & x = h2 . 0 & S1[S,x, 0 ] ) by A10;
A16: for n being Nat ex S being non empty ManySortedSign st
( S = f2 . n & S1[S,h2 . n,n] ) from CIRCCMB2:sch_2(A15, A13, A14);
A17: now__::_thesis:_for_n_being_Nat_st_S2[n]_holds_
S2[n_+_1]
let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A18: S2[n] ; ::_thesis: S2[n + 1]
 ex S being non empty ManySortedSign st
( S = f1 . n & S1[S,h1 . n,n] ) by A8;
then A19: h1 . (n + 1) = F4((h1 . n),n) by A4;
 ex S being non empty ManySortedSign st
( S = f2 . n & S1[S,h2 . n,n] ) by A16;
hence  S2[n + 1] by A12, A18, A19; ::_thesis: verum
end;
defpred S3[ Nat] means f1 . $1 = f2 . $1;
A20: S2[ 0 ] by A3, A11;
 for i being Nat holds S2[i] from NAT_1:sch_2(A20, A17);
then  for i being set st i in NAT holds
h1 . i = h2 . i ;
then A21: h1 = h2 by PBOOLE:3;
A22: now__::_thesis:_for_n_being_Nat_st_S3[n]_holds_
S3[n_+_1]
let n be Nat; ::_thesis: ( S3[n] implies S3[n + 1] )
assume A23: S3[n] ; ::_thesis: S3[n + 1]
consider S being non empty ManySortedSign  such that
A24: S = f1 . n and
 S1[S,h1 . n,n] by A8;
f1 . (n + 1) = F3(S,(h1 . n),n) by A4, A24
.= f2 . (n + 1) by A12, A21, A23, A24 ;
hence  S3[n + 1] ; ::_thesis: verum
end;
A25: S3[ 0 ] by A2, A10;
 for i being Nat holds S3[i] from NAT_1:sch_2(A25, A22);
hence  S1 = S2 by A1, A9; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 6
CIRCCMB29sch6{ F1() ->  non empty ManySortedSign , F2() ->  set , F3( set , set , set ) ->  non empty ManySortedSign , F4( set , set ) ->  set , F5() ->  Nat } :
 ( ex S being non empty ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ( for S1, S2 being non empty ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2 ) )
proof
thus  ex S being non empty ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) from CIRCCMB2:sch_4(); ::_thesis: for S1, S2 being non empty ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2
thus  for S1, S2 being non empty ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2 from CIRCCMB2:sch_5(); ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 7
CIRCCMB29sch7{ F1() ->  non empty ManySortedSign , F2( set , set , set ) ->  non empty ManySortedSign , F3() ->  set , F4( set , set ) ->  set , F5() ->  Nat } :
 ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
provided
A1: ( F1() is unsplit & F1() is gate`1=arity & F1() is gate`2isBoolean & not F1() is void & not F1() is empty & F1() is strict ) and
A2: for S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for x being set
for n being Nat holds
( F2(S,x,n) is unsplit & F2(S,x,n) is gate`1=arity & F2(S,x,n) is gate`2isBoolean & not F2(S,x,n) is void & not F2(S,x,n) is empty & F2(S,x,n) is strict )
proof
defpred S2[ non empty ManySortedSign , set ] means ( $1 is unsplit & $1 is gate`1=arity & $1 is gate`2isBoolean & not $1 is void & $1 is strict );
defpred S3[ non empty ManySortedSign , set , set ] means S2[$1,$2];
consider S being non empty ManySortedSign , f, h being ManySortedSet of NAT  such that
A3: ( S = f . F5() & f . 0 = F1() & h . 0 = F3() ) and
A4: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) from CIRCCMB2:sch_4();
A5: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n & S3[S,x,n] holds
S3[F2(S,x,n),F4(x,n),n + 1] by A2;
A6: ex S being non empty ManySortedSign ex x being set st
( S = f . 0 & x = h . 0 & S3[S,x, 0 ] ) by A1, A3;
 for n being Nat ex S being non empty ManySortedSign st
( S = f . n & S3[S,h . n,n] ) from CIRCCMB2:sch_2(A6, A4, A5);
then  ex S being non empty ManySortedSign st
( S = f . F5() & S2[S,F5()] ) ;
then reconsider S = S as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A3;
take  S ; ::_thesis: ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
take  f ; ::_thesis: ex h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
take  h ; ::_thesis: ( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) ) )
thus  ( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F2(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) by A3, A4; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 8
CIRCCMB29sch8{ F1() ->  non empty ManySortedSign , F2( set , set ) ->  non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() ->  set , F4( set , set ) ->  set , F5() ->  Nat } :
 ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = S +* F2(x,n) & h . (n + 1) = F4(x,n) ) ) )
provided
A1: ( F1() is unsplit & F1() is gate`1=arity & F1() is gate`2isBoolean & not F1() is void & not F1() is empty & F1() is strict )
proof
deffunc H1( non empty ManySortedSign , set , set ) ->  ManySortedSign = $1 +* F2($2,$3);
A2: for S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for x being set
for n being Nat holds
( H1(S,x,n) is unsplit & H1(S,x,n) is gate`1=arity & H1(S,x,n) is gate`2isBoolean & not H1(S,x,n) is void & not H1(S,x,n) is empty & H1(S,x,n) is strict ) ;
thus  ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex f, h being ManySortedSet of NAT st
( S = f . F5() & f . 0 = F1() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = H1(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) from CIRCCMB2:sch_7(A1, A2); ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 9
CIRCCMB29sch9{ F1() ->  non empty ManySortedSign , F2() ->  set , F3( set , set , set ) ->  non empty ManySortedSign , F4( set , set ) ->  set , F5() ->  Nat } :
 for S1, S2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2
proof
 for S1, S2 being non empty ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2 from CIRCCMB2:sch_5();
hence  for S1, S2 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign st ex f, h being ManySortedSet of NAT st
( S1 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) & ex f, h being ManySortedSet of NAT st
( S2 = f . F5() & f . 0 = F1() & h . 0 = F2() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F3(S,x,n) & h . (n + 1) = F4(x,n) ) ) ) holds
S1 = S2 ; ::_thesis: verum
end;

begin

theorem Th5: :: CIRCCMB2:5
for S1, S2 being 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 ; ::_thesis: ( S1 tolerates S2 implies InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1)) )
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 ; ::_thesis: InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1))
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  InputVertices (S1 +* S2) = ((InputVertices S1) \ (InnerVertices S2)) \/ ((InputVertices S2) \ (InnerVertices S1)) by A1, XBOOLE_1:41; ::_thesis: verum
end;

theorem Th6: :: CIRCCMB2:6
for X being without_pairs set
for Y being Relation holds X \ Y = X
proof
let X be without_pairs set ; ::_thesis: for Y being Relation holds X \ Y = X
let Y be Relation; ::_thesis: X \ Y = X
 X /\ Y = {} ;
then  X misses Y by XBOOLE_0:def_7;
hence  X \ Y = X by XBOOLE_1:83; ::_thesis: verum
end;

theorem :: CIRCCMB2:7
for X being Relation
for Y, Z being set st Z c= Y & Y \ Z is without_pairs holds
X \ Y = X \ Z
proof
let X be Relation; ::_thesis: for Y, Z being set st Z c= Y & Y \ Z is without_pairs holds
X \ Y = X \ Z
let Y, Z be set ; ::_thesis: ( Z c= Y & Y \ Z is without_pairs implies X \ Y = X \ Z )
assume A1: Z c= Y ; ::_thesis: ( not Y \ Z is without_pairs or X \ Y = X \ Z )
assume  Y \ Z is without_pairs ; ::_thesis: X \ Y = X \ Z
then  for x being set holds not 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  X \ Y = X \ Z ; ::_thesis: verum
end;

theorem Th8: :: CIRCCMB2:8
for X, Z being set
for Y being Relation st Z c= Y & X \ Z is without_pairs holds
X \ Y = X \ Z
proof
let X, Z be set ; ::_thesis: for Y being Relation st Z c= Y & X \ Z is without_pairs holds
X \ Y = X \ Z
let Y be Relation; ::_thesis: ( Z c= Y & X \ Z is without_pairs implies X \ Y = X \ Z )
assume A1: Z c= Y ; ::_thesis: ( not X \ Z is without_pairs or X \ Y = X \ Z )
assume  X \ Z is without_pairs ; ::_thesis: X \ Y = X \ Z
then  for x being set holds not 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  X \ Y = X \ Z ; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 10
CIRCCMB29sch10{ F1() ->  non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2( set ) ->  set , F3() ->  ManySortedSet of NAT , F4( set , set ) ->  non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F5( set , set ) ->  set } :
 for n being Nat ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F2(n) & S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
provided
A1: InnerVertices F1() is Relation and
A2: InputVertices F1() is without_pairs and
A3: ( F2(0) = F1() & F3() . 0 in InnerVertices F1() ) and
A4: for n being Nat
for x being set holds InnerVertices F4(x,n) is Relation and
A5: for n being Nat
for x being set st x = F3() . n holds
(InputVertices F4(x,n)) \ {x} is without_pairs and
A6: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F2(n) & x = F3() . n holds
( F2((n + 1)) = S +* F4(x,n) & F3() . (n + 1) = F5(x,n) & x in InputVertices F4(x,n) & F5(x,n) in InnerVertices F4(x,n) )
proof
A7: InnerVertices F4((F3() . 0),0) is Relation by A4;
defpred S2[ Nat] means  ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F2($1) & S2 = F2(($1 + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . $1),$1)) \ {(F3() . $1)}) & F3() . ($1 + 1) in InnerVertices S2 & InputVertices S2 is without_pairs & InnerVertices S2 is Relation );
A8: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; ::_thesis: ( S2[i] implies S2[i + 1] )
given S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign  such that  S1 = F2(i) and
A9: S2 = F2((i + 1)) and
 InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . i),i)) \ {(F3() . i)}) and
A10: F3() . (i + 1) in InnerVertices S2 and
A11: InputVertices S2 is without_pairs and
A12: InnerVertices S2 is Relation ; ::_thesis: S2[i + 1]
A13: {(F3() . (i + 1))} c= InnerVertices S2 by A10, ZFMISC_1:31;
take  S2 ; ::_thesis: ex S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S2 = F2((i + 1)) & S2 = F2(((i + 1) + 1)) & InputVertices S2 = (InputVertices S2) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))}) & F3() . ((i + 1) + 1) in InnerVertices S2 & InputVertices S2 is without_pairs & InnerVertices S2 is Relation )
take S3 = S2 +* F4((F3() . (i + 1)),(i + 1)); ::_thesis: ( S2 = F2((i + 1)) & S3 = F2(((i + 1) + 1)) & InputVertices S3 = (InputVertices S2) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))}) & F3() . ((i + 1) + 1) in InnerVertices S3 & InputVertices S3 is without_pairs & InnerVertices S3 is Relation )
thus  ( S2 = F2((i + 1)) & S3 = F2(((i + 1) + 1)) ) by A6, A9; ::_thesis: ( InputVertices S3 = (InputVertices S2) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))}) & F3() . ((i + 1) + 1) in InnerVertices S3 & InputVertices S3 is without_pairs & InnerVertices S3 is Relation )
A14: (InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))} is without_pairs by A5;
reconsider X1 = InputVertices S2, X2 = (InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))} as without_pairs set by A5, A11;
A15: InnerVertices F4((F3() . (i + 1)),(i + 1)) is Relation by A4;
thus  InputVertices S3 = ((InputVertices S2) \ (InnerVertices F4((F3() . (i + 1)),(i + 1)))) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ (InnerVertices S2)) by Th5, CIRCCOMB:47
.= (InputVertices S2) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ (InnerVertices S2)) by A11, A15, Th6
.= (InputVertices S2) \/ ((InputVertices F4((F3() . (i + 1)),(i + 1))) \ {(F3() . (i + 1))}) by A12, A14, A13, Th8 ; ::_thesis: ( F3() . ((i + 1) + 1) in InnerVertices S3 & InputVertices S3 is without_pairs & InnerVertices S3 is Relation )
then A16: InputVertices S3 = X1 \/ X2 ;
A17: ( F3() . ((i + 1) + 1) = F5((F3() . (i + 1)),(i + 1)) & F5((F3() . (i + 1)),(i + 1)) in InnerVertices F4((F3() . (i + 1)),(i + 1)) ) by A6, A9;
reconsider X1 = InnerVertices S2, X2 = InnerVertices F4((F3() . (i + 1)),(i + 1)) as Relation by A4, A12;
 S2 tolerates F4((F3() . (i + 1)),(i + 1)) by CIRCCOMB:47;
then  InnerVertices S3 = X1 \/ X2 by CIRCCOMB:11;
hence  ( F3() . ((i + 1) + 1) in InnerVertices S3 & InputVertices S3 is without_pairs & InnerVertices S3 is Relation ) by A17, A16, XBOOLE_0:def_3; ::_thesis: verum
end;
let n be Nat; ::_thesis: ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F2(n) & S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
A18: F1() tolerates F4((F3() . 0),0) by CIRCCOMB:47;
A19: InputVertices (F1() +* F4((F3() . 0),0)) = ((InputVertices F1()) \ (InnerVertices F4((F3() . 0),0))) \/ ((InputVertices F4((F3() . 0),0)) \ (InnerVertices F1())) by Th5, CIRCCOMB:47
.= (InputVertices F1()) \/ ((InputVertices F4((F3() . 0),0)) \ (InnerVertices F1())) by A2, A7, Th6 ;
A20: S2[ 0 ]
proof
reconsider A = (InputVertices F4((F3() . 0),0)) \ {(F3() . 0)}, B = InputVertices F1() as without_pairs set by A2, A5;
take S0 = F1(); ::_thesis: ex S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S0 = F2(0) & S2 = F2((0 + 1)) & InputVertices S2 = (InputVertices S0) \/ ((InputVertices F4((F3() . 0),0)) \ {(F3() . 0)}) & F3() . (0 + 1) in InnerVertices S2 & InputVertices S2 is without_pairs & InnerVertices S2 is Relation )
take S1 = F1() +* F4((F3() . 0),0); ::_thesis: ( S0 = F2(0) & S1 = F2((0 + 1)) & InputVertices S1 = (InputVertices S0) \/ ((InputVertices F4((F3() . 0),0)) \ {(F3() . 0)}) & F3() . (0 + 1) in InnerVertices S1 & InputVertices S1 is without_pairs & InnerVertices S1 is Relation )
thus  ( S0 = F2(0) & S1 = F2((0 + 1)) ) by A3, A6; ::_thesis: ( InputVertices S1 = (InputVertices S0) \/ ((InputVertices F4((F3() . 0),0)) \ {(F3() . 0)}) & F3() . (0 + 1) in InnerVertices S1 & InputVertices S1 is without_pairs & InnerVertices S1 is Relation )
reconsider R1 = InnerVertices F1(), R2 = InnerVertices F4((F3() . 0),0) as Relation by A1, A4;
 for x being set st x in {(F3() . 0)} holds
x in InnerVertices F1() by A3, TARSKI:def_1;
then  {(F3() . 0)} c= InnerVertices F1() by TARSKI:def_3;
then A21: InputVertices S1 = B \/ A by A1, A19, Th8;
 ( F3() . (0 + 1) = F5((F3() . 0),0) & F5((F3() . 0),0) in R2 ) by A3, A6;
then  F3() . (0 + 1) in R1 \/ R2 by XBOOLE_0:def_3;
hence  ( InputVertices S1 = (InputVertices S0) \/ ((InputVertices F4((F3() . 0),0)) \ {(F3() . 0)}) & F3() . (0 + 1) in InnerVertices S1 & InputVertices S1 is without_pairs & InnerVertices S1 is Relation ) by A18, A21, CIRCCOMB:11; ::_thesis: verum
end;
A22: for i being Nat holds S2[i] from NAT_1:sch_2(A20, A8);
then consider S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign  such that
A23: S1 = F2(n) and
A24: ( S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . n)}) ) and
 F3() . (n + 1) in InnerVertices S2 and
 InputVertices S2 is without_pairs and
 InnerVertices S2 is Relation ;
take  S1 ; ::_thesis: ex S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F2(n) & S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
take  S2 ; ::_thesis: ( S1 = F2(n) & S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
thus  ( S1 = F2(n) & S2 = F2((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F4((F3() . n),n)) \ {(F3() . n)}) ) by A23, A24; ::_thesis: ( InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
percases ( n = 0 or ex i being Nat st n = i + 1 ) by NAT_1:6;
suppose n = 0 ; ::_thesis: ( InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
hence  ( InnerVertices S1 is Relation & InputVertices S1 is without_pairs ) by A1, A2, A3, A23; ::_thesis: verum
end;
suppose ex i being Nat st n = i + 1 ; ::_thesis: ( InnerVertices S1 is Relation & InputVertices S1 is without_pairs )
then consider i being Nat such that
A25: n = i + 1 ;
reconsider i = i as Nat ;
 ex T1, T2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( T1 = F2(i) & T2 = F2((i + 1)) & InputVertices T2 = (InputVertices T1) \/ ((InputVertices F4((F3() . i),i)) \ {(F3() . i)}) & F3() . (i + 1) in InnerVertices T2 & InputVertices T2 is without_pairs & InnerVertices T2 is Relation ) by A22;
hence  ( InnerVertices S1 is Relation & InputVertices S1 is without_pairs ) by A23, A25; ::_thesis: verum
end;
end;
end;

scheme :: CIRCCMB2:sch 11
CIRCCMB29sch11{ F1( set ) ->  non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() ->  ManySortedSet of NAT , F3( set , set ) ->  non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F4( set , set ) ->  set } :
 for n being Nat holds
( InputVertices F1((n + 1)) = (InputVertices F1(n)) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices F1(n) is Relation & InputVertices F1(n) is without_pairs )
provided
A1: InnerVertices F1(0) is Relation and
A2: InputVertices F1(0) is without_pairs and
A3: F2() . 0 in InnerVertices F1(0) and
A4: for n being Nat
for x being set holds InnerVertices F3(x,n) is Relation and
A5: for n being Nat
for x being set st x = F2() . n holds
(InputVertices F3(x,n)) \ {x} is without_pairs and
A6: for n being Nat
for S being non empty ManySortedSign
for x being set st S = F1(n) & x = F2() . n holds
( F1((n + 1)) = S +* F3(x,n) & F2() . (n + 1) = F4(x,n) & x in InputVertices F3(x,n) & F4(x,n) in InnerVertices F3(x,n) )
proof
deffunc H1( set ) ->  non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign = F1($1);
A7: for n being Nat
for S being non empty ManySortedSign
for x being set st S = H1(n) & x = F2() . n holds
( H1(n + 1) = S +* F3(x,n) & F2() . (n + 1) = F4(x,n) & x in InputVertices F3(x,n) & F4(x,n) in InnerVertices F3(x,n) ) by A6;
let n be Nat; ::_thesis: ( InputVertices F1((n + 1)) = (InputVertices F1(n)) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices F1(n) is Relation & InputVertices F1(n) is without_pairs )
A8: for n being Nat
for x being set st x = F2() . n holds
(InputVertices F3(x,n)) \ {x} is without_pairs by A5;
A9: ( H1( 0 ) = H1( 0 ) & F2() . 0 in InnerVertices H1( 0 ) ) by A3;
A10: for n being Nat
for x being set holds InnerVertices F3(x,n) is Relation by A4;
 for n being Nat ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = H1(n) & S2 = H1(n + 1) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs ) from CIRCCMB2:sch_10(A1, A2, A9, A10, A8, A7);
then  ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = F1(n) & S2 = F1((n + 1)) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs ) ;
hence  ( InputVertices F1((n + 1)) = (InputVertices F1(n)) \/ ((InputVertices F3((F2() . n),n)) \ {(F2() . n)}) & InnerVertices F1(n) is Relation & InputVertices F1(n) is without_pairs ) ; ::_thesis: verum
end;

begin

scheme :: CIRCCMB2:sch 12
CIRCCMB29sch12{ F1() ->  non empty ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), F3() ->  set , F4( set , set , set ) ->  non empty ManySortedSign , F5( set , set , set , set ) ->  set , F6( set , set ) ->  set } :
 ex f, g, h being ManySortedSet of NAT st
( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
proof
deffunc H1( set , set ) ->  set = [[F4(($2 `11),($2 `2),$1),F5(($2 `11),($2 `12),($2 `2),$1)],F6(($2 `2),$1)];
consider F being Function such that
A1: ( dom F = NAT & F . 0 = [[F1(),F2()],F3()] ) and
A2: for n being Nat holds F . (n + 1) = H1(n,F . n) from NAT_1:sch_11();
A3: (F . 0) `2 = F3() by A1, MCART_1:7;
deffunc H2( set ) ->  set = (F . $1) `2 ;
deffunc H3( set ) ->  set = (F . $1) `12 ;
deffunc H4( set ) ->  set = (F . $1) `11 ;
consider f being ManySortedSet of NAT  such that
A4: for n being set st n in NAT holds
f . n = H4(n) from PBOOLE:sch_4();
consider h being ManySortedSet of NAT  such that
A5: for n being set st n in NAT holds
h . n = H2(n) from PBOOLE:sch_4();
consider g being ManySortedSet of NAT  such that
A6: for n being set st n in NAT holds
g . n = H3(n) from PBOOLE:sch_4();
take  f ; ::_thesis: ex g, h being ManySortedSet of NAT st
( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
take  g ; ::_thesis: ex h being ManySortedSet of NAT st
( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
take  h ; ::_thesis: ( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
 ( (F . 0) `11 = F1() & (F . 0) `12 = F2() ) by A1, MCART_1:85;
hence  ( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() ) by A4, A6, A5, A3; ::_thesis: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) )
let n be Nat; ::_thesis: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) )
let S be non empty ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) )
let A be non-empty MSAlgebra over S; ::_thesis: for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) )
let x be set ; ::_thesis: ( S = f . n & A = g . n & x = h . n implies ( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) )
set x = F . n;
A7: n in NAT by ORDINAL1:def_12;
then A8: h . n = (F . n) `2 by A5;
assume that
A9: S = f . n and
A10: A = g . n ; ::_thesis: ( not x = h . n or ( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) )
A11: A = (F . n) `12 by A6, A7, A10;
 S = (F . n) `11 by A4, A7, A9;
then A12: F . (n + 1) = [[F4(S,(h . n),n),F5(S,A,(h . n),n)],F6((h . n),n)] by A2, A11, A8;
then A13: (F . (n + 1)) `2 = F6((h . n),n) by MCART_1:7;
 ( (F . (n + 1)) `11 = F4(S,(h . n),n) & (F . (n + 1)) `12 = F5(S,A,(h . n),n) ) by A12, MCART_1:85;
hence  ( not x = h . n or ( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) by A4, A6, A5, A13; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 13
CIRCCMB29sch13{ F1( set , set , set ) ->  non empty ManySortedSign , F2( set , set , set , set ) ->  set , F3( set , set ) ->  set , P1[ set , set , set , set ], F4() ->  ManySortedSet of NAT , F5() ->  ManySortedSet of NAT , F6() ->  ManySortedSet of NAT } :
 for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F4() . n & A = F5() . n & P1[S,A,F6() . n,n] )
provided
A1: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = F4() . 0 & A = F5() . 0 & x = F6() . 0 & P1[S,A,x, 0 ] ) and
A2: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F4() . n & A = F5() . n & x = F6() . n holds
( F4() . (n + 1) = F1(S,x,n) & F5() . (n + 1) = F2(S,A,x,n) & F6() . (n + 1) = F3(x,n) ) and
A3: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F4() . n & A = F5() . n & x = F6() . n & P1[S,A,x,n] holds
P1[F1(S,x,n),F2(S,A,x,n),F3(x,n),n + 1] and
A4: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F2(S,A,x,n) is non-empty MSAlgebra over F1(S,x,n)
proof
defpred S2[ Nat] means  ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = F4() . $1 & A = F5() . $1 & x = F6() . $1 & P1[S,A,x,$1] );
A5: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] )
given S being non empty ManySortedSign , A being non-empty MSAlgebra over S, x being set  such that A6: ( S = F4() . n & A = F5() . n & x = F6() . n ) and
A7: P1[S,A,x,n] ; ::_thesis: S2[n + 1]
take S9 = F1(S,x,n); ::_thesis: ex A being non-empty MSAlgebra over S9 ex x being set st
( S9 = F4() . (n + 1) & A = F5() . (n + 1) & x = F6() . (n + 1) & P1[S9,A,x,n + 1] )
reconsider A9 = F2(S,A,x,n) as non-empty MSAlgebra over S9 by A4;
take  A9 ; ::_thesis: ex x being set st
( S9 = F4() . (n + 1) & A9 = F5() . (n + 1) & x = F6() . (n + 1) & P1[S9,A9,x,n + 1] )
take y = F6() . (n + 1); ::_thesis: ( S9 = F4() . (n + 1) & A9 = F5() . (n + 1) & y = F6() . (n + 1) & P1[S9,A9,y,n + 1] )
 y = F3(x,n) by A2, A6;
hence  ( S9 = F4() . (n + 1) & A9 = F5() . (n + 1) & y = F6() . (n + 1) & P1[S9,A9,y,n + 1] ) by A2, A3, A6, A7; ::_thesis: verum
end;
let n be Nat; ::_thesis: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F4() . n & A = F5() . n & P1[S,A,F6() . n,n] )
A8: S2[ 0 ] by A1;
 for n being Nat holds S2[n] from NAT_1:sch_2(A8, A5);
then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S, x being set  such that
A9: ( S = F4() . n & A = F5() . n & x = F6() . n & P1[S,A,x,n] ) ;
take  S ; ::_thesis: ex A being non-empty MSAlgebra over S st
( S = F4() . n & A = F5() . n & P1[S,A,F6() . n,n] )
take  A ; ::_thesis: ( S = F4() . n & A = F5() . n & P1[S,A,F6() . n,n] )
thus  ( S = F4() . n & A = F5() . n & P1[S,A,F6() . n,n] ) by A9; ::_thesis: verum
end;

defpred S2[ set , set , set , set ] means verum;

scheme :: CIRCCMB2:sch 14
CIRCCMB29sch14{ F1( set , set , set ) ->  non empty ManySortedSign , F2( set , set , set , set ) ->  set , F3( set , set ) ->  set , F4() ->  ManySortedSet of NAT , F5() ->  ManySortedSet of NAT , F6() ->  ManySortedSet of NAT , F7() ->  ManySortedSet of NAT , F8() ->  ManySortedSet of NAT , F9() ->  ManySortedSet of NAT } :
 ( F4() = F5() & F6() = F7() & F8() = F9() )
provided
A1: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F4() . 0 & A = F6() . 0 ) and
A2: ( F4() . 0 = F5() . 0 & F6() . 0 = F7() . 0 & F8() . 0 = F9() . 0 ) and
A3: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F4() . n & A = F6() . n & x = F8() . n holds
( F4() . (n + 1) = F1(S,x,n) & F6() . (n + 1) = F2(S,A,x,n) & F8() . (n + 1) = F3(x,n) ) and
A4: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F5() . n & A = F7() . n & x = F9() . n holds
( F5() . (n + 1) = F1(S,x,n) & F7() . (n + 1) = F2(S,A,x,n) & F9() . (n + 1) = F3(x,n) ) and
A5: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F2(S,A,x,n) is non-empty MSAlgebra over F1(S,x,n)
proof
A6: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F4() . n & A = F6() . n & x = F8() . n holds
( F4() . (n + 1) = F1(S,x,n) & F6() . (n + 1) = F2(S,A,x,n) & F8() . (n + 1) = F3(x,n) ) by A3;
set f1 = F4();
set g1 = F6();
set h1 = F8();
A7: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F4() . n & A = F6() . n & x = F8() . n & S2[S,A,x,n] holds
S2[F1(S,x,n),F2(S,A,x,n),F3(x,n),n + 1] ;
A8: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F2(S,A,x,n) is non-empty MSAlgebra over F1(S,x,n) by A5;
A9: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = F4() . 0 & A = F6() . 0 & x = F8() . 0 & S2[S,A,x, 0 ] ) by A1;
A10: for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F4() . n & A = F6() . n & S2[S,A,F8() . n,n] ) from CIRCCMB2:sch_13(A9, A6, A7, A8);
set f2 = F5();
set g2 = F7();
set h2 = F9();
A11: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F5() . n & A = F7() . n & x = F9() . n & S2[S,A,x,n] holds
S2[F1(S,x,n),F2(S,A,x,n),F3(x,n),n + 1] ;
defpred S3[ Nat] means F8() . $1 = F9() . $1;
A12: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F5() . n & A = F7() . n & x = F9() . n holds
( F5() . (n + 1) = F1(S,x,n) & F7() . (n + 1) = F2(S,A,x,n) & F9() . (n + 1) = F3(x,n) ) by A4;
A13: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = F5() . 0 & A = F7() . 0 & x = F9() . 0 & S2[S,A,x, 0 ] ) by A1, A2;
A14: for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F5() . n & A = F7() . n & S2[S,A,F9() . n,n] ) from CIRCCMB2:sch_13(A13, A12, A11, A8);
A15: now__::_thesis:_for_n_being_Nat_st_S3[n]_holds_
S3[n_+_1]
let n be Nat; ::_thesis: ( S3[n] implies S3[n + 1] )
assume A16: S3[n] ; ::_thesis: S3[n + 1]
 ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F4() . n & A = F6() . n ) by A10;
then A17: F8() . (n + 1) = F3((F8() . n),n) by A3;
 ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F5() . n & A = F7() . n ) by A14;
hence  S3[n + 1] by A4, A16, A17; ::_thesis: verum
end;
A18: S3[ 0 ] by A2;
 for i being Nat holds S3[i] from NAT_1:sch_2(A18, A15);
then A19: for i being set st i in NAT holds
F8() . i = F9() . i ;
defpred S4[ Nat] means ( F4() . $1 = F5() . $1 & F6() . $1 = F7() . $1 );
A20: F8() = F9() by A19, PBOOLE:3;
A21: now__::_thesis:_for_n_being_Nat_st_S4[n]_holds_
S4[n_+_1]
let n be Nat; ::_thesis: ( S4[n] implies S4[n + 1] )
assume A22: S4[n] ; ::_thesis: S4[n + 1]
consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A23: ( S = F4() . n & A = F6() . n ) by A10;
A24: F6() . (n + 1) = F2(S,A,(F8() . n),n) by A3, A23
.= F7() . (n + 1) by A4, A20, A22, A23 ;
F4() . (n + 1) = F1(S,(F8() . n),n) by A3, A23
.= F5() . (n + 1) by A4, A20, A22, A23 ;
hence  S4[n + 1] by A24; ::_thesis: verum
end;
A25: S4[ 0 ] by A2;
 for i being Nat holds S4[i] from NAT_1:sch_2(A25, A21);
then  ( ( for i being set st i in NAT holds
F4() . i = F5() . i ) & ( for i being set st i in NAT holds
F6() . i = F7() . i ) ) ;
hence  ( F4() = F5() & F6() = F7() & F8() = F9() ) by A19, PBOOLE:3; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 15
CIRCCMB29sch15{ F1() ->  non empty ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), F3( set , set , set ) ->  non empty ManySortedSign , F4( set , set , set , set ) ->  set , F5( set , set ) ->  set , F6() ->  ManySortedSet of NAT , F7() ->  ManySortedSet of NAT , F8() ->  ManySortedSet of NAT } :
 for n being Nat
for S being non empty ManySortedSign
for x being set st S = F6() . n & x = F8() . n holds
( F6() . (n + 1) = F3(S,x,n) & F8() . (n + 1) = F5(x,n) )
provided
A1: ( F6() . 0 = F1() & F7() . 0 = F2() ) and
A2: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F6() . n & A = F7() . n & x = F8() . n holds
( F6() . (n + 1) = F3(S,x,n) & F7() . (n + 1) = F4(S,A,x,n) & F8() . (n + 1) = F5(x,n) ) and
A3: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F4(S,A,x,n) is non-empty MSAlgebra over F3(S,x,n)
proof
A4: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = F6() . 0 & A = F7() . 0 & x = F8() . 0 & S2[S,A,x, 0 ] ) by A1;
let n be Nat; ::_thesis: for S being non empty ManySortedSign
for x being set st S = F6() . n & x = F8() . n holds
( F6() . (n + 1) = F3(S,x,n) & F8() . (n + 1) = F5(x,n) )
let S be non empty ManySortedSign ; ::_thesis: for x being set st S = F6() . n & x = F8() . n holds
( F6() . (n + 1) = F3(S,x,n) & F8() . (n + 1) = F5(x,n) )
let x be set ; ::_thesis: ( S = F6() . n & x = F8() . n implies ( F6() . (n + 1) = F3(S,x,n) & F8() . (n + 1) = F5(x,n) ) )
A5: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F6() . n & A = F7() . n & x = F8() . n & S2[S,A,x,n] holds
S2[F3(S,x,n),F4(S,A,x,n),F5(x,n),n + 1] ;
A6: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F4(S,A,x,n) is non-empty MSAlgebra over F3(S,x,n) by A3;
A7: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = F6() . n & A = F7() . n & x = F8() . n holds
( F6() . (n + 1) = F3(S,x,n) & F7() . (n + 1) = F4(S,A,x,n) & F8() . (n + 1) = F5(x,n) ) by A2;
 for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F6() . n & A = F7() . n & S2[S,A,F8() . n,n] ) from CIRCCMB2:sch_13(A4, A7, A5, A6);
then A8: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = F6() . n & A = F7() . n ) ;
assume  ( S = F6() . n & x = F8() . n ) ; ::_thesis: ( F6() . (n + 1) = F3(S,x,n) & F8() . (n + 1) = F5(x,n) )
hence  ( F6() . (n + 1) = F3(S,x,n) & F8() . (n + 1) = F5(x,n) ) by A2, A8; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 16
CIRCCMB29sch16{ F1() ->  non empty ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), F3() ->  set , F4( set , set , set ) ->  non empty ManySortedSign , F5( set , set , set , set ) ->  set , F6( set , set ) ->  set , F7() ->  Nat } :
 ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex f, g, h being ManySortedSet of NAT st
( S = f . F7() & A = g . F7() & f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
provided
A1: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F5(S,A,x,n) is non-empty MSAlgebra over F4(S,x,n)
proof
A2: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F5(S,A,x,n) is non-empty MSAlgebra over F4(S,x,n) by A1;
consider f, g, h being ManySortedSet of NAT  such that
A3: ( f . 0 = F1() & g . 0 = F2() & h . 0 = F3() ) and
A4: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) from CIRCCMB2:sch_12();
A5: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n & S2[S,A,x,n] holds
S2[F4(S,x,n),F5(S,A,x,n),F6(x,n),n + 1] ;
A6: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f . 0 & A = g . 0 & x = h . 0 & S2[S,A,x, 0 ] ) by A3;
 for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n & S2[S,A,h . n,n] ) from CIRCCMB2:sch_13(A6, A4, A5, A2);
then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A7: ( S = f . F7() & A = g . F7() ) ;
take  S ; ::_thesis: ex A being non-empty MSAlgebra over S ex f, g, h being ManySortedSet of NAT st
( S = f . F7() & A = g . F7() & f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
take  A ; ::_thesis: ex f, g, h being ManySortedSet of NAT st
( S = f . F7() & A = g . F7() & f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
take  f ; ::_thesis: ex g, h being ManySortedSet of NAT st
( S = f . F7() & A = g . F7() & f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
take  g ; ::_thesis: ex h being ManySortedSet of NAT st
( S = f . F7() & A = g . F7() & f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
take  h ; ::_thesis: ( S = f . F7() & A = g . F7() & f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) )
thus  ( S = f . F7() & A = g . F7() & f . 0 = F1() & g . 0 = F2() & h . 0 = F3() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F6(x,n) ) ) ) by A3, A4, A7; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 17
CIRCCMB29sch17{ F1() ->  non empty ManySortedSign , F2() ->  non empty ManySortedSign , F3() ->  non-empty MSAlgebra over F1(), F4() ->  set , F5( set , set , set ) ->  non empty ManySortedSign , F6( set , set , set , set ) ->  set , F7( set , set ) ->  set , F8() ->  Nat } :
 ex A being non-empty MSAlgebra over F2() ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
provided
A1: ex f, h being ManySortedSet of NAT st
( F2() = f . F8() & f . 0 = F1() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & h . (n + 1) = F7(x,n) ) ) ) and
A2: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra over F5(S,x,n)
proof
A3: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra over F5(S,x,n) by A2;
consider f, g, h being ManySortedSet of NAT  such that
A4: ( f . 0 = F1() & g . 0 = F3() & h . 0 = F4() ) and
A5: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) from CIRCCMB2:sch_12();
A6: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n & S2[S,A,x,n] holds
S2[F5(S,x,n),F6(S,A,x,n),F7(x,n),n + 1] ;
A7: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n & S2[S,A,x,n] holds
S2[F5(S,x,n),F6(S,A,x,n),F7(x,n),n + 1] ;
A8: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f . 0 & A = g . 0 & x = h . 0 & S2[S,A,x, 0 ] ) by A4;
A9: for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n & S2[S,A,h . n,n] ) from CIRCCMB2:sch_13(A8, A5, A7, A3);
A10: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f . 0 & A = g . 0 & x = h . 0 & S2[S,A,x, 0 ] ) by A4;
 for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n & S2[S,A,h . n,n] ) from CIRCCMB2:sch_13(A10, A5, A6, A3);
then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A11: S = f . F8() and
A12: A = g . F8() ;
consider f1, h1 being ManySortedSet of NAT  such that
A13: F2() = f1 . F8() and
A14: f1 . 0 = F1() and
A15: h1 . 0 = F4() and
A16: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n holds
( f1 . (n + 1) = F5(S,x,n) & h1 . (n + 1) = F7(x,n) ) by A1;
A17: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n & S1[S,x,n] holds
S1[F5(S,x,n),F7(x,n),n + 1] ;
defpred S3[ Nat] means h1 . $1 = h . $1;
A18: ex S being non empty ManySortedSign ex x being set st
( S = f1 . 0 & x = h1 . 0 & S1[S,x, 0 ] ) by A14;
A19: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S1[S,h1 . n,n] ) from CIRCCMB2:sch_2(A18, A16, A17);
A20: now__::_thesis:_for_n_being_Nat_st_S3[n]_holds_
S3[n_+_1]
let n be Nat; ::_thesis: ( S3[n] implies S3[n + 1] )
assume A21: S3[n] ; ::_thesis: S3[n + 1]
 ex S being non empty ManySortedSign st S = f1 . n by A19;
then A22: h1 . (n + 1) = F7((h1 . n),n) by A16;
 ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n ) by A9;
hence  S3[n + 1] by A5, A21, A22; ::_thesis: verum
end;
A23: S3[ 0 ] by A4, A15;
A24: for i being Nat holds S3[i] from NAT_1:sch_2(A23, A20);
defpred S4[ Nat] means f1 . $1 = f . $1;
 for i being set st i in NAT holds
h1 . i = h . i by A24;
then A25: h1 = h by PBOOLE:3;
A26: now__::_thesis:_for_n_being_Nat_st_S4[n]_holds_
S4[n_+_1]
let n be Nat; ::_thesis: ( S4[n] implies S4[n + 1] )
consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A27: S = f . n and
A28: A = g . n by A9;
assume  S4[n] ; ::_thesis: S4[n + 1]
then f1 . (n + 1) = F5(S,(h1 . n),n) by A16, A27
.= f . (n + 1) by A5, A25, A27, A28 ;
hence  S4[n + 1] ; ::_thesis: verum
end;
A29: S4[ 0 ] by A4, A14;
A30: for i being Nat holds S4[i] from NAT_1:sch_2(A29, A26);
then  for i being set st i in NAT holds
f1 . i = f . i ;
then  f1 = f by PBOOLE:3;
then reconsider A = A as non-empty MSAlgebra over F2() by A13, A11;
take  A ; ::_thesis: ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
take  f ; ::_thesis: ex g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
take  g ; ::_thesis: ex h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
take  h ; ::_thesis: ( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
thus  ( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) by A4, A5, A13, A30, A12; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 18
CIRCCMB29sch18{ F1() ->  non empty ManySortedSign , F2() ->  non empty ManySortedSign , F3() ->  non-empty MSAlgebra over F1(), F4() ->  set , F5( set , set , set ) ->  non empty ManySortedSign , F6( set , set , set , set ) ->  set , F7( set , set ) ->  set , F8() ->  Nat } :
 for A1, A2 being non-empty MSAlgebra over F2() st ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A1 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A2 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) holds
A1 = A2
provided
A1: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra over F5(S,x,n)
proof
A2: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra over F5(S,x,n) by A1;
let A1, A2 be non-empty MSAlgebra over F2(); ::_thesis: ( ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A1 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A2 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) implies A1 = A2 )
given f1, g1, h1 being ManySortedSet of NAT  such that  F2() = f1 . F8() and
A3: A1 = g1 . F8() and
A4: ( f1 . 0 = F1() & g1 . 0 = F3() ) and
A5: h1 . 0 = F4() and
A6: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f1 . n & A = g1 . n & x = h1 . n holds
( f1 . (n + 1) = F5(S,x,n) & g1 . (n + 1) = F6(S,A,x,n) & h1 . (n + 1) = F7(x,n) ) ; ::_thesis: ( for f, g, h being ManySortedSet of NAT holds
( not F2() = f . F8() or not A2 = g . F8() or not f . 0 = F1() or not g . 0 = F3() or not h . 0 = F4() or ex n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f . n & A = g . n & x = h . n & not ( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) or A1 = A2 )
A7: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f1 . 0 & A = g1 . 0 ) by A4;
given f2, g2, h2 being ManySortedSet of NAT  such that  F2() = f2 . F8() and
A8: A2 = g2 . F8() and
A9: ( f2 . 0 = F1() & g2 . 0 = F3() & h2 . 0 = F4() ) and
A10: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f2 . n & A = g2 . n & x = h2 . n holds
( f2 . (n + 1) = F5(S,x,n) & g2 . (n + 1) = F6(S,A,x,n) & h2 . (n + 1) = F7(x,n) ) ; ::_thesis: A1 = A2
A11: ( f1 . 0 = f2 . 0 & g1 . 0 = g2 . 0 & h1 . 0 = h2 . 0 ) by A4, A5, A9;
 ( f1 = f2 & g1 = g2 & h1 = h2 ) from CIRCCMB2:sch_14(A7, A11, A6, A10, A2);
hence  A1 = A2 by A3, A8; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 19
CIRCCMB29sch19{ F1() ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() ->  strict gate`2=den Boolean Circuit of F1(), F4( set , set , set ) ->  non empty ManySortedSign , F5( set , set , set , set ) ->  set , F6() ->  set , F7( set , set ) ->  set , F8() ->  Nat } :
 ex A being strict gate`2=den Boolean Circuit of F2() ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
provided
A1: for S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for x being set
for n being Nat holds
( F4(S,x,n) is unsplit & F4(S,x,n) is gate`1=arity & F4(S,x,n) is gate`2isBoolean & not F4(S,x,n) is void & F4(S,x,n) is strict ) and
A2: ex f, h being ManySortedSet of NAT st
( F2() = f . F8() & f . 0 = F1() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & h . (n + 1) = F7(x,n) ) ) ) and
A3: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F5(S,A,x,n) is non-empty MSAlgebra over F4(S,x,n) and
A4: for S, S1 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign
for A being strict gate`2=den Boolean Circuit of S
for x being set
for n being Nat st S1 = F4(S,x,n) holds
F5(S,A,x,n) is strict gate`2=den Boolean Circuit of S1
proof
A5: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F5(S,A,x,n) is non-empty MSAlgebra over F4(S,x,n) by A3;
defpred S3[ set , set , Nat] means  ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex A being strict gate`2=den Boolean Circuit of S st
( S = $1 & A = $2 );
consider f, g, h being ManySortedSet of NAT  such that
A6: ( f . 0 = F1() & g . 0 = F3() & h . 0 = F6() ) and
A7: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F7(x,n) ) from CIRCCMB2:sch_12();
A8: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n & S2[S,A,x,n] holds
S2[F4(S,x,n),F5(S,A,x,n),F7(x,n),n + 1] ;
A9: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f . 0 & A = g . 0 & x = h . 0 & S2[S,A,x, 0 ] ) by A6;
A10: for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n & S2[S,A,h . n,n] ) from CIRCCMB2:sch_13(A9, A7, A8, A5);
defpred S4[ set , set , set , Nat] means S3[$1,$2,$4];
A11: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n & S4[S,A,x,n] holds
S4[F4(S,x,n),F5(S,A,x,n),F7(x,n),n + 1]
proof
let n be Nat; ::_thesis: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n & S4[S,A,x,n] holds
S4[F4(S,x,n),F5(S,A,x,n),F7(x,n),n + 1]
let S be non empty ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n & S4[S,A,x,n] holds
S4[F4(S,x,n),F5(S,A,x,n),F7(x,n),n + 1]
let A be non-empty MSAlgebra over S; ::_thesis: for x being set st S = f . n & A = g . n & x = h . n & S4[S,A,x,n] holds
S4[F4(S,x,n),F5(S,A,x,n),F7(x,n),n + 1]
let x be set ; ::_thesis: ( S = f . n & A = g . n & x = h . n & S4[S,A,x,n] implies S4[F4(S,x,n),F5(S,A,x,n),F7(x,n),n + 1] )
assume that
 S = f . n and
 A = g . n and
 x = h . n and
A12: S3[S,A,n] ; ::_thesis: S4[F4(S,x,n),F5(S,A,x,n),F7(x,n),n + 1]
reconsider S = S as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A12;
reconsider A = A as strict gate`2=den Boolean Circuit of S by A12;
reconsider S1 = F4(S,x,n) as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A1;
 F5(S,A,x,n) is strict gate`2=den Boolean Circuit of S1 by A4;
hence  S4[F4(S,x,n),F5(S,A,x,n),F7(x,n),n + 1] ; ::_thesis: verum
end;
A13: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f . 0 & A = g . 0 & x = h . 0 & S4[S,A,x, 0 ] ) by A6;
 for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n & S4[S,A,h . n,n] ) from CIRCCMB2:sch_13(A13, A7, A11, A5);
then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A14: S = f . F8() and
A15: A = g . F8() and
A16: S3[S,A,F8()] ;
consider f1, h1 being ManySortedSet of NAT  such that
A17: F2() = f1 . F8() and
A18: f1 . 0 = F1() and
A19: h1 . 0 = F6() and
A20: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n holds
( f1 . (n + 1) = F4(S,x,n) & h1 . (n + 1) = F7(x,n) ) by A2;
A21: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n & S1[S,x,n] holds
S1[F4(S,x,n),F7(x,n),n + 1] ;
defpred S5[ Nat] means h1 . $1 = h . $1;
A22: ex S being non empty ManySortedSign ex x being set st
( S = f1 . 0 & x = h1 . 0 & S1[S,x, 0 ] ) by A18;
A23: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S1[S,h1 . n,n] ) from CIRCCMB2:sch_2(A22, A20, A21);
A24: now__::_thesis:_for_n_being_Nat_st_S5[n]_holds_
S5[n_+_1]
let n be Nat; ::_thesis: ( S5[n] implies S5[n + 1] )
assume A25: S5[n] ; ::_thesis: S5[n + 1]
 ex S being non empty ManySortedSign st S = f1 . n by A23;
then A26: h1 . (n + 1) = F7((h1 . n),n) by A20;
 ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n ) by A10;
hence  S5[n + 1] by A7, A25, A26; ::_thesis: verum
end;
A27: S5[ 0 ] by A6, A19;
A28: for i being Nat holds S5[i] from NAT_1:sch_2(A27, A24);
defpred S6[ Nat] means f1 . $1 = f . $1;
 for i being set st i in NAT holds
h1 . i = h . i by A28;
then A29: h1 = h by PBOOLE:3;
A30: now__::_thesis:_for_n_being_Nat_st_S6[n]_holds_
S6[n_+_1]
let n be Nat; ::_thesis: ( S6[n] implies S6[n + 1] )
consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A31: S = f . n and
A32: A = g . n by A10;
assume  S6[n] ; ::_thesis: S6[n + 1]
then f1 . (n + 1) = F4(S,(h1 . n),n) by A20, A31
.= f . (n + 1) by A7, A29, A31, A32 ;
hence  S6[n + 1] ; ::_thesis: verum
end;
A33: S6[ 0 ] by A6, A18;
A34: for i being Nat holds S6[i] from NAT_1:sch_2(A33, A30);
then  for i being set st i in NAT holds
f1 . i = f . i ;
then  f1 = f by PBOOLE:3;
then reconsider A = A as strict gate`2=den Boolean Circuit of F2() by A17, A14, A16;
take  A ; ::_thesis: ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
take  f ; ::_thesis: ex g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
take  g ; ::_thesis: ex h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
take  h ; ::_thesis: ( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) )
thus  ( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F4(S,x,n) & g . (n + 1) = F5(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) by A6, A7, A17, A34, A15; ::_thesis: verum
end;

definition
let S be non empty ManySortedSign ;
let A be set ;
assume A1: A is non-empty MSAlgebra over S ;
func MSAlg (A,S) ->  non-empty MSAlgebra over S means :Def1: :: CIRCCMB2:def 1
it = A;
existence
 ex b1 being non-empty MSAlgebra over S st b1 = A by A1;
uniqueness
 for b1, b2 being non-empty MSAlgebra over S st b1 = A & b2 = A holds
b1 = b2 ;
end;

:: deftheorem Def1 defines MSAlg CIRCCMB2:def_1_:_
 for S being non empty ManySortedSign
for A being set st A is non-empty MSAlgebra over S holds
for b3 being non-empty MSAlgebra over S holds
( b3 = MSAlg (A,S) iff b3 = A );

scheme :: CIRCCMB2:sch 20
CIRCCMB29sch20{ F1() ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() ->  strict gate`2=den Boolean Circuit of F1(), F4( set , set ) ->  non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign , F5( set , set ) ->  set , F6() ->  set , F7( set , set ) ->  set , F8() ->  Nat } :
 ex A being strict gate`2=den Boolean Circuit of F2() ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) ) ) )
provided
A1: ex f, h being ManySortedSet of NAT st
( F2() = f . F8() & f . 0 = F1() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = h . n holds
( f . (n + 1) = S +* F4(x,n) & h . (n + 1) = F7(x,n) ) ) ) and
A2: for x being set
for n being Nat holds F5(x,n) is strict gate`2=den Boolean Circuit of F4(x,n)
proof
deffunc H1( non empty ManySortedSign , set , set ) ->  ManySortedSign = $1 +* F4($2,$3);
consider f1, h1 being ManySortedSet of NAT  such that
A3: F2() = f1 . F8() and
A4: f1 . 0 = F1() and
A5: h1 . 0 = F6() and
A6: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n holds
( f1 . (n + 1) = H1(S,x,n) & h1 . (n + 1) = F7(x,n) ) by A1;
defpred S3[ set , set , Nat] means ( $3 <> 0 implies ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex A being strict gate`2=den Boolean Circuit of S st
( S = $1 & A = $2 ) );
deffunc H2( non empty ManySortedSign , non-empty MSAlgebra over $1, set , set ) ->  MSAlgebra over $1 +* F4($3,$4) = $2 +* (MSAlg (F5($3,$4),F4($3,$4)));
A7: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds H2(S,A,x,n) is non-empty MSAlgebra over H1(S,x,n) ;
A8: for n being Nat
for S being non empty ManySortedSign
for x being set st S = f1 . n & x = h1 . n & S1[S,x,n] holds
S1[H1(S,x,n),F7(x,n),n + 1] ;
consider f, g, h being ManySortedSet of NAT  such that
A9: ( f . 0 = F1() & g . 0 = F3() & h . 0 = F6() ) and
A10: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = H1(S,x,n) & g . (n + 1) = H2(S,A,x,n) & h . (n + 1) = F7(x,n) ) from CIRCCMB2:sch_12();
A11: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n & S2[S,A,x,n] holds
S2[H1(S,x,n),H2(S,A,x,n),F7(x,n),n + 1] ;
A12: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f . 0 & A = g . 0 & x = h . 0 & S2[S,A,x, 0 ] ) by A9;
A13: for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n & S2[S,A,h . n,n] ) from CIRCCMB2:sch_13(A12, A10, A11, A7);
defpred S4[ Nat] means h1 . $1 = h . $1;
A14: ex S being non empty ManySortedSign ex x being set st
( S = f1 . 0 & x = h1 . 0 & S1[S,x, 0 ] ) by A4;
A15: for n being Nat ex S being non empty ManySortedSign st
( S = f1 . n & S1[S,h1 . n,n] ) from CIRCCMB2:sch_2(A14, A6, A8);
A16: now__::_thesis:_for_n_being_Nat_st_S4[n]_holds_
S4[n_+_1]
let n be Nat; ::_thesis: ( S4[n] implies S4[n + 1] )
assume A17: S4[n] ; ::_thesis: S4[n + 1]
 ex S being non empty ManySortedSign st S = f1 . n by A15;
then A18: h1 . (n + 1) = F7((h1 . n),n) by A6;
 ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n ) by A13;
hence  S4[n + 1] by A10, A17, A18; ::_thesis: verum
end;
A19: S4[ 0 ] by A9, A5;
A20: for i being Nat holds S4[i] from NAT_1:sch_2(A19, A16);
defpred S5[ Nat] means f1 . $1 = f . $1;
 for i being set st i in NAT holds
h1 . i = h . i by A20;
then A21: h1 = h by PBOOLE:3;
A22: now__::_thesis:_for_n_being_Nat_st_S5[n]_holds_
S5[n_+_1]
let n be Nat; ::_thesis: ( S5[n] implies S5[n + 1] )
consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A23: S = f . n and
A24: A = g . n by A13;
assume  S5[n] ; ::_thesis: S5[n + 1]
then f1 . (n + 1) = S +* F4((h1 . n),n) by A6, A23
.= f . (n + 1) by A10, A21, A23, A24 ;
hence  S5[n + 1] ; ::_thesis: verum
end;
defpred S6[ set , set , set , Nat] means S3[$1,$2,$4];
A25: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n & S6[S,A,x,n] holds
S6[H1(S,x,n),H2(S,A,x,n),F7(x,n),n + 1]
proof
let n be Nat; ::_thesis: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n & S6[S,A,x,n] holds
S6[H1(S,x,n),H2(S,A,x,n),F7(x,n),n + 1]
let S be non empty ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n & S6[S,A,x,n] holds
S6[H1(S,x,n),H2(S,A,x,n),F7(x,n),n + 1]
let A be non-empty MSAlgebra over S; ::_thesis: for x being set st S = f . n & A = g . n & x = h . n & S6[S,A,x,n] holds
S6[H1(S,x,n),H2(S,A,x,n),F7(x,n),n + 1]
let x be set ; ::_thesis: ( S = f . n & A = g . n & x = h . n & S6[S,A,x,n] implies S6[H1(S,x,n),H2(S,A,x,n),F7(x,n),n + 1] )
assume that
A26: ( S = f . n & A = g . n ) and
 x = h . n and
A27: S3[S,A,n] and
 n + 1 <> 0 ; ::_thesis: ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex A being strict gate`2=den Boolean Circuit of S st
( S = H1(S,x,n) & A = H2(S,A,x,n) )
percases ( n = 0 or n <> 0 ) ;
supposeA28: n = 0 ; ::_thesis: ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex A being strict gate`2=den Boolean Circuit of S st
( S = H1(S,x,n) & A = H2(S,A,x,n) )
reconsider A2 = F5(x,0) as strict gate`2=den Boolean Circuit of F4(x,0) by A2;
 F3() +* (MSAlg (F5(x,0),F4(x,0))) = F3() +* A2 by Def1;
hence  ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex A being strict gate`2=den Boolean Circuit of S st
( S = H1(S,x,n) & A = H2(S,A,x,n) ) by A9, A26, A28; ::_thesis: verum
end;
supposeA29: n <> 0 ; ::_thesis: ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex A being strict gate`2=den Boolean Circuit of S st
( S = H1(S,x,n) & A = H2(S,A,x,n) )
then reconsider S = S as non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign by A27;
reconsider A = A as strict gate`2=den Boolean Circuit of S by A27, A29;
reconsider A9 = F5(x,n) as strict gate`2=den Boolean Circuit of F4(x,n) by A2;
 A +* (MSAlg (F5(x,n),F4(x,n))) = A +* A9 by Def1;
hence  ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex A being strict gate`2=den Boolean Circuit of S st
( S = H1(S,x,n) & A = H2(S,A,x,n) ) ; ::_thesis: verum
end;
end;
end;
A30: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f . 0 & A = g . 0 & x = h . 0 & S6[S,A,x, 0 ] ) by A9;
 for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n & S6[S,A,h . n,n] ) from CIRCCMB2:sch_13(A30, A10, A25, A7);
then consider S being non empty ManySortedSign , A being non-empty MSAlgebra over S such that
A31: S = f . F8() and
A32: A = g . F8() and
A33: S3[S,A,F8()] ;
A34: S5[ 0 ] by A9, A4;
A35: for i being Nat holds S5[i] from NAT_1:sch_2(A34, A22);
then  for i being set st i in NAT holds
f1 . i = f . i ;
then  f1 = f by PBOOLE:3;
then reconsider A = A as strict gate`2=den Boolean Circuit of F2() by A9, A3, A31, A32, A33;
take  A ; ::_thesis: ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) ) ) )
take  f ; ::_thesis: ex g, h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) ) ) )
take  g ; ::_thesis: ex h being ManySortedSet of NAT st
( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) ) ) )
take  h ; ::_thesis: ( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) ) ) )
thus  ( F2() = f . F8() & A = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F6() ) by A9, A3, A35, A32; ::_thesis: for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )
let n be Nat; ::_thesis: for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )
let S be non empty ManySortedSign ; ::_thesis: for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )
let A1 be non-empty MSAlgebra over S; ::_thesis: for x being set
for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )
let x be set ; ::_thesis: for A2 being non-empty MSAlgebra over F4(x,n) st S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) holds
( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )
let A2 be non-empty MSAlgebra over F4(x,n); ::_thesis: ( S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) implies ( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) ) )
assume A36: ( S = f . n & A1 = g . n & x = h . n & A2 = F5(x,n) ) ; ::_thesis: ( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) )
 A2 = MSAlg (A2,F4(x,n)) by Def1;
hence  ( f . (n + 1) = S +* F4(x,n) & g . (n + 1) = A1 +* A2 & h . (n + 1) = F7(x,n) ) by A10, A36; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 21
CIRCCMB29sch21{ F1() ->  non empty ManySortedSign , F2() ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() ->  non-empty MSAlgebra over F1(), F4() ->  set , F5( set , set , set ) ->  non empty ManySortedSign , F6( set , set , set , set ) ->  set , F7( set , set ) ->  set , F8() ->  Nat } :
 for A1, A2 being strict gate`2=den Boolean Circuit of F2() st ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A1 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A2 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) holds
A1 = A2
provided
A1: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra over F5(S,x,n)
proof
A2: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds F6(S,A,x,n) is non-empty MSAlgebra over F5(S,x,n) by A1;
 for A1, A2 being non-empty MSAlgebra over F2() st ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A1 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A2 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) holds
A1 = A2 from CIRCCMB2:sch_18(A2);
hence  for A1, A2 being strict gate`2=den Boolean Circuit of F2() st ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A1 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) & ex f, g, h being ManySortedSet of NAT st
( F2() = f . F8() & A2 = g . F8() & f . 0 = F1() & g . 0 = F3() & h . 0 = F4() & ( for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = h . n holds
( f . (n + 1) = F5(S,x,n) & g . (n + 1) = F6(S,A,x,n) & h . (n + 1) = F7(x,n) ) ) ) holds
A1 = A2 ; ::_thesis: verum
end;

begin

theorem :: CIRCCMB2:9
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 holds
for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s2 being State of C2
for s being 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 empty non void Circuit-like ManySortedSign ; ::_thesis: ( InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 implies for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2 )
assume A1: ( InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 ) ; ::_thesis: for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2
let C1 be non-empty Circuit of S1; ::_thesis: for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2
let C2 be non-empty Circuit of S2; ::_thesis: for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2
let C be non-empty Circuit of S; ::_thesis: ( C1 tolerates C2 & C = C1 +* C2 implies for s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2 )
assume that
A2: C1 tolerates C2 and
A3: C = C1 +* C2 ; ::_thesis: for s2 being State of C2
for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2
let s2 be State of C2; ::_thesis: for s being State of C st s2 = s | the carrier of S2 holds
Following s2 = (Following s) | the carrier of S2
let s be State of C; ::_thesis: ( s2 = s | the carrier of S2 implies Following s2 = (Following s) | the carrier of S2 )
assume A4: s2 = s | the carrier of S2 ; ::_thesis: Following s2 = (Following 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  Following s2 = (Following s) | the carrier of S2 by FUNCT_4:23; ::_thesis: verum
end;

theorem Th10: :: CIRCCMB2:10
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s being 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 empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 implies for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s being State of C st s1 = s | the carrier of S1 holds
Following s1 = (Following s) | the carrier of S1 )
assume A1: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 ) ; ::_thesis: for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s being State of C st s1 = s | the carrier of S1 holds
Following s1 = (Following s) | the carrier of S1
let C1 be non-empty Circuit of S1; ::_thesis: for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s being State of C st s1 = s | the carrier of S1 holds
Following s1 = (Following s) | the carrier of S1
let C2 be non-empty Circuit of S2; ::_thesis: for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s being State of C st s1 = s | the carrier of S1 holds
Following s1 = (Following s) | the carrier of S1
let C be non-empty Circuit of S; ::_thesis: ( C1 tolerates C2 & C = C1 +* C2 implies for s1 being State of C1
for s being State of C st s1 = s | the carrier of S1 holds
Following s1 = (Following s) | the carrier of S1 )
assume that
A2: C1 tolerates C2 and
A3: C = C1 +* C2 ; ::_thesis: for s1 being State of C1
for s being State of C st s1 = s | the carrier of S1 holds
Following s1 = (Following s) | the carrier of S1
let s1 be State of C1; ::_thesis: for s being State of C st s1 = s | the carrier of S1 holds
Following s1 = (Following s) | the carrier of S1
let s be State of C; ::_thesis: ( s1 = s | the carrier of S1 implies Following s1 = (Following s) | the carrier of S1 )
assume A4: s1 = s | the carrier of S1 ; ::_thesis: Following s1 = (Following 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  Following s1 = (Following s) | the carrier of S1 by FUNCT_4:23; ::_thesis: verum
end;

theorem :: CIRCCMB2:11
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 holds
for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being 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 empty non void Circuit-like ManySortedSign ; ::_thesis: ( InnerVertices S1 misses InputVertices S2 & S = S1 +* S2 implies for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being 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 )
assume that
A1: InnerVertices S1 misses InputVertices S2 and
A2: S = S1 +* S2 ; ::_thesis: for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being 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
let C1 be non-empty Circuit of S1; ::_thesis: for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being 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
let C2 be non-empty Circuit of S2; ::_thesis: for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being 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
let C be non-empty Circuit of S; ::_thesis: ( C1 tolerates C2 & C = C1 +* C2 implies for s1 being State of C1
for s2 being State of C2
for s being 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 )
assume A3: ( C1 tolerates C2 & C = C1 +* C2 ) ; ::_thesis: for s1 being State of C1
for s2 being State of C2
for s being 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
let s1 be State of C1; ::_thesis: for s2 being State of C2
for s being 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
let s2 be State of C2; ::_thesis: for s being 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
let s be State of C; ::_thesis: ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable implies s is stable )
assume that
A4: ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 ) and
A5: s1 is stable and
A6: s2 is stable ; ::_thesis: s 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, CIRCUIT2:def_6
.= (Following s1) +* (Following s2) by A6, CIRCUIT2:def_6
.= Following s by A1, A2, A3, A4, CIRCCOMB:32 ;
hence  s = Following s ; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem :: CIRCCMB2:12
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being 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 empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 implies for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being 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 )
assume that
A1: InputVertices S1 misses InnerVertices S2 and
A2: S = S1 +* S2 ; ::_thesis: for C1 being non-empty Circuit of S1
for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being 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
let C1 be non-empty Circuit of S1; ::_thesis: for C2 being non-empty Circuit of S2
for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being 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
let C2 be non-empty Circuit of S2; ::_thesis: for C being non-empty Circuit of S st C1 tolerates C2 & C = C1 +* C2 holds
for s1 being State of C1
for s2 being State of C2
for s being 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
let C be non-empty Circuit of S; ::_thesis: ( C1 tolerates C2 & C = C1 +* C2 implies for s1 being State of C1
for s2 being State of C2
for s being 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 )
assume A3: ( C1 tolerates C2 & C = C1 +* C2 ) ; ::_thesis: for s1 being State of C1
for s2 being State of C2
for s being 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
let s1 be State of C1; ::_thesis: for s2 being State of C2
for s being 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
let s2 be State of C2; ::_thesis: for s being 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
let s be State of C; ::_thesis: ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable & s2 is stable implies s is stable )
assume that
A4: ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 ) and
A5: s1 is stable and
A6: s2 is stable ; ::_thesis: s 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, CIRCUIT2:def_6
.= (Following s2) +* (Following s1) by A5, CIRCUIT2:def_6
.= Following s by A1, A2, A3, A4, CIRCCOMB:33 ;
hence  s = Following s ; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem Th13: :: CIRCCMB2:13
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
proof
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n) )
assume A1: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 ) ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let A1 be non-empty Circuit of S1; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n) )
assume A2: ( A1 tolerates A2 & A = A1 +* A2 ) ; ::_thesis: for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let s be State of A; ::_thesis: for s1 being State of A1 st s1 = s | the carrier of S1 holds
for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
let s1 be State of A1; ::_thesis: ( s1 = s | the carrier of S1 implies for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n) )
assume A3: s1 = s | the carrier of S1 ; ::_thesis: for n being Nat holds (Following (s,n)) | the carrier of S1 = Following (s1,n)
defpred S3[ Nat] means (Following (s,$1)) | the carrier of S1 = Following (s1,$1);
A4: now__::_thesis:_for_n_being_Nat_st_S3[n]_holds_
S3[n_+_1]
let n be Nat; ::_thesis: ( S3[n] implies S3[n + 1] )
A5: ( Following (s,(n + 1)) = Following (Following (s,n)) & Following (Following (s1,n)) = Following (s1,(n + 1)) ) by FACIRC_1:12;
assume  S3[n] ; ::_thesis: S3[n + 1]
hence  S3[n + 1] by A1, A2, A5, Th10; ::_thesis: verum
end;
(Following (s,0)) | the carrier of S1 = s1 by A3, FACIRC_1:11
.= Following (s1,0) by FACIRC_1:11 ;
then A6: S3[ 0 ] ;
thus  for n being Nat holds S3[n] from NAT_1:sch_2(A6, A4); ::_thesis: verum
end;

theorem Th14: :: CIRCCMB2:14
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
proof
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n) )
assume that
A1: InputVertices S2 misses InnerVertices S1 and
A2: S = S1 +* S2 ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let A1 be non-empty Circuit of S1; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n) )
assume that
A3: A1 tolerates A2 and
A4: A = A1 +* A2 ; ::_thesis: for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
 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  for s being State of A
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n) by A1, A3, A5, Th13, CIRCCOMB:19; ::_thesis: verum
end;

theorem Th15: :: CIRCCMB2:15
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being 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 empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2 )
assume that
A1: InputVertices S1 misses InnerVertices S2 and
A2: S = S1 +* S2 ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following 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; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2 )
assume that
A4: A1 tolerates A2 and
A5: A = A1 +* A2 ; ::_thesis: for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
let s be State of A; ::_thesis: for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
let s1 be State of A1; ::_thesis: ( s1 = s | the carrier of S1 & s1 is stable implies for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2 )
assume that
A6: s1 = s | the carrier of S1 and
A7: s1 is stable ; ::_thesis: for s2 being State of A2 st s2 = s | the carrier of S2 holds
(Following s) | the carrier of S2 = Following s2
let s2 be State of A2; ::_thesis: ( s2 = s | the carrier of S2 implies (Following s) | the carrier of S2 = Following s2 )
assume A8: s2 = s | the carrier of S2 ; ::_thesis: (Following s) | the carrier of S2 = Following s2
A9: now__::_thesis:_for_a_being_set_st_a_in_the_carrier_of_S2_holds_
((Following_s)_|_the_carrier_of_S2)_._a_=_(Following_s2)_._a
let a be set ; ::_thesis: ( a in the carrier of S2 implies ((Following s) | the carrier of S2) . a = (Following s2) . a )
assume  a in the carrier of S2 ; ::_thesis: ((Following s) | the carrier of S2) . a = (Following s2) . a
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__::_thesis:_(_v_in_InputVertices_S2_&_v_in_InnerVertices_S1_implies_(Following_s)_._vv_=_(Following_s2)_._vv_)
assume that
A13: v in InputVertices S2 and
A14: v in InnerVertices S1 ; ::_thesis: (Following s) . vv = (Following s2) . vv
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, CIRCUIT2:def_6
.= s . v1 by A6, FUNCT_1:49
.= s2 . v by A8, FUNCT_1:49
.= (Following s2) . vv by A13, CIRCUIT2:def_5 ; ::_thesis: verum
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 ; ::_thesis: verum
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  (Following s) | the carrier of S2 = Following s2 by A9, FUNCT_1:2; ::_thesis: verum
end;

theorem :: CIRCCMB2:16
for S1, S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 & s2 is stable holds
s is stable
proof
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 & s2 is stable holds
s is stable )
assume A1: S = S1 +* S2 ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 & s2 is stable holds
s is stable
let A1 be non-empty Circuit of S1; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 & s2 is stable holds
s is stable
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 & s2 is stable holds
s is stable
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 & s2 is stable holds
s is stable )
assume that
A2: A1 tolerates A2 and
A3: A = A1 +* A2 ; ::_thesis: for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 & s2 is stable holds
s is stable
 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; ::_thesis: for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stable holds
for s2 being State of A2 st s2 = s | the carrier of S2 & s2 is stable holds
s is stable
let s1 be State of A1; ::_thesis: ( s1 = s | the carrier of S1 & s1 is stable implies for s2 being State of A2 st s2 = s | the carrier of S2 & s2 is stable holds
s is stable )
assume that
A5: s1 = s | the carrier of S1 and
A6: s1 = Following s1 ; :: according to CIRCUIT2:def_6 ::_thesis: for s2 being State of A2 st s2 = s | the carrier of S2 & s2 is stable holds
s is stable
let s2 be State of A2; ::_thesis: ( s2 = s | the carrier of S2 & s2 is stable implies s is stable )
assume that
A7: s2 = s | the carrier of S2 and
A8: s2 = Following s2 ; :: according to CIRCUIT2:def_6 ::_thesis: s is stable
A9: the carrier of S = the carrier of S1 \/ the carrier of S2 by A1, CIRCCOMB:def_2;
A10: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_S_holds_
s_._x_=_(Following_s)_._x
let x be set ; ::_thesis: ( x in the carrier of S implies s . x = (Following s) . x )
assume  x in the carrier of S ; ::_thesis: s . x = (Following s) . x
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; ::_thesis: verum
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; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem Th17: :: CIRCCMB2:17
for S1, S2, S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A st s is stable holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 holds
s1 is stable ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 holds
s2 is stable ) )
proof
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A st s is stable holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 holds
s1 is stable ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 holds
s2 is stable ) ) )
assume A1: S = S1 +* S2 ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A st s is stable holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 holds
s1 is stable ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 holds
s2 is stable ) )
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; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A st s is stable holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 holds
s1 is stable ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 holds
s2 is stable ) )
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A st s is stable holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 holds
s1 is stable ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 holds
s2 is stable ) )
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for s being State of A st s is stable holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 holds
s1 is stable ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 holds
s2 is stable ) ) )
assume A3: ( A1 tolerates A2 & A = A1 +* A2 ) ; ::_thesis: for s being State of A st s is stable holds
( ( for s1 being State of A1 st s1 = s | the carrier of S1 holds
s1 is stable ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 holds
s2 is stable ) )
let s be State of A; ::_thesis: ( s is stable implies ( ( for s1 being State of A1 st s1 = s | the carrier of S1 holds
s1 is stable ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 holds
s2 is stable ) ) )
assume A4: s = Following s ; :: according to CIRCUIT2:def_6 ::_thesis: ( ( for s1 being State of A1 st s1 = s | the carrier of S1 holds
s1 is stable ) & ( for s2 being State of A2 st s2 = s | the carrier of S2 holds
s2 is stable ) )
hereby  ::_thesis: for s2 being State of A2 st s2 = s | the carrier of S2 holds
s2 is stable
let s1 be State of A1; ::_thesis: ( s1 = s | the carrier of S1 implies s1 is stable )
assume A5: s1 = s | the carrier of S1 ; ::_thesis: s1 is stable
A6: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_S1_holds_
s1_._x_=_(Following_s1)_._x
let x be set ; ::_thesis: ( x in the carrier of S1 implies s1 . x = (Following s1) . x )
assume  x in the carrier of S1 ; ::_thesis: s1 . x = (Following s1) . x
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; ::_thesis: verum
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 by CIRCUIT2:def_6; ::_thesis: verum
end;
let s2 be State of A2; ::_thesis: ( s2 = s | the carrier of S2 implies s2 is stable )
assume A7: s2 = s | the carrier of S2 ; ::_thesis: s2 is stable
A8: now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_S2_holds_
s2_._x_=_(Following_s2)_._x
let x be set ; ::_thesis: ( x in the carrier of S2 implies s2 . x = (Following s2) . x )
assume  x in the carrier of S2 ; ::_thesis: s2 . x = (Following s2) . x
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; ::_thesis: verum
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; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem Th18: :: CIRCCMB2:18
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
proof
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n) )
assume A1: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 ) ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let A1 be non-empty Circuit of S1; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n) )
assume that
A2: A1 tolerates A2 and
A3: A = A1 +* A2 ; ::_thesis: for s1 being State of A1
for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let s1 be State of A1; ::_thesis: for s2 being State of A2
for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let s2 be State of A2; ::_thesis: for s being State of A st s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable holds
for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
let s be State of A; ::_thesis: ( s1 = s | the carrier of S1 & s2 = s | the carrier of S2 & s1 is stable implies for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n) )
assume that
A4: s1 = s | the carrier of S1 and
A5: s2 = s | the carrier of S2 and
A6: s1 is stable ; ::_thesis: for n being Nat holds (Following (s,n)) | the carrier of S2 = Following (s2,n)
defpred S3[ Nat] means (Following (s,$1)) | the carrier of S2 = Following (s2,$1);
A7: now__::_thesis:_for_n_being_Nat_st_S3[n]_holds_
S3[n_+_1]
let n be Nat; ::_thesis: ( S3[n] implies S3[n + 1] )
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  S3[n] ; ::_thesis: S3[n + 1]
hence  S3[n + 1] by A1, A2, A3, A8, A9, Th15; ::_thesis: verum
end;
(Following (s,0)) | the carrier of S2 = s2 by A5, FACIRC_1:11
.= Following (s2,0) by FACIRC_1:11 ;
then A10: S3[ 0 ] ;
thus  for n being Nat holds S3[n] from NAT_1:sch_2(A10, A7); ::_thesis: verum
end;

theorem Th19: :: CIRCCMB2:19
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being 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 empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being 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 )
assume that
A1: InputVertices S1 misses InnerVertices S2 and
A2: S = S1 +* S2 ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being 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
let A1 be non-empty Circuit of S1; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being 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
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being 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
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being 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 )
assume that
A3: A1 tolerates A2 and
A4: A = A1 +* A2 ; ::_thesis: for n1, n2 being Nat
for s being State of A
for s1 being State of A1
for s2 being 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
let n1, n2 be Nat; ::_thesis: for s being State of A
for s1 being State of A1
for s2 being 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
let s be State of A; ::_thesis: for s1 being State of A1
for s2 being 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
let s9 be State of A1; ::_thesis: for s2 being State of A2 st s9 = s | the carrier of S1 & Following (s9,n1) is stable & s2 = (Following (s,n1)) | the carrier of S2 & Following (s2,n2) is stable holds
Following (s,(n1 + n2)) is stable
let s99 be State of A2; ::_thesis: ( s9 = s | the carrier of S1 & Following (s9,n1) is stable & s99 = (Following (s,n1)) | the carrier of S2 & Following (s99,n2) is stable implies Following (s,(n1 + n2)) is stable )
assume 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 ) ; ::_thesis: Following (s,(n1 + 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, CIRCUIT2:def_6
.= (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  Following (s,(n1 + n2)) is stable by CIRCUIT2:def_6; ::_thesis: verum
end;

theorem Th20: :: CIRCCMB2:20
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(n1 + n2)) is stable
proof
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(n1 + n2)) is stable )
assume A1: ( InputVertices S1 misses InnerVertices S2 & S = S1 +* S2 ) ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(n1 + n2)) is stable
let A1 be non-empty Circuit of S1; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(n1 + n2)) is stable
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(n1 + n2)) is stable
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(n1 + n2)) is stable )
assume that
A2: A1 tolerates A2 and
A3: A = A1 +* A2 ; ::_thesis: for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(n1 + n2)) is stable
let n1, n2 be Nat; ::_thesis: ( ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) implies for s being State of A holds Following (s,(n1 + n2)) is stable )
assume A4: ( ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) ) ; ::_thesis: for s being State of A holds Following (s,(n1 + n2)) is stable
let s be State of A; ::_thesis: Following (s,(n1 + n2)) is stable
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  Following (s,(n1 + n2)) is stable by A1, A2, A3, Th19; ::_thesis: verum
end;

theorem Th21: :: CIRCCMB2:21
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n))
proof
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n)) )
assume that
A1: InputVertices S1 misses InnerVertices S2 and
A2: InputVertices S2 misses InnerVertices S1 and
A3: S = S1 +* S2 ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n))
let A1 be non-empty Circuit of S1; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n))
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n))
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n)) )
assume that
A4: A1 tolerates A2 and
A5: A = A1 +* A2 ; ::_thesis: for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n))
let s be State of A; ::_thesis: for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n))
let s1 be State of A1; ::_thesis: ( s1 = s | the carrier of S1 implies for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n)) )
assume A6: s1 = s | the carrier of S1 ; ::_thesis: for s2 being State of A2 st s2 = s | the carrier of S2 holds
for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n))
let s2 be State of A2; ::_thesis: ( s2 = s | the carrier of S2 implies for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n)) )
assume A7: s2 = s | the carrier of S2 ; ::_thesis: for n being Nat holds Following (s,n) = (Following (s1,n)) +* (Following (s2,n))
let n be Nat; ::_thesis: Following (s,n) = (Following (s1,n)) +* (Following (s2,n))
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  Following (s,n) = (Following (s1,n)) +* (Following (s2,n)) by A8, A9, FUNCT_4:70; ::_thesis: verum
end;

theorem Th22: :: CIRCCMB2:22
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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 empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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 )
assume that
A1: InputVertices S1 misses InnerVertices S2 and
A2: InputVertices S2 misses InnerVertices S1 and
A3: S = S1 +* S2 ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
let A1 be non-empty Circuit of S1; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for n1, n2 being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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 )
assume that
A4: A1 tolerates A2 and
A5: A = A1 +* A2 ; ::_thesis: for n1, n2 being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
let n1, n2 be Nat; ::_thesis: for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
let s be State of A; ::_thesis: for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
set n = max (n1,n2);
let s0 be State of A1; ::_thesis: ( s0 = s | the carrier of S1 implies for s2 being State of A2 st s2 = s | the carrier of S2 & Following (s0,n1) is stable & Following (s2,n2) is stable holds
Following (s,(max (n1,n2))) is stable )
assume A6: s0 = s | the carrier of S1 ; ::_thesis: for s2 being State of A2 st s2 = s | the carrier of S2 & Following (s0,n1) is stable & Following (s2,n2) is stable holds
Following (s,(max (n1,n2))) is stable
A7: (Following (s,(max (n1,n2)))) | the carrier of S1 = Following (s0,(max (n1,n2))) 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; ::_thesis: ( s3 = s | the carrier of S2 & Following (s0,n1) is stable & Following (s3,n2) is stable implies Following (s,(max (n1,n2))) is stable )
assume that
A9: s3 = s | the carrier of S2 and
A10: Following (s0,n1) is stable and
A11: Following (s3,n2) is stable ; ::_thesis: Following (s,(max (n1,n2))) is stable
 A1 +* A2 = A2 +* A1 by A4, CIRCCOMB:22;
then A12: (Following (s,(max (n1,n2)))) | the carrier of S2 = Following (s3,(max (n1,n2))) by A2, A3, A4, A5, A9, A8, Th13, CIRCCOMB:19;
A13: Following (s3,(max (n1,n2))) is stable by A11, Th4, XXREAL_0:25;
A14: Following (s0,(max (n1,n2))) is stable by A10, Th4, XXREAL_0:25;
thus  Following (s,(max (n1,n2))) = (Following (s0,(max (n1,n2)))) +* (Following (s3,(max (n1,n2)))) by A1, A2, A3, A4, A5, A6, A9, Th21
.= (Following (Following (s0,(max (n1,n2))))) +* (Following (s3,(max (n1,n2)))) by A14, CIRCUIT2:def_6
.= (Following (Following (s0,(max (n1,n2))))) +* (Following (Following (s3,(max (n1,n2))))) by A13, CIRCUIT2:def_6
.= Following (Following (s,(max (n1,n2)))) by A2, A3, A4, A5, A7, A12, CIRCCOMB:32 ; :: according to CIRCUIT2:def_6 ::_thesis: verum
end;

theorem :: CIRCCMB2:23
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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 empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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 )
assume that
A1: InputVertices S1 misses InnerVertices S2 and
A2: InputVertices S2 misses InnerVertices S1 and
A3: S = S1 +* S2 ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
let A1 be non-empty Circuit of S1; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for n being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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 )
assume A4: ( A1 tolerates A2 & A = A1 +* A2 ) ; ::_thesis: for n being Nat
for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
let n be Nat; ::_thesis: for s being State of A
for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
let s be State of A; ::_thesis: for s1 being State of A1 st s1 = s | the carrier of S1 holds
for s2 being 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
let s0 be State of A1; ::_thesis: ( s0 = s | the carrier of S1 implies for s2 being State of A2 st s2 = s | the carrier of S2 & ( not Following (s0,n) is stable or not Following (s2,n) is stable ) holds
not Following (s,n) is stable )
assume  s0 = s | the carrier of S1 ; ::_thesis: for s2 being State of A2 st s2 = s | the carrier of S2 & ( not Following (s0,n) is stable or not Following (s2,n) is stable ) holds
not Following (s,n) is stable
then A5: (Following (s,n)) | the carrier of S1 = Following (s0,n) by A1, A3, A4, Th13;
let s3 be State of A2; ::_thesis: ( s3 = s | the carrier of S2 & ( not Following (s0,n) is stable or not Following (s3,n) is stable ) implies not Following (s,n) is stable )
assume that
A6: s3 = s | the carrier of S2 and
A7: ( not Following (s0,n) is stable or not Following (s3,n) is stable ) ; ::_thesis: not Following (s,n) is stable
 (Following (s,n)) | the carrier of S2 = Following (s3,n) by A2, A3, A4, A6, Th14;
hence  not Following (s,n) is stable by A3, A4, A7, A5, Th17; ::_thesis: verum
end;

theorem :: CIRCCMB2:24
for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(max (n1,n2))) is stable
proof
let S1, S2, S be non empty non void Circuit-like ManySortedSign ; ::_thesis: ( InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 implies for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(max (n1,n2))) is stable )
assume A1: ( InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses InnerVertices S1 & S = S1 +* S2 ) ; ::_thesis: for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(max (n1,n2))) is stable
let A1 be non-empty Circuit of S1; ::_thesis: for A2 being non-empty Circuit of S2
for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(max (n1,n2))) is stable
let A2 be non-empty Circuit of S2; ::_thesis: for A being non-empty Circuit of S st A1 tolerates A2 & A = A1 +* A2 holds
for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(max (n1,n2))) is stable
let A be non-empty Circuit of S; ::_thesis: ( A1 tolerates A2 & A = A1 +* A2 implies for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(max (n1,n2))) is stable )
assume that
A2: A1 tolerates A2 and
A3: A = A1 +* A2 ; ::_thesis: for n1, n2 being Nat st ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) holds
for s being State of A holds Following (s,(max (n1,n2))) is stable
let n1, n2 be Nat; ::_thesis: ( ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) implies for s being State of A holds Following (s,(max (n1,n2))) is stable )
assume A4: ( ( for s being State of A1 holds Following (s,n1) is stable ) & ( for s being State of A2 holds Following (s,n2) is stable ) ) ; ::_thesis: for s being State of A holds Following (s,(max (n1,n2))) is stable
let s be State of A; ::_thesis: Following (s,(max (n1,n2))) is stable
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  Following (s,(max (n1,n2))) is stable by A1, A2, A3, Th22; ::_thesis: verum
end;

scheme :: CIRCCMB2:sch 22
CIRCCMB29sch22{ F1() ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F2() ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F3() ->  strict gate`2=den Boolean Circuit of F1(), F4() ->  strict gate`2=den Boolean Circuit of F2(), F5( set , set ) ->  non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , F6( set , set ) ->  set , F7() ->  ManySortedSet of NAT , F8() ->  set , F9( set , set ) ->  set , F10( Nat) ->  Nat } :
 for s being State of F4() holds Following (s,(F10(0) + (F10(2) * F10(1)))) is stable
provided
A1: for x being set
for n being Nat holds F6(x,n) is strict gate`2=den Boolean Circuit of F5(x,n) and
A2: for s being State of F3() holds Following (s,F10(0)) is stable and
A3: for n being Nat
for x being set
for A being non-empty Circuit of F5(x,n) st x = F7() . n & A = F6(x,n) holds
for s being State of A holds Following (s,F10(1)) is stable and
A4: ex f, g being ManySortedSet of NAT st
( F2() = f . F10(2) & F4() = g . F10(2) & f . 0 = F1() & g . 0 = F3() & F7() . 0 = F8() & ( for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F5(x,n) st S = f . n & A1 = g . n & x = F7() . n & A2 = F6(x,n) holds
( f . (n + 1) = S +* F5(x,n) & g . (n + 1) = A1 +* A2 & F7() . (n + 1) = F9(x,n) ) ) ) and
A5: ( InnerVertices F1() is Relation & InputVertices F1() is without_pairs ) and
A6: ( F7() . 0 = F8() & F8() in InnerVertices F1() ) and
A7: for n being Nat
for x being set holds InnerVertices F5(x,n) is Relation and
A8: for n being Nat
for x being set st x = F7() . n holds
(InputVertices F5(x,n)) \ {x} is without_pairs and
A9: for n being Nat
for x being set st x = F7() . n holds
( F7() . (n + 1) = F9(x,n) & x in InputVertices F5(x,n) & F9(x,n) in InnerVertices F5(x,n) )
proof
deffunc H1( non empty ManySortedSign , non-empty MSAlgebra over $1, set , set ) ->  MSAlgebra over $1 +* F5($3,$4) = $2 +* (MSAlg (F6($3,$4),F5($3,$4)));
deffunc H2( non empty ManySortedSign , set , set ) ->  ManySortedSign = $1 +* F5($2,$3);
defpred S3[ set , set , set , Nat] means  ex S being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign ex A being strict gate`2=den Boolean Circuit of S st
( $1 = S & $2 = A & $3 = F7() . $4 & ( for s being State of A holds Following (s,(F10(0) + ($4 * F10(1)))) is stable ) );
deffunc H3( set ) ->  set = F7() . $1;
consider f, g being ManySortedSet of NAT  such that
A10: ( F2() = f . F10(2) & F4() = g . F10(2) ) and
A11: f . 0 = F1() and
A12: g . 0 = F3() and
 F7() . 0 = F8() and
A13: for n being Nat
for S being non empty ManySortedSign
for A1 being non-empty MSAlgebra over S
for x being set
for A2 being non-empty MSAlgebra over F5(x,n) st S = f . n & A1 = g . n & x = F7() . n & A2 = F6(x,n) holds
( f . (n + 1) = S +* F5(x,n) & g . (n + 1) = A1 +* A2 & F7() . (n + 1) = F9(x,n) ) by A4;
deffunc H4( set ) ->  set = f . $1;
A14: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = F7() . n holds
( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(x,n) )
proof
let n be Nat; ::_thesis: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = F7() . n holds
( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(x,n) )
let S be non empty ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = F7() . n holds
( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(x,n) )
let A be non-empty MSAlgebra over S; ::_thesis: for x being set st S = f . n & A = g . n & x = F7() . n holds
( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(x,n) )
let x be set ; ::_thesis: ( S = f . n & A = g . n & x = F7() . n implies ( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(x,n) ) )
reconsider A2 = F6(x,n) as strict gate`2=den Boolean Circuit of F5(x,n) by A1;
 A2 = MSAlg (F6(x,n),F5(x,n)) by Def1;
hence  ( S = f . n & A = g . n & x = F7() . n implies ( f . (n + 1) = H2(S,x,n) & g . (n + 1) = H1(S,A,x,n) & F7() . (n + 1) = F9(x,n) ) ) by A13; ::_thesis: verum
end;
A15: for n being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = F7() . n & S3[S,A,x,n] holds
S3[H2(S,x,n),H1(S,A,x,n),F9(x,n),n + 1]
proof
let n be Nat; ::_thesis: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = F7() . n & S3[S,A,x,n] holds
S3[H2(S,x,n),H1(S,A,x,n),F9(x,n),n + 1]
let S be non empty ManySortedSign ; ::_thesis: for A being non-empty MSAlgebra over S
for x being set st S = f . n & A = g . n & x = F7() . n & S3[S,A,x,n] holds
S3[H2(S,x,n),H1(S,A,x,n),F9(x,n),n + 1]
let A be non-empty MSAlgebra over S; ::_thesis: for x being set st S = f . n & A = g . n & x = F7() . n & S3[S,A,x,n] holds
S3[H2(S,x,n),H1(S,A,x,n),F9(x,n),n + 1]
let x be set ; ::_thesis: ( S = f . n & A = g . n & x = F7() . n & S3[S,A,x,n] implies S3[H2(S,x,n),H1(S,A,x,n),F9(x,n),n + 1] )
assume that
A16: S = f . n and
 A = g . n and
 x = F7() . n ; ::_thesis: ( not S3[S,A,x,n] or S3[H2(S,x,n),H1(S,A,x,n),F9(x,n),n + 1] )
given S9 being non empty non void strict unsplit gate`1=arity gate`2isBoolean ManySortedSign , A9 being strict gate`2=den Boolean Circuit of S9 such that A17: S = S9 and
A18: A = A9 and
A19: x = F7() . n and
A20: for s being State of A9 holds Following (s,(F10(0) + (n * F10(1)))) is stable ; ::_thesis: S3[H2(S,x,n),H1(S,A,x,n),F9(x,n),n + 1]
thus  S3[S +* F5(x,n),A +* (MSAlg (F6(x,n),F5(x,n))),F9(x,n),n + 1] ::_thesis: verum
proof
reconsider A2 = F6(x,n) as strict gate`2=den Boolean Circuit of F5(x,n) by A1;
take  S9 +* F5(x,n) ; ::_thesis: ex A being strict gate`2=den Boolean Circuit of S9 +* F5(x,n) st
( S +* F5(x,n) = S9 +* F5(x,n) & A +* (MSAlg (F6(x,n),F5(x,n))) = A & F9(x,n) = F7() . (n + 1) & ( for s being State of A holds Following (s,(F10(0) + ((n + 1) * F10(1)))) is stable ) )
A21: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds H1(S,A,x,n) is non-empty MSAlgebra over H2(S,x,n) ;
A22: ( f . 0 = F1() & g . 0 = F3() ) by A11, A12;
 for n being Nat
for S being non empty ManySortedSign
for x being set st S = f . n & x = F7() . n holds
( f . (n + 1) = H2(S,x,n) & F7() . (n + 1) = F9(x,n) ) from CIRCCMB2:sch_15(A22, A14, A21);
then A23: for n being Nat
for S being non empty ManySortedSign
for x being set st S = H4(n) & x = F7() . n holds
( H4(n + 1) = S +* F5(x,n) & F7() . (n + 1) = F9(x,n) & x in InputVertices F5(x,n) & F9(x,n) in InnerVertices F5(x,n) ) by A9;
 A9 +* A2 = A +* (MSAlg (F6(x,n),F5(x,n))) by A17, A18, Def1;
then reconsider AA = A +* (MSAlg (F6(x,n),F5(x,n))) as strict gate`2=den Boolean Circuit of S9 +* F5(x,n) ;
take  AA ; ::_thesis: ( S +* F5(x,n) = S9 +* F5(x,n) & A +* (MSAlg (F6(x,n),F5(x,n))) = AA & F9(x,n) = F7() . (n + 1) & ( for s being State of AA holds Following (s,(F10(0) + ((n + 1) * F10(1)))) is stable ) )
A24: F10(0) + ((n + 1) * F10(1)) = (F10(0) + (n * F10(1))) + F10(1) ;
thus  ( S9 +* F5(x,n) = S +* F5(x,n) & A +* (MSAlg (F6(x,n),F5(x,n))) = AA ) by A17; ::_thesis: ( F9(x,n) = F7() . (n + 1) & ( for s being State of AA holds Following (s,(F10(0) + ((n + 1) * F10(1)))) is stable ) )
thus  F9(x,n) = H3(n + 1) by A9, A19; ::_thesis: for s being State of AA holds Following (s,(F10(0) + ((n + 1) * F10(1)))) is stable
let s be State of AA; ::_thesis: Following (s,(F10(0) + ((n + 1) * F10(1)))) is stable
A25: InnerVertices F1() is Relation by A5;
A26: for n being Nat
for x being set st x = F7() . n holds
(InputVertices F5(x,n)) \ {x} is without_pairs by A8;
A27: for n being Nat
for x being set holds InnerVertices F5(x,n) is Relation by A7;
A28: InputVertices F1() is without_pairs by A5;
A29: ( H4( 0 ) = F1() & F7() . 0 in InnerVertices F1() ) by A6, A11;
 for n being Nat ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = H4(n) & S2 = H4(n + 1) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F5((F7() . n),n)) \ {(F7() . n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs ) from CIRCCMB2:sch_10(A25, A28, A29, A27, A26, A23);
then  ex S1, S2 being non empty non void unsplit gate`1=arity gate`2isBoolean ManySortedSign st
( S1 = f . n & S2 = f . (n + 1) & InputVertices S2 = (InputVertices S1) \/ ((InputVertices F5(H3(n),n)) \ {H3(n)}) & InnerVertices S1 is Relation & InputVertices S1 is without_pairs ) ;
then A30: InputVertices S9 misses InnerVertices F5(x,n) by A7, A16, A17, FACIRC_1:5;
 ( A2 = MSAlg (F6(x,n),F5(x,n)) & ( for s being State of A2 holds Following (s,F10(1)) is stable ) ) by A3, A19, Def1;
hence  Following (s,(F10(0) + ((n + 1) * F10(1)))) is stable by A17, A18, A20, A30, A24, Th20, CIRCCOMB:60; ::_thesis: verum
end;
end;
A31: for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S
for x being set
for n being Nat holds H1(S,A,x,n) is non-empty MSAlgebra over H2(S,x,n) ;
A32: ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S ex x being set st
( S = f . 0 & A = g . 0 & x = F7() . 0 & S3[S,A,x, 0 ] ) by A2, A11, A12;
 for n being Nat ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . n & A = g . n & S3[S,A,F7() . n,n] ) from CIRCCMB2:sch_13(A32, A14, A15, A31);
then  ex S being non empty ManySortedSign ex A being non-empty MSAlgebra over S st
( S = f . F10(2) & A = g . F10(2) & S3[S,A,F7() . F10(2),F10(2)] ) ;
hence  for s being State of F4() holds Following (s,(F10(0) + (F10(2) * F10(1)))) is stable by A10; ::_thesis: verum
end;