let I be set ; for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for h being Endomorphism of Free (S,X)
for t being Element of (Free (S,X)) st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds
for xi being Node of (h . t) holds
( xi in (dom t) \ I or ex nu being Element of dom t st
( nu in I & ex mu being Node of ((h . t) | nu) st xi = nu ^ mu ) )
let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of the carrier of S
for h being Endomorphism of Free (S,X)
for t being Element of (Free (S,X)) st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds
for xi being Node of (h . t) holds
( xi in (dom t) \ I or ex nu being Element of dom t st
( nu in I & ex mu being Node of ((h . t) | nu) st xi = nu ^ mu ) )
let X be V5() ManySortedSet of the carrier of S; for h being Endomorphism of Free (S,X)
for t being Element of (Free (S,X)) st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds
for xi being Node of (h . t) holds
( xi in (dom t) \ I or ex nu being Element of dom t st
( nu in I & ex mu being Node of ((h . t) | nu) st xi = nu ^ mu ) )
let h be Endomorphism of Free (S,X); for t being Element of (Free (S,X)) st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds
for xi being Node of (h . t) holds
( xi in (dom t) \ I or ex nu being Element of dom t st
( nu in I & ex mu being Node of ((h . t) | nu) st xi = nu ^ mu ) )
let t be Element of (Free (S,X)); ( I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } implies for xi being Node of (h . t) holds
( xi in (dom t) \ I or ex nu being Element of dom t st
( nu in I & ex mu being Node of ((h . t) | nu) st xi = nu ^ mu ) ) )
defpred S1[ Element of (Free (S,X))] means for I being set st I = { xi where xi is Element of dom $1 : ex s being SortSymbol of S ex x being Element of X . s st $1 . xi = [x,s] } holds
for xi being Node of (h . $1) holds
( xi in (dom $1) \ I or ex nu being Element of dom $1 st
( nu in I & ex mu being Node of ((h . $1) | nu) st xi = nu ^ mu ) );
A1:
for s being SortSymbol of S
for x being Element of X . s holds S1[x -term ]
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;
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)));
( ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) implies S1[o -term p] )
assume Z0:
for
t being
Element of
(Free (S,X)) st
t in rng p holds
S1[
t]
;
S1[o -term p]
let I be
set ;
( I = { xi where xi is Element of dom (o -term p) : ex s being SortSymbol of S ex x being Element of X . s st (o -term p) . xi = [x,s] } implies for xi being Node of (h . (o -term p)) holds
( xi in (dom (o -term p)) \ I or ex nu being Element of dom (o -term p) st
( nu in I & ex mu being Node of ((h . (o -term p)) | nu) st xi = nu ^ mu ) ) )
assume A4:
I = { xi where xi is Node of (o -term p) : ex s being SortSymbol of S ex x being Element of X . s st (o -term p) . xi = [x,s] }
;
for xi being Node of (h . (o -term p)) holds
( xi in (dom (o -term p)) \ I or ex nu being Element of dom (o -term p) st
( nu in I & ex mu being Node of ((h . (o -term p)) | nu) st xi = nu ^ mu ) )
let xi be
Node of
(h . (o -term p));
( xi in (dom (o -term p)) \ I or ex nu being Element of dom (o -term p) st
( nu in I & ex mu being Node of ((h . (o -term p)) | nu) st xi = nu ^ mu ) )
assume A5:
xi nin (dom (o -term p)) \ I
;
ex nu being Element of dom (o -term p) st
( nu in I & ex mu being Node of ((h . (o -term p)) | nu) st xi = nu ^ mu )
the_sort_of (o -term p) = the_result_sort_of o
by Th8;
then A6:
h . (o -term p) =
(h . (the_result_sort_of o)) . (o -term p)
by ABBR
.=
(h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . p)
by MSAFREE4:13
.=
(Den (o,(Free (S,X)))) . (h # p)
by MSUALG_6:def 2, MSUALG_3:def 7
.=
o -term (h # p)
by MSAFREE4:13
;
per cases then
( xi = {} or ex i being Nat ex T being DecoratedTree ex q being Node of T st
( i < len (h # p) & T = (h # p) . (i + 1) & xi = <*i*> ^ q ) )
by TREES_4:11;
suppose
ex
i being
Nat ex
T being
DecoratedTree ex
q being
Node of
T st
(
i < len (h # p) &
T = (h # p) . (i + 1) &
xi = <*i*> ^ q )
;
ex nu being Element of dom (o -term p) st
( nu in I & ex mu being Node of ((h . (o -term p)) | nu) st xi = nu ^ mu )then consider i being
Nat,
T being
DecoratedTree,
q being
Node of
T such that B3:
(
i < len (h # p) &
T = (h # p) . (i + 1) &
xi = <*i*> ^ q )
;
(
dom (h # p) = dom (the_arity_of o) &
dom (the_arity_of o) = dom p )
by MSUALG_6:2;
then BA:
len (h # p) = len p
by FINSEQ_3:29;
then
( 1
<= i + 1 &
i + 1
<= len p )
by B3, NAT_1:12, NAT_1:13;
then B4:
i + 1
in dom p
by FINSEQ_3:25;
then reconsider t =
p . (i + 1) as
Element of
(Free (S,X)) by FUNCT_1:102;
set II =
{ xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } ;
B5:
t = p /. (i + 1)
by B4, PARTFUN1:def 6;
B6:
T =
(h . ((the_arity_of o) /. (i + 1))) . t
by B3, B4, MSUALG_3:def 6
.=
(h . (the_sort_of (p /. (i + 1)))) . t
by B4, Th4A
.=
h . t
by B5, ABBR
;
then reconsider q =
q as
Node of
(h . t) ;
t in rng p
by B4, FUNCT_1:def 3;
per cases then
( q in (dom t) \ { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } or ex nu being Element of dom t st
( nu in { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & ex mu being Node of ((h . t) | nu) st q = nu ^ mu ) )
by Z0;
suppose
ex
nu being
Element of
dom t st
(
nu in { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & ex
mu being
Node of
((h . t) | nu) st
q = nu ^ mu )
;
ex nu being Element of dom (o -term p) st
( nu in I & ex mu being Node of ((h . (o -term p)) | nu) st xi = nu ^ mu )then consider nu being
Node of
t,
mu being
Node of
((h . t) | nu) such that C1:
(
nu in { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } &
q = nu ^ mu )
;
reconsider inu =
<*i*> ^ nu as
Node of
(o -term p) by B3, BA, TREES_4:11;
take
inu
;
( inu in I & ex mu being Node of ((h . (o -term p)) | inu) st xi = inu ^ mu )consider xi1 being
Node of
t such that C2:
(
nu = xi1 & ex
s being
SortSymbol of
S ex
x being
Element of
X . s st
t . xi1 = [x,s] )
by C1;
ex
s being
SortSymbol of
S ex
x being
Element of
X . s st
(o -term p) . inu = [x,s]
by C2, B3, BA, TREES_4:12;
hence
inu in I
by A4;
ex mu being Node of ((h . (o -term p)) | inu) st xi = inu ^ mu
(
h . t = (h . (o -term p)) | <*i*> &
inu in dom (o -term p) &
dom (o -term p) c= dom (h . (o -term p)) )
by B3, A6, B6, Th135, TREES_4:def 4;
then reconsider mu =
mu as
Node of
((h . (o -term p)) | inu) by TREES_9:3;
take
mu
;
xi = inu ^ muthus
xi = inu ^ mu
by B3, C1, FINSEQ_1:32;
verum end; end; end; end;
end;
S1[t]
from MSAFREE5:sch 2(A1, A3);
hence
( I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } implies for xi being Node of (h . t) holds
( xi in (dom t) \ I or ex nu being Element of dom t st
( nu in I & ex mu being Node of ((h . t) | nu) st xi = nu ^ mu ) ) )
; verum