### The Mizar article:

### Basic Notation of Universal Algebra

**by****Jaroslaw Kotowicz,****Beata Madras, and****Malgorzata Korolkiewicz**

- Received December 29, 1992
Copyright (c) 1992 Association of Mizar Users

- MML identifier: UNIALG_1
- [ MML identifier index ]

environ vocabulary FINSEQ_1, PARTFUN1, RELAT_1, FUNCT_2, FUNCOP_1, BOOLE, FUNCT_1, ZF_REFLE, INCPROJ, UNIALG_1; notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FUNCOP_1, STRUCT_0, PARTFUN1; constructors FINSEQ_4, STRUCT_0, FUNCOP_1, PARTFUN1, XREAL_0, XCMPLX_0, MEMBERED, XBOOLE_0; clusters SUBSET_1, RELSET_1, STRUCT_0, PARTFUN1, FUNCOP_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET; definitions TARSKI, STRUCT_0, RELAT_1; theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, RELAT_1, RELSET_1; schemes MATRIX_2; begin reserve A,z for set, x,y for FinSequence of A, h for PartFunc of A*,A, n,m for Nat; definition let A; let IT be PartFunc of A*,A; attr IT is homogeneous means :Def1: for x,y st x in dom IT & y in dom IT holds len x = len y; end; definition let A; let IT be PartFunc of A*,A; attr IT is quasi_total means for x,y st len x = len y & x in dom IT holds y in dom IT; end; definition let A be non empty set; cluster homogeneous quasi_total non empty PartFunc of A*,A; existence proof consider a be Element of A; set f = {<*>A} -->a; A1: dom f = {<*>A} & rng f = {a} by FUNCOP_1:14,19; A2: dom f c= A* proof let z; assume z in dom f; then z = <*>A by A1,TARSKI:def 1; hence thesis by FINSEQ_1:def 11; end; rng f c= A proof let z; assume z in rng f; then z = a by A1,TARSKI:def 1; hence thesis; end; then reconsider f as PartFunc of A*,A by A2,RELSET_1:11; A3: f is homogeneous proof let x,y be FinSequence of A; assume x in dom f & y in dom f; then x = <*>A & y = <*>A by A1,TARSKI:def 1; hence thesis; end; A4: f is quasi_total proof let x,y be FinSequence of A; assume A5: len x = len y & x in dom f; then x = <*>A by A1,TARSKI:def 1; then len x = 0 by FINSEQ_1:32; then y = <*>A by A5,FINSEQ_1:32; hence thesis by A1,TARSKI:def 1; end; f is non empty by FUNCOP_1:19,RELAT_1:60; hence thesis by A3,A4; end; end; theorem h is non empty iff dom h <> {} by RELAT_1:60,64; theorem Th2: for A being non empty set, a being Element of A holds {<*>A} -->a is homogeneous quasi_total non empty PartFunc of A*,A proof let A be non empty set, a be Element of A; set f = {<*>A} -->a; A1: dom f = {<*>A} & rng f = {a} by FUNCOP_1:14,19; A2: dom f c= A* proof let z; assume z in dom f; then z = <*>A by A1,TARSKI:def 1; hence thesis by FINSEQ_1:def 11; end; rng f c= A proof let z; assume z in rng f; then z = a by A1,TARSKI:def 1; hence thesis; end; then reconsider f as PartFunc of A*,A by A2,RELSET_1:11; A3: f is homogeneous proof let x,y be FinSequence of A; assume x in dom f & y in dom f; then x = <*>A & y = <*>A by A1,TARSKI:def 1; hence thesis; end; f is quasi_total proof let x,y be FinSequence of A; assume A4: len x = len y & x in dom f; then x = <*>A by A1,TARSKI:def 1; then len x = 0 by FINSEQ_1:32; then y = <*>A by A4,FINSEQ_1:32; hence thesis by A1,TARSKI:def 1; end; hence thesis by A3,FUNCOP_1:19,RELAT_1:60; end; theorem Th3: for A being non empty set, a being Element of A holds {<*>A} -->a is Element of PFuncs(A*,A) proof let A be non empty set, a be Element of A; set f = {<*>A} -->a; A1: dom f = {<*>A} & rng f = {a} by FUNCOP_1:14,19; A2: dom f c= A* proof let z; assume z in dom f; then z = <*>A by A1,TARSKI:def 1; hence thesis by FINSEQ_1:def 11; end; rng f c= A proof let z; assume z in rng f; then z = a by A1,TARSKI:def 1; hence thesis; end; then reconsider f as PartFunc of A*,A by A2,RELSET_1:11; f in PFuncs(A*,A) by PARTFUN1:119; hence {<*>A} -->a is Element of PFuncs(A*,A); end; definition let A; mode PFuncFinSequence of A is FinSequence of PFuncs(A*,A); canceled; end; definition struct (1-sorted) UAStr (# carrier -> set, charact -> PFuncFinSequence of the carrier #); end; definition cluster non empty strict UAStr; existence proof consider D being non empty set, c being PFuncFinSequence of D; take UAStr (#D,c #); thus the carrier of UAStr (#D,c #) is non empty; thus thesis; end; end; definition let D be non empty set, c be PFuncFinSequence of D; cluster UAStr (#D,c #) -> non empty; coherence proof thus the carrier of UAStr (#D,c #) is non empty; end; end; definition let A; let IT be PFuncFinSequence of A; attr IT is homogeneous means :Def4: for n,h st n in dom IT & h = IT.n holds h is homogeneous; end; definition let A; let IT be PFuncFinSequence of A; attr IT is quasi_total means :Def5: for n,h st n in dom IT & h = IT.n holds h is quasi_total; end; definition let F be Function; redefine attr F is non-empty means :Def6: for n being set st n in dom F holds F.n is non empty; compatibility proof hereby assume F is non-empty; then A1: not {} in rng F by RELAT_1:def 9; let i be set; assume i in dom F; hence F.i is non empty by A1,FUNCT_1:def 5; end; assume A2: for n being set st n in dom F holds F.n is non empty; assume {} in rng F; then ex i being set st i in dom F & F.i = {} by FUNCT_1:def 5; hence contradiction by A2; end; end; definition let A be non empty set; let x be Element of PFuncs(A*,A); redefine func <*x*> -> PFuncFinSequence of A; coherence proof <*x*> is FinSequence of PFuncs(A*,A); hence thesis; end; end; definition let A be non empty set; cluster homogeneous quasi_total non-empty PFuncFinSequence of A; existence proof consider a being Element of A; reconsider f = {<*>A} -->a as PartFunc of A*,A by Th2; reconsider f as Element of PFuncs(A*,A) by PARTFUN1:119; take <*f*>; thus <*f*> is homogeneous proof let n; let h be PartFunc of A*,A; assume A1: n in dom <*f*> & h =<*f*>.n; then n in {1} by FINSEQ_1:4,def 8; then h = <*f*>.1 by A1,TARSKI:def 1; then h = f & f is homogeneous PartFunc of A*,A by Th2,FINSEQ_1:def 8; hence thesis; end; thus <*f*> is quasi_total proof let n; let h be PartFunc of A*,A; assume A2: n in dom <*f*> & h =<*f*>.n; then n in {1} by FINSEQ_1:4,def 8; then h = <*f*>.1 by A2,TARSKI:def 1; then h = f & f is quasi_total PartFunc of A*,A by Th2,FINSEQ_1:def 8; hence thesis; end; thus <*f*> is non-empty proof let n be set; assume A3: n in dom <*f*>; then reconsider n as Nat; n in {1} by A3,FINSEQ_1:4,def 8; then n = 1 by TARSKI:def 1; then <*f*>.n=f by FINSEQ_1:def 8; hence thesis by Th2; end; end; end; definition let IT be UAStr; attr IT is partial means :Def7: the charact of IT is homogeneous; attr IT is quasi_total means :Def8: the charact of IT is quasi_total; attr IT is non-empty means :Def9: the charact of IT <> {} & the charact of IT is non-empty; end; reserve A for non empty set, h for PartFunc of A*,A , x,y for FinSequence of A, a for Element of A; theorem Th4: for x be Element of PFuncs(A*,A) st x = {<*>A} --> a holds <*x*> is homogeneous quasi_total non-empty proof let x be Element of PFuncs(A*,A) such that A1: x = {<*>A} --> a; reconsider f=x as PartFunc of A*,A by PARTFUN1:121; A2: for n,h st n in dom <*x*> & h = <*x*>.n holds h is homogeneous proof let n,h; assume A3: n in dom <*x*> & h =<*x*>.n; then n in {1} by FINSEQ_1:4,def 8; then h = <*x*>.1 by A3,TARSKI:def 1; then h = x & f is homogeneous PartFunc of A*,A by A1,Th2,FINSEQ_1:def 8; hence thesis; end; A4: for n,h st n in dom <*x*> & h = <*x*>.n holds h is quasi_total proof let n,h; assume A5: n in dom <*x*> & h =<*x*>.n; then n in {1} by FINSEQ_1:4,def 8; then h = <*x*>.1 by A5,TARSKI:def 1; then h = x & f is quasi_total PartFunc of A*,A by A1,Th2,FINSEQ_1:def 8; hence thesis; end; for n being set st n in dom <*x*> holds <*x*>.n is non empty proof let n be set; assume n in dom <*x*>; then n in {1} by FINSEQ_1:4,def 8; then <*x*>.n = <*x*>.1 by TARSKI:def 1; then <*x*>.n = x & f is non empty PartFunc of A*,A by A1,Th2,FINSEQ_1:def 8 ; hence thesis; end; hence thesis by A2,A4,Def4,Def5,Def6; end; definition cluster quasi_total partial non-empty strict non empty UAStr; existence proof consider A be non empty set; consider a be Element of A; reconsider w = {<*>A} --> a as Element of PFuncs(A*,A) by Th3; set U1 = UAStr (# A, <*w*> #); take U1; A1: the charact of U1 is quasi_total & the charact of U1 is homogeneous & the charact of U1 is non-empty by Th4; the charact of U1 <> {} proof assume A2: the charact of U1 = {}; len(the charact of U1) = 1 by FINSEQ_1:56; hence contradiction by A2,FINSEQ_1:25; end; hence thesis by A1,Def7,Def8,Def9; end; end; definition let U1 be partial UAStr; cluster the charact of U1 -> homogeneous; coherence by Def7; end; definition let U1 be quasi_total UAStr; cluster the charact of U1 -> quasi_total; coherence by Def8; end; definition let U1 be non-empty UAStr; cluster the charact of U1 -> non-empty non empty; coherence by Def9; end; definition mode Universal_Algebra is quasi_total partial non-empty non empty UAStr; end; reserve U1 for partial non-empty non empty UAStr; definition let A; let f be homogeneous non empty PartFunc of A*,A; func arity(f) -> Nat means x in dom f implies it = len x; existence proof ex n st for x st x in dom f holds n = len x proof A1: dom f <> {} by RELAT_1:64; consider x being Element of dom f; dom f c= A* by RELSET_1:12; then x in A* by A1,TARSKI:def 3; then reconsider x as FinSequence of A by FINSEQ_1:def 11; take n = len x; let y; assume y in dom f; hence n = len y by Def1; end; hence thesis; end; uniqueness proof let n,m such that A2: (for x st x in dom f holds n = len x) & for x st x in dom f holds m = len x; A3: dom f <> {} by RELAT_1:64; consider x being Element of dom f; dom f c= A* by RELSET_1:12; then x in A* by A3,TARSKI:def 3; then reconsider x as FinSequence of A by FINSEQ_1:def 11; n = len x & m = len x by A2,A3; hence thesis; end; end; theorem Th5: for U1 holds for n st n in dom the charact of(U1) holds (the charact of(U1)).n is PartFunc of (the carrier of U1)*,the carrier of U1 proof let U1,n; set o = the charact of(U1); assume n in dom o; then o.n in rng o & rng o c= PFuncs((the carrier of U1)*, the carrier of U1) by FINSEQ_1:def 4,FUNCT_1:def 5; hence thesis by PARTFUN1:121; end; definition let U1; func signature U1 ->FinSequence of NAT means len it = len the charact of(U1) & for n st n in dom it holds for h be homogeneous non empty PartFunc of (the carrier of U1 )*,the carrier of U1 st h = (the charact of(U1)).n holds it.n = arity(h); existence proof defpred P[Nat,set] means for h be homogeneous non empty PartFunc of (the carrier of U1 )*,the carrier of U1 st h = (the charact of(U1)).$1 holds $2 = arity(h); A1: now let m; assume m in Seg len the charact of(U1); then m in dom the charact of(U1) by FINSEQ_1:def 3; then reconsider H=(the charact of(U1)).m as homogeneous non empty PartFunc of (the carrier of U1 )*,the carrier of U1 by Def4,Def6,Th5; take n=arity(H); thus P[m,n]; end; consider p be FinSequence of NAT such that A2: dom p = Seg(len the charact of(U1)) and A3: for m st m in Seg(len the charact of(U1)) holds P[m,p.m] from SeqDEx(A1); take p; thus len p = len the charact of(U1) by A2,FINSEQ_1:def 3; let n; assume A4: n in dom p; let h be homogeneous non empty PartFunc of (the carrier of U1 )*,the carrier of U1; assume h = (the charact of U1).n; hence p.n = arity(h) by A2,A3,A4; end; uniqueness proof let x,y be FinSequence of NAT; assume that A5: len x = len the charact of(U1) and A6: for n st n in dom x holds for h be homogeneous non empty PartFunc of (the carrier of U1 )*,the carrier of U1 st h = (the charact of(U1)).n holds x.n = arity(h) and A7: len y = len the charact of(U1) and A8: for n st n in dom y holds for h be homogeneous non empty PartFunc of (the carrier of U1 )*,the carrier of U1 st h = (the charact of(U1)).n holds y.n = arity(h); now let m; assume 1<=m & m<=len x; then m in Seg len x by FINSEQ_1:3; then A9: m in dom the charact of(U1) & m in dom x & m in dom y by A5,A7, FINSEQ_1:def 3; then reconsider h=(the charact of(U1)).m as homogeneous non empty PartFunc of (the carrier of U1 )*,the carrier of U1 by Def4,Def6,Th5; x.m=arity(h) & y.m=arity(h) by A6,A8,A9; hence x.m=y.m; end; hence thesis by A5,A7,FINSEQ_1:18; end; end;

Back to top