:: The Correspondence Between Monotonic Many Sorted Signatures
:: and Well-Founded Graphs. {P}art {II}
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received April 10, 1996
:: Copyright (c) 1996-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 NUMBERS, NAT_1, MSUALG_1, STRUCT_0, SUBSET_1, RELAT_1, FUNCT_1,
ZFMISC_1, TARSKI, MCART_1, XBOOLE_0, GRAPH_1, PBOOLE, XXREAL_0, MSAFREE,
MSAFREE2, WAYBEL_0, TREES_2, FINSEQ_1, GRAPH_2, ARYTM_3, MSATERM,
FINSET_1, TREES_1, TREES_9, TREES_4, MARGREL1, ORDINAL4, RFINSEQ,
ARYTM_1, CARD_1, PARTFUN1, FUNCT_6, TREES_3, TREES_A, MSSCYC_1, CARD_3,
UNIALG_2, MSSCYC_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, MCART_1, STRUCT_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
RFINSEQ, FINSET_1, TREES_1, TREES_2, TREES_3, TREES_4, CARD_3, GRAPH_1,
GRAPH_2, PBOOLE, MSUALG_1, MSUALG_2, MSAFREE, MSAFREE2, XXREAL_2,
CIRCUIT1, TREES_9, MSATERM, MSSCYC_1, FINSEQ_1, XXREAL_0;
constructors WELLORD2, REAL_1, NAT_1, RFINSEQ, MSUALG_2, MSATERM, CIRCUIT1,
GRAPH_2, MSSCYC_1, XXREAL_2, RELSET_1, XTUPLE_0, XREAL_0;
registrations XBOOLE_0, ORDINAL1, FINSET_1, XREAL_0, NAT_1, MEMBERED,
FINSEQ_1, TREES_2, TREES_3, PRE_CIRC, STRUCT_0, GRAPH_1, MSUALG_1,
MSAFREE, MSATERM, MSAFREE2, MSSCYC_1, XXREAL_2, PBOOLE, RELSET_1,
FUNCT_1, TREES_1, CARD_2, XTUPLE_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, MSAFREE2;
equalities MSAFREE2;
expansions TARSKI, MSAFREE2;
theorems TARSKI, NAT_1, MCART_1, ZFMISC_1, MSSCYC_1, FUNCT_6, CARD_1, CARD_3,
FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5,
RFINSEQ, TREES_1, TREES_2, TREES_3, TREES_4, DTCONSTR, MSUALG_1, MSAFREE,
MSAFREE2, CIRCUIT1, TREES_9, MSATERM, XBOOLE_1, ORDINAL1, XREAL_1,
XXREAL_0, PARTFUN1, XXREAL_2, FINSET_1, CARD_2, XTUPLE_0;
schemes NAT_1, FINSEQ_1, FUNCT_2, RECDEF_1, FRAENKEL, TOPREAL1, PBOOLE,
XBOOLE_0;
begin
reserve k, n for Nat;
definition
let S be ManySortedSign;
defpred P[object] means
ex op, v being set st $1 = [op, v] & op in the carrier'
of S & v in the carrier of S & ex n being Nat, args being Element of (the
carrier of S)* st (the Arity of S).op = args & n in dom args & args.n = v;
func InducedEdges S -> set means
:Def1:
for x being object holds x in it iff ex
op, v being set st x = [op, v] & op in the carrier' of S & v in the carrier of
S & ex n being Nat, args being Element of (the carrier of S)* st (the Arity of
S).op = args & n in dom args & args.n = v;
existence
proof
set XX = [:the carrier' of S, the carrier of S:];
consider X being set such that
A1: for x being object holds x in X iff x in XX & P[x] from XBOOLE_0:sch
1;
take X;
let x be object;
thus x in X implies P[x] by A1;
assume
A2: P[x];
then x in XX by ZFMISC_1:def 2;
hence thesis by A1,A2;
end;
uniqueness
proof
for X1,X2 being set st (for x being object holds x in X1 iff P[x])
& (for
x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
hence thesis;
end;
end;
theorem Th1:
for S being ManySortedSign holds InducedEdges S c= [: the
carrier' of S, the carrier of S :]
proof
let S be ManySortedSign;
let x be object;
assume x in InducedEdges S;
then ex op, v being set st x = [op, v] & op in the carrier' of S & v in the
carrier of S & ex n being Nat, args being Element of (the carrier of S)* st (
the Arity of S).op = args & n in dom args & args.n = v by Def1;
hence thesis by ZFMISC_1:def 2;
end;
definition
let S be ManySortedSign;
set IE = InducedEdges S, IV = the carrier of S;
func InducedSource S -> Function of InducedEdges S, the carrier of S means
:
Def2: for e being object st e in InducedEdges S holds it.e = e`2;
existence
proof
deffunc F(object)= $1 `2;
A1: for x being object st x in IE holds F(x) in IV
proof
let x be object;
assume
A2: x in IE;
IE c= [: the carrier' of S, IV :] by Th1;
hence thesis by A2,MCART_1:10;
end;
ex f being Function of InducedEdges S,the carrier of S st
for x be object
st x in InducedEdges S holds f.x = F(x) from FUNCT_2:sch 2 (A1);
hence thesis;
end;
uniqueness
proof
let F1, F2 be Function of IE, IV such that
A3: for e being object st e in IE holds F1.e = e`2 and
A4: for e being object st e in IE holds F2.e = e`2;
A5: now
let x be object;
assume
A6: x in IE;
then F1.x = x`2 by A3;
hence F1.x = F2.x by A4,A6;
end;
now
assume IV is empty;
then [:the carrier' of S, IV:] is empty by ZFMISC_1:90;
hence IE is empty by Th1,XBOOLE_1:3;
end;
then dom F1 = IE & dom F2 = IE by FUNCT_2:def 1;
hence F1 = F2 by A5,FUNCT_1:2;
end;
set OS = the carrier' of S, RS = the ResultSort of S;
func InducedTarget S -> Function of InducedEdges S, the carrier of S means
:
Def3: for
e being object st e in InducedEdges S holds it.e = (the ResultSort of S)
.e`1;
existence
proof
deffunc F(object) = RS.($1)`1;
A7: for x being object st x in IE holds F(x) in IV
proof
let x be object;
assume
A8: x in IE;
IE c= [: OS, IV :] by Th1;
then x`1 in OS & x`2 in IV by A8,MCART_1:10;
hence thesis by FUNCT_2:5;
end;
ex f being Function of InducedEdges S, the carrier of S st for x be
object st x in InducedEdges S holds f.x = F(x) from FUNCT_2:sch 2 (A7);
hence thesis;
end;
uniqueness
proof
let F1, F2 be Function of IE, IV such that
A9: for e being object st e in IE holds F1.e = RS.e`1 and
A10: for e being object st e in IE holds F2.e = RS.e`1;
A11: now
let x be object;
assume
A12: x in IE;
then F1.x = RS.x`1 by A9;
hence F1.x = F2.x by A10,A12;
end;
now
assume IV is empty;
then [:the carrier' of S, IV:] is empty by ZFMISC_1:90;
hence IE is empty by Th1,XBOOLE_1:3;
end;
then dom F1 = IE & dom F2 = IE by FUNCT_2:def 1;
hence F1 = F2 by A11,FUNCT_1:2;
end;
end;
definition
let S be non empty ManySortedSign;
func InducedGraph S -> Graph equals
MultiGraphStruct (# the carrier of S,
InducedEdges S, InducedSource S, InducedTarget S #);
coherence;
end;
theorem Th2:
for S being non void non empty ManySortedSign, X being
non-empty ManySortedSet of the carrier of S, v being SortSymbol of S, n st 1<=n
holds (ex t being Element of (the Sorts of FreeMSA X).v st depth t = n) iff (ex
c being directed Chain of InducedGraph S st len c = n & (vertex-seq c).(len c +
1) = v)
proof
let S be non void non empty ManySortedSign, X be non-empty ManySortedSet
of the carrier of S, v be SortSymbol of S, n;
assume
A1: 1<=n;
set G = InducedGraph S;
FreeMSA X = MSAlgebra(#FreeSort(X),FreeOper(X)#)by MSAFREE:def 14;
then
A2: (the Sorts of FreeMSA X).v = FreeSort(X,v) by MSAFREE:def 11;
A3: FreeSort(X,v) c= S-Terms X by MSATERM:12;
thus (ex t being Element of (the Sorts of FreeMSA X).v st depth t = n)
implies ex c being directed Chain of InducedGraph S st len c = n & (vertex-seq
c).(len c +1) = v
proof
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
set D = (the carrier' of G)*;
given t being Element of (the Sorts of FreeMSA X).v such that
A4: depth t = n;
t in FreeSort(X,v) by A2;
then reconsider t9 = t as Term of S, X by A3;
consider dt being finite DecoratedTree, tr being finite Tree such that
A5: dt = t & tr = dom dt and
A6: depth t = height tr by MSAFREE2:def 14;
not t is root by A1,A4,A5,A6,TREES_1:42,TREES_9:def 1;
then consider o being OperSymbol of S such that
A7: t9.{} =[o, the carrier of S] by MSSCYC_1:20;
consider a being ArgumentSeq of Sym(o,X) such that
A8: t = [o,the carrier of S]-tree a by A7,MSATERM:10;
set args = the_arity_of o;
A9: dom a = dom args by MSATERM:22;
consider p being FinSequence of NAT such that
A10: p in tr and
A11: len p = height tr by TREES_1:def 12;
consider i being Nat, T being DecoratedTree, q being Node of T
such that
A12: i < len a and
T = a.(i+1) and
A13: p = <*i*>^q by A1,A4,A5,A6,A10,A11,A8,CARD_1:27,TREES_4:11;
defpred P[Nat, set, set] means ex t1, t2 being Term of S, X st t1 = t|(p|
$1) & t2 = t|(p|($1+1)) & ex o being OperSymbol of S, rs1 being SortSymbol of S
, Ck being Element of D st Ck = $2 & $3 = <*[o,rs1]*>^Ck & [o,the carrier of S]
= t1.{} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of G;
1<=i+1 & i+1<=len a by A12,NAT_1:11,13;
then
A14: i+1 in dom args by A9,FINSEQ_3:25;
then reconsider rs1 = args.(i+1) as SortSymbol of S by DTCONSTR:2;
set e1 = [o,rs1];
A15: (the Arity of S).o = the_arity_of o by MSUALG_1:def 1;
then
A16: [o,rs1] in InducedEdges S by A14,Def1;
then reconsider E9 = the carrier' of G as non empty set;
reconsider e19 = e1 as Element of E9 by A14,A15,Def1;
reconsider C19 = <*e19*> as Element of D by FINSEQ_1:def 11;
A17: for k being Nat st 1 <= k & k < n1 for x being Element of
D ex y being Element of D st P[k,x,y]
proof
let k be Nat;
set pk9 = p/^k;
k<=k+1 by NAT_1:13;
then
A18: Seg k c= Seg (k+1) by FINSEQ_1:5;
k in NAT by ORDINAL1:def 12;
then
reconsider pk = p|k, pk1 = p|(k+1) as Node of t by A5,A10,MSSCYC_1:19;
assume that
1 <= k and
A19: k < n1;
A20: len pk9 = n - k by A4,A6,A11,A19,RFINSEQ:def 1;
then
A21: len pk9 <> 0 by A19;
then
A22: 1 in dom pk9 by CARD_1:27,FINSEQ_5:6;
reconsider t1 = t9|pk, t2 = t9|pk1 as Term of S, X by MSATERM:29;
p = pk^pk9 by RFINSEQ:8;
then
A23: pk9 in tr|pk by A5,A10,TREES_1:def 6;
then
A24: pk9 in dom t1 by A5,TREES_2:def 10;
A25: k+1<=n by A19,NAT_1:13;
then
A26: 1<=n-k by XREAL_1:19;
now
assume t1 is root;
then dom t1 = elementary_tree 0 by TREES_9:def 1;
hence contradiction by A20,A26,A24,TREES_1:42,def 12;
end;
then consider o being OperSymbol of S such that
A27: t1.{} =[o, the carrier of S] by MSSCYC_1:20;
consider a being ArgumentSeq of Sym(o,X) such that
A28: t1 = [o,the carrier of S]-tree a by A27,MSATERM:10;
A29: pk9|1 = <*pk9.1*> by A21,CARD_1:27,FINSEQ_5:20;
consider i being Nat, T being DecoratedTree, q being Node of
T such that
A30: i < len a and
T = a.(i+1) and
A31: pk9 = <*i*>^q by A21,A24,A28,CARD_1:27,TREES_4:11;
reconsider pk9 as Node of t1 by A5,A23,TREES_2:def 10;
reconsider p1 = pk9|(0+1) as Node of t1 by MSSCYC_1:19;
reconsider t29 = t1|p1 as Term of S, X;
A32: p|(k+1)|k = p|(k+1)|Seg k by FINSEQ_1:def 16
.= p|Seg (k+1)|Seg k by FINSEQ_1:def 16
.= p|Seg k by A18,FUNCT_1:51
.= pk by FINSEQ_1:def 16;
set args = the_arity_of o;
let x be Element of D;
A33: dom a = dom args by MSATERM:22;
A34: 1<=k+1 by NAT_1:11;
then
A35: k+1 in dom p by A4,A6,A11,A25,FINSEQ_3:25;
A36: len pk1 = k+1 by A4,A6,A11,A25,FINSEQ_1:59;
then
A37: k+1 in dom pk1 by A34,FINSEQ_3:25;
p1 = <*p.(k+1)*> by A4,A6,A11,A19,A22,A29,RFINSEQ:def 1
.= <*p/.(k+1)*> by A35,PARTFUN1:def 6
.= <*(p|(k+1))/.(k+1)*> by A37,FINSEQ_4:70
.= <*pk1.(k+1)*> by A37,PARTFUN1:def 6;
then pk1 = pk^p1 by A36,A32,RFINSEQ:7;
then
A38: t29 = t2 by TREES_9:3;
1<=i+1 & i+1<=len a by A30,NAT_1:11,13;
then
A39: i+1 in dom args by A33,FINSEQ_3:25;
then reconsider rs1 = args.(i+1) as SortSymbol of S by DTCONSTR:2;
set e1 = [o,rs1];
A40: (the Arity of S).o = the_arity_of o by MSUALG_1:def 1;
then [o,rs1] in InducedEdges S by A39,Def1;
then reconsider E9 = the carrier' of G as non empty set;
reconsider e19 = e1 as Element of E9 by A39,A40,Def1;
reconsider x9 = x as FinSequence of E9 by FINSEQ_1:def 11;
reconsider y = <*e19*>^x9 as Element of D by FINSEQ_1:def 11;
take y;
take t1, t2;
thus t1 = t|(p|k) & t2 = t|(p|(k+1));
take o, rs1, x;
thus x = x & y = <*[o,rs1]*>^x;
thus [o,the carrier of S] = t1.{} by A27;
pk9|1 = <*i*> by A31,A29,FINSEQ_1:41;
then t29 = a.(i+1) by A28,A30,TREES_4:def 4;
hence rs1 = the_sort_of t2 by A33,A39,A38,MSATERM:23;
thus thesis by A39,A40,Def1;
end;
consider C being FinSequence of D such that
A41: len C = n1 & (C.1 = C19 or n1 = 0) & for k being Nat
st 1 <= k & k < n1 holds P[k,C.k,C.(k+1)] from RECDEF_1:sch 4(A17);
defpred Z[Nat] means 1<=$1 & $1<=n implies ex Ck being directed Chain of G
, t1 being Term of S, X st Ck = C.$1 & len Ck = $1 & t1 = t|(p|$1) & (
vertex-seq Ck).(len Ck +1) = v & (vertex-seq Ck).1 = the_sort_of t1;
A42: for i be Nat st Z[i] holds Z[i+1]
proof
let k;
assume
A43: 1<=k & k<=n implies ex Ck being directed Chain of G, t1 being
Term of S, X st Ck = C.k & len Ck = k & t1 = t|(p|k) & (vertex-seq Ck).(len Ck
+1) = v & (vertex-seq Ck).1 = the_sort_of t1;
A44: k<=k+1 by NAT_1:11;
assume that
1<=k+1 and
A45: k+1<=n;
A46: k<n by A45,NAT_1:13;
per cases;
suppose
A47: k=0;
reconsider C1 = <*e1*> as directed Chain of G by A16,MSSCYC_1:5;
reconsider p1 = p|(0+1) as Node of t by A5,A10,MSSCYC_1:19;
reconsider t2 = t9|p1 as Term of S, X by MSATERM:29;
take C1, t2;
thus C1 = C.(k+1) by A1,A41,A47;
thus len C1 = k+1 by A47,FINSEQ_1:39;
thus t2 = t|(p|(k+1)) by A47;
reconsider p9=p as PartFunc of NAT, NAT;
A48: vertex-seq C1 = <*(the Source of G).e1, (the Target of G).e1*> by A16,
MSSCYC_1:7;
(vertex-seq C1).(len C1 +1) = (vertex-seq C1).(1+1) by FINSEQ_1:39
.= (the Target of G).e1 by A48
.= (the ResultSort of S).e1`1 by A16,Def3
.= (the ResultSort of S).o
.= the_result_sort_of o by MSUALG_1:def 2
.= the_sort_of t9 by A7,MSATERM:17
.= v by A2,MSATERM:def 5;
hence (vertex-seq C1).(len C1 +1) = v;
p|1 = <*p9.1*> by A1,A4,A6,A11,CARD_1:27,FINSEQ_5:20
.= <*p.1*>
.= <*i*> by A13,FINSEQ_1:41;
then
A50: t2 = a.(i+1) by A8,A12,TREES_4:def 4;
(vertex-seq C1).1 = (the Source of G).e1 by A48
.= e1`2 by A16,Def2
.= rs1
.= the_sort_of t2 by A9,A14,A50,MSATERM:23;
hence thesis;
end;
suppose
A51: k<>0;
consider t1, t2 being Term of S, X such that
A52: t1 = t|(p|k) and
A53: t2 = t|(p|(k+1)) and
A54: ex o being OperSymbol of S,rs1 being SortSymbol of S,Ck being
Element of D st Ck = C.k & C.(k+1) = <*[o,rs1]*>^Ck & [o,the carrier of S] = t1
.{}& rs1 = the_sort_of t2 & [o,rs1] in the carrier' of G by A41,A46,A51,
NAT_1:14;
consider o being OperSymbol of S, rs1 being SortSymbol of S, Ck9 being
Element of D such that
A55: Ck9 = C.k & C.(k+1) = <*[o,rs1]*>^Ck9 and
A56: [o,the carrier of S] = t1.{} and
A57: rs1 = the_sort_of t2 and
A58: [o,rs1] in the carrier' of G by A54;
A59: G is non void by A58;
reconsider C1 = <*[o,rs1]*> as directed Chain of G by A58,MSSCYC_1:5;
set e1 = [o,rs1];
A60: vertex-seq C1 = <*(the Source of G).e1, (the Target of G).e1*> by A58,
MSSCYC_1:7;
consider Ck being directed Chain of G, t19 being Term of S, X such
that
A61: Ck = C.k and
A62: len Ck = k and
A63: t19 = t|(p|k) and
A64: (vertex-seq Ck).(len Ck +1)=v and
A65: (vertex-seq Ck).1=the_sort_of t19 by A43,A45,A44,A51,NAT_1:14
,XXREAL_0:2;
(vertex-seq C1).(len C1 +1) = (vertex-seq C1).(1+1) by FINSEQ_1:39
.= (the Target of G).e1 by A60
.= (the ResultSort of S).e1`1 by A58,Def3
.= (the ResultSort of S).o
.= the_result_sort_of o by MSUALG_1:def 2
.= the_sort_of t1 by A56,MSATERM:17;
then reconsider
d = C1^Ck as directed Chain of G by A51,A62,A63,A65,A52,A59,CARD_1:27
,MSSCYC_1:15;
take d, t2;
thus d = C.(k+1) by A61,A55;
thus len d = len C1 + k by A62,FINSEQ_1:22
.= k+1 by FINSEQ_1:39;
thus t2 = t|(p|(k+1)) by A53;
thus (vertex-seq d).(len d +1) = v by A51,A62,A64,A59,CARD_1:27
,MSSCYC_1:16;
(vertex-seq C1).1 = (the Source of G).e1 by A60
.= e1`2 by A58,Def2
.= the_sort_of t2 by A57;
hence thesis by A51,A62,A59,CARD_1:27,MSSCYC_1:16;
end;
end;
A66: Z[ 0 ];
for k holds Z[k] from NAT_1:sch 2(A66, A42);
then
ex c being directed Chain of G, t1 being Term of S, X st c = C.n & len
c = n & t1 = t|(p|n) & (vertex-seq c).(len c +1) = v & ( vertex-seq c).1 =
the_sort_of t1 by A1;
hence thesis;
end;
given c being directed Chain of InducedGraph S such that
A67: len c = n and
A68: (vertex-seq c).(len c +1) = v;
set EG = the carrier' of G;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
deffunc F(object) = X.$1;
set TG = the Target of G;
set SG = the Source of G;
set D = S-Terms X;
set cS = the carrier of S;
A69: for e being object st e in cS holds F(e) <> {};
consider cX being ManySortedSet of cS such that
A70: for e being object st e in cS holds cX.e in F(e) from PBOOLE:sch 1 (
A69);
defpred P[Nat, set, set] means ex o being OperSymbol of S, rs1 being
SortSymbol of S, Ck, Ck1 being Term of S, X, a being ArgumentSeq of Sym(o,X) st
Ck = $2 & $3 = Ck1 & c.($1+1) = [o, rs1] & Ck1 = [o,cS]-tree a & (for i being
Nat st i in dom a ex t being Term of S,X st t = a.i & the_sort_of t = (
the_arity_of o).i & (the_sort_of t = rs1 & the_sort_of Ck = rs1 implies t = Ck)
& (the_sort_of t <> rs1 or the_sort_of Ck <> rs1 implies t = root-tree [cX.(
the_sort_of t), the_sort_of t]));
A71: c is FinSequence of the carrier' of InducedGraph S by MSSCYC_1:def 1;
A72: 1 in dom c by A1,A67,FINSEQ_3:25;
then reconsider EG as non empty set by A71;
c.1 in InducedEdges S by A71,A72,DTCONSTR:2;
then consider o, rs1 being set such that
A73: c.1 = [o, rs1] and
A74: o in the carrier' of S and
A75: rs1 in the carrier of S and
A76: ex n being Nat, args being Element of (the carrier of S)* st (the
Arity of S).o = args & n in dom args & args.n = rs1 by Def1;
reconsider rs1 as SortSymbol of S by A75;
reconsider o as OperSymbol of S by A74;
deffunc F(Nat) = root-tree [cX.((the_arity_of o).$1),(the_arity_of o).$1];
consider a being FinSequence such that
A77: len a = len the_arity_of o & for k be Nat st k in dom a holds a.k
= F(k) from FINSEQ_1:sch 2;
A78: dom a = Seg len a by FINSEQ_1:def 3;
A79: for i being Nat st i in dom a ex t being Term of S,X st t = a.i &
the_sort_of t = (the_arity_of o).i
proof
let i be Nat;
assume
A80: i in dom a;
set s = (the_arity_of o).i;
dom the_arity_of o = Seg len the_arity_of o by FINSEQ_1:def 3;
then reconsider s as SortSymbol of S by A77,A78,A80,DTCONSTR:2;
set x = cX.((the_arity_of o).i);
reconsider x as Element of X.s by A70;
reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4;
take t;
thus t = a.i by A77,A80;
thus thesis by MSATERM:14;
end;
A81: dom a = Seg len the_arity_of o by A77,FINSEQ_1:def 3;
reconsider a as ArgumentSeq of Sym(o,X) by A77,A79,MSATERM:24;
set C1 = [o,the carrier of S]-tree a;
reconsider C1 as Term of S, X by MSATERM:1;
A82: for k being Nat st 1 <= k & k < n1 for x being Element of D
ex y being Element of D st P[k,x,y]
proof
let k be Nat;
assume that
1 <= k and
A83: k < n1;
A84: 1<=k+1 by NAT_1:11;
k+1<=n by A83,NAT_1:13;
then k+1 in dom c by A67,A84,FINSEQ_3:25;
then reconsider ck1 = c.(k+1) as Element of EG by A71,DTCONSTR:2;
let x be Element of D;
consider o, rs1 being set such that
A85: ck1 = [o,rs1] and
A86: o in the carrier' of S and
A87: rs1 in cS and
ex n being Nat, args being Element of (the carrier of S)* st (the
Arity of S).o = args & n in dom args & args.n = rs1 by Def1;
reconsider rs1 as SortSymbol of S by A87;
reconsider o as OperSymbol of S by A86;
set DA = dom the_arity_of o;
set ar = the_arity_of o;
defpred P[object, object] means
(ar.$1 = rs1 & the_sort_of x = rs1 implies $2 =
x) & (ar.$1 <> rs1 or the_sort_of x <> rs1 implies $2 = root-tree [cX.(ar.$1),
ar.$1]);
A88: for e being object st e in DA ex u being object st u in D & P[e,u]
proof
let e be object;
assume
A89: e in DA;
per cases;
suppose
A90: ar.e = rs1 & the_sort_of x = rs1;
take x;
thus thesis by A90;
end;
suppose
A91: ar.e <> rs1 or the_sort_of x <> rs1;
reconsider s = (the_arity_of o).e as SortSymbol of S by A89,DTCONSTR:2;
reconsider x = cX.((the_arity_of o).e) as Element of X.s by A70;
reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4;
take t;
thus thesis by A91;
end;
end;
consider a being Function of DA,D such that
A92: for e being object st e in DA holds P[e,a.e] from FUNCT_2:sch 1 (
A88);
DA = Seg len ar by FINSEQ_1:def 3;
then reconsider a as FinSequence of D by FINSEQ_2:25;
A93: dom a = DA by FUNCT_2:def 1;
now
let i be Nat;
assume
A94: i in dom a;
then reconsider t = a.i as Term of S,X by DTCONSTR:2;
take t;
thus t = a.i;
per cases;
suppose
ar.i = rs1 & the_sort_of x = rs1;
hence the_sort_of t = ar.i by A92,A93,A94;
end;
suppose
A95: ar.i <> rs1 or the_sort_of x <> rs1;
reconsider s = (the_arity_of o).i as SortSymbol of S by A93,A94,
DTCONSTR:2;
A96: cX.((the_arity_of o).i) is Element of X.s by A70;
t = root-tree [cX.(ar.i),ar.i] by A92,A93,A94,A95;
hence the_sort_of t = ar.i by A96,MSATERM:14;
end;
end;
then reconsider a as ArgumentSeq of Sym(o,X) by A93,MSATERM:24;
reconsider y = [o,cS]-tree a as Term of S,X by MSATERM:1;
take y, o, rs1, x, y, a;
thus x = x & y = y;
thus c.(k+1) = [o, rs1] by A85;
thus y = [o,cS]-tree a;
let i be Nat;
assume
A97: i in dom a;
then reconsider t = a.i as Term of S,X by DTCONSTR:2;
take t;
thus t = a.i;
thus the_sort_of t = (the_arity_of o).i by A97,MSATERM:23;
hence thesis by A92,A93,A97;
end;
consider C being FinSequence of D such that
A98: len C = n1 & (C.1 = C1 or n1 = 0) & for k be Nat st 1
<= k & k < n1 holds P[k,C.k,C.(k+1)] from RECDEF_1:sch 4(A82);
defpred P[Nat] means 1<=$1 & $1<=n implies ex C0 being Term of S, X, o being
OperSymbol of S st C0 = C.$1 & o = (c.$1)`1 & the_sort_of C0 =
the_result_sort_of o & height dom C0 = $1;
A99: G is non void by A72;
A100: for k be Nat st P[k] holds P[k+1]
proof
let k;
assume
A101: 1<=k & k<=n implies ex Ck being Term of S, X, o being OperSymbol
of S st Ck = C.k & o = (c.k)`1 & the_sort_of Ck = the_result_sort_of o & height
dom Ck = k;
assume that
A102: 1<=k+1 and
A103: k+1<=n;
A104: k<n by A103,NAT_1:13;
A105: k<=k+1 by NAT_1:11;
then
A106: k<=n by A103,XXREAL_0:2;
per cases;
suppose
A107: k = 0;
take C1, o;
thus C1 = C.(k+1) by A1,A98,A107;
thus o = (c.(k+1))`1 by A73,A107;
reconsider w = doms a as FinTree-yielding FinSequence;
A108: dom doms a = dom a by TREES_3:37;
C1.{} = [o, cS] by TREES_4:def 4;
hence the_sort_of C1 = the_result_sort_of o by MSATERM:17;
consider i being Nat, args being Element of (the carrier of S)* such
that
A109: (the Arity of S).o = args and
A110: i in dom args and
args.i = rs1 by A76;
A111: dom args = Seg len args by FINSEQ_1:def 3;
A112: args = the_arity_of o by A109,MSUALG_1:def 1;
then reconsider t = a.i as Term of S, X by A77,A78,A110,A111,MSATERM:22;
(doms a).i = dom t by A77,A78,A110,A112,A111,FUNCT_6:22;
then
A113: dom C1 = tree doms a & dom t in rng w by A77,A78,A108,A110,A112,A111,
FUNCT_1:def 3,TREES_4:10;
reconsider dt = dom t as finite Tree;
A114: a.i = root-tree [cX.((the_arity_of o).i),(the_arity_of o).i] by A77,A81
,A110,A112,A111;
A115: now
let t9 be finite Tree;
assume t9 in rng w;
then consider j being Nat such that
A116: j in dom w and
A117: w.j = t9 by FINSEQ_2:10;
reconsider t99 = a.j as Term of S, X by A108,A116,MSATERM:22;
a.j = root-tree [cX.((the_arity_of o).j),(the_arity_of o).j] by A77
,A108,A116;
then
A118: dom t99 = elementary_tree 0 by TREES_4:3;
w.j = dom t99 by A108,A116,FUNCT_6:22;
hence height t9 <= height dt by A114,A117,A118,TREES_4:3;
end;
dom t = elementary_tree 0 by A114,TREES_4:3;
hence thesis by A107,A113,A115,TREES_1:42,TREES_3:79;
end;
suppose
A119: k <> 0;
then
A120: 1<=k by NAT_1:14;
then k in dom c by A67,A106,FINSEQ_3:25;
then reconsider ck = c.k as Element of EG by A71,DTCONSTR:2;
consider Ck being Term of S, X, o being OperSymbol of S such that
A121: Ck = C.k and
A122: o = (c.k)`1 & the_sort_of Ck = the_result_sort_of o and
A123: height dom Ck = k by A101,A103,A105,A119,NAT_1:14,XXREAL_0:2;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
consider o1 being OperSymbol of S, rs1 being SortSymbol of S, Ck9, Ck1
being Term of S, X, a being ArgumentSeq of Sym(o1,X) such that
A124: Ck9 = C.k and
A125: C.(kk+1) = Ck1 and
A126: c.(k+1) = [o1, rs1] and
A127: Ck1 = [o1,cS]-tree a and
A128: for i being Nat st i in dom a ex t being Term of S,X st t = a.
i & the_sort_of t = (the_arity_of o1).i & (the_sort_of t = rs1 & the_sort_of
Ck9 = rs1 implies t = Ck9) & (the_sort_of t <> rs1 or the_sort_of Ck9 <> rs1
implies t = root-tree [cX.(the_sort_of t), the_sort_of t]) by A98,A104,A119,
NAT_1:14;
set ck1 = c.(kk+1);
A129: k+1 in dom c by A67,A102,A103,FINSEQ_3:25;
then ck1 in EG by A71,DTCONSTR:2;
then consider o9, rs19 being set such that
A130: ck1=[o9, rs19] and
A131: o9 in the carrier' of S and
rs19 in the carrier of S and
A132: ex n being Nat, args being Element of (the carrier of S)* st (
the Arity of S).o9 = args & n in dom args & args.n = rs19 by Def1;
A133: o1 = o9 by A126,A130,XTUPLE_0:1;
take Ck1, o1;
thus Ck1 = C.(k+1) by A125;
thus o1 = (c.(k+1))`1 by A126;
Ck1.{} = [o1,cS] by A127,TREES_4:def 4;
hence the_sort_of Ck1 = the_result_sort_of o1 by MSATERM:17;
A134: dom Ck1 = tree doms a by A127,TREES_4:10;
reconsider ck1 as Element of EG by A71,A129,DTCONSTR:2;
reconsider w = doms a as FinTree-yielding FinSequence;
A135: len a = len the_arity_of o1 & dom a = Seg len a by FINSEQ_1:def 3
,MSATERM:22;
rs1 = rs19 by A126,A130,XTUPLE_0:1;
then consider
i being Nat, args being Element of (the carrier of S)* such
that
A136: (the Arity of S).o9 = args and
A137: i in dom args and
A138: args.i = rs1 by A132;
reconsider o9 as OperSymbol of S by A131;
A139: dom args = Seg len args by FINSEQ_1:def 3;
A140: args = the_arity_of o9 by A136,MSUALG_1:def 1;
then consider t being Term of S, X such that
A141: t = a.i and
A142: the_sort_of t = (the_arity_of o1).i &( the_sort_of t = rs1 &
the_sort_of Ck9 = rs1 implies t = Ck9) and
the_sort_of t <> rs1 or the_sort_of Ck9 <> rs1 implies t = root-tree
[cX.(the_sort_of t), the_sort_of t] by A128,A135,A133,A137,A139;
reconsider dt = dom t as finite Tree;
A143: dom doms a = dom a by TREES_3:37;
A144: now
let t9 be finite Tree;
assume t9 in rng w;
then consider j being Nat such that
A145: j in dom w and
A146: w.j = t9 by FINSEQ_2:10;
consider t99 being Term of S, X such that
A147: t99 = a.j and
the_sort_of t99 = (the_arity_of o1).j and
A148: the_sort_of t99 = rs1 & the_sort_of Ck9 = rs1 implies t99 = Ck9 and
A149: the_sort_of t99 <> rs1 or the_sort_of Ck9 <> rs1 implies t99
= root-tree [cX.(the_sort_of t99), the_sort_of t99] by A128,A143,A145;
A150: w.j = dom t99 by A143,A145,A147,FUNCT_6:22;
per cases;
suppose
the_sort_of t99 = rs1 & the_sort_of Ck9 = rs1;
hence height t9 <= height dt by A143,A133,A136,A138,A142,A145,A146
,A147,A148,FUNCT_6:22,MSUALG_1:def 1;
end;
suppose
the_sort_of t99 <> rs1 or the_sort_of Ck9 <> rs1;
hence height t9 <= height dt by A146,A149,A150,TREES_1:42,TREES_4:3;
end;
end;
(doms a).i = dom t by A135,A133,A137,A140,A139,A141,FUNCT_6:22;
then
A151: dom t in rng w by A143,A135,A133,A137,A140,A139,FUNCT_1:def 3;
the_sort_of Ck = (the ResultSort of S).(ck`1) by A122,MSUALG_1:def 2
.= TG.ck by Def3
.= (vertex-seq c).(kk+1) by A67,A99,A106,A120,CARD_1:27,MSSCYC_1:11
.= SG.ck1 by A67,A99,A102,A103,CARD_1:27,MSSCYC_1:11
.= ck1`2 by Def2
.= rs1 by A126;
hence thesis by A121,A123,A124,A134,A133,A136,A138,A142,A151,A144,
MSUALG_1:def 1,TREES_3:79;
end;
end;
set cn = c.len c;
n in dom c by A1,A67,CARD_1:27,FINSEQ_5:6;
then
A152: cn in InducedEdges S by A67,A71,DTCONSTR:2;
A153: P[ 0 ];
for k holds P[k] from NAT_1:sch 2(A153, A100);
then consider Cn being Term of S, X, o being OperSymbol of S such that
Cn = C.n and
A154: o = (c.n)`1 and
A155: the_sort_of Cn = the_result_sort_of o and
A156: height dom Cn = n by A1;
G is non void by A72;
then (vertex-seq c).(len c +1) = (the Target of G).(c.len c) by A1,A67,
CARD_1:27,MSSCYC_1:14
.= (the ResultSort of S).cn`1 by A152,Def3
.= the_result_sort_of o by A67,A154,MSUALG_1:def 2;
then reconsider Cn as Element of (the Sorts of FreeMSA X).v by A2,A68,A155,
MSATERM:def 5;
take Cn;
thus thesis by A156,MSAFREE2:def 14;
end;
theorem
for S being void non empty ManySortedSign holds S is monotonic iff
InducedGraph S is well-founded
proof
let S be void non empty ManySortedSign;
set G = InducedGraph S, OS = the carrier' of S, CA = the carrier of S, AR =
the Arity of S;
hereby
assume S is monotonic;
assume not G is well-founded;
then consider v being Element of the carrier of G such that
A1: for n being Nat ex c being directed Chain of G st c is
non empty & (vertex-seq c).(len c +1) = v & len c > n by MSSCYC_1:def 4;
consider e being directed Chain of G such that
A2: e is non empty and
(vertex-seq e).(len e +1) = v and
len e>0 by A1;
e is FinSequence of the carrier' of G by MSSCYC_1:def 1;
then
A3: rng e c= the carrier' of G by FINSEQ_1:def 4;
1 in dom e by A2,FINSEQ_5:6;
then e.1 in rng e by FUNCT_1:def 3;
then
ex op, v being set st e.1 = [op, v] & op in OS & v in CA & ex n being
Nat, args being Element of CA* st AR.op=args & n in dom args & args.n = v by A3
,Def1;
hence contradiction;
end;
assume G is well-founded;
let A be finitely-generated non-empty MSAlgebra over S;
thus the Sorts of A is finite-yielding by MSAFREE2:def 10;
end;
theorem
for S being non void non empty ManySortedSign st S is monotonic
holds InducedGraph S is well-founded
proof
let S be non void non empty ManySortedSign;
set G = InducedGraph S;
assume S is monotonic;
then reconsider S as monotonic non void non empty ManySortedSign;
set A = the finite-yielding non-empty MSAlgebra over S;
assume G is non well-founded;
then consider v being Element of the carrier of G such that
A1: for n being Nat ex c being directed Chain of G st c is
non empty & (vertex-seq c).(len c +1)=v & len c>n by MSSCYC_1:def 4;
reconsider v as SortSymbol of S;
consider s being finite non empty Subset of NAT such that
A2: s = the set of all
depth t where t is Element of (the Sorts of FreeEnv A).v and
depth(v,A) = max s by CIRCUIT1:def 6;
max s is Nat by TARSKI:1;
then consider c being directed Chain of G such that
c is non empty and
A3: (vertex-seq c).(len c +1) = v and
A4: len c>max s by A1;
1<=len c by A4,NAT_1:14;
then consider
t being Element of (the Sorts of FreeMSA the Sorts of A).v such
that
A5: depth t = len c by A3,Th2;
reconsider t9 = t as Element of (the Sorts of FreeEnv A).v;
(ex t99 being Element of (the Sorts of FreeMSA the Sorts of A ).v st t9
= t99 & depth t9 = depth t99 )& depth t9 in s by A2,CIRCUIT1:def 5;
hence contradiction by A4,A5,XXREAL_2:def 8;
end;
theorem Th5:
for S being non void non empty ManySortedSign, X being non-empty
finite-yielding ManySortedSet of the carrier of S st S is finitely_operated for
n being Nat, v being SortSymbol of S holds {t where t is Element of (the Sorts
of FreeMSA X).v: depth t <= n} is finite
proof
let S be non void non empty ManySortedSign, X be non-empty finite-yielding
ManySortedSet of the carrier of S such that
A1: S is finitely_operated;
set SF = the Sorts of FreeMSA X;
defpred P[Nat] means for v being SortSymbol of S holds {t where t is Element
of SF.v: depth t <= $1} is finite;
A2: FreeMSA X = MSAlgebra (#FreeSort(X), FreeOper(X)#) by MSAFREE:def 14;
A3: for k be Nat st P[k] holds P[k+1]
proof
deffunc F(set) = $1;
let n be Nat;
assume
A4: for v being SortSymbol of S holds {t where t is Element of SF.v:
depth t <= n} is finite;
let v be SortSymbol of S;
defpred QZ[Element of SF.v] means depth $1 = n+1;
defpred P[Element of SF.v] means depth $1 <= n+1;
defpred Q[Element of SF.v] means depth $1 <= n or depth $1 = n+1;
set dn1 = {F(t) where t is Element of SF.v: P[t]};
set dn11 = {F(t) where t is Element of SF.v: Q[t]};
set den1 = {t where t is Element of SF.v: QZ[t]};
set ov = {o where o is OperSymbol of S: the_result_sort_of o = v};
A5: SF.v = FreeSort(X,v) by A2,MSAFREE:def 11;
ov is finite by A1,MSSCYC_1:def 5;
then consider ovs being FinSequence such that
A6: rng ovs = ov by FINSEQ_1:52;
deffunc F(set) = {t where t is Element of SF.v: depth t = n+1 & t.{} = [
ovs.$1,the carrier of S]};
consider dvs being FinSequence such that
A7: len dvs = len ovs & for k being Nat st k in dom dvs holds dvs.k =
F(k) from FINSEQ_1:sch 2;
A8: dom ovs = Seg len ovs & dom dvs = Seg len dvs by FINSEQ_1:def 3;
A9: FreeSort(X,v) c= S-Terms X by MSATERM:12;
A10: den1 c= Union dvs
proof
let x be object;
assume x in den1;
then consider t being Element of SF.v such that
A11: x = t and
A12: depth t = n+1;
t in FreeSort(X,v) by A5;
then reconsider t9 = t as Term of S, X by A9;
now
A13: ex dt being finite DecoratedTree, tt being finite Tree st dt = t &
tt = dom dt & depth t = height tt by MSAFREE2:def 14;
assume t9 is root;
hence contradiction by A12,A13,TREES_1:42,TREES_9:def 1;
end;
then consider o being OperSymbol of S such that
A14: t9.{} = [o,the carrier of S] by MSSCYC_1:20;
the_result_sort_of o = the_sort_of t9 by A14,MSATERM:17
.= v by A5,MSATERM:def 5;
then o in rng ovs by A6;
then consider k being object such that
A15: k in dom ovs and
A16: o = ovs.k by FUNCT_1:def 3;
dvs.k = {t1 where t1 is Element of SF.v: depth t1 = n+1 & t1.{} = [
ovs.k,the carrier of S]} by A7,A8,A15;
then
A17: t in dvs.k by A12,A14,A16;
dvs.k in rng dvs by A7,A8,A15,FUNCT_1:def 3;
then t in union rng dvs by A17,TARSKI:def 4;
hence thesis by A11,CARD_3:def 4;
end;
for k being object st k in dom dvs holds dvs.k is finite
proof
let k be object;
set dvsk = {t where t is Element of SF.v: depth t = n+1 & t.{} = [ovs.k,
the carrier of S]};
assume
A18: k in dom dvs;
then ovs.k in rng ovs by A7,A8,FUNCT_1:def 3;
then consider o being OperSymbol of S such that
A19: o = ovs.k and
the_result_sort_of o = v by A6;
set davsk = {[o,the carrier of S]-tree a where a is Element of (S-Terms
X)* : a is ArgumentSeq of Sym(o,X) & ex t being Element of SF.v st depth t = n+
1 & t = [o,the carrier of S]-tree a};
A20: dvsk c= davsk
proof
let x be object;
assume x in dvsk;
then consider t being Element of SF.v such that
A21: x = t and
A22: depth t = n+1 and
A23: t.{} = [o,the carrier of S] by A19;
t in FreeSort(X,v) by A5;
then reconsider t9 = t as Term of S, X by A9;
consider a being ArgumentSeq of Sym(o,X) such that
A24: t9 = [o,the carrier of S]-tree a by A23,MSATERM:10;
reconsider a9 = a as Element of (S-Terms X)* by FINSEQ_1:def 11;
[o,the carrier of S]-tree a9 in davsk by A22,A24;
hence thesis by A21,A24;
end;
deffunc F(Nat)= {t where t is Element of SF.((the_arity_of o)/.$1):
depth t <=n};
set avsk = {a where a is Element of (S-Terms X)* : a is ArgumentSeq of
Sym(o,X) & ex t being Element of SF.v st depth t = n+1 & t = [o,the carrier of
S]-tree a};
A25: avsk,davsk are_equipotent
proof
set Z = {[a,[o,the carrier of S]-tree a] where a is Element of (S
-Terms X)* : a is ArgumentSeq of Sym(o,X) & ex t being Element of SF.v st depth
t = n+1 & t = [o,the carrier of S]-tree a};
take Z;
hereby
let x be object;
assume x in avsk;
then consider a being Element of (S-Terms X)* such that
A26: x = a and
A27: a is ArgumentSeq of Sym(o,X) & ex t being Element of SF.v
st depth t = n+1 & t = [o,the carrier of S]-tree a;
reconsider y9 = [o,the carrier of S]-tree a as object;
take y9;
thus y9 in davsk by A27;
thus [x,y9] in Z by A26,A27;
end;
hereby
let y be object;
assume y in davsk;
then consider a being Element of (S-Terms X)* such that
A28: y = [o,the carrier of S]-tree a and
A29: a is ArgumentSeq of Sym(o,X) & ex t being Element of SF.v
st depth t = n+1 & t = [o,the carrier of S]-tree a;
reconsider a9 = a as object;
take a9;
thus a9 in avsk by A29;
thus [a9,y] in Z by A28,A29;
end;
let x,y,z,u be object;
assume [x,y] in Z;
then consider xa being Element of (S-Terms X)* such that
A30: [x,y] = [xa,[o,the carrier of S]-tree xa] and
A31: xa is ArgumentSeq of Sym(o,X) and
ex t being Element of SF.v st depth t = n+1 & t = [o,the carrier
of S]-tree xa;
A32: x = xa by A30,XTUPLE_0:1;
assume [z,u] in Z;
then consider za being Element of (S-Terms X)* such that
A33: [z,u] = [za,[o,the carrier of S]-tree za] and
A34: za is ArgumentSeq of Sym(o,X) and
ex t being Element of SF.v st depth t = n+1 & t = [o,the carrier
of S]-tree za;
A35: z = za by A33,XTUPLE_0:1;
hence x = z implies y = u by A30,A33,A32,XTUPLE_0:1;
A36: u = [o,the carrier of S]-tree za by A33,XTUPLE_0:1;
A37: y = [o,the carrier of S]-tree xa by A30,XTUPLE_0:1;
assume y = u;
hence thesis by A31,A34,A32,A37,A35,A36,TREES_4:15;
end;
consider nS being FinSequence such that
A38: len nS = len the_arity_of o & for k being Nat st k in dom nS
holds nS.k = F(k) from FINSEQ_1:sch 2;
A39: dom nS = Seg len nS by FINSEQ_1:def 3;
A40: dom nS = Seg len the_arity_of o by A38,FINSEQ_1:def 3;
A41: avsk c= product nS
proof
let x be object;
assume x in avsk;
then consider a being Element of (S-Terms X)* such that
A42: x = a and
A43: a is ArgumentSeq of Sym(o,X) and
A44: ex t being Element of SF.v st depth t = n+1 & t = [o,the
carrier of S]-tree a;
reconsider a as ArgumentSeq of Sym(o,X) by A43;
A45: len a = len the_arity_of o & dom a = Seg len a by FINSEQ_1:def 3
,MSATERM:22;
now
let x be object;
assume
A46: x in dom a;
then reconsider k = x as Element of NAT;
reconsider ak = a.k as Term of S, X by A46,MSATERM:22;
A47: the_sort_of ak = (the_arity_of o)/.k by A46,MSATERM:23;
SF.(the_sort_of ak) = FreeSort(X,the_sort_of ak) by A2,MSAFREE:def 11
;
then reconsider ak as Element of SF.((the_arity_of o)/.k) by A47,
MSATERM:def 5;
depth ak < n+1 by A44,A46,MSSCYC_1:27;
then
A48: depth ak <= n by NAT_1:13;
set nSk = {tk where tk is Element of SF.((the_arity_of o)/.k): depth
tk <=n};
nSk = nS.x by A38,A40,A45,A46;
hence a.x in nS.x by A48;
end;
hence thesis by A38,A39,A42,A45,CARD_3:def 5;
end;
now
let x be object;
assume
A49: x in dom nS;
then reconsider k = x as Nat;
set nSk = {t where t is Element of SF.((the_arity_of o)/.k): depth t
<=n};
nS.k = nSk by A38,A49;
hence nS.x is finite by A4;
end;
then nS is finite-yielding by FINSET_1:def 4;
then product nS is finite;
then davsk is finite by A25,A41,CARD_1:38;
hence thesis by A7,A18,A20;
end;
then
A50: Union dvs is finite by CARD_2:88;
defpred Z[Element of SF.v] means depth $1 <= n;
set dln = {t where t is Element of SF.v: Z[t]};
A51: {t where t is Element of SF.v: Z[t] or QZ[t]} = dln \/ den1 from
TOPREAL1:sch 1;
A52: for t being Element of SF.v holds P[t] iff Q[t] by NAT_1:8,12;
A53: dn1 = dn11 from FRAENKEL:sch 3(A52);
dln is finite by A4;
hence thesis by A53,A51,A50,A10;
end;
A54: P[ 0 ]
proof
let v be SortSymbol of S;
set dle0 = {t where t is Element of SF.v: depth t <= 0};
set d0 = {t where t is Element of SF.v: depth t = 0};
A55: dle0 c= d0
proof
let x be object;
assume x in dle0;
then consider t being Element of SF.v such that
A56: x = t and
A57: depth t <= 0;
depth t = 0 by A57;
hence thesis by A56;
end;
Constants(FreeMSA X, v) is finite & d0 = FreeGen(v, X) \/ Constants(
FreeMSA X, v) by A1,MSSCYC_1:25,26;
hence thesis by A55;
end;
thus for n being Nat holds P[n] from NAT_1:sch 2(A54, A3);
end;
theorem
for S being non void non empty ManySortedSign st S is
finitely_operated & InducedGraph S is well-founded holds S is monotonic
proof
let S be non void non empty ManySortedSign;
set G = InducedGraph S;
assume that
A1: S is finitely_operated and
A2: G is well-founded;
given A being finitely-generated non-empty MSAlgebra over S such that
A3: A is non finite-yielding;
set GS = the non-empty finite-yielding GeneratorSet of A;
reconsider gs = GS as non-empty finite-yielding ManySortedSet of the carrier
of S;
FreeMSA gs is non finite-yielding by A3,MSSCYC_1:23;
then the Sorts of FreeMSA gs is non finite-yielding;
then consider v being object such that
A4: v in the carrier of S and
A5: (the Sorts of FreeMSA gs).v is non finite by FINSET_1:def 5;
reconsider v as SortSymbol of S by A4;
consider n being Nat such that
A6: for c being directed Chain of G st c is non empty & (vertex-seq c).(
len c +1) = v holds len c <= n by A2,MSSCYC_1:def 4;
set V = (the Sorts of FreeMSA gs).v;
set Vn = {t where t is Element of V : depth t<=n};
Vn is finite by A1,Th5;
then not V c= Vn by A5;
then consider t being object such that
A7: t in V and
A8: not t in Vn;
reconsider t as Element of V by A7;
A9: not depth t<=n by A8;
then 1 <=depth t by NAT_1:14;
then ex d being directed Chain of InducedGraph S st len d = depth t & (
vertex-seq d).(len d +1) = v by Th2;
hence contradiction by A6,A9,CARD_1:27;
end;