MSATERM: Terms over many sorted universal algebra

:: Terms over many sorted universal algebra
:: by Grzegorz Bancerek
::
:: Received November 25, 1994
:: Copyright (c) 1994-2021 Association of Mizar Users

Lm1: for n being set
for p being FinSequence st n in dom p holds
ex k being Element of NAT st
( n = k + 1 & k < len p )

proof end;

Lm2: now :: thesis:

let n be Element of NAT ; :: thesis:
let x be set ; :: thesis:
let p be FinSequence of x; :: thesis:
n >= 0 by NAT_1:2;
then A1: n + 1 >= 0 + 1 by XREAL_1:7;
assume n < len p ; :: thesis:
then n + 1 <= len p by NAT_1:13;
then n + 1 in dom p by A1, FINSEQ_3:25;
then A2: p . (n + 1) in rng p by FUNCT_1:def 3;
rng p c= x by FINSEQ_1:def 4;
hence p . (n + 1) in x by A2; :: thesis:

end;

definition

let S be non empty non void ManySortedSign ;
let V be ManySortedSet of the carrier of S;

func S -Terms V -> Subset of (FinTrees the carrier of (DTConMSA V)) equals :Def1: :: MSATERM:def 1
TS (DTConMSA V);

correctness ;

end;

:: deftheorem Def1 defines -Terms MSATERM:def 1 :

registration

let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;

cluster S -Terms V -> non empty ;

correctness ;

end;

definition

let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
mode Term of S,V is Element of S -Terms V;

end;

definition

let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let o be OperSymbol of S;
:: original: Sym
redefine func Sym (o,V) -> NonTerminal of (DTConMSA V);
coherence

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let sy be NonTerminal of (DTConMSA V);

mode ArgumentSeq of sy -> FinSequence of S -Terms V means :Def2: :: MSATERM:def 2
it is SubtreeSeq of sy;

existence

proof end;

end;

:: deftheorem Def2 defines ArgumentSeq MSATERM:def 2 :

theorem Th1: :: MSATERM:1

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence holds
( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )

proof end;

Lm3: now :: thesis:

let S be non empty non void ManySortedSign ; :: thesis:
let V be V2() ManySortedSet of the carrier of S; :: thesis:
let x be set ; :: thesis:
set X = V;
set G = DTConMSA V;
A1: Terminals (DTConMSA V) = Union (coprod V) by MSAFREE:6;

hereby :: thesis:

assume x in Terminals (DTConMSA V) ; :: thesis:
then consider s being object such that
A2: s in dom (coprod V) and
A3: x in (coprod V) . s by A1, CARD_5:2;
reconsider s = s as SortSymbol of S by A2, PARTFUN1:def 2;
(coprod V) . s = coprod (s,V) by MSAFREE:def 3;
then ex a being set st
( a in V . s & x = [a,s] ) by A3, MSAFREE:def 2;
hence ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ; :: thesis:

end;

let s be SortSymbol of S; :: thesis:
let a be Element of V . s; :: thesis:
assume x = [a,s] ; :: thesis:
then x in coprod (s,V) by MSAFREE:def 2;
then A4: x in (coprod V) . s by MSAFREE:def 3;
dom (coprod V) = the carrier of S by PARTFUN1:def 2;
hence x in Terminals (DTConMSA V) by A1, A4, CARD_5:2; :: thesis:

end;

Lm4: now :: thesis:

let S be non empty non void ManySortedSign ; :: thesis:
let A be MSAlgebra over S; :: thesis:
let V be V2() ManySortedSet of the carrier of S; :: thesis:
let x be set ; :: thesis:
set X = the Sorts of A (\/) V;
set G = DTConMSA ( the Sorts of A (\/) V);
A1: dom (coprod ( the Sorts of A (\/) V)) = the carrier of S by PARTFUN1:def 2;
A2: Terminals (DTConMSA ( the Sorts of A (\/) V)) = Union (coprod ( the Sorts of A (\/) V)) by MSAFREE:6;

hereby :: thesis:

assume x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ; :: thesis:
then consider s being object such that
A3: s in dom (coprod ( the Sorts of A (\/) V)) and
A4: x in (coprod ( the Sorts of A (\/) V)) . s by A2, CARD_5:2;
reconsider s = s as SortSymbol of S by A3, PARTFUN1:def 2;
(coprod ( the Sorts of A (\/) V)) . s = coprod (s,( the Sorts of A (\/) V)) by MSAFREE:def 3;
then consider a being set such that
A5: a in ( the Sorts of A (\/) V) . s and
A6: x = [a,s] by A4, MSAFREE:def 2;
( the Sorts of A (\/) V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def 4;
then ( a in the Sorts of A . s or a in V . s ) by A5, XBOOLE_0:def 3;
hence ( ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) by A6; :: thesis:

end;

let s be SortSymbol of S; :: thesis:
A7: ( the Sorts of A (\/) V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def 4;

hereby :: thesis:

let a be set ; :: thesis:
assume a in the Sorts of A . s ; :: thesis:
then A8: a in ( the Sorts of A (\/) V) . s by A7, XBOOLE_0:def 3;
assume x = [a,s] ; :: thesis:
then x in coprod (s,( the Sorts of A (\/) V)) by A8, MSAFREE:def 2;
then x in (coprod ( the Sorts of A (\/) V)) . s by MSAFREE:def 3;
hence x in Terminals (DTConMSA ( the Sorts of A (\/) V)) by A2, A1, CARD_5:2; :: thesis:

end;

let a be Element of V . s; :: thesis:
assume A9: x = [a,s] ; :: thesis:
a in ( the Sorts of A (\/) V) . s by A7, XBOOLE_0:def 3;
then x in coprod (s,( the Sorts of A (\/) V)) by A9, MSAFREE:def 2;
then x in (coprod ( the Sorts of A (\/) V)) . s by MSAFREE:def 3;
hence x in Terminals (DTConMSA ( the Sorts of A (\/) V)) by A2, A1, CARD_5:2; :: thesis:

end;

Lm5: now :: thesis:

let S be non empty non void ManySortedSign ; :: thesis:
let V be V2() ManySortedSet of the carrier of S; :: thesis:
set G = DTConMSA V;
let x be set ; :: thesis:
NonTerminals (DTConMSA V) = [: the carrier' of S,{ the carrier of S}:] by MSAFREE:6;
hence ( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] ) ; :: thesis:

end;

scheme :: MSATERM:sch 1
TermInd{ F₁() -> non empty non void ManySortedSign , F₂() -> V2() ManySortedSet of the carrier of F₁(), P₁[ set ] } :

for t being Term of F₁(),F₂() holds P₁[t]

provided

A1: for s being SortSymbol of F₁()
for v being Element of F₂() . s holds P₁[ root-tree [v,s]] and
A2: for o being OperSymbol of F₁()
for p being ArgumentSeq of Sym (o,F₂()) st ( for t being Term of F₁(),F₂() st t in rng p holds
P₁[t] ) holds
P₁[[o, the carrier of F₁()] -tree p]

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let V be V2() ManySortedSet of the carrier of S;
mode c-Term of A,V is Term of S,( the Sorts of A (\/) V);

end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let V be V2() ManySortedSet of the carrier of S;
let o be OperSymbol of S;
mode ArgumentSeq of o,A,V is ArgumentSeq of Sym (o,( the Sorts of A (\/) V));

end;

scheme :: MSATERM:sch 2
CTermInd{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), F₃() -> V2() ManySortedSet of the carrier of F₁(), P₁[ set ] } :

for t being c-Term of F₂(),F₃() holds P₁[t]

provided

A1: for s being SortSymbol of F₁()
for x being Element of the Sorts of F₂() . s holds P₁[ root-tree [x,s]] and
A2: for s being SortSymbol of F₁()
for v being Element of F₃() . s holds P₁[ root-tree [v,s]] and
A3: for o being OperSymbol of F₁()
for p being ArgumentSeq of o,F₂(),F₃() st ( for t being c-Term of F₂(),F₃() st t in rng p holds
P₁[t] ) holds
P₁[(Sym (o,( the Sorts of F₂() (\/) F₃()))) -tree p]

proof end;

definition

let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let t be Term of S,V;
let p be Node of t;
:: original: .
redefine func t . p -> Symbol of (DTConMSA V);
coherence

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;

cluster -> finite for Element of S -Terms V;

coherence ;

end;

Lm6: now :: thesis:

let G be non empty with_terminals with_nonterminals DTConstrStr ; :: thesis:
let s be Symbol of G; :: thesis:
the carrier of G = (Terminals G) \/ (NonTerminals G) by LANG1:1;
hence ( s is Terminal of G or s is NonTerminal of G ) by XBOOLE_0:def 3; :: thesis:
Terminals G misses NonTerminals G by DTCONSTR:8;
hence ( not s is Terminal of G or not s is NonTerminal of G ) by XBOOLE_0:3; :: thesis:

end;

theorem Th2: :: MSATERM:2

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for t being Term of S,V holds
( ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] )

proof end;

theorem :: MSATERM:3

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V holds
( ex s being SortSymbol of S ex x being set st
( x in the Sorts of A . s & t . {} = [x,s] ) or ex s being SortSymbol of S ex v being Element of V . s st t . {} = [v,s] or t . {} in [: the carrier' of S,{ the carrier of S}:] )

proof end;

theorem Th4: :: MSATERM:4

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is Term of S,V

proof end;

theorem Th5: :: MSATERM:5

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]

proof end;

theorem Th6: :: MSATERM:6

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
root-tree [x,s] is c-Term of A,V

proof end;

theorem :: MSATERM:7

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for x being set st x in the Sorts of A . s & t . {} = [x,s] holds
t = root-tree [x,s]

proof end;

theorem Th8: :: MSATERM:8

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is c-Term of A,V

proof end;

theorem :: MSATERM:9

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for t being c-Term of A,V
for s being SortSymbol of S
for v being Element of V . s st t . {} = [v,s] holds
t = root-tree [v,s]

proof end;

theorem Th10: :: MSATERM:10

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for t being Term of S,V
for o being OperSymbol of S st t . {} = [o, the carrier of S] holds
ex a being ArgumentSeq of Sym (o,V) st t = [o, the carrier of S] -tree a

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let V be V2() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
let x be Element of the Sorts of A . s;

func x -term (A,V) -> c-Term of A,V equals :: MSATERM:def 3
root-tree [x,s];

correctness by Th6;

end;

:: deftheorem defines -term MSATERM:def 3 :

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let V be V2() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
let v be Element of V . s;

func v -term A -> c-Term of A,V equals :: MSATERM:def 4
root-tree [v,s];

correctness by Th8;

end;

:: deftheorem defines -term MSATERM:def 4 :

definition

let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let sy be NonTerminal of (DTConMSA V);
let p be ArgumentSeq of sy;
:: original: -tree
redefine func sy -tree p -> Term of S,V;
coherence

proof end;

end;

scheme :: MSATERM:sch 3
TermInd2{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), F₃() -> V2() ManySortedSet of the carrier of F₁(), P₁[ set ] } :

for t being c-Term of F₂(),F₃() holds P₁[t]

provided

A1: for s being SortSymbol of F₁()
for x being Element of the Sorts of F₂() . s holds P₁[x -term (F₂(),F₃())] and
A2: for s being SortSymbol of F₁()
for v being Element of F₃() . s holds P₁[v -term F₂()] and
A3: for o being OperSymbol of F₁()
for p being ArgumentSeq of Sym (o,( the Sorts of F₂() (\/) F₃())) st ( for t being c-Term of F₂(),F₃() st t in rng p holds
P₁[t] ) holds
P₁[(Sym (o,( the Sorts of F₂() (\/) F₃()))) -tree p]

proof end;

theorem Th11: :: MSATERM:11

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for t being Term of S,V ex s being SortSymbol of S st t in FreeSort (V,s)

proof end;

theorem :: MSATERM:12

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeSort (V,s) c= S -Terms V ;

theorem :: MSATERM:13

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S holds S -Terms V = Union (FreeSort V)

proof end;

Lm7: for x being set holds not x in x
;

definition

let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let t be Term of S,V;

func the_sort_of t -> SortSymbol of S means :Def5: :: MSATERM:def 5
t in FreeSort (V,it);

existence by Th11;
uniqueness

proof end;

end;

:: deftheorem Def5 defines the_sort_of MSATERM:def 5 :

theorem Th14: :: MSATERM:14

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for t being Term of S,V
for s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
the_sort_of t = s

proof end;

theorem Th15: :: MSATERM:15

proof end;

theorem :: MSATERM:16

proof end;

theorem Th17: :: MSATERM:17

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for t being Term of S,V
for o being OperSymbol of S st t . {} = [o, the carrier of S] holds
the_sort_of t = the_result_sort_of o

proof end;

theorem :: MSATERM:18

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds the_sort_of (x -term (A,V)) = s by Th15;

theorem Th19: :: MSATERM:19

proof end;

theorem Th20: :: MSATERM:20

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,V) holds the_sort_of ((Sym (o,V)) -tree p) = the_result_sort_of o

proof end;

theorem Th21: :: MSATERM:21

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence of S -Terms V holds
( a is ArgumentSeq of Sym (o,V) iff Sym (o,V) ==> roots a )

proof end;

Lm8: for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )

proof end;

theorem Th22: :: MSATERM:22

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
a . i is Term of S,V ) )

proof end;

theorem :: MSATERM:23

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V)
for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
( t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i )

proof end;

theorem Th24: :: MSATERM:24

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) . i ) or for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & the_sort_of t = (the_arity_of o) /. i ) ) holds
a is ArgumentSeq of Sym (o,V)

proof end;

theorem :: MSATERM:25

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being FinSequence of S -Terms V st ( len a = len (the_arity_of o) or dom a = dom (the_arity_of o) ) & ( for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) . i or for i being Nat st i in dom a holds
for t being Term of S,V st t = a . i holds
the_sort_of t = (the_arity_of o) /. i ) holds
a is ArgumentSeq of Sym (o,V)

proof end;

theorem Th26: :: MSATERM:26

for S being non empty non void ManySortedSign
for V1, V2 being V2() ManySortedSet of the carrier of S st V1 c= V2 holds
for t being Term of S,V1 holds t is Term of S,V2

proof end;

theorem :: MSATERM:27

for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for V being V2() ManySortedSet of the carrier of S
for t being Term of S,V holds t is c-Term of A,V by Th26, PBOOLE:14;

definition

let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;

mode CompoundTerm of S,V -> Term of S,V means :: MSATERM:def 6
it . {} in [: the carrier' of S,{ the carrier of S}:];

existence

proof end;

end;

:: deftheorem defines CompoundTerm MSATERM:def 6 :

definition

let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;

mode SetWithCompoundTerm of S,V -> non empty Subset of (S -Terms V) means :: MSATERM:def 7
ex t being CompoundTerm of S,V st t in it;

existence

proof end;

end;

:: deftheorem defines SetWithCompoundTerm MSATERM:def 7 :

theorem :: MSATERM:28

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for t being Term of S,V st not t is root holds
t is CompoundTerm of S,V

proof end;

Lm9: for n being Element of NAT
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )

proof end;

theorem Th29: :: MSATERM:29

for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for t being Term of S,V
for p being Node of t holds t | p is Term of S,V

proof end;

definition

let S be non empty non void ManySortedSign ;
let V be V2() ManySortedSet of the carrier of S;
let t be Term of S,V;
let p be Node of t;
:: original: |
redefine func t | p -> Term of S,V;
coherence by Th29;

end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;

mode Variables of A -> V2() ManySortedSet of the carrier of S means :Def8: :: MSATERM:def 8
it misses the Sorts of A;

existence

proof end;

end;

:: deftheorem Def8 defines Variables MSATERM:def 8 :

theorem Th30: :: MSATERM:30

for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for V being Variables of A
for s being SortSymbol of S
for x being set st x in the Sorts of A . s holds
for v being Element of V . s holds x <> v

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let V be V2() ManySortedSet of the carrier of S;
let t be c-Term of A,V;
let f be ManySortedFunction of V, the Sorts of A;
let vt be finite DecoratedTree;

pred vt is_an_evaluation_of t,f means :: MSATERM:def 9
( dom vt = dom t & ( for p being Node of vt holds
( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
vt . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
vt . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
vt . p = (Den (o,A)) . (succ (vt,p)) ) ) ) );

end;

:: deftheorem defines is_an_evaluation_of MSATERM:def 9 :

theorem Th31: :: MSATERM:31

for S being 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 s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f

proof end;

theorem Th32: :: MSATERM:32

for S being 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 s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
root-tree ((f . s) . v) is_an_evaluation_of t,f

proof end;

theorem Th33: :: MSATERM:33

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )

proof end;

theorem Th34: :: MSATERM:34

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f

proof end;

theorem Th35: :: MSATERM:35

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( 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 ) ) )

proof end;

theorem Th36: :: MSATERM:36

for S being 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 ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f

proof end;

theorem Th37: :: MSATERM:37

for S being 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 e1, e2 being finite DecoratedTree st e1 is_an_evaluation_of t,f & e2 is_an_evaluation_of t,f holds
e1 = e2

proof end;

theorem Th38: :: MSATERM:38

for S being 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)

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let V be Variables of A;
let t be c-Term of A,V;
let f be ManySortedFunction of V, the Sorts of A;

func t @ f -> Element of the Sorts of A . (the_sort_of t) means :Def10: :: MSATERM:def 10
ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & it = vt . {} );

existence

proof end;

uniqueness by Th37;

end;

:: deftheorem Def10 defines @ MSATERM:def 10 :

theorem Th39: :: MSATERM:39

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
t @ f = vt . {}

proof end;

theorem :: MSATERM:40

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for t being c-Term of A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
for p being Node of t holds vt . p = (t | p) @ f

proof end;

theorem :: MSATERM:41

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds (x -term (A,V)) @ f = x

proof end;

theorem :: MSATERM:42

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for s being SortSymbol of S
for v being Element of V . s holds (v -term A) @ f = (f . s) . v

proof end;

theorem :: MSATERM:43

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for q being FinSequence st len q = len p & ( for i being Nat st i in dom p holds
for t being c-Term of A,V st t = p . i holds
q . i = t @ f ) holds
((Sym (o,( the Sorts of A (\/) V))) -tree p) @ f = (Den (o,A)) . q

proof end;