let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis:
let SCS be non-empty finite-yielding MSAlgebra of 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:
A5: FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def 16;
then A6: the Sorts of (FreeEnv SCS) . v = FreeSort the Sorts of SCS,v by MSAFREE:def 13;
then A7: e1 in TS (DTConMSA the Sorts of SCS) by TARSKI:def 3;
reconsider av = action_at v as OperSymbol of IIG ;
A8: NonTerminals (DTConMSA the Sorts of SCS) = [:the carrier' of IIG,{the carrier of IIG}:] by MSAFREE:6;
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then reconsider nt = [av,the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of SCS) by A8, ZFMISC_1:106;
e1 . {} = nt by A2, TREES_4:def 4;
then consider p' being FinSequence of TS (DTConMSA the Sorts of SCS) such that
A9: e1 = nt -tree p' and
nt ==> roots p' by A7, DTCONSTR:10;
reconsider q1' = q1 as FinSequence of TS (DTConMSA the Sorts of SCS) by A2, A9, TREES_4:15;
reconsider e1' = e1 as DecoratedTree ;
consider p' being DTree-yielding FinSequence such that
A10: p' = q1 and
A11: dom e1' = tree (doms p') by A2, TREES_4:def 4;
reconsider m = <*k1*> as Element of dom e1 by A3, A10, A11, PRE_CIRC:17;
reconsider m' = m as FinSequence of NAT ;
consider qq being DTree-yielding FinSequence such that
A12: e1 with-replacement m',e2 = [av,the carrier of IIG] -tree qq and
A13: len qq = len q1 and
A14: qq . (k1 + 1) = e2 and
A15: for i being Element of NAT st i in dom q1 & i <> k1 + 1 holds
qq . i = q1 . i by A2, PRE_CIRC:19;
A16: dom qq = dom q1 by A13, FINSEQ_3:31;
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 * ) ;
A17: DTConMSA the Sorts of SCS = DTConstrStr(# O,R #) by MSAFREE:def 10;
then reconsider TSDT = TS (DTConMSA the Sorts of SCS) as Subset of (FinTrees O) ;

now

let x be set ; :: thesis:
assume x in TSDT ; :: thesis:
then x is Element of FinTrees O ;
hence x is DecoratedTree of ; :: thesis:

end;

then reconsider TSDT = TSDT as DTree-set of O by TREES_3:def 6;
the Sorts of (FreeEnv SCS) . w = FreeSort the Sorts of SCS,w by A5, MSAFREE:def 13;
then A18: e2 in FreeSort the Sorts of SCS,w ;
then e2 in { a' where a' is Element of TS (DTConMSA the Sorts of SCS) : ( ex x being set st
( x in the Sorts of SCS . w & a' = root-tree [x,w] ) or ex o being OperSymbol of IIG st
( [o,the carrier of IIG] = a' . {} & the_result_sort_of o = w ) ) } by MSAFREE:def 12;
then consider aa being Element of TS (DTConMSA the Sorts of SCS) such that
A19: aa = e2 and
A20: ( 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 ) ) ;
rng qq c= TS (DTConMSA the Sorts of SCS)

proof

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

per cases ;

suppose x = k1 + 1 ; :: thesis:

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

end;

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

then qq . x = q1' . x by A15, A16, A21;
hence y in TS (DTConMSA the Sorts of SCS) by A16, A21, A22, FINSEQ_2:13; :: thesis:

end;

then reconsider q' = qq as FinSequence of TSDT by FINSEQ_1:def 4;
reconsider rq = roots q' as FinSequence of O ;
reconsider rq = rq as Element of O * by FINSEQ_1:def 11;
A23: dom rq = dom qq by TREES_3:def 18;
then A24: len rq = len qq by FINSEQ_3:31;
A25: v in InnerVertices IIG by A1, XBOOLE_0:def 5;
then A26: the Sorts of (FreeEnv SCS) . (the_result_sort_of av) = the Sorts of (FreeEnv SCS) . v by MSAFREE2:def 7;
then A27: len q1 = len (the_arity_of av) by A2, MSAFREE2:13;
then A28: dom rq = dom (the_arity_of av) by A13, A23, FINSEQ_3:31;
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

let x be set ; :: thesis:
assume A29: x in dom rq ; :: thesis:
then reconsider x' = x as Element of NAT ;
A30: (the_arity_of av) /. x' = (the_arity_of av) . x' by A28, A29, PARTFUN1:def 8;
consider T being DecoratedTree such that
A31: T = qq . x' and
A32: rq . x' = T . {} by A23, A29, TREES_3:def 18;
A33: dom (roots q1) = dom q1 by TREES_3:def 18;
consider T' being DecoratedTree such that
A34: T' = q1 . x' and
A35: (roots q1) . x' = T' . {} by A16, A23, A29, TREES_3:def 18;
reconsider q1' = q1' as FinSequence of TSDT ;
reconsider b = roots q1' as Element of ([:the carrier' of IIG,{the carrier of IIG}:] \/ (Union (coprod the Sorts of SCS))) * by FINSEQ_1:def 11;
A36: dom q1 = dom (the_arity_of av) by A27, FINSEQ_3:31;
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 A37: n in dom q1 ; :: thesis:
then A38: q1 . n in the Sorts of (FreeEnv SCS) . ((the_arity_of av) . n) by A2, A26, A36, MSAFREE2:14;
(the_arity_of av) . n = (the_arity_of av) /. n by A36, A37, PARTFUN1:def 8;
hence q1 . n in FreeSort the Sorts of SCS,((the_arity_of av) /. n) by A5, A38, MSAFREE:def 13; :: thesis:

end;

then A39: q1' in (((FreeSort the Sorts of SCS) # ) * the Arity of IIG) . av by A36, MSAFREE:9;
reconsider b = b as FinSequence ;
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:106;
then reconsider av' = [av,the carrier of IIG] as Symbol of (DTConMSA the Sorts of SCS) by A17, XBOOLE_0:def 3;
Sym av,the Sorts of SCS = [av,the carrier of IIG] by MSAFREE:def 11;
then av' ==> b by A39, MSAFREE:10;
then A40: [av',b] in R by A17, LANG1:def 1;
A41: (the_arity_of av) /. (k1 + 1) = w by A2, A3, A4, A25, Th6;
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 A42: rq . x in [:the carrier' of IIG,{the carrier of IIG}:] ; :: thesis:
let o1 be OperSymbol of IIG; :: thesis:
assume A43: [o1,the carrier of IIG] = rq . x ; :: thesis:

per cases ;

suppose A44: x' = k1 + 1 ; :: thesis:

now

per cases by A20;

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
A45: aa = root-tree [xx,w] ;
[o1,the carrier of IIG] = [xx,w] by A14, A19, A31, A32, A43, A44, A45, TREES_4:3;
then A46: the carrier of IIG = w by ZFMISC_1:33;
for X being set holds not X in X ;
hence contradiction by A46; :: thesis:

end;

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

then consider o being OperSymbol of IIG such that
A47: [o,the carrier of IIG] = aa . {} and
A48: the_result_sort_of o = w ;
thus the_result_sort_of o1 = (the_arity_of av) . x by A14, A19, A30, A31, A32, A41, A43, A44, A47, A48, ZFMISC_1:33; :: thesis:

end;

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

end;

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

then (roots q1) . x' = [o1,the carrier of IIG] by A15, A16, A23, A29, A31, A32, A34, A35, A43;
hence the_result_sort_of o1 = (the_arity_of av) . x by A16, A23, A29, A33, A40, A42, A43, 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 A49: 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, x'' being set such that
A50: x'' in the Sorts of SCS . s1 and
A51: rq . x = [x'',s1] by MSAFREE:7;

per cases ;

suppose A52: x' = k1 + 1 ; :: thesis:

A53: e2 in (FreeSort the Sorts of SCS) . w by A18, MSAFREE:def 13;
reconsider rqx = rq . x' as Terminal of (DTConMSA the Sorts of SCS) by A49, MSAFREE:6;
aa = root-tree rqx by A14, A19, A31, A32, A52, DTCONSTR:9;
then aa in { a'' where a'' is Element of TS (DTConMSA the Sorts of SCS) : ( ex x''' being set st
( x''' in the Sorts of SCS . s1 & a'' = root-tree [x''',s1] ) or ex o being OperSymbol of IIG st
( [o,the carrier of IIG] = a'' . {} & the_result_sort_of o = s1 ) ) } by A50, A51;
then A54: aa in FreeSort the Sorts of SCS,s1 by MSAFREE:def 12;

now

A55: e2 in (FreeSort the Sorts of SCS) . s1 by A19, A54, MSAFREE:def 13;
assume w <> s1 ; :: thesis:
then (FreeSort the Sorts of SCS) . w misses (FreeSort the Sorts of SCS) . s1 by MSAFREE:13;
then ((FreeSort the Sorts of SCS) . w) /\ ((FreeSort the Sorts of SCS) . s1) = {} by XBOOLE_0:def 7;
hence contradiction by A53, A55, XBOOLE_0:def 4; :: thesis:

end;

hence rq . x in coprod ((the_arity_of av) . x),the Sorts of SCS by A30, A41, A50, A51, A52, MSAFREE:def 2; :: thesis:

end;

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

then rq . x' = (roots q1) . x' by A15, A16, A23, A29, A31, A32, A34, A35;
hence rq . x in coprod ((the_arity_of av) . x),the Sorts of SCS by A16, A23, A29, A33, A40, A49, MSAFREE1:3; :: thesis:

end;

then [nt,(roots qq)] in REL the Sorts of SCS by A13, A24, A27, MSAFREE:5;
then nt ==> roots qq by A17, LANG1:def 1;
then reconsider q' = q' as SubtreeSeq of nt by DTCONSTR:def 9;
e1 with-replacement <*k1*>,e2 = nt -tree q' by A12;
then reconsider eke' = e1 with-replacement <*k1*>,e2 as Element of TS (DTConMSA the Sorts of SCS) ;
set q'' = <*> NAT ;
<*> NAT in (dom e1) with-replacement m',(dom e2) by TREES_1:47;
then ( ( not m' 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 = m' ^ r & (e1 with-replacement <*k1*>,e2) . (<*> NAT ) = e2 . r ) ) by TREES_2:def 12;
then A56: (e1 with-replacement <*k1*>,e2) . {} = [av,the carrier of IIG] by A2, TREES_4:def 4;

now

take av = av; :: thesis:
the_result_sort_of av = v by A25, 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 A56; :: thesis:

end;

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