:: Term Context
:: by Grzegorz Bancerek
::
:: Received June 13, 2014
:: Copyright (c) 2014-2021 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 b₂,b₁ -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 b₁ being Element of T holds b₁ is finite

proof end;

end;

registration

cluster natural-membered -> c=-linear for set ;

coherence
for b₁ being set st b₁ is natural-membered holds
b₁ 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 b₁ being Element of I st b₁ 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 (the_arity_of o);

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 (the_arity_of o) );

:: deftheorem defines growable MSAFREE5:def 5 :
for S being non empty non void ManySortedSign holds
( S is growable iff for X being V5() ManySortedSet of the carrier of S
for n being Nat ex t being Element of (Free (S,X)) st height (dom t) = n );

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

registration

let n be Nat;

cluster non empty non void feasible V193() n -ary_oper_including for ManySortedSign ;

existence
ex b₁ being non empty non void ManySortedSign st b₁ is n -ary_oper_including

proof end;

end;

registration

cluster non empty non void feasible V193() sufficiently_rich for ManySortedSign ;

existence
ex b₁ being non empty non void ManySortedSign st b₁ 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

cluster Relation-like non-trivial -> non-empty for set ;

coherence
for b₁ being Relation st b₁ is non-trivial holds
b₁ is non-empty

proof end;

cluster Relation-like infinite-yielding -> non-trivial for set ;

coherence
for b₁ being Relation st b₁ is infinite-yielding holds
b₁ is non-trivial ;

end;

registration

let I be set ;

cluster Relation-like I -defined Function-like total infinite-yielding for set ;

existence
ex b₁ being ManySortedSet of I st b₁ is infinite-yielding

proof end;

end;

registration

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

existence
ex b₁ being FinSequence st b₁ 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 b₁ being Element of Args (o,(Free (S,X))) holds b₁ 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;

cluster p ^^ I -> FinSequence-membered ;

coherence
p ^^ I is FinSequence-membered

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 ;

cluster p . a -> Relation-like ;

coherence
p . a is Relation-like ;

end;

registration

cluster Tree-like -> FinSequence-membered for set ;

coherence
for b₁ being set st b₁ is Tree-like holds
b₁ 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 ((<*> NAT),t) to t;

reducibility
t1 with-replacement ((<*> NAT),t) = t

proof end;

end;

registration

let d, d1 be DecoratedTree;

reduce d1 with-replacement ((<*> NAT),d) to d;

reducibility
d1 with-replacement ((<*> NAT),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{ F₁( object ) -> set , F₂() -> FinSequence of NAT } :

card (union { F₁(i) where i is Nat : i < len F₂() } ) = Sum F₂()

provided

A1: for i, j being Nat st i < len F₂() & j < len F₂() & i <> j holds
F₁(i) misses F₁(j) and
A2: for i being Nat st i < len F₂() holds
card F₁(i) = F₂() . (i + 1)

proof end;

registration

let f be FinSequence;

cluster {f} -> FinSequence-membered ;

coherence
{f} is FinSequence-membered

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

Leaves (elementary_tree 0) = {{}} by TREES_1:29, HUFFMAN1:15;

registration

Tree ex b₁ being set st
for b₂ being Tree holds b₂ in b₁

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 (root-tree c) = {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 ((root-tree c),c) <- d to d;

reducibility
((root-tree c),c) <- d = d

proof end;

end;

theorem ThL7: :: MSAFREE5:18

for c1, c2 being set
for d being DecoratedTree st c1 <> c2 holds
((root-tree c1),c2) <- d = root-tree c1

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 b₁ being Element of A st b₁ is s -sort

proof end;

cluster -> s -sort for Element of the Sorts of A . s;

coherence
for b₁ being Element of the Sorts of A . s holds b₁ 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 b₁ being SortSymbol of S st a in the Sorts of A . b₁

proof end;

uniqueness
for b₁, b₂ being SortSymbol of S st a in the Sorts of A . b₁ & a in the Sorts of A . b₂ holds
b₁ = b₂ by A, XBOOLE_0:3, PROB_2:def 2;

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

theorem :: MSAFREE5:20

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for A being non-empty disjoint_valued MSAlgebra over S
for a being b₂ -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 b₂,b₁ -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 b₃,b₁ -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 b₁ being Element of Args (o,T) holds b₁ 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 b₄,b₂ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for q being Element of Args (o,T) st i in dom q holds
the_sort_of (q /. i) = (the_arity_of o) /. i

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 . (the_sort_of a)) . a;

coherence
(f . (the_sort_of a)) . 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 . (the_sort_of a)) . a;

theorem Th9: :: MSAFREE5:26

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for A being non-empty disjoint_valued MSAlgebra over S
for B being non-empty MSAlgebra over S
for f being ManySortedFunction of A,B
for a being Element of the Sorts of A . s holds f . a = (f . s) . a

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 b₁ being ManySortedFunction of A,B st b₁ 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 b₄ being ManySortedFunction of A,B holds
( b₄ is Homomorphism of A,B iff b₄ 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 b₂,b₁ -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 (canonical_homomorphism T) . (@ r) to r;

reducibility
(canonical_homomorphism T) . (@ 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 b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for t1, t2 being Element of (Free (S,X)) st t2 = (canonical_homomorphism T) . t1 holds
(canonical_homomorphism T) . t1 = (canonical_homomorphism T) . t2

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)),(the_result_sort_of o) 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)),(the_result_sort_of o)

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 (x -term) = s by SORT;

theorem Th8: :: MSAFREE5:34

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for X being V5() ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) holds the_sort_of (o -term p) = the_result_sort_of o

proof end;

theorem Th119: :: MSAFREE5:35

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for T being b₃,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for i being object holds
( i in (FreeGen T) . s iff ex x being Element of X . s st i = x -term )

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

cluster o -term p -> compound the_result_sort_of o -sort ;

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;

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

existence
ex b₁ being Element of (Free (S,X)) st b₁ 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 ((main-constr e),(Free (S,X)));
coherence
args e is Element of Args ((main-constr e),(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 (x -term) = {}

proof end;

theorem :: MSAFREE5:41

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for t being compound Element of (Free (S,X)) holds t = (main-constr t) -term (args t)

proof end;

theorem Th24: :: MSAFREE5:42

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for T being b₃,b₁ -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 (canonical_homomorphism T) . (x -term) to x -term ;

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

proof end;

end;

scheme :: MSAFREE5:sch 2
TermInd{ P₁[ set ], F₁() -> non empty non void ManySortedSign , F₂() -> V5() ManySortedSet of the carrier of F₁(), F₃() -> Element of (Free (F₁(),F₂())) } :

P₁[F₃()]

provided

A1: for s being SortSymbol of F₁()
for x being Element of F₂() . s holds P₁[x -term ] and
A2: for o being OperSymbol of F₁()
for p being Element of Args (o,(Free (F₁(),F₂()))) st ( for t being Element of (Free (F₁(),F₂())) st t in rng p holds
P₁[t] ) holds
P₁[o -term p]

proof end;

scheme :: MSAFREE5:sch 3
TermAlgebraInd{ P₁[ set ], F₁() -> non empty non void ManySortedSign , F₂() -> V5() ManySortedSet of the carrier of F₁(), F₃() -> F₂(),F₁() -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over F₁(), F₄() -> Element of F₃() } :

P₁[F₄()]

provided

A1: for s being SortSymbol of F₁()
for x being Element of F₂() . s
for r being Element of F₃() st r = x -term holds
P₁[r] and
A2: for o being OperSymbol of F₁()
for p being Element of Args (o,(Free (F₁(),F₂())))
for r being Element of F₃() st r = o -term p & ( for t being Element of F₃() st t in rng p holds
P₁[t] ) holds
P₁[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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 (x -term) = 0 by TREES_1:42;

registration

cluster natural-membered -> finite-membered ordinal-membered for set ;

coherence
for b₁ being set st b₁ is natural-membered holds
( b₁ is ordinal-membered & b₁ is finite-membered )

proof end;

end;

registration

let I be finite natural-membered set ;

cluster union I -> natural ;

coherence
union I is natural ;

end;

registration

let I be non empty finite natural-membered set ;

identify max I with union I;

compatibility
max I = union I

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 { (height t) where t is Element of (Free (S,X)) : t in rng p } is Nat )

proof end;

theorem Th26: :: MSAFREE5:47

for n being Nat
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for X being V5() ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) st the_arity_of o <> {} & n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } holds
height (o -term p) = n + 1

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 (x -term) = 0

proof end;

theorem Th22: :: MSAFREE5:50

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( deg t <> 0 iff ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st t = o -term p )

proof end;

registration

let t be DecoratedTree;
let I be set ;

cluster t " I -> FinSequence-membered ;

coherence
t " I is FinSequence-membered

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 (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) holds
deg (o -term p) = i + 1

proof end;

definition

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of the carrier of S;
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S;
let i be Nat;

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 b₂,b₁ -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 b₂,b₁ -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 b₃,b₂ -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 b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum }

proof end;

theorem Th12: :: MSAFREE5:55

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T height<= 0 = { (x -term) where s is SortSymbol of S, x is Element of X . s : verum } \/ { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ( o -term p in T & the_arity_of o = {} ) }

proof end;

theorem Th44: :: MSAFREE5:56

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= 0 = Union (FreeGen T)

proof end;

theorem Th10a: :: MSAFREE5:57

for i being Nat
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₃,b₂ -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 b₄,b₃ -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 b₄,b₃ -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 b₃,b₂ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T deg<= (i + 1) = (T deg<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : ex f being FinSequence of NAT st
( i >= Sum f & dom f = dom (the_arity_of o) & ( for i being Nat
for t being Element of (Free (S,X)) st i in dom (the_arity_of o) & t = p . i holds
f . i = deg t ) ) } /\ (Union the Sorts of T))

proof end;

theorem :: MSAFREE5:61

for i being Nat
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₃,b₂ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds T height<= (i + 1) = (T height<= 0) \/ ( { (o -term p) where o is OperSymbol of S, p is Element of Args (o,(Free (S,X))) : union { (height t) where t is Element of (Free (S,X)) : t in rng p } c= i } /\ (Union the Sorts of T))

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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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 b₂,b₁ -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) /\ [:(Union X), the carrier of S:]);

coherence
proj1 ((rng r) /\ [:(Union X), 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 b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T holds vf r = proj1 ((rng r) /\ [:(Union X), the carrier of S:]);

theorem ThR1: :: MSAFREE5:66

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T holds vf r = Union (X variables_in r)

proof end;

theorem :: MSAFREE5:67

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s holds vf (x -term) = {x}

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 b₃,b₁ -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 b₁ being Element of (Free (S,X)) st b₁ is x -context holds
b₁ 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 b₁ being Element of (Free (S,X)) st
( b₁ is x -context & not b₁ is compound )

proof end;

cluster x -omitting -> non x -context for Element of Union the Sorts of (Free (S,X));

coherence
for b₁ being Element of (Free (S,X)) st b₁ is x -omitting holds
not b₁ 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;

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

existence
ex b₁ being Element of (Free (S,Z)) st b₁ 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;

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

existence
ex b₁ being Element of (Free (S,Z)) st
( b₁ is z -omitting & b₁ 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 b₁ being Element of Args (o,(Free (S,X))) st b₁ is x -context_including holds
not b₁ 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 (the_arity_of o);

end;

:: deftheorem DEP defines -dependent MSAFREE5:def 25 :
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for o being OperSymbol of S holds
( o is s -dependent iff s in rng (the_arity_of o) );

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 b₁ being OperSymbol of S st b₁ 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;

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

existence
ex b₁ being Element of Args (o9,(Free (S9,X9))) st b₁ 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 b₁ being Nat st p . b₁ is context of x by B;
uniqueness
for b₁, b₂ being Nat st p . b₁ is context of x & p . b₂ is context of x holds
b₁ = b₂

proof end;

func x -context_in p -> context of x means :CIn: :: MSAFREE5:def 27
it in rng p;

existence
ex b₁ being context of x st b₁ in rng p

proof end;

uniqueness
for b₁, b₂ being context of x st b₁ in rng p & b₂ in rng p holds
b₁ = b₂

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 b₇ being Nat holds
( b₇ = x -context_pos_in p iff p . b₇ 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 b₇ being context of x holds
( b₇ = x -context_in p iff b₇ 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 . (x -context_pos_in p) )

proof end;

theorem Th72: :: MSAFREE5:78

for i being Nat
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for o being OperSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for p being Element of Args (o,(Free (S,X))) st p is x -context_including & x -context_pos_in p <> i & i in dom p holds
p /. i is x -omitting

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_in p) = x -context_pos_in p

proof end;

theorem :: MSAFREE5:81

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for C being context of x holds
( C = x -term or ex o being OperSymbol of S ex p being Element of Args (o,(Free (S,X))) st
( p is x -context_including & C = o -term p ) )

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 b₁ being Element of (Free (S9,X9)) st
( b₁ is x9 -context & b₁ is compound )

proof end;

end;

scheme :: MSAFREE5:sch 4
ContextInd{ P₁[ set ], F₁() -> non empty non void ManySortedSign , F₂() -> SortSymbol of F₁(), F₃() -> V5() ManySortedSet of the carrier of F₁(), F₄() -> Element of F₃() . F₂(), F₅() -> context of F₄() } :

P₁[F₅()]

provided

A0: P₁[F₄() -term ] and
A1: for o being OperSymbol of F₁()
for w being Element of Args (o,(Free (F₁(),F₃()))) st w is F₄() -context_including & P₁[F₄() -context_in w] holds
for C being context of F₄() st C = o -term w holds
P₁[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)) . (the_sort_of t)

proof end;

definition

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
let x be Element of X . s;
let C be context of x;
let t be Element of (Free (S,X));
assume A: the_sort_of t = s ;

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

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

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
(x -term) -sub t = t

proof end;

registration

let S be non empty non void ManySortedSign ;
let X be V5() ManySortedSet of the carrier of S;
let s be SortSymbol of S;
let x be Element of X . s;
let C be context of x;

reduce C -sub (x -term) to C;

reducibility
C -sub (x -term) = 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 = (the_arity_of o) . (z -context_pos_in w) holds
w +* ((z -context_pos_in w),t) in Args (o,(Free (S,Z)))

proof end;

theorem Th94: :: MSAFREE5:86

for S being non empty non void ManySortedSign
for s, s1 being SortSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z st the_sort_of C9 = s1 holds
for z1 being b₅ -different Element of Z . s1
for C1 being b₅ -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 +* ((z -context_pos_in w),((z -context_in w) -sub t)) & the_sort_of t = s holds
C9 -sub t = o -term p

proof end;

theorem :: MSAFREE5:88

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x holds the_sort_of (C -sub t) = the_sort_of C by SORT;

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 (x -context_in p) = (the_arity_of o) . (x -context_pos_in p)

proof end;

theorem Th47: :: MSAFREE5:92

for S being non empty non void ManySortedSign
for A being non-empty disjoint_valued MSAlgebra over S
for B being non-empty MSAlgebra over S
for o being OperSymbol of S
for p, q being Element of Args (o,A)
for h being ManySortedFunction of A,B
for a being Element of A
for i being Nat st i in dom p & q = p +* (i,a) holds
h # q = (h # p) +* (i,(h . a))

proof end;

theorem :: MSAFREE5:93

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for R being b₃,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for C9 being context of z
for t being Element of (Free (S,Z)) st the_sort_of t = s holds
(canonical_homomorphism R) . (C9 -sub t) = (canonical_homomorphism R) . (C9 -sub (@ ((canonical_homomorphism R) . t)))

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) = 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 b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for s being SortSymbol of S
for x being Element of X . s
for h being ManySortedFunction of (Free (S,X)),T holds
( h is x -constant iff ( h . (x -term) = x -term & ( for s1 being SortSymbol of S
for x1 being Element of X . s1 st ( x1 <> x or s <> s1 ) holds
h . (x1 -term) is x -omitting ) ) );

theorem Th51: :: MSAFREE5:94

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for T being b₃,b₁ -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;

cluster non empty Relation-like the carrier of S -defined Function-like total Function-yielding Relation-yielding x -constant for Homomorphism of Free (S,X),T;

existence
ex b₁ being Homomorphism of Free (S,X),T st b₁ 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 b₁ being Function
for x, y being object st b₁ = {[x,y],[y,x]} holds
b₁ = {[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) = y -term ) );

existence
ex b₁ being Endomorphism of T st
( (b₁ . s) . (x1 -term) = x2 -term & (b₁ . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S
for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
(b₁ . s1) . (y -term) = y -term ) )

proof end;

uniqueness
for b₁, b₂ being Endomorphism of T st (b₁ . s) . (x1 -term) = x2 -term & (b₁ . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S
for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
(b₁ . s1) . (y -term) = y -term ) & (b₂ . s) . (x1 -term) = x2 -term & (b₂ . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S
for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
(b₂ . s1) . (y -term) = y -term ) holds
b₁ = b₂

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 b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for s being SortSymbol of S
for x1, x2 being Element of X . s
for b₇ being Endomorphism of T holds
( b₇ = Hom (T,x1,x2) iff ( (b₇ . s) . (x1 -term) = x2 -term & (b₇ . s) . (x2 -term) = x1 -term & ( for s1 being SortSymbol of S
for y being Element of X . s1 st ( s1 <> s or ( y <> x1 & y <> x2 ) ) holds
(b₇ . s1) . (y -term) = 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 b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being Endomorphism of T st ( for s being SortSymbol of S
for x being Element of X . s holds (h . s) . (x -term) = x -term ) holds
h = id the Sorts of T

proof end;

theorem :: MSAFREE5:97

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for T being b₃,b₁ -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 b₃,b₁ -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 b₃,b₁ -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 b₃,b₁ -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 ((canonical_homomorphism T) . s) . (x -term) to x -term ;

reducibility
((canonical_homomorphism T) . s) . (x -term) = 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 b₃,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S holds (canonical_homomorphism T) ** (Hom ((Free (S,X)),x,x1)) = (Hom (T,x,x1)) ** (canonical_homomorphism T)

proof end;

theorem :: MSAFREE5:102

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for T being b₃,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T,s holds ((Hom (T,x1,x2)) . s) . r = (((canonical_homomorphism T) ** (Hom ((Free (S,X)),x1,x2))) . s) . r

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 b₂,b₁ -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 b₃,b₁ -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 b₃,b₁ -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 b₃,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for v being Element of (Free (S,Y)) st Q is struct-invariant & v is y -omitting holds
(canonical_homomorphism Q) . v is y -omitting

proof end;

theorem Th77: :: MSAFREE5:108

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for o being OperSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for y being Element of Y . s
for Q being b₄,b₁ -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 b₃,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for v being Element of (Free (S,Y))
for h2 being b₄ -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 (NFAlgebra R) holds ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of t)) . t = (Hom ((NFAlgebra R),x1,x2)) . t ) & (Hom ((Free (S,X)),x1,x2)) || (NForms R) = Hom ((NFAlgebra R),x1,x2) )

proof end;

theorem Th113: :: MSAFREE5:111

for i being Nat
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for X being V5() ManySortedSet of the carrier of S
for t1, t2 being Element of (Free (S,X))
for p being Element of Args (o,(Free (S,X)))
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) st i in dom p & R . ((the_arity_of o) /. i) reduces t1,t2 holds
R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . (p +* (i,t1)),(Den (o,(Free (S,X)))) . (p +* (i,t2))

proof end;

theorem Th90: :: MSAFREE5:112

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))
for t being Element of (Free (S,X)) holds R . (the_sort_of t) reduces t,(canonical_homomorphism (NFAlgebra R)) . t

proof end;

theorem Th98: :: MSAFREE5:113

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) holds R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p)

proof end;

theorem Th69: :: MSAFREE5:114

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X)))
for q being Element of Args (o,(NFAlgebra R)) st p = q holds
R . (the_result_sort_of o) reduces o -term p,(Den (o,(NFAlgebra R))) . q

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

cluster NFAlgebra R -> struct-invariant ;

coherence
NFAlgebra R is struct-invariant

proof end;

end;

registration

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

cluster non-empty disjoint_valued X,S -terms all_vars_including inheriting_operations free_in_itself non empty struct-invariant for MSAlgebra over S;

existence
ex b₁ being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S st b₁ 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 b₁ being SortSymbol of S st b₁ 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;

cluster the_sort_of C -> s -reachable ;

coherence
the_sort_of C is s -reachable

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)) . (the_sort_of C)) means :TRANS: :: MSAFREE5:def 35
for t being Element of (Free (S,X)) st the_sort_of t = s holds
it . t = C -sub t;

existence
ex b₁ being Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . (the_sort_of C)) st
for t being Element of (Free (S,X)) st the_sort_of t = s holds
b₁ . t = C -sub t

proof end;

uniqueness
for b₁, b₂ being Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . (the_sort_of C)) st ( for t being Element of (Free (S,X)) st the_sort_of t = s holds
b₁ . t = C -sub t ) & ( for t being Element of (Free (S,X)) st the_sort_of t = s holds
b₂ . t = C -sub t ) holds
b₁ = b₂

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 b₆ being Function of ( the Sorts of (Free (S,X)) . s),( the Sorts of (Free (S,X)) . (the_sort_of C)) holds
( b₆ = transl C iff for t being Element of (Free (S,X)) st the_sort_of t = s holds
b₆ . 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 +* ((z -context_pos_in k),l) holds
C9 -sub l = o -term k1

proof end;

theorem :: MSAFREE5:118

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for Z being non-trivial ManySortedSet of the carrier of S
for z being Element of Z . s
for C9 being context of z st C9 is basic holds
transl C9 is_e.translation_of Free (S,Z),s, the_sort_of C9

proof end;

theorem Th59: :: MSAFREE5:119

for m being Element of NAT
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for o being OperSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for q being Element of Args (o,(Free (S,Y)))
for V being finite set st m in dom q & (the_arity_of o) /. m = s holds
ex y being Element of Y . s ex C1 being context of y ex q1 being Element of Args (o,(Free (S,Y))) st
( y nin V & C1 = o -term q1 & q1 = q +* (m,(y -term)) & q1 is y -context_including & m = y -context_pos_in q1 & y -context_in q1 = y -term )

proof end;

theorem Th91: :: MSAFREE5:120

for m being Element of NAT
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for q being Element of Args (o,(Free (S,Y)))
for s1, s2 being SortSymbol of S
for V being finite set st m in dom q & s1 = (the_arity_of o) /. m holds
ex y being Element of Y . s1 ex C being context of y ex q1 being Element of Args (o,(Free (S,Y))) st
( y nin V & q1 = q +* (m,(y -term)) & q1 is y -context_including & y -context_in q1 = y -term & C = o -term q1 & m = y -context_pos_in q1 & transl C = transl (o,m,q,(Free (S,Y))) )

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) * (transl C)

proof end;

theorem :: MSAFREE5:125

for S being non empty non void ManySortedSign
for s1 being SortSymbol of S
for Y being infinite-yielding ManySortedSet of the carrier of S
for s2 being b₂ -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{ F₁() -> non empty non void ManySortedSign , F₂() -> V5() ManySortedSet of the carrier of F₁(), F₃() -> F₂(),F₁() -terms all_vars_including inheriting_operations MSAlgebra over F₁(), F₄() -> F₂(),F₁() -terms all_vars_including inheriting_operations MSAlgebra over F₁(), F₅( object ) -> Element of F₄() } :

ex f being ManySortedFunction of F₃(),F₄() st
for t being Element of F₃() holds f . t = F₅(t)

provided

A0: for t being Element of F₃() holds the_sort_of t = the_sort_of F₅(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 b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being Endomorphism of Free (S,X) ex g being Endomorphism of T st
( (canonical_homomorphism T) ** h = g ** (canonical_homomorphism T) & ( for t being Element of T holds g . t = (canonical_homomorphism T) . (h . (@ t)) ) )

proof end;

theorem :: MSAFREE5:127

for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for h being Endomorphism of Free (S,X)
for t being Element of (Free (S,X)) holds (canonical_homomorphism T) . (h . t) = (canonical_homomorphism T) . (h . (@ ((canonical_homomorphism T) . t)))

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;

cluster Relation-like omega -defined Union X -valued Function-like finite FinSequence-like FinSubsequence-like countable B -sorts for FinSequence of Union X;

existence
ex b₁ being FinSequence of Union X st b₁ 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 b₁ being FinSequence of Union X st b₁ is B -sorts holds
not b₁ 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;

cluster Relation-like omega -defined Union the Sorts of (Free (S,X)) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding Relation-yielding DTree-yielding countable B -sorts for FinSequence of Union the Sorts of (Free (S,X));

existence
ex b₁ being FinSequence of (Free (S,X)) st b₁ 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 b₁ being FinSequence of (Free (S,X)) st b₁ is B -sorts holds
not b₁ 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 b₃ -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 b₁ being FinSequence of (Free (S,X)) st b₁ is V -context-sequence holds
not b₁ is empty ;

end;

scheme :: MSAFREE5:sch 6
FinSeqLambda{ F₁() -> non empty FinSequence, F₂( set ) -> object } :

ex p being non empty FinSequence st
( dom p = dom F₁() & ( for i being Element of dom F₁() holds p . i = F₂(i) ) )

proof end;

scheme :: MSAFREE5:sch 7
FinSeqRecLambda{ F₁() -> non empty FinSequence, F₂() -> object , F₃( object , object ) -> set } :

ex p being non empty FinSequence st
( dom p = dom F₁() & p . 1 = F₂() & ( for i, j being Element of dom F₁() st j = i + 1 holds
p . j = F₃(i,(p . i)) ) )

proof end;

scheme :: MSAFREE5:sch 8
FinSeqRec2Lambda{ F₁() -> non empty FinSequence, F₂() -> DecoratedTree, F₃( object , DecoratedTree) -> DecoratedTree } :

ex p being non empty DTree-yielding FinSequence st
( dom p = dom F₁() & p . 1 = F₂() & ( for i, j being Element of dom F₁() st j = i + 1 holds
for d being DecoratedTree st d = p . i holds
p . j = F₃(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;

cluster Relation-like omega -defined Union the Sorts of (Free (S,X)) -valued Function-like finite FinSequence-like FinSubsequence-like Function-yielding Relation-yielding DTree-yielding countable V -context-sequence for FinSequence of Union the Sorts of (Free (S,X));

existence
ex b₁ being FinSequence of (Free (S,X)) st b₁ 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 b₃ -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 b₃ -sorts FinSequence of Union X
for D being b₃ -sorts FinSequence of (Free (S,X))
for F being b₅ -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 b₃ -sorts FinSequence of (Free (S,X))
for V being b₃ -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 b₃ -sorts FinSequence of (Free (S,X))
for V being b₃ -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));

cluster non empty Relation-like omega -defined Union Y -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like countable B -sorts V -omitting D -omitting for FinSequence of Union Y;

existence
ex b₁ being B -sorts FinSequence of Union Y st
( b₁ is one-to-one & b₁ is V -omitting & b₁ 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 b₁ being FinSequence ex f being one-to-one FinSequence st
( rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & dom b₁ = dom f & ( for i being Nat st i in dom b₁ holds
b₁ . 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 b₄ being FinSequence holds
( b₄ is vf-sequence of t iff ex f being one-to-one FinSequence st
( rng f = { xi where xi is Element of dom t : ex s being SortSymbol of S ex x being Element of X . s st t . xi = [x,s] } & dom b₄ = dom f & ( for i being Nat st i in dom b₄ holds
b₄ . i = t . (f . i) ) ) );

registration

let f be FinSequence;

cluster pr1 f -> FinSequence-like ;

coherence
pr1 f is FinSequence-like

proof end;

cluster pr2 f -> FinSequence-like ;

coherence
pr2 f is FinSequence-like

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 b₅ -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 FINSEQ_5:6, SUBSET_1:def 8;

reduce In ((len f),(dom f)) to len f;

reducibility
In ((len f),(dom f)) = len f by SUBSET_1:def 8, FINSEQ_5:6;

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)),(the_sort_of t)

proof end;

theorem Th118: :: MSAFREE5:132

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t being Element of (Free (S,X))
for C being context of x st X is non-trivial holds
for xi being Element of dom C st C . xi = [x,s] & the_sort_of t = s holds
C -sub t = C with-replacement (xi,t)

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,(x -term)) & t is x -omitting holds
t1 is context of x

proof end;

theorem Lem11: :: MSAFREE5:135

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t, t1 being Element of (Free (S,X))
for xi being Element of dom t st t . xi = [x,s] holds
dom t c= dom (t with-replacement (xi,t1))

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 b₆ -sorts FinSequence of Union Y st
( dom B = dom f & B = pr2 f & V1 = pr1 f & ex D being b₆ -sorts FinSequence of (Free (S,Y)) ex V2 being b₆ -sorts b₇ -omitting b₈ -omitting FinSequence of Union Y st
( ( for i being Element of dom B holds D . i = h . ((V1 . i) -term) ) & ex F being b₉ -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;