Copyright (c) 1996 Association of Mizar Users
environ vocabulary MSUALG_1, FUNCT_1, RELAT_1, MCART_1, GRAPH_1, AMI_1, ZF_REFLE, PBOOLE, MSAFREE, MSAFREE2, QUANTAL1, ORDERS_1, FINSEQ_1, GRAPH_2, MSATERM, FINSET_1, TREES_2, TREES_1, BOOLE, TREES_4, RFINSEQ, ARYTM_1, TREES_9, FREEALG, QC_LANG1, PARTFUN1, TREES_3, FUNCT_6, MSSCYC_1, PRE_CIRC, SQUARE_1, UNIALG_2, TARSKI, FINSEQ_4, PROB_1, MSSCYC_2, CARD_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, MCART_1, STRUCT_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, TOPREAL1, RFINSEQ, FINSET_1, TREES_1, TREES_2, TREES_3, TREES_4, PROB_1, CARD_3, GRAPH_1, GRAPH_2, PBOOLE, MSUALG_1, MSUALG_2, MSAFREE, MSAFREE2, PRE_CIRC, CIRCUIT1, TREES_9, MSATERM, MSSCYC_1, FINSEQ_1, FINSEQ_4; constructors MCART_1, RFINSEQ, GRAPH_2, WELLORD2, CIRCUIT1, TREES_9, MSATERM, MSSCYC_1, NAT_1, REAL_1, TOPREAL1, FINSOP_1, FINSEQ_4; clusters STRUCT_0, RELSET_1, FINSEQ_5, GRAPH_1, TREES_3, DTCONSTR, TREES_9, MSUALG_1, MSAFREE, PRE_CIRC, MSAFREE2, MSSCYC_1, GROUP_2, XREAL_0, FINSEQ_1, MSATERM, NAT_1, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions TARSKI, MSAFREE2; theorems TARSKI, AXIOMS, REAL_1, NAT_1, MCART_1, ZFMISC_1, GRAPH_1, MSSCYC_1, FUNCT_6, CARD_1, CARD_3, CARD_4, RLVECT_1, FUNCT_1, FUNCT_2, FINSET_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5, RFINSEQ, TOPREAL1, TREES_1, TREES_2, TREES_3, TREES_4, DTCONSTR, PBOOLE, MSUALG_1, MSAFREE, MSAFREE2, PRE_CIRC, PROB_1, CIRCUIT1, TREES_9, MSATERM, XBOOLE_0, XBOOLE_1, ORDINAL2; 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[set] means ex op, v being set st $1 = [op, v] & op in the OperSymbols 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 set holds x in it iff ex op, v being set st x = [op, v] & op in the OperSymbols 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 OperSymbols of S, the carrier of S:]; consider X being set such that A1: for x being set holds x in X iff x in XX & P[x] from Separation; take X; let x be set; thus x in X implies P[x] by A1; assume A2: P[x]; then consider op, v being set such that A3: x = [op, v] & op in the OperSymbols of S & v in the carrier of S and 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; x in XX by A3,ZFMISC_1:def 2; hence x in X by A1,A2; end; uniqueness proof for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq; hence thesis; end; end; theorem Th1: for S being ManySortedSign holds InducedEdges S c= [: the OperSymbols of S, the carrier of S :] proof let S be ManySortedSign; let x be set; assume x in InducedEdges S; then consider op, v being set such that A1: x = [op, v] & op in the OperSymbols of S & v in the carrier of S and 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; thus thesis by A1,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 set st e in InducedEdges S holds it.e = e`2; existence proof deffunc F(set)= $1 `2; A1: for x being set st x in IE holds F(x) in IV proof let x be set; assume A2: x in IE; IE c= [: the OperSymbols 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 set st x in InducedEdges S holds f.x = F(x) from Lambda1 (A1); hence thesis; end; uniqueness proof let F1, F2 be Function of IE, IV such that A3: for e being set st e in IE holds F1.e = e`2 and A4: for e being set st e in IE holds F2.e = e`2; now assume IV is empty; then [:the OperSymbols of S, IV:] is empty & IE c= [:the OperSymbols of S, IV:] by Th1,ZFMISC_1:113; hence IE is empty by XBOOLE_1:3; end; then A5: dom F1 = IE & dom F2 = IE by FUNCT_2:def 1; now let x be set; assume x in IE; then F1.x = x`2 & F2.x = x`2 by A3,A4; hence F1.x = F2.x; end; hence F1 = F2 by A5,FUNCT_1:9; end; set OS = the OperSymbols of S, RS = the ResultSort of S; func InducedTarget S -> Function of InducedEdges S, the carrier of S means :Def3: for e being set st e in InducedEdges S holds it.e = (the ResultSort of S).e`1; existence proof deffunc F(set) = RS.($1)`1; A6: for x being set st x in IE holds F(x) in IV proof let x be set; assume A7: x in IE; IE c= [: OS, IV :] by Th1; then x`1 in OS & x`2 in IV by A7,MCART_1:10; hence thesis by FUNCT_2:7; end; ex f being Function of InducedEdges S, the carrier of S st for x be set st x in InducedEdges S holds f.x = F(x) from Lambda1 (A6); hence thesis; end; uniqueness proof let F1, F2 be Function of IE, IV such that A8: for e being set st e in IE holds F1.e = RS.e`1 and A9: for e being set st e in IE holds F2.e = RS.e`1; now assume IV is empty; then [:the OperSymbols of S, IV:] is empty & IE c= [:the OperSymbols of S, IV:] by Th1,ZFMISC_1:113; hence IE is empty by XBOOLE_1:3; end; then A10: dom F1 = IE & dom F2 = IE by FUNCT_2:def 1; now let x be set; assume x in IE; then F1.x = RS.x`1 & F2.x = RS.x`1 by A8,A9; hence F1.x = F2.x; end; hence F1 = F2 by A10,FUNCT_1:9; end; end; definition let S be non empty ManySortedSign; func InducedGraph S -> Graph equals :Def4: MultiGraphStruct (# the carrier of S, InducedEdges S, InducedSource S, InducedTarget S #); coherence by GRAPH_1:def 1; 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; A2: G = MultiGraphStruct (# the carrier of S, InducedEdges S, InducedSource S, InducedTarget S #) by Def4; A3: FreeSort(X,v) c= S-Terms X by MSATERM:12; FreeMSA X = MSAlgebra(#FreeSort(X),FreeOper(X)#)by MSAFREE:def 16; then A4: (the Sorts of FreeMSA X).v = FreeSort(X,v) by MSAFREE:def 13; 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 given t being Element of (the Sorts of FreeMSA X).v such that A5: depth t = n; t in FreeSort(X,v) by A4; then reconsider t' = t as Term of S, X by A3; consider dt being finite DecoratedTree, tr being finite Tree such that A6: dt = t & tr = dom dt & depth t = height tr by MSAFREE2:def 14; consider p being FinSequence of NAT such that A7: p in tr & len p = height tr by TREES_1:def 15; set D = (the Edges of G)*; 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 Edges of G; A8: for k being Nat st 1 <= k & k < n for x being Element of D ex y being Element of D st P[k,x,y] proof let k be Nat; assume A9: 1 <= k & k < n; then A10: k<=k+1 & k+1<=n by NAT_1:38; let x be Element of D; reconsider pk = p|k, pk1 = p|(k+1) as Node of t by A6,A7,MSSCYC_1:19; reconsider t1 = t'|pk, t2 = t'|pk1 as Term of S, X by MSATERM:29; set pk' = p/^k; A11: len pk' = n - k by A5,A6,A7,A9,RFINSEQ:def 2; A12: 1<=n-k by A10,REAL_1:84; len pk' <> 0 by A10,A11,REAL_1:84; then A13: pk' is non empty by FINSEQ_1:25; p = pk^pk' by RFINSEQ:21; then A14: pk' in tr|pk by A6,A7,TREES_1:def 9; then A15: pk' in dom t1 by A6,TREES_2:def 11; now assume t1 is root; then A16: dom t1 = elementary_tree 0 by TREES_9:def 1 ; len pk'<=height dom t1 by A15,TREES_1:def 15; hence contradiction by A11,A12,A16,AXIOMS:22,TREES_1:79; end; then consider o being OperSymbol of S such that A17: t1.{} =[o, the carrier of S] by MSSCYC_1:20; consider a being ArgumentSeq of Sym(o,X) such that A18: t1 = [o,the carrier of S]-tree a by A17,MSATERM:10; consider i being Nat, T being DecoratedTree, q being Node of T such that A19: i < len a & T = a.(i+1) & pk' = <*i*>^q by A13,A15,A18,TREES_4:11; set args = the_arity_of o; A20: dom a = dom args by MSATERM:22; 1<=i+1 & i+1<=len a by A19,NAT_1:29,38; then A21: i+1 in dom args by A20,FINSEQ_3:27; then reconsider rs1 = args.(i+1) as SortSymbol of S by DTCONSTR:2; set e1 = [o,rs1]; A22: (the Arity of S).o = the_arity_of o by MSUALG_1:def 6; then [o,rs1] in InducedEdges S by A21,Def1; then reconsider E' = the Edges of G as non empty set by A2; reconsider x' = x as FinSequence of E' by FINSEQ_1:def 11; reconsider e1' = e1 as Element of E' by A2,A21,A22,Def1; reconsider y = <*e1'*>^x' 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 A17; A23: 1 in dom pk' by A13,FINSEQ_5:6; A24: pk'|1 = <*pk'/.1*> by A13,FINSEQ_5:23 .= <*pk'.1*> by A23,FINSEQ_4:def 4; reconsider pk' as Node of t1 by A6,A14,TREES_2:def 11; reconsider p1 = pk'|(0+1) as Node of t1 by MSSCYC_1:19; reconsider t2' = t1|p1 as Term of S, X; pk'|1 = <*i*> by A19,A24,FINSEQ_1:58; then A25: t2' = a.(i+1) by A18,A19,TREES_4:def 4; A26: len pk1 = k+1 by A5,A6,A7,A10,TOPREAL1:3; A27: 1<=k+1 by NAT_1:29; then A28: k+1 in dom pk1 by A26,FINSEQ_3:27; A29: k+1 in dom p by A5,A6,A7,A10,A27,FINSEQ_3:27; A30: Seg k c= Seg (k+1) by A10,FINSEQ_1:7; A31: p|(k+1)|k = p|(k+1)|Seg k by TOPREAL1:def 1 .= p|Seg (k+1)|Seg k by TOPREAL1:def 1 .= p|Seg k by A30,FUNCT_1:82 .= pk by TOPREAL1:def 1; p1 = <*p.(k+1)*> by A5,A6,A7,A9,A23,A24,RFINSEQ:def 2 .= <*p/.(k+1)*> by A29,FINSEQ_4:def 4 .= <*(p|(k+1))/.(k+1)*> by A28,TOPREAL1:1 .= <*pk1.(k+1)*> by A28,FINSEQ_4:def 4; then pk1 = pk^p1 by A26,A31,RFINSEQ:20; then t2' = t2 by TREES_9:3; hence rs1 = the_sort_of t2 by A20,A21,A25,MSATERM:23; thus [o,rs1] in the Edges of G by A2,A21,A22,Def1; end; now assume t is root; then dom t = elementary_tree 0 by TREES_9:def 1; hence contradiction by A1,A5,A6,TREES_1:79; end; then consider o being OperSymbol of S such that A32: t'.{} =[o, the carrier of S] by MSSCYC_1:20; consider a being ArgumentSeq of Sym(o,X) such that A33: t = [o,the carrier of S]-tree a by A32,MSATERM:10; A34: now assume p = {}; then len p = 0 by FINSEQ_1:25; hence contradiction by A1,A5,A6,A7; end; then consider i being Nat, T being DecoratedTree, q being Node of T such that A35: i < len a & T = a.(i+1) & p = <*i*>^q by A6,A7,A33,TREES_4:11; set args = the_arity_of o; A36: dom a = dom args by MSATERM:22; 1<=i+1 & i+1<=len a by A35,NAT_1:29,38; then A37: i+1 in dom args by A36,FINSEQ_3:27; then reconsider rs1 = args.(i+1) as SortSymbol of S by DTCONSTR:2; set e1 = [o,rs1]; A38: (the Arity of S).o = the_arity_of o by MSUALG_1:def 6; then A39: [o,rs1] in InducedEdges S by A37,Def1; then reconsider E' = the Edges of G as non empty set by A2; reconsider e1' = e1 as Element of E' by A2,A37,A38,Def1; reconsider C1' = <*e1'*> as Element of D by FINSEQ_1:def 11; consider C being FinSequence of D such that A40: len C = n & (C.1 = C1' or n = 0) & for k st 1 <= k & k < n holds P[k,C.k,C.(k+1)] from FinRecExD(A8); 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; A41:Z[0]; 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; assume A44: 1<=k+1 & k+1<=n; A45: k<=k+1 by NAT_1:29; A46: k<n by A44,NAT_1:38; per cases; suppose A47: k=0; reconsider C1 = <*e1*> as directed Chain of G by A2,A39,MSSCYC_1:5; A48: vertex-seq C1 = <*(the Source of G).e1, (the Target of G).e1*> by A2,A39,MSSCYC_1:7; A49: (vertex-seq C1).(len C1 +1) = (vertex-seq C1).(1+1) by FINSEQ_1:56 .= (the Target of G).e1 by A48,FINSEQ_1:61 .= (the ResultSort of S).e1`1 by A2,A39,Def3 .= (the ResultSort of S).o by MCART_1:7 .= the_result_sort_of o by MSUALG_1:def 7 .= the_sort_of t' by A32,MSATERM:17 .= v by A4,MSATERM:def 5; reconsider p1 = p|(0+1) as Node of t by A6,A7,MSSCYC_1:19; reconsider t2 = t'|p1 as Term of S, X by MSATERM:29; A50: 1 in dom p by A34,FINSEQ_5:6; reconsider p'=p as PartFunc of NAT, NAT; p|1 = <*p'/.1*> by A34,FINSEQ_5:23 .= <*p.1*> by A50,FINSEQ_4:def 4 .= <*i*> by A35,FINSEQ_1:58; then A51: t2 = a.(i+1) by A33,A35,TREES_4:def 4; A52: (vertex-seq C1).1 = (the Source of G).e1 by A48,FINSEQ_1:61 .= e1`2 by A2,A39,Def2 .= rs1 by MCART_1:7 .= the_sort_of t2 by A36,A37,A51,MSATERM:23; take C1, t2; thus C1 = C.(k+1) by A1,A40,A47; thus len C1 = k+1 by A47,FINSEQ_1:56; thus t2 = t|(p|(k+1)) by A47; thus (vertex-seq C1).(len C1 +1) = v by A49; thus (vertex-seq C1).1 = the_sort_of t2 by A52; suppose A53: k<>0; then A54: 1<=k by RLVECT_1:99; consider Ck being directed Chain of G, t1' being Term of S, X such that A55: 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' by A43, A44,A45,A53,AXIOMS:22,RLVECT_1:99; consider t1, t2 being Term of S, X such that A56: t1 = t|(p|k) & t2 = t|(p|(k+1)) and A57: 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 Edges of G by A40,A46,A54; consider o being OperSymbol of S, rs1 being SortSymbol of S, Ck' being Element of D such that A58: Ck' = C.k & C.(k+1) = <*[o,rs1]*>^Ck' & [o,the carrier of S] = t1.{} & rs1 = the_sort_of t2 & [o,rs1] in the Edges of G by A57; set e1 = [o,rs1]; reconsider C1 = <*[o,rs1]*> as directed Chain of G by A58,MSSCYC_1:5; A59: Ck is non empty by A53,A55,FINSEQ_1:25; A60: G is non empty by A58,MSSCYC_1:def 3; A61: vertex-seq C1 = <*(the Source of G).e1, (the Target of G).e1*> by A58,MSSCYC_1:7; A62: (vertex-seq C1).(len C1 +1) = (vertex-seq C1).(1+1) by FINSEQ_1:56 .= (the Target of G).e1 by A61,FINSEQ_1:61 .= (the ResultSort of S).e1`1 by A2,A58,Def3 .= (the ResultSort of S).o by MCART_1:7 .= the_result_sort_of o by MSUALG_1:def 7 .= the_sort_of t1 by A58,MSATERM:17; then reconsider d = C1^Ck as directed Chain of G by A55,A56,A59,A60,MSSCYC_1: 15; A63: d is non empty by A55,A56,A59,A60,A62,MSSCYC_1:15; take d, t2; thus d = C.(k+1) by A55,A58; thus len d = len C1 + k by A55,FINSEQ_1:35 .= k+1 by FINSEQ_1:56; thus t2 = t|(p|(k+1)) by A56; thus (vertex-seq d).(len d +1) = v by A55,A59,A60,A63,MSSCYC_1:16; (vertex-seq C1).1 = (the Source of G).e1 by A61,FINSEQ_1:61 .= e1`2 by A2,A58,Def2 .= the_sort_of t2 by A58,MCART_1:7; hence (vertex-seq d).1 = the_sort_of t2 by A59,A60,A63,MSSCYC_1:16; end; for k holds Z[k] from Ind (A41, A42); then consider c being directed Chain of G, t1 being Term of S, X such that A64: 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 ; thus ex c being directed Chain of InducedGraph S st len c = n & (vertex-seq c).(len c +1) = v by A64; end; given c being directed Chain of InducedGraph S such that A65: len c = n & (vertex-seq c).(len c +1) = v; set cS = the carrier of S; set EG = the Edges of G; set D = S-Terms X; set SG = the Source of G; set TG = the Target of G; A66: c is FinSequence of the Edges of InducedGraph S by MSSCYC_1:def 1; A67: 1 in dom c by A1,A65,FINSEQ_3:27; then A68: c.1 in InducedEdges S by A2,A66,DTCONSTR:2; reconsider EG as non empty set by A66,A67,DTCONSTR:2; A69: G is non empty by A2,A68,MSSCYC_1:def 3; len c <> 0 by A1,A65; then A70: c is non empty by FINSEQ_1:25; deffunc F(set) = X.$1; A71: for e being set st e in cS holds F(e) <> {} by PBOOLE:def 16; consider cX being ManySortedSet of cS such that A72: for e being set st e in cS holds cX.e in F(e) from Kuratowski_Function (A71); 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])); A73: for k being Nat st 1 <= k & k < n for x being Element of D ex y being Element of D st P[k,x,y] proof let k be Nat; assume 1 <= k & k < n; then A74: k<=k+1 & k+1<=n by NAT_1:38; let x be Element of D; 1<=k+1 by NAT_1:29; then k+1 in dom c by A65,A74,FINSEQ_3:27; then reconsider ck1 = c.(k+1) as Element of EG by A66,DTCONSTR:2; consider o, rs1 being set such that A75: ck1 = [o,rs1] & o in the OperSymbols of S & 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 A2,Def1; reconsider o as OperSymbol of S by A75; reconsider rs1 as SortSymbol of S by A75; set DA = dom the_arity_of o; set ar = the_arity_of o; defpred P[set, set] 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]); A76: for e being set st e in DA ex u being set st u in D & P[e,u] proof let e be set; assume A77: e in DA; per cases; suppose A78: ar.e = rs1 & the_sort_of x = rs1; take x; thus thesis by A78; suppose A79: ar.e <> rs1 or the_sort_of x <> rs1; reconsider s = (the_arity_of o).e as SortSymbol of S by A77,DTCONSTR:2; reconsider x = cX.((the_arity_of o).e) as Element of X.s by A72; reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4; take t; thus thesis by A79; end; consider a being Function of DA,D such that A80: for e being set st e in DA holds P[e,a.e] from FuncEx1 (A76); DA = Seg len ar by FINSEQ_1:def 3; then reconsider a as FinSequence of D by FINSEQ_2:28; A81: dom a = DA by FUNCT_2:def 1; now let i be Nat; assume A82: 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 A80,A81,A82; suppose ar.i <> rs1 or the_sort_of x <> rs1; then A83: t = root-tree [cX.(ar.i),ar.i] by A80,A81,A82; reconsider s = (the_arity_of o).i as SortSymbol of S by A81,A82,DTCONSTR:2; cX.((the_arity_of o).i) is Element of X.s by A72; hence the_sort_of t = ar.i by A83,MSATERM:14; end; then reconsider a as ArgumentSeq of Sym(o,X) by A81,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 A75; thus y = [o,cS]-tree a; let i be Nat; assume A84: 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 A84,MSATERM:23; hence (the_sort_of t = rs1 & the_sort_of x = rs1 implies t = x) & (the_sort_of t <> rs1 or the_sort_of x <> rs1 implies t = root-tree [cX.(the_sort_of t), the_sort_of t]) by A80,A81,A84; end; consider o, rs1 being set such that A85: c.1 = [o, rs1] & o in the OperSymbols of S & rs1 in the carrier of S & 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 A68,Def1; reconsider o as OperSymbol of S by A85; reconsider rs1 as SortSymbol of S by A85; deffunc F(Nat) = root-tree [cX.((the_arity_of o).$1),(the_arity_of o).$1]; consider a being FinSequence such that A86: len a = len the_arity_of o & for k st k in Seg len the_arity_of o holds a.k = F(k) from SeqLambda; A87: dom a = Seg len a by FINSEQ_1:def 3; 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 A88: i in dom a; set s = (the_arity_of o).i; set x = cX.((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 A86,A87,A88,DTCONSTR:2; reconsider x as Element of X.s by A72; reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4; take t; thus t = a.i by A86,A87,A88; thus the_sort_of t = (the_arity_of o).i by MSATERM:14; end; then reconsider a as ArgumentSeq of Sym(o,X) by A86,MSATERM:24; set C1 = [o,the carrier of S]-tree a; reconsider C1 as Term of S, X by MSATERM:1; consider C being FinSequence of D such that A89: len C = n & (C.1 = C1 or n = 0) & for k st 1 <= k & k < n holds P[k,C.k,C.(k+1)] from FinRecExD(A73); 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; A90: P[0]; A91: for k be Nat st P[k] holds P[k+1] proof let k; assume A92: 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 A93: 1<=k+1 & k+1<=n; A94: k<=k+1 by NAT_1:29; then A95: k<=n by A93,AXIOMS:22; A96: k<n by A93,NAT_1:38; per cases; suppose A97: k = 0; take C1, o; thus C1 = C.(k+1) by A1,A89,A97; thus o = (c.(k+1))`1 by A85,A97,MCART_1:7; C1.{} = [o, cS] by TREES_4:def 4; hence the_sort_of C1 = the_result_sort_of o by MSATERM:17; A98: dom C1 = tree doms a by TREES_4:10; A99: dom doms a = dom a by TREES_3:39; consider i being Nat, args being Element of (the carrier of S)* such that A100: (the Arity of S).o = args & i in dom args & args.i = rs1 by A85; A101: args = the_arity_of o by A100,MSUALG_1:def 6; A102: dom args = Seg len args by FINSEQ_1:def 3; then reconsider t = a.i as Term of S, X by A86,A87,A100,A101,MSATERM:22; reconsider w = doms a as FinTree-yielding FinSequence; reconsider dt = dom t as finite Tree; (doms a).i = dom t by A86,A87,A100,A101,A102,FUNCT_6:31; then A103: dom t in rng w by A86,A87,A99,A100,A101,A102,FUNCT_1:def 5; A104: a.i = root-tree [cX.((the_arity_of o).i),(the_arity_of o).i] by A86, A100,A101,A102; then A105: dom t = elementary_tree 0 by TREES_4:3; now let t' be finite Tree; assume t' in rng w; then consider j being Nat such that A106: j in dom w & w.j = t' by FINSEQ_2:11; A107: a.j = root-tree [cX.((the_arity_of o).j),(the_arity_of o).j] by A86,A87, A99,A106; reconsider t'' = a.j as Term of S, X by A99,A106,MSATERM:22; A108: w.j = dom t'' by A99,A106,FUNCT_6:31; dom t'' = elementary_tree 0 by A107,TREES_4:3; hence height t' <= height dt by A104,A106,A108,TREES_4:3; end; hence height dom C1 = k+1 by A97,A98,A103,A105,TREES_1:79,TREES_3:82; suppose A109: k <> 0; then A110: 1<=k by RLVECT_1:99; consider Ck being Term of S, X, o being OperSymbol of S such that A111: Ck = C.k & o = (c.k)`1 & the_sort_of Ck = the_result_sort_of o & height dom Ck = k by A92,A93,A94,A109,AXIOMS:22,RLVECT_1:99; consider o1 being OperSymbol of S, rs1 being SortSymbol of S, Ck', Ck1 being Term of S, X, a being ArgumentSeq of Sym(o1,X) such that A112: Ck' = C.k & C.(k+1) = Ck1 & c.(k+1) = [o1, rs1] and A113: Ck1 = [o1,cS]-tree a and A114: (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 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])) by A89,A96,A110; A115: len a = len the_arity_of o1 by MSATERM:22; A116: dom Ck1 = tree doms a by A113,TREES_4:10; A117: dom doms a = dom a by TREES_3:39; A118: dom a = Seg len a by FINSEQ_1:def 3; set ck1 = c.(k+1); A119: k+1 in dom c by A65,A93,FINSEQ_3:27; then ck1 in EG by A66,DTCONSTR:2; then consider o', rs1' being set such that A120: ck1=[o', rs1'] & o' in the OperSymbols of S & rs1' in the carrier of S & 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 A2,Def1; k in dom c by A65,A95,A110,FINSEQ_3:27; then reconsider ck = c.k as Element of EG by A66,DTCONSTR:2; reconsider ck1 as Element of EG by A66,A119,DTCONSTR:2; A121: the_sort_of Ck :: the_result_sort_of o = (the ResultSort of S).(ck`1) by A111,MSUALG_1:def 7 .= TG.ck by A2,Def3 .= (vertex-seq c).(k+1) by A65,A69,A70,A95,A110,MSSCYC_1:11 .= SG.ck1 by A65,A69,A70,A93,MSSCYC_1:11 .= ck1`2 by A2,Def2 .= rs1 by A112,MCART_1:7; A122: o1 = o' & rs1 = rs1' by A112,A120,ZFMISC_1:33; then consider i being Nat, args being Element of (the carrier of S)* such that A123: (the Arity of S).o' = args & i in dom args & args.i = rs1 by A120; reconsider o' as OperSymbol of S by A120; A124: args = the_arity_of o' by A123,MSUALG_1:def 6; A125: dom args = Seg len args by FINSEQ_1:def 3; then consider t being Term of S, X such that A126: t = a.i & the_sort_of t = (the_arity_of o1).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]) by A114, A115,A118,A122,A123,A124; reconsider w = doms a as FinTree-yielding FinSequence; reconsider dt = dom t as finite Tree; (doms a).i = dom t by A115,A118,A122,A123,A124,A125,A126,FUNCT_6:31; then A127: dom t in rng w by A115,A117,A118,A122,A123,A124,A125,FUNCT_1:def 5; A128: now let t' be finite Tree; assume t' in rng w; then consider j being Nat such that A129: j in dom w & w.j = t' by FINSEQ_2:11; consider t'' being Term of S, X such that A130: t'' = a.j & the_sort_of t'' = (the_arity_of o1).j & (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'']) by A114, A117,A129; A131: w.j = dom t'' by A117,A129,A130,FUNCT_6:31; per cases; suppose the_sort_of t'' = rs1 & the_sort_of Ck' = rs1; hence height t' <= height dt by A117,A122,A123,A126,A129,A130,FUNCT_6:31, MSUALG_1:def 6; suppose the_sort_of t'' <> rs1 or the_sort_of Ck' <> rs1; then dom t'' = elementary_tree 0 by A130,TREES_4:3; hence height t' <= height dt by A129,A131,NAT_1:18,TREES_1:79; end; take Ck1, o1; thus Ck1 = C.(k+1) by A112; thus o1 = (c.(k+1))`1 by A112,MCART_1:7; Ck1.{} = [o1,cS] by A113,TREES_4:def 4; hence the_sort_of Ck1 = the_result_sort_of o1 by MSATERM:17; thus height dom Ck1 = k+1 by A111,A112,A116,A121,A122,A123,A126,A127,A128, MSUALG_1:def 6,TREES_3:82; end; for k holds P[k] from Ind (A90, A91); then consider Cn being Term of S, X, o being OperSymbol of S such that A132: Cn = C.n & o = (c.n)`1 & the_sort_of Cn = the_result_sort_of o & height dom Cn = n by A1; len c <> 0 by A1,A65; then A133: c is non empty by FINSEQ_1:25; A134: G is non empty by A2,A68,MSSCYC_1:def 3; set cn = c.len c; n in dom c by A65,A133,FINSEQ_5:6; then A135: cn in InducedEdges S by A2,A65,A66,DTCONSTR:2; (vertex-seq c).(len c +1) = (the Target of G).(c.len c) by A133,A134,MSSCYC_1:14 .= (the ResultSort of S).cn`1 by A2,A135,Def3 .= the_result_sort_of o by A65,A132,MSUALG_1:def 7; then reconsider Cn as Element of (the Sorts of FreeMSA X).v by A4,A65,A132, MSATERM:def 5; take Cn; thus thesis by A132,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, E = InducedEdges S, Sou = InducedSource S, T = InducedTarget S, OS = the OperSymbols of S, CA = the carrier of S, AR = the Arity of S; A1: G = MultiGraphStruct (#the carrier of S,E,Sou,T#) by Def4; hereby assume S is monotonic; assume not G is well-founded; then consider v being Element of the Vertices of G such that A2: for n 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 5; consider e being directed Chain of G such that A3: e is non empty & (vertex-seq e).(len e +1) = v & len e>0 by A2; A4: e is FinSequence of the Edges of G by MSSCYC_1:def 1; 1 in dom e by A3,FINSEQ_5:6; then e.1 in rng e & rng e c= the Edges of G by A4,FINSEQ_1:def 4,FUNCT_1:def 5 ; 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 A1,Def1; hence contradiction by MSUALG_1:def 5; end; assume G is well-founded; let A be finitely-generated (non-empty MSAlgebra over S); thus the Sorts of A is locally-finite 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 A1: S is monotonic; assume G is non well-founded; then consider v being Element of the Vertices of G such that A2: for n 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 5; reconsider S as monotonic non void (non empty ManySortedSign) by A1; G = MultiGraphStruct (# the carrier of S, InducedEdges S, InducedSource S, InducedTarget S #) by Def4; then reconsider v as SortSymbol of S; consider A being locally-finite non-empty MSAlgebra over S; consider s being finite non empty Subset of NAT such that A3: s = { depth t where t is Element of (the Sorts of FreeEnv A).v : not contradiction } & depth(v,A) = max s by CIRCUIT1:def 6; max s is Nat by ORDINAL2:def 21; then consider c being directed Chain of G such that A4: c is non empty & (vertex-seq c).(len c +1) = v & len c>max s by A2; 0<=max s by NAT_1:18; then 1<=len c by A4,RLVECT_1:99; then consider t being Element of (the Sorts of FreeMSA the Sorts of A).v such that A5: depth t = len c by A4,Th2; reconsider t' = t as Element of (the Sorts of FreeEnv A).v by MSAFREE2:def 8; consider t'' being Element of (the Sorts of FreeMSA the Sorts of A).v such that A6: t' = t'' & depth t' = depth t'' by CIRCUIT1:def 5; depth t' in s by A3; hence contradiction by A4,A5,A6,PRE_CIRC:def 1; end; theorem Th5: for S being non void non empty ManySortedSign, X being non-empty locally-finite 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 locally-finite ManySortedSet of the carrier of S such that A1: S is finitely_operated; set SF = the Sorts of FreeMSA X; A2: FreeMSA X = MSAlgebra (#FreeSort(X), FreeOper(X)#) by MSAFREE:def 16; defpred P[Nat] means for v being SortSymbol of S holds {t where t is Element of SF.v: depth t <= $1} is finite; A3: 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}; Constants(FreeMSA X, v) is finite by A1,MSSCYC_1:26; then A4: FreeGen(v, X) \/ Constants(FreeMSA X, v) is finite by FINSET_1:14; A5: d0 = FreeGen(v, X) \/ Constants(FreeMSA X, v) by MSSCYC_1:27; dle0 c= d0 proof let x be set; assume x in dle0; then consider t being Element of SF.v such that A6: x = t & depth t <= 0; depth t = 0 by A6,NAT_1:18; hence x in d0 by A6; end; hence dle0 is finite by A4,A5,FINSET_1:13; end; A7: for k be Nat st P[k] holds P[k+1] proof let n be Nat; assume A8: 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; A9: SF.v = FreeSort(X,v) by A2,MSAFREE:def 13; A10: FreeSort(X,v) c= S-Terms X by MSATERM:12; defpred Z[Element of SF.v] means depth $1 <= n; 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; deffunc F(set) = $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]}; A11: for t being Element of SF.v holds P[t] iff Q[t] by NAT_1:26,37; A12: dn1 = dn11 from Fraenkel6'(A11); set dln = {t where t is Element of SF.v: Z[t]}; set den1 = {t where t is Element of SF.v: QZ[t]}; A13: {t where t is Element of SF.v: Z[t] or QZ[t]} = dln \/ den1 from Fraenkel_Alt; set ov = {o where o is OperSymbol of S: the_result_sort_of o = v}; ov is finite by A1,MSSCYC_1:def 6; then consider ovs being FinSequence such that A14: rng ovs = ov by FINSEQ_1:73; 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 A15: len dvs = len ovs & for k being Nat st k in Seg len ovs holds dvs.k =F(k) from SeqLambda; A16: dom ovs = Seg len ovs & dom dvs = Seg len dvs by FINSEQ_1:def 3; for k being set st k in dom dvs holds dvs.k is finite proof let k be set; set dvsk = {t where t is Element of SF.v: depth t = n+1 & t.{} = [ovs.k,the carrier of S]}; assume A17: k in dom dvs; then A18: dvs.k = dvsk by A15,A16; ovs.k in rng ovs by A15,A16,A17,FUNCT_1:def 5; then consider o being OperSymbol of S such that A19: o = ovs.k & the_result_sort_of o = v by A14; 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 set; assume x in dvsk; then consider t being Element of SF.v such that A21: x = t & depth t = n+1 & t.{} = [o,the carrier of S] by A19; t in FreeSort(X,v) by A9; then reconsider t' = t as Term of S, X by A10; consider a being ArgumentSeq of Sym(o,X) such that A22: t' = [o,the carrier of S]-tree a by A21,MSATERM:10; reconsider a' = a as Element of (S-Terms X)* by FINSEQ_1:def 11; [o,the carrier of S]-tree a' in davsk by A21,A22; hence x in davsk by A21,A22; end; 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}; A23: 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 set; assume x in avsk; then consider a being Element of (S-Terms X)* such that A24: x = a & 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 y' = [o,the carrier of S]-tree a as set; take y'; thus y' in davsk by A24; thus [x,y'] in Z by A24; end; hereby let y be set; assume y in davsk; then consider a being Element of (S-Terms X)* such that A25: y = [o,the carrier of S]-tree a & 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 a' = a as set; take a'; thus a' in avsk by A25; thus [a',y] in Z by A25; end; let x,y,z,u be set; assume [x,y] in Z; then consider xa being Element of (S-Terms X)* such that A26: [x,y] = [xa,[o,the carrier of S]-tree xa] & xa 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 xa; assume [z,u] in Z; then consider za being Element of (S-Terms X)* such that A27: [z,u] = [za,[o,the carrier of S]-tree za] & za 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 za; A28: x = xa & y = [o,the carrier of S]-tree xa & z = za & u = [o,the carrier of S]-tree za by A26,A27,ZFMISC_1:33; hence x = z implies y = u; assume y = u; hence x = z by A26,A27,A28,TREES_4:15; end; deffunc F(Nat)= {t where t is Element of SF.((the_arity_of o)/.$1): depth t <=n}; consider nS being FinSequence such that A29: len nS = len the_arity_of o & for k being Nat st k in Seg len the_arity_of o holds nS.k = F(k) from SeqLambda; A30: dom nS = Seg len nS by FINSEQ_1:def 3; now let x be set; assume A31: 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 A29,A30,A31; hence nS.x is finite by A8; end; then A32: product nS is finite by MSSCYC_1:1; avsk c= product nS proof let x be set; assume x in avsk; then consider a being Element of (S-Terms X)* such that A33: x = a & 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 a as ArgumentSeq of Sym(o,X) by A33; consider t being Element of SF.v such that A34: depth t = n+1 & t = [o,the carrier of S]-tree a by A33; A35: len a = len the_arity_of o & dom a = dom the_arity_of o by MSATERM:22; A36: dom a = Seg len a by FINSEQ_1:def 3; now let x be set; assume A37: x in dom a; then reconsider k = x as Nat; reconsider ak = a.k as Term of S, X by A37,MSATERM:22; A38: ak = (a qua FinSequence of S-Terms X)/.k & the_sort_of ak = (the_arity_of o).k & the_sort_of ak = (the_arity_of o)/.k by A37,MSATERM:23; SF.(the_sort_of ak) = FreeSort(X,the_sort_of ak) by A2,MSAFREE:def 13; then reconsider ak as Element of SF.((the_arity_of o)/.k) by A38,MSATERM :def 5; set nSk = {tk where tk is Element of SF.((the_arity_of o)/.k): depth tk <=n}; A39: nSk = nS.x by A29,A35,A36,A37; depth ak < n+1 by A34,A37,MSSCYC_1:28; then depth ak <= n by NAT_1:38; hence a.x in nS.x by A39; end; hence x in product nS by A29,A30,A33,A35,A36,CARD_3:def 5; end; then avsk is finite by A32,FINSET_1:13; then davsk is finite by A23,CARD_1:68; hence dvs.k is finite by A18,A20,FINSET_1:13; end; then A40: Union dvs is finite by A16,CARD_4:63; den1 c= Union dvs proof let x be set; assume x in den1; then consider t being Element of SF.v such that A41: x = t & depth t = n+1; t in FreeSort(X,v) by A9; then reconsider t' = t as Term of S, X by A10; now assume A42: t' is root; consider dt being finite DecoratedTree, tt being finite Tree such that A43: dt = t & tt = dom dt & depth t = height tt by MSAFREE2:def 14; thus contradiction by A41,A42,A43,TREES_1:79,TREES_9:def 1; end; then consider o being OperSymbol of S such that A44: t'.{} = [o,the carrier of S] by MSSCYC_1:20; the_result_sort_of o = the_sort_of t' by A44,MSATERM:17 .= v by A9,MSATERM:def 5; then o in rng ovs by A14; then consider k being set such that A45: k in dom ovs & o = ovs.k by FUNCT_1:def 5; dvs.k = {t1 where t1 is Element of SF.v: depth t1 = n+1 & t1.{} = [ovs.k,the carrier of S]} by A15,A16,A45; then A46: t in dvs.k by A41,A44,A45; dvs.k in rng dvs by A15,A16,A45,FUNCT_1:def 5; then t in union rng dvs by A46,TARSKI:def 4; hence x in Union dvs by A41,PROB_1:def 3; end; then A47: den1 is finite by A40,FINSET_1:13; dln is finite by A8; hence dn1 is finite by A12,A13,A47,FINSET_1:14; end; thus for n being Nat holds P[n] from Ind(A3, A7); 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, E = InducedEdges S, Sou = InducedSource S, T = InducedTarget S; A1: G = MultiGraphStruct (#the carrier of S,E,Sou,T#) by Def4; assume A2: S is finitely_operated & G is well-founded; given A being finitely-generated (non-empty MSAlgebra over S) such that A3: A is non locally-finite; consider GS being non-empty locally-finite GeneratorSet of A; reconsider gs = GS as non-empty locally-finite ManySortedSet of the carrier of S; FreeMSA gs is non locally-finite by A3,MSSCYC_1:23; then the Sorts of FreeMSA gs is non locally-finite by MSAFREE2:def 11; then consider v being set such that A4: v in the carrier of S & (the Sorts of FreeMSA gs).v is non finite by PRE_CIRC:def 3; reconsider v as SortSymbol of S by A4; consider n such that A5: for c being directed Chain of G st c is non empty & (vertex-seq c).(len c +1) = v holds len c <= n by A1,A2,MSSCYC_1:def 5; set V = (the Sorts of FreeMSA gs).v; set Vn = {t where t is Element of V : depth t<=n}; A6: Vn is finite by A2,Th5; Vn c= V proof let x be set; assume x in Vn; then ex t being Element of V st x=t & depth t<=n; hence x in V; end; then not V c= Vn by A4,A6,XBOOLE_0:def 10; then consider t being set such that A7: t in V & not t in Vn by TARSKI:def 3; reconsider t as Element of V by A7; A8: not depth t<=n by A7; A9: 0<=n by NAT_1:18; then 1 <=depth t by A8,RLVECT_1:99; then consider d being directed Chain of InducedGraph S such that A10: len d = depth t & (vertex-seq d).(len d +1) = v by Th2; d is non empty by A8,A9,A10,FINSEQ_1:25; hence contradiction by A5,A8,A10; end;