:: by Grzegorz Bancerek

::

:: Received May 15, 2012

:: Copyright (c) 2012-2021 Association of Mizar Users

deffunc H

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_{1} being Element of A holds b_{1} is Element of Union X

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

proof 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

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

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)

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_{8} . b_{9} is Function of (b_{6} . b_{9}),(b_{7} . b_{9})

let X, Y be ManySortedSet of I; :: thesis: for f being ManySortedFunction of X,Y

for x being object holds b_{6} . b_{7} is Function of (b_{4} . b_{7}),(b_{5} . b_{7})

let f be ManySortedFunction of X,Y; :: thesis: for x being object holds b_{5} . b_{6} is Function of (b_{3} . b_{6}),(b_{4} . b_{6})

let x be object ; :: thesis: b_{4} . b_{5} is Function of (b_{2} . b_{5}),(b_{3} . b_{5})

end;
for f being ManySortedFunction of X,Y

for x being object holds b

let X, Y be ManySortedSet of I; :: thesis: for f being ManySortedFunction of X,Y

for x being object holds b

let f be ManySortedFunction of X,Y; :: thesis: for x being object holds b

let x be object ; :: thesis: b

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

end;

suppose A1:
x nin I
; :: thesis: b_{4} . b_{5} is Function of (b_{2} . b_{5}),(b_{3} . b_{5})

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

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

scheme :: MSAFREE4:sch 1

Sch1{ F_{1}() -> set , F_{2}() -> V5() ManySortedSet of F_{1}(), F_{3}( object , object ) -> set } :

Sch1{ F

ex f being ManySortedFunction of F_{1}() st

for x being set st x in F_{1}() holds

( dom (f . x) = F_{2}() . x & ( for y being Element of F_{2}() . x holds (f . x) . y = F_{3}(x,y) ) )

for x being set st x in F

( dom (f . x) = F

proof end;

scheme :: MSAFREE4:sch 2

Sch2{ F_{1}() -> non empty set , F_{2}() -> V5() ManySortedSet of F_{1}(), F_{3}() -> V5() ManySortedSet of F_{1}(), F_{4}( object , object ) -> set } :

Sch2{ F

ex f being ManySortedFunction of F_{2}(),F_{3}() st

for i being Element of F_{1}()

for a being Element of F_{2}() . i holds (f . i) . a = F_{4}(i,a)

providedfor i being Element of F

for a being Element of F

A1:
for i being Element of F_{1}()

for a being Element of F_{2}() . i holds F_{4}(i,a) in F_{3}() . i

for a being Element of F

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

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

coherence

F * p is FinSequence-like

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

coherence

F * p is FinSequence-like

proof end;

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

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

proof end;

registration

ex b_{1} being FinSequence st

( b_{1} is V32() & b_{1} is DTree-yielding & not b_{1} is empty )

ex b_{1} being FinSequence st

( b_{1} is V32() & b_{1} is Tree-yielding & not b_{1} is empty )
end;

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

existence ex b

( b

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

( b

proof end;

registration
end;

registration
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

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;

for b_{1} being S -Terms X -valued Function holds b_{1} is finite-yielding

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

proof 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

for t being DecoratedTree st t in X holds

Subtrees t 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

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

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;

coherence

rngs f is non-empty

end;
let A, B be V5() ManySortedSet of I;

let f be ManySortedFunction of A,B;

coherence

rngs f is non-empty

proof end;

registration

let S be non empty non void ManySortedSign ;

coherence

for b_{1} being Element of (TermAlg S) holds

( b_{1} is Relation-like & b_{1} is Function-like )

end;
coherence

for b

( b

proof end;

registration

let I be set ;

let A be ManySortedSet of I;

let f be FinSequence of I;

coherence

A * f is dom f -defined

end;
let A be ManySortedSet of I;

let f be FinSequence of I;

coherence

A * f is dom f -defined

proof end;

registration

let I be set ;

let A be ManySortedSet of I;

let f be FinSequence of I;

coherence

for b_{1} being dom f -defined Relation st b_{1} = A * f holds

b_{1} is total

end;
let A be ManySortedSet of I;

let f be FinSequence of I;

coherence

for b

b

proof 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

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

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

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)

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 ;

coherence

for b_{1} being Element of A . x holds

( b_{1} is Relation-like & b_{1} is Function-like )

end;
let X be V5() ManySortedSet of S;

let A be MSSubset of (FreeMSA X);

let x be object ;

coherence

for b

( b

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

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 ;

coherence

for b_{1} being ManySortedSet of I st b_{1} = I --> X holds

b_{1} is countable
by FUNCOP_1:7;

end;
let X be countable set ;

coherence

for b

b

registration

let I be set ;

existence

ex b_{1} being ManySortedSet of I st

( b_{1} is V5() & b_{1} is countable )

end;
existence

ex b

( b

proof end;

registration

let I be set ;

let X be countable ManySortedSet of I;

let x be object ;

coherence

X . x is countable

end;
let X be countable ManySortedSet of I;

let x be object ;

coherence

X . x is countable

proof end;

registration

let A be countable set ;

ex b_{1} being Function of A,NAT st b_{1} is one-to-one

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

existence ex b

proof end;

registration

let I be set ;

let X0 be countable ManySortedSet of I;

ex b_{1} being ManySortedFunction of X0,I --> NAT st b_{1} is "1-1"

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

proof 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

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

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

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

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

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

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

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 ;

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

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)

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;

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

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

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

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;

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

X . x is trivial )

end;
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 redefine attr X is trivial-yielding means :Def2: :: MSAFREE4:def 2

for x being set st x in I holds

X . x is trivial ;

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

X . x is trivial )

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

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 ;

existence

ex b_{1} being ManySortedSet of I st

( b_{1} is V5() & b_{1} is V276() )

end;
existence

ex b

( b

proof end;

registration

let I be set ;

let S be V276() ManySortedSet of I;

let x be object ;

coherence

S . x is trivial

end;
let S be V276() ManySortedSet of I;

let x be object ;

coherence

S . x is trivial

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

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 ;

existence

ex b_{1} being strict MSAlgebra over S st

( b_{1} is trivial & b_{1} is disjoint_valued & b_{1} is non-empty )

end;
existence

ex b

( b

proof end;

registration

let S be non empty non void ManySortedSign ;

let A be trivial MSAlgebra over S;

coherence

the Sorts of A is trivial-yielding by Def3;

end;
let A be trivial MSAlgebra over S;

coherence

the Sorts of A is trivial-yielding by Def3;

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

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

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

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;

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

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

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

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;

coherence

for b_{1} being MSAlgebra over S st b_{1} is A -Image holds

b_{1} is non-empty

ex b_{1} being strict non-empty MSAlgebra over S st b_{1} is A -Image

end;
let A be non-empty MSAlgebra over S;

coherence

for b

b

proof end;

existence ex b

proof end;

definition

let S be non empty non void ManySortedSign ;

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

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

end;
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 ex h being ManySortedFunction of A,C st h is_epimorphism A,C;

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

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

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;
let A be non-empty MSAlgebra over S;

mode image of A is non-empty A -Image MSAlgebra over S;

registration

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

existence

ex b_{1} being image of A st

( b_{1} is disjoint_valued & b_{1} is trivial )

end;
let A be non-empty MSAlgebra over S;

existence

ex b

( b

proof 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_{2} -Image MSAlgebra over S

for s being SortSymbol of S

for e being Element of (Equations S) . s st A |= e holds

B |= e

for A being non-empty MSAlgebra over S

for B being b

for s being SortSymbol of S

for e being Element of (Equations S) . s st A |= e holds

B |= e

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of S;

let A be MSAlgebra over S;

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

the Sorts of A is ManySortedSubset of the Sorts of (Free (S,X));

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

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;

coherence

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

end;
let X be V5() ManySortedSet of S;

coherence

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

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of S;

coherence

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

end;
let X be V5() ManySortedSet of S;

coherence

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

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of S;

existence

ex b_{1} being strict MSAlgebra over S st

( b_{1} is X,S -terms & b_{1} is non-empty )

end;
let X be V5() ManySortedSet of S;

existence

ex b

( b

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

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

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

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

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

:: 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_{2},b_{1} -terms MSAlgebra over S holds

( A is all_vars_including iff FreeGen X is ManySortedSubset of the Sorts of A );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of S

for A being b

( 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_{2},b_{1} -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 ) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of S

for A being b

( 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_{2},b_{1} -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 ) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of S

for A being b

( 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

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_{2},b_{1} -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 ) )

for X being V5() ManySortedSet of S

for A, B being non-empty b

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

not for b_{1} being GeneratorSet of T holds b_{1} is V5()

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

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of S;

coherence

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

end;
let X be V5() ManySortedSet of S;

coherence

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

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of S;

coherence

for b_{1} being X,S -terms MSAlgebra over S st b_{1} is all_vars_including holds

b_{1} is non-empty

ex b_{1} being strict X,S -terms MSAlgebra over S st

( b_{1} is all_vars_including & b_{1} is inheriting_operations & b_{1} is free_in_itself )

end;
let X be V5() ManySortedSet of S;

coherence

for b

b

proof end;

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

existence ex b

( b

proof 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_{2},b_{1} -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 ) )

for X being V5() ManySortedSet of S

for A0 being non-empty b

( ( 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_{2},b_{1} -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

for X being V5() ManySortedSet of S

for A1 being b

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_{2},b_{1} -terms all_vars_including MSAlgebra over S

for o being OperSymbol of S holds Args (o,A1) c= Args (o,(Free (S,X)))

for X being V5() ManySortedSet of S

for A1 being b

for o being OperSymbol of S holds Args (o,A1) c= Args (o,(Free (S,X)))

proof end;

registration

let S be set ;

existence

ex b_{1} being ManySortedSet of S st

( b_{1} is disjoint_valued & b_{1} is V5() )

end;
existence

ex b

( b

proof end;

registration

let S be set ;

let T be V5() disjoint_valued ManySortedSet of S;

coherence

for b_{1} being ManySortedSubset of T holds b_{1} is disjoint_valued

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

coherence

for b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of S;

existence

ex b_{1} being MSAlgebra over S st

( b_{1} is X,S -terms & b_{1} is strict )

end;
let X be V5() ManySortedSet of S;

existence

ex b

( b

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

ex b_{1} being ManySortedFunction of (Free (S,X)),A1 st

( b_{1} is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds

id G = b_{1} || G ) )

for b_{1}, b_{2} being ManySortedFunction of (Free (S,X)),A1 st b_{1} is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds

id G = b_{1} || G ) & b_{2} is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds

id G = b_{2} || G ) holds

b_{1} = b_{2}

end;
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 ( it is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds

id G = it || G ) );

ex b

( b

id G = b

proof end;

uniqueness for b

id G = b

id G = b

b

proof 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_{2},b_{1} -terms all_vars_including MSAlgebra over S

for b_{4} being ManySortedFunction of (Free (S,X)),A1 holds

( b_{4} = canonical_homomorphism A1 iff ( b_{4} is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds

id G = b_{4} || G ) ) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of S

for A1 being b

for b

( b

id G = b

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;

coherence

for b_{1} being Element of A0 holds

( b_{1} is Function-like & b_{1} is Relation-like )

coherence

for b_{1} being Element of A0,s holds

( b_{1} is Function-like & b_{1} is Relation-like )

end;
let X be V5() ManySortedSet of S;

let A0 be non-empty X,S -terms MSAlgebra over S;

coherence

for b

( b

proof end;

let s be SortSymbol of S;coherence

for b

( b

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

coherence

for b_{1} being Element of A0 holds b_{1} is DecoratedTree-like

coherence

for b_{1} being Element of A0,s holds b_{1} is DecoratedTree-like

end;
let X be V5() ManySortedSet of S;

let A0 be non-empty X,S -terms MSAlgebra over S;

coherence

for b

proof end;

let s be SortSymbol of S;coherence

for b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of S;

coherence

for b_{1} being MSAlgebra over S st b_{1} is X,S -terms holds

b_{1} is disjoint_valued

end;
let X be V5() ManySortedSet of S;

coherence

for b

b

proof 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_{2},b_{1} -terms MSAlgebra over S

for t being Element of A0 holds t is Term of S,X

for X being V5() ManySortedSet of S

for A0 being non-empty b

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_{2},b_{1} -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

for X being V5() ManySortedSet of S

for A0 being non-empty b

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_{2},b_{1} -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

for X being V5() ManySortedSet of S

for A2 being b

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_{2},b_{1} -terms all_vars_including inheriting_operations MSAlgebra over S holds FreeGen X is GeneratorSet of A2

for X being V5() ManySortedSet of S

for A2 being b

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_{2},b_{1} -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 )

for X being V5() ManySortedSet of S

for T being non-empty b

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_{2},b_{1} -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 ) )

for X being V5() ManySortedSet of S

for A2 being b

( 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_{2},b_{1} -terms all_vars_including inheriting_operations MSAlgebra over S holds (canonical_homomorphism A2) ** (canonical_homomorphism A2) = canonical_homomorphism A2

for X being V5() ManySortedSet of S

for A2 being b

proof end;

theorem :: MSAFREE4:49

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of S

for A being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds A is Free (S,X) -Image

for X being V5() ManySortedSet of S

for A being b

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 ;

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

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

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

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

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;

existence

ex b_{1} being MSAlgebra over S st

( b_{1} is T -satisfying & b_{1} is non-empty & b_{1} is trivial )

end;
let T be EqualSet of S;

existence

ex b

( b

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

coherence

for b_{1} being non-empty MSAlgebra over S st b_{1} is A -Image holds

b_{1} is T -satisfying
by Def11, Th36;

end;
let T be EqualSet of S;

let A be non-empty T -satisfying MSAlgebra over S;

coherence

for b

b

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;

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

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

:: 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_{3} -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 ) );

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

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

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;

ex b_{1} being EqualSet of S st

for s being SortSymbol of S holds b_{1} . s = { e where e is Element of (Equations S) . s : A |= e }

for b_{1}, b_{2} being EqualSet of S st ( for s being SortSymbol of S holds b_{1} . s = { e where e is Element of (Equations S) . s : A |= e } ) & ( for s being SortSymbol of S holds b_{2} . s = { e where e is Element of (Equations S) . s : A |= e } ) holds

b_{1} = b_{2}

end;
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 for s being SortSymbol of S holds it . s = { e where e is Element of (Equations S) . s : A |= e } ;

ex b

for s being SortSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def14 defines Equations MSAFREE4:def 14 :

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for b_{3} being EqualSet of S holds

( b_{3} = Equations (S,A) iff for s being SortSymbol of S holds b_{3} . s = { e where e is Element of (Equations S) . s : A |= e } );

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for b

( b

theorem Th54: :: MSAFREE4:54

for S being non empty non void ManySortedSign

for A being MSAlgebra over S holds A |= Equations (S,A)

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;

coherence

for b_{1} being A -Image MSAlgebra over S holds b_{1} is Equations (S,A) -satisfying

end;
let A be non-empty MSAlgebra over S;

coherence

for b

proof end;

scheme :: MSAFREE4:sch 3

TermDefEx{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> V5() ManySortedSet of F_{1}(), F_{3}( set , set ) -> set , F_{4}( set , set ) -> set } :

TermDefEx{ F

ex F being ManySortedSet of F_{1}() -Terms F_{2}() st

( ( for s being SortSymbol of F_{1}()

for x being Element of F_{2}() . s holds F . (root-tree [x,s]) = F_{3}(x,s) ) & ( for o being OperSymbol of F_{1}()

for p being ArgumentSeq of Sym (o,F_{2}()) holds F . ((Sym (o,F_{2}())) -tree p) = F_{4}(o,(F * p)) ) )

( ( for s being SortSymbol of F

for x being Element of F

for p being ArgumentSeq of Sym (o,F

proof end;

scheme :: MSAFREE4:sch 4

TermDefUniq{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> V5() ManySortedSet of F_{1}(), F_{3}( set , set ) -> set , F_{4}( set , FinSequence) -> set , F_{5}() -> ManySortedSet of F_{1}() -Terms F_{2}(), F_{6}() -> ManySortedSet of F_{1}() -Terms F_{2}() } :

provided

TermDefUniq{ F

provided

A1:
for s being SortSymbol of F_{1}()

for x being Element of F_{2}() . s holds F_{5}() . (root-tree [x,s]) = F_{3}(x,s)
and

A2: for o being OperSymbol of F_{1}()

for p being ArgumentSeq of Sym (o,F_{2}()) holds F_{5}() . ((Sym (o,F_{2}())) -tree p) = F_{4}(o,(F_{5}() * p))
and

A3: for s being SortSymbol of F_{1}()

for x being Element of F_{2}() . s holds F_{6}() . (root-tree [x,s]) = F_{3}(x,s)
and

A4: for o being OperSymbol of F_{1}()

for p being ArgumentSeq of Sym (o,F_{2}()) holds F_{6}() . ((Sym (o,F_{2}())) -tree p) = F_{4}(o,(F_{6}() * p))

for x being Element of F

A2: for o being OperSymbol of F

for p being ArgumentSeq of Sym (o,F

A3: for s being SortSymbol of F

for x being Element of F

A4: for o being OperSymbol of F

for p being ArgumentSeq of Sym (o,F

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_{2}( set , set ) -> set = root-tree [((w . $2) . $1),$2];

deffunc H_{3}( OperSymbol of S, FinSequence) -> set = (Sym ($1,( the carrier of S --> NAT))) -tree $2;

ex b_{1} being Element of (TermAlg S) ex F being ManySortedSet of S -Terms X st

( b_{1} = 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) ) )

for b_{1}, b_{2} being Element of (TermAlg S) st ex F being ManySortedSet of S -Terms X st

( b_{1} = 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_{2} = 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_{1} = b_{2}

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

deffunc H

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

ex b

( b

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

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

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

proof 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_{5} being Element of (TermAlg S) holds

( b_{5} = # (t,w) iff ex F being ManySortedSet of S -Terms X st

( b_{5} = 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) ) ) );

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

( b

( b

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)

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;

coherence

for b_{1} being Element of G . s holds

( b_{1} is Relation-like & b_{1} is Function-like )

end;
let X be V5() ManySortedSet of S;

let G be V5() MSSubset of (Free (S,X));

let s be SortSymbol of S;

coherence

for b

( b

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

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]

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

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)

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

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

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_{2},b_{1} -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] ) )

for X being V5() ManySortedSet of S

for A being b

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]

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_{2},b_{1} -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] ) ) )

for X0 being V5() countable ManySortedSet of S

for A0 being b

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_{2},b_{1} -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) )

for X being V5() ManySortedSet of S

for A being b

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_{2},b_{1} -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

for X being V5() ManySortedSet of S

for A being b

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_{2},b_{1} -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)

for X being V5() ManySortedSet of S

for A being b

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_{2},b_{1} -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)

for X being V5() ManySortedSet of S

for A being b

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_{2},b_{1} -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))

for X being V5() ManySortedSet of S

for A being b

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_{2},b_{1} -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 ) )

for X0, Y0 being V5() countable ManySortedSet of S

for A being b

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_{2},b_{1} -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

for X0 being V5() countable ManySortedSet of S

for A0 being b

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_{2},b_{1} -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

for X0 being V5() countable ManySortedSet of S

for A0 being b

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

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

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_{2},b_{1} -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

for X0 being V5() countable ManySortedSet of S

for A0 being b

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_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds A0 is Equations (S,A0) -free

for X0 being V5() countable ManySortedSet of S

for A0 being b

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)

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

definition

let I be set ;

let X be ManySortedSet of I;

let R be ManySortedRelation of X;

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

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 ;

for x being set st x in I holds

R . x is with_UN_property ;

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

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

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

coherence

for b_{1} being empty set holds

( b_{1} is strongly-normalizing & b_{1} is with_UN_property )
;

end;
for b

( b

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 )

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;

coherence

for b_{1} being ManySortedRelation of X st b_{1} is V6() holds

( b_{1} is with_UN_property & b_{1} is terminating )
;

not for b_{1} being ManySortedRelation of X holds b_{1} is V6()

end;
let X be ManySortedSet of I;

coherence

for b

( b

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

existence not for b

proof end;

registration

let I be set ;

let X be ManySortedSet of I;

let R be terminating ManySortedRelation of X;

let i be object ;

coherence

for b_{1} being Relation st b_{1} = R . i holds

b_{1} is strongly-normalizing

end;
let X be ManySortedSet of I;

let R be terminating ManySortedRelation of X;

let i be object ;

coherence

for b

b

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

coherence

for b_{1} being Relation st b_{1} = R . i holds

b_{1} is with_UN_property

end;
let X be ManySortedSet of I;

let R be with_UN_property ManySortedRelation of X;

let i be object ;

coherence

for b

b

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

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

for s being SortSymbol of S

for x being Element of (FreeGen X) . s holds x is_a_normal_form_wrt R . s;

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

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

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of S;

for b_{1} being ManySortedRelation of (Free (S,X)) st b_{1} is V6() holds

( b_{1} is NF-var & b_{1} is invariant & b_{1} is stable )

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

( b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of S;

ex b_{1} being invariant stable ManySortedRelation of (Free (S,X)) st

( b_{1} is NF-var & b_{1} is terminating & b_{1} is with_UN_property )

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

( b

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

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

definition

let I be non empty set ;

let X be V5() ManySortedSet of I;

let R be terminating with_UN_property ManySortedRelation of X;

ex b_{1} being V5() ManySortedSubset of X st

for i being Element of I holds b_{1} . i = { (nf (x,(R . i))) where x is Element of X . i : verum }

for b_{1}, b_{2} being V5() ManySortedSubset of X st ( for i being Element of I holds b_{1} . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ) & ( for i being Element of I holds b_{2} . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ) holds

b_{1} = b_{2}

end;
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 for i being Element of I holds it . i = { (nf (x,(R . i))) where x is Element of X . i : verum } ;

ex b

for i being Element of I holds b

proof end;

uniqueness for b

b

proof 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_{4} being V5() ManySortedSubset of X holds

( b_{4} = NForms R iff for i being Element of I holds b_{4} . i = { (nf (x,(R . i))) where x is Element of X . i : verum } );

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

( b

scheme :: MSAFREE4:sch 7

MSFLambda{ F_{1}() -> non empty set , F_{2}( object ) -> non empty set , F_{3}( object , object ) -> set } :

MSFLambda{ F

ex f being ManySortedFunction of F_{1}() st

for o being Element of F_{1}() holds

( dom (f . o) = F_{2}(o) & ( for x being Element of F_{2}(o) holds (f . o) . x = F_{3}(o,x) ) )

for o being Element of F

( dom (f . o) = F

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

ex b_{1} being strict non-empty MSAlgebra over S st

( the Sorts of b_{1} = NForms R & ( for o being OperSymbol of S

for a being Element of Args (o,b_{1}) holds (Den (o,b_{1})) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) )

for b_{1}, b_{2} being strict non-empty MSAlgebra over S st the Sorts of b_{1} = NForms R & ( for o being OperSymbol of S

for a being Element of Args (o,b_{1}) holds (Den (o,b_{1})) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) & the Sorts of b_{2} = NForms R & ( for o being OperSymbol of S

for a being Element of Args (o,b_{2}) holds (Den (o,b_{2})) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) holds

b_{1} = b_{2}

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

ex b

( the Sorts of b

for a being Element of Args (o,b

proof end;

uniqueness for b

for a being Element of Args (o,b

for a being Element of Args (o,b

b

proof 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_{4} being strict non-empty MSAlgebra over S holds

( b_{4} = NFAlgebra R iff ( the Sorts of b_{4} = NForms R & ( for o being OperSymbol of S

for a being Element of Args (o,b_{4}) holds (Den (o,b_{4})) . a = nf (((Den (o,(Free (S,X)))) . a),(R . (the_result_sort_of o))) ) ) );

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

( b

for a being Element of Args (o,b

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

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

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

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

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 Th82: :: MSAFREE4:82

for x, y being set

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

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

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

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

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

coherence

NFAlgebra R is X,S -terms

end;
let X be V5() ManySortedSet of S;

let R be invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X));

coherence

NFAlgebra R is X,S -terms

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 NF-var ManySortedRelation of (Free (S,X));

coherence

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

end;
let X be V5() ManySortedSet of S;

let R be invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X));

coherence

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

proof end;