:: MSSCYC_2 semantic presentation begin definition let S be ManySortedSign ; defpred S1[ set ] 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 ex 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: :: MSSCYC_2:def 1 for x being set 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 ex args being Element of the carrier of S * st ( the Arity of S . op = args & n in dom args & args . n = v ) ) ); existence ex b1 being set st for x being set holds ( x in b1 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 ex args being Element of the carrier of S * st ( the Arity of S . op = args & n in dom args & args . n = v ) ) ) proof set XX = [: the carrier' of S, the carrier of S:]; consider X being set such that A1: for x being set holds ( x in X iff ( x in [: the carrier' of S, the carrier of S:] & S1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X 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 ex args being Element of the carrier of S * st ( the Arity of S . op = args & n in dom args & args . n = v ) ) ) let x be set ; ::_thesis: ( x in X 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 ex args being Element of the carrier of S * st ( the Arity of S . op = args & n in dom args & args . n = v ) ) ) thus ( x in X implies S1[x] ) by A1; ::_thesis: ( 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 ex args being Element of the carrier of S * st ( the Arity of S . op = args & n in dom args & args . n = v ) ) implies x in X ) assume A2: S1[x] ; ::_thesis: x in X then x in [: the carrier' of S, the carrier of S:] by ZFMISC_1:def_2; hence x in X by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 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 ex args being Element of the carrier of S * st ( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) & ( for x being set holds ( x in b2 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 ex args being Element of the carrier of S * st ( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) holds b1 = b2 proof for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); hence for b1, b2 being set st ( for x being set holds ( x in b1 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 ex args being Element of the carrier of S * st ( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) & ( for x being set holds ( x in b2 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 ex args being Element of the carrier of S * st ( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ) holds b1 = b2 ; ::_thesis: verum end; end; :: deftheorem Def1 defines InducedEdges MSSCYC_2:def_1_:_ for S being ManySortedSign for b2 being set holds ( b2 = InducedEdges S iff for x being set holds ( x in b2 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 ex args being Element of the carrier of S * st ( the Arity of S . op = args & n in dom args & args . n = v ) ) ) ); theorem Th1: :: MSSCYC_2:1 for S being ManySortedSign holds InducedEdges S c= [: the carrier' of S, the carrier of S:] proof let S be ManySortedSign ; ::_thesis: InducedEdges S c= [: the carrier' of S, the carrier of S:] let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InducedEdges S or x in [: the carrier' of S, the carrier of S:] ) assume x in InducedEdges S ; ::_thesis: x in [: the carrier' of S, the carrier of 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 ex 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 x in [: the carrier' of S, the carrier of S:] by ZFMISC_1:def_2; ::_thesis: verum end; definition let S be ManySortedSign ; set IE = InducedEdges S; set IV = the carrier of S; func InducedSource S -> Function of (InducedEdges S), the carrier of S means :Def2: :: MSSCYC_2:def 2 for e being set st e in InducedEdges S holds it . e = e `2 ; existence ex b1 being Function of (InducedEdges S), the carrier of S st for e being set st e in InducedEdges S holds b1 . e = e `2 proof deffunc H1( set ) -> set = \$1 `2 ; A1: for x being set st x in InducedEdges S holds H1(x) in the carrier of S proof let x be set ; ::_thesis: ( x in InducedEdges S implies H1(x) in the carrier of S ) assume A2: x in InducedEdges S ; ::_thesis: H1(x) in the carrier of S InducedEdges S c= [: the carrier' of S, the carrier of S:] by Th1; hence H1(x) in the carrier of S by A2, MCART_1:10; ::_thesis: verum end; ex f being Function of (InducedEdges S), the carrier of S st for x being set st x in InducedEdges S holds f . x = H1(x) from FUNCT_2:sch_2(A1); hence ex b1 being Function of (InducedEdges S), the carrier of S st for e being set st e in InducedEdges S holds b1 . e = e `2 ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (InducedEdges S), the carrier of S st ( for e being set st e in InducedEdges S holds b1 . e = e `2 ) & ( for e being set st e in InducedEdges S holds b2 . e = e `2 ) holds b1 = b2 proof let F1, F2 be Function of (InducedEdges S), the carrier of S; ::_thesis: ( ( for e being set st e in InducedEdges S holds F1 . e = e `2 ) & ( for e being set st e in InducedEdges S holds F2 . e = e `2 ) implies F1 = F2 ) assume that A3: for e being set st e in InducedEdges S holds F1 . e = e `2 and A4: for e being set st e in InducedEdges S holds F2 . e = e `2 ; ::_thesis: F1 = F2 A5: now__::_thesis:_for_x_being_set_st_x_in_InducedEdges_S_holds_ F1_._x_=_F2_._x let x be set ; ::_thesis: ( x in InducedEdges S implies F1 . x = F2 . x ) assume A6: x in InducedEdges S ; ::_thesis: F1 . x = F2 . x then F1 . x = x `2 by A3; hence F1 . x = F2 . x by A4, A6; ::_thesis: verum end; now__::_thesis:_(_the_carrier_of_S_is_empty_implies_InducedEdges_S_is_empty_) assume the carrier of S is empty ; ::_thesis: InducedEdges S is empty then [: the carrier' of S, the carrier of S:] is empty by ZFMISC_1:90; hence InducedEdges S is empty by Th1, XBOOLE_1:3; ::_thesis: verum end; then ( dom F1 = InducedEdges S & dom F2 = InducedEdges S ) by FUNCT_2:def_1; hence F1 = F2 by A5, FUNCT_1:2; ::_thesis: verum end; set OS = the carrier' of S; set RS = the ResultSort of S; func InducedTarget S -> Function of (InducedEdges S), the carrier of S means :Def3: :: MSSCYC_2:def 3 for e being set st e in InducedEdges S holds it . e = the ResultSort of S . (e `1); existence ex b1 being Function of (InducedEdges S), the carrier of S st for e being set st e in InducedEdges S holds b1 . e = the ResultSort of S . (e `1) proof deffunc H1( set ) -> set = the ResultSort of S . (\$1 `1); A7: for x being set st x in InducedEdges S holds H1(x) in the carrier of S proof let x be set ; ::_thesis: ( x in InducedEdges S implies H1(x) in the carrier of S ) assume A8: x in InducedEdges S ; ::_thesis: H1(x) in the carrier of S InducedEdges S c= [: the carrier' of S, the carrier of S:] by Th1; then ( x `1 in the carrier' of S & x `2 in the carrier of S ) by A8, MCART_1:10; hence H1(x) in the carrier of S by FUNCT_2:5; ::_thesis: verum end; ex f being Function of (InducedEdges S), the carrier of S st for x being set st x in InducedEdges S holds f . x = H1(x) from FUNCT_2:sch_2(A7); hence ex b1 being Function of (InducedEdges S), the carrier of S st for e being set st e in InducedEdges S holds b1 . e = the ResultSort of S . (e `1) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of (InducedEdges S), the carrier of S st ( for e being set st e in InducedEdges S holds b1 . e = the ResultSort of S . (e `1) ) & ( for e being set st e in InducedEdges S holds b2 . e = the ResultSort of S . (e `1) ) holds b1 = b2 proof let F1, F2 be Function of (InducedEdges S), the carrier of S; ::_thesis: ( ( for e being set st e in InducedEdges S holds F1 . e = the ResultSort of S . (e `1) ) & ( for e being set st e in InducedEdges S holds F2 . e = the ResultSort of S . (e `1) ) implies F1 = F2 ) assume that A9: for e being set st e in InducedEdges S holds F1 . e = the ResultSort of S . (e `1) and A10: for e being set st e in InducedEdges S holds F2 . e = the ResultSort of S . (e `1) ; ::_thesis: F1 = F2 A11: now__::_thesis:_for_x_being_set_st_x_in_InducedEdges_S_holds_ F1_._x_=_F2_._x let x be set ; ::_thesis: ( x in InducedEdges S implies F1 . x = F2 . x ) assume A12: x in InducedEdges S ; ::_thesis: F1 . x = F2 . x then F1 . x = the ResultSort of S . (x `1) by A9; hence F1 . x = F2 . x by A10, A12; ::_thesis: verum end; now__::_thesis:_(_the_carrier_of_S_is_empty_implies_InducedEdges_S_is_empty_) assume the carrier of S is empty ; ::_thesis: InducedEdges S is empty then [: the carrier' of S, the carrier of S:] is empty by ZFMISC_1:90; hence InducedEdges S is empty by Th1, XBOOLE_1:3; ::_thesis: verum end; then ( dom F1 = InducedEdges S & dom F2 = InducedEdges S ) by FUNCT_2:def_1; hence F1 = F2 by A11, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines InducedSource MSSCYC_2:def_2_:_ for S being ManySortedSign for b2 being Function of (InducedEdges S), the carrier of S holds ( b2 = InducedSource S iff for e being set st e in InducedEdges S holds b2 . e = e `2 ); :: deftheorem Def3 defines InducedTarget MSSCYC_2:def_3_:_ for S being ManySortedSign for b2 being Function of (InducedEdges S), the carrier of S holds ( b2 = InducedTarget S iff for e being set st e in InducedEdges S holds b2 . e = the ResultSort of S . (e `1) ); definition let S be non empty ManySortedSign ; func InducedGraph S -> Graph equals :: MSSCYC_2:def 4 MultiGraphStruct(# the carrier of S,(InducedEdges S),(InducedSource S),(InducedTarget S) #); coherence MultiGraphStruct(# the carrier of S,(InducedEdges S),(InducedSource S),(InducedTarget S) #) is Graph ; end; :: deftheorem defines InducedGraph MSSCYC_2:def_4_:_ for S being non empty ManySortedSign holds InducedGraph S = MultiGraphStruct(# the carrier of S,(InducedEdges S),(InducedSource S),(InducedTarget S) #); theorem Th2: :: MSSCYC_2:2 for S being non empty non void ManySortedSign for X being V2() ManySortedSet of the carrier of S for v being SortSymbol of S for n being Nat 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 empty non void ManySortedSign ; ::_thesis: for X being V2() ManySortedSet of the carrier of S for v being SortSymbol of S for n being Nat 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 ) ) let X be V2() ManySortedSet of the carrier of S; ::_thesis: for v being SortSymbol of S for n being Nat 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 ) ) let v be SortSymbol of S; ::_thesis: for n being Nat 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 ) ) let n be Nat; ::_thesis: ( 1 <= n implies ( 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 ) ) ) assume A1: 1 <= n ; ::_thesis: ( 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 ) ) 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 ) ) ::_thesis: ( ex c being directed Chain of InducedGraph S st ( len c = n & (vertex-seq c) . ((len c) + 1) = v ) implies ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n ) proof reconsider n1 = n as Element of NAT by ORDINAL1:def_12; set D = the carrier' of (InducedGraph S) * ; given t being Element of the Sorts of (FreeMSA X) . v such that A4: depth t = n ; ::_thesis: ex c being directed Chain of InducedGraph S st ( len c = n & (vertex-seq c) . ((len c) + 1) = v ) 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 (the_arity_of o) 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 Element of 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 S1[ 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 ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * st ( Ck = \$2 & \$3 = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) ); ( 1 <= i + 1 & i + 1 <= len a ) by A12, NAT_1:11, NAT_1:13; then A14: i + 1 in dom (the_arity_of o) by A9, FINSEQ_3:25; then reconsider rs1 = (the_arity_of o) . (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 (InducedGraph S) as non empty set ; reconsider e19 = [o,rs1] as Element of E9 by A14, A15, Def1; reconsider C19 = <*e19*> as Element of the carrier' of (InducedGraph S) * by FINSEQ_1:def_11; A17: for k being Element of NAT st 1 <= k & k < n1 holds for x being Element of the carrier' of (InducedGraph S) * ex y being Element of the carrier' of (InducedGraph S) * st S1[k,x,y] proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k < n1 implies for x being Element of the carrier' of (InducedGraph S) * ex y being Element of the carrier' of (InducedGraph S) * st S1[k,x,y] ) set pk9 = p /^ k; k <= k + 1 by NAT_1:13; then A18: Seg k c= Seg (k + 1) by FINSEQ_1:5; 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 ; ::_thesis: for x being Element of the carrier' of (InducedGraph S) * ex y being Element of the carrier' of (InducedGraph S) * st S1[k,x,y] A20: len (p /^ k) = n - k by A4, A6, A11, A19, RFINSEQ:def_1; then A21: len (p /^ k) <> 0 by A19; then A22: 1 in dom (p /^ k) by CARD_1:27, FINSEQ_5:6; reconsider t1 = t9 | pk, t2 = t9 | pk1 as Term of S,X by MSATERM:29; p = pk ^ (p /^ k) by RFINSEQ:8; then A23: p /^ k in tr | pk by A5, A10, TREES_1:def_6; then A24: p /^ k 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__::_thesis:_not_t1_is_root assume t1 is root ; ::_thesis: contradiction then dom t1 = elementary_tree 0 by TREES_9:def_1; hence contradiction by A20, A26, A24, TREES_1:42, TREES_1:def_12; ::_thesis: verum 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: (p /^ k) | 1 = <*((p /^ k) /. 1)*> by A21, CARD_1:27, FINSEQ_5:20 .= <*((p /^ k) . 1)*> by A22, PARTFUN1:def_6 ; consider i being Element of NAT , T being DecoratedTree, q being Node of T such that A30: i < len a and T = a . (i + 1) and A31: p /^ k = <*i*> ^ q by A21, A24, A28, CARD_1:27, TREES_4:11; reconsider pk9 = p /^ k 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_15 .= (p | (Seg (k + 1))) | (Seg k) by FINSEQ_1:def_15 .= p | (Seg k) by A18, FUNCT_1:51 .= pk by FINSEQ_1:def_15 ; set args = the_arity_of o; let x be Element of the carrier' of (InducedGraph S) * ; ::_thesis: ex y being Element of the carrier' of (InducedGraph S) * st S1[k,x,y] A33: dom a = dom (the_arity_of o) 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, NAT_1:13; then A39: i + 1 in dom (the_arity_of o) by A33, FINSEQ_3:25; then reconsider rs1 = (the_arity_of o) . (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 (InducedGraph S) as non empty set ; reconsider e19 = [o,rs1] 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 the carrier' of (InducedGraph S) * by FINSEQ_1:def_11; take y ; ::_thesis: S1[k,x,y] take t1 ; ::_thesis: ex t2 being Term of S,X st ( t1 = t | (p | k) & t2 = t | (p | (k + 1)) & ex o being OperSymbol of S ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * st ( Ck = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) ) take t2 ; ::_thesis: ( t1 = t | (p | k) & t2 = t | (p | (k + 1)) & ex o being OperSymbol of S ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * st ( Ck = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) ) thus ( t1 = t | (p | k) & t2 = t | (p | (k + 1)) ) ; ::_thesis: ex o being OperSymbol of S ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * st ( Ck = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) take o ; ::_thesis: ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * st ( Ck = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) take rs1 ; ::_thesis: ex Ck being Element of the carrier' of (InducedGraph S) * st ( Ck = x & y = <*[o,rs1]*> ^ Ck & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) take x ; ::_thesis: ( x = x & y = <*[o,rs1]*> ^ x & [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) thus ( x = x & y = <*[o,rs1]*> ^ x ) ; ::_thesis: ( [o, the carrier of S] = t1 . {} & rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) thus [o, the carrier of S] = t1 . {} by A27; ::_thesis: ( rs1 = the_sort_of t2 & [o,rs1] in the carrier' of (InducedGraph S) ) 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; ::_thesis: [o,rs1] in the carrier' of (InducedGraph S) thus [o,rs1] in the carrier' of (InducedGraph S) by A39, A40, Def1; ::_thesis: verum end; consider C being FinSequence of the carrier' of (InducedGraph S) * such that A41: ( len C = n1 & ( C . 1 = C19 or n1 = 0 ) & ( for k being Element of NAT st 1 <= k & k < n1 holds S1[k,C . k,C . (k + 1)] ) ) from RECDEF_1:sch_4(A17); defpred S2[ Nat] means ( 1 <= \$1 & \$1 <= n implies ex Ck being directed Chain of InducedGraph S ex 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 being Nat st S2[i] holds S2[i + 1] proof let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A43: ( 1 <= k & k <= n implies ex Ck being directed Chain of InducedGraph S ex 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 ) ) ; ::_thesis: S2[k + 1] A44: k <= k + 1 by NAT_1:11; assume that 1 <= k + 1 and A45: k + 1 <= n ; ::_thesis: ex Ck being directed Chain of InducedGraph S ex t1 being Term of S,X st ( Ck = C . (k + 1) & len Ck = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq Ck) . ((len Ck) + 1) = v & (vertex-seq Ck) . 1 = the_sort_of t1 ) A46: k < n by A45, NAT_1:13; percases ( k = 0 or k <> 0 ) ; supposeA47: k = 0 ; ::_thesis: ex Ck being directed Chain of InducedGraph S ex t1 being Term of S,X st ( Ck = C . (k + 1) & len Ck = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq Ck) . ((len Ck) + 1) = v & (vertex-seq Ck) . 1 = the_sort_of t1 ) reconsider C1 = <*[o,rs1]*> as directed Chain of InducedGraph S 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 ; ::_thesis: ex t1 being Term of S,X st ( C1 = C . (k + 1) & len C1 = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t1 ) take t2 ; ::_thesis: ( C1 = C . (k + 1) & len C1 = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 ) thus C1 = C . (k + 1) by A1, A41, A47; ::_thesis: ( len C1 = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 ) thus len C1 = k + 1 by A47, FINSEQ_1:39; ::_thesis: ( t2 = t | (p | (k + 1)) & (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 ) thus t2 = t | (p | (k + 1)) by A47; ::_thesis: ( (vertex-seq C1) . ((len C1) + 1) = v & (vertex-seq C1) . 1 = the_sort_of t2 ) reconsider p9 = p as PartFunc of NAT,NAT ; A48: vertex-seq C1 = <*( the Source of (InducedGraph S) . [o,rs1]),( the Target of (InducedGraph S) . [o,rs1])*> by A16, MSSCYC_1:7; (vertex-seq C1) . ((len C1) + 1) = (vertex-seq C1) . (1 + 1) by FINSEQ_1:39 .= the Target of (InducedGraph S) . [o,rs1] by A48, FINSEQ_1:44 .= the ResultSort of S . ([o,rs1] `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 ; ::_thesis: (vertex-seq C1) . 1 = the_sort_of t2 A49: 1 in dom p by A1, A4, A6, A11, CARD_1:27, FINSEQ_5:6; p | 1 = <*(p9 /. 1)*> by A1, A4, A6, A11, CARD_1:27, FINSEQ_5:20 .= <*(p . 1)*> by A49, PARTFUN1:def_6 .= <*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 (InducedGraph S) . [o,rs1] by A48, FINSEQ_1:44 .= [o,rs1] `2 by A16, Def2 .= rs1 .= the_sort_of t2 by A9, A14, A50, MSATERM:23 ; hence (vertex-seq C1) . 1 = the_sort_of t2 ; ::_thesis: verum end; supposeA51: k <> 0 ; ::_thesis: ex Ck being directed Chain of InducedGraph S ex t1 being Term of S,X st ( Ck = C . (k + 1) & len Ck = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq Ck) . ((len Ck) + 1) = v & (vertex-seq Ck) . 1 = the_sort_of t1 ) k in NAT by ORDINAL1:def_12; then 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 ex rs1 being SortSymbol of S ex Ck being Element of the carrier' of (InducedGraph S) * 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 (InducedGraph S) ) by A41, A46, A51, NAT_1:14; consider o being OperSymbol of S, rs1 being SortSymbol of S, Ck9 being Element of the carrier' of (InducedGraph S) * 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 (InducedGraph S) by A54; A59: not InducedGraph S is void by A58; reconsider C1 = <*[o,rs1]*> as directed Chain of InducedGraph S by A58, MSSCYC_1:5; set e1 = [o,rs1]; A60: vertex-seq C1 = <*( the Source of (InducedGraph S) . [o,rs1]),( the Target of (InducedGraph S) . [o,rs1])*> by A58, MSSCYC_1:7; consider Ck being directed Chain of InducedGraph S, 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 (InducedGraph S) . [o,rs1] by A60, FINSEQ_1:44 .= the ResultSort of S . ([o,rs1] `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 InducedGraph S by A51, A62, A63, A65, A52, A59, CARD_1:27, MSSCYC_1:15; take d ; ::_thesis: ex t1 being Term of S,X st ( d = C . (k + 1) & len d = k + 1 & t1 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t1 ) take t2 ; ::_thesis: ( d = C . (k + 1) & len d = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 ) thus d = C . (k + 1) by A61, A55; ::_thesis: ( len d = k + 1 & t2 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 ) thus len d = (len C1) + k by A62, FINSEQ_1:22 .= k + 1 by FINSEQ_1:39 ; ::_thesis: ( t2 = t | (p | (k + 1)) & (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 ) thus t2 = t | (p | (k + 1)) by A53; ::_thesis: ( (vertex-seq d) . ((len d) + 1) = v & (vertex-seq d) . 1 = the_sort_of t2 ) thus (vertex-seq d) . ((len d) + 1) = v by A51, A62, A64, A59, CARD_1:27, MSSCYC_1:16; ::_thesis: (vertex-seq d) . 1 = the_sort_of t2 (vertex-seq C1) . 1 = the Source of (InducedGraph S) . [o,rs1] by A60, FINSEQ_1:44 .= [o,rs1] `2 by A58, Def2 .= the_sort_of t2 by A57 ; hence (vertex-seq d) . 1 = the_sort_of t2 by A51, A62, A59, CARD_1:27, MSSCYC_1:16; ::_thesis: verum end; end; end; A66: S2[ 0 ] ; for k being Nat holds S2[k] from NAT_1:sch_2(A66, A42); then ex c being directed Chain of InducedGraph S ex 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 ex c being directed Chain of InducedGraph S st ( len c = n & (vertex-seq c) . ((len c) + 1) = v ) ; ::_thesis: verum end; given c being directed Chain of InducedGraph S such that A67: len c = n and A68: (vertex-seq c) . ((len c) + 1) = v ; ::_thesis: ex t being Element of the Sorts of (FreeMSA X) . v st depth t = n set EG = the carrier' of (InducedGraph S); reconsider n1 = n as Element of NAT by ORDINAL1:def_12; deffunc H1( set ) -> set = X . \$1; set TG = the Target of (InducedGraph S); set SG = the Source of (InducedGraph S); set D = S -Terms X; set cS = the carrier of S; A69: for e being set st e in the carrier of S holds H1(e) <> {} ; consider cX being ManySortedSet of the carrier of S such that A70: for e being set st e in the carrier of S holds cX . e in H1(e) from PBOOLE:sch_1(A69); defpred S1[ Nat, set , set ] means ex o being OperSymbol of S ex rs1 being SortSymbol of S ex Ck, Ck1 being Term of S,X ex a being ArgumentSeq of Sym (o,X) st ( Ck = \$2 & \$3 = Ck1 & c . (\$1 + 1) = [o,rs1] & Ck1 = [o, the carrier of S] -tree a & ( for i being Nat st i in dom a holds 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 = the carrier' of (InducedGraph S) 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 ex 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 = rs1 as SortSymbol of S by A75; reconsider o = o as OperSymbol of S by A74; deffunc H2( Nat) -> set = 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 being Nat st k in dom a holds a . k = H2(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 holds 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; ::_thesis: ( i in dom a implies ex t being Term of S,X st ( t = a . i & the_sort_of t = (the_arity_of o) . i ) ) assume A80: i in dom a ; ::_thesis: ex t being Term of S,X st ( t = a . i & the_sort_of t = (the_arity_of o) . i ) 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 = (the_arity_of o) . i as SortSymbol of S by A77, A78, A80, DTCONSTR:2; set x = cX . ((the_arity_of o) . i); reconsider x = cX . ((the_arity_of o) . i) as Element of X . s by A70; reconsider t = root-tree [x,s] as Term of S,X by MSATERM:4; take t ; ::_thesis: ( t = a . i & the_sort_of t = (the_arity_of o) . i ) thus t = a . i by A77, A80; ::_thesis: the_sort_of t = (the_arity_of o) . i thus the_sort_of t = (the_arity_of o) . i by MSATERM:14; ::_thesis: verum end; A81: dom a = Seg (len (the_arity_of o)) by A77, FINSEQ_1:def_3; reconsider a = a as ArgumentSeq of Sym (o,X) by A77, A79, MSATERM:24; set C1 = [o, the carrier of S] -tree a; reconsider C1 = [o, the carrier of S] -tree a as Term of S,X by MSATERM:1; A82: for k being Element of NAT st 1 <= k & k < n1 holds for x being Element of S -Terms X ex y being Element of S -Terms X st S1[k,x,y] proof let k be Element of NAT ; ::_thesis: ( 1 <= k & k < n1 implies for x being Element of S -Terms X ex y being Element of S -Terms X st S1[k,x,y] ) assume that 1 <= k and A83: k < n1 ; ::_thesis: for x being Element of S -Terms X ex y being Element of S -Terms X st S1[k,x,y] 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 S -Terms X; ::_thesis: ex y being Element of S -Terms X st S1[k,x,y] consider o, rs1 being set such that A85: ck1 = [o,rs1] and A86: o in the carrier' of S and A87: rs1 in the carrier of S and ex n being Nat ex 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 = rs1 as SortSymbol of S by A87; reconsider o = o as OperSymbol of S by A86; set DA = dom (the_arity_of o); set ar = the_arity_of o; defpred S2[ set , set ] means ( ( (the_arity_of o) . \$1 = rs1 & the_sort_of x = rs1 implies \$2 = x ) & ( ( (the_arity_of o) . \$1 <> rs1 or the_sort_of x <> rs1 ) implies \$2 = root-tree [(cX . ((the_arity_of o) . \$1)),((the_arity_of o) . \$1)] ) ); A88: for e being set st e in dom (the_arity_of o) holds ex u being set st ( u in S -Terms X & S2[e,u] ) proof let e be set ; ::_thesis: ( e in dom (the_arity_of o) implies ex u being set st ( u in S -Terms X & S2[e,u] ) ) assume A89: e in dom (the_arity_of o) ; ::_thesis: ex u being set st ( u in S -Terms X & S2[e,u] ) percases ( ( (the_arity_of o) . e = rs1 & the_sort_of x = rs1 ) or (the_arity_of o) . e <> rs1 or the_sort_of x <> rs1 ) ; supposeA90: ( (the_arity_of o) . e = rs1 & the_sort_of x = rs1 ) ; ::_thesis: ex u being set st ( u in S -Terms X & S2[e,u] ) take x ; ::_thesis: ( x in S -Terms X & S2[e,x] ) thus ( x in S -Terms X & S2[e,x] ) by A90; ::_thesis: verum end; supposeA91: ( (the_arity_of o) . e <> rs1 or the_sort_of x <> rs1 ) ; ::_thesis: ex u being set st ( u in S -Terms X & S2[e,u] ) 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 ; ::_thesis: ( t in S -Terms X & S2[e,t] ) thus ( t in S -Terms X & S2[e,t] ) by A91; ::_thesis: verum end; end; end; consider a being Function of (dom (the_arity_of o)),(S -Terms X) such that A92: for e being set st e in dom (the_arity_of o) holds S2[e,a . e] from FUNCT_2:sch_1(A88); dom (the_arity_of o) = Seg (len (the_arity_of o)) by FINSEQ_1:def_3; then reconsider a = a as FinSequence of S -Terms X by FINSEQ_2:25; A93: dom a = dom (the_arity_of o) by FUNCT_2:def_1; now__::_thesis:_for_i_being_Nat_st_i_in_dom_a_holds_ ex_t_being_Term_of_S,X_st_ (_t_=_a_._i_&_the_sort_of_t_=_(the_arity_of_o)_._i_) let i be Nat; ::_thesis: ( i in dom a implies ex t being Term of S,X st ( t = a . i & the_sort_of b3 = (the_arity_of o) . b2 ) ) assume A94: i in dom a ; ::_thesis: ex t being Term of S,X st ( t = a . i & the_sort_of b3 = (the_arity_of o) . b2 ) then reconsider t = a . i as Term of S,X by DTCONSTR:2; take t = t; ::_thesis: ( t = a . i & the_sort_of b2 = (the_arity_of o) . b1 ) thus t = a . i ; ::_thesis: the_sort_of b2 = (the_arity_of o) . b1 percases ( ( (the_arity_of o) . i = rs1 & the_sort_of x = rs1 ) or (the_arity_of o) . i <> rs1 or the_sort_of x <> rs1 ) ; suppose ( (the_arity_of o) . i = rs1 & the_sort_of x = rs1 ) ; ::_thesis: the_sort_of b2 = (the_arity_of o) . b1 hence the_sort_of t = (the_arity_of o) . i by A92, A93, A94; ::_thesis: verum end; supposeA95: ( (the_arity_of o) . i <> rs1 or the_sort_of x <> rs1 ) ; ::_thesis: the_sort_of b2 = (the_arity_of o) . b1 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 . ((the_arity_of o) . i)),((the_arity_of o) . i)] by A92, A93, A94, A95; hence the_sort_of t = (the_arity_of o) . i by A96, MSATERM:14; ::_thesis: verum end; end; end; then reconsider a = a as ArgumentSeq of Sym (o,X) by A93, MSATERM:24; reconsider y = [o, the carrier of S] -tree a as Term of S,X by MSATERM:1; take y ; ::_thesis: S1[k,x,y] take o ; ::_thesis: ex rs1 being SortSymbol of S ex Ck, Ck1 being Term of S,X ex a being ArgumentSeq of Sym (o,X) st ( Ck = x & y = Ck1 & c . (k + 1) = [o,rs1] & Ck1 = [o, the carrier of S] -tree a & ( for i being Nat st i in dom a holds 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)] ) ) ) ) take rs1 ; ::_thesis: ex Ck, Ck1 being Term of S,X ex a being ArgumentSeq of Sym (o,X) st ( Ck = x & y = Ck1 & c . (k + 1) = [o,rs1] & Ck1 = [o, the carrier of S] -tree a & ( for i being Nat st i in dom a holds 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)] ) ) ) ) take x ; ::_thesis: ex Ck1 being Term of S,X ex a being ArgumentSeq of Sym (o,X) st ( x = x & y = Ck1 & c . (k + 1) = [o,rs1] & Ck1 = [o, the carrier of S] -tree a & ( for i being Nat st i in dom a holds 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 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)] ) ) ) ) take y ; ::_thesis: ex a being ArgumentSeq of Sym (o,X) st ( x = x & y = y & c . (k + 1) = [o,rs1] & y = [o, the carrier of S] -tree a & ( for i being Nat st i in dom a holds 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 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)] ) ) ) ) take a ; ::_thesis: ( x = x & y = y & c . (k + 1) = [o,rs1] & y = [o, the carrier of S] -tree a & ( for i being Nat st i in dom a holds 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 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)] ) ) ) ) thus ( x = x & y = y ) ; ::_thesis: ( c . (k + 1) = [o,rs1] & y = [o, the carrier of S] -tree a & ( for i being Nat st i in dom a holds 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 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)] ) ) ) ) thus c . (k + 1) = [o,rs1] by A85; ::_thesis: ( y = [o, the carrier of S] -tree a & ( for i being Nat st i in dom a holds 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 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)] ) ) ) ) thus y = [o, the carrier of S] -tree a ; ::_thesis: for i being Nat st i in dom a holds 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 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)] ) ) let i be Nat; ::_thesis: ( i in dom a implies 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 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)] ) ) ) assume A97: i in dom a ; ::_thesis: 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 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)] ) ) then reconsider t = a . i as Term of S,X by DTCONSTR:2; take t ; ::_thesis: ( t = a . i & the_sort_of t = (the_arity_of o) . i & ( 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)] ) ) thus t = a . i ; ::_thesis: ( the_sort_of t = (the_arity_of o) . i & ( 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)] ) ) thus the_sort_of t = (the_arity_of o) . i by A97, MSATERM:23; ::_thesis: ( ( 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)] ) ) 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 A92, A93, A97; ::_thesis: verum end; consider C being FinSequence of S -Terms X such that A98: ( len C = n1 & ( C . 1 = C1 or n1 = 0 ) & ( for k being Element of NAT st 1 <= k & k < n1 holds S1[k,C . k,C . (k + 1)] ) ) from RECDEF_1:sch_4(A82); defpred S2[ Nat] means ( 1 <= \$1 & \$1 <= n implies ex C0 being Term of S,X ex 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: not InducedGraph S is void by A72; A100: for k being Nat st S2[k] holds S2[k + 1] proof let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A101: ( 1 <= k & k <= n implies ex Ck being Term of S,X ex 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 ) ) ; ::_thesis: S2[k + 1] assume that A102: 1 <= k + 1 and A103: k + 1 <= n ; ::_thesis: ex C0 being Term of S,X ex o being OperSymbol of S st ( C0 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C0 = the_result_sort_of o & height (dom C0) = k + 1 ) 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; percases ( k = 0 or k <> 0 ) ; supposeA107: k = 0 ; ::_thesis: ex C0 being Term of S,X ex o being OperSymbol of S st ( C0 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C0 = the_result_sort_of o & height (dom C0) = k + 1 ) take C1 ; ::_thesis: ex o being OperSymbol of S st ( C1 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 ) take o ; ::_thesis: ( C1 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 ) thus C1 = C . (k + 1) by A1, A98, A107; ::_thesis: ( o = (c . (k + 1)) `1 & the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 ) thus o = (c . (k + 1)) `1 by A73, A107, MCART_1:7; ::_thesis: ( the_sort_of C1 = the_result_sort_of o & height (dom C1) = k + 1 ) reconsider w = doms a as FinTree-yielding FinSequence ; A108: dom (doms a) = dom a by TREES_3:37; C1 . {} = [o, the carrier of S] by TREES_4:def_4; hence the_sort_of C1 = the_result_sort_of o by MSATERM:17; ::_thesis: height (dom C1) = k + 1 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__::_thesis:_for_t9_being_finite_Tree_st_t9_in_rng_w_holds_ height_t9_<=_height_dt let t9 be finite Tree; ::_thesis: ( t9 in rng w implies height t9 <= height dt ) assume t9 in rng w ; ::_thesis: height t9 <= height dt 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; ::_thesis: verum end; dom t = elementary_tree 0 by A114, TREES_4:3; hence height (dom C1) = k + 1 by A107, A113, A115, TREES_1:42, TREES_3:79; ::_thesis: verum end; supposeA119: k <> 0 ; ::_thesis: ex C0 being Term of S,X ex o being OperSymbol of S st ( C0 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of C0 = the_result_sort_of o & height (dom C0) = k + 1 ) 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, the carrier of S] -tree a and A128: for i being Nat st i in dom a holds 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 c . (kk + 1) in EG by A71, DTCONSTR:2; then consider o9, rs19 being set such that A130: c . (kk + 1) = [o9,rs19] and A131: o9 in the carrier' of S and rs19 in the carrier of S and A132: ex n being Nat ex 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 ; ::_thesis: ex o being OperSymbol of S st ( Ck1 = C . (k + 1) & o = (c . (k + 1)) `1 & the_sort_of Ck1 = the_result_sort_of o & height (dom Ck1) = k + 1 ) take o1 ; ::_thesis: ( Ck1 = C . (k + 1) & o1 = (c . (k + 1)) `1 & the_sort_of Ck1 = the_result_sort_of o1 & height (dom Ck1) = k + 1 ) thus Ck1 = C . (k + 1) by A125; ::_thesis: ( o1 = (c . (k + 1)) `1 & the_sort_of Ck1 = the_result_sort_of o1 & height (dom Ck1) = k + 1 ) thus o1 = (c . (k + 1)) `1 by A126, MCART_1:7; ::_thesis: ( the_sort_of Ck1 = the_result_sort_of o1 & height (dom Ck1) = k + 1 ) Ck1 . {} = [o1, the carrier of S] by A127, TREES_4:def_4; hence the_sort_of Ck1 = the_result_sort_of o1 by MSATERM:17; ::_thesis: height (dom Ck1) = k + 1 A134: dom Ck1 = tree (doms a) by A127, TREES_4:10; reconsider ck1 = c . (kk + 1) 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 = 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__::_thesis:_for_t9_being_finite_Tree_st_t9_in_rng_w_holds_ height_t9_<=_height_dt let t9 be finite Tree; ::_thesis: ( t9 in rng w implies height b1 <= height dt ) assume t9 in rng w ; ::_thesis: height b1 <= height dt 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; percases ( ( the_sort_of t99 = rs1 & the_sort_of Ck9 = rs1 ) or the_sort_of t99 <> rs1 or the_sort_of Ck9 <> rs1 ) ; suppose ( the_sort_of t99 = rs1 & the_sort_of Ck9 = rs1 ) ; ::_thesis: height b1 <= height dt hence height t9 <= height dt by A143, A133, A136, A138, A142, A145, A146, A147, A148, FUNCT_6:22, MSUALG_1:def_1; ::_thesis: verum end; suppose ( the_sort_of t99 <> rs1 or the_sort_of Ck9 <> rs1 ) ; ::_thesis: height b1 <= height dt hence height t9 <= height dt by A146, A149, A150, TREES_1:42, TREES_4:3; ::_thesis: verum end; 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 .= the Target of (InducedGraph S) . ck by Def3 .= (vertex-seq c) . (kk + 1) by A67, A99, A106, A120, CARD_1:27, MSSCYC_1:11 .= the Source of (InducedGraph S) . ck1 by A67, A99, A102, A103, CARD_1:27, MSSCYC_1:11 .= ck1 `2 by Def2 .= rs1 by A126, MCART_1:7 ; hence height (dom Ck1) = k + 1 by A121, A123, A124, A134, A133, A136, A138, A142, A151, A144, MSUALG_1:def_1, TREES_3:79; ::_thesis: verum end; end; end; set cn = c . (len c); n in dom c by A1, A67, CARD_1:27, FINSEQ_5:6; then A152: c . (len c) in InducedEdges S by A67, A71, DTCONSTR:2; A153: S2[ 0 ] ; for k being Nat holds S2[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; not InducedGraph S is void by A72; then (vertex-seq c) . ((len c) + 1) = the Target of (InducedGraph S) . (c . (len c)) by A1, A67, CARD_1:27, MSSCYC_1:14 .= the ResultSort of S . ((c . (len c)) `1) by A152, Def3 .= the_result_sort_of o by A67, A154, MSUALG_1:def_2 ; then reconsider Cn = Cn as Element of the Sorts of (FreeMSA X) . v by A2, A68, A155, MSATERM:def_5; take Cn ; ::_thesis: depth Cn = n thus depth Cn = n by A156, MSAFREE2:def_14; ::_thesis: verum end; theorem :: MSSCYC_2:3 for S being non empty void ManySortedSign holds ( S is monotonic iff InducedGraph S is well-founded ) proof let S be non empty void ManySortedSign ; ::_thesis: ( S is monotonic iff InducedGraph S is well-founded ) set G = InducedGraph S; set OS = the carrier' of S; set CA = the carrier of S; set AR = the Arity of S; hereby ::_thesis: ( InducedGraph S is well-founded implies S is monotonic ) assume S is monotonic ; ::_thesis: InducedGraph S is well-founded assume not InducedGraph S is well-founded ; ::_thesis: contradiction then consider v being Element of the carrier of (InducedGraph S) such that A1: for n being Element of NAT ex c being directed Chain of InducedGraph S st ( not c is empty & (vertex-seq c) . ((len c) + 1) = v & len c > n ) by MSSCYC_1:def_4; consider e being directed Chain of InducedGraph S such that A2: not e is empty and (vertex-seq e) . ((len e) + 1) = v and len e > 0 by A1; e is FinSequence of the carrier' of (InducedGraph S) by MSSCYC_1:def_1; then A3: rng e c= the carrier' of (InducedGraph S) 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 the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st ( the Arity of S . op = args & n in dom args & args . n = v ) ) by A3, Def1; hence contradiction ; ::_thesis: verum end; assume InducedGraph S is well-founded ; ::_thesis: S is monotonic let A be non-empty finitely-generated MSAlgebra over S; :: according to MSAFREE2:def_13 ::_thesis: A is finite-yielding thus the Sorts of A is V34() by MSAFREE2:def_10; :: according to MSAFREE2:def_11 ::_thesis: verum end; theorem :: MSSCYC_2:4 for S being non empty non void ManySortedSign st S is monotonic holds InducedGraph S is well-founded proof let S be non empty non void ManySortedSign ; ::_thesis: ( S is monotonic implies InducedGraph S is well-founded ) set G = InducedGraph S; assume S is monotonic ; ::_thesis: InducedGraph S is well-founded then reconsider S = S as non empty non void monotonic ManySortedSign ; set A = the non-empty finite-yielding MSAlgebra over S; assume not InducedGraph S is well-founded ; ::_thesis: contradiction then consider v being Element of the carrier of (InducedGraph S) such that A1: for n being Element of NAT ex c being directed Chain of InducedGraph S st ( not c is empty & (vertex-seq c) . ((len c) + 1) = v & len c > n ) by MSSCYC_1:def_4; reconsider v = v as SortSymbol of S ; consider s being non empty finite Subset of NAT such that A2: s = { (depth t) where t is Element of the Sorts of (FreeEnv the non-empty finite-yielding MSAlgebra over S) . v : verum } and depth (v, the non-empty finite-yielding MSAlgebra over S) = max s by CIRCUIT1:def_6; max s in NAT by ORDINAL1:def_12; then consider c being directed Chain of InducedGraph S such that not c is 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 the non-empty finite-yielding MSAlgebra over S) . v such that A5: depth t = len c by A3, Th2; reconsider t9 = t as Element of the Sorts of (FreeEnv the non-empty finite-yielding MSAlgebra over S) . v ; ( ex t99 being Element of the Sorts of (FreeMSA the Sorts of the non-empty finite-yielding MSAlgebra over S) . 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; ::_thesis: verum end; theorem Th5: :: MSSCYC_2:5 for S being non empty non void ManySortedSign for X being V2() V34() ManySortedSet of the carrier of S st S is finitely_operated holds for n being Nat for 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 empty non void ManySortedSign ; ::_thesis: for X being V2() V34() ManySortedSet of the carrier of S st S is finitely_operated holds for n being Nat for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite let X be V2() V34() ManySortedSet of the carrier of S; ::_thesis: ( S is finitely_operated implies for n being Nat for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite ) assume A1: S is finitely_operated ; ::_thesis: for n being Nat for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite set SF = the Sorts of (FreeMSA X); defpred S1[ Nat] means for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= \$1 } is finite ; A2: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def_14; A3: for k being Nat st S1[k] holds S1[k + 1] proof deffunc H1( set ) -> set = \$1; let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: for v being SortSymbol of S holds { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n } is finite ; ::_thesis: S1[n + 1] let v be SortSymbol of S; ::_thesis: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n + 1 } is finite defpred S2[ Element of the Sorts of (FreeMSA X) . v] means depth \$1 = n + 1; defpred S3[ Element of the Sorts of (FreeMSA X) . v] means depth \$1 <= n + 1; defpred S4[ Element of the Sorts of (FreeMSA X) . v] means ( depth \$1 <= n or depth \$1 = n + 1 ); set dn1 = { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S3[t] } ; set dn11 = { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S4[t] } ; set den1 = { t where t is Element of the Sorts of (FreeMSA X) . v : S2[t] } ; set ov = { o where o is OperSymbol of S : the_result_sort_of o = v } ; A5: the Sorts of (FreeMSA X) . v = FreeSort (X,v) by A2, MSAFREE:def_11; { o where o is OperSymbol of S : the_result_sort_of o = v } is finite by A1, MSSCYC_1:def_5; then consider ovs being FinSequence such that A6: rng ovs = { o where o is OperSymbol of S : the_result_sort_of o = v } by FINSEQ_1:52; deffunc H2( set ) -> set = { t where t is Element of the Sorts of (FreeMSA X) . 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 = H2(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: { t where t is Element of the Sorts of (FreeMSA X) . v : S2[t] } c= Union dvs proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Element of the Sorts of (FreeMSA X) . v : S2[t] } or x in Union dvs ) assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : S2[t] } ; ::_thesis: x in Union dvs then consider t being Element of the Sorts of (FreeMSA X) . 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__::_thesis:_not_t9_is_root A13: ex dt being finite DecoratedTree ex tt being finite Tree st ( dt = t & tt = dom dt & depth t = height tt ) by MSAFREE2:def_14; assume t9 is root ; ::_thesis: contradiction hence contradiction by A12, A13, TREES_1:42, TREES_9:def_1; ::_thesis: verum 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 set 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 the Sorts of (FreeMSA X) . 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 x in Union dvs by A11, CARD_3:def_4; ::_thesis: verum end; for k being set st k in dom dvs holds dvs . k is finite proof let k be set ; ::_thesis: ( k in dom dvs implies dvs . k is finite ) set dvsk = { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . k), the carrier of S] ) } ; assume A18: k in dom dvs ; ::_thesis: dvs . k is finite 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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; A20: { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . k), the carrier of S] ) } c= { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . k), the carrier of S] ) } or x in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : ( depth t = n + 1 & t . {} = [(ovs . k), the carrier of S] ) } ; ::_thesis: x in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } then consider t being Element of the Sorts of (FreeMSA X) . 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 { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A22, A24; hence x in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A21, A24; ::_thesis: verum end; deffunc H3( Nat) -> set = { t where t is Element of the Sorts of (FreeMSA X) . ((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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; A25: { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree 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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } 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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; take { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; :: according to TARSKI:def_6 ::_thesis: ( ( for b1 being set holds ( not b1 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ex b2 being set st ( b2 in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [b1,b2] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) ) ) & ( for b1 being set holds ( not b1 in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ex b2 being set st ( b2 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [b2,b1] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) ) ) & ( for b1, b2, b3, b4 being set holds ( not [b1,b2] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [b3,b4] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) ) hereby ::_thesis: ( ( for b1 being set holds ( not b1 in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ex b2 being set st ( b2 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [b2,b1] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) ) ) & ( for b1, b2, b3, b4 being set holds ( not [b1,b2] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [b3,b4] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) ) let x be set ; ::_thesis: ( x in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } implies ex y9 being set st ( y9 in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [x,y9] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) ) assume x in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; ::_thesis: ex y9 being set st ( y9 in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [x,y9] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) 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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) ; reconsider y9 = [o, the carrier of S] -tree a as set ; take y9 = y9; ::_thesis: ( y9 in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [x,y9] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) thus y9 in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A27; ::_thesis: [x,y9] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } thus [x,y9] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A26, A27; ::_thesis: verum end; hereby ::_thesis: for b1, b2, b3, b4 being set holds ( not [b1,b2] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [b3,b4] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) let y be set ; ::_thesis: ( y in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } implies ex a9 being set st ( a9 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [a9,y] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) ) assume y in { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; ::_thesis: ex a9 being set st ( a9 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [a9,y] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) 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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) ; reconsider a9 = a as set ; take a9 = a9; ::_thesis: ( a9 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } & [a9,y] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ) thus a9 in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A29; ::_thesis: [a9,y] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } thus [a9,y] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } by A28, A29; ::_thesis: verum end; let x, y, z, u be set ; ::_thesis: ( not [x,y] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or not [z,u] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) ) assume [x,y] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; ::_thesis: ( not [z,u] in { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or ( ( not x = z or y = u ) & ( not y = u or x = 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 the Sorts of (FreeMSA X) . 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 { [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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; ::_thesis: ( ( not x = z or y = u ) & ( not y = u or x = 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 the Sorts of (FreeMSA X) . 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; ::_thesis: ( not y = u or x = z ) 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 ; ::_thesis: x = z hence x = z by A31, A34, A32, A37, A35, A36, TREES_4:15; ::_thesis: verum 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 = H3(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: { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } c= product nS proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } or x in product nS ) assume x in { a where a is Element of (S -Terms X) * : ( a is ArgumentSeq of Sym (o,X) & ex t being Element of the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } ; ::_thesis: x in product nS 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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ; reconsider a = 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__::_thesis:_for_x_being_set_st_x_in_dom_a_holds_ a_._x_in_nS_._x let x be set ; ::_thesis: ( x in dom a implies a . x in nS . x ) assume A46: x in dom a ; ::_thesis: a . x in nS . x 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; the Sorts of (FreeMSA X) . (the_sort_of ak) = FreeSort (X,(the_sort_of ak)) by A2, MSAFREE:def_11; then reconsider ak = ak as Element of the Sorts of (FreeMSA X) . ((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 the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth tk <= n } ; { tk where tk is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth tk <= n } = nS . x by A38, A40, A45, A46; hence a . x in nS . x by A48; ::_thesis: verum end; hence x in product nS by A38, A39, A42, A45, CARD_3:def_5; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_nS_holds_ nS_._x_is_finite let x be set ; ::_thesis: ( x in dom nS implies nS . x is finite ) assume A49: x in dom nS ; ::_thesis: nS . x is finite then reconsider k = x as Nat ; set nSk = { t where t is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth t <= n } ; nS . k = { t where t is Element of the Sorts of (FreeMSA X) . ((the_arity_of o) /. k) : depth t <= n } by A38, A49; hence nS . x is finite by A4; ::_thesis: verum end; then nS is V34() by FINSET_1:def_4; then product nS is finite ; then { ([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 the Sorts of (FreeMSA X) . v st ( depth t = n + 1 & t = [o, the carrier of S] -tree a ) ) } is finite by A25, A41, CARD_1:38; hence dvs . k is finite by A7, A18, A20; ::_thesis: verum end; then A50: Union dvs is finite by CARD_2:88; defpred S5[ Element of the Sorts of (FreeMSA X) . v] means depth \$1 <= n; set dln = { t where t is Element of the Sorts of (FreeMSA X) . v : S5[t] } ; A51: { t where t is Element of the Sorts of (FreeMSA X) . v : ( S5[t] or S2[t] ) } = { t where t is Element of the Sorts of (FreeMSA X) . v : S5[t] } \/ { t where t is Element of the Sorts of (FreeMSA X) . v : S2[t] } from TOPREAL1:sch_1(); A52: for t being Element of the Sorts of (FreeMSA X) . v holds ( S3[t] iff S4[t] ) by NAT_1:8, NAT_1:12; A53: { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S3[t] } = { H1(t) where t is Element of the Sorts of (FreeMSA X) . v : S4[t] } from FRAENKEL:sch_3(A52); { t where t is Element of the Sorts of (FreeMSA X) . v : S5[t] } is finite by A4; hence { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= n + 1 } is finite by A53, A51, A50, A10; ::_thesis: verum end; A54: S1[ 0 ] proof let v be SortSymbol of S; ::_thesis: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } is finite set dle0 = { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } ; set d0 = { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } ; A55: { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } c= { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } or x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } ) assume x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } ; ::_thesis: x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } then consider t being Element of the Sorts of (FreeMSA X) . v such that A56: x = t and A57: depth t <= 0 ; depth t = 0 by A57; hence x in { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } by A56; ::_thesis: verum end; ( Constants ((FreeMSA X),v) is finite & { t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0 } = (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v)) ) by A1, MSSCYC_1:25, MSSCYC_1:26; hence { t where t is Element of the Sorts of (FreeMSA X) . v : depth t <= 0 } is finite by A55; ::_thesis: verum end; thus for n being Nat holds S1[n] from NAT_1:sch_2(A54, A3); ::_thesis: verum end; theorem :: MSSCYC_2:6 for S being non empty non void ManySortedSign st S is finitely_operated & InducedGraph S is well-founded holds S is monotonic proof let S be non empty non void ManySortedSign ; ::_thesis: ( S is finitely_operated & InducedGraph S is well-founded implies S is monotonic ) set G = InducedGraph S; assume that A1: S is finitely_operated and A2: InducedGraph S is well-founded ; ::_thesis: S is monotonic given A being non-empty finitely-generated MSAlgebra over S such that A3: not A is finite-yielding ; :: according to MSAFREE2:def_13 ::_thesis: contradiction set GS = the V2() V34() GeneratorSet of A; reconsider gs = the V2() V34() GeneratorSet of A as V2() V34() ManySortedSet of the carrier of S ; not FreeMSA gs is finite-yielding by A3, MSSCYC_1:23; then the Sorts of (FreeMSA gs) is V34() by MSAFREE2:def_11; then consider v being set such that A4: v in the carrier of S and A5: not the Sorts of (FreeMSA gs) . v is finite by FINSET_1:def_5; reconsider v = v as SortSymbol of S by A4; consider n being Element of NAT such that A6: for c being directed Chain of InducedGraph S st not c is 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 the Sorts of (FreeMSA gs) . v : depth t <= n } ; { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } is finite by A1, Th5; then not the Sorts of (FreeMSA gs) . v c= { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } by A5; then consider t being set such that A7: t in the Sorts of (FreeMSA gs) . v and A8: not t in { t where t is Element of the Sorts of (FreeMSA gs) . v : depth t <= n } by TARSKI:def_3; reconsider t = t as Element of the Sorts of (FreeMSA gs) . 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; ::_thesis: verum end;