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
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 V5() 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 w be 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 t be Term of S,X; ( # (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;
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;
take
t
;
( root-tree [x,s] = t & # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) )
thus
root-tree [x,s] = t
;
# (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;
verum
thus
verum
;
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;
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 A6:
for
t being
Term of
S,
X st
t in rng p holds
S1[
t]
;
S1[[o, the carrier of S] -tree p]
take tt =
(Sym (o,X)) -tree p;
( [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
;
# (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 ;
TARSKI:def 3 ( not y in rng p or y in Union the Sorts of (Free (S,X)) )
assume
y in rng p
;
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;
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 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)) . ylet y be
object ;
( 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)
;
(F * p) . y in ( the Sorts of (Free (S,(rngs w))) * (the_arity_of o)) . ythen 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;
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;
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)
; # (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; verum