msscyc_2.miz



    begin

    reserve k,n for Nat;

    definition

      let S be ManySortedSign;

      defpred P[ object] means ex op,v be set st $1 = [op, v] & op in the carrier' of S & v in the carrier of S & ex n be Nat, args be Element of (the carrier of S * ) st (the Arity of S . op) = args & n in ( dom args) & (args . n) = v;

      :: MSSCYC_2:def1

      func InducedEdges S -> set means

      : Def1: for x be object holds x in it iff ex op,v be set st x = [op, v] & op in the carrier' of S & v in the carrier of S & ex n be Nat, args be Element of (the carrier of S * ) st (the Arity of S . op) = args & n in ( dom args) & (args . n) = v;

      existence

      proof

        set XX = [:the carrier' of S, the carrier of S:];

        consider X be set such that

         A1: for x be object holds x in X iff x in XX & P[x] from XBOOLE_0:sch 1;

        take X;

        let x be object;

        thus x in X implies P[x] by A1;

        assume

         A2: P[x];

        then x in XX by ZFMISC_1:def 2;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

        hence thesis;

      end;

    end

    theorem :: MSSCYC_2:1

    

     Th1: for S be ManySortedSign holds ( InducedEdges S) c= [:the carrier' of S, the carrier of S:]

    proof

      let S be ManySortedSign;

      let x be object;

      assume x in ( InducedEdges S);

      then ex op,v be set st x = [op, v] & op in the carrier' of S & v in the carrier of S & ex n be Nat, args be Element of (the carrier of S * ) st (the Arity of S . op) = args & n in ( dom args) & (args . n) = v by Def1;

      hence thesis by ZFMISC_1:def 2;

    end;

    definition

      let S be ManySortedSign;

      set IE = ( InducedEdges S), IV = the carrier of S;

      :: MSSCYC_2:def2

      func InducedSource S -> Function of ( InducedEdges S), the carrier of S means

      : Def2: for e be object st e in ( InducedEdges S) holds (it . e) = (e `2 );

      existence

      proof

        deffunc F( object) = ($1 `2 );

        

         A1: for x be object st x in IE holds F(x) in IV

        proof

          let x be object;

          assume

           A2: x in IE;

          IE c= [:the carrier' of S, IV:] by Th1;

          hence thesis by A2, MCART_1: 10;

        end;

        ex f be Function of ( InducedEdges S), the carrier of S st for x be object st x in ( InducedEdges S) holds (f . x) = F(x) from FUNCT_2:sch 2( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Function of IE, IV such that

         A3: for e be object st e in IE holds (F1 . e) = (e `2 ) and

         A4: for e be object st e in IE holds (F2 . e) = (e `2 );

         A5:

        now

          let x be object;

          assume

           A6: x in IE;

          then (F1 . x) = (x `2 ) by A3;

          hence (F1 . x) = (F2 . x) by A4, A6;

        end;

        now

          assume IV is empty;

          then [:the carrier' of S, IV:] is empty by ZFMISC_1: 90;

          hence IE is empty by Th1, XBOOLE_1: 3;

        end;

        then ( dom F1) = IE & ( dom F2) = IE by FUNCT_2:def 1;

        hence F1 = F2 by A5, FUNCT_1: 2;

      end;

      set OS = the carrier' of S, RS = the ResultSort of S;

      :: MSSCYC_2:def3

      func InducedTarget S -> Function of ( InducedEdges S), the carrier of S means

      : Def3: for e be object st e in ( InducedEdges S) holds (it . e) = (the ResultSort of S . (e `1 ));

      existence

      proof

        deffunc F( object) = (RS . ($1 `1 ));

        

         A7: for x be object st x in IE holds F(x) in IV

        proof

          let x be object;

          assume

           A8: x in IE;

          IE c= [:OS, IV:] by Th1;

          then (x `1 ) in OS & (x `2 ) in IV by A8, MCART_1: 10;

          hence thesis by FUNCT_2: 5;

        end;

        ex f be Function of ( InducedEdges S), the carrier of S st for x be object st x in ( InducedEdges S) holds (f . x) = F(x) from FUNCT_2:sch 2( A7);

        hence thesis;

      end;

      uniqueness

      proof

        let F1,F2 be Function of IE, IV such that

         A9: for e be object st e in IE holds (F1 . e) = (RS . (e `1 )) and

         A10: for e be object st e in IE holds (F2 . e) = (RS . (e `1 ));

         A11:

        now

          let x be object;

          assume

           A12: x in IE;

          then (F1 . x) = (RS . (x `1 )) by A9;

          hence (F1 . x) = (F2 . x) by A10, A12;

        end;

        now

          assume IV is empty;

          then [:the carrier' of S, IV:] is empty by ZFMISC_1: 90;

          hence IE is empty by Th1, XBOOLE_1: 3;

        end;

        then ( dom F1) = IE & ( dom F2) = IE by FUNCT_2:def 1;

        hence F1 = F2 by A11, FUNCT_1: 2;

      end;

    end

    definition

      let S be non empty ManySortedSign;

      :: MSSCYC_2:def4

      func InducedGraph S -> Graph equals MultiGraphStruct (# the carrier of S, ( InducedEdges S), ( InducedSource S), ( InducedTarget S) #);

      coherence ;

    end

    theorem :: MSSCYC_2:2

    

     Th2: for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be SortSymbol of S, n st 1 <= n holds (ex t be Element of (the Sorts of ( FreeMSA X) . v) st ( depth t) = n) iff (ex c be directed Chain of ( InducedGraph S) st ( len c) = n & (( vertex-seq c) . (( len c) + 1)) = v)

    proof

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be SortSymbol of S, n;

      assume

       A1: 1 <= n;

      set G = ( InducedGraph S);

      ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

      then

       A2: (the Sorts of ( FreeMSA X) . v) = ( FreeSort (X,v)) by MSAFREE:def 11;

      

       A3: ( FreeSort (X,v)) c= (S -Terms X) by MSATERM: 12;

      thus (ex t be Element of (the Sorts of ( FreeMSA X) . v) st ( depth t) = n) implies ex c be directed Chain of ( InducedGraph S) st ( len c) = n & (( vertex-seq c) . (( len c) + 1)) = v

      proof

        reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

        set D = (the carrier' of G * );

        given t be Element of (the Sorts of ( FreeMSA X) . v) such that

         A4: ( depth t) = n;

        t in ( FreeSort (X,v)) by A2;

        then

        reconsider t9 = t as Term of S, X by A3;

        consider dt be finite DecoratedTree, tr be 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 be OperSymbol of S such that

         A7: (t9 . {} ) = [o, the carrier of S] by MSSCYC_1: 20;

        consider a be ArgumentSeq of ( Sym (o,X)) such that

         A8: t = ( [o, the carrier of S] -tree a) by A7, MSATERM: 10;

        set args = ( the_arity_of o);

        

         A9: ( dom a) = ( dom args) by MSATERM: 22;

        consider p be FinSequence of NAT such that

         A10: p in tr and

         A11: ( len p) = ( height tr) by TREES_1:def 12;

        consider i be Nat, T be DecoratedTree, q be Node of T such that

         A12: i < ( len a) and T = (a . (i + 1)) and

         A13: p = ( <*i*> ^ q) by A1, A4, A5, A6, A10, A11, A8, CARD_1: 27, TREES_4: 11;

        defpred P[ Nat, set, set] means ex t1,t2 be Term of S, X st t1 = (t | (p | $1)) & t2 = (t | (p | ($1 + 1))) & ex o be OperSymbol of S, rs1 be SortSymbol of S, Ck be Element of D st Ck = $2 & $3 = ( <* [o, rs1]*> ^ Ck) & [o, the carrier of S] = (t1 . {} ) & rs1 = ( the_sort_of t2) & [o, rs1] in the carrier' of G;

        1 <= (i + 1) & (i + 1) <= ( len a) by A12, NAT_1: 11, NAT_1: 13;

        then

         A14: (i + 1) in ( dom args) by A9, FINSEQ_3: 25;

        then

        reconsider rs1 = (args . (i + 1)) as SortSymbol of S by DTCONSTR: 2;

        set e1 = [o, rs1];

        

         A15: (the Arity of S . o) = ( the_arity_of o) by MSUALG_1:def 1;

        then

         A16: [o, rs1] in ( InducedEdges S) by A14, Def1;

        then

        reconsider E9 = the carrier' of G as non empty set;

        reconsider e19 = e1 as Element of E9 by A14, A15, Def1;

        reconsider C19 = <*e19*> as Element of D by FINSEQ_1:def 11;

        

         A17: for k be Nat st 1 <= k & k < n1 holds for x be Element of D holds ex y be Element of D st P[k, x, y]

        proof

          let k be Nat;

          set pk9 = (p /^ k);

          k <= (k + 1) by NAT_1: 13;

          then

           A18: ( Seg k) c= ( Seg (k + 1)) by FINSEQ_1: 5;

          k in NAT by ORDINAL1:def 12;

          then

          reconsider pk = (p | k), pk1 = (p | (k + 1)) as Node of t by A5, A10, MSSCYC_1: 19;

          assume that 1 <= k and

           A19: k < n1;

          

           A20: ( len pk9) = (n - k) by A4, A6, A11, A19, RFINSEQ:def 1;

          then

           A21: ( len pk9) <> 0 by A19;

          then

           A22: 1 in ( dom pk9) by CARD_1: 27, FINSEQ_5: 6;

          reconsider t1 = (t9 | pk), t2 = (t9 | pk1) as Term of S, X by MSATERM: 29;

          p = (pk ^ pk9) by RFINSEQ: 8;

          then

           A23: pk9 in (tr | pk) by A5, A10, TREES_1:def 6;

          then

           A24: pk9 in ( dom t1) by A5, TREES_2:def 10;

          

           A25: (k + 1) <= n by A19, NAT_1: 13;

          then

           A26: 1 <= (n - k) by XREAL_1: 19;

          now

            assume t1 is root;

            then ( dom t1) = ( elementary_tree 0 ) by TREES_9:def 1;

            hence contradiction by A20, A26, A24, TREES_1: 42, TREES_1:def 12;

          end;

          then

          consider o be OperSymbol of S such that

           A27: (t1 . {} ) = [o, the carrier of S] by MSSCYC_1: 20;

          consider a be ArgumentSeq of ( Sym (o,X)) such that

           A28: t1 = ( [o, the carrier of S] -tree a) by A27, MSATERM: 10;

          

           A29: (pk9 | 1) = <*(pk9 . 1)*> by A21, CARD_1: 27, FINSEQ_5: 20;

          consider i be Nat, T be DecoratedTree, q be Node of T such that

           A30: i < ( len a) and T = (a . (i + 1)) and

           A31: pk9 = ( <*i*> ^ q) by A21, A24, A28, CARD_1: 27, TREES_4: 11;

          reconsider pk9 as Node of t1 by A5, A23, TREES_2:def 10;

          reconsider p1 = (pk9 | ( 0 + 1)) as Node of t1 by MSSCYC_1: 19;

          reconsider t29 = (t1 | p1) as Term of S, X;

          

           A32: ((p | (k + 1)) | k) = ((p | (k + 1)) | ( Seg k)) by FINSEQ_1:def 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 D;

          

           A33: ( dom a) = ( dom args) by MSATERM: 22;

          

           A34: 1 <= (k + 1) by NAT_1: 11;

          then

           A35: (k + 1) in ( dom p) by A4, A6, A11, A25, FINSEQ_3: 25;

          

           A36: ( len pk1) = (k + 1) by A4, A6, A11, A25, FINSEQ_1: 59;

          then

           A37: (k + 1) in ( dom pk1) by A34, FINSEQ_3: 25;

          p1 = <*(p . (k + 1))*> by A4, A6, A11, A19, A22, A29, RFINSEQ:def 1

          .= <*(p /. (k + 1))*> by A35, PARTFUN1:def 6

          .= <*((p | (k + 1)) /. (k + 1))*> by A37, FINSEQ_4: 70

          .= <*(pk1 . (k + 1))*> by A37, PARTFUN1:def 6;

          then pk1 = (pk ^ p1) by A36, A32, RFINSEQ: 7;

          then

           A38: t29 = t2 by TREES_9: 3;

          1 <= (i + 1) & (i + 1) <= ( len a) by A30, NAT_1: 11, NAT_1: 13;

          then

           A39: (i + 1) in ( dom args) by A33, FINSEQ_3: 25;

          then

          reconsider rs1 = (args . (i + 1)) as SortSymbol of S by DTCONSTR: 2;

          set e1 = [o, rs1];

          

           A40: (the Arity of S . o) = ( the_arity_of o) by MSUALG_1:def 1;

          then [o, rs1] in ( InducedEdges S) by A39, Def1;

          then

          reconsider E9 = the carrier' of G as non empty set;

          reconsider e19 = e1 as Element of E9 by A39, A40, Def1;

          reconsider x9 = x as FinSequence of E9 by FINSEQ_1:def 11;

          reconsider y = ( <*e19*> ^ x9) as Element of D by FINSEQ_1:def 11;

          take y;

          take t1, t2;

          thus t1 = (t | (p | k)) & t2 = (t | (p | (k + 1)));

          take o, rs1, x;

          thus x = x & y = ( <* [o, rs1]*> ^ x);

          thus [o, the carrier of S] = (t1 . {} ) by A27;

          (pk9 | 1) = <*i*> by A31, A29, FINSEQ_1: 41;

          then t29 = (a . (i + 1)) by A28, A30, TREES_4:def 4;

          hence rs1 = ( the_sort_of t2) by A33, A39, A38, MSATERM: 23;

          thus thesis by A39, A40, Def1;

        end;

        consider C be FinSequence of D such that

         A41: ( len C) = n1 & ((C . 1) = C19 or n1 = 0 ) & for k be Nat st 1 <= k & k < n1 holds P[k, (C . k), (C . (k + 1))] from RECDEF_1:sch 4( A17);

        defpred Z[ Nat] means 1 <= $1 & $1 <= n implies ex Ck be directed Chain of G, t1 be Term of S, X st Ck = (C . $1) & ( len Ck) = $1 & t1 = (t | (p | $1)) & (( vertex-seq Ck) . (( len Ck) + 1)) = v & (( vertex-seq Ck) . 1) = ( the_sort_of t1);

        

         A42: for i be Nat st Z[i] holds Z[(i + 1)]

        proof

          let k;

          assume

           A43: 1 <= k & k <= n implies ex Ck be directed Chain of G, t1 be Term of S, X st Ck = (C . k) & ( len Ck) = k & t1 = (t | (p | k)) & (( vertex-seq Ck) . (( len Ck) + 1)) = v & (( vertex-seq Ck) . 1) = ( the_sort_of t1);

          

           A44: k <= (k + 1) by NAT_1: 11;

          assume that 1 <= (k + 1) and

           A45: (k + 1) <= n;

          

           A46: k < n by A45, NAT_1: 13;

          per cases ;

            suppose

             A47: k = 0 ;

            reconsider C1 = <*e1*> as directed Chain of G by A16, MSSCYC_1: 5;

            reconsider p1 = (p | ( 0 + 1)) as Node of t by A5, A10, MSSCYC_1: 19;

            reconsider t2 = (t9 | p1) as Term of S, X by MSATERM: 29;

            take C1, t2;

            thus C1 = (C . (k + 1)) by A1, A41, A47;

            thus ( len C1) = (k + 1) by A47, FINSEQ_1: 39;

            thus t2 = (t | (p | (k + 1))) by A47;

            reconsider p9 = p as PartFunc of NAT , NAT ;

            

             A48: ( vertex-seq C1) = <*(the Source of G . e1), (the Target of G . e1)*> by A16, MSSCYC_1: 7;

            (( vertex-seq C1) . (( len C1) + 1)) = (( vertex-seq C1) . (1 + 1)) by FINSEQ_1: 39

            .= (the Target of G . e1) by A48, FINSEQ_1: 44

            .= (the ResultSort of S . (e1 `1 )) by A16, Def3

            .= (the ResultSort of S . o)

            .= ( the_result_sort_of o) by MSUALG_1:def 2

            .= ( the_sort_of t9) by A7, MSATERM: 17

            .= v by A2, MSATERM:def 5;

            hence (( vertex-seq C1) . (( len C1) + 1)) = v;

            (p | 1) = <*(p9 . 1)*> by A1, A4, A6, A11, CARD_1: 27, FINSEQ_5: 20

            .= <*(p . 1)*>

            .= <*i*> by A13, FINSEQ_1: 41;

            then

             A50: t2 = (a . (i + 1)) by A8, A12, TREES_4:def 4;

            (( vertex-seq C1) . 1) = (the Source of G . e1) by A48, FINSEQ_1: 44

            .= (e1 `2 ) by A16, Def2

            .= rs1

            .= ( the_sort_of t2) by A9, A14, A50, MSATERM: 23;

            hence thesis;

          end;

            suppose

             A51: k <> 0 ;

            consider t1,t2 be Term of S, X such that

             A52: t1 = (t | (p | k)) and

             A53: t2 = (t | (p | (k + 1))) and

             A54: ex o be OperSymbol of S, rs1 be SortSymbol of S, Ck be Element of D st Ck = (C . k) & (C . (k + 1)) = ( <* [o, rs1]*> ^ Ck) & [o, the carrier of S] = (t1 . {} ) & rs1 = ( the_sort_of t2) & [o, rs1] in the carrier' of G by A41, A46, A51, NAT_1: 14;

            consider o be OperSymbol of S, rs1 be SortSymbol of S, Ck9 be Element of D such that

             A55: Ck9 = (C . k) & (C . (k + 1)) = ( <* [o, rs1]*> ^ Ck9) and

             A56: [o, the carrier of S] = (t1 . {} ) and

             A57: rs1 = ( the_sort_of t2) and

             A58: [o, rs1] in the carrier' of G by A54;

            

             A59: G is non void by A58;

            reconsider C1 = <* [o, rs1]*> as directed Chain of G by A58, MSSCYC_1: 5;

            set e1 = [o, rs1];

            

             A60: ( vertex-seq C1) = <*(the Source of G . e1), (the Target of G . e1)*> by A58, MSSCYC_1: 7;

            consider Ck be directed Chain of G, t19 be Term of S, X such that

             A61: Ck = (C . k) and

             A62: ( len Ck) = k and

             A63: t19 = (t | (p | k)) and

             A64: (( vertex-seq Ck) . (( len Ck) + 1)) = v and

             A65: (( vertex-seq Ck) . 1) = ( the_sort_of t19) by A43, A45, A44, A51, NAT_1: 14, XXREAL_0: 2;

            (( vertex-seq C1) . (( len C1) + 1)) = (( vertex-seq C1) . (1 + 1)) by FINSEQ_1: 39

            .= (the Target of G . e1) by A60, FINSEQ_1: 44

            .= (the ResultSort of S . (e1 `1 )) by A58, Def3

            .= (the ResultSort of S . o)

            .= ( the_result_sort_of o) by MSUALG_1:def 2

            .= ( the_sort_of t1) by A56, MSATERM: 17;

            then

            reconsider d = (C1 ^ Ck) as directed Chain of G by A51, A62, A63, A65, A52, A59, CARD_1: 27, MSSCYC_1: 15;

            take d, t2;

            thus d = (C . (k + 1)) by A61, A55;

            

            thus ( len d) = (( len C1) + k) by A62, FINSEQ_1: 22

            .= (k + 1) by FINSEQ_1: 39;

            thus t2 = (t | (p | (k + 1))) by A53;

            thus (( vertex-seq d) . (( len d) + 1)) = v by A51, A62, A64, A59, CARD_1: 27, MSSCYC_1: 16;

            (( vertex-seq C1) . 1) = (the Source of G . e1) by A60, FINSEQ_1: 44

            .= (e1 `2 ) by A58, Def2

            .= ( the_sort_of t2) by A57;

            hence thesis by A51, A62, A59, CARD_1: 27, MSSCYC_1: 16;

          end;

        end;

        

         A66: Z[ 0 ];

        for k holds Z[k] from NAT_1:sch 2( A66, A42);

        then ex c be directed Chain of G, t1 be Term of S, X st c = (C . n) & ( len c) = n & t1 = (t | (p | n)) & (( vertex-seq c) . (( len c) + 1)) = v & (( vertex-seq c) . 1) = ( the_sort_of t1) by A1;

        hence thesis;

      end;

      given c be directed Chain of ( InducedGraph S) such that

       A67: ( len c) = n and

       A68: (( vertex-seq c) . (( len c) + 1)) = v;

      set EG = the carrier' of G;

      reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

      deffunc F( object) = (X . $1);

      set TG = the Target of G;

      set SG = the Source of G;

      set D = (S -Terms X);

      set cS = the carrier of S;

      

       A69: for e be object st e in cS holds F(e) <> {} ;

      consider cX be ManySortedSet of cS such that

       A70: for e be object st e in cS holds (cX . e) in F(e) from PBOOLE:sch 1( A69);

      defpred P[ Nat, set, set] means ex o be OperSymbol of S, rs1 be SortSymbol of S, Ck,Ck1 be Term of S, X, a be ArgumentSeq of ( Sym (o,X)) st Ck = $2 & $3 = Ck1 & (c . ($1 + 1)) = [o, rs1] & Ck1 = ( [o, cS] -tree a) & (for i be Nat st i in ( dom a) holds ex t be Term of S, X st t = (a . i) & ( the_sort_of t) = (( the_arity_of o) . i) & (( the_sort_of t) = rs1 & ( the_sort_of Ck) = rs1 implies t = Ck) & (( the_sort_of t) <> rs1 or ( the_sort_of Ck) <> rs1 implies t = ( root-tree [(cX . ( the_sort_of t)), ( the_sort_of t)])));

      

       A71: c is FinSequence of the carrier' of ( InducedGraph S) by MSSCYC_1:def 1;

      

       A72: 1 in ( dom c) by A1, A67, FINSEQ_3: 25;

      then

      reconsider EG as non empty set by A71;

      (c . 1) in ( InducedEdges S) by A71, A72, DTCONSTR: 2;

      then

      consider o,rs1 be 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 be Nat, args be Element of (the carrier of S * ) st (the Arity of S . o) = args & n in ( dom args) & (args . n) = rs1 by Def1;

      reconsider rs1 as SortSymbol of S by A75;

      reconsider o as OperSymbol of S by A74;

      deffunc F( Nat) = ( root-tree [(cX . (( the_arity_of o) . $1)), (( the_arity_of o) . $1)]);

      consider a be FinSequence such that

       A77: ( len a) = ( len ( the_arity_of o)) & for k be Nat st k in ( dom a) holds (a . k) = F(k) from FINSEQ_1:sch 2;

      

       A78: ( dom a) = ( Seg ( len a)) by FINSEQ_1:def 3;

      

       A79: for i be Nat st i in ( dom a) holds ex t be Term of S, X st t = (a . i) & ( the_sort_of t) = (( the_arity_of o) . i)

      proof

        let i be Nat;

        assume

         A80: i in ( dom a);

        set s = (( the_arity_of o) . i);

        ( dom ( the_arity_of o)) = ( Seg ( len ( the_arity_of o))) by FINSEQ_1:def 3;

        then

        reconsider s as SortSymbol of S by A77, A78, A80, DTCONSTR: 2;

        set x = (cX . (( the_arity_of o) . i));

        reconsider x as Element of (X . s) by A70;

        reconsider t = ( root-tree [x, s]) as Term of S, X by MSATERM: 4;

        take t;

        thus t = (a . i) by A77, A80;

        thus thesis by MSATERM: 14;

      end;

      

       A81: ( dom a) = ( Seg ( len ( the_arity_of o))) by A77, FINSEQ_1:def 3;

      reconsider a as ArgumentSeq of ( Sym (o,X)) by A77, A79, MSATERM: 24;

      set C1 = ( [o, the carrier of S] -tree a);

      reconsider C1 as Term of S, X by MSATERM: 1;

      

       A82: for k be Nat st 1 <= k & k < n1 holds for x be Element of D holds ex y be Element of D st P[k, x, y]

      proof

        let k be Nat;

        assume that 1 <= k and

         A83: k < n1;

        

         A84: 1 <= (k + 1) by NAT_1: 11;

        (k + 1) <= n by A83, NAT_1: 13;

        then (k + 1) in ( dom c) by A67, A84, FINSEQ_3: 25;

        then

        reconsider ck1 = (c . (k + 1)) as Element of EG by A71, DTCONSTR: 2;

        let x be Element of D;

        consider o,rs1 be set such that

         A85: ck1 = [o, rs1] and

         A86: o in the carrier' of S and

         A87: rs1 in cS and ex n be Nat, args be Element of (the carrier of S * ) st (the Arity of S . o) = args & n in ( dom args) & (args . n) = rs1 by Def1;

        reconsider rs1 as SortSymbol of S by A87;

        reconsider o as OperSymbol of S by A86;

        set DA = ( dom ( the_arity_of o));

        set ar = ( the_arity_of o);

        defpred P[ object, object] means ((ar . $1) = rs1 & ( the_sort_of x) = rs1 implies $2 = x) & ((ar . $1) <> rs1 or ( the_sort_of x) <> rs1 implies $2 = ( root-tree [(cX . (ar . $1)), (ar . $1)]));

        

         A88: for e be object st e in DA holds ex u be object st u in D & P[e, u]

        proof

          let e be object;

          assume

           A89: e in DA;

          per cases ;

            suppose

             A90: (ar . e) = rs1 & ( the_sort_of x) = rs1;

            take x;

            thus thesis by A90;

          end;

            suppose

             A91: (ar . e) <> rs1 or ( the_sort_of x) <> rs1;

            reconsider s = (( the_arity_of o) . e) as SortSymbol of S by A89, DTCONSTR: 2;

            reconsider x = (cX . (( the_arity_of o) . e)) as Element of (X . s) by A70;

            reconsider t = ( root-tree [x, s]) as Term of S, X by MSATERM: 4;

            take t;

            thus thesis by A91;

          end;

        end;

        consider a be Function of DA, D such that

         A92: for e be object st e in DA holds P[e, (a . e)] from FUNCT_2:sch 1( A88);

        DA = ( Seg ( len ar)) by FINSEQ_1:def 3;

        then

        reconsider a as FinSequence of D by FINSEQ_2: 25;

        

         A93: ( dom a) = DA by FUNCT_2:def 1;

        now

          let i be Nat;

          assume

           A94: i in ( dom a);

          then

          reconsider t = (a . i) as Term of S, X by DTCONSTR: 2;

          take t;

          thus t = (a . i);

          per cases ;

            suppose (ar . i) = rs1 & ( the_sort_of x) = rs1;

            hence ( the_sort_of t) = (ar . i) by A92, A93, A94;

          end;

            suppose

             A95: (ar . i) <> rs1 or ( the_sort_of x) <> rs1;

            reconsider s = (( the_arity_of o) . i) as SortSymbol of S by A93, A94, DTCONSTR: 2;

            

             A96: (cX . (( the_arity_of o) . i)) is Element of (X . s) by A70;

            t = ( root-tree [(cX . (ar . i)), (ar . i)]) by A92, A93, A94, A95;

            hence ( the_sort_of t) = (ar . i) by A96, MSATERM: 14;

          end;

        end;

        then

        reconsider a as ArgumentSeq of ( Sym (o,X)) by A93, MSATERM: 24;

        reconsider y = ( [o, cS] -tree a) as Term of S, X by MSATERM: 1;

        take y, o, rs1, x, y, a;

        thus x = x & y = y;

        thus (c . (k + 1)) = [o, rs1] by A85;

        thus y = ( [o, cS] -tree a);

        let i be Nat;

        assume

         A97: i in ( dom a);

        then

        reconsider t = (a . i) as Term of S, X by DTCONSTR: 2;

        take t;

        thus t = (a . i);

        thus ( the_sort_of t) = (( the_arity_of o) . i) by A97, MSATERM: 23;

        hence thesis by A92, A93, A97;

      end;

      consider C be FinSequence of D such that

       A98: ( len C) = n1 & ((C . 1) = C1 or n1 = 0 ) & for k be Nat st 1 <= k & k < n1 holds P[k, (C . k), (C . (k + 1))] from RECDEF_1:sch 4( A82);

      defpred P[ Nat] means 1 <= $1 & $1 <= n implies ex C0 be Term of S, X, o be OperSymbol of S st C0 = (C . $1) & o = ((c . $1) `1 ) & ( the_sort_of C0) = ( the_result_sort_of o) & ( height ( dom C0)) = $1;

      

       A99: G is non void by A72;

      

       A100: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k;

        assume

         A101: 1 <= k & k <= n implies ex Ck be Term of S, X, o be OperSymbol of S st Ck = (C . k) & o = ((c . k) `1 ) & ( the_sort_of Ck) = ( the_result_sort_of o) & ( height ( dom Ck)) = k;

        assume that

         A102: 1 <= (k + 1) and

         A103: (k + 1) <= n;

        

         A104: k < n by A103, NAT_1: 13;

        

         A105: k <= (k + 1) by NAT_1: 11;

        then

         A106: k <= n by A103, XXREAL_0: 2;

        per cases ;

          suppose

           A107: k = 0 ;

          take C1, o;

          thus C1 = (C . (k + 1)) by A1, A98, A107;

          thus o = ((c . (k + 1)) `1 ) by A73, A107;

          reconsider w = ( doms a) as FinTree-yielding FinSequence;

          

           A108: ( dom ( doms a)) = ( dom a) by TREES_3: 37;

          (C1 . {} ) = [o, cS] by TREES_4:def 4;

          hence ( the_sort_of C1) = ( the_result_sort_of o) by MSATERM: 17;

          consider i be Nat, args be Element of (the carrier of S * ) such that

           A109: (the Arity of S . o) = args and

           A110: i in ( dom args) and (args . i) = rs1 by A76;

          

           A111: ( dom args) = ( Seg ( len args)) by FINSEQ_1:def 3;

          

           A112: args = ( the_arity_of o) by A109, MSUALG_1:def 1;

          then

          reconsider t = (a . i) as Term of S, X by A77, A78, A110, A111, MSATERM: 22;

          (( doms a) . i) = ( dom t) by A77, A78, A110, A112, A111, FUNCT_6: 22;

          then

           A113: ( dom C1) = ( tree ( doms a)) & ( dom t) in ( rng w) by A77, A78, A108, A110, A112, A111, FUNCT_1:def 3, TREES_4: 10;

          reconsider dt = ( dom t) as finite Tree;

          

           A114: (a . i) = ( root-tree [(cX . (( the_arity_of o) . i)), (( the_arity_of o) . i)]) by A77, A81, A110, A112, A111;

           A115:

          now

            let t9 be finite Tree;

            assume t9 in ( rng w);

            then

            consider j be Nat such that

             A116: j in ( dom w) and

             A117: (w . j) = t9 by FINSEQ_2: 10;

            reconsider t99 = (a . j) as Term of S, X by A108, A116, MSATERM: 22;

            (a . j) = ( root-tree [(cX . (( the_arity_of o) . j)), (( the_arity_of o) . j)]) by A77, A108, A116;

            then

             A118: ( dom t99) = ( elementary_tree 0 ) by TREES_4: 3;

            (w . j) = ( dom t99) by A108, A116, FUNCT_6: 22;

            hence ( height t9) <= ( height dt) by A114, A117, A118, TREES_4: 3;

          end;

          ( dom t) = ( elementary_tree 0 ) by A114, TREES_4: 3;

          hence thesis by A107, A113, A115, TREES_1: 42, TREES_3: 79;

        end;

          suppose

           A119: k <> 0 ;

          then

           A120: 1 <= k by NAT_1: 14;

          then k in ( dom c) by A67, A106, FINSEQ_3: 25;

          then

          reconsider ck = (c . k) as Element of EG by A71, DTCONSTR: 2;

          consider Ck be Term of S, X, o be 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 be OperSymbol of S, rs1 be SortSymbol of S, Ck9,Ck1 be Term of S, X, a be ArgumentSeq of ( Sym (o1,X)) such that

           A124: Ck9 = (C . k) and

           A125: (C . (kk + 1)) = Ck1 and

           A126: (c . (k + 1)) = [o1, rs1] and

           A127: Ck1 = ( [o1, cS] -tree a) and

           A128: for i be Nat st i in ( dom a) holds ex t be Term of S, X st t = (a . i) & ( the_sort_of t) = (( the_arity_of o1) . i) & (( the_sort_of t) = rs1 & ( the_sort_of Ck9) = rs1 implies t = Ck9) & (( the_sort_of t) <> rs1 or ( the_sort_of Ck9) <> rs1 implies t = ( root-tree [(cX . ( the_sort_of t)), ( the_sort_of t)])) by A98, A104, A119, NAT_1: 14;

          set ck1 = (c . (kk + 1));

          

           A129: (k + 1) in ( dom c) by A67, A102, A103, FINSEQ_3: 25;

          then ck1 in EG by A71, DTCONSTR: 2;

          then

          consider o9,rs19 be set such that

           A130: ck1 = [o9, rs19] and

           A131: o9 in the carrier' of S and rs19 in the carrier of S and

           A132: ex n be Nat, args be Element of (the carrier of S * ) st (the Arity of S . o9) = args & n in ( dom args) & (args . n) = rs19 by Def1;

          

           A133: o1 = o9 by A126, A130, XTUPLE_0: 1;

          take Ck1, o1;

          thus Ck1 = (C . (k + 1)) by A125;

          thus o1 = ((c . (k + 1)) `1 ) by A126;

          (Ck1 . {} ) = [o1, cS] by A127, TREES_4:def 4;

          hence ( the_sort_of Ck1) = ( the_result_sort_of o1) by MSATERM: 17;

          

           A134: ( dom Ck1) = ( tree ( doms a)) by A127, TREES_4: 10;

          reconsider ck1 as Element of EG by A71, A129, DTCONSTR: 2;

          reconsider w = ( doms a) as FinTree-yielding FinSequence;

          

           A135: ( len a) = ( len ( the_arity_of o1)) & ( dom a) = ( Seg ( len a)) by FINSEQ_1:def 3, MSATERM: 22;

          rs1 = rs19 by A126, A130, XTUPLE_0: 1;

          then

          consider i be Nat, args be Element of (the carrier of S * ) such that

           A136: (the Arity of S . o9) = args and

           A137: i in ( dom args) and

           A138: (args . i) = rs1 by A132;

          reconsider o9 as OperSymbol of S by A131;

          

           A139: ( dom args) = ( Seg ( len args)) by FINSEQ_1:def 3;

          

           A140: args = ( the_arity_of o9) by A136, MSUALG_1:def 1;

          then

          consider t be Term of S, X such that

           A141: t = (a . i) and

           A142: ( the_sort_of t) = (( the_arity_of o1) . i) & (( the_sort_of t) = rs1 & ( the_sort_of Ck9) = rs1 implies t = Ck9) and ( the_sort_of t) <> rs1 or ( the_sort_of Ck9) <> rs1 implies t = ( root-tree [(cX . ( the_sort_of t)), ( the_sort_of t)]) by A128, A135, A133, A137, A139;

          reconsider dt = ( dom t) as finite Tree;

          

           A143: ( dom ( doms a)) = ( dom a) by TREES_3: 37;

           A144:

          now

            let t9 be finite Tree;

            assume t9 in ( rng w);

            then

            consider j be Nat such that

             A145: j in ( dom w) and

             A146: (w . j) = t9 by FINSEQ_2: 10;

            consider t99 be Term of S, X such that

             A147: t99 = (a . j) and ( the_sort_of t99) = (( the_arity_of o1) . j) and

             A148: ( the_sort_of t99) = rs1 & ( the_sort_of Ck9) = rs1 implies t99 = Ck9 and

             A149: ( the_sort_of t99) <> rs1 or ( the_sort_of Ck9) <> rs1 implies t99 = ( root-tree [(cX . ( the_sort_of t99)), ( the_sort_of t99)]) by A128, A143, A145;

            

             A150: (w . j) = ( dom t99) by A143, A145, A147, FUNCT_6: 22;

            per cases ;

              suppose ( the_sort_of t99) = rs1 & ( the_sort_of Ck9) = rs1;

              hence ( height t9) <= ( height dt) by A143, A133, A136, A138, A142, A145, A146, A147, A148, FUNCT_6: 22, MSUALG_1:def 1;

            end;

              suppose ( the_sort_of t99) <> rs1 or ( the_sort_of Ck9) <> rs1;

              hence ( height t9) <= ( height dt) by A146, A149, A150, TREES_1: 42, TREES_4: 3;

            end;

          end;

          (( doms a) . i) = ( dom t) by A135, A133, A137, A140, A139, A141, FUNCT_6: 22;

          then

           A151: ( dom t) in ( rng w) by A143, A135, A133, A137, A140, A139, FUNCT_1:def 3;

          ( the_sort_of Ck) = (the ResultSort of S . (ck `1 )) by A122, MSUALG_1:def 2

          .= (TG . ck) by Def3

          .= (( vertex-seq c) . (kk + 1)) by A67, A99, A106, A120, CARD_1: 27, MSSCYC_1: 11

          .= (SG . ck1) by A67, A99, A102, A103, CARD_1: 27, MSSCYC_1: 11

          .= (ck1 `2 ) by Def2

          .= rs1 by A126;

          hence thesis by A121, A123, A124, A134, A133, A136, A138, A142, A151, A144, MSUALG_1:def 1, TREES_3: 79;

        end;

      end;

      set cn = (c . ( len c));

      n in ( dom c) by A1, A67, CARD_1: 27, FINSEQ_5: 6;

      then

       A152: cn in ( InducedEdges S) by A67, A71, DTCONSTR: 2;

      

       A153: P[ 0 ];

      for k holds P[k] from NAT_1:sch 2( A153, A100);

      then

      consider Cn be Term of S, X, o be OperSymbol of S such that Cn = (C . n) and

       A154: o = ((c . n) `1 ) and

       A155: ( the_sort_of Cn) = ( the_result_sort_of o) and

       A156: ( height ( dom Cn)) = n by A1;

      G is non void by A72;

      

      then (( vertex-seq c) . (( len c) + 1)) = (the Target of G . (c . ( len c))) by A1, A67, CARD_1: 27, MSSCYC_1: 14

      .= (the ResultSort of S . (cn `1 )) by A152, Def3

      .= ( the_result_sort_of o) by A67, A154, MSUALG_1:def 2;

      then

      reconsider Cn as Element of (the Sorts of ( FreeMSA X) . v) by A2, A68, A155, MSATERM:def 5;

      take Cn;

      thus thesis by A156, MSAFREE2:def 14;

    end;

    theorem :: MSSCYC_2:3

    for S be void non empty ManySortedSign holds S is monotonic iff ( InducedGraph S) is well-founded

    proof

      let S be void non empty ManySortedSign;

      set G = ( InducedGraph S), OS = the carrier' of S, CA = the carrier of S, AR = the Arity of S;

      hereby

        assume S is monotonic;

        assume not G is well-founded;

        then

        consider v be Element of the carrier of G such that

         A1: for n be Nat holds ex c be directed Chain of G st c is non empty & (( vertex-seq c) . (( len c) + 1)) = v & ( len c) > n by MSSCYC_1:def 4;

        consider e be directed Chain of G such that

         A2: e is non empty and (( vertex-seq e) . (( len e) + 1)) = v and ( len e) > 0 by A1;

        e is FinSequence of the carrier' of G by MSSCYC_1:def 1;

        then

         A3: ( rng e) c= the carrier' of G by FINSEQ_1:def 4;

        1 in ( dom e) by A2, FINSEQ_5: 6;

        then (e . 1) in ( rng e) by FUNCT_1:def 3;

        then ex op,v be set st (e . 1) = [op, v] & op in OS & v in CA & ex n be Nat, args be Element of (CA * ) st (AR . op) = args & n in ( dom args) & (args . n) = v by A3, Def1;

        hence contradiction;

      end;

      assume G is well-founded;

      let A be finitely-generated non-empty MSAlgebra over S;

      thus the Sorts of A is finite-yielding by MSAFREE2:def 10;

    end;

    theorem :: MSSCYC_2:4

    for S be non void non empty ManySortedSign st S is monotonic holds ( InducedGraph S) is well-founded

    proof

      let S be non void non empty ManySortedSign;

      set G = ( InducedGraph S);

      assume S is monotonic;

      then

      reconsider S as monotonic non void non empty ManySortedSign;

      set A = the finite-yielding non-empty MSAlgebra over S;

      assume G is non well-founded;

      then

      consider v be Element of the carrier of G such that

       A1: for n be Nat holds ex c be directed Chain of G st c is non empty & (( vertex-seq c) . (( len c) + 1)) = v & ( len c) > n by MSSCYC_1:def 4;

      reconsider v as SortSymbol of S;

      consider s be finite non empty Subset of NAT such that

       A2: s = the set of all ( depth t) where t be Element of (the Sorts of ( FreeEnv A) . v) and ( depth (v,A)) = ( max s) by CIRCUIT1:def 6;

      ( max s) is Nat by TARSKI: 1;

      then

      consider c be directed Chain of G such that c is non empty and

       A3: (( vertex-seq c) . (( len c) + 1)) = v and

       A4: ( len c) > ( max s) by A1;

      1 <= ( len c) by A4, NAT_1: 14;

      then

      consider t be Element of (the Sorts of ( FreeMSA the Sorts of A) . v) such that

       A5: ( depth t) = ( len c) by A3, Th2;

      reconsider t9 = t as Element of (the Sorts of ( FreeEnv A) . v);

      (ex t99 be Element of (the Sorts of ( FreeMSA the Sorts of A) . v) st t9 = t99 & ( depth t9) = ( depth t99)) & ( depth t9) in s by A2, CIRCUIT1:def 5;

      hence contradiction by A4, A5, XXREAL_2:def 8;

    end;

    theorem :: MSSCYC_2:5

    

     Th5: for S be non void non empty ManySortedSign, X be non-empty finite-yielding ManySortedSet of the carrier of S st S is finitely_operated holds for n be Nat, v be SortSymbol of S holds { t where t be Element of (the Sorts of ( FreeMSA X) . v) : ( depth t) <= n } is finite

    proof

      let S be non void non empty ManySortedSign, X be non-empty finite-yielding ManySortedSet of the carrier of S such that

       A1: S is finitely_operated;

      set SF = the Sorts of ( FreeMSA X);

      defpred P[ Nat] means for v be SortSymbol of S holds { t where t be Element of (SF . v) : ( depth t) <= $1 } is finite;

      

       A2: ( FreeMSA X) = MSAlgebra (# ( FreeSort X), ( FreeOper X) #) by MSAFREE:def 14;

      

       A3: for k be Nat st P[k] holds P[(k + 1)]

      proof

        deffunc F( set) = $1;

        let n be Nat;

        assume

         A4: for v be SortSymbol of S holds { t where t be Element of (SF . v) : ( depth t) <= n } is finite;

        let v be SortSymbol of S;

        defpred QZ[ Element of (SF . v)] means ( depth $1) = (n + 1);

        defpred P[ Element of (SF . v)] means ( depth $1) <= (n + 1);

        defpred Q[ Element of (SF . v)] means ( depth $1) <= n or ( depth $1) = (n + 1);

        set dn1 = { F(t) where t be Element of (SF . v) : P[t] };

        set dn11 = { F(t) where t be Element of (SF . v) : Q[t] };

        set den1 = { t where t be Element of (SF . v) : QZ[t] };

        set ov = { o where o be OperSymbol of S : ( the_result_sort_of o) = v };

        

         A5: (SF . v) = ( FreeSort (X,v)) by A2, MSAFREE:def 11;

        ov is finite by A1, MSSCYC_1:def 5;

        then

        consider ovs be FinSequence such that

         A6: ( rng ovs) = ov by FINSEQ_1: 52;

        deffunc F( set) = { t where t be Element of (SF . v) : ( depth t) = (n + 1) & (t . {} ) = [(ovs . $1), the carrier of S] };

        consider dvs be FinSequence such that

         A7: ( len dvs) = ( len ovs) & for k be Nat st k in ( dom dvs) holds (dvs . k) = F(k) from FINSEQ_1:sch 2;

        

         A8: ( dom ovs) = ( Seg ( len ovs)) & ( dom dvs) = ( Seg ( len dvs)) by FINSEQ_1:def 3;

        

         A9: ( FreeSort (X,v)) c= (S -Terms X) by MSATERM: 12;

        

         A10: den1 c= ( Union dvs)

        proof

          let x be object;

          assume x in den1;

          then

          consider t be Element of (SF . v) such that

           A11: x = t and

           A12: ( depth t) = (n + 1);

          t in ( FreeSort (X,v)) by A5;

          then

          reconsider t9 = t as Term of S, X by A9;

          now

            

             A13: ex dt be finite DecoratedTree, tt be finite Tree st dt = t & tt = ( dom dt) & ( depth t) = ( height tt) by MSAFREE2:def 14;

            assume t9 is root;

            hence contradiction by A12, A13, TREES_1: 42, TREES_9:def 1;

          end;

          then

          consider o be 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 be object such that

           A15: k in ( dom ovs) and

           A16: o = (ovs . k) by FUNCT_1:def 3;

          (dvs . k) = { t1 where t1 be Element of (SF . v) : ( depth t1) = (n + 1) & (t1 . {} ) = [(ovs . k), the carrier of S] } by A7, A8, A15;

          then

           A17: t in (dvs . k) by A12, A14, A16;

          (dvs . k) in ( rng dvs) by A7, A8, A15, FUNCT_1:def 3;

          then t in ( union ( rng dvs)) by A17, TARSKI:def 4;

          hence thesis by A11, CARD_3:def 4;

        end;

        for k be object st k in ( dom dvs) holds (dvs . k) is finite

        proof

          let k be object;

          set dvsk = { t where t be Element of (SF . v) : ( depth t) = (n + 1) & (t . {} ) = [(ovs . k), the carrier of S] };

          assume

           A18: k in ( dom dvs);

          then (ovs . k) in ( rng ovs) by A7, A8, FUNCT_1:def 3;

          then

          consider o be 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 be Element of ((S -Terms X) * ) : a is ArgumentSeq of ( Sym (o,X)) & ex t be Element of (SF . v) st ( depth t) = (n + 1) & t = ( [o, the carrier of S] -tree a) };

          

           A20: dvsk c= davsk

          proof

            let x be object;

            assume x in dvsk;

            then

            consider t be Element of (SF . v) such that

             A21: x = t and

             A22: ( depth t) = (n + 1) and

             A23: (t . {} ) = [o, the carrier of S] by A19;

            t in ( FreeSort (X,v)) by A5;

            then

            reconsider t9 = t as Term of S, X by A9;

            consider a be ArgumentSeq of ( Sym (o,X)) such that

             A24: t9 = ( [o, the carrier of S] -tree a) by A23, MSATERM: 10;

            reconsider a9 = a as Element of ((S -Terms X) * ) by FINSEQ_1:def 11;

            ( [o, the carrier of S] -tree a9) in davsk by A22, A24;

            hence thesis by A21, A24;

          end;

          deffunc F( Nat) = { t where t be Element of (SF . (( the_arity_of o) /. $1)) : ( depth t) <= n };

          set avsk = { a where a be Element of ((S -Terms X) * ) : a is ArgumentSeq of ( Sym (o,X)) & ex t be Element of (SF . v) st ( depth t) = (n + 1) & t = ( [o, the carrier of S] -tree a) };

          

           A25: (avsk,davsk) are_equipotent

          proof

            set Z = { [a, ( [o, the carrier of S] -tree a)] where a be Element of ((S -Terms X) * ) : a is ArgumentSeq of ( Sym (o,X)) & ex t be Element of (SF . v) st ( depth t) = (n + 1) & t = ( [o, the carrier of S] -tree a) };

            take Z;

            hereby

              let x be object;

              assume x in avsk;

              then

              consider a be Element of ((S -Terms X) * ) such that

               A26: x = a and

               A27: a is ArgumentSeq of ( Sym (o,X)) & ex t be Element of (SF . v) st ( depth t) = (n + 1) & t = ( [o, the carrier of S] -tree a);

              reconsider y9 = ( [o, the carrier of S] -tree a) as object;

              take y9;

              thus y9 in davsk by A27;

              thus [x, y9] in Z by A26, A27;

            end;

            hereby

              let y be object;

              assume y in davsk;

              then

              consider a be 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 be Element of (SF . v) st ( depth t) = (n + 1) & t = ( [o, the carrier of S] -tree a);

              reconsider a9 = a as object;

              take a9;

              thus a9 in avsk by A29;

              thus [a9, y] in Z by A28, A29;

            end;

            let x,y,z,u be object;

            assume [x, y] in Z;

            then

            consider xa be 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 be Element of (SF . v) st ( depth t) = (n + 1) & t = ( [o, the carrier of S] -tree xa);

            

             A32: x = xa by A30, XTUPLE_0: 1;

            assume [z, u] in Z;

            then

            consider za be 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 be Element of (SF . v) st ( depth t) = (n + 1) & t = ( [o, the carrier of S] -tree za);

            

             A35: z = za by A33, XTUPLE_0: 1;

            hence x = z implies y = u by A30, A33, A32, XTUPLE_0: 1;

            

             A36: u = ( [o, the carrier of S] -tree za) by A33, XTUPLE_0: 1;

            

             A37: y = ( [o, the carrier of S] -tree xa) by A30, XTUPLE_0: 1;

            assume y = u;

            hence thesis by A31, A34, A32, A37, A35, A36, TREES_4: 15;

          end;

          consider nS be FinSequence such that

           A38: ( len nS) = ( len ( the_arity_of o)) & for k be Nat st k in ( dom nS) holds (nS . k) = F(k) from FINSEQ_1:sch 2;

          

           A39: ( dom nS) = ( Seg ( len nS)) by FINSEQ_1:def 3;

          

           A40: ( dom nS) = ( Seg ( len ( the_arity_of o))) by A38, FINSEQ_1:def 3;

          

           A41: avsk c= ( product nS)

          proof

            let x be object;

            assume x in avsk;

            then

            consider a be Element of ((S -Terms X) * ) such that

             A42: x = a and

             A43: a is ArgumentSeq of ( Sym (o,X)) and

             A44: ex t be Element of (SF . v) st ( depth t) = (n + 1) & t = ( [o, the carrier of S] -tree a);

            reconsider a as ArgumentSeq of ( Sym (o,X)) by A43;

            

             A45: ( len a) = ( len ( the_arity_of o)) & ( dom a) = ( Seg ( len a)) by FINSEQ_1:def 3, MSATERM: 22;

            now

              let x be object;

              assume

               A46: x in ( dom a);

              then

              reconsider k = x as Element of NAT ;

              reconsider ak = (a . k) as Term of S, X by A46, MSATERM: 22;

              

               A47: ( the_sort_of ak) = (( the_arity_of o) /. k) by A46, MSATERM: 23;

              (SF . ( the_sort_of ak)) = ( FreeSort (X,( the_sort_of ak))) by A2, MSAFREE:def 11;

              then

              reconsider ak as Element of (SF . (( the_arity_of o) /. k)) by A47, MSATERM:def 5;

              ( depth ak) < (n + 1) by A44, A46, MSSCYC_1: 27;

              then

               A48: ( depth ak) <= n by NAT_1: 13;

              set nSk = { tk where tk be Element of (SF . (( the_arity_of o) /. k)) : ( depth tk) <= n };

              nSk = (nS . x) by A38, A40, A45, A46;

              hence (a . x) in (nS . x) by A48;

            end;

            hence thesis by A38, A39, A42, A45, CARD_3:def 5;

          end;

          now

            let x be object;

            assume

             A49: x in ( dom nS);

            then

            reconsider k = x as Nat;

            set nSk = { t where t be Element of (SF . (( the_arity_of o) /. k)) : ( depth t) <= n };

            (nS . k) = nSk by A38, A49;

            hence (nS . x) is finite by A4;

          end;

          then nS is finite-yielding by FINSET_1:def 4;

          then ( product nS) is finite;

          then davsk is finite by A25, A41, CARD_1: 38;

          hence thesis by A7, A18, A20;

        end;

        then

         A50: ( Union dvs) is finite by CARD_2: 88;

        defpred Z[ Element of (SF . v)] means ( depth $1) <= n;

        set dln = { t where t be Element of (SF . v) : Z[t] };

        

         A51: { t where t be Element of (SF . v) : Z[t] or QZ[t] } = (dln \/ den1) from TOPREAL1:sch 1;

        

         A52: for t be Element of (SF . v) holds P[t] iff Q[t] by NAT_1: 8, NAT_1: 12;

        

         A53: dn1 = dn11 from FRAENKEL:sch 3( A52);

        dln is finite by A4;

        hence thesis by A53, A51, A50, A10;

      end;

      

       A54: P[ 0 ]

      proof

        let v be SortSymbol of S;

        set dle0 = { t where t be Element of (SF . v) : ( depth t) <= 0 };

        set d0 = { t where t be Element of (SF . v) : ( depth t) = 0 };

        

         A55: dle0 c= d0

        proof

          let x be object;

          assume x in dle0;

          then

          consider t be Element of (SF . v) such that

           A56: x = t and

           A57: ( depth t) <= 0 ;

          ( depth t) = 0 by A57;

          hence thesis by A56;

        end;

        ( Constants (( FreeMSA X),v)) is finite & d0 = (( FreeGen (v,X)) \/ ( Constants (( FreeMSA X),v))) by A1, MSSCYC_1: 25, MSSCYC_1: 26;

        hence thesis by A55;

      end;

      thus for n be Nat holds P[n] from NAT_1:sch 2( A54, A3);

    end;

    theorem :: MSSCYC_2:6

    for S be non void non empty ManySortedSign st S is finitely_operated & ( InducedGraph S) is well-founded holds S is monotonic

    proof

      let S be non void non empty ManySortedSign;

      set G = ( InducedGraph S);

      assume that

       A1: S is finitely_operated and

       A2: G is well-founded;

      given A be finitely-generated non-empty MSAlgebra over S such that

       A3: A is non finite-yielding;

      set GS = the non-empty finite-yielding GeneratorSet of A;

      reconsider gs = GS as non-empty finite-yielding ManySortedSet of the carrier of S;

      ( FreeMSA gs) is non finite-yielding by A3, MSSCYC_1: 23;

      then the Sorts of ( FreeMSA gs) is non finite-yielding;

      then

      consider v be object such that

       A4: v in the carrier of S and

       A5: (the Sorts of ( FreeMSA gs) . v) is non finite by FINSET_1:def 5;

      reconsider v as SortSymbol of S by A4;

      consider n be Nat such that

       A6: for c be directed Chain of G st c is non empty & (( vertex-seq c) . (( len c) + 1)) = v holds ( len c) <= n by A2, MSSCYC_1:def 4;

      set V = (the Sorts of ( FreeMSA gs) . v);

      set Vn = { t where t be Element of V : ( depth t) <= n };

      Vn is finite by A1, Th5;

      then not V c= Vn by A5;

      then

      consider t be object such that

       A7: t in V and

       A8: not t in Vn;

      reconsider t as Element of V by A7;

      

       A9: not ( depth t) <= n by A8;

      then 1 <= ( depth t) by NAT_1: 14;

      then ex d be directed Chain of ( InducedGraph S) st ( len d) = ( depth t) & (( vertex-seq d) . (( len d) + 1)) = v by Th2;

      hence contradiction by A6, A9, CARD_1: 27;

    end;