let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for t being Term of S,X holds
( # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) & # (t,w) is Element of (TermAlg S),(the_sort_of t) )
let X be non-empty ManySortedSet of S; :: thesis: for w being ManySortedFunction of X, the carrier of S --> NAT
for t being Term of S,X holds
( # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) & # (t,w) is Element of (TermAlg S),(the_sort_of t) )
let w be ManySortedFunction of X, the carrier of S --> NAT; :: thesis: for t being Term of S,X holds
( # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) & # (t,w) is Element of (TermAlg S),(the_sort_of t) )
let t be Term of S,X; :: thesis: ( # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) & # (t,w) is Element of (TermAlg S),(the_sort_of t) )
defpred S1[ DecoratedTree] means ex t being Term of S,X st
( $1 = t & # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) );
A1: for s being SortSymbol of S
for x being Element of X . s holds S1[ root-tree [x,s]]
proof
let s be SortSymbol of S; :: thesis: for x being Element of X . s holds S1[ root-tree [x,s]]
let x be Element of X . s; :: thesis: S1[ root-tree [x,s]]
reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4;
take t ; :: thesis: ( root-tree [x,s] = t & # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) )
thus root-tree [x,s] = t ; :: thesis: # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t)
S -Terms X = Union the Sorts of (FreeMSA X) by MSATERM:13;
then t is Element of (Free (S,X)) by MSAFREE3:31;
then consider F being ManySortedSet of S -Terms X such that
A2: ( # (t,w) = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) by Def15;
A3: # (t,w) = root-tree [((w . s) . x),s] by A2;
dom w = the carrier of S by PARTFUN1:def 2;
then rng (w . s) = (rngs w) . s by FUNCT_6:22;
then A4: (w . s) . x in (rngs w) . s by FUNCT_2:4;
then reconsider tw = # (t,w) as Term of S,(rngs w) by A3, MSATERM:4;
( the_sort_of tw = s & the_sort_of t = s ) by A3, A4, MSATERM:14;
then tw in FreeSort ((rngs w),(the_sort_of t)) by MSATERM:def 5;
then tw in the Sorts of (FreeMSA (rngs w)) . (the_sort_of t) by MSAFREE:def 11;
hence # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) by MSAFREE3:31; :: thesis: verum
thus verum ; :: thesis: verum
end;
A5: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
proof
let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X st t in rng p holds
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,X); :: thesis: ( ( for t being Term of S,X st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume A6: for t being Term of S,X st t in rng p holds
S1[t] ; :: thesis: S1[[o, the carrier of S] -tree p]
take tt = (Sym (o,X)) -tree p; :: thesis: ( [o, the carrier of S] -tree p = tt & # (tt,w) is Element of (Free (S,(rngs w))),(the_sort_of tt) )
thus tt = [o, the carrier of S] -tree p ; :: thesis: # (tt,w) is Element of (Free (S,(rngs w))),(the_sort_of tt)
S -Terms X = Union the Sorts of (FreeMSA X) by MSATERM:13;
then tt is Element of (Free (S,X)) by MSAFREE3:31;
then consider F being ManySortedSet of S -Terms X such that
A7: ( # (tt,w) = F . tt & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) by Def15;
A8: # (tt,w) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) by A7;
A9: ( Args (o,(Free (S,(rngs w)))) = product ( the Sorts of (Free (S,(rngs w))) * (the_arity_of o)) & dom ( the Sorts of (Free (S,(rngs w))) * (the_arity_of o)) = dom (the_arity_of o) ) by PRALG_2:3;
p is Element of Args (o,(FreeMSA X)) by INSTALG1:1;
then ( p is Element of Args (o,(Free (S,X))) & Args (o,(Free (S,X))) = product ( the Sorts of (Free (S,X)) * (the_arity_of o)) ) by PRALG_2:3, MSAFREE3:31;
then A10: ( p in product ( the Sorts of (Free (S,X)) * (the_arity_of o)) & dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom (the_arity_of o) ) by PRALG_2:3;
then A11: dom p = dom (the_arity_of o) by CARD_3:9;
A12: dom F = S -Terms X by PARTFUN1:def 2
.= Union the Sorts of (FreeMSA X) by MSATERM:13
.= Union the Sorts of (Free (S,X)) by MSAFREE3:31 ;
A13: rng p c= Union the Sorts of (Free (S,X))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in Union the Sorts of (Free (S,X)) )
assume y in rng p ; :: thesis: y in Union the Sorts of (Free (S,X))
then consider x being object such that
A14: ( x in dom p & y = p . x ) by FUNCT_1:def 3;
y in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . x by A10, A14, A11, CARD_3:9;
then ( y in the Sorts of (Free (S,X)) . ((the_arity_of o) . x) & (the_arity_of o) . x in the carrier of S & dom the Sorts of (Free (S,X)) = the carrier of S ) by A14, A11, FUNCT_1:13, FUNCT_1:102, PARTFUN1:def 2;
hence y in Union the Sorts of (Free (S,X)) by CARD_5:2; :: thesis: verum
end;
then A15: dom (F * p) = dom p by A12, RELAT_1:27
.= dom (the_arity_of o) by A10, CARD_3:9 ;
A16: now :: thesis: for y being object st y in dom (the_arity_of o) holds
(F * p) . y in ( the Sorts of (Free (S,(rngs w))) * (the_arity_of o)) . y
let y be object ; :: thesis: ( y in dom (the_arity_of o) implies (F * p) . y in ( the Sorts of (Free (S,(rngs w))) * (the_arity_of o)) . y )
assume A17: y in dom (the_arity_of o) ; :: thesis: (F * p) . y in ( the Sorts of (Free (S,(rngs w))) * (the_arity_of o)) . y
then A18: p . y in rng p by A11, FUNCT_1:def 3;
p . y is Element of (FreeMSA X) by A18, A13, MSAFREE3:31;
then reconsider t = p . y as Term of S,X by MSAFREE3:6;
A19: ( S1[t] & F . t = # (t,w) ) by A7, A6, A18, A13, Th55;
reconsider i = y as Nat by A17;
(the_arity_of o) . i = the_sort_of t by A11, A17, MSATERM:23;
then F . t in the Sorts of (Free (S,(rngs w))) . ((the_arity_of o) . i) by A19;
then F . t in ( the Sorts of (Free (S,(rngs w))) * (the_arity_of o)) . i by A17, FUNCT_1:13;
hence (F * p) . y in ( the Sorts of (Free (S,(rngs w))) * (the_arity_of o)) . y by A11, A17, FUNCT_1:13; :: thesis: verum
end;
(Den (o,(Free (S,(rngs w))))) . (F * p) = [o, the carrier of S] -tree (F * p) by A16, A9, A15, CARD_3:9, Th13;
then ( [o, the carrier of S] -tree (F * p) in Result (o,(Free (S,(rngs w)))) & dom the ResultSort of S = the carrier' of S ) by A16, A9, A15, CARD_3:9, FUNCT_2:5, FUNCT_2:def 1;
then ( # (tt,w) in the Sorts of (Free (S,(rngs w))) . (the_result_sort_of o) & tt . {} = Sym (o,X) ) by A8, FUNCT_1:13, TREES_4:def 4;
hence # (tt,w) is Element of (Free (S,(rngs w))),(the_sort_of tt) by MSATERM:17; :: thesis: verum
end;
for t being Term of S,X holds S1[t] from MSATERM:sch 1(A1, A5);
 then S1[t] ;
hence # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) ; :: thesis: # (t,w) is Element of (TermAlg S),(the_sort_of t)
then A20: # (t,w) in the Sorts of (Free (S,(rngs w))) . (the_sort_of t) ;
X is_transformable_to the carrier of S --> NAT by Th21;
then rngs w is ManySortedSubset of the carrier of S --> NAT by PBOOLE:def 18, MSSUBFAM:17;
then Free (S,(rngs w)) is MSSubAlgebra of Free (S,( the carrier of S --> NAT)) by Th59;
then the Sorts of (Free (S,(rngs w))) is MSSubset of (Free (S,( the carrier of S --> NAT))) by MSUALG_2:def 9;
then the Sorts of (Free (S,(rngs w))) is MSSubset of (TermAlg S) by MSAFREE3:31;
then the Sorts of (Free (S,(rngs w))) . (the_sort_of t) c= the Sorts of (TermAlg S) . (the_sort_of t) by PBOOLE:def 2, PBOOLE:def 18;
hence # (t,w) is Element of (TermAlg S),(the_sort_of t) by A20; :: thesis: verum