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

Lm1: for x being set holds not x in x
;

theorem Th1: :: CIRCUIT2: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 monotonic ManySortedSign
for X being V3 ManySortedSet of the carrier of IIG
for H being ManySortedFunction of (FreeMSA X),(FreeMSA X)
for HH being Function-yielding Function
for v being SortSymbol of IIG
for p being DTree-yielding FinSequence
for t being Element of the Sorts of (FreeMSA X) . v st v in InnerVertices IIG & t = [(action_at v),the carrier of IIG] -tree p & H is_homomorphism FreeMSA X, FreeMSA X & HH = H * (the_arity_of (action_at v)) holds
ex HHp being DTree-yielding FinSequence st
( HHp = HH .. p & (H . v) . t = [(action_at v),the carrier of IIG] -tree HHp )
proof end;

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let s be State of SCS;
let iv be InputValues of SCS;
:: original: +*
redefine func s +* iv -> State of SCS;
coherence
s +* iv is State of SCS
proof end;
end;

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let A be non-empty Circuit of IIG;
let iv be InputValues of A;
func Fix_inp iv -> ManySortedFunction of FreeGen the Sorts of A,the Sorts of (FreeEnv A) means :Def1: :: CIRCUIT2:def 1
for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it . v = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies it . v = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies it . v = id (FreeGen v,the Sorts of A) ) );
existence
ex b1 being ManySortedFunction of FreeGen the Sorts of A,the Sorts of (FreeEnv A) st
for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b1 . v = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b1 . v = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b1 . v = id (FreeGen v,the Sorts of A) ) )
proof end;
uniqueness
for b1, b2 being ManySortedFunction of FreeGen the Sorts of A,the Sorts of (FreeEnv A) st ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b1 . v = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b1 . v = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b1 . v = id (FreeGen v,the Sorts of A) ) ) ) & ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b2 . v = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b2 . v = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b2 . v = id (FreeGen v,the Sorts of A) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Fix_inp CIRCUIT2:def 1 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for iv being InputValues of A
for b4 being ManySortedFunction of FreeGen the Sorts of A,the Sorts of (FreeEnv A) holds
( b4 = Fix_inp iv iff for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b4 . v = (FreeGen v,the Sorts of A) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b4 . v = (FreeGen v,the Sorts of A) --> (root-tree [(action_at v),the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b4 . v = id (FreeGen v,the Sorts of A) ) ) );

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let A be non-empty Circuit of IIG;
let iv be InputValues of A;
func Fix_inp_ext iv -> ManySortedFunction of (FreeEnv A),(FreeEnv A) means :Def2: :: CIRCUIT2:def 2
( it is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= it );
existence
ex b1 being ManySortedFunction of (FreeEnv A),(FreeEnv A) st
( b1 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b1 )
proof end;
uniqueness
for b1, b2 being ManySortedFunction of (FreeEnv A),(FreeEnv A) st b1 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b1 & b2 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Fix_inp_ext CIRCUIT2:def 2 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for A being non-empty Circuit of IIG
for iv being InputValues of A
for b4 being ManySortedFunction of (FreeEnv A),(FreeEnv A) holds
( b4 = Fix_inp_ext iv iff ( b4 is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b4 ) );

theorem Th2: :: CIRCUIT2: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 monotonic ManySortedSign
for A being non-empty Circuit of IIG
for iv being InputValues of A
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds
((Fix_inp_ext iv) . v) . e = e
proof end;

theorem Th3: :: CIRCUIT2:3  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 iv being InputValues of A
for v being Vertex of IIG
for x being Element of the Sorts of A . v st v in InputVertices IIG holds
((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
proof end;

theorem Th4: :: CIRCUIT2: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 monotonic ManySortedSign
for A being non-empty Circuit of IIG
for iv being InputValues of A
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v),the carrier of IIG] -tree p & dom p = dom q & ( for k being Nat st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v),the carrier of IIG] -tree q
proof end;

theorem Th5: :: CIRCUIT2: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 monotonic ManySortedSign
for A being non-empty Circuit of IIG
for iv being InputValues of A
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v),the carrier of IIG]
proof end;

theorem Th6: :: CIRCUIT2: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 A being non-empty Circuit of IIG
for iv being InputValues of A
for v being Vertex of IIG
for e, e1 being Element of the Sorts of (FreeEnv A) . v
for t, t1 being DecoratedTree st t = e & t1 = e1 & e1 = ((Fix_inp_ext iv) . v) . e holds
dom t = dom t1
proof end;

theorem Th7: :: CIRCUIT2: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 A being non-empty Circuit of IIG
for iv being InputValues of A
for v being Vertex of IIG
for e, e1 being Element of the Sorts of (FreeEnv A) . v st e1 = ((Fix_inp_ext iv) . v) . e holds
card e = card e1
proof end;

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let v be Vertex of IIG;
let iv be InputValues of SCS;
A1: FreeEnv SCS = FreeMSA the Sorts of SCS by MSAFREE2:def 8;
func IGTree v,iv -> Element of the Sorts of (FreeEnv SCS) . v means :Def3: :: CIRCUIT2:def 3
 ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size v,SCS & it = ((Fix_inp_ext iv) . v) . e );
existence
ex b1, e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size v,SCS & b1 = ((Fix_inp_ext iv) . v) . e )
proof end;
uniqueness
for b1, b2 being Element of the Sorts of (FreeEnv SCS) . v st ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size v,SCS & b1 = ((Fix_inp_ext iv) . v) . e ) & ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size v,SCS & b2 = ((Fix_inp_ext iv) . v) . e ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines IGTree CIRCUIT2:def 3 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for iv being InputValues of SCS
for b5 being Element of the Sorts of (FreeEnv SCS) . v holds
( b5 = IGTree v,iv iff ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size v,SCS & b5 = ((Fix_inp_ext iv) . v) . e ) );

theorem Th8: :: CIRCUIT2: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 SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for iv being InputValues of SCS holds IGTree v,iv = ((Fix_inp_ext iv) . v) . (IGTree v,iv)
proof end;

theorem Th9: :: CIRCUIT2: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 monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for iv being InputValues of SCS
for p being DTree-yielding FinSequence st v in InnerVertices IIG & dom p = dom (the_arity_of (action_at v)) & ( for k being Nat st k in dom p holds
p . k = IGTree ((the_arity_of (action_at v)) /. k),iv ) holds
IGTree v,iv = [(action_at v),the carrier of IIG] -tree p
proof end;

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let v be Vertex of IIG;
let iv be InputValues of SCS;
func IGValue v,iv -> Element of the Sorts of SCS . v equals :: CIRCUIT2:def 4
((Eval SCS) . v) . (IGTree v,iv);
coherence
((Eval SCS) . v) . (IGTree v,iv) is Element of the Sorts of SCS . v ;
end;

:: deftheorem defines IGValue CIRCUIT2:def 4 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for iv being InputValues of SCS holds IGValue v,iv = ((Eval SCS) . v) . (IGTree v,iv);

theorem Th10: :: CIRCUIT2: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 SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for iv being InputValues of SCS st v in InputVertices IIG holds
IGValue v,iv = iv . v
proof end;

theorem Th11: :: CIRCUIT2: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 SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for iv being InputValues of SCS st v in SortsWithConstants IIG holds
IGValue v,iv = (Set-Constants 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;
func Following s -> State of SCS means :Def5: :: CIRCUIT2:def 5
for v being Vertex of IIG holds
( ( v in InputVertices IIG implies it . v = s . v ) & ( v in InnerVertices IIG implies it . v = (Den (action_at v),SCS) . ((action_at v) depends_on_in s) ) );
existence
ex b1 being State of SCS st
for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b1 . v = s . v ) & ( v in InnerVertices IIG implies b1 . v = (Den (action_at v),SCS) . ((action_at v) depends_on_in s) ) )
proof end;
uniqueness
for b1, b2 being State of SCS st ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b1 . v = s . v ) & ( v in InnerVertices IIG implies b1 . v = (Den (action_at v),SCS) . ((action_at v) depends_on_in s) ) ) ) & ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b2 . v = s . v ) & ( v in InnerVertices IIG implies b2 . v = (Den (action_at v),SCS) . ((action_at v) depends_on_in s) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Following CIRCUIT2:def 5 :
for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for s, b4 being State of SCS holds
( b4 = Following s iff for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b4 . v = s . v ) & ( v in InnerVertices IIG implies b4 . v = (Den (action_at v),SCS) . ((action_at v) depends_on_in s) ) ) );

theorem Th12: :: CIRCUIT2: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 Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS st iv c= s holds
iv c= Following s
proof end;

definition
let IIG be non empty non void Circuit-like ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let IT be State of SCS;
attr IT is stable means :Def6: :: CIRCUIT2:def 6
IT = Following IT;
end;

:: deftheorem Def6 defines stable CIRCUIT2:def 6 :
for IIG being non empty non void Circuit-like ManySortedSign
for SCS being non-empty Circuit of IIG
for IT being State of SCS holds
( IT is stable iff IT = Following IT );

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let s be State of SCS;
let iv be InputValues of SCS;
func Following s,iv -> State of SCS equals :: CIRCUIT2:def 7
 Following (s +* iv);
coherence
Following (s +* iv) is State of SCS ;
end;

:: deftheorem defines Following CIRCUIT2:def 7 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS holds Following s,iv = Following (s +* iv);

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let InpFs be InputFuncs of SCS;
let s be State of SCS;
func InitialComp s,InpFs -> State of SCS equals :: CIRCUIT2:def 8
(s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS);
coherence
(s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) is State of SCS
proof end;
end;

:: deftheorem defines InitialComp CIRCUIT2:def 8 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for s being State of SCS holds InitialComp s,InpFs = (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS);

definition
let IIG be non empty non void Circuit-like monotonic ManySortedSign ;
let SCS be non-empty Circuit of IIG;
let InpFs be InputFuncs of SCS;
let s be State of SCS;
func Computation s,InpFs -> Function of NAT , product the Sorts of SCS means :Def9: :: CIRCUIT2:def 9
( it . 0 = InitialComp s,InpFs & ( for i being Nat holds it . (i + 1) = Following (it . i),((i + 1) -th_InputValues InpFs) ) );
correctness
existence
ex b1 being Function of NAT , product the Sorts of SCS st
( b1 . 0 = InitialComp s,InpFs & ( for i being Nat holds b1 . (i + 1) = Following (b1 . i),((i + 1) -th_InputValues InpFs) ) );
uniqueness
for b1, b2 being Function of NAT , product the Sorts of SCS st b1 . 0 = InitialComp s,InpFs & ( for i being Nat holds b1 . (i + 1) = Following (b1 . i),((i + 1) -th_InputValues InpFs) ) & b2 . 0 = InitialComp s,InpFs & ( for i being Nat holds b2 . (i + 1) = Following (b2 . i),((i + 1) -th_InputValues InpFs) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def9 defines Computation CIRCUIT2:def 9 :
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for s being State of SCS
for b5 being Function of NAT , product the Sorts of SCS holds
( b5 = Computation s,InpFs iff ( b5 . 0 = InitialComp s,InpFs & ( for i being Nat holds b5 . (i + 1) = Following (b5 . i),((i + 1) -th_InputValues InpFs) ) ) );

theorem Th13: :: CIRCUIT2: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 SCS being non-empty Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS
for k being Nat st ( for v being Vertex of IIG st depth v,SCS <= k holds
s . v = IGValue v,iv ) holds
for v1 being Vertex of IIG st depth v1,SCS <= k + 1 holds
(Following s) . v1 = IGValue v1,iv
proof end;

theorem Th14: :: CIRCUIT2: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 finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Nat holds iv c= (Computation s,InpFs) . k
proof end;

theorem :: CIRCUIT2: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 finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for s being State of SCS
for n being Nat st commute InpFs is constant & not InputVertices IIG is empty & (Computation s,InpFs) . n is stable holds
for m being Nat st n <= m holds
(Computation s,InpFs) . n = (Computation s,InpFs) . m
proof end;

theorem Th16: :: CIRCUIT2: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 finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Nat
for v being Vertex of IIG st depth v,SCS <= k holds
((Computation s,InpFs) . k) . v = IGValue v,iv
proof end;

theorem Th17: :: CIRCUIT2: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 finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS
for iv being InputValues of SCS st commute InpFs is constant & not InputVertices IIG is empty & iv = (commute InpFs) . 0 holds
for s being State of SCS
for v being Vertex of IIG
for n being Element of NAT st n = depth SCS holds
((Computation s,InpFs) . n) . v = IGValue v,iv
proof end;

theorem :: CIRCUIT2: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 SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for n being Element of NAT st n = depth SCS holds
(Computation s,InpFs) . n is stable
proof end;

theorem :: CIRCUIT2: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 finite non void Circuit-like monotonic ManySortedSign
for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s1, s2 being State of SCS holds (Computation s1,InpFs) . (depth SCS) = (Computation s2,InpFs) . (depth SCS)
proof end;