:: Introduction to Circuits, I
:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received December 15, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users


::---------------------------------------------------------------------------
:: Circuits
::---------------------------------------------------------------------------
definition
let S be non empty non void Circuit-like ManySortedSign ;
mode Circuit of S is finite-yielding MSAlgebra over S;
end;

definition
let IIG be non empty non void Circuit-like ManySortedSign ;
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
ex b1 being ManySortedSet of SortsWithConstants IIG st
for x being Vertex of IIG st x in dom b1 holds
b1 . x in Constants (SCS,x)
proof end;
correctness
uniqueness
for b1, b2 being ManySortedSet of SortsWithConstants IIG st ( for x being Vertex of IIG st x in dom b1 holds
b1 . x in Constants (SCS,x) ) & ( for x being Vertex of IIG st x in dom b2 holds
b2 . x in Constants (SCS,x) ) holds
b1 = b2;
proof end;
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 b3 being ManySortedSet of SortsWithConstants IIG holds
( b3 = Set-Constants SCS iff for x being Vertex of IIG st x in dom b3 holds
b3 . x in Constants (SCS,x) );

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

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 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 Nat;
func n -th_InputValues InpFs -> InputValues of SCS equals :: CIRCUIT1:def 2
(commute InpFs) . n;
coherence
(commute InpFs) . n is InputValues of SCS by A1, Th2;
correctness
;
end;

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

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;

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
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;
func o depends_on_in s -> Element of Args (o,SCS) equals :: CIRCUIT1:def 3
s * (the_arity_of o);
coherence
s * (the_arity_of o) is Element of Args (o,SCS)
proof end;
correctness
;
end;

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

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
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;
cluster -> Relation-like Function-like non empty finite for Element of the Sorts of (FreeEnv SCS) . v;
coherence
for b1 being Element of the Sorts of (FreeEnv SCS) . v holds
( b1 is finite & not b1 is empty & b1 is Function-like & b1 is Relation-like ) ;
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;
cluster -> DecoratedTree-like for Element of the Sorts of (FreeEnv SCS) . v;
coherence
for b1 being Element of the Sorts of (FreeEnv SCS) . v holds b1 is DecoratedTree-like ;
end;

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

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;
cluster the Sorts of (FreeEnv A) . v -> finite ;
coherence
the Sorts of (FreeEnv A) . v is finite
proof end;
end;

defpred S1[ set ] means verum;

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;
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 b1 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 } & b1 = max s )
proof end;
correctness
uniqueness
for b1, b2 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 } & b1 = 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 } & b2 = max s ) holds
b1 = b2;
;
end;

:: 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 b4 being Nat holds
( b4 = 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 } & b4 = max s ) );

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) )
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)
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
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]
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;
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 b1 being Element of NAT ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e9 & b1 = depth e9 )
proof end;
correctness
uniqueness
for b1, b2 being Element of NAT st ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e9 & b1 = depth e9 ) & ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e9 & b2 = depth e9 ) holds
b1 = b2;
;
end;

:: 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 b5 being Element of NAT holds
( b5 = depth e iff ex e9 being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e9 & b5 = depth e9 ) );

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

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;
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 b1 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 } & b1 = max s )
proof end;
correctness
uniqueness
for b1, b2 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 } & b1 = 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 } & b2 = max s ) holds
b1 = b2;
;
end;

:: 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 b4 being Nat holds
( b4 = 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 } & b4 = max s ) );

definition
let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ;
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 b1 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 } & b1 = max Ds )
proof end;
uniqueness
for b1, b2 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 } & b1 = 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 } & b2 = max Ds ) holds
b1 = b2 ;
end;

:: 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 b3 being Nat holds
( b3 = 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 } & b3 = max Ds ) );

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