:: Introduction to Circuits, II
:: by Yatsuka Nakamura, Piotr Rudnicki, Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received April 10, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


begin

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

theorem Th1: :: CIRCUIT2:1
for IIG being non empty non void Circuit-like monotonic ManySortedSign
for X being V2() 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
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
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
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 Element of 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
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
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
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;
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
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
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 Element of 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
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
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;

begin

::---------------------------------------------------------------------------
:: Computations
::---------------------------------------------------------------------------
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
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
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 Element of 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
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 Element of NAT holds iv c= (Computation (s,InpFs)) . k
proof end;

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

theorem Th16: :: CIRCUIT2:16
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 Element of 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
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
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
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;