let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p

set U1 = FreeEnv SCS;

set o = action_at v;

then reconsider p99 = p as Element of Args ((action_at v),(FreeEnv SCS)) by A4, MSAFREE2:5;

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 5

.= the Sorts of (FreeEnv SCS) . ( the ResultSort of IIG . (action_at v)) by A5, FUNCT_1:13 ;

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 14, MSUALG_1:def 4;

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

then A8: 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 ;

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 12

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

the ResultSort of IIG . (action_at v) = the_result_sort_of (action_at v) by MSUALG_1:def 2

.= 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:5;

hence IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p by A11, Def3; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p

set U1 = FreeEnv SCS;

set o = action_at v;

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

len p = len (the_arity_of (action_at v))
by A2, FINSEQ_3:29;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 A3;

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

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

then reconsider p99 = p as Element of Args ((action_at v),(FreeEnv SCS)) by A4, MSAFREE2:5;

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 5

.= the Sorts of (FreeEnv SCS) . ( the ResultSort of IIG . (action_at v)) by A5, FUNCT_1:13 ;

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 14, MSUALG_1:def 4;

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

then A8: 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 ;

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 12

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

the ResultSort of IIG . (action_at v) = the_result_sort_of (action_at v) by MSUALG_1:def 2

.= 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:5;

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

ex ek being Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) st

( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),SCS) )

then A11:
card t = size (v,SCS)
by A1, CIRCUIT1:16;ex ek being Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) st

( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),SCS) )

let k be Element of NAT ; :: thesis: ( k in dom p implies ex ek being Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) st

( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),SCS) ) )

set v1 = (the_arity_of (action_at v)) /. k;

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

( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),SCS) )

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

then reconsider ek = p . k as Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) ;

take ek = ek; :: thesis: ( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),SCS) )

thus ek = p . k ; :: thesis: card ek = size (((the_arity_of (action_at v)) /. k),SCS)

ex e1 being Element of the Sorts of (FreeMSA the Sorts of SCS) . ((the_arity_of (action_at v)) /. k) st

( card e1 = size (((the_arity_of (action_at v)) /. k),SCS) & ek = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . e1 ) by A10, Def3;

hence card ek = size (((the_arity_of (action_at v)) /. k),SCS) by Th7; :: thesis: verum

end;( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),SCS) ) )

set v1 = (the_arity_of (action_at v)) /. k;

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

( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),SCS) )

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

then reconsider ek = p . k as Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) ;

take ek = ek; :: thesis: ( ek = p . k & card ek = size (((the_arity_of (action_at v)) /. k),SCS) )

thus ek = p . k ; :: thesis: card ek = size (((the_arity_of (action_at v)) /. k),SCS)

ex e1 being Element of the Sorts of (FreeMSA the Sorts of SCS) . ((the_arity_of (action_at v)) /. k) st

( card e1 = size (((the_arity_of (action_at v)) /. k),SCS) & ek = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . e1 ) by A10, Def3;

hence card ek = size (((the_arity_of (action_at v)) /. k),SCS) by Th7; :: thesis: verum

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

p . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k)

then
[(action_at v), the carrier of IIG] -tree p = ((Fix_inp_ext iv) . v) . t
by A1, Th4;p . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k)

let k be Element of NAT ; :: thesis: ( k in dom p implies p . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) )

assume k in dom p ; :: thesis: p . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k)

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

hence p . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) by Th8; :: thesis: verum

end;assume k in dom p ; :: thesis: p . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k)

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

hence p . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) by Th8; :: thesis: verum

hence IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p by A11, Def3; :: thesis: verum