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

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 b₁ 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 b₁ . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b₁ . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b₁ . v = id (FreeGen (v, the Sorts of A)) ) )

proof end;

uniqueness
for b₁, b₂ 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 b₁ . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b₁ . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b₁ . v = id (FreeGen (v, the Sorts of A)) ) ) ) & ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b₂ . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b₂ . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b₂ . v = id (FreeGen (v, the Sorts of A)) ) ) ) holds
b₁ = b₂

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 b₄ being ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) holds
( b₄ = Fix_inp iv iff for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b₄ . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b₄ . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b₄ . 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 b₁ being ManySortedFunction of (FreeEnv A),(FreeEnv A) st
( b₁ is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b₁ )

proof end;

uniqueness
for b₁, b₂ being ManySortedFunction of (FreeEnv A),(FreeEnv A) st b₁ is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b₁ & b₂ is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b₂ holds
b₁ = b₂

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 b₄ being ManySortedFunction of (FreeEnv A),(FreeEnv A) holds
( b₄ = Fix_inp_ext iv iff ( b₄ is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b₄ ) );

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 b₁, e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & b₁ = ((Fix_inp_ext iv) . v) . e )

proof end;

uniqueness
for b₁, b₂ 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) & b₁ = ((Fix_inp_ext iv) . v) . e ) & ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & b₂ = ((Fix_inp_ext iv) . v) . e ) holds
b₁ = b₂

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 b₅ being Element of the Sorts of (FreeEnv SCS) . v holds
( b₅ = IGTree (v,iv) iff ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & b₅ = ((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;

::---------------------------------------------------------------------------
:: 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 b₁ being State of SCS st
for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b₁ . v = s . v ) & ( v in InnerVertices IIG implies b₁ . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) )

proof end;

uniqueness
for b₁, b₂ being State of SCS st ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b₁ . v = s . v ) & ( v in InnerVertices IIG implies b₁ . 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 b₂ . v = s . v ) & ( v in InnerVertices IIG implies b₂ . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) ) holds
b₁ = b₂

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, b₄ being State of SCS holds
( b₄ = Following s iff for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b₄ . v = s . v ) & ( v in InnerVertices IIG implies b₄ . 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 :: CIRCUIT2:def 6
IT = Following IT;

end;

:: deftheorem 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) -> sequence of (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 b₁ being sequence of (product the Sorts of SCS) st
( b₁ . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b₁ . (i + 1) = Following ((b₁ . i),((i + 1) -th_InputValues InpFs)) ) );
uniqueness
for b₁, b₂ being sequence of (product the Sorts of SCS) st b₁ . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b₁ . (i + 1) = Following ((b₁ . i),((i + 1) -th_InputValues InpFs)) ) & b₂ . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b₂ . (i + 1) = Following ((b₂ . i),((i + 1) -th_InputValues InpFs)) ) holds
b₁ = b₂;

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 b₅ being sequence of (product the Sorts of SCS) holds
( b₅ = Computation (s,InpFs) iff ( b₅ . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b₅ . (i + 1) = Following ((b₅ . 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 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 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 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 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;