:: 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: for n being Element of NAT
for x being set
for p being FinSequence of x st n < len p holds
p . (n + 1) in x
let n be Element of NAT ; :: thesis: for x being set
for p being FinSequence of x st n < len p holds
p . (n + 1) in x

let x be set ; :: thesis: for p being FinSequence of x st n < len p holds
p . (n + 1) in x

let p be FinSequence of x; :: thesis: ( n < len p implies p . (n + 1) in x )
n >= 0 by NAT_1:2;
then A1: n + 1 >= 0 + 1 by XREAL_1:7;
assume n < len p ; :: thesis: p . (n + 1) in x
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: verum
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
coherence
TS (DTConMSA V) is Subset of (FinTrees the carrier of (DTConMSA V))
;
;
end;

:: deftheorem Def1 defines -Terms MSATERM:def 1 :
for S being non empty non void ManySortedSign
for V being ManySortedSet of the carrier of S holds S -Terms V = TS (DTConMSA V);

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
coherence
not S -Terms V is empty
;
;
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
Sym (o,V) is NonTerminal of (DTConMSA V)
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
ex b1 being FinSequence of S -Terms V st b1 is SubtreeSeq of sy
proof end;
end;

:: deftheorem Def2 defines ArgumentSeq MSATERM:def 2 :
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for sy being NonTerminal of (DTConMSA V)
for b4 being FinSequence of S -Terms V holds
( b4 is ArgumentSeq of sy iff b4 is SubtreeSeq of sy );

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: for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for x being set holds
( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )
let S be non empty non void ManySortedSign ; :: thesis: for V being V2() ManySortedSet of the carrier of S
for x being set holds
( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )

let V be V2() ManySortedSet of the carrier of S; :: thesis: for x being set holds
( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )

let x be set ; :: thesis: ( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )

set X = V;
set G = DTConMSA V;
A1: Terminals (DTConMSA V) = Union (coprod V) by MSAFREE:6;
hereby :: thesis: for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V)
assume x in Terminals (DTConMSA V) ; :: thesis: ex s being SortSymbol of S ex v being Element of V . s st x = [v,s]
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: verum
end;
let s be SortSymbol of S; :: thesis: for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V)

let a be Element of V . s; :: thesis: ( x = [a,s] implies x in Terminals (DTConMSA V) )
assume x = [a,s] ; :: thesis: x in Terminals (DTConMSA V)
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: verum
end;

Lm4: now :: thesis: 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 x being set holds
( ( not x in Terminals (DTConMSA ( the Sorts of A (\/) V)) or 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] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) ) ) )
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over S
for V being V2() ManySortedSet of the carrier of S
for x being set holds
( ( not x in Terminals (DTConMSA ( the Sorts of A (\/) V)) or 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] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) ) ) )

let A be MSAlgebra over S; :: thesis: for V being V2() ManySortedSet of the carrier of S
for x being set holds
( ( not x in Terminals (DTConMSA ( the Sorts of A (\/) V)) or 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] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) ) ) )

let V be V2() ManySortedSet of the carrier of S; :: thesis: for x being set holds
( ( not x in Terminals (DTConMSA ( the Sorts of A (\/) V)) or 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] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) ) ) )

let x be set ; :: thesis: ( ( not x in Terminals (DTConMSA ( the Sorts of A (\/) V)) or 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] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) ) ) )

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: for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) )
assume x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ; :: thesis: ( 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] )

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: verum
end;
let s be SortSymbol of S; :: thesis: ( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V)) ) )

A7: ( the Sorts of A (\/) V) . s = ( the Sorts of A . s) \/ (V . s) by PBOOLE:def 4;
hereby :: thesis: for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA ( the Sorts of A (\/) V))
let a be set ; :: thesis: ( a in the Sorts of A . s & x = [a,s] implies x in Terminals (DTConMSA ( the Sorts of A (\/) V)) )
assume a in the Sorts of A . s ; :: thesis: ( x = [a,s] implies x in Terminals (DTConMSA ( the Sorts of A (\/) V)) )
then A8: a in ( the Sorts of A (\/) V) . s by A7, XBOOLE_0:def 3;
assume x = [a,s] ; :: thesis: x in Terminals (DTConMSA ( the Sorts of A (\/) V))
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: verum
end;
let a be Element of V . s; :: thesis: ( x = [a,s] implies x in Terminals (DTConMSA ( the Sorts of A (\/) V)) )
assume A9: x = [a,s] ; :: thesis: x in Terminals (DTConMSA ( the Sorts of A (\/) V))
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: verum
end;

Lm5: now :: thesis: for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for x being set holds
( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] )
let S be non empty non void ManySortedSign ; :: thesis: for V being V2() ManySortedSet of the carrier of S
for x being set holds
( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] )

let V be V2() ManySortedSet of the carrier of S; :: thesis: for x being set holds
( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] )

set G = DTConMSA V;
let x be set ; :: thesis: ( x is NonTerminal of (DTConMSA V) iff x in [: the carrier' of S,{ the carrier of S}:] )
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: verum
end;

scheme :: MSATERM:sch 1
TermInd{ F1() -> non empty non void ManySortedSign , F2() -> V2() ManySortedSet of the carrier of F1(), P1[ set ] } :
for t being Term of F1(),F2() holds P1[t]
provided
A1: for s being SortSymbol of F1()
for v being Element of F2() . s holds P1[ root-tree [v,s]] and
A2: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) st ( for t being Term of F1(),F2() st t in rng p holds
P1[t] ) holds
P1[[o, the carrier of F1()] -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{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> V2() ManySortedSet of the carrier of F1(), P1[ set ] } :
for t being c-Term of F2(),F3() holds P1[t]
provided
A1: for s being SortSymbol of F1()
for x being Element of the Sorts of F2() . s holds P1[ root-tree [x,s]] and
A2: for s being SortSymbol of F1()
for v being Element of F3() . s holds P1[ root-tree [v,s]] and
A3: for o being OperSymbol of F1()
for p being ArgumentSeq of o,F2(),F3() st ( for t being c-Term of F2(),F3() st t in rng p holds
P1[t] ) holds
P1[(Sym (o,( the Sorts of F2() (\/) F3()))) -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
t . p is Symbol of (DTConMSA V)
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
for b1 being Term of S,V holds b1 is finite
;
end;

Lm6: now :: thesis: for G being non empty with_terminals with_nonterminals DTConstrStr
for s being Symbol of G holds
( ( s is Terminal of G or s is NonTerminal of G ) & ( not s is Terminal of G or not s is NonTerminal of G ) )
let G be non empty with_terminals with_nonterminals DTConstrStr ; :: thesis: for s being Symbol of G holds
( ( s is Terminal of G or s is NonTerminal of G ) & ( not s is Terminal of G or not s is NonTerminal of G ) )

let s be Symbol of G; :: thesis: ( ( s is Terminal of G or s is NonTerminal of G ) & ( not s is Terminal of G or not s is NonTerminal of G ) )
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: ( not s is Terminal of G or not s is NonTerminal of G )
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: verum
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
coherence
root-tree [x,s] is c-Term of A,V
;
by Th6;
end;

:: deftheorem defines -term MSATERM:def 3 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being V2() ManySortedSet of the carrier of S
for s being SortSymbol of S
for x being Element of the Sorts of A . s holds x -term (A,V) = root-tree [x,s];

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
coherence
root-tree [v,s] is c-Term of A,V
;
by Th8;
end;

:: deftheorem defines -term MSATERM:def 4 :
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 s being SortSymbol of S
for v being Element of V . s holds v -term A = root-tree [v,s];

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
sy -tree p is Term of S,V
proof end;
end;

scheme :: MSATERM:sch 3
TermInd2{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra over F1(), F3() -> V2() ManySortedSet of the carrier of F1(), P1[ set ] } :
for t being c-Term of F2(),F3() holds P1[t]
provided
A1: for s being SortSymbol of F1()
for x being Element of the Sorts of F2() . s holds P1[x -term (F2(),F3())] and
A2: for s being SortSymbol of F1()
for v being Element of F3() . s holds P1[v -term F2()] and
A3: for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,( the Sorts of F2() (\/) F3())) st ( for t being c-Term of F2(),F3() st t in rng p holds
P1[t] ) holds
P1[(Sym (o,( the Sorts of F2() (\/) F3()))) -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
ex b1 being SortSymbol of S st t in FreeSort (V,b1)
by Th11;
uniqueness
for b1, b2 being SortSymbol of S st t in FreeSort (V,b1) & t in FreeSort (V,b2) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines the_sort_of MSATERM:def 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 b4 being SortSymbol of S holds
( b4 = the_sort_of t iff t in FreeSort (V,b4) );

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
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 = root-tree [x,s] holds
the_sort_of t = s
proof end;

theorem :: MSATERM:16
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 = root-tree [v,s] holds
the_sort_of t = s
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
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 the_sort_of (v -term A) = s
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
ex b1 being Term of S,V st b1 . {} in [: the carrier' of S,{ the carrier of S}:]
proof end;
end;

:: deftheorem defines CompoundTerm MSATERM:def 6 :
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for b3 being Term of S,V holds
( b3 is CompoundTerm of S,V iff b3 . {} in [: the carrier' of S,{ the carrier of S}:] );

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
ex b1 being non empty Subset of (S -Terms V) ex t being CompoundTerm of S,V st t in b1
proof end;
end;

:: deftheorem defines SetWithCompoundTerm MSATERM:def 7 :
for S being non empty non void ManySortedSign
for V being V2() ManySortedSet of the carrier of S
for b3 being non empty Subset of (S -Terms V) holds
( b3 is SetWithCompoundTerm of S,V iff ex t being CompoundTerm of S,V st t in b3 );

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
t | p is Term of S,V
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
ex b1 being V2() ManySortedSet of the carrier of S st b1 misses the Sorts of A
proof end;
end;

:: deftheorem Def8 defines Variables MSATERM:def 8 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for b3 being V2() ManySortedSet of the carrier of S holds
( b3 is Variables of A iff b3 misses the Sorts of A );

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 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being V2() ManySortedSet of the carrier of S
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for vt being finite DecoratedTree holds
( vt is_an_evaluation_of t,f iff ( 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)) ) ) ) ) );

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
ex b1 being Element of the Sorts of A . (the_sort_of t) ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & b1 = vt . {} )
proof end;
uniqueness
for b1, b2 being Element of the Sorts of A . (the_sort_of t) st ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & b1 = vt . {} ) & ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & b2 = vt . {} ) holds
b1 = b2
by Th37;
end;

:: deftheorem Def10 defines @ MSATERM:def 10 :
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 b6 being Element of the Sorts of A . (the_sort_of t) holds
( b6 = t @ f iff ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & b6 = vt . {} ) );

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;