:: Free Many Sorted Universal Algebra
:: by Beata Perkowska
::
:: Received April 27, 1994
:: Copyright (c) 1994-2026 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, FUNCT_1, RELAT_1, PBOOLE, SUBSET_1, CARD_3, REALSET1,
TARSKI, ZFMISC_1, PARTFUN1, STRUCT_0, MSUALG_1, MSUALG_2, PRELAMB,
MSUALG_3, FINSEQ_1, MARGREL1, LANG1, TDGROUP, DTCONSTR, TREES_3, TREES_4,
NAT_1, TREES_2, MCART_1, UNIALG_2, QC_LANG1, GROUP_6, MSAFREE;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NAT_1,
RELAT_1, RELSET_1, STRUCT_0, FUNCT_1, PARTFUN1, MCART_1, FUNCT_2,
FINSEQ_1, PBOOLE, TREES_2, FINSEQ_2, CARD_3, LANG1, TREES_4, DTCONSTR,
MSUALG_1, MSUALG_2, MSUALG_3;
constructors XXREAL_0, NAT_1, NAT_D, CARD_3, FINSEQOP, DTCONSTR, MSUALG_3,
RELSET_1, PBOOLE, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
FINSEQ_1, PBOOLE, TREES_2, TREES_3, STRUCT_0, DTCONSTR, MSUALG_1,
MSUALG_3, FUNCT_2, RELSET_1, XTUPLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, PBOOLE, MSUALG_3;
equalities TARSKI;
expansions TARSKI, XBOOLE_0, PBOOLE, MSUALG_3;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, PBOOLE, CARD_3, MSUALG_1,
MSUALG_2, MSUALG_3, RELAT_1, LANG1, DTCONSTR, FINSEQ_1, TREES_4, TREES_1,
DOMAIN_1, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, TREES_3, PARTFUN1,
FINSEQ_3, FINSEQ_2, XTUPLE_0;
schemes CLASSES1, FUNCT_1, RELSET_1, DTCONSTR, XBOOLE_0;
begin
::
:: Preliminaries
::
theorem Th1:
for I be set, J be non empty set, f be Function of I,J*, X be
ManySortedSet of J, p be Element of J*, x be set st x in I & p = f.x holds (X#
* f).x = product (X * p)
proof
let I be set, J be non empty set, f be Function of I,J*, X be ManySortedSet
of J, p be Element of J*, x be set;
assume
A1: x in I & p = f.x;
A2: dom f = I by FUNCT_2:def 1;
then dom (X# * f) = dom f by PARTFUN1:def 2;
hence (X# * f).x =(X# qua ManySortedSet of J*).p by A1,A2,FUNCT_1:12
.= product (X * p) by FINSEQ_2:def 5;
end;
definition
let I be set, A,B be ManySortedSet of I, C be ManySortedSubset of A;
let F be ManySortedFunction of A,B;
func F || C -> ManySortedFunction of C,B means
:Def1:
for i be set st i in I holds it.i = (F.i) | (C.i);
existence
proof
defpred P[object,object] means $2 = (F.$1) | (C.$1);
A1: for i be object st i in I ex u be object st P[i,u];
consider H be Function such that
A2: dom H = I & for i be object st i in I holds P[i,H.i] from CLASSES1:
sch 1 (A1);
reconsider H as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18;
for i be object st i in I holds H.i is Function of C.i,B.i
proof
let i be object;
assume
A3: i in I;
then reconsider f = F.i as Function of A.i,B.i by PBOOLE:def 15;
A4: H.i = f | (C.i) by A2,A3;
C c= A by PBOOLE:def 18;
then
A5: C.i c= A.i by A3;
per cases;
suppose
A6: B.i is empty;
then H.i = {} by A4;
hence thesis by A6,FUNCT_2:def 1,RELSET_1:12;
end;
suppose
A8: B.i is non empty;
then
A9: dom f = A.i by FUNCT_2:def 1;
A10: rng (f|(C.i)) c= B.i by RELAT_1:def 19;
dom (f|(C.i)) = dom f /\ (C.i) by RELAT_1:61
.= C.i by A5,A9,XBOOLE_1:28;
hence thesis by A4,A8,A10,FUNCT_2:def 1,RELSET_1:4;
end;
end;
then reconsider H as ManySortedFunction of C,B by PBOOLE:def 15;
take H;
thus thesis by A2;
end;
uniqueness
proof
let X,Y be ManySortedFunction of C,B;
assume that
A11: for i be set st i in I holds X.i = (F.i) | (C.i) and
A12: for i be set st i in I holds Y.i = (F.i) | (C.i);
let i be object;
assume
A13: i in I;
then X.i = (F.i)|(C.i) by A11;
hence thesis by A12,A13;
end;
end;
definition
let I be set, X be ManySortedSet of I, i be object;
assume
A1: i in I;
func coprod(i,X) -> set means
:Def2:
for x be set holds x in it iff ex a be set st a in X.i & x = [a,i];
existence
proof
defpred P[object] means ex a be set st a in X.i & $1 = [a,i];
consider A be set such that
A2: for x be object holds x in A iff x in [:X.i,I:] & P[x] from XBOOLE_0:
sch 1;
take A;
let x be set;
thus x in A implies ex a be set st a in X.i & x = [a,i] by A2;
given a be set such that
A3: a in X.i & x = [a,i];
x in [:X.i,I:] by A1,A3,ZFMISC_1:87;
hence thesis by A2,A3;
end;
uniqueness
proof
let A,B be set;
assume that
A4: for x be set holds x in A iff ex a be set st a in X.i & x = [a,i] and
A5: for x be set holds x in B iff ex a be set st a in X.i & x = [a,i];
thus A c= B
proof
let x be object;
assume x in A;
then ex a be set st a in X.i & x = [a,i] by A4;
hence thesis by A5;
end;
let x be object;
assume x in B;
then ex a be set st a in X.i & x = [a,i] by A5;
hence thesis by A4;
end;
end;
notation
let I be set, X be ManySortedSet of I;
synonym coprod X for disjoin X;
end;
registration
let I be set, X be ManySortedSet of I;
cluster coprod X -> I-defined;
coherence
proof
dom coprod X = dom X by CARD_3:def 3;
then dom coprod X = I by PARTFUN1:def 2;
hence thesis by RELAT_1:def 18;
end;
end;
registration
let I be set, X be ManySortedSet of I;
cluster coprod X -> total;
coherence
proof
dom coprod X = dom X by CARD_3:def 3;
then dom coprod X = I by PARTFUN1:def 2;
hence thesis by PARTFUN1:def 2;
end;
end;
definition
let I be set, X be ManySortedSet of I;
redefine func coprod X means :: redefines coprod (MSAFREE, synonym) → disjoin (CARD_3, definition)
:Def3:
dom it = I & for i be set st i in I holds it.i = coprod(i,X);
compatibility
proof
let IT be Function;
hereby
assume
A1: IT = disjoin X;
hence dom IT = I by PARTFUN1:def 2;
let i be set;
assume
A2: i in I;
then i in dom X by PARTFUN1:def 2;
then
A3: IT.i = [:X.i,{i}:] by A1,CARD_3:def 3;
now
let x be set;
hereby
assume x in IT.i;
then consider a,b being object such that
A4: a in X.i and
A5: b in {i} & x = [a,b] by A3,ZFMISC_1:def 2;
reconsider a as set by TARSKI:1;
take a;
thus a in X.i by A4;
thus x = [a,i] by A5,TARSKI:def 1;
end;
given a being set such that
A6: a in X.i & x = [a,i];
i in {i} by TARSKI:def 1;
hence x in IT.i by A3,A6,ZFMISC_1:def 2;
end;
hence IT.i = coprod(i,X) by A2,Def2;
end;
assume that
A7: dom IT = I and
A8: for i be set st i in I holds IT.i = coprod(i,X);
A9: dom IT = dom X by A7,PARTFUN1:def 2;
now
let x be object;
assume
A10: x in dom X;
then
A11: x in I;
A12: now
let a be object;
hereby
assume a in coprod(x,X);
then
A13: ex b being set st b in X.x & a = [b,x] by A11,Def2;
x in {x} by TARSKI:def 1;
hence a in [:X.x,{x}:] by A13,ZFMISC_1:def 2;
end;
assume a in [:X.x,{x}:];
then consider a1,a2 being object such that
A14: a1 in X.x and
A15: a2 in {x} and
A16: a = [a1,a2] by ZFMISC_1:def 2;
a2 = x by A15,TARSKI:def 1;
hence a in coprod(x,X) by A11,A14,A16,Def2;
end;
thus IT.x = coprod(x,X) by A8,A10
.= [:X.x,{x}:] by A12,TARSKI:2;
end;
hence thesis by A9,CARD_3:def 3;
end;
end;
registration
let I be set, X be non-empty ManySortedSet of I;
cluster coprod X -> non-empty;
coherence
proof
let x be object;
assume
A1: x in I;
then reconsider i = x as Element of I;
consider a be object such that
A2: a in X.i by A1,XBOOLE_0:def 1;
(coprod X).i = coprod(i,X) by A1,Def3;
then [a,i] in (coprod X).i by A1,A2,Def2;
hence thesis;
end;
end;
registration
let I be non empty set, X be non-empty ManySortedSet of I;
cluster Union X -> non empty;
coherence
proof
set i = the Element of I;
consider a be object such that
A1: a in X.i by XBOOLE_0:def 1;
dom X = I by PARTFUN1:def 2;
then X.i in rng X by FUNCT_1:def 3;
then a in union rng X by A1,TARSKI:def 4;
hence thesis by CARD_3:def 4;
end;
end;
theorem
for I be set, X be ManySortedSet of I, i be set st i in I holds
X.i <> {} iff (coprod X).i <> {}
proof
let I be set, X be ManySortedSet of I, i be set;
assume
A1: i in I;
then
A2: (coprod X).i = coprod(i,X) by Def3;
thus X.i <> {} implies (coprod X).i <> {}
proof
assume X.i <> {};
then consider x be object such that
A3: x in X.i by XBOOLE_0:def 1;
[x,i] in (coprod X).i by A1,A2,A3,Def2;
hence thesis;
end;
assume (coprod X).i <> {};
then consider a be object such that
A4: a in coprod(i,X) by A2,XBOOLE_0:def 1;
ex x be set st x in X.i & a = [x,i] by A1,A4,Def2;
hence thesis;
end;
begin
::
:: Free Many Sorted Universal Algebra - General Notions
::
reserve S for non void non empty ManySortedSign,
U0 for MSAlgebra over S;
definition
let S be non void non empty ManySortedSign, U0 be MSAlgebra over S;
mode GeneratorSet of U0 -> MSSubset of U0 means
:Def4:
the Sorts of GenMSAlg (it) = the Sorts of U0;
existence
proof
set A = the Sorts of U0;
reconsider A as MSSubset of U0 by PBOOLE:def 18;
take A;
set G = GenMSAlg(A);
the Sorts of G is MSSubset of U0 by MSUALG_2:def 9;
then
A1: the Sorts of G c= A by PBOOLE:def 18;
A is MSSubset of G by MSUALG_2:def 17;
then A c= the Sorts of G by PBOOLE:def 18;
hence thesis by A1,PBOOLE:146;
end;
end;
theorem
for S be non void non empty ManySortedSign, U0 be strict non-empty
MSAlgebra over S, A be MSSubset of U0 holds A is GeneratorSet of U0 iff
GenMSAlg(A) = U0
proof
let S be non void non empty ManySortedSign, U0 be strict non-empty MSAlgebra
over S, A be MSSubset of U0;
thus A is GeneratorSet of U0 implies GenMSAlg(A) = U0
proof
reconsider U1 = U0 as MSSubAlgebra of U0 by MSUALG_2:5;
assume A is GeneratorSet of U0;
then the Sorts of GenMSAlg(A) = the Sorts of U1 by Def4;
hence thesis by MSUALG_2:9;
end;
assume GenMSAlg(A) = U0;
hence thesis by Def4;
end;
definition
let S,U0;
let IT be GeneratorSet of U0;
attr IT is free means
for U1 be non-empty MSAlgebra over S for f be
ManySortedFunction of IT,the Sorts of U1 ex h be ManySortedFunction of U0,U1 st
h is_homomorphism U0,U1 & h || IT = f;
end;
definition
let S be non void non empty ManySortedSign;
let IT be MSAlgebra over S;
attr IT is free means
:Def6:
ex G being GeneratorSet of IT st G is free;
end;
theorem Th4:
for S be non void non empty ManySortedSign, X be ManySortedSet of
the carrier of S holds Union coprod X misses [:the carrier' of S,{the carrier
of S}:]
proof
let S be non void non empty ManySortedSign, X be ManySortedSet of the
carrier of S;
assume Union (coprod X) /\ [:the carrier' of S,{the carrier of S}:] <> {};
then consider x be object such that
A1: x in Union (coprod X) /\ [:the carrier' of S,{the carrier of S}:] by
XBOOLE_0:def 1;
x in Union (coprod X) by A1,XBOOLE_0:def 4;
then x in union rng (coprod X) by CARD_3:def 4;
then consider A be set such that
A2: x in A and
A3: A in rng (coprod X) by TARSKI:def 4;
consider s be object such that
A4: s in dom (coprod X) and
A5: (coprod X).s = A by A3,FUNCT_1:def 3;
reconsider s as SortSymbol of S by A4;
A = coprod(s,X) by A5,Def3;
then
A6: ex a be set st a in X.s & x = [a,s] by A2,Def2;
x in [:the carrier' of S,{the carrier of S}:] by A1,XBOOLE_0:def 4;
then s in {the carrier of S} by A6,ZFMISC_1:87;
then s in the carrier of S & s = the carrier of S by TARSKI:def 1;
hence contradiction;
end;
begin
::
:: Construction of Free Many Sorted Algebras for Given Signature
::
definition
let S be non void non empty ManySortedSign, X be ManySortedSet of the
carrier of S;
func REL(X) -> Relation of ([:the carrier' of S,{the carrier of S}:] \/
Union (coprod X)), (([:the carrier' of S,{the carrier of S}:] \/ Union (coprod
X))*) means
:Def7:
for a be Element of [:the carrier' of S,{the carrier of S}:]
\/ Union (coprod X), b be Element of ([:the carrier' of S,{the carrier of S}:]
\/ Union (coprod X))* holds [a,b] in it iff a in [:the carrier' of S,{the
carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a holds
len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the
carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the
carrier of S] = b.x holds the_result_sort_of o1 = (the_arity_of o).x) & (b.x in
Union (coprod X) implies b.x in coprod((the_arity_of o).x,X));
existence
proof
set O = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X);
defpred P[Element of O,Element of O*] means $1 in [:the carrier' of S,{the
carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = $1 holds
len $2 = len (the_arity_of o) & for x be set st x in dom $2 holds ($2.x in [:
the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1
,the carrier of S] = $2.x holds the_result_sort_of o1 = (the_arity_of o).x) & (
$2.x in Union (coprod X) implies $2.x in coprod((the_arity_of o).x,X));
consider R be Relation of O,O* such that
A1: for a be Element of O, b be Element of O* holds [a,b] in R iff P[a
,b] from RELSET_1:sch 2;
take R;
let a be Element of O, b be Element of O*;
thus [a,b] in R implies a in [:the carrier' of S,{the carrier of S}:] &
for o be OperSymbol of S st [o,the carrier of S] = a holds len b = len (
the_arity_of o) & for x be set st x in dom b holds (b.x in [:the carrier' of S,
{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S]
= b.x holds the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union (coprod
X) implies b.x in coprod((the_arity_of o).x,X)) by A1;
assume a in [:the carrier' of S,{the carrier of S}:] & for o be
OperSymbol of S st [o,the carrier of S] = a holds len b = len (the_arity_of o)
& for x be set st x in dom b holds (b.x in [:the carrier' of S,{the carrier of
S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds
the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union ( coprod X) implies
b.x in coprod(( the_arity_of o).x,X));
hence thesis by A1;
end;
uniqueness
proof
set O = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X);
let R,P be Relation of O,O*;
assume that
A2: for a be Element of O, b be Element of O* holds [a,b] in R iff a
in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o,
the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in
dom b holds (b.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 = (
the_arity_of o).x) & (b.x in Union (coprod X) implies b.x in coprod((
the_arity_of o).x,X)) and
A3: for a be Element of O, b be Element of O* holds [a,b] in P iff a
in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o,
the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in
dom b holds (b.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 = (
the_arity_of o).x) & (b.x in Union (coprod X) implies b.x in coprod((
the_arity_of o).x,X));
for x,y be object holds [x,y] in R iff [x,y] in P
proof
let x,y be object;
thus [x,y] in R implies [x,y] in P
proof
assume
A4: [x,y] in R;
then reconsider a = x as Element of O by ZFMISC_1:87;
reconsider b = y as Element of O* by A4,ZFMISC_1:87;
[a,b] in R by A4;
then
A5: a in [:the carrier' of S,{the carrier of S}:] by A2;
for o be OperSymbol of S st [o,the carrier of S] = a holds len b =
len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the carrier'
of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier
of S ] = b.x holds the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union
( coprod X) implies b.x in coprod((the_arity_of o).x,X)) by A2,A4;
hence thesis by A3,A5;
end;
assume
A6: [x,y] in P;
then reconsider a = x as Element of O by ZFMISC_1:87;
reconsider b = y as Element of O* by A6,ZFMISC_1:87;
[a,b] in P by A6;
then
A7: a in [:the carrier' of S,{the carrier of S}:] by A3;
for o be OperSymbol of S st [o,the carrier of S] = a holds len b =
len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the carrier'
of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier
of S ] = b.x holds the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union
( coprod X) implies b.x in coprod((the_arity_of o).x,X)) by A3,A6;
hence thesis by A2,A7;
end;
hence thesis by RELAT_1:def 2;
end;
end;
reserve S for non void non empty ManySortedSign,
X for ManySortedSet of the carrier of S,
o for OperSymbol of S,
b for Element of ([:the carrier' of S,{the
carrier of S}:] \/ Union (coprod X))*;
theorem Th5:
[[o,the carrier of S],b] in REL(X) iff len b = len (the_arity_of
o) & for x be set st x in dom b holds (b.x in [:the carrier' of S,{the carrier
of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds
the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union (coprod X) implies
b.x in coprod((the_arity_of o).x,X))
proof
defpred P[OperSymbol of S,Element of ([:the carrier' of S,{the carrier of S}
:] \/ Union (coprod X))*] means len $2 = len (the_arity_of $1) & for x be set
st x in dom $2 holds ($2.x in [:the carrier' of S,{the carrier of S}:] implies
for o1 be OperSymbol of S st [o1,the carrier of S] = $2.x holds
the_result_sort_of o1 = (the_arity_of $1).x) & ($2.x in Union (coprod X)
implies b.x in coprod((the_arity_of $1).x,X));
set a = [o,the carrier of S];
the carrier of S in {the carrier of S} by TARSKI:def 1;
then
A1: a in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:87;
then reconsider
a as Element of [:the carrier' of S,{the carrier of S}:] \/ Union
(coprod X) by XBOOLE_0:def 3;
thus [[o,the carrier of S],b] in REL(X) implies P[o,b]
proof
assume [[o,the carrier of S],b] in REL(X);
then for o1 be OperSymbol of S st [o1,the carrier of S] = a holds P[o1,b]
by Def7;
hence thesis;
end;
assume
A2: P[o,b];
now
let o1 be OperSymbol of S;
assume [o1,the carrier of S] = a;
then o1 = o by XTUPLE_0:1;
hence P[o1,b] by A2;
end;
hence thesis by A1,Def7;
end;
definition
let S be non void non empty ManySortedSign, X be ManySortedSet of the
carrier of S;
func DTConMSA(X) -> DTConstrStr equals
DTConstrStr (# [:the carrier' of S,{
the carrier of S}:] \/ Union (coprod X), REL(X) #);
correctness;
end;
registration
let S be non void non empty ManySortedSign, X be ManySortedSet of the
carrier of S;
cluster DTConMSA(X) -> strict non empty;
coherence;
end;
theorem Th6:
for S be non void non empty ManySortedSign, X be ManySortedSet of
the carrier of S holds NonTerminals(DTConMSA(X))c= [:the carrier' of S,{the
carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA(X)) & (X is non-empty
implies NonTerminals(DTConMSA(X)) = [:the carrier' of S,{the carrier of S}:] &
Terminals (DTConMSA(X)) = Union (coprod X))
proof
let S be non void non empty ManySortedSign, X be ManySortedSet of the
carrier of S;
set D = DTConMSA(X), A = [:the carrier' of S,{the carrier of S}:] \/ Union (
coprod (X qua ManySortedSet of the carrier of S));
A1: the carrier of D = (Terminals D) \/ (NonTerminals D) by LANG1:1;
thus
A2: NonTerminals D c= [:the carrier' of S,{the carrier of S}:]
proof
let x be object;
assume x in NonTerminals D;
then
x in { s where s is Symbol of D: ex n being FinSequence st s ==> n} by
LANG1:def 3;
then consider s be Symbol of D such that
A3: s = x and
A4: ex n being FinSequence st s ==> n;
consider n be FinSequence such that
A5: s ==> n by A4;
[s,n] in the Rules of D by A5,LANG1:def 1;
then reconsider n as Element of A* by ZFMISC_1:87;
reconsider s as Element of A;
[s,n] in REL X by A5,LANG1:def 1;
hence thesis by A3,Def7;
end;
A6: Union(coprod X) misses [:the carrier' of S,{the carrier of S}:] by Th4;
thus
A7: Union (coprod X) c= Terminals (DTConMSA(X))
proof
let x be object;
assume
A8: x in Union (coprod X);
then x in A by XBOOLE_0:def 3;
then x in Terminals D or x in NonTerminals D by A1,XBOOLE_0:def 3;
hence thesis by A6,A2,A8,XBOOLE_0:3;
end;
assume
A9: X is non-empty;
thus NonTerminals D c= [:the carrier' of S,{the carrier of S}:] by A2;
thus
A10: [:the carrier' of S,{the carrier of S}:] c= NonTerminals D
proof
let x be object;
assume
A11: x in [:the carrier' of S,{the carrier of S}:];
then consider
o being OperSymbol of S, x2 being Element of {the carrier of S}
such that
A12: x = [o,x2] by DOMAIN_1:1;
set O = the_arity_of o;
defpred P[object,object] means $2 in coprod (O.$1,X);
A13: for a be object st a in Seg len O ex b be object st P[a,b]
proof
let a be object;
assume a in Seg len O;
then a in dom O by FINSEQ_1:def 3;
then
A14: O.a in rng O by FUNCT_1:def 3;
A15: rng O c= the carrier of S by FINSEQ_1:def 4;
then consider x be object such that
A16: x in X.(O.a) by A9,A14,XBOOLE_0:def 1;
take [x,O.a];
thus thesis by A14,A15,A16,Def2;
end;
consider b be Function such that
A17: dom b = Seg len O &
for a be object st a in Seg len O holds P[a,b.a]
from CLASSES1:sch 1(A13);
reconsider b as FinSequence by A17,FINSEQ_1:def 2;
rng b c= A
proof
let a be object;
A18: rng O c= the carrier of S by FINSEQ_1:def 4;
assume a in rng b;
then consider c be object such that
A19: c in dom b and
A20: b.c = a by FUNCT_1:def 3;
dom O = Seg len O by FINSEQ_1:def 3;
then
A21: O.c in rng O by A17,A19,FUNCT_1:def 3;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).(O.c) in rng coprod(X) by A21,A18,FUNCT_1:def 3;
then
A22: coprod(O.c,X) in rng coprod(X) by A21,A18,Def3;
a in coprod(O.c,X) by A17,A19,A20;
then a in union rng coprod(X) by A22,TARSKI:def 4;
then a in Union coprod(X) by CARD_3:def 4;
hence thesis by XBOOLE_0:def 3;
end;
then reconsider b as FinSequence of A by FINSEQ_1:def 4;
reconsider b as Element of A* by FINSEQ_1:def 11;
A23: now
let c be set;
assume
A24: c in dom b;
dom O = Seg len O by FINSEQ_1:def 3;
then
A25: O.c in rng O by A17,A24,FUNCT_1:def 3;
A26: rng O c= the carrier of S by FINSEQ_1:def 4;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).(O.c) in rng coprod(X) by A25,A26,FUNCT_1:def 3;
then
A27: coprod(O.c,X) in rng coprod(X) by A25,A26,Def3;
P[c,b.c] by A17,A24;
then b.c in union rng coprod(X) by A27,TARSKI:def 4;
then b.c in Union coprod(X) by CARD_3:def 4;
hence b.c in [:the carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = b.c holds the_result_sort_of o1 = O.
c by A6,XBOOLE_0:3;
assume b.c in Union (coprod X);
thus b.c in coprod(O.c,X) by A17,A24;
end;
A28: the carrier of S = x2 by TARSKI:def 1;
then reconsider
xa = [o,the carrier of S] as Element of (the carrier of D) by A11,A12,
XBOOLE_0:def 3;
len b = len O by A17,FINSEQ_1:def 3;
then [xa,b] in REL(X) by A23,Th5;
then xa ==> b by LANG1:def 1;
then xa in { t where t is Symbol of D: ex n be FinSequence st t ==> n};
hence thesis by A12,A28,LANG1:def 3;
end;
A29: (Terminals D) misses (NonTerminals D) by DTCONSTR:8;
thus Terminals D c= Union (coprod X)
proof
let x be object;
assume x in Terminals D;
then x in A & not x in [:the carrier' of S,{the carrier of S}:] by A1,A29
,A10,XBOOLE_0:3,def 3;
hence thesis by XBOOLE_0:def 3;
end;
thus thesis by A7;
end;
reserve x for set;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
cluster DTConMSA(X) -> with_terminals with_nonterminals
with_useful_nonterminals;
coherence
proof
set D = DTConMSA(X), A = [:the carrier' of S,{the carrier of S}:] \/ Union
(coprod (X qua ManySortedSet of the carrier of S));
A1: Terminals D = Union (coprod X) by Th6;
A2: NonTerminals D = [:the carrier' of S,{the carrier of S}:] by Th6;
A3: Union (coprod X) misses [:the carrier' of S,{the carrier of S}:] by Th4;
for nt being Symbol of D st nt in NonTerminals D ex p being
FinSequence of TS(D) st nt ==> roots p
proof
let nt be Symbol of D;
assume nt in NonTerminals D;
then consider
o being OperSymbol of S, x2 being Element of {the carrier of S}
such that
A4: nt = [o,x2] by A2,DOMAIN_1:1;
set O = the_arity_of o;
defpred P[object,object] means $2 in coprod(O.$1,X);
A5: for a be object st a in Seg len O ex b be object st P[a,b]
proof
let a be object;
assume a in Seg len O;
then a in dom O by FINSEQ_1:def 3;
then
A6: O.a in rng O by FUNCT_1:def 3;
A7: rng O c= the carrier of S by FINSEQ_1:def 4;
then consider x be object such that
A8: x in X.(O.a) by A6,XBOOLE_0:def 1;
take [x,O.a];
thus thesis by A6,A7,A8,Def2;
end;
consider b be Function such that
A9: dom b = Seg len O & for a be object st a in Seg len O holds P[a,b.
a] from CLASSES1:sch 1(A5);
reconsider b as FinSequence by A9,FINSEQ_1:def 2;
A10: rng b c= A
proof
let a be object;
A11: rng O c= the carrier of S by FINSEQ_1:def 4;
assume a in rng b;
then consider c be object such that
A12: c in dom b and
A13: b.c = a by FUNCT_1:def 3;
dom O = Seg len O by FINSEQ_1:def 3;
then
A14: O.c in rng O by A9,A12,FUNCT_1:def 3;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).(O.c) in rng coprod(X) by A14,A11,FUNCT_1:def 3;
then
A15: coprod(O.c,X) in rng coprod(X) by A14,A11,Def3;
a in coprod (O.c,X) by A9,A12,A13;
then a in union rng coprod(X) by A15,TARSKI:def 4;
then a in Union coprod(X) by CARD_3:def 4;
hence thesis by XBOOLE_0:def 3;
end;
then reconsider b as FinSequence of A by FINSEQ_1:def 4;
reconsider b as Element of A* by FINSEQ_1:def 11;
deffunc F(object)=root-tree (b.$1);
consider f be Function such that
A16: dom f = dom b &
for x being object st x in dom b holds f.x = F(x) from
FUNCT_1:sch 3;
reconsider f as FinSequence by A9,A16,FINSEQ_1:def 2;
rng f c= TS(D)
proof
let x be object;
A17: rng O c= the carrier of S by FINSEQ_1:def 4;
assume x in rng f;
then consider y be object such that
A18: y in dom f and
A19: f.y = x by FUNCT_1:def 3;
dom O = Seg len O by FINSEQ_1:def 3;
then
A20: O.y in rng O by A9,A16,A18,FUNCT_1:def 3;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).(O.y) in rng coprod(X) by A20,A17,FUNCT_1:def 3;
then
A21: coprod(O.y,X) in rng coprod(X) by A20,A17,Def3;
b.y in rng b by A16,A18,FUNCT_1:def 3;
then reconsider a = b.y as Symbol of D by A10;
P[y,b.y] by A9,A16,A18;
then b.y in union rng coprod(X) by A21,TARSKI:def 4;
then
A22: a in Terminals D by A1,CARD_3:def 4;
x = root-tree(b.y) by A16,A18,A19;
hence thesis by A22,DTCONSTR:def 1;
end;
then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4;
A23: for x being object st x in dom b holds (roots f).x = b.x
proof
let x be object;
assume
A24: x in dom b;
then reconsider i = x as Nat;
f.x = root-tree (b.x) & ex T be DecoratedTree st T = f.i & (roots
f).i = T .{} by A16,A24,TREES_3:def 18;
hence thesis by TREES_4:3;
end;
A25: now
let c be set;
assume
A26: c in dom b;
dom O = Seg len O by FINSEQ_1:def 3;
then
A27: O.c in rng O by A9,A26,FUNCT_1:def 3;
A28: rng O c= the carrier of S by FINSEQ_1:def 4;
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).(O.c) in rng coprod(X) by A27,A28,FUNCT_1:def 3;
then
A29: coprod(O.c,X) in rng coprod(X) by A27,A28,Def3;
P[c,b.c] by A9,A26;
then b.c in union rng coprod(X) by A29,TARSKI:def 4;
then b.c in Union coprod(X) by CARD_3:def 4;
hence
b.c in [:the carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = b.c holds the_result_sort_of o1 = O.
c by A3,XBOOLE_0:3;
assume b.c in Union (coprod X);
thus b.c in coprod(O.c,X) by A9,A26;
end;
the carrier of S = x2 & len b = len O by A9,FINSEQ_1:def 3,TARSKI:def 1;
then [nt,b] in REL(X) by A4,A25,Th5;
then
A30: nt ==> b by LANG1:def 1;
take f;
dom (roots f) = dom f by TREES_3:def 18;
hence thesis by A30,A16,A23,FUNCT_1:2;
end;
hence thesis by A1,A2,DTCONSTR:def 3,def 4,def 5;
end;
end;
theorem Th7:
for S be non void non empty ManySortedSign, X be ManySortedSet of
the carrier of S, t be set holds (t in Terminals DTConMSA(X) & X is non-empty
implies ex s be SortSymbol of S, x be set st x in X.s & t = [x,s]) & for s be
SortSymbol of S, x be set st x in X.s holds [x,s] in Terminals DTConMSA(X)
proof
let S be non void non empty ManySortedSign, X be ManySortedSet of the
carrier of S, t be set;
set D = DTConMSA(X);
A1: Union (coprod X) c= Terminals (DTConMSA(X)) by Th6;
A2: Union (coprod X) = union rng (coprod X) by CARD_3:def 4;
thus t in Terminals D & X is non-empty implies ex s be SortSymbol of S, x be
set st x in X.s & t = [x,s]
proof
assume that
A3: t in Terminals D and
A4: X is non-empty;
Terminals D = Union (coprod X) by A4,Th6;
then consider A be set such that
A5: t in A and
A6: A in rng(coprod X) by A2,A3,TARSKI:def 4;
consider s be object such that
A7: s in dom (coprod X) and
A8: (coprod X).s = A by A6,FUNCT_1:def 3;
reconsider s as SortSymbol of S by A7;
(coprod X).s = coprod(s,X) by Def3;
then consider x be set such that
A9: x in X.s & t = [x,s] by A5,A8,Def2;
take s;
take x;
thus thesis by A9;
end;
let s be SortSymbol of S, x be set such that
A10: x in X.s;
set t = [x,s];
dom(coprod X) = the carrier of S by PARTFUN1:def 2;
then
A11: (coprod X).s in rng (coprod X) by FUNCT_1:def 3;
t in coprod(s,X) by A10,Def2;
then t in (coprod X).s by Def3;
then t in Union (coprod X) by A2,A11,TARSKI:def 4;
hence thesis by A1;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, o be OperSymbol of S;
func Sym(o,X) ->Symbol of DTConMSA(X) equals
[o,the carrier of S];
coherence
proof
the carrier of S in {the carrier of S} by TARSKI:def 1;
then [o,the carrier of S] in [:the carrier' of S,{the carrier of S}:] by
ZFMISC_1:87;
then [o,the carrier of S] in NonTerminals (DTConMSA X) by Th6;
hence thesis;
end;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, s be SortSymbol of S;
func FreeSort(X,s) -> Subset of TS(DTConMSA(X)) equals
{a where a is Element
of TS(DTConMSA(X)): (ex x be set st x in X.s & a = root-tree [x,s]) or ex o be
OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = s};
coherence
proof
set A = {a where a is Element of TS(DTConMSA(X)): (ex x be set st x in X.s
& a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a.
{} & the_result_sort_of o = s};
A c= TS(DTConMSA(X))
proof
let x be object;
assume x in A;
then
ex a be Element of TS(DTConMSA(X)) st x = a &( (ex x be set st x in X
.s & a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] =
a.{} & the_result_sort_of o = s);
hence thesis;
end;
hence thesis;
end;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, s be SortSymbol of S;
cluster FreeSort(X,s) -> non empty;
coherence
proof
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3;
then
A1: coprod(s,X) in rng coprod(X) by Def3;
set A = {a where a is Element of TS(DTConMSA(X)): (ex x be set st x in X.s
& a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a.
{} & the_result_sort_of o = s};
consider x be object such that
A2: x in X.s by XBOOLE_0:def 1;
set a = [x,s];
A3: (Terminals (DTConMSA(X))) = Union (coprod X) by Th6;
a in coprod(s,X) by A2,Def2;
then a in union rng coprod(X) by A1,TARSKI:def 4;
then
A4: a in Terminals (DTConMSA X) by A3,CARD_3:def 4;
then reconsider a as Symbol of DTConMSA(X);
reconsider b = root-tree a as Element of TS(DTConMSA X) by A4,
DTCONSTR:def 1;
b in A by A2;
hence thesis;
end;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
func FreeSort(X) -> ManySortedSet of the carrier of S means
:Def11:
for s be SortSymbol of S holds it.s = FreeSort(X,s);
existence
proof
deffunc F(Element of S)=FreeSort(X,$1);
consider f be Function such that
A1: dom f = the carrier of S & for d be Element of S holds f.d =F(d)
from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2
,RELAT_1:def 18;
take f;
thus thesis by A1;
end;
uniqueness
proof
let A,B be ManySortedSet of the carrier of S;
assume that
A2: for s be SortSymbol of S holds A.s = FreeSort(X,s) and
A3: for s be SortSymbol of S holds B.s = FreeSort(X,s);
for i be object st i in the carrier of S holds A.i = B.i
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A.s = FreeSort(X,s) by A2;
hence thesis by A3;
end;
hence thesis;
end;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
cluster FreeSort(X) -> non-empty;
coherence
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
(FreeSort(X)).s = FreeSort(X,s) by Def11;
hence thesis;
end;
end;
theorem Th8:
for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S, o be OperSymbol of S, x be set st x in ((
FreeSort X)# * (the Arity of S)).o holds x is FinSequence of TS(DTConMSA(X))
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, o be OperSymbol of S, x be set;
set D = DTConMSA(X), ar = the_arity_of o, cr = the carrier of S;
A1: (the Arity of S).o = ar by MSUALG_1:def 1;
rng ar c= cr & dom ((FreeSort X)) = cr by FINSEQ_1:def 4,PARTFUN1:def 2;
then
A2: dom ((FreeSort X) * ar) = dom ar by RELAT_1:27;
assume x in ((FreeSort X)# * (the Arity of S)).o;
then x in product ((FreeSort X) * ar) by A1,Th1;
then consider f be Function such that
A3: x = f and
A4: dom f = dom ((FreeSort X) * ar) and
A5: for y be object st y in dom ((FreeSort X)* ar) holds f.y in ((FreeSort
X) * ar).y by CARD_3:def 5;
dom ar = Seg len ar by FINSEQ_1:def 3;
then reconsider f as FinSequence by A4,A2,FINSEQ_1:def 2;
rng f c= TS D
proof
let a be object;
assume a in rng f;
then consider b be object such that
A6: b in dom f and
A7: f.b = a by FUNCT_1:def 3;
A8: a in ((FreeSort X) * ar).b by A4,A5,A6,A7;
reconsider b as Nat by A6;
((FreeSort X) * ar).b = (FreeSort X).(ar.b) by A4,A6,FUNCT_1:12
.= (FreeSort X). (ar/.b) by A4,A2,A6,PARTFUN1:def 6
.= FreeSort(X,ar/.b) by Def11
.= { s where s is Element of TS D: (ex x be set st x in X.(ar/.b) & s
= root-tree [x,ar/.b]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = s
.{} & the_result_sort_of o1=ar/.b};
then
ex e be Element of TS D st a = e &( (ex x be set st x in X.(ar/.b) & e
= root-tree [x,(ar/.b)]) or ex o be OperSymbol of S st [o,the carrier of S] = e
.{} & the_result_sort_of o=ar/.b) by A8;
hence thesis;
end;
then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4;
f = x by A3;
hence thesis;
end;
theorem Th9:
for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S, o be OperSymbol of S, p be FinSequence of TS
(DTConMSA(X)) holds p in ((FreeSort X)# * (the Arity of S)).o iff dom p = dom (
the_arity_of o) & for n be Nat st n in dom p holds p.n in FreeSort(X,(
the_arity_of o)/.n)
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, o be OperSymbol of S, p be FinSequence of TS(DTConMSA(X));
set AR = the Arity of S, cr = the carrier of S, ar = the_arity_of o;
thus p in ((FreeSort X)# * AR).o implies dom p = dom (the_arity_of o) & for
n be Nat st n in dom p holds p.n in FreeSort(X,(the_arity_of o)/.n)
proof
A1: AR.o = ar by MSUALG_1:def 1;
A2: rng ar c= cr & dom ((FreeSort X)) = cr by FINSEQ_1:def 4,PARTFUN1:def 2;
then
A3: dom ((FreeSort X) * ar) = dom ar by RELAT_1:27;
assume p in ((FreeSort X)# * (the Arity of S)).o;
then
A4: p in product ((FreeSort X) * ar) by A1,Th1;
then
A5: dom p = dom ((FreeSort X) * ar) by CARD_3:9;
hence dom p = dom ar by A2,RELAT_1:27;
let n be Nat;
assume
A6: n in dom p;
then ((FreeSort X) * ar).n = (FreeSort X).(ar.n) by A5,FUNCT_1:12
.= (FreeSort X). (ar/.n) by A5,A3,A6,PARTFUN1:def 6
.= FreeSort(X,ar/.n) by Def11;
hence thesis by A4,A5,A6,CARD_3:9;
end;
assume that
A7: dom p = dom (the_arity_of o) and
A8: for n be Nat st n in dom p holds p.n in FreeSort(X,(the_arity_of o) /.n);
rng ar c= cr & dom ((FreeSort X)) = cr by FINSEQ_1:def 4,PARTFUN1:def 2;
then
A9: dom p = dom ((FreeSort X) * ar) by A7,RELAT_1:27;
A10: for x be object st x in dom((FreeSort X) * ar) holds p.x in ((FreeSort X)
* ar).x
proof
let x be object;
assume
A11: x in dom ((FreeSort X) * ar);
then reconsider n = x as Nat;
FreeSort(X,ar/.n) = (FreeSort X). (ar/.n) by Def11
.= (FreeSort X).(ar.n) by A7,A9,A11,PARTFUN1:def 6
.= ((FreeSort X) * ar).x by A11,FUNCT_1:12;
hence thesis by A8,A9,A11;
end;
AR.o = ar by MSUALG_1:def 1;
then ((FreeSort X)# * AR).o = product ((FreeSort X) * ar) by Th1;
hence thesis by A9,A10,CARD_3:9;
end;
theorem Th10:
for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S, o be OperSymbol of S, p be FinSequence of TS
(DTConMSA(X)) holds Sym(o,X) ==> roots p iff p in ((FreeSort X)# * (the Arity
of S)).o
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, o be OperSymbol of S, p be FinSequence of TS(DTConMSA(X));
set D = DTConMSA(X), ar = the_arity_of o;
set r = roots p, OU = [:the carrier' of S,{the carrier of S}:] \/ Union (
coprod X);
A1: dom p = dom r by TREES_3:def 18;
thus Sym(o,X) ==> roots p implies p in ((FreeSort X)# * (the Arity of S)).o
proof
assume Sym(o,X) ==> roots p;
then
A2: [[o,the carrier of S],roots p] in REL(X) by LANG1:def 1;
then reconsider
r = roots p as Element of ([:the carrier' of S,{the carrier of
S}:] \/ Union (coprod X))* by ZFMISC_1:87;
A3: dom p = dom r by TREES_3:def 18;
A4: dom r = Seg len r & Seg len ar = dom ar by FINSEQ_1:def 3;
A5: len r = len ar by A2,Th5;
for n be Nat st n in dom p holds p.n in FreeSort(X,ar/.n)
proof
let n be Nat;
set s = ar/.n;
assume
A6: n in dom p;
then consider T be DecoratedTree such that
A7: T = p.n and
A8: r.n = T.{} by TREES_3:def 18;
rng p c= TS D & p.n in rng p by A6,FINSEQ_1:def 4,FUNCT_1:def 3;
then reconsider T as Element of TS(D) by A7;
A9: rng r c= [:the carrier' of S,{the carrier of S}:] \/ Union (coprod
X) & r.n in rng r by A3,A6,FINSEQ_1:def 4,FUNCT_1:def 3;
per cases by A9,XBOOLE_0:def 3;
suppose
A10: r.n in [:the carrier' of S,{the carrier of S}:];
then consider
o1 being OperSymbol of S, x2 being Element of {the carrier of
S} such that
A11: r.n = [o1,x2] by DOMAIN_1:1;
A12: x2 = the carrier of S by TARSKI:def 1;
then the_result_sort_of o1 = ar.n by A2,A3,A6,A10,A11,Th5
.= ar/.n by A5,A3,A4,A6,PARTFUN1:def 6;
then (ex x be set st x in X.s & T = root-tree [x,s]) or ex o be
OperSymbol of S st [o,the carrier of S] = T.{} & the_result_sort_of o = s by A8
,A11,A12;
hence thesis by A7;
end;
suppose
A13: r.n in Union (coprod X);
then r.n in coprod(ar.n,X) by A2,A3,A6,Th5;
then r.n in coprod(s,X) by A5,A3,A4,A6,PARTFUN1:def 6;
then
A14: ex a be set st a in X.s & r.n = [a,s] by Def2;
reconsider t = r.n as Terminal of D by A13,Th6;
T = root-tree t by A8,DTCONSTR:9;
hence thesis by A7,A14;
end;
end;
hence thesis by A5,A3,A4,Th9;
end;
A15: dom r = Seg len r by FINSEQ_1:def 3;
reconsider r as FinSequence of OU;
reconsider r as Element of OU* by FINSEQ_1:def 11;
assume
A16: p in ((FreeSort X)# * (the Arity of S)).o;
then
A17: dom p = dom ar by Th9;
A18: Union (coprod X) misses [:the carrier' of S,{the carrier of S}:] by Th4;
A19: for x be set st x in dom r holds (r.x in [:the carrier' of S,{the
carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = r.
x holds the_result_sort_of o1 = ar.x) & (r.x in Union (coprod X) implies r.x in
coprod(ar.x,X))
proof
let x be set;
assume
A20: x in dom r;
then reconsider n = x as Nat;
A21: ex T be DecoratedTree st T = p.n & r.n = T.{} by A1,A20,TREES_3:def 18;
set s = ar/.n;
p.n in FreeSort(X,s) by A16,A1,A20,Th9;
then consider a be Element of TS D such that
A22: a = p.n and
A23: (ex x be set st x in X.s & a = root-tree [x,s]) or ex o be
OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = s;
A24: s = ar.n by A17,A1,A20,PARTFUN1:def 6;
thus r.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = r.x holds the_result_sort_of o1 = ar
.x
proof
assume
A25: r.x in [:the carrier' of S,{the carrier of S}:];
A26: now
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3;
then
A27: coprod(s,X) in rng coprod(X) by Def3;
given y be set such that
A28: y in X.s & a = root-tree [y,s];
r.x = [y,s] & [y,s] in coprod(s,X) by A22,A21,A28,Def2,TREES_4:3;
then r.x in union rng coprod(X) by A27,TARSKI:def 4;
then r.x in Union (coprod X) by CARD_3:def 4;
hence contradiction by A18,A25,XBOOLE_0:3;
end;
let o1 be OperSymbol of S;
assume [o1,the carrier of S] = r.x;
hence thesis by A22,A23,A21,A24,A26,XTUPLE_0:1;
end;
assume
A29: r.x in Union (coprod X);
now
given o1 be OperSymbol of S such that
A30: [o1,the carrier of S] = a.{} and
the_result_sort_of o1 = s;
the carrier of S in {the carrier of S} by TARSKI:def 1;
then [o1,the carrier of S] in [:the carrier' of S,{the carrier of S}:]
by ZFMISC_1:87;
hence contradiction by A18,A22,A21,A29,A30,XBOOLE_0:3;
end;
then consider y be set such that
A31: y in X.s and
A32: a = root-tree [y,s] by A23;
r.x = [y,s] by A22,A21,A32,TREES_4:3;
hence thesis by A24,A31,Def2;
end;
len r = len ar by A17,A1,A15,FINSEQ_1:def 3;
then [[o,the carrier of S],r] in REL X by A19,Th5;
hence thesis by LANG1:def 1;
end;
theorem Th11:
for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S holds union rng (FreeSort X) = TS (DTConMSA(X
))
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
set D = DTConMSA(X);
A1: dom (FreeSort X) = the carrier of S by PARTFUN1:def 2;
thus union rng (FreeSort X) c= TS D
proof
let x be object;
assume x in union rng (FreeSort X);
then consider A be set such that
A2: x in A and
A3: A in rng (FreeSort X) by TARSKI:def 4;
consider s be object such that
A4: s in dom (FreeSort X) and
A5: (FreeSort X).s = A by A3,FUNCT_1:def 3;
reconsider s as SortSymbol of S by A4;
A = FreeSort(X,s) by A5,Def11
.= {a where a is Element of TS(D): (ex x be set st x in X.s & a =
root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} &
the_result_sort_of o1 = s};
then ex a be Element of TS(D) st a = x &( (ex x be set st x in X.s & a =
root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] =a.{} &
the_result_sort_of o1 = s) by A2;
hence thesis;
end;
let x be object;
assume x in TS D;
then reconsider t = x as Element of TS(D);
A6: rng t c= the carrier of D & the carrier of D = (Terminals D) \/ (
NonTerminals D) by LANG1:1,RELAT_1:def 19;
{} in dom t by TREES_1:22;
then
A7: t.{} in rng t by FUNCT_1:def 3;
A8: NonTerminals D = [:the carrier' of S,{the carrier of S}:] by Th6;
A9: Terminals D = Union (coprod X) by Th6;
per cases by A7,A6,XBOOLE_0:def 3;
suppose
A10: t.{} in Terminals D;
then reconsider a = t.{} as Terminal of D;
a in union rng(coprod X) by A9,A10,CARD_3:def 4;
then consider A be set such that
A11: a in A and
A12: A in rng(coprod X) by TARSKI:def 4;
consider s be object such that
A13: s in dom(coprod X) and
A14: (coprod X).s = A by A12,FUNCT_1:def 3;
reconsider s as SortSymbol of S by A13;
A = coprod(s,X) by A14,Def3;
then t = root-tree a & ex b be set st b in X.s & a = [b,s] by A11,Def2,
DTCONSTR:9;
then t in FreeSort(X,s);
then
A15: t in (FreeSort X).s by Def11;
(FreeSort X).s in rng (FreeSort X) by A1,FUNCT_1:def 3;
hence thesis by A15,TARSKI:def 4;
end;
suppose
t.{} in NonTerminals D;
then reconsider a = t.{} as NonTerminal of D;
consider o being OperSymbol of S, x2 being Element of {the carrier of S}
such that
A16: a = [o,x2] by A8,DOMAIN_1:1;
set rs = the_result_sort_of o;
x2 = the carrier of S by TARSKI:def 1;
then t in FreeSort(X,rs) by A16;
then
A17: t in (FreeSort X).rs by Def11;
(FreeSort X).rs in rng (FreeSort X) by A1,FUNCT_1:def 3;
hence thesis by A17,TARSKI:def 4;
end;
end;
theorem Th12:
for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S, s1,s2 be SortSymbol of S st s1 <> s2 holds (
FreeSort X).s1 misses (FreeSort X).s2
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, s1,s2 be SortSymbol of S;
assume that
A1: s1 <> s2 and
A2: (FreeSort X).s1 /\ (FreeSort X).s2 <> {};
consider x being object such that
A3: x in (FreeSort X).s1 /\ (FreeSort X).s2 by A2,XBOOLE_0:def 1;
set D = DTConMSA(X);
A4: (FreeSort X).s1 = FreeSort(X,s1) by Def11;
A5: (FreeSort X).s2 = FreeSort(X,s2) by Def11;
x in (FreeSort X).s2 by A3,XBOOLE_0:def 4;
then consider b be Element of TS D such that
A6: b = x and
A7: (ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2]) or ex o2 be
OperSymbol of S st [o2,the carrier of S]=b.{} & the_result_sort_of o2 = s2
by A5;
x in (FreeSort X).s1 by A3,XBOOLE_0:def 4;
then consider a be Element of TS D such that
A8: a = x and
A9: (ex x1 be set st x1 in X.s1 & a = root-tree [x1,s1]) or ex o1 be
OperSymbol of S st [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s1
by A4;
per cases by A9;
suppose
ex x1 be set st x1 in X.s1 & a = root-tree [x1,s1];
then consider x1 be set such that
x1 in X.s1 and
A10: a = root-tree [x1,s1];
now
per cases by A7;
case
ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2];
then consider x2 be set such that
x2 in X.s2 and
A11: b = root-tree [x2,s2];
[x1,s1] = [x2,s2] by A8,A6,A10,A11,TREES_4:4;
hence contradiction by A1,XTUPLE_0:1;
end;
case
ex o2 be OperSymbol of S st [o2,the carrier of S]=b.{} &
the_result_sort_of o2 = s2;
then consider o2 be OperSymbol of S such that
A12: [o2,the carrier of S] = b.{} and
the_result_sort_of o2 = s2;
[o2,the carrier of S] = [x1,s1] by A8,A6,A10,A12,TREES_4:3;
then
A13: the carrier of S = s1 by XTUPLE_0:1;
for X be set holds not X in X;
hence contradiction by A13;
end;
end;
hence contradiction;
end;
suppose
ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} &
the_result_sort_of o1 = s1;
then consider o1 be OperSymbol of S such that
A14: [o1,the carrier of S] = a.{} and
A15: the_result_sort_of o1 = s1;
now
per cases by A7;
case
ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2];
then consider x2 be set such that
x2 in X.s2 and
A16: b = root-tree [x2,s2];
[o1,the carrier of S] = [x2,s2] by A8,A6,A14,A16,TREES_4:3;
then
A17: the carrier of S = s2 by XTUPLE_0:1;
for X be set holds not X in X;
hence contradiction by A17;
end;
case
ex o2 be OperSymbol of S st [o2,the carrier of S]=b.{} &
the_result_sort_of o2 = s2;
hence contradiction by A1,A8,A6,A14,A15,XTUPLE_0:1;
end;
end;
hence contradiction;
end;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, o be OperSymbol of S;
func DenOp(o,X) -> Function of ((FreeSort X)# * (the Arity of S)).o, ((
FreeSort X) * (the ResultSort of S)).o means
:Def12:
for p be FinSequence of TS
(DTConMSA(X)) st Sym(o,X) ==> roots p holds it.p = (Sym(o,X))-tree p;
existence
proof
set AL = ((FreeSort X)# * (the Arity of S)).o, AX = ((FreeSort X) * (the
ResultSort of S)).o, D = DTConMSA(X), O = the carrier' of S, rs =
the_result_sort_of o, RS = the ResultSort of S;
defpred P[object,object] means
for p be FinSequence of TS D st p = $1 holds $2 =
(Sym(o,X))-tree p;
A1: for x be object st x in AL ex y be object st y in AX & P[x,y]
proof
let x be object;
assume
A2: x in AL;
then reconsider p = x as FinSequence of TS(D) by Th8;
Sym(o,X) ==> roots p by A2,Th10;
then reconsider a = (Sym(o,X))-tree p as Element of TS D by
DTCONSTR:def 1;
take y = (Sym(o,X))-tree p;
o in O;
then o in dom ((FreeSort X) * RS) by PARTFUN1:def 2;
then
A3: AX =(FreeSort X).(RS.o) by FUNCT_1:12
.= (FreeSort X).rs by MSUALG_1:def 2
.= FreeSort(X,rs) by Def11;
a.{} = Sym(o,X) by TREES_4:def 4;
hence y in AX by A3;
thus thesis;
end;
consider f be Function such that
A4: dom f = AL & rng f c= AX & for x be object st x in AL holds P[x,f.x]
from FUNCT_1:sch 6(A1);
reconsider g = f as Function of AL,rng f by A4,FUNCT_2:1;
reconsider g as Function of AL,AX by A4,FUNCT_2:2;
take g;
let p be FinSequence of TS D;
assume Sym(o,X) ==> roots p;
then p in AL by Th10;
hence thesis by A4;
end;
uniqueness
proof
set AL = ((FreeSort X)# * (the Arity of S)).o, AX = ((FreeSort X) * (the
ResultSort of S)).o, D = DTConMSA(X);
let f,g be Function of AL, AX;
assume that
A5: for p be FinSequence of TS D st Sym(o,X) ==> roots p holds f.p =
(Sym(o,X))-tree p and
A6: for p be FinSequence of TS D st Sym(o,X) ==> roots p holds g.p =
(Sym(o,X))-tree p;
A7: for x be object st x in AL holds f.x = g.x
proof
let x be object;
assume
A8: x in AL;
then reconsider p = x as FinSequence of TS(D) by Th8;
A9: Sym(o,X) ==> roots p by A8,Th10;
then f.p = (Sym(o,X))-tree p by A5;
hence thesis by A6,A9;
end;
thus thesis by A7;
end;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
func FreeOper(X) -> ManySortedFunction of (FreeSort X)# * (the Arity of S),
(FreeSort X) * (the ResultSort of S) means
:Def13:
for o be OperSymbol of S holds it.o = DenOp(o,X);
existence
proof
defpred P[object,object] means
for o be OperSymbol of S st $1 = o holds $2 =
DenOp(o,X);
set Y = the carrier' of S;
A1: for x be object st x in Y ex y be object st P[x,y]
proof
let x be object;
assume x in Y;
then reconsider o = x as OperSymbol of S;
take DenOp(o,X);
thus thesis;
end;
consider f be Function such that
A2: dom f = Y & for x be object st x in Y holds P[x,f.x] from CLASSES1:
sch 1( A1);
reconsider f as ManySortedSet of Y by A2,PARTFUN1:def 2,RELAT_1:def 18;
for x be object st x in dom f holds f.x is Function
proof
let x be object;
assume x in dom f;
then reconsider o = x as OperSymbol of S;
f.o = DenOp(o,X) by A2;
hence thesis;
end;
then reconsider f as ManySortedFunction of Y by FUNCOP_1:def 6;
for x be object st x in Y holds f.x is Function of ((FreeSort X)# * (the
Arity of S)).x, ((FreeSort X) * (the ResultSort of S)).x
proof
let x be object;
assume x in Y;
then reconsider o = x as OperSymbol of S;
f.o = DenOp(o,X) by A2;
hence thesis;
end;
then reconsider
f as ManySortedFunction of (FreeSort X)# * (the Arity of S), (
FreeSort X) * (the ResultSort of S) by PBOOLE:def 15;
take f;
let o be OperSymbol of S;
thus thesis by A2;
end;
uniqueness
proof
let A,B be ManySortedFunction of (FreeSort X)# * (the Arity of S), (
FreeSort X) * (the ResultSort of S);
assume that
A3: for o be OperSymbol of S holds A.o = DenOp(o,X) and
A4: for o be OperSymbol of S holds B.o = DenOp(o,X);
for i be object st i in the carrier' of S holds A.i = B.i
proof
let i be object;
assume i in the carrier' of S;
then reconsider s = i as OperSymbol of S;
A.s = DenOp(s,X) by A3;
hence thesis by A4;
end;
hence thesis;
end;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
func FreeMSA(X) -> MSAlgebra over S equals
MSAlgebra (# FreeSort(X),
FreeOper(X) #);
coherence;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
cluster FreeMSA(X) -> strict non-empty;
coherence by MSUALG_1:def 3;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, s be SortSymbol of S;
func FreeGen(s,X) -> Subset of (FreeSort(X)).s means
:Def15:
for x be set holds x in it iff ex a be set st a in X.s & x = root-tree [a,s];
existence
proof
defpred P[object] means ex a be set st a in X.s & $1 = root-tree [a,s];
set D = DTConMSA(X);
consider A be set such that
A1: for x being object holds x in A iff x in (FreeSort(X)).s & P[x]
from XBOOLE_0:
sch 1;
A c= (FreeSort(X)).s
by A1;
then reconsider A as Subset of (FreeSort(X)).s;
for x holds x in A iff P[x]
proof
dom coprod(X) = the carrier of S by PARTFUN1:def 2;
then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3;
then
A2: coprod(s,X) in rng coprod(X) by Def3;
A3: Terminals D = Union (coprod X) by Th6;
let x;
thus x in A implies P[x] by A1;
set A = {aa where aa is Element of TS(D): (ex x be set st x in X.s & aa
= root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = aa.{}
& the_result_sort_of o1 = s};
assume
A4: P[x];
then consider a be set such that
A5: a in X.s and
A6: x = root-tree [a,s];
A7: (FreeSort X).s = FreeSort(X,s) by Def11;
set sa = [a,s];
sa in coprod(s,X) by A5,Def2;
then sa in union rng coprod(X) by A2,TARSKI:def 4;
then
A8: sa in Terminals D by A3,CARD_3:def 4;
then reconsider sa as Symbol of D;
reconsider b = root-tree sa as Element of TS(D) by A8,DTCONSTR:def 1;
b in A by A5;
hence thesis by A1,A4,A6,A7;
end;
hence thesis;
end;
uniqueness
proof
let A,B be Subset of (FreeSort(X)).s;
assume that
A9: for x be set holds x in A iff ex a be set st a in X.s & x =
root-tree [a,s] and
A10: for x be set holds x in B iff ex a be set st a in X.s & x =
root-tree [a,s];
thus A c= B
proof
let x be object;
assume x in A;
then ex a be set st a in X.s & x = root-tree [a,s] by A9;
hence thesis by A10;
end;
let x be object;
assume x in B;
then ex a be set st a in X.s & x = root-tree [a,s] by A10;
hence thesis by A9;
end;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, s be SortSymbol of S;
cluster FreeGen(s,X) -> non empty;
coherence
proof
consider x being object such that
A1: x in X.s by XBOOLE_0:def 1;
ex a be set st a in X.s & root-tree [x,s] = root-tree [a,s] by A1;
hence thesis by Def15;
end;
end;
theorem Th13:
for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S, s be SortSymbol of S holds FreeGen(s,X) = {
root-tree t where t is Symbol of DTConMSA(X): t in Terminals DTConMSA(X) & t`2
= s}
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, s be SortSymbol of S;
set D = DTConMSA(X), A = {root-tree t where t is Symbol of D : t in
Terminals D & t`2 = s};
thus FreeGen(s,X) c= A
proof
let x be object;
assume x in FreeGen(s,X);
then consider a be set such that
A1: a in X.s and
A2: x = root-tree [a,s] by Def15;
A3: [a,s] in Terminals D by A1,Th7;
then reconsider t = [a,s] as Symbol of D;
t`2 = s;
hence thesis by A2,A3;
end;
let x be object;
assume x in A;
then consider t be Symbol of D such that
A4: x = root-tree t and
A5: t in Terminals D and
A6: t`2 = s;
consider s1 be SortSymbol of S, a be set such that
A7: a in X.s1 and
A8: t = [a,s1] by A5,Th7;
s = s1 by A6,A8;
hence thesis by A4,A7,A8,Def15;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
func FreeGen(X) -> GeneratorSet of FreeMSA(X) means
:Def16:
for s be SortSymbol of S holds it.s = FreeGen(s,X);
existence
proof
deffunc F(Element of S)=FreeGen($1,X);
set FM = FreeMSA(X), D = DTConMSA(X);
consider f be Function such that
A1: dom f = the carrier of S & for s be Element of S holds f.s = F(s)
from FUNCT_1:sch 4;
reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2
,RELAT_1:def 18;
f c= the Sorts of FM
proof
let x be object;
assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
f.s = FreeGen(s,X) by A1;
hence thesis;
end;
then reconsider f as MSSubset of FM by PBOOLE:def 18;
the Sorts of GenMSAlg(f) = the Sorts of FM
proof
defpred P[set] means $1 in union rng (the Sorts of GenMSAlg(f));
the Sorts of GenMSAlg(f) is MSSubset of FM by MSUALG_2:def 9;
then
A2: the Sorts of GenMSAlg(f) c= the Sorts of FM by PBOOLE:def 18;
A3: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==>
roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P
[t] holds P[nt-tree ts]
proof
set G = GenMSAlg(f), OU = [:the carrier' of S,{the carrier of S}:] \/
Union (coprod (X qua ManySortedSet of the carrier of S));
let nt be Symbol of D, ts be FinSequence of TS(D);
assume that
A4: nt ==> roots ts and
A5: for t being DecoratedTree of the carrier of D st t in rng ts
holds P[t];
reconsider sy = nt as Element of OU;
A6: [nt,roots ts] in the Rules of D by A4,LANG1:def 1;
then reconsider rt = roots ts as Element of OU* by ZFMISC_1:87;
[sy,rt] in REL(X) by A4,LANG1:def 1;
then sy in [:the carrier' of S,{the carrier of S}:] by Def7;
then consider
o being OperSymbol of S, x2 being Element of {the carrier of
S} such that
A7: sy = [o,x2] by DOMAIN_1:1;
set ar = the_arity_of o, rs = the_result_sort_of o;
A8: x2 = the carrier of S by TARSKI:def 1;
[nt,roots ts] in REL(X) by A4,LANG1:def 1;
then
A9: len rt = len ar by A7,A8,Th5;
reconsider B = the Sorts of G as MSSubset of FM by MSUALG_2:def 9;
A10: dom B = the carrier of S by PARTFUN1:def 2;
A11: dom (roots ts) = dom ts by TREES_3:def 18;
rng ar c= the carrier of S by FINSEQ_1:def 4;
then
A12: dom (B * ar) = dom ar by A10,RELAT_1:27;
A13: Seg len rt = dom rt & Seg len ar = dom ar by FINSEQ_1:def 3;
then
A14: dom ts = dom ar by A6,A7,A8,A11,Th5;
A15: for x being object st x in dom (B * ar) holds ts.x in (B * ar).x
proof
let x be object;
assume
A16: x in dom (B * ar);
then reconsider n = x as Nat;
A17: ts.n in rng ts by A12,A11,A9,A13,A16,FUNCT_1:def 3;
rng ts c= TS D by FINSEQ_1:def 4;
then reconsider T = ts.x as Element of TS(D) by A17;
P[T] by A5,A17;
then consider A be set such that
A18: T in A and
A19: A in rng (the Sorts of G) by TARSKI:def 4;
set b = ar/.n, A1 = {a where a is Element of TS D: (ex x be set st x
in X.b & a = root-tree [x,b]) or ex o be OperSymbol of S st [o,the carrier of S
] = a.{} & the_result_sort_of o = b};
A20: A1 = FreeSort(X,b) .= (FreeSort X).b by Def11;
A21: ex t be DecoratedTree st t = ts.n & rt.n = t.{} by A12,A11,A9,A13,A16
,TREES_3:def 18;
consider s be object such that
A22: s in dom(the Sorts of G) and
A23: (the Sorts of G).s = A by A19,FUNCT_1:def 3;
reconsider s as SortSymbol of S by A22;
A24: rng rt c= [:the carrier' of S,{the carrier of S}:] \/ Union (
coprod X) & rt. n in rng rt by A12,A9,A13,A16,FINSEQ_1:def 4,FUNCT_1:def 3;
A25: now
per cases by A24,XBOOLE_0:def 3;
suppose
A26: rt.n in [:the carrier' of S,{the carrier of S}:];
then consider o1 being OperSymbol of S, x2 being Element of {the
carrier of S} such that
A27: rt.n = [o1,x2] by DOMAIN_1:1;
A28: x2 = the carrier of S by TARSKI:def 1;
then
the_result_sort_of o1 = ar.n by A6,A7,A8,A12,A11,A14,A16,A26,A27
,Th5
.= b by A12,A16,PARTFUN1:def 6;
hence T in (FreeSort X).b by A20,A21,A27,A28;
end;
suppose
A29: rt.n in Union (coprod X);
then rt.n in coprod(ar.n,X) by A6,A7,A8,A12,A11,A14,A16,Th5;
then rt.n in coprod(b,X) by A12,A16,PARTFUN1:def 6;
then
A30: ex a be set st a in X.b & rt.n = [a,b] by Def2;
reconsider tt = rt.n as Terminal of D by A29,Th6;
T = root-tree tt by A21,DTCONSTR:9;
hence T in (FreeSort X).b by A20,A30;
end;
end;
A31: now
assume b <> s;
then
A32: (FreeSort X).s misses (FreeSort X).b by Th12;
(the Sorts of G).s c= (the Sorts of FM).s by A2;
hence contradiction by A18,A23,A25,A32,XBOOLE_0:3;
end;
(B * ar).x = B.(ar.n) by A16,FUNCT_1:12
.= B.(ar/.n) by A12,A16,PARTFUN1:def 6;
hence thesis by A18,A23,A31;
end;
set AR = the Arity of S, RS = the ResultSort of S, BH = B# * the Arity
of S, O = the carrier' of S;
A33: Den(o,FM) = (FreeOper X).o by MSUALG_1:def 6
.= DenOp(o,X) by Def13;
A34: Sym(o,X) = [o,the carrier of S] & nt = [o,the carrier of S] by A7,
TARSKI:def 1;
AR.o = ar by MSUALG_1:def 1;
then BH.o = product (B * ar) by Th1;
then
A35: ts in BH.o by A12,A11,A9,A13,A15,CARD_3:9;
dom DenOp(o,X) = ((FreeSort X)# * AR).o by FUNCT_2:def 1;
then ts in dom DenOp(o,X) by A4,A34,Th10;
then ts in (dom DenOp(o,X)) /\ (BH.o) by A35,XBOOLE_0:def 4;
then
A36: ts in dom (DenOp(o,X) | (BH.o)) by RELAT_1:61;
then (DenOp(o,X) | (BH.o)).ts = (DenOp(o,X)).ts by FUNCT_1:47
.= nt-tree ts by A4,A34,Def12;
then
A37: nt-tree ts in rng ((Den(o,FM))|(BH.o)) by A33,A36,FUNCT_1:def 3;
RS.o = rs & dom (B * RS) = O by MSUALG_1:def 2,PARTFUN1:def 2;
then
A38: (B * RS).o = B.rs by FUNCT_1:12;
B is opers_closed by MSUALG_2:def 9;
then B is_closed_on o by MSUALG_2:def 6;
then
A39: rng ((Den(o,FM))|(BH.o)) c= (B * RS).o by MSUALG_2:def 5;
B.rs in rng B by A10,FUNCT_1:def 3;
hence thesis by A39,A37,A38,TARSKI:def 4;
end;
A40: for s be Symbol of D st s in Terminals D holds P[root-tree s]
proof
let t be Symbol of D;
assume t in Terminals D;
then t in Union (coprod X) by Th6;
then t in union rng(coprod X) by CARD_3:def 4;
then consider A be set such that
A41: t in A and
A42: A in rng (coprod X) by TARSKI:def 4;
consider s be object such that
A43: s in dom (coprod X) and
A44: (coprod X).s = A by A42,FUNCT_1:def 3;
reconsider s as SortSymbol of S by A43;
A = coprod(s,X) by A44,Def3;
then ex a be set st a in X.s & t = [a,s] by A41,Def2;
then
A45: root-tree t in FreeGen(s,X) by Def15;
f is MSSubset of GenMSAlg(f) by MSUALG_2:def 17;
then f c= the Sorts of GenMSAlg(f) by PBOOLE:def 18;
then f.s c= (the Sorts of GenMSAlg(f)).s;
then
A46: FreeGen(s,X) c= (the Sorts of GenMSAlg(f)).s by A1;
dom (the Sorts of GenMSAlg(f)) = the carrier of S by PARTFUN1:def 2;
then
(the Sorts of GenMSAlg(f)).s in rng (the Sorts of GenMSAlg(f)) by
FUNCT_1:def 3;
hence thesis by A46,A45,TARSKI:def 4;
end;
A47: for t being DecoratedTree of the carrier of D st t in TS D holds P[
t] from DTCONSTR:sch 7(A40,A3);
A48: union rng(the Sorts of FM) c= union rng (the Sorts of GenMSAlg(f))
proof
set D = DTConMSA(X);
let x be object;
assume x in union rng(the Sorts of FM);
then consider A be set such that
A49: x in A and
A50: A in rng(the Sorts of FM) by TARSKI:def 4;
consider s be object such that
A51: s in dom (FreeSort X) and
A52: (FreeSort X).s = A by A50,FUNCT_1:def 3;
reconsider s as SortSymbol of S by A51;
A = FreeSort(X,s) by A52,Def11
.= {a where a is Element of TS(D): (ex x be set st x in X.s & a =
root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} &
the_result_sort_of o1 = s};
then ex a be Element of TS(D) st a = x &( (ex x be set st x in X.s & a
= root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] =a.{} &
the_result_sort_of o1 = s) by A49;
hence thesis by A47;
end;
let x be Element of S;
reconsider s = x as SortSymbol of S;
thus (the Sorts of GenMSAlg(f)).x c= (the Sorts of FM).x
by A2;
let a be object;
assume
A53: a in (the Sorts of FM).x;
the carrier of S = dom (the Sorts of FM) by PARTFUN1:def 2;
then (the Sorts of FM).s in rng (the Sorts of FM) by FUNCT_1:def 3;
then a in union rng (the Sorts of FM) by A53,TARSKI:def 4;
then consider A be set such that
A54: a in A and
A55: A in rng (the Sorts of GenMSAlg(f)) by A48,TARSKI:def 4;
consider b be object such that
A56: b in dom (the Sorts of GenMSAlg(f)) and
A57: (the Sorts of GenMSAlg(f)).b = A by A55,FUNCT_1:def 3;
reconsider b as SortSymbol of S by A56;
now
assume b <> s;
then (FreeSort X).s misses (FreeSort X).b by Th12;
then
A58: (FreeSort X).s /\ (FreeSort X).b = {};
(the Sorts of GenMSAlg(f)).b c= (the Sorts of FM).b by A2;
hence contradiction by A53,A54,A57,A58,XBOOLE_0:def 4;
end;
hence thesis by A54,A57;
end;
then reconsider f as GeneratorSet of FM by Def4;
take f;
thus thesis by A1;
end;
uniqueness
proof
let A,B be GeneratorSet of FreeMSA(X);
assume that
A59: for s be SortSymbol of S holds A.s = FreeGen(s,X) and
A60: for s be SortSymbol of S holds B.s = FreeGen(s,X);
for i be object st i in the carrier of S holds A.i = B.i
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A.s = FreeGen(s,X) by A59;
hence thesis by A60;
end;
hence thesis;
end;
end;
theorem
for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S holds FreeGen(X)is non-empty
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
let x be object;
assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
(FreeGen(X)).s = FreeGen(s,X) by Def16;
hence thesis;
end;
theorem
for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S holds union rng FreeGen(X) = {root-tree t
where t is Symbol of DTConMSA(X): t in Terminals DTConMSA(X)}
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
set D = DTConMSA(X), A = union rng FreeGen(X), B = {root-tree t where t is
Symbol of D : t in Terminals D};
thus A c= B
proof
let x be object;
assume x in A;
then consider C be set such that
A1: x in C and
A2: C in rng FreeGen(X) by TARSKI:def 4;
consider s be object such that
A3: s in dom FreeGen(X) and
A4: (FreeGen(X)).s = C by A2,FUNCT_1:def 3;
reconsider s as SortSymbol of S by A3;
C = FreeGen(s,X) by A4,Def16
.= {root-tree t where t is Symbol of D : t in Terminals D & t`2 = s}
by Th13;
then
ex t be Symbol of D st x = root-tree t & t in Terminals D & t`2 = s by A1;
hence thesis;
end;
let x be object;
assume x in B;
then consider t be Symbol of D such that
A5: x = root-tree t and
A6: t in Terminals D;
consider s be SortSymbol of S, a be set such that
a in X.s and
A7: t = [a,s] by A6,Th7;
t`2 = s by A7;
then
x in {root-tree tt where tt is Symbol of D : tt in Terminals D & tt`2 =
s} by A5,A6;
then x in FreeGen(s,X) by Th13;
then
A8: x in (FreeGen(X)).s by Def16;
dom FreeGen(X) = the carrier of S by PARTFUN1:def 2;
then (FreeGen(X)).s in rng (FreeGen(X)) by FUNCT_1:def 3;
hence thesis by A8,TARSKI:def 4;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, s be SortSymbol of S;
func Reverse(s,X) -> Function of FreeGen(s,X),X.s means
:Def17:
for t be
Symbol of DTConMSA(X) st root-tree t in FreeGen(s,X) holds it.(root-tree t) = t
`1;
existence
proof
set A = FreeGen(s,X), D = DTConMSA(X);
defpred P[object,object] means
for t be Symbol of D st $1 = root-tree t holds $2
= t`1;
A1: for x be object st x in A ex a be object st a in X.s & P[x,a]
proof
let x be object;
assume x in A;
then
x in {root-tree t where t is Symbol of D: t in Terminals D & t`2 = s
} by Th13;
then consider t be Symbol of D such that
A2: x = root-tree t and
A3: t in Terminals D and
A4: t`2 = s;
consider s1 be SortSymbol of S, a be set such that
A5: a in X.s1 and
A6: t = [a,s1] by A3,Th7;
take a;
thus a in X.s by A4,A5,A6;
let t1 be Symbol of D;
assume x = root-tree t1;
then t = t1 by A2,TREES_4:4;
hence thesis by A6;
end;
consider f be Function such that
A7: dom f = A & rng f c= X.s & for x be object st x in A holds P[x,f.x]
from FUNCT_1:sch 6(A1);
reconsider f as Function of A,X.s by A7,FUNCT_2:2;
take f;
let t be Symbol of D;
assume root-tree t in A;
hence thesis by A7;
end;
uniqueness
proof
set D = DTConMSA(X), C = {root-tree t where t is Symbol of D : t in
Terminals D & t`2 = s};
let A,B be Function of FreeGen(s,X),X.s;
assume that
A8: for t be Symbol of DTConMSA(X) st root-tree t in FreeGen(s,X)
holds A.(root-tree t) = t`1 and
A9: for t be Symbol of DTConMSA(X) st root-tree t in FreeGen(s,X)
holds B.(root-tree t) = t`1;
A10: FreeGen(s,X) = C by Th13;
A11: for i be object st i in C holds A.i = B.i
proof
let i be object;
assume
A12: i in C;
then consider t be Symbol of D such that
A13: i = root-tree t and
t in Terminals D and
t`2 = s;
A.(root-tree t) = t`1 by A8,A10,A12,A13;
hence thesis by A9,A10,A12,A13;
end;
dom A = C & dom B = C by A10,FUNCT_2:def 1;
hence thesis by A11,FUNCT_1:2;
end;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
func Reverse(X) -> ManySortedFunction of FreeGen(X),X means
:Def18:
for s be SortSymbol of S holds it.s = Reverse(s,X);
existence
proof
defpred P[object,object] means
for s be SortSymbol of S st s = $1 holds $2 =
Reverse(s,X);
set I = the carrier of S, FG = FreeGen(X);
A1: for i be object st i in I ex u be object st P[i,u]
proof
let i be object;
assume i in I;
then reconsider s = i as SortSymbol of S;
take Reverse(s,X);
let s1 be SortSymbol of S;
assume s1 = i;
hence thesis;
end;
consider H be Function such that
A2: dom H = I & for i be object st i in I holds P[i,H.i] from CLASSES1:
sch 1 (A1);
reconsider H as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18;
for x be object st x in dom H holds H.x is Function
proof
let i be object;
assume i in dom H;
then reconsider s = i as SortSymbol of S;
H.s = Reverse(s,X) by A2;
hence thesis;
end;
then reconsider H as ManySortedFunction of I by FUNCOP_1:def 6;
for i be object st i in I holds H.i is Function of FG.i,X.i
proof
let i be object;
assume i in I;
then reconsider s = i as SortSymbol of S;
(FreeGen X).s = FreeGen(s,X) & H.i = Reverse(s,X) by A2,Def16;
hence thesis;
end;
then reconsider H as ManySortedFunction of FG,X by PBOOLE:def 15;
take H;
let s be SortSymbol of S;
thus thesis by A2;
end;
uniqueness
proof
let A,B be ManySortedFunction of FreeGen(X),X;
assume that
A3: for s be SortSymbol of S holds A.s = Reverse(s,X) and
A4: for s be SortSymbol of S holds B.s = Reverse(s,X);
for i be object st i in the carrier of S holds A.i = B.i
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
A.s = Reverse(s,X) by A3;
hence thesis by A4;
end;
hence thesis;
end;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, A be non-empty ManySortedSet of the carrier of S, F be
ManySortedFunction of FreeGen(X), A, t be Symbol of DTConMSA(X);
assume
A1: t in Terminals (DTConMSA(X));
func pi(F,A,t) -> Element of Union A means
:Def19:
for f be Function st f = F.(t`2) holds it = f.(root-tree t);
existence
proof
set FG = FreeGen(X), D = DTConMSA(X);
consider s be SortSymbol of S, x be set such that
x in X.s and
A2: t = [x,s] by A1,Th7;
FG.s = FreeGen(s,X) by Def16;
then
A3: dom (F.s) = FreeGen(s,X) by FUNCT_2:def 1
.= {root-tree tt where tt is Symbol of D: tt in Terminals D & tt`2 = s
} by Th13;
t`2 = s by A2;
then root-tree t in dom (F.s) by A1,A3;
then
A4: (F.s).(root-tree t) in rng (F.s) by FUNCT_1:def 3;
dom A = the carrier of S by PARTFUN1:def 2;
then rng (F.s) c= A.s & A.s in rng A by FUNCT_1:def 3,RELAT_1:def 19;
then (F.s).(root-tree t) in union rng A by A4,TARSKI:def 4;
then reconsider eu = (F.s).(root-tree t) as Element of Union A by
CARD_3:def 4;
take eu;
let f be Function;
assume f = F.(t`2);
hence thesis by A2;
end;
uniqueness
proof
consider s be SortSymbol of S, x be set such that
x in X.s and
A5: t = [x,s] by A1,Th7;
reconsider f = F.s as Function;
let a,b be Element of Union A;
assume that
A6: for f be Function st f = F.(t`2) holds a = f.(root-tree t) and
A7: for f be Function st f = F.(t`2) holds b = f.(root-tree t);
A8: f = F.(t`2) by A5;
then a = f.(root-tree t) by A6;
hence thesis by A7,A8;
end;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, t be Symbol of DTConMSA(X);
assume
A1: ex p be FinSequence st t ==> p;
func @(X,t) -> OperSymbol of S means
:Def20:
[it,the carrier of S] = t;
existence
proof
set D = DTConMSA(X), OU = [:the carrier' of S,{the carrier of S}:] \/
Union (coprod (X qua ManySortedSet of the carrier of S));
reconsider a = t as Element of OU;
consider p be FinSequence such that
A2: t ==> p by A1;
[t,p] in the Rules of D by A2,LANG1:def 1;
then reconsider p as Element of OU* by ZFMISC_1:87;
[a,p] in REL(X) by A2,LANG1:def 1;
then a in [:the carrier' of S,{the carrier of S}:] by Def7;
then consider
o being OperSymbol of S, x2 being Element of {the carrier of S}
such that
A3: a = [o,x2] by DOMAIN_1:1;
take o;
thus thesis by A3,TARSKI:def 1;
end;
uniqueness by XTUPLE_0:1;
end;
definition
let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S
, o be OperSymbol of S, p be FinSequence;
assume
A1: p in Args(o,U0);
func pi(o,U0,p) -> Element of Union (the Sorts of U0) equals
:Def21:
Den(o,
U0).p;
coherence
proof
set F = Den(o,U0), S0 = the Sorts of U0;
dom F = Args(o,U0) by FUNCT_2:def 1;
then rng F c= Result(o,U0) & F.p in rng F by A1,FUNCT_1:def 3
,RELAT_1:def 19;
then F.p in union rng S0 by TARSKI:def 4;
hence thesis by CARD_3:def 4;
end;
end;
theorem Th16:
for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S holds FreeGen(X) is free
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
set D = DTConMSA(X), FA = FreeMSA(X), FG = FreeGen(X);
let U1 be non-empty MSAlgebra over S, F be ManySortedFunction of FG,the
Sorts of U1;
set SA =the Sorts of FA, AR = the Arity of S, S1 = the Sorts of U1, O = the
carrier' of S, RS = the ResultSort of S, DU = Union (the Sorts of U1);
deffunc TermVal(Symbol of D) = pi(F,the Sorts of U1,$1);
deffunc NTermVal(Symbol of D, FinSequence, FinSequence) = pi(@(X,$1),U1,$3);
consider G being Function of TS(D), DU such that
A1: for t being Symbol of D st t in Terminals D holds G.(root-tree t) =
TermVal(t) and
A2: for nt be Symbol of D, ts be FinSequence of TS(D) st nt ==> roots ts
holds G.(nt-tree ts) = NTermVal(nt,roots ts,G * ts) from DTCONSTR:sch 8;
deffunc F(object) = G | ((the Sorts of FA).$1);
consider h be Function such that
A3: dom h = the carrier of S & for s be object st s in the carrier of S
holds h.s = F(s) from FUNCT_1:sch 3;
reconsider h as ManySortedSet of the carrier of S by A3,PARTFUN1:def 2
,RELAT_1:def 18;
for s be object st s in dom h holds h.s is Function
proof
let s be object;
assume s in dom h;
then h.s = G | ((the Sorts of FA).s) by A3;
hence thesis;
end;
then reconsider h as ManySortedFunction of the carrier of S by FUNCOP_1:def 6
;
defpred P[set] means for s be SortSymbol of S st $1 in (the Sorts of FA).s
holds (h.s).$1 in (the Sorts of U1).s;
A4: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots
ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P[t]
holds P[nt-tree ts]
proof
let nt be Symbol of D, ts be FinSequence of TS(D);
assume that
A5: nt ==> roots ts and
A6: for t being DecoratedTree of the carrier of D st t in rng ts holds P[t];
set p = G * ts, o = @(X,nt), ar = the_arity_of o, rs = the_result_sort_of
o, OU = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua
ManySortedSet of the carrier of S)), rt = roots ts;
A7: [o,the carrier of S] = nt by A5,Def20;
then
A8: [[o,the carrier of S],rt] in the Rules of D by A5,LANG1:def 1;
A9: [o,the carrier of S] = Sym(o,X);
then
A10: (DenOp(o,X)).ts = nt-tree ts by A5,A7,Def12;
dom (DenOp (o,X)) = ((FreeSort X)# * AR).o by FUNCT_2:def 1;
then ts in dom (DenOp(o,X)) by A5,A7,A9,Th10;
then
rng (DenOp (o,X)) c= ((FreeSort X) * RS).o & nt-tree ts in rng (DenOp
(o,X)) by A10,FUNCT_1:def 3,RELAT_1:def 19;
then
A11: nt-tree ts in (SA * RS).o;
set ppi = pi(o,U1,p);
A12: rng RS c= the carrier of S by RELAT_1:def 19;
A13: rng ar c= the carrier of S by FINSEQ_1:def 4;
reconsider rt as Element of OU* by A8,ZFMISC_1:87;
A14: len rt = len ar by A8,Th5;
A15: dom rt = Seg len rt by FINSEQ_1:def 3;
dom SA = the carrier of S by PARTFUN1:def 2;
then
A16: dom(SA* ar) = dom ar by A13,RELAT_1:27;
A17: ar = AR.o by MSUALG_1:def 1;
dom S1 = the carrier of S by PARTFUN1:def 2;
then
A18: dom(S1* ar) = dom ar by A13,RELAT_1:27;
A19: dom rt = dom ts & Seg len ar = dom ar by FINSEQ_1:def 3,TREES_3:def 18;
A20: dom p = dom ts by FINSEQ_3:120;
then
A21: dom p = dom (S1 * ar) by A18,A8,A15,A19,Th5;
A22: for x being object st x in dom (S1 * ar) holds p.x in (S1 * ar).x
proof
let x be object;
assume
A23: x in dom (S1 * ar);
then reconsider n = x as Nat;
A24: ts.n in rng ts by A18,A14,A15,A19,A23,FUNCT_1:def 3;
rng ts c= TS D by FINSEQ_1:def 4;
then reconsider t = ts.n as Element of TS(D) by A24;
A25: p.n = G.(ts.n) by A21,A23,FINSEQ_3:120;
ar.x in rng ar by A18,A23,FUNCT_1:def 3;
then reconsider s = ar.x as SortSymbol of S by A13;
A26: h.s = G | (SA.s) by A3;
dom SA = the carrier of S by PARTFUN1:def 2;
then
A27: SA.s in rng SA by FUNCT_1:def 3;
dom G = TS D by FUNCT_2:def 1
.= union rng SA by Th11;
then
A28: dom (h.s) = SA.s by A26,A27,RELAT_1:62,ZFMISC_1:74;
ts in ((FreeSort X)# * AR).o by A5,A7,A9,Th10;
then ts in product ((FreeSort X) * ar) by A17,Th1;
then ts.x in ((FreeSort X) * ar).x by A18,A16,A23,CARD_3:9;
then
A29: ts.x in (FreeSort X).(ar.x) by A18,A16,A23,FUNCT_1:12;
then (h.s).t in S1.s by A6,A24;
then G.t in S1.s by A29,A26,A28,FUNCT_1:47;
hence thesis by A23,A25,FUNCT_1:12;
end;
dom S1 = the carrier of S by PARTFUN1:def 2;
then
A30: dom (S1 *RS) = dom RS by A12,RELAT_1:27;
let s be SortSymbol of S;
A31: dom Den(o,U1) = Args(o,U1) by FUNCT_2:def 1;
A32: dom RS = O by FUNCT_2:def 1;
dom SA = the carrier of S by PARTFUN1:def 2;
then dom (SA * RS) = dom RS by A12,RELAT_1:27;
then nt-tree ts in SA.(RS.o) by A32,A11,FUNCT_1:12;
then
A33: nt-tree ts in SA.rs by MSUALG_1:def 2;
Args(o,U1) = (S1# * AR).o by MSUALG_1:def 4
.= product (S1 * ar) by A17,Th1;
then
A34: p in Args(o,U1) by A20,A18,A14,A15,A19,A22,CARD_3:9;
then pi(o,U1,p) = Den(o,U1).p by Def21;
then rng Den(o,U1) c= Result(o,U1) & ppi in rng Den(o,U1) by A34,A31,
FUNCT_1:def 3,RELAT_1:def 19;
then
A35: ppi in Result(o,U1);
assume
A36: nt-tree ts in SA.s;
A37: rs = s by A33,A36,XBOOLE_0:3,Th12;
G.(nt-tree ts) = ppi by A2,A5;
then
A38: ppi = (G | (SA.rs)).(nt-tree ts) by A33,FUNCT_1:49;
Result(o,U1) = (S1 *RS).o by MSUALG_1:def 5
.= S1.(RS.o) by A30,A32,FUNCT_1:12
.= S1.rs by MSUALG_1:def 2;
hence thesis by A3,A35,A38,A37;
end;
A39: for t being Symbol of D st t in Terminals D holds P[root-tree t]
proof
let t be Symbol of D;
assume
A40: t in Terminals D;
then consider s be SortSymbol of S, x be set such that
x in X.s and
A41: t = [x,s] by Th7;
set E = {root-tree tt where tt is Symbol of D: tt in Terminals D & tt`2 =
s}, a = root-tree t;
A42: t`2 = s by A41;
then
A43: a in E by A40;
let s1 be SortSymbol of S;
reconsider f = F.s as Function of FG.s,S1.s;
A44: dom f = FG.s by FUNCT_2:def 1;
A45: E = FreeGen(s,X) by Th13;
then FG.s = E by Def16;
then
A46: rng f c= S1.s & f.a in rng f by A43,A44,FUNCT_1:def 3,RELAT_1:def 19;
assume
A47: a in SA.s1;
A48: now
a in (FreeSort X).s /\ (FreeSort X).s1 by A43,A45,A47,XBOOLE_0:def 4;
then
A49: (FreeSort X).s meets (FreeSort X).s1;
assume s <> s1;
hence contradiction by A49,Th12;
end;
h.s = G | (SA.s) by A3;
then (h.s).a = G.a by A43,A45,FUNCT_1:49
.= pi(F,S1,t) by A1,A40
.= f.a by A40,A42,Def19;
hence thesis by A46,A48;
end;
A50: for t being DecoratedTree of the carrier of D st t in TS(D) holds P[t]
from DTCONSTR:sch 7(A39,A4);
for s be object st s in the carrier of S holds h.s is Function of (the
Sorts of FA).s, (the Sorts of U1).s
proof
let x be object;
assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
A51: dom G = TS D by FUNCT_2:def 1
.= union rng SA by Th11;
dom SA = the carrier of S by PARTFUN1:def 2;
then
A52: SA.s in rng SA by FUNCT_1:def 3;
A53: h.s = G | (SA.s) by A3;
then
A54: dom (h.s) = SA.s by A51,A52,RELAT_1:62,ZFMISC_1:74;
A55: SA.s c= dom G by A51,A52,ZFMISC_1:74;
rng (h.s) c= S1.s
proof
let a be object;
assume a in rng (h.s);
then consider T be object such that
A56: T in dom (h.s) and
A57: (h.s).T = a by FUNCT_1:def 3;
reconsider T as Element of TS(D) by A55,A54,A56,FUNCT_2:def 1;
T in SA.s by A53,A51,A52,A56,RELAT_1:62,ZFMISC_1:74;
hence thesis by A50,A57;
end;
hence thesis by A54,FUNCT_2:def 1,RELSET_1:4;
end;
then reconsider h as ManySortedFunction of FA,U1 by PBOOLE:def 15;
take h;
thus h is_homomorphism FA,U1
proof
rng RS c= the carrier of S & dom SA = the carrier of S by PARTFUN1:def 2
,RELAT_1:def 19;
then
A58: dom RS = O & dom (SA * RS) = dom RS by FUNCT_2:def 1,RELAT_1:27;
let o be OperSymbol of S such that
Args(o,FA) <> {};
let x be Element of Args(o,FA);
set rs = the_result_sort_of o, DA = Den(o,FA), D1 = Den(o,U1), OU = [:the
carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of the
carrier of S)), ar = the_arity_of o;
A59: ar = AR.o by MSUALG_1:def 1;
A60: Args(o,FA) = ((FreeSort X)# * AR).o by MSUALG_1:def 4;
then reconsider p = x as FinSequence of TS(D) by Th8;
A61: Sym(o,X) ==> roots p by A60,Th10;
then
A62: @(X,Sym(o,X)) = o by Def20;
A63: dom (G *p) = dom p by FINSEQ_3:120;
A64: x in ((FreeSort X)# * AR).o by A60;
A65: for a be object st a in dom p holds (G*p).a = (h#x).a
proof
rng ar c= the carrier of S & dom SA = the carrier of S by FINSEQ_1:def 4
,PARTFUN1:def 2;
then
A66: dom(SA* ar) = dom ar by RELAT_1:27;
set rt = roots p;
let a be object;
assume
A67: a in dom p;
then reconsider n = a as Nat;
A68: [[o,the carrier of S],rt] in the Rules of D by A61,LANG1:def 1;
then reconsider rt as Element of OU* by ZFMISC_1:87;
A69: len rt = len ar by A68,Th5;
A70: (G*p).n = G.(x.n) & (h#x).n = (h.(ar/.n)).(x.n) by A63,A67,FINSEQ_3:120
,MSUALG_3:def 6;
A71: h.(ar/.n) = G | (SA.(ar/.n)) by A3;
A72: Seg len rt = dom rt by FINSEQ_1:def 3;
A73: dom rt = dom p & Seg len ar = dom ar by FINSEQ_1:def 3,TREES_3:def 18;
p in product((FreeSort X) * ar) by A64,A59,Th1;
then
A74: p.n in ((FreeSort X) * ar).n by A67,A66,A69,A72,A73,CARD_3:9;
((FreeSort X) * ar).n = SA.(ar.n) by A67,A66,A69,A72,A73,FUNCT_1:12
.= SA.(ar/.n) by A67,A69,A72,A73,PARTFUN1:def 6;
hence thesis by A70,A71,A74,FUNCT_1:49;
end;
dom (h#x) = dom ar by MSUALG_3:6;
then
A75: G*p = h#x by A63,A65,FUNCT_1:2,MSUALG_3:6;
A76: h.rs = G | (SA.rs) by A3;
A77: dom (DenOp (o,X)) = ((FreeSort X)# * AR).o by FUNCT_2:def 1;
(DenOp(o,X)).p = (Sym(o,X))-tree p by A61,Def12;
then rng (DenOp (o,X)) c= ((FreeSort X) * RS).o & (Sym(o,X))-tree p in
rng (DenOp (o,X)) by A60,A77,FUNCT_1:def 3,RELAT_1:def 19;
then (Sym(o,X))-tree p in (SA * RS).o;
then (Sym(o,X))-tree p in SA.(RS.o) by A58,FUNCT_1:12;
then
A78: (Sym(o,X))-tree p in SA.rs by MSUALG_1:def 2;
dom SA = the carrier of S by PARTFUN1:def 2;
then
A79: SA.rs in rng SA by FUNCT_1:def 3;
dom G = TS D by FUNCT_2:def 1
.= union rng SA by Th11;
then
A80: dom (h.rs) = SA.rs by A76,A79,RELAT_1:62,ZFMISC_1:74;
DA = (FreeOper(X)).o by MSUALG_1:def 6
.= DenOp(o,X) by Def13;
then DA.x = (Sym(o,X))-tree p by A61,Def12;
hence (h.rs).(DA.x) = G.((Sym(o,X))-tree p) by A78,A76,A80,FUNCT_1:47
.= pi(@(X,Sym(o,X)),U1,G*p) by A2,A61
.= D1.(h#x) by A62,A75,Def21;
end;
for x being object st x in the carrier of S holds (h || FG).x = F.x
proof
set hf = h || FG;
let x be object;
assume x in the carrier of S;
then reconsider s = x as SortSymbol of S;
A81: dom (h.s) = SA.s by FUNCT_2:def 1;
A82: dom (hf.s) = FG.s by FUNCT_2:def 1;
A83: FG.s = FreeGen(s,X) by Def16;
A84: hf.s = (h.s) | (FG.s) by Def1;
A85: for a be object st a in FG.s holds (hf.s).a = (F.s).a
proof
let a be object;
A86: h.s = G | (SA.s) by A3;
assume
A87: a in FG.s;
then a in {root-tree t where t is Symbol of D: t in Terminals D & t`2 =
s } by A83,Th13;
then consider t be Symbol of D such that
A88: a = root-tree t & t in Terminals D and
A89: t`2 = s;
thus (hf.s).a = (h.s).a by A84,A82,A87,FUNCT_1:47
.= G.a by A81,A83,A87,A86,FUNCT_1:47
.= pi(F,S1,t) by A1,A88
.= (F.s).a by A88,A89,Def19;
end;
dom (F.s) = FG.s by FUNCT_2:def 1;
hence thesis by A82,A85,FUNCT_1:2;
end;
hence thesis;
end;
theorem Th17:
for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S holds FreeMSA(X) is free
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S;
take FreeGen(X);
thus thesis by Th16;
end;
registration
let S be non void non empty ManySortedSign;
cluster free strict for non-empty MSAlgebra over S;
existence
proof
set U1 = the non-empty MSAlgebra over S;
set X = the Sorts of U1;
take FreeMSA(X);
thus thesis by Th17;
end;
end;
registration
let S be non void non empty ManySortedSign, U0 be free MSAlgebra over S;
cluster free for GeneratorSet of U0;
existence by Def6;
end;
theorem Th18:
for S be non void non empty ManySortedSign, U1 be non-empty
MSAlgebra over S ex U0 be strict free non-empty MSAlgebra over S, F be
ManySortedFunction of U0,U1 st F is_epimorphism U0,U1
proof
let S be non void non empty ManySortedSign, U1 be non-empty MSAlgebra over S;
set S1 = the Sorts of U1, FA = FreeMSA(S1), FG = FreeGen(S1);
reconsider fa = FA as strict free non-empty MSAlgebra over S by Th17;
set f = Reverse(S1);
take fa;
FG is free by Th16;
then consider F be ManySortedFunction of FA,U1 such that
A1: F is_homomorphism FA,U1 and
A2: F || FG = f;
reconsider a = F as ManySortedFunction of fa,U1;
take a;
thus a is_homomorphism fa,U1 by A1;
thus a is "onto"
proof
let s be set;
assume s in the carrier of S;
then reconsider s0 = s as SortSymbol of S;
reconsider g = a.s as Function of (the Sorts of fa).s0, S1.s0 by
PBOOLE:def 15;
A3: f.s0 = g | (FG.s0) by A2,Def1;
then
A4: rng (f.s0) c= rng g by RELAT_1:70;
thus rng (a.s) c= S1.s by A3,RELAT_1:def 19;
let x be object;
set D = DTConMSA(S1), t = [x,s0];
assume x in S1.s;
then
A5: t in Terminals D by Th7;
then reconsider t as Symbol of D;
t`2 = s0;
then root-tree t in {root-tree tt where tt is Symbol of D : tt in
Terminals D & tt`2 = s0} by A5;
then
A6: root-tree t in FreeGen(s0,S1) by Th13;
A7: f.s0 = Reverse(s0,S1) by Def18;
then dom (f.s0) = FreeGen(s0,S1) by FUNCT_2:def 1;
then
A8: (f.s0).(root-tree t) in rng (f.s0) by A6,FUNCT_1:def 3;
(f.s0).(root-tree t) = t`1 by A7,A6,Def17
.= x;
hence thesis by A4,A8;
end;
end;
theorem
for S be non void non empty ManySortedSign, U1 be strict non-empty
MSAlgebra over S ex U0 be strict free non-empty MSAlgebra over S, F be
ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 & Image F = U1
proof
let S be non void non empty ManySortedSign, U1 be strict non-empty MSAlgebra
over S;
consider U0 be strict free non-empty MSAlgebra over S, F be
ManySortedFunction of U0,U1 such that
A1: F is_epimorphism U0,U1 by Th18;
Image F = U1 by A1,MSUALG_3:19;
hence thesis by A1;
end;