let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: 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)

let SCS be non-empty Circuit of IIG; :: thesis: 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)

let s be State of SCS; :: thesis: 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)

let iv be InputValues of SCS; :: thesis: 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)

let k be Nat; :: thesis: ( ( for v being Vertex of IIG st depth (v,SCS) <= k holds

s . v = IGValue (v,iv) ) implies for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds

(Following s) . v1 = IGValue (v1,iv) )

assume A1: for v being Vertex of IIG st depth (v,SCS) <= k holds

s . v = IGValue (v,iv) ; :: thesis: for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds

(Following s) . v1 = IGValue (v1,iv)

let v be Vertex of IIG; :: thesis: ( depth (v,SCS) <= k + 1 implies (Following s) . v = IGValue (v,iv) )

assume A2: depth (v,SCS) <= k + 1 ; :: thesis: (Following s) . v = IGValue (v,iv)

v in the carrier of IIG ;

then A3: v in (InputVertices IIG) \/ (InnerVertices IIG) by XBOOLE_1:45;

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)

let SCS be non-empty Circuit of IIG; :: thesis: 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)

let s be State of SCS; :: thesis: 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)

let iv be InputValues of SCS; :: thesis: 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)

let k be Nat; :: thesis: ( ( for v being Vertex of IIG st depth (v,SCS) <= k holds

s . v = IGValue (v,iv) ) implies for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds

(Following s) . v1 = IGValue (v1,iv) )

assume A1: for v being Vertex of IIG st depth (v,SCS) <= k holds

s . v = IGValue (v,iv) ; :: thesis: for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds

(Following s) . v1 = IGValue (v1,iv)

let v be Vertex of IIG; :: thesis: ( depth (v,SCS) <= k + 1 implies (Following s) . v = IGValue (v,iv) )

assume A2: depth (v,SCS) <= k + 1 ; :: thesis: (Following s) . v = IGValue (v,iv)

v in the carrier of IIG ;

then A3: v in (InputVertices IIG) \/ (InnerVertices IIG) by XBOOLE_1:45;

per cases
( v in InputVertices IIG or v in InnerVertices IIG )
by A3, XBOOLE_0:def 3;

end;

suppose A4:
v in InputVertices IIG
; :: thesis: (Following s) . v = IGValue (v,iv)

then A5:
depth (v,SCS) = 0
by CIRCUIT1:18;

thus (Following s) . v = s . v by A4, Def5

.= IGValue (v,iv) by A1, A5, NAT_1:2 ; :: thesis: verum

end;thus (Following s) . v = s . v by A4, Def5

.= IGValue (v,iv) by A1, A5, NAT_1:2 ; :: thesis: verum

suppose A6:
v in InnerVertices IIG
; :: thesis: (Following s) . v = IGValue (v,iv)

set F = Eval SCS;

set X = the Sorts of SCS;

set U1 = FreeEnv SCS;

set o = action_at v;

set taofo = the_arity_of (action_at v);

deffunc H_{1}( Nat) -> Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. $1) = IGTree (((the_arity_of (action_at v)) /. $1),iv);

consider p being FinSequence such that

A7: len p = len (the_arity_of (action_at v)) and

A8: for k being Nat st k in dom p holds

p . k = H_{1}(k)
from FINSEQ_1:sch 2();

A9: for k being Element of NAT st k in dom p holds

p . k = H_{1}(k)
by A8;

then A11: Den ((action_at v),(FreeEnv SCS)) = (FreeOper the Sorts of SCS) . (action_at v) by MSUALG_1:def 6

.= DenOp ((action_at v), the Sorts of SCS) by MSAFREE:def 13 ;

reconsider ods = (action_at v) depends_on_in s as Function ;

A12: Eval SCS is_homomorphism FreeEnv SCS,SCS by MSAFREE2:def 9;

dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;

then A13: (( the Sorts of SCS #) * the Arity of IIG) . (action_at v) = ( the Sorts of SCS #) . ( the Arity of IIG . (action_at v)) by FUNCT_1:13

.= ( the Sorts of SCS #) . (the_arity_of (action_at v)) by MSUALG_1:def 1

.= product ( the Sorts of SCS * (the_arity_of (action_at v))) by FINSEQ_2:def 5 ;

A14: dom p = dom (the_arity_of (action_at v)) by A7, FINSEQ_3:29;

reconsider p = p as Element of Args ((action_at v),(FreeEnv SCS)) by A7, A10, MSAFREE2:5;

A15: ( FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) & Args ((action_at v),(FreeEnv SCS)) = (( the Sorts of (FreeEnv SCS) #) * the Arity of IIG) . (action_at v) ) by MSAFREE:def 14, MSUALG_1:def 4;

then reconsider p9 = p as FinSequence of TS (DTConMSA the Sorts of SCS) by MSAFREE:8;

Sym ((action_at v), the Sorts of SCS) ==> roots p9 by A15, MSAFREE:10;

then A16: (Den ((action_at v),(FreeEnv SCS))) . p = (Sym ((action_at v), the Sorts of SCS)) -tree p9 by A11, MSAFREE:def 12

.= [(action_at v), the carrier of IIG] -tree p9 by MSAFREE:def 9

.= IGTree (v,iv) by A6, A9, A14, Th9 ;

reconsider Fp = (Eval SCS) # p as Function ;

A17: Args ((action_at v),SCS) = (( the Sorts of SCS #) * the Arity of IIG) . (action_at v) by MSUALG_1:def 4;

hence (Following s) . v = (Den ((action_at v),SCS)) . ((Eval SCS) # p) by A6, Def5

.= ((Eval SCS) . (the_result_sort_of (action_at v))) . ((Den ((action_at v),(FreeEnv SCS))) . p) by A12, MSUALG_3:def 7

.= IGValue (v,iv) by A6, A16, MSAFREE2:def 7 ;

:: thesis: verum

end;set X = the Sorts of SCS;

set U1 = FreeEnv SCS;

set o = action_at v;

set taofo = the_arity_of (action_at v);

deffunc H

consider p being FinSequence such that

A7: len p = len (the_arity_of (action_at v)) and

A8: for k being Nat st k in dom p holds

p . k = H

A9: for k being Element of NAT st k in dom p holds

p . k = H

A10: now :: thesis: for k being Nat st k in dom p holds

p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k)

FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #)
by MSAFREE:def 14;p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k)

let k be Nat; :: thesis: ( k in dom p implies p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) )

assume k in dom p ; :: thesis: p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k)

then p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) by A8;

hence p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) ; :: thesis: verum

end;assume k in dom p ; :: thesis: p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k)

then p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) by A8;

hence p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) ; :: thesis: verum

then A11: Den ((action_at v),(FreeEnv SCS)) = (FreeOper the Sorts of SCS) . (action_at v) by MSUALG_1:def 6

.= DenOp ((action_at v), the Sorts of SCS) by MSAFREE:def 13 ;

reconsider ods = (action_at v) depends_on_in s as Function ;

A12: Eval SCS is_homomorphism FreeEnv SCS,SCS by MSAFREE2:def 9;

dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;

then A13: (( the Sorts of SCS #) * the Arity of IIG) . (action_at v) = ( the Sorts of SCS #) . ( the Arity of IIG . (action_at v)) by FUNCT_1:13

.= ( the Sorts of SCS #) . (the_arity_of (action_at v)) by MSUALG_1:def 1

.= product ( the Sorts of SCS * (the_arity_of (action_at v))) by FINSEQ_2:def 5 ;

A14: dom p = dom (the_arity_of (action_at v)) by A7, FINSEQ_3:29;

reconsider p = p as Element of Args ((action_at v),(FreeEnv SCS)) by A7, A10, MSAFREE2:5;

A15: ( FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) & Args ((action_at v),(FreeEnv SCS)) = (( the Sorts of (FreeEnv SCS) #) * the Arity of IIG) . (action_at v) ) by MSAFREE:def 14, MSUALG_1:def 4;

then reconsider p9 = p as FinSequence of TS (DTConMSA the Sorts of SCS) by MSAFREE:8;

Sym ((action_at v), the Sorts of SCS) ==> roots p9 by A15, MSAFREE:10;

then A16: (Den ((action_at v),(FreeEnv SCS))) . p = (Sym ((action_at v), the Sorts of SCS)) -tree p9 by A11, MSAFREE:def 12

.= [(action_at v), the carrier of IIG] -tree p9 by MSAFREE:def 9

.= IGTree (v,iv) by A6, A9, A14, Th9 ;

reconsider Fp = (Eval SCS) # p as Function ;

A17: Args ((action_at v),SCS) = (( the Sorts of SCS #) * the Arity of IIG) . (action_at v) by MSUALG_1:def 4;

now :: thesis: ( dom (the_arity_of (action_at v)) = dom Fp & dom (the_arity_of (action_at v)) = dom ods & ( for x being object st x in dom (the_arity_of (action_at v)) holds

Fp . x = ods . x ) )

then
(Eval SCS) # p = (action_at v) depends_on_in s
by FUNCT_1:2;Fp . x = ods . x ) )

( dom the Sorts of SCS = the carrier of IIG & rng (the_arity_of (action_at v)) c= the carrier of IIG )
by FINSEQ_1:def 4, PARTFUN1:def 2;

hence dom (the_arity_of (action_at v)) = dom ( the Sorts of SCS * (the_arity_of (action_at v))) by RELAT_1:27

.= dom Fp by A13, A17, CARD_3:9 ;

:: thesis: ( dom (the_arity_of (action_at v)) = dom ods & ( for x being object st x in dom (the_arity_of (action_at v)) holds

Fp . x = ods . x ) )

( dom s = the carrier of IIG & rng (the_arity_of (action_at v)) c= the carrier of IIG ) by CIRCUIT1:3, FINSEQ_1:def 4;

hence dom (the_arity_of (action_at v)) = dom (s * (the_arity_of (action_at v))) by RELAT_1:27

.= dom ods by CIRCUIT1:def 3 ;

:: thesis: for x being object st x in dom (the_arity_of (action_at v)) holds

Fp . x = ods . x

let x be object ; :: thesis: ( x in dom (the_arity_of (action_at v)) implies Fp . x = ods . x )

reconsider v1 = (the_arity_of (action_at v)) /. x as Element of IIG ;

assume A18: x in dom (the_arity_of (action_at v)) ; :: thesis: Fp . x = ods . x

then reconsider x9 = x as Element of NAT ;

A19: v1 = (the_arity_of (action_at v)) . x9 by A18, PARTFUN1:def 6;

then v1 in rng (the_arity_of (action_at v)) by A18, FUNCT_1:def 3;

then depth (v1,SCS) < k + 1 by A2, A6, CIRCUIT1:19, XXREAL_0:2;

then A20: depth (v1,SCS) <= k by NAT_1:13;

thus Fp . x = ((Eval SCS) . v1) . (p9 . x9) by A14, A18, MSUALG_3:def 6

.= IGValue (v1,iv) by A8, A14, A18

.= s . v1 by A1, A20

.= (s * (the_arity_of (action_at v))) . x by A18, A19, FUNCT_1:13

.= ods . x by CIRCUIT1:def 3 ; :: thesis: verum

end;hence dom (the_arity_of (action_at v)) = dom ( the Sorts of SCS * (the_arity_of (action_at v))) by RELAT_1:27

.= dom Fp by A13, A17, CARD_3:9 ;

:: thesis: ( dom (the_arity_of (action_at v)) = dom ods & ( for x being object st x in dom (the_arity_of (action_at v)) holds

Fp . x = ods . x ) )

( dom s = the carrier of IIG & rng (the_arity_of (action_at v)) c= the carrier of IIG ) by CIRCUIT1:3, FINSEQ_1:def 4;

hence dom (the_arity_of (action_at v)) = dom (s * (the_arity_of (action_at v))) by RELAT_1:27

.= dom ods by CIRCUIT1:def 3 ;

:: thesis: for x being object st x in dom (the_arity_of (action_at v)) holds

Fp . x = ods . x

let x be object ; :: thesis: ( x in dom (the_arity_of (action_at v)) implies Fp . x = ods . x )

reconsider v1 = (the_arity_of (action_at v)) /. x as Element of IIG ;

assume A18: x in dom (the_arity_of (action_at v)) ; :: thesis: Fp . x = ods . x

then reconsider x9 = x as Element of NAT ;

A19: v1 = (the_arity_of (action_at v)) . x9 by A18, PARTFUN1:def 6;

then v1 in rng (the_arity_of (action_at v)) by A18, FUNCT_1:def 3;

then depth (v1,SCS) < k + 1 by A2, A6, CIRCUIT1:19, XXREAL_0:2;

then A20: depth (v1,SCS) <= k by NAT_1:13;

thus Fp . x = ((Eval SCS) . v1) . (p9 . x9) by A14, A18, MSUALG_3:def 6

.= IGValue (v1,iv) by A8, A14, A18

.= s . v1 by A1, A20

.= (s * (the_arity_of (action_at v))) . x by A18, A19, FUNCT_1:13

.= ods . x by CIRCUIT1:def 3 ; :: thesis: verum

hence (Following s) . v = (Den ((action_at v),SCS)) . ((Eval SCS) # p) by A6, Def5

.= ((Eval SCS) . (the_result_sort_of (action_at v))) . ((Den ((action_at v),(FreeEnv SCS))) . p) by A12, MSUALG_3:def 7

.= IGValue (v,iv) by A6, A16, MSAFREE2:def 7 ;

:: thesis: verum