let IIG be 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
let SCS be 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
let v be 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
let iv be 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
let p be DTree-yielding FinSequence; ( 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 ) implies IGTree v,iv = [(action_at v),the carrier of IIG] -tree p )
assume that
A1:
v in InnerVertices IIG
and
A2:
dom p = dom (the_arity_of (action_at v))
and
A3:
for k being Element of NAT st k in dom p holds
p . k = IGTree ((the_arity_of (action_at v)) /. k),iv
; IGTree v,iv = [(action_at v),the carrier of IIG] -tree p
set U1 = FreeEnv SCS;
set o = action_at v;
len p = len (the_arity_of (action_at v))
by A2, FINSEQ_3:31;
then reconsider p99 = p as Element of Args (action_at v),(FreeEnv SCS) by A4, MSAFREE2:7;
set X = the Sorts of SCS;
A5:
dom the ResultSort of IIG = the carrier' of IIG
by FUNCT_2:def 1;
A6: Result (action_at v),(FreeEnv SCS) =
(the Sorts of (FreeEnv SCS) * the ResultSort of IIG) . (action_at v)
by MSUALG_1:def 10
.=
the Sorts of (FreeEnv SCS) . (the ResultSort of IIG . (action_at v))
by A5, FUNCT_1:23
;
A7:
( 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 16, MSUALG_1:def 9;
then reconsider p9 = p99 as FinSequence of TS (DTConMSA the Sorts of SCS) by MSAFREE:8;
FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #)
by MSAFREE:def 16;
then A8: 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
;
Sym (action_at v),the Sorts of SCS ==> roots p9
by A7, MSAFREE:10;
then A9: (Den (action_at v),(FreeEnv SCS)) . p =
(Sym (action_at v),the Sorts of SCS) -tree p9
by A8, MSAFREE:def 14
.=
[(action_at v),the carrier of IIG] -tree p9
by MSAFREE:def 11
;
the ResultSort of IIG . (action_at v) =
the_result_sort_of (action_at v)
by MSUALG_1:def 7
.=
v
by A1, MSAFREE2:def 7
;
then reconsider t = [(action_at v),the carrier of IIG] -tree p as Element of the Sorts of (FreeMSA the Sorts of SCS) . v by A9, A6, FUNCT_2:7;
then A11:
card t = size v,SCS
by A1, CIRCUIT1:17;
then
[(action_at v),the carrier of IIG] -tree p = ((Fix_inp_ext iv) . v) . t
by A1, Th4;
hence
IGTree v,iv = [(action_at v),the carrier of IIG] -tree p
by A11, Def3; verum