:: by Grzegorz Bancerek

::

:: Received November 25, 1994

:: Copyright (c) 1994-2018 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

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;
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

definition

let S be non empty non void ManySortedSign ;

let V be ManySortedSet of the carrier of S;

coherence

TS (DTConMSA V) is Subset of (FinTrees the carrier of (DTConMSA V));

;

end;
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 TS (DTConMSA V);

coherence

TS (DTConMSA V) is Subset of (FinTrees the carrier of (DTConMSA V));

;

:: 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);

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;

correctness

coherence

not S -Terms V is empty ;

;

end;
let V be V2() ManySortedSet of the carrier of S;

correctness

coherence

not S -Terms V is empty ;

;

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;
let V be V2() ManySortedSet of the carrier of S;

mode Term of S,V is Element of S -Terms V;

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)

end;
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;

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);

ex b_{1} being FinSequence of S -Terms V st b_{1} is SubtreeSeq of sy

end;
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 it is SubtreeSeq of sy;

ex b

proof 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 b_{4} being FinSequence of S -Terms V holds

( b_{4} is ArgumentSeq of sy iff b_{4} is SubtreeSeq of sy );

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 b

( b

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) )

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) ) )

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;

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;
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)

let s be SortSymbol of S; :: thesis: for a being Element of V . s st x = [a,s] holds 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;
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

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

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)) ) ) ) )

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;

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;

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;
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)) ) )

let s be SortSymbol of S; :: thesis: ( ( for a being set st a in the Sorts of A . s & x = [a,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;
( 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

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 Element of V . s; :: thesis: ( x = [a,s] implies x in Terminals (DTConMSA ( the Sorts of A (\/) V)) )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;
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

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

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}:] )

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;
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

scheme :: MSATERM:sch 1

TermInd{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> V2() ManySortedSet of the carrier of F_{1}(), P_{1}[ set ] } :

provided

TermInd{ F

provided

A1:
for s being SortSymbol of F_{1}()

for v being Element of F_{2}() . s holds P_{1}[ root-tree [v,s]]
and

A2: for o being OperSymbol of F_{1}()

for p being ArgumentSeq of Sym (o,F_{2}()) st ( for t being Term of F_{1}(),F_{2}() st t in rng p holds

P_{1}[t] ) holds

P_{1}[[o, the carrier of F_{1}()] -tree p]

for v being Element of F

A2: for o being OperSymbol of F

for p being ArgumentSeq of Sym (o,F

P

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;
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);

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;
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));

scheme :: MSATERM:sch 2

CTermInd{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), F_{3}() -> V2() ManySortedSet of the carrier of F_{1}(), P_{1}[ set ] } :

provided

CTermInd{ F

provided

A1:
for s being SortSymbol of F_{1}()

for x being Element of the Sorts of F_{2}() . s holds P_{1}[ root-tree [x,s]]
and

A2: for s being SortSymbol of F_{1}()

for v being Element of F_{3}() . s holds P_{1}[ root-tree [v,s]]
and

A3: for o being OperSymbol of F_{1}()

for p being ArgumentSeq of o,F_{2}(),F_{3}() st ( for t being c-Term of F_{2}(),F_{3}() st t in rng p holds

P_{1}[t] ) holds

P_{1}[(Sym (o,( the Sorts of F_{2}() (\/) F_{3}()))) -tree p]

for x being Element of the Sorts of F

A2: for s being SortSymbol of F

for v being Element of F

A3: for o being OperSymbol of F

for p being ArgumentSeq of o,F

P

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)

end;
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;

registration

let S be non empty non void ManySortedSign ;

let V be V2() ManySortedSet of the carrier of S;

coherence

for b_{1} being Term of S,V holds b_{1} is finite
;

end;
let V be V2() ManySortedSet of the carrier of S;

coherence

for b

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 ) )

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;
( ( 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

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}:] )

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}:] )

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

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]

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

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]

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

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]

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

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;

correctness

coherence

root-tree [x,s] is c-Term of A,V;

by Th6;

end;
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;

correctness

coherence

root-tree [x,s] is c-Term of A,V;

by Th6;

:: 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];

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;

correctness

coherence

root-tree [v,s] is c-Term of A,V;

by Th8;

end;
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;

correctness

coherence

root-tree [v,s] is c-Term of A,V;

by Th8;

:: 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];

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

end;
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;

scheme :: MSATERM:sch 3

TermInd2{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), F_{3}() -> V2() ManySortedSet of the carrier of F_{1}(), P_{1}[ set ] } :

provided

TermInd2{ F

provided

A1:
for s being SortSymbol of F_{1}()

for x being Element of the Sorts of F_{2}() . s holds P_{1}[x -term (F_{2}(),F_{3}())]
and

A2: for s being SortSymbol of F_{1}()

for v being Element of F_{3}() . s holds P_{1}[v -term F_{2}()]
and

A3: for o being OperSymbol of F_{1}()

for p being ArgumentSeq of Sym (o,( the Sorts of F_{2}() (\/) F_{3}())) st ( for t being c-Term of F_{2}(),F_{3}() st t in rng p holds

P_{1}[t] ) holds

P_{1}[(Sym (o,( the Sorts of F_{2}() (\/) F_{3}()))) -tree p]

for x being Element of the Sorts of F

A2: for s being SortSymbol of F

for v being Element of F

A3: for o being OperSymbol of F

for p being ArgumentSeq of Sym (o,( the Sorts of F

P

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)

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 ;

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)

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;

existence

ex b_{1} being SortSymbol of S st t in FreeSort (V,b_{1})
by Th11;

uniqueness

for b_{1}, b_{2} being SortSymbol of S st t in FreeSort (V,b_{1}) & t in FreeSort (V,b_{2}) holds

b_{1} = b_{2}

end;
let V be V2() ManySortedSet of the carrier of S;

let t be Term of S,V;

existence

ex b

uniqueness

for b

b

proof 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 b_{4} being SortSymbol of S holds

( b_{4} = the_sort_of t iff t in FreeSort (V,b_{4}) );

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 b

( b

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

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

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

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

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;

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

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

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 )

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 ) )

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 )

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)

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)

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

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

definition

let S be non empty non void ManySortedSign ;

let V be V2() ManySortedSet of the carrier of S;

ex b_{1} being Term of S,V st b_{1} . {} in [: the carrier' of S,{ the carrier of S}:]

end;
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 it . {} in [: the carrier' of S,{ the carrier of S}:];

ex b

proof 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 b_{3} being Term of S,V holds

( b_{3} is CompoundTerm of S,V iff b_{3} . {} in [: the carrier' of S,{ the carrier of S}:] );

for S being non empty non void ManySortedSign

for V being V2() ManySortedSet of the carrier of S

for b

( b

definition

let S be non empty non void ManySortedSign ;

let V be V2() ManySortedSet of the carrier of S;

ex b_{1} being non empty Subset of (S -Terms V) ex t being CompoundTerm of S,V st t in b_{1}

end;
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 t being CompoundTerm of S,V st t in it;

ex b

proof 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 b_{3} being non empty Subset of (S -Terms V) holds

( b_{3} is SetWithCompoundTerm of S,V iff ex t being CompoundTerm of S,V st t in b_{3} );

for S being non empty non void ManySortedSign

for V being V2() ManySortedSet of the carrier of S

for b

( b

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

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

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;
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;

definition

let S be non empty non void ManySortedSign ;

let A be MSAlgebra over S;

ex b_{1} being V2() ManySortedSet of the carrier of S st b_{1} misses the Sorts of A

end;
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 it misses the Sorts of A;

ex b

proof end;

:: deftheorem Def8 defines Variables MSATERM:def 8 :

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for b_{3} being V2() ManySortedSet of the carrier of S holds

( b_{3} is Variables of A iff b_{3} misses the Sorts of A );

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for b

( b

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

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;

end;
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)) ) ) ) );

( 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)) ) ) ) );

:: 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)) ) ) ) ) );

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

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

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 )

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

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 ) ) )

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

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

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)

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;

ex b_{1} being Element of the Sorts of A . (the_sort_of t) ex vt being finite DecoratedTree st

( vt is_an_evaluation_of t,f & b_{1} = vt . {} )

for b_{1}, b_{2} 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 & b_{1} = vt . {} ) & ex vt being finite DecoratedTree st

( vt is_an_evaluation_of t,f & b_{2} = vt . {} ) holds

b_{1} = b_{2}
by Th37;

end;
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 vt being finite DecoratedTree st

( vt is_an_evaluation_of t,f & it = vt . {} );

ex b

( vt is_an_evaluation_of t,f & b

proof end;

uniqueness for b

( vt is_an_evaluation_of t,f & b

( vt is_an_evaluation_of t,f & b

b

:: 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 b_{6} being Element of the Sorts of A . (the_sort_of t) holds

( b_{6} = t @ f iff ex vt being finite DecoratedTree st

( vt is_an_evaluation_of t,f & b_{6} = vt . {} ) );

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 b

( b

( vt is_an_evaluation_of t,f & b

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 . {}

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

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

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

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

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;