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 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
let SCS be non-empty Circuit of IIG; :: thesis: 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
let s be State of SCS; :: thesis: 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
let iv be InputValues of SCS; :: thesis: 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
let k be Element of 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;
suppose A6:
v in InnerVertices IIG
;
:: thesis: (Following s) . v = IGValue v,ivset o =
action_at v;
set U1 =
FreeEnv SCS;
set F =
Eval SCS;
set taofo =
the_arity_of (action_at v);
A7:
dom the
Arity of
IIG = the
carrier' of
IIG
by FUNCT_2:def 1;
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 A8:
len p = len (the_arity_of (action_at v))
and A9:
for
k being
Nat st
k in dom p holds
p . k = H1(
k)
from FINSEQ_1:sch 2();
A10:
for
k being
Element of
NAT st
k in dom p holds
p . k = H1(
k)
by A9;
A11:
dom p = dom (the_arity_of (action_at v))
by A8, FINSEQ_3:31;
then reconsider p =
p as
Element of
Args (action_at v),
(FreeEnv SCS) by A8, MSAFREE2:7;
A12:
Eval SCS is_homomorphism FreeEnv SCS,
SCS
by MSAFREE2:def 9;
set X = the
Sorts of
SCS;
A13:
FreeEnv SCS = MSAlgebra(#
(FreeSort the Sorts of SCS),
(FreeOper the Sorts of SCS) #)
by MSAFREE:def 16;
A14:
Args (action_at v),
(FreeEnv SCS) = ((the Sorts of (FreeEnv SCS) # ) * the Arity of IIG) . (action_at v)
by MSUALG_1:def 9;
then reconsider p' =
p as
FinSequence of
TS (DTConMSA the Sorts of SCS) by A13, MSAFREE:8;
A15:
Sym (action_at v),the
Sorts of
SCS ==> roots p'
by A13, A14, MSAFREE:10;
FreeEnv SCS = MSAlgebra(#
(FreeSort the Sorts of SCS),
(FreeOper the Sorts of SCS) #)
by MSAFREE:def 16;
then Den (action_at v),
(FreeEnv SCS) =
(FreeOper the Sorts of SCS) . (action_at v)
by MSUALG_1:def 11
.=
DenOp (action_at v),the
Sorts of
SCS
by MSAFREE:def 15
;
then A16:
(Den (action_at v),(FreeEnv SCS)) . p =
(Sym (action_at v),the Sorts of SCS) -tree p'
by A15, MSAFREE:def 14
.=
[(action_at v),the carrier of IIG] -tree p'
by MSAFREE:def 11
.=
IGTree v,
iv
by A6, A10, A11, Th9
;
A17:
((the Sorts of SCS # ) * the Arity of IIG) . (action_at v) =
(the Sorts of SCS # ) . (the Arity of IIG . (action_at v))
by A7, FUNCT_1:23
.=
(the Sorts of SCS # ) . (the_arity_of (action_at v))
by MSUALG_1:def 6
.=
product (the Sorts of SCS * (the_arity_of (action_at v)))
by PBOOLE:def 19
;
A18:
Args (action_at v),
SCS = ((the Sorts of SCS # ) * the Arity of IIG) . (action_at v)
by MSUALG_1:def 9;
reconsider Fp =
(Eval SCS) # p as
Function ;
reconsider ods =
(action_at v) depends_on_in s as
Function ;
now
(
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 4;
hence dom (the_arity_of (action_at v)) =
dom (the Sorts of SCS * (the_arity_of (action_at v)))
by RELAT_1:46
.=
dom Fp
by A17, A18, CARD_3:18
;
:: thesis: ( dom (the_arity_of (action_at v)) = dom ods & ( for x being set 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:4, FINSEQ_1:def 4;
hence dom (the_arity_of (action_at v)) =
dom (s * (the_arity_of (action_at v)))
by RELAT_1:46
.=
dom ods
by CIRCUIT1:def 3
;
:: thesis: for x being set st x in dom (the_arity_of (action_at v)) holds
Fp . x = ods . xlet x be
set ;
:: thesis: ( x in dom (the_arity_of (action_at v)) implies Fp . x = ods . x )assume A19:
x in dom (the_arity_of (action_at v))
;
:: thesis: Fp . x = ods . xreconsider v1 =
(the_arity_of (action_at v)) /. x as
Element of the
carrier of
IIG ;
reconsider x' =
x as
Element of
NAT by A19;
A20:
v1 = (the_arity_of (action_at v)) . x'
by A19, PARTFUN1:def 8;
then
v1 in rng (the_arity_of (action_at v))
by A19, FUNCT_1:def 5;
then
depth v1,
SCS < k + 1
by A2, A6, CIRCUIT1:20, XXREAL_0:2;
then A21:
depth v1,
SCS <= k
by NAT_1:13;
thus Fp . x =
((Eval SCS) . v1) . (p' . x')
by A11, A19, MSUALG_3:def 8
.=
IGValue v1,
iv
by A9, A19, A11
.=
s . v1
by A1, A21
.=
(s * (the_arity_of (action_at v))) . x
by A19, A20, FUNCT_1:23
.=
ods . x
by CIRCUIT1:def 3
;
:: thesis: verum then
(Eval SCS) # p = (action_at v) depends_on_in s
by FUNCT_1:9;
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 9
.=
IGValue v,
iv
by A6, A16, MSAFREE2:def 7
;
:: thesis: verum end;