Copyright (c) 1994 Association of Mizar Users
environ
vocabulary ZF_REFLE, PBOOLE, BOOLE, RELAT_1, FUNCT_1, PRALG_1, TDGROUP,
CARD_3, FINSEQ_2, FINSEQ_1, FUNCOP_1, FUNCT_2, AMI_1, QC_LANG1, UNIALG_1,
PARTFUN1, REALSET1, MSUALG_1;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, NAT_1, RELAT_1, FUNCT_1,
FUNCT_2, FINSEQ_1, STRUCT_0, FUNCOP_1, PARTFUN1, FINSEQ_2, CARD_3,
PBOOLE, REALSET1, PRALG_1, UNIALG_1;
constructors REALSET1, PRALG_1, MEMBERED, XBOOLE_0;
clusters FUNCT_1, PBOOLE, UNIALG_1, TEX_2, PRALG_1, RELSET_1, STRUCT_0,
FINSEQ_2, FUNCOP_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS,
ORDINAL2;
requirements BOOLE, SUBSET;
definitions TARSKI, PRALG_1, FINSEQ_1, UNIALG_1, PBOOLE, STRUCT_0, XBOOLE_0;
theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, UNIALG_1, PBOOLE,
FUNCT_2, CARD_3, FINSEQ_3, FINSEQ_2, REALSET1, RELAT_1, RELSET_1,
STRUCT_0;
schemes ZFREFLE1, FUNCT_1, FRAENKEL, FUNCT_2;
begin :: Preliminaries
reserve i,j for set,
I for set;
theorem Th1:
not ex M being non-empty ManySortedSet of I st {} in rng M
proof let M be non-empty ManySortedSet of I;
assume
A1: {} in rng M;
dom M = I by PBOOLE:def 3;
then ex i st i in I & M.i = {} by A1,FUNCT_1:def 5;
hence contradiction by PBOOLE:def 16;
end;
scheme MSSEx { I() -> set, P[set,set] }:
ex f being ManySortedSet of I() st
for i st i in I() holds P[i,f.i]
provided A1: for i st i in I() ex j st P[i,j]
proof
defpred Q[set,set] means P[$1,$2];
A2: for i st i in I() ex j st Q[i,j] by A1;
consider f being Function such that
A3: dom f = I() and
A4: for i st i in I() holds Q[i,f.i] from NonUniqFuncEx(A2);
reconsider f as ManySortedSet of I() by A3,PBOOLE:def 3;
take f; thus thesis by A4;
end;
scheme MSSLambda { I() -> set, F(set) -> set }:
ex f being ManySortedSet of I() st
for i st i in I() holds f.i = F(i)
proof
deffunc G(set)=F($1);
consider f being Function such that
A1: dom f = I() and
A2: for i st i in I() holds f.i = G(i) from Lambda;
reconsider f as ManySortedSet of I() by A1,PBOOLE:def 3;
take f; thus thesis by A2;
end;
definition let I be set; let M be ManySortedSet of I;
mode Component of M is Element of rng M;
end;
theorem Th2:
for I being non empty set
for M being ManySortedSet of I, A being Component of M
ex i st i in I & A = M.i
proof let I be non empty set;
let M be ManySortedSet of I, A be Component of M;
A1: dom M = I by PBOOLE:def 3;
then rng M <> {} by RELAT_1:65;
hence ex i st i in I & A = M.i by A1,FUNCT_1:def 5;
end;
theorem Th3:
for M being ManySortedSet of I, i st i in I holds M.i is Component of M
proof let M be ManySortedSet of I, i;
A1: dom M = I by PBOOLE:def 3;
assume i in I;
hence thesis by A1,FUNCT_1:def 5;
end;
definition let I; let B be ManySortedSet of I;
mode Element of B -> ManySortedSet of I means
for i st i in I holds it.i is Element of B.i;
existence
proof
defpred Q[set,set] means $2 is Element of B.$1;
A1: for i st i in I ex j st Q[i,j]
proof let i such that i in I;
consider j being Element of B.i;
reconsider j as set;
take j; thus j is Element of B.i;
end;
thus ex f being ManySortedSet of I st
for i st i in I holds Q[i,f.i] from MSSEx(A1);
end;
end;
begin :: Many Sorted Functions
definition let I;
let A be ManySortedSet of I, B be ManySortedSet of I;
mode ManySortedFunction of A,B -> ManySortedSet of I means
:Def2: for i st i in I holds it.i is Function of A.i, B.i;
correctness
proof
defpred P[set,set] means $2 is Function of A.$1,B.$1;
A1: for i st i in I ex j st P[i,j]
proof let i such that i in I;
consider j being Function of A.i,B.i;
reconsider j as set;
take j; thus j is Function of A.i,B.i;
end;
consider f being ManySortedSet of I such that
A2: for i st i in I holds P[i,f.i] from MSSEx(A1);
f is Function-yielding
proof let i;
assume i in dom f;
then i in I by PBOOLE:def 3;
hence f.i is Function by A2;
end;
then reconsider f as ManySortedFunction of I;
take f;
let i;
assume i in I;
hence f.i is Function of A.i,B.i by A2;
end;
end;
definition let I;
let A be ManySortedSet of I, B be ManySortedSet of I;
cluster ->Function-yielding ManySortedFunction of A,B;
coherence
proof let f be ManySortedFunction of A,B;
let i;
assume i in dom f;
then i in I by PBOOLE:def 3;
hence f.i is Function by Def2;
end;
end;
definition let I be set; let M be ManySortedSet of I;
func M# -> ManySortedSet of I* means
:Def3: for i being Element of I* holds it.i = product(M*i);
existence
proof
defpred P[set,set] means ex j being Element of I* st j = $1
& $2 = product(M*j);
A1: for i st i in I* ex j st P[i,j]
proof let i; assume
i in I*;
then reconsider j = i as Element of I*;
reconsider e = product(M*j) as set;
take e,j;
thus j = i & e = product(M*j);
end;
consider f being ManySortedSet of I* such that
A2: for i st i in I* holds P[i,f.i]
from MSSEx(A1);
take f; let i be Element of I*;
ex j being Element of I* st j = i & f.i = product(M*j) by A2;
hence thesis;
end;
uniqueness
proof let N1,N2 be ManySortedSet of I* such that
A3: for i being Element of I* holds N1.i = product(M*i) and
A4: for i being Element of I* holds N2.i = product(M*i);
now let i;
assume
i in I*;
then reconsider e = i as Element of I*;
thus N1.i = product(M*e) by A3 .= N2.i by A4;
end;
hence thesis by PBOOLE:3;
end;
end;
definition let I be set; let M be non-empty ManySortedSet of I;
cluster M# -> non-empty;
coherence
proof
M# is non-empty
proof let i;
assume
i in I*;
then reconsider f = i as Element of I*;
not {} in rng M by Th1;
then not {} in rng(M*f) by FUNCT_1:25;
then product(M*f) <> {} by CARD_3:37;
hence M#.i is non empty by Def3;
end;
hence thesis;
end;
end;
definition let I; let J be non empty set;
let O be Function of I,J;
let F be ManySortedSet of J;
redefine func F*O -> ManySortedSet of I;
coherence
proof
rng O c= J & dom O = I & dom F = J
by FUNCT_2:def 1,PBOOLE:def 3,RELSET_1:12;
hence dom(F*O) = I by RELAT_1:46;
end;
end;
definition let I; let J be non empty set;
let O be Function of I,J;
let F be non-empty ManySortedSet of J;
redefine func F*O -> non-empty ManySortedSet of I;
coherence
proof
F*O is non-empty
proof let i;
assume
A1: i in I;
then O.i in J by FUNCT_2:7;
then A2: F.(O.i) is non empty by PBOOLE:def 16;
dom O = I by FUNCT_2:def 1;
hence (F*O).i is non empty by A1,A2,FUNCT_1:23;
end;
hence thesis;
end;
end;
definition let a be set;
func *-->a -> Function of NAT,{a}* means
:Def4: for n being Nat holds it.n = n |-> a;
existence
proof
defpred P[Element of NAT,Element of {a}*] means $2 = $1 |-> a;
A1: for x being Element of NAT ex y being Element of {a}* st P[x,y]
proof let n be Nat;
a is Element of {a} by TARSKI:def 1;
then n |-> a is FinSequence of {a} by FINSEQ_2:77;
then reconsider u = n |-> a as Element of {a}* by FINSEQ_1:def 11;
take u;
thus u = n |-> a;
end;
ex f being Function of NAT,{a}* st for x being Element of NAT
holds P[x,f.x] from FuncExD(A1);
hence thesis;
end;
uniqueness
proof let f1,f2 be Function of NAT,{a}* such that
A2: for n being Nat holds f1.n = n |-> a and
A3: for n being Nat holds f2.n = n |-> a;
now let k be Nat;
thus f1.k = k |-> a by A2
.= f2.k by A3;
end;
hence f1 = f2 by FUNCT_2:113;
end;
end;
reserve D for non empty set,
n for Nat;
theorem Th4:
for a,b being set holds ({a} --> b)*(n|->a) = n |-> b
proof let a,b be set;
A1: now let x be set;
hereby assume x in dom (n |-> b);
then A2: x in Seg n by FINSEQ_2:68;
hence x in dom(n|->a) by FINSEQ_2:68;
A3: dom({a} --> b) = {a} by FUNCOP_1:19;
(n|->a).x = a by A2,FINSEQ_2:70;
hence (n|->a).x in dom({a} --> b) by A3,TARSKI:def 1;
end;
assume that
A4: x in dom(n|->a) and (n|->a).x in dom({a} --> b);
x in Seg n by A4,FINSEQ_2:68;
hence x in dom (n |-> b) by FINSEQ_2:68;
end;
now let x be set;
assume
x in dom (n |-> b);
then A5: x in Seg n by FINSEQ_2:68;
A6: a in {a} by TARSKI:def 1;
thus (n |-> b).x = b by A5,FINSEQ_2:70
.= ({a} --> b).a by A6,FUNCOP_1:13
.= ({a} --> b).((n|->a).x) by A5,FINSEQ_2:70;
end;
hence ({a} --> b)*(n|->a) = n |-> b by A1,FUNCT_1:20;
end;
theorem Th5:
for a being set
for M being ManySortedSet of {a} st M = {a} --> D
holds (M#**-->a).n = Funcs(Seg n, D)
proof let a be set;
let M be ManySortedSet of {a} such that
A1: M = {a} --> D;
A2: dom(*-->a) = NAT by FUNCT_2:def 1;
a is Element of {a} by TARSKI:def 1;
then n |-> a is FinSequence of {a} by FINSEQ_2:77;
then A3: n |-> a in {a}* by FINSEQ_1:def 11;
thus (M#**-->a).n = M#.((*-->a).n) by A2,FUNCT_1:23
.= M#.(n|->a) by Def4
.= product(({a} --> D)*(n|->a)) by A1,A3,Def3
.= product(n |-> D) by Th4
.= product(Seg(n) --> D) by FINSEQ_2:def 2
.= Funcs(Seg n, D) by CARD_3:20;
end;
definition let I,i;
redefine func I --> i -> Function of I,{i};
coherence
proof
dom (I --> i) = I & rng (I --> i) c= {i} by FUNCOP_1:19;
hence I --> i is Function of I,{i} by FUNCT_2:def 1,RELSET_1:11;
end;
end;
begin :: Many Sorted Signatures
definition
struct(1-sorted) ManySortedSign
(# carrier -> set,
OperSymbols -> set,
Arity -> Function of the OperSymbols, the carrier*,
ResultSort -> Function of the OperSymbols, the carrier
#);
end;
definition let IT be ManySortedSign;
attr IT is void means
:Def5: the OperSymbols of IT = {};
end;
definition
cluster void strict non empty ManySortedSign;
existence
proof
{} in {{}}* by FINSEQ_1:66;
then reconsider f = {}-->{} as Function of {},{{}}* by FUNCOP_1:58;
reconsider g = {}-->{} as Function of {},{{}};
take ManySortedSign(#{{}},{},f,g#);
thus thesis by Def5,STRUCT_0:def 1;
end;
cluster non void strict non empty ManySortedSign;
existence
proof
{} in {{}}* by FINSEQ_1:66;
then reconsider f = {{}}-->{} as Function of {{}},{{}}* by FUNCOP_1:58;
reconsider g = {{}}-->{} as Function of {{}},{{}};
take ManySortedSign(#{{}},{{}},f,g#);
thus thesis by Def5,STRUCT_0:def 1;
end;
end;
reserve S for non empty ManySortedSign;
definition let S;
mode SortSymbol of S is Element of S;
mode OperSymbol of S is Element of the OperSymbols of S;
end;
definition let S be non void non empty ManySortedSign;
let o be OperSymbol of S;
func the_arity_of o -> Element of (the carrier of S)* equals
:Def6: (the Arity of S).o;
coherence
proof the OperSymbols of S <> {} by Def5;
then o in the OperSymbols of S;
then o in dom(the Arity of S) by FUNCT_2:def 1;
then A1: (the Arity of S).o in rng(the Arity of S) by FUNCT_1:def 5;
rng(the Arity of S) c= (the carrier of S)* by RELSET_1:12;
hence thesis by A1;
end;
correctness;
func the_result_sort_of o -> Element of S equals
(the ResultSort of S).o;
coherence
proof the OperSymbols of S <> {} by Def5;
then o in the OperSymbols of S;
then o in dom(the ResultSort of S) by FUNCT_2:def 1;
then A2: (the ResultSort of S).o in rng(the ResultSort of S) by FUNCT_1:
def 5;
rng(the ResultSort of S) c= the carrier of S by RELSET_1:12;
hence thesis by A2;
end;
end;
begin :: Many Sorted Algebras
definition let S be 1-sorted;
struct many-sorted over S (# Sorts -> ManySortedSet of the carrier of S #);
end;
definition let S;
struct(many-sorted over S) MSAlgebra over S (#
Sorts -> ManySortedSet of the carrier of S,
Charact -> ManySortedFunction of
(the Sorts)# * the Arity of S, the Sorts * the ResultSort of S#);
end;
definition let S be 1-sorted; let A be many-sorted over S;
attr A is non-empty means
:Def8: the Sorts of A is non-empty;
end;
definition let S;
cluster strict non-empty MSAlgebra over S;
existence
proof
dom((the carrier of S) --> {0}) = the carrier of S by FUNCOP_1:19;
then reconsider s = (the carrier of S) --> {0}
as ManySortedSet of the carrier of S by PBOOLE:def 3;
consider o being ManySortedFunction of
s# * the Arity of S, s * the ResultSort of S;
take MSAlgebra(#s,o#);
thus MSAlgebra(#s,o#) is strict;
let i be set;
assume i in the carrier of S;
hence thesis by FUNCOP_1:13;
end;
end;
definition let S be 1-sorted;
cluster strict non-empty many-sorted over S;
existence
proof
dom ((the carrier of S) --> {0}) = the carrier of S by FUNCOP_1:19;
then reconsider s = (the carrier of S) --> {0}
as ManySortedSet of the carrier of S by PBOOLE:def 3;
take many-sorted(#s#);
thus many-sorted (#s#) is strict;
let i be set;
assume i in the carrier of S;
hence thesis by FUNCOP_1:13;
end;
end;
definition let S be 1-sorted; let A be non-empty many-sorted over S;
cluster the Sorts of A -> non-empty;
coherence by Def8;
end;
definition let S; let A be non-empty MSAlgebra over S;
cluster -> non empty Component of the Sorts of A;
coherence
proof let C be Component of the Sorts of A;
ex i st i in the carrier of S & C = (the Sorts of A).i by Th2;
hence thesis by PBOOLE:def 16;
end;
cluster -> non empty Component of (the Sorts of A)#;
coherence
proof let C be Component of (the Sorts of A)#;
ex i st i in (the carrier of S)* & C = (the Sorts of A)#.i by Th2;
hence thesis by PBOOLE:def 16;
end;
end;
definition let S be non void non empty ManySortedSign;
let o be OperSymbol of S; let A be MSAlgebra over S;
func Args(o,A) -> Component of (the Sorts of A)# equals
:Def9: ((the Sorts of A)# * the Arity of S).o;
coherence
proof
the OperSymbols of S <> {} by Def5;
then o in the OperSymbols of S;
then o in dom((the Sorts of A)# * the Arity of S) by PBOOLE:def 3;
then ((the Sorts of A)# * the Arity of S).o
in rng((the Sorts of A)# * the Arity of S) by FUNCT_1:def 5;
hence thesis by FUNCT_1:25;
end;
correctness;
func Result(o,A) -> Component of the Sorts of A equals
:Def10: ((the Sorts of A) * the ResultSort of S).o;
coherence
proof
the OperSymbols of S <> {} by Def5;
then o in the OperSymbols of S;
then o in dom((the Sorts of A) * the ResultSort of S) by PBOOLE:def 3;
then ((the Sorts of A) * the ResultSort of S).o
in rng((the Sorts of A) * the ResultSort of S) by FUNCT_1:def 5;
hence thesis by FUNCT_1:25;
end;
correctness;
end;
definition let S be non void non empty ManySortedSign;
let o be OperSymbol of S; let A be MSAlgebra over S;
func Den(o,A) -> Function of Args(o,A), Result(o,A) equals
:Def11: (the Charact of A).o;
coherence
proof
A1: the OperSymbols of S <> {} by Def5;
Result(o,A) = ((the Sorts of A) * the ResultSort of S).o &
Args(o,A) = ((the Sorts of A)# * the Arity of S).o by Def9,Def10;
hence thesis by A1,Def2;
end;
end;
theorem Th6:
for S being non void non empty ManySortedSign, o being OperSymbol of S,
A being non-empty MSAlgebra over S
holds Den(o,A) is non empty
proof let S be non void non empty ManySortedSign, o be OperSymbol of S,
A be non-empty MSAlgebra over S;
thus Den(o,A) is non empty by FUNCT_2:def 1,RELAT_1:60;
end;
begin :: On the one-sorted algebras
Lm1:
for h being homogeneous quasi_total non empty PartFunc of D*,D
holds dom h = (arity h)-tuples_on D
proof let h be homogeneous quasi_total non empty PartFunc of D*,D;
A1: dom h c= D* by RELSET_1:12;
thus dom h c= (arity h)-tuples_on D
proof let x be set;
assume
A2: x in dom h;
then reconsider f = x as FinSequence of D by A1,FINSEQ_1:def 11;
A3: len f = arity h by A2,UNIALG_1:def 10;
f is Element of (len f)-tuples_on D by FINSEQ_2:110;
hence x in (arity h)-tuples_on D by A3;
end;
let x be set;
assume x in (arity h)-tuples_on D;
then reconsider f = x as Element of (arity h)-tuples_on D;
consider x0 being Element of dom h;
A4: dom h <> {} by RELAT_1:64;
then x0 in dom h;
then reconsider x0 as FinSequence of D by A1,FINSEQ_1:def 11;
len x0 = arity h by A4,UNIALG_1:def 10 .= len f by FINSEQ_2:109;
hence x in dom h by A4,UNIALG_1:def 2;
end;
theorem Th7:
for C being set, A,B being non empty set,
F being PartFunc of C,A, G being Function of A,B
holds G*F is Function of dom F,B
proof let C be set; let A,B be non empty set;
let F be PartFunc of C,A; let G be Function of A,B;
now dom G = A by FUNCT_2:def 1;
then rng F c= dom G by RELSET_1:12;
hence dom(G*F) = dom F by RELAT_1:46;
thus rng(G*F) c= B by RELSET_1:12;
end;
hence G*F is Function of dom F,B by FUNCT_2:def 1,RELSET_1:11;
end;
theorem Th8:
for h being homogeneous quasi_total non empty PartFunc of D*,D
holds dom h = Funcs(Seg(arity h),D)
proof let h be homogeneous quasi_total non empty PartFunc of D*,D;
thus dom h = (arity h)-tuples_on D by Lm1
.= Funcs(Seg(arity h),D) by FINSEQ_2:111;
end;
theorem Th9:
for A being Universal_Algebra holds signature A is non empty
proof let A be Universal_Algebra;
len(the charact of A) <> 0 by FINSEQ_1:25;
then len(signature A) <> 0 by UNIALG_1:def 11;
hence signature A is non empty by FINSEQ_1:25;
end;
begin :: Relationship to one sorted algebras
definition let A be Universal_Algebra;
redefine func signature A -> FinSequence of NAT;
coherence;
end;
definition let IT be ManySortedSign;
attr IT is segmental means
:Def12: ex n st the OperSymbols of IT = Seg n;
end;
theorem Th10:
for S being non empty ManySortedSign st S is trivial
for A being MSAlgebra over S,
c1,c2 being Component of the Sorts of A holds c1 = c2
proof let S be non empty ManySortedSign such that
A1: S is trivial;
let A be MSAlgebra over S, c1,c2 be Component of the Sorts of A;
consider i1 being set such that
A2: i1 in the carrier of S and
A3: c1 = (the Sorts of A).i1 by Th2;
consider i2 being set such that
A4: i2 in the carrier of S and
A5: c2 = (the Sorts of A).i2 by Th2;
thus c1 = c2 by A1,A2,A3,A4,A5,REALSET1:def 20;
end;
Lm2:
for A being Universal_Algebra
for f being Function of dom signature A, {0}*
st f = (*-->0)*(signature A)
holds
ManySortedSign
(#{0},dom signature(A),f,dom signature(A)-->0#)
is non empty segmental trivial non void strict
proof let A be Universal_Algebra;
let f be Function of dom signature A, {0}* such that
f = (*-->0)*(signature A);
set S = ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->0#);
thus
the carrier of S is non empty;
signature A <> {} by Th9;
then A1: the OperSymbols of S <> {} by RELAT_1:64;
S is segmental
proof
take len signature(A);
thus the OperSymbols of S = Seg len signature(A) by FINSEQ_1:def 3;
end;
hence thesis by A1,Def5,REALSET1:def 13;
end;
definition
cluster segmental trivial non void strict non empty ManySortedSign;
existence
proof consider A being Universal_Algebra;
reconsider f = (*-->0)*(signature A) as Function of dom signature A, {0}*
by Th7;
ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->0#)
is segmental trivial non void strict non empty by Lm2;
hence thesis;
end;
end;
definition let A be Universal_Algebra;
func MSSign A -> non void strict segmental trivial ManySortedSign means
:Def13:
the carrier of it = {0} &
the OperSymbols of it = dom signature A &
the Arity of it = (*-->0)*signature A &
the ResultSort of it = dom signature(A)-->0;
correctness
proof
reconsider f = (*-->0)*(signature A) as Function of dom signature A, {0}*
by Th7;
ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->0#)
is segmental trivial non void strict by Lm2;
hence thesis;
end;
end;
definition let A be Universal_Algebra;
cluster MSSign A -> non empty;
coherence
proof
thus the carrier of MSSign A is non empty by Def13;
end;
end;
definition let A be Universal_Algebra;
func MSSorts A -> non-empty ManySortedSet of the carrier of MSSign A equals
:Def14: {0}-->the carrier of A;
coherence
proof
A1: the carrier of MSSign A = {0} &
the OperSymbols of MSSign A = dom signature A &
the Arity of MSSign A = (*-->0)*signature A &
the ResultSort of MSSign A = dom signature(A)-->0 by Def13;
set M = {0}-->the carrier of A;
dom M = the carrier of MSSign A by A1,FUNCOP_1:19;
then reconsider M as ManySortedSet of the carrier of MSSign A
by PBOOLE:def 3;
M is non-empty
proof let i;
assume
i in the carrier of MSSign A;
hence thesis by A1,FUNCOP_1:13;
end;
hence thesis;
end;
correctness;
end;
definition let A be Universal_Algebra;
func MSCharact A -> ManySortedFunction of
(MSSorts A)# * the Arity of MSSign A, (MSSorts A)* the ResultSort of MSSign A
equals
:Def15: the charact of A;
coherence
proof
reconsider OS = the OperSymbols of MSSign A as non empty set by Def5;
A1: the carrier of MSSign A = {0} &
the OperSymbols of MSSign A = dom signature A &
the Arity of MSSign A = (*-->0)*signature A &
the ResultSort of MSSign A = dom signature(A)-->0 by Def13;
len signature A = len the charact of A by UNIALG_1:def 11;
then A2: dom the charact of A = OS by A1,FINSEQ_3:31;
then reconsider O = the charact of A as ManySortedSet of OS
by PBOOLE:def 3;
O is Function-yielding
proof let i;
assume
A3: i in dom O;
dom O = dom the charact of A;
then reconsider n = i as Nat by A3;
O.n is Function by A3,UNIALG_1:5;
hence O.i is Function;
end;
then reconsider O as ManySortedFunction of OS;
reconsider DO = (MSSorts A)# * the Arity of MSSign A,
RO = (MSSorts A)* the ResultSort of MSSign A
as ManySortedSet of OS;
O is ManySortedFunction of DO,RO
proof let i;
assume
A4: i in OS;
then reconsider o = i as Element of OS;
reconsider n = i as Nat by A1,A4;
set D = the carrier of A;
reconsider h = O.n as homogeneous quasi_total non empty PartFunc of D*,D
by A2,A4,UNIALG_1:5,def 4,def 5,def 6;
dom({0}-->D) = {0} by FUNCOP_1:19;
then reconsider M = {0}-->D as ManySortedSet of {0} by PBOOLE:def 3;
A5: n in dom(dom signature(A)-->0) by A1,A4,FUNCOP_1:19;
A6: 0 in {0} by TARSKI:def 1;
A7: DO.i = ((MSSorts A)#*(*-->0)*signature A).n by A1,RELAT_1:55
.= ((MSSorts A)#*(*-->0)).((signature A).n) by A1,A4,FUNCT_1:23
.= (M#*(*-->0)).((signature A).n) by A1,Def14
.= (M#*(*-->0)).arity h by A1,A4,UNIALG_1:def 11
.= Funcs(Seg arity h,D) by Th5
.= dom(O.o) by Th8;
A8: RO.i = (MSSorts A).((dom signature(A)-->0).n) by A1,A5,FUNCT_1:23
.= (MSSorts A).0 by A1,A4,FUNCOP_1:13
.= ({0}-->the carrier of A).0 by Def14
.= the carrier of A by A6,FUNCOP_1:13;
then rng h c= RO.i by RELSET_1:12;
hence O.i is Function of DO.i,RO.i by A7,A8,FUNCT_2:def 1,RELSET_1:11;
end;
hence thesis;
end;
correctness;
end;
definition let A be Universal_Algebra;
func MSAlg A -> strict MSAlgebra over MSSign A equals
:Def16: MSAlgebra(#MSSorts A,MSCharact A#);
correctness;
end;
definition let A be Universal_Algebra;
cluster MSAlg A -> non-empty;
coherence
proof
MSAlg A = MSAlgebra(#MSSorts A,MSCharact A#) by Def16;
hence the Sorts of MSAlg A is non-empty;
end;
end;
:: Manysorted Algebras with 1 Sort Only
definition let MS be trivial non empty ManySortedSign;
let A be MSAlgebra over MS;
func the_sort_of A -> set means
:Def17: ex c being Component of the Sorts of A st it = c;
existence
proof consider c being Component of the Sorts of A;
take c; thus thesis;
end;
uniqueness by Th10;
end;
definition let MS be trivial non empty ManySortedSign;
let A be non-empty MSAlgebra over MS;
cluster the_sort_of A -> non empty;
coherence
proof
ex c being Component of the Sorts of A st the_sort_of A = c by Def17;
hence thesis;
end;
end;
theorem Th11:
for MS being segmental trivial non void non empty ManySortedSign,
i being OperSymbol of MS,
A being non-empty MSAlgebra over MS
holds Args(i,A) = (len the_arity_of i)-tuples_on the_sort_of A
proof
let MS be segmental trivial non void non empty ManySortedSign,
i be OperSymbol of MS,
A be non-empty MSAlgebra over MS;
set m = len the_arity_of i;
A1: the OperSymbols of MS <> {} by Def5;
A2: dom(the Arity of MS) = the OperSymbols of MS by FUNCT_2:def 1;
A3: Args(i,A) = ((the Sorts of A)# * the Arity of MS).i by Def9
.= (the Sorts of A)# .((the Arity of MS).i) by A1,A2,FUNCT_1:23
.= (the Sorts of A)# .the_arity_of i by Def6
.= product((the Sorts of A)*the_arity_of i) by Def3;
consider n being Nat such that
A4: dom the_arity_of i = Seg n by FINSEQ_1:def 2;
A5: rng the_arity_of i c= the carrier of MS by FINSEQ_1:def 4;
then rng the_arity_of i c= dom the Sorts of A by PBOOLE:def 3;
then A6: dom((the Sorts of A)*the_arity_of i) = dom the_arity_of i by RELAT_1
:46;
thus Args(i,A) c= m-tuples_on the_sort_of A
proof
let x be set;
assume x in Args(i,A);
then consider g being Function such that
A7: x = g and
A8: dom g = dom((the Sorts of A)*the_arity_of i) and
A9: for j being set st j in dom((the Sorts of A)*the_arity_of i)
holds g.j in ((the Sorts of A)*the_arity_of i).j by A3,CARD_3:def 5;
reconsider p = g as FinSequence by A4,A6,A8,FINSEQ_1:def 2;
rng p c= the_sort_of A
proof let j be set;
assume j in rng p;
then consider u being set such that
A10: u in dom g and
A11: p.u = j by FUNCT_1:def 5;
g.u in ((the Sorts of A)*the_arity_of i).u by A8,A9,A10;
then A12: g.u in (the Sorts of A).((the_arity_of i).u) by A6,A8,A10,
FUNCT_1:23;
(the_arity_of i).u in rng the_arity_of i by A6,A8,A10,FUNCT_1:def 5;
then (the Sorts of A).((the_arity_of i).u) is
Component of the Sorts of A by A5,Th3;
hence j in the_sort_of A by A11,A12,Def17;
end;
then A13: p is FinSequence of the_sort_of A by FINSEQ_1:def 4;
len p = m by A6,A8,FINSEQ_3:31;
then x is Element of m-tuples_on the_sort_of A by A7,A13,FINSEQ_2:110;
hence x in m-tuples_on the_sort_of A;
end;
let x be set;
assume x in m-tuples_on the_sort_of A;
then x in Funcs(Seg m, the_sort_of A) by FINSEQ_2:111;
then consider g being Function such that
A14: x = g and
A15: dom g = Seg m and
A16: rng g c= the_sort_of A by FUNCT_2:def 2;
A17: dom g = dom((the Sorts of A)*the_arity_of i) by A6,A15,FINSEQ_1:def 3;
now let x be set;
assume
A18: x in dom((the Sorts of A)*the_arity_of i);
then g.x in rng g by A17,FUNCT_1:def 5;
then A19: g.x in the_sort_of A by A16;
(the_arity_of i).x in rng the_arity_of i by A6,A18,FUNCT_1:def 5;
then (the Sorts of A).((the_arity_of i).x) is
Component of the Sorts of A by A5,Th3;
then g.x in (the Sorts of A).((the_arity_of i).x) by A19,Def17;
hence g.x in ((the Sorts of A)*the_arity_of i).x by A6,A18,FUNCT_1:23;
end;
hence x in Args(i,A) by A3,A14,A17,CARD_3:18;
end;
theorem Th12:
for A being non empty set, n holds n-tuples_on A c= A*
proof let A be non empty set, n;
defpred P[Element of A*] means len $1 = n;
{ s where s is Element of A*: P[s] } c= A* from Fr_Set0;
hence n-tuples_on A c= A* by FINSEQ_2:def 4;
end;
theorem Th13:
for MS being segmental trivial non void non empty ManySortedSign,
i being OperSymbol of MS,
A being non-empty MSAlgebra over MS holds Args(i,A) c= (the_sort_of A)*
proof
let MS be segmental trivial non void non empty ManySortedSign,
i be OperSymbol of MS,
A be non-empty MSAlgebra over MS;
Args(i,A) = (len the_arity_of i)-tuples_on the_sort_of A by Th11;
hence Args(i,A) c= (the_sort_of A)* by Th12;
end;
theorem Th14:
for MS being segmental trivial non void non empty ManySortedSign,
A being non-empty MSAlgebra over MS holds
the Charact of A is FinSequence of PFuncs((the_sort_of A)*,the_sort_of A)
proof
let MS be segmental trivial non void non empty ManySortedSign,
A be non-empty MSAlgebra over MS;
A1: dom the Charact of A = the OperSymbols of MS by PBOOLE:def 3;
ex n st the OperSymbols of MS = Seg n by Def12;
then reconsider f = the Charact of A as FinSequence by A1,FINSEQ_1:def 2;
f is FinSequence of PFuncs((the_sort_of A)*,the_sort_of A)
proof let x be set;
assume x in rng f;
then consider i such that
A2: i in the OperSymbols of MS and
A3: f.i = x by A1,FUNCT_1:def 5;
reconsider i as OperSymbol of MS by A2;
A4: dom(the ResultSort of MS) = the OperSymbols of MS by FUNCT_2:def 1;
A5: ((the Sorts of A)# * the Arity of MS).i = Args(i,A) by Def9;
(the ResultSort of MS).i in the carrier of MS by A2,FUNCT_2:7;
then A6: (the Sorts of A).((the ResultSort of MS).i)
is Component of the Sorts of A by Th3;
A7: Args(i,A) c= (the_sort_of A)* by Th13;
((the Sorts of A)*the ResultSort of MS).i
= (the Sorts of A).((the ResultSort of MS).i) by A2,A4,FUNCT_1:23
.= the_sort_of A by A6,Def17;
then x is Function of Args(i,A),the_sort_of A by A2,A3,A5,Def2;
then x is PartFunc of (the_sort_of A)*,the_sort_of A by A7,PARTFUN1:30;
hence x in PFuncs((the_sort_of A)*,the_sort_of A) by PARTFUN1:119;
end;
hence thesis;
end;
definition let MS be segmental trivial non void non empty ManySortedSign;
let A be non-empty MSAlgebra over MS;
func the_charact_of A -> PFuncFinSequence of the_sort_of A equals
:Def18: the Charact of A;
coherence by Th14;
end;
reserve MS for segmental trivial non void non empty ManySortedSign,
A for non-empty MSAlgebra over MS,
h for PartFunc of (the_sort_of A)*,(the_sort_of A),
x,y for FinSequence of the_sort_of A;
definition let MS,A;
func 1-Alg A -> non-empty strict Universal_Algebra equals
:Def19: UAStr(#the_sort_of A, the_charact_of A#);
coherence
proof
A1: the_charact_of A is quasi_total
proof let n,h such that
A2: n in dom(the_charact_of A) and
A3: h = (the_charact_of A).n;
let x,y such that
A4: len x = len y and
A5: x in dom h;
A6: dom(the_charact_of A) = dom the Charact of A by Def18
.= the OperSymbols of MS by PBOOLE:def 3;
then reconsider o = n as OperSymbol of MS by A2;
A7: dom(the ResultSort of MS) = the OperSymbols of MS by FUNCT_2:def 1;
A8: ((the Sorts of A)# * the Arity of MS).o = Args(o,A) by Def9;
(the ResultSort of MS).o in the carrier of MS by A2,A6,FUNCT_2:7;
then A9: (the Sorts of A).((the ResultSort of MS).o)
is Component of the Sorts of A by Th3;
A10: ((the Sorts of A)*the ResultSort of MS).o
= (the Sorts of A).((the ResultSort of MS).o) by A2,A6,A7,FUNCT_1:23
.= the_sort_of A by A9,Def17;
h = (the Charact of A).o by A3,Def18;
then h is Function of
((the Sorts of A)# * the Arity of MS).o,
((the Sorts of A) * the ResultSort of MS).o by A2,A6,Def2;
then A11: dom h = ((the Sorts of A)# * the Arity of MS).o by A10,
FUNCT_2:def 1
.= (len the_arity_of o)-tuples_on the_sort_of A by A8,Th11;
then len y = len the_arity_of o by A4,A5,FINSEQ_2:109;
then y is Element of dom h by A11,FINSEQ_2:110;
hence y in dom h by A5;
end;
A12: the_charact_of A is homogeneous
proof let n,h such that
A13: n in dom(the_charact_of A) and
A14: h = (the_charact_of A).n;
let x,y such that
A15: x in dom h & y in dom h;
A16: dom(the_charact_of A) = dom the Charact of A by Def18
.= the OperSymbols of MS by PBOOLE:def 3;
then reconsider o = n as OperSymbol of MS by A13;
A17: dom(the ResultSort of MS) = the OperSymbols of MS by FUNCT_2:def 1;
A18: ((the Sorts of A)# * the Arity of MS).o = Args(o,A) by Def9;
(the ResultSort of MS).o in the carrier of MS by A13,A16,FUNCT_2:7;
then A19: (the Sorts of A).((the ResultSort of MS).o)
is Component of the Sorts of A by Th3;
A20: ((the Sorts of A)*the ResultSort of MS).o
= (the Sorts of A).((the ResultSort of MS).o) by A13,A16,A17,FUNCT_1:
23
.= the_sort_of A by A19,Def17;
h = (the Charact of A).o by A14,Def18;
then h is Function of
((the Sorts of A)# * the Arity of MS).o,
((the Sorts of A) * the ResultSort of MS).o by A13,A16,Def2;
then A21: dom h = ((the Sorts of A)# * the Arity of MS).o by A20,
FUNCT_2:def 1
.= (len the_arity_of o)-tuples_on the_sort_of A by A18,Th11;
hence len x = len the_arity_of o by A15,FINSEQ_2:109
.= len y by A15,A21,FINSEQ_2:109;
end;
the OperSymbols of MS <> {} by Def5;
then the Charact of A <> {} by PBOOLE:def 3,RELAT_1:60;
then A22: the_charact_of A <> {} by Def18;
the_charact_of A is non-empty
proof let n be set such that
A23: n in dom the_charact_of A;
set h = (the_charact_of A).n;
dom(the_charact_of A) = dom the Charact of A by Def18
.= the OperSymbols of MS by PBOOLE:def 3;
then reconsider o = n as OperSymbol of MS by A23;
h = (the Charact of A).o by Def18
.= Den(o,A) by Def11;
hence h is non empty by Th6;
end;
hence thesis by A1,A12,A22,UNIALG_1:def 7,def 8,def 9;
end;
correctness;
end;
theorem
for A being strict Universal_Algebra holds
A = 1-Alg MSAlg A
proof let A be strict Universal_Algebra;
A1: MSAlg A = MSAlgebra(#MSSorts A,MSCharact A#) by Def16;
the carrier of A in {the carrier of A} by TARSKI:def 1;
then the carrier of A in rng({0}-->the carrier of A) by FUNCOP_1:14;
then the carrier of A in rng the Sorts of MSAlg A by A1,Def14;
then A2: the carrier of A = the_sort_of MSAlg A by Def17;
the charact of A = MSCharact A by Def15
.= the_charact_of MSAlg A by A1,Def18;
hence A = 1-Alg MSAlg A by A2,Def19;
end;
theorem
for A being Universal_Algebra
for f being Function of dom signature A, {0}*
st f = (*-->0)*signature A
holds MSSign A = ManySortedSign(#{0},dom signature A,f,dom signature(A)-->0#)
proof let A be Universal_Algebra;
the carrier of MSSign A = {0} &
the OperSymbols of MSSign A = dom signature A &
the Arity of MSSign A = (*-->0)*signature A &
the ResultSort of MSSign A = dom signature(A)-->0 by Def13;
hence thesis;
end;