:: Term Context
:: by Grzegorz Bancerek
::
:: Copyright (c) 2014-2019 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;

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;
func @ r -> Element of (Free (S,X)) equals :: MSAFREE5:def 1
r;
coherence
r is Element of (Free (S,X))
by MSAFREE4:39;
end;

:: 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 b2,b1 -terms all_vars_including MSAlgebra over S
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;
cluster -> finite for Element of Union the Sorts of T;
coherence
for b1 being Element of T holds b1 is finite
proof end;
end;

registration
coherence
for b1 being set st b1 is natural-membered holds
b1 is c=-linear
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let a be object ;
pred a in A means :ELEM: :: MSAFREE5:def 2
a in Union the Sorts of A;
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 );

definition
let a, b be object ;
attr b is a -different means :DIFF: :: MSAFREE5:def 3
b <> a;
end;

:: deftheorem DIFF defines -different MSAFREE5:def 3 :
for a, b being object holds
( b is a -different iff b <> a );

registration
let I be non trivial set ;
let a be object ;
cluster a -different for Element of I;
existence
ex b1 being Element of I st b1 is a -different
proof end;
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 ) )
proof end;

theorem Lem8: :: MSAFREE5:2
for p, q, r being FinSequence st p ^ q is_a_prefix_of r holds
p is_a_prefix_of r
proof end;

theorem Lem8A: :: MSAFREE5:3
for p, q, r being FinSequence st p ^ q is_a_prefix_of p ^ r holds
q is_a_prefix_of r
proof end;

theorem LemP: :: MSAFREE5:4
for i being Nat
for p, q being FinSequence st i <= len p holds
(p ^ q) | (Seg i) = p | (Seg i)
proof 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 )
proof end;

definition
let S be non empty non void ManySortedSign ;
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 ();
attr S is growable means :: MSAFREE5:def 5
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;
end;

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

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

definition
let n be Nat;
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 () = n;
end;

:: 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 () = n );

registration
let n be Nat;
existence
ex b1 being non empty non void ManySortedSign st b1 is n -ary_oper_including
proof end;
end;

registration
existence
ex b1 being non empty non void ManySortedSign st b1 is sufficiently_rich
proof end;
end;

definition
let R be Relation;
attr R is non-trivial means :NT: :: MSAFREE5:def 7
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 ;
end;

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

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

registration
coherence
for b1 being Relation st b1 is non-trivial holds
b1 is non-empty
proof end;
coherence
for b1 being Relation st b1 is infinite-yielding holds
b1 is non-trivial
;
end;

registration
let I be set ;
existence
ex b1 being ManySortedSet of I st b1 is infinite-yielding
proof end;
end;

registration
existence
ex b1 being FinSequence st b1 is infinite-yielding
proof end;
end;

registration
let I be non empty set ;
let f be non-trivial ManySortedSet of I;
let a be Element of I;
cluster f . a -> non trivial ;
coherence
not f . a is trivial
by NT;
end;

registration
let I be non empty set ;
let f be infinite-yielding ManySortedSet of I;
let a be Element of I;
cluster f . a -> infinite ;
coherence
not f . a is finite
by INF;
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;
cluster -> DTree-yielding for Element of Args (o,(Free (S,X)));
coherence
for b1 being Element of Args (o,(Free (S,X))) holds b1 is DTree-yielding
proof end;
end;

registration
let p be FinSequence;
reduce p ^ {} to p;
reducibility
p ^ {} = p
by FINSEQ_1:34;
reduce {} ^ p to p;
reducibility
{} ^ p = p
by FINSEQ_1:34;
end;

definition
let I be FinSequence-membered set ;
let p be FinSequence;
func p ^^ I -> set equals :: MSAFREE5:def 9
{ (p ^ q) where q is Element of I : q in I } ;
coherence
{ (p ^ q) where q is Element of I : q in I } is set
;
end;

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

registration
let I be FinSequence-membered set ;
let p be FinSequence;
coherence
proof end;
end;

registration
let f be FinSequence;
let E be empty set ;
reduce f ^^ E to E;
reducibility
f ^^ E = E
proof end;
end;

registration
let p be DTree-yielding FinSequence;
let a be object ;
coherence
p . a is Relation-like
;
end;

registration
coherence
for b1 being set st b1 is Tree-like holds
b1 is FinSequence-membered
proof end;
end;

registration
let p be DTree-yielding FinSequence;
let a be object ;
cluster proj1 (p . a) -> FinSequence-membered ;
coherence
dom (p . a) is FinSequence-membered
proof end;
end;

registration
let t, t1 be Tree;
reduce t1 with-replacement ((),t) to t;
reducibility
t1 with-replacement ((),t) = t
proof end;
end;

registration
let d, d1 be DecoratedTree;
reduce d1 with-replacement ((),d) to d;
reducibility
d1 with-replacement ((),d) = d
proof end;
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
proof end;

registration
let F be Function-yielding Function;
let f be Function;
let a be object ;
cluster F +* (a,f) -> Function-yielding ;
coherence
F +* (a,f) is Function-yielding
proof end;
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))
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
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 } )
proof end;

registration
let p be DTree-yielding FinSequence;
let a be object ;
let I be set ;
cluster (p . a) " I -> FinSequence-membered ;
coherence
(p . a) " I is FinSequence-membered
proof end;
end;

theorem Th1: :: MSAFREE5:10
for I being FinSequence-membered set
for p being FinSequence holds card (p ^^ I) = card I
proof end;

registration
let I be finite FinSequence-membered set ;
let p be FinSequence;
cluster p ^^ I -> finite ;
coherence
p ^^ I is finite
proof end;
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
proof end;

registration
let i be Nat;
reduce card i to i;
reducibility
card i = i
;
let j be Nat;
identify i + j with i + j;
compatibility
i + j = i + j
proof end;
end;

scheme :: MSAFREE5:sch 1
CardUnion{ F1( object ) -> set , F2() -> FinSequence of NAT } :
card (union { F1(i) where i is Nat : i < len F2() } ) = Sum F2()
provided
A1: for i, j being Nat st i < len F2() & j < len F2() & i <> j holds
F1(i) misses F1(j) and
A2: for i being Nat st i < len F2() holds
card F1(i) = F2() . (i + 1)
proof end;

registration
let f be FinSequence;
coherence
proof end;
end;

theorem Th6: :: MSAFREE5:12
for f, g being FinSequence holds f ^^ {g} = {(f ^ g)}
proof 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 )
proof end;

theorem :: MSAFREE5:14

registration
Tree ex b1 being set st
for b2 being Tree holds b2 in b1
proof end;
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:16
for c being set holds Leaves () = {c}
proof end;

theorem :: MSAFREE5:17
for c being set
for d, d1 being DecoratedTree holds dom d c= dom ((d,c) <- d1) by TREES_4:def 7;

registration
let c be set ;
let d be DecoratedTree;
reduce ((),c) <- d to d;
reducibility
((),c) <- d = d
proof end;
end;

theorem ThL7: :: MSAFREE5:18
for c1, c2 being set
for d being DecoratedTree st c1 <> c2 holds
((),c2) <- d = root-tree c1
proof end;

registration
let f be non empty Function-yielding Function;
cluster doms f -> non empty ;
coherence
not doms f is empty
proof end;
cluster rngs f -> non empty ;
coherence
not rngs f is empty
proof end;
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
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;
attr a is s -sort means :AS: :: MSAFREE5:def 10
a in the Sorts of A . s;
end;

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

registration
let S be non empty non void ManySortedSign ;
let s be SortSymbol of S;
let A be non-empty MSAlgebra over S;
cluster s -sort for Element of Union the Sorts of A;
existence
ex b1 being Element of A st b1 is s -sort
proof end;
cluster -> s -sort for Element of the Sorts of A . s;
coherence
for b1 being Element of the Sorts of A . s holds b1 is s -sort
;
end;

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;
func the_sort_of a -> SortSymbol of S means :SORT: :: MSAFREE5:def 11
a in the Sorts of A . it;
existence
ex b1 being SortSymbol of S st a in the Sorts of A . b1
proof end;
uniqueness
for b1, b2 being SortSymbol of S st a in the Sorts of A . b1 & a in the Sorts of A . b2 holds
b1 = b2
by ;
end;

:: 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 b4 being SortSymbol of S holds
( b4 = the_sort_of a iff a in the Sorts of A . b4 );

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 b2 -sort Element of A holds the_sort_of a = s
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;

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 b2,b1 -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
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 b3,b1 -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;

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
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;
cluster -> Union the Sorts of T -valued for Element of Args (o,T);
coherence
for b1 being Element of Args (o,T) holds b1 is Union the Sorts of T -valued
proof end;
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 b4,b2 -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) = () /. 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;
func f . a -> Element of B equals :ABBR: :: MSAFREE5:def 12
(f . ()) . a;
coherence
(f . ()) . a is Element of B
proof end;
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 . ()) . 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
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
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
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)
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
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 ;
mode Homomorphism of A,B -> ManySortedFunction of A,B means :HOMO: :: MSAFREE5:def 13
it is_homomorphism A,B;
existence
ex b1 being ManySortedFunction of A,B st b1 is_homomorphism A,B
by A;
end;

:: 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 b4 being ManySortedFunction of A,B holds
( b4 is Homomorphism of A,B iff b4 is_homomorphism A,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 b2,b1 -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 )
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
proof end;
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;
reduce . (@ r) to r;
reducibility
. (@ r) = r
proof end;
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 b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for t1, t2 being Element of (Free (S,X)) st t2 = . t1 holds
. t1 = . 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;
func x -term -> Element of the Sorts of (Free (S,X)) . s equals :: MSAFREE5:def 14
root-tree [x,s];
coherence
root-tree [x,s] is Element of the Sorts of (Free (S,X)) . s
proof end;
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];

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)));
func o -term p -> Element of (Free (S,X)), equals :: MSAFREE5:def 15
[o, the carrier of S] -tree p;
coherence
[o, the carrier of S] -tree p is Element of (Free (S,X)),
proof end;
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;

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 () = 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
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 b3,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for i being object holds
( i in () . 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;
cluster x -term -> non compound ;
coherence
not x -term is compound
proof end;
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 )
proof end;
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 )
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
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
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 ;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of the carrier of S;
existence
ex b1 being Element of (Free (S,X)) st b1 is compound
proof end;
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
proof end;
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 ((),(Free (S,X)));
coherence
args e is Element of Args ((),(Free (S,X)))
proof end;
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 () = {}
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 = () -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 b3,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds x -term in 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 s be SortSymbol of S;
let x be Element of X . s;
reduce . () to x -term ;
reducibility
. () = x -term
proof end;
end;

scheme :: MSAFREE5:sch 2
TermInd{ P1[ set ], F1() -> non empty non void ManySortedSign , F2() -> V5() ManySortedSet of the carrier of F1(), F3() -> Element of (Free (F1(),F2())) } :
P1[F3()]
provided
A1: for s being SortSymbol of F1()
for x being Element of F2() . s holds P1[x -term ] and
A2: for o being OperSymbol of F1()
for p being Element of Args (o,(Free (F1(),F2()))) st ( for t being Element of (Free (F1(),F2())) st t in rng p holds
P1[t] ) holds
P1[o -term p]
proof end;

scheme :: MSAFREE5:sch 3
TermAlgebraInd{ P1[ set ], F1() -> non empty non void ManySortedSign , F2() -> V5() ManySortedSet of the carrier of F1(), F3() -> F2(),F1() -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over F1(), F4() -> Element of F3() } :
P1[F4()]
provided
A1: for s being SortSymbol of F1()
for x being Element of F2() . s
for r being Element of F3() st r = x -term holds
P1[r] and
A2: for o being OperSymbol of F1()
for p being Element of Args (o,(Free (F1(),F2())))
for r being Element of F3() st r = o -term p & ( for t being Element of F3() st t in rng p holds
P1[t] ) holds
P1[r]
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;
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}:]) is Nat
;
func height r -> Nat equals :: MSAFREE5:def 17
height (dom r);
coherence
height (dom r) is Nat
;
end;

:: 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 b2,b1 -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}:]);

:: 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 b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
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;

theorem :: MSAFREE5:43
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
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 b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
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 () = 0 by TREES_1:42;

registration
coherence
for b1 being set st b1 is natural-membered holds
( b1 is ordinal-membered & b1 is finite-membered )
proof end;
end;

registration
let I be finite natural-membered set ;
coherence
union I is natural
;
end;

registration
let I be non empty finite natural-membered set ;
identify max I with union I;
compatibility
proof end;
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 { () 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
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
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 () = 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 )
proof end;

registration
let t be DecoratedTree;
let I be set ;
coherence
proof end;
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;

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 } )
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 () & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom () & 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;
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 } is Subset of T
proof end;
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 b2,b1 -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 } ;

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;
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 ) } is Subset of T
proof end;
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 b2,b1 -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 ) } ;

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 b3,b2 -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 )
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 b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= 0 = { () where s is SortSymbol of S, x is Element of X . s : verum }
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 b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T height<= 0 = { () 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 = {} ) }
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 b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= 0 = Union ()
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 b3,b2 -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 )
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;
cluster T deg<= i -> non empty ;
coherence
not T deg<= i is empty
proof end;
cluster T height<= i -> non empty ;
coherence
not T height<= i is empty
proof end;
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 b4,b3 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st i <= j holds
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 b4,b3 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st i <= j holds
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 b3,b2 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= (i + 1) = () \/ ( { (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 () & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom () & 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 b3,b2 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T height<= (i + 1) = () \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { () where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T))
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
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 b2,b1 -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 }
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 b2,b1 -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 }
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 b2,b1 -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
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;
attr r is x -context means :CONTEXT: :: MSAFREE5:def 20
card (Coim (r,[x,s])) = 1;
attr r is x -omitting means :OMIT: :: MSAFREE5:def 21
Coim (r,[x,s]) = {} ;
end;

:: 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 b2,b1 -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 );

:: 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 b2,b1 -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]) = {} );

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;
func vf r -> set equals :: MSAFREE5:def 22
proj1 ((rng r) /\ [:(), the carrier of S:]);
coherence
proj1 ((rng r) /\ [:(), the carrier of S:]) is set
;
end;

:: 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 b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T holds vf r = proj1 ((rng r) /\ [:(), 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 b2,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T holds vf r = Union ()
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}
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 }
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;
cluster vf r -> finite ;
coherence
vf r is finite
;
end;

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 b3,b1 -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
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));
attr t is s -context means :: MSAFREE5:def 23
ex x being Element of X . s st t is x -context ;
end;

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

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;
cluster x -context -> s -context for Element of Union the Sorts of (Free (S,X));
coherence
for b1 being Element of (Free (S,X)) st b1 is x -context holds
b1 is s -context
;
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;
cluster x -term -> x -context ;
coherence
x -term is x -context
proof end;
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;
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 b1 being Element of (Free (S,X)) st
( b1 is x -context & not b1 is compound )
proof end;
cluster x -omitting -> non x -context for Element of Union the Sorts of (Free (S,X));
coherence
for b1 being Element of (Free (S,X)) st b1 is x -omitting holds
not b1 is x -context
;
end;

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 )
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;
cluster z9 -term -> z -omitting ;
coherence
z9 -term is z -omitting
proof end;
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;
existence
ex b1 being Element of (Free (S,Z)) st b1 is z -omitting
proof end;
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;
existence
ex b1 being Element of (Free (S,Z)) st
( b1 is z -omitting & b1 is z1 -context )
proof end;
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;

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

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 ;

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
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)));
attr p is x -context_including means :: MSAFREE5:def 24
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 ) );
end;

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

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;
cluster x -context_including -> non empty for Element of Args (o,(Free (S,X)));
coherence
for b1 being Element of Args (o,(Free (S,X))) st b1 is x -context_including holds
not b1 is empty
;
end;

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

definition
let S be non empty non void ManySortedSign ;
let s be SortSymbol of S;
let o be OperSymbol of S;
attr o is s -dependent means :DEP: :: MSAFREE5:def 25
s in rng ();
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 () );

registration
let S be non empty non void sufficiently_rich ManySortedSign ;
let s be SortSymbol of S;
cluster s -dependent for Element of the carrier' of S;
existence
ex b1 being OperSymbol of S st b1 is s -dependent
proof end;
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;
existence
ex b1 being Element of Args (o9,(Free (S9,X9))) st b1 is x9 -context_including
proof end;
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)));
cluster o9 -term p9 -> x9 -context ;
coherence
o9 -term p9 is x9 -context
by Th53;
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)));
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;
func x -context_pos_in p -> Nat means :CPI: :: MSAFREE5:def 26
p . it is context of x;
existence
ex b1 being Nat st p . b1 is context of x
by B;
uniqueness
for b1, b2 being Nat st p . b1 is context of x & p . b2 is context of x holds
b1 = b2
proof end;
func x -context_in p -> context of x means :CIn: :: MSAFREE5:def 27
it in rng p;
existence
ex b1 being context of x st b1 in rng p
proof end;
uniqueness
for b1, b2 being context of x st b1 in rng p & b2 in rng p holds
b1 = b2
proof end;
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 b7 being Nat holds
( b7 = x -context_pos_in p iff p . b7 is context of x );

:: 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 b7 being context of x holds
( b7 = x -context_in p iff b7 in rng p );

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 . () )
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
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
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_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 ) )
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;
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 b1 being Element of (Free (S9,X9)) st
( b1 is x9 -context & b1 is compound )
proof end;
end;

scheme :: MSAFREE5:sch 4
ContextInd{ P1[ set ], F1() -> non empty non void ManySortedSign , F2() -> SortSymbol of F1(), F3() -> V5() ManySortedSet of the carrier of F1(), F4() -> Element of F3() . F2(), F5() -> context of F4() } :
P1[F5()]
provided
A0: P1[F4() -term ] and
A1: for o being OperSymbol of F1()
for w being Element of Args (o,(Free (F1(),F3()))) st w is F4() -context_including & P1[F4() -context_in w] holds
for C being context of F4() st C = o -term w holds
P1[C]
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
proof end;

theorem aaa1: :: 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)) . ()
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 ;
func C -sub t -> Element of the Sorts of (Free (S,X)) . () equals :SUB: :: MSAFREE5:def 28
(C,[x,s]) <- t;
coherence
(C,[x,s]) <- t is Element of the Sorts of (Free (S,X)) . ()
proof end;
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;

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
() -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;
reduce C -sub () to C;
reducibility
C -sub () = C
proof end;
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 = () . () holds
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 b5 -different Element of Z . s1
for C1 being b5 -omitting context of z1 holds C1 -sub C9 is context of z
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 +* ((),(() -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;

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)
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
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 () = () . ()
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))
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 b3,b1 -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
. (C9 -sub t) = . (C9 -sub (@ ()))
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;
attr h is x -constant means :CNST: :: MSAFREE5:def 29
( h . () = 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 ) );
end;

:: 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 b2,b1 -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 & ( 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 b3,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds canonical_homomorphism T is x -constant
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;
existence
ex b1 being Homomorphism of Free (S,X),T st b1 is x -constant
proof end;
end;

definition
let x, y be object ;
func x <-> y -> Function equals :: MSAFREE5:def 30
{[x,y],[y,x]};
coherence
{[x,y],[y,x]} is Function
proof end;
commutativity
for b1 being Function
for x, y being object st b1 = {[x,y],[y,x]} holds
b1 = {[y,x],[x,y]}
;
end;

:: deftheorem defines <-> MSAFREE5:def 30 :
for x, y being object holds x <-> y = {[x,y],[y,x]};

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

registration
let A be non empty set ;
let a, b be Element of A;
cluster a <-> b -> A -defined A -valued ;
coherence
( a <-> b is A -valued & a <-> b is A -defined )
proof end;
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
proof end;
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
proof end;
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;
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 ) );
existence
ex b1 being Endomorphism of T st
( (b1 . s) . (x1 -term) = x2 -term & (b1 . 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
(b1 . s1) . () = y -term ) )
proof end;
uniqueness
for b1, b2 being Endomorphism of T st (b1 . s) . (x1 -term) = x2 -term & (b1 . 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
(b1 . s1) . () = y -term ) & (b2 . s) . (x1 -term) = x2 -term & (b2 . 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
(b2 . s1) . () = y -term ) holds
b1 = b2
proof end;
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 b2,b1 -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 b7 being Endomorphism of T holds
( b7 = Hom (T,x1,x2) iff ( (b7 . s) . (x1 -term) = x2 -term & (b7 . 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
(b7 . s1) . () = y -term ) ) );

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 b2,b1 -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 ) 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 b3,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Hom (T,x,x) = id the Sorts of T
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 b3,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds Hom (T,x1,x2) = Hom (T,x2,x1)
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 b3,b1 -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
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 b3,b1 -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
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;
reduce () . () to x -term ;
reducibility
() . () = x -term
proof end;
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 b3,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds ** (Hom ((Free (S,X)),x,x1)) = (Hom (T,x,x1)) **
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 b3,b1 -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 = (( ** (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
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
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;
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);
end;

:: 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 b2,b1 -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) );

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 b3,b1 -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
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 b3,b1 -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
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 b3,b1 -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
. 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 b4,b1 -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
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 b3,b1 -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for v being Element of (Free (S,Y))
for h2 being b4 -constant Homomorphism of Free (S,Y),Q st Q is struct-invariant & v is y -omitting holds
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 () holds ((Hom ((Free (S,X)),x1,x2)) . ()) . t = (Hom ((),x1,x2)) . t ) & (Hom ((Free (S,X)),x1,x2)) || () = Hom ((),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 . (() /. i) reduces t1,t2 holds
R . 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 . () reduces t, . 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 . reduces o -term p,(Den (o,())) . ( # 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,()) st p = q holds
R . reduces o -term p,(Den (o,())) . 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
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of the carrier of S;
existence
ex b1 being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st b1 is struct-invariant
proof end;
end;

definition
let S be non empty non void ManySortedSign ;
let s1, s2 be SortSymbol of S;
attr s2 is s1 -reachable means :REACH: :: MSAFREE5:def 33
TranslationRel S reduces s1,s2;
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 );

registration
let S be non empty non void ManySortedSign ;
let s1 be SortSymbol of S;
cluster s1 -reachable for Element of the carrier of S;
existence
ex b1 being SortSymbol of S st b1 is s1 -reachable
proof end;
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
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
proof end;
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;

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

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

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;
func transl C -> Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . ()) 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
ex b1 being Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . ()) st
for t being Element of (Free (S,X)) st the_sort_of t = s holds
b1 . t = C -sub t
proof end;
uniqueness
for b1, b2 being Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . ()) st ( for t being Element of (Free (S,X)) st the_sort_of t = s holds
b1 . t = C -sub t ) & ( for t being Element of (Free (S,X)) st the_sort_of t = s holds
b2 . t = C -sub t ) holds
b1 = b2
proof end;
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 b6 being Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . ()) holds
( b6 = transl C iff for t being Element of (Free (S,X)) st the_sort_of t = s holds
b6 . t = C -sub t );

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)
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 +* ((),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
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 & () /. 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,()) & 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 = () /. 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,()) & 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 ;
cluster Coim (t,a) -> FinSequence-membered ;
coherence
Coim (t,a) is FinSequence-membered
;
end;

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

scheme :: MSAFREE5:sch 5
LambdaTerm{ F1() -> non empty non void ManySortedSign , F2() -> V5() ManySortedSet of the carrier of F1(), F3() -> F2(),F1() -terms all_vars_including inheriting_operations MSAlgebra over F1(), F4() -> F2(),F1() -terms all_vars_including inheriting_operations MSAlgebra over F1(), F5( object ) -> Element of F4() } :
ex f being ManySortedFunction of F3(),F4() st
for t being Element of F3() holds f . t = F5(t)
provided
A0: for t being Element of F3() holds the_sort_of t = the_sort_of F5(t)
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 b2,b1 -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
( ** h = g ** & ( for t being Element of T holds g . 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 b2,b1 -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 . (h . t) = . (h . (@ ()))
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;

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;
attr V is B -sorts means :SORTS: :: MSAFREE5:def 36
( dom V = dom B & ( for i being Nat st i in dom B holds
V . i in X . (B . i) ) );
end;

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

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;
existence
ex b1 being FinSequence of Union X st b1 is B -sorts
proof end;
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;
cluster B -sorts -> non empty for FinSequence of Union X;
coherence
for b1 being FinSequence of Union X st b1 is B -sorts holds
not b1 is empty
;
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 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;

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));
attr D is B -sorts means :SORTS2: :: MSAFREE5:def 37
( 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) ) );
end;

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

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;
existence
ex b1 being FinSequence of (Free (S,X)) st b1 is B -sorts
proof end;
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;
cluster B -sorts -> non empty for FinSequence of Union the Sorts of (Free (S,X));
coherence
for b1 being FinSequence of (Free (S,X)) st b1 is B -sorts holds
not b1 is empty
;
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 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;

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));
attr F is V -context-sequence means :CONTEXTSEQ: :: MSAFREE5:def 38
( dom F = dom B & ( for i being Element of dom B holds F . i is context of V . i ) );
end;

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

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;
cluster V -context-sequence -> non empty for FinSequence of Union the Sorts of (Free (S,X));
coherence
for b1 being FinSequence of (Free (S,X)) st b1 is V -context-sequence holds
not b1 is empty
;
end;

scheme :: MSAFREE5:sch 6
FinSeqLambda{ F1() -> non empty FinSequence, F2( set ) -> object } :
ex p being non empty FinSequence st
( dom p = dom F1() & ( for i being Element of dom F1() holds p . i = F2(i) ) )
proof end;

scheme :: MSAFREE5:sch 7
FinSeqRecLambda{ F1() -> non empty FinSequence, F2() -> object , F3( object , object ) -> set } :
ex p being non empty FinSequence st
( dom p = dom F1() & p . 1 = F2() & ( for i, j being Element of dom F1() st j = i + 1 holds
p . j = F3(i,(p . i)) ) )
proof end;

scheme :: MSAFREE5:sch 8
FinSeqRec2Lambda{ F1() -> non empty FinSequence, F2() -> DecoratedTree, F3( object , DecoratedTree) -> DecoratedTree } :
ex p being non empty DTree-yielding FinSequence st
( dom p = dom F1() & p . 1 = F2() & ( for i, j being Element of dom F1() st j = i + 1 holds
for d being DecoratedTree st d = p . i holds
p . j = F3(i,d) ) )
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;
existence
ex b1 being FinSequence of (Free (S,X)) st b1 is V -context-sequence
proof end;
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;

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;
attr V2 is V1 -omitting means :OMIT2: :: MSAFREE5:def 39
rng V1 misses rng V2;
let D be B -sorts FinSequence of (Free (S,X));
let F be V2 -context-sequence FinSequence of (Free (S,X));
attr F is V1,V2,D -consequent-context-sequence means :: MSAFREE5:def 40
for i, j being Element of dom B st i + 1 = j holds
(F . j) -sub ((V1 . j) -term) = (F . i) -sub (D . i);
end;

:: 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 b3 -sorts FinSequence of Union X holds
( 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 b3 -sorts FinSequence of Union X
for D being b3 -sorts FinSequence of (Free (S,X))
for F being b5 -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) );

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;
attr V is D -omitting means :: MSAFREE5:def 41
for t being Element of (Free (S,X)) st t in rng D holds
vf t misses rng V;
end;

:: 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 b3 -sorts FinSequence of (Free (S,X))
for V being b3 -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 );

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 b3 -sorts FinSequence of (Free (S,X))
for V being b3 -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
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));
existence
ex b1 being B -sorts FinSequence of Union Y st
( b1 is one-to-one & b1 is V -omitting & b1 is D -omitting )
proof end;
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));
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 b1 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 b1 = dom f & ( for i being Nat st i in dom b1 holds
b1 . i = t . (f . i) ) )
proof end;
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 b4 being FinSequence holds
( b4 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 b4 = dom f & ( for i being Nat st i in dom b4 holds
b4 . i = t . (f . i) ) ) );

registration
let f be FinSequence;
coherence
proof end;
coherence
proof end;
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
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 b5 -sorts FinSequence of Union X
proof end;

registration
let f be non empty FinSequence;
reduce In (1,(dom f)) to 1;
reducibility
In (1,(dom f)) = 1
by ;
reduce In ((len f),(dom f)) to len f;
reducibility
In ((len f),(dom f)) = len f
by ;
end;

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

theorem Th129: :: MSAFREE5:137
for t, t1 being Tree
for xi being Element of t holds (t with-replacement (xi,t1)) | xi = t1
proof end;

theorem Th130: :: MSAFREE5:138
for t, t1 being DecoratedTree
for xi being Node of t holds (t with-replacement (xi,t1)) | xi = t1
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
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
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
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
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
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) ) )
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 ) )
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
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 b6 -sorts FinSequence of Union Y st
( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being b6 -sorts FinSequence of (Free (S,Y)) ex V2 being b6 -sorts b7 -omitting b8 -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b9 -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)))) ) ) )
proof end;