:: MSATERM semantic presentation

Lemma1: for b1 being set
for b2 being FinSequence st b1 in dom b2 holds
ex b3 being Nat st
( b1 = b3 + 1 & b3 < len b2 )
proof end;

E2: now
let c1 be Nat;
let c2 be set ;
let c3 be FinSequence of c2;
assume E3: c1 < len c3 ;
c1 >= 0 by NAT_1:18;
then ( c1 + 1 >= 0 + 1 & c1 + 1 <= len c3 ) by E3, NAT_1:38, XREAL_1:9;
then c1 + 1 in dom c3 by FINSEQ_3:27;
then E4: c3 . (c1 + 1) in rng c3 by FUNCT_1:def 5;
rng c3 c= c2 by FINSEQ_1:def 4;
hence c3 . (c1 + 1) in c2 by E4;
end;

registration
let c1 be non empty set ;
let c2 be V3 ManySortedSet of c1;
let c3 be Element of c1;
cluster a2 . a3 -> non empty ;
coherence
not c2 . c3 is empty ;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be ManySortedSet of the carrier of c1;
func c1 -Terms c2 -> Subset of (FinTrees the carrier of (DTConMSA a2)) equals :Def1: :: MSATERM:def 1
 TS (DTConMSA a2);
correctness
coherence
TS (DTConMSA c2) is Subset of (FinTrees the carrier of (DTConMSA c2));
;
end;

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

registration
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
cluster a1 -Terms a2 -> non empty ;
correctness
coherence
not c1 -Terms c2 is empty;
;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
mode Term of a1,a2 is Element of a1 -Terms a2;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
let c3 be OperSymbol of c1;
redefine func Sym as Sym c3,c2 -> NonTerminal of (DTConMSA a2);
coherence
Sym c3,c2 is NonTerminal of (DTConMSA c2)
proof end;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
let c3 be NonTerminal of (DTConMSA c2);
mode ArgumentSeq of c3 -> FinSequence of a1 -Terms a2 means :Def2: :: MSATERM:def 2
a4 is SubtreeSeq of a3;
existence
ex b1 being FinSequence of c1 -Terms c2 st b1 is SubtreeSeq of c3
proof end;
end;

:: deftheorem Def2 defines ArgumentSeq MSATERM:def 2 :
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being NonTerminal of (DTConMSA b2)
for b4 being FinSequence of b1 -Terms b2 holds
( b4 is ArgumentSeq of b3 iff b4 is SubtreeSeq of b3 );

theorem Th1: :: MSATERM:1
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being OperSymbol of b1
for b4 being FinSequence holds
( ( [b3,the carrier of b1] -tree b4 in b1 -Terms b2 & b4 is DTree-yielding ) iff b4 is ArgumentSeq of Sym b3,b2 )
proof end;

E6: now
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
let c3 be set ;
set c4 = c2;
set c5 = DTConMSA c2;
E7: Terminals (DTConMSA c2) = Union (coprod c2) by MSAFREE:6;
E8: dom (coprod c2) = the carrier of c1 by PBOOLE:def 3;
hereby
assume c3 in Terminals (DTConMSA c2) ;
then consider c6 being set such that
E9: ( c6 in dom (coprod c2) & c3 in (coprod c2) . c6 ) by E7, CARD_5:10;
reconsider c7 = c6 as SortSymbol of c1 by E9, PBOOLE:def 3;
(coprod c2) . c7 = coprod c7,c2 by MSAFREE:def 3;
then consider c8 being set such that
E10: ( c8 in c2 . c7 & c3 = [c8,c7] ) by E9, MSAFREE:def 2;
thus ex b1 being SortSymbol of c1ex b2 being Element of c2 . b1 st c3 = [b2,b1] by E10;
end;
let c6 be SortSymbol of c1;
let c7 be Element of c2 . c6;
assume c3 = [c7,c6] ;
then c3 in coprod c6,c2 by MSAFREE:def 2;
then c3 in (coprod c2) . c6 by MSAFREE:def 3;
hence c3 in Terminals (DTConMSA c2) by E7, E8, CARD_5:10;
end;

E7: now
let c1 be non empty non void ManySortedSign ;
let c2 be MSAlgebra of c1;
let c3 be V3 ManySortedSet of the carrier of c1;
let c4 be set ;
set c5 = the Sorts of c2 \/ c3;
set c6 = DTConMSA (the Sorts of c2 \/ c3);
E8: Terminals (DTConMSA (the Sorts of c2 \/ c3)) = Union (coprod (the Sorts of c2 \/ c3)) by MSAFREE:6;
E9: dom (coprod (the Sorts of c2 \/ c3)) = the carrier of c1 by PBOOLE:def 3;
hereby
assume c4 in Terminals (DTConMSA (the Sorts of c2 \/ c3)) ;
then consider c7 being set such that
E10: ( c7 in dom (coprod (the Sorts of c2 \/ c3)) & c4 in (coprod (the Sorts of c2 \/ c3)) . c7 ) by E8, CARD_5:10;
reconsider c8 = c7 as SortSymbol of c1 by E10, PBOOLE:def 3;
(coprod (the Sorts of c2 \/ c3)) . c8 = coprod c8,(the Sorts of c2 \/ c3) by MSAFREE:def 3;
then consider c9 being set such that
E11: ( c9 in (the Sorts of c2 \/ c3) . c8 & c4 = [c9,c8] ) by E10, MSAFREE:def 2;
(the Sorts of c2 \/ c3) . c8 = (the Sorts of c2 . c8) \/ (c3 . c8) by PBOOLE:def 7;
then ( c9 in the Sorts of c2 . c8 or c9 in c3 . c8 ) by E11, XBOOLE_0:def 2;
hence ( ex b1 being SortSymbol of c1ex b2 being set st
( b2 in the Sorts of c2 . b1 & c4 = [b2,b1] ) or ex b1 being SortSymbol of c1ex b2 being Element of c3 . b1 st c4 = [b2,b1] ) by E11;
end;
let c7 be SortSymbol of c1;
E10: (the Sorts of c2 \/ c3) . c7 = (the Sorts of c2 . c7) \/ (c3 . c7) by PBOOLE:def 7;
hereby
let c8 be set ;
assume E11: c8 in the Sorts of c2 . c7 ;
assume E12: c4 = [c8,c7] ;
c8 in (the Sorts of c2 \/ c3) . c7 by E10, E11, XBOOLE_0:def 2;
then c4 in coprod c7,(the Sorts of c2 \/ c3) by E12, MSAFREE:def 2;
then c4 in (coprod (the Sorts of c2 \/ c3)) . c7 by MSAFREE:def 3;
hence c4 in Terminals (DTConMSA (the Sorts of c2 \/ c3)) by E8, E9, CARD_5:10;
end;
let c8 be Element of c3 . c7;
assume E11: c4 = [c8,c7] ;
c8 in (the Sorts of c2 \/ c3) . c7 by E10, XBOOLE_0:def 2;
then c4 in coprod c7,(the Sorts of c2 \/ c3) by E11, MSAFREE:def 2;
then c4 in (coprod (the Sorts of c2 \/ c3)) . c7 by MSAFREE:def 3;
hence c4 in Terminals (DTConMSA (the Sorts of c2 \/ c3)) by E8, E9, CARD_5:10;
end;

E8: now
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
set c3 = DTConMSA c2;
let c4 be set ;
NonTerminals (DTConMSA c2) = [:the OperSymbols of c1,{the carrier of c1}:] by MSAFREE:6;
hence ( c4 is NonTerminal of (DTConMSA c2) iff c4 in [:the OperSymbols of c1,{the carrier of c1}:] ) ;
end;

scheme :: MSATERM:sch 1
s1{ F1() -> non empty non void ManySortedSign , F2() -> V3 ManySortedSet of the carrier of F1(), P1[ set ] } :
for b1 being Term of F1(),F2() holds P1[b1]
provided
E9: for b1 being SortSymbol of F1()
for b2 being Element of F2() . b1 holds P1[ root-tree [b2,b1]] and
E10: for b1 being OperSymbol of F1()
for b2 being ArgumentSeq of Sym b1,F2() st ( for b3 being Term of F1(),F2() st b3 in rng b2 holds
P1[b3] ) holds
P1[[b1,the carrier of F1()] -tree b2]
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be MSAlgebra of c1;
let c3 be V3 ManySortedSet of the carrier of c1;
mode c-Term of a2,a3 is Term of a1,(the Sorts of a2 \/ a3);
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be MSAlgebra of c1;
let c3 be V3 ManySortedSet of the carrier of c1;
let c4 be OperSymbol of c1;
mode ArgumentSeq of a4,a2,a3 is ArgumentSeq of Sym a4,(the Sorts of a2 \/ a3);
end;

scheme :: MSATERM:sch 2
s2{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of F1(), F3() -> V3 ManySortedSet of the carrier of F1(), P1[ set ] } :
for b1 being c-Term of F2(),F3() holds P1[b1]
provided
E9: for b1 being SortSymbol of F1()
for b2 being Element of the Sorts of F2() . b1 holds P1[ root-tree [b2,b1]] and
E10: for b1 being SortSymbol of F1()
for b2 being Element of F3() . b1 holds P1[ root-tree [b2,b1]] and
E11: for b1 being OperSymbol of F1()
for b2 being ArgumentSeq of b1,F2(),F3() st ( for b3 being c-Term of F2(),F3() st b3 in rng b2 holds
P1[b3] ) holds
P1[(Sym b1,(the Sorts of F2() \/ F3())) -tree b2]
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
let c3 be Term of c1,c2;
let c4 be Node of c3;
redefine func . as c3 . c4 -> Symbol of (DTConMSA a2);
coherence
c3 . c4 is Symbol of (DTConMSA c2)
proof end;
end;

registration
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
cluster -> finite Element of a1 -Terms a2;
coherence
for b1 being Term of c1,c2 holds b1 is finite ;
end;

E9: now
let c1 be non empty with_terminals with_nonterminals DTConstrStr ;
let c2 be Symbol of c1;
the carrier of c1 = (Terminals c1) \/ (NonTerminals c1) by LANG1:1;
hence ( c2 is Terminal of c1 or c2 is NonTerminal of c1 ) by XBOOLE_0:def 2;
Terminals c1 misses NonTerminals c1 by DTCONSTR:8;
hence ( not c2 is Terminal of c1 or not c2 is NonTerminal of c1 ) by XBOOLE_0:3;
end;

theorem Th2: :: MSATERM:2
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being Term of b1,b2 holds
( ex b4 being SortSymbol of b1ex b5 being Element of b2 . b4 st b3 . {} = [b5,b4] or b3 . {} in [:the OperSymbols of b1,{the carrier of b1}:] )
proof end;

theorem Th3: :: MSATERM:3
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being MSAlgebra of b1
for b4 being c-Term of b3,b2 holds
( ex b5 being SortSymbol of b1ex b6 being set st
( b6 in the Sorts of b3 . b5 & b4 . {} = [b6,b5] ) or ex b5 being SortSymbol of b1ex b6 being Element of b2 . b5 st b4 . {} = [b6,b5] or b4 . {} in [:the OperSymbols of b1,{the carrier of b1}:] )
proof end;

theorem Th4: :: MSATERM:4
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being SortSymbol of b1
for b4 being Element of b2 . b3 holds root-tree [b4,b3] is Term of b1,b2
proof end;

theorem Th5: :: MSATERM:5
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being Term of b1,b2
for b4 being SortSymbol of b1
for b5 being Element of b2 . b4 st b3 . {} = [b5,b4] holds
b3 = root-tree [b5,b4]
proof end;

theorem Th6: :: MSATERM:6
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being MSAlgebra of b1
for b4 being SortSymbol of b1
for b5 being set st b5 in the Sorts of b3 . b4 holds
root-tree [b5,b4] is c-Term of b3,b2
proof end;

theorem Th7: :: MSATERM:7
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being MSAlgebra of b1
for b4 being c-Term of b3,b2
for b5 being SortSymbol of b1
for b6 being set st b6 in the Sorts of b3 . b5 & b4 . {} = [b6,b5] holds
b4 = root-tree [b6,b5]
proof end;

theorem Th8: :: MSATERM:8
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being MSAlgebra of b1
for b4 being SortSymbol of b1
for b5 being Element of b2 . b4 holds root-tree [b5,b4] is c-Term of b3,b2
proof end;

theorem Th9: :: MSATERM:9
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being MSAlgebra of b1
for b4 being c-Term of b3,b2
for b5 being SortSymbol of b1
for b6 being Element of b2 . b5 st b4 . {} = [b6,b5] holds
b4 = root-tree [b6,b5]
proof end;

theorem Th10: :: MSATERM:10
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being Term of b1,b2
for b4 being OperSymbol of b1 st b3 . {} = [b4,the carrier of b1] holds
ex b5 being ArgumentSeq of Sym b4,b2 st b3 = [b4,the carrier of b1] -tree b5
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be V3 ManySortedSet of the carrier of c1;
let c4 be SortSymbol of c1;
let c5 be Element of the Sorts of c2 . c4;
func c5 -term c2,c3 -> c-Term of a2,a3 equals :: MSATERM:def 3
 root-tree [a5,a4];
correctness
coherence
root-tree [c5,c4] is c-Term of c2,c3;
by Th6;
end;

:: deftheorem Def3 defines -term MSATERM:def 3 :
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being V3 ManySortedSet of the carrier of b1
for b4 being SortSymbol of b1
for b5 being Element of the Sorts of b2 . b4 holds b5 -term b2,b3 = root-tree [b5,b4];

definition
let c1 be non empty non void ManySortedSign ;
let c2 be MSAlgebra of c1;
let c3 be V3 ManySortedSet of the carrier of c1;
let c4 be SortSymbol of c1;
let c5 be Element of c3 . c4;
func c5 -term c2 -> c-Term of a2,a3 equals :: MSATERM:def 4
 root-tree [a5,a4];
correctness
coherence
root-tree [c5,c4] is c-Term of c2,c3;
by Th8;
end;

:: deftheorem Def4 defines -term MSATERM:def 4 :
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1
for b3 being V3 ManySortedSet of the carrier of b1
for b4 being SortSymbol of b1
for b5 being Element of b3 . b4 holds b5 -term b2 = root-tree [b5,b4];

definition
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
let c3 be NonTerminal of (DTConMSA c2);
let c4 be ArgumentSeq of c3;
redefine func -tree as c3 -tree c4 -> Term of a1,a2;
coherence
c3 -tree c4 is Term of c1,c2
proof end;
end;

scheme :: MSATERM:sch 3
s3{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of F1(), F3() -> V3 ManySortedSet of the carrier of F1(), P1[ set ] } :
for b1 being c-Term of F2(),F3() holds P1[b1]
provided
E16: for b1 being SortSymbol of F1()
for b2 being Element of the Sorts of F2() . b1 holds P1[b2 -term F2(),F3()] and
E17: for b1 being SortSymbol of F1()
for b2 being Element of F3() . b1 holds P1[b2 -term F2()] and
E18: for b1 being OperSymbol of F1()
for b2 being ArgumentSeq of Sym b1,(the Sorts of F2() \/ F3()) st ( for b3 being c-Term of F2(),F3() st b3 in rng b2 holds
P1[b3] ) holds
P1[(Sym b1,(the Sorts of F2() \/ F3())) -tree b2]
proof end;

theorem Th11: :: MSATERM:11
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being Term of b1,b2 ex b4 being SortSymbol of b1 st b3 in FreeSort b2,b4
proof end;

theorem Th12: :: MSATERM:12
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being SortSymbol of b1 holds FreeSort b2,b3 c= b1 -Terms b2 ;

theorem Th13: :: MSATERM:13
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1 holds b1 -Terms b2 = Union (FreeSort b2)
proof end;

Lemma17: for b1 being set holds not b1 in b1
;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
let c3 be Term of c1,c2;
func the_sort_of c3 -> SortSymbol of a1 means :Def5: :: MSATERM:def 5
a3 in FreeSort a2,a4;
existence
ex b1 being SortSymbol of c1 st c3 in FreeSort c2,b1 by Th11;
uniqueness
for b1, b2 being SortSymbol of c1 st c3 in FreeSort c2,b1 & c3 in FreeSort c2,b2 holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines the_sort_of MSATERM:def 5 :
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being Term of b1,b2
for b4 being SortSymbol of b1 holds
( b4 = the_sort_of b3 iff b3 in FreeSort b2,b4 );

theorem Th14: :: MSATERM:14
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being Term of b1,b2
for b4 being SortSymbol of b1
for b5 being Element of b2 . b4 st b3 = root-tree [b5,b4] holds
the_sort_of b3 = b4
proof end;

theorem Th15: :: MSATERM:15
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being MSAlgebra of b1
for b4 being c-Term of b3,b2
for b5 being SortSymbol of b1
for b6 being set st b6 in the Sorts of b3 . b5 & b4 = root-tree [b6,b5] holds
the_sort_of b4 = b5
proof end;

theorem Th16: :: MSATERM:16
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being MSAlgebra of b1
for b4 being c-Term of b3,b2
for b5 being SortSymbol of b1
for b6 being Element of b2 . b5 st b4 = root-tree [b6,b5] holds
the_sort_of b4 = b5
proof end;

theorem Th17: :: MSATERM:17
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being Term of b1,b2
for b4 being OperSymbol of b1 st b3 . {} = [b4,the carrier of b1] holds
the_sort_of b3 = the_result_sort_of b4
proof end;

theorem Th18: :: MSATERM:18
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being non-empty MSAlgebra of b1
for b4 being SortSymbol of b1
for b5 being Element of the Sorts of b3 . b4 holds the_sort_of (b5 -term b3,b2) = b4 by Th15;

theorem Th19: :: MSATERM:19
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being MSAlgebra of b1
for b4 being SortSymbol of b1
for b5 being Element of b2 . b4 holds the_sort_of (b5 -term b3) = b4
proof end;

theorem Th20: :: MSATERM:20
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being OperSymbol of b1
for b4 being ArgumentSeq of Sym b3,b2 holds the_sort_of ((Sym b3,b2) -tree b4) = the_result_sort_of b3
proof end;

theorem Th21: :: MSATERM:21
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being OperSymbol of b1
for b4 being FinSequence of b1 -Terms b2 holds
( b4 is ArgumentSeq of Sym b3,b2 iff Sym b3,b2 ==> roots b4 )
proof end;

Lemma26: for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being OperSymbol of b1
for b4 being ArgumentSeq of Sym b3,b2 holds
( len b4 = len (the_arity_of b3) & dom b4 = dom (the_arity_of b3) & ( for b5 being Nat st b5 in dom b4 holds
ex b6 being Term of b1,b2 st
( b6 = b4 . b5 & b6 = b4 /. b5 & the_sort_of b6 = (the_arity_of b3) . b5 & the_sort_of b6 = (the_arity_of b3) /. b5 ) ) )
proof end;

theorem Th22: :: MSATERM:22
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being OperSymbol of b1
for b4 being ArgumentSeq of Sym b3,b2 holds
( len b4 = len (the_arity_of b3) & dom b4 = dom (the_arity_of b3) & ( for b5 being Nat st b5 in dom b4 holds
b4 . b5 is Term of b1,b2 ) )
proof end;

theorem Th23: :: MSATERM:23
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being OperSymbol of b1
for b4 being ArgumentSeq of Sym b3,b2
for b5 being Nat st b5 in dom b4 holds
for b6 being Term of b1,b2 st b6 = b4 . b5 holds
( b6 = b4 /. b5 & the_sort_of b6 = (the_arity_of b3) . b5 & the_sort_of b6 = (the_arity_of b3) /. b5 )
proof end;

theorem Th24: :: MSATERM:24
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being OperSymbol of b1
for b4 being FinSequence st ( len b4 = len (the_arity_of b3) or dom b4 = dom (the_arity_of b3) ) & ( for b5 being Nat st b5 in dom b4 holds
ex b6 being Term of b1,b2 st
( b6 = b4 . b5 & the_sort_of b6 = (the_arity_of b3) . b5 ) or for b5 being Nat st b5 in dom b4 holds
ex b6 being Term of b1,b2 st
( b6 = b4 . b5 & the_sort_of b6 = (the_arity_of b3) /. b5 ) ) holds
b4 is ArgumentSeq of Sym b3,b2
proof end;

theorem Th25: :: MSATERM:25
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being OperSymbol of b1
for b4 being FinSequence of b1 -Terms b2 st ( len b4 = len (the_arity_of b3) or dom b4 = dom (the_arity_of b3) ) & ( for b5 being Nat st b5 in dom b4 holds
for b6 being Term of b1,b2 st b6 = b4 . b5 holds
the_sort_of b6 = (the_arity_of b3) . b5 or for b5 being Nat st b5 in dom b4 holds
for b6 being Term of b1,b2 st b6 = b4 . b5 holds
the_sort_of b6 = (the_arity_of b3) /. b5 ) holds
b4 is ArgumentSeq of Sym b3,b2
proof end;

theorem Th26: :: MSATERM:26
for b1 being non empty non void ManySortedSign
for b2, b3 being V3 ManySortedSet of the carrier of b1 st b2 c= b3 holds
for b4 being Term of b1,b2 holds b4 is Term of b1,b3
proof end;

theorem Th27: :: MSATERM:27
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1
for b3 being V3 ManySortedSet of the carrier of b1
for b4 being Term of b1,b3 holds b4 is c-Term of b2,b3
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
mode CompoundTerm of c1,c2 -> Term of a1,a2 means :: MSATERM:def 6
a3 . {} in [:the OperSymbols of a1,{the carrier of a1}:];
existence
ex b1 being Term of c1,c2 st b1 . {} in [:the OperSymbols of c1,{the carrier of c1}:]
proof end;
end;

:: deftheorem Def6 defines CompoundTerm MSATERM:def 6 :
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being Term of b1,b2 holds
( b3 is CompoundTerm of b1,b2 iff b3 . {} in [:the OperSymbols of b1,{the carrier of b1}:] );

definition
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
mode SetWithCompoundTerm of c1,c2 -> non empty Subset of (a1 -Terms a2) means :: MSATERM:def 7
ex b1 being CompoundTerm of a1,a2 st b1 in a3;
existence
ex b1 being non empty Subset of (c1 -Terms c2)ex b2 being CompoundTerm of c1,c2 st b2 in b1
proof end;
end;

:: deftheorem Def7 defines SetWithCompoundTerm MSATERM:def 7 :
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being non empty Subset of (b1 -Terms b2) holds
( b3 is SetWithCompoundTerm of b1,b2 iff ex b4 being CompoundTerm of b1,b2 st b4 in b3 );

theorem Th28: :: MSATERM:28
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being Term of b1,b2 st not b3 is root holds
b3 is CompoundTerm of b1,b2
proof end;

Lemma30: for b1 being Nat
for b2 being FinSequence st b1 < len b2 holds
( b1 + 1 in dom b2 & b2 . (b1 + 1) in rng b2 )
proof end;

theorem Th29: :: MSATERM:29
for b1 being non empty non void ManySortedSign
for b2 being V3 ManySortedSet of the carrier of b1
for b3 being Term of b1,b2
for b4 being Node of b3 holds b3 | b4 is Term of b1,b2
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be V3 ManySortedSet of the carrier of c1;
let c3 be Term of c1,c2;
let c4 be Node of c3;
redefine func | as c3 | c4 -> Term of a1,a2;
coherence
c3 | c4 is Term of c1,c2 by Th29;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be MSAlgebra of c1;
mode Variables of c2 -> V3 ManySortedSet of the carrier of a1 means :Def8: :: MSATERM:def 8
a3 misses the Sorts of a2;
existence
ex b1 being V3 ManySortedSet of the carrier of c1 st b1 misses the Sorts of c2
proof end;
end;

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

theorem Th30: :: MSATERM:30
for b1 being non empty non void ManySortedSign
for b2 being MSAlgebra of b1
for b3 being Variables of b2
for b4 being SortSymbol of b1
for b5 being set st b5 in the Sorts of b2 . b4 holds
for b6 being Element of b3 . b4 holds b5 <> b6
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be V3 ManySortedSet of the carrier of c1;
let c4 be c-Term of c2,c3;
let c5 be ManySortedFunction of c3,the Sorts of c2;
let c6 be finite DecoratedTree;
pred c6 is_an_evaluation_of c4,c5 means :Def9: :: MSATERM:def 9
( dom a6 = dom a4 & ( for b1 being Node of a6 holds
( ( for b2 being SortSymbol of a1
for b3 being Element of a3 . b2 st a4 . b1 = [b3,b2] holds
a6 . b1 = (a5 . b2) . b3 ) & ( for b2 being SortSymbol of a1
for b3 being Element of the Sorts of a2 . b2 st a4 . b1 = [b3,b2] holds
a6 . b1 = b3 ) & ( for b2 being OperSymbol of a1 st a4 . b1 = [b2,the carrier of a1] holds
a6 . b1 = (Den b2,a2) . (succ a6,b1) ) ) ) );
end;

:: deftheorem Def9 defines is_an_evaluation_of MSATERM:def 9 :
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being V3 ManySortedSet of the carrier of b1
for b4 being c-Term of b2,b3
for b5 being ManySortedFunction of b3,the Sorts of b2
for b6 being finite DecoratedTree holds
( b6 is_an_evaluation_of b4,b5 iff ( dom b6 = dom b4 & ( for b7 being Node of b6 holds
( ( for b8 being SortSymbol of b1
for b9 being Element of b3 . b8 st b4 . b7 = [b9,b8] holds
b6 . b7 = (b5 . b8) . b9 ) & ( for b8 being SortSymbol of b1
for b9 being Element of the Sorts of b2 . b8 st b4 . b7 = [b9,b8] holds
b6 . b7 = b9 ) & ( for b8 being OperSymbol of b1 st b4 . b7 = [b8,the carrier of b1] holds
b6 . b7 = (Den b8,b2) . (succ b6,b7) ) ) ) ) );

theorem Th31: :: MSATERM:31
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being c-Term of b2,b3
for b5 being ManySortedFunction of b3,the Sorts of b2
for b6 being SortSymbol of b1
for b7 being Element of the Sorts of b2 . b6 st b4 = root-tree [b7,b6] holds
root-tree b7 is_an_evaluation_of b4,b5
proof end;

theorem Th32: :: MSATERM:32
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being c-Term of b2,b3
for b5 being ManySortedFunction of b3,the Sorts of b2
for b6 being SortSymbol of b1
for b7 being Element of b3 . b6 st b4 = root-tree [b7,b6] holds
root-tree ((b5 . b6) . b7) is_an_evaluation_of b4,b5
proof end;

theorem Th33: :: MSATERM:33
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being ManySortedFunction of b3,the Sorts of b2
for b5 being OperSymbol of b1
for b6 being ArgumentSeq of b5,b2,b3
for b7 being DTree-yielding FinSequence st len b7 = len b6 & ( for b8 being Nat
for b9 being c-Term of b2,b3 st b8 in dom b6 & b9 = b6 . b8 holds
ex b10 being finite DecoratedTree st
( b10 = b7 . b8 & b10 is_an_evaluation_of b9,b4 ) ) holds
ex b8 being finite DecoratedTree st
( b8 = ((Den b5,b2) . (roots b7)) -tree b7 & b8 is_an_evaluation_of (Sym b5,(the Sorts of b2 \/ b3)) -tree b6,b4 )
proof end;

theorem Th34: :: MSATERM:34
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being ManySortedFunction of b3,the Sorts of b2
for b5 being c-Term of b2,b3
for b6 being finite DecoratedTree st b6 is_an_evaluation_of b5,b4 holds
for b7 being Node of b5
for b8 being Node of b6 st b8 = b7 holds
b6 | b8 is_an_evaluation_of b5 | b7,b4
proof end;

theorem Th35: :: MSATERM:35
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being ManySortedFunction of b3,the Sorts of b2
for b5 being OperSymbol of b1
for b6 being ArgumentSeq of b5,b2,b3
for b7 being finite DecoratedTree st b7 is_an_evaluation_of (Sym b5,(the Sorts of b2 \/ b3)) -tree b6,b4 holds
ex b8 being DTree-yielding FinSequence st
( len b8 = len b6 & b7 = ((Den b5,b2) . (roots b8)) -tree b8 & ( for b9 being Nat
for b10 being c-Term of b2,b3 st b9 in dom b6 & b10 = b6 . b9 holds
ex b11 being finite DecoratedTree st
( b11 = b8 . b9 & b11 is_an_evaluation_of b10,b4 ) ) )
proof end;

theorem Th36: :: MSATERM:36
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being c-Term of b2,b3
for b5 being ManySortedFunction of b3,the Sorts of b2 ex b6 being finite DecoratedTree st b6 is_an_evaluation_of b4,b5
proof end;

theorem Th37: :: MSATERM:37
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being c-Term of b2,b3
for b5 being ManySortedFunction of b3,the Sorts of b2
for b6, b7 being finite DecoratedTree st b6 is_an_evaluation_of b4,b5 & b7 is_an_evaluation_of b4,b5 holds
b6 = b7
proof end;

theorem Th38: :: MSATERM:38
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being c-Term of b2,b3
for b5 being ManySortedFunction of b3,the Sorts of b2
for b6 being finite DecoratedTree st b6 is_an_evaluation_of b4,b5 holds
b6 . {} in the Sorts of b2 . (the_sort_of b4)
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
let c3 be Variables of c2;
let c4 be c-Term of c2,c3;
let c5 be ManySortedFunction of c3,the Sorts of c2;
func c4 @ c5 -> Element of the Sorts of a2 . (the_sort_of a4) means :Def10: :: MSATERM:def 10
ex b1 being finite DecoratedTree st
( b1 is_an_evaluation_of a4,a5 & a6 = b1 . {} );
existence
ex b1 being Element of the Sorts of c2 . (the_sort_of c4)ex b2 being finite DecoratedTree st
( b2 is_an_evaluation_of c4,c5 & b1 = b2 . {} )
proof end;
uniqueness
for b1, b2 being Element of the Sorts of c2 . (the_sort_of c4) st ex b3 being finite DecoratedTree st
( b3 is_an_evaluation_of c4,c5 & b1 = b3 . {} ) & ex b3 being finite DecoratedTree st
( b3 is_an_evaluation_of c4,c5 & b2 = b3 . {} ) holds
b1 = b2 by Th37;
end;

:: deftheorem Def10 defines @ MSATERM:def 10 :
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being c-Term of b2,b3
for b5 being ManySortedFunction of b3,the Sorts of b2
for b6 being Element of the Sorts of b2 . (the_sort_of b4) holds
( b6 = b4 @ b5 iff ex b7 being finite DecoratedTree st
( b7 is_an_evaluation_of b4,b5 & b6 = b7 . {} ) );

theorem Th39: :: MSATERM:39
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being ManySortedFunction of b3,the Sorts of b2
for b5 being c-Term of b2,b3
for b6 being finite DecoratedTree st b6 is_an_evaluation_of b5,b4 holds
b5 @ b4 = b6 . {}
proof end;

theorem Th40: :: MSATERM:40
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being ManySortedFunction of b3,the Sorts of b2
for b5 being c-Term of b2,b3
for b6 being finite DecoratedTree st b6 is_an_evaluation_of b5,b4 holds
for b7 being Node of b5 holds b6 . b7 = (b5 | b7) @ b4
proof end;

theorem Th41: :: MSATERM:41
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being ManySortedFunction of b3,the Sorts of b2
for b5 being SortSymbol of b1
for b6 being Element of the Sorts of b2 . b5 holds (b6 -term b2,b3) @ b4 = b6
proof end;

theorem Th42: :: MSATERM:42
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being ManySortedFunction of b3,the Sorts of b2
for b5 being SortSymbol of b1
for b6 being Element of b3 . b5 holds (b6 -term b2) @ b4 = (b4 . b5) . b6
proof end;

theorem Th43: :: MSATERM:43
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being Variables of b2
for b4 being ManySortedFunction of b3,the Sorts of b2
for b5 being OperSymbol of b1
for b6 being ArgumentSeq of b5,b2,b3
for b7 being FinSequence st len b7 = len b6 & ( for b8 being Nat st b8 in dom b6 holds
for b9 being c-Term of b2,b3 st b9 = b6 . b8 holds
b7 . b8 = b9 @ b4 ) holds
((Sym b5,(the Sorts of b2 \/ b3)) -tree b6) @ b4 = (Den b5,b2) . b7
proof end;