:: Yet another construction of free algebra
:: by Grzegorz Bancerek and Artur Korni{\l}owicz
::
:: Received August 8, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users


begin

registration
let S be non empty non void ManySortedSign ;
let A be non empty MSAlgebra over S;
cluster Union the Sorts of A -> non empty ;
coherence
not Union the Sorts of A is empty
proof end;
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;

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

definition
let S be non void Signature;
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
for b1, b2 being strict MSAlgebra over S st ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( b1 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) & ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( b2 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) holds
b1 = b2
;
existence
ex b1 being strict MSAlgebra over S ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( b1 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X )
proof end;
end;

:: deftheorem Def1 defines Free MSAFREE3:def 1 :
for S being non void Signature
for X being ManySortedSet of the carrier of S
for b3 being strict MSAlgebra over S holds
( b3 = Free (S,X) iff ex A being MSSubset of (FreeMSA (X \/ ( the carrier of S --> {0}))) st
( b3 = GenMSAlg A & A = (Reverse (X \/ ( the carrier of S --> {0}))) "" X ) );

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

registration
let S be non void Signature;
let X be V9() ManySortedSet of the carrier of S;
cluster Free (S,X) -> strict non empty ;
coherence
not Free (S,X) is empty
proof end;
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 )
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 )
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}))
proof end;

registration
let S be non empty non void ManySortedSign ;
let X be V9() ManySortedSet of the carrier of S;
cluster -> Relation-like Function-like for Element of Union the Sorts of (Free (S,X));
coherence
for b1 being Element of (Free (S,X)) holds
( b1 is Relation-like & b1 is Function-like )
by Th8;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V9() ManySortedSet of the carrier of S;
cluster -> finite DecoratedTree-like for Element of Union the Sorts of (Free (S,X));
coherence
for b1 being Element of (Free (S,X)) holds
( b1 is finite & b1 is DecoratedTree-like )
by Th8;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V9() ManySortedSet of the carrier of S;
cluster -> finite-branching for Element of Union the Sorts of (Free (S,X));
coherence
for b1 being Element of (Free (S,X)) holds b1 is finite-branching
;
end;

registration
cluster Relation-like Function-like DecoratedTree-like -> non empty for set ;
coherence
for b1 being DecoratedTree holds not b1 is empty
by RELAT_1:38;
end;

definition
let S be ManySortedSign ;
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 set st s in the carrier of S holds
it . s = { (a `1) where a is Element of rng t : a `2 = s } ;
existence
ex b1 being ManySortedSet of the carrier of S st
for s being set st s in the carrier of S holds
b1 . s = { (a `1) where a is Element of rng t : a `2 = s }
proof end;
uniqueness
for b1, b2 being ManySortedSet of the carrier of S st ( for s being set st s in the carrier of S holds
b1 . s = { (a `1) where a is Element of rng t : a `2 = s } ) & ( for s being set st s in the carrier of S holds
b2 . s = { (a `1) where a is Element of rng t : a `2 = s } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines variables_in MSAFREE3:def 2 :
for S being ManySortedSign
for t being non empty Relation
for b3 being ManySortedSet of the carrier of S holds
( b3 = S variables_in t iff for s being set st s in the carrier of S holds
b3 . s = { (a `1) where a is Element of rng t : a `2 = s } );

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 3
X /\ (S variables_in t);
coherence
X /\ (S variables_in t) is ManySortedSubset of X
proof end;
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);

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

theorem Th10: :: MSAFREE3:10
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 s9 being set 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 ) )
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 = {} ) )
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 ) )
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
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;
func variables_in t -> ManySortedSubset of X equals :: MSAFREE3:def 4
S variables_in t;
correctness
coherence
S variables_in t is ManySortedSubset of X
;
proof end;
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;

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;

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;
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
ex b1 being MSSubset of (FreeMSA Y) st
for s being SortSymbol of S holds b1 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) }
proof end;
correctness
uniqueness
for b1, b2 being MSSubset of (FreeMSA Y) st ( for s being SortSymbol of S holds b1 . 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 b2 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } ) holds
b1 = b2
;
proof end;
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 b4 being MSSubset of (FreeMSA Y) holds
( b4 = S -Terms (X,Y) iff for s being SortSymbol of S holds b4 . s = { t where t is Term of S,Y : ( the_sort_of t = s & variables_in t c= X ) } );

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
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 )
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 ) )
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)) )
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) )
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
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)
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
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})))
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)
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 #)
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
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
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
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
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
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
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))
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)]
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 ) ) )
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
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)
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
proof end;

registration
let S be non void Signature;
let A be feasible MSAlgebra over S;
cluster -> feasible for MSSubAlgebra of A;
coherence
for b1 being MSSubAlgebra of A holds b1 is feasible
by Th38;
end;

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 )
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
( Free (S,X) is feasible & Free (S,X) is free )
by Th39;
end;