:: MSAFREE3 semantic presentation

registration

let S be non empty non void ManySortedSign ;
let A be non empty MSAlgebra of S;
cluster Union the Sorts of A -> non empty ;
coherence

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let A be non empty MSAlgebra of S;
mode Element of A is Element of Union the Sorts of A;

end;

theorem Th1: :: MSAFREE3:1

for X being set
for f being Function st X c= dom f & f is one-to-one holds
f " (f .: X) = X

proof end;

theorem :: MSAFREE3:2

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

proof end;

definition

let S be non void Signature;
let X be ManySortedSet of the carrier of S;
canceled;
func Free S,X -> strict MSAlgebra of S means :Def2: :: MSAFREE3:def 2
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 ;
existence

proof end;

end;

:: deftheorem MSAFREE3:def 1 :

:: deftheorem Def2 defines Free MSAFREE3:def 2 :

theorem Th3: :: MSAFREE3:3

for x being set
for S being non void Signature
for X being V3 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 Th4: :: MSAFREE3:4

for x being set
for S being non void Signature
for Y being V3 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 Th5: :: MSAFREE3:5

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

proof end;

theorem Th6: :: MSAFREE3:6

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)

proof end;

registration

let S be non void Signature;
let X be V4 ManySortedSet of the carrier of S;
cluster Free S,X -> strict non empty ;
coherence

proof end;

end;

theorem :: MSAFREE3:7

for x being set
for S being non void Signature
for X being V3 ManySortedSet of the carrier of S holds
( x is Element of (FreeMSA X) iff x is Term of S,X )

proof end;

theorem Th8: :: MSAFREE3:8

for S being non void Signature
for X being V3 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 Th9: :: MSAFREE3:9

for S being non void Signature
for X being V4 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 V4 ManySortedSet of the carrier of S;
cluster -> Relation-like Function-like Element of Union the Sorts of (Free S,X);
coherence by Th9;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V4 ManySortedSet of the carrier of S;
cluster -> Relation-like Function-like finite DecoratedTree-like Element of Union the Sorts of (Free S,X);
coherence by Th9;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V4 ManySortedSet of the carrier of S;
cluster -> Relation-like Function-like finite DecoratedTree-like finite-branching Element of Union the Sorts of (Free S,X);
coherence ;

end;

registration

cluster -> non empty set ;
coherence

proof end;

end;

definition

let S be ManySortedSign ;
let t be non empty Relation;
func S variables_in t -> ManySortedSet of the carrier of S means :Def3: :: MSAFREE3:def 3
for s being set st s in the carrier of S holds
it . s = { (a `1 ) where a is Element of rng t : a `2 = s } ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines variables_in MSAFREE3:def 3 :

definition

let S be ManySortedSign ;
let X be ManySortedSet of the carrier of S;
let t be non empty Relation;
func X variables_in t -> ManySortedSubset of X equals :: MSAFREE3:def 4
X /\ (S variables_in t);
coherence

proof end;

end;

:: deftheorem defines variables_in MSAFREE3:def 4 :

theorem Th10: :: MSAFREE3:10

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

proof end;

theorem Th11: :: MSAFREE3:11

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

proof end;

theorem Th12: :: MSAFREE3:12

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

proof end;

theorem Th13: :: MSAFREE3:13

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 s' being set st ( s' <> s or not x in X . s ) holds
(X variables_in (root-tree [x,s])) . s' = {} ) )

proof end;

theorem Th14: :: MSAFREE3:14

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

proof end;

theorem Th15: :: MSAFREE3:15

for S being non void Signature
for X being V3 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 V3 ManySortedSet of the carrier of S;
let t be Term of S,X;
func variables_in t -> ManySortedSubset of X equals :: MSAFREE3:def 5
S variables_in t;
correctness

proof end;

end;

:: deftheorem defines variables_in MSAFREE3:def 5 :

theorem Th16: :: MSAFREE3:16

for S being non void Signature
for X being V3 ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t = X variables_in t

proof end;

definition

let S be non void Signature;
let Y be V3 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 :Def6: :: MSAFREE3:def 6
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

proof end;

correctness

proof end;

end;

:: deftheorem Def6 defines -Terms MSAFREE3:def 6 :

theorem Th17: :: MSAFREE3:17

for x being set
for S being non void Signature
for Y being V3 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 Th18: :: MSAFREE3:18

for S being non void Signature
for Y being V3 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 Th19: :: MSAFREE3:19

for x being set
for S being non void Signature
for Y being V3 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 Th20: :: MSAFREE3:20

for S being non void Signature
for Y being V3 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 Th21: :: MSAFREE3:21

for S being non void Signature
for X being V3 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 Th22: :: MSAFREE3:22

for S being non void Signature
for Y being V3 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 Th23: :: MSAFREE3:23

for S being non void Signature
for Y being V3 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 Th24: :: MSAFREE3:24

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

proof end;

theorem Th25: :: MSAFREE3:25

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

proof end;

theorem :: MSAFREE3:26

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

proof end;

theorem Th27: :: MSAFREE3:27

for S being non void Signature
for X, Y being V3 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 Th28: :: MSAFREE3:28

for S being non void Signature
for X being V4 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 Th29: :: MSAFREE3:29

for S being non void Signature
for X being V3 ManySortedSet of the carrier of S
for t being Term of S,X holds variables_in t c= X

proof end;

theorem Th30: :: MSAFREE3:30

for S being non void Signature
for X, Y being V3 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 Th31: :: MSAFREE3:31

for S being non void Signature
for X, Y being V3 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:32

for S being non void Signature
for X being V3 ManySortedSet of the carrier of S holds Free S,X = FreeMSA X

proof end;

theorem Th33: :: MSAFREE3:33

for S being non void Signature
for Y being V3 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 Th34: :: MSAFREE3:34

for S being non void Signature
for X being V4 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 Th35: :: MSAFREE3:35

for S being non void Signature
for X being V3 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:36

for x being set
for S being non void Signature
for X being V4 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:37

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

proof end;

theorem Th38: :: MSAFREE3:38

for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for B being MSSubAlgebra of A
for o being OperSymbol of S holds Args o,B c= Args o,A

proof end;

theorem Th39: :: MSAFREE3:39

for S being non void Signature
for A being feasible MSAlgebra of 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 of S;
cluster -> feasible MSSubAlgebra of A;
coherence by Th39;

end;

theorem Th40: :: MSAFREE3:40

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 )

proof end;

registration

let S be non void Signature;
let X be ManySortedSet of the carrier of S;
cluster Free S,X -> strict free feasible ;
coherence by Th40;

end;