let IIG be 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)
let SCS be 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 s be 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 iv be 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 k be Nat; ( ( 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)
; 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; ( depth (v,SCS) <= k + 1 implies (Following s) . v = IGValue (v,iv) )
assume A2:
depth (v,SCS) <= k + 1
; (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;
suppose A6:
v in InnerVertices IIG
;
(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 H1(
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 = H1(
k)
from FINSEQ_1:sch 2();
A9:
for
k being
Element of
NAT st
k in dom p holds
p . k = H1(
k)
by A8;
FreeEnv SCS = MSAlgebra(#
(FreeSort the Sorts of SCS),
(FreeOper the Sorts of SCS) #)
by MSAFREE:def 14;
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 ( 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 ) )
(
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
;
( 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
;
for x being object st x in dom (the_arity_of (action_at v)) holds
Fp . x = ods . xlet x be
object ;
( 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))
;
Fp . x = ods . xthen 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
;
verum then
(Eval SCS) # p = (action_at v) depends_on_in s
by FUNCT_1:2;
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
;
verum end;