:: by Grzegorz Bancerek and Adam Naumowicz

::

:: Received July 26, 2002

:: Copyright (c) 2002-2021 Association of Mizar Users

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 Nat holds (Following (s,n)) . x = s . x

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 Nat holds (Following (s,n)) . x = s . x

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

end;
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 Element of NAT st Following (s,n) is stable ;

ex n being Element of NAT st Following (s,n) is stable ;

:: deftheorem 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 );

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;

end;
let A be non-empty Circuit of S;

attr A is stabilizing means :Def2: :: CIRCCMB3:def 2

for s being State of A holds s is stabilizing ;

for s being State of A holds s is stabilizing ;

attr A 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 ;

ex n being Element of NAT st

for s being State of A holds Following (s,n) is stable ;

:: 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 );

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

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 ;

for b_{1} being non-empty Circuit of S st b_{1} is with_stabilization-limit holds

b_{1} is stabilizing

end;
cluster non-empty finite-yielding with_stabilization-limit -> non-empty stabilizing for MSAlgebra over S;

coherence for b

b

proof 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 A1: s is stabilizing ;

ex b_{1} being State of A st

( b_{1} is stable & ex n being Element of NAT st b_{1} = Following (s,n) )
by A1;

uniqueness

for b_{1}, b_{2} being State of A st b_{1} is stable & ex n being Element of NAT st b_{1} = Following (s,n) & b_{2} is stable & ex n being Element of NAT st b_{2} = Following (s,n) holds

b_{1} = b_{2}

end;
let A be non-empty Circuit of S;

let s be State of A;

assume A1: 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 ( it is stable & ex n being Element of NAT st it = Following (s,n) );

ex b

( b

uniqueness

for b

b

proof 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 b_{4} being State of A holds

( b_{4} = Result s iff ( b_{4} is stable & ex n being Element of NAT st b_{4} = Following (s,n) ) );

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 b

( b

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 ;

ex b_{1} being Element of NAT st

( Following (s,b_{1}) is stable & ( for n being Element of NAT st n < b_{1} holds

not Following (s,n) is stable ) )

for b_{1}, b_{2} being Element of NAT st Following (s,b_{1}) is stable & ( for n being Element of NAT st n < b_{1} holds

not Following (s,n) is stable ) & Following (s,b_{2}) is stable & ( for n being Element of NAT st n < b_{2} holds

not Following (s,n) is stable ) holds

b_{1} = b_{2}

end;
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 & ( for n being Element of NAT st n < it holds

not Following (s,n) is stable ) );

existence ( Following (s,it) is stable & ( for n being Element of NAT st n < it holds

not Following (s,n) is stable ) );

ex b

( Following (s,b

not Following (s,n) is stable ) )

proof end;

uniqueness for b

not Following (s,n) is stable ) & Following (s,b

not Following (s,n) is stable ) holds

b

proof 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 b_{4} being Element of NAT holds

( b_{4} = stabilization-time s iff ( Following (s,b_{4}) is stable & ( for n being Element of NAT st n < b_{4} holds

not Following (s,n) is stable ) ) );

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 b

( b

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))

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))

proof end;

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

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

proof end;

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)

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)

proof end;

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 & n >= stabilization-time s holds

Result s = Following (s,n)

for A being non-empty Circuit of S

for s being State of A

for n being Element of NAT st s is stabilizing & n >= stabilization-time s holds

Result s = Following (s,n)

proof end;

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

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

proof end;

theorem Th7: :: CIRCCMB3:7

for S1, S2 being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & 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 & s2 = s | the carrier of S2 & s1 is stabilizing & s2 is stabilizing holds

s is stabilizing

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 & s2 = s | the carrier of S2 & s1 is stabilizing & s2 is stabilizing holds

s is stabilizing

proof end;

theorem :: CIRCCMB3:8

for S1, S2 being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & 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 & s1 is stabilizing holds

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))

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 & s1 is stabilizing holds

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))

proof end;

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 & s1 is stabilizing holds

for s2 being State of A2 st s2 = (Following (s,(stabilization-time s1))) | the carrier of S2 & s2 is stabilizing holds

s is stabilizing

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 & s1 is stabilizing holds

for s2 being State of A2 st s2 = (Following (s,(stabilization-time s1))) | the carrier of S2 & s2 is stabilizing holds

s is stabilizing

proof end;

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 & s1 is stabilizing holds

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)

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 & s1 is stabilizing holds

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)

proof end;

theorem :: CIRCCMB3:11

for S1, S2, S being non empty non void Circuit-like ManySortedSign st InputVertices S1 misses InnerVertices S2 & 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 & A = A1 +* A2 holds

for s being State of A

for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stabilizing holds

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

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 & A = A1 +* A2 holds

for s being State of A

for s1 being State of A1 st s1 = s | the carrier of S1 & s1 is stabilizing holds

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

proof end;

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

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

proof end;

definition

let S be ManySortedSign ;

end;
attr S 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);

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

:: 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) );

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;

end;
let A be MSAlgebra over S;

attr A 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) & A = 1GateCircuit (p,f) );

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) & A = 1GateCircuit (p,f) );

:: 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) & A = 1GateCircuit (p,f) ) );

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) & A = 1GateCircuit (p,f) ) );

registration
end;

registration

coherence

for b_{1} being ManySortedSign st b_{1} is one-gate holds

( b_{1} is strict & not b_{1} is void & not b_{1} is empty & b_{1} is unsplit & b_{1} is gate`1=arity & b_{1} is finite )
;

end;
for b

( b

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

coherence

1GateCircStr (p,f) is one-gate ;

end;
let n be Element of NAT ;

let p be FinSeqLen of n;

let f be Function of (n -tuples_on X),X;

coherence

1GateCircStr (p,f) is one-gate ;

registration

let S be one-gate ManySortedSign ;

coherence

for b_{1} being Circuit of S st b_{1} is one-gate holds

( b_{1} is strict & b_{1} is non-empty )
;

end;
coherence

for b

( b

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;

coherence

1GateCircuit (p,f) is one-gate ;

end;
let n be Element of NAT ;

let p be FinSeqLen of n;

let f be Function of (n -tuples_on X),X;

coherence

1GateCircuit (p,f) is one-gate ;

registration

let S be one-gate ManySortedSign ;

existence

ex b_{1} being Circuit of S st

( b_{1} is one-gate & b_{1} is non-empty )

end;
existence

ex b

( b

proof end;

definition
end;

:: deftheorem defines Output CIRCCMB3:def 8 :

for S being one-gate ManySortedSign holds Output S = union the carrier' of S;

for S being one-gate ManySortedSign holds Output S = union the carrier' of S;

registration
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]

for p being FinSequence

for x being set st S = 1GateCircStr (p,x) holds

Output S = [p,x]

proof end;

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)

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)

proof end;

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)

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)

proof end;

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

for A being one-gate Circuit of S

for s being State of A holds Following s is stable

proof end;

registration

let S be non empty non void Circuit-like ManySortedSign ;

for b_{1} being non-empty Circuit of S st b_{1} is one-gate holds

b_{1} is with_stabilization-limit

end;
cluster non-empty finite-yielding one-gate -> non-empty with_stabilization-limit for MSAlgebra over S;

coherence for b

b

proof 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

for A being one-gate Circuit of S

for s being State of A holds Result s = Following s

proof end;

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

for A being one-gate Circuit of S

for s being State of A holds stabilization-time s <= 1

proof end;

scheme :: CIRCCMB3:sch 1

OneGate1Ex{ F_{1}() -> object , F_{2}() -> non empty finite set , F_{3}( object ) -> Element of F_{2}() } :

OneGate1Ex{ F

ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st

( InputVertices S = {F_{1}()} & ( for s being State of A holds (Result s) . (Output S) = F_{3}((s . F_{1}())) ) )

( InputVertices S = {F

proof end;

scheme :: CIRCCMB3:sch 2

OneGate2Ex{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> non empty finite set , F_{4}( object , object ) -> Element of F_{3}() } :

OneGate2Ex{ F

ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st

( InputVertices S = {F_{1}(),F_{2}()} & ( for s being State of A holds (Result s) . (Output S) = F_{4}((s . F_{1}()),(s . F_{2}())) ) )

( InputVertices S = {F

proof end;

scheme :: CIRCCMB3:sch 3

OneGate3Ex{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> object , F_{4}() -> non empty finite set , F_{5}( object , object , object ) -> Element of F_{4}() } :

OneGate3Ex{ F

ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st

( InputVertices S = {F_{1}(),F_{2}(),F_{3}()} & ( for s being State of A holds (Result s) . (Output S) = F_{5}((s . F_{1}()),(s . F_{2}()),(s . F_{3}())) ) )

( InputVertices S = {F

proof end;

scheme :: CIRCCMB3:sch 4

OneGate4Ex{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> object , F_{4}() -> object , F_{5}() -> non empty finite set , F_{6}( object , object , object , object ) -> Element of F_{5}() } :

OneGate4Ex{ F

ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st

( InputVertices S = {F_{1}(),F_{2}(),F_{3}(),F_{4}()} & ( for s being State of A holds (Result s) . (Output S) = F_{6}((s . F_{1}()),(s . F_{2}()),(s . F_{3}()),(s . F_{4}())) ) )

( InputVertices S = {F

proof end;

scheme :: CIRCCMB3:sch 5

OneGate5Ex{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> object , F_{4}() -> object , F_{5}() -> object , F_{6}() -> non empty finite set , F_{7}( object , object , object , object , object ) -> Element of F_{6}() } :

OneGate5Ex{ F

ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st

( InputVertices S = {F_{1}(),F_{2}(),F_{3}(),F_{4}(),F_{5}()} & ( for s being State of A holds (Result s) . (Output S) = F_{7}((s . F_{1}()),(s . F_{2}()),(s . F_{3}()),(s . F_{4}()),(s . F_{5}())) ) )

( InputVertices S = {F

proof end;

theorem Th22: :: CIRCCMB3:22

for X, Y being non empty set

for n, m being Element of NAT st n <> 0 & n -tuples_on X = m -tuples_on Y holds

( X = Y & n = m )

for n, m being Element of NAT st n <> 0 & n -tuples_on X = m -tuples_on Y holds

( X = Y & n = m )

proof end;

definition

let X be non empty finite set ;

ex b_{1} being non empty non void unsplit gate`1=arity gate`2=den ManySortedSign ex A being Circuit of b_{1} st

( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den )

end;
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 & the_value_of the Sorts of A = X & A is gate`2=den );

existence 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 );

ex b

( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den )

proof end;

:: deftheorem Def9 defines Signature CIRCCMB3:def 9 :

for X being non empty finite set

for b_{2} being non empty non void unsplit gate`1=arity gate`2=den ManySortedSign holds

( b_{2} is Signature of X iff ex A being Circuit of b_{2} st

( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den ) );

for X being non empty finite set

for b

( b

( the Sorts of A is constant & the_value_of the Sorts of A = X & 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

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

proof end;

registration

let X be non empty finite set ;

ex b_{1} being Signature of X st

( b_{1} is strict & b_{1} is one-gate )

end;
cluster non empty non void V82() strict Circuit-like unsplit gate`1=arity gate`2=den one-gate for Signature of X;

existence ex b

( b

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

definition

let X be non empty finite set ;

let S be Signature of X;

ex b_{1} being Circuit of S st

( b_{1} is gate`2=den & the Sorts of b_{1} is constant & the_value_of the Sorts of b_{1} = X )

end;
let S be Signature of X;

mode Circuit of X,S -> Circuit of S means :Def10: :: CIRCCMB3:def 10

( it is gate`2=den & the Sorts of it is constant & the_value_of the Sorts of it = X );

existence ( it is gate`2=den & the Sorts of it is constant & the_value_of the Sorts of it = X );

ex b

( b

proof end;

:: deftheorem Def10 defines Circuit CIRCCMB3:def 10 :

for X being non empty finite set

for S being Signature of X

for b_{3} being Circuit of S holds

( b_{3} is Circuit of X,S iff ( b_{3} is gate`2=den & the Sorts of b_{3} is constant & the_value_of the Sorts of b_{3} = X ) );

for X being non empty finite set

for S being Signature of X

for b

( b

registration

let X be non empty finite set ;

let S be Signature of X;

coherence

for b_{1} being Circuit of X,S holds

( b_{1} is gate`2=den & b_{1} is non-empty )

end;
let S be Signature of X;

coherence

for b

( b

proof 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)

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)

proof end;

registration

let X be non empty finite set ;

let S be one-gate Signature of X;

existence

ex b_{1} being Circuit of X,S st

( b_{1} is strict & b_{1} is one-gate )

end;
let S be one-gate Signature of X;

existence

ex b

( b

proof end;

registration

let X be non empty finite set ;

let S be Signature of X;

existence

ex b_{1} being Circuit of X,S st b_{1} is strict

end;
let S be Signature of X;

existence

ex b

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

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

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

proof end;

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

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

proof end;

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

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

proof end;

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 & the_value_of the Sorts of (A1 +* A2) = X )

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 )

proof end;

registration
end;

registration

let X be non empty finite set ;

let S1, S2 be Signature of X;

coherence

S1 +* S2 is gate`2=den

end;
let S1, S2 be Signature of X;

coherence

S1 +* S2 is gate`2=den

proof end;

definition

let X be non empty finite set ;

let S1, S2 be Signature of X;

:: original: +*

redefine func S1 +* S2 -> strict Signature of X;

coherence

S1 +* S2 is strict Signature of X

end;
let S1, S2 be Signature of X;

:: original: +*

redefine func S1 +* S2 -> strict Signature of X;

coherence

S1 +* S2 is strict Signature of X

proof 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 func A1 +* A2 -> strict Circuit of X,S1 +* S2;

coherence

A1 +* A2 is strict Circuit of X,S1 +* S2

end;
let S1, S2 be Signature of X;

let A1 be Circuit of X,S1;

let A2 be Circuit of X,S2;

:: original: +*

redefine func A1 +* A2 -> strict Circuit of X,S1 +* S2;

coherence

A1 +* A2 is strict Circuit of X,S1 +* S2

proof end;

theorem Th31: :: CIRCCMB3:31

for x, y being object holds

( the_rank_of x in the_rank_of [x,y] & the_rank_of y in the_rank_of [x,y] )

( the_rank_of x in the_rank_of [x,y] & the_rank_of y in the_rank_of [x,y] )

proof end;

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

for A being non-empty Circuit of S st A is gate`2=den holds

A is with_stabilization-limit

proof end;

registration

let X be non empty finite set ;

let S be finite Signature of X;

coherence

for b_{1} being Circuit of X,S holds b_{1} is with_stabilization-limit
by Th32;

end;
let S be finite Signature of X;

coherence

for b

scheme :: CIRCCMB3:sch 6

1AryDef{ F_{1}() -> non empty set , F_{2}( object ) -> Element of F_{1}() } :

1AryDef{ F

( ex f being Function of (1 -tuples_on F_{1}()),F_{1}() st

for x being Element of F_{1}() holds f . <*x*> = F_{2}(x) & ( for f1, f2 being Function of (1 -tuples_on F_{1}()),F_{1}() st ( for x being Element of F_{1}() holds f1 . <*x*> = F_{2}(x) ) & ( for x being Element of F_{1}() holds f2 . <*x*> = F_{2}(x) ) holds

f1 = f2 ) )

for x being Element of F

f1 = f2 ) )

proof end;

scheme :: CIRCCMB3:sch 7

2AryDef{ F_{1}() -> non empty set , F_{2}( object , object ) -> Element of F_{1}() } :

2AryDef{ F

( ex f being Function of (2 -tuples_on F_{1}()),F_{1}() st

for x, y being Element of F_{1}() holds f . <*x,y*> = F_{2}(x,y) & ( for f1, f2 being Function of (2 -tuples_on F_{1}()),F_{1}() st ( for x, y being Element of F_{1}() holds f1 . <*x,y*> = F_{2}(x,y) ) & ( for x, y being Element of F_{1}() holds f2 . <*x,y*> = F_{2}(x,y) ) holds

f1 = f2 ) )

for x, y being Element of F

f1 = f2 ) )

proof end;

scheme :: CIRCCMB3:sch 8

3AryDef{ F_{1}() -> non empty set , F_{2}( object , object , object ) -> Element of F_{1}() } :

3AryDef{ F

( ex f being Function of (3 -tuples_on F_{1}()),F_{1}() st

for x, y, z being Element of F_{1}() holds f . <*x,y,z*> = F_{2}(x,y,z) & ( for f1, f2 being Function of (3 -tuples_on F_{1}()),F_{1}() st ( for x, y, z being Element of F_{1}() holds f1 . <*x,y,z*> = F_{2}(x,y,z) ) & ( for x, y, z being Element of F_{1}() holds f2 . <*x,y,z*> = F_{2}(x,y,z) ) holds

f1 = f2 ) )

for x, y, z being Element of F

f1 = f2 ) )

proof end;

theorem Th33: :: CIRCCMB3:33

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)*>

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)*>

proof end;

theorem Th34: :: CIRCCMB3:34

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)*>

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)*>

proof end;

scheme :: CIRCCMB3:sch 9

OneGate1Result{ F_{1}() -> object , F_{2}() -> non empty finite set , F_{3}( object ) -> Element of F_{2}(), F_{4}() -> Function of (1 -tuples_on F_{2}()),F_{2}() } :

OneGate1Result{ F

for s being State of (1GateCircuit (<*F_{1}()*>,F_{4}()))

for a1 being Element of F_{2}() st a1 = s . F_{1}() holds

(Result s) . (Output (1GateCircStr (<*F_{1}()*>,F_{4}()))) = F_{3}(a1)

providedfor a1 being Element of F

(Result s) . (Output (1GateCircStr (<*F

A1:
for g being Function of (1 -tuples_on F_{2}()),F_{2}() holds

( g = F_{4}() iff for a1 being Element of F_{2}() holds g . <*a1*> = F_{3}(a1) )

( g = F

proof end;

scheme :: CIRCCMB3:sch 10

OneGate2Result{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> non empty finite set , F_{4}( object , object ) -> Element of F_{3}(), F_{5}() -> Function of (2 -tuples_on F_{3}()),F_{3}() } :

OneGate2Result{ F

for s being State of (1GateCircuit (<*F_{1}(),F_{2}()*>,F_{5}()))

for a1, a2 being Element of F_{3}() st a1 = s . F_{1}() & a2 = s . F_{2}() holds

(Result s) . (Output (1GateCircStr (<*F_{1}(),F_{2}()*>,F_{5}()))) = F_{4}(a1,a2)

providedfor a1, a2 being Element of F

(Result s) . (Output (1GateCircStr (<*F

A1:
for g being Function of (2 -tuples_on F_{3}()),F_{3}() holds

( g = F_{5}() iff for a1, a2 being Element of F_{3}() holds g . <*a1,a2*> = F_{4}(a1,a2) )

( g = F

proof end;

scheme :: CIRCCMB3:sch 11

OneGate3Result{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> object , F_{4}() -> non empty finite set , F_{5}( object , object , object ) -> Element of F_{4}(), F_{6}() -> Function of (3 -tuples_on F_{4}()),F_{4}() } :

OneGate3Result{ F

for s being State of (1GateCircuit (<*F_{1}(),F_{2}(),F_{3}()*>,F_{6}()))

for a1, a2, a3 being Element of F_{4}() st a1 = s . F_{1}() & a2 = s . F_{2}() & a3 = s . F_{3}() holds

(Result s) . (Output (1GateCircStr (<*F_{1}(),F_{2}(),F_{3}()*>,F_{6}()))) = F_{5}(a1,a2,a3)

providedfor a1, a2, a3 being Element of F

(Result s) . (Output (1GateCircStr (<*F

A1:
for g being Function of (3 -tuples_on F_{4}()),F_{4}() holds

( g = F_{6}() iff for a1, a2, a3 being Element of F_{4}() holds g . <*a1,a2,a3*> = F_{5}(a1,a2,a3) )

( g = F

proof end;

scheme :: CIRCCMB3:sch 12

OneGate4Result{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> object , F_{4}() -> object , F_{5}() -> non empty finite set , F_{6}( object , object , object , object ) -> Element of F_{5}(), F_{7}() -> Function of (4 -tuples_on F_{5}()),F_{5}() } :

OneGate4Result{ F

for s being State of (1GateCircuit (<*F_{1}(),F_{2}(),F_{3}(),F_{4}()*>,F_{7}()))

for a1, a2, a3, a4 being Element of F_{5}() st a1 = s . F_{1}() & a2 = s . F_{2}() & a3 = s . F_{3}() & a4 = s . F_{4}() holds

(Result s) . (Output (1GateCircStr (<*F_{1}(),F_{2}(),F_{3}(),F_{4}()*>,F_{7}()))) = F_{6}(a1,a2,a3,a4)

providedfor a1, a2, a3, a4 being Element of F

(Result s) . (Output (1GateCircStr (<*F

A1:
for g being Function of (4 -tuples_on F_{5}()),F_{5}() holds

( g = F_{7}() iff for a1, a2, a3, a4 being Element of F_{5}() holds g . <*a1,a2,a3,a4*> = F_{6}(a1,a2,a3,a4) )

( g = F

proof end;

scheme :: CIRCCMB3:sch 13

OneGate5Result{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> object , F_{4}() -> object , F_{5}() -> object , F_{6}() -> non empty finite set , F_{7}( object , object , object , object , object ) -> Element of F_{6}(), F_{8}() -> Function of (5 -tuples_on F_{6}()),F_{6}() } :

OneGate5Result{ F

for s being State of (1GateCircuit (<*F_{1}(),F_{2}(),F_{3}(),F_{4}(),F_{5}()*>,F_{8}()))

for a1, a2, a3, a4, a5 being Element of F_{6}() st a1 = s . F_{1}() & a2 = s . F_{2}() & a3 = s . F_{3}() & a4 = s . F_{4}() & a5 = s . F_{5}() holds

(Result s) . (Output (1GateCircStr (<*F_{1}(),F_{2}(),F_{3}(),F_{4}(),F_{5}()*>,F_{8}()))) = F_{7}(a1,a2,a3,a4,a5)

providedfor a1, a2, a3, a4, a5 being Element of F

(Result s) . (Output (1GateCircStr (<*F

A1:
for g being Function of (5 -tuples_on F_{6}()),F_{6}() holds

( g = F_{8}() iff for a1, a2, a3, a4, a5 being Element of F_{6}() holds g . <*a1,a2,a3,a4,a5*> = F_{7}(a1,a2,a3,a4,a5) )

( g = F

proof end;

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 & not Output (1GateCircStr (p,f)) in InputVertices S holds

InputVertices (S +* (1GateCircStr (p,f))) = InputVertices S

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 & not Output (1GateCircStr (p,f)) in InputVertices S holds

InputVertices (S +* (1GateCircStr (p,f))) = InputVertices S

proof end;

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 & 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

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 & 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

proof end;

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 & not Output (1GateCircStr (<*x1*>,f)) in InputVertices S holds

InputVertices (S +* (1GateCircStr (<*x1*>,f))) = InputVertices S

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 & not Output (1GateCircStr (<*x1*>,f)) in InputVertices S holds

InputVertices (S +* (1GateCircStr (<*x1*>,f))) = InputVertices S

proof end;

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 & not x2 in InnerVertices S & not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds

InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x2}

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 & not x2 in InnerVertices S & not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds

InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x2}

proof end;

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 & not x1 in InnerVertices S & not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds

InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x1}

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 & not x1 in InnerVertices S & not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds

InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = (InputVertices S) \/ {x1}

proof end;

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 & x2 in the carrier of S & not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds

InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = InputVertices S

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 & x2 in the carrier of S & not Output (1GateCircStr (<*x1,x2*>,f)) in InputVertices S holds

InputVertices (S +* (1GateCircStr (<*x1,x2*>,f))) = InputVertices S

proof end;

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 & 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}

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 & 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}

proof end;

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 & 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}

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 & 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}

proof end;

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 & 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}

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 & 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}

proof end;

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 & 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}

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 & 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}

proof end;

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 & 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}

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 & 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}

proof end;

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 & 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}

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 & 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}

proof end;

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 & 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

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 & 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

proof end;

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)

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)

proof end;

scheme :: CIRCCMB3:sch 14

Comb1CircResult{ F_{1}() -> object , F_{2}() -> non empty finite set , F_{3}( object ) -> Element of F_{2}(), F_{4}() -> finite Signature of F_{2}(), F_{5}() -> Circuit of F_{2}(),F_{4}(), F_{6}() -> Function of (1 -tuples_on F_{2}()),F_{2}() } :

Comb1CircResult{ F

for s being State of (F_{5}() +* (1GateCircuit (<*F_{1}()*>,F_{6}())))

for s9 being State of F_{5}() st s9 = s | the carrier of F_{4}() holds

for a1 being Element of F_{2}() st ( F_{1}() in InnerVertices F_{4}() implies a1 = (Result s9) . F_{1}() ) & ( not F_{1}() in InnerVertices F_{4}() implies a1 = s . F_{1}() ) holds

(Result s) . (Output (1GateCircStr (<*F_{1}()*>,F_{6}()))) = F_{3}(a1)

providedfor s9 being State of F

for a1 being Element of F

(Result s) . (Output (1GateCircStr (<*F

A1:
for g being Function of (1 -tuples_on F_{2}()),F_{2}() holds

( g = F_{6}() iff for a1 being Element of F_{2}() holds g . <*a1*> = F_{3}(a1) )
and

A2: not Output (1GateCircStr (<*F_{1}()*>,F_{6}())) in InputVertices F_{4}()

( g = F

A2: not Output (1GateCircStr (<*F

proof end;

scheme :: CIRCCMB3:sch 15

Comb2CircResult{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> non empty finite set , F_{4}( object , object ) -> Element of F_{3}(), F_{5}() -> finite Signature of F_{3}(), F_{6}() -> Circuit of F_{3}(),F_{5}(), F_{7}() -> Function of (2 -tuples_on F_{3}()),F_{3}() } :

Comb2CircResult{ F

for s being State of (F_{6}() +* (1GateCircuit (<*F_{1}(),F_{2}()*>,F_{7}())))

for s9 being State of F_{6}() st s9 = s | the carrier of F_{5}() holds

for a1, a2 being Element of F_{3}() st ( F_{1}() in InnerVertices F_{5}() implies a1 = (Result s9) . F_{1}() ) & ( not F_{1}() in InnerVertices F_{5}() implies a1 = s . F_{1}() ) & ( F_{2}() in InnerVertices F_{5}() implies a2 = (Result s9) . F_{2}() ) & ( not F_{2}() in InnerVertices F_{5}() implies a2 = s . F_{2}() ) holds

(Result s) . (Output (1GateCircStr (<*F_{1}(),F_{2}()*>,F_{7}()))) = F_{4}(a1,a2)

providedfor s9 being State of F

for a1, a2 being Element of F

(Result s) . (Output (1GateCircStr (<*F

A1:
for g being Function of (2 -tuples_on F_{3}()),F_{3}() holds

( g = F_{7}() iff for a1, a2 being Element of F_{3}() holds g . <*a1,a2*> = F_{4}(a1,a2) )
and

A2: not Output (1GateCircStr (<*F_{1}(),F_{2}()*>,F_{7}())) in InputVertices F_{5}()

( g = F

A2: not Output (1GateCircStr (<*F

proof end;

scheme :: CIRCCMB3:sch 16

Comb3CircResult{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> object , F_{4}() -> non empty finite set , F_{5}( object , object , object ) -> Element of F_{4}(), F_{6}() -> finite Signature of F_{4}(), F_{7}() -> Circuit of F_{4}(),F_{6}(), F_{8}() -> Function of (3 -tuples_on F_{4}()),F_{4}() } :

Comb3CircResult{ F

for s being State of (F_{7}() +* (1GateCircuit (<*F_{1}(),F_{2}(),F_{3}()*>,F_{8}())))

for s9 being State of F_{7}() st s9 = s | the carrier of F_{6}() holds

for a1, a2, a3 being Element of F_{4}() st ( F_{1}() in InnerVertices F_{6}() implies a1 = (Result s9) . F_{1}() ) & ( not F_{1}() in InnerVertices F_{6}() implies a1 = s . F_{1}() ) & ( F_{2}() in InnerVertices F_{6}() implies a2 = (Result s9) . F_{2}() ) & ( not F_{2}() in InnerVertices F_{6}() implies a2 = s . F_{2}() ) & ( F_{3}() in InnerVertices F_{6}() implies a3 = (Result s9) . F_{3}() ) & ( not F_{3}() in InnerVertices F_{6}() implies a3 = s . F_{3}() ) holds

(Result s) . (Output (1GateCircStr (<*F_{1}(),F_{2}(),F_{3}()*>,F_{8}()))) = F_{5}(a1,a2,a3)

providedfor s9 being State of F

for a1, a2, a3 being Element of F

(Result s) . (Output (1GateCircStr (<*F

A1:
for g being Function of (3 -tuples_on F_{4}()),F_{4}() holds

( g = F_{8}() iff for a1, a2, a3 being Element of F_{4}() holds g . <*a1,a2,a3*> = F_{5}(a1,a2,a3) )
and

A2: not Output (1GateCircStr (<*F_{1}(),F_{2}(),F_{3}()*>,F_{8}())) in InputVertices F_{6}()

( g = F

A2: not Output (1GateCircStr (<*F

proof end;

scheme :: CIRCCMB3:sch 17

Comb4CircResult{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> object , F_{4}() -> object , F_{5}() -> non empty finite set , F_{6}( object , object , object , object ) -> Element of F_{5}(), F_{7}() -> finite Signature of F_{5}(), F_{8}() -> Circuit of F_{5}(),F_{7}(), F_{9}() -> Function of (4 -tuples_on F_{5}()),F_{5}() } :

Comb4CircResult{ F

for s being State of (F_{8}() +* (1GateCircuit (<*F_{1}(),F_{2}(),F_{3}(),F_{4}()*>,F_{9}())))

for s9 being State of F_{8}() st s9 = s | the carrier of F_{7}() holds

for a1, a2, a3, a4 being Element of F_{5}() st ( F_{1}() in InnerVertices F_{7}() implies a1 = (Result s9) . F_{1}() ) & ( not F_{1}() in InnerVertices F_{7}() implies a1 = s . F_{1}() ) & ( F_{2}() in InnerVertices F_{7}() implies a2 = (Result s9) . F_{2}() ) & ( not F_{2}() in InnerVertices F_{7}() implies a2 = s . F_{2}() ) & ( F_{3}() in InnerVertices F_{7}() implies a3 = (Result s9) . F_{3}() ) & ( not F_{3}() in InnerVertices F_{7}() implies a3 = s . F_{3}() ) & ( F_{4}() in InnerVertices F_{7}() implies a4 = (Result s9) . F_{4}() ) & ( not F_{4}() in InnerVertices F_{7}() implies a4 = s . F_{4}() ) holds

(Result s) . (Output (1GateCircStr (<*F_{1}(),F_{2}(),F_{3}(),F_{4}()*>,F_{9}()))) = F_{6}(a1,a2,a3,a4)

providedfor s9 being State of F

for a1, a2, a3, a4 being Element of F

(Result s) . (Output (1GateCircStr (<*F

A1:
for g being Function of (4 -tuples_on F_{5}()),F_{5}() holds

( g = F_{9}() iff for a1, a2, a3, a4 being Element of F_{5}() holds g . <*a1,a2,a3,a4*> = F_{6}(a1,a2,a3,a4) )
and

A2: not Output (1GateCircStr (<*F_{1}(),F_{2}(),F_{3}(),F_{4}()*>,F_{9}())) in InputVertices F_{7}()

( g = F

A2: not Output (1GateCircStr (<*F

proof end;

scheme :: CIRCCMB3:sch 18

Comb5CircResult{ F_{1}() -> object , F_{2}() -> object , F_{3}() -> object , F_{4}() -> object , F_{5}() -> object , F_{6}() -> non empty finite set , F_{7}( object , object , object , object , object ) -> Element of F_{6}(), F_{8}() -> finite Signature of F_{6}(), F_{9}() -> Circuit of F_{6}(),F_{8}(), F_{10}() -> Function of (5 -tuples_on F_{6}()),F_{6}() } :

Comb5CircResult{ F

for s being State of (F_{9}() +* (1GateCircuit (<*F_{1}(),F_{2}(),F_{3}(),F_{4}(),F_{5}()*>,F_{10}())))

for s9 being State of F_{9}() st s9 = s | the carrier of F_{8}() holds

for a1, a2, a3, a4, a5 being Element of F_{6}() st ( F_{1}() in InnerVertices F_{8}() implies a1 = (Result s9) . F_{1}() ) & ( not F_{1}() in InnerVertices F_{8}() implies a1 = s . F_{1}() ) & ( F_{2}() in InnerVertices F_{8}() implies a2 = (Result s9) . F_{2}() ) & ( not F_{2}() in InnerVertices F_{8}() implies a2 = s . F_{2}() ) & ( F_{3}() in InnerVertices F_{8}() implies a3 = (Result s9) . F_{3}() ) & ( not F_{3}() in InnerVertices F_{8}() implies a3 = s . F_{3}() ) & ( F_{4}() in InnerVertices F_{8}() implies a4 = (Result s9) . F_{4}() ) & ( not F_{4}() in InnerVertices F_{8}() implies a4 = s . F_{4}() ) & ( F_{5}() in InnerVertices F_{8}() implies a5 = (Result s9) . F_{5}() ) & ( not F_{5}() in InnerVertices F_{8}() implies a5 = s . F_{5}() ) holds

(Result s) . (Output (1GateCircStr (<*F_{1}(),F_{2}(),F_{3}(),F_{4}(),F_{5}()*>,F_{10}()))) = F_{7}(a1,a2,a3,a4,a5)

providedfor s9 being State of F

for a1, a2, a3, a4, a5 being Element of F

(Result s) . (Output (1GateCircStr (<*F

A1:
for g being Function of (5 -tuples_on F_{6}()),F_{6}() holds

( g = F_{10}() iff for a1, a2, a3, a4, a5 being Element of F_{6}() holds g . <*a1,a2,a3,a4,a5*> = F_{7}(a1,a2,a3,a4,a5) )
and

A2: not Output (1GateCircStr (<*F_{1}(),F_{2}(),F_{3}(),F_{4}(),F_{5}()*>,F_{10}())) in InputVertices F_{8}()

( g = F

A2: not Output (1GateCircStr (<*F

proof 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 );

for S being non empty ManySortedSign holds

( S is with_nonpair_inputs iff InputVertices S is without_pairs );

registration

coherence

not NAT is with_pair ;

let X be without_pairs set ;

coherence

for b_{1} being Subset of X holds b_{1} is without_pairs
by FACIRC_1:def 2;

end;
not NAT is with_pair ;

let X be without_pairs set ;

coherence

for b

registration

coherence

for b_{1} being Function st b_{1} is natural-valued holds

b_{1} is nonpair-yielding

end;
for b

b

proof end;

registration

ex b_{1} being FinSequence st

( b_{1} is one-to-one & b_{1} is natural-valued )
end;

cluster Relation-like NAT -defined Function-like one-to-one finite FinSequence-like FinSubsequence-like V98() natural-valued for set ;

existence ex b

( b

proof end;

registration

let n be Element of NAT ;

ex b_{1} being FinSeqLen of n st

( b_{1} is one-to-one & b_{1} is natural-valued )

end;
cluster Relation-like NAT -defined Function-like one-to-one finite V45(n) FinSequence-like FinSubsequence-like V98() natural-valued for set ;

existence ex b

( b

proof end;

registration

let p be nonpair-yielding FinSequence;

let f be set ;

coherence

1GateCircStr (p,f) is with_nonpair_inputs

end;
let f be set ;

coherence

1GateCircStr (p,f) is with_nonpair_inputs

proof end;

registration

ex b_{1} being one-gate ManySortedSign st b_{1} is with_nonpair_inputs

ex b_{1} being one-gate Signature of X st b_{1} is with_nonpair_inputs
end;

cluster non empty finite non void V82() strict Circuit-like unsplit gate`1=arity gate`2=den one-gate with_nonpair_inputs for ManySortedSign ;

existence ex b

proof end;

let X be non empty finite set ;
cluster non empty finite non void V82() strict Circuit-like unsplit gate`1=arity gate`2=den one-gate with_nonpair_inputs for Signature of X;

existence ex b

proof end;

registration

let S be non empty with_nonpair_inputs ManySortedSign ;

coherence

not InputVertices S is with_pair by Def11;

end;
coherence

not InputVertices S is with_pair by Def11;

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

for x being Vertex of S st x is pair holds

x in InnerVertices S

proof end;

registration

let S be non empty unsplit gate`1=arity ManySortedSign ;

coherence

InnerVertices S is Relation-like

end;
coherence

InnerVertices S is Relation-like

proof end;

registration

let S be non empty non void unsplit gate`2=den ManySortedSign ;

coherence

InnerVertices S is Relation-like

end;
coherence

InnerVertices S is Relation-like

proof end;

registration

let S1, S2 be non empty unsplit gate`1=arity with_nonpair_inputs ManySortedSign ;

coherence

S1 +* S2 is with_nonpair_inputs

end;
coherence

S1 +* S2 is with_nonpair_inputs

proof end;

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

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

proof end;

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;

coherence

S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs by Th51;

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

coherence

S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs by Th51;

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;

coherence

S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs ;

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

coherence

S +* (1GateCircStr (<*x1*>,f)) is with_nonpair_inputs ;

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 ) & ( x2 in the carrier of S or not x2 is pair ) holds

S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs

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 ) & ( x2 in the carrier of S or not x2 is pair ) holds

S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs

proof end;

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;

coherence

S +* (1GateCircStr (<*x1,n2*>,f)) is with_nonpair_inputs by Th52;

coherence

S +* (1GateCircStr (<*n2,x1*>,f)) is with_nonpair_inputs by Th52;

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

coherence

S +* (1GateCircStr (<*x1,n2*>,f)) is with_nonpair_inputs by Th52;

coherence

S +* (1GateCircStr (<*n2,x1*>,f)) is with_nonpair_inputs by Th52;

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;

coherence

S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs by Th52;

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

coherence

S +* (1GateCircStr (<*x1,x2*>,f)) is with_nonpair_inputs by Th52;

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 ) & ( x2 in the carrier of S or not x2 is pair ) & ( x3 in the carrier of S or not x3 is pair ) holds

S +* (1GateCircStr (<*x1,x2,x3*>,f)) is with_nonpair_inputs

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 ) & ( x2 in the carrier of S or not x2 is pair ) & ( x3 in the carrier of S or not x3 is pair ) holds

S +* (1GateCircStr (<*x1,x2,x3*>,f)) is with_nonpair_inputs

proof 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 n be non pair set ;

let f be Function of (3 -tuples_on X),X;

coherence

S +* (1GateCircStr (<*x1,x2,n*>,f)) is with_nonpair_inputs by Th53;

coherence

S +* (1GateCircStr (<*x1,n,x2*>,f)) is with_nonpair_inputs by Th53;

coherence

S +* (1GateCircStr (<*n,x1,x2*>,f)) is with_nonpair_inputs by Th53;

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

coherence

S +* (1GateCircStr (<*x1,x2,n*>,f)) is with_nonpair_inputs by Th53;

coherence

S +* (1GateCircStr (<*x1,n,x2*>,f)) is with_nonpair_inputs by Th53;

coherence

S +* (1GateCircStr (<*n,x1,x2*>,f)) is with_nonpair_inputs by Th53;

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;

coherence

S +* (1GateCircStr (<*x,n1,n2*>,f)) is with_nonpair_inputs by Th53;

coherence

S +* (1GateCircStr (<*n1,x,n2*>,f)) is with_nonpair_inputs by Th53;

coherence

S +* (1GateCircStr (<*n1,n2,x*>,f)) is with_nonpair_inputs by Th53;

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

coherence

S +* (1GateCircStr (<*x,n1,n2*>,f)) is with_nonpair_inputs by Th53;

coherence

S +* (1GateCircStr (<*n1,x,n2*>,f)) is with_nonpair_inputs by Th53;

coherence

S +* (1GateCircStr (<*n1,n2,x*>,f)) is with_nonpair_inputs by Th53;

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;

coherence

S +* (1GateCircStr (<*x1,x2,x3*>,f)) is with_nonpair_inputs by Th53;

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

coherence

S +* (1GateCircStr (<*x1,x2,x3*>,f)) is with_nonpair_inputs by Th53;