msscyc_1.miz



    begin

    reserve G for Graph,

k,m,n for Nat;

    definition

      let G be Graph;

      :: original: Chain

      redefine

      :: MSSCYC_1:def1

      mode Chain of G means

      : Def1: it is FinSequence of the carrier' of G & ex p be FinSequence of the carrier of G st p is_vertex_seq_of it ;

      compatibility

      proof

        let c be FinSequence;

        hereby

          assume

           A1: c is Chain of G;

          then

          consider p be FinSequence such that

           A2: ( len p) = (( len c) + 1) and

           A3: for n st 1 <= n & n <= ( len p) holds (p . n) in the carrier of G and

           A4: for n st 1 <= n & n <= ( len c) holds ex x9,y9 be Element of the carrier of G st x9 = (p . n) & y9 = (p . (n + 1)) & (c . n) joins (x9,y9) by GRAPH_1:def 14;

          thus c is FinSequence of the carrier' of G by A1;

          now

            let i be Nat;

            assume i in ( dom p);

            then

             A5: 1 <= i & i <= ( len p) by FINSEQ_3: 25;

            thus (p . i) in the carrier of G by A3, A5;

          end;

          then

          reconsider p as FinSequence of the carrier of G by FINSEQ_2: 12;

          take p;

          thus p is_vertex_seq_of c

          proof

            thus ( len p) = (( len c) + 1) by A2;

            let n;

            assume that

             A6: 1 <= n and

             A7: n <= ( len c);

            (n + 1) <= ( len p) by A2, A7, XREAL_1: 6;

            then

             A8: (p /. (n + 1)) = (p . (n + 1)) by FINSEQ_4: 15, NAT_1: 12;

            n <= ( len p) & ex x9,y9 be Element of the carrier of G st x9 = (p . n) & y9 = (p . (n + 1)) & (c . n) joins (x9,y9) by A2, A4, A6, A7, NAT_1: 12;

            hence thesis by A6, A8, FINSEQ_4: 15;

          end;

        end;

        assume

         A9: c is FinSequence of the carrier' of G;

        given p be FinSequence of the carrier of G such that

         A10: p is_vertex_seq_of c;

        hereby

          let n;

          assume 1 <= n & n <= ( len c);

          then n in ( dom c) by FINSEQ_3: 25;

          then

           A11: (c . n) in ( rng c) by FUNCT_1:def 3;

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

          hence (c . n) in the carrier' of G by A11;

        end;

        take p;

        thus

         A12: ( len p) = (( len c) + 1) by A10;

        hereby

          let n;

          assume 1 <= n & n <= ( len p);

          then n in ( dom p) by FINSEQ_3: 25;

          then

           A13: (p . n) in ( rng p) by FUNCT_1:def 3;

          ( rng p) c= the carrier of G by FINSEQ_1:def 4;

          hence (p . n) in the carrier of G by A13;

        end;

        let n;

        assume that

         A14: 1 <= n and

         A15: n <= ( len c);

        take x9 = (p /. n), y9 = (p /. (n + 1));

        n <= ( len p) & (n + 1) <= ( len p) by A12, A15, NAT_1: 12, XREAL_1: 6;

        hence x9 = (p . n) & y9 = (p . (n + 1)) by A14, FINSEQ_4: 15, NAT_1: 12;

        thus thesis by A10, A14, A15;

      end;

    end

    ::$Canceled

    theorem :: MSSCYC_1:2

    for p,q be FinSequence st n <= ( len p) holds ((1,n) -cut p) = ((1,n) -cut (p ^ q))

    proof

      let p,q be FinSequence;

      assume

       A1: n <= ( len p);

      per cases ;

        suppose

         A2: n < 1;

        then ((1,n) -cut p) = {} by FINSEQ_6:def 4;

        hence thesis by A2, FINSEQ_6:def 4;

      end;

        suppose

         A3: 1 <= n;

        set cp = ((1,n) -cut p), cpq = ((1,n) -cut (p ^ q));

        now

          

           A4: (( len cp) + 1) = (n + 1) by A1, A3, FINSEQ_6:def 4;

          ( len (p ^ q)) = (( len p) + ( len q)) by FINSEQ_1: 22;

          then

           A5: n <= ( len (p ^ q)) by A1, NAT_1: 12;

          then

           A6: (( len cpq) + 1) = (n + 1) by A3, FINSEQ_6:def 4;

          hence ( len cp) = ( len cpq) by A4;

          let k be Nat;

          assume that

           A7: 1 <= k and

           A8: k <= ( len cp);

          k <= ( len p) by A1, A4, A8, XXREAL_0: 2;

          then

           A9: k in ( dom p) by A7, FINSEQ_3: 25;

          ( 0 + 1) = 1;

          then

           A10: ex i be Nat st 0 <= i & i < ( len cp) & k = (i + 1) by A7, A8, FINSEQ_6: 127;

          

          hence (cp . k) = (p . k) by A1, A3, FINSEQ_6:def 4

          .= ((p ^ q) . k) by A9, FINSEQ_1:def 7

          .= (cpq . k) by A3, A5, A4, A6, A10, FINSEQ_6:def 4;

        end;

        hence thesis by FINSEQ_1: 14;

      end;

    end;

    notation

      let G be Graph;

      let IT be Chain of G;

      synonym IT is directed for IT is oriented;

    end

    definition

      let G be Graph;

      let IT be Chain of G;

      :: MSSCYC_1:def2

      attr IT is cyclic means ex p be FinSequence of the carrier of G st p is_vertex_seq_of IT & (p . 1) = (p . ( len p));

    end

    registration

      cluster void for Graph;

      existence

      proof

        set V = {1}, E = {} ;

        set S = the Function of E, V;

        reconsider G = MultiGraphStruct (# V, E, S, S #) as Graph;

        take G;

        thus the carrier' of G is empty;

      end;

    end

    theorem :: MSSCYC_1:3

    

     Th2: for G be Graph holds (( rng the Source of G) \/ ( rng the Target of G)) c= the carrier of G

    proof

      let G be Graph;

      ( rng the Source of G) c= the carrier of G & ( rng the Target of G) c= the carrier of G by RELAT_1:def 19;

      hence thesis by XBOOLE_1: 8;

    end;

    registration

      cluster finite simple connected non void strict for Graph;

      existence

      proof

        set V = {1, 2}, E = {1};

        1 in V & 2 in V by TARSKI:def 2;

        then

        reconsider S = (E --> 1), T = (E --> 2) as Function of E, V by FUNCOP_1: 45;

        reconsider G = MultiGraphStruct (# V, E, S, T #) as Graph;

        take G;

        thus G is finite;

        

         A1: 1 in E by TARSKI:def 1;

        then

         A2: (S . 1) = 1 by FUNCOP_1: 7;

        thus G is simple

        proof

          given x be set such that

           A3: x in the carrier' of G and

           A4: (the Source of G . x) = (the Target of G . x);

          x = 1 by A3, TARSKI:def 1;

          hence contradiction by A1, A2, A4, FUNCOP_1: 7;

        end;

        

         A5: (T . 1) = 2 by A1, FUNCOP_1: 7;

        thus G is connected

        proof

          set MSG = the MultiGraphStruct of G;

          given G1,G2 be Graph such that

           A6: the carrier of G1 misses the carrier of G2 and

           A7: G is_sum_of (G1,G2);

          

           A8: the MultiGraphStruct of G = (G1 \/ G2) by A7;

          set V1 = the carrier of G1, V2 = the carrier of G2;

          set T1 = the Target of G1, T2 = the Target of G2;

          set S1 = the Source of G1, S2 = the Source of G2;

          set E1 = the carrier' of G1, E2 = the carrier' of G2;

          

           A9: (( rng S1) \/ ( rng T1)) c= V1 by Th2;

          

           A10: (( rng S2) \/ ( rng T2)) c= V2 by Th2;

          

           A11: the Target of G1 tolerates the Target of G2 & the Source of G1 tolerates the Source of G2 by A7;

          then

           A12: the carrier of MSG = (the carrier of G1 \/ the carrier of G2) by A8, GRAPH_1:def 5;

          

           A13: the carrier' of MSG = (the carrier' of G1 \/ the carrier' of G2) by A11, A8, GRAPH_1:def 5;

          per cases by A13, ZFMISC_1: 37;

            suppose

             A14: E1 = E & E2 = E;

            then (S2 . 1) = (S . 1) by A1, A11, A8, GRAPH_1:def 5;

            then 1 in ( rng S2) by A1, A2, A14, FUNCT_2: 4;

            then

             A15: 1 in (( rng S2) \/ ( rng T2)) by XBOOLE_0:def 3;

            (S1 . 1) = (S . 1) by A1, A11, A8, A14, GRAPH_1:def 5;

            then 1 in ( rng S1) by A1, A2, A14, FUNCT_2: 4;

            then 1 in (( rng S1) \/ ( rng T1)) by XBOOLE_0:def 3;

            hence contradiction by A6, A9, A10, A15, XBOOLE_0: 3;

          end;

            suppose

             A16: E1 = E & E2 = {} ;

            then (T1 . 1) = (T . 1) by A1, A11, A8, GRAPH_1:def 5;

            then 2 in ( rng T1) by A1, A5, A16, FUNCT_2: 4;

            then

             A17: 2 in (( rng S1) \/ ( rng T1)) by XBOOLE_0:def 3;

            

             A18: V1 c= V by A12, XBOOLE_1: 7;

            (S1 . 1) = (S . 1) by A1, A11, A8, A16, GRAPH_1:def 5;

            then 1 in ( rng S1) by A1, A2, A16, FUNCT_2: 4;

            then 1 in (( rng S1) \/ ( rng T1)) by XBOOLE_0:def 3;

            then V c= V1 by A9, A17, ZFMISC_1: 32;

            then V = V1 by A18, XBOOLE_0:def 10;

            then V2 c= V1 by A12, XBOOLE_1: 7;

            hence contradiction by A6, XBOOLE_1: 67;

          end;

            suppose

             A19: E1 = {} & E2 = E;

            then (T2 . 1) = (T . 1) by A1, A11, A8, GRAPH_1:def 5;

            then 2 in ( rng T2) by A1, A5, A19, FUNCT_2: 4;

            then

             A20: 2 in (( rng S2) \/ ( rng T2)) by XBOOLE_0:def 3;

            

             A21: V2 c= V by A12, XBOOLE_1: 7;

            (S2 . 1) = (S . 1) by A1, A11, A8, A19, GRAPH_1:def 5;

            then 1 in ( rng S2) by A1, A2, A19, FUNCT_2: 4;

            then 1 in (( rng S2) \/ ( rng T2)) by XBOOLE_0:def 3;

            then V c= V2 by A10, A20, ZFMISC_1: 32;

            then V = V2 by A21, XBOOLE_0:def 10;

            then V1 c= V2 by A12, XBOOLE_1: 7;

            hence contradiction by A6, XBOOLE_1: 67;

          end;

        end;

        thus G is non void;

        thus thesis;

      end;

    end

    theorem :: MSSCYC_1:4

    

     Th3: for e be set holds for s,t be Element of the carrier of G st s = (the Source of G . e) & t = (the Target of G . e) holds <*s, t*> is_vertex_seq_of <*e*>

    proof

      let e be set;

      let s,t be Element of the carrier of G;

      assume

       A1: s = (the Source of G . e) & t = (the Target of G . e);

      set c = <*e*>;

      set vs = <*s, t*>;

      

       A2: (vs /. (1 + 1)) = t by FINSEQ_4: 17;

      

       A3: ( len c) = 1 by FINSEQ_1: 39;

      hence ( len vs) = (( len c) + 1) by FINSEQ_1: 44;

      let n be Nat;

      assume 1 <= n & n <= ( len c);

      then

       A4: n = 1 by A3, XXREAL_0: 1;

      (c . 1) = e & (vs /. 1) = s by FINSEQ_1: 40, FINSEQ_4: 17;

      hence thesis by A1, A4, A2;

    end;

    theorem :: MSSCYC_1:5

    

     Th4: for e be set st e in the carrier' of G holds <*e*> is directed Chain of G

    proof

      let e be set;

      assume

       A1: e in the carrier' of G;

      then

      reconsider s = (the Source of G . e), t = (the Target of G . e) as Element of the carrier of G by FUNCT_2: 5;

      reconsider E = the carrier' of G as non empty set by A1;

      reconsider e as Element of E by A1;

       <*s, t*> is_vertex_seq_of <*e*> by Th3;

      then

      reconsider c = <*e*> as Chain of G by Def1;

      c is directed by FINSEQ_1: 39;

      hence thesis;

    end;

    reserve G for non void Graph;

    registration

      let G;

      cluster directed non empty one-to-one for Chain of G;

      existence

      proof

        set e = the Element of the carrier' of G;

        reconsider c = <*e*> as directed Chain of G by Th4;

        take c;

        thus c is directed;

        thus c is non empty;

        let n,m be Nat;

        assume that

         A1: 1 <= n & n < m and

         A2: m <= ( len c);

        1 < m by A1, XXREAL_0: 2;

        hence thesis by A2, FINSEQ_1: 39;

      end;

    end

    

     Lm1: for G be non empty Graph, c be Chain of G, p be FinSequence of the carrier of G st c is cyclic & p is_vertex_seq_of c holds (p . 1) = (p . ( len p))

    proof

      let G be non empty Graph;

      let c be Chain of G, p be FinSequence of the carrier of G;

      assume that

       A1: c is cyclic and

       A2: p is_vertex_seq_of c;

      consider P be FinSequence of the carrier of G such that

       A3: P is_vertex_seq_of c and

       A4: (P . 1) = (P . ( len P)) by A1;

      per cases ;

        suppose ( card the carrier of G) = 1 or c <> {} & not c alternates_vertices_in G;

        then P = ( vertex-seq c) & p = ( vertex-seq c) by A2, A3, GRAPH_2:def 8;

        hence thesis by A4;

      end;

        suppose

         A5: not (( card the carrier of G) = 1 or c <> {} & not c alternates_vertices_in G);

        

         A6: ( len p) = (( len c) + 1) by A2;

        

         A7: ( len P) = (( len c) + 1) by A3;

        now

          per cases by A5;

            suppose ( card the carrier of G) <> 1 & c = {} ;

            then ( len c) = 0 ;

            hence thesis by A6;

          end;

            suppose

             A8: ( card the carrier of G) <> 1 & c alternates_vertices_in G;

            then

             A9: p is TwoValued Alternating & P is TwoValued Alternating by A2, A3, GRAPH_2: 37;

            now

              set S = the Source of G, T = the Target of G;

              assume p <> P;

              

               A10: ( rng p) = {(S . (c . 1)), (T . (c . 1))} by A2, A8, GRAPH_2: 36;

              

               A11: 1 <= ( len p) by A6, NAT_1: 11;

              then ( len p) in ( dom p) by FINSEQ_3: 25;

              then (p . ( len p)) in ( rng p) by FUNCT_1:def 3;

              then

               A12: (p . ( len p)) = (S . (c . 1)) or (p . ( len p)) = (T . (c . 1)) by A10, TARSKI:def 2;

              

               A13: ( rng P) = {(S . (c . 1)), (T . (c . 1))} by A3, A8, GRAPH_2: 36;

              1 in ( dom P) by A6, A7, A11, FINSEQ_3: 25;

              then (P . 1) in ( rng p) by A10, A13, FUNCT_1:def 3;

              then

               A14: (P . 1) = (S . (c . 1)) or (P . 1) = (T . (c . 1)) by A10, TARSKI:def 2;

              1 in ( dom p) by A11, FINSEQ_3: 25;

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

              then (p . 1) = (S . (c . 1)) or (p . 1) = (T . (c . 1)) by A10, TARSKI:def 2;

              hence thesis by A4, A6, A7, A9, A10, A13, A11, A12, A14, FINSEQ_6: 147;

            end;

            hence thesis by A4;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: MSSCYC_1:6

    

     Th5: for G be Graph, c be Chain of G, vs be FinSequence of the carrier of G st c is cyclic & vs is_vertex_seq_of c holds (vs . 1) = (vs . ( len vs)) by Lm1;

    theorem :: MSSCYC_1:7

    

     Th6: for G be Graph, e be set st e in the carrier' of G holds for fe be directed Chain of G st fe = <*e*> holds ( vertex-seq fe) = <*(the Source of G . e), (the Target of G . e)*>

    proof

      let G be Graph;

      let e be set;

      assume e in the carrier' of G;

      then

      reconsider so = (the Source of G . e), ta = (the Target of G . e) as Element of the carrier of G by FUNCT_2: 5;

      reconsider sota = <*so, ta*> as FinSequence of the carrier of G;

      let fe be directed Chain of G;

      assume

       A1: fe = <*e*>;

      then

       A2: ( len fe) = 1 by FINSEQ_1: 39;

      

       A3: sota is_vertex_seq_of fe

      proof

        thus ( len sota) = (( len fe) + 1) by A2, FINSEQ_1: 44;

        let n;

        

         A4: (sota /. 2) = ta by FINSEQ_4: 17;

        assume 1 <= n & n <= ( len fe);

        then

         A5: n = 1 by A2, XXREAL_0: 1;

        e joins (so,ta) & (sota /. 1) = so by FINSEQ_4: 17;

        hence thesis by A1, A5, A4, FINSEQ_1: 40;

      end;

      e = (fe . 1) by A1, FINSEQ_1: 40;

      then (sota . 1) = (the Source of G . (fe . 1)) by FINSEQ_1: 44;

      hence thesis by A1, A3, GRAPH_2:def 10;

    end;

    theorem :: MSSCYC_1:8

    for f be FinSequence holds ( len ((m,n) -cut f)) <= ( len f)

    proof

      let f be FinSequence;

      set lmnf = ( len ((m,n) -cut f));

      set lf = ( len f);

      per cases ;

        suppose

         A1: 1 <= m & m <= n & n <= ( len f);

        then (lmnf + m) = (n + 1) by FINSEQ_6:def 4;

        then (n + (lmnf + m)) <= ((n + 1) + lf) by A1, XREAL_1: 6;

        then (n + (lmnf + m)) <= (n + (1 + lf));

        then (lmnf + m) <= (1 + lf) by XREAL_1: 6;

        then ((lmnf + m) + 1) <= (m + (1 + lf)) by A1, XREAL_1: 7;

        then (lmnf + (m + 1)) <= ((m + 1) + lf);

        hence thesis by XREAL_1: 6;

      end;

        suppose not (1 <= m & m <= n & n <= ( len f));

        then ((m,n) -cut f) is empty by FINSEQ_6:def 4;

        hence thesis;

      end;

    end;

    theorem :: MSSCYC_1:9

    for c be directed Chain of G st 1 <= m & m <= n & n <= ( len c) holds ((m,n) -cut c) is directed Chain of G

    proof

      let c be directed Chain of G;

      assume that

       A1: 1 <= m and

       A2: m <= n and

       A3: n <= ( len c);

      reconsider mnc = ((m,n) -cut c) as Chain of G by A1, A2, A3, GRAPH_2: 41;

      

       A4: (( len mnc) + m) = (n + 1) by A1, A2, A3, FINSEQ_6:def 4;

      now

        

         A5: (( len mnc) + m) <= (( len c) + 1) by A3, A4, XREAL_1: 6;

        let k;

        assume that

         A6: 1 <= k and

         A7: k < ( len mnc);

        ( 0 + 1) <= k by A6;

        then

        consider i be Nat such that 0 <= i and

         A8: i < ( len mnc) and

         A9: k = (i + 1) by A7, FINSEQ_6: 127;

        

         A10: 1 <= (m + i) by A1, NAT_1: 12;

        (m + (i + 1)) < (( len mnc) + m) by A7, A9, XREAL_1: 6;

        then ((m + i) + 1) < (( len c) + 1) by A5, XXREAL_0: 2;

        then

         A11: (m + i) < ( len c) by XREAL_1: 6;

        

         A12: (mnc . (k + 1)) = (c . (m + k)) by A1, A2, A3, A7, FINSEQ_6:def 4;

        (mnc . (i + 1)) = (c . (m + i)) & (m + k) = ((m + i) + 1) by A1, A2, A3, A8, A9, FINSEQ_6:def 4;

        hence (the Source of G . (mnc . (k + 1))) = (the Target of G . (mnc . k)) by A12, A10, A11, GRAPH_1:def 15;

      end;

      hence thesis by GRAPH_1:def 15;

    end;

    theorem :: MSSCYC_1:10

    

     Th9: for oc be non empty directed Chain of G holds ( len ( vertex-seq oc)) = (( len oc) + 1)

    proof

      let oc be non empty directed Chain of G;

      ( vertex-seq oc) is_vertex_seq_of oc by GRAPH_2:def 10;

      hence thesis;

    end;

    registration

      let G;

      let oc be directed non empty Chain of G;

      cluster ( vertex-seq oc) -> non empty;

      coherence

      proof

        ( len ( vertex-seq oc)) = (( len oc) + 1) by Th9;

        hence thesis;

      end;

    end

    theorem :: MSSCYC_1:11

    

     Th10: for oc be directed non empty Chain of G, n st 1 <= n & n <= ( len oc) holds (( vertex-seq oc) . n) = (the Source of G . (oc . n)) & (( vertex-seq oc) . (n + 1)) = (the Target of G . (oc . n))

    proof

      let oc be directed non empty Chain of G;

      set vsoc = ( vertex-seq oc), S = the Source of G, T = the Target of G;

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len oc) implies (vsoc . $1) = (S . (oc . $1)) & (vsoc . ($1 + 1)) = (T . (oc . $1));

      

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

      proof

        let n;

        assume

         A2: 1 <= n & n <= ( len oc) implies (vsoc . n) = (S . (oc . n)) & (vsoc . (n + 1)) = (T . (oc . n));

        

         A3: vsoc is_vertex_seq_of oc by GRAPH_2:def 10;

        assume that

         A4: 1 <= (n + 1) and

         A5: (n + 1) <= ( len oc);

        per cases ;

          suppose

           A6: n = 0 ;

          hence

           A7: (vsoc . (n + 1)) = (S . (oc . (n + 1))) by GRAPH_2:def 10;

          1 in ( dom vsoc) by FINSEQ_5: 6;

          then

           A8: (vsoc /. 1) = (vsoc . 1) by PARTFUN1:def 6;

          

           A9: 1 <= ( len oc) by A4, A5, XXREAL_0: 2;

          ( len vsoc) = (( len oc) + 1) by Th9;

          then (1 + 1) <= ( len vsoc) by A9, XREAL_1: 6;

          then (1 + 1) in ( dom vsoc) by FINSEQ_3: 25;

          then

           A10: (vsoc /. (1 + 1)) = (vsoc . (1 + 1)) by PARTFUN1:def 6;

          (oc . 1) joins ((vsoc /. 1),(vsoc /. (1 + 1))) by A3, A9;

          hence thesis by A6, A7, A8, A10;

        end;

          suppose

           A11: n <> 0 ;

          

           A12: n < ( len oc) by A5, NAT_1: 13;

          1 <= n by A11, NAT_1: 14;

          hence

           A13: (vsoc . (n + 1)) = (S . (oc . (n + 1))) by A2, A12, GRAPH_1:def 15;

          

           A14: ( len vsoc) = (( len oc) + 1) by Th9;

          then 1 <= ((n + 1) + 1) & ((n + 1) + 1) <= ( len vsoc) by A5, NAT_1: 11, XREAL_1: 6;

          then ((n + 1) + 1) in ( dom vsoc) by FINSEQ_3: 25;

          then

           A15: (vsoc /. ((n + 1) + 1)) = (vsoc . ((n + 1) + 1)) by PARTFUN1:def 6;

          n <= (n + 1) by NAT_1: 11;

          then n <= ( len oc) by A5, XXREAL_0: 2;

          then (n + 1) <= ( len vsoc) by A14, XREAL_1: 6;

          then (n + 1) in ( dom vsoc) by A4, FINSEQ_3: 25;

          then

           A16: (vsoc /. (n + 1)) = (vsoc . (n + 1)) by PARTFUN1:def 6;

          (oc . (n + 1)) joins ((vsoc /. (n + 1)),(vsoc /. ((n + 1) + 1))) by A4, A5, A3;

          hence thesis by A13, A16, A15;

        end;

      end;

      

       A17: P[ 0 ];

      thus for n holds P[n] from NAT_1:sch 2( A17, A1);

    end;

    theorem :: MSSCYC_1:12

    

     Th11: for f be non empty FinSequence st 1 <= m & m <= n & n <= ( len f) holds ((m,n) -cut f) is non empty

    proof

      let f be non empty FinSequence;

      set lmn = ( len ((m,n) -cut f));

      assume 1 <= m & m <= n & n <= ( len f);

      then m < (n + 1) & (lmn + m) = (n + 1) by FINSEQ_6:def 4, NAT_1: 13;

      then (m - (lmn + m)) < ((n + 1) - (n + 1)) by XREAL_1: 9;

      then ( - ( - lmn)) > 0 ;

      hence thesis;

    end;

    theorem :: MSSCYC_1:13

    for c,c1 be directed Chain of G st 1 <= m & m <= n & n <= ( len c) & c1 = ((m,n) -cut c) holds ( vertex-seq c1) = ((m,(n + 1)) -cut ( vertex-seq c))

    proof

      let c,c1 be directed Chain of G;

      assume that

       A1: 1 <= m and

       A2: m <= n and

       A3: n <= ( len c) and

       A4: c1 = ((m,n) -cut c);

      set mn1c = ((m,(n + 1)) -cut ( vertex-seq c));

      

       A5: c is non empty by A1, A2, A3;

      then

       A6: ( vertex-seq c) is_vertex_seq_of c by GRAPH_2:def 10;

      then

       A7: mn1c is_vertex_seq_of c1 by A1, A2, A3, A4, GRAPH_2: 42;

      set vsc = ( vertex-seq c);

      

       A8: m <= (n + 1) by A2, NAT_1: 12;

      

       A9: ( len vsc) = (( len c) + 1) by A6;

      then

       A10: (n + 1) <= ( len vsc) by A3, XREAL_1: 6;

      

       A11: c1 is non empty by A1, A2, A3, A4, A5, Th11;

      then 0 < ( len c1);

      then

       A12: (c1 . ( 0 + 1)) = (c . (m + 0 )) by A1, A2, A3, A4, FINSEQ_6:def 4;

      

       A13: m <= (n + 1) by A2, NAT_1: 12;

      vsc is non empty by A9;

      then mn1c is non empty by A1, A8, A10, Th11;

      then 0 < ( len mn1c);

      then

       A14: (vsc . (m + 0 )) = (mn1c . ( 0 + 1)) by A1, A10, A13, FINSEQ_6:def 4;

      m <= ( len c) by A2, A3, XXREAL_0: 2;

      then (mn1c . 1) = (the Source of G . (c1 . 1)) by A1, A5, A12, A14, Th10;

      hence thesis by A7, A11, GRAPH_2:def 10;

    end;

    theorem :: MSSCYC_1:14

    

     Th13: for oc be directed non empty Chain of G holds (( vertex-seq oc) . (( len oc) + 1)) = (the Target of G . (oc . ( len oc)))

    proof

      let oc be directed non empty Chain of G;

      1 in ( dom oc) by FINSEQ_5: 6;

      then 1 <= ( len oc) by FINSEQ_3: 25;

      hence thesis by Th10;

    end;

    theorem :: MSSCYC_1:15

    

     Th14: for c1,c2 be directed non empty Chain of G holds (( vertex-seq c1) . (( len c1) + 1)) = (( vertex-seq c2) . 1) iff (c1 ^ c2) is directed non empty Chain of G

    proof

      let c1,c2 be directed non empty Chain of G;

      set vsc1 = ( vertex-seq c1), vsc2 = ( vertex-seq c2);

      

       A1: ( len (c1 ^ c2)) = (( len c1) + ( len c2)) by FINSEQ_1: 22;

      

       A2: vsc1 is_vertex_seq_of c1 by GRAPH_2:def 10;

      then

       A3: vsc2 is_vertex_seq_of c2 & ( len vsc1) = (( len c1) + 1) by GRAPH_2:def 10;

      hereby

        assume

         A4: (( vertex-seq c1) . (( len c1) + 1)) = (( vertex-seq c2) . 1);

        then

        reconsider c1c2 = (c1 ^ c2) as Chain of G by A2, A3, GRAPH_2: 43;

        c1c2 is directed

        proof

          let n;

          assume that

           A5: 1 <= n and

           A6: n < ( len c1c2);

          per cases by XXREAL_0: 1;

            suppose

             A7: n < ( len c1);

            then 1 <= (n + 1) & (n + 1) <= ( len c1) by NAT_1: 11, NAT_1: 13;

            then (n + 1) in ( dom c1) by FINSEQ_3: 25;

            then

             A8: (c1c2 . (n + 1)) = (c1 . (n + 1)) by FINSEQ_1:def 7;

            n in ( dom c1) by A5, A7, FINSEQ_3: 25;

            then (c1c2 . n) = (c1 . n) by FINSEQ_1:def 7;

            hence thesis by A5, A7, A8, GRAPH_1:def 15;

          end;

            suppose

             A9: n = ( len c1);

            then n in ( dom c1) by FINSEQ_5: 6;

            then

             A10: (c1c2 . n) = (c1 . n) by FINSEQ_1:def 7;

            1 in ( dom c2) by FINSEQ_5: 6;

            then

             A11: (c1c2 . (n + 1)) = (c2 . 1) by A9, FINSEQ_1:def 7;

            (vsc1 . (( len c1) + 1)) = (the Target of G . (c1 . ( len c1))) by Th13;

            hence thesis by A4, A9, A11, A10, GRAPH_2:def 10;

          end;

            suppose

             A12: n > ( len c1);

            then

            reconsider k = (n - ( len c1)) as Element of NAT by INT_1: 5;

            

             A13: n = (( len c1) + k);

            

             A14: (n + 1) = (( len c1) + (k + 1));

            

             A15: k < ( len c2) by A1, A6, XREAL_1: 19;

            then 1 <= (k + 1) & (k + 1) <= ( len c2) by NAT_1: 11, NAT_1: 13;

            then (k + 1) in ( dom c2) by FINSEQ_3: 25;

            then

             A16: (c1c2 . (n + 1)) = (c2 . (k + 1)) by A14, FINSEQ_1:def 7;

            n >= (( len c1) + 1) by A12, NAT_1: 13;

            then

             A17: 1 <= k by XREAL_1: 19;

            then k in ( dom c2) by A15, FINSEQ_3: 25;

            then (c1c2 . n) = (c2 . k) by A13, FINSEQ_1:def 7;

            hence thesis by A17, A15, A16, GRAPH_1:def 15;

          end;

        end;

        hence (c1 ^ c2) is directed non empty Chain of G;

      end;

      set n = ( len c1);

      assume (c1 ^ c2) is directed non empty Chain of G;

      then

      reconsider c1c2 = (c1 ^ c2) as directed non empty Chain of G;

      

       A18: n < ( len c1c2) by A1, XREAL_1: 29;

      

       A19: n in ( dom c1) by FINSEQ_5: 6;

      then

       A20: (c1c2 . n) = (c1 . n) by FINSEQ_1:def 7;

      1 <= n by A19, FINSEQ_3: 25;

      then

       A21: (the Source of G . (c1c2 . (n + 1))) = (the Target of G . (c1c2 . n)) by A18, GRAPH_1:def 15;

      1 in ( dom c2) by FINSEQ_5: 6;

      then

       A22: (c1c2 . (n + 1)) = (c2 . 1) by FINSEQ_1:def 7;

      (vsc1 . (( len c1) + 1)) = (the Target of G . (c1 . ( len c1))) by Th13;

      hence thesis by A21, A22, A20, GRAPH_2:def 10;

    end;

    theorem :: MSSCYC_1:16

    

     Th15: for c,c1,c2 be directed non empty Chain of G st c = (c1 ^ c2) holds (( vertex-seq c) . 1) = (( vertex-seq c1) . 1) & (( vertex-seq c) . (( len c) + 1)) = (( vertex-seq c2) . (( len c2) + 1))

    proof

      let c,c1,c2 be directed non empty Chain of G;

      1 in ( dom c) by FINSEQ_5: 6;

      then 1 <= ( len c) by FINSEQ_3: 25;

      then

       A1: (( vertex-seq c) . 1) = (the Source of G . (c . 1)) & (( vertex-seq c) . (( len c) + 1)) = (the Target of G . (c . ( len c))) by Th10;

      

       A2: 1 in ( dom c1) by FINSEQ_5: 6;

      then 1 <= ( len c1) by FINSEQ_3: 25;

      then

       A3: (( vertex-seq c1) . 1) = (the Source of G . (c1 . 1)) by Th10;

      1 in ( dom c2) by FINSEQ_5: 6;

      then 1 <= ( len c2) by FINSEQ_3: 25;

      then

       A4: (( vertex-seq c2) . (( len c2) + 1)) = (the Target of G . (c2 . ( len c2))) by Th10;

      assume

       A5: c = (c1 ^ c2);

      then ( len c2) in ( dom c2) & ( len c) = (( len c1) + ( len c2)) by FINSEQ_1: 22, FINSEQ_5: 6;

      hence thesis by A5, A2, A3, A1, A4, FINSEQ_1:def 7;

    end;

    theorem :: MSSCYC_1:17

    

     Th16: for oc be directed non empty Chain of G st oc is cyclic holds (( vertex-seq oc) . 1) = (( vertex-seq oc) . (( len oc) + 1))

    proof

      let oc be directed non empty Chain of G;

      assume

       A1: oc is cyclic;

      set vsoc = ( vertex-seq oc);

      

       A2: vsoc is_vertex_seq_of oc by GRAPH_2:def 10;

      thus thesis by A1, A2, Th5;

    end;

    theorem :: MSSCYC_1:18

    

     Th17: for c be directed non empty Chain of G st c is cyclic holds for n holds ex ch be directed Chain of G st ( len ch) = n & (ch ^ c) is directed non empty Chain of G

    proof

      let c be directed non empty Chain of G;

      defpred Z[ Nat] means ex ch be directed Chain of G st ( rng ch) c= ( rng c) & ( len ch) = $1 & (ch ^ c) is directed non empty Chain of G;

      c is FinSequence of the carrier' of G by Def1;

      then

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

      assume

       A2: c is cyclic;

      

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

      proof

        ( len c) in ( dom c) by FINSEQ_5: 6;

        then

         A4: (c . ( len c)) in ( rng c) by FUNCT_1:def 3;

        then

        reconsider clc = (c . ( len c)) as Element of the carrier' of G by A1;

        reconsider ch9 = <*clc*> as directed Chain of G by Th4;

        

         A5: ( rng ch9) = {(c . ( len c))} by FINSEQ_1: 38;

        then

         A6: ( rng ch9) c= ( rng c) by A4, ZFMISC_1: 31;

        

         A7: ( len ch9) = 1 by FINSEQ_1: 39;

        let n be Nat;

        given ch be directed Chain of G such that

         A8: ( rng ch) c= ( rng c) and

         A9: ( len ch) = n and

         A10: (ch ^ c) is directed non empty Chain of G;

        per cases ;

          suppose

           A11: n = 0 ;

          take ch9;

          thus ( rng ch9) c= ( rng c) by A4, A5, ZFMISC_1: 31;

          thus ( len ch9) = (n + 1) by A11, FINSEQ_1: 39;

          set vsch9 = ( vertex-seq ch9);

          vsch9 = <*(the Source of G . clc), (the Target of G . clc)*> by Th6;

          

          then (vsch9 . (( len ch9) + 1)) = (the Target of G . clc) by A7, FINSEQ_1: 44

          .= (( vertex-seq c) . (( len c) + 1)) by Th13

          .= (( vertex-seq c) . 1) by A2, Th16;

          hence thesis by Th14;

        end;

          suppose n <> 0 ;

          then

           A12: ch is non empty by A9;

          then 1 in ( dom ch) by FINSEQ_5: 6;

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

          then

          consider i be Nat such that

           A13: i in ( dom c) and

           A14: (c . i) = (ch . 1) by A8, FINSEQ_2: 10;

          

           A15: i <= ( len c) by A13, FINSEQ_3: 25;

          

           A16: 1 <= i by A13, FINSEQ_3: 25;

          now

            per cases ;

              suppose

               A17: i = 1;

              set vsch9 = ( vertex-seq ch9);

              vsch9 = <*(the Source of G . clc), (the Target of G . clc)*> by Th6;

              

              then (vsch9 . (( len ch9) + 1)) = (the Target of G . clc) by A7, FINSEQ_1: 44

              .= (( vertex-seq c) . (( len c) + 1)) by Th13

              .= (( vertex-seq c) . 1) by A2, Th16

              .= (the Source of G . (ch . 1)) by A14, A17, GRAPH_2:def 10

              .= (( vertex-seq ch) . 1) by A12, GRAPH_2:def 10;

              then

              reconsider ch1 = (ch9 ^ ch) as directed Chain of G by A12, Th14;

              take ch1;

              ( rng ch1) = (( rng ch9) \/ ( rng ch)) by FINSEQ_1: 31;

              hence ( rng ch1) c= ( rng c) by A8, A6, XBOOLE_1: 8;

              thus ( len ch1) = (n + 1) by A9, A7, FINSEQ_1: 22;

              (( vertex-seq ch1) . (( len ch1) + 1)) = (( vertex-seq ch) . (( len ch) + 1)) by A12, Th15

              .= (( vertex-seq c) . 1) by A10, A12, Th14;

              hence (ch1 ^ c) is directed non empty Chain of G by Th14;

            end;

              suppose i <> 1;

              then 1 < i by A16, XXREAL_0: 1;

              then (1 + 1) <= i by NAT_1: 13;

              then

              consider k be Nat such that

               A18: 1 <= k & k < ( len c) and

               A19: i = (k + 1) by A15, FINSEQ_6: 127;

              k in ( dom c) by A18, FINSEQ_3: 25;

              then

               A20: (c . k) in ( rng c) by FUNCT_1:def 3;

              then

              reconsider ck = (c . k) as Element of the carrier' of G by A1;

              reconsider ch9 = <*ck*> as directed Chain of G by Th4;

              set vsch9 = ( vertex-seq ch9);

              

               A21: ( len ch9) = 1 by FINSEQ_1: 39;

              vsch9 = <*(the Source of G . ck), (the Target of G . ck)*> by Th6;

              

              then (vsch9 . (( len ch9) + 1)) = (the Target of G . ck) by A21, FINSEQ_1: 44

              .= (the Source of G . (ch . 1)) by A14, A18, A19, GRAPH_1:def 15

              .= (( vertex-seq ch) . 1) by A12, GRAPH_2:def 10;

              then

              reconsider ch1 = (ch9 ^ ch) as directed Chain of G by A12, Th14;

              take ch1;

              ( rng ch9) = {(c . k)} by FINSEQ_1: 38;

              then

               A22: ( rng ch9) c= ( rng c) by A20, ZFMISC_1: 31;

              ( rng ch1) = (( rng ch9) \/ ( rng ch)) by FINSEQ_1: 31;

              hence ( rng ch1) c= ( rng c) by A8, A22, XBOOLE_1: 8;

              thus ( len ch1) = (n + 1) by A9, A21, FINSEQ_1: 22;

              (( vertex-seq ch1) . (( len ch1) + 1)) = (( vertex-seq ch) . (( len ch) + 1)) by A12, Th15

              .= (( vertex-seq c) . 1) by A10, A12, Th14;

              hence (ch1 ^ c) is directed non empty Chain of G by Th14;

            end;

          end;

          hence thesis;

        end;

      end;

      let n be Nat;

      

       A23: Z[ 0 ]

      proof

        reconsider ch = {} as empty Chain of G by GRAPH_1: 14;

        reconsider ch as directed Chain of G;

        take ch;

        thus ( rng ch) c= ( rng c);

        thus ( len ch) = 0 ;

        thus thesis by FINSEQ_1: 34;

      end;

      for n be Nat holds Z[n] from NAT_1:sch 2( A23, A3);

      then ex ch be directed Chain of G st ( rng ch) c= ( rng c) & ( len ch) = n & (ch ^ c) is directed non empty Chain of G;

      hence thesis;

    end;

    definition

      let IT be Graph;

      :: MSSCYC_1:def3

      attr IT is directed_cycle-less means for dc be directed Chain of IT st dc is non empty holds dc is non cyclic;

    end

    notation

      let IT be Graph;

      antonym IT is with_directed_cycle for IT is directed_cycle-less;

    end

    registration

      cluster void -> directed_cycle-less for Graph;

      coherence

      proof

        let G be Graph;

        assume

         A1: G is void;

        let c be directed Chain of G;

        assume

         A2: c is non empty;

        c is FinSequence of the carrier' of G by Def1;

        hence thesis by A1, A2;

      end;

    end

    definition

      let IT be Graph;

      :: MSSCYC_1:def4

      attr IT is well-founded means for v be Element of the carrier of IT holds ex n st for c be directed Chain of IT st c is non empty & (( vertex-seq c) . (( len c) + 1)) = v holds ( len c) <= n;

    end

    registration

      let G be void Graph;

      cluster -> empty for Chain of G;

      coherence

      proof

        let c be Chain of G;

        assume

         A1: c is non empty;

        c is FinSequence of the carrier' of G by Def1;

        hence thesis by A1;

      end;

    end

    registration

      cluster void -> well-founded for Graph;

      coherence

      proof

        let G be Graph;

        assume G is void;

        then

        reconsider G9 = G as void Graph;

        let v be Element of the carrier of G;

        take 0 ;

        let c be directed Chain of G;

        reconsider c as Chain of G9;

        c is empty;

        hence thesis;

      end;

    end

    registration

      cluster non well-founded -> non void for Graph;

      coherence ;

    end

    registration

      cluster well-founded for Graph;

      existence

      proof

        set G = the void Graph;

        G is well-founded;

        hence thesis;

      end;

    end

    registration

      cluster well-founded -> directed_cycle-less for Graph;

      coherence

      proof

        let G be Graph;

        per cases ;

          suppose G is void;

          then

          reconsider G as void Graph;

          G is directed_cycle-less;

          hence thesis;

        end;

          suppose G is non void;

          then

          reconsider G9 = G as non void Graph;

          assume that

           A1: G is well-founded and

           A2: G is non directed_cycle-less;

          consider dc be directed Chain of G9 such that

           A3: dc is non empty and

           A4: dc is cyclic by A2;

          set p = ( vertex-seq dc);

          ( len p) = (( len dc) + 1) by A3, Th9;

          then 1 <= ( len p) by NAT_1: 11;

          then 1 in ( dom p) by FINSEQ_3: 25;

          then

          reconsider v = (p . 1) as Element of the carrier of G by FINSEQ_2: 11;

          consider n such that

           A5: for c be directed Chain of G9 st c is non empty & (( vertex-seq c) . (( len c) + 1)) = v holds ( len c) <= n by A1;

          consider ch be directed Chain of G9 such that

           A6: ( len ch) = (n + 1) and

           A7: (ch ^ dc) is directed non empty Chain of G9 by A3, A4, Th17;

          reconsider ch as directed non empty Chain of G9 by A6;

          reconsider cc = (ch ^ dc) as directed non empty Chain of G9 by A7;

          (( vertex-seq dc) . 1) = (( vertex-seq dc) . (( len dc) + 1)) by A3, A4, Th16;

          then (( vertex-seq cc) . (( len cc) + 1)) = v by A3, Th15;

          then

           A8: ( len cc) <= n by A5;

          ( len cc) = ((n + 1) + ( len dc)) by A6, FINSEQ_1: 22;

          then (n + 1) <= ( len cc) by NAT_1: 11;

          hence contradiction by A8, NAT_1: 13;

        end;

      end;

    end

    registration

      cluster non well-founded for Graph;

      existence

      proof

        set V = {1}, E = {1};

        reconsider j = 1 as Element of V by TARSKI:def 1;

        reconsider S = (E --> j), T = (E --> j) as Function of E, V;

        reconsider G = MultiGraphStruct (# V, E, S, T #) as Graph;

        reconsider v = 1 as Element of the carrier of G;

        take G;

        

         A1: (S . 1) = 1 by FUNCOP_1: 7;

        

         A2: G is with_directed_cycle

        proof

          reconsider dc = <*1*> as directed Chain of G by Th4;

          take dc;

          thus dc is non empty;

          

           A3: ( <*v, v*> . 2) = v & ( len <*v, v*>) = 2 by FINSEQ_1: 44;

           <*v, v*> is_vertex_seq_of dc & ( <*v, v*> . 1) = v by A1, Th3, FINSEQ_1: 44;

          hence thesis by A3;

        end;

        assume G is well-founded;

        then

        reconsider G as well-founded Graph;

        G is directed_cycle-less;

        hence contradiction by A2;

      end;

    end

    registration

      cluster directed_cycle-less for Graph;

      existence

      proof

        set G = the well-founded Graph;

        G is directed_cycle-less;

        hence thesis;

      end;

    end

    theorem :: MSSCYC_1:19

    for t be DecoratedTree, p be Node of t, k be Element of NAT holds (p | k) is Node of t

    proof

      let t be DecoratedTree, p be Node of t, k be Element of NAT ;

      (p | k) = (p | ( Seg k)) by FINSEQ_1:def 15;

      then (p | k) is_a_prefix_of p by TREES_1:def 1;

      hence thesis by TREES_1: 20;

    end;

    begin

    theorem :: MSSCYC_1:20

    for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, t be Term of S, X st not t is root holds ex o be OperSymbol of S st (t . {} ) = [o, the carrier of S]

    proof

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, t be Term of S, X;

      assume

       A1: not t is root;

      per cases by MSATERM: 2;

        suppose ex s be SortSymbol of S, v be Element of (X . s) st (t . {} ) = [v, s];

        then

        consider s be SortSymbol of S, v be Element of (X . s) such that

         A2: (t . {} ) = [v, s];

        t = ( root-tree [v, s]) by A2, MSATERM: 5;

        hence thesis by A1;

      end;

        suppose (t . {} ) in [:the carrier' of S, {the carrier of S}:];

        then

        consider o,c be object such that

         A3: o in the carrier' of S and

         A4: c in {the carrier of S} & (t . {} ) = [o, c] by ZFMISC_1:def 2;

        reconsider o as OperSymbol of S by A3;

        take o;

        thus thesis by A4, TARSKI:def 1;

      end;

    end;

    theorem :: MSSCYC_1:21

    

     Th20: for S be non void non empty ManySortedSign, A be MSAlgebra over S, G be GeneratorSet of A, B be MSSubset of A st G c= B holds B is GeneratorSet of A

    proof

      let S be non void non empty ManySortedSign, A be MSAlgebra over S, G be GeneratorSet of A, B be MSSubset of A;

      B is MSSubset of ( GenMSAlg B) by MSUALG_2:def 17;

      then

       A1: B c= the Sorts of ( GenMSAlg B) by PBOOLE:def 18;

      assume G c= B;

      then G c= the Sorts of ( GenMSAlg B) by A1, PBOOLE: 13;

      then G is MSSubset of ( GenMSAlg B) by PBOOLE:def 18;

      then ( GenMSAlg G) is MSSubAlgebra of ( GenMSAlg B) by MSUALG_2:def 17;

      then the Sorts of ( GenMSAlg G) is MSSubset of ( GenMSAlg B) by MSUALG_2:def 9;

      then

       A2: the Sorts of ( GenMSAlg G) c= the Sorts of ( GenMSAlg B) by PBOOLE:def 18;

      

       A3: the Sorts of ( GenMSAlg G) = the Sorts of A by MSAFREE:def 4;

      then the Sorts of ( GenMSAlg B) is MSSubset of ( GenMSAlg G) by MSUALG_2:def 9;

      then the Sorts of ( GenMSAlg B) c= the Sorts of ( GenMSAlg G) by PBOOLE:def 18;

      hence the Sorts of ( GenMSAlg B) = the Sorts of A by A3, A2, PBOOLE: 146;

    end;

    registration

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

      cluster non-empty finite-yielding for GeneratorSet of A;

      existence

      proof

        consider G be GeneratorSet of A such that

         A1: G is finite-yielding by MSAFREE2:def 10;

        consider B be ManySortedSet of the carrier of S such that

         A2: B in the Sorts of A by PBOOLE: 134;

        deffunc F( object) = {(B . $1)};

        consider C be ManySortedSet of the carrier of S such that

         A3: for i be object st i in the carrier of S holds (C . i) = F(i) from PBOOLE:sch 4;

        set H = (G (\/) C);

        now

          let i be object;

          assume

           A4: i in the carrier of S;

          then (B . i) in (the Sorts of A . i) by A2;

          then {(B . i)} c= (the Sorts of A . i) by ZFMISC_1: 31;

          hence (C . i) c= (the Sorts of A . i) by A3, A4;

        end;

        then G c= the Sorts of A & C c= the Sorts of A by PBOOLE:def 18;

        then

         A5: C c= H & (G (\/) C) c= the Sorts of A by PBOOLE: 14, PBOOLE: 16;

        now

          let i be object;

          assume i in the carrier of S;

          then (C . i) = {(B . i)} by A3;

          hence (C . i) is non empty;

        end;

        then C is non-empty;

        then

        reconsider H as non-empty MSSubset of A by A5, PBOOLE: 131, PBOOLE:def 18;

        G c= H by PBOOLE: 14;

        then

        reconsider H as GeneratorSet of A by Th20;

        take H;

        thus H is non-empty;

        let i be object;

        assume

         A6: i in the carrier of S;

        then

         A7: (C . i) = {(B . i)} by A3;

        

         A8: (H . i) = ((G . i) \/ (C . i)) by A6, PBOOLE:def 4;

        (G . i) is finite by A1;

        hence thesis by A7, A8;

      end;

    end

    theorem :: MSSCYC_1:22

    

     Th21: for S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S, X be non-empty GeneratorSet of A holds ex F be ManySortedFunction of ( FreeMSA X), A st F is_epimorphism (( FreeMSA X),A)

    proof

      let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S, X be non-empty GeneratorSet of A;

      reconsider X9 = X as MSSubset of A;

      now

        let i be object such that

         A1: i in the carrier of S;

        

         A2: (( Reverse X) . i) is Function of (( FreeGen X) . i), (X . i) by A1, PBOOLE:def 15;

        X c= the Sorts of A by PBOOLE:def 18;

        then (X . i) c= (the Sorts of A . i) by A1;

        hence (( Reverse X) . i) is Function of (( FreeGen X) . i), (the Sorts of A . i) by A1, A2, FUNCT_2: 7;

      end;

      then

      reconsider ff = ( Reverse X) as ManySortedFunction of ( FreeGen X), the Sorts of A by PBOOLE:def 15;

      ( FreeGen X) is free by MSAFREE: 16;

      then

      consider h be ManySortedFunction of ( FreeMSA X), A such that

       A3: h is_homomorphism (( FreeMSA X),A) and

       A4: (h || ( FreeGen X)) = ff;

      take h;

      thus h is_homomorphism (( FreeMSA X),A) by A3;

      let i be set;

      assume i in the carrier of S;

      then

      reconsider s = i as SortSymbol of S;

      set f = (h . s);

      consider g be ManySortedFunction of ( FreeMSA X), ( Image h) such that

       A5: h = g and

       A6: g is_epimorphism (( FreeMSA X),( Image h)) by A3, MSUALG_3: 21;

      

       A7: g is_homomorphism (( FreeMSA X),( Image h)) by A6;

      

       A8: ( Image g) = ( Image h) by A6, MSUALG_3: 19;

      X is MSSubset of ( Image h)

      proof

        let i be object;

        assume

         A9: i in the carrier of S;

        then

        reconsider s = i as SortSymbol of S;

        s in ( dom ( Reverse X)) by A9, PARTFUN1:def 2;

        then

         A10: ( rngs ( Reverse X)) = X & (( rngs ( Reverse X)) . s) = ( rng (( Reverse X) . s)) by EXTENS_1: 10, FUNCT_6: 22;

        reconsider hs = (h . s) as Function of (the Sorts of ( FreeMSA X) . s), (the Sorts of A . s);

        let x be object;

        ( FreeGen X) c= the Sorts of ( FreeMSA X) by PBOOLE:def 18;

        then

         A11: (( FreeGen X) . s) c= (the Sorts of ( FreeMSA X) . s);

        the Sorts of ( Image h) = (h .:.: the Sorts of ( FreeMSA X)) by A3, MSUALG_3:def 12;

        then

         A12: (the Sorts of ( Image h) . s) = (hs .: (the Sorts of ( FreeMSA X) . s)) by PBOOLE:def 20;

        assume x in (X . i);

        then

        consider c be object such that

         A13: c in ( dom (ff . s)) and

         A14: x = ((ff . s) . c) by A10, FUNCT_1:def 3;

        

         A15: (ff . s) = (hs | (( FreeGen X) . s)) by A4, MSAFREE:def 1;

        then ( dom (ff . s)) = (( dom hs) /\ (( FreeGen X) . s)) by RELAT_1: 61;

        then

         A16: c in (( FreeGen X) . s) & c in ( dom hs) by A13, XBOOLE_0:def 4;

        x = (hs . c) by A15, A13, A14, FUNCT_1: 47;

        hence thesis by A12, A11, A16, FUNCT_1:def 6;

      end;

      then ( GenMSAlg X9) is MSSubAlgebra of ( Image h) by MSUALG_2:def 17;

      then the Sorts of ( GenMSAlg X9) is MSSubset of ( Image h) by MSUALG_2:def 9;

      then

       A17: the Sorts of ( GenMSAlg X9) c= the Sorts of ( Image h) by PBOOLE:def 18;

      the Sorts of ( Image g) = (h .:.: the Sorts of ( FreeMSA X)) by A5, A7, MSUALG_3:def 12;

      then

       A18: (the Sorts of ( Image g) . i) = (f .: (the Sorts of ( FreeMSA X) . i)) by PBOOLE:def 20;

      the Sorts of ( Image h) is MSSubset of A by MSUALG_2:def 9;

      then the Sorts of ( GenMSAlg X9) = the Sorts of A & the Sorts of ( Image h) c= the Sorts of A by MSAFREE:def 4, PBOOLE:def 18;

      then the Sorts of ( Image h) = the Sorts of A by A17, PBOOLE: 146;

      hence thesis by A18, A8, RELSET_1: 22;

    end;

    theorem :: MSSCYC_1:23

    for S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S, X be non-empty GeneratorSet of A st A is non finite-yielding holds ( FreeMSA X) is non finite-yielding

    proof

      let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S, X be non-empty GeneratorSet of A such that

       A1: A is non finite-yielding and

       A2: ( FreeMSA X) is finite-yielding;

      the Sorts of A is non finite-yielding by A1, MSAFREE2:def 11;

      then

      consider i be object such that

       A3: i in the carrier of S and

       A4: (the Sorts of A . i) is infinite;

      the Sorts of ( FreeMSA X) is finite-yielding by A2, MSAFREE2:def 11;

      then

       A5: (the Sorts of ( FreeMSA X) . i) is finite;

      reconsider FXi = (the Sorts of ( FreeMSA X) . i) as non empty set by A3;

      reconsider SAi = (the Sorts of A . i) as non empty set by A3;

      consider F be ManySortedFunction of ( FreeMSA X), A such that

       A6: F is_epimorphism (( FreeMSA X),A) by Th21;

      reconsider i as Element of S by A3;

      reconsider Fi = (F . i) as Function of FXi, SAi;

      F is "onto" by A6;

      then ( rng Fi) = SAi;

      hence contradiction by A4, A5;

    end;

    registration

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

      cluster ( FreeGen (v,X)) -> finite;

      coherence

      proof

        

         A1: ((X . v),( FreeGen (v,X))) are_equipotent

        proof

          set Z = the set of all [a, ( root-tree [a, v])] where a be Element of (X . v);

          take Z;

          hereby

            let x be object such that

             A2: x in (X . v);

            reconsider y = ( root-tree [x, v]) as object;

            take y;

            thus y in ( FreeGen (v,X)) by A2, MSAFREE:def 15;

            thus [x, y] in Z by A2;

          end;

          hereby

            let y be object;

            assume y in ( FreeGen (v,X));

            then

            consider x be set such that

             A3: x in (X . v) and

             A4: y = ( root-tree [x, v]) by MSAFREE:def 15;

            reconsider x as object;

            take x;

            thus x in (X . v) by A3;

            thus [x, y] in Z by A3, A4;

          end;

          let x,y,z,u be object;

          assume that

           A5: [x, y] in Z and

           A6: [z, u] in Z;

          consider a be Element of (X . v) such that

           A7: [x, y] = [a, ( root-tree [a, v])] by A5;

          consider b be Element of (X . v) such that

           A8: [z, u] = [b, ( root-tree [b, v])] by A6;

          

           A9: z = b by A8, XTUPLE_0: 1;

          

           A10: x = a by A7, XTUPLE_0: 1;

          hence x = z implies y = u by A7, A8, A9, XTUPLE_0: 1;

          

           A11: y = ( root-tree [a, v]) by A7, XTUPLE_0: 1;

          

           A12: u = ( root-tree [b, v]) by A8, XTUPLE_0: 1;

          assume y = u;

          then [a, v] = [b, v] by A11, A12, TREES_4: 4;

          hence thesis by A10, A9, XTUPLE_0: 1;

        end;

        thus thesis by A1, CARD_1: 38;

      end;

    end

    theorem :: MSSCYC_1:24

    

     Th23: for S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S, o be OperSymbol of S st (the Arity of S . o) = {} holds ( dom ( Den (o,A))) = { {} }

    proof

      ( dom {} ) = {} & ( rng {} ) = {} ;

      then

      reconsider b = {} as Function of {} , {} by FUNCT_2: 1;

      let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S, o be OperSymbol of S such that

       A1: (the Arity of S . o) = {} ;

      

       A2: ( dom the Arity of S) = the carrier' of S by FUNCT_2:def 1;

      then ( dom (the Sorts of A # ) qua ManySortedSet of (the carrier of S * )) = (the carrier of S * ) & (the Arity of S . o) in ( rng the Arity of S) by FUNCT_1:def 3, PARTFUN1:def 2;

      then

       A3: o in ( dom ((the Sorts of A # ) * the Arity of S)) by A2, FUNCT_1: 11;

      

      thus ( dom ( Den (o,A))) = ( Args (o,A)) by FUNCT_2:def 1

      .= (((the Sorts of A # ) * the Arity of S) . o) by MSUALG_1:def 4

      .= ((the Sorts of A # ) . (the Arity of S . o)) by A3, FUNCT_1: 12

      .= ((the Sorts of A # ) . ( the_arity_of o)) by MSUALG_1:def 1

      .= ( product (the Sorts of A * ( the_arity_of o)) qua Function) by FINSEQ_2:def 5

      .= ( product (the Sorts of A * b)) by A1, MSUALG_1:def 1

      .= { {} } by CARD_3: 10;

    end;

    definition

      let IT be non void non empty ManySortedSign;

      :: MSSCYC_1:def5

      attr IT is finitely_operated means for s be SortSymbol of IT holds { o where o be OperSymbol of IT : ( the_result_sort_of o) = s } is finite;

    end

    theorem :: MSSCYC_1:25

    for S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S, v be SortSymbol of S st S is finitely_operated holds ( Constants (A,v)) is finite

    proof

      let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S, v be SortSymbol of S such that

       A1: S is finitely_operated;

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

      consider Av be non empty set such that Av = (the Sorts of A . v) and

       A2: ( Constants (A,v)) = { a where a be Element of Av : ex o be OperSymbol of S st (the Arity of S . o) = {} & (the ResultSort of S . o) = v & a in ( rng ( Den (o,A))) } by MSUALG_2:def 3;

      

       A3: Ov is finite by A1;

       A4:

      now

        assume Ov is non empty;

        then

        reconsider Ov as non empty set;

        deffunc G( Element of the carrier' of S) = (( Den ($1,A)) . {} );

        defpred P[ Element of Ov] means (the Arity of S . $1) = {} ;

        set COv = { o where o be Element of Ov : P[o] };

        set aCOv = { G(o) where o be Element of the carrier' of S : o in COv };

        

         A5: ( Constants (A,v)) c= aCOv

        proof

          let c be object;

          assume c in ( Constants (A,v));

          then

          consider a be Element of Av such that

           A6: a = c and

           A7: ex o be OperSymbol of S st (the Arity of S . o) = {} & (the ResultSort of S . o) = v & a in ( rng ( Den (o,A))) by A2;

          consider o be OperSymbol of S such that

           A8: (the Arity of S . o) = {} and

           A9: (the ResultSort of S . o) = v and

           A10: a in ( rng ( Den (o,A))) by A7;

          ( the_result_sort_of o) = (the ResultSort of S . o) by MSUALG_1:def 2;

          then o in Ov by A9;

          then

          reconsider o9 = o as Element of Ov;

          

           A11: o9 in COv by A8;

          set f = ( Den (o,A));

          consider x be object such that

           A12: x in ( dom f) and

           A13: a = (f . x) by A10, FUNCT_1:def 3;

          ( dom f) = { {} } by A8, Th23;

          then x = {} by A12, TARSKI:def 1;

          hence thesis by A6, A11, A13;

        end;

        COv is Subset of Ov from DOMAIN_1:sch 7;

        then

         A14: COv is finite by A3;

        aCOv is finite from FRAENKEL:sch 21( A14);

        hence thesis by A5;

      end;

      now

        assume

         A15: Ov is empty;

        now

          assume ( Constants (A,v)) is non empty;

          then

          consider c be object such that

           A16: c in ( Constants (A,v)) by XBOOLE_0:def 1;

          consider a be Element of Av such that a = c and

           A17: ex o be OperSymbol of S st (the Arity of S . o) = {} & (the ResultSort of S . o) = v & a in ( rng ( Den (o,A))) by A2, A16;

          consider o be OperSymbol of S such that (the Arity of S . o) = {} and

           A18: (the ResultSort of S . o) = v and a in ( rng ( Den (o,A))) by A17;

          ( the_result_sort_of o) = (the ResultSort of S . o) by MSUALG_1:def 2;

          then o in Ov by A18;

          hence contradiction by A15;

        end;

        hence thesis;

      end;

      hence thesis by A4;

    end;

    theorem :: MSSCYC_1:26

    for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v be SortSymbol of S holds { t where t be Element of (the Sorts of ( FreeMSA X) . v) : ( depth t) = 0 } = (( FreeGen (v,X)) \/ ( Constants (( FreeMSA X),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;

      set SF = the Sorts of ( FreeMSA X);

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

      

       A1: d0 c= (( FreeGen (v,X)) \/ ( Constants (( FreeMSA X),v)))

      proof

        let x be object;

        assume x in d0;

        then

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

         A2: x = t and

         A3: ( depth t) = 0 ;

        t in (SF . v);

        then t in ( FreeSort (X,v)) by MSAFREE:def 11;

        then

        consider a be Element of ( TS ( DTConMSA X)) such that

         A4: t = a and

         A5: (ex x be set st x in (X . v) & a = ( root-tree [x, v])) or ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = v;

        consider dt be finite DecoratedTree, ft be finite Tree such that

         A6: dt = t and

         A7: ft = ( dom dt) & ( depth t) = ( height ft) by MSAFREE2:def 14;

        per cases by A5;

          suppose ex x be set st x in (X . v) & a = ( root-tree [x, v]);

          then t in ( FreeGen (v,X)) by A4, MSAFREE:def 15;

          hence thesis by A2, XBOOLE_0:def 3;

        end;

          suppose ex o be OperSymbol of S st [o, the carrier of S] = (a . {} ) & ( the_result_sort_of o) = v;

          then

          consider o be OperSymbol of S such that

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

           A9: ( the_result_sort_of o) = v;

          

           A10: (the ResultSort of S . o) = v by A9, MSUALG_1:def 2;

          set ars9 = ( <*> ( TS ( DTConMSA X)));

          reconsider t9 = t as Term of S, X by A4, MSATERM:def 1;

          

           A11: ex Av be non empty set st Av = (SF . v) & ( Constants (( FreeMSA X),v)) = { a1 where a1 be Element of Av : ex o be OperSymbol of S st (the Arity of S . o) = {} & (the ResultSort of S . o) = v & a1 in ( rng ( Den (o,( FreeMSA X)))) } by MSUALG_2:def 3;

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

           A12: t9 = ( [o, the carrier of S] -tree ars) by A4, A8, MSATERM: 10;

          dt = ( root-tree (dt . {} )) by A3, A7, TREES_1: 43, TREES_4: 5;

          then

           A13: ars = {} by A6, A12, TREES_4: 17;

          

          then 0 = ( len ars)

          .= ( len ( the_arity_of o)) by MSATERM: 22;

          then ( the_arity_of o) = {} ;

          then

           A14: (the Arity of S . o) = {} by MSUALG_1:def 1;

          then ( dom ( Den (o,( FreeMSA X)))) = { {} } by Th23;

          then

           A15: {} in ( dom ( Den (o,( FreeMSA X)))) by TARSKI:def 1;

          ( Sym (o,X)) ==> ( roots ars) by MSATERM: 21;

          then

           A16: (( DenOp (o,X)) . ars9) = t by A12, A13, MSAFREE:def 12;

          ( Den (o,( FreeMSA X))) = (( FreeOper X) . o) by MSUALG_1:def 6

          .= ( DenOp (o,X)) by MSAFREE:def 13;

          then t in ( rng ( Den (o,( FreeMSA X)))) by A16, A15, FUNCT_1:def 3;

          then t in ( Constants (( FreeMSA X),v)) by A14, A10, A11;

          hence thesis by A2, XBOOLE_0:def 3;

        end;

      end;

      

       A17: ( Constants (( FreeMSA X),v)) c= d0

      proof

        set p = ( <*> ( TS ( DTConMSA X)));

        let x be object;

        consider Av be non empty set such that

         A18: Av = (the Sorts of ( FreeMSA X) . v) and

         A19: ( Constants (( FreeMSA X),v)) = { a where a be Element of Av : ex o be OperSymbol of S st (the Arity of S . o) = {} & (the ResultSort of S . o) = v & a in ( rng ( Den (o,( FreeMSA X)))) } by MSUALG_2:def 3;

        assume x in ( Constants (( FreeMSA X),v));

        then

        consider a be Element of Av such that

         A20: x = a and

         A21: ex o be OperSymbol of S st (the Arity of S . o) = {} & (the ResultSort of S . o) = v & a in ( rng ( Den (o,( FreeMSA X)))) by A19;

        consider o be OperSymbol of S such that

         A22: (the Arity of S . o) = {} and (the ResultSort of S . o) = v and

         A23: a in ( rng ( Den (o,( FreeMSA X)))) by A21;

        

         A24: ( dom ( Den (o,( FreeMSA X)))) = { {} } by A22, Th23;

        (((( FreeSort X) # ) * the Arity of S) . o) = ( Args (o,( FreeMSA X))) by MSUALG_1:def 4

        .= ( dom ( Den (o,( FreeMSA X)))) by FUNCT_2:def 1;

        then p in (((( FreeSort X) # ) * the Arity of S) . o) by A24, TARSKI:def 1;

        then ( Sym (o,X)) ==> ( roots p) by MSAFREE: 10;

        then

         A25: (( DenOp (o,X)) . p) = (( Sym (o,X)) -tree p) by MSAFREE:def 12;

        reconsider a as Element of (the Sorts of ( FreeMSA X) . v) by A18;

        consider d be object such that

         A26: d in ( dom ( Den (o,( FreeMSA X)))) and

         A27: a = (( Den (o,( FreeMSA X))) . d) by A23, FUNCT_1:def 3;

        consider dt be finite DecoratedTree, t be finite Tree such that

         A28: dt = a & t = ( dom dt) and

         A29: ( depth a) = ( height t) by MSAFREE2:def 14;

        

         A30: ( Den (o,( FreeMSA X))) = (( FreeOper X) . o) by MSUALG_1:def 6

        .= ( DenOp (o,X)) by MSAFREE:def 13;

        d = {} by A24, A26, TARSKI:def 1;

        then a = ( root-tree ( Sym (o,X))) by A27, A30, A25, TREES_4: 20;

        then ( height t) = 0 by A28, TREES_1: 42, TREES_4: 3;

        hence thesis by A20, A29;

      end;

      ( FreeGen (v,X)) c= d0

      proof

        let x be object;

        assume

         A31: x in ( FreeGen (v,X));

        then

        reconsider x9 = x as Element of (SF . v);

        consider dt be finite DecoratedTree, t be finite Tree such that

         A32: dt = x9 & t = ( dom dt) and

         A33: ( depth x9) = ( height t) by MSAFREE2:def 14;

        ex a be set st a in (X . v) & x = ( root-tree [a, v]) by A31, MSAFREE:def 15;

        then ( height t) = 0 by A32, TREES_1: 42, TREES_4: 3;

        hence thesis by A33;

      end;

      then (( FreeGen (v,X)) \/ ( Constants (( FreeMSA X),v))) c= d0 by A17, XBOOLE_1: 8;

      hence thesis by A1, XBOOLE_0:def 10;

    end;

    theorem :: MSSCYC_1:27

    for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v,vk be SortSymbol of S, o be OperSymbol of S, t be Element of (the Sorts of ( FreeMSA X) . v), a be ArgumentSeq of ( Sym (o,X)), k be Element of NAT , ak be Element of (the Sorts of ( FreeMSA X) . vk) st t = ( [o, the carrier of S] -tree a) & k in ( dom a) & ak = (a . k) holds ( depth ak) < ( depth t)

    proof

      let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, v,vk be SortSymbol of S, o be OperSymbol of S, t be Element of (the Sorts of ( FreeMSA X) . v), a be ArgumentSeq of ( Sym (o,X)), k be Element of NAT , ak be Element of (the Sorts of ( FreeMSA X) . vk);

      assume that

       A1: t = ( [o, the carrier of S] -tree a) and

       A2: k in ( dom a) and

       A3: ak = (a . k);

      reconsider a9 = a as DTree-yielding FinSequence;

      

       A4: (ex dt be finite DecoratedTree, tt be finite Tree st dt = t & tt = ( dom dt) & ( depth t) = ( height tt)) & ex q be DTree-yielding FinSequence st a9 = q & ( dom t) = ( tree ( doms q)) by A1, MSAFREE2:def 14, TREES_4:def 4;

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

      consider dtk be finite DecoratedTree, ttk be finite Tree such that

       A5: dtk = ak & ttk = ( dom dtk) and

       A6: ( depth ak) = ( height ttk) by MSAFREE2:def 14;

      ( dom ( doms a9)) = ( dom a9) & ttk = (da . k) by A2, A3, A5, FUNCT_6: 22, TREES_3: 37;

      then ttk in ( rng da) by A2, FUNCT_1:def 3;

      hence thesis by A6, A4, TREES_3: 78;

    end;