let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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);
A1:
now let s be
SortSymbol of
S;
:: thesis: 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;
:: thesis: S1[x -term A,V]thus
S1[
x -term A,
V]
:: thesis: verumproof
set t =
x -term A,
V;
let vt be
finite DecoratedTree;
:: thesis: ( vt is_an_evaluation_of x -term A,V,f implies vt . {} in the Sorts of A . (the_sort_of (x -term A,V)) )
assume A2:
vt is_an_evaluation_of x -term A,
V,
f
;
:: thesis: 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 A2, Th37;
then
(
vt . {} = x &
s = the_sort_of (x -term A,V) )
by Th15, TREES_4:3;
hence
vt . {} in the
Sorts of
A . (the_sort_of (x -term A,V))
;
:: thesis: verum
end; end;
A5:
now let o be
OperSymbol of
S;
:: thesis: 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;
:: thesis: ( ( 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 A6:
for
t being
c-Term of
A,
V st
t in rng p holds
S1[
t]
;
:: thesis: S1[(Sym o,(the Sorts of A \/ V)) -tree p]thus
S1[
(Sym o,(the Sorts of A \/ V)) -tree p]
:: thesis: verumproof
set t =
(Sym o,(the Sorts of A \/ V)) -tree p;
let vt be
finite DecoratedTree;
:: thesis: ( 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)) )
assume
vt is_an_evaluation_of (Sym o,(the Sorts of A \/ V)) -tree p,
f
;
:: thesis: 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;
A11:
(
dom (the Sorts of A * the ResultSort of S) = the
carrier' of
S &
dom ((the Sorts of A # ) * the Arity of S) = the
carrier' of
S &
o in the
carrier' of
S )
by PARTFUN1:def 4;
A12:
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 A11, 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
;
now A13:
(
dom the
Sorts of
A = the
carrier of
S &
rng (the_arity_of o) c= the
carrier of
S )
by FINSEQ_1:def 4, PARTFUN1:def 4;
A14:
dom (roots q) = dom q
by TREES_3:def 18;
hence A15:
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 A13, RELAT_1:46
;
:: thesis: 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 ;
:: thesis: ( 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 A16:
x in dom (the Sorts of A * (the_arity_of o))
;
:: thesis: (roots q) . x in (the Sorts of A * (the_arity_of o)) . xthen consider i being
Element of
NAT such that A17:
(
x = i + 1 &
i < len q )
by A14, A15, Lm1;
consider T being
DecoratedTree such that A18:
(
T = q . (i + 1) &
(roots q) . (i + 1) = T . {} )
by A14, A15, A16, A17, TREES_3:def 18;
reconsider t =
p . (i + 1) as
c-Term of
A,
V by A7, A17, Lm2;
A19:
i + 1
in dom p
by A7, A17, Lm9;
then consider vt being
finite DecoratedTree such that A20:
(
vt = q . (i + 1) &
vt is_an_evaluation_of t,
f )
by A9;
A21:
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 A19, Lm8;
t in rng p
by A7, A17, Lm9;
then
vt . {} in the
Sorts of
A . (the_sort_of t)
by A6, A20;
hence
(roots q) . x in (the Sorts of A * (the_arity_of o)) . x
by A16, A17, A18, A20, A21, FUNCT_1:22;
:: thesis: 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
roots q in (the Sorts of A # ) . (the Arity of S . o)
by MSUALG_1:def 6;
then
roots q in ((the Sorts of A # ) * the Arity of S) . o
by A11, FUNCT_1:22;
then
(
roots q in Args o,
A &
Den o,
A is
Function of
(Args o,A),
(Result o,A) )
by MSUALG_1:def 9;
hence
vt . {} in the
Sorts of
A . (the_sort_of ((Sym o,(the Sorts of A \/ V)) -tree p))
by A10, A12, FUNCT_2:7;
:: thesis: verum
end; end;
for t being c-Term of A,V holds S1[t]
from MSATERM:sch 3(A1, A3, A5);
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)
; :: thesis: verum