CIRCCOMB

:: Combining of Circuits
::  by Yatsuka Nakamura and Grzegorz Bancerek
::
:: Received May 11, 1995
:: Copyright (c) 1995-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 MSUALG_1, SUBSET_1, STRUCT_0, NUMBERS, XBOOLE_0, CARD_3,
      FINSEQ_1, FUNCOP_1, FINSEQ_2, PBOOLE, FUNCT_4, RELAT_1, PARTFUN1,
      FUNCT_1, TARSKI, MSAFREE2, FINSET_1, GLIB_000, MARGREL1, CIRCUIT1, FSM_1,
      CIRCUIT2, MCART_1, NAT_1, CARD_1, LATTICES, XBOOLEAN, CIRCCOMB;
 notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
      MCART_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_2,
      FUNCOP_1, PARTFUN1, FUNCT_4, CARD_3, MARGREL1, PBOOLE, STRUCT_0,
      MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2;
 constructors MARGREL1, CIRCUIT1, CIRCUIT2, RELSET_1, XTUPLE_0, NUMBERS;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1,
      FINSEQ_1, MARGREL1, CARD_3, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_2,
      MSAFREE2, FUNCT_4, RELSET_1, FINSEQ_2, XTUPLE_0;
 requirements NUMERALS, BOOLE, SUBSET;
 definitions TARSKI, PARTFUN1, FINSET_1, MSAFREE2, STRUCT_0, XBOOLE_0,
      FUNCOP_1, PBOOLE;
 equalities TARSKI, MSUALG_1, MSAFREE2, FUNCOP_1, MARGREL1;
 expansions TARSKI, PARTFUN1, MSUALG_1, XBOOLE_0;
 theorems TARSKI, ZFMISC_1, FINSEQ_1, FINSEQ_2, MSUALG_1, FUNCT_1, FUNCT_2,
      FUNCT_4, PBOOLE, GRFUNC_1, FUNCOP_1, PARTFUN1, RELAT_1, MSAFREE2,
      CIRCUIT1, CIRCUIT2, CARD_3, MONOID_1, RELSET_1, XBOOLE_0, XBOOLE_1,
      CARD_1, FINSEQ_3, XTUPLE_0, XREGULAR;
 schemes FUNCT_1;

begin :: Combining of ManySortedSign's

definition
  let S be ManySortedSign;
  mode Gate of S is Element of the carrier' of S;
end;

Lm1: now
  let i be Element of NAT, X be non empty set;
  thus product ((Seg i) --> X) = product (i |-> X) by FINSEQ_2:def 2
    .= i-tuples_on X by FINSEQ_3:131;
end;

registration
  let A,B be set;
  let f be ManySortedSet of A;
  let g be ManySortedSet of B;
  cluster f+*g -> A \/ B-defined;
  coherence
  proof
A1: dom g = B by PARTFUN1:def 2;
    dom f = A by PARTFUN1:def 2;
    then dom (f+*g) = A \/ B by A1,FUNCT_4:def 1;
    hence thesis by RELAT_1:def 18;
  end;
end;

registration
  let A,B be set;
  let f be ManySortedSet of A;
  let g be ManySortedSet of B;
  cluster f+*g -> total for A \/ B-defined Function;
  coherence
  proof
A1: dom g = B by PARTFUN1:def 2;
    dom f = A by PARTFUN1:def 2;
    then dom (f+*g) = A \/ B by A1,FUNCT_4:def 1;
    hence thesis;
  end;
end;

registration
  let A,B be set;
  cluster A .--> B -> {A}-defined;
  coherence;
end;

registration
  let A,B be set;
  cluster A .--> B -> total for {A}-defined Function;
  coherence;
end;

registration
  let A be set, B be non empty set;
  cluster A .--> B -> non-empty;
  coherence;
end;

theorem Th1:
  for A,B being set, f being ManySortedSet of A for g being
  ManySortedSet of B st f c= g holds f# c= g#
proof
  let A,B be set, f be ManySortedSet of A;
  let g be ManySortedSet of B;
  assume
A1: f c= g;
A2: dom f c= dom g by A1,RELAT_1:11;
A3: dom g = B by PARTFUN1:def 2;
A4: dom (g# ) = B* by PARTFUN1:def 2;
    let z be object;
A5: dom f = A by PARTFUN1:def 2;
    assume
A6: z in f#;
    then consider x,y being object such that
A7: [x,y] = z by RELAT_1:def 1;
    dom (f# ) = A* by PARTFUN1:def 2;
    then reconsider x as Element of A* by A6,A7,XTUPLE_0:def 12;
A8: rng x c= A by FINSEQ_1:def 4;
    rng x c= A by FINSEQ_1:def 4;
    then rng x c= B by A5,A3,A2;
    then x is FinSequence of B by FINSEQ_1:def 4;
    then reconsider x9 = x as Element of B* by FINSEQ_1:def 11;
A9: rng x9 c= B by FINSEQ_1:def 4;
    y = f#.x by A6,A7,FUNCT_1:1
      .= product (f*x) by FINSEQ_2:def 5
      .= product (g*x9) by A1,A5,A3,A8,A9,PARTFUN1:54,79
      .= g#.x9 by FINSEQ_2:def 5;
    hence z in g# by A7,A4,FUNCT_1:1;
end;

theorem Th2:
  for X being set, Y being non empty set, p being FinSequence of X
  holds (X --> Y)#.p = (len p)-tuples_on Y
proof
  let X be set, Y be non empty set, p be FinSequence of X;
  rng p c= X by FINSEQ_1:def 4;
  then rng p /\ X = rng p by XBOOLE_1:28;
  then
A1: p"X = p"rng p by RELAT_1:133
    .= dom p by RELAT_1:134;
  p in X* by FINSEQ_1:def 11;
  hence (X --> Y)#.p = product ((X --> Y)*p) by FINSEQ_2:def 5
    .= product (p"X --> Y) by FUNCOP_1:19
    .= product ((Seg len p) --> Y) by A1,FINSEQ_1:def 3
    .= (len p)-tuples_on Y by Lm1;
end;

definition
  let A be set;
  let f1,g1 be non-empty ManySortedSet of A;
  let B be set;
  let f2,g2 be non-empty ManySortedSet of B;
  let h1 be ManySortedFunction of f1,g1;
  let h2 be ManySortedFunction of f2,g2;
  redefine func h1+*h2 -> ManySortedFunction of f1+*f2, g1+*g2;  :: redefines +* (FUNCT_4, definition)
  coherence
  proof
    set f = f1+*f2, g = g1+*g2, h = h1+*h2;
A1: dom g1 = A by PARTFUN1:def 2;
A2: dom f2 = B by PARTFUN1:def 2;
A3: dom g2 = B by PARTFUN1:def 2;
A4: dom h2 = B by PARTFUN1:def 2;
A5: dom h1 = A by PARTFUN1:def 2;
    reconsider h as ManySortedFunction of A \/ B;
A6: dom f1 = A by PARTFUN1:def 2;
    h is ManySortedFunction of f, g
    proof
      let x be object;
A7:   not x in B or x in B;
      assume
A8:   x in A \/ B;
      then x in A or x in B by XBOOLE_0:def 3;
      then
      h.x = h1.x & h1.x is Function of f1.x, g1.x & f.x = f1.x & g.x = g1
.x or h.x = h2.x & h2.x is Function of f2.x, g2.x & f.x = f2.x & g.x = g2.x by
A6,A1,A5,A2,A3,A4,A8,A7,FUNCT_4:def 1,PBOOLE:def 15;
      hence thesis;
    end;
    hence thesis;
  end;
end;

definition
  let S1,S2 be ManySortedSign;
  pred S1 tolerates S2 means
  the Arity of S1 tolerates the Arity of S2 & the
  ResultSort of S1 tolerates the ResultSort of S2;
  reflexivity;
  symmetry;
end;

definition
  let S1,S2 be non empty ManySortedSign;
  func S1 +* S2 -> strict non empty ManySortedSign means
  :Def2:
  the carrier of
  it = (the carrier of S1) \/ (the carrier of S2) & the carrier' of it = (the
  carrier' of S1) \/ (the carrier' of S2) & the Arity of it = (the Arity of S1)
  +* (the Arity of S2) & the ResultSort of it = (the ResultSort of S1) +* (the
  ResultSort of S2);
  existence
  proof
    set RESULT = (the ResultSort of S1) +* (the ResultSort of S2);
    set ARITY = (the Arity of S1) +* (the Arity of S2);
    set OPER = (the carrier' of S1) \/ (the carrier' of S2);
    reconsider CARR = (the carrier of S1) \/ (the carrier of S2) as non empty
    set;
A1: dom the ResultSort of S2 = the carrier' of S2 by FUNCT_2:def 1;
    dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def 1;
    then
A2: dom RESULT = OPER by A1,FUNCT_4:def 1;
A3: the carrier of S1 c= CARR by XBOOLE_1:7;
A4: the carrier of S2 c= CARR by XBOOLE_1:7;
    rng (the ResultSort of S2) c= the carrier of S2 by RELAT_1:def 19;
    then
A5: rng (the ResultSort of S2) c= CARR by A4;
    rng (the ResultSort of S1) c= the carrier of S1 by RELAT_1:def 19;
    then rng (the ResultSort of S1) c= CARR by A3;
    then
A6: rng (the ResultSort of S1) \/ rng (the ResultSort of S2) c= CARR by A5,
XBOOLE_1:8;
    rng RESULT c= rng (the ResultSort of S1) \/ rng (the ResultSort of S2
    ) by FUNCT_4:17;
    then rng RESULT c= CARR by A6;
    then reconsider RESULT as Function of OPER, CARR by A2,FUNCT_2:def 1
,RELSET_1:4;
A7: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
    dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;
    then
A8: dom ARITY = OPER by A7,FUNCT_4:def 1;
A9: rng (the Arity of S1) c= (the carrier of S1)* by RELAT_1:def 19;
A10: rng (the Arity of S2) c= (the carrier of S2)* by RELAT_1:def 19;
    (the carrier of S2)* c= CARR* by FINSEQ_1:62,XBOOLE_1:7;
    then
A11: rng (the Arity of S2) c= CARR* by A10;
    (the carrier of S1)* c= CARR* by FINSEQ_1:62,XBOOLE_1:7;
    then rng (the Arity of S1) c= CARR* by A9;
    then
A12: rng (the Arity of S1) \/ rng (the Arity of S2) c= CARR* by A11,XBOOLE_1:8;
    rng ARITY c= rng (the Arity of S1) \/ rng (the Arity of S2) by FUNCT_4:17;
    then rng ARITY c= CARR* by A12;
    then reconsider ARITY as Function of OPER, CARR* by A8,FUNCT_2:def 1
,RELSET_1:4;
    take ManySortedSign(#CARR, OPER, ARITY, RESULT#);
    thus thesis;
  end;
  uniqueness;
end;

theorem Th3:
  for S1,S2,S3 being non empty ManySortedSign st S1 tolerates S2 &
  S2 tolerates S3 & S3 tolerates S1 holds S1+*S2 tolerates S3
proof
  let S1,S2,S3 be non empty ManySortedSign such that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2 and
A3: the Arity of S2 tolerates the Arity of S3 and
A4: the ResultSort of S2 tolerates the ResultSort of S3 and
A5: the Arity of S3 tolerates the Arity of S1 and
A6: the ResultSort of S3 tolerates the ResultSort of S1;
  the Arity of S1+*S2 = (the Arity of S1)+*the Arity of S2 by Def2;
  hence the Arity of S1+*S2 tolerates the Arity of S3 by A1,A3,A5,FUNCT_4:125;
  the ResultSort of S1+*S2 = (the ResultSort of S1)+*the ResultSort of S2
  by Def2;
  hence thesis by A2,A4,A6,FUNCT_4:125;
end;

theorem
  for S being non empty ManySortedSign holds S+*S = the ManySortedSign of S
proof
  let S be non empty ManySortedSign;
A1: the carrier' of S = (the carrier' of S) \/ the carrier' of S;
A2: the Arity of S = (the Arity of S)+*the Arity of S;
A3: the ResultSort of S = (the ResultSort of S)+*the ResultSort of S;
  the carrier of S = (the carrier of S) \/ the carrier of S;
  hence thesis by A1,A2,A3,Def2;
end;

theorem Th5:
  for S1,S2 being non empty ManySortedSign st S1 tolerates S2 holds
  S1+*S2 = S2+*S1
proof
  let S1,S2 be non empty ManySortedSign;
  set S = S1+*S2;
  assume that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2;
A3: the carrier' of S = (the carrier' of S1) \/ (the carrier' of S2) by Def2;
  (the ResultSort of S1)+*the ResultSort of S2 = (the ResultSort of S2)+*
  the ResultSort of S1 by A2,FUNCT_4:34;
  then
A4: the ResultSort of S = (the ResultSort of S2) +* (the ResultSort of S1)
  by Def2;
  (the Arity of S1)+*the Arity of S2 = (the Arity of S2)+*the Arity of S1
  by A1,FUNCT_4:34;
  then
A5: the Arity of S = (the Arity of S2) +* (the Arity of S1) by Def2;
  the carrier of S = (the carrier of S1) \/ (the carrier of S2) by Def2;
  hence thesis by A3,A5,A4,Def2;
end;

theorem
  for S1,S2,S3 being non empty ManySortedSign holds (S1+*S2)+*S3 = S1+*(
  S2+*S3 )
proof
  let S1,S2,S3 be non empty ManySortedSign;
  set S12 = S1+*S2, S23 = S2+*S3;
  set S1293 = S12+*S3, S1923 = S1+*S23;
A1: the carrier of S23 = (the carrier of S2) \/ (the carrier of S3) by Def2;
A2: the carrier of S1293 = (the carrier of S12) \/ (the carrier of S3) by Def2;
A3: the carrier of S1923 = (the carrier of S1) \/ (the carrier of S23) by Def2;
  the carrier of S12 = (the carrier of S1) \/ (the carrier of S2) by Def2;
  then
A4: the carrier of S1293 = the carrier of S1923 by A1,A2,A3,XBOOLE_1:4;
A5: the carrier' of S23 = (the carrier' of S2) \/ the carrier' of S3 by Def2;
A6: the carrier' of S1293 = (the carrier' of S12) \/ the carrier' of S3 by Def2
;
A7: the Arity of S23 = (the Arity of S2) +* (the Arity of S3) by Def2;
A8: the Arity of S1923 = (the Arity of S1) +* (the Arity of S23) by Def2;
A9: the carrier' of S1923 = (the carrier' of S1) \/ the carrier' of S23 by Def2
;
  the carrier' of S12 = (the carrier' of S1) \/ the carrier' of S2 by Def2;
  then
A10: the carrier' of S1293 = the carrier' of S1923 by A5,A6,A9,XBOOLE_1:4;
A11: the ResultSort of S1923 = (the ResultSort of S1)+*the ResultSort of S23
  by Def2;
A12: the ResultSort of S1293 = (the ResultSort of S12)+*the ResultSort of S3
  by Def2;
A13: the Arity of S1293 = (the Arity of S12) +* (the Arity of S3) by Def2;
  the Arity of S12 = (the Arity of S1) +* (the Arity of S2) by Def2;
  then
A14: the Arity of S1293 = the Arity of S1923 by A7,A13,A8,FUNCT_4:14;
A15: the ResultSort of S23 = (the ResultSort of S2)+*the ResultSort of S3 by
Def2;
  the ResultSort of S12 = (the ResultSort of S1)+*the ResultSort of S2 by Def2;
  hence thesis by A15,A12,A11,A4,A10,A14,FUNCT_4:14;
end;

theorem
  for f being one-to-one Function for S1,S2 being Circuit-like non
empty ManySortedSign st the ResultSort of S1 c= f & the ResultSort of S2 c= f
  holds S1+*S2 is Circuit-like
proof
  let f be one-to-one Function;
  let S1,S2 be Circuit-like non empty ManySortedSign such that
A1: the ResultSort of S1 c= f and
A2: the ResultSort of S2 c= f;
  let S be non void non empty ManySortedSign;
  set r1 = the ResultSort of S1, r2 =the ResultSort of S2;
  set r = the ResultSort of S;
A3: r1+*r2 c= r1 \/ r2 by FUNCT_4:29;
  assume S = S1+*S2;
  then
A4: r = r1+*r2 by Def2;
  r1 \/ r2 c= f by A1,A2,XBOOLE_1:8;
  then
A5: r1+*r2 c= f by A3;
  then
A6: dom r c= dom f by A4,GRFUNC_1:2;
  let o1, o2 be Gate of S;
A7: dom r = the carrier' of S by FUNCT_2:def 1;
  then
A8: o1 in dom r;
A9: o2 in dom r by A7;
  assume
A10: the_result_sort_of o1 = the_result_sort_of o2;
A11: r.o2 = f.o2 by A4,A7,A5,GRFUNC_1:2;
  r.o1 = f.o1 by A4,A7,A5,GRFUNC_1:2;
  hence thesis by A10,A8,A9,A11,A6,FUNCT_1:def 4;
end;

theorem
  for S1,S2 being Circuit-like non empty ManySortedSign st
  InnerVertices S1 misses InnerVertices S2 holds S1+*S2 is Circuit-like
proof
  let S1,S2 be Circuit-like non empty ManySortedSign;
  assume
A1: InnerVertices S1 misses InnerVertices S2;
  set r1 = the ResultSort of S1, r2 = the ResultSort of S2;
  let S be non void non empty ManySortedSign;
  set r = the ResultSort of S;
A2: dom r1 = the carrier' of S1 by FUNCT_2:def 1;
  assume
A3: S = S1+*S2;
  then
A4: r = r1+*r2 by Def2;
A5: dom r2 = the carrier' of S2 by FUNCT_2:def 1;
  let o1, o2 be Gate of S;
A6: the carrier' of S = (the carrier' of S1) \/ the carrier' of S2 by A3,Def2;
  then not o1 in the carrier' of S2 & o1 in the carrier' of S1 or o1 in the
  carrier' of S2 by XBOOLE_0:def 3;
  then
A7: r.o1 = r1.o1 & r1.o1 in rng r1 & o1 in the carrier' of S1 or r.o1 = r2.
  o1 & r2.o1 in rng r2 & o1 in the carrier' of S2 by A4,A2,A5,A6,FUNCT_1:def 3
,FUNCT_4:def 1;
  not o2 in the carrier' of S2 & o2 in the carrier' of S1 or o2 in the
  carrier' of S2 by A6,XBOOLE_0:def 3;
  then
A8: r.o2 = r1.o2 & r1.o2 in rng r1 & o2 in the carrier' of S1 or r.o2 = r2.
  o2 & r2.o2 in rng r2 & o2 in the carrier' of S2 by A4,A2,A5,A6,FUNCT_1:def 3
,FUNCT_4:def 1;
  assume
A9: the_result_sort_of o1 = the_result_sort_of o2;
  per cases by A1,A9,A7,A8,XBOOLE_0:3;
  suppose
A10: r.o1 = r1.o1 & o1 in the carrier' of S1 & r.o2 = r1.o2 & o2 in
    the carrier' of S1;
    then reconsider
    S = S1 as non void Circuit-like non empty ManySortedSign;
    reconsider p1 = o1, p2 = o2 as Gate of S by A10;
A11: the_result_sort_of p2 = r1.p2;
    the_result_sort_of p1 = r1.p1;
    hence thesis by A9,A10,A11,MSAFREE2:def 6;
  end;
  suppose
A12: r.o1 = r2.o1 & o1 in the carrier' of S2 & r.o2 = r2.o2 & o2 in
    the carrier' of S2;
    then reconsider
    S = S2 as non void Circuit-like non empty ManySortedSign;
    reconsider p1 = o1, p2 = o2 as Gate of S by A12;
A13: the_result_sort_of p2 = r2.p2;
    the_result_sort_of p1 = r2.p1;
    hence thesis by A9,A12,A13,MSAFREE2:def 6;
  end;
end;

theorem Th9:
  for S1,S2 being non empty ManySortedSign st S1 is not void or S2
  is not void holds S1+*S2 is non void
proof
  let S1,S2 be non empty ManySortedSign;

  assume
A1: S1 is not void or S2 is not void;
  the carrier' of S1+*S2 = (the carrier' of S1) \/ the carrier' of S2 by Def2;
  hence the carrier' of S1+*S2 is non empty by A1;
end;

theorem
  for S1,S2 being finite non empty ManySortedSign holds S1+*S2 is finite
proof
  let S1,S2 be finite non empty ManySortedSign;
  reconsider C1 = the carrier of S1, C2 = the carrier of S2 as finite set;
  the carrier of S1+*S2 = C1 \/ C2 by Def2;
  hence thesis;
end;

registration
  let S1 be non void non empty ManySortedSign;
  let S2 be non empty ManySortedSign;
  cluster S1 +* S2 -> non void;
  coherence by Th9;
  cluster S2 +* S1 -> non void;
  coherence by Th9;
end;

::theorem
:: for S1,S2 being monotonic (non void ManySortedSign) st
::  InputVertices S1 misses InnerVertices S2 or
::  InputVertices S2 misses InnerVertices S1
:: holds S1+*S2 is monotonic;

theorem Th11:
  for S1,S2 being non empty ManySortedSign st S1 tolerates S2
  holds InnerVertices (S1+*S2) = (InnerVertices S1) \/ (InnerVertices S2) &
  InputVertices (S1+*S2) c= (InputVertices S1) \/ (InputVertices S2)
proof
  let S1,S2 be non empty ManySortedSign;
  set R1 = the ResultSort of S1, R2 = the ResultSort of S2;
  assume that
  the Arity of S1 tolerates the Arity of S2 and
A1: R1 tolerates R2;
  set S = S1+*S2, R = the ResultSort of S;
A2: R = R1+*R2 by Def2;
  then R1 c= R by A1,FUNCT_4:28;
  then
A3: rng R1 c= rng R by RELAT_1:11;
  rng R2 c= rng R by A2,FUNCT_4:18;
  then
A4: (rng R1) \/ (rng R2) c= rng R by A3,XBOOLE_1:8;
A5: rng R c= (rng R1) \/ (rng R2) by A2,FUNCT_4:17;
  hence InnerVertices S = (InnerVertices S1) \/ (InnerVertices S2) by A4;
  let x be object;
  assume
A6: x in InputVertices S;
  then
A7: not x in rng R by XBOOLE_0:def 5;
A8: rng R = (rng R1) \/ (rng R2) by A5,A4;
  then
A9: not x in rng R2 by A7,XBOOLE_0:def 3;
  the carrier of S = (the carrier of S1) \/ the carrier of S2 by Def2;
  then
A10: x in the carrier of S1 or x in the carrier of S2 by A6,XBOOLE_0:def 3;
  not x in rng R1 by A8,A7,XBOOLE_0:def 3;
  then x in (the carrier of S1) \ rng R1 or x in (the carrier of S2) \ rng R2
  by A10,A9,XBOOLE_0:def 5;
  hence thesis by XBOOLE_0:def 3;
end;

theorem Th12:
  for S1,S2 being non empty ManySortedSign for v2 being Vertex of
  S2 st v2 in InputVertices (S1+*S2) holds v2 in InputVertices S2
proof
  let S1,S2 be non empty ManySortedSign;
  set R1 = the ResultSort of S1, R2 = the ResultSort of S2;
  set S = S1+*S2, R = the ResultSort of S;
  let v2 be Vertex of S2;
  R = R1+*R2 by Def2;
  then
A1: rng R2 c= rng R by FUNCT_4:18;
  assume v2 in InputVertices S;
  then not v2 in rng R2 by A1,XBOOLE_0:def 5;
  hence thesis by XBOOLE_0:def 5;
end;

theorem Th13:
  for S1,S2 being non empty ManySortedSign st S1 tolerates S2 for
v1 being Vertex of S1 st v1 in InputVertices (S1+*S2) holds v1 in InputVertices
  S1
proof
  let S1,S2 be non empty ManySortedSign such that
  the Arity of S1 tolerates the Arity of S2 and
A1: the ResultSort of S1 tolerates the ResultSort of S2;
  set S = S1+*S2, R = the ResultSort of S;
  set R1 = the ResultSort of S1, R2 = the ResultSort of S2;
  R = R1+*R2 by Def2;
  then R1 c= R by A1,FUNCT_4:28;
  then
A2: rng R1 c= rng R by RELAT_1:11;
  let v1 be Vertex of S1;
  assume v1 in InputVertices S;
  then not v1 in rng R1 by A2,XBOOLE_0:def 5;
  hence thesis by XBOOLE_0:def 5;
end;

theorem Th14:
  for S1 being non empty ManySortedSign, S2 being non void non
empty ManySortedSign for o2 being OperSymbol of S2, o being OperSymbol of S1+*
  S2 st o2 = o holds the_arity_of o = the_arity_of o2 & the_result_sort_of o =
  the_result_sort_of o2
proof
  let S1 be non empty ManySortedSign;
  let S2 be non void non empty ManySortedSign;
  let o2 be OperSymbol of S2, o be OperSymbol of S1+*S2;
  assume
A1: o2 = o;
A2: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
  the Arity of S1+*S2 = (the Arity of S1)+*(the Arity of S2) by Def2;
  hence the_arity_of o = the_arity_of o2 by A1,A2,FUNCT_4:13;
A3: dom the ResultSort of S2 = the carrier' of S2 by FUNCT_2:def 1;
  the ResultSort of S1+*S2 = (the ResultSort of S1)+*(the ResultSort of S2
  ) by Def2;
  hence thesis by A1,A3,FUNCT_4:13;
end;

theorem Th15:
  for S1 being non empty ManySortedSign, S2,S being Circuit-like
non void non empty ManySortedSign st S = S1+*S2 for v2 being Vertex of S2 st
  v2 in InnerVertices S2 for v being Vertex of S st v2 = v holds v in
  InnerVertices S & action_at v = action_at v2
proof
  let S1 be non empty ManySortedSign, S2,S be Circuit-like non void non empty
  ManySortedSign such that
A1: S = S1+*S2;
  let v2 be Vertex of S2 such that
A2: v2 in InnerVertices S2;
  the carrier' of S = (the carrier' of S1) \/ the carrier' of S2 by A1,Def2;
  then reconsider o = action_at v2 as OperSymbol of S by XBOOLE_0:def 3;
  let v be Vertex of S such that
A3: v2 = v;
  the ResultSort of S = (the ResultSort of S1)+*the ResultSort of S2 by A1,Def2
;
  then
A4: InnerVertices S2 c= InnerVertices S by FUNCT_4:18;
  hence v in InnerVertices S by A2,A3;
  the_result_sort_of action_at v2 = v2 by A2,MSAFREE2:def 7;
  then v = the_result_sort_of o by A1,A3,Th14;
  hence thesis by A2,A3,A4,MSAFREE2:def 7;
end;

theorem Th16:
  for S1 being non void non empty ManySortedSign, S2 being non
empty ManySortedSign st S1 tolerates S2 for o1 being OperSymbol of S1, o being
  OperSymbol of S1+*S2 st o1 = o holds the_arity_of o = the_arity_of o1 &
  the_result_sort_of o = the_result_sort_of o1
proof
  let S1 be non void non empty ManySortedSign, S2 be non empty ManySortedSign
  such that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2;
  let o1 be OperSymbol of S1, o be OperSymbol of S1+*S2;
  assume
A3: o1 = o;
A4: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;
  the Arity of S1+*S2 = (the Arity of S1)+*(the Arity of S2) by Def2;
  hence the_arity_of o = the_arity_of o1 by A1,A3,A4,FUNCT_4:15;
A5: dom the ResultSort of S1 = the carrier' of S1 by FUNCT_2:def 1;
  the ResultSort of S1+*S2 = (the ResultSort of S1)+*(the ResultSort of S2
  ) by Def2;
  hence thesis by A2,A3,A5,FUNCT_4:15;
end;

theorem Th17:
  for S1,S being Circuit-like non void non empty ManySortedSign,
S2 being non empty ManySortedSign st S1 tolerates S2 & S = S1+*S2 for v1 being
Vertex of S1 st v1 in InnerVertices S1 for v being Vertex of S st v1 = v holds
  v in InnerVertices S & action_at v = action_at v1
proof
  let S1,S be Circuit-like non void non empty ManySortedSign, S2 be non
  empty ManySortedSign such that
A1: S1 tolerates S2 and
A2: S = S1+*S2;
  let v1 be Vertex of S1 such that
A3: v1 in InnerVertices S1;
  let v be Vertex of S such that
A4: v1 = v;
  InnerVertices S = (InnerVertices S1) \/ (InnerVertices S2) by A1,A2,Th11;
  hence
A5: v in InnerVertices S by A3,A4,XBOOLE_0:def 3;
  the carrier' of S = (the carrier' of S1) \/ the carrier' of S2 by A2,Def2;
  then reconsider o = action_at v1 as OperSymbol of S by XBOOLE_0:def 3;
  the_result_sort_of action_at v1 = v1 by A3,MSAFREE2:def 7;
  then v = the_result_sort_of o by A1,A2,A4,Th16;
  hence thesis by A5,MSAFREE2:def 7;
end;

begin :: Combining of Circuits

definition
  let S1,S2 be non empty ManySortedSign;
  let A1 be MSAlgebra over S1;
  let A2 be MSAlgebra over S2;
  pred A1 tolerates A2 means

  S1 tolerates S2 & the Sorts of A1
  tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2;
end;

definition
  let S1,S2 be non empty ManySortedSign;
  let A1 be non-empty MSAlgebra over S1;
  let A2 be non-empty MSAlgebra over S2;
  assume
A1: the Sorts of A1 tolerates the Sorts of A2;
  func A1 +* A2 -> strict non-empty MSAlgebra over S1+*S2 means
  :Def4:
  the Sorts of it = (the Sorts of A1) +* (the Sorts of A2) &
  the Charact of it = (the Charact of A1) +* (the Charact of A2);
  uniqueness;
  existence
  proof
    set CHARACT = (the Charact of A1) +* (the Charact of A2);
    set SA1 = the Sorts of A1, SA2 = the Sorts of A2;
    set S = S1+*S2;
    set I = the carrier of S, I1 = the carrier of S1, I2 = the carrier of S2;
    set SA12 = SA1#+*(SA2# );
A2: dom (SA2# ) = I2* by PARTFUN1:def 2;
A3: the ResultSort of S = (the ResultSort of S1) +* (the ResultSort of S2)
    by Def2;
A4: rng the ResultSort of S2 c= I2 by RELAT_1:def 19;
A5: dom SA2 = I2 by PARTFUN1:def 2;
    the carrier of S = (the carrier of S1) \/ (the carrier of S2) by Def2;
    then reconsider SORTS = (the Sorts of A1)+*the Sorts of A2 as non-empty
    ManySortedSet of the carrier of S1+*S2;
A6: dom (SORTS# ) = I* by PARTFUN1:def 2;
A7: SORTS = SA1 \/ SA2 by A1,FUNCT_4:30;
    then
A8: SA2# c= SORTS# by Th1,XBOOLE_1:7;
A9: dom SA12 = I1* \/ (I2* ) by PARTFUN1:def 2;
A10: dom SA1 = I1 by PARTFUN1:def 2;
    rng the ResultSort of S1 c= I1 by RELAT_1:def 19;
    then
A11: (SA1+*SA2)*((the ResultSort of S1)+*the ResultSort of S2) = (SA1*the
    ResultSort of S1)+*(SA2*the ResultSort of S2) by A1,A10,A5,A4,FUNCT_4:69;
A12: rng the Arity of S2 c= I2* by RELAT_1:def 19;
A13: dom (SA1# ) = I1* by PARTFUN1:def 2;
A14: SA1# tolerates SA2#
    proof
      let x be object;
      assume
A15:  x in (dom (SA1# )) /\ dom (SA2# );
      then reconsider i1 = x as Element of I1* by A13,XBOOLE_0:def 4;
      reconsider i2 = x as Element of I2* by A2,A15,XBOOLE_0:def 4;
A16:  rng i1 c= I1 by FINSEQ_1:def 4;
A17:  rng i2 c= I2 by FINSEQ_1:def 4;
      thus SA1#.x = product (SA1*i1) by FINSEQ_2:def 5
        .= product (SA2*i2) by A1,A10,A5,A16,A17,PARTFUN1:79
        .= SA2#.x by FINSEQ_2:def 5;
    end;
    then
A18: SA12 = SA1# \/ (SA2# ) by FUNCT_4:30;
    SA1# c= SORTS# by A7,Th1,XBOOLE_1:7;
    then
A19: SA12 c= SORTS# by A18,A8,XBOOLE_1:8;
A20: the carrier' of S = (the carrier' of S1) \/ (the carrier' of S2) by Def2;
A21: rng the Arity of S c= I* by RELAT_1:def 19;
A22: rng the Arity of S1 c= I1* by RELAT_1:def 19;
    then
A23: (rng the Arity of S1) \/ rng the Arity of S2 c= I1* \/ (I2* ) by A12,
XBOOLE_1:13;
A24: the Arity of S = (the Arity of S1) +* (the Arity of S2) by Def2;
    then
    rng the Arity of S c= (rng the Arity of S1) \/ rng the Arity of S2 by
FUNCT_4:17;
    then
A25: rng the Arity of S c= dom SA12 by A23,A9;
A26:  SA12 tolerates SORTS# by A19,PARTFUN1:54;
A27: (SA1#+*(SA2# ))*((the Arity of S1)+*the Arity of S2)
     = (SA1#*the Arity of S1)+*(SA2#*the Arity of S2)
      by A13,A2,A22,A12,A14,FUNCT_4:69;
    reconsider
    CHARACT as ManySortedFunction
      of SORTS#*the Arity of S, SORTS*the ResultSort of S
       by A20,A24,A3,A6,A21,A25,A11,A26,A27,PARTFUN1:79;
    reconsider A = MSAlgebra(#SORTS, CHARACT#) as strict non-empty MSAlgebra
    over S by MSUALG_1:def 3;
    take A;
    thus thesis;
  end;
end;

theorem
  for S being non void non empty ManySortedSign, A being MSAlgebra over
  S holds A tolerates A;

theorem Th19:
  for S1,S2 be non void non empty ManySortedSign for A1 be
  MSAlgebra over S1, A2 be MSAlgebra over S2 st A1 tolerates A2 holds A2
  tolerates A1;

theorem
  for S1,S2,S3 being non empty ManySortedSign, A1 being non-empty
  MSAlgebra over S1, A2 being non-empty MSAlgebra over S2, A3 being MSAlgebra
  over S3 st A1 tolerates A2 & A2 tolerates A3 & A3 tolerates A1 holds A1+*A2
  tolerates A3
proof
  let S1,S2,S3 be non empty ManySortedSign;
  let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2, A3
  be MSAlgebra over S3 such that
A1: S1 tolerates S2 and
A2: the Sorts of A1 tolerates the Sorts of A2 and
A3: the Charact of A1 tolerates the Charact of A2 and
A4: S2 tolerates S3 and
A5: the Sorts of A2 tolerates the Sorts of A3 and
A6: the Charact of A2 tolerates the Charact of A3 and
A7: S3 tolerates S1 and
A8: the Sorts of A3 tolerates the Sorts of A1 and
A9: the Charact of A3 tolerates the Charact of A1;
  thus S1+*S2 tolerates S3 by A1,A4,A7,Th3;
  the Sorts of A1+*A2 = (the Sorts of A1)+*the Sorts of A2 by A2,Def4;
  hence the Sorts of A1+*A2 tolerates the Sorts of A3 by A2,A5,A8,FUNCT_4:125;
  the Charact of A1+*A2 = (the Charact of A1)+*the Charact of A2 by A2,Def4;
  hence thesis by A3,A6,A9,FUNCT_4:125;
end;

theorem
  for S being strict non empty ManySortedSign, A being non-empty
  MSAlgebra over S holds A+*A = the MSAlgebra of A
proof
  let S be strict non empty ManySortedSign, A be non-empty MSAlgebra over S;
  set A9 = the MSAlgebra of A;
  set SA = the Sorts of A9, CA = the Charact of A9;
  set SAA = the Sorts of A+*A, CAA = the Charact of A+*A;
  CA = CA+*CA;
  then
A1: CAA = CA by Def4;
  SA = SA+*SA;
  then SAA = SA by Def4;
  hence thesis by A1;
end;

theorem Th22:
  for S1,S2 being non empty ManySortedSign, A1 being non-empty
  MSAlgebra over S1, A2 being non-empty MSAlgebra over S2 st A1 tolerates A2
  holds A1+*A2 = A2+*A1
proof
  let S1,S2 be non empty ManySortedSign;
  let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2;
  set A = A1+*A2;
  assume that
A1: S1 tolerates S2 and
A2: the Sorts of A1 tolerates the Sorts of A2 and
A3: the Charact of A1 tolerates the Charact of A2;
  (the Sorts of A1)+*the Sorts of A2 = (the Sorts of A2)+*the Sorts of A1
  by A2,FUNCT_4:34;
  then
A4: the Sorts of A = (the Sorts of A2) +* (the Sorts of A1) by A2,Def4;
  (the Charact of A1)+*the Charact of A2 = (the Charact of A2)+*the
  Charact of A1 by A3,FUNCT_4:34;
  then
A5: the Charact of A = (the Charact of A2) +* (the Charact of A1) by A2,Def4;
  S1+*S2 = S2+*S1 by A1,Th5;
  hence thesis by A2,A4,A5,Def4;
end;

theorem
  for S1,S2,S3 being non empty ManySortedSign, A1 being non-empty
  MSAlgebra over S1, A2 being non-empty MSAlgebra over S2, A3 being non-empty
  MSAlgebra over S3 st the Sorts of A1 tolerates the Sorts of A2 & the Sorts of
A2 tolerates the Sorts of A3 & the Sorts of A3 tolerates the Sorts of A1 holds
  (A1+*A2)+*A3 = A1+*(A2+*A3)
proof
  let S1,S2,S3 be non empty ManySortedSign, A1 be non-empty MSAlgebra over S1,
A2 be non-empty MSAlgebra over S2, A3 be non-empty MSAlgebra over S3 such that
A1: the Sorts of A1 tolerates the Sorts of A2 and
A2: the Sorts of A2 tolerates the Sorts of A3 and
A3: the Sorts of A3 tolerates the Sorts of A1;
  set A12 = A1+*A2, A23 = A2+*A3;
A4: the Charact of A12 = (the Charact of A1) +* (the Charact of A2) by A1,Def4;
  set A1293 = A12+*A3, A1923 = A1+*A23;
  set s1 = the Sorts of A1, s2 = the Sorts of A2, s3 = the Sorts of A3;
A5: the Sorts of A23 = (the Sorts of A2) +* (the Sorts of A3) by A2,Def4;
A6: the Sorts of A1 tolerates the Sorts of A23
  proof
    let x be object;
    assume
A7: x in (dom s1) /\ dom the Sorts of A23;
    then x in dom the Sorts of A23 by XBOOLE_0:def 4;
    then
A8: x in dom s2 or x in dom s3 by A5,FUNCT_4:12;
    x in dom s1 by A7,XBOOLE_0:def 4;
    then x in (dom s1) /\ dom s2 & (s2+*s3).x = s2.x or x in (dom s3) /\ dom
    s1 & (s2+*s3).x = s3.x by A2,A8,FUNCT_4:13,15,XBOOLE_0:def 4;
    hence thesis by A1,A3,A5;
  end;
  then
A9: the Sorts of A1923 = (the Sorts of A1) +* (the Sorts of A23) by Def4;
A10: the Charact of A23 = (the Charact of A2) +* (the Charact of A3) by A2,Def4
;
A11: the Charact of A1923 = (the Charact of A1) +* (the Charact of A23) by A6
,Def4;
A12: the Sorts of A12 = (the Sorts of A1) +* (the Sorts of A2) by A1,Def4;
A13: the Sorts of A12 tolerates the Sorts of A3
  proof
    let x be object;
    assume
A14: x in (dom the Sorts of A12) /\ dom s3;
    then x in dom the Sorts of A12 by XBOOLE_0:def 4;
    then
A15: x in dom s1 or x in dom s2 by A12,FUNCT_4:12;
    x in dom s3 by A14,XBOOLE_0:def 4;
    then x in (dom s3) /\ dom s1 & (s1+*s2).x = s1.x or x in (dom s2) /\ dom
    s3 & (s1+*s2).x = s2.x by A1,A15,FUNCT_4:13,15,XBOOLE_0:def 4;
    hence thesis by A2,A3,A12;
  end;
  then the Charact of A1293 = (the Charact of A12) +* (the Charact of A3) by
Def4;
  then
A16: the Charact of A1293 = the Charact of A1923 by A4,A10,A11,FUNCT_4:14;
  the Sorts of A1293 = (the Sorts of A12) +* (the Sorts of A3) by A13,Def4;
  then the Sorts of A1293 = the Sorts of A1923 by A12,A5,A9,FUNCT_4:14;
  hence thesis by A16;
end;

theorem
  for S1,S2 being non empty ManySortedSign for A1 being finite-yielding
  non-empty MSAlgebra over S1 for A2 being finite-yielding non-empty MSAlgebra
  over S2 st the Sorts of A1 tolerates the Sorts of A2 holds A1+*A2 is
  finite-yielding
proof
  let S1,S2 be non empty ManySortedSign;
  let A1 be finite-yielding non-empty MSAlgebra over S1, A2 be finite-yielding
  non-empty MSAlgebra over S2 such that
A1: the Sorts of A1 tolerates the Sorts of A2;
  let x be object;
  set A = A1+*A2;
  set SA = the Sorts of A, SA1 = the Sorts of A1, SA2 = the Sorts of A2;
A2: dom SA1 = the carrier of S1 by PARTFUN1:def 2;
A3: SA1 is finite-yielding by MSAFREE2:def 11;
  assume x in the carrier of S1+*S2;
  then reconsider x as Vertex of S1+*S2;
A4: dom SA2 = the carrier of S2 by PARTFUN1:def 2;
  the carrier of S1+*S2 = (the carrier of S1) \/ the carrier of S2 by Def2;
  then
A5: x in the carrier of S1 or x in the carrier of S2 by XBOOLE_0:def 3;
A6: SA2 is finite-yielding by MSAFREE2:def 11;
  SA = SA1+*SA2 by A1,Def4;
  then
  SA.x = SA1.x & SA1.x is finite or SA.x = SA2.x & SA2.x is finite by A1,A2,A4
,A5,A3,A6,FUNCT_4:13,15;
  hence thesis;
end;

theorem
  for S1,S2 being non empty ManySortedSign for A1 being non-empty
  MSAlgebra over S1, s1 being Element of product the Sorts of A1 for A2 being
non-empty MSAlgebra over S2, s2 being Element of product the Sorts of A2 st the
Sorts of A1 tolerates the Sorts of A2 holds s1+*s2 in product the Sorts of A1+*
  A2
proof
  let S1,S2 be non empty ManySortedSign;
  let A1 be non-empty MSAlgebra over S1;
  let s1 be Element of product ((the Sorts of A1) qua non-empty ManySortedSet
  of the carrier of S1);
  let A2 be non-empty MSAlgebra over S2;
  let s2 be Element of product ((the Sorts of A2) qua non-empty ManySortedSet
  of the carrier of S2);
  assume the Sorts of A1 tolerates the Sorts of A2;
  then the Sorts of A1+*A2 = (the Sorts of A1)+*the Sorts of A2 by Def4;
  hence thesis by CARD_3:97;
end;

theorem
  for S1,S2 being non empty ManySortedSign for A1 being non-empty
  MSAlgebra over S1, A2 being non-empty MSAlgebra over S2 st the Sorts of A1
  tolerates the Sorts of A2 for s being Element of product the Sorts of A1+*A2
  holds s|the carrier of S1 in product the Sorts of A1 & s|the carrier of S2 in
  product the Sorts of A2
proof
  let S1,S2 be non empty ManySortedSign;
  let A1 be non-empty MSAlgebra over S1;
  let A2 be non-empty MSAlgebra over S2;
A1: dom the Sorts of A1 = the carrier of S1 by PARTFUN1:def 2;
A2: dom the Sorts of A2 = the carrier of S2 by PARTFUN1:def 2;
  assume
A3: the Sorts of A1 tolerates the Sorts of A2;
  then the Sorts of A1+*A2 = (the Sorts of A1)+*the Sorts of A2 by Def4;
  hence thesis by A3,A1,A2,CARD_3:98,99;
end;

theorem Th27:
  for S1,S2 being non void non empty ManySortedSign for A1 being
non-empty MSAlgebra over S1, A2 being non-empty MSAlgebra over S2 st the Sorts
  of A1 tolerates the Sorts of A2 for o being OperSymbol of S1+*S2, o2 being
  OperSymbol of S2 st o = o2 holds Den(o, A1+*A2) = Den(o2, A2)
proof
  let S1,S2 be non void non empty ManySortedSign;
  let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2;
A1: dom the Charact of A2 = the carrier' of S2 by PARTFUN1:def 2;
  assume the Sorts of A1 tolerates the Sorts of A2;
  then
A2: the Charact of A1+*A2 = (the Charact of A1)+*the Charact of A2 by Def4;
  let o be OperSymbol of S1+*S2, o2 be OperSymbol of S2;
  assume o = o2;
  hence thesis by A2,A1,FUNCT_4:13;
end;

theorem Th28:
  for S1,S2 being non void non empty ManySortedSign for A1 being
non-empty MSAlgebra over S1, A2 being non-empty MSAlgebra over S2 st the Sorts
of A1 tolerates the Sorts of A2 & the Charact of A1 tolerates the Charact of A2
for o being OperSymbol of S1+*S2, o1 being OperSymbol of S1 st o = o1 holds Den
  (o, A1+*A2) = Den(o1, A1)
proof
  let S1,S2 be non void non empty ManySortedSign;
  let A1 be non-empty MSAlgebra over S1, A2 be non-empty MSAlgebra over S2;
A1: dom the Charact of A1 = the carrier' of S1 by PARTFUN1:def 2;
  assume the Sorts of A1 tolerates the Sorts of A2;
  then
A2: the Charact of A1+*A2 = (the Charact of A1)+*the Charact of A2 by Def4;
  assume
A3: the Charact of A1 tolerates the Charact of A2;
  let o be OperSymbol of S1+*S2, o1 be OperSymbol of S1;
  assume o = o1;
  hence thesis by A2,A3,A1,FUNCT_4:15;
end;

theorem Th29:
  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, A being non-empty Circuit of S for s being State of A,
  s2 being State of A2 st s2 = s|the carrier of S2 for g being Gate of S, g2
  being Gate of S2 st g = g2 holds g depends_on_in s = g2 depends_on_in s2
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;
  let s be State of A, s2 be State of A2 such that
A2: s2 = s|the carrier of S2;
  let o be OperSymbol of S, o2 be OperSymbol of S2 such that
A3: o = o2;
A4: (the carrier of S2)|`the_arity_of o2 = the_arity_of o2;
  thus o depends_on_in s = s*the_arity_of o by CIRCUIT1:def 3
    .= s*the_arity_of o2 by A1,A3,Th14
    .= s2*the_arity_of o2 by A2,A4,MONOID_1:1
    .= o2 depends_on_in s2 by CIRCUIT1:def 3;
end;

theorem Th30:
  for S1,S2,S being non void Circuit-like non empty
ManySortedSign st S = S1+*S2 & S1 tolerates S2 for A1 being non-empty Circuit
  of S1, A2 being non-empty Circuit of S2, A being non-empty Circuit of S for s
being State of A, s1 being State of A1 st s1 = s|the carrier of S1 for g being
  Gate of S, g1 being Gate of S1 st g = g1 holds g depends_on_in s = g1
  depends_on_in s1
proof
  let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: S = S1+*S2 and
A2: S1 tolerates S2;
  let A1 be non-empty Circuit of S1, A2 be non-empty Circuit of S2;
  let A be non-empty Circuit of S;
  let s be State of A, s1 be State of A1 such that
A3: s1 = s|the carrier of S1;
  let o be Gate of S, o1 be Gate of S1 such that
A4: o = o1;
A5: (the carrier of S1)|`the_arity_of o1 = the_arity_of o1;
  thus o depends_on_in s = s*the_arity_of o by CIRCUIT1:def 3
    .= s*the_arity_of o1 by A1,A2,A4,Th16
    .= s1*the_arity_of o1 by A3,A5,MONOID_1:1
    .= o1 depends_on_in s1 by CIRCUIT1:def 3;
end;

theorem Th31:
  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, v being Vertex of S holds (for s1 being
State of A1 st s1 = s|the carrier of S1 holds v in InnerVertices S1 or v in the
carrier of S1 & v in InputVertices S implies (Following s).v = (Following s1).v
  ) & (for s2 being State of A2 st s2 = s|the carrier of S2 holds v in
  InnerVertices S2 or v in the carrier of S2 & v in InputVertices S implies (
  Following s).v = (Following s2).v)
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: S1 tolerates S2 and
A3: the Sorts of A1 tolerates the Sorts of A2 and
A4: the Charact of A1 tolerates the Charact of A2 and
A5: A = A1+*A2;
  let s be State of A, v be Vertex of S;
  hereby
    let s1 be State of A1 such that
A6: s1 = s|the carrier of S1;
A7: now
      assume v in InnerVertices S1;
      then reconsider v1 = v as Element of InnerVertices S1;
A8:   (Following s1).v1 = (Den (action_at v1, A1)).(action_at v1
      depends_on_in s1) by CIRCUIT2:def 5;
      v1 in InnerVertices S by A1,A2,Th17;
      then
A9:   (Following s).v = (Den (action_at v, A)).(action_at v depends_on_in
      s) by CIRCUIT2:def 5;
A10:  action_at v = action_at v1 by A1,A2,Th17;
      then Den (action_at v1, A1) = Den (action_at v, A) by A1,A3,A4,A5,Th28;
      hence (Following s).v = (Following s1).v by A1,A2,A6,A10,A9,A8,Th30;
    end;
    now
      assume that
A11:  v in the carrier of S1 and
A12:  v in InputVertices S;
      reconsider v1 = v as Vertex of S1 by A11;
      v1 in InputVertices S1 by A1,A2,A12,Th13;
      then
A13:  (Following s1).v1 = s1.v1 by CIRCUIT2:def 5;
A14:  dom s1 = the carrier of S1 by CIRCUIT1:3;
      (Following s).v = s.v by A12,CIRCUIT2:def 5;
      hence (Following s).v = (Following s1).v by A6,A13,A14,FUNCT_1:47;
    end;
    hence v in InnerVertices S1 or v in the carrier of S1 & v in InputVertices
    S implies (Following s).v = (Following s1).v by A7;
  end;
  let s2 be State of A2 such that
A15: s2 = s|the carrier of S2;
A16: now
    assume v in InnerVertices S2;
    then reconsider v2 = v as Element of InnerVertices S2;
A17: (Following s2).v2 = (Den (action_at v2, A2)).(action_at v2
    depends_on_in s2) by CIRCUIT2:def 5;
    v2 in InnerVertices S by A1,Th15;
    then
A18: (Following s).v = (Den (action_at v, A)).(action_at v depends_on_in s
    ) by CIRCUIT2:def 5;
A19: action_at v = action_at v2 by A1,Th15;
    then Den (action_at v2, A2) = Den (action_at v, A) by A1,A3,A5,Th27;
    hence (Following s).v = (Following s2).v by A1,A15,A19,A18,A17,Th29;
  end;
  now
    assume that
A20: v in the carrier of S2 and
A21: v in InputVertices S;
    reconsider v2 = v as Vertex of S2 by A20;
    v2 in InputVertices S2 by A1,A21,Th12;
    then
A22: (Following s2).v2 = s2.v2 by CIRCUIT2:def 5;
A23: dom s2 = the carrier of S2 by CIRCUIT1:3;
    (Following s).v = s.v by A21,CIRCUIT2:def 5;
    hence (Following s).v = (Following s2).v by A15,A22,A23,FUNCT_1:47;
  end;
  hence thesis by A16;
end;

theorem Th32:
  for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InnerVertices S1 misses InputVertices 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 being State of A1, s2 being State of A2 st s1 = s|the carrier of S1 & s2 = s
  |the carrier of S2 holds Following s = (Following s1)+*(Following s2)
proof
  let S1,S2,S be non void Circuit-like non empty ManySortedSign;
  assume that
A1: InnerVertices S1 misses InputVertices S2 and
A2: S = S1+*S2;
A3: the carrier of S = (the carrier of S1) \/ the carrier of S2 by A2,Def2;
  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, s1 be State of A1, s2 be State of A2 such that
A6: s1 = s|the carrier of S1 and
A7: s2 = s|the carrier of S2;
A8: dom Following s2 = the carrier of S2 by CIRCUIT1:3;
A9: dom Following s1 = the carrier of S1 by CIRCUIT1:3;
A10: now
    let x be object;
    assume x in (dom Following s1) \/ dom Following s2;
    then reconsider v = x as Vertex of S by A2,A9,A8,Def2;
    hereby
      assume x in dom Following s2;
      then reconsider v2 = x as Vertex of S2 by CIRCUIT1:3;
A11:  now
        the ResultSort of S = (the ResultSort of S1)+*the ResultSort of
        S2 by A2,Def2;
        then
A12:    rng the ResultSort of S c= (rng the ResultSort of S1) \/ rng the
        ResultSort of S2 by FUNCT_4:17;
        assume
A13:    v2 in InputVertices S2;
        then
A14:    not v2 in rng the ResultSort of S2 by XBOOLE_0:def 5;
        not v2 in rng the ResultSort of S1 by A1,A13,XBOOLE_0:3;
        then not v in rng the ResultSort of S by A14,A12,XBOOLE_0:def 3;
        hence v in InputVertices S by XBOOLE_0:def 5;
      end;
      InputVertices S2 \/ InnerVertices S2 = the carrier of S2 by XBOOLE_1:45;
      then v2 in InnerVertices S2 or v2 in InputVertices S2 by XBOOLE_0:def 3;
      then v in InnerVertices S2 or v in the carrier of S2 & v in
      InputVertices S by A11;
      hence (Following s).x = (Following s2).x by A2,A4,A5,A7,Th31;
    end;
    assume
A15: not x in dom Following s2;
    then reconsider v1 = v as Vertex of S1 by A3,A8,XBOOLE_0:def 3;
    rng the ResultSort of S2 c= the carrier of S2 by RELAT_1:def 19;
    then
A16: not v1 in rng the ResultSort of S2 by A8,A15;
A17: now
      assume v1 in InputVertices S1;
      then
A18:  not v1 in rng the ResultSort of S1 by XBOOLE_0:def 5;
      the ResultSort of S = (the ResultSort of S1)+*the ResultSort of S2
      by A2,Def2;
      then rng the ResultSort of S c= (rng the ResultSort of S1) \/ rng the
      ResultSort of S2 by FUNCT_4:17;
      then not v in rng the ResultSort of S by A16,A18,XBOOLE_0:def 3;
      hence v in InputVertices S by XBOOLE_0:def 5;
    end;
    InputVertices S1 \/ InnerVertices S1 = the carrier of S1 by XBOOLE_1:45;
    then v1 in InnerVertices S1 or v1 in InputVertices S1 by XBOOLE_0:def 3;
    hence (Following s).x = (Following s1).x by A2,A4,A5,A6,A17,Th31;
  end;
  dom Following s = the carrier of S by CIRCUIT1:3;
  hence thesis by A3,A9,A8,A10,FUNCT_4:def 1;
end;

theorem Th33:
  for S1,S2,S being non void Circuit-like non empty
ManySortedSign st InnerVertices S2 misses InputVertices 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,
s1 being State of A1, s2 being State of A2 st s1 = s|the carrier of S1 & s2 = s
  |the carrier of S2 holds Following s = (Following s2)+*(Following s1)
proof
  let S1,S2,S be non void Circuit-like non empty ManySortedSign such that
A1: InnerVertices S2 misses InputVertices 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;
  then
A5: S = S2+*S1 by A2,Th5;
  A = A2+*A1 by A3,A4,Th22;
  hence thesis by A1,A3,A5,Th19,Th32;
end;

theorem
  for S1,S2,S being non void Circuit-like non empty ManySortedSign st
  InputVertices S1 c= InputVertices 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 being State of
A1, s2 being State of A2 st s1 = s|the carrier of S1 & s2 = s|the carrier of S2
  holds Following s = (Following s2)+*(Following s1)
proof
  let S1,S2,S be non void Circuit-like non empty ManySortedSign;
  assume InputVertices S1 c= InputVertices S2;
  then InnerVertices S2 misses InputVertices S1 by XBOOLE_1:63,79;
  hence thesis by Th33;
end;

theorem
  for S1,S2,S being non void Circuit-like non empty ManySortedSign st
  InputVertices S2 c= InputVertices 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, s1 being State of
A1, s2 being State of A2 st s1 = s|the carrier of S1 & s2 = s|the carrier of S2
  holds Following s = (Following s1)+*(Following s2)
proof
  let S1,S2,S be non void Circuit-like non empty ManySortedSign;
  assume InputVertices S2 c= InputVertices S1;
  then InnerVertices S1 misses InputVertices S2 by XBOOLE_1:63,79;
  hence thesis by Th32;
end;

begin :: ManySortedSign with One Operation

definition
  let f be object;
  let p be FinSequence;
  let x be object;
  func 1GateCircStr(p,f,x) -> non void strict ManySortedSign means
  : Def5:
  the
  carrier of it = (rng p) \/ {x} & the carrier' of it = {[p,f]} & (the Arity of
  it).[p,f] = p & (the ResultSort of it).[p,f] = x;
  existence
  proof
    set pf = [p,f];
    reconsider C = (rng p) \/ {x} as non empty set;
    x in {x} by TARSKI:def 1;
    then reconsider ox = x as Element of C by XBOOLE_0:def 3;
    rng p c= C by XBOOLE_1:7;
    then p is FinSequence of C by FINSEQ_1:def 4;
    then reconsider pp = p as Element of C* by FINSEQ_1:def 11;
    reconsider R = {pf} --> ox as Function of {pf}, C;
    reconsider A = {pf} --> pp as Function of {pf}, C*;
    reconsider S = ManySortedSign(#C, {pf}, A, R#) as non void strict
    ManySortedSign;
    take S;
    pf in {pf} by TARSKI:def 1;
    hence thesis by FUNCOP_1:7;
  end;
  uniqueness
  proof
    let S1,S2 be non void strict ManySortedSign;
    assume
A1: not thesis;
    then dom the Arity of S1 = {[p,f]} by FUNCT_2:def 1;
    then
A2: the Arity of S1 = {[[p,f],p]} by A1,GRFUNC_1:7;
    dom the ResultSort of S1 = {[p,f]} by A1,FUNCT_2:def 1;
    then
A3: the ResultSort of S1 = {[[p,f],x]} by A1,GRFUNC_1:7;
    dom the Arity of S2 = {[p,f]} by A1,FUNCT_2:def 1;
    then
A4: the Arity of S2 = {[[p,f],p]} by A1,GRFUNC_1:7;
    dom the ResultSort of S2 = {[p,f]} by A1,FUNCT_2:def 1;
    hence thesis by A1,A2,A4,A3,GRFUNC_1:7;
  end;
end;

registration
  let f be object;
  let p be FinSequence;
  let x be object;
  cluster 1GateCircStr(p,f,x) -> non empty;
  coherence
  proof
    the carrier of 1GateCircStr(p,f,x) = rng p \/ {x} by Def5;
    hence the carrier of 1GateCircStr(p,f,x) is non empty;
  end;
end;

theorem Th36:
  for f,x being set, p being FinSequence holds the Arity of
1GateCircStr(p,f,x) = (p,f) .--> p & the ResultSort of 1GateCircStr(p,f,x) = (p
  ,f) .--> x
proof
  let f,x be set, p be FinSequence;
  set S = 1GateCircStr(p,f,x);
  (the Arity of S).[p,f] = p by Def5;
  then
A1: for x being object st x in {[p,f]} holds (the Arity of S).x = p by
TARSKI:def 1;
A2: the carrier' of S = {[p,f]} by Def5;
  then dom the Arity of S = {[p,f]} by FUNCT_2:def 1;
  hence the Arity of S = (p,f) .--> p by A1,FUNCOP_1:11;
  (the ResultSort of S).[p,f] = x by Def5;
  then
A3: for y being object st y in {[p,f]} holds (the ResultSort of S).y = x by
TARSKI:def 1;
  dom the ResultSort of S = {[p,f]} by A2,FUNCT_2:def 1;
  hence thesis by A3,FUNCOP_1:11;
end;

theorem
  for f,x being set, p being FinSequence for g being Gate of
1GateCircStr(p,f,x) holds g = [p,f] & the_arity_of g = p & the_result_sort_of g
  = x
proof
  let f,x be set, p be FinSequence;
  set S = 1GateCircStr(p,f,x);
  let o be Gate of 1GateCircStr(p,f,x);
A1: (the ResultSort of S).[p,f] = x by Def5;
A2: the carrier' of S = {[p,f]} by Def5;
  hence o = [p,f] by TARSKI:def 1;
  (the Arity of S).[p,f] = p by Def5;
  hence thesis by A2,A1,TARSKI:def 1;
end;

theorem
  for f,x being set, p being FinSequence holds InputVertices
  1GateCircStr(p,f,x) = (rng p) \ {x} & InnerVertices 1GateCircStr(p,f,x) = {x}
proof
  let f,x be set;
  let p be FinSequence;
  the ResultSort of 1GateCircStr(p,f,x) = (p,f) .--> x by Th36;
  then
A1: rng the ResultSort of 1GateCircStr(p,f,x) = {x} by FUNCOP_1:8;
  the carrier of 1GateCircStr(p,f,x) = (rng p) \/ {x} by Def5;
  hence thesis by A1,XBOOLE_1:40;
end;

definition
  let f be object;
  let p be FinSequence;
  func 1GateCircStr(p,f) -> non void strict ManySortedSign means
  : Def6:
  the
carrier of it = (rng p) \/ {[p,f]} & the carrier' of it = {[p,f]} & (the Arity
  of it).[p,f] = p & (the ResultSort of it).[p,f] = [p,f];
  existence
  proof
    take 1GateCircStr(p,f, [p,f]);
    thus thesis by Def5;
  end;
  uniqueness
  proof
    let S1,S2 be non void strict ManySortedSign;
    assume
A1: not thesis;
    then S1 = 1GateCircStr(p,f, [p,f]) by Def5;
    hence thesis by A1,Def5;
  end;
end;

registration
  let f be object;
  let p be FinSequence;
  cluster 1GateCircStr(p,f) -> non empty;
  coherence
  proof
    the carrier of 1GateCircStr(p,f) = rng p \/ {[p,f]} by Def6;
    hence the carrier of 1GateCircStr(p,f) is non empty;
  end;
end;

theorem
  for f being set, p being FinSequence holds 1GateCircStr(p,f) =
  1GateCircStr(p,f,[p,f])
proof
  let f be set, p be FinSequence;
  set S = 1GateCircStr(p,f);
A1: the carrier' of S = {[p,f]} by Def6;
A2: (the Arity of S).[p,f] = p by Def6;
A3: (the ResultSort of S).[p,f] = [p,f] by Def6;
  the carrier of S = (rng p) \/ {[p,f]} by Def6;
  hence thesis by A1,A2,A3,Def5;
end;

theorem Th40:
  for f being object, p being FinSequence holds the Arity of
1GateCircStr(p,f) = (p,f) .--> p & the ResultSort of 1GateCircStr(p,f) = (p,f)
  .--> [p,f]
proof
  let f be object, p be FinSequence;
  set S = 1GateCircStr(p,f);
  (the Arity of S).[p,f] = p by Def6;
  then
A1: for x being object st x in {[p,f]} holds (the Arity of S).x = p by
TARSKI:def 1;
A2: the carrier' of S = {[p,f]} by Def6;
  then dom the Arity of S = {[p,f]} by FUNCT_2:def 1;
  hence the Arity of 1GateCircStr(p,f) = (p,f) .--> p by A1,FUNCOP_1:11;
  (the ResultSort of S).[p,f] = [p,f] by Def6;
  then
A3: for x being object st x in {[p,f]} holds (the ResultSort of S).x = [p,f]
    by TARSKI:def 1;
  dom the ResultSort of S = {[p,f]} by A2,FUNCT_2:def 1;
  hence thesis by A3,FUNCOP_1:11;
end;

theorem Th41:
  for f being set, p being FinSequence for g being Gate of
1GateCircStr(p,f) holds g = [p,f] & the_arity_of g = p & the_result_sort_of g =
  g
proof
  let f be set, p be FinSequence;
  set S = 1GateCircStr(p,f);
  let o be Gate of 1GateCircStr(p,f);
  the carrier' of S = {[p,f]} by Def6;
  hence o = [p,f] by TARSKI:def 1;
  hence thesis by Def6;
end;

theorem Th42:
  for f being object, p being FinSequence holds InputVertices
  1GateCircStr(p,f) = rng p & InnerVertices 1GateCircStr(p,f) = {[p,f]}
proof
  let f be object;
  let p be FinSequence;
A1: the ResultSort of 1GateCircStr(p,f) = (p,f) .--> [p,f] by Th40;
  then
A2: rng the ResultSort of 1GateCircStr(p,f) = {[p,f]} by FUNCOP_1:8;
A3: the carrier of 1GateCircStr(p,f) = (rng p) \/ {[p,f]} by Def6;
  hence InputVertices 1GateCircStr(p,f) c= rng p by A2,XBOOLE_1:43;
A4: now
    assume [p,f] in rng p;
    then consider x being object such that
A5: [x,[p,f]] in p by XTUPLE_0:def 13;
A6: {x,[p,f]} in {{x,[p,f]},{x}} by TARSKI:def 2;
A7: {p,f} in {{p,f},{p}} by TARSKI:def 2;
A8: p in {p,f} by TARSKI:def 2;
    [p,f] in {x,[p,f]} by TARSKI:def 2;
    hence contradiction by A5,A8,A7,A6,XREGULAR:9;
  end;
  thus rng p c= InputVertices 1GateCircStr(p,f)
  proof
    let x be object;
    assume
A9: x in rng p;
    then
A10: x in (rng p) \/ {[p,f]} by XBOOLE_0:def 3;
    not x in {[p,f]} by A4,A9,TARSKI:def 1;
    hence thesis by A2,A3,A10,XBOOLE_0:def 5;
  end;
  thus thesis by A1,FUNCOP_1:8;
end;

theorem Th43:
  for f being set, p,q being FinSequence holds 1GateCircStr(p,f)
  tolerates 1GateCircStr(q,f)
proof
  let f be set, p,q be FinSequence;
  set S1 = 1GateCircStr(p,f), S2 = 1GateCircStr(q,f);
A1: [p,f] <> [q,f] implies {[p,f]} misses {[q,f]} by ZFMISC_1:11;
A2: the Arity of S2 = (q,f) .--> q by Th40;
  the Arity of S1 = (p,f) .--> p by Th40;
  hence the Arity of S1 tolerates the Arity of S2
   by A2,A1,XTUPLE_0:1;
A3: the ResultSort of S2 = (q,f) .--> [q,f] by Th40;
  the ResultSort of S1 = (p,f) .--> [p,f] by Th40;
  hence thesis by A3,A1;
end;

begin :: Unsplit condition

definition
  let IT be ManySortedSign;
  attr IT is unsplit means
  : Def7:
  the ResultSort of IT = id the carrier' of IT;
  attr IT is gate`1=arity means
  : Def8:
  for g being set st g in the carrier'
  of IT holds g = [(the Arity of IT).g, g`2];
  attr IT is gate`2isBoolean means
  : Def9:
  for g being set st g in the
  carrier' of IT for p being FinSequence st p = (the Arity of IT).g ex f being
  Function of (len p)-tuples_on BOOLEAN, BOOLEAN st g = [g`1, f];
end;

definition
  let S be non empty ManySortedSign;
  let IT be MSAlgebra over S;
  attr IT is gate`2=den means

  for g being set st g in the carrier' of
  S holds g = [g`1, (the Charact of IT).g];
end;

definition
  let IT be non empty ManySortedSign;
  attr IT is gate`2=den means
  ex A being MSAlgebra over IT st A is gate`2=den;
end;

scheme
  MSSLambdaWeak {A,B() -> set, g() -> Function of A(),B(),
     f(object,object) -> object}:
ex f being ManySortedSet of A() st for a being set, b being Element of B() st a
  in A() & b = g().a holds f.a = f(a,b) proof
  deffunc F(object) = f($1,g().$1);
  consider f being Function such that
A1: dom f = A() and
A2: for a being object st a in A() holds f.a = F(a) from FUNCT_1:sch 3;
  reconsider f as ManySortedSet of A() by A1,PARTFUN1:def 2,RELAT_1:def 18;
  take f;
  thus thesis by A2;
end;

scheme
  Lemma {S() -> non empty ManySortedSign, F(object,object) -> object}:
ex A being
strict MSAlgebra over S() st the Sorts of A = (the carrier of S()) --> BOOLEAN
  & for g being set, p being Element of (the carrier of S())* st g in the
carrier' of S() & p = (the Arity of S()).g holds (the Charact of A).g = F(g,p)
provided
A1: for g being set, p being Element of (the carrier of S())* st g in
the carrier' of S() & p = (the Arity of S()).g holds F(g,p) is Function of (len
p)-tuples_on BOOLEAN, BOOLEAN
proof
  set S = S(), SORTS = (the carrier of S) --> BOOLEAN;
  consider CHARACT being ManySortedSet of the carrier' of S such that
A2: for o being set, p being Element of (the carrier of S)* st o in the
  carrier' of S & p = (the Arity of S).o holds CHARACT.o = F(o,p) from
  MSSLambdaWeak;
A3: dom CHARACT = the carrier' of S by PARTFUN1:def 2;
  CHARACT is Function-yielding
  proof
    let x be object;
    assume
A4: x in dom CHARACT;
    then reconsider o = x as Gate of S by PARTFUN1:def 2;
    reconsider p = (the Arity of S).o as Element of (the carrier of S)* by A3
,A4,FUNCT_2:5;
    CHARACT.x = F(o,p) by A2,A3,A4;
    hence thesis by A1,A3,A4;
  end;
  then reconsider CHARACT as ManySortedFunction of the carrier' of S;
A5: dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
A6: dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
  now
    let i be object;
    assume
A7: i in the carrier' of S;
    then reconsider o = i as Gate of S;
    reconsider p = (the Arity of S).o as Element of (the carrier of S)* by A7,
FUNCT_2:5;
A8: (SORTS#*the Arity of S).i = SORTS#.p by A6,A7,FUNCT_1:13;
    reconsider v = (the ResultSort of S).o as Vertex of S by A7,FUNCT_2:5;
    SORTS.v = BOOLEAN;
    then
A9: (SORTS*the ResultSort of S).i = BOOLEAN by A5,A7,FUNCT_1:13;
A10: SORTS#.p = (len p)-tuples_on BOOLEAN by Th2;
    CHARACT.i = F(o,p) by A2,A7;
    hence CHARACT.i is Function of (SORTS#*the Arity of S).i, (SORTS*the
    ResultSort of S).i by A1,A7,A8,A10,A9;
  end;
  then reconsider
  CHARACT as ManySortedFunction of SORTS#*the Arity of S, SORTS*the
  ResultSort of S by PBOOLE:def 15;
  take MSAlgebra(#SORTS, CHARACT#);
  thus thesis by A2;
end;

registration
  cluster gate`2isBoolean -> gate`2=den for non empty ManySortedSign;
  coherence
  proof
    deffunc F(object,object) = $1`2;
    let S be non empty ManySortedSign;
    assume
A1: for g being set st g in the carrier' of S for p being FinSequence
    st p = (the Arity of S).g ex f being Function of (len p)-tuples_on BOOLEAN,
    BOOLEAN st g = [g`1,f];
A2: now
      let g be set, p be Element of (the carrier of S)*;
      assume that
A3:   g in the carrier' of S and
A4:   p = (the Arity of S).g;
      ex f being Function of (len p)-tuples_on BOOLEAN, BOOLEAN st g = [g
      `1,f] by A1,A3,A4;
      hence F(g,p) is Function of (len p)-tuples_on BOOLEAN, BOOLEAN;
    end;
    consider A being strict MSAlgebra over S such that
A5: the Sorts of A = (the carrier of S) --> BOOLEAN & for g being set,
    p being Element of (the carrier of S)* st g in the carrier' of S & p = (the
    Arity of S).g holds (the Charact of A).g = F(g,p) from Lemma(A2);
    take A;
    let g be set;
    assume
A6: g in the carrier' of S;
    then reconsider
    p = (the Arity of S).g as Element of (the carrier of S)* by FUNCT_2:5;
    consider f being Function of (len p)-tuples_on BOOLEAN, BOOLEAN such that
A7: g = [g`1,f] by A1,A6;
    f = g`2 by A7;
    hence thesis by A5,A6,A7;
  end;
end;

theorem Th44:
  for S being non empty ManySortedSign holds S is unsplit iff for
  o being object st o in the carrier' of S holds (the ResultSort of S).o = o
proof
  let S be non empty ManySortedSign;
  thus S is unsplit implies
  for o being object st o in the carrier' of S holds
  (the ResultSort of S).o = o by FUNCT_1:17;
  assume
A1: for o being object st o in the carrier' of S holds (the ResultSort of S
  ).o = o;
  dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
  hence the ResultSort of S = id the carrier' of S by A1,FUNCT_1:17;
end;

theorem
  for S being non empty ManySortedSign st S is unsplit holds the
  carrier' of S c= the carrier of S
proof
  let S be non empty ManySortedSign;
  assume
A1: S is unsplit;
  let x be object;
  assume
A2: x in the carrier' of S;
  then (the ResultSort of S).x = x by A1,Th44;
  hence thesis by A2,FUNCT_2:5;
end;

registration
  cluster unsplit -> Circuit-like for non empty ManySortedSign;
  coherence
  proof
    let S be non empty ManySortedSign such that
A1: the ResultSort of S = id the carrier' of S;
    let S9 be non void non empty ManySortedSign such that
A2: S9 = S;
    let o1,o2 be Gate of S9;
    thus thesis by A1,A2,FUNCT_1:17;
  end;
end;

theorem Th46:
  for f being object, p being FinSequence holds 1GateCircStr(p,f) is
  unsplit gate`1=arity
proof
  let f be object, p be FinSequence;
  set S = 1GateCircStr(p,f);
A1: now
    let x be object;
    assume x in {[p,f]};
    then x = [p,f] by TARSKI:def 1;
    hence (the ResultSort of S).x = x by Def6;
  end;
A2: the carrier' of S = {[p,f]} by Def6;
  then dom the ResultSort of S = {[p,f]} by FUNCT_2:def 1;
  hence the ResultSort of S = id the carrier' of S by A2,A1,FUNCT_1:17;
  let g be set;
  assume g in the carrier' of S;
  then
A3: g = [p,f] by A2,TARSKI:def 1;
  then (the Arity of S).g = p by Def6;
  hence thesis by A3;
end;

registration
  let f be object, p be FinSequence;
  cluster 1GateCircStr(p,f) -> unsplit gate`1=arity;
  coherence by Th46;
end;

registration
  cluster unsplit gate`1=arity non void strict non empty for ManySortedSign;
  existence
  proof
    set f = the set,p = the FinSequence;
    take 1GateCircStr(p,f);
    thus thesis;
  end;
end;

theorem Th47:
  for S1,S2 being unsplit gate`1=arity non empty ManySortedSign
  holds S1 tolerates S2
proof
  let S1,S2 be unsplit gate`1=arity non empty ManySortedSign;
  set A1 = the Arity of S1, A2 = the Arity of S2;
  set R1 = the ResultSort of S1, R2 = the ResultSort of S2;
  thus A1 tolerates A2
  proof
    let x be object;
    assume
A1: x in dom A1 /\ dom A2;
    then x in dom A2 by XBOOLE_0:def 4;
    then x in the carrier' of S2 by FUNCT_2:def 1;
    then
A2: x = [A2.x, x`2] by Def8;
    x in dom A1 by A1,XBOOLE_0:def 4;
    then x in the carrier' of S1 by FUNCT_2:def 1;
    then x = [A1.x, x`2] by Def8;
    hence thesis by A2,XTUPLE_0:1;
  end;
  let x be object;
  assume
A3: x in dom R1 /\ dom R2;
  then x in dom R1 by XBOOLE_0:def 4;
  then x in the carrier' of S1 by FUNCT_2:def 1;
  then
A4: R1.x = x by Th44;
  x in dom R2 by A3,XBOOLE_0:def 4;
  then x in the carrier' of S2 by FUNCT_2:def 1;
  hence thesis by A4,Th44;
end;

theorem Th48:
  for S1,S2 being non empty ManySortedSign, A1 being MSAlgebra
  over S1 for A2 being MSAlgebra over S2 st A1 is gate`2=den & A2 is gate`2=den
  holds the Charact of A1 tolerates the Charact of A2
proof
  let S1,S2 be non empty ManySortedSign;
  let A1 be MSAlgebra over S1, A2 be MSAlgebra over S2 such that
A1: A1 is gate`2=den and
A2: A2 is gate`2=den;
  let x be object;
  set C1 = the Charact of A1, C2 = the Charact of A2;
  assume
A3: x in dom C1 /\ dom C2;
  then x in dom C2 by XBOOLE_0:def 4;
  then x in the carrier' of S2 by PARTFUN1:def 2;
  then
A4: x = [x`1, C2.x] by A2;
  x in dom C1 by A3,XBOOLE_0:def 4;
  then x in the carrier' of S1 by PARTFUN1:def 2;
  then x = [x`1, C1.x] by A1;
  hence thesis by A4,XTUPLE_0:1;
end;

theorem Th49:
  for S1,S2 being unsplit non empty ManySortedSign holds S1+*S2 is unsplit
proof
  let S1,S2 be unsplit non empty ManySortedSign;
  set S = S1+*S2;
A1: the ResultSort of S = (the ResultSort of S1)+*the ResultSort of S2 by Def2;
A2: the ResultSort of S1 = id the carrier' of S1 by Def7;
A3: the ResultSort of S2 = id the carrier' of S2 by Def7;
  the carrier' of S = (the carrier' of S1) \/ the carrier' of S2 by Def2;
  hence the ResultSort of S = id the carrier' of S by A1,A2,A3,FUNCT_4:22;
end;

registration
  let S1,S2 be unsplit non empty ManySortedSign;
  cluster S1+*S2 -> unsplit;
  coherence by Th49;
end;

theorem Th50:
  for S1,S2 being gate`1=arity non empty ManySortedSign holds S1+*
  S2 is gate`1=arity
proof
  let S1,S2 be gate`1=arity non empty ManySortedSign;
  set S = S1+*S2;
  let g be set;
A1: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;
A2: the Arity of S = (the Arity of S1)+*the Arity of S2 by Def2;
  assume
A3: g in the carrier' of S;
  then reconsider g as Gate of S;
A4: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
A5: the carrier' of S = (the carrier' of S1) \/ the carrier' of S2 by Def2;
  then
A6: g in the carrier' of S1 or g in the carrier' of S2 by A3,XBOOLE_0:def 3;
A7: now
    assume
A8: not g in the carrier' of S2;
    then reconsider g1 = g as Gate of S1 by A5,A3,XBOOLE_0:def 3;
    thus g = [(the Arity of S1).g1, g`2] by A6,A8,Def8
      .= [(the Arity of S).g, g`2] by A5,A2,A3,A1,A4,A8,FUNCT_4:def 1;
  end;
  now
    assume
A9: g in the carrier' of S2;
    then reconsider g2 = g as Gate of S2;
    thus g = [(the Arity of S2).g2, g`2] by A9,Def8
      .= [(the Arity of S).g, g`2] by A5,A2,A1,A4,A9,FUNCT_4:def 1;
  end;
  hence thesis by A7;
end;

registration
  let S1,S2 be gate`1=arity non empty ManySortedSign;
  cluster S1+*S2 -> gate`1=arity;
  coherence by Th50;
end;

theorem Th51:
  for S1,S2 being non empty ManySortedSign st S1 is
  gate`2isBoolean & S2 is gate`2isBoolean holds S1+*S2 is gate`2isBoolean
proof
  let S1,S2 be non empty ManySortedSign;
  set S = S1+*S2;
  assume that
A1: S1 is gate`2isBoolean and
A2: S2 is gate`2isBoolean;
  let g be set;
  assume
A3: g in the carrier' of S;
  let p be FinSequence such that
A4: p = (the Arity of S).g;
  reconsider g as Gate of S by A3;
A5: dom the Arity of S1 = the carrier' of S1 by FUNCT_2:def 1;
A6: the Arity of S = (the Arity of S1)+*the Arity of S2 by Def2;
A7: dom the Arity of S2 = the carrier' of S2 by FUNCT_2:def 1;
A8: the carrier' of S = (the carrier' of S1) \/ the carrier' of S2 by Def2;
  then
A9: g in the carrier' of S1 or g in the carrier' of S2 by A3,XBOOLE_0:def 3;
A10: now
    assume
A11: not g in the carrier' of S2;
    then reconsider g1 = g as Gate of S1 by A8,A3,XBOOLE_0:def 3;
    (the Arity of S1).g1 = p by A8,A6,A3,A4,A5,A7,A11,FUNCT_4:def 1;
    hence thesis by A1,A9,A11;
  end;
  now
    assume
A12: g in the carrier' of S2;
    then reconsider g2 = g as Gate of S2;
    (the Arity of S2).g2 = p by A8,A6,A4,A5,A7,A12,FUNCT_4:def 1;
    hence thesis by A2,A12;
  end;
  hence thesis by A10;
end;

begin :: One Gate Circuit

definition
  let n be Nat;
  mode FinSeqLen of n is n-element FinSequence;
end;

definition
  let n be Nat;
  let X,Y be non empty set;
  let f be Function of n-tuples_on X, Y;
  let p be FinSeqLen of n;
  let x be set such that
A1: x in rng p implies X = Y;
  func 1GateCircuit(p,f,x) -> strict non-empty MSAlgebra over 1GateCircStr(p,f
  ,x) means
  the Sorts of it = ((rng p) --> X) +* (x .--> Y) & (the Charact of it)
  .[p,f] = f;
  existence
  proof
    p is FinSequence of rng p by FINSEQ_1:def 4;
    then reconsider p9 = p as Element of (rng p)* by FINSEQ_1:def 11;
    set g1 = (rng p) --> X, g2 = x .--> Y;
    set S = 1GateCircStr(p,f,x);
    set SORTS = g1 +* g2;
    set CHARACT = (the carrier' of S) --> f;
A2: dom (x .--> Y) = {x};
A3: x in {x} by TARSKI:def 1;
    then
A4: SORTS.x = (x .--> Y).x by A2,FUNCT_4:13
      .= Y by A3,FUNCOP_1:7;
A5: the carrier of S = (rng p) \/ {x} by Def5;
    then reconsider SORTS as non-empty ManySortedSet of the carrier of S;
    rng p c= the carrier of S by A5,XBOOLE_1:7;
    then p is FinSequence of the carrier of S by FINSEQ_1:def 4;
    then reconsider pp = p as Element of (the carrier of S)* by FINSEQ_1:def 11
;
A6: dom (g1# ) = (rng p)* by PARTFUN1:def 2;
    g1 tolerates g2
    proof
      let y be object;
      assume
A8:   y in dom g1 /\ dom g2;
      then y in rng p by XBOOLE_0:def 4;
      then
A9:   g1.y = X by FUNCOP_1:7;
A10:  y in {x} by A8,XBOOLE_0:def 4;
      then x = y by TARSKI:def 1;
      hence thesis by A1,A8,A10,A9,FUNCOP_1:7,XBOOLE_0:def 4;
    end;
    then g1 c= SORTS by FUNCT_4:28;
    then g1# c= SORTS# by Th1;
    then
A11: g1#.p9 = SORTS#.pp by A6,GRFUNC_1:2;
A12: the carrier' of S = {[p,f]} by Def5;
    then
A13: dom the ResultSort of S = {[p,f]} by FUNCT_2:def 1;
A14: (the ResultSort of S).[p,f] = x by Def5;
A15: (the Arity of S).[p,f] = p by Def5;
A16: len p = n by CARD_1:def 7;
A17: dom the Arity of S = {[p,f]} by A12,FUNCT_2:def 1;
    now
      let i be object;
A18:  SORTS#.pp = n-tuples_on X by A16,A11,Th2;
      assume
A19:  i in the carrier' of S;
      then
A20:  i = [p,f] by A12,TARSKI:def 1;
      then
A21:  (SORTS#*the Arity of S).i = SORTS#.p by A12,A15,A17,A19,FUNCT_1:13;
      (SORTS*the ResultSort of S).i = Y by A12,A14,A4,A13,A19,A20,FUNCT_1:13;
      hence CHARACT.i is Function of (SORTS#*the Arity of S).i, (SORTS*the
      ResultSort of S).i by A19,A21,A18,FUNCOP_1:7;
    end;
    then reconsider
    CHARACT as ManySortedFunction of SORTS#*the Arity of S, SORTS*
    the ResultSort of S by PBOOLE:def 15;
    reconsider A = MSAlgebra(#SORTS, CHARACT#) as non-empty strict MSAlgebra
    over 1GateCircStr(p,f,x) by MSUALG_1:def 3;
    take A;
    [p,f] in {[p,f]} by TARSKI:def 1;
    hence thesis by A12,FUNCOP_1:7;
  end;
  uniqueness
  proof
    set S = 1GateCircStr(p,f,x);
    let A1,A2 be strict non-empty MSAlgebra over S such that
A22: not thesis;
A23: the carrier' of S = {[p,f]} by Def5;
    then dom the Charact of A1 = {[p,f]} by PARTFUN1:def 2;
    then
A24: the Charact of A1 = {[[p,f],f]} by A22,GRFUNC_1:7;
    dom the Charact of A2 = {[p,f]} by A23,PARTFUN1:def 2;
    hence thesis by A22,A24,GRFUNC_1:7;
  end;
end;

definition
  let n be Nat;
  let X be non empty set;
  let f be Function of n-tuples_on X, X;
  let p be FinSeqLen of n;
  func 1GateCircuit(p,f) -> strict non-empty MSAlgebra over 1GateCircStr(p,f)
  means
  : Def13:
  the Sorts of it = (the carrier of 1GateCircStr(p,f)) --> X & (
  the Charact of it).[p,f] = f;
  existence
  proof
    set S = 1GateCircStr(p,f);
    set SORTS = (the carrier of S) --> X;
    set CHARACT = (the carrier' of S) --> f;
A1: len p = n by CARD_1:def 7;
A2: (the Arity of S).[p,f] = p by Def6;
A3: (the ResultSort of S).[p,f] = [p,f] by Def6;
A4: the carrier' of S = {[p,f]} by Def6;
    then
A5: dom the ResultSort of S = {[p,f]} by FUNCT_2:def 1;
A6: the carrier of S = (rng p) \/ {[p,f]} by Def6;
    then rng p c= the carrier of S by XBOOLE_1:7;
    then p is FinSequence of the carrier of S by FINSEQ_1:def 4;
    then reconsider pp = p as Element of (the carrier of S)* by FINSEQ_1:def 11
;
A7: [p,f] in {[p,f]} by TARSKI:def 1;
    then [p,f] in the carrier of S by A6,XBOOLE_0:def 3;
    then
A8: SORTS.[p,f] = X by FUNCOP_1:7;
A9: dom the Arity of S = {[p,f]} by A4,FUNCT_2:def 1;
    now
      let i be object;
A10:  SORTS#.pp = n-tuples_on X by A1,Th2;
      assume
A11:  i in the carrier' of S;
      then
A12:  i = [p,f] by A4,TARSKI:def 1;
      then
A13:  (SORTS#*the Arity of S).i = SORTS#.p by A4,A2,A9,A11,FUNCT_1:13;
      (SORTS*the ResultSort of S).i = X by A4,A3,A8,A5,A11,A12,FUNCT_1:13;
      hence CHARACT.i is Function of (SORTS#*the Arity of S).i, (SORTS*the
      ResultSort of S).i by A11,A13,A10,FUNCOP_1:7;
    end;
    then reconsider
    CHARACT as ManySortedFunction of SORTS#*the Arity of S, SORTS*
    the ResultSort of S by PBOOLE:def 15;
    reconsider A = MSAlgebra(#SORTS, CHARACT#) as non-empty strict MSAlgebra
    over 1GateCircStr(p,f) by MSUALG_1:def 3;
    take A;
    thus thesis by A4,A7,FUNCOP_1:7;
  end;
  uniqueness
  proof
    set S = 1GateCircStr(p,f);
    let A1,A2 be strict non-empty MSAlgebra over S such that
A14: not thesis;
A15: the carrier' of S = {[p,f]} by Def6;
    then dom the Charact of A1 = {[p,f]} by PARTFUN1:def 2;
    then
A16: the Charact of A1 = {[[p,f],f]} by A14,GRFUNC_1:7;
    dom the Charact of A2 = {[p,f]} by A15,PARTFUN1:def 2;
    hence thesis by A14,A16,GRFUNC_1:7;
  end;
end;

theorem Th52:
  for n being Nat, X being non empty set for f being Function of n
  -tuples_on X, X for p being FinSeqLen of n holds 1GateCircuit(p,f) is
  gate`2=den & 1GateCircStr(p,f) is gate`2=den
proof
  let n be Nat;
  let X be non empty set;
  let f be Function of n-tuples_on X, X;
  let p be FinSeqLen of n;
  thus
A1: 1GateCircuit(p,f) is gate`2=den
  proof
    let g be set;
    assume g in the carrier' of 1GateCircStr(p,f);
    then
A2: g = [p,f] by Th41;
    hence g = [g`1, f]
      .= [g`1, (the Charact of 1GateCircuit(p,f)).g] by A2,Def13;
  end;
  take 1GateCircuit(p,f);
  thus thesis by A1;
end;

registration
  let n be Nat, X be non empty set;
  let f be Function of n-tuples_on X, X;
  let p be FinSeqLen of n;
  cluster 1GateCircuit(p,f) -> gate`2=den;
  coherence by Th52;
  cluster 1GateCircStr(p,f) -> gate`2=den;
  coherence by Th52;
end;

theorem Th53:
  for n being Nat for p being FinSeqLen of n for f being Function
  of n-tuples_on BOOLEAN, BOOLEAN holds 1GateCircStr(p,f) is gate`2isBoolean
proof
  set X = BOOLEAN;
  let n be Nat;
  let p be FinSeqLen of n;
  let f be Function of n-tuples_on X, X;
  let g be set;
A1: len p = n by CARD_1:def 7;
A2: (the Arity of 1GateCircStr(p,f)).[p,f] = p by Def6;
  assume g in the carrier' of 1GateCircStr(p,f);
  then
A3: g = [p,f] by Th41;
  let q be FinSequence;
  assume q = (the Arity of 1GateCircStr(p,f)).g;
  then reconsider f as Function of (len q)-tuples_on X, X by A3,A2,A1;
  take f;
  thus thesis by A3;
end;

registration
  let n be Nat;
  let f be Function of n-tuples_on BOOLEAN, BOOLEAN;
  let p be FinSeqLen of n;
  cluster 1GateCircStr(p,f) -> gate`2isBoolean;
  coherence by Th53;
end;

registration
  cluster gate`2isBoolean non empty for ManySortedSign;
  existence
  proof
    set p = the FinSeqLen of 0;
    set f = the Function of 0-tuples_on BOOLEAN, BOOLEAN;
    take 1GateCircStr(p,f);
    thus thesis;
  end;
end;

registration
  let S1,S2 be gate`2isBoolean non empty ManySortedSign;
  cluster S1+*S2 -> gate`2isBoolean;
  coherence by Th51;
end;

theorem Th54:
  for n being Nat, X being non empty set, f being Function of n
-tuples_on X, X for p being FinSeqLen of n holds the Charact of 1GateCircuit(p,
f) = (p,f) .--> f & for v being Vertex of 1GateCircStr(p,f) holds (the Sorts of
  1GateCircuit(p,f)).v = X
proof
  let n be Nat, X be non empty set, f be Function of n-tuples_on X, X;
  let p be FinSeqLen of n;
  set S = 1GateCircStr(p,f), A = 1GateCircuit(p,f);
  (the Charact of A).[p,f] = f by Def13;
  then
A1: for x being object st x in {[p,f]} holds (the Charact of A).x = f by
TARSKI:def 1;
  the carrier' of S = {[p,f]} by Def6;
  then dom the Charact of A = {[p,f]} by PARTFUN1:def 2;
  hence the Charact of A = (p,f) .--> f by A1,FUNCOP_1:11;
  let v be Vertex of S;
  the Sorts of A = (the carrier of S) --> X by Def13;
  hence thesis;
end;

registration
  let n be Nat;
  let X be non empty finite set;
  let f be Function of n-tuples_on X, X;
  let p be FinSeqLen of n;
  cluster 1GateCircuit(p,f) -> finite-yielding;
  coherence
  proof
    let i be object;
    set S = 1GateCircStr(p,f);
    assume i in the carrier of S;
    hence thesis by Th54;
  end;
end;

theorem
  for n being Nat, X being non empty set, f being Function of n
  -tuples_on X, X, p,q being FinSeqLen of n holds 1GateCircuit(p,f) tolerates
  1GateCircuit(q,f)
proof
  let n be Nat, X be non empty set, f be Function of n-tuples_on X, X;
  let p,q be FinSeqLen of n;
  set S1 = 1GateCircStr(p,f), S2 = 1GateCircStr(q,f);
  set A1 = 1GateCircuit(p,f), A2 = 1GateCircuit(q,f);
  thus 1GateCircStr(p,f) tolerates 1GateCircStr(q,f) by Th43;
A1: the Sorts of A2 = (the carrier of S2) --> X by Def13;
  the Sorts of A1 = (the carrier of S1) --> X by Def13;
  hence the Sorts of A1 tolerates the Sorts of A2 by A1,FUNCOP_1:87;
A2: the Charact of A2 = (q,f) .--> f by Th54;
  the Charact of A1 = (p,f) .--> f by Th54;
  hence thesis by A2,FUNCOP_1:87;
end;

theorem
  for n being Nat, X being finite non empty set, f being Function of n
-tuples_on X, X, p being FinSeqLen of n for s being State of 1GateCircuit(p,f)
  holds (Following s).[p,f] = f.(s*p)
proof
  let n be Nat;
  let X be non empty finite set;
  let f be Function of n-tuples_on X, X;
  let p be FinSeqLen of n;
  let s be State of 1GateCircuit(p,f);
  set S = 1GateCircStr(p,f), A = 1GateCircuit(p,f);
  set IV = InnerVertices S;
  IV = {[p,f]} by Th42;
  then reconsider v = [p,f] as Element of IV by TARSKI:def 1;
  the carrier' of S = {[p,f]} by Def6;
  then reconsider o = [p,f] as Gate of S by TARSKI:def 1;
  the_result_sort_of o = v by Def6;
  then
A1: action_at v = o by MSAFREE2:def 7;
  the_arity_of o = p by Def6;
  then
A2: o depends_on_in s = s*p by CIRCUIT1:def 3;
  (Following s).v = (Den (action_at v, A)).(action_at v depends_on_in s)
  by CIRCUIT2:def 5;
  hence thesis by A1,A2,Def13;
end;

begin :: Boolean Circuits

:: definition
::   redefine func BOOLEAN -> Subset of NAT;
::   coherence by MARGREL1:def 12,ZFMISC_1:38;
:: end;

definition
  let S be non empty ManySortedSign;
  let IT be MSAlgebra over S;
  attr IT is Boolean means

  for v being Vertex of S holds (the Sorts of IT).v = BOOLEAN;
end;

theorem Th57:
  for S being non empty ManySortedSign, A being MSAlgebra over S
  holds A is Boolean iff the Sorts of A = (the carrier of S) --> BOOLEAN
proof
  let S be non empty ManySortedSign, A be MSAlgebra over S;
A1: dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
  thus A is Boolean implies the Sorts of A = (the carrier of S) --> BOOLEAN
  proof
    assume for v being Vertex of S holds (the Sorts of A).v = BOOLEAN;
    then for v being object st v in the carrier of S
     holds (the Sorts of A).v = BOOLEAN;
    hence thesis by A1,FUNCOP_1:11;
  end;
  assume
A2: the Sorts of A = (the carrier of S) --> BOOLEAN;
  let v be Vertex of S;
  thus thesis by A2;
end;

registration
  let S be non empty ManySortedSign;
  cluster Boolean -> non-empty finite-yielding for MSAlgebra over S;
  coherence
  proof
    let A be MSAlgebra over S;
    assume
A1: A is Boolean;
    then the Sorts of A = (the carrier of S) --> BOOLEAN by Th57;
    hence A is non-empty;
    let v be object;
    thus thesis by A1;
  end;
end;

theorem
  for S being non empty ManySortedSign, A being MSAlgebra over S holds A
  is Boolean iff rng the Sorts of A c= {BOOLEAN}
proof
  let S be non empty ManySortedSign, A be MSAlgebra over S;
  hereby
    assume A is Boolean;
    then the Sorts of A = (the carrier of S) --> BOOLEAN by Th57;
    hence rng the Sorts of A c= {BOOLEAN} by FUNCOP_1:13;
  end;
  assume
A1: rng the Sorts of A c= {BOOLEAN};
  let v be Vertex of S;
  dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
  then (the Sorts of A).v in rng the Sorts of A by FUNCT_1:def 3;
  hence thesis by A1,TARSKI:def 1;
end;

theorem Th59:
  for S1,S2 being non empty ManySortedSign for A1 being MSAlgebra
over S1, A2 being MSAlgebra over S2 st A1 is Boolean & A2 is Boolean holds the
  Sorts of A1 tolerates the Sorts of A2
proof
  let S1,S2 be non empty ManySortedSign;
  let A1 be MSAlgebra over S1, A2 be MSAlgebra over S2;
  assume that
A1: A1 is Boolean and
A2: A2 is Boolean;
A3: the Sorts of A2 = (the carrier of S2) --> BOOLEAN by A2,Th57;
  the Sorts of A1 = (the carrier of S1) --> BOOLEAN by A1,Th57;
  hence thesis by A3,FUNCOP_1:87;
end;

theorem Th60:
  for S1,S2 being unsplit gate`1=arity non empty ManySortedSign
  for A1 being MSAlgebra over S1, A2 being MSAlgebra over S2 st A1 is Boolean
  gate`2=den & A2 is Boolean gate`2=den holds A1 tolerates A2
by Th47,Th48,Th59;

registration
  let S be non empty ManySortedSign;
  cluster Boolean for strict MSAlgebra over S;
  existence
  proof
    deffunc F(set,Element of (the carrier of S)*) = ((len $2)-tuples_on
    BOOLEAN) --> FALSE;
A1: for g being set, p being Element of (the carrier of S)* st g in the
    carrier' of S & p = (the Arity of S).g holds F(g,p) is Function of (len p)
    -tuples_on BOOLEAN, BOOLEAN;
    consider A being strict MSAlgebra over S such that
A2: the Sorts of A = (the carrier of S) --> BOOLEAN & for g being set,
    p being Element of (the carrier of S)* st g in the carrier' of S & p = (the
    Arity of S).g holds (the Charact of A).g = F(g,p) from Lemma(A1);
    take A;
    let v be Vertex of S;
    thus thesis by A2;
  end;
end;

theorem
  for n being Nat, f being Function of n-tuples_on BOOLEAN, BOOLEAN for
  p being FinSeqLen of n holds 1GateCircuit(p,f) is Boolean
proof
  let n be Nat, f be Function of n-tuples_on BOOLEAN, BOOLEAN;
  let p be FinSeqLen of n;
  set S = 1GateCircStr(p,f), A = 1GateCircuit(p,f);
  let v be Vertex of S;
  the Sorts of A = (the carrier of S) --> BOOLEAN by Def13;
  hence thesis;
end;

theorem Th62:
  for S1,S2 being non empty ManySortedSign for A1 be Boolean
  MSAlgebra over S1 for A2 be Boolean MSAlgebra over S2 holds A1+*A2 is Boolean
proof
  let S1,S2 be non empty ManySortedSign;
  let A1 be Boolean MSAlgebra over S1;
  let A2 be Boolean MSAlgebra over S2;
  set A = A1+*A2;
  set S = S1+*S2;
  let x be Vertex of S;
  the carrier of S = (the carrier of S1) \/ the carrier of S2 by Def2;
  then
A3: x in the carrier of S1 or x in the carrier of S2 by XBOOLE_0:def 3;
A4: the Sorts of A2 = (the carrier of S2) --> BOOLEAN by Th57;
A5: the Sorts of A1 = (the carrier of S1) --> BOOLEAN by Th57;
  then
A6: the Sorts of A1 tolerates the Sorts of A2 by A4,FUNCOP_1:87;
  then the Sorts of A = (the Sorts of A1)+*the Sorts of A2 by Def4;
  then
  (the Sorts of A).x = (the Sorts of A1).x & (the Sorts of A1).x = BOOLEAN
or (the Sorts of A).x = (the Sorts of A2).x & (the Sorts of A2).x = BOOLEAN by
A5,A4,A6,A3,FUNCOP_1:7,FUNCT_4:13,15;
  hence thesis;
end;

theorem Th63:
  for S1,S2 being non empty ManySortedSign for A1 be non-empty
  MSAlgebra over S1, A2 be non-empty MSAlgebra over S2 st A1 is gate`2=den & A2
  is gate`2=den & the Sorts of A1 tolerates the Sorts of A2 holds A1+*A2 is
  gate`2=den
proof
  let S1,S2 be non empty ManySortedSign;
  let A1 be non-empty MSAlgebra over S1;
  let A2 be non-empty MSAlgebra over S2;
  set A = A1+*A2;
  set S = S1+*S2;
  assume that
A1: A1 is gate`2=den and
A2: A2 is gate`2=den and
A3: the Sorts of A1 tolerates the Sorts of A2;
A4: the Charact of A = (the Charact of A1)+*the Charact of A2 by A3,Def4;
  let g be set;
A5: dom the Charact of A1 = the carrier' of S1 by PARTFUN1:def 2;
A6: dom the Charact of A2 = the carrier' of S2 by PARTFUN1:def 2;
A7: the carrier' of S = (the carrier' of S1) \/ the carrier' of S2 by Def2;
  assume g in the carrier' of S;
  then
A8: g in the carrier' of S1 or g in the carrier' of S2 by A7,XBOOLE_0:def 3;
  the Charact of A1 tolerates the Charact of A2 by A1,A2,Th48;
  then
  (the Charact of A).g = (the Charact of A1).g & [g`1, (the Charact of A1
  ).g] = g or (the Charact of A).g = (the Charact of A2).g & [g`1, (the Charact
  of A2).g] = g by A1,A2,A4,A5,A6,A8,FUNCT_4:13,15;
  hence thesis;
end;

registration
  cluster unsplit gate`1=arity gate`2=den gate`2isBoolean non void strict for
non
    empty ManySortedSign;
  existence
  proof
    set p = the FinSeqLen of 1;
    set f = the Function of 1-tuples_on BOOLEAN, BOOLEAN;
    take 1GateCircStr(p,f);
    thus thesis;
  end;
end;

registration
  let S be gate`2isBoolean non empty ManySortedSign;
  cluster Boolean gate`2=den for strict MSAlgebra over S;
  existence
  proof
    deffunc F(set,set) = $1`2;
A1: now
      let g be set, p be Element of (the carrier of S)*;
      assume that
A2:   g in the carrier' of S and
A3:   p = (the Arity of S).g;
      ex f being Function of (len p)-tuples_on BOOLEAN, BOOLEAN st g = [g
      `1, f] by A2,A3,Def9;
      hence F(g,p) is Function of (len p)-tuples_on BOOLEAN, BOOLEAN;
    end;
    consider A being strict MSAlgebra over S such that
A4: the Sorts of A = (the carrier of S) --> BOOLEAN & for g being set,
    p being Element of (the carrier of S)* st g in the carrier' of S & p = (the
    Arity of S).g holds (the Charact of A).g = F(g,p) from Lemma(A1);
    take A;
    thus A is Boolean
    by A4;
    let g be set;
    assume
A5: g in the carrier' of S;
    then reconsider
    p = (the Arity of S).g as Element of (the carrier of S)* by FUNCT_2:5;
    consider f being Function of (len p)-tuples_on BOOLEAN, BOOLEAN such that
A6: g = [g`1, f] by A5,Def9;
    g`2 = f by A6;
    hence thesis by A4,A5,A6;
  end;
end;

registration
  let S1,S2 be unsplit gate`2isBoolean non void non empty ManySortedSign;
  let A1 be Boolean gate`2=den Circuit of S1;
  let A2 be Boolean gate`2=den Circuit of S2;
  cluster A1+*A2 -> Boolean gate`2=den;
  coherence
  proof
    the Sorts of A1 tolerates the Sorts of A2 by Th59;
    hence thesis by Th62,Th63;
  end;
end;

registration
  let n be Nat;
  let X be finite non empty set;
  let f be Function of n-tuples_on X, X;
  let p be FinSeqLen of n;
  cluster gate`2=den strict non-empty for Circuit of 1GateCircStr(p,f);
  existence
  proof
    take 1GateCircuit(p,f);
    thus thesis;
  end;
end;

registration
  let n be Nat;
  let X be finite non empty set;
  let f be Function of n-tuples_on X, X;
  let p be FinSeqLen of n;
  cluster 1GateCircuit(p,f) -> gate`2=den;
  coherence;
end;

theorem
  for S1,S2 being unsplit gate`1=arity gate`2isBoolean non void non
empty ManySortedSign for A1 being Boolean gate`2=den Circuit of S1 for A2 being
Boolean gate`2=den Circuit of S2 for s being State of A1+*A2, v being Vertex of
  S1+*S2 holds (for s1 being State of A1 st s1 = s|the carrier of S1 holds v in
InnerVertices S1 or v in the carrier of S1 & v in InputVertices(S1+*S2) implies
  (Following s).v = (Following s1).v) & for s2 being State of A2 st s2 = s|the
  carrier of S2 holds v in InnerVertices S2 or v in the carrier of S2 & v in
  InputVertices(S1+*S2) implies (Following s).v = (Following s2).v
proof
  let S1,S2 be unsplit gate`1=arity gate`2isBoolean non void non empty
  ManySortedSign;
  let A1 be Boolean gate`2=den Circuit of S1;
  let A2 be Boolean gate`2=den Circuit of S2;
  A1 tolerates A2 by Th60;
  hence thesis by Th31;
end;