let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over 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 over 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 for o being 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 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 2;
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 ( dom (roots q) = dom ( the Sorts of A * (the_arity_of o)) & ( for x being object 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)) . x ) )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 2;
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:27
;
for x being object 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
object ;
( 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:12;
verum end;
then
roots q in product ( the Sorts of A * (the_arity_of o))
by CARD_3:9;
then
roots q in ( the Sorts of A #) . (the_arity_of o)
by FINSEQ_2:def 5;
then A22:
roots q in ( the Sorts of A #) . ( the Arity of S . o)
by MSUALG_1:def 1;
dom (( the Sorts of A #) * the Arity of S) = the
carrier' of
S
by PARTFUN1:def 2;
then
roots q in (( the Sorts of A #) * the Arity of S) . o
by A22, FUNCT_1:12;
then A23:
roots q in Args (
o,
A)
by MSUALG_1:def 4;
Result (
o,
A) =
( the Sorts of A * the ResultSort of S) . o
by MSUALG_1:def 5
.=
the
Sorts of
A . ( the ResultSort of S . o)
by A6, FUNCT_1:12
.=
the
Sorts of
A . (the_result_sort_of o)
by MSUALG_1:def 2
.=
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:5;
verum
end; end;
A24:
now for s being SortSymbol of S
for x being Element of the Sorts of A . s holds S1[x -term (A,V)]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