set q99 = <*> NAT;
let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty finite-yielding MSAlgebra over IIG
for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence
for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let SCS be non-empty finite-yielding MSAlgebra over IIG; :: thesis: for v, w being Vertex of IIG
for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence
for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let v, w be Vertex of IIG; :: thesis: for e1 being Element of the Sorts of (FreeEnv SCS) . v
for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence
for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let e1 be Element of the Sorts of (FreeEnv SCS) . v; :: thesis: for e2 being Element of the Sorts of (FreeEnv SCS) . w
for q1 being DTree-yielding FinSequence
for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let e2 be Element of the Sorts of (FreeEnv SCS) . w; :: thesis: for q1 being DTree-yielding FinSequence
for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let q1 be DTree-yielding FinSequence; :: thesis: for k1 being Element of NAT st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w holds
e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
let k1 be Element of NAT ; :: thesis: ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e1 = [(action_at v), the carrier of IIG] -tree q1 & k1 + 1 in dom q1 & q1 . (k1 + 1) in the Sorts of (FreeEnv SCS) . w implies e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v )
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: e1 with-replacement (<*k1*>,e2) in the Sorts of (FreeEnv SCS) . v
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) 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) ) ) 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;
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: verum