:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto

::

:: Received December 15, 1994

:: Copyright (c) 1994-2012 Association of Mizar Users

begin

definition

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

mode Circuit of S is finite-yielding MSAlgebra over S;

end;
mode Circuit of S is finite-yielding MSAlgebra over S;

definition

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

let SCS be non-empty Circuit of IIG;

ex b_{1} being ManySortedSet of SortsWithConstants IIG st

for x being Vertex of IIG st x in dom b_{1} holds

b_{1} . x in Constants (SCS,x)

uniqueness

for b_{1}, b_{2} being ManySortedSet of SortsWithConstants IIG st ( for x being Vertex of IIG st x in dom b_{1} holds

b_{1} . x in Constants (SCS,x) ) & ( for x being Vertex of IIG st x in dom b_{2} holds

b_{2} . x in Constants (SCS,x) ) holds

b_{1} = b_{2};

end;
let SCS be non-empty Circuit of IIG;

func Set-Constants SCS -> ManySortedSet of SortsWithConstants IIG means :Def1: :: CIRCUIT1:def 1

for x being Vertex of IIG st x in dom it holds

it . x in Constants (SCS,x);

existence for x being Vertex of IIG st x in dom it holds

it . x in Constants (SCS,x);

ex b

for x being Vertex of IIG st x in dom b

b

proof end;

correctness uniqueness

for b

b

b

b

proof end;

:: deftheorem Def1 defines Set-Constants CIRCUIT1:def 1 :

for IIG being non empty non void Circuit-like ManySortedSign

for SCS being non-empty Circuit of IIG

for b_{3} being ManySortedSet of SortsWithConstants IIG holds

( b_{3} = Set-Constants SCS iff for x being Vertex of IIG st x in dom b_{3} holds

b_{3} . x in Constants (SCS,x) );

for IIG being non empty non void Circuit-like ManySortedSign

for SCS being non-empty Circuit of IIG

for b

( b

b

theorem :: CIRCUIT1:1

for IIG being non empty non void Circuit-like ManySortedSign

for SCS being non-empty Circuit of IIG

for v being Vertex of IIG

for e being Element of the Sorts of SCS . v st v in SortsWithConstants IIG & e in Constants (SCS,v) holds

(Set-Constants SCS) . v = e

for SCS being non-empty Circuit of IIG

for v being Vertex of IIG

for e being Element of the Sorts of SCS . v st v in SortsWithConstants IIG & e in Constants (SCS,v) holds

(Set-Constants SCS) . v = e

proof end;

definition

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

let CS be Circuit of IIG;

mode InputFuncs of CS is ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of CS | (InputVertices IIG);

end;
let CS be Circuit of IIG;

mode InputFuncs of CS is ManySortedFunction of (InputVertices IIG) --> NAT, the Sorts of CS | (InputVertices IIG);

theorem Th2: :: CIRCUIT1:2

for IIG being non empty non void Circuit-like ManySortedSign

for SCS being non-empty Circuit of IIG

for InpFs being InputFuncs of SCS

for n being Element of NAT st IIG is with_input_V holds

(commute InpFs) . n is InputValues of SCS

for SCS being non-empty Circuit of IIG

for InpFs being InputFuncs of SCS

for n being Element of NAT st IIG is with_input_V holds

(commute InpFs) . n is InputValues of SCS

proof end;

definition

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

assume A1: IIG is with_input_V ;

let SCS be non-empty Circuit of IIG;

let InpFs be InputFuncs of SCS;

let n be Element of NAT ;

coherence

(commute InpFs) . n is InputValues of SCS by A1, Th2;

correctness

;

end;
assume A1: IIG is with_input_V ;

let SCS be non-empty Circuit of IIG;

let InpFs be InputFuncs of SCS;

let n be Element of NAT ;

coherence

(commute InpFs) . n is InputValues of SCS by A1, Th2;

correctness

;

:: deftheorem defines -th_InputValues CIRCUIT1:def 2 :

for IIG being non empty non void Circuit-like ManySortedSign st IIG is with_input_V holds

for SCS being non-empty Circuit of IIG

for InpFs being InputFuncs of SCS

for n being Element of NAT holds n -th_InputValues InpFs = (commute InpFs) . n;

for IIG being non empty non void Circuit-like ManySortedSign st IIG is with_input_V holds

for SCS being non-empty Circuit of IIG

for InpFs being InputFuncs of SCS

for n being Element of NAT holds n -th_InputValues InpFs = (commute InpFs) . n;

definition

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

let SCS be Circuit of IIG;

mode State of SCS is Element of product the Sorts of SCS;

end;
let SCS be Circuit of IIG;

mode State of SCS is Element of product the Sorts of SCS;

theorem :: CIRCUIT1:3

for IIG being non empty non void Circuit-like ManySortedSign

for SCS being non-empty Circuit of IIG

for s being State of SCS holds dom s = the carrier of IIG by PARTFUN1:def 2;

for SCS being non-empty Circuit of IIG

for s being State of SCS holds dom s = the carrier of IIG by PARTFUN1:def 2;

theorem :: CIRCUIT1:4

for IIG being non empty non void Circuit-like ManySortedSign

for SCS being non-empty Circuit of IIG

for s being State of SCS

for v being Vertex of IIG holds s . v in the Sorts of SCS . v

for SCS being non-empty Circuit of IIG

for s being State of SCS

for v being Vertex of IIG holds s . v in the Sorts of SCS . v

proof end;

definition

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

let SCS be non-empty Circuit of IIG;

let s be State of SCS;

let o be OperSymbol of IIG;

coherence

s * (the_arity_of o) is Element of Args (o,SCS)

;

end;
let SCS be non-empty Circuit of IIG;

let s be State of SCS;

let o be OperSymbol of IIG;

coherence

s * (the_arity_of o) is Element of Args (o,SCS)

proof end;

correctness ;

:: deftheorem defines depends_on_in CIRCUIT1:def 3 :

for IIG being non empty non void Circuit-like ManySortedSign

for SCS being non-empty Circuit of IIG

for s being State of SCS

for o being OperSymbol of IIG holds o depends_on_in s = s * (the_arity_of o);

for IIG being non empty non void Circuit-like ManySortedSign

for SCS being non-empty Circuit of IIG

for s being State of SCS

for o being OperSymbol of IIG holds o depends_on_in s = s * (the_arity_of o);

theorem Th5: :: CIRCUIT1:5

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for SCS being non-empty finite-yielding MSAlgebra over IIG

for v, w being Vertex of IIG

for e1 being Element of the Sorts of (FreeEnv SCS) . v

for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds

for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds

w = (the_arity_of (action_at v)) /. k

for SCS being non-empty finite-yielding MSAlgebra over IIG

for v, w being Vertex of IIG

for e1 being Element of the Sorts of (FreeEnv SCS) . v

for q1 being DTree-yielding FinSequence st v in InnerVertices IIG & e1 = [(action_at v), the carrier of IIG] -tree q1 holds

for k being Element of NAT st k in dom q1 & q1 . k in the Sorts of (FreeEnv SCS) . w holds

w = (the_arity_of (action_at v)) /. k

proof end;

registration

let IIG be non empty non void Circuit-like monotonic ManySortedSign ;

let SCS be non-empty finite-yielding MSAlgebra over IIG;

let v be Vertex of IIG;

for b_{1} being Element of the Sorts of (FreeEnv SCS) . v holds

( b_{1} is finite & not b_{1} is empty & b_{1} is Function-like & b_{1} is Relation-like )
;

end;
let SCS be non-empty finite-yielding MSAlgebra over IIG;

let v be Vertex of IIG;

cluster -> Relation-like Function-like non empty finite for Element of the Sorts of (FreeEnv SCS) . v;

coherence for b

( b

registration

let IIG be non empty non void Circuit-like monotonic ManySortedSign ;

let SCS be non-empty finite-yielding MSAlgebra over IIG;

let v be Vertex of IIG;

coherence

for b_{1} being Element of the Sorts of (FreeEnv SCS) . v holds b_{1} is DecoratedTree-like
;

end;
let SCS be non-empty finite-yielding MSAlgebra over IIG;

let v be Vertex of IIG;

coherence

for b

theorem Th6: :: CIRCUIT1:6

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for SCS being non-empty finite-yielding MSAlgebra over IIG

for v, w being Vertex of IIG

for e1 being Element of the Sorts of (FreeEnv SCS) . v

for e2 being Element of the Sorts of (FreeEnv SCS) . w

for q1 being DTree-yielding FinSequence

for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds

e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v

for SCS being non-empty finite-yielding MSAlgebra over IIG

for v, w being Vertex of IIG

for e1 being Element of the Sorts of (FreeEnv SCS) . v

for e2 being Element of the Sorts of (FreeEnv SCS) . w

for q1 being DTree-yielding FinSequence

for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds

e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v

proof end;

theorem Th7: :: CIRCUIT1:7

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty finite-yielding MSAlgebra over IIG

for v being Element of IIG

for e being Element of the Sorts of (FreeEnv A) . v st 1 < card e holds

ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]

for A being non-empty finite-yielding MSAlgebra over IIG

for v being Element of IIG

for e being Element of the Sorts of (FreeEnv A) . v st 1 < card e holds

ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]

proof end;

theorem :: CIRCUIT1:8

for IIG being non empty non void Circuit-like ManySortedSign

for SCS being non-empty Circuit of IIG

for s being State of SCS

for o being OperSymbol of IIG holds (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o)

for SCS being non-empty Circuit of IIG

for s being State of SCS

for o being OperSymbol of IIG holds (Den (o,SCS)) . (o depends_on_in s) in the Sorts of SCS . (the_result_sort_of o)

proof end;

theorem Th9: :: CIRCUIT1:9

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty Circuit of IIG

for v being Vertex of IIG

for e being Element of the Sorts of (FreeEnv A) . v st e . {} = [(action_at v), the carrier of IIG] holds

ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p

for A being non-empty Circuit of IIG

for v being Vertex of IIG

for e being Element of the Sorts of (FreeEnv A) . v st e . {} = [(action_at v), the carrier of IIG] holds

ex p being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree p

proof end;

begin

registration

let IIG be non empty non void monotonic ManySortedSign ;

let A be non-empty finite-yielding MSAlgebra over IIG;

let v be SortSymbol of IIG;

coherence

the Sorts of (FreeEnv A) . v is finite

end;
let A be non-empty finite-yielding MSAlgebra over IIG;

let v be SortSymbol of IIG;

coherence

the Sorts of (FreeEnv A) . v is finite

proof end;

defpred S

definition

let IIG be non empty non void Circuit-like monotonic ManySortedSign ;

let A be non-empty finite-yielding MSAlgebra over IIG;

let v be SortSymbol of IIG;

ex b_{1} being Nat ex s being non empty finite Subset of NAT st

( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b_{1} = max s )

uniqueness

for b_{1}, b_{2} being Nat st ex s being non empty finite Subset of NAT st

( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b_{1} = max s ) & ex s being non empty finite Subset of NAT st

( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b_{2} = max s ) holds

b_{1} = b_{2};

;

end;
let A be non-empty finite-yielding MSAlgebra over IIG;

let v be SortSymbol of IIG;

func size (v,A) -> Nat means :Def4: :: CIRCUIT1:def 4

ex s being non empty finite Subset of NAT st

( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & it = max s );

existence ex s being non empty finite Subset of NAT st

( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & it = max s );

ex b

( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b

proof end;

correctness uniqueness

for b

( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b

( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b

b

;

:: deftheorem Def4 defines size CIRCUIT1:def 4 :

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty finite-yielding MSAlgebra over IIG

for v being SortSymbol of IIG

for b_{4} being Nat holds

( b_{4} = size (v,A) iff ex s being non empty finite Subset of NAT st

( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b_{4} = max s ) );

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty finite-yielding MSAlgebra over IIG

for v being SortSymbol of IIG

for b

( b

( s = { (card t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b

theorem Th10: :: CIRCUIT1:10

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty finite-yielding MSAlgebra over IIG

for v being Element of IIG holds

( size (v,A) = 1 iff v in (InputVertices IIG) \/ (SortsWithConstants IIG) )

for A being non-empty finite-yielding MSAlgebra over IIG

for v being Element of IIG holds

( size (v,A) = 1 iff v in (InputVertices IIG) \/ (SortsWithConstants IIG) )

proof end;

theorem :: CIRCUIT1:11

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for SCS being non-empty finite-yielding MSAlgebra over IIG

for v, w being Vertex of IIG

for e1 being Element of the Sorts of (FreeEnv SCS) . v

for e2 being Element of the Sorts of (FreeEnv SCS) . w

for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds

card e2 = size (w,SCS)

for SCS being non-empty finite-yielding MSAlgebra over IIG

for v, w being Vertex of IIG

for e1 being Element of the Sorts of (FreeEnv SCS) . v

for e2 being Element of the Sorts of (FreeEnv SCS) . w

for q1 being DTree-yielding FinSequence st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e1 = size (v,SCS) & e1 = [(action_at v), the carrier of IIG] -tree q1 & e2 in rng q1 holds

card e2 = size (w,SCS)

proof end;

theorem Th12: :: CIRCUIT1:12

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty finite-yielding MSAlgebra over IIG

for v being Vertex of IIG

for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds

ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q

for A being non-empty finite-yielding MSAlgebra over IIG

for v being Vertex of IIG

for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds

ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q

proof end;

theorem :: CIRCUIT1:13

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty finite-yielding MSAlgebra over IIG

for v being Vertex of IIG

for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds

ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]

for A being non-empty finite-yielding MSAlgebra over IIG

for v being Vertex of IIG

for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size (v,A) holds

ex o being OperSymbol of IIG st e . {} = [o, the carrier of IIG]

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be non-empty finite-yielding MSAlgebra over S;

let v be SortSymbol of S;

let e be Element of the Sorts of (FreeEnv A) . v;

ex b_{1} being Element of NAT ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st

( e = e9 & b_{1} = depth e9 )

uniqueness

for b_{1}, b_{2} being Element of NAT st ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st

( e = e9 & b_{1} = depth e9 ) & ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st

( e = e9 & b_{2} = depth e9 ) holds

b_{1} = b_{2};

;

end;
let A be non-empty finite-yielding MSAlgebra over S;

let v be SortSymbol of S;

let e be Element of the Sorts of (FreeEnv A) . v;

func depth e -> Element of NAT means :Def5: :: CIRCUIT1:def 5

ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st

( e = e9 & it = depth e9 );

existence ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st

( e = e9 & it = depth e9 );

ex b

( e = e9 & b

proof end;

correctness uniqueness

for b

( e = e9 & b

( e = e9 & b

b

;

:: deftheorem Def5 defines depth CIRCUIT1:def 5 :

for S being non empty non void ManySortedSign

for A being non-empty finite-yielding MSAlgebra over S

for v being SortSymbol of S

for e being Element of the Sorts of (FreeEnv A) . v

for b_{5} being Element of NAT holds

( b_{5} = depth e iff ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st

( e = e9 & b_{5} = depth e9 ) );

for S being non empty non void ManySortedSign

for A being non-empty finite-yielding MSAlgebra over S

for v being SortSymbol of S

for e being Element of the Sorts of (FreeEnv A) . v

for b

( b

( e = e9 & b

theorem Th14: :: CIRCUIT1:14

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty finite-yielding MSAlgebra over IIG

for v, w being Element of IIG st v in InnerVertices IIG & w in rng (the_arity_of (action_at v)) holds

size (w,A) < size (v,A)

for A being non-empty finite-yielding MSAlgebra over IIG

for v, w being Element of IIG st v in InnerVertices IIG & w in rng (the_arity_of (action_at v)) holds

size (w,A) < size (v,A)

proof end;

theorem Th15: :: CIRCUIT1:15

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty finite-yielding MSAlgebra over IIG

for v being SortSymbol of IIG holds size (v,A) > 0

for A being non-empty finite-yielding MSAlgebra over IIG

for v being SortSymbol of IIG holds size (v,A) > 0

proof end;

theorem :: CIRCUIT1:16

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty Circuit of IIG

for v being Vertex of IIG

for e being Element of the Sorts of (FreeEnv A) . v

for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds

ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st

( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds

card e = size (v,A)

for A being non-empty Circuit of IIG

for v being Vertex of IIG

for e being Element of the Sorts of (FreeEnv A) . v

for p being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v), the carrier of IIG] -tree p & ( for k being Element of NAT st k in dom p holds

ex ek being Element of the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) st

( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),A) ) ) holds

card e = size (v,A)

proof end;

begin

definition

let S be non empty non void monotonic ManySortedSign ;

let A be non-empty finite-yielding MSAlgebra over S;

let v be SortSymbol of S;

ex b_{1} being Nat ex s being non empty finite Subset of NAT st

( s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b_{1} = max s )

uniqueness

for b_{1}, b_{2} being Nat st ex s being non empty finite Subset of NAT st

( s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b_{1} = max s ) & ex s being non empty finite Subset of NAT st

( s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b_{2} = max s ) holds

b_{1} = b_{2};

;

end;
let A be non-empty finite-yielding MSAlgebra over S;

let v be SortSymbol of S;

func depth (v,A) -> Nat means :Def6: :: CIRCUIT1:def 6

ex s being non empty finite Subset of NAT st

( s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & it = max s );

existence ex s being non empty finite Subset of NAT st

( s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & it = max s );

ex b

( s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b

proof end;

correctness uniqueness

for b

( s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b

( s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b

b

;

:: deftheorem Def6 defines depth CIRCUIT1:def 6 :

for S being non empty non void monotonic ManySortedSign

for A being non-empty finite-yielding MSAlgebra over S

for v being SortSymbol of S

for b_{4} being Nat holds

( b_{4} = depth (v,A) iff ex s being non empty finite Subset of NAT st

( s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b_{4} = max s ) );

for S being non empty non void monotonic ManySortedSign

for A being non-empty finite-yielding MSAlgebra over S

for v being SortSymbol of S

for b

( b

( s = { (depth t) where t is Element of the Sorts of (FreeEnv A) . v : verum } & b

definition

let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ;

let A be non-empty Circuit of IIG;

ex b_{1} being Nat ex Ds being non empty finite Subset of NAT st

( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & b_{1} = max Ds )

for b_{1}, b_{2} being Nat st ex Ds being non empty finite Subset of NAT st

( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & b_{1} = max Ds ) & ex Ds being non empty finite Subset of NAT st

( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & b_{2} = max Ds ) holds

b_{1} = b_{2}
;

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

func depth A -> Nat means :Def7: :: CIRCUIT1:def 7

ex Ds being non empty finite Subset of NAT st

( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & it = max Ds );

existence ex Ds being non empty finite Subset of NAT st

( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & it = max Ds );

ex b

( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & b

proof end;

uniqueness for b

( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & b

( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & b

b

:: deftheorem Def7 defines depth CIRCUIT1:def 7 :

for IIG being non empty finite non void Circuit-like monotonic ManySortedSign

for A being non-empty Circuit of IIG

for b_{3} being Nat holds

( b_{3} = depth A iff ex Ds being non empty finite Subset of NAT st

( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & b_{3} = max Ds ) );

for IIG being non empty finite non void Circuit-like monotonic ManySortedSign

for A being non-empty Circuit of IIG

for b

( b

( Ds = { (depth (v,A)) where v is Element of IIG : v in the carrier of IIG } & b

theorem :: CIRCUIT1:17

for IIG being non empty finite non void Circuit-like monotonic ManySortedSign

for A being non-empty Circuit of IIG

for v being Vertex of IIG holds depth (v,A) <= depth A

for A being non-empty Circuit of IIG

for v being Vertex of IIG holds depth (v,A) <= depth A

proof end;

theorem Th18: :: CIRCUIT1:18

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty Circuit of IIG

for v being Vertex of IIG holds

( depth (v,A) = 0 iff ( v in InputVertices IIG or v in SortsWithConstants IIG ) )

for A being non-empty Circuit of IIG

for v being Vertex of IIG holds

( depth (v,A) = 0 iff ( v in InputVertices IIG or v in SortsWithConstants IIG ) )

proof end;

theorem :: CIRCUIT1:19

for IIG being non empty non void Circuit-like monotonic ManySortedSign

for A being non-empty finite-yielding MSAlgebra over IIG

for v, v1 being SortSymbol of IIG st v in InnerVertices IIG & v1 in rng (the_arity_of (action_at v)) holds

depth (v1,A) < depth (v,A)

for A being non-empty finite-yielding MSAlgebra over IIG

for v, v1 being SortSymbol of IIG st v in InnerVertices IIG & v1 in rng (the_arity_of (action_at v)) holds

depth (v1,A) < depth (v,A)

proof end;

:: Circuits

::---------------------------------------------------------------------------