let S be non empty non void ManySortedSign ; for X0 being V5() countable ManySortedSet of S
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
ex g being ManySortedFunction of (TermAlg S),(Free (S,X0)) st
( g is_homomorphism TermAlg S, Free (S,X0) & ( for s being SortSymbol of S
for t being Element of (Free (S,X0)),s holds (g . s) . (# (t,w)) = t ) )
let X0 be V5() countable ManySortedSet of S; for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
ex g being ManySortedFunction of (TermAlg S),(Free (S,X0)) st
( g is_homomorphism TermAlg S, Free (S,X0) & ( for s being SortSymbol of S
for t being Element of (Free (S,X0)),s holds (g . s) . (# (t,w)) = t ) )
let w be ManySortedFunction of X0, the carrier of S --> NAT; ( w is "1-1" implies ex g being ManySortedFunction of (TermAlg S),(Free (S,X0)) st
( g is_homomorphism TermAlg S, Free (S,X0) & ( for s being SortSymbol of S
for t being Element of (Free (S,X0)),s holds (g . s) . (# (t,w)) = t ) ) )
assume A1:
w is "1-1"
; ex g being ManySortedFunction of (TermAlg S),(Free (S,X0)) st
( g is_homomorphism TermAlg S, Free (S,X0) & ( for s being SortSymbol of S
for t being Element of (Free (S,X0)),s holds (g . s) . (# (t,w)) = t ) )
A2:
Free (S,X0) = FreeMSA X0
by MSAFREE3:31;
reconsider G = FreeGen ( the carrier of S --> NAT) as V5() GeneratorSet of TermAlg S ;
set Y = the carrier of S --> NAT;
defpred S1[ set , set , set ] means for x being Element of ( the carrier of S --> NAT) . $1 st $2 = root-tree [x,$1] holds
( ( x in rng (w . $1) implies $3 = root-tree [(((w . $1) ") . x),$1] ) & ( x nin rng (w . $1) implies $3 = the Element of the Sorts of (Free (S,X0)) . $1 ) );
A3:
for s being SortSymbol of S
for t being Element of G . s ex T being Element of the Sorts of (Free (S,X0)) . s st S1[s,t,T]
proof
let s be
SortSymbol of
S;
for t being Element of G . s ex T being Element of the Sorts of (Free (S,X0)) . s st S1[s,t,T]let t be
Element of
G . s;
ex T being Element of the Sorts of (Free (S,X0)) . s st S1[s,t,T]
t in G . s
;
then
t in FreeGen (
s,
( the carrier of S --> NAT))
by MSAFREE:def 16;
then consider x being
set such that A4:
(
x in ( the carrier of S --> NAT) . s &
t = root-tree [x,s] )
by MSAFREE:def 15;
reconsider x =
x as
Element of
( the carrier of S --> NAT) . s by A4;
per cases
( x in rng (w . s) or x nin rng (w . s) )
;
suppose A5:
x in rng (w . s)
;
ex T being Element of the Sorts of (Free (S,X0)) . s st S1[s,t,T]then consider a being
object such that A6:
(
a in dom (w . s) &
x = (w . s) . a )
by FUNCT_1:def 3;
reconsider T =
root-tree [a,s] as
Element of the
Sorts of
(Free (S,X0)) . s by A6, MSAFREE3:4;
take
T
;
S1[s,t,T]let x0 be
Element of
( the carrier of S --> NAT) . s;
( t = root-tree [x0,s] implies ( ( x0 in rng (w . s) implies T = root-tree [(((w . s) ") . x0),s] ) & ( x0 nin rng (w . s) implies T = the Element of the Sorts of (Free (S,X0)) . s ) ) )assume
t = root-tree [x0,s]
;
( ( x0 in rng (w . s) implies T = root-tree [(((w . s) ") . x0),s] ) & ( x0 nin rng (w . s) implies T = the Element of the Sorts of (Free (S,X0)) . s ) )then A7:
[x0,s] = [x,s]
by A4, TREES_4:4;
then A8:
x = x0
by XTUPLE_0:1;
w . s is
one-to-one
by A1, MSUALG_3:1;
hence
(
x0 in rng (w . s) implies
T = root-tree [(((w . s) ") . x0),s] )
by A6, A8, FUNCT_1:34;
( x0 nin rng (w . s) implies T = the Element of the Sorts of (Free (S,X0)) . s )thus
(
x0 nin rng (w . s) implies
T = the
Element of the
Sorts of
(Free (S,X0)) . s )
by A5, A7, XTUPLE_0:1;
verum end; suppose A9:
x nin rng (w . s)
;
ex T being Element of the Sorts of (Free (S,X0)) . s st S1[s,t,T]set T = the
Element of the
Sorts of
(Free (S,X0)) . s;
take
the
Element of the
Sorts of
(Free (S,X0)) . s
;
S1[s,t, the Element of the Sorts of (Free (S,X0)) . s]let x0 be
Element of
( the carrier of S --> NAT) . s;
( t = root-tree [x0,s] implies ( ( x0 in rng (w . s) implies the Element of the Sorts of (Free (S,X0)) . s = root-tree [(((w . s) ") . x0),s] ) & ( x0 nin rng (w . s) implies the Element of the Sorts of (Free (S,X0)) . s = the Element of the Sorts of (Free (S,X0)) . s ) ) )assume
t = root-tree [x0,s]
;
( ( x0 in rng (w . s) implies the Element of the Sorts of (Free (S,X0)) . s = root-tree [(((w . s) ") . x0),s] ) & ( x0 nin rng (w . s) implies the Element of the Sorts of (Free (S,X0)) . s = the Element of the Sorts of (Free (S,X0)) . s ) )then
[x0,s] = [x,s]
by A4, TREES_4:4;
hence
( (
x0 in rng (w . s) implies the
Element of the
Sorts of
(Free (S,X0)) . s = root-tree [(((w . s) ") . x0),s] ) & (
x0 nin rng (w . s) implies the
Element of the
Sorts of
(Free (S,X0)) . s = the
Element of the
Sorts of
(Free (S,X0)) . s ) )
by A9, XTUPLE_0:1;
verum end; end;
end;
consider gg being ManySortedFunction of G, the Sorts of (Free (S,X0)) such that
A10:
for s being SortSymbol of S
for t being Element of G . s holds S1[s,t,(gg . s) . t]
from CIRCTRM1:sch 1(A3);
consider g being ManySortedFunction of (TermAlg S),(Free (S,X0)) such that
A11:
( g is_homomorphism TermAlg S, Free (S,X0) & g || G = gg )
by MSAFREE:def 5;
take
g
; ( g is_homomorphism TermAlg S, Free (S,X0) & ( for s being SortSymbol of S
for t being Element of (Free (S,X0)),s holds (g . s) . (# (t,w)) = t ) )
thus
g is_homomorphism TermAlg S, Free (S,X0)
by A11; for s being SortSymbol of S
for t being Element of (Free (S,X0)),s holds (g . s) . (# (t,w)) = t
defpred S2[ DecoratedTree] means for s being SortSymbol of S st $1 in the Sorts of (Free (S,X0)) . s holds
(g . s) . (# ($1,w)) = $1;
A12:
for s being SortSymbol of S
for v being Element of X0 . s holds S2[ root-tree [v,s]]
proof
let s be
SortSymbol of
S;
for v being Element of X0 . s holds S2[ root-tree [v,s]]let v be
Element of
X0 . s;
S2[ root-tree [v,s]]
set t =
root-tree [v,s];
let s0 be
SortSymbol of
S;
( root-tree [v,s] in the Sorts of (Free (S,X0)) . s0 implies (g . s0) . (# ((root-tree [v,s]),w)) = root-tree [v,s] )
assume A13:
root-tree [v,s] in the
Sorts of
(Free (S,X0)) . s0
;
(g . s0) . (# ((root-tree [v,s]),w)) = root-tree [v,s]
root-tree [v,s] in the
Sorts of
(Free (S,X0)) . s
by MSAFREE3:4;
then A14:
s = s0
by A13, XBOOLE_0:3, PROB_2:def 2;
then A15:
(
(w . s0) . v in rng (w . s0) &
(w . s0) . v in ( the carrier of S --> NAT) . s0 )
by FUNCT_2:4, FUNCT_2:5;
then
root-tree [((w . s0) . v),s0] in FreeGen (
s0,
( the carrier of S --> NAT))
by MSAFREE:def 15;
then A16:
root-tree [((w . s0) . v),s0] in G . s0
by MSAFREE:def 16;
then A17:
(gg . s0) . (root-tree [((w . s0) . v),s0]) = root-tree [(((w . s0) ") . ((w . s0) . v)),s0]
by A15, A10;
A18:
# (
(root-tree [v,s]),
w)
= root-tree [((w . s0) . v),s0]
by A14, Th57;
gg . s0 = (g . s0) | (G . s0)
by A11, MSAFREE:def 1;
then A19:
(g . s0) . (root-tree [((w . s0) . v),s0]) = root-tree [(((w . s0) ") . ((w . s0) . v)),s0]
by A16, A17, FUNCT_1:49;
w . s0 is
one-to-one
by A1, MSUALG_3:1;
hence
(g . s0) . (# ((root-tree [v,s]),w)) = root-tree [v,s]
by A14, A18, A19, FUNCT_2:26;
verum
end;
A20:
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X0) st ( for t being Term of S,X0 st t in rng p holds
S2[t] ) holds
S2[[o, the carrier of S] -tree p]
proof
let o be
OperSymbol of
S;
for p being ArgumentSeq of Sym (o,X0) st ( for t being Term of S,X0 st t in rng p holds
S2[t] ) holds
S2[[o, the carrier of S] -tree p]let p be
ArgumentSeq of
Sym (
o,
X0);
( ( for t being Term of S,X0 st t in rng p holds
S2[t] ) implies S2[[o, the carrier of S] -tree p] )
assume A21:
for
t being
Term of
S,
X0 st
t in rng p holds
S2[
t]
;
S2[[o, the carrier of S] -tree p]
set t =
[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,X0)) . s implies (g . s) . (# (([o, the carrier of S] -tree p),w)) = [o, the carrier of S] -tree p )
assume A22:
[o, the carrier of S] -tree p in the
Sorts of
(Free (S,X0)) . s
;
(g . s) . (# (([o, the carrier of S] -tree p),w)) = [o, the carrier of S] -tree p
([o, the carrier of S] -tree p) . {} = [o, the carrier of S]
by TREES_4:def 4;
then
the_sort_of ((Sym (o,X0)) -tree p) = the_result_sort_of o
by MSATERM:17;
then
[o, the carrier of S] -tree p in FreeSort (
X0,
(the_result_sort_of o))
by MSATERM:def 5;
then
[o, the carrier of S] -tree p in the
Sorts of
(Free (S,X0)) . (the_result_sort_of o)
by A2, MSAFREE:def 11;
then A23:
s = the_result_sort_of o
by A22, XBOOLE_0:3, PROB_2:def 2;
defpred S3[
Nat,
object ]
means for
t being
Element of
(Free (S,X0)) st
t = p . $1 holds
$2
= # (
t,
w);
A24:
dom p = Seg (len p)
by FINSEQ_1:def 3;
A25:
for
i being
Nat st
i in Seg (len p) holds
ex
x being
object st
S3[
i,
x]
consider q being
FinSequence such that A26:
(
dom q = Seg (len p) & ( for
i being
Nat st
i in Seg (len p) holds
S3[
i,
q . i] ) )
from FINSEQ_1:sch 1(A25);
(
dom q = dom p & ( for
i being
Nat for
t being
Element of
(Free (S,X0)) st
i in dom p &
t = p . i holds
q . i = # (
t,
w) ) )
by A24, A26;
then A27:
# (
([o, the carrier of S] -tree p),
w)
= (Sym (o,( the carrier of S --> NAT))) -tree q
by Th58;
then A29:
q is
DTree-yielding
by TREES_3:24;
TermAlg S = Free (
S,
( the carrier of S --> NAT))
by MSAFREE3:31;
then
(
(# (([o, the carrier of S] -tree p),w)) . {} = Sym (
o,
( the carrier of S --> NAT)) &
# (
([o, the carrier of S] -tree p),
w) is
Term of
S,
( the carrier of S --> NAT) )
by Th42, A29, A27, TREES_4:def 4;
then consider r being
ArgumentSeq of
Sym (
o,
( the carrier of S --> NAT))
such that A30:
# (
([o, the carrier of S] -tree p),
w)
= [o, the carrier of S] -tree r
by MSATERM:10;
r = q
by A29, A27, A30, TREES_4:15;
then reconsider q =
q as
Element of
Args (
o,
(TermAlg S))
by INSTALG1:1;
reconsider a =
p as
Element of
Args (
o,
(Free (S,X0)))
by A2, INSTALG1:1;
for
n being
Nat st
n in dom q holds
a . n = (g . ((the_arity_of o) /. n)) . (q . n)
proof
let n be
Nat;
( n in dom q implies a . n = (g . ((the_arity_of o) /. n)) . (q . n) )
assume A31:
n in dom q
;
a . n = (g . ((the_arity_of o) /. n)) . (q . n)
A32:
(
dom q = dom (the_arity_of o) &
dom a = dom (the_arity_of o) )
by MSUALG_3:6;
then reconsider tn =
a . n as
Term of
S,
X0 by A31, MSATERM:22;
A33:
tn in rng p
by A31, A32, FUNCT_1:def 3;
the_sort_of tn = (the_arity_of o) /. n
by A31, A32, MSATERM:23;
then
tn in FreeSort (
X0,
((the_arity_of o) /. n))
by MSATERM:def 5;
then
tn in the
Sorts of
(Free (S,X0)) . ((the_arity_of o) /. n)
by A2, MSAFREE:def 11;
then A34:
(g . ((the_arity_of o) /. n)) . (# (tn,w)) = tn
by A21, A33;
(
S3[
n,
q . n] &
tn is
Element of
(Free (S,X0)) )
by A2, A26, A31, MSATERM:13;
hence
a . n = (g . ((the_arity_of o) /. n)) . (q . n)
by A34;
verum
end;
then A35:
g # q = a
by MSUALG_3:def 6;
thus (g . s) . (# (([o, the carrier of S] -tree p),w)) =
(g . s) . ((Den (o,(TermAlg S))) . q)
by A27, INSTALG1:3
.=
(Den (o,(Free (S,X0)))) . (g # q)
by A11, A23
.=
[o, the carrier of S] -tree p
by A2, A35, INSTALG1:3
;
verum
end;
A36:
for t being Term of S,X0 holds S2[t]
from MSATERM:sch 1(A12, A20);
let s be SortSymbol of S; for t being Element of (Free (S,X0)),s holds (g . s) . (# (t,w)) = t
let t be Element of the Sorts of (Free (S,X0)) . s; (g . s) . (# (t,w)) = t
t is Term of S,X0
by Th42;
hence
(g . s) . (# (t,w)) = t
by A36; verum