:: Term Context
:: by Grzegorz Bancerek
::
:: Received June 13, 2014
:: Copyright (c) 2014-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, STRUCT_0, RELAT_1, FUNCT_1, PBOOLE, MSUALG_1, MSAFREE4,
MSAFREE, CIRCUIT2, REWRITE1, MSUALG_4, ZF_MODEL, MSUALG_6, SUBSET_1,
NAT_1, FUNCOP_1, MARGREL1, PARTFUN1, FUNCT_4, MOD_4, FINSEQ_1, FUNCT_7,
ARYTM_3, XXREAL_0, RLTOPSP1, NUMBERS, CARD_1, TARSKI, TREES_4, MSATERM,
CARD_3, HURWITZ, MSAFREE5, ZFMISC_1, FINSET_1, QC_LANG1, GLIB_000,
PROB_2, FINSEQ_4, TREES_2, ABCMIZ_A, ABCMIZ_1, PRE_POLY, FINSEQ_2,
TREES_3, AOFA_000, ORDINAL1, TREES_1, MEMBERED, MEMBER_1, FUNCT_6, CAT_1,
REALSET1, AOFA_A01, VALUED_2, MSUALG_2, MCART_1, ORDINAL4, MSUALG_3,
MATRIX_7, CARD_2, MATROID0, ORDINAL6, GROUP_6, TREES_A, AOFA_A00,
ZF_LANG1, FACIRC_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, DOMAIN_1, FINSET_1,
RELAT_1, RELSET_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, FUNCOP_1,
ORDINAL1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_7, FUNCT_4, MCART_1,
CARD_2, TREES_1, TREES_2, FUNCT_6, TREES_3, TREES_4, CARD_3, MATRIX_7,
XXREAL_0, XXREAL_2, XCMPLX_0, NUMBERS, WSIERP_1, MEMBERED, ORDINAL6,
REWRITE1, PBOOLE, MSUALG_1, MSUALG_2, MSUALG_3, MSUALG_4, MSUALG_6,
MSAFREE, MSAFREE1, MSATERM, CATALG_1, ABCMIZ_1, ABCMIZ_A, AOFA_A00,
AOFA_A01, MSAFREE3, CARD_1, MSAFREE4;
constructors RELSET_1, FINSEQ_4, DOMAIN_1, CARD_2, WSIERP_1, MSAFREE1,
AOFA_A01, CATALG_1, ABCMIZ_A, ORDINAL6, RECDEF_1, XFAMILY, SEQ_4,
MSUALG_3;
registrations RELSET_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, XCMPLX_0, SUBSET_1,
CARD_1, XXREAL_0, RELAT_1, FUNCT_1, FUNCT_7, PBOOLE, STRUCT_0, MSUALG_1,
MSUALG_3, MSUALG_9, INSTALG1, CATALG_1, XBOOLE_0, MSAFREE, MSAFREE1,
MSAFREE3, MSAFREE4, ZFMISC_1, FINSET_1, TREES_2, TREES_3, CARD_3,
XXREAL_2, MEMBERED, XTUPLE_0, FOMODEL0, RAMSEY_1, REWRITE1, INT_1,
ABCMIZ_1, MSUALG_2, ALGSPEC1, VALUED_0, NAT_1, ORDINAL6, FINSEQ_6;
requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;
begin :: Preliminary
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;
reserve
a,b for object, I,J for set, f for Function, R for Relation,
i,j,n for Nat, m for (Element of NAT),
S for non empty non void ManySortedSign,
s,s1,s2 for SortSymbol of S,
o for OperSymbol of S,
X for non-empty ManySortedSet of the carrier of S,
x,x1,x2 for (Element of X.s), x11 for (Element of X.s1),
T for all_vars_including inheriting_operations free_in_itself
(X,S)-terms MSAlgebra over S,
g for Translation of Free(S,X),s1,s2,
h for Endomorphism of Free(S,X);
definition
let S,X; let T be all_vars_including (X,S)-terms MSAlgebra over S;
let r be Element of T;
func @r -> Element of Free(S,X) equals
:: MSAFREE5:def 1
r;
end;
registration
let S,X,T;
cluster -> finite for Element of T;
end;
registration
cluster natural-membered -> c=-linear for set;
end;
reserve
r,r1,r2 for (Element of T),
t,t1,t2 for (Element of Free(S,X));
definition
let S;
let A be MSAlgebra over S;
let a;
pred a in A means
:: MSAFREE5:def 2
a in Union the Sorts of A;
end;
definition
let a,b;
attr b is a-different means
:: MSAFREE5:def 3
b <> a;
end;
registration
let I be non trivial set;
let a;
cluster a-different for Element of I;
end;
theorem :: MSAFREE5:1
for t,t1 being Tree, 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;
registration
let R be finite Relation;
let a;
cluster Coim(R,a) -> finite;
end;
theorem :: MSAFREE5:2
for p,q,r being FinSequence st p^q is_a_prefix_of r holds p is_a_prefix_of r;
theorem :: MSAFREE5:3
for p,q,r being FinSequence st p^q is_a_prefix_of p^r holds
q is_a_prefix_of r;
theorem :: MSAFREE5:4
for p,q being FinSequence st i <= len p holds (p^q)|Seg i = p|Seg i;
theorem :: MSAFREE5:5
for p,q,r being FinSequence st q is_a_prefix_of p^r holds
q is_a_prefix_of p or p is_a_prefix_of q;
definition
let S;
attr S is sufficiently_rich means
:: MSAFREE5:def 4
for s ex o st s in rng the_arity_of o;
attr S is growable means
:: MSAFREE5:def 5
for X,n ex t st height dom t = n;
end;
definition
let n,S;
attr S is n-ary_oper_including means
:: MSAFREE5:def 6
ex o st len the_arity_of o = n;
end;
registration
let n;
cluster n-ary_oper_including for non empty non void ManySortedSign;
end;
registration
cluster sufficiently_rich for non empty non void ManySortedSign;
end;
definition
let R;
attr R is non-trivial means
:: MSAFREE5:def 7
I in rng R implies I is non trivial;
attr R is infinite-yielding means
:: MSAFREE5:def 8
I in rng R implies I is infinite;
end;
registration
cluster non-trivial -> non-empty for Relation;
cluster infinite-yielding -> non-trivial for Relation;
end;
registration
let I be set;
cluster infinite-yielding for ManySortedSet of I;
end;
registration
cluster infinite-yielding for FinSequence;
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;
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;
end;
registration
let S,X,o;
cluster -> DTree-yielding for Element of Args(o,Free(S,X));
end;
reserve
Y for infinite-yielding ManySortedSet of the carrier of S,
y,y1 for (Element of Y.s), y11 for (Element of Y.s1),
Q for all_vars_including inheriting_operations free_in_itself
(Y,S)-terms MSAlgebra over S,
q,q1 for (Element of Args(o,Free(S,Y))),
u,u1,u2 for (Element of Q),
v,v1,v2 for (Element of Free(S,Y)),
Z for non-trivial ManySortedSet of the carrier of S,
z,z1 for (Element of Z.s),
l,l1 for (Element of Free(S,Z)),
R for all_vars_including inheriting_operations free_in_itself
(Z,S)-terms MSAlgebra over S,
k,k1 for Element of Args(o,Free(S,Z));
registration
let p be FinSequence;
reduce p ^ {} to p;
reduce {} ^ p to p;
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};
end;
registration
let I be FinSequence-membered set;
let p be FinSequence;
cluster p^^I -> FinSequence-membered;
end;
registration
let f be FinSequence, E be empty set;
reduce f^^E to E;
end;
registration
let p be DTree-yielding FinSequence;
let a;
cluster p.a -> Relation-like;
end;
registration
cluster Tree-like -> FinSequence-membered for set;
end;
registration
let p be DTree-yielding FinSequence;
let a;
cluster dom (p.a) -> FinSequence-membered;
end;
registration
let t,t1 be Tree;
reduce t1 with-replacement(<*>NAT, t) to t;
end;
registration
let d,d1 be DecoratedTree;
reduce d1 with-replacement(<*>NAT, d) to d;
end;
theorem :: MSAFREE5:6
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;
registration
let F be Function-yielding Function;
let f be Function;
let a;
cluster F+*(a,f) -> Function-yielding;
end;
theorem :: MSAFREE5:7
for F being Function-yielding Function, f being Function holds
doms(F+*(a,f)) = (doms F)+*(a, dom f);
theorem :: MSAFREE5:8
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;
theorem :: MSAFREE5:9
for a being set, w being DTree-yielding FinSequence holds
dom (a-tree w) = {{}} \/ union {<*i*>^^dom (w.(i+1)): i < len w};
registration
let p be DTree-yielding FinSequence;
let a,I;
cluster (p.a)"I -> FinSequence-membered;
end;
theorem :: MSAFREE5:10
for I being FinSequence-membered set, p being FinSequence holds
card (p^^I) = card I;
registration
let I be finite FinSequence-membered set;
let p be FinSequence;
cluster p^^I -> finite;
end;
theorem :: MSAFREE5:11
for I,J being FinSequence-membered set, p,q being FinSequence
st len p = len q & p <> q holds p^^I misses q^^J;
registration
let i;
reduce card i to i;
let j;
identify i +` j with i+j;
end;
scheme :: MSAFREE5:sch 1
CardUnion {I(object) -> set, f() -> FinSequence of NAT}:
card union {I(i): i < len f()} = Sum f()
provided
for i,j st i < len f() & j < len f() & i <> j holds I(i) misses I(j) and
for i st i < len f() holds card I(i) = f().(i+1);
registration
let f be FinSequence;
cluster {f} -> FinSequence-membered;
end;
theorem :: MSAFREE5:12
for f,g being FinSequence holds f^^{g} = {f^g};
theorem :: MSAFREE5:13
for I,J being FinSequence-membered set
for f being FinSequence holds I c= J iff f^^I c= f^^J;
reserve c,c1,c2 for set, d,d1 for DecoratedTree;
theorem :: MSAFREE5:14
Leaves elementary_tree 0 = {{}};
registration
sethood of Tree;
end;
theorem :: MSAFREE5:15
for p being non empty Tree-yielding FinSequence holds
Leaves tree p = {<*i*>^q where i where q is FinSequence of NAT,
d is Tree: q in Leaves d & i+1 in dom p & d = p.(i+1)};
theorem :: MSAFREE5:16
Leaves root-tree c = {c};
theorem :: MSAFREE5:17
dom d c= dom((d,c)<-d1);
registration
let c,d;
reduce (root-tree c,c)<-d to d;
end;
theorem :: MSAFREE5:18
c1 <> c2 implies (root-tree c1,c2)<-d = root-tree c1;
registration
let f be non empty Function-yielding Function;
cluster doms f -> non empty;
cluster rngs f -> non empty;
end;
theorem :: MSAFREE5:19
for p,q being non empty DTree-yielding FinSequence st
dom q = dom p & (for i,d1 st i in dom p & d1 = p.i holds q.i = (d1,c)<-d)
holds (b-tree p,c)<-d = b-tree q;
definition
let S,s;
let A be non empty MSAlgebra over S;
let a be Element of A;
attr a is s-sort means
:: MSAFREE5:def 10
a in (the Sorts of A).s;
end;
registration
let S,s;
let A be non-empty MSAlgebra over S;
cluster s-sort for Element of A;
cluster -> s-sort for Element of (the Sorts of A).s;
end;
definition
let S;
let A be non empty MSAlgebra over S such that
A is disjoint_valued;
let a be Element of A;
func the_sort_of a -> SortSymbol of S means
:: MSAFREE5:def 11
a in (the Sorts of A).it;
end;
theorem :: MSAFREE5:20
for A being disjoint_valued non-empty MSAlgebra over S
for a being s-sort Element of A
holds the_sort_of a = s;
theorem :: MSAFREE5:21
for A being disjoint_valued non empty MSAlgebra over S
for a being Element of A
holds a is (the_sort_of a)-sort;
theorem :: MSAFREE5:22
the_sort_of @r = the_sort_of r;
theorem :: MSAFREE5:23
for r being Element of (the Sorts of T).s holds the_sort_of r = s;
theorem :: MSAFREE5:24
for u being Term of S,X st t = u holds the_sort_of t = the_sort_of u;
registration
let S,X,o,T;
cluster -> (Union the Sorts of T)-valued for Element of Args(o,T);
end;
theorem :: MSAFREE5:25
for q being Element of Args(o,T) holds
i in dom q implies the_sort_of (q/.i) = (the_arity_of o)/.i;
definition
let S;
let A,B be non-empty MSAlgebra over S;
let f be ManySortedFunction of A,B such that
A is disjoint_valued;
let a be Element of A;
func f.a -> Element of B equals
:: MSAFREE5:def 12
f.(the_sort_of a).a;
end;
theorem :: MSAFREE5:26
for A being disjoint_valued non-empty 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;
theorem :: MSAFREE5:27
for A being disjoint_valued non-empty 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;
theorem :: MSAFREE5:28
for A,B being disjoint_valued non-empty 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;
theorem :: MSAFREE5:29
for A,B being disjoint_valued non-empty 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);
theorem :: MSAFREE5:30
for A being disjoint_valued non-empty 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;
definition
let S;
let A,B be MSAlgebra over S such that
ex h being ManySortedFunction of A,B st h is_homomorphism A,B;
mode Homomorphism of A,B -> ManySortedFunction of A,B means
:: MSAFREE5:def 13
it is_homomorphism A,B;
end;
theorem :: MSAFREE5:31
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;
definition
let S,X,T;
redefine func canonical_homomorphism T -> Homomorphism of Free(S,X), T;
end;
registration
let S,X,T,r;
reduce (canonical_homomorphism T).@r to r;
end;
theorem :: MSAFREE5:32
for t1,t2 st t2 = (canonical_homomorphism T).t1 holds
(canonical_homomorphism T).t1 = (canonical_homomorphism T).t2;
begin :: Constructing terms
reserve
w for (Element of Args(o,T)),
p,p1 for Element of Args(o,Free(S,X));
definition
let S,X,s,x;
func x-term -> Element of (the Sorts of Free(S,X)).s equals
:: MSAFREE5:def 14
root-tree [x,s];
end;
definition
let S,X,o,p;
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;
end;
theorem :: MSAFREE5:33
the_sort_of (x-term) = s;
theorem :: MSAFREE5:34
the_sort_of (o-term p) = the_result_sort_of o;
theorem :: MSAFREE5:35
for i being object holds i in (FreeGen T).s iff ex x st i = x-term;
registration
let S,X,s,x;
cluster x-term -> non compound;
end;
registration
let S,X,o,p;
cluster o-term p -> compound (the_result_sort_of o)-sort;
end;
theorem :: MSAFREE5:36
(ex s,x st t = x-term) or ex o,p st t = o-term p;
theorem :: MSAFREE5:37
t is not compound implies ex s,x st t = x-term;
theorem :: MSAFREE5:38
t is compound implies ex o,p st t = o-term p;
theorem :: MSAFREE5:39
x-term <> o-term p;
registration
let S;
let X be non-empty ManySortedSet of the carrier of S;
cluster compound for Element of Free(S,X);
end;
definition
let S,X;
let e be compound Element of Free(S,X);
redefine func main-constr e -> OperSymbol of S;
end;
definition
let S,X;
let e be compound Element of Free(S,X);
redefine func args e -> Element of Args(main-constr e, Free(S, X));
end;
theorem :: MSAFREE5:40
args (x-term) = {};
theorem :: MSAFREE5:41
for t being compound Element of Free(S,X) holds
t = (main-constr t)-term args t;
theorem :: MSAFREE5:42
x-term in T;
registration
let S,X,T,s,x;
reduce (canonical_homomorphism T).(x-term) to x-term;
end;
scheme :: MSAFREE5:sch 2
TermInd{P[set], S() -> non empty non void ManySortedSign,
X() -> non-empty ManySortedSet of the carrier of S(),
t() -> Element of Free(S(),X())}:
P[t()]
provided
for s being SortSymbol of S(), x being Element of X().s holds P[x-term] and
for o being OperSymbol of S(), p being Element of Args(o,Free(S(),X())) st
for t being Element of Free(S(),X()) st t in rng p holds P[t]
holds P[o-term p];
scheme :: MSAFREE5:sch 3
TermAlgebraInd{P[set], S() -> non empty non void ManySortedSign,
X() -> non-empty ManySortedSet of the carrier of S(),
A() -> all_vars_including inheriting_operations free_in_itself
(X(),S())-terms MSAlgebra over S(),
t() -> Element of A()}:
P[t()]
provided
for s being SortSymbol of S(), x being Element of X().s
for r being Element of A() st r = x-term holds P[r] and
for o being OperSymbol of S(), p being Element of Args(o,Free(S(),X()))
for r being Element of A() st r = o-term p &
for t being Element of A() st t in rng p holds P[t]
holds P[r];
begin :: Construction Degree
definition
let S,X,T,r;
func construction_degree r -> Nat equals
:: MSAFREE5:def 16
card (r"[:the carrier' of S, {the carrier of S}:]);
func height r -> Nat equals
:: MSAFREE5:def 17
height dom r;
end;
notation
let S,X,T,r;
synonym deg r for construction_degree r;
end;
theorem :: MSAFREE5:43
deg @r = deg r;
theorem :: MSAFREE5:44
height @r = height r;
theorem :: MSAFREE5:45
height (x-term) = 0;
registration
cluster natural-membered -> ordinal-membered finite-membered for set;
end;
registration
let I be finite natural-membered set;
cluster union I -> natural;
end;
registration
let I be non empty finite natural-membered set;
identify max I with union I;
end;
theorem :: MSAFREE5:46
for S,X,o,p holds {height t1: t1 in rng p} is natural-membered finite &
union {height t: t in rng p} is Nat;
theorem :: MSAFREE5:47
the_arity_of o <> {} & n = union {height t1: t1 in rng p}
implies height (o-term p) = n+1;
theorem :: MSAFREE5:48
the_arity_of o = {} implies height (o-term p) = 0;
theorem :: MSAFREE5:49
deg (x-term) = 0;
theorem :: MSAFREE5:50
deg t <> 0 iff ex o,p st t = o-term p;
registration
let t be DecoratedTree;
let I;
cluster t"I -> FinSequence-membered;
end;
definition
let a,I;
let J,K be set;
redefine func IFIN(a,I,J,K) -> set;
end;
theorem :: MSAFREE5:51
J = [o,the carrier of S] implies (o-term p)"I = IFIN(J,I,{{}},{}) \/
union {<*i*>^^((p.(i+1))"I): i < len p};
theorem :: MSAFREE5:52
(ex f being FinSequence of NAT st i = Sum f & dom f = dom the_arity_of o &
for i,t st i in dom the_arity_of o & t = p.i holds f.i = deg t)
implies deg (o-term p) = i+1;
definition
let S,X,T,i;
func T deg<= i -> Subset of T equals
:: MSAFREE5:def 18
{r: deg r <= i};
end;
definition
let S,X,T,i;
func T height<= i -> Subset of T equals
:: MSAFREE5:def 19
{t: t in T & height t <= i};
end;
theorem :: MSAFREE5:53
r in T deg<= i iff deg r <= i;
theorem :: MSAFREE5:54
T deg<= 0 = the set of all x-term;
theorem :: MSAFREE5:55
T height<= 0 = (the set of all x-term) \/
{o-term p: o-term p in T & the_arity_of o = {}};
theorem :: MSAFREE5:56
T deg<= 0 = Union FreeGen T;
theorem :: MSAFREE5:57
r in T height<= i iff height r <= i;
registration
let S,X,T,i;
cluster T deg<= i -> non empty;
cluster T height<= i -> non empty;
end;
theorem :: MSAFREE5:58
i <= j implies T deg<= i c= T deg<= j;
theorem :: MSAFREE5:59
i <= j implies T height<= i c= T height<= j;
theorem :: MSAFREE5:60
T deg<= (i+1) = T deg<= 0 \/ {o-term p:
ex f being FinSequence of NAT st i >= Sum f & dom f = dom the_arity_of o &
for i,t st i in dom the_arity_of o & t = p.i holds f.i = deg t}
/\ Union the Sorts of T;
theorem :: MSAFREE5:61
T height<= (i+1) = T height<= 0 \/ {o-term p:
union {height t: t in rng p} c= i}
/\ Union the Sorts of T;
theorem :: MSAFREE5:62
deg t >= height t;
theorem :: MSAFREE5:63
Union the Sorts of T = union {T deg<= i: not contradiction};
theorem :: MSAFREE5:64
Union the Sorts of T = union {T height<= i: not contradiction};
theorem :: MSAFREE5:65
for i holds T deg<= i c= Free(S,X) deg<= i;
begin :: Context
definition
let S,X,T,s,x,r;
attr r is x-context means
:: MSAFREE5:def 20
card Coim(r,[x,s]) = 1;
attr r is x-omitting means
:: MSAFREE5:def 21
Coim(r,[x,s]) = {};
end;
definition
let S,X,T,r;
func vf r -> set equals
:: MSAFREE5:def 22
proj1(rng r /\ [:Union X,the carrier of S:]);
end;
theorem :: MSAFREE5:66
vf r = Union (X variables_in r);
theorem :: MSAFREE5:67
vf (x-term) = {x};
theorem :: MSAFREE5:68
vf (o-term p) = union {vf t: t in rng p};
registration
let S,X,T,r;
cluster vf r -> finite;
end;
theorem :: MSAFREE5:69
x nin vf r implies r is x-omitting;
definition
let S,X,s,t;
attr t is s-context means
:: MSAFREE5:def 23
ex x st t is x-context;
end;
registration
let S,X,s,x;
cluster x-context -> s-context for Element of Free(S,X);
end;
registration
let S,X,s,x;
cluster x-term -> x-context;
end;
registration
let S,X,s,x;
cluster x-context non compound for Element of Free(S,X);
cluster x-omitting -> non x-context for Element of Free(S,X);
end;
theorem :: MSAFREE5:70
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;
registration
let S,s,s1,Z,z;
let z9 be z-different Element of Z.s1;
cluster z9-term -> z-omitting;
end;
registration
let S,s,Z,z;
cluster z-omitting for Element of Free(S,Z);
end;
registration
let S,s,s1,Z,z;
let z1 be z-different Element of Z.s1;
cluster z-omitting z1-context for Element of Free(S,Z);
end;
definition
let S,X,s,x;
mode context of x is x-context Element of Free(S,X);
end;
theorem :: MSAFREE5:71
for r being SortSymbol of S, y being Element of X.r holds
x-term is context of y iff r = s & x = y;
definition
let S,X,s;
mode context of s,X is s-context Element of Free(S,X);
end;
reserve C for (context of x), C1 for (context of y), C9 for (context of z),
C11 for (context of x11), C12 for (context of y11), D for context of s,X;
theorem :: MSAFREE5:72
C is context of s,X;
theorem :: MSAFREE5:73
x in vf C;
definition
let S,o,s,X,x,p;
attr p is x-context_including means
:: MSAFREE5:def 24
ex i st i in dom p & p.i is context of x &
for j,t st j in dom p & j <> i & t = p.j
holds t is x-omitting;
end;
registration
let S,o,s,X,x;
cluster x-context_including -> non empty for Element of Args(o,Free(S,X));
end;
theorem :: MSAFREE5:74
p is x-context_including iff o-term p is context of x;
theorem :: MSAFREE5:75
(for i st i in dom p holds p/.i is x-omitting) iff o-term p is x-omitting;
theorem :: MSAFREE5:76
(for t st t in rng p holds t is x-omitting) iff o-term p is x-omitting;
definition
let S,s,o;
attr o is s-dependent means
:: MSAFREE5:def 25
s in rng the_arity_of o;
end;
registration
let S be sufficiently_rich non void non empty ManySortedSign;
let s be SortSymbol of S;
cluster s-dependent for OperSymbol of S;
end;
reserve
S9 for sufficiently_rich non empty non void ManySortedSign,
s9 for SortSymbol of S9,
o9 for s9-dependent OperSymbol of S9,
X9 for non-trivial ManySortedSet of the carrier of S9,
x9 for (Element of X9.s9);
registration
let S9,s9,o9,X9,x9;
cluster x9-context_including for Element of Args(o9,Free(S9,X9));
end;
registration
let S9,X9,s9,x9,o9;
let p9 be x9-context_including Element of Args(o9,Free(S9,X9));
cluster o9-term p9 -> x9-context;
end;
definition
let S,o,s,X,x,p such that
p is x-context_including;
func x-context_pos_in p -> Nat means
:: MSAFREE5:def 26
p.it is context of x;
func x-context_in p -> context of x means
:: MSAFREE5:def 27
it in rng p;
end;
theorem :: MSAFREE5:77
p is x-context_including implies x-context_pos_in p in dom p &
x-context_in p = p.(x-context_pos_in p);
theorem :: MSAFREE5:78
p is x-context_including & x-context_pos_in p <> i in dom p implies
p/.i is x-omitting;
theorem :: MSAFREE5:79
p is x-context_including implies p just_once_values x-context_in p;
theorem :: MSAFREE5:80
p is x-context_including implies p<-(x-context_in p) = x-context_pos_in p;
theorem :: MSAFREE5:81
C = x-term or
ex o,p st p is x-context_including & C = o-term p;
registration
let S9,X9,s9,x9;
cluster x9-context compound for Element of Free(S9,X9);
end;
scheme :: MSAFREE5:sch 4
ContextInd{P[set],
S() -> non empty non void ManySortedSign,
s() -> SortSymbol of S(),
X() -> non-empty ManySortedSet of the carrier of S(),
x() -> (Element of X().s()),
C() -> context of x()}:
P[C()]
provided
P[x()-term] and
for o being OperSymbol of S()
for w being Element of Args(o, Free(S(),X()))
st w is x()-context_including
holds P[x()-context_in w] implies
for C being context of x() st C = o-term w holds P[C];
theorem :: MSAFREE5:82
t is x-omitting implies (t,[x,s])<-t1 = t;
theorem :: MSAFREE5:83
the_sort_of t1 = s implies
(t,[x,s])<-t1 in (the Sorts of Free(S,X)).the_sort_of t;
definition
let S,X,s,x,C,t such that
the_sort_of t = s;
func C-sub(t) -> Element of (the Sorts of Free(S,X)).the_sort_of C equals
:: MSAFREE5:def 28
(C,[x,s])<-t;
end;
theorem :: MSAFREE5:84
the_sort_of t = s implies (x-term)-sub(t) = t;
registration
let S,X,s,x,C;
reduce C-sub(x-term) to C;
end;
theorem :: MSAFREE5:85
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));
theorem :: MSAFREE5:86
the_sort_of C9 = s1 implies
for z1 being z-different Element of Z.s1
for C1 being z-omitting context of z1 holds C1-sub(C9) is context of z;
theorem :: MSAFREE5:87
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;
theorem :: MSAFREE5:88
the_sort_of (C-sub t) = the_sort_of C;
theorem :: MSAFREE5:89
t.a = [x,s] implies a in Leaves dom t;
theorem :: MSAFREE5:90
for s0 being SortSymbol of S, x0 being Element of X.s0 holds
the_sort_of t = s & C is x0-omitting & t is x0-omitting implies
C-sub t is x0-omitting;
theorem :: MSAFREE5:91
p is x-context_including implies
the_sort_of (x-context_in p) = (the_arity_of o).(x-context_pos_in p);
theorem :: MSAFREE5:92
for A being disjoint_valued non-empty MSAlgebra over S
for B being non-empty MSAlgebra over S
for o being OperSymbol of S, p,q being Element of Args(o,A)
for h being ManySortedFunction of A,B, a being Element of A
for i st i in dom p & q = p+*(i,a) holds h#q = (h#p)+*(i,h.a);
theorem :: MSAFREE5:93
for t being Element of Free(S,Z) holds
the_sort_of t = s implies
(canonical_homomorphism R).(C9-sub(t))
= (canonical_homomorphism R).(C9-sub @((canonical_homomorphism R).t));
definition
let S,X,T,s,x;
let h be ManySortedFunction of Free(S,X), T;
attr h is x-constant means
:: MSAFREE5:def 29
h.(x-term) = x-term &
for s1 for x1 being Element of X.s1 st x1 <> x or s <> s1
holds h.(x1-term) is x-omitting;
end;
theorem :: MSAFREE5:94
canonical_homomorphism T is x-constant;
registration
let S,X,T,s,x;
cluster x-constant for Homomorphism of Free(S,X), T;
end;
reserve h1 for x-constant Homomorphism of Free(S,X), T,
h2 for y-constant Homomorphism of Free(S,Y), Q;
definition
let x,y be object;
func x<->y -> Function equals
:: MSAFREE5:def 30
{[x,y],[y,x]};
commutativity;
end;
theorem :: MSAFREE5:95
dom (a<->b) = {a,b} & (a<->b).a = b & (a<->b).b = a & rng (a<->b) = {a,b};
registration
let A be non empty set;
let a,b be Element of A;
cluster a<->b -> A-valued A-defined;
end;
definition
let A be set, B be non empty set;
let f be Function of A,B;
let g be A-defined B-valued Function;
redefine func f+*g -> Function of A,B;
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;
redefine func f+*(x,g) -> ManySortedFunction of A,B;
end;
definition
let S,X, T;
let s,x1,x2;
func Hom(T,x1,x2) -> Endomorphism of T means
:: MSAFREE5:def 31
it.s.(x1-term) = x2-term & it.s.(x2-term) = x1-term &
for s1 for y being Element of X.s1 st s1 <> s or y <> x1 & y <> x2
holds it.s1.(y-term) = y-term;
end;
theorem :: MSAFREE5:96
for h being Endomorphism of T st
(for s,x holds h.s.(x-term) = x-term) holds h = id the Sorts of T;
theorem :: MSAFREE5:97
Hom(T,x,x) = id the Sorts of T;
theorem :: MSAFREE5:98
Hom(T,x1,x2) = Hom(T,x2,x1);
theorem :: MSAFREE5:99
Hom(T,x1,x2)**Hom(T,x1,x2) = id the Sorts of T;
theorem :: MSAFREE5:100
r is x1-omitting x2-omitting implies Hom(T,x1,x2).r = r;
registration
let S,X,T,s,x;
reduce (canonical_homomorphism T).s.(x-term) to x-term;
end;
theorem :: MSAFREE5:101
(canonical_homomorphism T)**Hom(Free(S,X),x,x1) =
Hom(T,x,x1)**canonical_homomorphism T;
theorem :: MSAFREE5:102
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;
theorem :: MSAFREE5:103
x1 <> x2 & t is x2-omitting implies Hom(Free(S,X),x1,x2).t is x1-omitting;
theorem :: MSAFREE5:104
for A being finite Subset of Union the Sorts of Free(S,Y)
ex y st for v st v in A holds v is y-omitting;
definition
let S,X,T;
attr T is struct-invariant means
:: MSAFREE5:def 32
for o for p being Element of Args(o,T) st Den(o,T).p = Den(o,Free(S,X)).p
for s,x1,x2 holds
Den(o,T).(Hom(T,x1,x2)#p) = Den(o,Free(S,X)).(Hom(T,x1,x2)#p);
end;
theorem :: MSAFREE5:105
T is struct-invariant implies for r being Element of T,s holds
Hom(T,x1,x2).s.r = Hom(Free(S,X),x1,x2).s.r;
theorem :: MSAFREE5:106
T is struct-invariant & x1 <> x2 & r is x2-omitting implies
Hom(T,x1,x2).r is x1-omitting;
theorem :: MSAFREE5:107
Q is struct-invariant & v is y-omitting implies
(canonical_homomorphism Q).v is y-omitting;
theorem :: MSAFREE5:108
Q is struct-invariant implies
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
for t being Element of Q st t = Den(o,Q).p holds t is y-omitting;
theorem :: MSAFREE5:109
Q is struct-invariant & v is y-omitting implies h2.v is y-omitting;
theorem :: MSAFREE5:110
for R being NF-var terminating with_UN_property invariant stable
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);
theorem :: MSAFREE5:111
for R being NF-var terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X) holds
i in dom p & R.((the_arity_of o)/.i) reduces t1,t2 implies
R.the_result_sort_of o reduces Den(o,Free(S,X)).(p+*(i,t1)),
Den(o,Free(S,X)).(p+*(i,t2));
theorem :: MSAFREE5:112
for R being NF-var terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X)
for t holds R.the_sort_of t reduces t, (canonical_homomorphism NFAlgebra R).t
;
theorem :: MSAFREE5:113
for R being NF-var terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X)
for o,p holds R.the_result_sort_of o reduces o-term p,
Den(o,NFAlgebra R).((canonical_homomorphism NFAlgebra R)#p);
theorem :: MSAFREE5:114
for R being NF-var terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X)
for o,p 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;
registration
let S,X;
let R be NF-var terminating with_UN_property invariant stable
ManySortedRelation of Free(S,X);
cluster NFAlgebra R -> struct-invariant;
end;
registration
let S,X;
cluster struct-invariant for all_vars_including inheriting_operations
free_in_itself (X,S)-terms MSAlgebra over S;
end;
begin :: Context vs translations
definition
let S,s1,s2;
attr s2 is s1-reachable means
:: MSAFREE5:def 33
TranslationRel S reduces s1,s2;
end;
registration
let S,s1;
cluster s1-reachable for SortSymbol of S;
end;
reserve
s2 for s1-reachable SortSymbol of S,
g1 for Translation of Free(S,Y),s1,s2;
theorem :: MSAFREE5:115
TranslationRel S reduces s,the_sort_of C9;
registration
let S,X,s,x,C;
cluster the_sort_of C -> s-reachable;
end;
definition
let S,X,s1,s2,g;
let t be Element of (the Sorts of Free(S,X)).s1;
redefine func g.t -> Element of (the Sorts of Free(S,X)).s2;
end;
definition
let S,X,s,x,C;
attr C is basic means
:: MSAFREE5:def 34
ex o,p st C = o-term p & x-context_in p = x-term;
end;
definition
let S,X,s,x,C;
func transl C -> Function of (the Sorts of Free(S,X)).s,
(the Sorts of Free(S,X)).the_sort_of C means
:: MSAFREE5:def 35
the_sort_of t = s implies it.t = C-sub(t);
end;
theorem :: MSAFREE5:116
for S,s,X,x,C st C = x-term holds
transl C = id((the Sorts of Free(S,X)).s);
theorem :: MSAFREE5:117
C9 = o-term k & z-context_in k = z-term & k1 = k+*(z-context_pos_in k,l)
implies C9-sub l = o-term k1;
theorem :: MSAFREE5:118
C9 is basic implies transl C9 is_e.translation_of Free(S,Z),s,the_sort_of C9;
theorem :: MSAFREE5:119
for V being finite set holds
m in dom q & (the_arity_of o)/.m = s implies
ex y,C1,q1 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;
theorem :: MSAFREE5:120
for s1,s2 being SortSymbol of S, V being finite set holds
m in dom q & s1 = (the_arity_of o)/.m implies
ex y being (Element of Y.s1), C being (context of y), q1 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));
registration
let S,X,t;
let a;
cluster Coim(t,a) -> FinSequence-membered;
end;
theorem :: MSAFREE5:121
X is non-trivial & the_sort_of t = s implies
card Coim(t,a) c= card Coim(C-sub t,a);
theorem :: MSAFREE5:122
p is x-context_including & i in dom p implies
(p/.i is non x-omitting iff p/.i is x-context);
theorem :: MSAFREE5:123
X is non-trivial & the_sort_of C = s1 implies
for x1 being Element of X.s1
for C1 being (context of x1), C2 being context of x st C2 = C1-sub(C)
for t st the_sort_of t = s holds C2-sub t = C1-sub(C-sub t);
theorem :: MSAFREE5:124
X is non-trivial & the_sort_of C = s1 implies
for x1 being Element of X.s1
for C1 being (context of x1), C2 being context of x st C2 = C1-sub(C)
holds transl C2 = (transl C1)*(transl C);
theorem :: MSAFREE5:125
ex y11,C12 st the_sort_of C12 = s2 & g1 = transl C12;
scheme :: MSAFREE5:sch 5
LambdaTerm {S() -> non empty non void ManySortedSign,
X() -> non-empty ManySortedSet of the carrier of S(),
T1,T2() -> all_vars_including inheriting_operations X(),S()-terms
MSAlgebra over S(),
F(object) -> Element of T2()}:
ex f being ManySortedFunction of T1(),T2() st
for t being Element of T1() holds f.t = F(t)
provided
for t being Element of T1() holds the_sort_of t = the_sort_of F(t);
theorem :: MSAFREE5:126
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);
theorem :: MSAFREE5:127
(canonical_homomorphism T).(h.t) =
(canonical_homomorphism T).(h.@((canonical_homomorphism T).t));
begin :: Context vs endomorphism
definition
let S;
let B be non empty FinSequence of the carrier of S;
let i being Element of dom B;
redefine func B.i -> SortSymbol of S;
end;
definition
let S,X;
let B be FinSequence of the carrier of S;
let V be FinSequence of Union X;
attr V is B-sorts means
:: MSAFREE5:def 36 :: Element of product (X*B)
dom V = dom B & for i st i in dom B holds V.i in X.(B.i);
end;
registration
let S,X;
let B be FinSequence of the carrier of S;
cluster B-sorts for FinSequence of Union X;
end;
registration
let S,X;
let B be non empty FinSequence of the carrier of S;
cluster B-sorts -> non empty for FinSequence of Union X;
end;
definition
let S,X;
let B be non empty FinSequence of the carrier of S;
let V be B-sorts FinSequence of Union X;
let i being Element of dom B;
redefine func V.i -> Element of X.(B.i);
end;
definition
let S,X;
let B be FinSequence of the carrier of S;
let D be FinSequence of Free(S,X);
attr D is B-sorts means
:: MSAFREE5:def 37 :: Element of product ((the Sorts of Free(S,X))*B)
dom D = dom B &
for i st i in dom B holds D.i in (the Sorts of Free(S,X)).(B.i);
end;
registration
let S,X;
let B be FinSequence of the carrier of S;
cluster B-sorts for FinSequence of Free(S,X);
end;
registration
let S,X;
let B be non empty FinSequence of the carrier of S;
cluster B-sorts -> non empty for FinSequence of Free(S,X);
end;
definition
let S,X;
let B be non empty FinSequence of the carrier of S;
let D be B-sorts FinSequence of Free(S,X);
let i being Element of dom B;
redefine func D.i -> Element of (the Sorts of Free(S,X)).(B.i);
end;
definition
let S,X;
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
:: MSAFREE5:def 38
dom F = dom B &
for i being Element of dom B holds F.i is context of V.i;
end;
registration
let S,X;
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 Free(S,X);
end;
scheme :: MSAFREE5:sch 6
FinSeqLambda{B() -> non empty FinSequence, F(set) -> object}:
ex p being non empty FinSequence st dom p = dom B() &
for i being Element of dom B() holds p.i = F(i);
scheme :: MSAFREE5:sch 7
FinSeqRecLambda{B() -> non empty FinSequence, A() -> object,
F(object,object) -> set}:
ex p being non empty FinSequence st dom p = dom B() & p.1 = A() &
for i,j being Element of dom B() st j = i+1 holds p.j = F(i,p.i);
scheme :: MSAFREE5:sch 8
FinSeqRec2Lambda{B() -> non empty FinSequence, A() -> DecoratedTree,
F(object,DecoratedTree) -> DecoratedTree}:
ex p being non empty DTree-yielding FinSequence st
dom p = dom B() & p.1 = A() &
for i,j being Element of dom B() st j = i+1
for d being DecoratedTree st d = p.i holds p.j = F(i,d);
registration
let S,X;
let B be non empty FinSequence of the carrier of S;
let V be B-sorts FinSequence of Union X;
cluster V-context-sequence for FinSequence of Free(S,X);
end;
definition
let S,X;
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 being Element of dom B;
redefine func F.i -> context of V.i;
end;
definition
let S,X;
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
:: 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;
definition
let S,X;
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
t in rng D implies vf t misses rng V;
end;
theorem :: MSAFREE5:128
for S,X 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
for b1,b2 being Element of dom B holds D.b1 is V.b2-omitting;
registration
let S,Y;
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 one-to-one V-omitting D-omitting for B-sorts FinSequence of Union Y;
end;
definition
let S,X,t;
mode vf-sequence of t -> FinSequence means
:: MSAFREE5:def 42
ex f being one-to-one FinSequence st
rng f = {xi where xi is Element of dom t: ex s,x st t.xi = [x,s]} &
dom it = dom f & for i st i in dom it holds it.i = t.(f.i);
end;
registration
let f be FinSequence;
cluster pr1 f -> FinSequence-like;
cluster pr2 f -> FinSequence-like;
end;
theorem :: MSAFREE5:129
for f being vf-sequence of t holds pr2 f is FinSequence of the carrier of S;
theorem :: MSAFREE5:130
for f being vf-sequence of t, B being FinSequence of the carrier of S
st B = pr2 f holds pr1 f is B-sorts FinSequence of Union X;
registration
let f be non empty FinSequence;
reduce In(1, dom f) to 1;
reduce In(len f, dom f) to len f;
end;
theorem :: MSAFREE5:131
for xi being Element of dom t st t.xi = [x,s]
holds the_sort_of t1 = s implies
t with-replacement (xi,t1) is Element of Free(S,X), the_sort_of t;
theorem :: MSAFREE5:132
X is non-trivial implies
for xi being Element of dom C st C.xi = [x,s]
holds the_sort_of t = s implies C-sub t = C with-replacement (xi,t);
theorem :: MSAFREE5:133
for xi1,xi2 being FinSequence st xi1 <> xi2 & xi1 in dom t & xi2 in dom t
for s1,s2 being SortSymbol of S, 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;
theorem :: MSAFREE5:134
for t,t1 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
;
theorem :: MSAFREE5:135
for t,t1 for xi being Element of dom t st t.xi = [x,s]
holds dom t c= dom (t with-replacement(xi,t1));
theorem :: MSAFREE5:136
for t for xi being Element of dom t st t.xi = [x,s]
holds dom t = dom (t with-replacement(xi,x1-term));
theorem :: MSAFREE5:137
for t,t1 being Tree, xi being Element of t holds
(t with-replacement(xi,t1))|xi = t1;
theorem :: MSAFREE5:138
for t,t1 being DecoratedTree, xi being Node of t holds
(t with-replacement(xi,t1))|xi = t1;
theorem :: MSAFREE5:139
for xi being Node of t st t1 = t|xi holds (h.t)|xi = h.t1;
theorem :: MSAFREE5:140
for xi being Node of t st t.xi = [x,s] holds t|xi = x-term;
theorem :: MSAFREE5:141
for t,t1 being Tree, xi,nu being Element of t st not xi c= nu &
not nu c= xi holds (t with-replacement(xi,t1))|nu = t|nu;
theorem :: MSAFREE5:142
for t,t1 being DecoratedTree, xi,nu being Node of t st not xi c= nu &
not nu c= xi holds (t with-replacement(xi,t1))|nu = t|nu;
theorem :: MSAFREE5:143
t c= t1 implies t = t1;
theorem :: MSAFREE5:144
for t
for h being Endomorphism of Free(S,X) holds dom t c= dom (h.t) &
for I st
I = {xi where xi is Element of dom t: ex s,x st t.xi = [x,s]}
holds t|((dom t) \ I) = (h.t)|((dom t) \ I);
theorem :: MSAFREE5:145
for t st I = {xi where xi is Element of dom t: ex s,x st t.xi = [x,s]}
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;
theorem :: MSAFREE5:146
for v,v1
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,y st v.xi = [y,s]} &
dom v c= dom v1 & v|((dom v) \ rng g) = v1|((dom v) \ rng g) &
for i st i in dom g holds (h.v)|(g/.i qua Node of v)=v1|(g/.i qua Node of v)
holds h.v = v1;
theorem :: MSAFREE5:147
for h being Endomorphism of Free(S,Y)
for f being vf-sequence of v st f <> {}
ex B being non empty FinSequence of the carrier of S st
ex V1 be 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) st
ex V2 being V1-omitting D-omitting B-sorts FinSequence of Union Y
st (for i being Element of dom B holds D.i = h.((V1.i)-term)) &
ex F be V2-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));