set q99 = <*> NAT;
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis:
let SCS be non-empty finite-yielding MSAlgebra over IIG; :: thesis:
let v, w be Vertex of IIG; :: thesis:
let e1 be Element of the Sorts of (FreeEnv SCS) . v; :: thesis:
let e2 be Element of the Sorts of (FreeEnv SCS) . w; :: thesis:
let q1 be DTree-yielding FinSequence; :: thesis:
let k1 be Element of NAT ; :: thesis:
set k = k1 + 1;
set eke = e1 with-replacement (<*k1*>,e2);
assume that
A1: v in (InnerVertices IIG) \ (SortsWithConstants IIG) and
A2: e1 = [(action_at v), the carrier of IIG] -tree q1 and
A3: k1 + 1 in dom q1 and
A4: q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w ; :: thesis:
reconsider O = [: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of SCS)) as non empty set ;
reconsider R = REL the Sorts of SCS as Relation of O,(O *) ;
A5: DTConMSA the Sorts of SCS = DTConstrStr(# O,R #) by MSAFREE:def 8;
then reconsider TSDT = TS (DTConMSA the Sorts of SCS) as Subset of (FinTrees O) ;
for x being object st x in TSDT holds
x is DecoratedTree of O ;
then reconsider TSDT = TSDT as DTree-set of O by TREES_3:def 6;
reconsider av = action_at v as OperSymbol of IIG ;
reconsider e19 = e1 as DecoratedTree ;
ex p9 being DTree-yielding FinSequence st
( p9 = q1 & dom e19 = tree (doms p9) ) by A2, TREES_4:def 4;
then reconsider m = <*k1*> as Element of dom e1 by A3, PRE_CIRC:13;
reconsider m9 = m as FinSequence of NAT ;
consider qq being DTree-yielding FinSequence such that
A6: e1 with-replacement (m9,e2) = [av, the carrier of IIG] -tree qq and
A7: len qq = len q1 and
A8: qq . (k1 + 1) = e2 and
A9: for i being Nat st i in dom q1 & i <> k1 + 1 holds
qq . i = q1 . i by A2, PRE_CIRC:15;
( NonTerminals (DTConMSA the Sorts of SCS) = [: the carrier' of IIG,{ the carrier of IIG}:] & the carrier of IIG in { the carrier of IIG} ) by MSAFREE:6, TARSKI:def 1;
then reconsider nt = [av, the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of SCS) by ZFMISC_1:87;
A10: FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def 14;
then A11: the Sorts of (FreeEnv SCS) . v = FreeSort ( the Sorts of SCS,v) by MSAFREE:def 11;
then A12: e1 in TS (DTConMSA the Sorts of SCS) by TARSKI:def 3;
e1 . {} = nt by A2, TREES_4:def 4;
then ex p9 being FinSequence of TS (DTConMSA the Sorts of SCS) st
( e1 = nt -tree p9 & nt ==> roots p9 ) by A12, DTCONSTR:10;
then reconsider q19 = q1 as FinSequence of TS (DTConMSA the Sorts of SCS) by A2, TREES_4:15;
the Sorts of (FreeEnv SCS) . w = FreeSort ( the Sorts of SCS,w) by A10, MSAFREE:def 11;
then A13: e2 in FreeSort ( the Sorts of SCS,w) ;
then e2 in { a9 where a9 is Element of TS (DTConMSA the Sorts of SCS) : ( ex x being set st
( x in the Sorts of SCS . w & a9 = root-tree [x,w] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a9 . {} & the_result_sort_of o = w ) ) } by MSAFREE:def 10;
then consider aa being Element of TS (DTConMSA the Sorts of SCS) such that
A14: aa = e2 and
A15: ( ex x being set st
( x in the Sorts of SCS . w & aa = root-tree [x,w] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = aa . {} & the_result_sort_of o = w ) ) ;
A16: dom qq = dom q1 by A7, FINSEQ_3:29;
rng qq c= TS (DTConMSA the Sorts of SCS)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng qq ; :: thesis:
then consider x being object such that
A17: x in dom qq and
A18: y = qq . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A17;

per cases ;

suppose x = k1 + 1 ; :: thesis:

hence y in TS (DTConMSA the Sorts of SCS) by A8, A14, A18; :: thesis:

end;

suppose x <> k1 + 1 ; :: thesis:

then qq . x = q19 . x by A9, A16, A17;
hence y in TS (DTConMSA the Sorts of SCS) by A16, A17, A18, FINSEQ_2:11; :: thesis:

end;

then reconsider q9 = qq as FinSequence of TSDT by FINSEQ_1:def 4;
reconsider rq = roots q9 as FinSequence of O ;
reconsider rq = rq as Element of O * by FINSEQ_1:def 11;
A19: dom rq = dom qq by TREES_3:def 18;
A20: v in InnerVertices IIG by A1, XBOOLE_0:def 5;
then A21: the Sorts of (FreeEnv SCS) . (the_result_sort_of av) = the Sorts of (FreeEnv SCS) . v by MSAFREE2:def 7;
then A22: len q1 = len (the_arity_of av) by A2, MSAFREE2:10;
then A23: dom rq = dom (the_arity_of av) by A7, A19, FINSEQ_3:29;
A24: for x being set st x in dom rq holds
( ( rq . x in [: the carrier' of IIG,{ the carrier of IIG}:] implies for o1 being OperSymbol of IIG st [o1, the carrier of IIG] = rq . x holds
the_result_sort_of o1 = (the_arity_of av) . x ) & ( rq . x in Union (coprod the Sorts of SCS) implies rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS) ) )

proof

the carrier of IIG in { the carrier of IIG} by TARSKI:def 1;
then [av, the carrier of IIG] in [: the carrier' of IIG,{ the carrier of IIG}:] by ZFMISC_1:87;
then reconsider av9 = [av, the carrier of IIG] as Symbol of (DTConMSA the Sorts of SCS) by A5, XBOOLE_0:def 3;
reconsider q19 = q19 as FinSequence of TSDT ;
let x be set ; :: thesis:
reconsider b = roots q19 as Element of ([: the carrier' of IIG,{ the carrier of IIG}:] \/ (Union (coprod the Sorts of SCS))) * by FINSEQ_1:def 11;
reconsider b = b as FinSequence ;
assume A25: x in dom rq ; :: thesis:
then reconsider x9 = x as Element of NAT ;
A26: (the_arity_of av) /. x9 = (the_arity_of av) . x9 by A23, A25, PARTFUN1:def 6;
A27: dom q1 = dom (the_arity_of av) by A22, FINSEQ_3:29;
for n being Nat st n in dom q1 holds
q1 . n in FreeSort ( the Sorts of SCS,((the_arity_of av) /. n))

proof

let n be Nat; :: thesis:
assume n in dom q1 ; :: thesis:
then ( q1 . n in the Sorts of (FreeEnv SCS) . ((the_arity_of av) . n) & (the_arity_of av) . n = (the_arity_of av) /. n ) by A2, A21, A27, MSAFREE2:11, PARTFUN1:def 6;
hence q1 . n in FreeSort ( the Sorts of SCS,((the_arity_of av) /. n)) by A10, MSAFREE:def 11; :: thesis:

end;

then A28: q19 in (((FreeSort the Sorts of SCS) #) * the Arity of IIG) . av by A27, MSAFREE:9;
Sym (av, the Sorts of SCS) = [av, the carrier of IIG] by MSAFREE:def 9;
then av9 ==> b by A28, MSAFREE:10;
then A29: ( dom (roots q1) = dom q1 & [av9,b] in R ) by A5, LANG1:def 1, TREES_3:def 18;
A30: (the_arity_of av) /. (k1 + 1) = w by A2, A3, A4, A20, Th5;
A31: ex T being DecoratedTree st
( T = qq . x9 & rq . x9 = T . {} ) by A19, A25, TREES_3:def 18;
A32: ex T9 being DecoratedTree st
( T9 = q1 . x9 & (roots q1) . x9 = T9 . {} ) by A16, A19, A25, TREES_3:def 18;
thus ( rq . x in [: the carrier' of IIG,{ the carrier of IIG}:] implies for o1 being OperSymbol of IIG st [o1, the carrier of IIG] = rq . x holds
the_result_sort_of o1 = (the_arity_of av) . x ) :: thesis:

proof

assume A33: rq . x in [: the carrier' of IIG,{ the carrier of IIG}:] ; :: thesis:
let o1 be OperSymbol of IIG; :: thesis:
assume A34: [o1, the carrier of IIG] = rq . x ; :: thesis:

per cases ;

suppose A35: x9 = k1 + 1 ; :: thesis:

now :: thesis:

per cases by A15;

case ex xx being set st
( xx in the Sorts of SCS . w & aa = root-tree [xx,w] ) ; :: thesis:

then consider xx being set such that
xx in the Sorts of SCS . w and
A36: aa = root-tree [xx,w] ;
[o1, the carrier of IIG] = [xx,w] by A8, A14, A31, A34, A35, A36, TREES_4:3;
then A37: the carrier of IIG = w by XTUPLE_0:1;
for X being set holds not X in X ;
hence contradiction by A37; :: thesis:

end;

case ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = aa . {} & the_result_sort_of o = w ) ; :: thesis:

hence the_result_sort_of o1 = (the_arity_of av) . x by A8, A14, A26, A31, A30, A34, A35, XTUPLE_0:1; :: thesis:

end;

hence the_result_sort_of o1 = (the_arity_of av) . x ; :: thesis:

end;

suppose x9 <> k1 + 1 ; :: thesis:

then (roots q1) . x9 = [o1, the carrier of IIG] by A9, A16, A19, A25, A31, A32, A34;
hence the_result_sort_of o1 = (the_arity_of av) . x by A16, A19, A25, A29, A33, A34, MSAFREE1:3; :: thesis:

end;

thus ( rq . x in Union (coprod the Sorts of SCS) implies rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS) ) :: thesis:

proof

assume A38: rq . x in Union (coprod the Sorts of SCS) ; :: thesis:
then rq . x in Terminals (DTConMSA the Sorts of SCS) by MSAFREE:6;
then consider s1 being SortSymbol of IIG, x99 being set such that
A39: ( x99 in the Sorts of SCS . s1 & rq . x = [x99,s1] ) by MSAFREE:7;

per cases ;

suppose A40: x9 = k1 + 1 ; :: thesis:

reconsider rqx = rq . x9 as Terminal of (DTConMSA the Sorts of SCS) by A38, MSAFREE:6;
aa = root-tree rqx by A8, A14, A31, A40, DTCONSTR:9;
then aa in { a99 where a99 is Element of TS (DTConMSA the Sorts of SCS) : ( ex x999 being set st
( x999 in the Sorts of SCS . s1 & a99 = root-tree [x999,s1] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a99 . {} & the_result_sort_of o = s1 ) ) } by A39;
then A41: aa in FreeSort ( the Sorts of SCS,s1) by MSAFREE:def 10;
A42: e2 in (FreeSort the Sorts of SCS) . w by A13, MSAFREE:def 11;

now :: thesis:

assume w <> s1 ; :: thesis:
then (FreeSort the Sorts of SCS) . w misses (FreeSort the Sorts of SCS) . s1 by MSAFREE:12;
then A43: ((FreeSort the Sorts of SCS) . w) /\ ((FreeSort the Sorts of SCS) . s1) = {} by XBOOLE_0:def 7;
e2 in (FreeSort the Sorts of SCS) . s1 by A14, A41, MSAFREE:def 11;
hence contradiction by A42, A43, XBOOLE_0:def 4; :: thesis:

end;

hence rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS) by A26, A30, A39, A40, MSAFREE:def 2; :: thesis:

end;

suppose x9 <> k1 + 1 ; :: thesis:

then rq . x9 = (roots q1) . x9 by A9, A16, A19, A25, A31, A32;
hence rq . x in coprod (((the_arity_of av) . x), the Sorts of SCS) by A16, A19, A25, A29, A38, MSAFREE1:3; :: thesis:

end;

len rq = len qq by A19, FINSEQ_3:29;
then [nt,(roots qq)] in REL the Sorts of SCS by A7, A22, A24, MSAFREE:5;
then nt ==> roots qq by A5, LANG1:def 1;
then reconsider q9 = q9 as SubtreeSeq of nt by DTCONSTR:def 6;
e1 with-replacement (<*k1*>,e2) = nt -tree q9 by A6;
then reconsider eke9 = e1 with-replacement (<*k1*>,e2) as Element of TS (DTConMSA the Sorts of SCS) ;
<*> NAT in (dom e1) with-replacement (m9,(dom e2)) by TREES_1:22;
then ( ( not m9 is_a_prefix_of <*> NAT & (e1 with-replacement (<*k1*>,e2)) . (<*> NAT) = e1 . (<*> NAT) ) or ex r being FinSequence of NAT st
( r in dom e2 & <*> NAT = m9 ^ r & (e1 with-replacement (<*k1*>,e2)) . (<*> NAT) = e2 . r ) ) by TREES_2:def 11;
then A44: (e1 with-replacement (<*k1*>,e2)) . {} = [av, the carrier of IIG] by A2, TREES_4:def 4;

now :: thesis:

take av = av; :: thesis:
the_result_sort_of av = v by A20, MSAFREE2:def 7;
hence ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = (e1 with-replacement (<*k1*>,e2)) . {} & the_result_sort_of o = v ) by A44; :: thesis:

end;

then eke9 in { a99 where a99 is Element of TS (DTConMSA the Sorts of SCS) : ( ex x being set st
( x in the Sorts of SCS . v & a99 = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a99 . {} & the_result_sort_of o = v ) ) } ;
then reconsider eke9 = eke9 as Element of the Sorts of (FreeEnv SCS) . v by A11, MSAFREE:def 10;
eke9 in the Sorts of (FreeEnv SCS) . v ;
hence e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v ; :: thesis: