:: CIRCUIT1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CIRCUIT1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th6: :: CIRCUIT1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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 )
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
for b1 being Element of the Sorts of (FreeEnv SCS) . v holds b1 is DecoratedTree-like
proof end;
end;

theorem Th7: :: CIRCUIT1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 locally-finite MSAlgebra of 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 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
ex b1 being natural number 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 natural number 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 locally-finite MSAlgebra of IIG
for v being SortSymbol of IIG
for b4 being natural number 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 Th11: :: CIRCUIT1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being Nat ex e' being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e' & b1 = depth e' )
proof end;
correctness
uniqueness
for b1, b2 being Nat st ex e' being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e' & b1 = depth e' ) & ex e' being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e' & b2 = depth e' ) holds
b1 = b2
;
;
end;

:: deftheorem Def5 defines depth CIRCUIT1:def 5 :
for S being non empty non void ManySortedSign
for A being non-empty locally-finite MSAlgebra of S
for v being SortSymbol of S
for e being Element of the Sorts of (FreeEnv A) . v
for b5 being Nat holds
( b5 = depth e iff ex e' being Element of the Sorts of (FreeMSA the Sorts of A) . v st
( e = e' & b5 = depth e' ) );

theorem Th15: :: CIRCUIT1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being natural number 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 natural number 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 locally-finite MSAlgebra of S
for v being SortSymbol of S
for b4 being natural number 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 -> 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
ex b1 being natural number 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 natural number 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 natural number 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:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;