MSAFREE3: Yet another construction of free algebra

:: Yet another construction of free algebra
:: 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;

cluster Union the Sorts of A -> non 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 ;
existence

proof end;

end;

:: deftheorem Def1 defines Free MSAFREE3:def 1 :

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 ;

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

end;

registration

cluster Relation-like Function-like DecoratedTree-like -> non empty for set ;

coherence 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 object st s in the carrier of S holds
it . s = { (a `1) where a is Element of rng t : a `2 = s } ;

proof end;

proof end;

end;

:: deftheorem Def2 defines variables_in MSAFREE3:def 2 :

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

proof end;

end;

:: deftheorem defines variables_in MSAFREE3:def 3 :

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

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;

proof end;

end;

:: deftheorem defines variables_in MSAFREE3:def 4 :

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

proof end;

proof end;

end;

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

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

end;