CIRCCMB3: Preliminaries to Automatic Generation of Mizar Documentation for Circuits

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

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;

attr s 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 :

definition

let S be non empty non void Circuit-like ManySortedSign ;
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 ;

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 ;

end;

:: deftheorem Def2 defines stabilizing CIRCCMB3:def 2 :

:: deftheorem defines with_stabilization-limit CIRCCMB3:def 3 :

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

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Result CIRCCMB3:def 4 :

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 & ( for n being Element of NAT st n < it holds
not Following (s,n) is stable ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines stabilization-time CIRCCMB3:def 5 :

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

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

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)

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)

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

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

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

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

proof end;

theorem Th10: :: CIRCCMB3:10

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

proof end;

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

proof end;

theorem Th13: :: CIRCCMB3:13

for x1, x2, x3, x4 being set holds rng <*x1,x2,x3,x4*> = {x1,x2,x3,x4}

proof end;

theorem Th14: :: CIRCCMB3:14

for x1, x2, x3, x4, x5 being set holds rng <*x1,x2,x3,x4,x5*> = {x1,x2,x3,x4,x5}

proof end;

definition

let S be ManySortedSign ;

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

end;

:: deftheorem Def6 defines one-gate CIRCCMB3:def 6 :

definition

let S be non empty ManySortedSign ;
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) );

end;

:: deftheorem Def7 defines one-gate CIRCCMB3:def 7 :

registration

let p be FinSequence;
let x be set ;

cluster 1GateCircStr (p,x) -> finite ;

coherence

proof end;

end;

registration

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

coherence

proof end;

end;

registration

cluster non empty one-gate -> non empty gate`2=den for ManySortedSign ;

coherence

proof end;

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 by Def6;

end;

registration

cluster one-gate for ManySortedSign ;

existence

proof end;

end;

registration

let S be one-gate ManySortedSign ;

cluster finite-yielding one-gate -> strict non-empty for MSAlgebra over S;

coherence

proof end;

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 by Def7;

end;

registration

let S be one-gate ManySortedSign ;

cluster non-empty finite-yielding one-gate for MSAlgebra over S;

existence

proof end;

end;

definition

let S be one-gate ManySortedSign ;

func Output S -> Vertex of S equals :: CIRCCMB3:def 8
union the carrier' of S;

coherence

proof end;

end;

:: deftheorem defines Output CIRCCMB3:def 8 :

registration

let S be one-gate ManySortedSign ;

cluster Output S -> pair ;

coherence

proof end;

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]

proof end;

theorem Th16: :: CIRCCMB3:16

for S being one-gate ManySortedSign holds InnerVertices S = {(Output S)}

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)

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)

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

proof end;

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

proof end;

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

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

proof end;

scheme :: CIRCCMB3:sch 1
OneGate1Ex{ F₁() -> set , F₂() -> non empty finite set , F₃( set ) -> Element of F₂() } :

ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st
( InputVertices S = {F₁()} & ( for s being State of A holds (Result s) . (Output S) = F₃((s . F₁())) ) )

proof end;

scheme :: CIRCCMB3:sch 2
OneGate2Ex{ F₁() -> set , F₂() -> set , F₃() -> non empty finite set , F₄( set , set ) -> Element of F₃() } :

ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st
( InputVertices S = {F₁(),F₂()} & ( for s being State of A holds (Result s) . (Output S) = F₄((s . F₁()),(s . F₂())) ) )

proof end;

scheme :: CIRCCMB3:sch 3
OneGate3Ex{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> non empty finite set , F₅( set , set , set ) -> Element of F₄() } :

ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st
( InputVertices S = {F₁(),F₂(),F₃()} & ( for s being State of A holds (Result s) . (Output S) = F₅((s . F₁()),(s . F₂()),(s . F₃())) ) )

proof end;

scheme :: CIRCCMB3:sch 4
OneGate4Ex{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> non empty finite set , F₆( set , set , set , set ) -> Element of F₅() } :

ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st
( InputVertices S = {F₁(),F₂(),F₃(),F₄()} & ( for s being State of A holds (Result s) . (Output S) = F₆((s . F₁()),(s . F₂()),(s . F₃()),(s . F₄())) ) )

proof end;

scheme :: CIRCCMB3:sch 5
OneGate5Ex{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> set , F₆() -> non empty finite set , F₇( set , set , set , set , set ) -> Element of F₆() } :

ex S being one-gate ManySortedSign ex A being one-gate Circuit of S st
( InputVertices S = {F₁(),F₂(),F₃(),F₄(),F₅()} & ( for s being State of A holds (Result s) . (Output S) = F₇((s . F₁()),(s . F₂()),(s . F₃()),(s . F₄()),(s . F₅())) ) )

proof end;

begin

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 )

proof end;

theorem :: CIRCCMB3:23

for S1, S2 being non empty ManySortedSign
for v being Vertex of S1 holds v is Vertex of (S1 +* S2)

proof end;

theorem :: CIRCCMB3:24

for S1, S2 being non empty ManySortedSign
for v being Vertex of S2 holds v is Vertex of (S1 +* S2)

proof end;

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

existence

proof end;

end;

:: deftheorem Def9 defines Signature CIRCCMB3:def 9 :

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

proof end;

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

proof end;

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 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 & the Sorts of it is constant & the_value_of the Sorts of it = X );

existence

proof end;

end;

:: deftheorem Def10 defines Circuit CIRCCMB3:def 10 :

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

proof end;

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)

proof end;

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

proof end;

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

proof end;

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

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

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

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 )

proof end;

registration

let S1, S2 be non empty finite ManySortedSign ;

cluster S1 +* S2 -> finite ;

coherence

proof end;

end;

registration

let X be non empty finite set ;
let S1, S2 be Signature of X;

cluster S1 +* S2 -> gate`2=den ;

coherence

proof end;

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

proof end;

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

proof end;

end;

theorem Th31: :: CIRCCMB3:31

for x, y being set holds
( the_rank_of x in the_rank_of [x,y] & the_rank_of y in the_rank_of [x,y] )

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

proof end;

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 by Th32;

end;

scheme :: CIRCCMB3:sch 6
1AryDef{ F₁() -> non empty set , F₂( set ) -> Element of F₁() } :

( ex f being Function of (1 -tuples_on F₁()),F₁() st
for x being Element of F₁() holds f . <*x*> = F₂(x) & ( for f1, f2 being Function of (1 -tuples_on F₁()),F₁() st ( for x being Element of F₁() holds f1 . <*x*> = F₂(x) ) & ( for x being Element of F₁() holds f2 . <*x*> = F₂(x) ) holds
f1 = f2 ) )

proof end;

scheme :: CIRCCMB3:sch 7
2AryDef{ F₁() -> non empty set , F₂( set , set ) -> Element of F₁() } :

( ex f being Function of (2 -tuples_on F₁()),F₁() st
for x, y being Element of F₁() holds f . <*x,y*> = F₂(x,y) & ( for f1, f2 being Function of (2 -tuples_on F₁()),F₁() st ( for x, y being Element of F₁() holds f1 . <*x,y*> = F₂(x,y) ) & ( for x, y being Element of F₁() holds f2 . <*x,y*> = F₂(x,y) ) holds
f1 = f2 ) )

proof end;

scheme :: CIRCCMB3:sch 8
3AryDef{ F₁() -> non empty set , F₂( set , set , set ) -> Element of F₁() } :

( ex f being Function of (3 -tuples_on F₁()),F₁() st
for x, y, z being Element of F₁() holds f . <*x,y,z*> = F₂(x,y,z) & ( for f1, f2 being Function of (3 -tuples_on F₁()),F₁() st ( for x, y, z being Element of F₁() holds f1 . <*x,y,z*> = F₂(x,y,z) ) & ( for x, y, z being Element of F₁() holds f2 . <*x,y,z*> = F₂(x,y,z) ) holds
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)*>

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

proof end;

scheme :: CIRCCMB3:sch 9
OneGate1Result{ F₁() -> set , F₂() -> non empty finite set , F₃( set ) -> Element of F₂(), F₄() -> Function of (1 -tuples_on F₂()),F₂() } :

for s being State of (1GateCircuit (<*F₁()*>,F₄()))
for a1 being Element of F₂() st a1 = s . F₁() holds
(Result s) . (Output (1GateCircStr (<*F₁()*>,F₄()))) = F₃(a1)

provided

A1: for g being Function of (1 -tuples_on F₂()),F₂() holds
( g = F₄() iff for a1 being Element of F₂() holds g . <*a1*> = F₃(a1) )

proof end;

scheme :: CIRCCMB3:sch 10
OneGate2Result{ F₁() -> set , F₂() -> set , F₃() -> non empty finite set , F₄( set , set ) -> Element of F₃(), F₅() -> Function of (2 -tuples_on F₃()),F₃() } :

for s being State of (1GateCircuit (<*F₁(),F₂()*>,F₅()))
for a1, a2 being Element of F₃() st a1 = s . F₁() & a2 = s . F₂() holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂()*>,F₅()))) = F₄(a1,a2)

provided

A1: for g being Function of (2 -tuples_on F₃()),F₃() holds
( g = F₅() iff for a1, a2 being Element of F₃() holds g . <*a1,a2*> = F₄(a1,a2) )

proof end;

scheme :: CIRCCMB3:sch 11
OneGate3Result{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> non empty finite set , F₅( set , set , set ) -> Element of F₄(), F₆() -> Function of (3 -tuples_on F₄()),F₄() } :

for s being State of (1GateCircuit (<*F₁(),F₂(),F₃()*>,F₆()))
for a1, a2, a3 being Element of F₄() st a1 = s . F₁() & a2 = s . F₂() & a3 = s . F₃() holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃()*>,F₆()))) = F₅(a1,a2,a3)

provided

A1: for g being Function of (3 -tuples_on F₄()),F₄() holds
( g = F₆() iff for a1, a2, a3 being Element of F₄() holds g . <*a1,a2,a3*> = F₅(a1,a2,a3) )

proof end;

scheme :: CIRCCMB3:sch 12
OneGate4Result{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> non empty finite set , F₆( set , set , set , set ) -> Element of F₅(), F₇() -> Function of (4 -tuples_on F₅()),F₅() } :

for s being State of (1GateCircuit (<*F₁(),F₂(),F₃(),F₄()*>,F₇()))
for a1, a2, a3, a4 being Element of F₅() st a1 = s . F₁() & a2 = s . F₂() & a3 = s . F₃() & a4 = s . F₄() holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₇()))) = F₆(a1,a2,a3,a4)

provided

A1: for g being Function of (4 -tuples_on F₅()),F₅() holds
( g = F₇() iff for a1, a2, a3, a4 being Element of F₅() holds g . <*a1,a2,a3,a4*> = F₆(a1,a2,a3,a4) )

proof end;

scheme :: CIRCCMB3:sch 13
OneGate5Result{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> set , F₆() -> non empty finite set , F₇( set , set , set , set , set ) -> Element of F₆(), F₈() -> Function of (5 -tuples_on F₆()),F₆() } :

for s being State of (1GateCircuit (<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈()))
for a1, a2, a3, a4, a5 being Element of F₆() st a1 = s . F₁() & a2 = s . F₂() & a3 = s . F₃() & a4 = s . F₄() & a5 = s . F₅() holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₈()))) = F₇(a1,a2,a3,a4,a5)

provided

A1: for g being Function of (5 -tuples_on F₆()),F₆() holds
( g = F₈() iff for a1, a2, a3, a4, a5 being Element of F₆() holds g . <*a1,a2,a3,a4,a5*> = F₇(a1,a2,a3,a4,a5) )

proof end;

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

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

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}

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}

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

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}

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}

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}

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}

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}

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}

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

proof end;

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)

proof end;

scheme :: CIRCCMB3:sch 14
Comb1CircResult{ F₁() -> set , F₂() -> non empty finite set , F₃( set ) -> Element of F₂(), F₄() -> finite Signature of F₂(), F₅() -> Circuit of F₂(),F₄(), F₆() -> Function of (1 -tuples_on F₂()),F₂() } :

for s being State of (F₅() +* (1GateCircuit (<*F₁()*>,F₆())))
for s9 being State of F₅() st s9 = s | the carrier of F₄() holds
for a1 being Element of F₂() st ( F₁() in InnerVertices F₄() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₄() implies a1 = s . F₁() ) holds
(Result s) . (Output (1GateCircStr (<*F₁()*>,F₆()))) = F₃(a1)

provided

A1: for g being Function of (1 -tuples_on F₂()),F₂() holds
( g = F₆() iff for a1 being Element of F₂() holds g . <*a1*> = F₃(a1) ) and
A2: not Output (1GateCircStr (<*F₁()*>,F₆())) in InputVertices F₄()

proof end;

scheme :: CIRCCMB3:sch 15
Comb2CircResult{ F₁() -> set , F₂() -> set , F₃() -> non empty finite set , F₄( set , set ) -> Element of F₃(), F₅() -> finite Signature of F₃(), F₆() -> Circuit of F₃(),F₅(), F₇() -> Function of (2 -tuples_on F₃()),F₃() } :

for s being State of (F₆() +* (1GateCircuit (<*F₁(),F₂()*>,F₇())))
for s9 being State of F₆() st s9 = s | the carrier of F₅() holds
for a1, a2 being Element of F₃() st ( F₁() in InnerVertices F₅() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₅() implies a1 = s . F₁() ) & ( F₂() in InnerVertices F₅() implies a2 = (Result s9) . F₂() ) & ( not F₂() in InnerVertices F₅() implies a2 = s . F₂() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂()*>,F₇()))) = F₄(a1,a2)

provided

A1: for g being Function of (2 -tuples_on F₃()),F₃() holds
( g = F₇() iff for a1, a2 being Element of F₃() holds g . <*a1,a2*> = F₄(a1,a2) ) and
A2: not Output (1GateCircStr (<*F₁(),F₂()*>,F₇())) in InputVertices F₅()

proof end;

scheme :: CIRCCMB3:sch 16
Comb3CircResult{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> non empty finite set , F₅( set , set , set ) -> Element of F₄(), F₆() -> finite Signature of F₄(), F₇() -> Circuit of F₄(),F₆(), F₈() -> Function of (3 -tuples_on F₄()),F₄() } :

for s being State of (F₇() +* (1GateCircuit (<*F₁(),F₂(),F₃()*>,F₈())))
for s9 being State of F₇() st s9 = s | the carrier of F₆() holds
for a1, a2, a3 being Element of F₄() st ( F₁() in InnerVertices F₆() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₆() implies a1 = s . F₁() ) & ( F₂() in InnerVertices F₆() implies a2 = (Result s9) . F₂() ) & ( not F₂() in InnerVertices F₆() implies a2 = s . F₂() ) & ( F₃() in InnerVertices F₆() implies a3 = (Result s9) . F₃() ) & ( not F₃() in InnerVertices F₆() implies a3 = s . F₃() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃()*>,F₈()))) = F₅(a1,a2,a3)

provided

A1: for g being Function of (3 -tuples_on F₄()),F₄() holds
( g = F₈() iff for a1, a2, a3 being Element of F₄() holds g . <*a1,a2,a3*> = F₅(a1,a2,a3) ) and
A2: not Output (1GateCircStr (<*F₁(),F₂(),F₃()*>,F₈())) in InputVertices F₆()

proof end;

scheme :: CIRCCMB3:sch 17
Comb4CircResult{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> non empty finite set , F₆( set , set , set , set ) -> Element of F₅(), F₇() -> finite Signature of F₅(), F₈() -> Circuit of F₅(),F₇(), F₉() -> Function of (4 -tuples_on F₅()),F₅() } :

for s being State of (F₈() +* (1GateCircuit (<*F₁(),F₂(),F₃(),F₄()*>,F₉())))
for s9 being State of F₈() st s9 = s | the carrier of F₇() holds
for a1, a2, a3, a4 being Element of F₅() st ( F₁() in InnerVertices F₇() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₇() implies a1 = s . F₁() ) & ( F₂() in InnerVertices F₇() implies a2 = (Result s9) . F₂() ) & ( not F₂() in InnerVertices F₇() implies a2 = s . F₂() ) & ( F₃() in InnerVertices F₇() implies a3 = (Result s9) . F₃() ) & ( not F₃() in InnerVertices F₇() implies a3 = s . F₃() ) & ( F₄() in InnerVertices F₇() implies a4 = (Result s9) . F₄() ) & ( not F₄() in InnerVertices F₇() implies a4 = s . F₄() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) = F₆(a1,a2,a3,a4)

provided

A1: for g being Function of (4 -tuples_on F₅()),F₅() holds
( g = F₉() iff for a1, a2, a3, a4 being Element of F₅() holds g . <*a1,a2,a3,a4*> = F₆(a1,a2,a3,a4) ) and
A2: not Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉())) in InputVertices F₇()

proof end;

scheme :: CIRCCMB3:sch 18
Comb5CircResult{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> set , F₆() -> non empty finite set , F₇( set , set , set , set , set ) -> Element of F₆(), F₈() -> finite Signature of F₆(), F₉() -> Circuit of F₆(),F₈(), F₁₀() -> Function of (5 -tuples_on F₆()),F₆() } :

for s being State of (F₉() +* (1GateCircuit (<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())))
for s9 being State of F₉() st s9 = s | the carrier of F₈() holds
for a1, a2, a3, a4, a5 being Element of F₆() st ( F₁() in InnerVertices F₈() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₈() implies a1 = s . F₁() ) & ( F₂() in InnerVertices F₈() implies a2 = (Result s9) . F₂() ) & ( not F₂() in InnerVertices F₈() implies a2 = s . F₂() ) & ( F₃() in InnerVertices F₈() implies a3 = (Result s9) . F₃() ) & ( not F₃() in InnerVertices F₈() implies a3 = s . F₃() ) & ( F₄() in InnerVertices F₈() implies a4 = (Result s9) . F₄() ) & ( not F₄() in InnerVertices F₈() implies a4 = s . F₄() ) & ( F₅() in InnerVertices F₈() implies a5 = (Result s9) . F₅() ) & ( not F₅() in InnerVertices F₈() implies a5 = s . F₅() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()))) = F₇(a1,a2,a3,a4,a5)

provided

A1: for g being Function of (5 -tuples_on F₆()),F₆() holds
( g = F₁₀() iff for a1, a2, a3, a4, a5 being Element of F₆() holds g . <*a1,a2,a3,a4,a5*> = F₇(a1,a2,a3,a4,a5) ) and
A2: not Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) in InputVertices F₈()

proof end;

begin

definition

let S be non empty ManySortedSign ;

attr S is with_nonpair_inputs means :Def11: :: CIRCCMB3:def 11
InputVertices S is without_pairs ;

end;

:: deftheorem Def11 defines with_nonpair_inputs CIRCCMB3:def 11 :

registration

cluster NAT -> without_pairs ;

coherence

proof end;

let X be without_pairs set ;

cluster -> without_pairs for Element of bool X;

coherence

proof end;

end;

registration

cluster Relation-like Function-like natural-valued -> nonpair-yielding for set ;

coherence

proof end;

end;

registration

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

existence

proof end;

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

proof end;

end;

registration

let p be nonpair-yielding FinSequence;
let f be set ;

cluster 1GateCircStr (p,f) -> with_nonpair_inputs ;

coherence

proof end;

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

proof end;

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

proof end;

end;

registration

let S be non empty with_nonpair_inputs ManySortedSign ;

cluster InputVertices S -> without_pairs ;

coherence 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

proof end;

registration

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

cluster InnerVertices S -> Relation-like ;

coherence

proof end;

end;

registration

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

cluster InnerVertices S -> Relation-like ;

coherence

proof end;

end;

registration

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

cluster S1 +* S2 -> with_nonpair_inputs ;

coherence

proof end;

end;

theorem :: CIRCCMB3:50

for x being non pair set
for R being Relation holds not x in R

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

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;

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

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

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

coherence ;

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

cluster S +* (1GateCircStr (<*x1,n2*>,f)) -> with_nonpair_inputs ;

coherence by Th52;

cluster S +* (1GateCircStr (<*n2,x1*>,f)) -> with_nonpair_inputs ;

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

cluster S +* (1GateCircStr (<*x1,x2*>,f)) -> with_nonpair_inputs ;

coherence 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 ) & ( 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;

cluster S +* (1GateCircStr (<*x1,x2,n*>,f)) -> with_nonpair_inputs ;

coherence by Th53;

cluster S +* (1GateCircStr (<*x1,n,x2*>,f)) -> with_nonpair_inputs ;

coherence by Th53;

cluster S +* (1GateCircStr (<*n,x1,x2*>,f)) -> with_nonpair_inputs ;

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

cluster S +* (1GateCircStr (<*x,n1,n2*>,f)) -> with_nonpair_inputs ;

coherence by Th53;

cluster S +* (1GateCircStr (<*n1,x,n2*>,f)) -> with_nonpair_inputs ;

coherence by Th53;

cluster S +* (1GateCircStr (<*n1,n2,x*>,f)) -> with_nonpair_inputs ;

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

cluster S +* (1GateCircStr (<*x1,x2,x3*>,f)) -> with_nonpair_inputs ;

coherence by Th53;

end;