let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] & the_sort_of t1 = s holds
t with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
let s be SortSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] & the_sort_of t1 = s holds
t with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] & the_sort_of t1 = s holds
t with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
let x be Element of X . s; :: thesis: for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] & the_sort_of t1 = s holds
t with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
let t, t1 be Element of (Free (S,X)); :: thesis: for xi being Element of dom t st t . xi = [x,s] & the_sort_of t1 = s holds
t with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
let xi be Element of dom t; :: thesis: ( t . xi = [x,s] & the_sort_of t1 = s implies t with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t) )
assume Z0: t . xi = [x,s] ; :: thesis: ( not the_sort_of t1 = s or t with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t) )
assume Z1: the_sort_of t1 = s ; :: thesis: t with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
defpred S1[ Element of (Free (S,X))] means for xi being Element of dom $1
for x1 being Element of X . s
for t being Element of (Free (S,X)) st $1 . xi = [x1,s] & t = $1 holds
$1 with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t);
A1: for s1 being SortSymbol of S
for x11 being Element of X . s1 holds S1[x11 -term ]
proof
let s1 be SortSymbol of S; :: thesis: for x11 being Element of X . s1 holds S1[x11 -term ]
let x11 be Element of X . s1; :: thesis: S1[x11 -term ]
let xi be Element of dom (x11 -term); :: thesis: for x1 being Element of X . s
for t being Element of (Free (S,X)) st (x11 -term) . xi = [x1,s] & t = x11 -term holds
(x11 -term) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
dom (x11 -term) = {{}} by TREES_1:29;
then A1: xi = <*> NAT ;
let x1 be Element of X . s; :: thesis: for t being Element of (Free (S,X)) st (x11 -term) . xi = [x1,s] & t = x11 -term holds
(x11 -term) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
let t be Element of (Free (S,X)); :: thesis: ( (x11 -term) . xi = [x1,s] & t = x11 -term implies (x11 -term) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t) )
assume (x11 -term) . xi = [x1,s] ; :: thesis: ( not t = x11 -term or (x11 -term) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t) )
then [x11,s1] = [x1,s] ;
then A2: ( s1 = s & x11 = x1 ) by XTUPLE_0:1;
(x11 -term) with-replacement (xi,t1) in the Sorts of (Free (S,X)) . (the_sort_of t1) by A1, SORT;
hence ( not t = x11 -term or (x11 -term) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t) ) by A2, Z1, SORT; :: thesis: verum
end;
A3: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) holds
S1[o -term p]
proof
let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) holds
S1[o -term p]
let p be Element of Args (o,(Free (S,X))); :: thesis: ( ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) implies S1[o -term p] )
assume A4: for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ; :: thesis: S1[o -term p]
let xi be Element of dom (o -term p); :: thesis: for x1 being Element of X . s
for t being Element of (Free (S,X)) st (o -term p) . xi = [x1,s] & t = o -term p holds
(o -term p) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
let x1 be Element of X . s; :: thesis: for t being Element of (Free (S,X)) st (o -term p) . xi = [x1,s] & t = o -term p holds
(o -term p) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
let t be Element of (Free (S,X)); :: thesis: ( (o -term p) . xi = [x1,s] & t = o -term p implies (o -term p) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t) )
assume A5: ( (o -term p) . xi = [x1,s] & t = o -term p ) ; :: thesis: (o -term p) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
A6: ( dom (o -term p) = tree (doms p) & doms p is Tree-yielding ) by TREES_4:10;
per cases then ( xi = {} or ex n being Nat ex w being FinSequence st
( n < len (doms p) & w in (doms p) . (n + 1) & xi = <*n*> ^ w ) ) by TREES_3:def 15;
suppose xi = {} ; :: thesis: (o -term p) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
then (o -term p) . xi = [o, the carrier of S] by TREES_4:def 4;
then ( s in the carrier of S & the carrier of S = s ) by A5, XTUPLE_0:1;
hence (o -term p) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t) ; :: thesis: verum
end;
suppose ex n being Nat ex w being FinSequence st
( n < len (doms p) & w in (doms p) . (n + 1) & xi = <*n*> ^ w ) ; :: thesis: (o -term p) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)
then consider w being FinSequence, n being Nat such that
B1: ( n < len (doms p) & w in (doms p) . (n + 1) & xi = <*n*> ^ w ) ;
( 1 <= n + 1 & n + 1 <= len (doms p) ) by B1, NAT_1:12, NAT_1:13;
then B2: ( n + 1 in dom (doms p) & dom (doms p) = dom p ) by FINSEQ_3:25, TREES_3:37;
then B3: ( p /. (n + 1) = p . (n + 1) & p . (n + 1) in rng p & (doms p) . (n + 1) = dom (p . (n + 1)) ) by FUNCT_1:def 3, PARTFUN1:def 6, FUNCT_6:def 2;
reconsider w = w as Element of dom (p /. (n + 1)) by B1, B3;
B4: n < len p by B1, TREES_3:38;
then (p /. (n + 1)) . w = [x1,s] by A5, B1, B3, TREES_4:12;
then (p /. (n + 1)) with-replacement (w,t1) is Element of (Free (S,X)),(the_sort_of (p /. (n + 1))) by B3, A4;
then (p /. (n + 1)) with-replacement (w,t1) is Element of (Free (S,X)),((the_arity_of o) /. (n + 1)) by B2, Th4A;
then reconsider q = p +* ((n + 1),((p /. (n + 1)) with-replacement (w,t1))) as Element of Args (o,(Free (S,X))) by MSUALG_6:7;
((Sym (o,X)) -tree p) with-replacement (xi,t1) = (Sym (o,X)) -tree q by B1, B3, B4, A6, Th123;
then (o -term p) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of (o -term q)) by SORT;
then (o -term p) with-replacement (xi,t1) is Element of (Free (S,X)),(the_result_sort_of o) by Th8;
hence (o -term p) with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t) by A5, Th8; :: thesis: verum
end;
end;
end;
S1[t] from MSAFREE5:sch 2(A1, A3);
hence t with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t) by Z0; :: thesis: verum