:: by Grzegorz Bancerek

::

:: Received June 13, 2014

:: Copyright (c) 2014-2016 Association of Mizar Users

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

let s be SortSymbol of S;

mode Element of A,s is Element of the Sorts of A . s;

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

let s be SortSymbol of S;

mode Element of A,s is Element of the Sorts of A . s;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including MSAlgebra over S;

let r be Element of T;

coherence

r is Element of (Free (S,X)) by MSAFREE4:39;

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

let T be X,S -terms all_vars_including MSAlgebra over S;

let r be Element of T;

coherence

r is Element of (Free (S,X)) by MSAFREE4:39;

:: deftheorem defines @ MSAFREE5:def 1 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including MSAlgebra over S

for r being Element of T holds @ r = r;

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for r being Element of T holds @ r = r;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

coherence

for b_{1} being Element of T holds b_{1} is finite

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

coherence

for b

proof end;

registration
end;

definition
end;

:: deftheorem ELEM defines in MSAFREE5:def 2 :

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for a being object holds

( a in A iff a in Union the Sorts of A );

for S being non empty non void ManySortedSign

for A being MSAlgebra over S

for a being object holds

( a in A iff a in Union the Sorts of A );

:: deftheorem DIFF defines -different MSAFREE5:def 3 :

for a, b being object holds

( b is a -different iff b <> a );

for a, b being object holds

( b is a -different iff b <> a );

registration

let I be non trivial set ;

let a be object ;

existence

ex b_{1} being Element of I st b_{1} is a -different

end;
let a be object ;

existence

ex b

proof end;

theorem Th01: :: MSAFREE5:1

for t, t1 being Tree

for p, q being FinSequence of NAT st p in t & q in t with-replacement (p,t1) holds

( ( not p is_a_prefix_of q implies q in t ) & ( for r being FinSequence of NAT st q = p ^ r holds

r in t1 ) )

for p, q being FinSequence of NAT st p in t & q in t with-replacement (p,t1) holds

( ( not p is_a_prefix_of q implies q in t ) & ( for r being FinSequence of NAT st q = p ^ r holds

r in t1 ) )

proof end;

registration
end;

theorem Lem8B: :: MSAFREE5:5

for p, q, r being FinSequence holds

( not q is_a_prefix_of p ^ r or q is_a_prefix_of p or p is_a_prefix_of q )

( not q is_a_prefix_of p ^ r or q is_a_prefix_of p or p is_a_prefix_of q )

proof end;

definition

let S be non empty non void ManySortedSign ;

end;
attr S is sufficiently_rich means :SR: :: MSAFREE5:def 4

for s being SortSymbol of S ex o being OperSymbol of S st s in rng (the_arity_of o);

for s being SortSymbol of S ex o being OperSymbol of S st s in rng (the_arity_of o);

:: deftheorem SR defines sufficiently_rich MSAFREE5:def 4 :

for S being non empty non void ManySortedSign holds

( S is sufficiently_rich iff for s being SortSymbol of S ex o being OperSymbol of S st s in rng (the_arity_of o) );

for S being non empty non void ManySortedSign holds

( S is sufficiently_rich iff for s being SortSymbol of S ex o being OperSymbol of S st s in rng (the_arity_of o) );

:: deftheorem defines growable MSAFREE5:def 5 :

for S being non empty non void ManySortedSign holds

( S is growable iff for X being V5() ManySortedSet of the carrier of S

for n being Nat ex t being Element of (Free (S,X)) st height (dom t) = n );

for S being non empty non void ManySortedSign holds

( S is growable iff for X being V5() ManySortedSet of the carrier of S

for n being Nat ex t being Element of (Free (S,X)) st height (dom t) = n );

definition

let n be Nat;

let S be non empty non void ManySortedSign ;

end;
let S be non empty non void ManySortedSign ;

attr S is n -ary_oper_including means :: MSAFREE5:def 6

ex o being OperSymbol of S st len (the_arity_of o) = n;

ex o being OperSymbol of S st len (the_arity_of o) = n;

:: deftheorem defines -ary_oper_including MSAFREE5:def 6 :

for n being Nat

for S being non empty non void ManySortedSign holds

( S is n -ary_oper_including iff ex o being OperSymbol of S st len (the_arity_of o) = n );

for n being Nat

for S being non empty non void ManySortedSign holds

( S is n -ary_oper_including iff ex o being OperSymbol of S st len (the_arity_of o) = n );

registration

let n be Nat;

existence

ex b_{1} being non empty non void ManySortedSign st b_{1} is n -ary_oper_including

end;
existence

ex b

proof end;

registration
end;

definition

let R be Relation;

end;
attr R is non-trivial means :NT: :: MSAFREE5:def 7

for I being set st I in rng R holds

not I is trivial ;

for I being set st I in rng R holds

not I is trivial ;

attr R is infinite-yielding means :INF: :: MSAFREE5:def 8

for I being set st I in rng R holds

I is infinite ;

for I being set st I in rng R holds

I is infinite ;

:: deftheorem NT defines non-trivial MSAFREE5:def 7 :

for R being Relation holds

( R is non-trivial iff for I being set st I in rng R holds

not I is trivial );

for R being Relation holds

( R is non-trivial iff for I being set st I in rng R holds

not I is trivial );

:: deftheorem INF defines infinite-yielding MSAFREE5:def 8 :

for R being Relation holds

( R is infinite-yielding iff for I being set st I in rng R holds

I is infinite );

for R being Relation holds

( R is infinite-yielding iff for I being set st I in rng R holds

I is infinite );

registration

coherence

for b_{1} being Relation st b_{1} is non-trivial holds

b_{1} is non-empty

for b_{1} being Relation st b_{1} is infinite-yielding holds

b_{1} is non-trivial
;

end;
for b

b

proof end;

coherence for b

b

registration
end;

registration

ex b_{1} being FinSequence st b_{1} is infinite-yielding
end;

cluster Relation-like omega -defined Function-like finite FinSequence-like FinSubsequence-like countable infinite-yielding for set ;

existence ex b

proof end;

registration

let I be non empty set ;

let f be non-trivial ManySortedSet of I;

let a be Element of I;

coherence

not f . a is trivial by NT;

end;
let f be non-trivial ManySortedSet of I;

let a be Element of I;

coherence

not f . a is trivial by NT;

registration

let I be non empty set ;

let f be infinite-yielding ManySortedSet of I;

let a be Element of I;

coherence

not f . a is finite by INF;

end;
let f be infinite-yielding ManySortedSet of I;

let a be Element of I;

coherence

not f . a is finite by INF;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let o be OperSymbol of S;

coherence

for b_{1} being Element of Args (o,(Free (S,X))) holds b_{1} is DTree-yielding

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

let o be OperSymbol of S;

coherence

for b

proof end;

registration

let p be FinSequence;

reducibility

p ^ {} = p by FINSEQ_1:34;

reducibility

{} ^ p = p by FINSEQ_1:34;

end;
reducibility

p ^ {} = p by FINSEQ_1:34;

reducibility

{} ^ p = p by FINSEQ_1:34;

definition

let I be FinSequence-membered set ;

let p be FinSequence;

coherence

{ (p ^ q) where q is Element of I : q in I } is set ;

end;
let p be FinSequence;

coherence

{ (p ^ q) where q is Element of I : q in I } is set ;

:: deftheorem defines ^^ MSAFREE5:def 9 :

for I being FinSequence-membered set

for p being FinSequence holds p ^^ I = { (p ^ q) where q is Element of I : q in I } ;

for I being FinSequence-membered set

for p being FinSequence holds p ^^ I = { (p ^ q) where q is Element of I : q in I } ;

registration

let I be FinSequence-membered set ;

let p be FinSequence;

coherence

p ^^ I is FinSequence-membered

end;
let p be FinSequence;

coherence

p ^^ I is FinSequence-membered

proof end;

registration
end;

registration
end;

registration
end;

registration

let p be DTree-yielding FinSequence;

let a be object ;

coherence

dom (p . a) is FinSequence-membered

end;
let a be object ;

coherence

dom (p . a) is FinSequence-membered

proof end;

registration
end;

theorem Th124: :: MSAFREE5:6

for i being Nat

for xi, w being FinSequence of NAT

for p, q being Tree-yielding FinSequence

for d, t being Tree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree p holds

(tree p) with-replacement (xi,t) = tree q

for xi, w being FinSequence of NAT

for p, q being Tree-yielding FinSequence

for d, t being Tree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree p holds

(tree p) with-replacement (xi,t) = tree q

proof end;

registration

let F be Function-yielding Function;

let f be Function;

let a be object ;

coherence

F +* (a,f) is Function-yielding

end;
let f be Function;

let a be object ;

coherence

F +* (a,f) is Function-yielding

proof end;

theorem Lem12: :: MSAFREE5:7

for a being object

for F being Function-yielding Function

for f being Function holds doms (F +* (a,f)) = (doms F) +* (a,(dom f))

for F being Function-yielding Function

for f being Function holds doms (F +* (a,f)) = (doms F) +* (a,(dom f))

proof end;

theorem Th123: :: MSAFREE5:8

for a being object

for i being Nat

for xi, w being FinSequence of NAT

for p, q being DTree-yielding FinSequence

for d, t being DecoratedTree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) holds

(a -tree p) with-replacement (xi,t) = a -tree q

for i being Nat

for xi, w being FinSequence of NAT

for p, q being DTree-yielding FinSequence

for d, t being DecoratedTree st i < len p & xi = <*i*> ^ w & d = p . (i + 1) & q = p +* ((i + 1),(d with-replacement (w,t))) & xi in tree (doms p) holds

(a -tree p) with-replacement (xi,t) = a -tree q

proof end;

theorem :: MSAFREE5:9

for a being set

for w being DTree-yielding FinSequence holds dom (a -tree w) = {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } )

for w being DTree-yielding FinSequence holds dom (a -tree w) = {{}} \/ (union { (<*i*> ^^ (dom (w . (i + 1)))) where i is Nat : i < len w } )

proof end;

registration

let p be DTree-yielding FinSequence;

let a be object ;

let I be set ;

coherence

(p . a) " I is FinSequence-membered

end;
let a be object ;

let I be set ;

coherence

(p . a) " I is FinSequence-membered

proof end;

registration

let I be finite FinSequence-membered set ;

let p be FinSequence;

coherence

p ^^ I is finite

end;
let p be FinSequence;

coherence

p ^^ I is finite

proof end;

theorem Th2: :: MSAFREE5:11

for I, J being FinSequence-membered set

for p, q being FinSequence st len p = len q & p <> q holds

p ^^ I misses q ^^ J

for p, q being FinSequence st len p = len q & p <> q holds

p ^^ I misses q ^^ J

proof end;

registration
end;

theorem Th18: :: MSAFREE5:13

for I, J being FinSequence-membered set

for f being FinSequence holds

( I c= J iff f ^^ I c= f ^^ J )

for f being FinSequence holds

( I c= J iff f ^^ I c= f ^^ J )

proof end;

theorem ThL0: :: MSAFREE5:15

for p being non empty Tree-yielding FinSequence holds Leaves (tree p) = { (<*i*> ^ q) where i is Nat, q is FinSequence of NAT , d is Tree : ( q in Leaves d & i + 1 in dom p & d = p . (i + 1) ) }

proof end;

theorem :: MSAFREE5:17

registration
end;

theorem ThL7: :: MSAFREE5:18

for c1, c2 being set

for d being DecoratedTree st c1 <> c2 holds

((root-tree c1),c2) <- d = root-tree c1

for d being DecoratedTree st c1 <> c2 holds

((root-tree c1),c2) <- d = root-tree c1

proof end;

registration

let f be non empty Function-yielding Function;

coherence

not doms f is empty

not rngs f is empty

end;
coherence

not doms f is empty

proof end;

coherence not rngs f is empty

proof end;

theorem ThL8: :: MSAFREE5:19

for b being object

for c being set

for d being DecoratedTree

for p, q being non empty DTree-yielding FinSequence st dom q = dom p & ( for i being Nat

for d1 being DecoratedTree st i in dom p & d1 = p . i holds

q . i = (d1,c) <- d ) holds

((b -tree p),c) <- d = b -tree q

for c being set

for d being DecoratedTree

for p, q being non empty DTree-yielding FinSequence st dom q = dom p & ( for i being Nat

for d1 being DecoratedTree st i in dom p & d1 = p . i holds

q . i = (d1,c) <- d ) holds

((b -tree p),c) <- d = b -tree q

proof end;

definition

let S be non empty non void ManySortedSign ;

let s be SortSymbol of S;

let A be non empty MSAlgebra over S;

let a be Element of A;

end;
let s be SortSymbol of S;

let A be non empty MSAlgebra over S;

let a be Element of A;

:: deftheorem AS defines -sort MSAFREE5:def 10 :

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for A being non empty MSAlgebra over S

for a being Element of A holds

( a is s -sort iff a in the Sorts of A . s );

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for A being non empty MSAlgebra over S

for a being Element of A holds

( a is s -sort iff a in the Sorts of A . s );

registration

let S be non empty non void ManySortedSign ;

let s be SortSymbol of S;

let A be non-empty MSAlgebra over S;

existence

ex b_{1} being Element of A st b_{1} is s -sort

for b_{1} being Element of the Sorts of A . s holds b_{1} is s -sort
;

end;
let s be SortSymbol of S;

let A be non-empty MSAlgebra over S;

existence

ex b

proof end;

coherence for b

definition

let S be non empty non void ManySortedSign ;

let A be non empty MSAlgebra over S;

assume A: A is disjoint_valued ;

let a be Element of A;

existence

ex b_{1} being SortSymbol of S st a in the Sorts of A . b_{1}

for b_{1}, b_{2} being SortSymbol of S st a in the Sorts of A . b_{1} & a in the Sorts of A . b_{2} holds

b_{1} = b_{2}
by A, XBOOLE_0:3, PROB_2:def 2;

end;
let A be non empty MSAlgebra over S;

assume A: A is disjoint_valued ;

let a be Element of A;

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem SORT defines the_sort_of MSAFREE5:def 11 :

for S being non empty non void ManySortedSign

for A being non empty MSAlgebra over S st A is disjoint_valued holds

for a being Element of A

for b_{4} being SortSymbol of S holds

( b_{4} = the_sort_of a iff a in the Sorts of A . b_{4} );

for S being non empty non void ManySortedSign

for A being non empty MSAlgebra over S st A is disjoint_valued holds

for a being Element of A

for b

( b

theorem :: MSAFREE5:20

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for A being non-empty disjoint_valued MSAlgebra over S

for a being b_{2} -sort Element of A holds the_sort_of a = s

for s being SortSymbol of S

for A being non-empty disjoint_valued MSAlgebra over S

for a being b

proof end;

theorem :: MSAFREE5:21

for S being non empty non void ManySortedSign

for A being disjoint_valued non empty MSAlgebra over S

for a being Element of A holds a is the_sort_of a -sort by SORT;

for A being disjoint_valued non empty MSAlgebra over S

for a being Element of A holds a is the_sort_of a -sort by SORT;

theorem Lem00: :: MSAFREE5:22

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T holds the_sort_of (@ r) = the_sort_of r

for X being V5() ManySortedSet of the carrier of S

for T being b

for r being Element of T holds the_sort_of (@ r) = the_sort_of r

proof end;

theorem :: MSAFREE5:23

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of the Sorts of T . s holds the_sort_of r = s by SORT;

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for T being b

for r being Element of the Sorts of T . s holds the_sort_of r = s by SORT;

theorem Th5: :: MSAFREE5:24

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for u being Term of S,X st t = u holds

the_sort_of t = the_sort_of u

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for u being Term of S,X st t = u holds

the_sort_of t = the_sort_of u

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let o be OperSymbol of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

coherence

for b_{1} being Element of Args (o,T) holds b_{1} is Union the Sorts of T -valued

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

let o be OperSymbol of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

coherence

for b

proof end;

theorem Th4A: :: MSAFREE5:25

for i being Nat

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for T being b_{4},b_{2} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for q being Element of Args (o,T) st i in dom q holds

the_sort_of (q /. i) = (the_arity_of o) /. i

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for T being b

for q being Element of Args (o,T) st i in dom q holds

the_sort_of (q /. i) = (the_arity_of o) /. i

proof end;

definition

let S be non empty non void ManySortedSign ;

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

let f be ManySortedFunction of A,B;

assume A: A is disjoint_valued ;

let a be Element of A;

coherence

(f . (the_sort_of a)) . a is Element of B

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

let f be ManySortedFunction of A,B;

assume A: A is disjoint_valued ;

let a be Element of A;

coherence

(f . (the_sort_of a)) . a is Element of B

proof end;

:: deftheorem ABBR defines . MSAFREE5:def 12 :

for S being non empty non void ManySortedSign

for A, B being non-empty MSAlgebra over S

for f being ManySortedFunction of A,B st A is disjoint_valued holds

for a being Element of A holds f . a = (f . (the_sort_of a)) . a;

for S being non empty non void ManySortedSign

for A, B being non-empty MSAlgebra over S

for f being ManySortedFunction of A,B st A is disjoint_valued holds

for a being Element of A holds f . a = (f . (the_sort_of a)) . a;

theorem Th9: :: MSAFREE5:26

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for A being non-empty disjoint_valued MSAlgebra over S

for B being non-empty MSAlgebra over S

for f being ManySortedFunction of A,B

for a being Element of the Sorts of A . s holds f . a = (f . s) . a

for s being SortSymbol of S

for A being non-empty disjoint_valued MSAlgebra over S

for B being non-empty MSAlgebra over S

for f being ManySortedFunction of A,B

for a being Element of the Sorts of A . s holds f . a = (f . s) . a

proof end;

theorem :: MSAFREE5:27

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for A being non-empty disjoint_valued MSAlgebra over S

for B being non-empty MSAlgebra over S

for f being ManySortedFunction of A,B

for a being Element of the Sorts of A . s holds f . a is Element of the Sorts of B . s

for s being SortSymbol of S

for A being non-empty disjoint_valued MSAlgebra over S

for B being non-empty MSAlgebra over S

for f being ManySortedFunction of A,B

for a being Element of the Sorts of A . s holds f . a is Element of the Sorts of B . s

proof end;

theorem Lem0: :: MSAFREE5:28

for S being non empty non void ManySortedSign

for A, B being non-empty disjoint_valued MSAlgebra over S

for f being ManySortedFunction of A,B

for a being Element of A holds the_sort_of (f . a) = the_sort_of a

for A, B being non-empty disjoint_valued MSAlgebra over S

for f being ManySortedFunction of A,B

for a being Element of A holds the_sort_of (f . a) = the_sort_of a

proof end;

theorem Th14: :: MSAFREE5:29

for S being non empty non void ManySortedSign

for A, B being non-empty disjoint_valued MSAlgebra over S

for C being non-empty MSAlgebra over S

for f being ManySortedFunction of A,B

for g being ManySortedFunction of B,C

for a being Element of A holds (g ** f) . a = g . (f . a)

for A, B being non-empty disjoint_valued MSAlgebra over S

for C being non-empty MSAlgebra over S

for f being ManySortedFunction of A,B

for g being ManySortedFunction of B,C

for a being Element of A holds (g ** f) . a = g . (f . a)

proof end;

theorem :: MSAFREE5:30

for S being non empty non void ManySortedSign

for A being non-empty disjoint_valued MSAlgebra over S

for B being non-empty MSAlgebra over S

for f1, f2 being ManySortedFunction of A,B st ( for a being Element of A holds f1 . a = f2 . a ) holds

f1 = f2

for A being non-empty disjoint_valued MSAlgebra over S

for B being non-empty MSAlgebra over S

for f1, f2 being ManySortedFunction of A,B st ( for a being Element of A holds f1 . a = f2 . a ) holds

f1 = f2

proof end;

definition

let S be non empty non void ManySortedSign ;

let A, B be MSAlgebra over S;

assume A: ex h being ManySortedFunction of A,B st h is_homomorphism A,B ;

ex b_{1} being ManySortedFunction of A,B st b_{1} is_homomorphism A,B
by A;

end;
let A, B be MSAlgebra over S;

assume A: ex h being ManySortedFunction of A,B st h is_homomorphism A,B ;

mode Homomorphism of A,B -> ManySortedFunction of A,B means :HOMO: :: MSAFREE5:def 13

it is_homomorphism A,B;

existence it is_homomorphism A,B;

ex b

:: deftheorem HOMO defines Homomorphism MSAFREE5:def 13 :

for S being non empty non void ManySortedSign

for A, B being MSAlgebra over S st ex h being ManySortedFunction of A,B st h is_homomorphism A,B holds

for b_{4} being ManySortedFunction of A,B holds

( b_{4} is Homomorphism of A,B iff b_{4} is_homomorphism A,B );

for S being non empty non void ManySortedSign

for A, B being MSAlgebra over S st ex h being ManySortedFunction of A,B st h is_homomorphism A,B holds

for b

( b

theorem :: MSAFREE5:31

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T 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)),T holds

( h is Homomorphism of Free (S,X),T iff h is_homomorphism Free (S,X),T )

for X being V5() ManySortedSet of the carrier of S

for T being b

for h being ManySortedFunction of (Free (S,X)),T holds

( h is Homomorphism of Free (S,X),T iff h is_homomorphism Free (S,X),T )

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

:: original: canonical_homomorphism

redefine func canonical_homomorphism T -> Homomorphism of Free (S,X),T;

coherence

canonical_homomorphism T is Homomorphism of Free (S,X),T

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

:: original: canonical_homomorphism

redefine func canonical_homomorphism T -> Homomorphism of Free (S,X),T;

coherence

canonical_homomorphism T is Homomorphism of Free (S,X),T

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let r be Element of T;

reducibility

(canonical_homomorphism T) . (@ r) = r

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let r be Element of T;

reducibility

(canonical_homomorphism T) . (@ r) = r

proof end;

theorem :: MSAFREE5:32

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for t1, t2 being Element of (Free (S,X)) st t2 = (canonical_homomorphism T) . t1 holds

(canonical_homomorphism T) . t1 = (canonical_homomorphism T) . t2

for X being V5() ManySortedSet of the carrier of S

for T being b

for t1, t2 being Element of (Free (S,X)) st t2 = (canonical_homomorphism T) . t1 holds

(canonical_homomorphism T) . t1 = (canonical_homomorphism T) . t2

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let x be Element of X . s;

coherence

root-tree [x,s] is Element of the Sorts of (Free (S,X)) . s

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

let s be SortSymbol of S;

let x be Element of X . s;

coherence

root-tree [x,s] is Element of the Sorts of (Free (S,X)) . s

proof end;

:: deftheorem defines -term MSAFREE5:def 14 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for s being SortSymbol of S

for x being Element of X . s holds x -term = root-tree [x,s];

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for s being SortSymbol of S

for x being Element of X . s holds x -term = root-tree [x,s];

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let o be OperSymbol of S;

let p be Element of Args (o,(Free (S,X)));

[o, the carrier of S] -tree p is Element of (Free (S,X)),(the_result_sort_of o)

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

let o be OperSymbol of S;

let p be Element of Args (o,(Free (S,X)));

func o -term p -> Element of (Free (S,X)),(the_result_sort_of o) equals :: MSAFREE5:def 15

[o, the carrier of S] -tree p;

coherence [o, the carrier of S] -tree p;

[o, the carrier of S] -tree p is Element of (Free (S,X)),(the_result_sort_of o)

proof end;

:: deftheorem defines -term MSAFREE5:def 15 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for o being OperSymbol of S

for p being Element of Args (o,(Free (S,X))) holds o -term p = [o, the carrier of S] -tree p;

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for o being OperSymbol of S

for p being Element of Args (o,(Free (S,X))) holds o -term p = [o, the carrier of S] -tree p;

theorem :: MSAFREE5:33

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s holds the_sort_of (x -term) = s by SORT;

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s holds the_sort_of (x -term) = s by SORT;

theorem Th8: :: MSAFREE5:34

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) holds the_sort_of (o -term p) = the_result_sort_of o

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) holds the_sort_of (o -term p) = the_result_sort_of o

proof end;

theorem Th119: :: MSAFREE5:35

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for i being object holds

( i in (FreeGen T) . s iff ex x being Element of X . s st i = x -term )

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for T being b

for i being object holds

( i in (FreeGen T) . s iff ex x being Element of X . s st i = x -term )

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let x be Element of X . s;

coherence

not x -term is compound

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

let s be SortSymbol of S;

let x be Element of X . s;

coherence

not x -term is compound

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let o be OperSymbol of S;

let p be Element of Args (o,(Free (S,X)));

coherence

( o -term p is compound & o -term p is the_result_sort_of o -sort )

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

let o be OperSymbol of S;

let p be Element of Args (o,(Free (S,X)));

coherence

( o -term p is compound & o -term p is the_result_sort_of o -sort )

proof end;

theorem Th16: :: MSAFREE5:36

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds

( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds

( ex s being SortSymbol of S ex x being Element of X . s st t = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )

proof end;

theorem :: MSAFREE5:37

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) st not t is compound holds

ex s being SortSymbol of S ex x being Element of X . s st t = x -term

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) st not t is compound holds

ex s being SortSymbol of S ex x being Element of X . s st t = x -term

proof end;

theorem Th17: :: MSAFREE5:38

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) st t is compound holds

ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) st t is compound holds

ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p

proof end;

theorem :: MSAFREE5:39

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) holds x -term <> o -term p ;

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) holds x -term <> o -term p ;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

ex b_{1} being Element of (Free (S,X)) st b_{1} is compound

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

cluster non empty Relation-like non pair Function-like finite DecoratedTree-like countable compound for Element of Union the Sorts of (Free (S,X));

existence ex b

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let e be compound Element of (Free (S,X));

:: original: main-constr

redefine func main-constr e -> OperSymbol of S;

coherence

main-constr e is OperSymbol of S

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

let e be compound Element of (Free (S,X));

:: original: main-constr

redefine func main-constr e -> OperSymbol of S;

coherence

main-constr e is OperSymbol of S

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let e be compound Element of (Free (S,X));

:: original: args

redefine func args e -> Element of Args ((main-constr e),(Free (S,X)));

coherence

args e is Element of Args ((main-constr e),(Free (S,X)))

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

let e be compound Element of (Free (S,X));

:: original: args

redefine func args e -> Element of Args ((main-constr e),(Free (S,X)));

coherence

args e is Element of Args ((main-constr e),(Free (S,X)))

proof end;

theorem :: MSAFREE5:40

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s holds args (x -term) = {}

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s holds args (x -term) = {}

proof end;

theorem :: MSAFREE5:41

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being compound Element of (Free (S,X)) holds t = (main-constr t) -term (args t)

for X being V5() ManySortedSet of the carrier of S

for t being compound Element of (Free (S,X)) holds t = (main-constr t) -term (args t)

proof end;

theorem Th24: :: MSAFREE5:42

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds x -term in T

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for T being b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x be Element of X . s;

reducibility

(canonical_homomorphism T) . (x -term) = x -term

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x be Element of X . s;

reducibility

(canonical_homomorphism T) . (x -term) = x -term

proof end;

scheme :: MSAFREE5:sch 2

TermInd{ P_{1}[ set ], F_{1}() -> non empty non void ManySortedSign , F_{2}() -> V5() ManySortedSet of the carrier of F_{1}(), F_{3}() -> Element of (Free (F_{1}(),F_{2}())) } :

provided

TermInd{ P

provided

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

for x being Element of F_{2}() . s holds P_{1}[x -term ]
and

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

for p being Element of Args (o,(Free (F_{1}(),F_{2}()))) st ( for t being Element of (Free (F_{1}(),F_{2}())) st t in rng p holds

P_{1}[t] ) holds

P_{1}[o -term p]

for x being Element of F

A2: for o being OperSymbol of F

for p being Element of Args (o,(Free (F

P

P

proof end;

scheme :: MSAFREE5:sch 3

TermAlgebraInd{ P_{1}[ set ], F_{1}() -> non empty non void ManySortedSign , F_{2}() -> V5() ManySortedSet of the carrier of F_{1}(), F_{3}() -> F_{2}(),F_{1}() -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over F_{1}(), F_{4}() -> Element of F_{3}() } :

provided

TermAlgebraInd{ P

provided

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

for x being Element of F_{2}() . s

for r being Element of F_{3}() st r = x -term holds

P_{1}[r]
and

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

for p being Element of Args (o,(Free (F_{1}(),F_{2}())))

for r being Element of F_{3}() st r = o -term p & ( for t being Element of F_{3}() st t in rng p holds

P_{1}[t] ) holds

P_{1}[r]

for x being Element of F

for r being Element of F

P

A2: for o being OperSymbol of F

for p being Element of Args (o,(Free (F

for r being Element of F

P

P

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let r be Element of T;

card (r " [: the carrier' of S,{ the carrier of S}:]) is Nat ;

coherence

height (dom r) is Nat ;

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let r be Element of T;

func construction_degree r -> Nat equals :: MSAFREE5:def 16

card (r " [: the carrier' of S,{ the carrier of S}:]);

coherence card (r " [: the carrier' of S,{ the carrier of S}:]);

card (r " [: the carrier' of S,{ the carrier of S}:]) is Nat ;

coherence

height (dom r) is Nat ;

:: deftheorem defines construction_degree MSAFREE5:def 16 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T holds construction_degree r = card (r " [: the carrier' of S,{ the carrier of S}:]);

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for r being Element of T holds construction_degree r = card (r " [: the carrier' of S,{ the carrier of S}:]);

:: deftheorem defines height MSAFREE5:def 17 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T holds height r = height (dom r);

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for r being Element of T holds height r = height (dom r);

notation

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let r be Element of T;

synonym deg r for construction_degree r;

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let r be Element of T;

synonym deg r for construction_degree r;

theorem :: MSAFREE5:43

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T holds deg (@ r) = deg r ;

for X being V5() ManySortedSet of the carrier of S

for T being b

for r being Element of T holds deg (@ r) = deg r ;

theorem :: MSAFREE5:44

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T holds height (@ r) = height r ;

for X being V5() ManySortedSet of the carrier of S

for T being b

for r being Element of T holds height (@ r) = height r ;

theorem :: MSAFREE5:45

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s holds height (x -term) = 0 by TREES_1:42, FUNCOP_1:13;

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s holds height (x -term) = 0 by TREES_1:42, FUNCOP_1:13;

registration

coherence

for b_{1} being set st b_{1} is natural-membered holds

( b_{1} is ordinal-membered & b_{1} is finite-membered )

end;
for b

( b

proof end;

registration
end;

registration
end;

theorem Th25: :: MSAFREE5:46

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for o being OperSymbol of S

for p being Element of Args (o,(Free (S,X))) holds

( { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is natural-membered & { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is finite & union { (height t) where t is Element of (Free (S,X)) : t in rng p } is Nat )

for X being V5() ManySortedSet of the carrier of S

for o being OperSymbol of S

for p being Element of Args (o,(Free (S,X))) holds

( { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is natural-membered & { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is finite & union { (height t) where t is Element of (Free (S,X)) : t in rng p } is Nat )

proof end;

theorem Th26: :: MSAFREE5:47

for n being Nat

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) st the_arity_of o <> {} & n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } holds

height (o -term p) = n + 1

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) st the_arity_of o <> {} & n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } holds

height (o -term p) = n + 1

proof end;

theorem Th20: :: MSAFREE5:48

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) st the_arity_of o = {} holds

height (o -term p) = 0

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) st the_arity_of o = {} holds

height (o -term p) = 0

proof end;

theorem Th21: :: MSAFREE5:49

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s holds deg (x -term) = 0

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s holds deg (x -term) = 0

proof end;

theorem Th22: :: MSAFREE5:50

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds

( deg t <> 0 iff ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds

( deg t <> 0 iff ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )

proof end;

registration
end;

definition

let a be object ;

let I be set ;

let J, K be set ;

:: original: IFIN

redefine func IFIN (a,I,J,K) -> set ;

coherence

IFIN (a,I,J,K) is set by TARSKI:1;

end;
let I be set ;

let J, K be set ;

:: original: IFIN

redefine func IFIN (a,I,J,K) -> set ;

coherence

IFIN (a,I,J,K) is set by TARSKI:1;

theorem Th80: :: MSAFREE5:51

for I, J being set

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) st J = [o, the carrier of S] holds

(o -term p) " I = (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } )

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) st J = [o, the carrier of S] holds

(o -term p) " I = (IFIN (J,I,{{}},{})) \/ (union { (<*i*> ^^ ((p . (i + 1)) " I)) where i is Nat : i < len p } )

proof end;

theorem Th29: :: MSAFREE5:52

for i being Nat

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) st ex f being FinSequence of NAT st

( i = Sum f & dom f = dom (the_arity_of o) & ( for i being Nat

for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds

f . i = deg t ) ) holds

deg (o -term p) = i + 1

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) st ex f being FinSequence of NAT st

( i = Sum f & dom f = dom (the_arity_of o) & ( for i being Nat

for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds

f . i = deg t ) ) holds

deg (o -term p) = i + 1

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let i be Nat;

{ r where r is Element of T : deg r <= i } is Subset of T

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let i be Nat;

func T deg<= i -> Subset of T equals :: MSAFREE5:def 18

{ r where r is Element of T : deg r <= i } ;

coherence { r where r is Element of T : deg r <= i } ;

{ r where r is Element of T : deg r <= i } is Subset of T

proof end;

:: deftheorem defines deg<= MSAFREE5:def 18 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for i being Nat holds T deg<= i = { r where r is Element of T : deg r <= i } ;

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for i being Nat holds T deg<= i = { r where r is Element of T : deg r <= i } ;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let i be Nat;

{ t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } is Subset of T

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let i be Nat;

func T height<= i -> Subset of T equals :: MSAFREE5:def 19

{ t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } ;

coherence { t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } ;

{ t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } is Subset of T

proof end;

:: deftheorem defines height<= MSAFREE5:def 19 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for i being Nat holds T height<= i = { t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } ;

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for i being Nat holds T height<= i = { t where t is Element of (Free (S,X)) : ( t in T & height t <= i ) } ;

theorem :: MSAFREE5:53

for i being Nat

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{3},b_{2} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T holds

( r in T deg<= i iff deg r <= i )

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for r being Element of T holds

( r in T deg<= i iff deg r <= i )

proof end;

theorem Th11: :: MSAFREE5:54

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum }

for X being V5() ManySortedSet of the carrier of S

for T being b

proof end;

theorem Th12: :: MSAFREE5:55

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T height<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) }

for X being V5() ManySortedSet of the carrier of S

for T being b

proof end;

theorem Th44: :: MSAFREE5:56

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= 0 = Union (FreeGen T)

for X being V5() ManySortedSet of the carrier of S

for T being b

proof end;

theorem Th10a: :: MSAFREE5:57

for i being Nat

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{3},b_{2} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T holds

( r in T height<= i iff height r <= i )

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for r being Element of T holds

( r in T height<= i iff height r <= i )

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let i be Nat;

coherence

not T deg<= i is empty

not T height<= i is empty

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let i be Nat;

coherence

not T deg<= i is empty

proof end;

coherence not T height<= i is empty

proof end;

theorem Th10b: :: MSAFREE5:58

for i, j being Nat

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{4},b_{3} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st i <= j holds

T deg<= i c= T deg<= j

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

T deg<= i c= T deg<= j

proof end;

theorem Th10c: :: MSAFREE5:59

for i, j being Nat

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{4},b_{3} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st i <= j holds

T height<= i c= T height<= j

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

T height<= i c= T height<= j

proof end;

theorem :: MSAFREE5:60

for i being Nat

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{3},b_{2} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= (i + 1) = (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st

( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat

for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds

f . i = deg t ) ) } /\ (Union the Sorts of T))

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat

for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds

f . i = deg t ) ) } /\ (Union the Sorts of T))

proof end;

theorem :: MSAFREE5:61

for i being Nat

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{3},b_{2} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T height<= (i + 1) = (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T))

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

proof end;

theorem :: MSAFREE5:62

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds deg t >= height t

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds deg t >= height t

proof end;

theorem :: MSAFREE5:63

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Union the Sorts of T = union { (T deg<= i) where i is Nat : verum }

for X being V5() ManySortedSet of the carrier of S

for T being b

proof end;

theorem :: MSAFREE5:64

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Union the Sorts of T = union { (T height<= i) where i is Nat : verum }

for X being V5() ManySortedSet of the carrier of S

for T being b

proof end;

theorem :: MSAFREE5:65

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for i being Nat holds T deg<= i c= (Free (S,X)) deg<= i

for X being V5() ManySortedSet of the carrier of S

for T being b

for i being Nat holds T deg<= i c= (Free (S,X)) deg<= i

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x be Element of X . s;

let r be Element of T;

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x be Element of X . s;

let r be Element of T;

:: deftheorem CONTEXT defines -context MSAFREE5:def 20 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for s being SortSymbol of S

for x being Element of X . s

for r being Element of T holds

( r is x -context iff card (Coim (r,[x,s])) = 1 );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for s being SortSymbol of S

for x being Element of X . s

for r being Element of T holds

( r is x -context iff card (Coim (r,[x,s])) = 1 );

:: deftheorem OMIT defines -omitting MSAFREE5:def 21 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for s being SortSymbol of S

for x being Element of X . s

for r being Element of T holds

( r is x -omitting iff Coim (r,[x,s]) = {} );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for s being SortSymbol of S

for x being Element of X . s

for r being Element of T holds

( r is x -omitting iff Coim (r,[x,s]) = {} );

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let r be Element of T;

coherence

proj1 ((rng r) /\ [:(Union X), the carrier of S:]) is set ;

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let r be Element of T;

coherence

proj1 ((rng r) /\ [:(Union X), the carrier of S:]) is set ;

:: deftheorem defines vf MSAFREE5:def 22 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T holds vf r = proj1 ((rng r) /\ [:(Union X), the carrier of S:]);

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for r being Element of T holds vf r = proj1 ((rng r) /\ [:(Union X), the carrier of S:]);

theorem ThR1: :: MSAFREE5:66

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T holds vf r = Union (X variables_in r)

for X being V5() ManySortedSet of the carrier of S

for T being b

for r being Element of T holds vf r = Union (X variables_in r)

proof end;

theorem :: MSAFREE5:67

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s holds vf (x -term) = {x}

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s holds vf (x -term) = {x}

proof end;

theorem :: MSAFREE5:68

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) holds vf (o -term p) = union { (vf t) where t is Element of (Free (S,X)) : t in rng p }

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for p being Element of Args (o,(Free (S,X))) holds vf (o -term p) = union { (vf t) where t is Element of (Free (S,X)) : t in rng p }

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let r be Element of T;

coherence

vf r is finite ;

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let r be Element of T;

coherence

vf r is finite ;

theorem Th92: :: MSAFREE5:69

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T st x nin vf r holds

r is x -omitting

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for T being b

for r being Element of T st x nin vf r holds

r is x -omitting

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let t be Element of (Free (S,X));

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

let s be SortSymbol of S;

let t be Element of (Free (S,X));

:: deftheorem defines -context MSAFREE5:def 23 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for s being SortSymbol of S

for t being Element of (Free (S,X)) holds

( t is s -context iff ex x being Element of X . s st t is x -context );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for s being SortSymbol of S

for t being Element of (Free (S,X)) holds

( t is s -context iff ex x being Element of X . s st t is x -context );

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let x be Element of X . s;

coherence

for b_{1} being Element of (Free (S,X)) st b_{1} is x -context holds

b_{1} is s -context
;

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

let s be SortSymbol of S;

let x be Element of X . s;

coherence

for b

b

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let x be Element of X . s;

coherence

x -term is x -context

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

let s be SortSymbol of S;

let x be Element of X . s;

coherence

x -term is x -context

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let x be Element of X . s;

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

( b_{1} is x -context & not b_{1} is compound )

for b_{1} being Element of (Free (S,X)) st b_{1} is x -omitting holds

not b_{1} is x -context
;

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

let s be SortSymbol of S;

let x be Element of X . s;

cluster non empty Relation-like non pair Function-like finite DecoratedTree-like countable non compound x -context for Element of Union the Sorts of (Free (S,X));

existence ex b

( b

proof end;

coherence for b

not b

theorem ThC1: :: MSAFREE5:70

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for s1, s2 being SortSymbol of S

for x1 being Element of X . s1

for x2 being Element of X . s2 holds

( ( s1 <> s2 or x1 <> x2 ) iff x1 -term is x2 -omitting )

for X being V5() ManySortedSet of the carrier of S

for s1, s2 being SortSymbol of S

for x1 being Element of X . s1

for x2 being Element of X . s2 holds

( ( s1 <> s2 or x1 <> x2 ) iff x1 -term is x2 -omitting )

proof end;

registration

let S be non empty non void ManySortedSign ;

let s, s1 be SortSymbol of S;

let Z be non-trivial ManySortedSet of the carrier of S;

let z be Element of Z . s;

let z9 be z -different Element of Z . s1;

coherence

z9 -term is z -omitting

end;
let s, s1 be SortSymbol of S;

let Z be non-trivial ManySortedSet of the carrier of S;

let z be Element of Z . s;

let z9 be z -different Element of Z . s1;

coherence

z9 -term is z -omitting

proof end;

registration

let S be non empty non void ManySortedSign ;

let s be SortSymbol of S;

let Z be non-trivial ManySortedSet of the carrier of S;

let z be Element of Z . s;

ex b_{1} being Element of (Free (S,Z)) st b_{1} is z -omitting

end;
let s be SortSymbol of S;

let Z be non-trivial ManySortedSet of the carrier of S;

let z be Element of Z . s;

cluster non empty Relation-like non pair Function-like finite DecoratedTree-like countable z -omitting for Element of Union the Sorts of (Free (S,Z));

existence ex b

proof end;

registration

let S be non empty non void ManySortedSign ;

let s, s1 be SortSymbol of S;

let Z be non-trivial ManySortedSet of the carrier of S;

let z be Element of Z . s;

let z1 be z -different Element of Z . s1;

ex b_{1} being Element of (Free (S,Z)) st

( b_{1} is z -omitting & b_{1} is z1 -context )

end;
let s, s1 be SortSymbol of S;

let Z be non-trivial ManySortedSet of the carrier of S;

let z be Element of Z . s;

let z1 be z -different Element of Z . s1;

cluster non empty Relation-like non pair Function-like finite DecoratedTree-like countable z1 -context z -omitting for Element of Union the Sorts of (Free (S,Z));

existence ex b

( b

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let x be Element of X . s;

mode context of x is x -context Element of (Free (S,X));

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

let s be SortSymbol of S;

let x be Element of X . s;

mode context of x is x -context Element of (Free (S,X));

theorem Th27: :: MSAFREE5:71

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for r being SortSymbol of S

for y being Element of X . r holds

( x -term is context of y iff ( r = s & x = y ) )

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for r being SortSymbol of S

for y being Element of X . r holds

( x -term is context of y iff ( r = s & x = y ) )

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

mode context of s,X is s -context Element of (Free (S,X));

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

let s be SortSymbol of S;

mode context of s,X is s -context Element of (Free (S,X));

theorem :: MSAFREE5:72

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x holds C is context of s,X ;

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x holds C is context of s,X ;

theorem Th95: :: MSAFREE5:73

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x holds x in vf C

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x holds x in vf C

proof end;

definition

let S be non empty non void ManySortedSign ;

let o be OperSymbol of S;

let s be SortSymbol of S;

let X be V5() ManySortedSet of the carrier of S;

let x be Element of X . s;

let p be Element of Args (o,(Free (S,X)));

end;
let o be OperSymbol of S;

let s be SortSymbol of S;

let X be V5() ManySortedSet of the carrier of S;

let x be Element of X . s;

let p be Element of Args (o,(Free (S,X)));

:: deftheorem defines -context_including MSAFREE5:def 24 :

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) holds

( p is x -context_including iff ex i being Nat st

( i in dom p & p . i is context of x & ( for j being Nat

for t being Element of (Free (S,X)) st j in dom p & j <> i & t = p . j holds

t is x -omitting ) ) );

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) holds

( p is x -context_including iff ex i being Nat st

( i in dom p & p . i is context of x & ( for j being Nat

for t being Element of (Free (S,X)) st j in dom p & j <> i & t = p . j holds

t is x -omitting ) ) );

registration

let S be non empty non void ManySortedSign ;

let o be OperSymbol of S;

let s be SortSymbol of S;

let X be V5() ManySortedSet of the carrier of S;

let x be Element of X . s;

coherence

for b_{1} being Element of Args (o,(Free (S,X))) st b_{1} is x -context_including holds

not b_{1} is empty
;

end;
let o be OperSymbol of S;

let s be SortSymbol of S;

let X be V5() ManySortedSet of the carrier of S;

let x be Element of X . s;

coherence

for b

not b

theorem Th53: :: MSAFREE5:74

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) holds

( p is x -context_including iff o -term p is context of x )

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) holds

( p is x -context_including iff o -term p is context of x )

proof end;

theorem Th54: :: MSAFREE5:75

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) holds

( ( for i being Nat st i in dom p holds

p /. i is x -omitting ) iff o -term p is x -omitting )

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) holds

( ( for i being Nat st i in dom p holds

p /. i is x -omitting ) iff o -term p is x -omitting )

proof end;

theorem Th54A: :: MSAFREE5:76

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) holds

( ( for t being Element of (Free (S,X)) st t in rng p holds

t is x -omitting ) iff o -term p is x -omitting )

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) holds

( ( for t being Element of (Free (S,X)) st t in rng p holds

t is x -omitting ) iff o -term p is x -omitting )

proof end;

definition
end;

:: deftheorem DEP defines -dependent MSAFREE5:def 25 :

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S holds

( o is s -dependent iff s in rng (the_arity_of o) );

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S holds

( o is s -dependent iff s in rng (the_arity_of o) );

registration

let S be non empty non void sufficiently_rich ManySortedSign ;

let s be SortSymbol of S;

existence

ex b_{1} being OperSymbol of S st b_{1} is s -dependent

end;
let s be SortSymbol of S;

existence

ex b

proof end;

registration

let S9 be non empty non void sufficiently_rich ManySortedSign ;

let s9 be SortSymbol of S9;

let o9 be s9 -dependent OperSymbol of S9;

let X9 be non-trivial ManySortedSet of the carrier of S9;

let x9 be Element of X9 . s9;

ex b_{1} being Element of Args (o9,(Free (S9,X9))) st b_{1} is x9 -context_including

end;
let s9 be SortSymbol of S9;

let o9 be s9 -dependent OperSymbol of S9;

let X9 be non-trivial ManySortedSet of the carrier of S9;

let x9 be Element of X9 . s9;

cluster Relation-like omega -defined Union the Sorts of (Free (S9,X9)) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding Relation-yielding DTree-yielding countable x9 -context_including for Element of Args (o9,(Free (S9,X9)));

existence ex b

proof end;

registration

let S9 be non empty non void sufficiently_rich ManySortedSign ;

let X9 be non-trivial ManySortedSet of the carrier of S9;

let s9 be SortSymbol of S9;

let x9 be Element of X9 . s9;

let o9 be s9 -dependent OperSymbol of S9;

let p9 be x9 -context_including Element of Args (o9,(Free (S9,X9)));

coherence

o9 -term p9 is x9 -context by Th53;

end;
let X9 be non-trivial ManySortedSet of the carrier of S9;

let s9 be SortSymbol of S9;

let x9 be Element of X9 . s9;

let o9 be s9 -dependent OperSymbol of S9;

let p9 be x9 -context_including Element of Args (o9,(Free (S9,X9)));

coherence

o9 -term p9 is x9 -context by Th53;

definition

let S be non empty non void ManySortedSign ;

let o be OperSymbol of S;

let s be SortSymbol of S;

let X be V5() ManySortedSet of the carrier of S;

let x be Element of X . s;

let p be Element of Args (o,(Free (S,X)));

assume A: p is x -context_including ;

consider i being Nat such that

B: ( i in dom p & p . i is context of x & ( for j being Nat

for t being Element of (Free (S,X)) st j in dom p & j <> i & t = p . j holds

t is x -omitting ) ) by A;

existence

ex b_{1} being Nat st p . b_{1} is context of x
by B;

uniqueness

for b_{1}, b_{2} being Nat st p . b_{1} is context of x & p . b_{2} is context of x holds

b_{1} = b_{2}

ex b_{1} being context of x st b_{1} in rng p

for b_{1}, b_{2} being context of x st b_{1} in rng p & b_{2} in rng p holds

b_{1} = b_{2}

end;
let o be OperSymbol of S;

let s be SortSymbol of S;

let X be V5() ManySortedSet of the carrier of S;

let x be Element of X . s;

let p be Element of Args (o,(Free (S,X)));

assume A: p is x -context_including ;

consider i being Nat such that

B: ( i in dom p & p . i is context of x & ( for j being Nat

for t being Element of (Free (S,X)) st j in dom p & j <> i & t = p . j holds

t is x -omitting ) ) by A;

existence

ex b

uniqueness

for b

b

proof end;

existence ex b

proof end;

uniqueness for b

b

proof end;

:: deftheorem CPI defines -context_pos_in MSAFREE5:def 26 :

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

for b_{7} being Nat holds

( b_{7} = x -context_pos_in p iff p . b_{7} is context of x );

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

for b

( b

:: deftheorem CIn defines -context_in MSAFREE5:def 27 :

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

for b_{7} being context of x holds

( b_{7} = x -context_in p iff b_{7} in rng p );

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

for b

( b

theorem Th71: :: MSAFREE5:77

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

( x -context_pos_in p in dom p & x -context_in p = p . (x -context_pos_in p) )

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

( x -context_pos_in p in dom p & x -context_in p = p . (x -context_pos_in p) )

proof end;

theorem Th72: :: MSAFREE5:78

for i being Nat

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including & x -context_pos_in p <> i & i in dom p holds

p /. i is x -omitting

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including & x -context_pos_in p <> i & i in dom p holds

p /. i is x -omitting

proof end;

theorem Th73: :: MSAFREE5:79

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

p just_once_values x -context_in p

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

p just_once_values x -context_in p

proof end;

theorem :: MSAFREE5:80

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

p <- (x -context_in p) = x -context_pos_in p

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

p <- (x -context_in p) = x -context_pos_in p

proof end;

theorem :: MSAFREE5:81

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x holds

( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st

( p is x -context_including & C = o -term p ) )

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x holds

( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st

( p is x -context_including & C = o -term p ) )

proof end;

registration

let S9 be non empty non void sufficiently_rich ManySortedSign ;

let X9 be non-trivial ManySortedSet of the carrier of S9;

let s9 be SortSymbol of S9;

let x9 be Element of X9 . s9;

ex b_{1} being Element of (Free (S9,X9)) st

( b_{1} is x9 -context & b_{1} is compound )

end;
let X9 be non-trivial ManySortedSet of the carrier of S9;

let s9 be SortSymbol of S9;

let x9 be Element of X9 . s9;

cluster non empty Relation-like non pair Function-like finite DecoratedTree-like countable compound x9 -context for Element of Union the Sorts of (Free (S9,X9));

existence ex b

( b

proof end;

scheme :: MSAFREE5:sch 4

ContextInd{ P_{1}[ set ], F_{1}() -> non empty non void ManySortedSign , F_{2}() -> SortSymbol of F_{1}(), F_{3}() -> V5() ManySortedSet of the carrier of F_{1}(), F_{4}() -> Element of F_{3}() . F_{2}(), F_{5}() -> context of F_{4}() } :

provided

ContextInd{ P

provided

A0:
P_{1}[F_{4}() -term ]
and

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

for w being Element of Args (o,(Free (F_{1}(),F_{3}()))) st w is F_{4}() -context_including & P_{1}[F_{4}() -context_in w] holds

for C being context of F_{4}() st C = o -term w holds

P_{1}[C]

A1: for o being OperSymbol of F

for w being Element of Args (o,(Free (F

for C being context of F

P

proof end;

theorem Th23: :: MSAFREE5:82

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t, t1 being Element of (Free (S,X)) st t is x -omitting holds

(t,[x,s]) <- t1 = t

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t, t1 being Element of (Free (S,X)) st t is x -omitting holds

(t,[x,s]) <- t1 = t

proof end;

theorem :: MSAFREE5:83

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t, t1 being Element of (Free (S,X)) st the_sort_of t1 = s holds

(t,[x,s]) <- t1 in the Sorts of (Free (S,X)) . (the_sort_of t)

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t, t1 being Element of (Free (S,X)) st the_sort_of t1 = s holds

(t,[x,s]) <- t1 in the Sorts of (Free (S,X)) . (the_sort_of t)

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let x be Element of X . s;

let C be context of x;

let t be Element of (Free (S,X));

assume A: the_sort_of t = s ;

(C,[x,s]) <- t is Element of the Sorts of (Free (S,X)) . (the_sort_of C)

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

let s be SortSymbol of S;

let x be Element of X . s;

let C be context of x;

let t be Element of (Free (S,X));

assume A: the_sort_of t = s ;

func C -sub t -> Element of the Sorts of (Free (S,X)) . (the_sort_of C) equals :SUB: :: MSAFREE5:def 28

(C,[x,s]) <- t;

coherence (C,[x,s]) <- t;

(C,[x,s]) <- t is Element of the Sorts of (Free (S,X)) . (the_sort_of C)

proof end;

:: deftheorem SUB defines -sub MSAFREE5:def 28 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for s being SortSymbol of S

for x being Element of X . s

for C being context of x

for t being Element of (Free (S,X)) st the_sort_of t = s holds

C -sub t = (C,[x,s]) <- t;

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for s being SortSymbol of S

for x being Element of X . s

for C being context of x

for t being Element of (Free (S,X)) st the_sort_of t = s holds

C -sub t = (C,[x,s]) <- t;

theorem Th41: :: MSAFREE5:84

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X)) st the_sort_of t = s holds

(x -term) -sub t = t

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X)) st the_sort_of t = s holds

(x -term) -sub t = t

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let x be Element of X . s;

let C be context of x;

reducibility

C -sub (x -term) = C

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

let s be SortSymbol of S;

let x be Element of X . s;

let C be context of x;

reducibility

C -sub (x -term) = C

proof end;

theorem Th42: :: MSAFREE5:85

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for w being Element of Args (o,(Free (S,Z)))

for t being Element of (Free (S,Z)) st w is z -context_including & the_sort_of t = (the_arity_of o) . (z -context_pos_in w) holds

w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))

for s being SortSymbol of S

for o being OperSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for w being Element of Args (o,(Free (S,Z)))

for t being Element of (Free (S,Z)) st w is z -context_including & the_sort_of t = (the_arity_of o) . (z -context_pos_in w) holds

w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))

proof end;

theorem Th94: :: MSAFREE5:86

for S being non empty non void ManySortedSign

for s, s1 being SortSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for C9 being context of z st the_sort_of C9 = s1 holds

for z1 being b_{5} -different Element of Z . s1

for C1 being b_{5} -omitting context of z1 holds C1 -sub C9 is context of z

for s, s1 being SortSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for C9 being context of z st the_sort_of C9 = s1 holds

for z1 being b

for C1 being b

proof end;

theorem Th43: :: MSAFREE5:87

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for C9 being context of z

for w, p being Element of Args (o,(Free (S,Z)))

for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds

C9 -sub t = o -term p

for s being SortSymbol of S

for o being OperSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for C9 being context of z

for w, p being Element of Args (o,(Free (S,Z)))

for t being Element of (Free (S,Z)) st w is z -context_including & C9 = o -term w & p = w +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds

C9 -sub t = o -term p

proof end;

theorem :: MSAFREE5:88

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X))

for C being context of x holds the_sort_of (C -sub t) = the_sort_of C by SORT;

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X))

for C being context of x holds the_sort_of (C -sub t) = the_sort_of C by SORT;

theorem Lem13: :: MSAFREE5:89

for a being object

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X)) st t . a = [x,s] holds

a in Leaves (dom t)

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X)) st t . a = [x,s] holds

a in Leaves (dom t)

proof end;

theorem Th45A: :: MSAFREE5:90

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X))

for C being context of x

for s0 being SortSymbol of S

for x0 being Element of X . s0 st the_sort_of t = s & C is x0 -omitting & t is x0 -omitting holds

C -sub t is x0 -omitting

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X))

for C being context of x

for s0 being SortSymbol of S

for x0 being Element of X . s0 st the_sort_of t = s & C is x0 -omitting & t is x0 -omitting holds

C -sub t is x0 -omitting

proof end;

theorem Th46: :: MSAFREE5:91

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

the_sort_of (x -context_in p) = (the_arity_of o) . (x -context_pos_in p)

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including holds

the_sort_of (x -context_in p) = (the_arity_of o) . (x -context_pos_in p)

proof end;

theorem Th47: :: MSAFREE5:92

for S being non empty non void ManySortedSign

for A being non-empty disjoint_valued MSAlgebra over S

for B being non-empty MSAlgebra over S

for o being OperSymbol of S

for p, q being Element of Args (o,A)

for h being ManySortedFunction of A,B

for a being Element of A

for i being Nat st i in dom p & q = p +* (i,a) holds

h # q = (h # p) +* (i,(h . a))

for A being non-empty disjoint_valued MSAlgebra over S

for B being non-empty MSAlgebra over S

for o being OperSymbol of S

for p, q being Element of Args (o,A)

for h being ManySortedFunction of A,B

for a being Element of A

for i being Nat st i in dom p & q = p +* (i,a) holds

h # q = (h # p) +* (i,(h . a))

proof end;

theorem :: MSAFREE5:93

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for R being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for C9 being context of z

for t being Element of (Free (S,Z)) st the_sort_of t = s holds

(canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t)))

for s being SortSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for R being b

for C9 being context of z

for t being Element of (Free (S,Z)) st the_sort_of t = s holds

(canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t)))

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x be Element of X . s;

let h be ManySortedFunction of (Free (S,X)),T;

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x be Element of X . s;

let h be ManySortedFunction of (Free (S,X)),T;

:: deftheorem CNST defines -constant MSAFREE5:def 29 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for s being SortSymbol of S

for x being Element of X . s

for h being ManySortedFunction of (Free (S,X)),T holds

( h is x -constant iff ( h . (x -term) = x -term & ( for s1 being SortSymbol of S

for x1 being Element of X . s1 st ( x1 <> x or s <> s1 ) holds

h . (x1 -term) is x -omitting ) ) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for s being SortSymbol of S

for x being Element of X . s

for h being ManySortedFunction of (Free (S,X)),T holds

( h is x -constant iff ( h . (x -term) = x -term & ( for s1 being SortSymbol of S

for x1 being Element of X . s1 st ( x1 <> x or s <> s1 ) holds

h . (x1 -term) is x -omitting ) ) );

theorem Th51: :: MSAFREE5:94

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds canonical_homomorphism T is x -constant

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for T being b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x be Element of X . s;

ex b_{1} being Homomorphism of Free (S,X),T st b_{1} is x -constant

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x be Element of X . s;

cluster non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding x -constant for Homomorphism of Free (S,X),T;

existence ex b

proof end;

definition

let x, y be object ;

coherence

{[x,y],[y,x]} is Function

for b_{1} being Function

for x, y being object st b_{1} = {[x,y],[y,x]} holds

b_{1} = {[y,x],[x,y]}
;

end;
coherence

{[x,y],[y,x]} is Function

proof end;

commutativity for b

for x, y being object st b

b

theorem LemS: :: MSAFREE5:95

for a, b being object holds

( dom (a <-> b) = {a,b} & (a <-> b) . a = b & (a <-> b) . b = a & rng (a <-> b) = {a,b} )

( dom (a <-> b) = {a,b} & (a <-> b) . a = b & (a <-> b) . b = a & rng (a <-> b) = {a,b} )

proof end;

registration

let A be non empty set ;

let a, b be Element of A;

coherence

( a <-> b is A -valued & a <-> b is A -defined )

end;
let a, b be Element of A;

coherence

( a <-> b is A -valued & a <-> b is A -defined )

proof end;

definition

let A be set ;

let B be non empty set ;

let f be Function of A,B;

let g be A -defined B -valued Function;

:: original: +*

redefine func f +* g -> Function of A,B;

coherence

f +* g is Function of A,B

end;
let B be non empty set ;

let f be Function of A,B;

let g be A -defined B -valued Function;

:: original: +*

redefine func f +* g -> Function of A,B;

coherence

f +* g is Function of A,B

proof end;

definition

let I be non empty set ;

let A, B be ManySortedSet of I;

let f be ManySortedFunction of A,B;

let x be Element of I;

let g be Function of (A . x),(B . x);

:: original: +*

redefine func f +* (x,g) -> ManySortedFunction of A,B;

coherence

f +* (x,g) is ManySortedFunction of A,B

end;
let A, B be ManySortedSet of I;

let f be ManySortedFunction of A,B;

let x be Element of I;

let g be Function of (A . x),(B . x);

:: original: +*

redefine func f +* (x,g) -> ManySortedFunction of A,B;

coherence

f +* (x,g) is ManySortedFunction of A,B

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x1, x2 be Element of X . s;

ex b_{1} being Endomorphism of T st

( (b_{1} . s) . (x1 -term) = x2 -term & (b_{1} . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S

for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds

(b_{1} . s1) . (y -term) = y -term ) )

for b_{1}, b_{2} being Endomorphism of T st (b_{1} . s) . (x1 -term) = x2 -term & (b_{1} . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S

for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds

(b_{1} . s1) . (y -term) = y -term ) & (b_{2} . s) . (x1 -term) = x2 -term & (b_{2} . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S

for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds

(b_{2} . s1) . (y -term) = y -term ) holds

b_{1} = b_{2}

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x1, x2 be Element of X . s;

func Hom (T,x1,x2) -> Endomorphism of T means :HOM: :: MSAFREE5:def 31

( (it . s) . (x1 -term) = x2 -term & (it . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S

for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds

(it . s1) . (y -term) = y -term ) );

existence ( (it . s) . (x1 -term) = x2 -term & (it . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S

for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds

(it . s1) . (y -term) = y -term ) );

ex b

( (b

for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds

(b

proof end;

uniqueness for b

for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds

(b

for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds

(b

b

proof end;

:: deftheorem HOM defines Hom MSAFREE5:def 31 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for s being SortSymbol of S

for x1, x2 being Element of X . s

for b_{7} being Endomorphism of T holds

( b_{7} = Hom (T,x1,x2) iff ( (b_{7} . s) . (x1 -term) = x2 -term & (b_{7} . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S

for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds

(b_{7} . s1) . (y -term) = y -term ) ) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

for s being SortSymbol of S

for x1, x2 being Element of X . s

for b

( b

for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds

(b

theorem Th52: :: MSAFREE5:96

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for h being Endomorphism of T st ( for s being SortSymbol of S

for x being Element of X . s holds (h . s) . (x -term) = x -term ) holds

h = id the Sorts of T

for X being V5() ManySortedSet of the carrier of S

for T being b

for h being Endomorphism of T st ( for s being SortSymbol of S

for x being Element of X . s holds (h . s) . (x -term) = x -term ) holds

h = id the Sorts of T

proof end;

theorem :: MSAFREE5:97

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Hom (T,x,x) = id the Sorts of T

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for T being b

proof end;

theorem Th56: :: MSAFREE5:98

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Hom (T,x1,x2) = Hom (T,x2,x1)

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b

proof end;

theorem Th157: :: MSAFREE5:99

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds (Hom (T,x1,x2)) ** (Hom (T,x1,x2)) = id the Sorts of T

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b

proof end;

theorem Th78: :: MSAFREE5:100

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T st r is x1 -omitting & r is x2 -omitting holds

(Hom (T,x1,x2)) . r = r

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b

for r being Element of T st r is x1 -omitting & r is x2 -omitting holds

(Hom (T,x1,x2)) . r = r

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x be Element of X . s;

reducibility

((canonical_homomorphism T) . s) . (x -term) = x -term

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

let s be SortSymbol of S;

let x be Element of X . s;

reducibility

((canonical_homomorphism T) . s) . (x -term) = x -term

proof end;

theorem Th66: :: MSAFREE5:101

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x, x1 being Element of X . s

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds (canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1)) = (Hom (T,x,x1)) ** (canonical_homomorphism T)

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x, x1 being Element of X . s

for T being b

proof end;

theorem :: MSAFREE5:102

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x1,x2))) . s) . r

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b

for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x1,x2))) . s) . r

proof end;

theorem :: MSAFREE5:103

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for t being Element of (Free (S,X)) st x1 <> x2 & t is x2 -omitting holds

(Hom ((Free (S,X)),x1,x2)) . t is x1 -omitting

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for t being Element of (Free (S,X)) st x1 <> x2 & t is x2 -omitting holds

(Hom ((Free (S,X)),x1,x2)) . t is x1 -omitting

proof end;

theorem Th3A: :: MSAFREE5:104

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for A being finite Subset of (Union the Sorts of (Free (S,Y))) ex y being Element of Y . s st

for v being Element of (Free (S,Y)) st v in A holds

v is y -omitting

for s being SortSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for A being finite Subset of (Union the Sorts of (Free (S,Y))) ex y being Element of Y . s st

for v being Element of (Free (S,Y)) st v in A holds

v is y -omitting

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

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

let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;

attr T is struct-invariant means :: MSAFREE5:def 32

for o being OperSymbol of S

for p being Element of Args (o,T) st (Den (o,T)) . p = (Den (o,(Free (S,X)))) . p holds

for s being SortSymbol of S

for x1, x2 being Element of X . s holds (Den (o,T)) . ((Hom (T,x1,x2)) # p) = (Den (o,(Free (S,X)))) . ((Hom (T,x1,x2)) # p);

for o being OperSymbol of S

for p being Element of Args (o,T) st (Den (o,T)) . p = (Den (o,(Free (S,X)))) . p holds

for s being SortSymbol of S

for x1, x2 being Element of X . s holds (Den (o,T)) . ((Hom (T,x1,x2)) # p) = (Den (o,(Free (S,X)))) . ((Hom (T,x1,x2)) # p);

:: deftheorem defines struct-invariant MSAFREE5:def 32 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds

( T is struct-invariant iff for o being OperSymbol of S

for p being Element of Args (o,T) st (Den (o,T)) . p = (Den (o,(Free (S,X)))) . p holds

for s being SortSymbol of S

for x1, x2 being Element of X . s holds (Den (o,T)) . ((Hom (T,x1,x2)) # p) = (Den (o,(Free (S,X)))) . ((Hom (T,x1,x2)) # p) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b

( T is struct-invariant iff for o being OperSymbol of S

for p being Element of Args (o,T) st (Den (o,T)) . p = (Den (o,(Free (S,X)))) . p holds

for s being SortSymbol of S

for x1, x2 being Element of X . s holds (Den (o,T)) . ((Hom (T,x1,x2)) # p) = (Den (o,(Free (S,X)))) . ((Hom (T,x1,x2)) # p) );

theorem :: MSAFREE5:105

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st T is struct-invariant holds

for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = ((Hom ((Free (S,X)),x1,x2)) . s) . r

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b

for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = ((Hom ((Free (S,X)),x1,x2)) . s) . r

proof end;

theorem Th79: :: MSAFREE5:106

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for r being Element of T st T is struct-invariant & x1 <> x2 & r is x2 -omitting holds

(Hom (T,x1,x2)) . r is x1 -omitting

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for T being b

for r being Element of T st T is struct-invariant & x1 <> x2 & r is x2 -omitting holds

(Hom (T,x1,x2)) . r is x1 -omitting

proof end;

theorem Th68: :: MSAFREE5:107

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for y being Element of Y . s

for Q being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for v being Element of (Free (S,Y)) st Q is struct-invariant & v is y -omitting holds

(canonical_homomorphism Q) . v is y -omitting

for s being SortSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for y being Element of Y . s

for Q being b

for v being Element of (Free (S,Y)) st Q is struct-invariant & v is y -omitting holds

(canonical_homomorphism Q) . v is y -omitting

proof end;

theorem Th77: :: MSAFREE5:108

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for y being Element of Y . s

for Q being b_{4},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st Q is struct-invariant holds

for p being Element of Args (o,Q) st ( for t being Element of Q st t in rng p holds

t is y -omitting ) holds

for t being Element of Q st t = (Den (o,Q)) . p holds

t is y -omitting

for s being SortSymbol of S

for o being OperSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for y being Element of Y . s

for Q being b

for p being Element of Args (o,Q) st ( for t being Element of Q st t in rng p holds

t is y -omitting ) holds

for t being Element of Q st t = (Den (o,Q)) . p holds

t is y -omitting

proof end;

theorem :: MSAFREE5:109

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for y being Element of Y . s

for Q being b_{3},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for v being Element of (Free (S,Y))

for h2 being b_{4} -constant Homomorphism of Free (S,Y),Q st Q is struct-invariant & v is y -omitting holds

h2 . v is y -omitting

for s being SortSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for y being Element of Y . s

for Q being b

for v being Element of (Free (S,Y))

for h2 being b

h2 . v is y -omitting

proof end;

theorem Th112: :: MSAFREE5:110

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) holds

( ( for t being Element of (NFAlgebra R) holds ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of t)) . t = (Hom ((NFAlgebra R),x1,x2)) . t ) & (Hom ((Free (S,X)),x1,x2)) || (NForms R) = Hom ((NFAlgebra R),x1,x2) )

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x1, x2 being Element of X . s

for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) holds

( ( for t being Element of (NFAlgebra R) holds ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of t)) . t = (Hom ((NFAlgebra R),x1,x2)) . t ) & (Hom ((Free (S,X)),x1,x2)) || (NForms R) = Hom ((NFAlgebra R),x1,x2) )

proof end;

theorem Th113: :: MSAFREE5:111

for i being Nat

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for t1, t2 being Element of (Free (S,X))

for p being Element of Args (o,(Free (S,X)))

for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) st i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 holds

R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2))

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for t1, t2 being Element of (Free (S,X))

for p being Element of Args (o,(Free (S,X)))

for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) st i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 holds

R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2))

proof end;

theorem Th90: :: MSAFREE5:112

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))

for t being Element of (Free (S,X)) holds R . (the_sort_of t) reduces t,(canonical_homomorphism (NFAlgebra R)) . t

for X being V5() ManySortedSet of the carrier of S

for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))

for t being Element of (Free (S,X)) holds R . (the_sort_of t) reduces t,(canonical_homomorphism (NFAlgebra R)) . t

proof end;

theorem Th98: :: MSAFREE5:113

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))

for o being OperSymbol of S

for p being Element of Args (o,(Free (S,X))) holds R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p)

for X being V5() ManySortedSet of the carrier of S

for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))

for o being OperSymbol of S

for p being Element of Args (o,(Free (S,X))) holds R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p)

proof end;

theorem Th69: :: MSAFREE5:114

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))

for o being OperSymbol of S

for p being Element of Args (o,(Free (S,X)))

for q being Element of Args (o,(NFAlgebra R)) st p = q holds

R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q

for X being V5() ManySortedSet of the carrier of S

for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))

for o being OperSymbol of S

for p being Element of Args (o,(Free (S,X)))

for q being Element of Args (o,(NFAlgebra R)) st p = q holds

R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

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

coherence

NFAlgebra R is struct-invariant

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

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

coherence

NFAlgebra R is struct-invariant

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

ex b_{1} being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st b_{1} is struct-invariant

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

cluster non-empty disjoint_valued X,S -terms all_vars_including inheriting_operations free_in_itself non empty struct-invariant for MSAlgebra over S;

existence ex b

proof end;

:: deftheorem REACH defines -reachable MSAFREE5:def 33 :

for S being non empty non void ManySortedSign

for s1, s2 being SortSymbol of S holds

( s2 is s1 -reachable iff TranslationRel S reduces s1,s2 );

for S being non empty non void ManySortedSign

for s1, s2 being SortSymbol of S holds

( s2 is s1 -reachable iff TranslationRel S reduces s1,s2 );

registration

let S be non empty non void ManySortedSign ;

let s1 be SortSymbol of S;

existence

ex b_{1} being SortSymbol of S st b_{1} is s1 -reachable

end;
let s1 be SortSymbol of S;

existence

ex b

proof end;

theorem :: MSAFREE5:115

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for C9 being context of z holds TranslationRel S reduces s, the_sort_of C9

for s being SortSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for C9 being context of z holds TranslationRel S reduces s, the_sort_of C9

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let x be Element of X . s;

let C be context of x;

coherence

the_sort_of C is s -reachable

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

let s be SortSymbol of S;

let x be Element of X . s;

let C be context of x;

coherence

the_sort_of C is s -reachable

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s1 be SortSymbol of S;

let s2 be s1 -reachable SortSymbol of S;

let g be Translation of Free (S,X),s1,s2;

let t be Element of the Sorts of (Free (S,X)) . s1;

:: original: .

redefine func g . t -> Element of the Sorts of (Free (S,X)) . s2;

coherence

g . t is Element of the Sorts of (Free (S,X)) . s2 by FUNCT_2:5;

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

let s1 be SortSymbol of S;

let s2 be s1 -reachable SortSymbol of S;

let g be Translation of Free (S,X),s1,s2;

let t be Element of the Sorts of (Free (S,X)) . s1;

:: original: .

redefine func g . t -> Element of the Sorts of (Free (S,X)) . s2;

coherence

g . t is Element of the Sorts of (Free (S,X)) . s2 by FUNCT_2:5;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let x be Element of X . s;

let C be context of x;

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

let s be SortSymbol of S;

let x be Element of X . s;

let C be context of x;

attr C is basic means :: MSAFREE5:def 34

ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st

( C = o -term p & x -context_in p = x -term );

ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st

( C = o -term p & x -context_in p = x -term );

:: deftheorem defines basic MSAFREE5:def 34 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for s being SortSymbol of S

for x being Element of X . s

for C being context of x holds

( C is basic iff ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st

( C = o -term p & x -context_in p = x -term ) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for s being SortSymbol of S

for x being Element of X . s

for C being context of x holds

( C is basic iff ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st

( C = o -term p & x -context_in p = x -term ) );

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

let x be Element of X . s;

let C be context of x;

ex b_{1} being Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . (the_sort_of C)) st

for t being Element of (Free (S,X)) st the_sort_of t = s holds

b_{1} . t = C -sub t

for b_{1}, b_{2} being Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . (the_sort_of C)) st ( for t being Element of (Free (S,X)) st the_sort_of t = s holds

b_{1} . t = C -sub t ) & ( for t being Element of (Free (S,X)) st the_sort_of t = s holds

b_{2} . t = C -sub t ) holds

b_{1} = b_{2}

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

let s be SortSymbol of S;

let x be Element of X . s;

let C be context of x;

func transl C -> Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . (the_sort_of C)) means :TRANS: :: MSAFREE5:def 35

for t being Element of (Free (S,X)) st the_sort_of t = s holds

it . t = C -sub t;

existence for t being Element of (Free (S,X)) st the_sort_of t = s holds

it . t = C -sub t;

ex b

for t being Element of (Free (S,X)) st the_sort_of t = s holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem TRANS defines transl MSAFREE5:def 35 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for s being SortSymbol of S

for x being Element of X . s

for C being context of x

for b_{6} being Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . (the_sort_of C)) holds

( b_{6} = transl C iff for t being Element of (Free (S,X)) st the_sort_of t = s holds

b_{6} . t = C -sub t );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for s being SortSymbol of S

for x being Element of X . s

for C being context of x

for b

( b

b

theorem Th57: :: MSAFREE5:116

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x st C = x -term holds

transl C = id ( the Sorts of (Free (S,X)) . s)

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x st C = x -term holds

transl C = id ( the Sorts of (Free (S,X)) . s)

proof end;

theorem Th58: :: MSAFREE5:117

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for l being Element of (Free (S,Z))

for k, k1 being Element of Args (o,(Free (S,Z)))

for C9 being context of z st C9 = o -term k & z -context_in k = z -term & k1 = k +* ((z -context_pos_in k),l) holds

C9 -sub l = o -term k1

for s being SortSymbol of S

for o being OperSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for l being Element of (Free (S,Z))

for k, k1 being Element of Args (o,(Free (S,Z)))

for C9 being context of z st C9 = o -term k & z -context_in k = z -term & k1 = k +* ((z -context_pos_in k),l) holds

C9 -sub l = o -term k1

proof end;

theorem :: MSAFREE5:118

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for C9 being context of z st C9 is basic holds

transl C9 is_e.translation_of Free (S,Z),s, the_sort_of C9

for s being SortSymbol of S

for Z being non-trivial ManySortedSet of the carrier of S

for z being Element of Z . s

for C9 being context of z st C9 is basic holds

transl C9 is_e.translation_of Free (S,Z),s, the_sort_of C9

proof end;

theorem Th59: :: MSAFREE5:119

for m being Element of NAT

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for q being Element of Args (o,(Free (S,Y)))

for V being finite set st m in dom q & (the_arity_of o) /. m = s holds

ex y being Element of Y . s ex C1 being context of y ex q1 being Element of Args (o,(Free (S,Y))) st

( y nin V & C1 = o -term q1 & q1 = q +* (m,(y -term)) & q1 is y -context_including & m = y -context_pos_in q1 & y -context_in q1 = y -term )

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for q being Element of Args (o,(Free (S,Y)))

for V being finite set st m in dom q & (the_arity_of o) /. m = s holds

ex y being Element of Y . s ex C1 being context of y ex q1 being Element of Args (o,(Free (S,Y))) st

( y nin V & C1 = o -term q1 & q1 = q +* (m,(y -term)) & q1 is y -context_including & m = y -context_pos_in q1 & y -context_in q1 = y -term )

proof end;

theorem Th91: :: MSAFREE5:120

for m being Element of NAT

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for q being Element of Args (o,(Free (S,Y)))

for s1, s2 being SortSymbol of S

for V being finite set st m in dom q & s1 = (the_arity_of o) /. m holds

ex y being Element of Y . s1 ex C being context of y ex q1 being Element of Args (o,(Free (S,Y))) st

( y nin V & q1 = q +* (m,(y -term)) & q1 is y -context_including & y -context_in q1 = y -term & C = o -term q1 & m = y -context_pos_in q1 & transl C = transl (o,m,q,(Free (S,Y))) )

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for q being Element of Args (o,(Free (S,Y)))

for s1, s2 being SortSymbol of S

for V being finite set st m in dom q & s1 = (the_arity_of o) /. m holds

ex y being Element of Y . s1 ex C being context of y ex q1 being Element of Args (o,(Free (S,Y))) st

( y nin V & q1 = q +* (m,(y -term)) & q1 is y -context_including & y -context_in q1 = y -term & C = o -term q1 & m = y -context_pos_in q1 & transl C = transl (o,m,q,(Free (S,Y))) )

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let t be Element of (Free (S,X));

let a be object ;

coherence

Coim (t,a) is FinSequence-membered ;

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

let t be Element of (Free (S,X));

let a be object ;

coherence

Coim (t,a) is FinSequence-membered ;

theorem Th70: :: MSAFREE5:121

for a being object

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X))

for C being context of x st X is non-trivial & the_sort_of t = s holds

card (Coim (t,a)) c= card (Coim ((C -sub t),a))

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X))

for C being context of x st X is non-trivial & the_sort_of t = s holds

card (Coim (t,a)) c= card (Coim ((C -sub t),a))

proof end;

theorem :: MSAFREE5:122

for i being Nat

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including & i in dom p holds

( not p /. i is x -omitting iff p /. i is x -context )

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for o being OperSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for p being Element of Args (o,(Free (S,X))) st p is x -context_including & i in dom p holds

( not p /. i is x -omitting iff p /. i is x -context )

proof end;

theorem Th60: :: MSAFREE5:123

for S being non empty non void ManySortedSign

for s, s1 being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x st X is non-trivial & the_sort_of C = s1 holds

for x1 being Element of X . s1

for C1 being context of x1

for C2 being context of x st C2 = C1 -sub C holds

for t being Element of (Free (S,X)) st the_sort_of t = s holds

C2 -sub t = C1 -sub (C -sub t)

for s, s1 being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x st X is non-trivial & the_sort_of C = s1 holds

for x1 being Element of X . s1

for C1 being context of x1

for C2 being context of x st C2 = C1 -sub C holds

for t being Element of (Free (S,X)) st the_sort_of t = s holds

C2 -sub t = C1 -sub (C -sub t)

proof end;

theorem Th93: :: MSAFREE5:124

for S being non empty non void ManySortedSign

for s, s1 being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x st X is non-trivial & the_sort_of C = s1 holds

for x1 being Element of X . s1

for C1 being context of x1

for C2 being context of x st C2 = C1 -sub C holds

transl C2 = (transl C1) * (transl C)

for s, s1 being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for C being context of x st X is non-trivial & the_sort_of C = s1 holds

for x1 being Element of X . s1

for C1 being context of x1

for C2 being context of x st C2 = C1 -sub C holds

transl C2 = (transl C1) * (transl C)

proof end;

theorem :: MSAFREE5:125

for S being non empty non void ManySortedSign

for s1 being SortSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for s2 being b_{2} -reachable SortSymbol of S

for g1 being Translation of Free (S,Y),s1,s2 ex y11 being Element of Y . s1 ex C12 being context of y11 st

( the_sort_of C12 = s2 & g1 = transl C12 )

for s1 being SortSymbol of S

for Y being infinite-yielding ManySortedSet of the carrier of S

for s2 being b

for g1 being Translation of Free (S,Y),s1,s2 ex y11 being Element of Y . s1 ex C12 being context of y11 st

( the_sort_of C12 = s2 & g1 = transl C12 )

proof end;

scheme :: MSAFREE5:sch 5

LambdaTerm{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> V5() ManySortedSet of the carrier of F_{1}(), F_{3}() -> F_{2}(),F_{1}() -terms all_vars_including inheriting_operations MSAlgebra over F_{1}(), F_{4}() -> F_{2}(),F_{1}() -terms all_vars_including inheriting_operations MSAlgebra over F_{1}(), F_{5}( object ) -> Element of F_{4}() } :

LambdaTerm{ F

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

for t being Element of F_{3}() holds f . t = F_{5}(t)

provided
for t being Element of F

proof end;

theorem Th86: :: MSAFREE5:126

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for h being Endomorphism of Free (S,X) ex g being Endomorphism of T st

( (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) & ( for t being Element of T holds g . t = (canonical_homomorphism T) . (h . (@ t)) ) )

for X being V5() ManySortedSet of the carrier of S

for T being b

for h being Endomorphism of Free (S,X) ex g being Endomorphism of T st

( (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) & ( for t being Element of T holds g . t = (canonical_homomorphism T) . (h . (@ t)) ) )

proof end;

theorem :: MSAFREE5:127

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for T being b_{2},b_{1} -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S

for h being Endomorphism of Free (S,X)

for t being Element of (Free (S,X)) holds (canonical_homomorphism T) . (h . t) = (canonical_homomorphism T) . (h . (@ ((canonical_homomorphism T) . t)))

for X being V5() ManySortedSet of the carrier of S

for T being b

for h being Endomorphism of Free (S,X)

for t being Element of (Free (S,X)) holds (canonical_homomorphism T) . (h . t) = (canonical_homomorphism T) . (h . (@ ((canonical_homomorphism T) . t)))

proof end;

definition

let S be non empty non void ManySortedSign ;

let B be non empty FinSequence of the carrier of S;

let i be Element of dom B;

:: original: .

redefine func B . i -> SortSymbol of S;

coherence

B . i is SortSymbol of S by PARTFUN1:4;

end;
let B be non empty FinSequence of the carrier of S;

let i be Element of dom B;

:: original: .

redefine func B . i -> SortSymbol of S;

coherence

B . i is SortSymbol of S by PARTFUN1:4;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be FinSequence of the carrier of S;

let V be FinSequence of Union X;

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

let B be FinSequence of the carrier of S;

let V be FinSequence of Union X;

:: deftheorem SORTS defines -sorts MSAFREE5:def 36 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being FinSequence of the carrier of S

for V being FinSequence of Union X holds

( V is B -sorts iff ( dom V = dom B & ( for i being Nat st i in dom B holds

V . i in X . (B . i) ) ) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being FinSequence of the carrier of S

for V being FinSequence of Union X holds

( V is B -sorts iff ( dom V = dom B & ( for i being Nat st i in dom B holds

V . i in X . (B . i) ) ) );

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be FinSequence of the carrier of S;

ex b_{1} being FinSequence of Union X st b_{1} is B -sorts

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

let B be FinSequence of the carrier of S;

cluster Relation-like omega -defined Union X -valued Function-like finite FinSequence-like FinSubsequence-like countable B -sorts for FinSequence of Union X;

existence ex b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

coherence

for b_{1} being FinSequence of Union X st b_{1} is B -sorts holds

not b_{1} is empty
;

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

let B be non empty FinSequence of the carrier of S;

coherence

for b

not b

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union X;

let i be Element of dom B;

:: original: .

redefine func V . i -> Element of X . (B . i);

coherence

V . i is Element of X . (B . i) by SORTS;

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

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union X;

let i be Element of dom B;

:: original: .

redefine func V . i -> Element of X . (B . i);

coherence

V . i is Element of X . (B . i) by SORTS;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be FinSequence of the carrier of S;

let D be FinSequence of (Free (S,X));

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

let B be FinSequence of the carrier of S;

let D be FinSequence of (Free (S,X));

:: deftheorem SORTS2 defines -sorts MSAFREE5:def 37 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being FinSequence of the carrier of S

for D being FinSequence of (Free (S,X)) holds

( D is B -sorts iff ( dom D = dom B & ( for i being Nat st i in dom B holds

D . i in the Sorts of (Free (S,X)) . (B . i) ) ) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being FinSequence of the carrier of S

for D being FinSequence of (Free (S,X)) holds

( D is B -sorts iff ( dom D = dom B & ( for i being Nat st i in dom B holds

D . i in the Sorts of (Free (S,X)) . (B . i) ) ) );

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be FinSequence of the carrier of S;

ex b_{1} being FinSequence of (Free (S,X)) st b_{1} is B -sorts

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

let B be FinSequence of the carrier of S;

cluster Relation-like omega -defined Union the Sorts of (Free (S,X)) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding Relation-yielding DTree-yielding countable B -sorts for FinSequence of Union the Sorts of (Free (S,X));

existence ex b

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

coherence

for b_{1} being FinSequence of (Free (S,X)) st b_{1} is B -sorts holds

not b_{1} is empty
;

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

let B be non empty FinSequence of the carrier of S;

coherence

for b

not b

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

let D be B -sorts FinSequence of (Free (S,X));

let i be Element of dom B;

:: original: .

redefine func D . i -> Element of the Sorts of (Free (S,X)) . (B . i);

coherence

D . i is Element of the Sorts of (Free (S,X)) . (B . i) by SORTS2;

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

let B be non empty FinSequence of the carrier of S;

let D be B -sorts FinSequence of (Free (S,X));

let i be Element of dom B;

:: original: .

redefine func D . i -> Element of the Sorts of (Free (S,X)) . (B . i);

coherence

D . i is Element of the Sorts of (Free (S,X)) . (B . i) by SORTS2;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union X;

let F be FinSequence of (Free (S,X));

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

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union X;

let F be FinSequence of (Free (S,X));

:: deftheorem CONTEXTSEQ defines -context-sequence MSAFREE5:def 38 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being non empty FinSequence of the carrier of S

for V being b_{3} -sorts FinSequence of Union X

for F being FinSequence of (Free (S,X)) holds

( F is V -context-sequence iff ( dom F = dom B & ( for i being Element of dom B holds F . i is context of V . i ) ) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being non empty FinSequence of the carrier of S

for V being b

for F being FinSequence of (Free (S,X)) holds

( F is V -context-sequence iff ( dom F = dom B & ( for i being Element of dom B holds F . i is context of V . i ) ) );

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union X;

coherence

for b_{1} being FinSequence of (Free (S,X)) st b_{1} is V -context-sequence holds

not b_{1} is empty
;

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

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union X;

coherence

for b

not b

scheme :: MSAFREE5:sch 6

FinSeqLambda{ F_{1}() -> non empty FinSequence, F_{2}( set ) -> object } :

FinSeqLambda{ F

ex p being non empty FinSequence st

( dom p = dom F_{1}() & ( for i being Element of dom F_{1}() holds p . i = F_{2}(i) ) )

( dom p = dom F

proof end;

scheme :: MSAFREE5:sch 7

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

FinSeqRecLambda{ F

ex p being non empty FinSequence st

( dom p = dom F_{1}() & p . 1 = F_{2}() & ( for i, j being Element of dom F_{1}() st j = i + 1 holds

p . j = F_{3}(i,(p . i)) ) )

( dom p = dom F

p . j = F

proof end;

scheme :: MSAFREE5:sch 8

FinSeqRec2Lambda{ F_{1}() -> non empty FinSequence, F_{2}() -> DecoratedTree, F_{3}( object , DecoratedTree) -> DecoratedTree } :

FinSeqRec2Lambda{ F

ex p being non empty DTree-yielding FinSequence st

( dom p = dom F_{1}() & p . 1 = F_{2}() & ( for i, j being Element of dom F_{1}() st j = i + 1 holds

for d being DecoratedTree st d = p . i holds

p . j = F_{3}(i,d) ) )

( dom p = dom F

for d being DecoratedTree st d = p . i holds

p . j = F

proof end;

registration

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union X;

ex b_{1} being FinSequence of (Free (S,X)) st b_{1} is V -context-sequence

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

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union X;

cluster Relation-like omega -defined Union the Sorts of (Free (S,X)) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding Relation-yielding DTree-yielding countable V -context-sequence for FinSequence of Union the Sorts of (Free (S,X));

existence ex b

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union X;

let F be V -context-sequence FinSequence of (Free (S,X));

let i be Element of dom B;

:: original: .

redefine func F . i -> context of V . i;

coherence

F . i is context of V . i by CONTEXTSEQ;

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

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union X;

let F be V -context-sequence FinSequence of (Free (S,X));

let i be Element of dom B;

:: original: .

redefine func F . i -> context of V . i;

coherence

F . i is context of V . i by CONTEXTSEQ;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

let V1, V2 be B -sorts FinSequence of Union X;

let D be B -sorts FinSequence of (Free (S,X));

let F be V2 -context-sequence FinSequence of (Free (S,X));

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

let B be non empty FinSequence of the carrier of S;

let V1, V2 be B -sorts FinSequence of Union X;

let D be B -sorts FinSequence of (Free (S,X));

let F be V2 -context-sequence FinSequence of (Free (S,X));

:: deftheorem OMIT2 defines -omitting MSAFREE5:def 39 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being non empty FinSequence of the carrier of S

for V1, V2 being b_{3} -sorts FinSequence of Union X holds

( V2 is V1 -omitting iff rng V1 misses rng V2 );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being non empty FinSequence of the carrier of S

for V1, V2 being b

( V2 is V1 -omitting iff rng V1 misses rng V2 );

:: deftheorem defines -consequent-context-sequence MSAFREE5:def 40 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being non empty FinSequence of the carrier of S

for V1, V2 being b_{3} -sorts FinSequence of Union X

for D being b_{3} -sorts FinSequence of (Free (S,X))

for F being b_{5} -context-sequence FinSequence of (Free (S,X)) holds

( F is V1,V2,D -consequent-context-sequence iff for i, j being Element of dom B st i + 1 = j holds

(F . j) -sub ((V1 . j) -term) = (F . i) -sub (D . i) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being non empty FinSequence of the carrier of S

for V1, V2 being b

for D being b

for F being b

( F is V1,V2,D -consequent-context-sequence iff for i, j being Element of dom B st i + 1 = j holds

(F . j) -sub ((V1 . j) -term) = (F . i) -sub (D . i) );

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

let D be B -sorts FinSequence of (Free (S,X));

let V be B -sorts FinSequence of Union X;

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

let B be non empty FinSequence of the carrier of S;

let D be B -sorts FinSequence of (Free (S,X));

let V be B -sorts FinSequence of Union X;

:: deftheorem defines -omitting MSAFREE5:def 41 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being non empty FinSequence of the carrier of S

for D being b_{3} -sorts FinSequence of (Free (S,X))

for V being b_{3} -sorts FinSequence of Union X holds

( V is D -omitting iff for t being Element of (Free (S,X)) st t in rng D holds

vf t misses rng V );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being non empty FinSequence of the carrier of S

for D being b

for V being b

( V is D -omitting iff for t being Element of (Free (S,X)) st t in rng D holds

vf t misses rng V );

theorem OMIT4: :: MSAFREE5:128

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for B being non empty FinSequence of the carrier of S

for D being b_{3} -sorts FinSequence of (Free (S,X))

for V being b_{3} -sorts FinSequence of Union X st V is D -omitting holds

for b1, b2 being Element of dom B holds D . b1 is V . b2 -omitting

for X being V5() ManySortedSet of the carrier of S

for B being non empty FinSequence of the carrier of S

for D being b

for V being b

for b1, b2 being Element of dom B holds D . b1 is V . b2 -omitting

proof end;

registration

let S be non empty non void ManySortedSign ;

let Y be infinite-yielding ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union Y;

let D be B -sorts FinSequence of (Free (S,Y));

ex b_{1} being B -sorts FinSequence of Union Y st

( b_{1} is one-to-one & b_{1} is V -omitting & b_{1} is D -omitting )

end;
let Y be infinite-yielding ManySortedSet of the carrier of S;

let B be non empty FinSequence of the carrier of S;

let V be B -sorts FinSequence of Union Y;

let D be B -sorts FinSequence of (Free (S,Y));

cluster non empty Relation-like omega -defined Union Y -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like countable B -sorts V -omitting D -omitting for FinSequence of Union Y;

existence ex b

( b

proof end;

definition

let S be non empty non void ManySortedSign ;

let X be V5() ManySortedSet of the carrier of S;

let t be Element of (Free (S,X));

ex b_{1} being FinSequence ex f being one-to-one FinSequence st

( rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & dom b_{1} = dom f & ( for i being Nat st i in dom b_{1} holds

b_{1} . i = t . (f . i) ) )

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

let t be Element of (Free (S,X));

mode vf-sequence of t -> FinSequence means :VFS: :: MSAFREE5:def 42

ex f being one-to-one FinSequence st

( rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & dom it = dom f & ( for i being Nat st i in dom it holds

it . i = t . (f . i) ) );

existence ex f being one-to-one FinSequence st

( rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & dom it = dom f & ( for i being Nat st i in dom it holds

it . i = t . (f . i) ) );

ex b

( rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & dom b

b

proof end;

:: deftheorem VFS defines vf-sequence MSAFREE5:def 42 :

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for b_{4} being FinSequence holds

( b_{4} is vf-sequence of t iff ex f being one-to-one FinSequence st

( rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & dom b_{4} = dom f & ( for i being Nat st i in dom b_{4} holds

b_{4} . i = t . (f . i) ) ) );

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for b

( b

( rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & dom b

b

registration

let f be FinSequence;

coherence

pr1 f is FinSequence-like

pr2 f is FinSequence-like

end;
coherence

pr1 f is FinSequence-like

proof end;

coherence pr2 f is FinSequence-like

proof end;

theorem Th96: :: MSAFREE5:129

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for f being vf-sequence of t holds pr2 f is FinSequence of the carrier of S

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for f being vf-sequence of t holds pr2 f is FinSequence of the carrier of S

proof end;

theorem Th97: :: MSAFREE5:130

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for f being vf-sequence of t

for B being FinSequence of the carrier of S st B = pr2 f holds

pr1 f is b_{5} -sorts FinSequence of Union X

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for f being vf-sequence of t

for B being FinSequence of the carrier of S st B = pr2 f holds

pr1 f is b

proof end;

registration

let f be non empty FinSequence;

reducibility

In (1,(dom f)) = 1 by FINSEQ_5:6, SUBSET_1:def 8;

reducibility

In ((len f),(dom f)) = len f by SUBSET_1:def 8, FINSEQ_5:6;

end;
reducibility

In (1,(dom f)) = 1 by FINSEQ_5:6, SUBSET_1:def 8;

reducibility

In ((len f),(dom f)) = len f by SUBSET_1:def 8, FINSEQ_5:6;

theorem Th117: :: MSAFREE5:131

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t, t1 being Element of (Free (S,X))

for xi being Element of dom t st t . xi = [x,s] & the_sort_of t1 = s holds

t with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t, t1 being Element of (Free (S,X))

for xi being Element of dom t st t . xi = [x,s] & the_sort_of t1 = s holds

t with-replacement (xi,t1) is Element of (Free (S,X)),(the_sort_of t)

proof end;

theorem Th118: :: MSAFREE5:132

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X))

for C being context of x st X is non-trivial holds

for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds

C -sub t = C with-replacement (xi,t)

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X))

for C being context of x st X is non-trivial holds

for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds

C -sub t = C with-replacement (xi,t)

proof end;

theorem Lem9: :: MSAFREE5:133

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for xi1, xi2 being FinSequence st xi1 <> xi2 & xi1 in dom t & xi2 in dom t holds

for s1, s2 being SortSymbol of S

for x1 being Element of X . s1

for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds

not xi1 is_a_prefix_of xi2

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for xi1, xi2 being FinSequence st xi1 <> xi2 & xi1 in dom t & xi2 in dom t holds

for s1, s2 being SortSymbol of S

for x1 being Element of X . s1

for x2 being Element of X . s2 st t . xi1 = [x1,s1] holds

not xi1 is_a_prefix_of xi2

proof end;

theorem Lem10: :: MSAFREE5:134

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t, t1 being Element of (Free (S,X))

for xi being Element of dom t st t1 = t with-replacement (xi,(x -term)) & t is x -omitting holds

t1 is context of x

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t, t1 being Element of (Free (S,X))

for xi being Element of dom t st t1 = t with-replacement (xi,(x -term)) & t is x -omitting holds

t1 is context of x

proof end;

theorem Lem11: :: MSAFREE5:135

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t, t1 being Element of (Free (S,X))

for xi being Element of dom t st t . xi = [x,s] holds

dom t c= dom (t with-replacement (xi,t1))

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t, t1 being Element of (Free (S,X))

for xi being Element of dom t st t . xi = [x,s] holds

dom t c= dom (t with-replacement (xi,t1))

proof end;

theorem Lem11A: :: MSAFREE5:136

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x, x1 being Element of X . s

for t being Element of (Free (S,X))

for xi being Element of dom t st t . xi = [x,s] holds

dom t = dom (t with-replacement (xi,(x1 -term)))

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x, x1 being Element of X . s

for t being Element of (Free (S,X))

for xi being Element of dom t st t . xi = [x,s] holds

dom t = dom (t with-replacement (xi,(x1 -term)))

proof end;

theorem Th131: :: MSAFREE5:139

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for h being Endomorphism of Free (S,X)

for t, t1 being Element of (Free (S,X))

for xi being Node of t st t1 = t | xi holds

(h . t) | xi = h . t1

for X being V5() ManySortedSet of the carrier of S

for h being Endomorphism of Free (S,X)

for t, t1 being Element of (Free (S,X))

for xi being Node of t st t1 = t | xi holds

(h . t) | xi = h . t1

proof end;

theorem Th132: :: MSAFREE5:140

for S being non empty non void ManySortedSign

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X))

for xi being Node of t st t . xi = [x,s] holds

t | xi = x -term

for s being SortSymbol of S

for X being V5() ManySortedSet of the carrier of S

for x being Element of X . s

for t being Element of (Free (S,X))

for xi being Node of t st t . xi = [x,s] holds

t | xi = x -term

proof end;

theorem Th134: :: MSAFREE5:141

for t, t1 being Tree

for xi, nu being Element of t st not xi c= nu & not nu c= xi holds

(t with-replacement (xi,t1)) | nu = t | nu

for xi, nu being Element of t st not xi c= nu & not nu c= xi holds

(t with-replacement (xi,t1)) | nu = t | nu

proof end;

theorem Th133: :: MSAFREE5:142

for t, t1 being DecoratedTree

for xi, nu being Node of t st not xi c= nu & not nu c= xi holds

(t with-replacement (xi,t1)) | nu = t | nu

for xi, nu being Node of t st not xi c= nu & not nu c= xi holds

(t with-replacement (xi,t1)) | nu = t | nu

proof end;

theorem Th136: :: MSAFREE5:143

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t, t1 being Element of (Free (S,X)) st t c= t1 holds

t = t1

for X being V5() ManySortedSet of the carrier of S

for t, t1 being Element of (Free (S,X)) st t c= t1 holds

t = t1

proof end;

theorem Th135: :: MSAFREE5:144

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for h being Endomorphism of Free (S,X) holds

( dom t c= dom (h . t) & ( for I being set st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds

t | ((dom t) \ I) = (h . t) | ((dom t) \ I) ) )

for X being V5() ManySortedSet of the carrier of S

for t being Element of (Free (S,X))

for h being Endomorphism of Free (S,X) holds

( dom t c= dom (h . t) & ( for I being set st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds

t | ((dom t) \ I) = (h . t) | ((dom t) \ I) ) )

proof end;

theorem Th137: :: MSAFREE5:145

for I being set

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for h being Endomorphism of Free (S,X)

for t being Element of (Free (S,X)) st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds

for xi being Node of (h . t) holds

( xi in (dom t) \ I or ex nu being Element of dom t st

( nu in I & ex mu being Node of ((h . t) | nu) st xi = nu ^ mu ) )

for S being non empty non void ManySortedSign

for X being V5() ManySortedSet of the carrier of S

for h being Endomorphism of Free (S,X)

for t being Element of (Free (S,X)) st I = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } holds

for xi being Node of (h . t) holds

( xi in (dom t) \ I or ex nu being Element of dom t st

( nu in I & ex mu being Node of ((h . t) | nu) st xi = nu ^ mu ) )

proof end;

theorem Th138: :: MSAFREE5:146

for S being non empty non void ManySortedSign

for Y being infinite-yielding ManySortedSet of the carrier of S

for v, v1 being Element of (Free (S,Y))

for h being Endomorphism of Free (S,Y)

for g being one-to-one FinSequence of dom v st rng g = { xi where xi is Element of dom v : ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] } & dom v c= dom v1 & v | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) & ( for i being Nat st i in dom g holds

(h . v) | (g /. i) = v1 | (g /. i) ) holds

h . v = v1

for Y being infinite-yielding ManySortedSet of the carrier of S

for v, v1 being Element of (Free (S,Y))

for h being Endomorphism of Free (S,Y)

for g being one-to-one FinSequence of dom v st rng g = { xi where xi is Element of dom v : ex s being SortSymbol of S ex y being Element of Y . s st v . xi = [y,s] } & dom v c= dom v1 & v | ((dom v) \ (rng g)) = v1 | ((dom v) \ (rng g)) & ( for i being Nat st i in dom g holds

(h . v) | (g /. i) = v1 | (g /. i) ) holds

h . v = v1

proof end;

theorem :: MSAFREE5:147

for S being non empty non void ManySortedSign

for Y being infinite-yielding ManySortedSet of the carrier of S

for v being Element of (Free (S,Y))

for h being Endomorphism of Free (S,Y)

for f being vf-sequence of v st f <> {} holds

ex B being non empty FinSequence of the carrier of S ex V1 being b_{6} -sorts FinSequence of Union Y st

( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being b_{6} -sorts FinSequence of (Free (S,Y)) ex V2 being b_{6} -sorts b_{7} -omitting b_{8} -omitting FinSequence of Union Y st

( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b_{9} -context-sequence FinSequence of (Free (S,Y)) st

( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) ) )

for Y being infinite-yielding ManySortedSet of the carrier of S

for v being Element of (Free (S,Y))

for h being Endomorphism of Free (S,Y)

for f being vf-sequence of v st f <> {} holds

ex B being non empty FinSequence of the carrier of S ex V1 being b

( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being b

( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b

( F is V1,V2,D -consequent-context-sequence & (F . (In (1,(dom B)))) -sub ((V1 . (In (1,(dom B)))) -term) = v & h . v = (F . (In ((len B),(dom B)))) -sub (D . (In ((len B),(dom B)))) ) ) )

proof end;