:: Preliminaries to Circuits, II
:: by Yatsuka Nakamura , Piotr Rudnicki , Andrzej Trybulec and Pauline N. Kawamoto
::
:: Received December 13, 1994
:: Copyright (c) 1994-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies MSUALG_1, GLIB_000, SUBSET_1, XBOOLE_0, UNIALG_2, STRUCT_0,
RELAT_1, TARSKI, FUNCT_1, FUNCOP_1, PBOOLE, CARD_3, FINSEQ_1, MARGREL1,
NAT_1, PARTFUN1, PRELAMB, MSAFREE, MSUALG_3, TREES_4, REALSET1, MSUALG_2,
FINSET_1, PRALG_1, CARD_1, TREES_2, DTCONSTR, TREES_3, ZFMISC_1, LANG1,
TDGROUP, TREES_1, MSAFREE2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NAT_1, CARD_1,
RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, FINSEQ_1, FUNCT_2, CARD_3, TREES_1,
TREES_2, TREES_3, TREES_4, PBOOLE, STRUCT_0, MSUALG_1, FINSEQ_2, MSAFREE,
MSUALG_2, FUNCOP_1, DTCONSTR, LANG1, PRE_POLY, RELSET_1, MSUALG_3;
constructors XXREAL_0, NAT_1, MSUALG_3, MSAFREE, SEQ_4, RELSET_1, PRE_POLY,
FINSEQ_2, NUMBERS;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCOP_1, FINSET_1, TREES_1,
CARD_3, TREES_2, TREES_3, PRE_CIRC, STRUCT_0, DTCONSTR, RELAT_1,
MSUALG_1, MSUALG_2, MSAFREE, ORDINAL1, PBOOLE, FINSEQ_1;
requirements BOOLE, SUBSET;
definitions TARSKI, FINSET_1, MSUALG_2, FUNCT_1, PBOOLE;
equalities MSUALG_1, FUNCOP_1;
expansions MSUALG_1, FINSET_1, MSUALG_2, PBOOLE;
theorems TARSKI, ZFMISC_1, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, TREES_3,
TREES_4, SUBSET_1, CARD_3, FUNCOP_1, PBOOLE, MSUALG_1, MSUALG_2, MSAFREE,
CARD_2, CARD_1, DTCONSTR, LANG1, PRE_CIRC, RELAT_1, RELSET_1, XBOOLE_0,
XBOOLE_1, FINSET_1, PARTFUN1, FINSEQ_2, XTUPLE_0;
schemes DOMAIN_1, PBOOLE, MSAFREE1, FUNCT_1;
begin
::---------------------------------------------------------------------------
:: Many Sorted Signatures
::---------------------------------------------------------------------------
definition
let S be ManySortedSign;
mode Vertex of S is Element of S;
end;
definition
let S be non empty ManySortedSign;
func SortsWithConstants S -> Subset of S equals
:Def1:
{ v where v is
SortSymbol of S : v is with_const_op } if S is non void otherwise {};
coherence
proof
hereby
defpred P[SortSymbol of S] means $1 is with_const_op;
assume S is non void;
{ v where v is SortSymbol of S : P[v] } is Subset of S from DOMAIN_1
:sch 7;
hence { v where v is SortSymbol of S : v is with_const_op } is Subset of
S;
end;
assume S is void;
thus thesis by SUBSET_1:1;
end;
consistency;
end;
definition
let G be non empty ManySortedSign;
func InputVertices G -> Subset of G equals
(the carrier of G) \ rng the ResultSort of G;
coherence;
func InnerVertices G -> Subset of G equals
rng the ResultSort of G;
coherence;
end;
theorem
for G being void non empty ManySortedSign holds InputVertices G = the
carrier of G;
theorem Th2:
for G being non void non empty ManySortedSign, v being Vertex of
G st v in InputVertices G holds not ex o being OperSymbol of G st
the_result_sort_of o = v
proof
let G be non void non empty ManySortedSign, v be Vertex of G;
assume
A1: v in InputVertices G;
let o be OperSymbol of G such that
A2: the_result_sort_of o = v;
o in the carrier' of G;
then o in dom the ResultSort of G by FUNCT_2:def 1;
then v in rng the ResultSort of G by A2,FUNCT_1:def 3;
hence contradiction by A1,XBOOLE_0:def 5;
end;
theorem Th3:
for G being non empty ManySortedSign holds SortsWithConstants G
c= InnerVertices G
proof
let G be non empty ManySortedSign;
per cases;
suppose
G is void;
hence thesis by Def1;
end;
suppose
A1: G is non void;
let x be object;
assume
A2: x in SortsWithConstants G;
SortsWithConstants G = {v where v is SortSymbol of G:v is
with_const_op } by A1,Def1;
then consider x9 being SortSymbol of G such that
A3: x9=x and
A4: x9 is with_const_op by A2;
ex o being OperSymbol of G st (the Arity of G).o = {} & ( the
ResultSort of G).o = x9 by A4;
hence thesis by A1,A3,FUNCT_2:4;
end;
end;
theorem
for G being non empty ManySortedSign holds InputVertices G misses
SortsWithConstants G
proof
let G be non empty ManySortedSign;
InputVertices G misses InnerVertices G by XBOOLE_1:79;
hence thesis by Th3,XBOOLE_1:63;
end;
definition
let IT be non empty ManySortedSign;
attr IT is with_input_V means
:Def4:
InputVertices IT <> {};
end;
registration
cluster non void with_input_V for non empty ManySortedSign;
existence
proof
{} in {{},{{}}} by TARSKI:def 2;
then reconsider g = {{}}-->{} as Function of {{}},{{},{{} }} by FUNCOP_1:46
;
{} in {{},{{}}}* by FINSEQ_1:49;
then reconsider f = {{}}-->{} as Function of {{}},{{},{{}}}* by FUNCOP_1:46
;
take c = ManySortedSign (# {{},{{}}}, {{}}, f, g #);
rng the ResultSort of c = {{}} by FUNCOP_1:8;
then {{}} in the carrier of c & not {{}} in rng the ResultSort of c by
TARSKI:def 2;
then InputVertices c <> {} by XBOOLE_0:def 5;
hence thesis;
end;
end;
registration
let G be with_input_V non empty ManySortedSign;
cluster InputVertices G -> non empty;
coherence by Def4;
end;
registration
let G be non void non empty ManySortedSign;
cluster InnerVertices G -> non empty;
coherence
proof
dom the ResultSort of G = the carrier' of G by FUNCT_2:def 1;
hence thesis by RELAT_1:42;
end;
end;
definition
let S be non empty ManySortedSign;
let MSA be non-empty MSAlgebra over S;
mode InputValues of MSA -> ManySortedSet of InputVertices S means
for v
being Vertex of S st v in InputVertices S holds it.v in (the Sorts of MSA).v;
existence
proof
set e = the Element of product(the Sorts of MSA);
set p = e | InputVertices S;
A1: dom the Sorts of MSA = the carrier of S & ex g being Function st e = g
& dom g = dom the Sorts of MSA &
for x being object st x in dom the Sorts of MSA
holds g.x in (the Sorts of MSA).x by CARD_3:def 5,PARTFUN1:def 2;
reconsider p as ManySortedSet of InputVertices S;
take p;
let v be Vertex of S;
assume v in InputVertices S;
then p.v = e.v by FUNCT_1:49;
hence thesis by A1;
end;
end;
:: Generalize this for arbitrary subset of the carrier
definition
let S be non empty ManySortedSign;
attr S is Circuit-like means
:Def6:
for S9 being non void non empty
ManySortedSign st S9 = S for o1, o2 being OperSymbol of S9 st
the_result_sort_of o1 = the_result_sort_of o2 holds o1 = o2;
end;
registration
cluster void -> Circuit-like for non empty ManySortedSign;
coherence;
end;
registration
cluster non void Circuit-like strict for non empty ManySortedSign;
existence
proof
{} in {{}}* by FINSEQ_1:49;
then reconsider f = {{}}-->{} as Function of {{}},{{}}* by FUNCOP_1:46;
reconsider g = {{}}-->{} as Function of {{}},{{}};
take c = ManySortedSign(#{{}},{{}},f,g#);
c is Circuit-like
proof
let S be non void non empty ManySortedSign;
assume
A1: S = c;
let v1, v2 be OperSymbol of S such that
the_result_sort_of v1 = the_result_sort_of v2;
thus v1 = {} by A1,TARSKI:def 1
.= v2 by A1,TARSKI:def 1;
end;
hence thesis;
end;
end;
definition
let IIG be Circuit-like non void non empty ManySortedSign;
let v be Vertex of IIG such that
A1: v in InnerVertices IIG;
func action_at v -> OperSymbol of IIG means
the_result_sort_of it = v;
existence
proof
consider x being object such that
A2: x in dom the ResultSort of IIG and
A3: (the ResultSort of IIG).x = v by A1,FUNCT_1:def 3;
reconsider x as OperSymbol of IIG by A2;
take x;
thus thesis by A3;
end;
uniqueness by Def6;
end;
begin
::---------------------------------------------------------------------------
:: Free Many Sorted Algebras
::---------------------------------------------------------------------------
theorem
for S being non void non empty ManySortedSign, A being MSAlgebra over
S, o being OperSymbol of S, p being FinSequence st len p = len the_arity_of o &
for k being Nat st k in dom p holds p.k in (the Sorts of A).((the_arity_of o)/.
k) holds p in Args (o, A)
proof
let S be non void non empty ManySortedSign, A be MSAlgebra over S, o be
OperSymbol of S, p be FinSequence such that
A1: len p = len the_arity_of o and
A2: for k being Nat st k in dom p holds p.k in (the Sorts of A).((
the_arity_of o)/.k);
set D = (the Sorts of A) * the_arity_of o;
A3: dom p = dom the_arity_of o by A1,FINSEQ_3:29;
rng the_arity_of o c= the carrier of S;
then rng the_arity_of o c= dom the Sorts of A by PARTFUN1:def 2;
then
A4: dom p = dom D by A3,RELAT_1:27;
A5: now
let x be object;
assume
A6: x in dom D;
then reconsider k = x as Nat;
D.k = (the Sorts of A).((the_arity_of o).k) by A6,FUNCT_1:12
.= (the Sorts of A).((the_arity_of o)/.k) by A3,A4,A6,PARTFUN1:def 6;
hence p.x in D.x by A2,A4,A6;
end;
dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then ((the Sorts of A)# * the Arity of S).o = (the Sorts of A)#.(
the_arity_of o) by FUNCT_1:13
.= product ((the Sorts of A) * the_arity_of o) by FINSEQ_2:def 5;
hence thesis by A4,A5,CARD_3:def 5;
end;
definition
let S be non void non empty ManySortedSign, MSA be non-empty MSAlgebra over
S;
func FreeEnv MSA -> free strict non-empty MSAlgebra over S equals
FreeMSA
(the Sorts of MSA);
coherence by MSAFREE:17;
end;
definition
let S be non void non empty ManySortedSign, MSA be non-empty MSAlgebra over
S;
func Eval MSA -> ManySortedFunction of FreeEnv MSA, MSA means
it
is_homomorphism FreeEnv MSA, MSA & for s being SortSymbol of S, x, y being set
st y in FreeSort(the Sorts of MSA, s) & y = root-tree [x, s] & x in (the Sorts
of MSA).s holds it.s.y = x;
existence
proof
reconsider A = FreeGen the Sorts of MSA as free GeneratorSet of FreeEnv
MSA by MSAFREE:16;
defpred P[object,object] means
ex s being SortSymbol of S, f being Function of A
.s, (the Sorts of MSA).s st f = $2 & s = $1 & for x, y being set st y in A.s &
y = root-tree [x, s] & x in (the Sorts of MSA).s holds f.y = x;
A1: for i being object st i in the carrier of S
ex j being object st P[i,j]
proof
let i be object;
assume i in the carrier of S;
then reconsider s = i as SortSymbol of S;
defpred P[object,object] means $1 = root-tree[$2, s];
A2: for e being object st e in A.s
ex u being object st u in (the Sorts of MSA).s & P[e,u]
proof
let e be object;
assume e in A.s;
then e in FreeGen(s,the Sorts of MSA) by MSAFREE:def 16;
then consider a be set such that
A3: a in (the Sorts of MSA).s & e = root-tree [a,s] by MSAFREE:def 15;
thus thesis by A3;
end;
consider j being Function such that
A4: dom j = A.s & rng j c= (the Sorts of MSA).s & for e being object st
e in A.s holds P[e,j.e] from FUNCT_1:sch 6(A2);
reconsider f = j as Function of A.s, (the Sorts of MSA).s by A4,
FUNCT_2:def 1,RELSET_1:4;
take j, s;
take f;
thus f = j & s = i;
let x, y be set such that
A5: y in A.s and
A6: y = root-tree [x, s] and
x in (the Sorts of MSA).s;
y = root-tree[j.y, s] by A4,A5;
then [x, s] = [j.y, s] by A6,TREES_4:4;
hence thesis by XTUPLE_0:1;
end;
consider f being ManySortedSet of the carrier of S such that
A7: for i being object st i in the carrier of S holds P[i,f.i] from
PBOOLE:sch 3(A1);
now
let x be object;
assume x in dom f;
then x in the carrier of S;
then P[x,f.x] by A7;
hence f.x is Function;
end;
then reconsider f as ManySortedFunction of the carrier of S by
FUNCOP_1:def 6;
now
let i be object;
assume i in the carrier of S;
then P[i,f.i] by A7;
hence f.i is Function of A.i, (the Sorts of MSA).i;
end;
then reconsider f as ManySortedFunction of A, the Sorts of MSA by
PBOOLE:def 15;
consider IT being ManySortedFunction of FreeEnv MSA, MSA such that
A8: IT is_homomorphism FreeEnv MSA, MSA and
A9: IT || A = f by MSAFREE:def 5;
take IT;
thus IT is_homomorphism FreeEnv MSA, MSA by A8;
let s be SortSymbol of S, x, y be set;
A10: ex t being SortSymbol of S, g being Function of A.t, (the Sorts of MSA
).t st g = f.s & t = s & for x, y being set st y in A.t & y = root-tree [x, t]
& x in (the Sorts of MSA).t holds g.y = x by A7;
assume that
y in FreeSort(the Sorts of MSA, s) and
A11: y = root-tree [x, s] & x in (the Sorts of MSA).s;
y in FreeGen(s, the Sorts of MSA) by A11,MSAFREE:def 15;
then
A12: y in A.s by MSAFREE:def 16;
hence IT.s.y = (IT.s | (A.s)).y by FUNCT_1:49
.= f.s.y by A9,MSAFREE:def 1
.= x by A11,A12,A10;
end;
uniqueness
proof
defpred P[set,set,set] means $3 = root-tree [$2, $1];
let IT1, IT2 be ManySortedFunction of FreeEnv MSA, MSA;
reconsider IT19 = IT1, IT29 = IT2 as ManySortedFunction of FreeMSA (the
Sorts of MSA), MSA;
assume IT1 is_homomorphism FreeEnv MSA, MSA;
then
A13: IT19 is_homomorphism FreeMSA (the Sorts of MSA), MSA;
assume
A14: for s being SortSymbol of S, x, y being set st y in FreeSort(the
Sorts of MSA, s) & y = root-tree [x, s] & x in (the Sorts of MSA).s holds IT1.s
.y = x;
A15: for s being SortSymbol of S, x,y being set st y in FreeGen(s,the
Sorts of MSA) holds IT19.s.y = x iff P[s,x,y]
proof
let s be SortSymbol of S, x,y be set;
assume
A16: y in FreeGen(s,the Sorts of MSA);
then consider a being set such that
A17: a in (the Sorts of MSA).s and
A18: y = root-tree [a,s] by MSAFREE:def 15;
y in (FreeSort the Sorts of MSA).s by A16;
then
A19: y in FreeSort(the Sorts of MSA, s) by MSAFREE:def 11;
hence IT19.s.y = x implies y = root-tree [x, s] by A14,A17,A18;
assume y = root-tree [x, s];
then [x,s] = [a,s] by A18,TREES_4:4;
then x = a by XTUPLE_0:1;
hence thesis by A14,A19,A17,A18;
end;
assume IT2 is_homomorphism FreeEnv MSA, MSA;
then
A20: IT29 is_homomorphism FreeMSA (the Sorts of MSA), MSA;
assume
A21: for s being SortSymbol of S, x, y being set st y in FreeSort(the
Sorts of MSA, s) & y = root-tree [x, s] & x in (the Sorts of MSA).s holds IT2.s
.y = x;
A22: for s being SortSymbol of S, x,y being set st y in FreeGen(s,the
Sorts of MSA) holds IT29.s.y = x iff P[s,x,y]
proof
let s be SortSymbol of S, x,y be set;
assume
A23: y in FreeGen(s,the Sorts of MSA);
then consider a being set such that
A24: a in (the Sorts of MSA).s and
A25: y = root-tree [a,s] by MSAFREE:def 15;
y in (FreeSort the Sorts of MSA).s by A23;
then
A26: y in FreeSort(the Sorts of MSA, s) by MSAFREE:def 11;
hence IT29.s.y = x implies y = root-tree [x, s] by A21,A24,A25;
assume y = root-tree [x, s];
then [x,s] = [a,s] by A25,TREES_4:4;
then x = a by XTUPLE_0:1;
hence thesis by A21,A26,A24,A25;
end;
IT19 = IT29 from MSAFREE1:sch 3(A13,A15,A20,A22);
hence thesis;
end;
end;
theorem Th6:
for S being non void non empty ManySortedSign, A being non-empty
MSAlgebra over S holds the Sorts of A is GeneratorSet of A
proof
let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S;
reconsider theA = the MSAlgebra of A as non-empty MSAlgebra over S;
reconsider AA = the Sorts of A as non-empty MSSubset of theA by PBOOLE:def 18
;
set GAA = GenMSAlg AA;
A1: the Sorts of GAA is MSSubset of A by MSUALG_2:def 9;
now
let B be MSSubset of A such that
A2: B = the Sorts of GAA;
reconsider C = B as MSSubset of theA;
A3: C is opers_closed by A2,MSUALG_2:def 9;
A4: now
let o be OperSymbol of S;
C is_closed_on o by A3;
then
A5: rng ((Den(o,the MSAlgebra of A))|((C# * the Arity of S).o)) c= (C *
the ResultSort of S).o;
thus B is_closed_on o by A5;
end;
hence B is opers_closed;
reconsider OAB = Opers(A, B) as ManySortedFunction of (C# * the Arity of S
),(C * the ResultSort of S);
A6: now
let o be OperSymbol of S;
A7: C is_closed_on o & Den (o, A) = Den (o, the MSAlgebra of A) by A3;
thus OAB.o = o/.B by MSUALG_2:def 8
.= (Den(o,A)) | ((B# * the Arity of S).o) by A4,MSUALG_2:def 7
.= o/.C by A7,MSUALG_2:def 7;
end;
the Charact of GAA = Opers(theA, C) by A2,MSUALG_2:def 9;
hence the Charact of GAA = Opers(A,B) by A6,MSUALG_2:def 8;
end;
then reconsider GAA as strict non-empty MSSubAlgebra of A by A1,
MSUALG_2:def 9;
reconsider BB = the Sorts of A as MSSubset of A by PBOOLE:def 18;
A8: now
let U1 be MSSubAlgebra of A;
A9: now
let B be MSSubset of theA such that
A10: B = the Sorts of U1;
reconsider C = B as MSSubset of A;
A11: C is opers_closed by A10,MSUALG_2:def 9;
A12: now
let o be OperSymbol of S;
C is_closed_on o by A11;
then
A13: rng ((Den(o,A))|((C# * the Arity of S).o)) c= (C * the ResultSort
of S).o;
thus B is_closed_on o by A13;
end;
hence B is opers_closed;
reconsider OAB = Opers(theA, B) as ManySortedFunction of (C# * the Arity
of S),(C * the ResultSort of S);
A14: now
let o be OperSymbol of S;
A15: Den (o, A) = Den (o, the MSAlgebra of A);
A16: C is_closed_on o by A11;
thus OAB.o = o/.B by MSUALG_2:def 8
.= (Den(o,A)) | ((B# * the Arity of S).o) by A12,A15,MSUALG_2:def 7
.= o/.C by A16,MSUALG_2:def 7;
end;
the Charact of U1 = Opers(A, C) by A10,MSUALG_2:def 9;
hence the Charact of U1 = Opers(theA,B) by A14,MSUALG_2:def 8;
end;
the Sorts of U1 is MSSubset of the MSAlgebra of A by MSUALG_2:def 9;
then reconsider U2 = U1 as MSSubAlgebra of theA by A9,MSUALG_2:def 9;
assume BB is MSSubset of U1;
then GAA is MSSubAlgebra of U2 by MSUALG_2:def 17;
hence GAA is MSSubAlgebra of U1;
end;
BB is MSSubset of GenMSAlg AA by MSUALG_2:def 17;
then GenMSAlg AA = GenMSAlg BB by A8,MSUALG_2:def 17;
then the Sorts of GenMSAlg BB = the Sorts of A by MSUALG_2:21;
hence thesis by MSAFREE:def 4;
end;
definition
let S be non empty ManySortedSign;
let IT be MSAlgebra over S;
attr IT is finitely-generated means
:Def10:
for S9 being non void non empty
ManySortedSign st S9 = S for A being MSAlgebra over S9 st A = IT ex G being
GeneratorSet of A st G is finite-yielding if S is not void otherwise the Sorts
of IT is finite-yielding;
consistency;
end;
definition
let S be non empty ManySortedSign;
let IT be MSAlgebra over S;
attr IT is finite-yielding means
the Sorts of IT is finite-yielding;
end;
registration
let S be non empty ManySortedSign;
cluster finite-yielding -> finitely-generated for
non-empty MSAlgebra over S;
coherence
proof
let A be non-empty MSAlgebra over S;
assume
A1: A is finite-yielding;
per cases;
case
S is non void;
let S9 be non void non empty ManySortedSign such that
A2: S9 = S;
let A9 be MSAlgebra over S9;
assume A9 = A;
then reconsider G = the Sorts of A as GeneratorSet of A9 by A2,Th6;
take G;
thus thesis by A1;
end;
case
S is void;
thus thesis by A1;
end;
end;
end;
definition
let S be non empty ManySortedSign;
func Trivial_Algebra S -> strict MSAlgebra over S means
:Def12:
the Sorts of it = (the carrier of S) --> {0};
existence
proof
reconsider f = (the carrier of S) --> {0} as ManySortedSet of the carrier
of S;
set Ch = the ManySortedFunction of f# * the Arity of S, f * the ResultSort of S
;
take MSAlgebra(#f,Ch#);
thus thesis;
end;
uniqueness
proof
let A1,A2 be strict MSAlgebra over S such that
A1: the Sorts of A1 = (the carrier of S) --> {0} and
A2: the Sorts of A2 = (the carrier of S) --> {0};
set B = the Sorts of A1;
A3: dom(the ResultSort of S) = the carrier' of S by FUNCT_2:def 1;
now
let i be object;
set A = (B*the ResultSort of S).i;
assume
A4: i in the carrier' of S;
then
A5: A = B.((the ResultSort of S).i) by A3,FUNCT_1:13
.= {0} by A1,A4,FUNCOP_1:7,FUNCT_2:5;
then reconsider A as non empty set;
reconsider f1=(the Charact of A1).i, f2=(the Charact of A2).i as
Function of (B# * the Arity of S).i, A by A1,A2,A4,PBOOLE:def 15;
now
let x be object;
assume
A6: x in (B# * the Arity of S).i;
then f1.x in A by FUNCT_2:5;
then
A7: f1.x = 0 by A5,TARSKI:def 1;
f2.x in A by A6,FUNCT_2:5;
hence f1.x = f2.x by A5,A7,TARSKI:def 1;
end;
hence (the Charact of A1).i = (the Charact of A2).i by FUNCT_2:12;
end;
hence thesis by A1,A2,PBOOLE:3;
end;
end;
registration
let S be non empty ManySortedSign;
cluster finite-yielding non-empty strict for MSAlgebra over S;
existence
proof
take T = Trivial_Algebra S;
A1: the Sorts of T = (the carrier of S) --> {0} by Def12;
the Sorts of T is finite-yielding
by A1,FUNCOP_1:7;
hence T is finite-yielding;
thus T is non-empty by A1;
thus thesis;
end;
end;
definition
let IT be non empty ManySortedSign;
attr IT is monotonic means
for A being finitely-generated non-empty
MSAlgebra over IT holds A is finite-yielding;
end;
registration
cluster non void finite monotonic Circuit-like for
non empty ManySortedSign;
existence
proof
{} in {{}}* by FINSEQ_1:49;
then reconsider f = {[{},{{}}]}-->{} as Function of {[{},{{}}]},{{}}* by
FUNCOP_1:46;
reconsider g = {[{},{{}}]}-->{} as Function of {[{},{{}}]},{{}};
take S = ManySortedSign (# {{}}, {[{},{{}}]}, f, g #);
thus S is non void;
thus S is finite;
thus S is monotonic
proof
reconsider S9 = S as non void non empty ManySortedSign;
let A be finitely-generated non-empty MSAlgebra over S;
reconsider A9 = A as non-empty MSAlgebra over S9;
set s = the SortSymbol of S9;
consider G being GeneratorSet of A9 such that
A1: G is finite-yielding by Def10;
reconsider Gs = G.s as finite set by A1;
set o = the OperSymbol of S9;
set T = s .--> (G.s \/ { Den(o,A9).{} });
set O = (o .--> Den(o,A9));
reconsider G9 = G as MSSubset of A9;
let i be object;
A2: s = {} by TARSKI:def 1;
then reconsider T as non-empty ManySortedSet of the carrier of S;
assume i in the carrier of S;
then
A3: i = s by A2,TARSKI:def 1;
reconsider T9 = T as ManySortedSet of the carrier of S9;
A4: Args(o,A9) = (the Sorts of A9)#.((the Arity of S).o) by FUNCT_2:15
.= (the Sorts of A9)#.<*>the carrier of S9
.= {{}} by PRE_CIRC:2;
then
A5: dom Den(o,A9) = {{}} by FUNCT_2:def 1;
A6: now
let i be object;
assume
A7: i in the carrier' of S;
then i = [{},{{}}] by TARSKI:def 1;
then
A8: i = o by TARSKI:def 1;
(T# * the Arity of S).i = T#.((the Arity of S).i) by A7,FUNCT_2:15
.= T#.(<*>the carrier of S)
.= {{}} by PRE_CIRC:2;
then reconsider
Oi = O.i as Function of (T# * the Arity of S).i, Result(o,
A9) by A4,A8,FUNCOP_1:72;
O.i = Den(o,A9) by A8,FUNCOP_1:72;
then
A9: rng (Oi) = { Den(o,A9).{} } by A5,FUNCT_1:4;
(T * the ResultSort of S).i = T.((the ResultSort of S).i) by A7,
FUNCT_2:15
.= T.s by A2
.= G.s \/ { Den(o,A9).{} } by FUNCOP_1:72;
then rng (Oi) c= (T * the ResultSort of S).i by A9,XBOOLE_1:7;
hence O.i is Function of (T# * the Arity of S).i, (T * the ResultSort
of S).i by FUNCT_2:6;
end;
A10: o = [{},{{}}] by TARSKI:def 1;
then reconsider
O as ManySortedFunction of (T# * the Arity of S), (T * the
ResultSort of S) by A6,PBOOLE:def 15;
A11: now
let B be MSSubset of A9;
assume
A12: B = the Sorts of MSAlgebra (# T, O #);
thus
A13: B is opers_closed
proof
let o9 be OperSymbol of S9;
let x be object;
assume
A14: x in rng ((Den(o9,A9))|((B# * the Arity of S9).o9));
A15: o9 = o by A10,TARSKI:def 1;
A16: dom the ResultSort of S9 = {[{},{{}}]} & (the ResultSort of S9)
.o = s by A2;
A17: Den(o,A9)|{{}} = Den(o,A9) by A5;
(B# * the Arity of S).o = B#.((the Arity of S).o) by FUNCT_2:15
.= T#.(<*>the carrier of S) by A12
.= {{}} by PRE_CIRC:2;
then
ex y being object st y in dom(Den(o,A9)) & x = (Den(o,A9)).y
by A15,A17
,A14,FUNCT_1:def 3;
then x = Den(o,A9).{} by A4,TARSKI:def 1;
then
A18: x in { Den(o,A9).{} } by TARSKI:def 1;
B.s = (G.s \/ { Den(o,A9).{} }) by A12,FUNCOP_1:72;
then x in B.s by A18,XBOOLE_0:def 3;
hence thesis by A15,A16,FUNCT_1:13;
end;
now
let o9 be OperSymbol of S9;
(B# * the Arity of S9).o = B#.((the Arity of S9).o) by FUNCT_2:15
.= T#.(<*>the carrier of S9) by A12
.= {{}} by PRE_CIRC:2;
then (Den(o,A9)) | ((B# * the Arity of S9).o) = Den(o,A9) by A5;
then
A19: (the Charact of MSAlgebra (# T, O #)).o = (Den(o,A9)) | ((B# *
the Arity of S9).o) by FUNCOP_1:72;
o9 = o & B is_closed_on o by A10,A13,TARSKI:def 1;
hence (the Charact of MSAlgebra (# T, O #)).o9 = o9/.B by A19,
MSUALG_2:def 7;
end;
hence the Charact of MSAlgebra (# T, O #) = Opers(A9,B) by A12,
MSUALG_2:def 8;
end;
reconsider A99 = MSAlgebra (# T, O #) as non-empty MSAlgebra over S9 by
MSUALG_1:def 3;
A20: Result(o,A9) = (the Sorts of A9).((the ResultSort of S).o) by FUNCT_2:15
.= (the Sorts of A9).{};
T9 c= the Sorts of A9
proof
let i be object;
assume i in the carrier of S9;
then
A21: i = {} by TARSKI:def 1;
then
A22: T9.i = (G.s \/ { Den(o,A9).{} }) by A2;
G c= the Sorts of A9 by PBOOLE:def 18;
then
A23: G.s c= (the Sorts of A9).i by A2,A21;
dom Den(o,A9) = Args(o,A9) by FUNCT_2:def 1;
then {} in dom Den(o,A9) by A4,TARSKI:def 1;
then Den(o,A9).{} in rng Den(o,A9) by FUNCT_1:def 3;
then { Den(o,A9).{} } c= (the Sorts of A9).i by A20,A21,ZFMISC_1:31;
hence thesis by A22,A23,XBOOLE_1:8;
end;
then the Sorts of MSAlgebra (# T, O #) is MSSubset of A9 by PBOOLE:def 18
;
then reconsider A99 as strict MSSubAlgebra of A9 by A11,MSUALG_2:def 9;
A24: now
let U1 be MSSubAlgebra of A9;
assume
A25: G9 is MSSubset of U1;
now
Constants(A9) is MSSubset of U1 by MSUALG_2:10;
then Constants(A9) c= the Sorts of U1 by PBOOLE:def 18;
then (Constants(A9)).s c= (the Sorts of U1).s;
then
A26: Constants(A9,s) c= (the Sorts of U1).s by MSUALG_2:def 4;
A27: {} in dom Den(o,A9) by A5,TARSKI:def 1;
then Den(o,A9).{} in rng Den(o,A9) by FUNCT_1:def 3;
then reconsider
b = Den(o,A9).{} as Element of (the Sorts of A9).s by A20,
TARSKI:def 1;
let i be object;
A28: (the Arity of S9).o = {} & ex X being non empty set st X =(the
Sorts of A9) .s & Constants(A9,s) = { a where a is Element of X : ex o be
OperSymbol of S9 st ( the Arity of S9).o = {} & (the ResultSort of S9).o = s &
a in rng Den (o, A9)} by MSUALG_2:def 3;
b in rng Den(o,A9) by A27,FUNCT_1:def 3;
then Den(o,A9).{} in Constants(A9,s) by A2,A28;
then
A29: { Den(o,A9).{} } c= (the Sorts of U1).s by A26,ZFMISC_1:31;
G c= (the Sorts of U1) by A25,PBOOLE:def 18;
then
A30: (the Sorts of A99).s = G.s \/ { Den(o,A9).{} } & G.s c= (the
Sorts of U1).s by FUNCOP_1:72;
assume i in the carrier of S9;
then i = s by A2,TARSKI:def 1;
hence (the Sorts of A99).i c= (the Sorts of U1).i by A30,A29,
XBOOLE_1:8;
end;
then the Sorts of A99 c= the Sorts of U1;
hence A99 is MSSubAlgebra of U1 by MSUALG_2:8;
end;
now
let i be object;
assume i in the carrier of S9;
then
A31: i = s by A2,TARSKI:def 1;
(the Sorts of A99).s = G.s \/ { Den(o,A9).{} } by FUNCOP_1:72;
hence G9.i c= (the Sorts of A99).i by A31,XBOOLE_1:7;
end;
then G9 c= the Sorts of A99;
then G9 is MSSubset of A99 by PBOOLE:def 18;
then s.--> (G.s \/ { Den(o, A9).{} }) = the Sorts of GenMSAlg(G) by A24,
MSUALG_2:def 17
.= the Sorts of A9 by MSAFREE:def 4;
then (the Sorts of A).i = Gs \/ { Den(o,A9).{} } by A3,FUNCOP_1:72;
hence thesis;
end;
thus S is Circuit-like
proof
let S9 be non void non empty ManySortedSign;
assume
A32: S9 = S;
let o1, o2 be OperSymbol of S9 such that
the_result_sort_of o1 = the_result_sort_of o2;
o1 = [{},{{}}] by A32,TARSKI:def 1;
hence thesis by A32,TARSKI:def 1;
end;
end;
end;
theorem Th7:
for S being non void non empty ManySortedSign for X being
non-empty ManySortedSet of the carrier of S, v be SortSymbol of S, e be Element
of (the Sorts of FreeMSA X).v holds e is finite DecoratedTree
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, v be SortSymbol of S, e be Element of (the Sorts of FreeMSA X
).v;
FreeMSA X = MSAlgebra (# FreeSort(X), FreeOper(X) #) by MSAFREE:def 14;
then (the Sorts of FreeMSA X).v = FreeSort (X, v) by MSAFREE:def 11;
then
A1: e in TS(DTConMSA(X)) by TARSKI:def 3;
then reconsider e9 = e as DecoratedTree;
dom e9 is finite by A1;
hence thesis by FINSET_1:10;
end;
theorem
for S being non void non empty ManySortedSign, X being non-empty
finite-yielding ManySortedSet of the carrier of S holds FreeMSA X is
finitely-generated
proof
let S be non void non empty ManySortedSign, X be non-empty finite-yielding
ManySortedSet of the carrier of S;
per cases;
case
S is non void;
reconsider G = FreeGen X as GeneratorSet of FreeMSA X;
let S9 be non void non empty ManySortedSign such that
A1: S9 = S;
let A be MSAlgebra over S9;
assume A = FreeMSA X;
then reconsider G as GeneratorSet of A by A1;
take G;
thus G is finite-yielding
proof
let i be object;
reconsider Gi = G.i as set;
assume i in the carrier of S9;
then reconsider iS = i as SortSymbol of S by A1;
reconsider Xi = X.iS as non empty finite set;
now
defpred P[object,object] means $1 = root-tree [$2,i];
A2: for e being object st e in Gi
ex u being object st u in Xi & P[e,u]
proof
A3: Gi = FreeGen(iS,X) by MSAFREE:def 16;
let e be object;
assume e in Gi;
then consider u being set such that
A4: u in Xi & e = root-tree[u,i] by A3,MSAFREE:def 15;
take u;
thus thesis by A4;
end;
consider f being Function such that
A5: dom f = Gi and
A6: rng f c= Xi and
A7: for e being object st e in Gi holds P[e,f.e] from FUNCT_1:sch 6
(A2);
take f;
f is one-to-one
proof
let x1, x2 be object;
assume that
A8: x1 in dom f and
A9: x2 in dom f and
A10: f.x1 = f.x2;
thus x1 = root-tree[f.x2,i] by A5,A7,A8,A10
.= x2 by A5,A7,A9;
end;
hence
ex f being Function st f is one-to-one & dom f = Gi & rng f c= Xi
by A5,A6;
end;
then card Gi c= card Xi or card Gi in card Xi by CARD_1:10;
hence thesis by CARD_2:49;
end;
end;
case
S is void;
hence thesis;
end;
end;
theorem
for S being non void non empty ManySortedSign, A being non-empty
MSAlgebra over S, v being Vertex of S, e being Element of (the Sorts of FreeEnv
A).v st v in InputVertices S ex x being Element of (the Sorts of A).v st e =
root-tree [x, v]
proof
let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S,
v be Vertex of S, e be Element of (the Sorts of FreeEnv A).v;
FreeEnv A = MSAlgebra (# FreeSort(the Sorts of A), FreeOper(the Sorts of
A) #) by MSAFREE:def 14;
then e in (FreeSort(the Sorts of A)).v;
then e in FreeSort(the Sorts of A, v) by MSAFREE:def 11;
then
e in {a where a is Element of TS(DTConMSA(the Sorts of A)): (ex x being
set st x in (the Sorts of A).v & a = root-tree [x,v]) or ex o being OperSymbol
of S st [o,the carrier of S] = a.{} & the_result_sort_of o = v} by
MSAFREE:def 10;
then consider a being Element of TS(DTConMSA(the Sorts of A)) such that
A1: a = e and
A2: (ex x being set st x in (the Sorts of A).v & a = root-tree [x,v]) or
ex o being OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of
o = v;
assume v in InputVertices S;
then consider x being set such that
A3: x in (the Sorts of A).v and
A4: a = root-tree [x,v] by A2,Th2;
reconsider x as Element of (the Sorts of A).v by A3;
take x;
thus thesis by A1,A4;
end;
theorem Th10:
for S being non void non empty ManySortedSign, X being non-empty
ManySortedSet of the carrier of S, o being OperSymbol of S, p being
DTree-yielding FinSequence st [o,the carrier of S]-tree p in (the Sorts of
FreeMSA X).(the_result_sort_of o) holds len p = len the_arity_of 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 DTree-yielding FinSequence;
set s = the_result_sort_of o;
assume
A1: [o,the carrier of S]-tree p in (the Sorts of FreeMSA X).(
the_result_sort_of o);
FreeMSA X = MSAlgebra (# FreeSort X, FreeOper X #) by MSAFREE:def 14;
then [o,the carrier of S]-tree p in FreeSort(X,s) by A1,MSAFREE:def 11;
then
A2: [o,the carrier of S]-tree p in {a where a is Element of TS(DTConMSA(X)):
(ex x being set st x in X.s & a = root-tree [x,s]) or ex o being OperSymbol of
S st [o,the carrier of S] = a.{} & the_result_sort_of o = s} by
MSAFREE:def 10;
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 reconsider nt = [o,the carrier of S] as NonTerminal of DTConMSA(X) by
MSAFREE:6;
reconsider O = [:the carrier' of S,{the carrier of S}:] \/ Union(coprod X)
as non empty set;
reconsider R = REL(X) as Relation of O, O*;
A3: DTConMSA(X) = DTConstrStr (# O, R #) by MSAFREE:def 8;
then reconsider TSDT = TS(DTConMSA(X)) as Subset of FinTrees(O);
reconsider c = nt as Element of O by A3;
for x being object st x in TSDT holds x is DecoratedTree of O;
then reconsider TSDT as DTree-set of O by TREES_3:def 6;
consider a being Element of TS(DTConMSA(X)) such that
A4: a = [o,the carrier of S]-tree p and
(ex x being set st x in X.s & a = root-tree [x,s]) or ex o being
OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = s by A2
;
a.{} = [o,the carrier of S] by A4,TREES_4:def 4;
then consider ts being FinSequence of TS(DTConMSA(X)) such that
A5: a = nt-tree ts and
A6: nt ==> roots ts by DTCONSTR:10;
reconsider ts9 = ts as FinSequence of TSDT;
reconsider b = roots ts9 as FinSequence of O;
reconsider b as Element of O* by FINSEQ_1:def 11;
[c, b] in R by A6,A3,LANG1:def 1;
then
A7: len roots ts = len (the_arity_of o) by MSAFREE:def 7;
reconsider ts as DTree-yielding FinSequence;
A8: dom roots ts = dom ts by TREES_3:def 18;
ts = p by A4,A5,TREES_4:15;
hence thesis by A7,A8,FINSEQ_3:29;
end;
theorem Th11:
for S being non void non empty ManySortedSign, X being non-empty
ManySortedSet of the carrier of S, o being OperSymbol of S, p being
DTree-yielding FinSequence st [o,the carrier of S]-tree p in (the Sorts of
FreeMSA X).(the_result_sort_of o) holds for i being Nat st i in dom
the_arity_of o holds p.i in (the Sorts of FreeMSA X).((the_arity_of o).i)
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 DTree-yielding FinSequence;
A1: FreeMSA X = MSAlgebra (# FreeSort X, FreeOper X #) by MSAFREE:def 14;
assume
A2: [o,the carrier of S]-tree p in (the Sorts of FreeMSA X).(
the_result_sort_of o);
now
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 reconsider
nt = [o,the carrier of S] as NonTerminal of DTConMSA(X) by MSAFREE:6;
set rso = the_result_sort_of o;
reconsider ao = the_arity_of o as Element of (the carrier of S)*;
let i be Nat;
assume
A3: i in dom the_arity_of o;
then ao.i in rng ao by FUNCT_1:def 3;
then reconsider s = ao.i as SortSymbol of S;
A4: (the Sorts of FreeMSA X).s = FreeSort(X,s) by A1,MSAFREE:def 11
.= FreeSort(X,(the_arity_of o)/.i) by A3,PARTFUN1:def 6;
[o,the carrier of S]-tree p in FreeSort(X,rso) by A2,A1,MSAFREE:def 11;
then
[o,the carrier of S]-tree p in {a where a is Element of TS(DTConMSA(X)
): (ex x being set st x in X.rso & a = root-tree [x,rso]) or ex o being
OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = rso}
by MSAFREE:def 10;
then consider a being Element of TS(DTConMSA(X)) such that
A5: a = [o,the carrier of S]-tree p and
(ex x being set st x in X.rso & a = root-tree [x,rso]) or ex o being
OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = rso;
a.{} = [o,the carrier of S] by A5,TREES_4:def 4;
then consider ts being FinSequence of TS(DTConMSA(X)) such that
A6: a = nt-tree ts and
A7: nt ==> roots ts by DTCONSTR:10;
nt = Sym(o,X) by MSAFREE:def 9;
then
A8: ts in ((FreeSort X)# * (the Arity of S)).o by A7,MSAFREE:10;
dom p = Seg len p & dom the_arity_of o = Seg len the_arity_of o by
FINSEQ_1:def 3;
then
A9: i in dom p by A2,A3,Th10;
reconsider ts as DTree-yielding FinSequence;
ts = p by A5,A6,TREES_4:15;
hence p.i in (the Sorts of FreeMSA X).((the_arity_of o).i) by A9,A8,A4,
MSAFREE:9;
end;
hence thesis;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, v be Vertex of S;
cluster -> finite non empty Function-like Relation-like for Element of (the
Sorts of FreeMSA X).v;
coherence
proof
let e be Element of (the Sorts of FreeMSA X).v;
reconsider e9 = e as DecoratedTree by Th7;
thus e is finite by Th7;
dom e9 is Tree;
hence e is non empty;
thus thesis by Th7;
end;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, v be Vertex of S;
cluster Function-like Relation-like for
Element of (the Sorts of FreeMSA X).v;
existence
proof
set e = the Element of (the Sorts of FreeMSA X).v;
take e;
thus thesis;
end;
end;
registration
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, v be Vertex of S;
cluster -> DecoratedTree-like for
Function-like Relation-like Element of (the
Sorts of FreeMSA X).v;
coherence by Th7;
end;
registration
let IIG be non void non empty ManySortedSign;
let X be non-empty ManySortedSet of the carrier of IIG, v be Vertex of IIG;
cluster finite for Element of (the Sorts of FreeMSA X).v;
existence
proof
set e = the Element of (the Sorts of FreeMSA X).v;
take e;
thus thesis;
end;
end;
theorem
for S being non void non empty ManySortedSign, X being non-empty
ManySortedSet of the carrier of S, v being Vertex of S, o being OperSymbol of S
, e being Element of (the Sorts of FreeMSA X).v st e.{} = [o,the carrier of S]
ex p being DTree-yielding FinSequence st len p = len the_arity_of o & for i
being Nat st i in dom p holds p.i in (the Sorts of FreeMSA X).((the_arity_of o)
.i)
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, v be Vertex of S, o be OperSymbol of S, e be Element of (the
Sorts of FreeMSA X).v such that
A1: e.{} = [o,the carrier of S];
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 reconsider nt = [o,the carrier of S] as NonTerminal of DTConMSA(X) by
MSAFREE:6;
FreeMSA X = MSAlgebra (# FreeSort X, FreeOper X #) by MSAFREE:def 14;
then (the Sorts of FreeMSA X).v = FreeSort(X,v) by MSAFREE:def 11;
then e in FreeSort(X,v);
then
e in {a where a is Element of TS(DTConMSA(X)): (ex x being set st x in X
.v & a = root-tree [x,v]) or ex o being OperSymbol of S st [o,the carrier of S]
= a.{} & the_result_sort_of o = v} by MSAFREE:def 10;
then consider a being Element of TS(DTConMSA(X)) such that
A2: a = e and
A3: (ex x being set st x in X.v & a = root-tree [x,v]) or ex o being
OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = v;
consider x being set such that
A4: x in X.v & a = root-tree[x,v] or ex o being OperSymbol of S st [o,
the carrier of S] = a.{} & the_result_sort_of o = v by A3;
consider p being FinSequence of TS(DTConMSA(X)) such that
A5: a = nt-tree p and
nt ==> roots p by A1,A2,DTCONSTR:10;
now
assume a = root-tree[x,v];
then
A6: a.{} = [x,v] by TREES_4:3;
A7: for X be set holds not X in X;
a.{} = [o,the carrier of S] by A5,TREES_4:def 4;
then the carrier of S = v by A6,XTUPLE_0:1;
hence contradiction by A7;
end;
then consider o9 being OperSymbol of S such that
A8: [o9,the carrier of S] = a.{} and
A9: the_result_sort_of o9 = v by A4;
A10: o = o9 by A1,A2,A8,XTUPLE_0:1;
then
A11: len p = len the_arity_of o by A2,A5,A9,Th10;
then dom p = Seg len the_arity_of o by FINSEQ_1:def 3
.= dom the_arity_of o by FINSEQ_1:def 3;
then for i being Nat st i in dom p holds p.i in (the Sorts of FreeMSA X).((
the_arity_of o).i) by A2,A5,A9,A10,Th11;
hence thesis by A11;
end;
definition
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, v be SortSymbol of S, e be Element of (the Sorts of FreeMSA X
).v;
func depth e -> Nat means
ex dt being finite DecoratedTree, t being finite
Tree st dt = e & t = dom dt & it = height t;
existence
proof
reconsider dt = e as finite DecoratedTree;
reconsider domdt = dom dt as finite Tree;
take height domdt, dt, domdt;
thus thesis;
end;
uniqueness;
end;