:: Preliminaries to Automatic Generation of Mizar Documentation for Circuits
:: by Grzegorz Bancerek and Adam Naumowicz
::
:: Received July 26, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

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

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

:: deftheorem Def1 defines stabilizing CIRCCMB3:def_1_:_
 for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A holds
( s is stabilizing iff ex n being Element of NAT st Following (s,n) is stable );

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

:: deftheorem Def2 defines stabilizing CIRCCMB3:def_2_:_
 for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S holds
( A is stabilizing iff for s being State of A holds s is stabilizing );

:: deftheorem  defines with_stabilization-limit CIRCCMB3:def_3_:_
 for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S holds
( A is with_stabilization-limit iff ex n being Element of NAT st
for s being State of A holds Following (s,n) is stable );

registration
let S be non empty non void Circuit-like ManySortedSign ;
cluster non-empty finite-yielding with_stabilization-limit  ->  non-empty stabilizing for MSAlgebra over S;
coherence
 for b1 being non-empty Circuit of S st b1 is with_stabilization-limit holds
b1 is stabilizing
proofend;
end;

definition
let S be non empty non void Circuit-like ManySortedSign ;
let A be non-empty Circuit of S;
let s be State of A;
assume B1: s is stabilizing ;
func Result s ->  State of A means :Def4: :: CIRCCMB3:def 4
( it is stable & ex n being Element of NAT st it = Following (s,n) );
existence
 ex b1 being State of A st
( b1 is stable & ex n being Element of NAT st b1 = Following (s,n) )
proofend;
uniqueness
 for b1, b2 being State of A st b1 is stable & ex n being Element of NAT st b1 = Following (s,n) & b2 is stable & ex n being Element of NAT st b2 = Following (s,n) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines Result CIRCCMB3:def_4_:_
 for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A st s is stabilizing holds
for b4 being State of A holds
( b4 = Result s iff ( b4 is stable & ex n being Element of NAT st b4 = Following (s,n) ) );

definition
let S be non empty non void Circuit-like ManySortedSign ;
let A be non-empty Circuit of S;
let s be State of A;
assume A1: s is stabilizing ;
func stabilization-time s ->  Element of NAT  means :Def5: :: CIRCCMB3:def 5
( Following (s,it) is stable &amp; ( for n being Element of NAT st n < it holds
not Following (s,n) is stable ) );
existence
 ex b1 being Element of NAT st
( Following (s,b1) is stable &amp; ( for n being Element of NAT st n < b1 holds
not Following (s,n) is stable ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st Following (s,b1) is stable &amp; ( for n being Element of NAT st n < b1 holds
not Following (s,n) is stable ) &amp; Following (s,b2) is stable &amp; ( for n being Element of NAT st n < b2 holds
not Following (s,n) is stable ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines stabilization-time CIRCCMB3:def_5_:_
 for S being non empty non void Circuit-like ManySortedSign
for A being non-empty Circuit of S
for s being State of A st s is stabilizing holds
for b4 being Element of NAT holds
( b4 = stabilization-time s iff ( Following (s,b4) is stable &amp; ( for n being Element of NAT st n < b4 holds
not Following (s,n) is stable ) ) );

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

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

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

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

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

theorem Th7: :: CIRCCMB3:7
for S1, S2 being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 &amp; InputVertices S2 misses InnerVertices S1 holds
for S being non empty non void Circuit-like ManySortedSign st S = S1 +* S2 holds
for A1 being non-empty Circuit of S1
for A2 being non-empty Circuit of S2 st A1 tolerates A2 holds
for A being non-empty Circuit of S st A = A1 +* A2 holds
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 &amp; s2 = s | the carrier of S2 &amp; s1 is stabilizing &amp; s2 is stabilizing holds
s is stabilizing
proofend;

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

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

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

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

begin

theorem Th12: :: CIRCCMB3:12
for x being set
for X being non empty finite set
for n being Element of 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
proofend;

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

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

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

:: deftheorem Def6 defines one-gate CIRCCMB3:def_6_:_
 for S being ManySortedSign holds
( S is one-gate iff ex X being non empty finite set ex n being Element of NAT ex p being FinSeqLen of n ex f being Function of (n -tuples_on X),X st S = 1GateCircStr (p,f) );

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

:: deftheorem Def7 defines one-gate CIRCCMB3:def_7_:_
 for S being non empty ManySortedSign
for A being MSAlgebra over S holds
( A is one-gate iff ex X being non empty finite set ex n being Element of NAT ex p being FinSeqLen of n ex f being Function of (n -tuples_on X),X st
( S = 1GateCircStr (p,f) &amp; A = 1GateCircuit (p,f) ) );

registration
let p be FinSequence;
let x be set ;
cluster 1GateCircStr (p,x) ->  finite ;
coherence
 1GateCircStr (p,x) is finite
proofend;
end;

registration
cluster one-gate  ->  non empty finite non void strict unsplit gate`1=arity for ManySortedSign ;
coherence
 for b1 being ManySortedSign st b1 is one-gate holds
( b1 is strict &amp; not b1 is void &amp; not b1 is empty &amp; b1 is unsplit &amp; b1 is gate`1=arity &amp; b1 is finite )
proofend;
end;

registration
cluster non empty one-gate  ->  non empty gate`2=den for ManySortedSign ;
coherence
 for b1 being non empty ManySortedSign st b1 is one-gate holds
b1 is gate`2=den
proofend;
end;

registration
let X be non empty finite set ;
let n be Element of NAT ;
let p be FinSeqLen of n;
let f be Function of (n -tuples_on X),X;
cluster 1GateCircStr (p,f) ->  one-gate ;
coherence
 1GateCircStr (p,f) is one-gate by Def6;
end;

registration
cluster one-gate for ManySortedSign ;
existence
 ex b1 being ManySortedSign st b1 is one-gate
proofend;
end;

registration
let S be one-gate ManySortedSign ;
cluster finite-yielding one-gate  ->  strict non-empty for MSAlgebra over S;
coherence
 for b1 being Circuit of S st b1 is one-gate holds
( b1 is strict &amp; b1 is non-empty )
proofend;
end;

registration
let X be non empty finite set ;
let n be Element of NAT ;
let p be FinSeqLen of n;
let f be Function of (n -tuples_on X),X;
cluster 1GateCircuit (p,f) ->  one-gate ;
coherence
 1GateCircuit (p,f) is one-gate by Def7;
end;

registration
let S be one-gate ManySortedSign ;
cluster non-empty finite-yielding one-gate for MSAlgebra over S;
existence
 ex b1 being Circuit of S st
( b1 is one-gate &amp; b1 is non-empty )
proofend;
end;

definition
let S be one-gate ManySortedSign ;
func Output S ->  Vertex of S equals :: CIRCCMB3:def 8
 union the carrier' of S;
coherence
 union the carrier' of S is Vertex of S
proofend;
end;

:: deftheorem  defines Output CIRCCMB3:def_8_:_
 for S being one-gate ManySortedSign holds Output S = union the carrier' of S;

registration
let S be one-gate ManySortedSign ;
cluster Output S ->  pair ;
coherence
 Output S is pair
proofend;
end;

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

theorem Th16: :: CIRCCMB3:16
for S being one-gate ManySortedSign holds InnerVertices S = {(Output S)}
proofend;

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

theorem :: CIRCCMB3:18
for n being Element of NAT
for 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 State of (1GateCircuit (p,f)) holds (Following s) . (Output (1GateCircStr (p,f))) = f . (s * p)
proofend;

theorem Th19: :: CIRCCMB3:19
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
proofend;

registration
let S be non empty non void Circuit-like ManySortedSign ;
cluster non-empty finite-yielding one-gate  ->  non-empty with_stabilization-limit for MSAlgebra over S;
coherence
 for b1 being non-empty Circuit of S st b1 is one-gate holds
b1 is with_stabilization-limit
proofend;
end;

theorem Th20: :: CIRCCMB3:20
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
proofend;

theorem Th21: :: CIRCCMB3:21
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
proofend;

scheme :: CIRCCMB3:sch 1
OneGate1Ex{ F1() ->  set , F2() ->  non empty finite set , F3( set ) ->  Element of F2() } :
 ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st
( InputVertices S = {F1()} &amp; ( for s being State of A holds (Result s) . (Output S) = F3((s . F1())) ) )
proofend;

scheme :: CIRCCMB3:sch 2
OneGate2Ex{ F1() ->  set , F2() ->  set , F3() ->  non empty finite set , F4( set , set ) ->  Element of F3() } :
 ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st
( InputVertices S = {F1(),F2()} &amp; ( for s being State of A holds (Result s) . (Output S) = F4((s . F1()),(s . F2())) ) )
proofend;

scheme :: CIRCCMB3:sch 3
OneGate3Ex{ F1() ->  set , F2() ->  set , F3() ->  set , F4() ->  non empty finite set , F5( set , set , set ) ->  Element of F4() } :
 ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st
( InputVertices S = {F1(),F2(),F3()} &amp; ( for s being State of A holds (Result s) . (Output S) = F5((s . F1()),(s . F2()),(s . F3())) ) )
proofend;

scheme :: CIRCCMB3:sch 4
OneGate4Ex{ F1() ->  set , F2() ->  set , F3() ->  set , F4() ->  set , F5() ->  non empty finite set , F6( set , set , set , set ) ->  Element of F5() } :
 ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st
( InputVertices S = {F1(),F2(),F3(),F4()} &amp; ( for s being State of A holds (Result s) . (Output S) = F6((s . F1()),(s . F2()),(s . F3()),(s . F4())) ) )
proofend;

scheme :: CIRCCMB3:sch 5
OneGate5Ex{ F1() ->  set , F2() ->  set , F3() ->  set , F4() ->  set , F5() ->  set , F6() ->  non empty finite set , F7( set , set , set , set , set ) ->  Element of F6() } :
 ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st
( InputVertices S = {F1(),F2(),F3(),F4(),F5()} &amp; ( for s being State of A holds (Result s) . (Output S) = F7((s . F1()),(s . F2()),(s . F3()),(s . F4()),(s . F5())) ) )
proofend;

begin

theorem Th22: :: CIRCCMB3:22
for X, Y being non empty set
for n, m being Element of NAT st n <> 0 &amp; n -tuples_on X = m -tuples_on Y holds
( X = Y &amp; n = m )
proofend;

theorem :: CIRCCMB3:23
for S1, S2 being non empty ManySortedSign
for v being Vertex of S1 holds v is Vertex of (S1 +* S2)
proofend;

theorem :: CIRCCMB3:24
for S1, S2 being non empty ManySortedSign
for v being Vertex of S2 holds v is Vertex of (S1 +* S2)
proofend;

definition
let X be non empty finite set ;
mode Signature of X ->  non empty non void unsplit gate`1=arity gate`2=den ManySortedSign  means :Def9: :: CIRCCMB3:def 9
 ex A being Circuit of it st
( the Sorts of A is constant &amp; the_value_of the Sorts of A = X &amp; A is gate`2=den );
existence
 ex b1 being non empty non void unsplit gate`1=arity gate`2=den ManySortedSign ex A being Circuit of b1 st
( the Sorts of A is constant &amp; the_value_of the Sorts of A = X &amp; A is gate`2=den )
proofend;
end;

:: deftheorem Def9 defines Signature CIRCCMB3:def_9_:_
 for X being non empty finite set
for b2 being non empty non void unsplit gate`1=arity gate`2=den ManySortedSign holds
( b2 is Signature of X iff ex A being Circuit of b2 st
( the Sorts of A is constant &amp; the_value_of the Sorts of A = X &amp; A is gate`2=den ) );

theorem Th25: :: CIRCCMB3:25
for n being Element of NAT
for 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
proofend;

registration
let X be non empty finite set ;
cluster non empty non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den one-gate for Signature of X;
existence
 ex b1 being Signature of X st
( b1 is strict &amp; b1 is one-gate )
proofend;
end;

definition
let n be Element of NAT ;
let X be non empty finite set ;
let f be Function of (n -tuples_on X),X;
let p be FinSeqLen of n;
:: original:1GateCircStr
redefine func 1GateCircStr (p,f) ->  strict Signature of X;
coherence
 1GateCircStr (p,f) is strict Signature of X by Th25;
end;

definition
let X be non empty finite set ;
let S be Signature of X;
mode Circuit of X,S ->  Circuit of S means :Def10: :: CIRCCMB3:def 10
( it is gate`2=den &amp; the Sorts of it is constant &amp; the_value_of the Sorts of it = X );
existence
 ex b1 being Circuit of S st
( b1 is gate`2=den &amp; the Sorts of b1 is constant &amp; the_value_of the Sorts of b1 = X )
proofend;
end;

:: deftheorem Def10 defines Circuit CIRCCMB3:def_10_:_
 for X being non empty finite set
for S being Signature of X
for b3 being Circuit of S holds
( b3 is Circuit of X,S iff ( b3 is gate`2=den &amp; the Sorts of b3 is constant &amp; the_value_of the Sorts of b3 = X ) );

registration
let X be non empty finite set ;
let S be Signature of X;
cluster  ->  non-empty gate`2=den for Circuit of X,S;
coherence
 for b1 being Circuit of X,S holds
( b1 is gate`2=den &amp; b1 is non-empty )
proofend;
end;

theorem Th26: :: CIRCCMB3:26
for n being Element of NAT
for 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)
proofend;

registration
let X be non empty finite set ;
let S be one-gate Signature of X;
cluster strict non-empty finite-yielding gate`2=den one-gate for Circuit of X,S;
existence
 ex b1 being Circuit of X,S st
( b1 is strict &amp; b1 is one-gate )
proofend;
end;

registration
let X be non empty finite set ;
let S be Signature of X;
cluster strict non-empty finite-yielding gate`2=den for Circuit of X,S;
existence
 ex b1 being Circuit of X,S st b1 is strict
proofend;
end;

definition
let n be Element of NAT ;
let X be non empty finite set ;
let f be Function of (n -tuples_on X),X;
let p be FinSeqLen of n;
:: original:1GateCircuit
redefine func 1GateCircuit (p,f) ->  strict Circuit of X, 1GateCircStr (p,f);
coherence
 1GateCircuit (p,f) is strict Circuit of X, 1GateCircStr (p,f) by Th26;
end;

theorem Th27: :: CIRCCMB3:27
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
proofend;

theorem Th28: :: CIRCCMB3:28
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
proofend;

theorem Th29: :: CIRCCMB3:29
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
proofend;

theorem Th30: :: 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
( the Sorts of (A1 +* A2) is constant &amp; the_value_of the Sorts of (A1 +* A2) = X )
proofend;

registration
let S1, S2 be non empty finite ManySortedSign ;
clusterS1 +* S2 ->  finite ;
coherence
 S1 +* S2 is finite
proofend;
end;

registration
let X be non empty finite set ;
let S1, S2 be Signature of X;
clusterS1 +* S2 ->  gate`2=den ;
coherence
 S1 +* S2 is gate`2=den
proofend;
end;

definition
let X be non empty finite set ;
let S1, S2 be Signature of X;
:: original:+*
redefine funcS1 +* S2 ->  strict Signature of X;
coherence
 S1 +* S2 is strict Signature of X
proofend;
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;
:: original:+*
redefine funcA1 +* A2 ->  strict Circuit of X,S1 +* S2;
coherence
 A1 +* A2 is strict Circuit of X,S1 +* S2
proofend;
end;

theorem Th31: :: CIRCCMB3:31
for x, y being set holds
( the_rank_of x in the_rank_of [x,y] &amp; the_rank_of y in the_rank_of [x,y] )
proofend;

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

registration
let X be non empty finite set ;
let S be finite Signature of X;
cluster  ->  with_stabilization-limit for Circuit of X,S;
coherence
 for b1 being Circuit of X,S holds b1 is with_stabilization-limit by Th32;
end;

scheme :: CIRCCMB3:sch 6
1AryDef{ F1() ->  non empty set , F2( set ) ->  Element of F1() } :
 ( ex f being Function of (1 -tuples_on F1()),F1() st
for x being Element of F1() holds f . <*x*> = F2(x) &amp; ( for f1, f2 being Function of (1 -tuples_on F1()),F1() st ( for x being Element of F1() holds f1 . <*x*> = F2(x) ) &amp; ( for x being Element of F1() holds f2 . <*x*> = F2(x) ) holds
f1 = f2 ) )
proofend;

scheme :: CIRCCMB3:sch 7
2AryDef{ F1() ->  non empty set , F2( set , set ) ->  Element of F1() } :
 ( ex f being Function of (2 -tuples_on F1()),F1() st
for x, y being Element of F1() holds f . <*x,y*> = F2(x,y) &amp; ( for f1, f2 being Function of (2 -tuples_on F1()),F1() st ( for x, y being Element of F1() holds f1 . <*x,y*> = F2(x,y) ) &amp; ( for x, y being Element of F1() holds f2 . <*x,y*> = F2(x,y) ) holds
f1 = f2 ) )
proofend;

scheme :: CIRCCMB3:sch 8
3AryDef{ F1() ->  non empty set , F2( set , set , set ) ->  Element of F1() } :
 ( ex f being Function of (3 -tuples_on F1()),F1() st
for x, y, z being Element of F1() holds f . <*x,y,z*> = F2(x,y,z) &amp; ( for f1, f2 being Function of (3 -tuples_on F1()),F1() st ( for x, y, z being Element of F1() holds f1 . <*x,y,z*> = F2(x,y,z) ) &amp; ( for x, y, z being Element of F1() holds f2 . <*x,y,z*> = F2(x,y,z) ) holds
f1 = f2 ) )
proofend;

theorem Th33: :: CIRCCMB3:33
for f being Function
for x1, x2, x3, x4 being set st x1 in dom f &amp; x2 in dom f &amp; x3 in dom f &amp; x4 in dom f holds
f * <*x1,x2,x3,x4*> = <*(f . x1),(f . x2),(f . x3),(f . x4)*>
proofend;

theorem Th34: :: CIRCCMB3:34
for f being Function
for x1, x2, x3, x4, x5 being set st x1 in dom f &amp; x2 in dom f &amp; x3 in dom f &amp; x4 in dom f &amp; x5 in dom f holds
f * <*x1,x2,x3,x4,x5*> = <*(f . x1),(f . x2),(f . x3),(f . x4),(f . x5)*>
proofend;

scheme :: CIRCCMB3:sch 9
OneGate1Result{ F1() ->  set , F2() ->  non empty finite set , F3( set ) ->  Element of F2(), F4() ->  Function of (1 -tuples_on F2()),F2() } :
 for s being State of (1GateCircuit (<*F1()*>,F4()))
for a1 being Element of F2() st a1 = s . F1() holds
(Result s) . (Output (1GateCircStr (<*F1()*>,F4()))) = F3(a1)
provided
A1: for g being Function of (1 -tuples_on F2()),F2() holds
( g = F4() iff for a1 being Element of F2() holds g . <*a1*> = F3(a1) )
proofend;

scheme :: CIRCCMB3:sch 10
OneGate2Result{ F1() ->  set , F2() ->  set , F3() ->  non empty finite set , F4( set , set ) ->  Element of F3(), F5() ->  Function of (2 -tuples_on F3()),F3() } :
 for s being State of (1GateCircuit (<*F1(),F2()*>,F5()))
for a1, a2 being Element of F3() st a1 = s . F1() &amp; a2 = s . F2() holds
(Result s) . (Output (1GateCircStr (<*F1(),F2()*>,F5()))) = F4(a1,a2)
provided
A1: for g being Function of (2 -tuples_on F3()),F3() holds
( g = F5() iff for a1, a2 being Element of F3() holds g . <*a1,a2*> = F4(a1,a2) )
proofend;

scheme :: CIRCCMB3:sch 11
OneGate3Result{ F1() ->  set , F2() ->  set , F3() ->  set , F4() ->  non empty finite set , F5( set , set , set ) ->  Element of F4(), F6() ->  Function of (3 -tuples_on F4()),F4() } :
 for s being State of (1GateCircuit (<*F1(),F2(),F3()*>,F6()))
for a1, a2, a3 being Element of F4() st a1 = s . F1() &amp; a2 = s . F2() &amp; a3 = s . F3() holds
(Result s) . (Output (1GateCircStr (<*F1(),F2(),F3()*>,F6()))) = F5(a1,a2,a3)
provided
A1: for g being Function of (3 -tuples_on F4()),F4() holds
( g = F6() iff for a1, a2, a3 being Element of F4() holds g . <*a1,a2,a3*> = F5(a1,a2,a3) )
proofend;

scheme :: CIRCCMB3:sch 12
OneGate4Result{ F1() ->  set , F2() ->  set , F3() ->  set , F4() ->  set , F5() ->  non empty finite set , F6( set , set , set , set ) ->  Element of F5(), F7() ->  Function of (4 -tuples_on F5()),F5() } :
 for s being State of (1GateCircuit (<*F1(),F2(),F3(),F4()*>,F7()))
for a1, a2, a3, a4 being Element of F5() st a1 = s . F1() &amp; a2 = s . F2() &amp; a3 = s . F3() &amp; a4 = s . F4() holds
(Result s) . (Output (1GateCircStr (<*F1(),F2(),F3(),F4()*>,F7()))) = F6(a1,a2,a3,a4)
provided
A1: for g being Function of (4 -tuples_on F5()),F5() holds
( g = F7() iff for a1, a2, a3, a4 being Element of F5() holds g . <*a1,a2,a3,a4*> = F6(a1,a2,a3,a4) )
proofend;

scheme :: CIRCCMB3:sch 13
OneGate5Result{ F1() ->  set , F2() ->  set , F3() ->  set , F4() ->  set , F5() ->  set , F6() ->  non empty finite set , F7( set , set , set , set , set ) ->  Element of F6(), F8() ->  Function of (5 -tuples_on F6()),F6() } :
 for s being State of (1GateCircuit (<*F1(),F2(),F3(),F4(),F5()*>,F8()))
for a1, a2, a3, a4, a5 being Element of F6() st a1 = s . F1() &amp; a2 = s . F2() &amp; a3 = s . F3() &amp; a4 = s . F4() &amp; a5 = s . F5() holds
(Result s) . (Output (1GateCircStr (<*F1(),F2(),F3(),F4(),F5()*>,F8()))) = F7(a1,a2,a3,a4,a5)
provided
A1: for g being Function of (5 -tuples_on F6()),F6() holds
( g = F8() iff for a1, a2, a3, a4, a5 being Element of F6() holds g . <*a1,a2,a3,a4,a5*> = F7(a1,a2,a3,a4,a5) )
proofend;

begin

theorem Th35: :: CIRCCMB3:35
for n being Element of NAT
for 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 &amp; not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = InputVertices S
proofend;

theorem Th36: :: CIRCCMB3:36
for X1, X2 being set
for X being non empty finite set
for n being Element of 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 &amp; X1 c= the carrier of S &amp; X2 misses InnerVertices S &amp; not Output (1GateCircStr (p,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (p,f))) = (InputVertices S) \/ X2
proofend;

theorem Th37: :: CIRCCMB3:37
for x1 being set
for 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 &amp; not Output (1GateCircStr (<*x1*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1*>,f))) = InputVertices S
proofend;

theorem Th38: :: CIRCCMB3:38
for x1, x2 being set
for 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 &amp; not x2 in InnerVertices S &amp; not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x2}
proofend;

theorem Th39: :: CIRCCMB3:39
for x1, x2 being set
for 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 &amp; not x1 in InnerVertices S &amp; not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x1}
proofend;

theorem Th40: :: CIRCCMB3:40
for x1, x2 being set
for 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 &amp; x2 in the carrier of S &amp; not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = InputVertices S
proofend;

theorem Th41: :: CIRCCMB3:41
for x1, x2, x3 being set
for 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 &amp; not x2 in InnerVertices S &amp; not x3 in InnerVertices S &amp; not Output (1GateCircStr (<*x1,x2,x3*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = (InputVertices S) \/ {x2,x3}
proofend;

theorem Th42: :: CIRCCMB3:42
for x1, x2, x3 being set
for 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 &amp; not x1 in InnerVertices S &amp; not x3 in InnerVertices S &amp; not Output (1GateCircStr (<*x1,x2,x3*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = (InputVertices S) \/ {x1,x3}
proofend;

theorem Th43: :: CIRCCMB3:43
for x1, x2, x3 being set
for 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 &amp; not x1 in InnerVertices S &amp; not x2 in InnerVertices S &amp; not Output (1GateCircStr (<*x1,x2,x3*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = (InputVertices S) \/ {x1,x2}
proofend;

theorem Th44: :: CIRCCMB3:44
for x1, x2, x3 being set
for 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 &amp; x2 in the carrier of S &amp; not x3 in InnerVertices S &amp; not Output (1GateCircStr (<*x1,x2,x3*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = (InputVertices S) \/ {x3}
proofend;

theorem Th45: :: CIRCCMB3:45
for x1, x2, x3 being set
for 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 &amp; x3 in the carrier of S &amp; not x2 in InnerVertices S &amp; not Output (1GateCircStr (<*x1,x2,x3*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = (InputVertices S) \/ {x2}
proofend;

theorem Th46: :: CIRCCMB3:46
for x1, x2, x3 being set
for 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 &amp; x3 in the carrier of S &amp; not x1 in InnerVertices S &amp; not Output (1GateCircStr (<*x1,x2,x3*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = (InputVertices S) \/ {x1}
proofend;

theorem Th47: :: CIRCCMB3:47
for x1, x2, x3 being set
for 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 &amp; x2 in the carrier of S &amp; x3 in the carrier of S &amp; not Output (1GateCircStr (<*x1,x2,x3*>,f)) in InputVertices S holds
InputVertices (S +* (1GateCircStr (<*x1,x2,x3*>,f))) = InputVertices S
proofend;

begin

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

scheme :: CIRCCMB3:sch 14
Comb1CircResult{ F1() ->  set , F2() ->  non empty finite set , F3( set ) ->  Element of F2(), F4() ->  finite Signature of F2(), F5() ->  Circuit of F2(),F4(), F6() ->  Function of (1 -tuples_on F2()),F2() } :
 for s being State of (F5() +* (1GateCircuit (<*F1()*>,F6())))
for s9 being State of F5() st s9 = s | the carrier of F4() holds
for a1 being Element of F2() st ( F1() in InnerVertices F4() implies a1 = (Result s9) . F1() ) &amp; ( not F1() in InnerVertices F4() implies a1 = s . F1() ) holds
(Result s) . (Output (1GateCircStr (<*F1()*>,F6()))) = F3(a1)
provided
A1: for g being Function of (1 -tuples_on F2()),F2() holds
( g = F6() iff for a1 being Element of F2() holds g . <*a1*> = F3(a1) ) and
A2: not Output (1GateCircStr (<*F1()*>,F6())) in InputVertices F4()
proofend;

scheme :: CIRCCMB3:sch 15
Comb2CircResult{ F1() ->  set , F2() ->  set , F3() ->  non empty finite set , F4( set , set ) ->  Element of F3(), F5() ->  finite Signature of F3(), F6() ->  Circuit of F3(),F5(), F7() ->  Function of (2 -tuples_on F3()),F3() } :
 for s being State of (F6() +* (1GateCircuit (<*F1(),F2()*>,F7())))
for s9 being State of F6() st s9 = s | the carrier of F5() holds
for a1, a2 being Element of F3() st ( F1() in InnerVertices F5() implies a1 = (Result s9) . F1() ) &amp; ( not F1() in InnerVertices F5() implies a1 = s . F1() ) &amp; ( F2() in InnerVertices F5() implies a2 = (Result s9) . F2() ) &amp; ( not F2() in InnerVertices F5() implies a2 = s . F2() ) holds
(Result s) . (Output (1GateCircStr (<*F1(),F2()*>,F7()))) = F4(a1,a2)
provided
A1: for g being Function of (2 -tuples_on F3()),F3() holds
( g = F7() iff for a1, a2 being Element of F3() holds g . <*a1,a2*> = F4(a1,a2) ) and
A2: not Output (1GateCircStr (<*F1(),F2()*>,F7())) in InputVertices F5()
proofend;

scheme :: CIRCCMB3:sch 16
Comb3CircResult{ F1() ->  set , F2() ->  set , F3() ->  set , F4() ->  non empty finite set , F5( set , set , set ) ->  Element of F4(), F6() ->  finite Signature of F4(), F7() ->  Circuit of F4(),F6(), F8() ->  Function of (3 -tuples_on F4()),F4() } :
 for s being State of (F7() +* (1GateCircuit (<*F1(),F2(),F3()*>,F8())))
for s9 being State of F7() st s9 = s | the carrier of F6() holds
for a1, a2, a3 being Element of F4() st ( F1() in InnerVertices F6() implies a1 = (Result s9) . F1() ) &amp; ( not F1() in InnerVertices F6() implies a1 = s . F1() ) &amp; ( F2() in InnerVertices F6() implies a2 = (Result s9) . F2() ) &amp; ( not F2() in InnerVertices F6() implies a2 = s . F2() ) &amp; ( F3() in InnerVertices F6() implies a3 = (Result s9) . F3() ) &amp; ( not F3() in InnerVertices F6() implies a3 = s . F3() ) holds
(Result s) . (Output (1GateCircStr (<*F1(),F2(),F3()*>,F8()))) = F5(a1,a2,a3)
provided
A1: for g being Function of (3 -tuples_on F4()),F4() holds
( g = F8() iff for a1, a2, a3 being Element of F4() holds g . <*a1,a2,a3*> = F5(a1,a2,a3) ) and
A2: not Output (1GateCircStr (<*F1(),F2(),F3()*>,F8())) in InputVertices F6()
proofend;

scheme :: CIRCCMB3:sch 17
Comb4CircResult{ F1() ->  set , F2() ->  set , F3() ->  set , F4() ->  set , F5() ->  non empty finite set , F6( set , set , set , set ) ->  Element of F5(), F7() ->  finite Signature of F5(), F8() ->  Circuit of F5(),F7(), F9() ->  Function of (4 -tuples_on F5()),F5() } :
 for s being State of (F8() +* (1GateCircuit (<*F1(),F2(),F3(),F4()*>,F9())))
for s9 being State of F8() st s9 = s | the carrier of F7() holds
for a1, a2, a3, a4 being Element of F5() st ( F1() in InnerVertices F7() implies a1 = (Result s9) . F1() ) &amp; ( not F1() in InnerVertices F7() implies a1 = s . F1() ) &amp; ( F2() in InnerVertices F7() implies a2 = (Result s9) . F2() ) &amp; ( not F2() in InnerVertices F7() implies a2 = s . F2() ) &amp; ( F3() in InnerVertices F7() implies a3 = (Result s9) . F3() ) &amp; ( not F3() in InnerVertices F7() implies a3 = s . F3() ) &amp; ( F4() in InnerVertices F7() implies a4 = (Result s9) . F4() ) &amp; ( not F4() in InnerVertices F7() implies a4 = s . F4() ) holds
(Result s) . (Output (1GateCircStr (<*F1(),F2(),F3(),F4()*>,F9()))) = F6(a1,a2,a3,a4)
provided
A1: for g being Function of (4 -tuples_on F5()),F5() holds
( g = F9() iff for a1, a2, a3, a4 being Element of F5() holds g . <*a1,a2,a3,a4*> = F6(a1,a2,a3,a4) ) and
A2: not Output (1GateCircStr (<*F1(),F2(),F3(),F4()*>,F9())) in InputVertices F7()
proofend;

scheme :: CIRCCMB3:sch 18
Comb5CircResult{ F1() ->  set , F2() ->  set , F3() ->  set , F4() ->  set , F5() ->  set , F6() ->  non empty finite set , F7( set , set , set , set , set ) ->  Element of F6(), F8() ->  finite Signature of F6(), F9() ->  Circuit of F6(),F8(), F10() ->  Function of (5 -tuples_on F6()),F6() } :
 for s being State of (F9() +* (1GateCircuit (<*F1(),F2(),F3(),F4(),F5()*>,F10())))
for s9 being State of F9() st s9 = s | the carrier of F8() holds
for a1, a2, a3, a4, a5 being Element of F6() st ( F1() in InnerVertices F8() implies a1 = (Result s9) . F1() ) &amp; ( not F1() in InnerVertices F8() implies a1 = s . F1() ) &amp; ( F2() in InnerVertices F8() implies a2 = (Result s9) . F2() ) &amp; ( not F2() in InnerVertices F8() implies a2 = s . F2() ) &amp; ( F3() in InnerVertices F8() implies a3 = (Result s9) . F3() ) &amp; ( not F3() in InnerVertices F8() implies a3 = s . F3() ) &amp; ( F4() in InnerVertices F8() implies a4 = (Result s9) . F4() ) &amp; ( not F4() in InnerVertices F8() implies a4 = s . F4() ) &amp; ( F5() in InnerVertices F8() implies a5 = (Result s9) . F5() ) &amp; ( not F5() in InnerVertices F8() implies a5 = s . F5() ) holds
(Result s) . (Output (1GateCircStr (<*F1(),F2(),F3(),F4(),F5()*>,F10()))) = F7(a1,a2,a3,a4,a5)
provided
A1: for g being Function of (5 -tuples_on F6()),F6() holds
( g = F10() iff for a1, a2, a3, a4, a5 being Element of F6() holds g . <*a1,a2,a3,a4,a5*> = F7(a1,a2,a3,a4,a5) ) and
A2: not Output (1GateCircStr (<*F1(),F2(),F3(),F4(),F5()*>,F10())) in InputVertices F8()
proofend;

begin

definition
let S be non empty ManySortedSign ;
attrS is with_nonpair_inputs  means :Def11: :: CIRCCMB3:def 11
 InputVertices S is without_pairs ;
end;

:: deftheorem Def11 defines with_nonpair_inputs CIRCCMB3:def_11_:_
 for S being non empty ManySortedSign holds
( S is with_nonpair_inputs iff InputVertices S is without_pairs );

registration
cluster NAT  ->  without_pairs ;
coherence
 not NAT is with_pair
proofend;
let X be without_pairs set ;
cluster  ->  without_pairs for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is without_pairs
proofend;
end;

registration
cluster Relation-like Function-like natural-valued  ->  nonpair-yielding for set ;
coherence
 for b1 being Function st b1 is natural-valued holds
b1 is nonpair-yielding
proofend;
end;

registration
cluster Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like V95() natural-valued for set ;
existence
 ex b1 being FinSequence st
( b1 is one-to-one &amp; b1 is natural-valued )
proofend;
end;

registration
let n be Element of NAT ;
cluster Relation-like NAT -defined Function-like one-to-one finite V42(n) FinSequence-like FinSubsequence-like V95() natural-valued for set ;
existence
 ex b1 being FinSeqLen of n st
( b1 is one-to-one &amp; b1 is natural-valued )
proofend;
end;

registration
let p be nonpair-yielding FinSequence;
let f be set ;
cluster 1GateCircStr (p,f) ->  with_nonpair_inputs ;
coherence
 1GateCircStr (p,f) is with_nonpair_inputs
proofend;
end;

registration
cluster non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den one-gate with_nonpair_inputs for ManySortedSign ;
existence
 ex b1 being one-gate ManySortedSign st b1 is with_nonpair_inputs
proofend;
let X be non empty finite set ;
cluster non empty finite non void V79() strict Circuit-like unsplit gate`1=arity gate`2=den one-gate with_nonpair_inputs for Signature of X;
existence
 ex b1 being one-gate Signature of X st b1 is with_nonpair_inputs
proofend;
end;

registration
let S be non empty with_nonpair_inputs ManySortedSign ;
cluster InputVertices S ->  without_pairs ;
coherence
 not InputVertices S is with_pair by Def11;
end;

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

registration
let S be non empty unsplit gate`1=arity ManySortedSign ;
cluster InnerVertices S ->  Relation-like ;
coherence
 InnerVertices S is Relation-like
proofend;
end;

registration
let S be non empty non void unsplit gate`2=den ManySortedSign ;
cluster InnerVertices S ->  Relation-like ;
coherence
 InnerVertices S is Relation-like
proofend;
end;

registration
let S1, S2 be non empty unsplit gate`1=arity with_nonpair_inputs ManySortedSign ;
clusterS1 +* S2 ->  with_nonpair_inputs ;
coherence
 S1 +* S2 is with_nonpair_inputs
proofend;
end;

theorem :: CIRCCMB3:50
for x being non pair set
for R being Relation holds not x in R
proofend;

theorem Th51: :: CIRCCMB3:51
for x1 being set
for 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 not x1 is pair ) holds
S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs
proofend;

registration
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;
clusterS +* (1GateCircStr (<*x1*>,f)) ->  with_nonpair_inputs ;
coherence
 S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs by Th51;
end;

registration
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;
clusterS +* (1GateCircStr (<*x1*>,f)) ->  with_nonpair_inputs ;
coherence
 S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs ;
end;

theorem Th52: :: CIRCCMB3:52
for x1, x2 being set
for 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 not x1 is pair ) &amp; ( x2 in the carrier of S or not x2 is pair ) holds
S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs
proofend;

registration
let X be non empty finite set ;
let S be with_nonpair_inputs Signature of X;
let x1 be Vertex of S;
let n2 be non pair set ;
let f be Function of (2 -tuples_on X),X;
clusterS +* (1GateCircStr (<*x1,n2*>,f)) ->  with_nonpair_inputs ;
coherence
 S +* (1GateCircStr (<*x1,n2*>,f)) is with_nonpair_inputs by Th52;
clusterS +* (1GateCircStr (<*n2,x1*>,f)) ->  with_nonpair_inputs ;
coherence
 S +* (1GateCircStr (<*n2,x1*>,f)) is with_nonpair_inputs by Th52;
end;

registration
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;
clusterS +* (1GateCircStr (<*x1,x2*>,f)) ->  with_nonpair_inputs ;
coherence
 S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs by Th52;
end;

theorem Th53: :: CIRCCMB3:53
for x1, x2, x3 being set
for 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 not x1 is pair ) &amp; ( x2 in the carrier of S or not x2 is pair ) &amp; ( x3 in the carrier of S or not x3 is pair ) holds
S +* (1GateCircStr (<*x1,x2,x3*>,f)) is with_nonpair_inputs
proofend;

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

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

registration
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;
clusterS +* (1GateCircStr (<*x1,x2,x3*>,f)) ->  with_nonpair_inputs ;
coherence
 S +* (1GateCircStr (<*x1,x2,x3*>,f)) is with_nonpair_inputs by Th53;
end;