let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of (Free (S,X)),(TermAlg S) st
( h is_homomorphism Free (S,X), TermAlg S & ( for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t ) )
let X be V5() ManySortedSet of S; for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of (Free (S,X)),(TermAlg S) st
( h is_homomorphism Free (S,X), TermAlg S & ( for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t ) )
let w be ManySortedFunction of X, the carrier of S --> NAT; ex h being ManySortedFunction of (Free (S,X)),(TermAlg S) st
( h is_homomorphism Free (S,X), TermAlg S & ( for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t ) )
A1:
TermAlg S = Free (S,( the carrier of S --> NAT))
by MSAFREE3:31;
reconsider G = FreeGen X as V5() GeneratorSet of Free (S,X) by MSAFREE3:31;
deffunc H2( SortSymbol of S, Element of G . $1) -> set = root-tree [((w . $1) . (($2 . {}) `1)),$1];
A2:
for s being SortSymbol of S
for x being Element of G . s holds H2(s,x) in the Sorts of (TermAlg S) . s
proof
let s be
SortSymbol of
S;
for x being Element of G . s holds H2(s,x) in the Sorts of (TermAlg S) . slet x be
Element of
G . s;
H2(s,x) in the Sorts of (TermAlg S) . s
G . s = FreeGen (
s,
X)
by MSAFREE:def 16;
then consider y being
set such that A3:
(
y in X . s &
x = root-tree [y,s] )
by MSAFREE:def 15;
x . {} = [y,s]
by A3, TREES_4:3;
then reconsider x1 =
(x . {}) `1 as
Element of
X . s by A3;
A4:
(w . s) . x1 in ( the carrier of S --> NAT) . s
;
then reconsider t =
H2(
s,
x) as
Term of
S,
( the carrier of S --> NAT) by MSATERM:4;
t in FreeSort (
( the carrier of S --> NAT),
(the_sort_of t))
by MSATERM:def 5;
then
t in FreeSort (
( the carrier of S --> NAT),
s)
by A4;
hence
H2(
s,
x)
in the
Sorts of
(TermAlg S) . s
by MSAFREE:def 11;
verum
end;
consider f being ManySortedFunction of G, the Sorts of (TermAlg S) such that
A5:
for s being SortSymbol of S
for x being Element of G . s holds (f . s) . x = H2(s,x)
from MSAFREE4:sch 2(A2);
( FreeGen X is free & FreeMSA X = Free (S,X) )
by MSAFREE3:31;
then consider h being ManySortedFunction of (Free (S,X)),(TermAlg S) such that
A6:
( h is_homomorphism Free (S,X), TermAlg S & h || G = f )
;
set t = the Element of (Free (S,X));
consider F being ManySortedSet of S -Terms X such that
A7:
( # ( the Element of (Free (S,X)),w) = F . the Element of (Free (S,X)) & ( 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;
take
h
; ( h is_homomorphism Free (S,X), TermAlg S & ( for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t ) )
thus
h is_homomorphism Free (S,X), TermAlg S
by A6; for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t
let s be SortSymbol of S; for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t
let t be Element of (Free (S,X)),s; # (t,w) = (h . s) . t
defpred S1[ DecoratedTree] means for s being SortSymbol of S st $1 in the Sorts of (Free (S,X)) . s holds
# ($1,w) = (h . s) . $1;
A8:
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;
for x being Element of X . s holds S1[ root-tree [x,s]]let x be
Element of
X . s;
S1[ root-tree [x,s]]
reconsider t =
root-tree [x,s] as
Term of
S,
X by MSATERM:4;
let s1 be
SortSymbol of
S;
( root-tree [x,s] in the Sorts of (Free (S,X)) . s1 implies # ((root-tree [x,s]),w) = (h . s1) . (root-tree [x,s]) )
assume
root-tree [x,s] in the
Sorts of
(Free (S,X)) . s1
;
# ((root-tree [x,s]),w) = (h . s1) . (root-tree [x,s])
then
t in the
Sorts of
(FreeMSA X) . s1
by MSAFREE3:31;
then
(
s = the_sort_of t &
t in FreeSort (
X,
s1) )
by MSAFREE:def 11, MSATERM:14;
then A9:
s = s1
by MSATERM:def 5;
t in FreeGen (
s,
X)
by MSAFREE:def 15;
then reconsider q =
t as
Element of
G . s by MSAFREE:def 16;
t is
Element of
(FreeMSA X)
by MSATERM:13;
then
t is
Element of
(Free (S,X))
by MSAFREE3:31;
hence # (
(root-tree [x,s]),
w) =
F . t
by A7, Th55
.=
root-tree [((w . s) . x),s]
by A7
.=
root-tree [((w . s) . ([x,s] `1)),s]
.=
H2(
s,
q)
by TREES_4:3
.=
(f . s) . t
by A5
.=
((h . s) | (G . s)) . q
by A6, MSAFREE:def 1
.=
(h . s1) . (root-tree [x,s])
by A9, FUNCT_1:49
;
verum
end;
A10:
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;
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);
( ( 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 A11:
for
t being
Term of
S,
X st
t in rng p holds
S1[
t]
;
S1[[o, the carrier of S] -tree p]
let s be
SortSymbol of
S;
( [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s implies # (([o, the carrier of S] -tree p),w) = (h . s) . ([o, the carrier of S] -tree p) )
reconsider t =
(Sym (o,X)) -tree p as
Term of
S,
X ;
assume
[o, the carrier of S] -tree p in the
Sorts of
(Free (S,X)) . s
;
# (([o, the carrier of S] -tree p),w) = (h . s) . ([o, the carrier of S] -tree p)
then
t in the
Sorts of
(FreeMSA X) . s
by MSAFREE3:31;
then
t in FreeSort (
X,
s)
by MSAFREE:def 11;
then
(
the_sort_of t = s &
t . {} = Sym (
o,
X) )
by TREES_4:def 4, MSATERM:def 5;
then A12:
s = the_result_sort_of o
by MSATERM:17;
FreeMSA X = Free (
S,
X)
by MSAFREE3:31;
then reconsider q =
p as
Element of
Args (
o,
(Free (S,X)))
by INSTALG1:1;
rng p c= dom F
then A14:
(
dom (F * p) = dom p &
dom (h # q) = dom (the_arity_of o) &
dom q = dom (the_arity_of o) )
by RELAT_1:27, MSUALG_3:6;
now for x being object st x in dom p holds
(F * p) . x = (h # q) . xlet x be
object ;
( x in dom p implies (F * p) . x = (h # q) . x )assume A15:
x in dom p
;
(F * p) . x = (h # q) . xthen reconsider i =
x as
Nat ;
reconsider t =
p . i as
Term of
S,
X by A15, MSATERM:22;
t is
Element of
(FreeMSA X)
by MSATERM:13;
then reconsider u =
t as
Element of
(Free (S,X)) by MSAFREE3:31;
reconsider s =
(the_arity_of o) /. i as
SortSymbol of
S ;
A16:
t in rng p
by A15, FUNCT_1:def 3;
the_sort_of t = s
by A15, MSATERM:23;
then
t in FreeSort (
X,
s)
by MSATERM:def 5;
then
t in the
Sorts of
(FreeMSA X) . s
by MSAFREE:def 11;
then A17:
t in the
Sorts of
(Free (S,X)) . s
by MSAFREE3:31;
thus (F * p) . x =
F . t
by A15, FUNCT_1:13
.=
# (
u,
w)
by A7, Th55
.=
(h . s) . u
by A11, A16, A17
.=
(h # q) . x
by A15, MSUALG_3:def 6
;
verum end;
then A18:
F * p = h # q
by A14;
t is
Element of
(FreeMSA X)
by MSATERM:13;
then
t is
Element of
(Free (S,X))
by MSAFREE3:31;
hence # (
([o, the carrier of S] -tree p),
w) =
F . t
by Th55, A7
.=
(Sym (o,( the carrier of S --> NAT))) -tree (F * p)
by A7
.=
(Den (o,(Free (S,( the carrier of S --> NAT))))) . (h # q)
by A18, A1, Th13
.=
(h . s) . ((Den (o,(Free (S,X)))) . q)
by A1, A6, A12
.=
(h . s) . ([o, the carrier of S] -tree p)
by Th13
;
verum
end;
A19:
for t being Term of S,X holds S1[t]
from MSATERM:sch 1(A8, A10);
t is Element of the Sorts of (Free (S,X)) . s
;
then
t is Element of (FreeMSA X)
by MSAFREE3:31;
then
t is Term of S,X
by MSATERM:13;
hence
# (t,w) = (h . s) . t
by A19; verum