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

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

end;
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;

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;

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

for b_{1}, b_{2} 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_{1} . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b_{1} . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b_{1} . v = id (FreeGen (v, the Sorts of A)) ) ) ) & ( for v being Vertex of IIG holds

( ( v in InputVertices IIG implies b_{2} . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b_{2} . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b_{2} . v = id (FreeGen (v, the Sorts of A)) ) ) ) holds

b_{1} = b_{2}

end;
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 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)) ) );

ex b

for v being Vertex of IIG holds

( ( v in InputVertices IIG implies b

proof end;

uniqueness for b

( ( v in InputVertices IIG implies b

( ( v in InputVertices IIG implies b

b

proof 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_{4} being ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) holds

( b_{4} = Fix_inp iv iff for v being Vertex of IIG holds

( ( v in InputVertices IIG implies b_{4} . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b_{4} . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b_{4} . v = id (FreeGen (v, the Sorts of A)) ) ) );

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

( b

( ( v in InputVertices IIG implies b

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;

ex b_{1} being ManySortedFunction of (FreeEnv A),(FreeEnv A) st

( b_{1} is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b_{1} )

for b_{1}, b_{2} being ManySortedFunction of (FreeEnv A),(FreeEnv A) st b_{1} is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b_{1} & b_{2} is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b_{2} holds

b_{1} = b_{2}

end;
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 ( it is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= it );

ex b

( b

proof end;

uniqueness for b

b

proof 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_{4} being ManySortedFunction of (FreeEnv A),(FreeEnv A) holds

( b_{4} = Fix_inp_ext iv iff ( b_{4} is_homomorphism FreeEnv A, FreeEnv A & Fix_inp iv c= b_{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 b

( 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

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]

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

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]

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

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

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;

ex b_{1}, e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & b_{1} = ((Fix_inp_ext iv) . v) . e )

for b_{1}, b_{2} 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_{1} = ((Fix_inp_ext iv) . v) . e ) & ex e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & b_{2} = ((Fix_inp_ext iv) . v) . e ) holds

b_{1} = b_{2}

end;
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 e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & it = ((Fix_inp_ext iv) . v) . e );

ex b

( card e = size (v,SCS) & b

proof end;

uniqueness for b

( card e = size (v,SCS) & b

( card e = size (v,SCS) & b

b

proof 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_{5} being Element of the Sorts of (FreeEnv SCS) . v holds

( b_{5} = IGTree (v,iv) iff ex e being Element of the Sorts of (FreeEnv SCS) . v st

( card e = size (v,SCS) & b_{5} = ((Fix_inp_ext iv) . v) . e ) );

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

( b

( card e = size (v,SCS) & b

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))

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

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;

((Eval SCS) . v) . (IGTree (v,iv)) is Element of the Sorts of SCS . v ;

end;
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));

((Eval SCS) . v) . (IGTree (v,iv)) is Element of the Sorts of SCS . v ;

:: 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));

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

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

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

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;

ex b_{1} being State of SCS st

for v being Vertex of IIG holds

( ( v in InputVertices IIG implies b_{1} . v = s . v ) & ( v in InnerVertices IIG implies b_{1} . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) )

for b_{1}, b_{2} being State of SCS st ( for v being Vertex of IIG holds

( ( v in InputVertices IIG implies b_{1} . v = s . v ) & ( v in InnerVertices IIG implies b_{1} . 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_{2} . v = s . v ) & ( v in InnerVertices IIG implies b_{2} . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) ) holds

b_{1} = b_{2}

end;
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 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) ) );

ex b

for v being Vertex of IIG holds

( ( v in InputVertices IIG implies b

proof end;

uniqueness for b

( ( v in InputVertices IIG implies b

( ( v in InputVertices IIG implies b

b

proof 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_{4} being State of SCS holds

( b_{4} = Following s iff for v being Vertex of IIG holds

( ( v in InputVertices IIG implies b_{4} . v = s . v ) & ( v in InnerVertices IIG implies b_{4} . v = (Den ((action_at v),SCS)) . ((action_at v) depends_on_in s) ) ) );

for IIG being non empty non void Circuit-like ManySortedSign

for SCS being non-empty Circuit of IIG

for s, b

( b

( ( v in InputVertices IIG implies b

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

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;

end;
let SCS be non-empty Circuit of IIG;

let IT be State of SCS;

:: 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 );

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;

coherence

Following (s +* iv) is State of SCS ;

end;
let SCS be non-empty Circuit of IIG;

let s be State of SCS;

let iv be InputValues of SCS;

coherence

Following (s +* iv) is State of SCS ;

:: 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);

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;

(s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) is State of SCS

end;
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);

(s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) is State of SCS

proof 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);

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;

existence

ex b_{1} being Function of NAT,(product the Sorts of SCS) st

( b_{1} . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b_{1} . (i + 1) = Following ((b_{1} . i),((i + 1) -th_InputValues InpFs)) ) );

uniqueness

for b_{1}, b_{2} being Function of NAT,(product the Sorts of SCS) st b_{1} . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b_{1} . (i + 1) = Following ((b_{1} . i),((i + 1) -th_InputValues InpFs)) ) & b_{2} . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b_{2} . (i + 1) = Following ((b_{2} . i),((i + 1) -th_InputValues InpFs)) ) holds

b_{1} = b_{2};

end;
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 ( it . 0 = InitialComp (s,InpFs) & ( for i being Nat holds it . (i + 1) = Following ((it . i),((i + 1) -th_InputValues InpFs)) ) );

existence

ex b

( b

uniqueness

for b

b

proof 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_{5} being Function of NAT,(product the Sorts of SCS) holds

( b_{5} = Computation (s,InpFs) iff ( b_{5} . 0 = InitialComp (s,InpFs) & ( for i being Nat holds b_{5} . (i + 1) = Following ((b_{5} . i),((i + 1) -th_InputValues InpFs)) ) ) );

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

( b

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)

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

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

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)

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)

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

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)

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;

:: Computations

::---------------------------------------------------------------------------