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 () & ( for k being Element of NAT st k in dom p holds
p . k = IGTree ((() /. k),iv) ) holds
IGTree (v,iv) = [(), 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 () & ( for k being Element of NAT st k in dom p holds
p . k = IGTree ((() /. k),iv) ) holds
IGTree (v,iv) = [(), 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 () & ( for k being Element of NAT st k in dom p holds
p . k = IGTree ((() /. k),iv) ) holds
IGTree (v,iv) = [(), 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 () & ( for k being Element of NAT st k in dom p holds
p . k = IGTree ((() /. k),iv) ) holds
IGTree (v,iv) = [(), the carrier of IIG] -tree p

let p be DTree-yielding FinSequence; :: thesis: ( v in InnerVertices IIG & dom p = dom () & ( for k being Element of NAT st k in dom p holds
p . k = IGTree ((() /. k),iv) ) implies IGTree (v,iv) = [(), the carrier of IIG] -tree p )

assume that
A1: v in InnerVertices IIG and
A2: dom p = dom () and
A3: for k being Element of NAT st k in dom p holds
p . k = IGTree ((() /. k),iv) ; :: thesis: IGTree (v,iv) = [(), 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) . (() /. k)
let k be Nat; :: thesis: ( k in dom p implies p . k in the Sorts of (FreeEnv SCS) . (() /. k) )
assume k in dom p ; :: thesis: p . k in the Sorts of (FreeEnv SCS) . (() /. k)
then p . k = IGTree ((() /. k),iv) by A3;
hence p . k in the Sorts of (FreeEnv SCS) . (() /. k) ; :: thesis: verum
end;
len p = len () by ;
then reconsider p99 = p as Element of Args ((),(FreeEnv SCS)) by ;
set X = the Sorts of SCS;
A5: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def 1;
A6: Result ((),(FreeEnv SCS)) = ( the Sorts of (FreeEnv SCS) * the ResultSort of IIG) . () by MSUALG_1:def 5
.= the Sorts of (FreeEnv SCS) . ( the ResultSort of IIG . ()) by ;
A7: ( FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) & Args ((),(FreeEnv SCS)) = (( the Sorts of (FreeEnv SCS) #) * the Arity of IIG) . () ) by ;
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 ((),(FreeEnv SCS)) = (FreeOper the Sorts of SCS) . () by MSUALG_1:def 6
.= DenOp ((), the Sorts of SCS) by MSAFREE:def 13 ;
Sym ((), the Sorts of SCS) ==> roots p9 by ;
then A9: (Den ((),(FreeEnv SCS))) . p = (Sym ((), the Sorts of SCS)) -tree p9 by
.= [(), the carrier of IIG] -tree p9 by MSAFREE:def 9 ;
the ResultSort of IIG . () = the_result_sort_of () by MSUALG_1:def 2
.= v by ;
then reconsider t = [(), the carrier of IIG] -tree p as Element of the Sorts of (FreeMSA the Sorts of SCS) . v by ;
now :: thesis: for k being Element of NAT st k in dom p holds
ex ek being Element of the Sorts of (FreeEnv SCS) . (() /. k) st
( ek = p . k & card ek = size ((() /. k),SCS) )
let k be Element of NAT ; :: thesis: ( k in dom p implies ex ek being Element of the Sorts of (FreeEnv SCS) . (() /. k) st
( ek = p . k & card ek = size ((() /. k),SCS) ) )

set v1 = () /. k;
assume k in dom p ; :: thesis: ex ek being Element of the Sorts of (FreeEnv SCS) . (() /. k) st
( ek = p . k & card ek = size ((() /. k),SCS) )

then A10: p . k = IGTree ((() /. k),iv) by A3;
then reconsider ek = p . k as Element of the Sorts of (FreeEnv SCS) . (() /. k) ;
take ek = ek; :: thesis: ( ek = p . k & card ek = size ((() /. k),SCS) )
thus ek = p . k ; :: thesis: card ek = size ((() /. k),SCS)
ex e1 being Element of the Sorts of (FreeMSA the Sorts of SCS) . (() /. k) st
( card e1 = size ((() /. k),SCS) & ek = (() . (() /. k)) . e1 ) by ;
hence card ek = size ((() /. k),SCS) by Th7; :: thesis: verum
end;
then A11: card t = size (v,SCS) by ;
now :: thesis: for k being Element of NAT st k in dom p holds
p . k = (() . (() /. k)) . (p . k)
let k be Element of NAT ; :: thesis: ( k in dom p implies p . k = (() . (() /. k)) . (p . k) )
assume k in dom p ; :: thesis: p . k = (() . (() /. k)) . (p . k)
then p . k = IGTree ((() /. k),iv) by A3;
hence p . k = (() . (() /. k)) . (p . k) by Th8; :: thesis: verum
end;
then [(), the carrier of IIG] -tree p = (() . v) . t by ;
hence IGTree (v,iv) = [(), the carrier of IIG] -tree p by ; :: thesis: verum