let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra of S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V,the Sorts of A
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
let A be non-empty MSAlgebra of S; for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V,the Sorts of A
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
let V be Variables of A; for t being c-Term of A,V
for f being ManySortedFunction of V,the Sorts of A
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
let t be c-Term of A,V; for f being ManySortedFunction of V,the Sorts of A
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
let f be ManySortedFunction of V,the Sorts of A; for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
defpred S1[ c-Term of A,V] means for vt being finite DecoratedTree st vt is_an_evaluation_of $1,f holds
vt . {} in the Sorts of A . (the_sort_of $1);
A4:
now let o be
OperSymbol of
S;
for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds
S1[t] ) holds
S1[(Sym o,(the Sorts of A \/ V)) -tree p]let p be
ArgumentSeq of
o,
A,
V;
( ( for t being c-Term of A,V st t in rng p holds
S1[t] ) implies S1[(Sym o,(the Sorts of A \/ V)) -tree p] )assume A5:
for
t being
c-Term of
A,
V st
t in rng p holds
S1[
t]
;
S1[(Sym o,(the Sorts of A \/ V)) -tree p]thus
S1[
(Sym o,(the Sorts of A \/ V)) -tree p]
verumproof
let vt be
finite DecoratedTree;
( vt is_an_evaluation_of (Sym o,(the Sorts of A \/ V)) -tree p,f implies vt . {} in the Sorts of A . (the_sort_of ((Sym o,(the Sorts of A \/ V)) -tree p)) )
set t =
(Sym o,(the Sorts of A \/ V)) -tree p;
A6:
dom (the Sorts of A * the ResultSort of S) = the
carrier' of
S
by PARTFUN1:def 4;
assume
vt is_an_evaluation_of (Sym o,(the Sorts of A \/ V)) -tree p,
f
;
vt . {} in the Sorts of A . (the_sort_of ((Sym o,(the Sorts of A \/ V)) -tree p))
then consider q being
DTree-yielding FinSequence such that A7:
len q = len p
and A8:
vt = ((Den o,A) . (roots q)) -tree q
and A9:
for
i being
Nat for
t being
c-Term of
A,
V st
i in dom p &
t = p . i holds
ex
vt being
finite DecoratedTree st
(
vt = q . i &
vt is_an_evaluation_of t,
f )
by Th35;
A10:
vt . {} = (Den o,A) . (roots q)
by A8, TREES_4:def 4;
now A11:
rng (the_arity_of o) c= the
carrier of
S
by FINSEQ_1:def 4;
A12:
dom the
Sorts of
A = the
carrier of
S
by PARTFUN1:def 4;
A13:
dom (roots q) = dom q
by TREES_3:def 18;
hence A14:
dom (roots q) =
Seg (len q)
by FINSEQ_1:def 3
.=
Seg (len (the_arity_of o))
by A7, Lm8
.=
dom (the_arity_of o)
by FINSEQ_1:def 3
.=
dom (the Sorts of A * (the_arity_of o))
by A12, A11, RELAT_1:46
;
for x being set st x in dom (the Sorts of A * (the_arity_of o)) holds
(roots q) . x in (the Sorts of A * (the_arity_of o)) . xlet x be
set ;
( x in dom (the Sorts of A * (the_arity_of o)) implies (roots q) . x in (the Sorts of A * (the_arity_of o)) . x )assume A15:
x in dom (the Sorts of A * (the_arity_of o))
;
(roots q) . x in (the Sorts of A * (the_arity_of o)) . xthen consider i being
Element of
NAT such that A16:
x = i + 1
and A17:
i < len q
by A13, A14, Lm1;
A18:
ex
T being
DecoratedTree st
(
T = q . (i + 1) &
(roots q) . (i + 1) = T . {} )
by A13, A14, A15, A16, TREES_3:def 18;
i + 1
in dom p
by A7, A17, Lm9;
then A19:
ex
t being
c-Term of
A,
V st
(
t = p . (i + 1) &
t = p /. (i + 1) &
the_sort_of t = (the_arity_of o) . (i + 1) &
the_sort_of t = (the_arity_of o) /. (i + 1) )
by Lm8;
reconsider t =
p . (i + 1) as
c-Term of
A,
V by A7, A17, Lm2;
consider vt being
finite DecoratedTree such that A20:
vt = q . (i + 1)
and A21:
vt is_an_evaluation_of t,
f
by A7, A9, A17, Lm9;
vt . {} in the
Sorts of
A . (the_sort_of t)
by A5, A7, A17, A21, Lm9;
hence
(roots q) . x in (the Sorts of A * (the_arity_of o)) . x
by A15, A16, A18, A20, A19, FUNCT_1:22;
verum end;
then
roots q in product (the Sorts of A * (the_arity_of o))
by CARD_3:18;
then
roots q in (the Sorts of A # ) . (the_arity_of o)
by PBOOLE:def 19;
then A22:
roots q in (the Sorts of A # ) . (the Arity of S . o)
by MSUALG_1:def 6;
dom ((the Sorts of A # ) * the Arity of S) = the
carrier' of
S
by PARTFUN1:def 4;
then
roots q in ((the Sorts of A # ) * the Arity of S) . o
by A22, FUNCT_1:22;
then A23:
roots q in Args o,
A
by MSUALG_1:def 9;
Result o,
A =
(the Sorts of A * the ResultSort of S) . o
by MSUALG_1:def 10
.=
the
Sorts of
A . (the ResultSort of S . o)
by A6, FUNCT_1:22
.=
the
Sorts of
A . (the_result_sort_of o)
by MSUALG_1:def 7
.=
the
Sorts of
A . (the_sort_of ((Sym o,(the Sorts of A \/ V)) -tree p))
by Th20
;
hence
vt . {} in the
Sorts of
A . (the_sort_of ((Sym o,(the Sorts of A \/ V)) -tree p))
by A10, A23, FUNCT_2:7;
verum
end; end;
A24:
now let s be
SortSymbol of
S;
for x being Element of the Sorts of A . s holds S1[x -term A,V]let x be
Element of the
Sorts of
A . s;
S1[x -term A,V]thus
S1[
x -term A,
V]
verumproof
let vt be
finite DecoratedTree;
( vt is_an_evaluation_of x -term A,V,f implies vt . {} in the Sorts of A . (the_sort_of (x -term A,V)) )
set t =
x -term A,
V;
assume A25:
vt is_an_evaluation_of x -term A,
V,
f
;
vt . {} in the Sorts of A . (the_sort_of (x -term A,V))
root-tree x is_an_evaluation_of x -term A,
V,
f
by Th31;
then
vt = root-tree x
by A25, Th37;
then A26:
vt . {} = x
by TREES_4:3;
s = the_sort_of (x -term A,V)
by Th15;
hence
vt . {} in the
Sorts of
A . (the_sort_of (x -term A,V))
by A26;
verum
end; end;
for t being c-Term of A,V holds S1[t]
from MSATERM:sch 3(A24, A1, A4);
hence
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t)
; verum