The abstract of the Mizar article:

Combining of Circuits

by

Yatsuka Nakamura, and

Grzegorz Bancerek

Received May 11, 1995

MML identifier: CIRCCOMB

[ Mizar article, MML identifier index ]

environ

 vocabulary MSUALG_1, FUNCT_1, FUNCOP_1, PRALG_1, RELAT_1, CARD_3, FINSEQ_1,
      FINSEQ_2, AMI_1, ZF_REFLE, FUNCT_4, BOOLE, PBOOLE, PARTFUN1, TDGROUP,
      MSAFREE2, FINSET_1, QC_LANG1, PRE_CIRC, CIRCUIT1, CLASSES1, MCART_1,
      MARGREL1, LATTICES, CIRCCOMB;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, NAT_1, MCART_1, RELAT_1,
      FUNCT_1, STRUCT_0, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_2, FUNCOP_1,
      PARTFUN1, FUNCT_4, GROUP_1, CARD_3, CLASSES1, MARGREL1, PBOOLE, PRALG_1,
      MSUALG_1, PRE_CIRC, MSAFREE2, CIRCUIT1, CIRCUIT2;
 constructors MCART_1, CLASSES1, MARGREL1, PRALG_1, CIRCUIT1, CIRCUIT2;
 clusters RELSET_1, FUNCT_1, FINSET_1, PRVECT_1, PBOOLE, MSUALG_1, MSAFREE2,
      STRUCT_0, MSUALG_2, FINSEQ_2, CANTOR_1, MARGREL1, FUNCOP_1, ARYTM_3,
      ORDINAL1, XBOOLE_0, FRAENKEL, MEMBERED, ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET;


begin :: Combining of ManySortedSign's

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

definition let A be set; let f be Function;
 cluster A --> f -> Function-yielding;
end;

definition
 let f,g be non-empty Function;
 cluster f+*g -> non-empty;
end;

definition
 let A,B be set;
 let f be ManySortedSet of A;
 let g be ManySortedSet of B;
 redefine func f+*g -> ManySortedSet of A \/ B;
end;

theorem :: CIRCCOMB:1
 for f1,f2, g1,g2 being Function st
  rng g1 c= dom f1 & rng g2 c= dom f2 & f1 tolerates f2
   holds (f1+*f2)*(g1+*g2) = (f1*g1)+*(f2*g2);

theorem :: CIRCCOMB:2
 for f1,f2, g being Function st
  rng g c= dom f1 & rng g c= dom f2 & f1 tolerates f2
 holds f1*g = f2*g;

theorem :: CIRCCOMB:3
 for A,B being set, f being ManySortedSet of A
  for g being ManySortedSet of B st f c= g holds f# c= g#;

theorem :: CIRCCOMB:4
 for X,Y,x,y being set holds X --> x tolerates Y --> y iff x = y or X misses Y;

theorem :: CIRCCOMB:5
 for f,g,h being Function st f tolerates g & g tolerates h & h tolerates f
  holds f+*g tolerates h;

theorem :: CIRCCOMB:6
 for X being set, Y being non empty set, p being FinSequence of X holds
  (X --> Y)#.p = (len p)-tuples_on Y;

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

definition
 let S1,S2 be ManySortedSign;
 pred S1 tolerates S2 means
:: CIRCCOMB:def 1
    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
:: CIRCCOMB:def 2
  the carrier of it = (the carrier of S1) \/ (the carrier of S2) &
  the OperSymbols of it = (the OperSymbols of S1) \/ (the OperSymbols 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);
end;

theorem :: CIRCCOMB:7
 for S1,S2,S3 being non empty ManySortedSign st
 S1 tolerates S2 & S2 tolerates S3 & S3 tolerates S1
  holds S1+*S2 tolerates S3;

theorem :: CIRCCOMB:8
 for S being non empty ManySortedSign holds S+*S = the ManySortedSign of S;

theorem :: CIRCCOMB:9
 for S1,S2 being non empty ManySortedSign st
  S1 tolerates S2 holds S1+*S2 = S2+*S1;

theorem :: CIRCCOMB:10
 for S1,S2,S3 being non empty ManySortedSign holds (S1+*S2)+*S3 = S1+*(S2+*S3);

definition
 cluster one-to-one Function;
end;

theorem :: CIRCCOMB:11
   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;

theorem :: CIRCCOMB:12
   for S1,S2 being Circuit-like (non empty ManySortedSign) st
  InnerVertices S1 misses InnerVertices S2
 holds S1+*S2 is Circuit-like;

theorem :: CIRCCOMB:13
 for S1,S2 being non empty ManySortedSign st
  S1 is not void or S2 is not void holds S1+*S2 is non void;

theorem :: CIRCCOMB:14
   for S1,S2 being finite non empty ManySortedSign holds S1+*S2 is finite;

definition
 let S1 be non void non empty ManySortedSign;
 let S2 be non empty ManySortedSign;
 cluster S1 +* S2 -> non void;
 cluster S2 +* S1 -> non void;
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 :: CIRCCOMB:15
 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);

theorem :: CIRCCOMB:16
 for S1,S2 being non empty ManySortedSign
 for v2 being Vertex of S2 st v2 in InputVertices (S1+*S2) holds
  v2 in InputVertices S2;

theorem :: CIRCCOMB:17
 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;

theorem :: CIRCCOMB:18
 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;

theorem :: CIRCCOMB:19
 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;

theorem :: CIRCCOMB:20
 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;


theorem :: CIRCCOMB:21
 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;

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
:: CIRCCOMB:def 3
  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
    the Sorts of A1 tolerates the Sorts of A2;
 func A1 +* A2 -> strict non-empty MSAlgebra over S1+*S2 means
:: CIRCCOMB:def 4
  the Sorts of it = (the Sorts of A1) +* (the Sorts of A2) &
  the Charact of it = (the Charact of A1) +* (the Charact of A2);
end;

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

theorem :: CIRCCOMB:23
 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 :: CIRCCOMB:24
   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
;

theorem :: CIRCCOMB:25
   for S being strict non empty ManySortedSign,
     A being non-empty MSAlgebra over S holds
   A+*A = the MSAlgebra of A;

theorem :: CIRCCOMB:26
 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;

theorem :: CIRCCOMB:27
   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);

theorem :: CIRCCOMB:28
   for S1,S2 being non empty ManySortedSign
 for A1 being locally-finite non-empty MSAlgebra over S1
 for A2 being locally-finite non-empty MSAlgebra over S2 st
  the Sorts of A1 tolerates the Sorts of A2 holds A1+*A2 is locally-finite;

theorem :: CIRCCOMB:29
 for f,g being non-empty Function, x being Element of product f,
  y being Element of product g holds x+*y in product (f+*g);

theorem :: CIRCCOMB:30
 for f,g being non-empty Function
 for x being Element of product (f+*g) holds x|dom g in product g;

theorem :: CIRCCOMB:31
 for f,g being non-empty Function st f tolerates g
 for x being Element of product (f+*g) holds x|dom f in product f;

theorem :: CIRCCOMB:32
   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;

theorem :: CIRCCOMB:33
   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;

theorem :: CIRCCOMB:34
 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);

theorem :: CIRCCOMB:35
 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);

theorem :: CIRCCOMB:36
 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;

theorem :: CIRCCOMB:37
 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;

theorem :: CIRCCOMB:38
 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);

theorem :: CIRCCOMB:39
 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);

theorem :: CIRCCOMB:40
 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);

theorem :: CIRCCOMB:41
   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);

theorem :: CIRCCOMB:42
   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);

begin :: ManySortedSign with One Operation

definition
 let A,B be non empty set;
 let a be Element of A;
 redefine func B --> a -> Function of B,A;
end;

definition
 let f be set;
 let p be FinSequence;
 let x be set;
 func 1GateCircStr(p,f,x) -> non void strict ManySortedSign means
:: CIRCCOMB:def 5

  the carrier of it = (rng p) \/ {x} &
  the OperSymbols of it = {[p,f]} &
  (the Arity of it).[p,f] = p &
  (the ResultSort of it).[p,f] = x;
end;

definition
 let f be set;
 let p be FinSequence;
 let x be set;
 cluster 1GateCircStr(p,f,x) -> non empty;
end;

theorem :: CIRCCOMB:43
 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;

theorem :: CIRCCOMB:44
   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;

theorem :: CIRCCOMB:45
   for f,x being set, p being FinSequence holds
  InputVertices 1GateCircStr(p,f,x) = (rng p) \ {x} &
   InnerVertices 1GateCircStr(p,f,x) = {x};

definition
 let f be set;
 let p be FinSequence;
 func 1GateCircStr(p,f) -> non void strict ManySortedSign means
:: CIRCCOMB:def 6

  the carrier of it = (rng p) \/ {[p,f]} &
  the OperSymbols of it = {[p,f]} &
  (the Arity of it).[p,f] = p &
  (the ResultSort of it).[p,f] = [p,f];
end;

definition
 let f be set;
 let p be FinSequence;
 cluster 1GateCircStr(p,f) -> non empty;
end;

theorem :: CIRCCOMB:46
   for f being set, p being FinSequence holds
  1GateCircStr(p,f) = 1GateCircStr(p,f,[p,f]);

theorem :: CIRCCOMB:47
 for f being set, p being FinSequence holds
  the Arity of 1GateCircStr(p,f) = {[p,f]} --> p &
  the ResultSort of 1GateCircStr(p,f) = {[p,f]} --> [p,f];

theorem :: CIRCCOMB:48
 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;

theorem :: CIRCCOMB:49
 for f being set, p being FinSequence holds
  InputVertices 1GateCircStr(p,f) = rng p &
   InnerVertices 1GateCircStr(p,f) = {[p,f]};

theorem :: CIRCCOMB:50
   for f being set, p being FinSequence
  for x being set st x in rng p holds the_rank_of x in the_rank_of [p,f];

theorem :: CIRCCOMB:51
 for f being set, p,q being FinSequence holds
  1GateCircStr(p,f) tolerates 1GateCircStr(q,f);

begin :: Unsplit condition

definition let IT be ManySortedSign;
 attr IT is unsplit means
:: CIRCCOMB:def 7

  the ResultSort of IT = id the OperSymbols of IT;
 attr IT is gate`1=arity means
:: CIRCCOMB:def 8

  for g being set st g in the OperSymbols of IT holds
   g = [(the Arity of IT).g, g`2];
 attr IT is gate`2isBoolean means
:: CIRCCOMB:def 9

  for g being set st g in the OperSymbols 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
:: CIRCCOMB:def 10

  for g being set st g in the OperSymbols 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
:: CIRCCOMB:def 11
    ex A being MSAlgebra over IT st A is gate`2=den;
end;

definition
 cluster gate`2isBoolean -> gate`2=den (non empty ManySortedSign);
end;

theorem :: CIRCCOMB:52
 for S being non empty ManySortedSign holds S is unsplit iff
  for o being set st o in the OperSymbols of S holds
   (the ResultSort of S).o = o;

theorem :: CIRCCOMB:53
   for S being non empty ManySortedSign st S is unsplit holds
  the OperSymbols of S c= the carrier of S;

definition
 cluster unsplit -> Circuit-like (non empty ManySortedSign);
end;

theorem :: CIRCCOMB:54
 for f being set, p being FinSequence holds
  1GateCircStr(p,f) is unsplit gate`1=arity;

definition
 let f be set, p be FinSequence;
 cluster 1GateCircStr(p,f) -> unsplit gate`1=arity;
end;

definition
 cluster unsplit gate`1=arity non void strict non empty ManySortedSign;
end;

theorem :: CIRCCOMB:55
 for S1,S2 being unsplit gate`1=arity non empty ManySortedSign holds
 S1 tolerates S2;

theorem :: CIRCCOMB:56
 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;

theorem :: CIRCCOMB:57
 for S1,S2 being unsplit non empty ManySortedSign holds S1+*S2 is unsplit;

definition
 let S1,S2 be unsplit non empty ManySortedSign;
 cluster S1+*S2 -> unsplit;
end;

theorem :: CIRCCOMB:58
 for S1,S2 being gate`1=arity non empty ManySortedSign holds
   S1+*S2 is gate`1=arity;

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

theorem :: CIRCCOMB:59
 for S1,S2 being non empty ManySortedSign st
    S1 is gate`2isBoolean & S2 is gate`2isBoolean
   holds S1+*S2 is gate`2isBoolean;

begin :: One Gate Circuit

definition let n be Nat;
 mode FinSeqLen of n -> FinSequence means
:: CIRCCOMB:def 12

  len it = n;
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
  x in rng p implies X = Y;
 func 1GateCircuit(p,f,x) ->
      strict non-empty MSAlgebra over 1GateCircStr(p,f,x) means
:: CIRCCOMB:def 13
    the Sorts of it = ((rng p) --> X) +* ({x} --> Y) &
  (the Charact of it).[p,f] = f;
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
:: CIRCCOMB:def 14

  the Sorts of it = (the carrier of 1GateCircStr(p,f)) --> X &
  (the Charact of it).[p,f] = f;
end;

theorem :: CIRCCOMB:60
 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;

definition
 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;
 cluster 1GateCircStr(p,f) -> gate`2=den;
end;

theorem :: CIRCCOMB:61
 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;

definition
 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;
end;

definition
 cluster gate`2isBoolean non empty ManySortedSign;
end;

definition
 let S1,S2 be gate`2isBoolean non empty ManySortedSign;
 cluster S1+*S2 -> gate`2isBoolean;
end;

theorem :: CIRCCOMB:62
 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;

definition 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) -> locally-finite;
end;

theorem :: CIRCCOMB:63
   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);

theorem :: CIRCCOMB:64
   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);

begin :: Boolean Circuits

definition
 redefine func BOOLEAN -> finite non empty Subset of NAT;
end;

definition
 let S be non empty ManySortedSign;
 let IT be MSAlgebra over S;
 attr IT is Boolean means
:: CIRCCOMB:def 15

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

theorem :: CIRCCOMB:65
 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;

definition
 let S be non empty ManySortedSign;
 cluster Boolean -> non-empty locally-finite MSAlgebra over S;
end;

theorem :: CIRCCOMB:66
   for S being non empty ManySortedSign, A being MSAlgebra over S holds
  A is Boolean iff rng the Sorts of A c= {BOOLEAN};

theorem :: CIRCCOMB:67
 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
;

theorem :: CIRCCOMB:68
 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;

definition let S be non empty ManySortedSign;
 cluster Boolean (strict MSAlgebra over S);
end;

theorem :: CIRCCOMB:69
   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;

theorem :: CIRCCOMB:70
 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;

theorem :: CIRCCOMB:71
 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;

definition
 cluster unsplit gate`1=arity gate`2=den gate`2isBoolean non void
         strict (non empty ManySortedSign);
end;

definition
 let S be gate`2isBoolean non empty ManySortedSign;
 cluster Boolean gate`2=den (strict MSAlgebra over S);
end;

definition
 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;
end;

definition 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 Circuit of 1GateCircStr(p,f);
end;

definition 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;
end;

theorem :: CIRCCOMB:72
   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);