:: by Grzegorz Bancerek and Artur Korni{\l}owicz

::

:: Received August 8, 2001

:: Copyright (c) 2001-2021 Association of Mizar Users

registration

let S be non empty non void ManySortedSign ;

let A be non empty MSAlgebra over S;

coherence

not Union the Sorts of A is empty

end;
let A be non empty MSAlgebra over S;

coherence

not Union the Sorts of A is empty

proof end;

definition

let S be non empty non void ManySortedSign ;

let A be non empty MSAlgebra over S;

mode Element of A is Element of Union the Sorts of A;

end;
let A be non empty MSAlgebra over S;

mode Element of A is Element of Union the Sorts of A;

theorem :: MSAFREE3:1

for I being set

for A being ManySortedSet of I

for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds

F "" (F .:.: A) = A

for A being ManySortedSet of I

for F being ManySortedFunction of I st F is "1-1" & A c= doms F holds

F "" (F .:.: A) = A

proof end;

definition

let S be non void Signature;

let X be ManySortedSet of the carrier of S;

for b_{1}, b_{2} being strict MSAlgebra over S st ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( b_{1} = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X ) & ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( b_{2} = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X ) holds

b_{1} = b_{2}
;

existence

ex b_{1} being strict MSAlgebra over S ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( b_{1} = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X )

end;
let X be ManySortedSet of the carrier of S;

func Free (S,X) -> strict MSAlgebra over S means :Def1: :: MSAFREE3:def 1

ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( it = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X );

uniqueness ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( it = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X );

for b

( b

( b

b

existence

ex b

( b

proof end;

:: deftheorem Def1 defines Free MSAFREE3:def 1 :

for S being non void Signature

for X being ManySortedSet of the carrier of S

for b_{3} being strict MSAlgebra over S holds

( b_{3} = Free (S,X) iff ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( b_{3} = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X ) );

for S being non void Signature

for X being ManySortedSet of the carrier of S

for b

( b

( b

theorem Th2: :: MSAFREE3:2

for x being set

for S being non void Signature

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S holds

( [x,s] in the carrier of (DTConMSA X) iff x in X . s )

for S being non void Signature

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S holds

( [x,s] in the carrier of (DTConMSA X) iff x in X . s )

proof end;

theorem Th3: :: MSAFREE3:3

for x being set

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S holds

( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S holds

( ( x in X . s & x in Y . s ) iff root-tree [x,s] in ((Reverse Y) "" X) . s )

proof end;

theorem Th4: :: MSAFREE3:4

for x being set

for S being non void Signature

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S st x in X . s holds

root-tree [x,s] in the Sorts of (Free (S,X)) . s

for S being non void Signature

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S st x in X . s holds

root-tree [x,s] in the Sorts of (Free (S,X)) . s

proof end;

theorem Th5: :: MSAFREE3:5

for S being non void Signature

for X being ManySortedSet of the carrier of S

for o being OperSymbol of S st the_arity_of o = {} holds

root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)

for X being ManySortedSet of the carrier of S

for o being OperSymbol of S st the_arity_of o = {} holds

root-tree [o, the carrier of S] in the Sorts of (Free (S,X)) . (the_result_sort_of o)

proof end;

registration

let S be non void Signature;

let X be V9() ManySortedSet of the carrier of S;

coherence

not Free (S,X) is empty

end;
let X be V9() ManySortedSet of the carrier of S;

coherence

not Free (S,X) is empty

proof end;

theorem :: MSAFREE3:6

for x being set

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S holds

( x is Element of (FreeMSA X) iff x is Term of S,X )

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S holds

( x is Element of (FreeMSA X) iff x is Term of S,X )

proof end;

theorem Th7: :: MSAFREE3:7

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S

for s being SortSymbol of S

for x being Term of S,X holds

( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s )

for X being V8() ManySortedSet of the carrier of S

for s being SortSymbol of S

for x being Term of S,X holds

( x in the Sorts of (FreeMSA X) . s iff the_sort_of x = s )

proof end;

theorem Th8: :: MSAFREE3:8

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for x being Element of (Free (S,X)) holds x is Term of S,(X (\/) ( the carrier of S --> {0}))

for X being V9() ManySortedSet of the carrier of S

for x being Element of (Free (S,X)) holds x is Term of S,(X (\/) ( the carrier of S --> {0}))

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V9() ManySortedSet of the carrier of S;

coherence

for b_{1} being Element of (Free (S,X)) holds

( b_{1} is Relation-like & b_{1} is Function-like )
by Th8;

end;
let X be V9() ManySortedSet of the carrier of S;

coherence

for b

( b

registration

let S be non empty non void ManySortedSign ;

let X be V9() ManySortedSet of the carrier of S;

coherence

for b_{1} being Element of (Free (S,X)) holds

( b_{1} is finite & b_{1} is DecoratedTree-like )
by Th8;

end;
let X be V9() ManySortedSet of the carrier of S;

coherence

for b

( b

registration

let S be non empty non void ManySortedSign ;

let X be V9() ManySortedSet of the carrier of S;

coherence

for b_{1} being Element of (Free (S,X)) holds b_{1} is finite-branching
;

end;
let X be V9() ManySortedSet of the carrier of S;

coherence

for b

definition

let S be ManySortedSign ;

let t be non empty Relation;

ex b_{1} being ManySortedSet of the carrier of S st

for s being object st s in the carrier of S holds

b_{1} . s = { (a `1) where a is Element of rng t : a `2 = s }

for b_{1}, b_{2} being ManySortedSet of the carrier of S st ( for s being object st s in the carrier of S holds

b_{1} . s = { (a `1) where a is Element of rng t : a `2 = s } ) & ( for s being object st s in the carrier of S holds

b_{2} . s = { (a `1) where a is Element of rng t : a `2 = s } ) holds

b_{1} = b_{2}

end;
let t be non empty Relation;

func S variables_in t -> ManySortedSet of the carrier of S means :Def2: :: MSAFREE3:def 2

for s being object st s in the carrier of S holds

it . s = { (a `1) where a is Element of rng t : a `2 = s } ;

existence for s being object st s in the carrier of S holds

it . s = { (a `1) where a is Element of rng t : a `2 = s } ;

ex b

for s being object st s in the carrier of S holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines variables_in MSAFREE3:def 2 :

for S being ManySortedSign

for t being non empty Relation

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

( b_{3} = S variables_in t iff for s being object st s in the carrier of S holds

b_{3} . s = { (a `1) where a is Element of rng t : a `2 = s } );

for S being ManySortedSign

for t being non empty Relation

for b

( b

b

definition

let S be ManySortedSign ;

let X be ManySortedSet of the carrier of S;

let t be non empty Relation;

coherence

X (/\) (S variables_in t) is ManySortedSubset of X

end;
let X be ManySortedSet of the carrier of S;

let t be non empty Relation;

coherence

X (/\) (S variables_in t) is ManySortedSubset of X

proof end;

:: deftheorem defines variables_in MSAFREE3:def 3 :

for S being ManySortedSign

for X being ManySortedSet of the carrier of S

for t being non empty Relation holds X variables_in t = X (/\) (S variables_in t);

for S being ManySortedSign

for X being ManySortedSet of the carrier of S

for t being non empty Relation holds X variables_in t = X (/\) (S variables_in t);

theorem Th9: :: MSAFREE3:9

for S being ManySortedSign

for X being ManySortedSet of the carrier of S

for t being non empty Relation

for V being ManySortedSubset of X holds

( V = X variables_in t iff for s being set st s in the carrier of S holds

V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } )

for X being ManySortedSet of the carrier of S

for t being non empty Relation

for V being ManySortedSubset of X holds

( V = X variables_in t iff for s being set st s in the carrier of S holds

V . s = (X . s) /\ { (a `1) where a is Element of rng t : a `2 = s } )

proof end;

theorem Th10: :: MSAFREE3:10

for S being ManySortedSign

for s, x being object holds

( ( s in the carrier of S implies (S variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being object st ( s9 <> s or not s in the carrier of S ) holds

(S variables_in (root-tree [x,s])) . s9 = {} ) )

for s, x being object holds

( ( s in the carrier of S implies (S variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being object st ( s9 <> s or not s in the carrier of S ) holds

(S variables_in (root-tree [x,s])) . s9 = {} ) )

proof end;

theorem Th11: :: MSAFREE3:11

for x, z being set

for S being ManySortedSign

for s being set st s in the carrier of S holds

for p being DTree-yielding FinSequence holds

( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) )

for S being ManySortedSign

for s being set st s in the carrier of S holds

for p being DTree-yielding FinSequence holds

( x in (S variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (S variables_in t) . s ) )

proof end;

theorem Th12: :: MSAFREE3:12

for S being ManySortedSign

for X being ManySortedSet of the carrier of S

for s, x being set holds

( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds

(X variables_in (root-tree [x,s])) . s9 = {} ) )

for X being ManySortedSet of the carrier of S

for s, x being set holds

( ( x in X . s implies (X variables_in (root-tree [x,s])) . s = {x} ) & ( for s9 being set st ( s9 <> s or not x in X . s ) holds

(X variables_in (root-tree [x,s])) . s9 = {} ) )

proof end;

theorem Th13: :: MSAFREE3:13

for x, z being set

for S being ManySortedSign

for X being ManySortedSet of the carrier of S

for s being set st s in the carrier of S holds

for p being DTree-yielding FinSequence holds

( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (X variables_in t) . s ) )

for S being ManySortedSign

for X being ManySortedSet of the carrier of S

for s being set st s in the carrier of S holds

for p being DTree-yielding FinSequence holds

( x in (X variables_in ([z, the carrier of S] -tree p)) . s iff ex t being DecoratedTree st

( t in rng p & x in (X variables_in t) . s ) )

proof end;

theorem Th14: :: MSAFREE3:14

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X holds S variables_in t c= X

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X holds S variables_in t c= X

proof end;

definition

let S be non void Signature;

let X be V8() ManySortedSet of the carrier of S;

let t be Term of S,X;

correctness

coherence

S variables_in t is ManySortedSubset of X;

end;
let X be V8() ManySortedSet of the carrier of S;

let t be Term of S,X;

correctness

coherence

S variables_in t is ManySortedSubset of X;

proof end;

:: deftheorem defines variables_in MSAFREE3:def 4 :

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X holds variables_in t = S variables_in t;

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X holds variables_in t = S variables_in t;

theorem Th15: :: MSAFREE3:15

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X holds variables_in t = X variables_in t by Th14, PBOOLE:23;

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X holds variables_in t = X variables_in t by Th14, PBOOLE:23;

definition

let S be non void Signature;

let Y be V8() ManySortedSet of the carrier of S;

let X be ManySortedSet of the carrier of S;

ex b_{1} being MSSubset of (FreeMSA Y) st

for s being SortSymbol of S holds b_{1} . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) }

uniqueness

for b_{1}, b_{2} being MSSubset of (FreeMSA Y) st ( for s being SortSymbol of S holds b_{1} . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ) & ( for s being SortSymbol of S holds b_{2} . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ) holds

b_{1} = b_{2};

end;
let Y be V8() ManySortedSet of the carrier of S;

let X be ManySortedSet of the carrier of S;

func S -Terms (X,Y) -> MSSubset of (FreeMSA Y) means :Def5: :: MSAFREE3:def 5

for s being SortSymbol of S holds it . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ;

existence for s being SortSymbol of S holds it . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ;

ex b

for s being SortSymbol of S holds b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def5 defines -Terms MSAFREE3:def 5 :

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for b_{4} being MSSubset of (FreeMSA Y) holds

( b_{4} = S -Terms (X,Y) iff for s being SortSymbol of S holds b_{4} . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } );

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for b

( b

theorem Th16: :: MSAFREE3:16

for x being set

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds

x is Term of S,Y

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S st x in (S -Terms (X,Y)) . s holds

x is Term of S,Y

proof end;

theorem Th17: :: MSAFREE3:17

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for t being Term of S,Y

for s being SortSymbol of S st t in (S -Terms (X,Y)) . s holds

( the_sort_of t = s & variables_in t c= X )

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for t being Term of S,Y

for s being SortSymbol of S st t in (S -Terms (X,Y)) . s holds

( the_sort_of t = s & variables_in t c= X )

proof end;

theorem Th18: :: MSAFREE3:18

for x being set

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S holds

( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for s being SortSymbol of S holds

( root-tree [x,s] in (S -Terms (X,Y)) . s iff ( x in X . s & x in Y . s ) )

proof end;

theorem Th19: :: MSAFREE3:19

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for o being OperSymbol of S

for p being ArgumentSeq of Sym (o,Y) holds

( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) )

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S

for o being OperSymbol of S

for p being ArgumentSeq of Sym (o,Y) holds

( (Sym (o,Y)) -tree p in (S -Terms (X,Y)) . (the_result_sort_of o) iff rng p c= Union (S -Terms (X,Y)) )

proof end;

theorem Th20: :: MSAFREE3:20

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S

for A being MSSubset of (FreeMSA X) holds

( A is opers_closed iff for o being OperSymbol of S

for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds

(Sym (o,X)) -tree p in A . (the_result_sort_of o) )

for X being V8() ManySortedSet of the carrier of S

for A being MSSubset of (FreeMSA X) holds

( A is opers_closed iff for o being OperSymbol of S

for p being ArgumentSeq of Sym (o,X) st rng p c= Union A holds

(Sym (o,X)) -tree p in A . (the_result_sort_of o) )

proof end;

theorem Th21: :: MSAFREE3:21

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S holds S -Terms (X,Y) is opers_closed

proof end;

theorem Th22: :: MSAFREE3:22

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S holds (Reverse Y) "" X c= S -Terms (X,Y)

for Y being V8() ManySortedSet of the carrier of S

for X being ManySortedSet of the carrier of S holds (Reverse Y) "" X c= S -Terms (X,Y)

proof end;

theorem Th23: :: MSAFREE3:23

for S being non void Signature

for X being ManySortedSet of the carrier of S

for t being Term of S,(X (\/) ( the carrier of S --> {0}))

for s being SortSymbol of S st t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s holds

t in the Sorts of (Free (S,X)) . s

for X being ManySortedSet of the carrier of S

for t being Term of S,(X (\/) ( the carrier of S --> {0}))

for s being SortSymbol of S st t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s holds

t in the Sorts of (Free (S,X)) . s

proof end;

theorem Th24: :: MSAFREE3:24

for S being non void Signature

for X being ManySortedSet of the carrier of S holds the Sorts of (Free (S,X)) = S -Terms (X,(X (\/) ( the carrier of S --> {0})))

for X being ManySortedSet of the carrier of S holds the Sorts of (Free (S,X)) = S -Terms (X,(X (\/) ( the carrier of S --> {0})))

proof end;

theorem :: MSAFREE3:25

for S being non void Signature

for X being ManySortedSet of the carrier of S holds (FreeMSA (X (\/) ( the carrier of S --> {0}))) | (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = Free (S,X)

for X being ManySortedSet of the carrier of S holds (FreeMSA (X (\/) ( the carrier of S --> {0}))) | (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) = Free (S,X)

proof end;

theorem Th26: :: MSAFREE3:26

for S being non void Signature

for X, Y being V8() ManySortedSet of the carrier of S

for A being MSSubAlgebra of FreeMSA X

for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds

MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)

for X, Y being V8() ManySortedSet of the carrier of S

for A being MSSubAlgebra of FreeMSA X

for B being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds

MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #)

proof end;

theorem Th27: :: MSAFREE3:27

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for Y being ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds S variables_in t c= X

for X being V9() ManySortedSet of the carrier of S

for Y being ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds S variables_in t c= X

proof end;

theorem Th28: :: MSAFREE3:28

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X holds variables_in t c= X

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X holds variables_in t c= X

proof end;

theorem Th29: :: MSAFREE3:29

for S being non void Signature

for X, Y being V8() ManySortedSet of the carrier of S

for t1 being Term of S,X

for t2 being Term of S,Y st t1 = t2 holds

the_sort_of t1 = the_sort_of t2

for X, Y being V8() ManySortedSet of the carrier of S

for t1 being Term of S,X

for t2 being Term of S,Y st t1 = t2 holds

the_sort_of t1 = the_sort_of t2

proof end;

theorem Th30: :: MSAFREE3:30

for S being non void Signature

for X, Y being V8() ManySortedSet of the carrier of S

for t being Term of S,Y st variables_in t c= X holds

t is Term of S,X

for X, Y being V8() ManySortedSet of the carrier of S

for t being Term of S,Y st variables_in t c= X holds

t is Term of S,X

proof end;

theorem :: MSAFREE3:31

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S holds Free (S,X) = FreeMSA X

for X being V8() ManySortedSet of the carrier of S holds Free (S,X) = FreeMSA X

proof end;

theorem Th32: :: MSAFREE3:32

for S being non void Signature

for Y being V8() ManySortedSet of the carrier of S

for t being Term of S,Y

for p being Element of dom t holds variables_in (t | p) c= variables_in t

for Y being V8() ManySortedSet of the carrier of S

for t being Term of S,Y

for p being Element of dom t holds variables_in (t | p) c= variables_in t

proof end;

theorem Th33: :: MSAFREE3:33

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for p being Element of dom t holds t | p is Element of (Free (S,X))

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for p being Element of dom t holds t | p is Element of (Free (S,X))

proof end;

theorem Th34: :: MSAFREE3:34

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X

for a being Element of rng t holds a = [(a `1),(a `2)]

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X

for a being Element of rng t holds a = [(a `1),(a `2)]

proof end;

theorem :: MSAFREE3:35

for x being set

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for s being SortSymbol of S holds

( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for s being SortSymbol of S holds

( ( x in (S variables_in t) . s implies [x,s] in rng t ) & ( [x,s] in rng t implies ( x in (S variables_in t) . s & x in X . s ) ) )

proof end;

theorem :: MSAFREE3:36

for S being non void Signature

for X being ManySortedSet of the carrier of S st ( for s being SortSymbol of S st X . s = {} holds

ex o being OperSymbol of S st

( the_result_sort_of o = s & the_arity_of o = {} ) ) holds

Free (S,X) is non-empty

for X being ManySortedSet of the carrier of S st ( for s being SortSymbol of S st X . s = {} holds

ex o being OperSymbol of S st

( the_result_sort_of o = s & the_arity_of o = {} ) ) holds

Free (S,X) is non-empty

proof end;

theorem Th37: :: MSAFREE3:37

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for B being MSSubAlgebra of A

for o being OperSymbol of S holds Args (o,B) c= Args (o,A)

for A being MSAlgebra over S

for B being MSSubAlgebra of A

for o being OperSymbol of S holds Args (o,B) c= Args (o,A)

proof end;

theorem Th38: :: MSAFREE3:38

for S being non void Signature

for A being feasible MSAlgebra over S

for B being MSSubAlgebra of A holds B is feasible

for A being feasible MSAlgebra over S

for B being MSSubAlgebra of A holds B is feasible

proof end;

registration

let S be non void Signature;

let A be feasible MSAlgebra over S;

coherence

for b_{1} being MSSubAlgebra of A holds b_{1} is feasible
by Th38;

end;
let A be feasible MSAlgebra over S;

coherence

for b

theorem Th39: :: MSAFREE3:39

for S being non void Signature

for X being ManySortedSet of the carrier of S holds

( Free (S,X) is feasible & Free (S,X) is free )

for X being ManySortedSet of the carrier of S holds

( Free (S,X) is feasible & Free (S,X) is free )

proof end;

registration

let S be non void Signature;

let X be ManySortedSet of the carrier of S;

coherence

( Free (S,X) is feasible & Free (S,X) is free ) by Th39;

end;
let X be ManySortedSet of the carrier of S;

coherence

( Free (S,X) is feasible & Free (S,X) is free ) by Th39;