The abstract of the Mizar article:

Preliminaries to Automatic Generation of Mizar Documentation for Circuits

by

Grzegorz Bancerek, and

Adam Naumowicz

Received July 26, 2002

MML identifier: CIRCCMB3

[ Mizar article, MML identifier index ]

environ

 vocabulary BOOLE, CIRCCMB3, MSUALG_1, CIRCCOMB, FUNCT_1, FINSEQ_2, AMI_1,
      CIRCUIT1, MSAFREE2, NET_1, TARSKI, ZF_REFLE, PRE_CIRC, FINSET_1, RELAT_1,
      FINSEQ_1, FUNCOP_1, PBOOLE, SEQM_3, CIRCUIT2, PARTFUN1, FUNCT_4,
      SQUARE_1, REWRITE1, CLASSES1, ORDINAL2, CATALG_1, YELLOW_6, FUNCT_5,
      MCART_1, TDGROUP, QC_LANG1, FACIRC_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, ENUMSET1, SCMPDS_1,
      ZFMISC_1, RELAT_1, FUNCT_1, FINSET_1, ORDINAL2, CLASSES1, FUNCT_2, NAT_1,
      PARTFUN1, LIMFUNC1, REWRITE1, STRUCT_0, FINSEQ_1, FINSEQ_2, FINSEQOP,
      PBOOLE, GROUP_1, MSUALG_1, FACIRC_1, MSAFREE2, CIRCUIT1, CIRCUIT2,
      CIRCCOMB, PRE_CIRC, MCART_1, BINARITH, FUNCT_5, SEQM_3, YELLOW_6;
 constructors CIRCUIT1, CIRCUIT2, FACIRC_1, REWRITE1, CLASSES1, FINSEQOP,
      PRALG_1, SCMPDS_1, LIMFUNC1, BINARITH, YELLOW_6, SEQM_3, DOMAIN_1;
 clusters MSUALG_1, CIRCCOMB, PRE_CIRC, FINSET_1, CIRCTRM1, RELSET_1, FINSEQ_1,
      FINSEQ_2, PRALG_1, STRUCT_0, SCMPDS_1, FSM_1, XBOOLE_0, ORDINAL1,
      YELLOW_6, MSAFREE, FACIRC_1, MEMBERED, SEQM_3, NUMBERS, ORDINAL2;
 requirements BOOLE, SUBSET, NUMERALS, REAL;


begin :: Stabilizing circuits

theorem :: CIRCCMB3:1
 for S being non void Circuit-like (non empty ManySortedSign)
 for A being non-empty Circuit of S
 for s being State of A, x being set st x in InputVertices S
 for n being Nat holds Following(s,n).x = s.x;

definition
 let S be non void Circuit-like (non empty ManySortedSign);
 let A be non-empty Circuit of S;
 let s be State of A;
 attr s is stabilizing means
:: CIRCCMB3:def 1
 ex n being Nat st Following(s,n) is stable;
end;

definition
 let S be non void Circuit-like (non empty ManySortedSign);
 let A be non-empty Circuit of S;
 attr A is stabilizing means
:: CIRCCMB3:def 2
 for s being State of A holds s is stabilizing;
 attr A is with_stabilization-limit means
:: CIRCCMB3:def 3
   ex n being Nat st
 for s being State of A holds Following(s,n) is stable;
end;

definition
 let S be non void Circuit-like (non empty ManySortedSign);
 cluster with_stabilization-limit -> stabilizing (non-empty Circuit of S);
end;

definition
 let S be non void Circuit-like (non empty ManySortedSign);
 let A be non-empty Circuit of S;
 let s be State of A such that  s is stabilizing;
 func Result s -> State of A means
:: CIRCCMB3:def 4
 it is stable & ex n being Nat st it = Following(s,n);
end;

definition
 let S be non void Circuit-like (non empty ManySortedSign);
 let A be non-empty Circuit of S;
 let s be State of A such that  s is stabilizing;
 func stabilization-time s -> Nat means
:: CIRCCMB3:def 5
 Following(s,it) is stable & for n being Nat st n < it holds
 not Following(s,n) is stable;
end;

theorem :: CIRCCMB3:2
 for S being non void Circuit-like (non empty ManySortedSign)
 for A being non-empty Circuit of S
 for s being State of A st s is stabilizing holds
   Result s = Following(s,stabilization-time s);

theorem :: CIRCCMB3:3
   for S being non void Circuit-like (non empty ManySortedSign)
 for A being non-empty Circuit of S
 for s being State of A, n being Nat st Following(s,n) is stable
  holds stabilization-time s <= n;

theorem :: CIRCCMB3:4
 for S being non void Circuit-like (non empty ManySortedSign)
 for A being non-empty Circuit of S
 for s being State of A, n being Nat st Following(s,n) is stable
  holds Result s = Following(s, n);

theorem :: CIRCCMB3:5
 for S being non void Circuit-like (non empty ManySortedSign)
 for A being non-empty Circuit of S
 for s being State of A, n being Nat
  st s is stabilizing & n >= stabilization-time s
  holds Result s = Following(s, n);

theorem :: CIRCCMB3:6
   for S being non void Circuit-like (non empty ManySortedSign)
 for A being non-empty Circuit of S
 for s being State of A st s is stabilizing
 for x being set st x in InputVertices S
  holds (Result s).x = s.x;

theorem :: CIRCCMB3:7
   for S1,S being non void Circuit-like (non empty ManySortedSign)
 for A1 being non-empty Circuit of S1
 for A being non-empty Circuit of S
 for s being State of A
 for s1 being State of A1 st s1 = s|the carrier of S1
 for v1 being Vertex of S1 holds s1.v1 = s.v1;

theorem :: CIRCCMB3:8
 for S1,S2 being non void Circuit-like (non empty ManySortedSign) st
 InputVertices S1 misses InnerVertices S2 &
 InputVertices S2 misses InnerVertices S1
 for S being non void Circuit-like (non empty ManySortedSign) st S=S1 +* S2
 for A1 being non-empty Circuit of S1
 for A2 being non-empty Circuit of S2 st
 A1 tolerates A2
 for A being non-empty Circuit of S st A = A1 +* A2
 for s being State of A
 for s1 being State of A1
 for s2 being State of A2 st
 s1=s|the carrier of S1 & s2=s|the carrier of S2 &
 s1 is stabilizing & s2 is stabilizing holds s is stabilizing;

theorem :: CIRCCMB3:9
   for S1,S2 being non void Circuit-like (non empty ManySortedSign) st
 InputVertices S1 misses InnerVertices S2 &
 InputVertices S2 misses InnerVertices S1
 for S being non void Circuit-like (non empty ManySortedSign) st S=S1 +* S2
 for A1 being non-empty Circuit of S1
 for A2 being non-empty Circuit of S2 st
 A1 tolerates A2
 for A being non-empty Circuit of S st A = A1 +* A2
 for s being State of A
 for s1 being State of A1 st s1=s|the carrier of S1 & s1 is stabilizing
 for s2 being State of A2 st s2=s|the carrier of S2 & s2 is stabilizing holds
 stabilization-time(s) = max (stabilization-time s1,stabilization-time s2);

theorem :: CIRCCMB3:10
 for S1,S2 being non void Circuit-like (non empty ManySortedSign) st
 InputVertices S1 misses InnerVertices S2
 for S being non void Circuit-like (non empty ManySortedSign) st S=S1 +* S2
 for A1 being non-empty Circuit of S1
 for A2 being non-empty Circuit of S2 st
 A1 tolerates A2
 for A being non-empty Circuit of S st A = A1 +* A2
 for s being State of A
 for s1 being State of A1 st s1 = s|the carrier of S1 & s1 is stabilizing
 for s2 being State of A2
  st s2 = Following(s, stabilization-time s1)|the carrier of S2 &
     s2 is stabilizing
  holds s is stabilizing;

theorem :: CIRCCMB3:11
 for S1,S2 being non void Circuit-like (non empty ManySortedSign) st
 InputVertices S1 misses InnerVertices S2
 for S being non void Circuit-like (non empty ManySortedSign) st S = S1+*S2
 for A1 being non-empty Circuit of S1
 for A2 being non-empty Circuit of S2 st
 A1 tolerates A2
 for A being non-empty Circuit of S st A = A1 +* A2
 for s being State of A
 for s1 being State of A1 st s1 = s|the carrier of S1 & s1 is stabilizing
 for s2 being State of A2
  st s2 = Following(s, stabilization-time s1)|the carrier of S2 &
     s2 is stabilizing
  holds stabilization-time(s) = (stabilization-time s1)+(stabilization-time s2)
;

theorem :: CIRCCMB3:12
   for S1,S2,S being non void Circuit-like (non empty ManySortedSign)
  st InputVertices S1 misses InnerVertices S2 & S = S1+*S2
 for A1 being non-empty Circuit of S1, A2 being non-empty Circuit of S2
 for A being non-empty Circuit of S
  st A1 tolerates A2 & A = A1+*A2
 for s being State of A, s1 be State of A1
  st s1 = s|the carrier of S1 & s1 is stabilizing
 for s2 being State of A2
  st s2 = Following(s, stabilization-time s1)|the carrier of S2 &
     s2 is stabilizing
  holds (Result s)|the carrier of S1 = Result s1;

begin :: One-gate circuits

theorem :: CIRCCMB3:13
 for x being set, X being non empty finite set
 for n being Nat
 for p being FinSeqLen of n
 for g being Function of n-tuples_on X, X
 for s being State of 1GateCircuit(p,g) holds
 s*p is Element of n-tuples_on X;

theorem :: CIRCCMB3:14
 for x1,x2,x3,x4 being set holds
 rng <*x1,x2,x3,x4*> = {x1,x2,x3,x4};

theorem :: CIRCCMB3:15
 for x1,x2,x3,x4,x5 being set holds
 rng <*x1,x2,x3,x4,x5*> = {x1,x2,x3,x4,x5};

definition
 let x1,x2,x3,x4 be set;
 redefine func <*x1,x2,x3,x4*> -> FinSeqLen of 4;
 let x5 be set;
 redefine func <*x1,x2,x3,x4,x5*> -> FinSeqLen of 5;
end;

definition
 let S be ManySortedSign;
 attr S is one-gate means
:: CIRCCMB3:def 6
  ex X being non empty finite set, n being Nat, p being FinSeqLen of n,
  f being Function of n-tuples_on X,X st
  S = 1GateCircStr(p,f);
end;

definition
 let S be non empty ManySortedSign;
 let A be MSAlgebra over S;
 attr A is one-gate means
:: CIRCCMB3:def 7
  ex X being non empty finite set, n being Nat, p being FinSeqLen of n,
  f being Function of n-tuples_on X,X st
  S = 1GateCircStr(p,f) & A = 1GateCircuit(p,f);
end;

definition
 let p being FinSequence, x be set;
 cluster 1GateCircStr(p,x) -> finite;
end;

definition
 cluster one-gate -> strict non void non empty unsplit gate`1=arity
 finite ManySortedSign;
end;

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

definition
 let X be non empty finite set,
     n be Nat, p be FinSeqLen of n,
     f be Function of n-tuples_on X,X;
 cluster 1GateCircStr(p,f) -> one-gate;
end;

definition
 cluster one-gate ManySortedSign;
end;

definition
 let S be one-gate ManySortedSign;
 cluster one-gate -> strict non-empty Circuit of S;
end;

definition
 let X be non empty finite set,
     n be Nat, p be FinSeqLen of n,
     f be Function of n-tuples_on X,X;
 cluster 1GateCircuit(p,f) -> one-gate;
end;

definition
 let S be one-gate ManySortedSign;
 cluster one-gate non-empty Circuit of S;
end;

definition
 let S be one-gate ManySortedSign;
 func Output S -> Vertex of S equals
:: CIRCCMB3:def 8
union the OperSymbols of S;
end;

definition
 let S be one-gate ManySortedSign;
 cluster Output S -> pair;
end;

theorem :: CIRCCMB3:16
 for S being one-gate ManySortedSign,
 p being FinSequence, x being set st S = 1GateCircStr(p,x) holds
 Output S = [p,x];

theorem :: CIRCCMB3:17
 for S being one-gate ManySortedSign holds InnerVertices S = {Output S};

theorem :: CIRCCMB3:18
   for S being one-gate ManySortedSign
 for A being one-gate Circuit of S
 for n being Nat
 for X being finite non empty set
 for f being Function of n-tuples_on X, X, p being FinSeqLen of n st
 A = 1GateCircuit(p,f) holds S = 1GateCircStr(p,f);

theorem :: CIRCCMB3:19
   for n being Nat
 for X being finite non empty set
 for 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).Output 1GateCircStr(p,f) = f.(s*p);

theorem :: CIRCCMB3:20
 for S being one-gate ManySortedSign
 for A being one-gate Circuit of S
 for s being State of A holds Following s is stable;

definition
 let S be non void Circuit-like (non empty ManySortedSign);
 cluster one-gate -> with_stabilization-limit (non-empty Circuit of S);
end;

theorem :: CIRCCMB3:21
 for S being one-gate ManySortedSign
 for A being one-gate Circuit of S
 for s being State of A holds
 Result s = Following s;

theorem :: CIRCCMB3:22
 for S being one-gate ManySortedSign
 for A being one-gate Circuit of S
 for s being State of A holds
 stabilization-time s <= 1;

scheme OneGate1Ex {x()->set,X()->non empty finite set,f(set)->Element of X()}:
 ex S being one-gate ManySortedSign,
 A being one-gate Circuit of S st
 InputVertices S = {x()} & for s being State of A holds
 (Result s).(Output S) = f(s.x());

scheme OneGate2Ex {x1,x2()->set,X()->non empty finite set,
                   f(set,set)->Element of X()}:
 ex S being one-gate ManySortedSign,
 A being one-gate Circuit of S st
 InputVertices S = {x1(),x2()} & for s being State of A holds
 (Result s).(Output S) = f(s.x1(),s.x2());

scheme OneGate3Ex {x1,x2,x3()->set,X()->non empty finite set,
                   f(set,set,set)->Element of X()}:
 ex S being one-gate ManySortedSign,
 A being one-gate Circuit of S st
 InputVertices S = {x1(),x2(),x3()} & for s being State of A holds
 (Result s).(Output S) = f(s.x1(),s.x2(),s.x3());

scheme OneGate4Ex {x1,x2,x3,x4()->set,X()->non empty finite set,
                   f(set,set,set,set)->Element of X()}:
 ex S being one-gate ManySortedSign,
 A being one-gate Circuit of S st
 InputVertices S = {x1(),x2(),x3(),x4()} & for s being State of A holds
 (Result s).(Output S) = f(s.x1(),s.x2(),s.x3(),s.x4());

scheme OneGate5Ex {x1,x2,x3,x4,x5()->set,X()->non empty finite set,
                   f(set,set,set,set,set)->Element of X()}:
 ex S being one-gate ManySortedSign,
 A being one-gate Circuit of S st
 InputVertices S = {x1(),x2(),x3(),x4(),x5()} & for s being State of A holds
 (Result s).(Output S) = f(s.x1(),s.x2(),s.x3(),s.x4(),s.x5());

begin :: Mono-sorted circuits

theorem :: CIRCCMB3:23
 for f being constant Function
 holds f = (dom f) --> the_value_of f;

theorem :: CIRCCMB3:24
 for X,Y being non empty set, n,m being Nat st
 n<>0 & n-tuples_on X = m-tuples_on Y
 holds X=Y & n=m;

theorem :: CIRCCMB3:25
   for S1,S2 being non empty ManySortedSign
 for v being Vertex of S1 holds v is Vertex of S1+*S2;

theorem :: CIRCCMB3:26
   for S1,S2 being non empty ManySortedSign
 for v being Vertex of S2 holds v is Vertex of S1+*S2;

definition
 let X be non empty finite set;
 mode Signature of X ->
 gate`2=den (non void non empty unsplit gate`1=arity ManySortedSign) means
:: CIRCCMB3:def 9

 ex A being Circuit of it st the Sorts of A is constant &
 the_value_of the Sorts of A = X & A is gate`2=den;
end;

theorem :: CIRCCMB3:27
 for n being Nat, X being non empty finite set
 for f being Function of n-tuples_on X, X
 for p being FinSeqLen of n
  holds 1GateCircStr(p,f) is Signature of X;

definition
 let X be non empty finite set;
 cluster strict one-gate Signature of X;
end;

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;
 redefine func 1GateCircStr(p,f) -> strict Signature of X;
end;

definition
 let X be non empty finite set;
 let S be Signature of X;
 mode Circuit of X,S -> Circuit of S means
:: CIRCCMB3:def 10
 it is gate`2=den &
 the Sorts of it is constant & the_value_of the Sorts of it = X;
end;

definition
 let X be non empty finite set;
 let S be Signature of X;
 cluster -> gate`2=den non-empty Circuit of X,S;
end;

theorem :: CIRCCMB3:28
 for n being Nat, X being non empty finite set
 for f being Function of n-tuples_on X, X
 for p being FinSeqLen of n
  holds 1GateCircuit(p,f) is Circuit of X, 1GateCircStr(p,f);

definition
 let X be non empty finite set;
 let S be one-gate Signature of X;
 cluster strict one-gate Circuit of X,S;
end;

definition
 let X be non empty finite set;
 let S be Signature of X;
 cluster strict Circuit of X,S;
end;

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;
 redefine func 1GateCircuit(p,f) -> strict Circuit of X,1GateCircStr(p,f);
end;

canceled;

theorem :: CIRCCMB3:30
 for X being non empty finite set
 for S1, S2 being Signature of X
 for A1 being Circuit of X,S1
 for A2 being Circuit of X,S2
  holds A1 tolerates A2;

theorem :: CIRCCMB3:31
 for X being non empty finite set
 for S1, S2 being Signature of X
 for A1 being Circuit of X,S1
 for A2 being Circuit of X,S2
  holds A1+*A2 is Circuit of S1+*S2;

theorem :: CIRCCMB3:32
 for X being non empty finite set
 for S1, S2 being Signature of X
 for A1 being Circuit of X,S1
 for A2 being Circuit of X,S2
  holds A1+*A2 is gate`2=den;

theorem :: CIRCCMB3:33
 for X being non empty finite set
 for S1, S2 being Signature of X
 for A1 being Circuit of X,S1
 for A2 being Circuit of X,S2
  holds the Sorts of A1+*A2 is constant &
        the_value_of the Sorts of A1+*A2 = X;

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

definition let X be non empty finite set;
 let S1,S2 be Signature of X;
 cluster S1+*S2 -> gate`2=den;
end;

definition let X be non empty finite set;
 let S1,S2 be Signature of X;
 redefine func S1+*S2 -> strict Signature of X;
end;

definition let X be non empty finite set;
 let S1,S2 be Signature of X;
 let A1 be Circuit of X,S1;
 let A2 be Circuit of X,S2;
 redefine func A1+*A2 -> strict Circuit of X,S1+*S2;
end;

theorem :: CIRCCMB3:34
for x,y being set holds
the_rank_of x in the_rank_of [x,y] & the_rank_of y in the_rank_of [x,y];

theorem :: CIRCCMB3:35
 for S being gate`2=den finite
 (non void non empty unsplit gate`1=arity ManySortedSign)
 for A being non-empty Circuit of S st A is gate`2=den holds
 A is with_stabilization-limit;

definition
 let X be non empty finite set;
 let S be finite Signature of X;
 cluster -> with_stabilization-limit Circuit of X,S;
end;

scheme 1AryDef {X()-> non empty set,F(set) -> Element of X()}:
 (ex f being Function of 1-tuples_on X(), X() st
  for x being Element of X() holds f.<*x*> = F(x)) &
 for f1,f2 being Function of 1-tuples_on X(), X() st
  (for x being Element of X() holds f1.<*x*> = F(x)) &
  (for x being Element of X() holds f2.<*x*> = F(x))
 holds f1 = f2;

scheme 2AryDef {X()-> non empty set,F(set,set) -> Element of X()}:
 (ex f being Function of 2-tuples_on X(), X() st
  for x,y being Element of X() holds f.<*x,y*> = F(x,y)) &
 for f1,f2 being Function of 2-tuples_on X(), X() st
  (for x,y being Element of X() holds f1.<*x,y*> = F(x,y)) &
  (for x,y being Element of X() holds f2.<*x,y*> = F(x,y))
 holds f1 = f2;

scheme 3AryDef {X()-> non empty set,F(set,set,set) -> Element of X()}:
 (ex f being Function of 3-tuples_on X(), X() st
  for x,y,z being Element of X() holds f.<*x,y,z*> = F(x,y,z)) &
 for f1,f2 being Function of 3-tuples_on X(), X() st
  (for x,y,z being Element of X() holds f1.<*x,y,z*> = F(x,y,z)) &
  (for x,y,z being Element of X() holds f2.<*x,y,z*> = F(x,y,z))
 holds f1 = f2;

theorem :: CIRCCMB3:36
 for f being Function, x being set st x in dom f
  holds f*<*x*> = <*f.x*>;

theorem :: CIRCCMB3:37
 for f being Function for x1,x2,x3,x4 being set st
  x1 in dom f & x2 in dom f & x3 in dom f & x4 in dom f holds
   f*<*x1,x2,x3,x4*> = <*f.x1,f.x2,f.x3,f.x4*>;

theorem :: CIRCCMB3:38
 for f being Function for x1,x2,x3,x4,x5 being set st
  x1 in dom f & x2 in dom f & x3 in dom f & x4 in dom f & x5 in dom f holds
   f*<*x1,x2,x3,x4,x5*> = <*f.x1,f.x2,f.x3,f.x4,f.x5*>;

scheme OneGate1Result
 {x1()-> set, B()-> non empty finite set, F(set)->Element of B(),
  f() -> Function of 1-tuples_on B(), B()}:
 for s being State of 1GateCircuit(<*x1()*>,f())
 for a1 being Element of B() st a1 = s.x1()
  holds
   (Result s).Output(1GateCircStr(<*x1()*>,f())) = F(a1)
provided
 for g being Function of 1-tuples_on B(), B() holds
   g = f() iff for a1 being Element of B() holds g.<*a1*> = F(a1);

scheme OneGate2Result
 {x1,x2()-> set, B()-> non empty finite set, F(set,set)->Element of B(),
  f() -> Function of 2-tuples_on B(), B()}:
 for s being State of 1GateCircuit(<*x1(),x2()*>,f())
 for a1, a2 being Element of B() st a1 = s.x1() & a2 = s.x2()
  holds
   (Result s).Output(1GateCircStr(<*x1(),x2()*>,f())) = F(a1,a2)
provided
 for g being Function of 2-tuples_on B(), B() holds
   g = f() iff for a1,a2 being Element of B() holds g.<*a1,a2*> = F(a1,a2);

scheme OneGate3Result
 {x1,x2,x3()-> set, B()-> non empty finite set,
  F(set,set,set)->Element of B(),
  f() -> Function of 3-tuples_on B(), B()}:
 for s being State of 1GateCircuit(<*x1(),x2(),x3()*>,f())
 for a1, a2, a3 being Element of B() st a1 = s.x1() & a2 = s.x2() & a3 = s.x3()
  holds
   (Result s).Output(1GateCircStr(<*x1(),x2(),x3()*>,f())) = F(a1,a2,a3)
provided
 for g being Function of 3-tuples_on B(), B() holds g = f() iff
   for a1,a2,a3 being Element of B() holds g.<*a1,a2,a3*> = F(a1,a2,a3);

scheme OneGate4Result
 {x1,x2,x3,x4()-> set, B()-> non empty finite set,
  F(set,set,set,set)->Element of B(),
  f() -> Function of 4-tuples_on B(), B()}:
 for s being State of 1GateCircuit(<*x1(),x2(),x3(),x4()*>,f())
 for a1, a2, a3, a4 being Element of B()
  st a1 = s.x1() & a2 = s.x2() & a3 = s.x3() & a4 = s.x4()
  holds
  (Result s).Output(1GateCircStr(<*x1(),x2(),x3(),x4()*>,f())) = F(a1,a2,a3,a4)
provided
 for g being Function of 4-tuples_on B(), B() holds g = f() iff
   for a1,a2,a3,a4 being Element of B()
    holds g.<*a1,a2,a3,a4*> = F(a1,a2,a3,a4);

scheme OneGate5Result
 {x1,x2,x3,x4,x5()-> set, B()-> non empty finite set,
  F(set,set,set,set,set)->Element of B(),
  f() -> Function of 5-tuples_on B(), B()}:
 for s being State of 1GateCircuit(<*x1(),x2(),x3(),x4(),x5()*>,f())
 for a1, a2, a3, a4, a5 being Element of B()
  st a1 = s.x1() & a2 = s.x2() & a3 = s.x3() & a4 = s.x4() & a5 = s.x5()
  holds
   (Result s).Output(1GateCircStr(<*x1(),x2(),x3(),x4(),x5()*>,f()))
     = F(a1,a2,a3,a4,a5)
provided
 for g being Function of 5-tuples_on B(), B() holds g = f() iff
   for a1,a2,a3,a4,a5 being Element of B()
    holds g.<*a1,a2,a3,a4,a5*> = F(a1,a2,a3,a4,a5);

begin :: Input of a compound circuit

theorem :: CIRCCMB3:39
 for n being Nat, X being non empty finite set
 for f being Function of n-tuples_on X, X
 for p being FinSeqLen of n
 for S being Signature of X
  st rng p c= the carrier of S &
     not Output 1GateCircStr(p,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(p,f)) = InputVertices S;

theorem :: CIRCCMB3:40
 for X1,X2 being set, X being non empty finite set, n be Nat
 for f being Function of n-tuples_on X, X
 for p being FinSeqLen of n
 for S being Signature of X
  st rng p = X1 \/ X2 & X1 c= the carrier of S & X2 misses InnerVertices S &
     not Output 1GateCircStr(p,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(p,f)) = (InputVertices S) \/ X2;

theorem :: CIRCCMB3:41
 for x1 being set, X being non empty finite set
 for f being Function of 1-tuples_on X, X
 for S being Signature of X
  st x1 in the carrier of S &
     not Output 1GateCircStr(<*x1*>,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(<*x1*>,f)) = InputVertices S;

theorem :: CIRCCMB3:42
 for x1,x2 being set, X being non empty finite set
 for f being Function of 2-tuples_on X, X
 for S being Signature of X
  st x1 in the carrier of S & not x2 in InnerVertices S &
     not Output 1GateCircStr(<*x1,x2*>,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(<*x1,x2*>,f)) = (InputVertices S) \/ {x2};

theorem :: CIRCCMB3:43
 for x1,x2 being set, X being non empty finite set
 for f being Function of 2-tuples_on X, X
 for S being Signature of X
  st x2 in the carrier of S & not x1 in InnerVertices S &
     not Output 1GateCircStr(<*x1,x2*>,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(<*x1,x2*>,f)) = (InputVertices S) \/ {x1};

theorem :: CIRCCMB3:44
 for x1,x2 being set, X being non empty finite set
 for f being Function of 2-tuples_on X, X
 for S being Signature of X
  st x1 in the carrier of S & x2 in the carrier of S &
     not Output 1GateCircStr(<*x1,x2*>,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(<*x1,x2*>,f)) = InputVertices S;

theorem :: CIRCCMB3:45
 for x1,x2,x3 being set, X being non empty finite set
 for f being Function of 3-tuples_on X, X
 for S being Signature of X
  st x1 in the carrier of S & not x2 in InnerVertices S &
     not x3 in InnerVertices S &
     not Output 1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>,f)) =
     (InputVertices S) \/ {x2,x3};

theorem :: CIRCCMB3:46
 for x1,x2,x3 being set, X being non empty finite set
 for f being Function of 3-tuples_on X, X
 for S being Signature of X
  st x2 in the carrier of S & not x1 in InnerVertices S &
     not x3 in InnerVertices S &
     not Output 1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>,f)) =
     (InputVertices S) \/ {x1,x3};

theorem :: CIRCCMB3:47
 for x1,x2,x3 being set, X being non empty finite set
 for f being Function of 3-tuples_on X, X
 for S being Signature of X
  st x3 in the carrier of S & not x1 in InnerVertices S &
     not x2 in InnerVertices S &
     not Output 1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>,f)) =
     (InputVertices S) \/ {x1,x2};

theorem :: CIRCCMB3:48
 for x1,x2,x3 being set, X being non empty finite set
 for f being Function of 3-tuples_on X, X
 for S being Signature of X
  st x1 in the carrier of S & x2 in the carrier of S &
     not x3 in InnerVertices S &
     not Output 1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>,f)) =
     (InputVertices S) \/ {x3};

theorem :: CIRCCMB3:49
 for x1,x2,x3 being set, X being non empty finite set
 for f being Function of 3-tuples_on X, X
 for S being Signature of X
  st x1 in the carrier of S & x3 in the carrier of S &
     not x2 in InnerVertices S &
     not Output 1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>,f)) =
     (InputVertices S) \/ {x2};

theorem :: CIRCCMB3:50
 for x1,x2,x3 being set, X being non empty finite set
 for f being Function of 3-tuples_on X, X
 for S being Signature of X
  st x2 in the carrier of S & x3 in the carrier of S &
     not x1 in InnerVertices S &
     not Output 1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>,f)) =
     (InputVertices S) \/ {x1};

theorem :: CIRCCMB3:51
 for x1,x2,x3 being set, X being non empty finite set
 for f being Function of 3-tuples_on X, X
 for S being Signature of X
  st x1 in the carrier of S & x2 in the carrier of S &
     x3 in the carrier of S &
     not Output 1GateCircStr(<*x1,x2,x3*>,f) in InputVertices S
  holds
   InputVertices (S +* 1GateCircStr(<*x1,x2,x3*>,f)) = InputVertices S;

begin :: Result of a compound circuit

theorem :: CIRCCMB3:52
 for X being non empty finite set
 for S being finite Signature of X
 for A being Circuit of X,S
 for n being Nat, f being Function of n-tuples_on X, X
 for p being FinSeqLen of n
  st not Output 1GateCircStr(p,f) in InputVertices S
 for s being State of A +* 1GateCircuit(p,f)
 for s' being State of A st s' = s|the carrier of S
  holds stabilization-time s <= 1+stabilization-time s';

scheme Comb1CircResult
 {x1()-> set, B()-> non empty finite set, F(set)->Element of B(),
  S() -> finite Signature of B(),
  C() -> Circuit of B(), S(),
  f() -> Function of 1-tuples_on B(), B()}:
 for s being State of C() +* 1GateCircuit(<*x1()*>,f())
 for s' being State of C() st s' = s|the carrier of S()
 for a1 being Element of B()
  st (x1() in InnerVertices S() implies a1 = (Result s').x1()) &
     (not x1() in InnerVertices S() implies a1 = s.x1())
  holds
   (Result s).Output 1GateCircStr(<*x1()*>,f()) = F(a1)
provided
 for g being Function of 1-tuples_on B(), B() holds
  g = f() iff for a1 being Element of B() holds g.<*a1*> = F(a1)
and
 not Output 1GateCircStr(<*x1()*>,f()) in InputVertices S();

scheme Comb2CircResult
 {x1,x2()-> set, B()-> non empty finite set,
  F(set,set)->Element of B(),
  S() -> finite Signature of B(),
  C() -> Circuit of B(), S(),
  f() -> Function of 2-tuples_on B(), B()}:
 for s being State of C() +* 1GateCircuit(<*x1(),x2()*>,f())
 for s' being State of C() st s' = s|the carrier of S()
 for a1, a2 being Element of B()
  st (x1() in InnerVertices S() implies a1 = (Result s').x1()) &
     (not x1() in InnerVertices S() implies a1 = s.x1()) &
     (x2() in InnerVertices S() implies a2 = (Result s').x2()) &
     (not x2() in InnerVertices S() implies a2 = s.x2())
  holds
   (Result s).Output(1GateCircStr(<*x1(),x2()*>,f())) = F(a1,a2)
provided
 for g being Function of 2-tuples_on B(), B() holds g = f() iff
   for a1,a2 being Element of B() holds g.<*a1,a2*> = F(a1,a2)
and
 not Output 1GateCircStr(<*x1(),x2()*>,f()) in InputVertices S();

scheme Comb3CircResult
 {x1,x2,x3()-> set, B()-> non empty finite set,
  F(set,set,set)->Element of B(),
  S() -> finite Signature of B(),
  C() -> Circuit of B(), S(),
  f() -> Function of 3-tuples_on B(), B()}:
 for s being State of C() +* 1GateCircuit(<*x1(),x2(),x3()*>,f())
 for s' being State of C() st s' = s|the carrier of S()
 for a1, a2, a3 being Element of B()
  st (x1() in InnerVertices S() implies a1 = (Result s').x1()) &
     (not x1() in InnerVertices S() implies a1 = s.x1()) &
     (x2() in InnerVertices S() implies a2 = (Result s').x2()) &
     (not x2() in InnerVertices S() implies a2 = s.x2()) &
     (x3() in InnerVertices S() implies a3 = (Result s').x3()) &
     (not x3() in InnerVertices S() implies a3 = s.x3())
  holds
   (Result s).Output(1GateCircStr(<*x1(),x2(),x3()*>,f())) = F(a1,a2,a3)
provided
 for g being Function of 3-tuples_on B(), B() holds g = f() iff
   for a1,a2,a3 being Element of B() holds g.<*a1,a2,a3*> = F(a1,a2,a3)
and
 not Output 1GateCircStr(<*x1(),x2(),x3()*>,f()) in InputVertices S();

scheme Comb4CircResult
 {x1,x2,x3,x4()-> set, B()-> non empty finite set,
  F(set,set,set,set)->Element of B(),
  S() -> finite Signature of B(),
  C() -> Circuit of B(), S(),
  f() -> Function of 4-tuples_on B(), B()}:
 for s being State of C() +* 1GateCircuit(<*x1(),x2(),x3(),x4()*>,f())
 for s' being State of C() st s' = s|the carrier of S()
 for a1, a2, a3, a4 being Element of B()
  st (x1() in InnerVertices S() implies a1 = (Result s').x1()) &
     (not x1() in InnerVertices S() implies a1 = s.x1()) &
     (x2() in InnerVertices S() implies a2 = (Result s').x2()) &
     (not x2() in InnerVertices S() implies a2 = s.x2()) &
     (x3() in InnerVertices S() implies a3 = (Result s').x3()) &
     (not x3() in InnerVertices S() implies a3 = s.x3()) &
     (x4() in InnerVertices S() implies a4 = (Result s').x4()) &
     (not x4() in InnerVertices S() implies a4 = s.x4())
  holds
   (Result s).Output(1GateCircStr(<*x1(),x2(),x3(),x4()*>,f()))
     = F(a1,a2,a3,a4)
provided
 for g being Function of 4-tuples_on B(), B() holds g = f() iff
   for a1,a2,a3,a4 being Element of B()
    holds g.<*a1,a2,a3,a4*> = F(a1,a2,a3,a4)
and
 not Output 1GateCircStr(<*x1(),x2(),x3(),x4()*>,f()) in InputVertices S();

scheme Comb5CircResult
 {x1,x2,x3,x4,x5()-> set, B()-> non empty finite set,
  F(set,set,set,set,set)->Element of B(),
  S() -> finite Signature of B(),
  C() -> Circuit of B(), S(),
  f() -> Function of 5-tuples_on B(), B()}:
 for s being State of C() +* 1GateCircuit(<*x1(),x2(),x3(),x4(),x5()*>,f())
 for s' being State of C() st s' = s|the carrier of S()
 for a1, a2, a3, a4, a5 being Element of B()
  st (x1() in InnerVertices S() implies a1 = (Result s').x1()) &
     (not x1() in InnerVertices S() implies a1 = s.x1()) &
     (x2() in InnerVertices S() implies a2 = (Result s').x2()) &
     (not x2() in InnerVertices S() implies a2 = s.x2()) &
     (x3() in InnerVertices S() implies a3 = (Result s').x3()) &
     (not x3() in InnerVertices S() implies a3 = s.x3()) &
     (x4() in InnerVertices S() implies a4 = (Result s').x4()) &
     (not x4() in InnerVertices S() implies a4 = s.x4()) &
     (x5() in InnerVertices S() implies a5 = (Result s').x5()) &
     (not x5() in InnerVertices S() implies a5 = s.x5())
  holds
   (Result s).Output(1GateCircStr(<*x1(),x2(),x3(),x4(),x5()*>,f()))
     = F(a1,a2,a3,a4,a5)
provided
 for g being Function of 5-tuples_on B(), B() holds g = f() iff
   for a1,a2,a3,a4,a5 being Element of B()
    holds g.<*a1,a2,a3,a4,a5*> = F(a1,a2,a3,a4,a5)
and
 not Output 1GateCircStr(<*x1(),x2(),x3(),x4(),x5()*>,f())
      in InputVertices S();

begin :: Inputs without pairs

definition
 let S be non empty ManySortedSign;
 attr S is with_nonpair_inputs means
:: CIRCCMB3:def 11

  InputVertices S is without_pairs;
end;

definition
 cluster NAT -> without_pairs;
 let X be without_pairs set;
 cluster -> without_pairs Subset of X;
end;

definition
 cluster natural-yielding -> nonpair-yielding Function;
end;

definition
 cluster -> natural-yielding FinSequence of NAT;
end;

definition
 cluster one-to-one natural-yielding FinSequence;
end;

definition
 let n be Nat;
 cluster one-to-one natural-yielding FinSeqLen of n;
end;

definition
 let p be nonpair-yielding FinSequence;
 let f be set;
 cluster 1GateCircStr(p,f) -> with_nonpair_inputs;
end;

definition
 cluster with_nonpair_inputs (one-gate ManySortedSign);
 let X be non empty finite set;
 cluster with_nonpair_inputs (one-gate Signature of X);
end;

definition
 let S be with_nonpair_inputs (non empty ManySortedSign);
 cluster InputVertices S -> without_pairs;
end;

theorem :: CIRCCMB3:53
   for S being with_nonpair_inputs (non empty ManySortedSign)
 for x being Vertex of S st x is pair
  holds x in InnerVertices S;

definition
 let S be unsplit gate`1=arity (non empty ManySortedSign);
 cluster InnerVertices S -> Relation-like;
end;

definition
 let S be unsplit gate`2=den (non empty non void ManySortedSign);
 cluster InnerVertices S -> Relation-like;
end;

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

theorem :: CIRCCMB3:54
   for x being non pair set, R being Relation holds not x in R;

theorem :: CIRCCMB3:55
 for x1 being set, X being non empty finite set
 for f being Function of 1-tuples_on X, X
 for S being with_nonpair_inputs Signature of X
  st x1 in the carrier of S or x1 is non pair
  holds S +* 1GateCircStr(<*x1*>, f) is with_nonpair_inputs;

definition
 let X be non empty finite set;
 let S be with_nonpair_inputs Signature of X;
 let x1 be Vertex of S;
 let f be Function of 1-tuples_on X, X;
 cluster S +* 1GateCircStr(<*x1*>, f) -> with_nonpair_inputs;
end;

definition
 let X be non empty finite set;
 let S be with_nonpair_inputs Signature of X;
 let x1 be non pair set;
 let f be Function of 1-tuples_on X, X;
 cluster S +* 1GateCircStr(<*x1*>, f) -> with_nonpair_inputs;
end;

theorem :: CIRCCMB3:56
 for x1,x2 being set, X being non empty finite set
 for f being Function of 2-tuples_on X, X
 for S being with_nonpair_inputs Signature of X
  st (x1 in the carrier of S or x1 is non pair) &
     (x2 in the carrier of S or x2 is non pair)
  holds S +* 1GateCircStr(<*x1,x2*>, f) is with_nonpair_inputs;

definition
 let X be non empty finite set;
 let S be with_nonpair_inputs Signature of X;
 let x1 be Vertex of S, n2 be non pair set;
 let f be Function of 2-tuples_on X, X;
 cluster S +* 1GateCircStr(<*x1,n2*>, f) -> with_nonpair_inputs;
 cluster S +* 1GateCircStr(<*n2,x1*>, f) -> with_nonpair_inputs;
end;

definition
 let X be non empty finite set;
 let S be with_nonpair_inputs Signature of X;
 let x1,x2 be Vertex of S;
 let f be Function of 2-tuples_on X, X;
 cluster S +* 1GateCircStr(<*x1,x2*>, f) -> with_nonpair_inputs;
end;

theorem :: CIRCCMB3:57
 for x1,x2,x3 being set, X being non empty finite set
 for f being Function of 3-tuples_on X, X
 for S being with_nonpair_inputs Signature of X
  st (x1 in the carrier of S or x1 is non pair) &
     (x2 in the carrier of S or x2 is non pair) &
     (x3 in the carrier of S or x3 is non pair)
  holds S +* 1GateCircStr(<*x1,x2,x3*>, f) is with_nonpair_inputs;

definition
 let X be non empty finite set;
 let S be with_nonpair_inputs Signature of X;
 let x1,x2 be Vertex of S, n be non pair set;
 let f be Function of 3-tuples_on X, X;
 cluster S +* 1GateCircStr(<*x1,x2,n*>, f) -> with_nonpair_inputs;
 cluster S +* 1GateCircStr(<*x1,n,x2*>, f) -> with_nonpair_inputs;
 cluster S +* 1GateCircStr(<*n,x1,x2*>, f) -> with_nonpair_inputs;
end;

definition
 let X be non empty finite set;
 let S be with_nonpair_inputs Signature of X;
 let x be Vertex of S, n1,n2 be non pair set;
 let f be Function of 3-tuples_on X, X;
 cluster S +* 1GateCircStr(<*x,n1,n2*>, f) -> with_nonpair_inputs;
 cluster S +* 1GateCircStr(<*n1,x,n2*>, f) -> with_nonpair_inputs;
 cluster S +* 1GateCircStr(<*n1,n2,x*>, f) -> with_nonpair_inputs;
end;

definition
 let X be non empty finite set;
 let S be with_nonpair_inputs Signature of X;
 let x1,x2,x3 be Vertex of S;
 let f be Function of 3-tuples_on X, X;
 cluster S +* 1GateCircStr(<*x1,x2,x3*>, f) -> with_nonpair_inputs;
end;