:: Free Term Algebras
:: by Grzegorz Bancerek
::
:: Received May 15, 2012
:: Copyright (c) 2012-2021 Association of Mizar Users

theorem Th1: :: MSAFREE4:1

for I being set
for f1, f2 being ManySortedSet of I st f1 c= f2 holds
Union f1 c= Union f2

proof end;

deffunc H₁( Function, set ) -> set = $1 . $2;

definition

let I be set ;
let X be V5() ManySortedSet of I;
let A be Component of X;
:: original: Element
redefine mode Element of A -> Element of Union X;
coherence
for b₁ being Element of A holds b₁ is Element of Union X

proof end;

end;

definition

let I be set ;
let X be ManySortedSet of I;
let i be Element of I;
:: original: .
redefine func X . i -> Component of X;
coherence
X . i is Component of X

proof end;

end;

Lm1: now :: thesis: for I being set
for X, Y being ManySortedSet of I
for f being ManySortedFunction of X,Y
for x being object holds f . x is Function of (X . x),(Y . x)

let I be set ; :: thesis: for X, Y being ManySortedSet of I
for f being ManySortedFunction of X,Y
for x being object holds b₈ . b₉ is Function of (b₆ . b₉),(b₇ . b₉)
let X, Y be ManySortedSet of I; :: thesis: for f being ManySortedFunction of X,Y
for x being object holds b₆ . b₇ is Function of (b₄ . b₇),(b₅ . b₇)
let f be ManySortedFunction of X,Y; :: thesis: for x being object holds b₅ . b₆ is Function of (b₃ . b₆),(b₄ . b₆)
let x be object ; :: thesis: b₄ . b₅ is Function of (b₂ . b₅),(b₃ . b₅)

per cases ( x in I or x nin I ) ;

suppose x in I ; :: thesis: b₄ . b₅ is Function of (b₂ . b₅),(b₃ . b₅)

hence f . x is Function of (X . x),(Y . x) by PBOOLE:def 15; :: thesis: verum

end;

suppose A1: x nin I ; :: thesis: b₄ . b₅ is Function of (b₂ . b₅),(b₃ . b₅)

( dom f = I & dom X = I & dom Y = I ) by PARTFUN1:def 2;
then ( f . x = {} & X . x = {} & Y . x = {} & dom {} = {} & rng {} = {} ) by A1, FUNCT_1:def 2;
hence f . x is Function of (X . x),(Y . x) by FUNCT_2:2; :: thesis: verum

end;

end;

end;

definition

let I be set ;
let X, Y be ManySortedSet of I;
let f be ManySortedFunction of X,Y;
let x be object ;
:: original: .
redefine func f . x -> Function of (X . x),(Y . x);
coherence
f . x is Function of (X . x),(Y . x) by Lm1;

end;

scheme :: MSAFREE4:sch 1
Sch1{ F₁() -> set , F₂() -> V5() ManySortedSet of F₁(), F₃( object , object ) -> set } :

ex f being ManySortedFunction of F₁() st
for x being set st x in F₁() holds
( dom (f . x) = F₂() . x & ( for y being Element of F₂() . x holds (f . x) . y = F₃(x,y) ) )

proof end;

scheme :: MSAFREE4:sch 2
Sch2{ F₁() -> non empty set , F₂() -> V5() ManySortedSet of F₁(), F₃() -> V5() ManySortedSet of F₁(), F₄( object , object ) -> set } :

ex f being ManySortedFunction of F₂(),F₃() st
for i being Element of F₁()
for a being Element of F₂() . i holds (f . i) . a = F₄(i,a)

provided

A1: for i being Element of F₁()
for a being Element of F₂() . i holds F₄(i,a) in F₃() . i

proof end;

definition

let X be non empty set ;
let O be set ;
let f be Function of O,X;
let g be ManySortedSet of X;
:: original: *
redefine func g * f -> ManySortedSet of O;
coherence
f * g is ManySortedSet of O ;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let F be ManySortedSet of S -Terms X;
let o be OperSymbol of S;
let p be ArgumentSeq of Sym (o,X);

cluster p * F -> FinSequence-like ;

coherence
F * p is FinSequence-like

proof end;

end;

theorem Th2: :: MSAFREE4:2

for x being set holds Subtrees (root-tree x) = {(root-tree x)}

proof end;

registration

let f be DTree-yielding Function;

cluster proj2 f -> constituted-DTrees ;

coherence
rng f is constituted-DTrees by TREES_3:def 11;

end;

theorem Th3: :: MSAFREE4:3

for x being set
for p being non empty DTree-yielding FinSequence holds Subtrees (x -tree p) = {(x -tree p)} \/ (Subtrees (rng p))

proof end;

theorem Th4: :: MSAFREE4:4

for x being set holds Subtrees (x -tree {}) = {(x -tree {})}

proof end;

theorem :: MSAFREE4:5

for x being set holds x -tree {} = root-tree x

proof end;

registration

cluster non empty Relation-like NAT -defined Function-like finite V32() FinSequence-like FinSubsequence-like DTree-yielding countable for set ;

existence
ex b₁ being FinSequence st
( b₁ is V32() & b₁ is DTree-yielding & not b₁ is empty )

proof end;

cluster non empty Relation-like NAT -defined Function-like finite V32() FinSequence-like FinSubsequence-like Tree-yielding countable for set ;

existence
ex b₁ being FinSequence st
( b₁ is V32() & b₁ is Tree-yielding & not b₁ is empty )

proof end;

end;

registration

let f be finite-yielding Function-yielding Function;

cluster doms f -> finite-yielding ;

coherence
doms f is finite-yielding

proof end;

end;

registration

let p be V32() Tree-yielding FinSequence;

cluster tree p -> finite ;

coherence
tree p is finite

proof end;

end;

registration

let t be finite DecoratedTree;

cluster Subtrees t -> finite-membered ;

coherence
Subtrees t is finite-membered ;

end;

registration

let p be V32() DTree-yielding FinSequence;
let x be set ;

cluster x -tree p -> finite ;

coherence
x -tree p is finite

proof end;

end;

theorem Th6: :: MSAFREE4:6

for t1, t2 being finite DecoratedTree st t1 in Subtrees t2 holds
height (dom t1) <= height (dom t2)

proof end;

theorem Th7: :: MSAFREE4:7

for x, y being set
for p being DTree-yielding FinSequence st p is V32() holds
for t being DecoratedTree st x in Subtrees t & t in rng p holds
x <> y -tree p

proof end;

registration

let S be non empty non void ManySortedSign ;
let X be ManySortedSet of S;

cluster Relation-like S -Terms X -valued Function-like -> S -Terms X -valued finite-yielding for set ;

coherence
for b₁ being S -Terms X -valued Function holds b₁ is finite-yielding

proof end;

end;

theorem Th8: :: MSAFREE4:8

for X being non empty constituted-DTrees set
for t being DecoratedTree st t in X holds
Subtrees t c= Subtrees X

proof end;

theorem Th9: :: MSAFREE4:9

for X being non empty constituted-DTrees set holds X c= Subtrees X

proof end;

theorem Th10: :: MSAFREE4:10

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for t being Term of S,X
for x being set st x in Subtrees t holds
x is Term of S,X

proof end;

theorem Th11: :: MSAFREE4:11

for x being set
for p being DTree-yielding FinSequence holds rng p c= Subtrees (x -tree p)

proof end;

theorem Th12: :: MSAFREE4:12

for t1, t2 being DecoratedTree st t1 in Subtrees t2 holds
Subtrees t1 c= Subtrees t2

proof end;

theorem Th13: :: MSAFREE4:13

for S being non empty non void ManySortedSign
for X being ManySortedSet of S
for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) holds
(Den (o,(Free (S,X)))) . p = [o, the carrier of S] -tree p

proof end;

registration

let I be set ;
let A, B be V5() ManySortedSet of I;
let f be ManySortedFunction of A,B;

cluster rngs f -> V5() ;

coherence
rngs f is non-empty

proof end;

end;

registration

let S be non empty non void ManySortedSign ;

cluster -> Relation-like Function-like for Element of Union the Sorts of (TermAlg S);

coherence
for b₁ being Element of (TermAlg S) holds
( b₁ is Relation-like & b₁ is Function-like )

proof end;

end;

registration

let I be set ;
let A be ManySortedSet of I;
let f be FinSequence of I;

cluster f * A -> dom f -defined ;

coherence
A * f is dom f -defined

proof end;

end;

registration

let I be set ;
let A be ManySortedSet of I;
let f be FinSequence of I;

cluster f * A -> dom f -defined total for dom f -defined Relation;

coherence
for b₁ being dom f -defined Relation st b₁ = A * f holds
b₁ is total

proof end;

end;

theorem :: MSAFREE4:14

for I being non empty set
for J being set
for A, B being ManySortedSet of I st A c= B holds
for f being Function of J,I holds A * f c= B * f

proof end;

theorem Th15: :: MSAFREE4:15

for I being set
for A, B being ManySortedSet of I st A c= B holds
for f being FinSequence of I holds A * f c= B * f

proof end;

theorem Th16: :: MSAFREE4:16

for I being set
for A, B being ManySortedSet of I st A c= B holds
product A c= product B

proof end;

theorem Th17: :: MSAFREE4:17

for x being set
for R being weakly-normalizing with_UN_property Relation st x is_a_normal_form_wrt R holds
nf (x,R) = x

proof end;

theorem Th18: :: MSAFREE4:18

for x being set
for R being weakly-normalizing with_UN_property Relation holds nf ((nf (x,R)),R) = nf (x,R)

proof end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A be MSSubset of (FreeMSA X);
let x be object ;

cluster -> Relation-like Function-like for Element of A . x;

coherence
for b₁ being Element of A . x holds
( b₁ is Relation-like & b₁ is Function-like )

proof end;

end;

definition

let I be set ;
let A be ManySortedSet of I;

attr A is countable means :Def1: :: MSAFREE4:def 1
for x being set st x in I holds
A . x is countable ;

end;

:: deftheorem Def1 defines countable MSAFREE4:def 1 :
for I being set
for A being ManySortedSet of I holds
( A is countable iff for x being set st x in I holds
A . x is countable );

registration

let I be set ;
let X be countable set ;

cluster I --> X -> countable for ManySortedSet of I;

coherence
for b₁ being ManySortedSet of I st b₁ = I --> X holds
b₁ is countable by FUNCOP_1:7;

end;

registration

let I be set ;

cluster Relation-like V5() I -defined Function-like total countable for set ;

existence
ex b₁ being ManySortedSet of I st
( b₁ is V5() & b₁ is countable )

proof end;

end;

registration

let I be set ;
let X be countable ManySortedSet of I;
let x be object ;

cluster X . x -> countable ;

coherence
X . x is countable

proof end;

end;

registration

let A be countable set ;

cluster Relation-like A -defined NAT -valued Function-like one-to-one V18(A, NAT ) for Element of bool [:A,NAT:];

existence
ex b₁ being Function of A,NAT st b₁ is one-to-one

proof end;

end;

registration

let I be set ;
let X0 be countable ManySortedSet of I;

cluster Relation-like I -defined Function-like total Function-yielding Relation-yielding "1-1" for ManySortedFunction of X0,I --> NAT;

existence
ex b₁ being ManySortedFunction of X0,I --> NAT st b₁ is "1-1"

proof end;

end;

theorem Th19: :: MSAFREE4:19

for S being set
for X being ManySortedSet of S
for Y being V5() ManySortedSet of S
for w being ManySortedFunction of X,Y holds rngs w is ManySortedSubset of Y

proof end;

theorem :: MSAFREE4:20

for S being set
for X being countable ManySortedSet of S ex Y being ManySortedSubset of S --> NAT ex w being ManySortedFunction of X,S --> NAT st
( w is "1-1" & Y = rngs w & ( for x being set st x in S holds
( w . x is Enumeration of (X . x) & Y . x = card (X . x) ) ) )

proof end;

theorem Th21: :: MSAFREE4:21

for I being set
for A being ManySortedSet of I
for B being V5() ManySortedSet of I holds A is_transformable_to B

proof end;

theorem Th22: :: MSAFREE4:22

for I being set
for A, B, C being V5() ManySortedSet of I
for f being ManySortedFunction of A,B st B is ManySortedSubset of C holds
f is ManySortedFunction of A,C

proof end;

theorem Th23: :: MSAFREE4:23

for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for f being ManySortedFunction of A,B st f is "onto" holds
ex g being ManySortedFunction of B,A st f ** g = id B

proof end;

Lm2: now :: thesis: for p being FinSequence
for i being Nat st i < len p holds
i + 1 in dom p

let p be FinSequence; :: thesis: for i being Nat st i < len p holds
i + 1 in dom p
let i be Nat; :: thesis: ( i < len p implies i + 1 in dom p )
assume i < len p ; :: thesis: i + 1 in dom p
then ( i + 1 <= len p & 1 <= i + 1 ) by NAT_1:13, NAT_1:11;
hence i + 1 in dom p by FINSEQ_3:25; :: thesis: verum

end;

theorem Th24: :: MSAFREE4:24

for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 holds
for o being OperSymbol of S st B1 is_closed_on o holds
B2 is_closed_on o ;

theorem Th25: :: MSAFREE4:25

for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 holds
for o being OperSymbol of S st B1 is_closed_on o holds
o /. B2 = o /. B1

proof end;

theorem Th26: :: MSAFREE4:26

for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 & B1 is opers_closed holds
Opers (A2,B2) = Opers (A1,B1)

proof end;

theorem Th27: :: MSAFREE4:27

for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 & B1 is opers_closed holds
B2 is opers_closed by Th24;

theorem :: MSAFREE4:28

for S being non empty non void ManySortedSign
for A1, A2, B being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubAlgebra of A1 st MSAlgebra(# the Sorts of B, the Charact of B #) = MSAlgebra(# the Sorts of B1, the Charact of B1 #) holds
B is MSSubAlgebra of A2

proof end;

theorem :: MSAFREE4:29

for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st A2 is empty holds
for h being ManySortedFunction of A1,A2 holds h is_homomorphism A1,A2

proof end;

theorem Th30: :: MSAFREE4:30

for S being non empty non void ManySortedSign
for A1, A2, B1 being MSAlgebra over S
for B2 being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) & MSAlgebra(# the Sorts of B1, the Charact of B1 #) = MSAlgebra(# the Sorts of B2, the Charact of B2 #) holds
for h1 being ManySortedFunction of A1,B1
for h2 being ManySortedFunction of A2,B2 st h1 = h2 & h1 is_homomorphism A1,B1 holds
h2 is_homomorphism A2,B2

proof end;

definition

let I be set ;
let X be ManySortedSet of I;

:: original: trivial-yielding
redefine attr X is trivial-yielding means :Def2: :: MSAFREE4:def 2
for x being set st x in I holds
X . x is trivial ;

compatibility
( X is trivial-yielding iff for x being set st x in I holds
X . x is trivial )

proof end;

end;

:: deftheorem Def2 defines trivial-yielding MSAFREE4:def 2 :
for I being set
for X being ManySortedSet of I holds
( X is trivial-yielding iff for x being set st x in I holds
X . x is trivial );

registration

let I be set ;

cluster Relation-like V5() I -defined Function-like total V276() for set ;

existence
ex b₁ being ManySortedSet of I st
( b₁ is V5() & b₁ is V276() )

proof end;

end;

registration

let I be set ;
let S be V276() ManySortedSet of I;
let x be object ;

cluster S . x -> trivial ;

coherence
S . x is trivial

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;

attr A is trivial means :Def3: :: MSAFREE4:def 3
the Sorts of A is V276();

end;

:: deftheorem Def3 defines trivial MSAFREE4:def 3 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S holds
( A is trivial iff the Sorts of A is V276() );

registration

let S be non empty non void ManySortedSign ;

cluster strict non-empty disjoint_valued trivial for MSAlgebra over S;

existence
ex b₁ being strict MSAlgebra over S st
( b₁ is trivial & b₁ is disjoint_valued & b₁ is non-empty )

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let A be trivial MSAlgebra over S;

cluster the Sorts of A -> V276() ;

coherence
the Sorts of A is trivial-yielding by Def3;

end;

theorem Th31: :: MSAFREE4:31

for S being non empty non void ManySortedSign
for A being non-empty trivial MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s holds A |= e

proof end;

theorem Th32: :: MSAFREE4:32

for S being non empty non void ManySortedSign
for A being non-empty trivial MSAlgebra over S
for T being EqualSet of S holds A |= T by Th31;

theorem Th33: :: MSAFREE4:33

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for T being non-empty trivial MSAlgebra over S
for f being ManySortedFunction of A,T holds f is_homomorphism A,T

proof end;

theorem Th34: :: MSAFREE4:34

for S being non empty non void ManySortedSign
for T being non-empty trivial MSAlgebra over S
for A being non-empty MSSubAlgebra of T holds MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of T, the Charact of T #)

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let C be MSAlgebra over S;

attr C is A -Image means :: MSAFREE4:def 4
ex B being non-empty MSAlgebra over S ex h being ManySortedFunction of A,B st
( h is_homomorphism A,B & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h );

end;

:: deftheorem defines -Image MSAFREE4:def 4 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for C being MSAlgebra over S holds
( C is A -Image iff ex B being non-empty MSAlgebra over S ex h being ManySortedFunction of A,B st
( h is_homomorphism A,B & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h ) );

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;

cluster A -Image -> non-empty for MSAlgebra over S;

coherence
for b₁ being MSAlgebra over S st b₁ is A -Image holds
b₁ is non-empty

proof end;

cluster strict non-empty feasible non empty A -Image for MSAlgebra over S;

existence
ex b₁ being strict non-empty MSAlgebra over S st b₁ is A -Image

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let A, C be non-empty MSAlgebra over S;

redefine attr C is A -Image means :Def5: :: MSAFREE4:def 5
ex h being ManySortedFunction of A,C st h is_epimorphism A,C;

compatibility
( C is A -Image iff ex h being ManySortedFunction of A,C st h is_epimorphism A,C )

proof end;

end;

:: deftheorem Def5 defines -Image MSAFREE4:def 5 :
for S being non empty non void ManySortedSign
for A, C being non-empty MSAlgebra over S holds
( C is A -Image iff ex h being ManySortedFunction of A,C st h is_epimorphism A,C );

definition

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
mode image of A is non-empty A -Image MSAlgebra over S;

end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;

cluster non-empty disjoint_valued feasible non empty trivial A -Image for MSAlgebra over S;

existence
ex b₁ being image of A st
( b₁ is disjoint_valued & b₁ is trivial )

proof end;

end;

theorem Th35: :: MSAFREE4:35

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for B being b₂ -Image MSAlgebra over S
for s being SortSymbol of S
for e being Element of (Equations S) . s st A |= e holds
B |= e

proof end;

theorem Th36: :: MSAFREE4:36

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for B being b₂ -Image MSAlgebra over S
for T being EqualSet of S st A |= T holds
B |= T by Th35;

definition

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A be MSAlgebra over S;

attr A is X,S -terms means :Def6: :: MSAFREE4:def 6
the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X));

end;

:: deftheorem Def6 defines -terms MSAFREE4:def 6 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being MSAlgebra over S holds
( A is X,S -terms iff the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X)) );

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;

cluster Free (S,X) -> X,S -terms ;

coherence
Free (S,X) is X,S -terms

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;

cluster Free (S,X) -> non-empty disjoint_valued ;

coherence
( Free (S,X) is non-empty & Free (S,X) is disjoint_valued )

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;

cluster strict non-empty X,S -terms for MSAlgebra over S;

existence
ex b₁ being strict MSAlgebra over S st
( b₁ is X,S -terms & b₁ is non-empty )

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A be X,S -terms MSAlgebra over S;

attr A is all_vars_including means :Def7: :: MSAFREE4:def 7
FreeGen X is ManySortedSubset of the Sorts of A;

attr A is inheriting_operations means :Def8: :: MSAFREE4:def 8
for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of A . (the_result_sort_of o) holds
( p in Args (o,A) & (Den (o,A)) . p = (Den (o,(Free (S,X)))) . p );

attr A is free_in_itself means :Def9: :: MSAFREE4:def 9
for f being ManySortedFunction of FreeGen X, the Sorts of A
for G being ManySortedSubset of the Sorts of A st G = FreeGen X holds
ex h being ManySortedFunction of A,A st
( h is_homomorphism A,A & f = h || G );

end;

:: deftheorem Def7 defines all_vars_including MSAFREE4:def 7 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms MSAlgebra over S holds
( A is all_vars_including iff FreeGen X is ManySortedSubset of the Sorts of A );

:: deftheorem Def8 defines inheriting_operations MSAFREE4:def 8 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms MSAlgebra over S holds
( A is inheriting_operations iff for o being OperSymbol of S
for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of A . (the_result_sort_of o) holds
( p in Args (o,A) & (Den (o,A)) . p = (Den (o,(Free (S,X)))) . p ) );

:: deftheorem Def9 defines free_in_itself MSAFREE4:def 9 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms MSAlgebra over S holds
( A is free_in_itself iff for f being ManySortedFunction of FreeGen X, the Sorts of A
for G being ManySortedSubset of the Sorts of A st G = FreeGen X holds
ex h being ManySortedFunction of A,A st
( h is_homomorphism A,A & f = h || G ) );

theorem :: MSAFREE4:37

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A, B being non-empty MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) & A is X,S -terms holds
B is X,S -terms ;

theorem :: MSAFREE4:38

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A, B being non-empty b₂,b₁ -terms MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
( ( A is all_vars_including implies B is all_vars_including ) & ( A is inheriting_operations implies B is inheriting_operations ) & ( A is free_in_itself implies B is free_in_itself ) )

proof end;

registration

let J be non empty non void ManySortedSign ;
let T be non-empty MSAlgebra over J;

cluster non empty Relation-like V5() the carrier of J -defined Function-like total for GeneratorSet of T;

existence
not for b₁ being GeneratorSet of T holds b₁ is V5()

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;

cluster Free (S,X) -> all_vars_including inheriting_operations free_in_itself ;

coherence
( Free (S,X) is all_vars_including & Free (S,X) is inheriting_operations & Free (S,X) is free_in_itself )

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;

cluster X,S -terms all_vars_including -> non-empty X,S -terms for MSAlgebra over S;

coherence
for b₁ being X,S -terms MSAlgebra over S st b₁ is all_vars_including holds
b₁ is non-empty

proof end;

cluster strict X,S -terms all_vars_including inheriting_operations free_in_itself for MSAlgebra over S;

existence
ex b₁ being strict X,S -terms MSAlgebra over S st
( b₁ is all_vars_including & b₁ is inheriting_operations & b₁ is free_in_itself )

proof end;

end;

theorem Th39: :: MSAFREE4:39

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A0 being non-empty b₂,b₁ -terms MSAlgebra over S holds
( ( for t being Element of A0 holds t is Element of (Free (S,X)) ) & ( for s being SortSymbol of S
for t being Element of A0,s holds t is Element of (Free (S,X)),s ) )

proof end;

theorem Th40: :: MSAFREE4:40

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A1 being b₂,b₁ -terms all_vars_including MSAlgebra over S
for s being SortSymbol of S
for x being Element of X . s holds root-tree [x,s] is Element of A1,s

proof end;

theorem Th41: :: MSAFREE4:41

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A1 being b₂,b₁ -terms all_vars_including MSAlgebra over S
for o being OperSymbol of S holds Args (o,A1) c= Args (o,(Free (S,X)))

proof end;

registration

let S be set ;

cluster Relation-like V5() S -defined Function-like total disjoint_valued for set ;

existence
ex b₁ being ManySortedSet of S st
( b₁ is disjoint_valued & b₁ is V5() )

proof end;

end;

registration

let S be set ;
let T be V5() disjoint_valued ManySortedSet of S;

cluster -> disjoint_valued for ManySortedSubset of T;

coherence
for b₁ being ManySortedSubset of T holds b₁ is disjoint_valued

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;

cluster strict X,S -terms for MSAlgebra over S;

existence
ex b₁ being MSAlgebra over S st
( b₁ is X,S -terms & b₁ is strict )

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A1 be X,S -terms all_vars_including MSAlgebra over S;

func canonical_homomorphism A1 -> ManySortedFunction of (Free (S,X)),A1 means :Def10: :: MSAFREE4:def 10
( it is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = it || G ) );

existence
ex b₁ being ManySortedFunction of (Free (S,X)),A1 st
( b₁ is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = b₁ || G ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedFunction of (Free (S,X)),A1 st b₁ is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = b₁ || G ) & b₂ is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = b₂ || G ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines canonical_homomorphism MSAFREE4:def 10 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A1 being b₂,b₁ -terms all_vars_including MSAlgebra over S
for b₄ being ManySortedFunction of (Free (S,X)),A1 holds
( b₄ = canonical_homomorphism A1 iff ( b₄ is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = b₄ || G ) ) );

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A0 be non-empty X,S -terms MSAlgebra over S;

cluster -> Relation-like Function-like for Element of Union the Sorts of A0;

coherence
for b₁ being Element of A0 holds
( b₁ is Function-like & b₁ is Relation-like )

proof end;

let s be SortSymbol of S;

cluster -> Relation-like Function-like for Element of the Sorts of A0 . s;

coherence
for b₁ being Element of A0,s holds
( b₁ is Function-like & b₁ is Relation-like )

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let A0 be non-empty X,S -terms MSAlgebra over S;

cluster -> DecoratedTree-like for Element of Union the Sorts of A0;

coherence
for b₁ being Element of A0 holds b₁ is DecoratedTree-like

proof end;

let s be SortSymbol of S;

cluster -> DecoratedTree-like for Element of the Sorts of A0 . s;

coherence
for b₁ being Element of A0,s holds b₁ is DecoratedTree-like

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;

cluster X,S -terms -> disjoint_valued for MSAlgebra over S;

coherence
for b₁ being MSAlgebra over S st b₁ is X,S -terms holds
b₁ is disjoint_valued

proof end;

end;

theorem Th42: :: MSAFREE4:42

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A0 being non-empty b₂,b₁ -terms MSAlgebra over S
for t being Element of A0 holds t is Term of S,X

proof end;

theorem Th43: :: MSAFREE4:43

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A0 being non-empty b₂,b₁ -terms MSAlgebra over S
for t being Element of A0
for s being SortSymbol of S st t in the Sorts of (Free (S,X)) . s holds
t in the Sorts of A0 . s

proof end;

theorem :: MSAFREE4:44

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A2 being b₂,b₁ -terms all_vars_including inheriting_operations MSAlgebra over S
for t being Element of A2
for p being Element of dom t holds t | p is Element of A2

proof end;

theorem Th45: :: MSAFREE4:45

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A2 being b₂,b₁ -terms all_vars_including inheriting_operations MSAlgebra over S holds FreeGen X is GeneratorSet of A2

proof end;

theorem :: MSAFREE4:46

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for T being non-empty b₂,b₁ -terms free_in_itself MSAlgebra over S
for A being image of T
for G being GeneratorSet of T st G = FreeGen X holds
for f being ManySortedFunction of G, the Sorts of A ex h being ManySortedFunction of T,A st
( h is_homomorphism T,A & f = h || G )

proof end;

theorem Th47: :: MSAFREE4:47

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A2 being b₂,b₁ -terms all_vars_including inheriting_operations MSAlgebra over S holds
( canonical_homomorphism A2 is_epimorphism Free (S,X),A2 & ( for s being SortSymbol of S
for t being Element of A2,s holds ((canonical_homomorphism A2) . s) . t = t ) )

proof end;

theorem Th48: :: MSAFREE4:48

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A2 being b₂,b₁ -terms all_vars_including inheriting_operations MSAlgebra over S holds (canonical_homomorphism A2) ** (canonical_homomorphism A2) = canonical_homomorphism A2

proof end;

theorem :: MSAFREE4:49

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds A is Free (S,X) -Image

proof end;

theorem :: MSAFREE4:50

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for t being Element of (TermAlg S),s holds A |= t '=' t ;

theorem :: MSAFREE4:51

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for t1, t2 being Element of (TermAlg S),s st A |= t1 '=' t2 holds
A |= t2 '=' t1 ;

theorem :: MSAFREE4:52

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for s being SortSymbol of S
for t1, t2, t3 being Element of (TermAlg S),s st A |= t1 '=' t2 & A |= t2 '=' t3 holds
A |= t1 '=' t3

proof end;

theorem :: MSAFREE4:53

for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S
for a1, a2 being FinSequence st a1 in Args (o,(TermAlg S)) & a2 in Args (o,(TermAlg S)) & ( for i being Nat st i in dom (the_arity_of o) holds
for s being SortSymbol of S st s = (the_arity_of o) . i holds
for t1, t2 being Element of (TermAlg S),s st t1 = a1 . i & t2 = a2 . i holds
A |= t1 '=' t2 ) holds
for t1, t2 being Element of (TermAlg S),(the_result_sort_of o) st t1 = [o, the carrier of S] -tree a1 & t2 = [o, the carrier of S] -tree a2 holds
A |= t1 '=' t2

proof end;

definition

let S be non empty non void ManySortedSign ;
let T be EqualSet of S;
let A be MSAlgebra over S;

attr A is T -satisfying means :Def11: :: MSAFREE4:def 11
A |= T;

end;

:: deftheorem Def11 defines -satisfying MSAFREE4:def 11 :
for S being non empty non void ManySortedSign
for T being EqualSet of S
for A being MSAlgebra over S holds
( A is T -satisfying iff A |= T );

registration

let S be non empty non void ManySortedSign ;
let T be EqualSet of S;

cluster non-empty trivial T -satisfying for MSAlgebra over S;

existence
ex b₁ being MSAlgebra over S st
( b₁ is T -satisfying & b₁ is non-empty & b₁ is trivial )

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let T be EqualSet of S;
let A be non-empty T -satisfying MSAlgebra over S;

cluster non-empty A -Image -> non-empty T -satisfying for MSAlgebra over S;

coherence
for b₁ being non-empty MSAlgebra over S st b₁ is A -Image holds
b₁ is T -satisfying by Def11, Th36;

end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let T be EqualSet of S;
let G be GeneratorSet of A;

attr G is T -free means :: MSAFREE4:def 12
for B being non-empty T -satisfying MSAlgebra over S
for f being ManySortedFunction of G, the Sorts of B ex h being ManySortedFunction of A,B st
( h is_homomorphism A,B & h || G = f );

end;

:: deftheorem defines -free MSAFREE4:def 12 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for T being EqualSet of S
for G being GeneratorSet of A holds
( G is T -free iff for B being non-empty b₃ -satisfying MSAlgebra over S
for f being ManySortedFunction of G, the Sorts of B ex h being ManySortedFunction of A,B st
( h is_homomorphism A,B & h || G = f ) );

definition

let S be non empty non void ManySortedSign ;
let T be EqualSet of S;
let A be MSAlgebra over S;

attr A is T -free means :: MSAFREE4:def 13
ex G being GeneratorSet of A st G is T -free ;

end;

:: deftheorem defines -free MSAFREE4:def 13 :
for S being non empty non void ManySortedSign
for T being EqualSet of S
for A being MSAlgebra over S holds
( A is T -free iff ex G being GeneratorSet of A st G is T -free );

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;

func Equations (S,A) -> EqualSet of S means :Def14: :: MSAFREE4:def 14
for s being SortSymbol of S holds it . s = { e where e is Element of (Equations S) . s : A |= e } ;

existence
ex b₁ being EqualSet of S st
for s being SortSymbol of S holds b₁ . s = { e where e is Element of (Equations S) . s : A |= e }

proof end;

uniqueness
for b₁, b₂ being EqualSet of S st ( for s being SortSymbol of S holds b₁ . s = { e where e is Element of (Equations S) . s : A |= e } ) & ( for s being SortSymbol of S holds b₂ . s = { e where e is Element of (Equations S) . s : A |= e } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines Equations MSAFREE4:def 14 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for b₃ being EqualSet of S holds
( b₃ = Equations (S,A) iff for s being SortSymbol of S holds b₃ . s = { e where e is Element of (Equations S) . s : A |= e } );

theorem Th54: :: MSAFREE4:54

for S being non empty non void ManySortedSign
for A being MSAlgebra over S holds A |= Equations (S,A)

proof end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;

cluster A -Image -> A -Image Equations (S,A) -satisfying for MSAlgebra over S;

coherence
for b₁ being A -Image MSAlgebra over S holds b₁ is Equations (S,A) -satisfying

proof end;

end;

scheme :: MSAFREE4:sch 3
TermDefEx{ F₁() -> non empty non void ManySortedSign , F₂() -> V5() ManySortedSet of F₁(), F₃( set , set ) -> set , F₄( set , set ) -> set } :

ex F being ManySortedSet of F₁() -Terms F₂() st
( ( for s being SortSymbol of F₁()
for x being Element of F₂() . s holds F . (root-tree [x,s]) = F₃(x,s) ) & ( for o being OperSymbol of F₁()
for p being ArgumentSeq of Sym (o,F₂()) holds F . ((Sym (o,F₂())) -tree p) = F₄(o,(F * p)) ) )

proof end;

scheme :: MSAFREE4:sch 4
TermDefUniq{ F₁() -> non empty non void ManySortedSign , F₂() -> V5() ManySortedSet of F₁(), F₃( set , set ) -> set , F₄( set , FinSequence) -> set , F₅() -> ManySortedSet of F₁() -Terms F₂(), F₆() -> ManySortedSet of F₁() -Terms F₂() } :

F₅() = F₆()

provided

A1: for s being SortSymbol of F₁()
for x being Element of F₂() . s holds F₅() . (root-tree [x,s]) = F₃(x,s) and
A2: for o being OperSymbol of F₁()
for p being ArgumentSeq of Sym (o,F₂()) holds F₅() . ((Sym (o,F₂())) -tree p) = F₄(o,(F₅() * p)) and
A3: for s being SortSymbol of F₁()
for x being Element of F₂() . s holds F₆() . (root-tree [x,s]) = F₃(x,s) and
A4: for o being OperSymbol of F₁()
for p being ArgumentSeq of Sym (o,F₂()) holds F₆() . ((Sym (o,F₂())) -tree p) = F₄(o,(F₆() * p))

proof end;

definition

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let w be ManySortedFunction of X, the carrier of S --> NAT;
let t be Function;
assume A1: t is Element of (Free (S,X)) ;
deffunc H₂( set , set ) -> set = root-tree [((w . $2) . $1),$2];
deffunc H₃( OperSymbol of S, FinSequence) -> set = (Sym ($1,( the carrier of S --> NAT))) -tree $2;

func # (t,w) -> Element of (TermAlg S) means :Def15: :: MSAFREE4:def 15
ex F being ManySortedSet of S -Terms X st
( it = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) );

existence
ex b₁ being Element of (TermAlg S) ex F being ManySortedSet of S -Terms X st
( b₁ = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) )

proof end;

uniqueness
for b₁, b₂ being Element of (TermAlg S) st ex F being ManySortedSet of S -Terms X st
( b₁ = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) & ex F being ManySortedSet of S -Terms X st
( b₂ = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines # MSAFREE4:def 15 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for t being Function st t is Element of (Free (S,X)) holds
for b₅ being Element of (TermAlg S) holds
( b₅ = # (t,w) iff ex F being ManySortedSet of S -Terms X st
( b₅ = F . t & ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) ) );

theorem Th55: :: MSAFREE4:55

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for F being ManySortedSet of S -Terms X st ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) holds
for t being Element of (Free (S,X)) holds F . t = # (t,w)

proof end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let G be V5() MSSubset of (Free (S,X));
let s be SortSymbol of S;

cluster -> Relation-like Function-like for Element of G . s;

coherence
for b₁ being Element of G . s holds
( b₁ is Relation-like & b₁ is Function-like )

proof end;

end;

theorem Th56: :: MSAFREE4:56

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of (Free (S,X)),(TermAlg S) st
( h is_homomorphism Free (S,X), TermAlg S & ( for s being SortSymbol of S
for t being Element of (Free (S,X)),s holds # (t,w) = (h . s) . t ) )

proof end;

theorem Th57: :: MSAFREE4:57

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for s being SortSymbol of S
for x being Element of X . s holds # ((root-tree [x,s]),w) = root-tree [((w . s) . x),s]

proof end;

theorem Th58: :: MSAFREE4:58

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X)
for q being FinSequence st dom q = dom p & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom p & t = p . i holds
q . i = # (t,w) ) holds
# (((Sym (o,X)) -tree p),w) = (Sym (o,( the carrier of S --> NAT))) -tree q

proof end;

theorem Th59: :: MSAFREE4:59

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for Y being ManySortedSubset of X holds Free (S,Y) is MSSubAlgebra of Free (S,X)

proof end;

theorem Th60: :: MSAFREE4:60

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for t being Term of S,X holds
( # (t,w) is Element of (Free (S,(rngs w))),(the_sort_of t) & # (t,w) is Element of (TermAlg S),(the_sort_of t) )

proof end;

theorem :: MSAFREE4:61

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT
for F being ManySortedSet of S -Terms X st ( for s being SortSymbol of S
for x being Element of X . s holds F . (root-tree [x,s]) = root-tree [((w . s) . x),s] ) & ( for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds F . ((Sym (o,X)) -tree p) = (Sym (o,( the carrier of S --> NAT))) -tree (F * p) ) holds
for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,X) holds
( F * p in Args (o,(Free (S,(rngs w)))) & F * p in Args (o,(Free (S,( the carrier of S --> NAT)))) )

proof end;

theorem Th62: :: MSAFREE4:62

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of the carrier of S --> NAT,X ex h being ManySortedFunction of (TermAlg S),A st
( h is_homomorphism TermAlg S,A & ( for s being SortSymbol of S
for i being Nat holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s] ) )

proof end;

theorem Th63: :: MSAFREE4:63

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for w being ManySortedFunction of X, the carrier of S --> NAT ex h being ManySortedFunction of FreeGen X, the Sorts of (TermAlg S) st
for s being SortSymbol of S
for i being Element of X . s holds (h . s) . (root-tree [i,s]) = root-tree [((w . s) . i),s]

proof end;

theorem :: MSAFREE4:64

for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for A0 being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (TermAlg S),A0 st h is_homomorphism TermAlg S,A0 holds
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
ex Y being V5() ManySortedSubset of the carrier of S --> NAT ex B being MSSubset of (TermAlg S) ex ww being ManySortedFunction of (Free (S,Y)),A0 ex g being ManySortedFunction of A0,A0 st
( Y = rngs w & B = the Sorts of (Free (S,Y)) & FreeGen (rngs w) c= B & ww is_homomorphism Free (S,Y),A0 & g is_homomorphism A0,A0 & h || B = g ** ww & ( for s being SortSymbol of S
for i being Nat st i in Y . s holds
ex x being Element of X0 . s st
( (w . s) . x = i & (ww . s) . (root-tree [i,s]) = root-tree [x,s] ) ) )

proof end;

theorem Th65: :: MSAFREE4:65

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
ex g being ManySortedFunction of A,A st
( g is_homomorphism A,A & h = g ** (canonical_homomorphism A) )

proof end;

theorem Th66: :: MSAFREE4:66

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A)
for x0 being Element of Args (o,(Free (S,X))) st x0 = x holds
(canonical_homomorphism A) # x0 = x

proof end;

theorem Th67: :: MSAFREE4:67

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for o being OperSymbol of S
for x being Element of Args (o,A) holds (Den (o,A)) . x = ((canonical_homomorphism A) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)

proof end;

theorem Th68: :: MSAFREE4:68

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
for o being OperSymbol of S
for x being Element of Args (o,A) holds (h . (the_result_sort_of o)) . ((Den (o,A)) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x)

proof end;

theorem Th69: :: MSAFREE4:69

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being ManySortedFunction of (Free (S,X)),A st h is_homomorphism Free (S,X),A holds
for o being OperSymbol of S
for x being Element of Args (o,(Free (S,X))) holds (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . x) = (h . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . ((canonical_homomorphism A) # x))

proof end;

theorem :: MSAFREE4:70

for S being non empty non void ManySortedSign
for X0, Y0 being V5() countable ManySortedSet of S
for A being b₂,b₁ -terms all_vars_including inheriting_operations MSAlgebra over S
for h being ManySortedFunction of (Free (S,Y0)),A st h is_homomorphism Free (S,Y0),A holds
ex g being ManySortedFunction of (Free (S,Y0)),(Free (S,X0)) st
( g is_homomorphism Free (S,Y0), Free (S,X0) & h = (canonical_homomorphism A) ** g & ( for G being GeneratorSet of Free (S,Y0) st G = FreeGen Y0 holds
g || G = h || G ) )

proof end;

theorem Th71: :: MSAFREE4:71

for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for A0 being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of X0, the carrier of S --> NAT
for s being SortSymbol of S
for t being Element of (Free (S,X0)),s
for t1, t2 being Element of (TermAlg S),s st t1 = # (t,w) & t2 = # ((((canonical_homomorphism A0) . s) . t),w) holds
A0 |= t1 '=' t2

proof end;

theorem :: MSAFREE4:72

for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for A0 being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for w being ManySortedFunction of X0, the carrier of S --> NAT
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X0)))
for q being Element of Args (o,A0) st (canonical_homomorphism A0) # p = q holds
for t1, t2 being Term of S,X0 st t1 = (Den (o,(Free (S,X0)))) . p & t2 = (Den (o,A0)) . q holds
for t3, t4 being Element of (TermAlg S),(the_result_sort_of o) st t3 = # (t1,w) & t4 = # (t2,w) holds
A0 |= t3 '=' t4

proof end;

theorem Th73: :: MSAFREE4:73

for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
ex g being ManySortedFunction of (TermAlg S),(Free (S,X0)) st
( g is_homomorphism TermAlg S, Free (S,X0) & ( for s being SortSymbol of S
for t being Element of (Free (S,X0)),s holds (g . s) . (# (t,w)) = t ) )

proof end;

theorem Th74: :: MSAFREE4:74

for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for B being non-empty MSAlgebra over S
for h being ManySortedFunction of (Free (S,X0)),B st h is_homomorphism Free (S,X0),B holds
for w being ManySortedFunction of X0, the carrier of S --> NAT st w is "1-1" holds
for s being SortSymbol of S
for t1, t2 being Element of (Free (S,X0)),s
for t3, t4 being Element of (TermAlg S),s st t3 = # (t1,w) & t4 = # (t2,w) & B |= t3 '=' t4 holds
(h . s) . t1 = (h . s) . t2

proof end;

theorem Th75: :: MSAFREE4:75

for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for A0 being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for G being GeneratorSet of A0 st G = FreeGen X0 holds
G is Equations (S,A0) -free

proof end;

theorem :: MSAFREE4:76

for S being non empty non void ManySortedSign
for X0 being V5() countable ManySortedSet of S
for A0 being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds A0 is Equations (S,A0) -free

proof end;

definition

let I be set ;
let X, Y be ManySortedSet of I;
let R be ManySortedRelation of X,Y;
let x be object ;
:: original: .
redefine func R . x -> Relation of (X . x),(Y . x);
coherence
R . x is Relation of (X . x),(Y . x)

proof end;

end;

definition

let I be set ;
let X be ManySortedSet of I;
let R be ManySortedRelation of X;

attr R is terminating means :Def16: :: MSAFREE4:def 16
for x being set st x in I holds
R . x is strongly-normalizing ;

attr R is with_UN_property means :Def17: :: MSAFREE4:def 17
for x being set st x in I holds
R . x is with_UN_property ;

end;

:: deftheorem Def16 defines terminating MSAFREE4:def 16 :
for I being set
for X being ManySortedSet of I
for R being ManySortedRelation of X holds
( R is terminating iff for x being set st x in I holds
R . x is strongly-normalizing );

:: deftheorem Def17 defines with_UN_property MSAFREE4:def 17 :
for I being set
for X being ManySortedSet of I
for R being ManySortedRelation of X holds
( R is with_UN_property iff for x being set st x in I holds
R . x is with_UN_property );

registration

cluster empty -> empty strongly-normalizing with_UN_property for set ;

coherence
for b₁ being empty set holds
( b₁ is strongly-normalizing & b₁ is with_UN_property ) ;

end;

theorem Th77: :: MSAFREE4:77

for I being set
for A being ManySortedSet of I ex R being ManySortedRelation of A st
( R = I --> {} & R is terminating )

proof end;

registration

let I be set ;
let X be ManySortedSet of I;

cluster V6() -> terminating with_UN_property for ManySortedRelation of X,X;

coherence
for b₁ being ManySortedRelation of X st b₁ is V6() holds
( b₁ is with_UN_property & b₁ is terminating ) ;

cluster Relation-like V6() I -defined Function-like total Relation-yielding for ManySortedRelation of X,X;

existence
not for b₁ being ManySortedRelation of X holds b₁ is V6()

proof end;

end;

registration

let I be set ;
let X be ManySortedSet of I;
let R be terminating ManySortedRelation of X;
let i be object ;

cluster R . i -> strongly-normalizing for Relation;

coherence
for b₁ being Relation st b₁ = R . i holds
b₁ is strongly-normalizing

proof end;

end;

registration

let I be set ;
let X be ManySortedSet of I;
let R be with_UN_property ManySortedRelation of X;
let i be object ;

cluster R . i -> with_UN_property for Relation;

coherence
for b₁ being Relation st b₁ = R . i holds
b₁ is with_UN_property

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let R be ManySortedRelation of (Free (S,X));

attr R is NF-var means :Def18: :: MSAFREE4:def 18
for s being SortSymbol of S
for x being Element of (FreeGen X) . s holds x is_a_normal_form_wrt R . s;

end;

:: deftheorem Def18 defines NF-var MSAFREE4:def 18 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being ManySortedRelation of (Free (S,X)) holds
( R is NF-var iff for s being SortSymbol of S
for x being Element of (FreeGen X) . s holds x is_a_normal_form_wrt R . s );

theorem :: MSAFREE4:78

for x being set holds x is_a_normal_form_wrt {} ;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;

cluster V6() -> invariant stable NF-var for ManySortedRelation of the Sorts of (Free (S,X)), the Sorts of (Free (S,X));

coherence
for b₁ being ManySortedRelation of (Free (S,X)) st b₁ is V6() holds
( b₁ is NF-var & b₁ is invariant & b₁ is stable )

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;

cluster non empty Relation-like the carrier of S -defined Function-like total Relation-yielding invariant stable terminating with_UN_property NF-var for ManySortedRelation of the Sorts of (Free (S,X)), the Sorts of (Free (S,X));

existence
ex b₁ being invariant stable ManySortedRelation of (Free (S,X)) st
( b₁ is NF-var & b₁ is terminating & b₁ is with_UN_property )

proof end;

end;

scheme :: MSAFREE4:sch 5
A{ F₁() -> set , F₂() -> set , F₃() -> Relation, P₁[ set ] } :

P₁[F₂()]

provided

A1: P₁[F₁()] and
A2: F₃() reduces F₁(),F₂() and
A3: for y, z being set st F₃() reduces F₁(),y & [y,z] in F₃() & P₁[y] holds
P₁[z]

proof end;

scheme :: MSAFREE4:sch 6
B{ F₁() -> set , F₂() -> set , F₃() -> Relation, P₁[ set ] } :

P₁[F₁()]

provided

A1: P₁[F₂()] and
A2: F₃() reduces F₁(),F₂() and
A3: for y, z being set st [y,z] in F₃() & P₁[z] holds
P₁[y]

proof end;

definition

let X be non empty set ;
let R be strongly-normalizing with_UN_property Relation of X;
let x be Element of X;
:: original: nf
redefine func nf (x,R) -> Element of X;
coherence
nf (x,R) is Element of X

proof end;

end;

definition

let I be non empty set ;
let X be V5() ManySortedSet of I;
let R be terminating with_UN_property ManySortedRelation of X;

func NForms R -> V5() ManySortedSubset of X means :Def19: :: MSAFREE4:def 19
for i being Element of I holds it . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ;

existence
ex b₁ being V5() ManySortedSubset of X st
for i being Element of I holds b₁ . i = { (nf (x,(R . i))) where x is Element of X . i : verum }

proof end;

uniqueness
for b₁, b₂ being V5() ManySortedSubset of X st ( for i being Element of I holds b₁ . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ) & ( for i being Element of I holds b₂ . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines NForms MSAFREE4:def 19 :
for I being non empty set
for X being V5() ManySortedSet of I
for R being terminating with_UN_property ManySortedRelation of X
for b₄ being V5() ManySortedSubset of X holds
( b₄ = NForms R iff for i being Element of I holds b₄ . i = { (nf (x,(R . i))) where x is Element of X . i : verum } );

scheme :: MSAFREE4:sch 7
MSFLambda{ F₁() -> non empty set , F₂( object ) -> non empty set , F₃( object , object ) -> set } :

ex f being ManySortedFunction of F₁() st
for o being Element of F₁() holds
( dom (f . o) = F₂(o) & ( for x being Element of F₂(o) holds (f . o) . x = F₃(o,x) ) )

proof end;

definition

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let R be invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X));

func NFAlgebra R -> strict non-empty MSAlgebra over S means :Def20: :: MSAFREE4:def 20
( the Sorts of it = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,it) holds (Den (o,it)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) );

existence
ex b₁ being strict non-empty MSAlgebra over S st
( the Sorts of b₁ = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,b₁) holds (Den (o,b₁)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) )

proof end;

uniqueness
for b₁, b₂ being strict non-empty MSAlgebra over S st the Sorts of b₁ = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,b₁) holds (Den (o,b₁)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) & the Sorts of b₂ = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,b₂) holds (Den (o,b₂)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines NFAlgebra MSAFREE4:def 20 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for b₄ being strict non-empty MSAlgebra over S holds
( b₄ = NFAlgebra R iff ( the Sorts of b₄ = NForms R & ( for o being OperSymbol of S
for a being Element of Args (o,b₄) holds (Den (o,b₄)) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) ) );

theorem Th79: :: MSAFREE4:79

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for x being set
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for a being SortSymbol of S st x in (NForms R) . a holds
nf (x,(R . a)) = x

proof end;

Lm3: now :: thesis: for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for o being OperSymbol of S holds Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X)))

let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for o being OperSymbol of S holds Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X)))
let X be V5() ManySortedSet of S; :: thesis: for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for o being OperSymbol of S holds Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X)))
let R be invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X)); :: thesis: for o being OperSymbol of S holds Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X)))
let o be OperSymbol of S; :: thesis: Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X)))
set A = NFAlgebra R;
A1: the Sorts of (NFAlgebra R) = NForms R by Def20;
(NForms R) * (the_arity_of o) c= the Sorts of (Free (S,X)) * (the_arity_of o) by Th15, PBOOLE:def 18;
then product ((NForms R) * (the_arity_of o)) c= product ( the Sorts of (Free (S,X)) * (the_arity_of o)) by Th16;
then product ((NForms R) * (the_arity_of o)) c= Args (o,(Free (S,X))) by PRALG_2:3;
hence Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X))) by A1, PRALG_2:3; :: thesis: verum

end;

theorem Th80: :: MSAFREE4:80

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for g being ManySortedFunction of (Free (S,X)),(Free (S,X)) st g is_homomorphism Free (S,X), Free (S,X) holds
for s being SortSymbol of S
for a being Element of (Free (S,X)),s holds nf (((g . s) . (nf (a,(R . s)))),(R . s)) = nf (((g . s) . a),(R . s))

proof end;

theorem Th81: :: MSAFREE4:81

for p being FinSequence holds
( p /^ 0 = p & ( for i being Nat st i >= len p holds
p /^ i = {} ) )

proof end;

theorem Th82: :: MSAFREE4:82

for x, y being set
for p, q being FinSequence holds ((p ^ <*x*>) ^ q) +* (((len p) + 1),y) = (p ^ <*y*>) ^ q

proof end;

theorem Th83: :: MSAFREE4:83

for p being FinSequence
for i being Nat st i + 1 <= len p holds
p | (i + 1) = (p | i) ^ <*(p . (i + 1))*>

proof end;

theorem Th84: :: MSAFREE4:84

for p being FinSequence
for i being Nat st i + 1 <= len p holds
p /^ i = <*(p . (i + 1))*> ^ (p /^ (i + 1))

proof end;

theorem Th85: :: MSAFREE4:85

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for g being ManySortedFunction of (Free (S,X)),(Free (S,X)) st g is_homomorphism Free (S,X), Free (S,X) holds
for h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) st ( for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s)) ) holds
for s being SortSymbol of S
for o being OperSymbol of S st s = the_result_sort_of o holds
for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))

proof end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let R be invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X));

cluster NFAlgebra R -> strict non-empty X,S -terms ;

coherence
NFAlgebra R is X,S -terms

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of S;
let R be invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X));

cluster NFAlgebra R -> strict non-empty all_vars_including inheriting_operations free_in_itself ;

coherence
( NFAlgebra R is all_vars_including & NFAlgebra R is inheriting_operations & NFAlgebra R is free_in_itself )

proof end;

end;