msafree.miz
begin
theorem ::
MSAFREE:1
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;
::
MSAFREE:def1
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 holds 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;
::
MSAFREE:def2
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;
:: original:
coprod
redefine
::
MSAFREE:def3
func
coprod X means
:
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 be
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 be
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 be
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 be
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 ::
MSAFREE:2
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
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;
::
MSAFREE:def4
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 ::
MSAFREE:3
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;
::
MSAFREE:def5
attr IT is
free means for U1 be
non-empty
MSAlgebra over S holds for f be
ManySortedFunction of IT, the
Sorts of U1 holds 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;
::
MSAFREE:def6
attr IT is
free means
:
Def6: ex G be
GeneratorSet of IT st G is
free;
end
theorem ::
MSAFREE:4
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
definition
let S be non
void non
empty
ManySortedSign, X be
ManySortedSet of the
carrier of S;
::
MSAFREE:def7
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 ::
MSAFREE:5
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;
::
MSAFREE:def8
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 ::
MSAFREE:6
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 be
Symbol of D : ex n be
FinSequence st s
==> n } by
LANG1:def 3;
then
consider s be
Symbol of D such that
A3: s
= x and
A4: ex n be
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 be
OperSymbol of S, x2 be
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)) holds 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 be
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,
XBOOLE_0: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 be
Symbol of D st nt
in (
NonTerminals D) holds ex p be
FinSequence of (
TS D) st nt
==> (
roots p)
proof
let nt be
Symbol of D;
assume nt
in (
NonTerminals D);
then
consider o be
OperSymbol of S, x2 be
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)) holds 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 be
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 be
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,
DTCONSTR:def 4,
DTCONSTR:def 5;
end;
end
theorem ::
MSAFREE:7
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;
::
MSAFREE:def9
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;
::
MSAFREE:def10
func
FreeSort (X,s) ->
Subset of (
TS (
DTConMSA X)) equals { a where a be
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 be
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 be
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;
::
MSAFREE:def11
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 ::
MSAFREE:8
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 be
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 ::
MSAFREE:9
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 ::
MSAFREE:10
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 be
OperSymbol of S, x2 be
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 ::
MSAFREE:11
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 be
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 be
OperSymbol of S, x2 be
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 ::
MSAFREE:12
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 be
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;
::
MSAFREE:def12
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 holds 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;
::
MSAFREE:def13
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 holds 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;
::
MSAFREE:def14
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;
::
MSAFREE:def15
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 be
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 be
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 be
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 ::
MSAFREE:13
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 be
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 be
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;
::
MSAFREE:def16
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 be
Symbol of D, ts be
FinSequence of (
TS D) st nt
==> (
roots ts) & for t be
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 be
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 be
OperSymbol of S, x2 be
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 be
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 be
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 be
OperSymbol of S, x2 be
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 be
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 be
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 ::
MSAFREE:14
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 ::
MSAFREE:15
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 be
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 be
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 be
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 be
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;
::
MSAFREE:def17
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 holds 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 be
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 be
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;
::
MSAFREE:def18
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 holds 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));
::
MSAFREE:def19
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 be
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;
::
MSAFREE:def20
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 be
OperSymbol of S, x2 be
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));
::
MSAFREE:def21
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 ::
MSAFREE:16
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 be
Function of (
TS D), DU such that
A1: for t be
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,*) 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 be
Symbol of D, ts be
FinSequence of (
TS D) st nt
==> (
roots ts) & for t be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 ::
MSAFREE:17
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 ::
MSAFREE:18
Th18: for S be non
void non
empty
ManySortedSign, U1 be
non-empty
MSAlgebra over S holds 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 be
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 ::
MSAFREE:19
for S be non
void non
empty
ManySortedSign, U1 be
strict
non-empty
MSAlgebra over S holds 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;