:: MSAFREE3 semantic presentation

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non empty MSAlgebra of c₁;
cluster Union the Sorts of a₂ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non empty MSAlgebra of c₁;
mode Element of a₂ is Element of Union the Sorts of a₂;

end;

theorem Th1: :: MSAFREE3:1

for b₁ being set
for b₂ being Function st b₁ c= dom b₂ & b₂ is one-to-one holds
b₂ " (b₂ .: b₁) = b₁

proof end;

theorem Th2: :: MSAFREE3:2

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being ManySortedFunction of b₁ st b₃ is "1-1" & b₂ c= doms b₃ holds
b₃ "" (b₃ .:.: b₂) = b₂

proof end;

definition

let c₁ be non void Signature;
let c₂ be ManySortedSet of the carrier of c₁;
canceled;
func Free c₁,c₂ -> strict MSAlgebra of a₁ means :Def2: :: MSAFREE3:def 2
ex b₁ being MSSubset of (FreeMSA (a₂ \/ (the carrier of a₁ --> {0}))) st
( a₃ = GenMSAlg b₁ & b₁ = (Reverse (a₂ \/ (the carrier of a₁ --> {0}))) "" a₂ );
uniqueness ;
existence

proof end;

end;

:: deftheorem Def1 MSAFREE3:def 1 :

:: deftheorem Def2 defines Free MSAFREE3:def 2 :

theorem Th3: :: MSAFREE3:3

for b₁ being set
for b₂ being non void Signature
for b₃ being V3 ManySortedSet of the carrier of b₂
for b₄ being SortSymbol of b₂ holds
( [b₁,b₄] in the carrier of (DTConMSA b₃) iff b₁ in b₃ . b₄ )

proof end;

theorem Th4: :: MSAFREE3:4

for b₁ being set
for b₂ being non void Signature
for b₃ being V3 ManySortedSet of the carrier of b₂
for b₄ being ManySortedSet of the carrier of b₂
for b₅ being SortSymbol of b₂ holds
( ( b₁ in b₄ . b₅ & b₁ in b₃ . b₅ ) iff root-tree [b₁,b₅] in ((Reverse b₃) "" b₄) . b₅ )

proof end;

theorem Th5: :: MSAFREE3:5

for b₁ being set
for b₂ being non void Signature
for b₃ being ManySortedSet of the carrier of b₂
for b₄ being SortSymbol of b₂ st b₁ in b₃ . b₄ holds
root-tree [b₁,b₄] in the Sorts of (Free b₂,b₃) . b₄

proof end;

theorem Th6: :: MSAFREE3:6

for b₁ being non void Signature
for b₂ being ManySortedSet of the carrier of b₁
for b₃ being OperSymbol of b₁ st the_arity_of b₃ = {} holds
root-tree [b₃,the carrier of b₁] in the Sorts of (Free b₁,b₂) . (the_result_sort_of b₃)

proof end;

registration

let c₁ be non void Signature;
let c₂ be V4 ManySortedSet of the carrier of c₁;
cluster Free a₁,a₂ -> strict non empty ;
coherence

proof end;

end;

theorem Th7: :: MSAFREE3:7

for b₁ being set
for b₂ being non void Signature
for b₃ being V3 ManySortedSet of the carrier of b₂ holds
( b₁ is Element of (FreeMSA b₃) iff b₁ is Term of b₂,b₃ )

proof end;

theorem Th8: :: MSAFREE3:8

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being SortSymbol of b₁
for b₄ being Term of b₁,b₂ holds
( b₄ in the Sorts of (FreeMSA b₂) . b₃ iff the_sort_of b₄ = b₃ )

proof end;

theorem Th9: :: MSAFREE3:9

for b₁ being non void Signature
for b₂ being V4 ManySortedSet of the carrier of b₁
for b₃ being Element of (Free b₁,b₂) holds b₃ is Term of b₁,(b₂ \/ (the carrier of b₁ --> {0}))

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be V4 ManySortedSet of the carrier of c₁;
cluster -> Relation-like Function-like Element of Union the Sorts of (Free a₁,a₂);
coherence by Th9;

end;

registration

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

end;

registration

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

end;

registration

cluster -> non empty set ;
coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines variables_in MSAFREE3:def 3 :

definition

let c₁ be ManySortedSign ;
let c₂ be ManySortedSet of the carrier of c₁;
let c₃ be non empty Relation;
func c₂ variables_in c₃ -> ManySortedSubset of a₂ equals :: MSAFREE3:def 4
a₂ /\ (a₁ variables_in a₃);
coherence

proof end;

end;

:: deftheorem Def4 defines variables_in MSAFREE3:def 4 :

theorem Th10: :: MSAFREE3:10

for b₁ being ManySortedSign
for b₂ being ManySortedSet of the carrier of b₁
for b₃ being non empty Relation
for b₄ being ManySortedSubset of b₂ holds
( b₄ = b₂ variables_in b₃ iff for b₅ being set st b₅ in the carrier of b₁ holds
b₄ . b₅ = (b₂ . b₅) /\ { (b₆ `1 ) where B is Element of rng b₃ : b₆ `2 = b₅ } )

proof end;

theorem Th11: :: MSAFREE3:11

for b₁ being ManySortedSign
for b₂, b₃ being set holds
( ( b₂ in the carrier of b₁ implies (b₁ variables_in (root-tree [b₃,b₂])) . b₂ = {b₃} ) & ( for b₄ being set st ( b₄ <> b₂ or not b₂ in the carrier of b₁ ) holds
(b₁ variables_in (root-tree [b₃,b₂])) . b₄ = {} ) )

proof end;

theorem Th12: :: MSAFREE3:12

for b₁, b₂ being set
for b₃ being ManySortedSign
for b₄ being set st b₄ in the carrier of b₃ holds
for b₅ being DTree-yielding FinSequence holds
( b₁ in (b₃ variables_in ([b₂,the carrier of b₃] -tree b₅)) . b₄ iff ex b₆ being DecoratedTree st
( b₆ in rng b₅ & b₁ in (b₃ variables_in b₆) . b₄ ) )

proof end;

theorem Th13: :: MSAFREE3:13

for b₁ being ManySortedSign
for b₂ being ManySortedSet of the carrier of b₁
for b₃, b₄ being set holds
( ( b₄ in b₂ . b₃ implies (b₂ variables_in (root-tree [b₄,b₃])) . b₃ = {b₄} ) & ( for b₅ being set st ( b₅ <> b₃ or not b₄ in b₂ . b₃ ) holds
(b₂ variables_in (root-tree [b₄,b₃])) . b₅ = {} ) )

proof end;

theorem Th14: :: MSAFREE3:14

for b₁, b₂ being set
for b₃ being ManySortedSign
for b₄ being ManySortedSet of the carrier of b₃
for b₅ being set st b₅ in the carrier of b₃ holds
for b₆ being DTree-yielding FinSequence holds
( b₁ in (b₄ variables_in ([b₂,the carrier of b₃] -tree b₆)) . b₅ iff ex b₇ being DecoratedTree st
( b₇ in rng b₆ & b₁ in (b₄ variables_in b₇) . b₅ ) )

proof end;

theorem Th15: :: MSAFREE3:15

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being Term of b₁,b₂ holds b₁ variables_in b₃ c= b₂

proof end;

definition

let c₁ be non void Signature;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be Term of c₁,c₂;
func variables_in c₃ -> ManySortedSubset of a₂ equals :: MSAFREE3:def 5
a₁ variables_in a₃;
correctness

proof end;

end;

:: deftheorem Def5 defines variables_in MSAFREE3:def 5 :

theorem Th16: :: MSAFREE3:16

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being Term of b₁,b₂ holds variables_in b₃ = b₂ variables_in b₃

proof end;

definition

let c₁ be non void Signature;
let c₂ be V3 ManySortedSet of the carrier of c₁;
let c₃ be ManySortedSet of the carrier of c₁;
func c₁ -Terms c₃,c₂ -> MSSubset of (FreeMSA a₂) means :Def6: :: MSAFREE3:def 6
for b₁ being SortSymbol of a₁ holds a₄ . b₁ = { b₂ where B is Term of a₁,a₂ : ( the_sort_of b₂ = b₁ & variables_in b₂ c= a₃ ) } ;
existence

proof end;

correctness

proof end;

end;

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

theorem Th17: :: MSAFREE3:17

for b₁ being set
for b₂ being non void Signature
for b₃ being V3 ManySortedSet of the carrier of b₂
for b₄ being ManySortedSet of the carrier of b₂
for b₅ being SortSymbol of b₂ st b₁ in (b₂ -Terms b₄,b₃) . b₅ holds
b₁ is Term of b₂,b₃

proof end;

theorem Th18: :: MSAFREE3:18

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being ManySortedSet of the carrier of b₁
for b₄ being Term of b₁,b₂
for b₅ being SortSymbol of b₁ st b₄ in (b₁ -Terms b₃,b₂) . b₅ holds
( the_sort_of b₄ = b₅ & variables_in b₄ c= b₃ )

proof end;

theorem Th19: :: MSAFREE3:19

for b₁ being set
for b₂ being non void Signature
for b₃ being V3 ManySortedSet of the carrier of b₂
for b₄ being ManySortedSet of the carrier of b₂
for b₅ being SortSymbol of b₂ holds
( root-tree [b₁,b₅] in (b₂ -Terms b₄,b₃) . b₅ iff ( b₁ in b₄ . b₅ & b₁ in b₃ . b₅ ) )

proof end;

theorem Th20: :: MSAFREE3:20

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being ManySortedSet of the carrier of b₁
for b₄ being OperSymbol of b₁
for b₅ being ArgumentSeq of Sym b₄,b₂ holds
( (Sym b₄,b₂) -tree b₅ in (b₁ -Terms b₃,b₂) . (the_result_sort_of b₄) iff rng b₅ c= Union (b₁ -Terms b₃,b₂) )

proof end;

theorem Th21: :: MSAFREE3:21

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being MSSubset of (FreeMSA b₂) holds
( b₃ is opers_closed iff for b₄ being OperSymbol of b₁
for b₅ being ArgumentSeq of Sym b₄,b₂ st rng b₅ c= Union b₃ holds
(Sym b₄,b₂) -tree b₅ in b₃ . (the_result_sort_of b₄) )

proof end;

theorem Th22: :: MSAFREE3:22

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being ManySortedSet of the carrier of b₁ holds b₁ -Terms b₃,b₂ is opers_closed

proof end;

theorem Th23: :: MSAFREE3:23

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being ManySortedSet of the carrier of b₁ holds (Reverse b₂) "" b₃ c= b₁ -Terms b₃,b₂

proof end;

theorem Th24: :: MSAFREE3:24

for b₁ being non void Signature
for b₂ being ManySortedSet of the carrier of b₁
for b₃ being Term of b₁,(b₂ \/ (the carrier of b₁ --> {0}))
for b₄ being SortSymbol of b₁ st b₃ in (b₁ -Terms b₂,(b₂ \/ (the carrier of b₁ --> {0}))) . b₄ holds
b₃ in the Sorts of (Free b₁,b₂) . b₄

proof end;

theorem Th25: :: MSAFREE3:25

for b₁ being non void Signature
for b₂ being ManySortedSet of the carrier of b₁ holds the Sorts of (Free b₁,b₂) = b₁ -Terms b₂,(b₂ \/ (the carrier of b₁ --> {0}))

proof end;

theorem Th26: :: MSAFREE3:26

for b₁ being non void Signature
for b₂ being ManySortedSet of the carrier of b₁ holds (FreeMSA (b₂ \/ (the carrier of b₁ --> {0}))) | (b₁ -Terms b₂,(b₂ \/ (the carrier of b₁ --> {0}))) = Free b₁,b₂

proof end;

theorem Th27: :: MSAFREE3:27

for b₁ being non void Signature
for b₂, b₃ being V3 ManySortedSet of the carrier of b₁
for b₄ being MSSubAlgebra of FreeMSA b₂
for b₅ being MSSubAlgebra of FreeMSA b₃ st the Sorts of b₄ = the Sorts of b₅ holds
MSAlgebra(# the Sorts of b₄,the Charact of b₄ #) = MSAlgebra(# the Sorts of b₅,the Charact of b₅ #)

proof end;

theorem Th28: :: MSAFREE3:28

for b₁ being non void Signature
for b₂ being V4 ManySortedSet of the carrier of b₁
for b₃ being ManySortedSet of the carrier of b₁
for b₄ being Element of (Free b₁,b₂) holds b₁ variables_in b₄ c= b₂

proof end;

theorem Th29: :: MSAFREE3:29

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being Term of b₁,b₂ holds variables_in b₃ c= b₂

proof end;

theorem Th30: :: MSAFREE3:30

for b₁ being non void Signature
for b₂, b₃ being V3 ManySortedSet of the carrier of b₁
for b₄ being Term of b₁,b₂
for b₅ being Term of b₁,b₃ st b₄ = b₅ holds
the_sort_of b₄ = the_sort_of b₅

proof end;

theorem Th31: :: MSAFREE3:31

for b₁ being non void Signature
for b₂, b₃ being V3 ManySortedSet of the carrier of b₁
for b₄ being Term of b₁,b₃ st variables_in b₄ c= b₂ holds
b₄ is Term of b₁,b₂

proof end;

theorem Th32: :: MSAFREE3:32

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁ holds Free b₁,b₂ = FreeMSA b₂

proof end;

theorem Th33: :: MSAFREE3:33

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being Term of b₁,b₂
for b₄ being Element of dom b₃ holds variables_in (b₃ | b₄) c= variables_in b₃

proof end;

theorem Th34: :: MSAFREE3:34

for b₁ being non void Signature
for b₂ being V4 ManySortedSet of the carrier of b₁
for b₃ being Element of (Free b₁,b₂)
for b₄ being Element of dom b₃ holds b₃ | b₄ is Element of (Free b₁,b₂)

proof end;

theorem Th35: :: MSAFREE3:35

for b₁ being non void Signature
for b₂ being V3 ManySortedSet of the carrier of b₁
for b₃ being Term of b₁,b₂
for b₄ being Element of rng b₃ holds b₄ = [(b₄ `1 ),(b₄ `2 )]

proof end;

theorem Th36: :: MSAFREE3:36

for b₁ being set
for b₂ being non void Signature
for b₃ being V4 ManySortedSet of the carrier of b₂
for b₄ being Element of (Free b₂,b₃)
for b₅ being SortSymbol of b₂ holds
( ( b₁ in (b₂ variables_in b₄) . b₅ implies [b₁,b₅] in rng b₄ ) & ( [b₁,b₅] in rng b₄ implies ( b₁ in (b₂ variables_in b₄) . b₅ & b₁ in b₃ . b₅ ) ) )

proof end;

theorem Th37: :: MSAFREE3:37

for b₁ being non void Signature
for b₂ being ManySortedSet of the carrier of b₁ st ( for b₃ being SortSymbol of b₁ st b₂ . b₃ = {} holds
ex b₄ being OperSymbol of b₁ st
( the_result_sort_of b₄ = b₃ & the_arity_of b₄ = {} ) ) holds
Free b₁,b₂ is non-empty

proof end;

theorem Th38: :: MSAFREE3:38

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubAlgebra of b₂
for b₄ being OperSymbol of b₁ holds Args b₄,b₃ c= Args b₄,b₂

proof end;

theorem Th39: :: MSAFREE3:39

for b₁ being non void Signature
for b₂ being feasible MSAlgebra of b₁
for b₃ being MSSubAlgebra of b₂ holds b₃ is feasible

proof end;

registration

let c₁ be non void Signature;
let c₂ be feasible MSAlgebra of c₁;
cluster -> feasible MSSubAlgebra of a₂;
coherence by Th39;

end;

theorem Th40: :: MSAFREE3:40

for b₁ being non void Signature
for b₂ being ManySortedSet of the carrier of b₁ holds
( Free b₁,b₂ is feasible & Free b₁,b₂ is free )

proof end;

registration

let c₁ be non void Signature;
let c₂ be ManySortedSet of the carrier of c₁;
cluster Free a₁,a₂ -> strict free feasible ;
coherence by Th40;

end;