CIRCCMB2

:: Combining of Multi Cell Circuits
::  by Grzegorz Bancerek , Shin'nosuke Yamaguchi and Yasunari Shidama
::
:: Received March 22, 2002
:: Copyright (c) 2002-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NAT_1, FUNCT_1, FINSEQ_2, MARGREL1, CIRCCOMB, LATTICES, FINSET_1,
      XBOOLE_0, MSUALG_1, FSM_1, CIRCUIT1, RELAT_1, CIRCUIT2, STRUCT_0,
      MSAFREE2, GLIB_000, ARYTM_3, CARD_1, XXREAL_0, PBOOLE, NUMBERS, MCART_1,
      FUNCT_4, PARTFUN1, FACIRC_1, TARSKI, ORDINAL1;
 notations TARSKI, XBOOLE_0, ORDINAL1, NUMBERS, XCMPLX_0, XFAMILY, XXREAL_0,
      NAT_1, XTUPLE_0, MCART_1, FINSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
      FINSEQ_2, FUNCT_4, PBOOLE, MARGREL1, STRUCT_0, MSUALG_1, MSAFREE2,
      CIRCUIT1, CIRCUIT2, CIRCCOMB, FACIRC_1;
 constructors LIMFUNC1, CIRCUIT1, CIRCUIT2, FACIRC_1, NAT_1, RELSET_1,
      XTUPLE_0, XFAMILY;
 registrations RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, CARD_3, STRUCT_0, CIRCCOMB,
      FACIRC_1, NAT_1, MARGREL1, CARD_1, XTUPLE_0;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions CIRCUIT2;
 equalities MSAFREE2;
 expansions CIRCUIT2;
 theorems TARSKI, FUNCT_1, RELAT_1, ZFMISC_1, NAT_1, MCART_1, PBOOLE, CIRCCOMB,
      FACIRC_1, FUNCT_4, FRECHET, CIRCUIT1, CIRCUIT2, XBOOLE_0, XBOOLE_1,
      XXREAL_0, ORDINAL1;
 schemes NAT_1, PBOOLE;

begin :: One gate circuits

registration
  let n be Nat;
  let f be Function of n-tuples_on BOOLEAN, BOOLEAN;
  let p be FinSeqLen of n;
  cluster 1GateCircuit(p,f) -> Boolean;
  coherence by CIRCCOMB:61;
end;

theorem Th1:
  for X being finite non empty set, 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 finite non empty set;
  let n be Nat;
  let p be FinSeqLen of n;
  let f be Function of n-tuples_on X, X;
  let o be OperSymbol of 1GateCircStr(p,f);
  let s be State of 1GateCircuit(p,f);
  o depends_on_in s = s * (the_arity_of o) by CIRCUIT1:def 3
    .= s*p by CIRCCOMB:41;
  hence thesis;
end;

theorem
  for X being finite non empty set, 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 finite non empty set, n be Nat;
  let p be FinSeqLen of n;
  let f be Function of n-tuples_on X, X;
  set S = 1GateCircStr(p,f);
  let s be State of 1GateCircuit(p,f);
  set s1 = Following s, s2 = Following s1;
A1: dom s1 = the carrier of S by CIRCUIT1:3;
A2: the carrier of S = rng p \/ {[p,f]} by CIRCCOMB:def 6;
A3: InputVertices S = rng p by CIRCCOMB:42;
A4: InnerVertices S = {[p,f]} by CIRCCOMB:42;
A5: now
    let a be object;
    assume a in the carrier of S;
    then reconsider v = a as Vertex of S;
    dom s = the carrier of S by CIRCUIT1:3;
    then
A6: dom (s*p) = dom p by A2,RELAT_1:27,XBOOLE_1:7;
A7: dom (s1*p) = dom p by A1,A2,RELAT_1:27,XBOOLE_1:7;
A8: now
      let i be object;
      assume
A9:   i in dom p;
      then
A10:  p.i in rng p by FUNCT_1:3;
      (s1*p).i = s1.(p.i) & (s*p).i = s.(p.i) by A7,A6,A9,FUNCT_1:12;
      hence (s1*p).i = (s*p).i by A3,A10,CIRCUIT2:def 5;
    end;
    v in rng p or v in {[p,f]} by A2,XBOOLE_0:def 3;
    then
    s2.v = s1.v or v = [p,f] & (v = [p,f] implies action_at v = v) & s2.v
= (Den(action_at v, 1GateCircuit(p,f))). (action_at v depends_on_in s1) & s1.v
    = (Den(action_at v, 1GateCircuit(p,f))). (action_at v depends_on_in s) & (
    action_at v = [p,f] implies action_at v depends_on_in s = s*p & action_at v
    depends_on_in s1 = s1*p) by A3,A4,Th1,CIRCCOMB:41,CIRCUIT2:def 5
,TARSKI:def 1;
    hence s2.a = s1.a by A7,A6,A8,FUNCT_1:2;
  end;
  dom s2 = the carrier of S by CIRCUIT1:3;
  hence Following s = Following Following s by A1,A5,FUNCT_1:2;
end;

theorem Th3:
  for S being non void Circuit-like non empty ManySortedSign for
  A being non-empty Circuit of S for s being State of A st s is stable
  for n being natural Number holds Following(s, n) = s
proof
  let S be non void Circuit-like non empty ManySortedSign;
  let A be non-empty Circuit of S;
  let s be State of A such that
A1: s is stable;
  let n be natural Number;
A0: n is Nat by TARSKI:1;
  defpred P[Nat] means Following(s,$1) = s;
A2: for n being Nat st P[n] holds P[n+1] by A1,FACIRC_1:12;
A3: P[ 0 ] by FACIRC_1:11;
  for n being Nat holds P[n] from NAT_1:sch 2(A3,A2);
  hence thesis by A0;
end;

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

begin :: Defining Many Cell Circuit Structures

scheme
  CIRCCMB29sch1 {S0() -> non empty ManySortedSign, o0()-> object,
    S(object,object,object)-> non empty ManySortedSign,
    o(object,object) -> object}:
ex f,h being ManySortedSet of
  NAT st f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(
  n+1) = o(x,n) proof
  deffunc f(object,object) = [S($2`1,$2`2,$1), o($2`2,$1)];
  consider F being Function such that
A1: dom F = NAT & F.0 = [S0(),o0()] and
A2: for n being Nat holds F.(n+1) = f(n,F.n) from NAT_1:sch 11;
  deffunc h(object) = (F.$1)`2;
  deffunc f(object) = (F.$1)`1;
  consider f being ManySortedSet of NAT such that
A3: for n being object st n in NAT holds f.n = f(n) from PBOOLE:sch 4;
  consider h being ManySortedSet of NAT such that
A4: for n being object st n in NAT holds h.n = h(n) from PBOOLE:sch 4;
  take f,h;
  (F.0)`1 = S0() & (F.0)`2 = o0() by A1;
  hence f.0 = S0() & h.0 = o0() by A3,A4;
  let n be Nat, S be non empty ManySortedSign, x be set;
  set x = F.n;
A5: n in NAT by ORDINAL1:def 12;
  then
A6: h.n = x`2 by A4;
  assume S = f.n;
  then S = x`1 by A3,A5;
  then F.(n+1) = [S(S,h.n,n), o(h.n,n)] by A2,A6;
  then (F.(n+1))`1 = S(S,h.n,n) & (F.(n+1))`2 = o(h.n,n);
  hence thesis by A3,A4;
end;

scheme ::CircSch1
  CIRCCMB29sch2 {S(object,object,object) -> non empty ManySortedSign,
   o(object,object) -> object, P[object,object,object],
   f,h() -> ManySortedSet of NAT}:
 for n being Nat ex S being
  non empty ManySortedSign st S = f().n & P[S,h().n,n]
provided
A1: ex S being non empty ManySortedSign, x being set st S = f().0 & x =
h().0 & P[S, x, 0] and
A2: for n being Nat, S being non empty ManySortedSign, x being set st S
= f().n & x = h().n holds f().(n+1) = S(S,x,n) & h().(n+1) = o(x,n) and
A3: for n being Nat, S being non empty ManySortedSign, x being set st S
= f().n & x = h().n & P[S,x,n] holds P[S(S,x,n), o(x,n), n+1]
proof
  defpred Q[Nat] means ex S being non empty ManySortedSign st S = f().$1 & P[S
  ,h().$1,$1];
A4: for n being Nat st Q[n] holds Q[n+1]
  proof
    let n be Nat;
    given S being non empty ManySortedSign such that
A5: S = f().n and
A6: P[S,h().n,n];
    take S(S,h().n,n);
    h().(n+1) = o(h().n, n) by A2,A5;
    hence thesis by A2,A3,A5,A6;
  end;
A7: Q[ 0 ] by A1;
  thus for n being Nat holds Q[n] from NAT_1:sch 2(A7,A4);
end;

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

scheme :: CircSchR0
  CIRCCMB29sch3 {S0() -> non empty ManySortedSign,
  S(object,object,object) -> non empty ManySortedSign,
  o(object,object) -> object, f,h() -> ManySortedSet of NAT}: for n being
  Nat, x being set st x = h().n holds h().(n+1) = o(x,n)
provided
A1: f().0 = S0() and
A2: for n being Nat, S being non empty ManySortedSign, x being set st S
= f().n & x = h().n holds f().(n+1) = S(S,x,n) & h().(n+1) = o(x,n)
proof
A3: ex S being non empty ManySortedSign, x being set st S = f().0 & x = h().
  0 & Pl[S, x, 0] by A1;
  let n be Nat, x be set;
A4: for n being Nat, S being non empty ManySortedSign, x being set st S = f(
  ).n & x = h().n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
A5: for n being Nat, S being non empty ManySortedSign, x being set st S = f(
  ).n & x = h().n holds f().(n+1) = S(S,x,n) & h().(n+1) = o(x,n) by A2;
  for n being Nat ex S being non empty ManySortedSign st S = f().n & Pl[S,
  h().n,n] from CIRCCMB29sch2(A3,A5,A4);
  then
A6: ex S being non empty ManySortedSign st S = f().n;
  assume x = h().n;
  hence thesis by A2,A6;
end;

scheme :: CircStrExSch
  CIRCCMB29sch4 {S0() -> non empty ManySortedSign, o0()-> object,
    S(object,object,object) -> non empty ManySortedSign,
    o(object,object) -> object, n() -> Nat}:
ex S being non
empty ManySortedSign, f,h being ManySortedSet of NAT st S = f.n() & f.0 = S0()
  & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
  st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) proof
  consider f,h being ManySortedSet of NAT such that
A1: f.0 = S0() & h.0 = o0() and
A2: for n being Nat, S being non empty ManySortedSign, x being set st S
= f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch1;
A3: for n being Nat, S being non empty ManySortedSign, x being set st S = f.
  n & x = h.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
A4: ex S being non empty ManySortedSign, x being set st S = f.0 & x = h.0 &
  Pl[S, x, 0] by A1;
  for n being Nat ex S being non empty ManySortedSign st S = f.n & Pl[S,h.
  n,n] from CIRCCMB29sch2(A4,A2,A3);
  then consider S being non empty ManySortedSign such that
A5: S = f.n();
  take S,f,h;
  thus thesis by A1,A2,A5;
end;

scheme :: CircStrUniqSch
  CIRCCMB29sch5 {S0() -> non empty ManySortedSign, o0()-> object,
  S(object,object,object) -> non empty ManySortedSign,
  o(object,object) -> object, n() -> Nat}:
 for S1,S2 being non empty ManySortedSign
 st (ex f,h being ManySortedSet of NAT st S1 = f.n() &
f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x
being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) & (
ex f,h being ManySortedSet of NAT st S2 = f.n() & f.0 = S0() & h.0 = o0() & for
n being Nat, S being non empty ManySortedSign, x being set st S = f.n & x = h.n
  holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1 = S2 proof
  let S1,S2 be non empty ManySortedSign;
  given f1,h1 being ManySortedSet of NAT such that
A1: S1 = f1.n() and
A2: f1.0 = S0() and
A3: h1.0 = o0() and
A4: for n being Nat, S being non empty ManySortedSign, x being set st S
  = f1.n & x = h1.n holds f1.(n+1) = S(S,x,n) & h1.(n+1) = o(x,n);
A5: for n being Nat, S being non empty ManySortedSign, x being set st S =
  f1.n & x = h1.n holds f1.(n+1) = S(S,x,n) & h1.(n+1) = o(x,n) by A4;
A6: for n being Nat, S being non empty ManySortedSign, x being set st S =
  f1.n & x = h1.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
A7: ex S being non empty ManySortedSign, x being set st S = f1.0 & x = h1.0
  & Pl[S,x,0] by A2;
A8: for n being Nat ex S being non empty ManySortedSign st S = f1.n & Pl[S,
  h1.n,n] from CIRCCMB29sch2(A7,A5,A6);
  given f2,h2 being ManySortedSet of NAT such that
A9: S2 = f2.n() and
A10: f2.0 = S0() and
A11: h2.0 = o0() and
A12: for n being Nat, S being non empty ManySortedSign, x being set st S
  = f2.n & x = h2.n holds f2.(n+1) = S(S,x,n) & h2.(n+1) = o(x,n);
A13: for n being Nat, S being non empty ManySortedSign, x being set st S =
  f2.n & x = h2.n holds f2.(n+1) = S(S,x,n) & h2.(n+1) = o(x,n) by A12;
  defpred A[Nat] means h1.$1 = h2.$1;
A14: for n being Nat, S being non empty ManySortedSign, x being set st S =
  f2.n & x = h2.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
A15: ex S being non empty ManySortedSign, x being set st S = f2.0 & x = h2.0
  & Pl[S,x,0] by A10;
A16: for n being Nat ex S being non empty ManySortedSign st S = f2.n & Pl[S,
  h2.n,n] from CIRCCMB29sch2(A15,A13,A14);
A17: now
    let n be Nat;
    assume
A18: A[n];
    ex S being non empty ManySortedSign st S = f1.n & Pl[S,h1.n,n] by A8;
    then
A19: h1.(n+1) = o(h1.n,n) by A4;
    ex S being non empty ManySortedSign st S = f2.n & Pl[S,h2.n,n] by A16;
    hence A[n+1] by A12,A18,A19;
  end;
  defpred B[Nat] means f1.$1 = f2.$1;
A20: A[ 0 ] by A3,A11;
  for i being Nat holds A[i] from NAT_1:sch 2(A20,A17);
  then for i being object st i in NAT holds h1.i = h2.i;
  then
A21: h1 = h2 by PBOOLE:3;
A22: now
    let n be Nat;
    assume
A23: B[n];
    consider S being non empty ManySortedSign such that
A24: S = f1.n and
    Pl[S,h1.n,n] by A8;
    f1.(n+1) = S(S,h1.n,n) by A4,A24
      .= f2.(n+1) by A12,A21,A23,A24;
    hence B[n+1];
  end;
A25: B[ 0 ] by A2,A10;
  for i being Nat holds B[i] from NAT_1:sch 2(A25,A22);
  hence thesis by A1,A9;
end;

scheme :: CircStrDefSch
  CIRCCMB29sch6 {S0() -> non empty ManySortedSign, o0()-> object,
  S(object,object,object) -> non empty ManySortedSign,
  o(object,object) -> object, n() -> Nat}: (ex S being non
empty ManySortedSign, f,h being ManySortedSet of NAT st S = f.n() & f.0 = S0()
  & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
  st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) & for S1,S2
being non empty ManySortedSign st (ex f,h being ManySortedSet of NAT st S1 = f.
  n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(
n+1) = o(x,n)) & (ex f,h being ManySortedSet of NAT st S2 = f.n() & f.0 = S0()
  & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1 = S2
proof
  thus ex S being non empty ManySortedSign, f,h being ManySortedSet of NAT st
  S = f.n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(
  n+1) = o(x,n) from CIRCCMB29sch4;
  thus for S1,S2 being non empty ManySortedSign st (ex f,h being ManySortedSet
  of NAT st S1 = f.n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non
empty ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n)
& h.(n+1) = o(x,n)) & (ex f,h being ManySortedSet of NAT st S2 = f.n() & f.0 =
S0() & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being
set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1
  = S2 from CIRCCMB29sch5;
end;

scheme :: attrCircStrExSch
  CIRCCMB29sch7 {S0() -> non empty ManySortedSign,
  S(object,object,object) -> non empty
ManySortedSign, o0()-> object, o(object,object) -> object, n() -> Nat}:
ex S being unsplit
gate`1=arity gate`2isBoolean non void non empty non empty strict ManySortedSign
, f,h being ManySortedSet of NAT st S = f.n() & f.0 = S0() & h.0 = o0() & for n
  being Nat, S being non empty ManySortedSign, x being set st S = f.n & x = h.n
  holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)
provided
A1: S0() is unsplit gate`1=arity gate`2isBoolean non void non empty strict and
A2: for S being unsplit gate`1=arity gate`2isBoolean non void strict non
empty ManySortedSign, x being set, n being Nat holds S(S,x,n) is unsplit
gate`1=arity gate`2isBoolean non void non empty strict
proof
  defpred P[non empty ManySortedSign, object] means
$1 is unsplit gate`1=arity
  gate`2isBoolean non void strict;
  defpred Pl[non empty ManySortedSign, object,object] means P[$1,$2];
  consider S being non empty ManySortedSign, f,h being ManySortedSet of NAT
  such that
A3: S = f.n() & f.0 = S0() & h.0 = o0() and
A4: for n being Nat, S being non empty ManySortedSign, x being set st S
= f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch4;
A5: for n being Nat, S being non empty ManySortedSign, x being set st S = f.
  n & x = h.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1] by A2;
A6: ex S being non empty ManySortedSign, x being set st S = f.0 & x = h.0 &
  Pl[S,x,0] by A1,A3;
  for n being Nat ex S being non empty ManySortedSign st S = f.n & Pl[S,h.
  n,n ] from CIRCCMB29sch2(A6,A4,A5);
  then ex S being non empty ManySortedSign st S = f.n() & P[S,n()];
  then reconsider
  S as unsplit gate`1=arity gate`2isBoolean non void strict non
  empty ManySortedSign by A3;
  take S,f,h;
  thus thesis by A3,A4;
end;

scheme :: ManyCellCircStrExSch
  CIRCCMB29sch8 {S0() -> non empty ManySortedSign, S(object,object) -> unsplit
gate`1=arity gate`2isBoolean non void non empty ManySortedSign,
  o0()-> object, o(object,object) -> object, n() -> Nat}:
ex S being unsplit gate`1=arity gate`2isBoolean
non void non empty non empty strict ManySortedSign, f,h being ManySortedSet of
NAT st S = f.n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S +* S(x,n) &
  h.(n+1) = o(x,n)
provided
A1: S0() is unsplit gate`1=arity gate`2isBoolean non void non empty strict
proof
  deffunc Sl(non empty ManySortedSign,set,set) = $1+*S($2,$3);
A2: for S being unsplit gate`1=arity gate`2isBoolean non void strict non
  empty ManySortedSign, x being set, n being Nat holds Sl(S,x,n) is unsplit
  gate`1=arity gate`2isBoolean non void non empty strict;
  thus ex S being unsplit gate`1=arity gate`2isBoolean non void non empty non
empty strict ManySortedSign, f,h being ManySortedSet of NAT st S = f.n() & f.0
  = S0() & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x
  being set st S = f.n & x = h.n holds f.(n+1) = Sl(S,x,n) & h.(n+1) = o(x,n)
  from CIRCCMB29sch7(A1,A2);
end;

scheme :: attrCircStrUniqSch
  CIRCCMB29sch9 {S0() -> non empty ManySortedSign, o0()-> object,
    S(object,object,object) -> non empty ManySortedSign,
    o(object,object) -> object,
    n() -> Nat}:
 for S1,S2 being
  unsplit gate`1=arity gate`2isBoolean non void non empty strict non empty
ManySortedSign st (ex f,h being ManySortedSet of NAT st S1 = f.n() & f.0 = S0()
  & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being set
  st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) & (ex f,h
  being ManySortedSet of NAT st S2 = f.n() & f.0 = S0() & h.0 = o0() & for n
  being Nat, S being non empty ManySortedSign, x being set st S = f.n & x = h.n
  holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1 = S2 proof
  for S1,S2 being non empty ManySortedSign st (ex f,h being ManySortedSet
  of NAT st S1 = f.n() & f.0 = S0() & h.0 = o0() & for n being Nat, S being non
empty ManySortedSign, x being set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n)
& h.(n+1) = o(x,n)) & (ex f,h being ManySortedSet of NAT st S2 = f.n() & f.0 =
S0() & h.0 = o0() & for n being Nat, S being non empty ManySortedSign, x being
set st S = f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n)) holds S1
  = S2 from CIRCCMB29sch5;
  hence thesis;
end;

begin

theorem Th5:
  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;
A1: ((the carrier of S1) \ ((rng the ResultSort of S1)\/(rng the ResultSort
  of S2))) =(InputVertices S1) \ (InnerVertices S2) by XBOOLE_1:41;
  assume S1 tolerates S2;
  then
A2: the ResultSort of S1 tolerates the ResultSort of S2 by CIRCCOMB:def 1;
  InputVertices (S1+*S2) = (the carrier of S1+*S2) \ rng ((the ResultSort
  of S1) +* (the ResultSort of S2)) by CIRCCOMB:def 2
    .= (the carrier of S1)\/(the carrier of S2) \ rng ((the ResultSort of S1
  ) +* (the ResultSort of S2)) by CIRCCOMB:def 2
    .= (the carrier of S1)\/(the carrier of S2) \ ((rng the ResultSort of S1
  )\/rng the ResultSort of S2) by A2,FRECHET:35
    .= ((the carrier of S1) \ ((rng the ResultSort of S1)\/(rng the
ResultSort of S2)))\/ ((the carrier of S2) \ ((rng the ResultSort of S1)\/(rng
  the ResultSort of S2))) by XBOOLE_1:42;
  hence thesis by A1,XBOOLE_1:41;
end;

theorem Th6:
  for X being without_pairs set, Y being Relation holds X \ Y = X
proof
  let X being without_pairs set;
  let Y being Relation;
  X /\ Y = {};
  then X misses Y by XBOOLE_0:def 7;
  hence thesis by XBOOLE_1:83;
end;

theorem
  for X being Relation, Y, Z being set st Z c= Y & Y \ Z is
  without_pairs holds X \ Y = X \ Z
proof
  let X be Relation;
  let Y,Z be set;
  assume
A1: Z c= Y;
  assume Y \ Z is without_pairs;
  then not(ex x being object st x in X /\ (Y \ Z));
  then X /\ (Y \ Z) = {} by XBOOLE_0:7;
  then X misses Y \ Z by XBOOLE_0:def 7;
  then
A2: X \ (Y \ Z) = X by XBOOLE_1:83;
  X \ Y = X \ ( (Y \ Z)\/Z ) by A1,XBOOLE_1:45
    .= X \ Z by A2,XBOOLE_1:41;
  hence thesis;
end;

theorem Th8:
  for X,Z being set, Y being Relation st Z c= Y & X \ Z is
  without_pairs holds X \ Y = X \ Z
proof
  let X,Z being set;
  let Y being Relation;
  assume
A1: Z c= Y;
  assume X \ Z is without_pairs;
  then not(ex x being object st x in (Y \ Z) /\ (X \ Z));
  then (Y \ Z) /\ (X \ Z) = {} by XBOOLE_0:7;
  then Y \ Z misses X \ Z by XBOOLE_0:def 7;
  then
A2: (X \ Z) \ (Y \ Z) = (X \ Z) by XBOOLE_1:83;
  X \ Y = X \ ((Y \ Z) \/ Z) by A1,XBOOLE_1:45
    .= X \ Z by A2,XBOOLE_1:41;
  hence thesis;
end;

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

scheme :: InputOfManyCellCircStr
  CIRCCMB29sch11 {Sn(set) -> unsplit gate`1=arity gate`2isBoolean non void non
  empty ManySortedSign, h() -> ManySortedSet of NAT,
  S(object,object) -> unsplit
  gate`1=arity gate`2isBoolean non void non empty ManySortedSign,
  o(object,object) -> object}:
  for n being Nat holds InputVertices Sn(n+1) = (InputVertices Sn(n))\/((
  InputVertices S(h().(n),n)) \ {h().(n)}) & InnerVertices Sn(n) is Relation &
  InputVertices Sn(n) is without_pairs
provided
A1: InnerVertices Sn(0) is Relation and
A2: InputVertices Sn(0) is without_pairs and
A3: h().(0) in InnerVertices Sn(0) and
A4: for n being Nat, x being set holds InnerVertices S(x,n) is Relation and
A5: for n being Nat, x being set st x = h().(n) holds (InputVertices S(x
,n)) \ {x} is without_pairs and
A6: for n being Nat, S being non empty ManySortedSign, x being set st S
= Sn(n) & x = h().(n) holds Sn(n+1) = S +* S(x,n) & h().(n+1) = o(x,n) & x in
InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n)
proof
  deffunc SN(set) = Sn($1);
A7: for n being Nat, S being non empty ManySortedSign, x being set st S = SN
  (n) & x = h().n holds SN(n+1) = S +* S(x,n) & h().(n+1) = o(x,n) & x in
  InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n) by A6;
  let n be Nat;
A8: for n being Nat, x being set st x = h().n holds (InputVertices S(x,n)) \
  {x} is without_pairs by A5;
A9: SN(0) = SN(0) & h().0 in InnerVertices SN(0) by A3;
A10: for n being Nat, x being set holds InnerVertices S(x,n) is Relation by A4;
  for n being Nat ex S1,S2 being unsplit gate`1=arity gate`2isBoolean non
void non empty ManySortedSign st S1 = SN(n) & S2 = SN(n+1) & InputVertices S2 =
  (InputVertices S1)\/((InputVertices S(h().n,n)) \ {h().n}) & InnerVertices S1
  is Relation & InputVertices S1 is without_pairs from CIRCCMB29sch10(A1,A2,A9,
  A10, A8,A7);
  then ex S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign st S1 = Sn(n) & S2 = Sn(n+1) & InputVertices S2 = (InputVertices
S1)\/((InputVertices S(h().(n),n)) \ {h().(n)}) & InnerVertices S1 is Relation
  & InputVertices S1 is without_pairs;
  hence thesis;
end;

begin :: Defining Many Cell Circuits

scheme
  CIRCCMB29sch12 {S0() -> non empty ManySortedSign, A0() -> non-empty
  MSAlgebra over S0(), o0()-> object,
  S(object,object,object) -> non empty ManySortedSign,
  A(object,object,object,object) -> object,
  o(object,object) -> object}:
ex f,g,h being ManySortedSet of
  NAT st f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being non
empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+
  1) = o(x,n) proof
  deffunc F(set,set) = [[S($2`11,$2`2,$1), A($2`11,$2`12,$2`2,$1)], o($2`2,$1)
  ];
  consider F being Function such that
A1: dom F = NAT & F.0 = [[S0(),A0()],o0()] and
A2: for n being Nat holds F.(n+1) = F(n,F.n) from NAT_1:sch 11;
A3: (F.0)`2 = o0() by A1;
  deffunc h(object) = (F.$1)`2;
  deffunc g(object) = (F.$1)`12;
  deffunc f(object) = (F.$1)`11;
  consider f being ManySortedSet of NAT such that
A4: for n being object st n in NAT holds f.n = f(n) from PBOOLE:sch 4;
  consider h being ManySortedSet of NAT such that
A5: for n being object st n in NAT holds h.n = h(n) from PBOOLE:sch 4;
  consider g being ManySortedSet of NAT such that
A6: for n being object st n in NAT holds g.n = g(n) from PBOOLE:sch 4;
  take f,g,h;
  (F.0)`11 = S0() & (F.0)`12 = A0() by A1,MCART_1:85;
  hence f.0 = S0() & g.0 = A0() & h.0 = o0() by A4,A6,A5,A3;
  let n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over S
  , x be set;
  set x = F.n;
A7: n in NAT by ORDINAL1:def 12;
  then
A8: h.n = x`2 by A5;
  assume that
A9: S = f.n and
A10: A = g.n;
A11: A = x`12 by A6,A7,A10;
  S = x`11 by A4,A7,A9;
  then
A12: F.(n+1) = [[S(S,h.n,n), A(S,A,h.n,n)], o(h.n,n)] by A2,A11,A8;
  then
A13: (F.(n+1))`2 = o(h.n,n);
  (F.(n+1))`11 = S(S,h.n,n) & (F.(n+1))`12 = A(S,A,h.n,n) by A12,MCART_1:85;
  hence thesis by A4,A6,A5,A13;
end;

scheme :: CircSch3
  CIRCCMB29sch13 {S(set,set,set) -> non empty ManySortedSign,
  A(object,object,object,object) -> object,
  o(object,object) -> object,
  P[object,object,object,object],
  f,g,h() -> ManySortedSet of NAT}:
for n being Nat ex S being non empty ManySortedSign, A being non-empty
  MSAlgebra over S st S = f().n & A = g().n & P[S,A,h().n,n]
provided
A1: ex S being non empty ManySortedSign, A being non-empty MSAlgebra
over S, x being set st S = f().0 & A = g().0 & x = h().0 & P[S, A, x, 0] and
A2: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g().(n+1) = A(S,A,x,n) & h().(n+1) = o(x,n) and
A3: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f().n & A = g().n & x = h().n & P[S,A,x
,n] holds P[S(S,x,n), A(S,A,x,n), o(x,n), n+1] and
A4: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
  defpred Q[Nat] means ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S, x being set st S = f().$1 & A = g().$1 & x = h().$1 & P[S,A,x
  ,$1];
A5: for n being Nat st Q[n] holds Q[n+1]
  proof
    let n be Nat;
    given S being non empty ManySortedSign, A being non-empty MSAlgebra over S
    , x being set such that
A6: S = f().n & A = g().n & x = h().n and
A7: P[S,A,x,n];
    take S9 = S(S,x,n);
    reconsider A9 = A(S,A,x,n) as non-empty MSAlgebra over S9 by A4;
    take A9, y = h().(n+1);
    y = o(x,n) by A2,A6;
    hence thesis by A2,A3,A6,A7;
  end;
  let n be Nat;
A8: Q[ 0 ] by A1;
  for n being Nat holds Q[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 = f().n & A = g().n & x = h().n & P[S,A,x,n];
  take S,A;
  thus thesis by A9;
end;

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

scheme :: CircSchU2
  CIRCCMB29sch14 {S(set,set,set) -> non empty ManySortedSign,
    A(object,object,object,object) -> object,
    o(object,object) -> object,
  f1,f2, g1,g2, h1,h2() -> ManySortedSet of NAT}:
  f1() = f2() & g1() = g2() & h1() = h2()
provided
A1: ex S being non empty ManySortedSign, A being non-empty MSAlgebra
over S st S = f1().0 & A = g1().0 and
A2: f1().0 = f2().0 & g1().0 = g2().0 & h1().0 = h2().0 and
A3: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g1().(n+1) = A(S,A,x,n) & h1().(n+1) = o(x,n) and
A4: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g2().(n+1) = A(S,A,x,n) & h2().(n+1) = o(x,n) and
A5: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A6: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g1().(n+1) = A(S,A,x,n) & h1().(n+1) = o(x,n) by A3;
  set f1 = f1(), g1 = g1(), h1 = h1();
A7: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f1.n & A = g1.n & x = h1.n & R[S,A,x,n]
  holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A8: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
  ,n) by A5;
A9: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S,
  x being set st S = f1.0 & A = g1.0 & x = h1.0 & R[S, A, x, 0] by A1;
A10: for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f1.n & A = g1.n & R[S,A,h1.n,n] from CIRCCMB29sch13(A9,
  A6,A7,A8);
  set f2 = f2(), g2 = g2(), h2 = h2();
A11: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f2.n & A = g2.n & x = h2.n & R[S,A,x,n]
  holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
  defpred P[Nat] means h1.$1 = h2.$1;
A12: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g2().(n+1) = A(S,A,x,n) & h2().(n+1) = o(x,n) by A4;
A13: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
  , x being set st S = f2.0 & A = g2.0 & x = h2.0 & R[S, A, x, 0] by A1,A2;
A14: for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f2.n & A = g2.n & R[S,A,h2.n,n] from CIRCCMB29sch13(A13
  ,A12,A11,A8);
A15: now
    let n be Nat;
    assume
A16: P[n];
    ex S being non empty ManySortedSign, A being non-empty MSAlgebra over
    S st S = f1.n & A = g1.n by A10;
    then
A17: h1.(n+1) = o(h1.n,n) by A3;
    ex S being non empty ManySortedSign, A being non-empty MSAlgebra over
    S st S = f2.n & A = g2.n by A14;
    hence P[n+1] by A4,A16,A17;
  end;
A18: P[ 0 ] by A2;
  for i being Nat holds P[i] from NAT_1:sch 2(A18,A15);
  then
A19: for i being object st i in NAT holds h1.i = h2.i;
  defpred P[Nat] means f1.$1 = f2.$1 & g1.$1 = g2.$1;
A20: h1 = h2 by A19,PBOOLE:3;
A21: now
    let n be Nat;
    assume
A22: P[n];
    consider S being non empty ManySortedSign, A being non-empty MSAlgebra
    over S such that
A23: S = f1.n & A = g1.n by A10;
A24: g1.(n+1) = A(S,A,h1.n,n) by A3,A23
      .= g2.(n+1) by A4,A20,A22,A23;
    f1.(n+1) = S(S,h1.n,n) by A3,A23
      .= f2.(n+1) by A4,A20,A22,A23;
    hence P[n+1] by A24;
  end;
A25: P[ 0 ] by A2;
  for i being Nat holds P[i] from NAT_1:sch 2(A25,A21);
  then ( for i being object st i in NAT holds f1.i = f2.i)&
for i being object st i
  in NAT holds g1.i = g2.i;
  hence thesis by A19,PBOOLE:3;
end;

scheme :: CircSchR2
  CIRCCMB29sch15 {S0() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), S(object,object,object) -> non empty ManySortedSign,
  A(object,object,object,object) -> object, o(object,object) -> object,
  f,g,h() -> ManySortedSet of NAT}: for n being
  Nat, S being non empty ManySortedSign, x being set st S = f().n & x = h().n
  holds f().(n+1) = S(S,x,n) & h().(n+1) = o(x,n)
provided
A1: f().0 = S0() & g().0 = A0() and
A2: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g().(n+1) = A(S,A,x,n) & h().(n+1) = o(x,n) and
A3: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A4: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S,
  x being set st S = f().0 & A = g().0 & x = h().0 & R[S,A,x,0] by A1;
  let n be Nat, S be non empty ManySortedSign, x be set;
A5: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f().n & A = g().n & x = h().n & R[S,A,x
  ,n] holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A6: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
  ,n) by A3;
A7: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g().(n+1) = A(S,A,x,n) & h().(n+1) = o(x,n) by A2;
  for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f().n & A = g().n & R[S,A,h().n,n] from CIRCCMB29sch13(
  A4,A7,A5, A6);
  then
A8: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
  st S = f().n & A = g().n;
  assume S = f().n & x = h().n;
  hence thesis by A2,A8;
end;

scheme :: CircuitExSch1
  CIRCCMB29sch16 {S0() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object, o(object,object) -> object,
n() -> Nat}: ex S being non empty
  ManySortedSign, A being non-empty MSAlgebra over S, f,g,h being ManySortedSet
of NAT st S = f.n() & A = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n
being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+
  1) = A(S,A,x,n) & h.(n+1) = o(x,n)
provided
A1: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A2: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
  ,n) by A1;
  consider f,g,h being ManySortedSet of NAT such that
A3: f.0 = S0() & g.0 = A0() & h.0 = o0() and
A4: for n being Nat, S being non empty ManySortedSign, 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) =
  S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch12;
A5: for n being Nat, S being non empty ManySortedSign, A being non-empty
  MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
  holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A6: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S,
  x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A3;
  for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A6,A4,
  A5,A2);
  then consider
  S being non empty ManySortedSign, A being non-empty MSAlgebra over
  S such that
A7: S = f.n() & A = g.n();
  take S,A,f,g,h;
  thus thesis by A3,A4,A7;
end;

scheme :: CircuitExSch2
  CIRCCMB29sch17 {S0,Sn() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), o0()-> object,
S(object,object,object) -> non empty ManySortedSign,
A(object,object,object,object) -> object,
o(object,object) -> object, n() -> Nat}: ex A being non-empty
MSAlgebra over Sn(), f,g,h being ManySortedSet of NAT st Sn() = f.n() & A = g.n
() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o
  (x,n)
provided
A1: ex f,h being ManySortedSet of NAT st Sn() = f.n() & f.0 = S0() & h.0
= o0() & for n being Nat, S being non empty ManySortedSign, x being set st S =
f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) and
A2: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A3: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
  ,n) by A2;
  consider f,g,h being ManySortedSet of NAT such that
A4: f.0 = S0() & g.0 = A0() & h.0 = o0() and
A5: for n being Nat, S being non empty ManySortedSign, 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) =
  S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch12;
A6: for n being Nat, S being non empty ManySortedSign, A being non-empty
  MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
  holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A7: for n being Nat, S being non empty ManySortedSign, A being non-empty
  MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
  holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A8: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
  , x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A4;
A9: for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A8,A5
  ,A7,A3);
A10: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
  , x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A4;
  for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A10,A5
  ,A6,A3);
  then consider
  S being non empty ManySortedSign, A being non-empty MSAlgebra over
  S such that
A11: S = f.n() and
A12: A = g.n();
  consider f1,h1 being ManySortedSet of NAT such that
A13: Sn() = f1.n() and
A14: f1.0 = S0() and
A15: h1.0 = o0() and
A16: for n being Nat, S being non empty ManySortedSign, x being set st S
  = f1.n & x = h1.n holds f1.(n+1) = S(S,x,n) & h1.(n+1) = o(x,n) by A1;
A17: for n being Nat, S being non empty ManySortedSign, x being set st S =
  f1.n & x = h1.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
  defpred P[Nat] means h1.$1 = h.$1;
A18: ex S being non empty ManySortedSign, x being set st S = f1.0 & x = h1.0
  & Pl[S,x,0] by A14;
A19: for n being Nat ex S being non empty ManySortedSign st S = f1.n & Pl[S,
  h1.n,n] from CIRCCMB29sch2(A18,A16,A17);
A20: now
    let n be Nat;
    assume
A21: P[n];
    ex S being non empty ManySortedSign st S = f1.n by A19;
    then
A22: h1.(n+1) = o(h1.n,n) by A16;
    ex S being non empty ManySortedSign, A being non-empty MSAlgebra over
    S st S = f.n & A = g.n by A9;
    hence P[n+1] by A5,A21,A22;
  end;
A23: P[ 0 ] by A4,A15;
A24: for i being Nat holds P[i] from NAT_1:sch 2(A23,A20);
  defpred P[Nat] means f1.$1 = f.$1;
  for i being object st i in NAT holds h1.i = h.i by A24;
  then
A25: h1 = h by PBOOLE:3;
A26: now
    let n be Nat;
    consider S 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 P[n];
    then f1.(n+1) = S(S,h1.n,n) by A16,A27
      .= f.(n+1) by A5,A25,A27,A28;
    hence P[n+1];
  end;
A29: P[ 0 ] by A4,A14;
A30: for i being Nat holds P[i] from NAT_1:sch 2(A29,A26);
  then for i being object st i in NAT holds f1.i = f.i;
  then f1 = f by PBOOLE:3;
  then reconsider A as non-empty MSAlgebra over Sn() by A13,A11;
  take A,f,g,h;
  thus thesis by A4,A5,A13,A30,A12;
end;

scheme :: CircuitUniqSch
  CIRCCMB29sch18 {S0,Sn() -> non empty ManySortedSign, A0() -> non-empty
MSAlgebra over S0(), o0()-> object,
  S(object,object,object) -> non empty ManySortedSign,
  A(object,object,object,object) -> object,
  o(object,object) -> object, n() -> Nat}:
 for A1,A2 being
non-empty MSAlgebra over Sn() st (ex f,g,h being ManySortedSet of NAT st Sn() =
f.n() & A1 = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S
being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x
,n) & h.(n+1) = o(x,n)) & (ex f,g,h being ManySortedSet of NAT st Sn() = f.n()
& A2 = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being
non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h
  .(n+1) = o(x,n)) holds A1 = A2
provided
A1: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A2: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
  ,n) by A1;
  let A1,A2 be non-empty MSAlgebra over Sn();
  given f1,g1,h1 being ManySortedSet of NAT such that
  Sn() = f1.n() and
A3: A1 = g1.n() and
A4: f1.0 = S0() & g1.0 = A0() and
A5: h1.0 = o0() and
A6: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g1.(n+1) = A(S,A,x,n) & h1.(n+1) = o(x,n);
A7: ex S being non empty ManySortedSign, 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
  Sn() = f2.n() and
A8: A2 = g2.n() and
A9: f2.0 = S0() & g2.0 = A0() & h2.0 = o0() and
A10: for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g2.(n+1) = A(S,A,x,n) & h2.(n+1) = o(x,n);
A11: f1.0 = f2.0 & g1.0 = g2.0 & h1.0 = h2.0 by A4,A5,A9;
  f1 = f2 & g1 = g2 & h1 = h2 from CIRCCMB29sch14(A7,A11,A6,A10, A2);
  hence thesis by A3,A8;
end;

scheme
  CIRCCMB29sch19 {S0, Sn() -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign, A0() -> Boolean gate`2=den strict Circuit of
S0(), S(object,object,object) -> non empty ManySortedSign,
   A(object,object,object,object) -> object, o0()-> object,
   o(object,object) -> object, n() -> Nat}:
  ex A being Boolean gate`2=den strict
Circuit of Sn(), f,g,h being ManySortedSet of NAT st Sn() = f.n() & A = g.n() &
  f.0 = S0() & g.0 = A0() & h.0 = o0() & for n being Nat, S being non empty
ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o
  (x,n)
provided
A1: for S being unsplit gate`1=arity gate`2isBoolean non void strict non
empty ManySortedSign, x being set, n being Nat holds S(S,x,n) is unsplit
gate`1=arity gate`2isBoolean non void strict and
A2: ex f,h being ManySortedSet of NAT st Sn() = f.n() & f.0 = S0() & h.0
= o0() & for n being Nat, S being non empty ManySortedSign, x being set st S =
f.n & x = h.n holds f.(n+1) = S(S,x,n) & h.(n+1) = o(x,n) and
A3: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n) and
A4: for S,S1 being unsplit gate`1=arity gate`2isBoolean non void strict
non empty ManySortedSign, A being Boolean gate`2=den strict Circuit of S for x
being set, n being Nat st S1 = S(S,x,n) holds A(S,A,x,n) is Boolean gate`2=den
strict Circuit of S1
proof
A5: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
  ,n) by A3;
  defpred P[object,object,Nat] means
  ex S being unsplit gate`1=arity gate`2isBoolean
  non void strict non empty ManySortedSign, A being Boolean gate`2=den strict
  Circuit of S st S = $1 & A = $2;
  consider f,g,h being ManySortedSet of NAT such that
A6: f.0 = S0() & g.0 = A0() & h.0 = o0() and
A7: for n being Nat, S being non empty ManySortedSign, 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) =
  S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch12;
A8: for n being Nat, S being non empty ManySortedSign, A being non-empty
  MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
  holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1];
A9: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
  , x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A6;
A10: for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A9,A7
  ,A8,A5);
  defpred R[object,object,object,Nat] means P[$1,$2,$4];
A11: for n being Nat, S being non empty ManySortedSign, A being non-empty
  MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
  holds R[S(S,x,n), A(S,A,x,n), o(x,n), n+1]
  proof
    let n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over
    S;
    let x be set;
    assume that
    S = f.n and
    A = g.n and
    x = h.n and
A12: P[S,A,n];
    reconsider S as unsplit gate`1=arity gate`2isBoolean non void non empty
    strict non empty ManySortedSign by A12;
    reconsider A as Boolean gate`2=den strict Circuit of S by A12;
    reconsider S1 = S(S,x,n) as unsplit gate`1=arity gate`2isBoolean non void
    non empty strict non empty ManySortedSign by A1;
    A(S,A,x,n) is Boolean gate`2=den strict Circuit of S1 by A4;
    hence thesis;
  end;
A13: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
  , x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A6;
  for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A13,A7
  ,A11,A5);
  then consider
  S being non empty ManySortedSign, A being non-empty MSAlgebra over
  S such that
A14: S = f.n() and
A15: A = g.n() and
A16: P[S,A,n()];
  consider f1,h1 being ManySortedSet of NAT such that
A17: Sn() = f1.n() and
A18: f1.0 = S0() and
A19: h1.0 = o0() and
A20: for n being Nat, S being non empty ManySortedSign, x being set st S
  = f1.n & x = h1.n holds f1.(n+1) = S(S,x,n) & h1.(n+1) = o(x,n) by A2;
A21: for n being Nat, S being non empty ManySortedSign, x being set st S =
  f1.n & x = h1.n & Pl[S,x,n] holds Pl[S(S,x,n), o(x,n), n+1];
  defpred P[Nat] means h1.$1 = h.$1;
A22: ex S being non empty ManySortedSign, x being set st S = f1.0 & x = h1.0
  & Pl[S,x,0] by A18;
A23: for n being Nat ex S being non empty ManySortedSign st S = f1.n & Pl[S,
  h1.n,n] from CIRCCMB29sch2(A22,A20,A21);
A24: now
    let n be Nat;
    assume
A25: P[n];
    ex S being non empty ManySortedSign st S = f1.n by A23;
    then
A26: h1.(n+1) = o(h1.n,n) by A20;
    ex S being non empty ManySortedSign, A being non-empty MSAlgebra over
    S st S = f.n & A = g.n by A10;
    hence P[n+1] by A7,A25,A26;
  end;
A27: P[ 0 ] by A6,A19;
A28: for i being Nat holds P[i] from NAT_1:sch 2(A27,A24);
  defpred P[Nat] means f1.$1 = f.$1;
  for i being object st i in NAT holds h1.i = h.i by A28;
  then
A29: h1 = h by PBOOLE:3;
A30: now
    let n be Nat;
    consider S 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 P[n];
    then f1.(n+1) = S(S,h1.n,n) by A20,A31
      .= f.(n+1) by A7,A29,A31,A32;
    hence P[n+1];
  end;
A33: P[ 0 ] by A6,A18;
A34: for i being Nat holds P[i] from NAT_1:sch 2(A33,A30);
  then for i being object st i in NAT holds f1.i = f.i;
  then f1 = f by PBOOLE:3;
  then reconsider A as Boolean gate`2=den strict Circuit of Sn() by A17,A14,A16
;
  take A,f,g,h;
  thus thesis by A6,A7,A17,A34,A15;
end;

definition
  let S be non empty ManySortedSign;
  let A be object such that
A1: A is non-empty MSAlgebra over S;
  func MSAlg(A,S) -> non-empty MSAlgebra over S means
  :Def1:
  it = A;
  existence by A1;
  uniqueness;
end;

scheme :: ManyCellCircuitExSch
  CIRCCMB29sch20 {S0, Sn() -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign, A0() -> Boolean gate`2=den strict Circuit of
  S0(),
  S(object,object) -> unsplit gate`1=arity gate`2isBoolean non void non empty
ManySortedSign, A(object,object) -> object, o0()-> object,
o(object,object) -> object, n() -> Nat}:
ex A being Boolean gate`2=den strict Circuit of Sn(), f,g,h being ManySortedSet
of NAT st Sn() = f.n() & A = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() & for
  n being Nat, S being non empty ManySortedSign, A1 being non-empty MSAlgebra
  over S for x being set, A2 being non-empty MSAlgebra over S(x,n) st S = f.n &
A1 = g.n & x = h.n & A2 = A(x,n) holds f.(n+1) = S +* S(x,n) & g.(n+1) = A1 +*
  A2 & h.(n+1) = o(x,n)
provided
A1: ex f,h being ManySortedSet of NAT st Sn() = f.n() & f.0 = S0() & h.0
= o0() & for n being Nat, S being non empty ManySortedSign, x being set st S =
f.n & x = h.n holds f.(n+1) = S +* S(x,n) & h.(n+1) = o(x,n) and
A2: for x being set, n being Nat holds A(x,n) is Boolean gate`2=den
strict Circuit of S(x,n)
proof
  deffunc Sl(non empty ManySortedSign,set,set) = $1+*S($2,$3);
  consider f1,h1 being ManySortedSet of NAT such that
A3: Sn() = f1.n() and
A4: f1.0 = S0() and
A5: h1.0 = o0() and
A6: for n being Nat, S being non empty ManySortedSign, x being set st S
  = f1.n & x = h1.n holds f1.(n+1) = Sl(S,x,n) & h1.(n+1) = o(x,n) by A1;
  defpred P[object,object,Nat] means $3 <> 0 implies
  ex S being unsplit gate`1=arity
  gate`2isBoolean non void strict non empty ManySortedSign, A being Boolean
  gate`2=den strict Circuit of S st S = $1 & A = $2;
  deffunc Al(non empty ManySortedSign,non-empty MSAlgebra over $1, set,set) =
  $2+*MSAlg(A($3,$4),S($3,$4));
A7: for S being non empty ManySortedSign, A being non-empty MSAlgebra over
S for x being set, n being Nat holds Al(S,A,x,n) is non-empty MSAlgebra over Sl
  (S,x,n);
A8: for n being Nat, S being non empty ManySortedSign, x being set st S =
  f1.n & x = h1.n & Pl[S,x,n] holds Pl[Sl(S,x,n), o(x,n), n+1];
  consider f,g,h being ManySortedSet of NAT such that
A9: f.0 = S0() & g.0 = A0() & h.0 = o0() and
A10: for n being Nat, S being non empty ManySortedSign, 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) =
  Sl(S,x,n) & g.(n+1) = Al(S,A,x,n) & h.(n+1) = o(x,n) from CIRCCMB29sch12;
A11: for n being Nat, S being non empty ManySortedSign, A being non-empty
  MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
  holds R[Sl(S,x,n), Al(S,A,x,n), o(x, n), n+1];
A12: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
  , x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A9;
A13: for n being Nat ex S being non empty ManySortedSign, A being non-empty
  MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A12,
  A10
  ,A11,A7);
  defpred P[Nat] means h1.$1 = h.$1;
A14: ex S being non empty ManySortedSign, x being set st S = f1.0 & x = h1.0
  & Pl[S,x,0] by A4;
A15: for n being Nat ex S being non empty ManySortedSign st S = f1.n & Pl[S,
  h1.n,n] from CIRCCMB29sch2(A14,A6,A8);
A16: now
    let n be Nat;
    assume
A17: P[n];
    ex S being non empty ManySortedSign st S = f1.n by A15;
    then
A18: h1.(n+1) = o(h1.n,n) by A6;
    ex S being non empty ManySortedSign, A being non-empty MSAlgebra over
    S st S = f.n & A = g.n by A13;
    hence P[n+1] by A10,A17,A18;
  end;
A19: P[ 0 ] by A9,A5;
A20: for i being Nat holds P[i] from NAT_1:sch 2(A19,A16);
  defpred P[Nat] means f1.$1 = f.$1;
  for i being object st i in NAT holds h1.i = h.i by A20;
  then
A21: h1 = h by PBOOLE:3;
A22: now
    let n be Nat;
    consider S 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 P[n];
    then f1.(n+1) = S+*S(h1.n,n) by A6,A23
      .= f.(n+1) by A10,A21,A23,A24;
    hence P[n+1];
  end;
  defpred R[object,object,object,Nat] means P[$1,$2,$4];
A25: for n being Nat, S being non empty ManySortedSign, A being non-empty
  MSAlgebra over S for x being set st S = f.n & A = g.n & x = h.n & R[S,A,x,n]
  holds R[Sl(S,x,n), Al(S,A,x,n), o(x, n), n+1]
  proof
    let n be Nat, S be non empty ManySortedSign, A be non-empty MSAlgebra over
    S;
    let x be set;
    assume that
A26: S = f.n & A = g.n and
    x = h.n and
A27: P[S,A,n] and
    n+1 <> 0;
    per cases;
    suppose
A28:  n = 0;
      reconsider A2 = A(x,0) as Boolean gate`2=den strict Circuit of S(x,0) by
A2;
      A0()+*MSAlg(A(x,0),S(x,0)) = A0()+*A2 by Def1;
      hence thesis by A9,A26,A28;
    end;
    suppose
A29:  n <> 0;
      then reconsider
      S as unsplit gate`1=arity gate`2isBoolean non void non empty
      strict non empty ManySortedSign by A27;
      reconsider A as Boolean gate`2=den strict Circuit of S by A27,A29;
      reconsider A9 = A(x,n) as Boolean gate`2=den strict Circuit of S(x,n) by
A2;
      A+*MSAlg(A(x,n),S(x,n)) = A+*A9 by Def1;
      hence thesis;
    end;
  end;
A30: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
  , x being set st S = f.0 & A = g.0 & x = h.0 & R[S,A,x,0] by A9;
  for n being Nat ex S being non empty ManySortedSign, A being non-empty
  MSAlgebra over S st S = f.n & A = g.n & R[S,A,h.n,n] from CIRCCMB29sch13(A30,
  A10
  ,A25,A7);
  then consider
  S being non empty ManySortedSign, A being non-empty MSAlgebra over
  S such that
A31: S = f.n() and
A32: A = g.n() and
A33: P[S,A,n()];
A34: P[ 0 ] by A9,A4;
A35: for i being Nat holds P[i] from NAT_1:sch 2(A34,A22);
  then for i being object st i in NAT holds f1.i = f.i;
  then f1 = f by PBOOLE:3;
  then reconsider A as Boolean gate`2=den strict Circuit of Sn() by A9,A3,A31
,A32,A33;
  take A,f,g,h;
  thus Sn() = f.n() & A = g.n() & f.0 = S0() & g.0 = A0() & h.0 = o0() by A9,A3
,A35,A32;
  let n being Nat, S being non empty ManySortedSign, A1 being non-empty
  MSAlgebra over S;
  let x being set, A2 being non-empty MSAlgebra over S(x,n);
  assume
A36: S = f.n & A1 = g.n & x = h.n & A2 = A(x,n);
  A2 = MSAlg(A2, S(x,n)) by Def1;
  hence thesis by A10,A36;
end;

scheme :: attrCircuitUniqSch
  CIRCCMB29sch21 {S0() -> non empty ManySortedSign, Sn() -> unsplit
gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign, A0() ->
  non-empty MSAlgebra over S0(), o0()-> object,
  S(object,object,object) -> non empty ManySortedSign,
  A(object,object,object,object) -> object,
  o(object,object) -> object, n() -> Nat}:
  for A1,A2 being Boolean gate`2=den strict Circuit of Sn() st
(ex f,g,h being
ManySortedSet of NAT st Sn() = f.n() & A1 = g.n() & f.0 = S0() & g.0 = A0() & h
  .0 = o0() & for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) & (ex f,g,h being
ManySortedSet of NAT st Sn() = f.n() & A2 = g.n() & f.0 = S0() & g.0 = A0() & h
  .0 = o0() & for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) holds A1 = A2
provided
A1: for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra
over S(S,x,n)
proof
A2: for S being non empty ManySortedSign, A being non-empty MSAlgebra over S
for x being set, n being Nat holds A(S,A,x,n) is non-empty MSAlgebra over S(S,x
  ,n) by A1;
  for A1,A2 being non-empty MSAlgebra over Sn() st (ex f,g,h being
ManySortedSet of NAT st Sn() = f.n() & A1 = g.n() & f.0 = S0() & g.0 = A0() & h
  .0 = o0() & for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) & (ex f,g,h being
ManySortedSet of NAT st Sn() = f.n() & A2 = g.n() & f.0 = S0() & g.0 = A0() & h
  .0 = o0() & for n being Nat, S being non empty ManySortedSign, 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) = S(S,x,n) & g.(n+1) = A(S,A,x,n) & h.(n+1) = o(x,n)) holds A1 = A2
  from CIRCCMB29sch18(A2);
  hence thesis;
end;

begin :: Correctness of Many Cell Circuit

theorem
  for S1,S2,S being non void Circuit-like non empty ManySortedSign st
  InnerVertices S1 misses InputVertices S2 & S = S1+*S2 for C1 being non-empty
  Circuit of S1, C2 being non-empty Circuit of S2 for C being non-empty Circuit
of S st C1 tolerates C2 & C = C1+*C2 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 void Circuit-likenon empty ManySortedSign such that
A1: InnerVertices S1 misses InputVertices S2 & S = S1+*S2;
  let C1 be non-empty Circuit of S1;
  let C2 be non-empty Circuit of S2;
  let C be non-empty Circuit of S such that
A2: C1 tolerates C2 and
A3: C = C1+*C2;
  let s2 be State of C2;
  let s be State of C such that
A4: s2 = s|the carrier of S2;
  the Sorts of C1 tolerates the Sorts of C2 by A2,CIRCCOMB:def 3;
  then reconsider s1 = s|the carrier of S1 as State of C1 by A3,CIRCCOMB:26;
  dom Following s2 = the carrier of S2 & Following s = (Following s1)+*(
  Following s2) by A1,A2,A3,A4,CIRCCOMB:32,CIRCUIT1:3;
  hence thesis by FUNCT_4:23;
end;

theorem Th10:
  for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for C1
  being non-empty Circuit of S1, C2 being non-empty Circuit of S2 for C being
non-empty Circuit of S st C1 tolerates C2 & C = C1+*C2 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 void Circuit-likenon empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & S = S1+*S2;
  let C1 be non-empty Circuit of S1;
  let C2 be non-empty Circuit of S2;
  let C be non-empty Circuit of S such that
A2: C1 tolerates C2 and
A3: C = C1+*C2;
  let s1 be State of C1;
  let s be State of C such that
A4: s1 = s|the carrier of S1;
  the Sorts of C1 tolerates the Sorts of C2 by A2,CIRCCOMB:def 3;
  then reconsider s2 = s|the carrier of S2 as State of C2 by A3,CIRCCOMB:26;
  dom Following s1 = the carrier of S1 & Following s = (Following s2)+*(
  Following s1) by A1,A2,A3,A4,CIRCCOMB:33,CIRCUIT1:3;
  hence thesis by FUNCT_4:23;
end;

theorem
  for S1,S2,S being non void Circuit-like non empty ManySortedSign st
  InnerVertices S1 misses InputVertices S2 & S = S1+*S2 for C1 being non-empty
  Circuit of S1, C2 being non-empty Circuit of S2 for C being non-empty Circuit
  of S st C1 tolerates C2 & C = C1+*C2 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 void Circuit-likenon empty ManySortedSign such that
A1: InnerVertices S1 misses InputVertices S2 and
A2: S = S1+*S2;
  let C1 be non-empty Circuit of S1;
  let C2 be non-empty Circuit of S2;
  let C be non-empty Circuit of S such that
A3: C1 tolerates C2 & C = C1+*C2;
  let s1 be State of C1;
  let s2 be State of C2;
  let s be State of C such that
A4: s1 = s|the carrier of S1 & s2 = s|the carrier of S2 and
A5: s1 is stable and
A6: s2 is stable;
  dom s = the carrier of S & the carrier of S = (the carrier of S1) \/ the
  carrier of S2 by A2,CIRCCOMB:def 2,CIRCUIT1:3;
  then s = s1+*s2 by A4,FUNCT_4:70;
  then s = (Following s1) +* s2 by A5
    .= (Following s1) +* (Following s2) by A6
    .= Following s by A1,A2,A3,A4,CIRCCOMB:32;
  hence s = Following s;
end;

theorem
  for S1,S2,S being non void Circuit-like non empty ManySortedSign st
  InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for C1 being non-empty
  Circuit of S1, C2 being non-empty Circuit of S2 for C being non-empty Circuit
  of S st C1 tolerates C2 & C = C1+*C2 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 void Circuit-likenon empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 and
A2: S = S1+*S2;
  let C1 be non-empty Circuit of S1;
  let C2 be non-empty Circuit of S2;
  let C be non-empty Circuit of S such that
A3: C1 tolerates C2 & C = C1+*C2;
  let s1 be State of C1;
  let s2 be State of C2;
  let s be State of C such that
A4: s1 = s|the carrier of S1 & s2 = s|the carrier of S2 and
A5: s1 is stable and
A6: s2 is stable;
  dom s = the carrier of S & the carrier of S = (the carrier of S1) \/ the
  carrier of S2 by A2,CIRCCOMB:def 2,CIRCUIT1:3;
  then s = s2+*s1 by A4,FUNCT_4:70;
  then s = (Following s2) +* s1 by A6
    .= (Following s2) +* (Following s1) by A5
    .= Following s by A1,A2,A3,A4,CIRCCOMB:33;
  hence s = Following s;
end;

theorem Th13:
  for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for A1
  being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A,
s1 be State of A1 st s1 = s|the carrier of S1
for n being natural Number holds
Following(s, n)|the carrier of S1 = Following(s1, n)
proof
  let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & S = S1+*S2;
  let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
  let A be non-empty Circuit of S such that
A2: A1 tolerates A2 & A = A1+*A2;
  let s be State of A, s1 be State of A1 such that
A3: s1 = s|the carrier of S1;
  let n be natural Number;
A0: n is Nat by TARSKI:1;
  defpred P[Nat] means Following(s, $1)|the carrier of S1 = Following(s1, $1);
A4: now
    let n be Nat;
A5: Following(s, n+1) = Following Following(s, n) & Following Following(s1
    , n) = Following(s1, n+1) by FACIRC_1:12;
    assume P[n];
    hence P[n+1] by A1,A2,A5,Th10;
  end;
  Following(s, 0)|the carrier of S1 = s1 by A3,FACIRC_1:11
    .= Following(s1, 0) by FACIRC_1:11;
  then
A6: P[ 0 ];
  for n being Nat holds P[n] from NAT_1:sch 2(A6,A4);
  hence thesis by A0;
end;

theorem Th14:
  for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S2 misses InnerVertices S1 & S = S1+*S2 for A1
  being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A,
s2 be State of A2 st s2 = s|the carrier of S2 for n being Nat holds Following(s
  , n)|the carrier of S2 = Following(s2, n)
proof
  let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S2 misses InnerVertices S1 and
A2: S = S1+*S2;
  let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
  let A be non-empty Circuit of S such that
A3: A1 tolerates A2 and
A4: A = A1+*A2;
  S1 tolerates S2 by A3,CIRCCOMB:def 3;
  then
A5: S = S2+*S1 by A2,CIRCCOMB:5;
  A = A2+*A1 by A3,A4,CIRCCOMB:22;
  hence thesis by A1,A3,A5,Th13,CIRCCOMB:19;
end;

theorem Th15:
  for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for A1
  being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
  non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s being State of A
  for s1 being State of A1 st s1 = s|the carrier of S1 & s1 is stable 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 void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 and
A2: S = S1+*S2;
A3: the carrier of S = (the carrier of S1)\/the carrier of S2 by A2,
CIRCCOMB:def 2;
  let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
  let A be non-empty Circuit of S such that
A4: A1 tolerates A2 and
A5: A = A1+*A2;
  let s be State of A;
  let s1 be State of A1 such that
A6: s1 = s|the carrier of S1 and
A7: s1 is stable;
  let s2 be State of A2 such that
A8: s2 = s|the carrier of S2;
A9: now
    let a be object;
    assume a in the carrier of S2;
    then reconsider v = a as Vertex of S2;
    reconsider vv = v as Vertex of S by A3,XBOOLE_0:def 3;
A10: v in InputVertices S2 & not v in InnerVertices S1 implies v in (
    InputVertices S2)\InnerVertices S1 by XBOOLE_0:def 5;
A11: S1 tolerates S2 by A4,CIRCCOMB:def 3;
A12: now
      assume that
A13:  v in InputVertices S2 and
A14:  v in InnerVertices S1;
      reconsider v1 = v as Vertex of S1 by A14;
      thus (Following s).vv = (Following s1).vv by A2,A4,A5,A6,A14,CIRCCOMB:31
        .= s1.v by A7
        .= s.v1 by A6,FUNCT_1:49
        .= s2.v by A8,FUNCT_1:49
        .= (Following s2).vv by A13,CIRCUIT2:def 5;
    end;
    the carrier of S2 = InnerVertices S2 \/ InputVertices S2 & (
InputVertices S1 )\InnerVertices S2 = InputVertices S1 by A1,XBOOLE_1:45,83;
    then v in InnerVertices S2 or v in InputVertices S2 & (v in InnerVertices
    S1 or not v in InnerVertices S1) & InputVertices S = (InputVertices S1)\/((
    InputVertices S2)\InnerVertices S1) by A2,A11,Th5,XBOOLE_0:def 3;
    then
A15: vv in InnerVertices S2 or v in InputVertices S or v in InputVertices
    S2 & v in InnerVertices S1 by A10,XBOOLE_0:def 3;
    thus ((Following s)|the carrier of S2).a = (Following s).v by FUNCT_1:49
      .= (Following s2).a by A2,A4,A5,A8,A12,A15,CIRCCOMB:31;
  end;
  dom Following s = the carrier of S by CIRCUIT1:3;
  then dom Following s2 = the carrier of S2 & dom ((Following s)|the carrier
  of S2) = the carrier of S2 by A3,CIRCUIT1:3,RELAT_1:62,XBOOLE_1:7;
  hence thesis by A9,FUNCT_1:2;
end;

theorem
  for S1,S2,S being non void Circuit-like non empty ManySortedSign st
S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being non-empty Circuit of
  S2 for A being non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s
  being State of A for s1 being State of A1 st s1 = s|the carrier of S1 & s1 is
  stable 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 void Circuit-like non empty ManySortedSign such that
A1: S = S1+*S2;
  let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
  let A be non-empty Circuit of S such that
A2: A1 tolerates A2 and
A3: A = A1+*A2;
  S1 tolerates S2 by A2,CIRCCOMB:def 3;
  then
A4: InnerVertices S = (InnerVertices S1) \/ InnerVertices S2 by A1,CIRCCOMB:11;
  let s be State of A;
  let s1 be State of A1 such that
A5: s1 = s|the carrier of S1 and
A6: s1 = Following s1;
  let s2 be State of A2 such that
A7: s2 = s|the carrier of S2 and
A8: s2 = Following s2;
A9: the carrier of S = (the carrier of S1) \/ the carrier of S2 by A1,
CIRCCOMB:def 2;
A10: now
    let x be object;
    assume x in the carrier of S;
    then reconsider v = x as Vertex of S;
    the carrier of S = (InputVertices S) \/ InnerVertices S by XBOOLE_1:45;
    then v in InputVertices S or v in InnerVertices S by XBOOLE_0:def 3;
    then
    v in InputVertices S & v in the carrier of S1 or v in InputVertices S
& v in the carrier of S2 or v in InnerVertices S1 or v in InnerVertices S2 by
A4,A9,XBOOLE_0:def 3;
    then (Following s).v = s1.v & v in the carrier of S1 or (Following s).v =
    s2.v & v in the carrier of S2 by A1,A2,A3,A5,A6,A7,A8,CIRCCOMB:31;
    hence s.x = (Following s).x by A5,A7,FUNCT_1:49;
  end;
  dom Following s = the carrier of S & dom s = the carrier of S by CIRCUIT1:3;
  hence s = Following s by A10,FUNCT_1:2;
end;

theorem Th17:
  for S1,S2,S being non void Circuit-like non empty
  ManySortedSign st S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being
non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 &
  A = A1+*A2 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 void Circuit-like non empty ManySortedSign such that
A1: S = S1+*S2;
A2: the carrier of S = (the carrier of S1) \/ the carrier of S2 by A1,
CIRCCOMB:def 2;
  let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
  let A be non-empty Circuit of S such that
A3: A1 tolerates A2 & A = A1+*A2;
  let s be State of A such that
A4: s = Following s;
  hereby
    let s1 be State of A1 such that
A5: s1 = s|the carrier of S1;
A6: now
      let x be object;
      assume x in the carrier of S1;
      then reconsider v = x as Vertex of S1;
      reconsider v9 = v as Vertex of S by A2,XBOOLE_0:def 3;
      the carrier of S1 = (InputVertices S1) \/ InnerVertices S1 by XBOOLE_1:45
;
      then v in InputVertices S1 or v9 in InnerVertices S1 by XBOOLE_0:def 3;
      then s1.v = (Following s1).v or s.v9 = (Following s1).v by A1,A3,A4,A5,
CIRCCOMB:31,CIRCUIT2:def 5;
      hence s1.x = (Following s1).x by A5,FUNCT_1:49;
    end;
    dom s1 = the carrier of S1 & dom Following s1 = the carrier of S1 by
CIRCUIT1:3;
    then s1 = Following s1 by A6,FUNCT_1:2;
    hence s1 is stable;
  end;
  let s2 be State of A2 such that
A7: s2 = s|the carrier of S2;
A8: now
    let x be object;
    assume x in the carrier of S2;
    then reconsider v = x as Vertex of S2;
    reconsider v9 = v as Vertex of S by A2,XBOOLE_0:def 3;
    the carrier of S2 = (InputVertices S2) \/ InnerVertices S2 by XBOOLE_1:45;
    then v in InputVertices S2 or v9 in InnerVertices S2 by XBOOLE_0:def 3;
    then s2.v = (Following s2).v or s.v9 = (Following s2).v by A1,A3,A4,A7,
CIRCCOMB:31,CIRCUIT2:def 5;
    hence s2.x = (Following s2).x by A7,FUNCT_1:49;
  end;
  dom s2 = the carrier of S2 & dom Following s2 = the carrier of S2 by
CIRCUIT1:3;
  hence s2 = Following s2 by A8,FUNCT_1:2;
end;

theorem Th18:
  for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for A1
  being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for s1 being State of A1
, s2 being State of A2, s being State of A st s1 = s|the carrier of S1 & s2 = s
  |the carrier of S2 & s1 is stable for n being Nat holds Following(s, n)|the
  carrier of S2 = Following(s2, n)
proof
  let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & S = S1+*S2;
  let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
  let A be non-empty Circuit of S such that
A2: A1 tolerates A2 and
A3: A = A1+*A2;
  let s1 be State of A1, s2 be State of A2, s be State of A such that
A4: s1 = s|the carrier of S1 and
A5: s2 = s|the carrier of S2 and
A6: s1 is stable;
  defpred P[Nat] means Following(s,$1)|the carrier of S2 = Following(s2,$1);
A7: now
    let n be Nat;
A8: Following(s, n+1) = Following Following(s, n) & Following Following(
    s2, n) = Following(s2, n+1) by FACIRC_1:12;
    the Sorts of A1 tolerates the Sorts of A2 by A2,CIRCCOMB:def 3;
    then reconsider
    Fs1 = Following(s, n)|the carrier of S1 as State of A1 by A3,CIRCCOMB:26;
    Following(s1, n) = Fs1 by A1,A2,A3,A4,Th13;
    then
A9: Fs1 is stable by A6,Th3;
    assume P[n];
    hence P[n+1] by A1,A2,A3,A8,A9,Th15;
  end;
  Following(s, 0)|the carrier of S2 = s2 by A5,FACIRC_1:11
    .= Following(s2, 0) by FACIRC_1:11;
  then
A10: P[ 0 ];
  thus for n being Nat holds P[n] from NAT_1:sch 2(A10,A7);
end;

theorem Th19:
  for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for A1
  being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 for n1,n2 being Nat for
s being State of A for s1 being State of A1, 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 void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 and
A2: S = S1+*S2;
  let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
  let A be non-empty Circuit of S such that
A3: A1 tolerates A2 and
A4: A = A1+*A2;
  let n1,n2 be Nat;
  let s be State of A, s9 be State of A1, s99 be State of A2 such that
A5: s9 = s|the carrier of S1 & Following(s9, n1) is stable and
A6: s99 = Following(s, n1)|the carrier of S2 & Following(s99, n2) is stable;
A7: the Sorts of A1 tolerates the Sorts of A2 by A3,CIRCCOMB:def 3;
  then reconsider
  s1 = Following(s, n1)|the carrier of S1, s0 = s|the carrier of S1
  as State of A1 by A4,CIRCCOMB:26;
A8: Following(Following(s, n1), n2) = Following(s, n1+n2) by FACIRC_1:13;
  then
A9: Following(s, n1+n2)|the carrier of S1 = Following(s1, n2) by A1,A2,A3,A4
,Th13;
  reconsider s2 = Following(s, n1)|the carrier of S2 as State of A2 by A4,A7,
CIRCCOMB:26;
A10: dom Following(s, n1+n2) = the carrier of S by CIRCUIT1:3;
A11: the carrier of S = (the carrier of S1)\/the carrier of S2 by A2,
CIRCCOMB:def 2;
A12: s1 = Following(s0, n1) by A1,A2,A3,A4,Th13;
  then
A13: Following(s, n1+n2)|the carrier of S2 = Following(s2, n2) by A1,A2,A3,A4
,A5,A8,Th18;
  then Following Following(s, n1+n2) = (Following Following(s2, n2))+*
  Following Following(s1, n2) by A1,A2,A3,A4,A9,CIRCCOMB:33
    .= Following(s2, n2)+*Following Following(s1, n2) by A6
    .= Following(s2, n2)+*Following(s1, n2+1) by FACIRC_1:12
    .= Following(s2, n2)+*s1 by A5,A12,Th3
    .= Following(s2, n2)+*Following(s1, n2) by A5,A12,Th3
    .= Following(s, n1+n2) by A11,A10,A9,A13,FUNCT_4:70;
  hence thesis;
end;

theorem Th20:
  for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & S = S1+*S2 for A1
  being non-empty Circuit of S1, A2 being non-empty Circuit of S2 for A being
non-empty Circuit of S st A1 tolerates A2 & A = A1+*A2 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) for s being State of A holds Following(
  s, n1+n2) is stable
proof
  let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & S = S1+*S2;
  let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
  let A be non-empty Circuit of S such that
A2: A1 tolerates A2 and
A3: A = A1+*A2;
  let n1,n2 be Nat such that
A4: ( for s being State of A1 holds Following(s, n1) is stable)& for s
  being State of A2 holds Following(s, n2) is stable;
  let s be State of A;
A5: the Sorts of A1 tolerates the Sorts of A2 by A2,CIRCCOMB:def 3;
  then reconsider s1 = s|the carrier of S1 as State of A1 by A3,CIRCCOMB:26;
  reconsider s2 = Following(s,n1)|the carrier of S2 as State of A2 by A3,A5,
CIRCCOMB:26;
  Following(s1,n1) is stable & Following(s2,n2) is stable by A4;
  hence thesis by A1,A2,A3,Th19;
end;

theorem Th21:
  for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InputVertices S1 misses InnerVertices S2 & InputVertices S2
  misses InnerVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2
  being non-empty Circuit of S2 for A being non-empty Circuit of S st A1
tolerates A2 & A = A1+*A2 for s being State of A for s1 being State of A1 st s1
= s|the carrier of S1 for s2 being State of A2 st s2 = s|the carrier of S2
for n being natural Number holds
Following(s, n) = Following(s1, n)+*Following(s2, n)
proof
  let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 and
A2: InputVertices S2 misses InnerVertices S1 and
A3: S = S1+*S2;
  let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
  let A be non-empty Circuit of S such that
A4: A1 tolerates A2 and
A5: A = A1+*A2;
  let s be State of A;
  let s1 be State of A1 such that
A6: s1 = s|the carrier of S1;
  let s2 be State of A2 such that
A7: s2 = s|the carrier of S2;
  let n be natural Number;
A8: Following(s, n)|the carrier of S1 = Following(s1, n) by A1,A3,A4,A5,A6,Th13
;
A9: dom Following(s, n) = the carrier of S & the carrier of S = (the
  carrier of S1) \/ the carrier of S2 by A3,CIRCCOMB:def 2,CIRCUIT1:3;
  S1 tolerates S2 by A4,CIRCCOMB:def 3;
  then
A10: S1+*S2 = S2+*S1 by CIRCCOMB:5;
  A1+*A2 = A2+*A1 by A4,CIRCCOMB:22;
  then Following(s, n)|the carrier of S2 = Following(s2, n) by A2,A3,A4,A5,A7
,A10,Th13,CIRCCOMB:19;
  hence thesis by A8,A9,FUNCT_4:70;
end;

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

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

theorem
  for S1,S2,S being non void Circuit-like non empty ManySortedSign st
  InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses
  InnerVertices S1 & S = S1+*S2 for A1 being non-empty Circuit of S1, A2 being
non-empty Circuit of S2 for A being non-empty Circuit of S st A1 tolerates A2 &
  A = A1+*A2 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) for
  s being State of A holds Following(s, max(n1,n2)) is stable
proof
  let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InputVertices S1 misses InnerVertices S2 & InputVertices S2 misses
  InnerVertices S1 & S = S1+*S2;
  let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
  let A be non-empty Circuit of S such that
A2: A1 tolerates A2 and
A3: A = A1+*A2;
  let n1,n2 be Nat such that
A4: ( for s being State of A1 holds Following(s, n1) is stable)& for s
  being State of A2 holds Following(s, n2) is stable;
  let s be State of A;
A5: the Sorts of A1 tolerates the Sorts of A2 by A2,CIRCCOMB:def 3;
  then reconsider s0 = s|the carrier of S1 as State of A1 by A3,CIRCCOMB:26;
  reconsider s3 = s|the carrier of S2 as State of A2 by A3,A5,CIRCCOMB:26;
  Following(s0, n1) is stable & Following(s3, n2) is stable by A4;
  hence thesis by A1,A2,A3,Th22;
end;

scheme
  CIRCCMB29sch22 {S0, Sn() -> unsplit gate`1=arity gate`2isBoolean non void
  strict non empty ManySortedSign, A0() -> Boolean gate`2=den strict Circuit of
S0(), An() -> Boolean gate`2=den strict Circuit of Sn(),
S(object,object) -> unsplit
  gate`1=arity gate`2isBoolean non void strict non empty ManySortedSign,
A(object,object) -> object, h() -> ManySortedSet of NAT,
o0()-> object, o(object,object) -> object, n(Nat)-> Nat}:
for s being State of An() holds Following(s, n(0)+n(2)*n(1)) is stable
provided
A1: for x being set, n being Nat holds A(x,n) is Boolean gate`2=den
strict Circuit of S(x,n) and
A2: for s being State of A0() holds Following(s, n(0)) is stable and
A3: for n being Nat, x being set for A being non-empty Circuit of S(x,n)
st x = h().(n) & A = A(x,n) for s being State of A holds Following(s, n(1)) is
stable and
A4: ex f,g being ManySortedSet of NAT st Sn() = f.n(2) & An() = g.n(2) &
f.0 = S0() & g.0 = A0() & h().0 = o0() & for n being Nat, S being non empty
ManySortedSign, A1 being non-empty MSAlgebra over S for x being set, A2 being
non-empty MSAlgebra over S(x,n) st S = f.n & A1 = g.n & x = h().n & A2 = A(x,n)
holds f.(n+1) = S +* S(x,n) & g.(n+1) = A1 +* A2 & h().(n+1) = o(x,n) and
A5: InnerVertices S0() is Relation & InputVertices S0() is without_pairs and
A6: h().0 = o0() & o0() in InnerVertices S0() and
A7: for n being Nat, x being set holds InnerVertices S(x,n) is Relation and
A8: for n being Nat, x being set st x = h().(n) holds (InputVertices S(x
,n)) \ {x} is without_pairs and
A9: for n being Nat, x being set st x = h().(n) holds h().(n+1) = o(x,n)
& x in InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n)
proof
  deffunc Al(non empty ManySortedSign,non-empty MSAlgebra over $1, set,set) =
  $2+*MSAlg(A($3,$4),S($3,$4));
  deffunc Sl(non empty ManySortedSign,set,set) = $1+*S($2,$3);
  defpred Q[object,object,object,Nat] means ex S being unsplit gate`1=arity
  gate`2isBoolean non void strict non empty ManySortedSign, A being Boolean
  gate`2=den strict Circuit of S st $1 = S & $2 = A & $3 = h().$4 & for s being
  State of A holds Following(s, n(0)+$4*n(1)) is stable;
  deffunc h(set) = h().$1;
  consider f,g being ManySortedSet of NAT such that
A10: Sn() = f.n(2) & An() = g.n(2) and
A11: f.0 = S0() and
A12: g.0 = A0() and
  h().0 = o0() and
A13: for n being Nat, S being non empty ManySortedSign, A1 being
non-empty MSAlgebra over S for x being set, A2 being non-empty MSAlgebra over S
(x,n) st S = f.n & A1 = g.n & x = h().n & A2 = A(x,n) holds f.(n+1) = S +* S(x,
  n) & g.(n+1) = A1 +* A2 & h().(n+1) = o(x,n) by A4;
  deffunc f(set) = f.$1;
A14: for n being Nat, S being non empty ManySortedSign, 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)
  = Sl(S,x,n) & g.(n+1) = Al(S,A,x,n) & h().(n+1) = o(x,n)
  proof
    let n be Nat, S be non empty ManySortedSign;
    let A be non-empty MSAlgebra over S, x be set;
    reconsider A2 = A(x,n) as Boolean gate`2=den strict Circuit of S(x,n)
    by A1;
    A2 = MSAlg(A(x,n),S(x,n)) by Def1;
    hence thesis by A13;
  end;
A15: for n being Nat, S being non empty ManySortedSign, A being non-empty
MSAlgebra over S for x being set st S = f.n & A = g.n & x = h().n & Q[S,A,x,n]
  holds Q[Sl(S,x,n), Al(S,A,x,n), o(x,n), n+1]
  proof
    let n be Nat, S be non empty ManySortedSign;
    let A being non-empty MSAlgebra over S, x being set such that
A16: S = f.n and
    A = g.n and
    x = h().n;
    given S9 being unsplit gate`1=arity gate`2isBoolean non void strict non
    empty ManySortedSign, A9 being Boolean gate`2=den strict Circuit of S9 such
    that
A17: S = S9 and
A18: A = A9 and
A19: x = h().(n) and
A20: for s being State of A9 holds Following(s, n(0)+n*n(1)) is stable;
    thus Q[S+*S(x,n), A+*MSAlg(A(x,n),S(x,n)), o(x,n), n+1]
    proof
      reconsider A2 = A(x,n) as Boolean gate`2=den strict Circuit of S(x,n) by
A1;
      take S9+*S(x,n);
A21:  for S being non empty ManySortedSign, A being non-empty MSAlgebra
over S for x being set, n being Nat holds Al(S,A,x,n) is non-empty MSAlgebra
      over Sl(S,x,n);
A22:  f.0 = S0() & g.0 = A0() by A11,A12;
      for n being Nat, S being non empty ManySortedSign, x being set st S
      = f.n & x = h().n holds f.(n+1) = Sl(S,x,n) & h().(n+1) = o(x,n) from
      CIRCCMB29sch15(A22,A14,A21);
      then
A23:  for n being Nat, S being non empty ManySortedSign, x being set st S
      = f(n) & x = h().n holds f(n+1) = S +* S(x,n) & h().(n+1) = o(x,n) & x in
      InputVertices S(x,n) & o(x,n) in InnerVertices S(x,n) by A9;
      A9+*A2 = A+*MSAlg(A(x,n),S(x,n)) by A17,A18,Def1;
      then reconsider
      AA = A+*MSAlg(A(x,n),S(x,n)) as Boolean gate`2=den strict
      Circuit of S9+*S(x,n);
      take AA;
A24:  n(0)+(n+1)*n(1) = n(0)+n*n(1)+n(1);
      thus S9+*S(x,n) = S+*S(x,n) & A+*MSAlg(A(x,n),S(x,n)) = AA by A17;
      thus o(x,n) = h(n+1) by A9,A19;
      let s be State of AA;
A25:  InnerVertices S0() is Relation by A5;
A26:  for n being Nat, x being set st x = h().n holds (InputVertices S(x,
      n)) \ {x} is without_pairs by A8;
A27:  for n being Nat, x being set holds InnerVertices S(x,n) is Relation
      by A7;
A28:  InputVertices S0() is without_pairs by A5;
A29:  f(0) = S0() & h().0 in InnerVertices S0() by A6,A11;
      for n being Nat ex S1,S2 being unsplit gate`1=arity gate`2isBoolean
non void non empty ManySortedSign st S1 = f(n) & S2 = f(n+1) & InputVertices S2
= (InputVertices S1)\/((InputVertices S(h().n,n)) \ {h().n}) & InnerVertices S1
is Relation & InputVertices S1 is without_pairs from CIRCCMB29sch10(A25,A28,A29
      ,A27,A26,A23);
      then ex S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non
      empty ManySortedSign st S1 = f.(n) & S2 = f.(n+1) & InputVertices S2 = (
InputVertices S1)\/((InputVertices S(h(n),n)) \ {h(n)}) & InnerVertices S1 is
      Relation & InputVertices S1 is without_pairs;
      then
A30:  InputVertices S9 misses InnerVertices S(x,n) by A7,A16,A17,FACIRC_1:5;
      A2 = MSAlg(A(x,n),S(x,n)) & for s being State of A2 holds Following
      (s, n(1)) is stable by A3,A19,Def1;
      hence Following(s, n(0)+(n+1)*n(1)) is stable by A17,A18,A20,A30,A24,Th20
,CIRCCOMB:60;
    end;
  end;
A31: for S being non empty ManySortedSign, A being non-empty MSAlgebra over
S for x being set, n being Nat holds Al(S,A,x,n) is non-empty MSAlgebra over Sl
  (S,x,n);
A32: ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
  , x being set st S = f.0 & A = g.0 & x = h().0 & Q[S, A, x, 0] by A2,A11,A12;
  for n being Nat ex S being non empty ManySortedSign, A being non-empty
MSAlgebra over S st S = f.n & A = g.n & Q[S,A,h().n,n] from CIRCCMB29sch13(A32,
  A14,A15,A31);
  then
  ex S being non empty ManySortedSign, A being non-empty MSAlgebra over S
  st S = f.n(2) & A = g.n(2) & Q[S,A,h().n(2),n(2)];
  hence thesis by A10;
end;