:: MSATERM semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for n being set
for p being FinSequence st n in dom p holds
ex k being Nat st
( n = k + 1 & k < len p )
proof end;

Lm2: now
let n be 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 )
assume A1: n < len p ; :: thesis: p . (n + 1) in x
n >= 0 by NAT_1:18;
then ( n + 1 >= 0 + 1 & n + 1 <= len p ) by A1, NAT_1:38, XREAL_1:9;
then n + 1 in dom p by FINSEQ_3:27;
then A2: p . (n + 1) in rng p by FUNCT_1:def 5;
rng p c= x by FINSEQ_1:def 4;
hence p . (n + 1) in x by A2; :: thesis: verum
end;

registration
let I be non empty set ;
let X be V3 ManySortedSet of I;
let i be Element of I;
cluster X . i -> non empty ;
coherence
not X . i is empty
;
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 V3 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 V3 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 V3 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 V3 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 V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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
let S be non empty non void ManySortedSign ; :: thesis: for V being V3 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 V3 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;
A2: dom (coprod V) = the carrier of S by PBOOLE:def 3;
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 set such that
A3: ( s in dom (coprod V) & x in (coprod V) . s ) by A1, CARD_5:10;
reconsider s = s as SortSymbol of S by A3, PBOOLE:def 3;
(coprod V) . s = coprod s,V by MSAFREE:def 3;
then consider a being set such that
A4: ( a in V . s & x = [a,s] ) by A3, MSAFREE:def 2;
thus ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] by A4; :: 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 x in (coprod V) . s by MSAFREE:def 3;
hence x in Terminals (DTConMSA V) by A1, A2, CARD_5:10; :: thesis: verum
end;

Lm4: now
let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of S
for V being V3 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 of S; :: thesis: for V being V3 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 V3 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: Terminals (DTConMSA (the Sorts of A \/ V)) = Union (coprod (the Sorts of A \/ V)) by MSAFREE:6;
A2: dom (coprod (the Sorts of A \/ V)) = the carrier of S by PBOOLE:def 3;
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 set such that
A3: ( s in dom (coprod (the Sorts of A \/ V)) & x in (coprod (the Sorts of A \/ V)) . s ) by A1, CARD_5:10;
reconsider s = s as SortSymbol of S by A3, PBOOLE:def 3;
(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
A4: ( a in (the Sorts of A \/ V) . s & x = [a,s] ) by A3, MSAFREE:def 2;
(the Sorts of A \/ V) . s = (the Sorts of A . s) \/ (V . s) by PBOOLE:def 7;
then ( a in the Sorts of A . s or a in V . s ) by A4, XBOOLE_0:def 2;
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 A4; :: 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)) ) )

A5: (the Sorts of A \/ V) . s = (the Sorts of A . s) \/ (V . s) by PBOOLE:def 7;
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 A6: a in the Sorts of A . s ; :: thesis: ( x = [a,s] implies x in Terminals (DTConMSA (the Sorts of A \/ V)) )
assume A7: x = [a,s] ; :: thesis: x in Terminals (DTConMSA (the Sorts of A \/ V))
a in (the Sorts of A \/ V) . s by A5, A6, XBOOLE_0:def 2;
then x in coprod s,(the Sorts of A \/ V) by A7, 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 A1, A2, CARD_5:10; :: 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 A8: x = [a,s] ; :: thesis: x in Terminals (DTConMSA (the Sorts of A \/ V))
a in (the Sorts of A \/ V) . s by A5, XBOOLE_0:def 2;
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 A1, A2, CARD_5:10; :: thesis: verum
end;

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

let V be V3 ManySortedSet of the carrier of S; :: thesis: for x being set holds
( x is NonTerminal of (DTConMSA V) iff x in [:the OperSymbols 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 OperSymbols of S,{the carrier of S}:] )
NonTerminals (DTConMSA V) = [:the OperSymbols of S,{the carrier of S}:] by MSAFREE:6;
hence ( x is NonTerminal of (DTConMSA V) iff x in [:the OperSymbols of S,{the carrier of S}:] ) ; :: thesis: verum
end;

scheme :: MSATERM:sch 1
TermInd{ F1() -> non empty non void ManySortedSign , F2() -> V3 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 of S;
let V be V3 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 of S;
let V be V3 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 of F1(), F3() -> V3 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 V3 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 V3 ManySortedSet of the carrier of S;
cluster -> finite Element of S -Terms V;
coherence
for b1 being Term of S,V holds b1 is finite
;
end;

Lm6: now
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 2; :: 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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 OperSymbols of S,{the carrier of S}:] )
proof end;

theorem :: MSATERM:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of 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 OperSymbols of S,{the carrier of S}:] )
proof end;

theorem Th4: :: MSATERM:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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 of S;
let V be V3 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 of S
for V being V3 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 of S;
let V be V3 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 of S
for V being V3 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 V3 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 of F1(), F3() -> V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeSort V,s c= S -Terms V ;

theorem :: MSATERM:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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 V3 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 V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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 Th18: :: MSATERM:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being non-empty MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 ManySortedSet of the carrier of S
for A being MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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 V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V1, V2 being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for V being V3 ManySortedSet of the carrier of S
for t being Term of S,V holds t is c-Term of A,V
proof end;

definition
let S be non empty non void ManySortedSign ;
let V be V3 ManySortedSet of the carrier of S;
mode CompoundTerm of S,V -> Term of S,V means :: MSATERM:def 6
it . {} in [:the OperSymbols of S,{the carrier of S}:];
existence
ex b1 being Term of S,V st b1 . {} in [:the OperSymbols 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 V3 ManySortedSet of the carrier of S
for b3 being Term of S,V holds
( b3 is CompoundTerm of S,V iff b3 . {} in [:the OperSymbols of S,{the carrier of S}:] );

definition
let S be non empty non void ManySortedSign ;
let V be V3 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 V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for V being V3 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 V3 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 of S;
mode Variables of A -> V3 ManySortedSet of the carrier of S means :Def8: :: MSATERM:def 8
it misses the Sorts of A;
existence
ex b1 being V3 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 of S
for b3 being V3 ManySortedSet of the carrier of S holds
( b3 is Variables of A iff b3 misses the Sorts of A );

theorem Th30: :: MSATERM:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being MSAlgebra of 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 of S;
let V be V3 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 :Def9: :: 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 Def9 defines is_an_evaluation_of MSATERM:def 9 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for V being V3 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being 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 ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
proof end;

theorem Th37: :: MSATERM:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being 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)
proof end;

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of 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 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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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;