:: CIRCUIT1 semantic presentation

definition

let S be non empty non void Circuit-like ManySortedSign ;
mode Circuit of S is locally-finite MSAlgebra of 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

proof end;

correctness

proof end;

end;

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

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 by A1, Th2;
correctness ;

end;

:: deftheorem defines -th_InputValues CIRCUIT1:def 2 :

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

canceled;

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 holds dom s = the carrier of IIG

proof end;

theorem :: CIRCUIT1:5

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

proof end;

correctness ;

end;

:: deftheorem defines depends_on_in CIRCUIT1:def 3 :

theorem Th6: :: CIRCUIT1:6

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty locally-finite MSAlgebra of 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 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 locally-finite MSAlgebra of IIG;
let v be Vertex of IIG;
cluster -> non empty Relation-like Function-like finite Element of the Sorts of (FreeEnv SCS) . v;
coherence

proof end;

end;

registration

let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty locally-finite MSAlgebra of IIG;
let v be Vertex of IIG;
cluster -> non empty Relation-like Function-like finite DecoratedTree-like Element of the Sorts of (FreeEnv SCS) . v;
coherence

proof end;

end;

theorem Th7: :: CIRCUIT1:7

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty locally-finite MSAlgebra of 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 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 Th8: :: CIRCUIT1:8

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty locally-finite MSAlgebra of 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:9

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 Th10: :: CIRCUIT1:10

proof end;

registration

let IIG be non empty non void monotonic ManySortedSign ;
let A be non-empty locally-finite MSAlgebra of IIG;
let v be SortSymbol of IIG;
cluster the Sorts of (FreeEnv A) . v -> finite ;
coherence

proof end;

end;

defpred S₁[ set ] means verum;

definition

let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let A be non-empty locally-finite MSAlgebra of IIG;
let v be SortSymbol of IIG;
func size v,A -> natural number 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

proof end;

correctness ;

end;

:: deftheorem Def4 defines size CIRCUIT1:def 4 :

theorem Th11: :: CIRCUIT1:11

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty locally-finite MSAlgebra of IIG
for v being Element of IIG holds
( size v,A = 1 iff v in (InputVertices IIG) \/ (SortsWithConstants IIG) )

proof end;

theorem :: CIRCUIT1:12

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty locally-finite MSAlgebra of 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 Th13: :: CIRCUIT1:13

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty locally-finite MSAlgebra of 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:14

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty locally-finite MSAlgebra of 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 locally-finite MSAlgebra of S;
let v be SortSymbol of S;
let e be Element of the Sorts of (FreeEnv A) . v;
func depth e -> Nat means :Def5: :: CIRCUIT1:def 5
ex e' being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e' & it = depth e' );
existence

proof end;

correctness ;

end;

:: deftheorem Def5 defines depth CIRCUIT1:def 5 :

theorem Th15: :: CIRCUIT1:15

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty locally-finite MSAlgebra of 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 Th16: :: CIRCUIT1:16

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty locally-finite MSAlgebra of IIG
for v being SortSymbol of IIG holds size v,A > 0

proof end;

theorem :: CIRCUIT1:17

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 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 locally-finite MSAlgebra of S;
let v be SortSymbol of S;
func depth v,A -> natural number 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

proof end;

correctness ;

end;

:: deftheorem Def6 defines depth CIRCUIT1:def 6 :

definition

let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ;
let A be non-empty Circuit of IIG;
func depth A -> natural number 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

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines depth CIRCUIT1:def 7 :

theorem :: CIRCUIT1:18

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 Th19: :: CIRCUIT1:19

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

for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty locally-finite MSAlgebra of 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;