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