lexbfs.miz



    begin

    

     Lm1: for F be Function, x,y be set holds ( dom (F +* (x .--> y))) = (( dom F) \/ {x})

    proof

      let F be Function, x,y be set;

      

      thus ( dom (F +* (x .--> y))) = (( dom F) \/ ( dom (x .--> y))) by FUNCT_4:def 1

      .= (( dom F) \/ {x});

    end;

    

     Lm2: for f be one-to-one Function, X,Y be set st X c= Y holds for x be set st x in ( dom ((f | X) " )) holds (((f | X) " ) . x) = (((f | Y) " ) . x)

    proof

      let f be one-to-one Function, X,Y be set;

      assume X c= Y;

      then (f | X) c= (f | Y) by RELAT_1: 75;

      then

       A1: ((f | X) qua Relation ~ ) c= ((f | Y) qua Relation ~ ) by SYSREL: 11;

      (f | X) is one-to-one by FUNCT_1: 52;

      then

       A2: ((f | X) qua Relation ~ ) = ((f | X) " ) by FUNCT_1:def 5;

      (f | Y) is one-to-one by FUNCT_1: 52;

      then

       A3: ((f | Y) qua Relation ~ ) = ((f | Y) " ) by FUNCT_1:def 5;

      let x be set;

      assume x in ( dom ((f | X) " ));

      hence thesis by A1, A2, A3, GRFUNC_1: 2;

    end;

    theorem :: LEXBFS:1

    for A,B be Element of NAT , X be non empty set holds for F be sequence of X st F is one-to-one holds ( card { (F . w) where w be Element of NAT : A <= w & w <= (A + B) }) = (B + 1)

    proof

      let A,B be Element of NAT , X be non empty set;

      let F be sequence of X such that

       A1: F is one-to-one;

      defpred P[ Nat] means ( card { (F . w) where w be Element of NAT : A <= w & w <= (A + $1) }) = ($1 + 1);

      

       A2: ( dom F) = NAT by FUNCT_2:def 1;

      

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

      proof

        let k be Nat such that

         A4: P[k];

        set Fwk = { (F . w) where w be Element of NAT : A <= w & w <= (A + k) };

        reconsider Fwk as finite set by A4;

        set Fwk1 = { (F . w) where w be Element of NAT : A <= w & w <= ((A + k) + 1) };

         A5:

        now

          let x be object;

          hereby

            assume x in Fwk1;

            then

            consider w be Element of NAT such that

             A6: x = (F . w) and

             A7: A <= w and

             A8: w <= ((A + k) + 1);

            

             A9: w = ((A + k) + 1) or w < ((A + k) + 1) by A8, XXREAL_0: 1;

            per cases by A9, NAT_1: 13;

              suppose w = ((A + k) + 1);

              then x in {(F . ((A + k) + 1))} by A6, TARSKI:def 1;

              hence x in (Fwk \/ {(F . ((A + k) + 1))}) by XBOOLE_0:def 3;

            end;

              suppose w <= (A + k);

              then x in Fwk by A6, A7;

              hence x in (Fwk \/ {(F . ((A + k) + 1))}) by XBOOLE_0:def 3;

            end;

          end;

          assume

           A10: x in (Fwk \/ {(F . ((A + k) + 1))});

          per cases by A10, XBOOLE_0:def 3;

            suppose x in Fwk;

            then

            consider w be Element of NAT such that

             A11: x = (F . w) and

             A12: A <= w and

             A13: w <= (A + k);

            w <= ((A + k) + 1) by A13, NAT_1: 13;

            hence x in Fwk1 by A11, A12;

          end;

            suppose

             A14: x in {(F . ((A + k) + 1))};

            

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

            x = (F . ((A + k) + 1)) by A14, TARSKI:def 1;

            hence x in Fwk1 by A15;

          end;

        end;

        now

          assume (F . ((A + k) + 1)) in Fwk;

          then

          consider w be Element of NAT such that

           A16: (F . ((A + k) + 1)) = (F . w) and A <= w and

           A17: w <= (A + k);

          ((A + k) + 1) = w by A1, A2, A16, FUNCT_1:def 4;

          hence contradiction by A17, NAT_1: 13;

        end;

        then ( card (Fwk \/ {(F . ((A + k) + 1))})) = ((k + 1) + 1) by A4, CARD_2: 41;

        hence thesis by A5, TARSKI: 2;

      end;

      now

        let x be object;

        hereby

          assume x in { (F . w) where w be Element of NAT : A <= w & w <= (A + 0 ) };

          then

          consider w be Element of NAT such that

           A18: (F . w) = x and

           A19: A <= w and

           A20: w <= (A + 0 );

          w = A by A19, A20, XXREAL_0: 1;

          hence x in {(F . A)} by A18, TARSKI:def 1;

        end;

        assume x in {(F . A)};

        then x = (F . A) by TARSKI:def 1;

        hence x in { (F . w) where w be Element of NAT : A <= w & w <= (A + 0 ) };

      end;

      then { (F . w) where w be Element of NAT : A <= w & w <= (A + 0 ) } = {(F . A)} by TARSKI: 2;

      then

       A21: P[ 0 ] by CARD_1: 30;

      for k be Nat holds P[k] from NAT_1:sch 2( A21, A3);

      hence thesis;

    end;

    

     Lm3: for a,b,c be Real st a < b holds ((c - b) + 1) < ((c - a) + 1)

    proof

      let a,b,c be Real;

      assume a < b;

      then (c - b) < (c - a) by XREAL_1: 10;

      hence thesis by XREAL_1: 6;

    end;

    theorem :: LEXBFS:2

    

     Th2: for n,m,k be Nat st m <= k & n < m holds (k -' m) < (k -' n)

    proof

      let n,m,k be Nat such that

       A1: m <= k and

       A2: n < m;

      

       A3: (k - m) < (k - n) by A2, XREAL_1: 15;

      (k -' n) = (k - n) by A1, A2, XREAL_1: 233, XXREAL_0: 2;

      hence thesis by A1, A3, XREAL_1: 233;

    end;

    notation

      let S be set;

      synonym S is with_finite-elements for S is finite-membered;

    end

    registration

      cluster non empty finite with_finite-elements for Subset of ( bool NAT );

      existence

      proof

        set x = { {1}};

        reconsider x as Subset of ( bool NAT );

        take x;

        thus x is non empty;

        thus x is finite;

        thus thesis;

      end;

    end

    definition

      ::$Canceled

      let f,g be Function;

      :: LEXBFS:def2

      func f .\/ g -> Function means

      : Def1: ( dom it ) = (( dom f) \/ ( dom g)) & for x be object st x in (( dom f) \/ ( dom g)) holds (it . x) = ((f . x) \/ (g . x));

      existence

      proof

        defpred P[ object, object] means ((f . $1) \/ (g . $1)) = $2;

        set A = (( dom f) \/ ( dom g));

        

         A1: for x be object st x in A holds ex y be object st P[x, y];

        ex f be Function st ( dom f) = A & for x be object st x in A holds P[x, (f . x)] from CLASSES1:sch 1( A1);

        then

        consider IT be Function such that

         A2: ( dom IT) = A and

         A3: for x be object st x in A holds P[x, (IT . x)];

        take IT;

        thus ( dom IT) = (( dom f) \/ ( dom g)) by A2;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let IT1,IT2 be Function such that

         A4: ( dom IT1) = (( dom f) \/ ( dom g)) and

         A5: for x be object st x in (( dom f) \/ ( dom g)) holds (IT1 . x) = ((f . x) \/ (g . x)) and

         A6: ( dom IT2) = (( dom f) \/ ( dom g)) and

         A7: for x be object st x in (( dom f) \/ ( dom g)) holds (IT2 . x) = ((f . x) \/ (g . x));

        now

          let x be object such that

           A8: x in ( dom IT1);

          (IT1 . x) = ((f . x) \/ (g . x)) by A4, A5, A8;

          hence (IT1 . x) = (IT2 . x) by A4, A7, A8;

        end;

        hence thesis by A4, A6, FUNCT_1: 2;

      end;

    end

    theorem :: LEXBFS:3

    

     Th3: for m,n,k be Nat holds m in (( Seg k) \ ( Seg (k -' n))) iff (k -' n) < m & m <= k

    proof

      let m,n,k be Nat;

      hereby

        assume

         A1: m in (( Seg k) \ ( Seg (k -' n)));

        then

         A2: not m in ( Seg (k -' n)) by XBOOLE_0:def 5;

        

         A3: m in ( Seg k) by A1, XBOOLE_0:def 5;

        then 1 <= m by FINSEQ_1: 1;

        hence (k -' n) < m & m <= k by A3, A2, FINSEQ_1: 1;

      end;

      assume that

       A4: (k -' n) < m and

       A5: m <= k;

      ( 0 + 1) <= m by A4, NAT_1: 13;

      then

       A6: m in ( Seg k) by A5, FINSEQ_1: 1;

       not m in ( Seg (k -' n)) by A4, FINSEQ_1: 1;

      hence thesis by A6, XBOOLE_0:def 5;

    end;

    theorem :: LEXBFS:4

    

     Th4: for n,k,m be Nat st n <= m holds (( Seg k) \ ( Seg (k -' n))) c= (( Seg k) \ ( Seg (k -' m)))

    proof

      let n,k,m be Nat such that

       A1: n <= m;

      per cases ;

        suppose

         A2: k < m;

        

         A3: for x be object st x in (( Seg k) \ ( Seg (k -' n))) holds x in ( Seg k) by XBOOLE_0:def 5;

        (k -' m) = 0 by A2, NAT_2: 8;

        then ( Seg (k -' m)) = {} ;

        hence thesis by A3;

      end;

        suppose

         A4: m <= k;

        now

          let x be object such that

           A5: x in (( Seg k) \ ( Seg (k -' n)));

          reconsider y = x as Element of NAT by A5;

          

           A6: (k -' n) < y by A5, Th3;

          per cases by A1, XXREAL_0: 1;

            suppose m = n;

            hence x in (( Seg k) \ ( Seg (k -' m))) by A5;

          end;

            suppose n < m;

            then (k -' m) < (k -' n) by A4, Th2;

            then

             A7: (k -' m) < y by A6, XXREAL_0: 2;

            y <= k by A5, Th3;

            hence x in (( Seg k) \ ( Seg (k -' m))) by A7, Th3;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: LEXBFS:5

    

     Th5: for n,k be Nat st n < k holds ((( Seg k) \ ( Seg (k -' n))) \/ {(k -' n)}) = (( Seg k) \ ( Seg (k -' (n + 1))))

    proof

      let n,k be Nat such that

       A1: n < k;

      set Sn1 = (( Seg k) \ ( Seg (k -' (n + 1))));

      set Sn = (( Seg k) \ ( Seg (k -' n)));

      now

        let x be object such that

         A2: x in (Sn \/ {(k -' n)});

        per cases by A2, XBOOLE_0:def 3;

          suppose

           A3: x in Sn;

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

          then Sn c= Sn1 by Th4;

          hence x in Sn1 by A3;

        end;

          suppose

           A4: x in {(k -' n)};

          then

          reconsider y = x as Nat;

          

           A5: n < (n + 1) by NAT_1: 13;

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

          then

           A6: (k -' (n + 1)) < (k -' n) by A5, Th2;

          

           A7: x = (k -' n) by A4, TARSKI:def 1;

          then y <= k by NAT_D: 35;

          hence x in Sn1 by A7, A6, Th3;

        end;

      end;

      then

       A8: (Sn \/ {(k -' n)}) c= Sn1;

      now

        let x be object such that

         A9: x in Sn1;

        reconsider y = x as Element of NAT by A9;

        

         A10: y <= k by A9, Th3;

        

         A11: ((k -' (n + 1)) + 1) = (k -' n) by A1, NAT_D: 59;

        (k -' (n + 1)) < y by A9, Th3;

        then

         A12: (k -' n) <= y by A11, NAT_1: 13;

        per cases by A12, XXREAL_0: 1;

          suppose (k -' n) = y;

          then y in {(k -' n)} by TARSKI:def 1;

          hence x in (Sn \/ {(k -' n)}) by XBOOLE_0:def 3;

        end;

          suppose (k -' n) < y;

          then y in Sn by A10, Th3;

          hence x in (Sn \/ {(k -' n)}) by XBOOLE_0:def 3;

        end;

      end;

      then Sn1 c= (Sn \/ {(k -' n)});

      hence thesis by A8, XBOOLE_0:def 10;

    end;

    definition

      let f be Relation;

      :: LEXBFS:def3

      attr f is natsubset-yielding means

      : Def2: ( rng f) c= ( bool NAT );

    end

    registration

      cluster finite-yielding natsubset-yielding for Function;

      existence

      proof

        set F = ( NAT --> {} );

        take F;

        for x be set st x in ( rng F) holds x is finite;

        hence F is finite-yielding by FINSET_1:def 2;

        now

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in ( rng F);

          then x = {} by TARSKI:def 1;

          then xx c= NAT ;

          hence x in ( bool NAT );

        end;

        then ( rng F) c= ( bool NAT );

        hence thesis;

      end;

    end

    definition

      let f be finite-yielding natsubset-yielding Function, x be set;

      :: original: .

      redefine

      func f . x -> finite Subset of NAT ;

      coherence

      proof

        per cases ;

          suppose

           A1: x in ( dom f);

          

           A2: ( rng f) c= ( bool NAT ) by Def2;

          (f . x) in ( rng f) by A1, FUNCT_1: 3;

          hence thesis by A2;

        end;

          suppose not x in ( dom f);

          then (f . x) = {} by FUNCT_1:def 2;

          hence thesis by XBOOLE_1: 2;

        end;

      end;

    end

    theorem :: LEXBFS:6

    

     Th6: for X be Ordinal, a,b be finite Subset of X st a <> b holds ((a,1) -bag ) <> ((b,1) -bag )

    proof

      let X be Ordinal, a,b be finite Subset of X such that

       A1: a <> b;

      assume

       A2: ((a,1) -bag ) = ((b,1) -bag );

      now

        let x be object;

        x in a iff (((b,1) -bag ) . x) = 1 by A2, UPROOTS: 6, UPROOTS: 7;

        hence x in a iff x in b by UPROOTS: 6, UPROOTS: 7;

      end;

      hence contradiction by A1, TARSKI: 2;

    end;

    definition

      let F be natural-valued Function, S be set, k be Nat;

      :: LEXBFS:def4

      func F .incSubset (S,k) -> natural-valued Function means

      : Def3: ( dom it ) = ( dom F) & for y be object holds (y in S & y in ( dom F) implies (it . y) = ((F . y) + k)) & ( not y in S implies (it . y) = (F . y));

      existence

      proof

        deffunc G( object) = ((F . $1) + k);

        consider H be Function such that

         A1: ( dom H) = (S /\ ( dom F)) and

         A2: for x be object st x in (S /\ ( dom F)) holds (H . x) = G(x) from FUNCT_1:sch 3;

        now

          let x be object;

          assume x in ( rng H);

          then

          consider y be object such that

           A3: y in ( dom H) and

           A4: (H . y) = x by FUNCT_1:def 3;

          (H . y) = ((F . y) + k) by A1, A2, A3;

          hence x in NAT by A4, ORDINAL1:def 12;

        end;

        then

         A5: ( rng H) c= NAT ;

        

         A6: ( rng (F +* H)) c= (( rng F) \/ ( rng H)) by FUNCT_4: 17;

        ( rng F) c= NAT by VALUED_0:def 6;

        then (( rng F) \/ ( rng H)) c= NAT by A5, XBOOLE_1: 8;

        then ( rng (F +* H)) c= NAT by A6;

        then

        reconsider IT = (F +* H) as natural-valued Function by VALUED_0:def 6;

        take IT;

        ( dom IT) = (( dom F) \/ (S /\ ( dom F))) by A1, FUNCT_4:def 1;

        hence ( dom IT) = ( dom F) by XBOOLE_1: 22;

        now

          let y be object;

           A7:

          now

            assume that

             A8: y in S and

             A9: y in ( dom F);

            y in ( dom H) by A1, A8, A9, XBOOLE_0:def 4;

            then

             A10: (IT . y) = (H . y) by FUNCT_4: 13;

            y in (S /\ ( dom F)) by A8, A9, XBOOLE_0:def 4;

            hence (IT . y) = ((F . y) + k) by A2, A10;

          end;

          now

            assume not y in S;

            then not y in ( dom H) by A1, XBOOLE_0:def 4;

            hence (IT . y) = (F . y) by FUNCT_4: 11;

          end;

          hence (y in S & y in ( dom F) implies (IT . y) = ((F . y) + k)) & ( not y in S implies (IT . y) = (F . y)) by A7;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be natural-valued Function such that

         A11: ( dom IT1) = ( dom F) and

         A12: for y be object holds (y in S & y in ( dom F) implies (IT1 . y) = ((F . y) + k)) & ( not y in S implies (IT1 . y) = (F . y)) and

         A13: ( dom IT2) = ( dom F) and

         A14: for y be object holds (y in S & y in ( dom F) implies (IT2 . y) = ((F . y) + k)) & ( not y in S implies (IT2 . y) = (F . y));

        now

          let x be object such that

           A15: x in ( dom IT1);

          per cases by A11, A15;

            suppose

             A16: x in S & x in ( dom F);

            then (IT1 . x) = ((F . x) + k) by A12;

            hence (IT1 . x) = (IT2 . x) by A14, A16;

          end;

            suppose

             A17: not x in S;

            then (IT1 . x) = (F . x) by A12;

            hence (IT1 . x) = (IT2 . x) by A14, A17;

          end;

        end;

        hence thesis by A11, A13, FUNCT_1: 2;

      end;

    end

    definition

      let n be Ordinal, T be connected TermOrder of n, B be non empty finite Subset of ( Bags n);

      :: LEXBFS:def5

      func max (B,T) -> bag of n means

      : Def4: it in B & for x be bag of n st x in B holds x <= (it ,T);

      existence

      proof

        consider p be FinSequence such that

         A1: ( rng p) = B by FINSEQ_1: 52;

        defpred P[ Nat] means $1 <= ( len p) implies (ex a be Nat, A be bag of n st a in ( dom p) & a <= $1 & (p . a) = A & (for c be Nat, C be bag of n st c in ( dom p) & c <= $1 & (p . c) = C holds C <= (A,T)));

        

         A2: for k be non zero Nat st P[k] holds P[(k + 1)]

        proof

          let k be non zero Nat such that

           A3: P[k];

          per cases ;

            suppose

             A4: k < ( len p);

            

             A5: 1 <= (k + 1) by CHORD: 1;

            (k + 1) <= ( len p) by A4, NAT_1: 13;

            then

             A6: (k + 1) in ( dom p) by A5, FINSEQ_3: 25;

            then (p . (k + 1)) in B by A1, FUNCT_1:def 3;

            then

            reconsider Ck = (p . (k + 1)) as bag of n;

            consider a be Nat, A be bag of n such that

             A7: a in ( dom p) and

             A8: a <= k and

             A9: (p . a) = A and

             A10: for c be Nat, C be bag of n st c in ( dom p) & c <= k & (p . c) = C holds C <= (A,T) by A3, A4;

            set m = ( max (A,Ck,T));

            

             A11: A <= (m,T) by TERMORD: 14;

            per cases by TERMORD: 12;

              suppose

               A12: m = A;

               A13:

              now

                let c be Nat, C be bag of n such that

                 A14: c in ( dom p) and

                 A15: c <= (k + 1) and

                 A16: (p . c) = C;

                per cases by A15, XXREAL_0: 1;

                  suppose c = (k + 1);

                  hence C <= (m,T) by A16, TERMORD: 14;

                end;

                  suppose c < (k + 1);

                  then c <= k by NAT_1: 13;

                  then C <= (A,T) by A10, A14, A16;

                  hence C <= (m,T) by A11, TERMORD: 8;

                end;

              end;

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

              hence thesis by A7, A9, A12, A13;

            end;

              suppose

               A17: m = Ck;

              now

                let c be Nat, C be bag of n such that

                 A18: c in ( dom p) and

                 A19: c <= (k + 1) and

                 A20: (p . c) = C;

                per cases by A19, XXREAL_0: 1;

                  suppose c = (k + 1);

                  hence C <= (m,T) by A20, TERMORD: 14;

                end;

                  suppose c < (k + 1);

                  then c <= k by NAT_1: 13;

                  then C <= (A,T) by A10, A18, A20;

                  hence C <= (m,T) by A11, TERMORD: 8;

                end;

              end;

              hence thesis by A6, A17;

            end;

          end;

            suppose k >= ( len p);

            hence thesis by NAT_1: 13;

          end;

        end;

        

         A21: p <> {} by A1;

        

         A22: P[1]

        proof

          

           A23: 1 in ( dom p) by A1, FINSEQ_3: 32;

          then (p . 1) in B by A1, FUNCT_1:def 3;

          then

          reconsider A = (p . 1) as bag of n;

          now

            let c be Nat, C be bag of n such that

             A24: c in ( dom p) and

             A25: c <= 1 and

             A26: (p . c) = C;

            1 <= c by A24, FINSEQ_3: 25;

            then C = A by A25, A26, XXREAL_0: 1;

            hence C <= (A,T) by TERMORD: 6;

          end;

          hence thesis by A23;

        end;

        for k be non zero Nat holds P[k] from NAT_1:sch 10( A22, A2);

        then

        consider a be Nat, A be bag of n such that

         A27: a in ( dom p) and a <= ( len p) and

         A28: (p . a) = A and

         A29: for c be Nat, C be bag of n st c in ( dom p) & c <= ( len p) & (p . c) = C holds C <= (A,T) by A21;

        take A;

        thus A in B by A1, A27, A28, FUNCT_1:def 3;

        now

          let x be bag of n;

          assume x in B;

          then

          consider y be Nat such that

           A30: y in ( dom p) and

           A31: (p . y) = x by A1, FINSEQ_2: 10;

          y <= ( len p) by A30, FINSEQ_3: 25;

          hence x <= (A,T) by A29, A30, A31;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be bag of n such that

         A32: IT1 in B and

         A33: for x be bag of n st x in B holds x <= (IT1,T) and

         A34: IT2 in B and

         A35: for x be bag of n st x in B holds x <= (IT2,T);

        

         A36: IT1 <= (IT2,T) by A32, A35;

        IT2 <= (IT1,T) by A33, A34;

        hence IT1 = IT2 by A36, TERMORD: 7;

      end;

    end

    registration

      let O be Ordinal;

      cluster ( InvLexOrder O) -> connected;

      coherence

      proof

        ( InvLexOrder O) is well-ordering by BAGORDER: 25;

        hence thesis by WELLORD1:def 4;

      end;

    end

    

     Lm4: for G be _Graph, W be Walk of G, e,v be object st e Joins ((W .last() ),v,G) holds ((W .addEdge e) .length() ) = ((W .length() ) + 1)

    proof

      let G be _Graph, W be Walk of G, e,v be object;

      assume e Joins ((W .last() ),v,G);

      then

       A1: ((W .addEdge e) .edgeSeq() ) = ((W .edgeSeq() ) ^ <*e*>) by GLIB_001: 82;

      ( len <*e*>) = 1 by FINSEQ_1: 39;

      hence thesis by A1, FINSEQ_1: 22;

    end;

    

     Lm5: for G be _Graph, W be Walk of G holds (W .length() ) = ((W .reverse() ) .length() )

    proof

      let G be _Graph, W be Walk of G;

      

       A1: ( len W) = ((2 * (W .length() )) + 1) by GLIB_001: 112;

      ( len W) = ( len (W .reverse() )) by GLIB_001: 21;

      then (((2 * (W .length() )) + 1) - 1) = (((2 * ((W .reverse() ) .length() )) + 1) - 1) by A1, GLIB_001: 112;

      hence thesis;

    end;

    

     Lm6: for G be _Graph, W be Walk of G holds for e,x be object st e Joins ((W .last() ),x,G) holds for n be Nat st n in ( dom W) holds ((W .addEdge e) . n) = (W . n) & n in ( dom (W .addEdge e))

    proof

      let G be _Graph, W be Walk of G;

      let e,x be object such that

       A1: e Joins ((W .last() ),x,G);

      let n be Nat such that

       A2: n in ( dom W);

      thus ((W .addEdge e) . n) = (W . n) by A1, A2, GLIB_001: 65;

      

       A3: 1 <= n by A2, FINSEQ_3: 25;

      

       A4: ( len W) < (( len W) + 2) by XREAL_1: 29;

      n <= ( len W) by A2, FINSEQ_3: 25;

      then

       A5: n <= (( len W) + 2) by A4, XXREAL_0: 2;

      ( len (W .addEdge e)) = (( len W) + 2) by A1, GLIB_001: 64;

      hence thesis by A3, A5, FINSEQ_3: 25;

    end;

    begin

    definition

      let s be ManySortedSet of NAT ;

      :: LEXBFS:def6

      attr s is iterative means

      : Def5: for k,n be Nat st (s . k) = (s . n) holds (s . (k + 1)) = (s . (n + 1));

    end

    definition

      let S be ManySortedSet of NAT ;

      :: LEXBFS:def7

      attr S is eventually-constant means

      : Def6: ex n be Nat st for m be Nat st n <= m holds (S . n) = (S . m);

    end

    registration

      cluster halting iterative eventually-constant for ManySortedSet of NAT ;

      existence

      proof

        set Fa = ( NAT --> 1);

        reconsider F = Fa as ManySortedSet of NAT ;

        take F;

        (F . 0 ) = (F . ( 0 + 1));

        hence F is halting;

        thus F is iterative;

        for n be Nat st 0 <= n holds (F . 0 ) = (F . n) by FUNCOP_1: 7, ORDINAL1:def 12;

        hence thesis;

      end;

    end

    theorem :: LEXBFS:7

    

     Th7: for Gs be ManySortedSet of NAT st Gs is halting & Gs is iterative holds Gs is eventually-constant

    proof

      let Gs be ManySortedSet of NAT such that

       A1: Gs is halting and

       A2: Gs is iterative;

      set GL = (Gs .Lifespan() );

      defpred P[ Nat] means (Gs . GL) = (Gs . (GL + $1));

      

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

      proof

        let k be Nat;

        assume P[k];

        then (Gs . (GL + 1)) = (Gs . ((GL + k) + 1)) by A2;

        hence thesis by A1, GLIB_000:def 56;

      end;

      

       A4: P[ 0 ];

      

       A5: for k be Nat holds P[k] from NAT_1:sch 2( A4, A3);

      now

        let n be Nat;

        assume GL <= n;

        then ex i be Nat st (GL + i) = n by NAT_1: 10;

        hence (Gs . GL) = (Gs . n) by A5;

      end;

      hence thesis;

    end;

    registration

      cluster halting iterative -> eventually-constant for ManySortedSet of NAT ;

      coherence by Th7;

    end

    theorem :: LEXBFS:8

    

     Th8: for Gs be ManySortedSet of NAT st Gs is eventually-constant holds Gs is halting

    proof

      let Gs be ManySortedSet of NAT ;

      assume Gs is eventually-constant;

      then

      consider n be Nat such that

       A1: for m be Nat st n <= m holds (Gs . n) = (Gs . m);

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

      then (Gs . n) = (Gs . (n + 1)) by A1;

      hence thesis;

    end;

    registration

      cluster eventually-constant -> halting for ManySortedSet of NAT ;

      coherence by Th8;

    end

    theorem :: LEXBFS:9

    

     Th9: for Gs be iterative eventually-constant ManySortedSet of NAT holds for n be Nat st (Gs .Lifespan() ) <= n holds (Gs . (Gs .Lifespan() )) = (Gs . n)

    proof

      let Gs be iterative eventually-constant ManySortedSet of NAT ;

      set GL = (Gs .Lifespan() );

      defpred P[ Nat] means (Gs . GL) = (Gs . (GL + $1));

      let n be Nat;

      assume GL <= n;

      then

       A1: ex i be Nat st (GL + i) = n by NAT_1: 10;

      

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

      proof

        let k be Nat;

        assume P[k];

        then (Gs . (GL + 1)) = (Gs . ((GL + k) + 1)) by Def5;

        hence thesis by GLIB_000:def 56;

      end;

      

       A3: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A3, A2);

      hence thesis by A1;

    end;

    theorem :: LEXBFS:10

    

     Th10: for Gs be iterative eventually-constant ManySortedSet of NAT holds for n,m be Nat st (Gs .Lifespan() ) <= n & n <= m holds (Gs . m) = (Gs . n)

    proof

      let Gs be iterative eventually-constant ManySortedSet of NAT ;

      let n,m be Nat such that

       A1: (Gs .Lifespan() ) <= n and

       A2: n <= m;

      (Gs . (Gs .Lifespan() )) = (Gs . m) by A1, A2, Th9, XXREAL_0: 2;

      hence thesis by A1, Th9;

    end;

    begin

    definition

      let G be _finite _Graph;

      :: LEXBFS:def8

      mode preVNumberingSeq of G -> ManySortedSet of NAT means

      : Def7: for i be Nat holds (it . i) is PartFunc of ( the_Vertices_of G), NAT ;

      existence

      proof

        deffunc F( object) = {} ;

        consider f be ManySortedSet of NAT such that

         A1: for i be object st i in NAT holds (f . i) = F(i) from PBOOLE:sch 4;

        take f;

        let i be Nat;

        i in NAT by ORDINAL1:def 12;

        then (f . i) = {} by A1;

        hence thesis by RELSET_1: 12;

      end;

    end

    definition

      let G be _finite _Graph, S be preVNumberingSeq of G, n be Nat;

      :: original: .

      redefine

      func S . n -> PartFunc of ( the_Vertices_of G), NAT ;

      coherence by Def7;

    end

    definition

      let G be _finite _Graph, S be preVNumberingSeq of G;

      :: LEXBFS:def9

      attr S is vertex-numbering means

      : Def8: (S . 0 ) = {} & S is iterative & S is halting & (S .Lifespan() ) = (G .order() ) & for n be Nat st n < (S .Lifespan() ) holds ex w be Vertex of G st not w in ( dom (S . n)) & (S . (n + 1)) = ((S . n) +* (w .--> ((S .Lifespan() ) -' n)));

    end

    registration

      let G be _finite _Graph;

      cluster vertex-numbering for preVNumberingSeq of G;

      existence

      proof

        set N = ( card ( the_Vertices_of G));

        set vs = ( canFS ( the_Vertices_of G));

        deffunc F( Element of NAT ) = ((N -' $1) + 1);

        consider s be sequence of NAT such that

         A1: for n be Element of NAT holds (s . n) = F(n) from FUNCT_2:sch 4;

        defpred P[ object, object] means ex n be Nat st $1 = n & $2 = (s * ((vs | ( Seg n)) " ));

        

         A2: for n be object st n in NAT holds ex j be object st P[n, j]

        proof

          let n be object;

          assume n in NAT ;

          then

          reconsider n9 = n as Nat;

          take (s * ((vs | ( Seg n9)) " ));

          thus thesis;

        end;

        consider S be ManySortedSet of NAT such that

         A3: for n be object st n in NAT holds P[n, (S . n)] from PBOOLE:sch 3( A2);

        

         A4: for n be Nat holds (S . n) = (s * ((vs | ( Seg n)) " ))

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          then ex i9 be Nat st n = i9 & (S . n) = (s * ((vs | ( Seg i9)) " )) by A3;

          hence thesis;

        end;

        

         A5: for n be Nat st n >= ( len vs) holds (S . n) = (s * (vs " ))

        proof

          

           A6: ( dom vs) = ( Seg ( len vs)) by FINSEQ_1:def 3;

          let n be Nat;

          assume n >= ( len vs);

          then ( dom vs) c= ( Seg n) by A6, FINSEQ_1: 5;

          then (vs | ( Seg n)) = vs by RELAT_1: 68;

          hence thesis by A4;

        end;

         A7:

        now

          let i be Nat;

          set Si = (s * ((vs | ( Seg i)) " ));

          

           A8: ( rng Si) c= NAT ;

          (vs | ( Seg i)) is one-to-one by FUNCT_1: 52;

          then

           A9: ((vs | ( Seg i)) ~ ) = ((vs | ( Seg i)) " ) by FUNCT_1:def 5;

          now

            let x be object;

            assume x in ( dom Si);

            then x in ( dom ((vs | ( Seg i)) " )) by FUNCT_1: 11;

            then x in ( rng (vs | ( Seg i))) by A9, RELAT_1: 20;

            hence x in ( the_Vertices_of G);

          end;

          then

           A10: ( dom Si) c= ( the_Vertices_of G);

          (S . i) = (s * ((vs | ( Seg i)) " )) by A4;

          hence (S . i) is PartFunc of ( the_Vertices_of G), NAT by A10, A8, RELSET_1: 4;

        end;

        

         A11: ( dom s) = NAT by FUNCT_2:def 1;

        

         A12: for n be Nat st n <= ( len vs) holds ( card (S . n)) = n

        proof

          let n be Nat;

          assume n <= ( len vs);

          then

           A13: ( Seg n) c= ( Seg ( len vs)) by FINSEQ_1: 5;

          

           A14: (vs | ( Seg n)) is one-to-one by FUNCT_1: 52;

          

           A15: (S . n) = (s * ((vs | ( Seg n)) " )) by A4;

          

           A16: ( card ( Seg n)) = n by FINSEQ_1: 57;

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

          then

           A17: ( dom (vs | ( Seg n))) = ( Seg n) by A13, RELAT_1: 62;

          then ( rng ((vs | ( Seg n)) " )) = ( Seg n) by A14, FUNCT_1: 33;

          

          then ( dom (s * ((vs | ( Seg n)) " ))) = ( dom ((vs | ( Seg n)) " )) by A11, RELAT_1: 27

          .= ( rng (vs | ( Seg n))) by A14, FUNCT_1: 33;

          then ( card ( dom (s * ((vs | ( Seg n)) " )))) = n by A14, A17, A16, CARD_1: 70;

          hence thesis by A15, CARD_1: 62;

        end;

        reconsider S as preVNumberingSeq of G by A7, Def7;

        

         A18: ( len vs) = N by FINSEQ_1: 93;

        

         A19: S is iterative

        proof

          

           A20: for k,n be Nat st k < n & (S . k) = (S . n) holds (S . (k + 1)) = (S . (n + 1))

          proof

            let k,n be Nat such that

             A21: k < n and

             A22: (S . k) = (S . n);

            per cases ;

              suppose

               A23: n < N;

              then ( card (S . n)) = n by A18, A12;

              hence thesis by A18, A12, A21, A22, A23, XXREAL_0: 2;

            end;

              suppose

               A24: N <= n;

              per cases ;

                suppose

                 A25: k < N;

                

                 A26: ( rng (vs " )) c= ( dom s)

                proof

                  let x be object;

                  assume x in ( rng (vs " ));

                  then x in ( rng (vs qua Relation ~ )) by FUNCT_1:def 5;

                  then x in ( dom vs) by RELAT_1: 20;

                  then x in NAT ;

                  hence thesis by FUNCT_2:def 1;

                end;

                

                 A27: (S . n) = ((vs " ) qua Relation * s) by A18, A5, A24;

                ( card (S . n)) = ( card ( dom (S . n))) by CARD_1: 62

                .= ( card ( dom (vs " ))) by A27, A26, RELAT_1: 27

                .= ( card ( rng vs)) by FUNCT_1: 33

                .= ( card ( dom vs)) by CARD_1: 70

                .= ( len vs) by CARD_1: 62;

                hence thesis by A18, A12, A22, A25;

              end;

                suppose

                 A28: k >= N;

                

                 A29: (n + 1) >= N by A24, NAT_1: 13;

                (k + 1) >= N by A28, NAT_1: 13;

                

                hence (S . (k + 1)) = (s * (vs " )) by A18, A5

                .= (S . (n + 1)) by A18, A5, A29;

              end;

            end;

          end;

          let k,n be Nat such that

           A30: (S . k) = (S . n);

          per cases by XXREAL_0: 1;

            suppose k < n;

            hence (S . (k + 1)) = (S . (n + 1)) by A20, A30;

          end;

            suppose k > n;

            hence (S . (k + 1)) = (S . (n + 1)) by A20, A30;

          end;

            suppose k = n;

            hence thesis;

          end;

        end;

        reconsider N as Element of NAT ;

        

         A31: N <= (N + 1) by NAT_1: 11;

        

         A32: N >= ( len vs) by FINSEQ_1: 93;

        

        then

         A33: (S . N) = (s * (vs " )) by A5

        .= (S . (N + 1)) by A5, A32, A31, XXREAL_0: 2;

        then

         A34: S is halting;

        

         A35: for n be Nat st (S . n) = (S . (n + 1)) holds N <= n

        proof

          let n be Nat such that

           A36: (S . n) = (S . (n + 1)) and

           A37: N > n;

          

           A38: (n + 1) <= N by A37, NAT_1: 13;

          n = ( card (S . (n + 1))) by A18, A12, A36, A37

          .= (n + 1) by A18, A12, A38;

          hence thesis;

        end;

        then

         A39: (S .Lifespan() ) = (G .order() ) by A33, A34, GLIB_000:def 56;

         A40:

        now

          let n be Nat such that

           A41: n < (S .Lifespan() );

          n < N by A33, A34, A35, A41, GLIB_000:def 56;

          then

           A42: (n + 1) <= N by NAT_1: 13;

          set w = (vs . (n + 1));

          

           A43: ( 0 + 1) <= (n + 1) by NAT_1: 13;

          (n + 1) <= ( len vs) by A42, FINSEQ_1: 93;

          then

           A44: (n + 1) in ( dom vs) by A43, FINSEQ_3: 25;

          then w in ( rng vs) by FUNCT_1: 3;

          then

          reconsider w as Vertex of G;

          take w;

          

           A45: (vs | ( Seg n)) is one-to-one by FUNCT_1: 52;

          hereby

            assume w in ( dom (S . n));

            then w in ( dom (s * ((vs | ( Seg n)) " ))) by A4;

            then w in ( dom ((vs | ( Seg n)) " )) by FUNCT_1: 11;

            then w in ( rng (vs | ( Seg n))) by A45, FUNCT_1: 33;

            then

            consider x be object such that

             A46: x in ( dom (vs | ( Seg n))) and

             A47: w = ((vs | ( Seg n)) . x) by FUNCT_1:def 3;

            

             A48: w = (vs . x) by A46, A47, FUNCT_1: 47;

            

             A49: x in ( Seg n) by A46, RELAT_1: 57;

            

             A50: x in ( dom vs) by A46, RELAT_1: 57;

            reconsider x as Nat by A46;

            x <= n by A49, FINSEQ_1: 1;

            then x <> (n + 1) by NAT_1: 13;

            hence contradiction by A44, A48, A50, FUNCT_1:def 4;

          end;

          

           A51: (vs | ( Seg (n + 1))) is one-to-one by FUNCT_1: 52;

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

          then

           A52: ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5;

          now

            now

              let x be object;

              hereby

                assume x in ( dom (S . (n + 1)));

                then x in ( dom (s * ((vs | ( Seg (n + 1))) " ))) by A4;

                then x in ( dom ((vs | ( Seg (n + 1))) " )) by FUNCT_1: 11;

                then x in ( rng (vs | ( Seg (n + 1)))) by A51, FUNCT_1: 33;

                then

                consider a be object such that

                 A53: a in ( dom (vs | ( Seg (n + 1)))) and

                 A54: x = ((vs | ( Seg (n + 1))) . a) by FUNCT_1:def 3;

                

                 A55: a in ( Seg (n + 1)) by A53, RELAT_1: 57;

                

                 A56: ( dom ((S . n) +* (w .--> ((S .Lifespan() ) -' n)))) = (( dom (S . n)) \/ ( dom (w .--> ((S .Lifespan() ) -' n)))) by FUNCT_4:def 1;

                reconsider a as Nat by A53;

                

                 A57: a in ( dom vs) by A53, RELAT_1: 57;

                

                 A58: a <= (n + 1) by A55, FINSEQ_1: 1;

                

                 A59: 1 <= a by A55, FINSEQ_1: 1;

                per cases by A58, NAT_1: 8;

                  suppose a <= n;

                  then

                   A60: a in ( Seg n) by A59, FINSEQ_1: 1;

                  then

                   A61: a in ( dom (vs | ( Seg n))) by A57, RELAT_1: 57;

                  

                   A62: ((vs | ( Seg n)) . a) = (vs . a) by A60, FUNCT_1: 49

                  .= x by A54, A55, FUNCT_1: 49;

                  then x in ( rng (vs | ( Seg n))) by A61, FUNCT_1: 3;

                  then

                   A63: x in ( dom ((vs | ( Seg n)) " )) by A45, FUNCT_1: 33;

                  (((vs | ( Seg n)) " ) . x) = a by A45, A61, A62, FUNCT_1: 32;

                  then (((vs | ( Seg n)) " ) . x) in ( dom s) by A11, ORDINAL1:def 12;

                  then x in ( dom (s * ((vs | ( Seg n)) " ))) by A63, FUNCT_1: 11;

                  then x in ( dom (S . n)) by A4;

                  hence x in ( dom ((S . n) +* (w .--> ((S .Lifespan() ) -' n)))) by A56, XBOOLE_0:def 3;

                end;

                  suppose a = (n + 1);

                  then x = w by A53, A54, FUNCT_1: 47;

                  then x in ( dom (w .--> ((S .Lifespan() ) -' n))) by FUNCOP_1: 74;

                  hence x in ( dom ((S . n) +* (w .--> ((S .Lifespan() ) -' n)))) by A56, XBOOLE_0:def 3;

                end;

              end;

              assume x in ( dom ((S . n) +* (w .--> ((S .Lifespan() ) -' n))));

              then

               A64: x in (( dom (S . n)) \/ ( dom (w .--> ((S .Lifespan() ) -' n)))) by FUNCT_4:def 1;

              per cases by A64, XBOOLE_0:def 3;

                suppose

                 A65: x in ( dom (S . n));

                (vs | ( Seg n)) c= (vs | ( Seg (n + 1))) by A52, RELAT_1: 75;

                then

                 A66: ( rng (vs | ( Seg n))) c= ( rng (vs | ( Seg (n + 1)))) by RELAT_1: 11;

                

                 A67: x in ( dom (s * ((vs | ( Seg n)) " ))) by A4, A65;

                then

                 A68: x in ( dom ((vs | ( Seg n)) " )) by FUNCT_1: 11;

                then x in ( rng (vs | ( Seg n))) by A45, FUNCT_1: 33;

                then x in ( rng (vs | ( Seg (n + 1)))) by A66;

                then

                 A69: x in ( dom ((vs | ( Seg (n + 1))) " )) by A51, FUNCT_1: 33;

                

                 A70: (((vs | ( Seg n)) " ) . x) in ( dom s) by A67, FUNCT_1: 11;

                (((vs | ( Seg n)) " ) . x) = (((vs | ( Seg (n + 1))) " ) . x) by A52, A68, Lm2;

                then x in ( dom (s * ((vs | ( Seg (n + 1))) " ))) by A70, A69, FUNCT_1: 11;

                hence x in ( dom (S . (n + 1))) by A4;

              end;

                suppose

                 A71: x in ( dom (w .--> ((S .Lifespan() ) -' n)));

                

                 A72: ( rng ((vs | ( Seg (n + 1))) " )) = ( dom (vs | ( Seg (n + 1)))) by A51, FUNCT_1: 33;

                x = w by A71, FUNCOP_1: 75;

                then x in ( rng (vs | ( Seg (n + 1)))) by A44, FINSEQ_1: 4, FUNCT_1: 50;

                then

                 A73: x in ( dom ((vs | ( Seg (n + 1))) " )) by A51, FUNCT_1: 33;

                then (((vs | ( Seg (n + 1))) " ) . x) in ( rng ((vs | ( Seg (n + 1))) " )) by FUNCT_1: 3;

                then x in ( dom (s * ((vs | ( Seg (n + 1))) " ))) by A11, A73, A72, FUNCT_1: 11;

                hence x in ( dom (S . (n + 1))) by A4;

              end;

            end;

            hence

             A74: ( dom (S . (n + 1))) = ( dom ((S . n) +* (w .--> ((S .Lifespan() ) -' n)))) by TARSKI: 2;

            let x be object such that

             A75: x in ( dom (S . (n + 1)));

            

             A76: x in (( dom (S . n)) \/ ( dom (w .--> ((S .Lifespan() ) -' n)))) by A74, A75, FUNCT_4:def 1;

            

             A77: (S . (n + 1)) = (s * ((vs | ( Seg (n + 1))) " )) by A4;

            

             A78: (S . n) = (s * ((vs | ( Seg n)) " )) by A4;

            per cases by A76, XBOOLE_0:def 3;

              suppose

               A79: x in ( dom (S . n));

              then

               A80: x in ( dom ((vs | ( Seg n)) " )) by A78, FUNCT_1: 11;

              then x in ( rng (vs | ( Seg n))) by A45, FUNCT_1: 33;

              then

              consider m be object such that

               A81: m in ( dom (vs | ( Seg n))) and

               A82: ((vs | ( Seg n)) . m) = x by FUNCT_1:def 3;

              

               A83: m in ( Seg n) by A81, RELAT_1: 57;

              reconsider m as Nat by A81;

              

               A84: m in ( dom vs) by A81, RELAT_1: 57;

              m <= n by A83, FINSEQ_1: 1;

              then

               A85: m < (n + 1) by NAT_1: 13;

              (vs . m) = x by A81, A82, FUNCT_1: 47;

              then

               A86: x <> w by A44, A84, A85, FUNCT_1:def 4;

              

              thus ((S . (n + 1)) . x) = (s . (((vs | ( Seg (n + 1))) " ) . x)) by A75, A77, FUNCT_1: 12

              .= (s . (((vs | ( Seg n)) " ) . x)) by A52, A80, Lm2

              .= ((S . n) . x) by A78, A79, FUNCT_1: 12

              .= (((S . n) +* (w .--> ((S .Lifespan() ) -' n))) . x) by A86, FUNCT_4: 83;

            end;

              suppose

               A87: x in ( dom (w .--> ((S .Lifespan() ) -' n)));

              (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

              then

               A88: (n + 1) in ( dom (vs | ( Seg (n + 1)))) by A44, RELAT_1: 57;

              then

               A89: ((vs | ( Seg (n + 1))) . (n + 1)) = w by FUNCT_1: 47;

              

               A90: x = w by A87, FUNCOP_1: 75;

              then x in ( rng (vs | ( Seg (n + 1)))) by A44, FINSEQ_1: 4, FUNCT_1: 50;

              then

               A91: x in ( dom ((vs | ( Seg (n + 1))) " )) by A51, FUNCT_1: 33;

              

               A92: (((S . n) +* (w .--> ((S .Lifespan() ) -' n))) . x) = ((w .--> ((S .Lifespan() ) -' n)) . x) by A87, FUNCT_4: 13

              .= ((S .Lifespan() ) -' n) by A90, FUNCOP_1: 72;

              ((S . (n + 1)) . x) = ((s * ((vs | ( Seg (n + 1))) " )) . x) by A4

              .= (s . (((vs | ( Seg (n + 1))) " ) . x)) by A91, FUNCT_1: 13

              .= (s . (n + 1)) by A51, A90, A88, A89, FUNCT_1: 32

              .= ((N -' (n + 1)) + 1) by A1

              .= ((N - (n + 1)) + 1) by A42, XREAL_1: 233

              .= (N - n)

              .= ((S .Lifespan() ) -' n) by A39, A41, XREAL_1: 233;

              hence ((S . (n + 1)) . x) = (((S . n) +* (w .--> ((S .Lifespan() ) -' n))) . x) by A92;

            end;

          end;

          hence (S . (n + 1)) = ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) by FUNCT_1: 2;

        end;

        take S;

        ( card (S . 0 )) = 0 by A12;

        then (S . 0 ) = {} ;

        hence thesis by A19, A34, A39, A40;

      end;

    end

    registration

      let G be _finite _Graph;

      cluster vertex-numbering -> halting iterative for preVNumberingSeq of G;

      correctness ;

    end

    definition

      let G be _finite _Graph;

      mode VNumberingSeq of G is vertex-numbering preVNumberingSeq of G;

    end

    definition

      let G be _finite _Graph, S be VNumberingSeq of G, n be Nat;

      :: LEXBFS:def10

      func S .PickedAt (n) -> set means

      : Def9: it = the Element of ( the_Vertices_of G) if n >= (S .Lifespan() )

      otherwise not it in ( dom (S . n)) & (S . (n + 1)) = ((S . n) +* (it .--> ((S .Lifespan() ) -' n)));

      existence

      proof

        per cases ;

          suppose n >= (S .Lifespan() );

          hence thesis;

        end;

          suppose n < (S .Lifespan() );

          then ex w be Vertex of G st ( not w in ( dom (S . n))) & (S . (n + 1)) = ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) by Def8;

          hence thesis;

        end;

      end;

      uniqueness

      proof

        set VL1 = (S . (n + 1));

        set VLN = (S . n);

        let IT1,IT2 be set;

        thus n >= (S .Lifespan() ) & IT1 = the Element of ( the_Vertices_of G) & IT2 = the Element of ( the_Vertices_of G) implies IT1 = IT2;

        assume n < (S .Lifespan() );

        assume that

         A1: not IT1 in ( dom VLN) and

         A2: VL1 = (VLN +* (IT1 .--> ((S .Lifespan() ) -' n)));

        set f2 = (IT2 .--> ((S .Lifespan() ) -' n));

        set f1 = (IT1 .--> ((S .Lifespan() ) -' n));

        assume that not IT2 in ( dom VLN) and

         A3: VL1 = (VLN +* (IT2 .--> ((S .Lifespan() ) -' n)));

        ( dom f2) = {IT2};

        then

         A4: ( dom VL1) = (( dom VLN) \/ {IT2}) by A3, FUNCT_4:def 1;

        ( dom f1) = {IT1};

        then

         A5: ( dom VL1) = (( dom VLN) \/ {IT1}) by A2, FUNCT_4:def 1;

        now

          assume IT1 <> IT2;

          then not IT1 in {IT2} by TARSKI:def 1;

          then

           A6: not IT1 in ( dom VL1) by A1, A4, XBOOLE_0:def 3;

          IT1 in {IT1} by TARSKI:def 1;

          hence contradiction by A5, A6, XBOOLE_0:def 3;

        end;

        hence thesis;

      end;

      consistency ;

    end

    theorem :: LEXBFS:11

    

     Th11: for G be _finite _Graph, S be VNumberingSeq of G, n be Nat st n < (S .Lifespan() ) holds (S .PickedAt n) in ( dom (S . (n + 1))) & ( dom (S . (n + 1))) = (( dom (S . n)) \/ {(S .PickedAt n)})

    proof

      let G be _finite _Graph, GS be VNumberingSeq of G, n be Nat such that

       A1: n < (GS .Lifespan() );

      set f = ((GS .PickedAt n) .--> ((GS .Lifespan() ) -' n));

      set CN1 = (GS . (n + 1));

      set CSN = (GS . n);

      set VLN = CSN;

      set VN1 = CN1;

      

       A2: ( dom f) = {(GS .PickedAt n)};

      

       A3: (GS .PickedAt n) in {(GS .PickedAt n)} by TARSKI:def 1;

      

       A4: VN1 = (VLN +* ((GS .PickedAt n) .--> ((GS .Lifespan() ) -' n))) by A1, Def9;

      then ( dom VN1) = (( dom VLN) \/ {(GS .PickedAt n)}) by A2, FUNCT_4:def 1;

      hence (GS .PickedAt n) in ( dom CN1) by A3, XBOOLE_0:def 3;

      thus thesis by A4, A2, FUNCT_4:def 1;

    end;

    theorem :: LEXBFS:12

    

     Th12: for G be _finite _Graph, S be VNumberingSeq of G, n be Nat st n < (S .Lifespan() ) holds ((S . (n + 1)) . (S .PickedAt n)) = ((S .Lifespan() ) -' n)

    proof

      let G be _finite _Graph, GS be VNumberingSeq of G, n be Nat such that

       A1: n < (GS .Lifespan() );

      set w = (GS .PickedAt n);

      set CN1 = (GS . (n + 1));

      set CSN = (GS . n);

      set VLN = CSN;

      set VN1 = CN1;

      set f = (w .--> ((GS .Lifespan() ) -' n));

      

       A2: (f . w) = ((GS .Lifespan() ) -' n) by FUNCOP_1: 72;

      

       A3: w in ( dom f) by TARSKI:def 1;

      VN1 = (VLN +* (w .--> ((GS .Lifespan() ) -' n))) by A1, Def9;

      hence thesis by A3, A2, FUNCT_4: 13;

    end;

    theorem :: LEXBFS:13

    for G be _finite _Graph, S be VNumberingSeq of G, n be Nat st n <= (S .Lifespan() ) holds ( card ( dom (S . n))) = n

    proof

      let G be _finite _Graph, S be VNumberingSeq of G, n be Nat such that

       A1: n <= (S .Lifespan() );

      defpred P[ Nat] means $1 <= (S .Lifespan() ) implies ( card ( dom (S . $1))) = $1;

      

       A2: for k be Nat st k < (S .Lifespan() ) & ( card ( dom (S . k))) = k holds ( card ( dom (S . (k + 1)))) = (k + 1)

      proof

        let k be Nat such that

         A3: k < (S .Lifespan() ) and

         A4: ( card ( dom (S . k))) = k;

        set w = (S .PickedAt k);

        set CK1 = (S . (k + 1));

        set CSK = (S . k);

        set VLK = CSK;

        set VK1 = CK1;

        set wf = (w .--> ((S .Lifespan() ) -' k));

        

         A5: ( dom wf) = {w};

        VK1 = (VLK +* (w .--> ((S .Lifespan() ) -' k))) by A3, Def9;

        then

         A6: ( dom VK1) = (( dom VLK) \/ {w}) by A5, FUNCT_4:def 1;

         not w in ( dom VLK) by A3, Def9;

        hence thesis by A4, A6, CARD_2: 41;

      end;

      

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

      proof

        let k be Nat such that

         A8: P[k];

        per cases ;

          suppose k < (S .Lifespan() );

          hence thesis by A2, A8;

        end;

          suppose k >= (S .Lifespan() );

          hence thesis by NAT_1: 13;

        end;

      end;

      

       A9: P[ 0 ] by Def8, CARD_1: 27, RELAT_1: 38;

      for k be Nat holds P[k] from NAT_1:sch 2( A9, A7);

      hence thesis by A1;

    end;

    theorem :: LEXBFS:14

    

     Th14: for G be _finite _Graph, S be VNumberingSeq of G, n be Nat holds ( rng (S . n)) = (( Seg (S .Lifespan() )) \ ( Seg ((S .Lifespan() ) -' n)))

    proof

      let G be _finite _Graph, S be VNumberingSeq of G, n be Nat;

      set CSN = (S . n);

      set CSO = (S . (S .Lifespan() ));

      set GN = (S .Lifespan() );

      defpred P[ Nat] means $1 <= GN implies ( rng (S . $1)) = (( Seg GN) \ ( Seg (GN -' $1)));

      

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

      proof

        let k be Nat such that

         A2: P[k];

        set CK1 = (S . (k + 1));

        set CSK = (S . k);

        set VLK = CSK;

        set VK1 = CK1;

        per cases ;

          suppose

           A3: (k + 1) <= GN;

          set w = (S .PickedAt k);

          set wf = (w .--> (GN -' k));

          

           A5: k < GN by A3, NAT_1: 13;

          then not w in ( dom VLK) by Def9;

          then

           A6: ( dom wf) misses ( dom VLK) by ZFMISC_1: 50;

          

           A7: ( rng wf) = {(GN -' k)} by FUNCOP_1: 8;

          VK1 = (VLK +* (w .--> (GN -' k))) by A5, Def9;

          then ( rng VK1) = (( rng VLK) \/ {(GN -' k)}) by A7, A6, NECKLACE: 6;

          hence thesis by A2, A5, Th5;

        end;

          suppose GN < (k + 1);

          hence thesis;

        end;

      end;

      

       A8: P[ 0 ]

      proof

        set CS0 = (S . 0 );

        set VL0 = CS0;

        

         A9: (GN -' 0 ) = (GN - 0 ) by XREAL_1: 233;

        ( rng VL0) = {} by Def8, RELAT_1: 38;

        hence thesis by A9, XBOOLE_1: 37;

      end;

      

       A10: for k be Nat holds P[k] from NAT_1:sch 2( A8, A1);

      per cases ;

        suppose n <= GN;

        hence thesis by A10;

      end;

        suppose

         A11: GN < n;

        then (GN - n) < (n - n) by XREAL_1: 9;

        then (GN -' n) = 0 by XREAL_0:def 2;

        then

         A12: (GN -' GN) = (GN -' n) by XREAL_1: 232;

        CSO = CSN by A11, Th9;

        hence thesis by A10, A12;

      end;

    end;

    theorem :: LEXBFS:15

    

     Th15: for G be _finite _Graph, S be VNumberingSeq of G, n be Nat, x be set holds ((S . n) . x) <= (S .Lifespan() ) & (x in ( dom (S . n)) implies 1 <= ((S . n) . x))

    proof

      let G be _finite _Graph, S be VNumberingSeq of G, n be Nat, x be set;

      set CSN = (S . n);

      set VLN = CSN;

       A1:

      now

        per cases ;

          suppose not x in ( dom VLN);

          hence (VLN . x) <= (S .Lifespan() ) by FUNCT_1:def 2;

        end;

          suppose x in ( dom VLN);

          then (VLN . x) in ( rng VLN) by FUNCT_1:def 3;

          then (VLN . x) in (( Seg (S .Lifespan() )) \ ( Seg ((S .Lifespan() ) -' n))) by Th14;

          hence (VLN . x) <= (S .Lifespan() ) by Th3;

        end;

      end;

      now

        assume x in ( dom (S . n));

        then (VLN . x) in ( rng VLN) by FUNCT_1:def 3;

        then (VLN . x) in (( Seg (S .Lifespan() )) \ ( Seg ((S .Lifespan() ) -' n))) by Th14;

        then ((S .Lifespan() ) -' n) < (VLN . x) by Th3;

        then ( 0 + 1) <= (VLN . x) by NAT_1: 13;

        hence 1 <= (VLN . x);

      end;

      hence thesis by A1;

    end;

    theorem :: LEXBFS:16

    

     Th16: for G be _finite _Graph, S be VNumberingSeq of G, n,m be Nat st ((S .Lifespan() ) -' n) < m & m <= (S .Lifespan() ) holds ex v be Vertex of G st v in ( dom (S . n)) & ((S . n) . v) = m

    proof

      let G be _finite _Graph, S be VNumberingSeq of G, n,m be Nat such that

       A1: ((S .Lifespan() ) -' n) < m and

       A2: m <= (S .Lifespan() );

      set CSN = (S . n);

      set VLN = CSN;

      m in (( Seg (S .Lifespan() )) \ ( Seg ((S .Lifespan() ) -' n))) by A1, A2, Th3;

      then m in ( rng VLN) by Th14;

      then

      consider v be object such that

       A3: v in ( dom VLN) and

       A4: m = (VLN . v) by FUNCT_1:def 3;

      reconsider v as set by TARSKI: 1;

      take v;

      thus v is Vertex of G by A3;

      thus v in ( dom CSN) by A3;

      thus thesis by A4;

    end;

    theorem :: LEXBFS:17

    

     Th17: for G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat st m <= n holds (S . m) c= (S . n)

    proof

      let G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat;

      assume m <= n;

      then

       A1: ex j be Nat st n = (m + j) by NAT_1: 10;

      set CSM = (S . m);

      set VLM = CSM;

      defpred P[ Nat] means VLM c= (S . (m + $1));

       A2:

      now

        let k be Nat;

        set CSK = (S . k);

        set VLK = CSK;

        set CK1 = (S . (k + 1));

        set VK1 = CK1;

        per cases ;

          suppose

           A3: k < (S .Lifespan() );

          set w = (S .PickedAt k);

          set wf = (w .--> ((S .Lifespan() ) -' k));

           not w in ( dom VLK) by A3, Def9;

          then

           A5: ( dom wf) misses ( dom VLK) by ZFMISC_1: 50;

          VK1 = (VLK +* (w .--> ((S .Lifespan() ) -' k))) by A3, Def9;

          hence VLK c= VK1 by A5, FUNCT_4: 32;

        end;

          suppose

           A6: (S .Lifespan() ) <= k;

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

          hence VLK c= VK1 by A6, Th10;

        end;

      end;

      

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

      proof

        let k be Nat such that

         A8: P[k];

        (S . (m + k)) c= (S . ((m + k) + 1)) by A2;

        hence thesis by A8, XBOOLE_1: 1;

      end;

      

       A9: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A9, A7);

      hence thesis by A1;

    end;

    theorem :: LEXBFS:18

    

     Th18: for G be _finite _Graph, S be VNumberingSeq of G, n be Nat holds (S . n) is one-to-one

    proof

      let G be _finite _Graph, S be VNumberingSeq of G, n be Nat;

      defpred P[ Nat] means (S . $1) is one-to-one;

      

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

      proof

        set GN = (S .Lifespan() );

        let k be Nat such that

         A2: P[k];

        set w = (S .PickedAt k);

        set CK1 = (S . (k + 1));

        set CSK = (S . k);

        set VLK = CSK;

        set VL1 = CK1;

        per cases ;

          suppose

           A3: k < GN;

          set wf = (w .--> (GN -' k));

           A4:

          now

            assume

             A5: (GN -' k) in ( rng VLK);

            ( rng VLK) = (( Seg GN) \ ( Seg (GN -' k))) by Th14;

            hence contradiction by A5, Th3;

          end;

          ( rng wf) = {(GN -' k)} by FUNCOP_1: 8;

          then

           A6: ( rng wf) misses ( rng VLK) by A4, ZFMISC_1: 50;

          VL1 = (VLK +* (w .--> (GN -' k))) by A3, Def9;

          hence thesis by A2, A6, FUNCT_4: 92;

        end;

          suppose

           A7: k >= GN;

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

          hence thesis by A2, A7, Th10;

        end;

      end;

      

       A8: P[ 0 ] by Def8;

      for k be Nat holds P[k] from NAT_1:sch 2( A8, A1);

      hence thesis;

    end;

    theorem :: LEXBFS:19

    

     Th19: for G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat, v be set st v in ( dom (S . m)) & v in ( dom (S . n)) holds ((S . m) . v) = ((S . n) . v)

    proof

      let G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat;

      let v be set such that

       A1: v in ( dom (S . m)) and

       A2: v in ( dom (S . n));

      set VLM = (S . m);

      

       A3: [v, (VLM . v)] in VLM by A1, FUNCT_1:def 2;

      set VLN = (S . n);

      

       A4: [v, (VLN . v)] in VLN by A2, FUNCT_1:def 2;

      per cases ;

        suppose m <= n;

        then VLM c= VLN by Th17;

        hence thesis by A2, A3, FUNCT_1:def 2;

      end;

        suppose m > n;

        then VLN c= VLM by Th17;

        hence thesis by A1, A4, FUNCT_1:def 2;

      end;

    end;

    theorem :: LEXBFS:20

    

     Th20: for G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat, v be set st v in ( dom (S . m)) & ((S . m) . v) = n holds (S .PickedAt ((S .Lifespan() ) -' n)) = v

    proof

      let G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat, v be set;

      set CSM = (S . m);

      set VLM = CSM;

      set j = ((S .Lifespan() ) -' n);

      set CJ1 = (S . (j + 1));

      set VJ1 = CJ1;

      assume that

       A1: v in ( dom CSM) and

       A2: (VLM . v) = n;

      set w = (S .PickedAt j);

      n <= (S .Lifespan() ) by A2, Th15;

      then

       A3: ((S .Lifespan() ) -' n) = ((S .Lifespan() ) - n) by XREAL_1: 233;

      

       A4: 0 < n by A1, A2, Th15;

      then

       A5: j < (S .Lifespan() ) by A3, XREAL_1: 44;

      then ((S .Lifespan() ) -' j) = ((S .Lifespan() ) - ((S .Lifespan() ) - n)) by A3, XREAL_1: 233;

      then

       A6: (VJ1 . w) = n by A4, A3, Th12, XREAL_1: 44;

      

       A7: VLM is one-to-one by Th18;

      

       A8: w in ( dom CJ1) by A5, Th11;

      per cases ;

        suppose

         A9: m <= j;

        then (m + n) <= (((S .Lifespan() ) - n) + n) by A3, XREAL_1: 6;

        then

         A10: ((n + m) - m) <= ((S .Lifespan() ) - m) by XREAL_1: 9;

        

         A11: ( rng VLM) = (( Seg (S .Lifespan() )) \ ( Seg ((S .Lifespan() ) -' m))) by Th14;

        

         A12: n in ( rng VLM) by A1, A2, FUNCT_1:def 3;

        ((S .Lifespan() ) - m) = ((S .Lifespan() ) -' m) by A5, A9, XREAL_1: 233, XXREAL_0: 2;

        hence thesis by A10, A12, A11, Th3;

      end;

        suppose j < m;

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

        then

         A13: VJ1 c= VLM by Th17;

        then

         A14: ( dom VJ1) c= ( dom VLM) by RELAT_1: 11;

         [w, n] in VJ1 by A8, A6, FUNCT_1:def 2;

        then (VLM . w) = n by A8, A13, A14, FUNCT_1:def 2;

        hence thesis by A1, A2, A8, A7, A14, FUNCT_1:def 4;

      end;

    end;

    theorem :: LEXBFS:21

    

     Th21: for G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat st n < (S .Lifespan() ) & n < m holds (S .PickedAt n) in ( dom (S . m)) & ((S . m) . (S .PickedAt n)) = ((S .Lifespan() ) -' n)

    proof

      let G be _finite _Graph, S be VNumberingSeq of G, m,n be Nat such that

       A1: n < (S .Lifespan() ) and

       A2: n < m;

      set CN1 = (S . (n + 1));

      set VN1 = CN1;

      set v = (S .PickedAt n);

      

       A3: (VN1 . v) = ((S .Lifespan() ) -' n) by A1, Th12;

      set CSM = (S . m);

      set VLM = CSM;

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

      then VN1 c= VLM by Th17;

      then

       A4: ( dom VN1) c= ( dom VLM) by RELAT_1: 11;

      v in ( dom CN1) by A1, Th11;

      hence thesis by A3, A4, Th19;

    end;

    theorem :: LEXBFS:22

    

     Th22: for G be _finite _Graph, S be VNumberingSeq of G, m be Nat, v be set st v in ( dom (S . m)) holds ((S .Lifespan() ) -' ((S . m) . v)) < m & ((S .Lifespan() ) -' m) < ((S . m) . v)

    proof

      let G be _finite _Graph, S be VNumberingSeq of G, m be Nat, v be set;

      set VLM = (S . m);

      set j = ((S .Lifespan() ) -' (VLM . v));

      set VLJ = (S . j);

      assume

       A1: v in ( dom VLM);

      then

       A2: (S .PickedAt j) = v by Th20;

      

       A3: 0 < (VLM . v) by A1, Th15;

      

       A4: (VLM . v) <= (S .Lifespan() ) by Th15;

      then j = ((S .Lifespan() ) - (VLM . v)) by XREAL_1: 233;

      then

       A5: j < (S .Lifespan() ) by A3, XREAL_1: 44;

       A6:

      now

        per cases ;

          suppose m <= j;

          then VLM c= VLJ by Th17;

          then ( dom VLM) c= ( dom VLJ) by RELAT_1: 11;

          hence ((S .Lifespan() ) -' (VLM . v)) < m by A1, A2, A5, Def9;

        end;

          suppose m > j;

          hence ((S .Lifespan() ) -' (VLM . v)) < m;

        end;

      end;

      now

        per cases ;

          suppose

           A7: ((S .Lifespan() ) - m) >= 0 ;

          ((S .Lifespan() ) - (VLM . v)) < m by A4, A6, XREAL_1: 233;

          then (((S .Lifespan() ) - (VLM . v)) + (VLM . v)) < (m + (VLM . v)) by XREAL_1: 6;

          then ((S .Lifespan() ) - m) < (((VLM . v) + m) - m) by XREAL_1: 9;

          hence ((S .Lifespan() ) -' m) < (VLM . v) by A7, XREAL_0:def 2;

        end;

          suppose ((S .Lifespan() ) - m) < 0 ;

          hence ((S .Lifespan() ) -' m) < (VLM . v) by A3, XREAL_0:def 2;

        end;

      end;

      hence thesis by A6;

    end;

    theorem :: LEXBFS:23

    

     Th23: for G be _finite _Graph, S be VNumberingSeq of G, i be Nat, a,b be set st a in ( dom (S . i)) & b in ( dom (S . i)) & ((S . i) . a) < ((S . i) . b) holds b in ( dom (S . ((S .Lifespan() ) -' ((S . i) . a))))

    proof

      let G be _finite _Graph, S be VNumberingSeq of G;

      let i be Nat, a,b be set such that

       A1: a in ( dom (S . i)) and

       A2: b in ( dom (S . i)) and

       A3: ((S . i) . a) < ((S . i) . b);

      set GN = (S .Lifespan() );

      set CSI = (S . i);

      set VLI = CSI;

      set j = ((S .Lifespan() ) -' (VLI . a));

      set CSJ = (S . j);

      set VLJ = CSJ;

      (VLI . a) <= GN by Th15;

      then

       A4: (GN -' (VLI . a)) = (GN - (VLI . a)) by XREAL_1: 233;

      then (GN -' j) = (GN - (GN - (VLI . a))) by NAT_D: 35, XREAL_1: 233;

      then

      consider w be Vertex of G such that

       A5: w in ( dom CSJ) and

       A6: (VLJ . w) = (VLI . b) by A3, Th15, Th16;

      now

        assume j >= i;

        then VLI c= VLJ by Th17;

        then

         A7: ( dom VLI) c= ( dom VLJ) by RELAT_1: 11;

         0 < (VLI . a) by A1, Th15;

        then

         A8: j < GN by A4, XREAL_1: 44;

        a = (S .PickedAt j) by A1, Th20;

        hence contradiction by A1, A7, A8, Def9;

      end;

      then

       A9: VLJ c= VLI by Th17;

      

       A10: [w, (VLI . b)] in VLJ by A5, A6, FUNCT_1: 1;

      then

       A11: (VLI . w) = (VLI . b) by A9, FUNCT_1: 1;

      

       A12: VLI is one-to-one by Th18;

      w in ( dom VLI) by A9, A10, FUNCT_1: 1;

      hence thesis by A2, A5, A11, A12, FUNCT_1:def 4;

    end;

    theorem :: LEXBFS:24

    

     Th24: for G be _finite _Graph, S be VNumberingSeq of G, i be Nat, a,b be set st a in ( dom (S . i)) & ((S . i) . a) < ((S . i) . b) holds not a in ( dom (S . ((S .Lifespan() ) -' ((S . i) . b))))

    proof

      let G be _finite _Graph, S be VNumberingSeq of G, i be Nat, a,b be set such that

       A1: a in ( dom (S . i)) and

       A2: ((S . i) . a) < ((S . i) . b);

      set GN = (S .Lifespan() );

      set CSI = (S . i);

      set VLI = CSI;

      set k = (GN -' (VLI . a));

      (VLI . a) <= GN by Th15;

      then

       A3: k = (GN - (VLI . a)) by XREAL_1: 233;

      set CSK = (S . k);

      set j = (GN -' (VLI . b));

      set CSJ = (S . j);

      set VLJ = CSJ;

      set VLK = CSK;

      (VLI . b) <= GN by Th15;

      then j = (GN - (VLI . b)) by XREAL_1: 233;

      then j < k by A2, A3, XREAL_1: 15;

      then VLJ c= VLK by Th17;

      then

       A4: ( dom VLJ) c= ( dom VLK) by RELAT_1: 11;

      assume

       A5: a in ( dom CSJ);

      1 <= (VLI . a) by A1, Th15;

      then

       A6: k < GN by A3, XREAL_1: 44;

      (S .PickedAt k) = a by A1, Th20;

      hence contradiction by A6, A5, A4, Def9;

    end;

    begin

    definition

      let X1,X3 be set, X2 be non empty set;

      let x be Element of [:( PFuncs (X1,X3)), X2:];

      :: original: `1

      redefine

      func x `1 -> Element of ( PFuncs (X1,X3)) ;

      coherence by MCART_1: 10;

    end

    definition

      let X1,X3 be non empty set, X2 be set;

      let x be Element of [:X1, ( Funcs (X2,X3)):];

      :: original: `2

      redefine

      func x `2 -> Element of ( Funcs (X2,X3)) ;

      coherence by MCART_1: 10;

    end

    definition

      let G be _Graph;

      mode LexBFS:Labeling of G is Element of [:( PFuncs (( the_Vertices_of G), NAT )), ( Funcs (( the_Vertices_of G),( Fin NAT ))):];

    end

    registration

      let G be _finite _Graph, L be LexBFS:Labeling of G;

      cluster (L `1 ) -> finite;

      coherence

      proof

        ( dom (L `1 )) c= ( the_Vertices_of G);

        hence thesis by FINSET_1: 10;

      end;

      cluster (L `2 ) -> finite;

      coherence ;

    end

    definition

      let G be _Graph;

      :: LEXBFS:def11

      func LexBFS:Init (G) -> LexBFS:Labeling of G equals [ {} , (( the_Vertices_of G) --> {} )];

      coherence

      proof

        set f = (( the_Vertices_of G) --> {} );

        

         A1: ( rng {} ) c= NAT ;

         {} c= NAT ;

        then {} in ( Fin NAT ) by FINSUB_1:def 5;

        then { {} } c= ( Fin NAT ) by ZFMISC_1: 31;

        then

         A2: ( rng f) c= ( Fin NAT );

        ( dom f) = ( the_Vertices_of G);

        then

         A3: f in ( Funcs (( the_Vertices_of G),( Fin NAT ))) by A2, FUNCT_2:def 2;

        ( dom {} ) c= ( the_Vertices_of G);

        then {} in ( PFuncs (( the_Vertices_of G), NAT )) by A1, PARTFUN1:def 3;

        hence thesis by A3, ZFMISC_1:def 2;

      end;

    end

    definition

      let G be _finite _Graph, L be LexBFS:Labeling of G;

      :: LEXBFS:def12

      func LexBFS:PickUnnumbered (L) -> Vertex of G means

      : Def11: it = the Element of ( the_Vertices_of G) if ( dom (L `1 )) = ( the_Vertices_of G)

      otherwise ex S be non empty finite Subset of ( bool NAT ), B be non empty finite Subset of ( Bags NAT ), F be Function st S = ( rng F) & F = ((L `2 ) | (( the_Vertices_of G) \ ( dom (L `1 )))) & (for x be finite Subset of NAT holds x in S implies (((x,1) -bag ) in B)) & (for x be set holds x in B implies ex y be finite Subset of NAT st y in S & x = ((y,1) -bag )) & it = the Element of (F " {( support ( max (B,( InvLexOrder NAT ))))});

      existence

      proof

        set VG = ( the_Vertices_of G);

        set V2G = (L `2 );

        set VLG = (L `1 );

        set F = (V2G | (VG \ ( dom VLG)));

        set S = ( rng F);

        

         A1: ex f be Function st (L `2 ) = f & ( dom f) = VG & ( rng f) c= ( Fin NAT ) by FUNCT_2:def 2;

        per cases ;

          suppose ( dom VLG) = VG;

          hence thesis;

        end;

          suppose

           A2: ( dom VLG) <> VG;

          ( dom F) = (( dom V2G) /\ (VG \ ( dom VLG))) by RELAT_1: 61;

          then

           A3: ( dom F) = ((VG /\ VG) \ ( dom VLG)) by A1, XBOOLE_1: 49;

           A4:

          now

            assume ( dom F) = {} ;

            then VG c= ( dom VLG) by A3, XBOOLE_1: 37;

            hence contradiction by A2, XBOOLE_0:def 10;

          end;

          

           A5: for x be set st x in S holds x is finite;

          

           A6: ( rng F) c= ( rng V2G) by RELAT_1: 70;

          now

            

             A7: ( rng V2G) c= ( bool NAT )

            proof

              let x be object;

              reconsider xx = x as set by TARSKI: 1;

              assume x in ( rng V2G);

              then xx c= NAT by FINSUB_1:def 5;

              hence thesis;

            end;

            let x be set such that

             A8: x in S;

            x in ( rng V2G) by A6, A8;

            hence x in ( bool NAT ) by A7;

            thus x is finite by A8;

          end;

          then for x be object holds x in S implies x in ( bool NAT );

          then

          reconsider S as non empty finite with_finite-elements Subset of ( bool NAT ) by A4, A5, FINSET_1:def 6, RELAT_1: 42, TARSKI:def 3;

          deffunc F( finite Subset of NAT ) = (($1,1) -bag );

          set B = { F(x) where x be Element of S : x in S };

          consider z be object such that

           A9: z in S by XBOOLE_0:def 1;

          reconsider z as finite Subset of NAT by A9;

          

           A10: ((z,1) -bag ) in B by A9;

          

           A11: S is finite;

          

           A12: B is finite from FRAENKEL:sch 21( A11);

          now

            let x be object;

            assume x in B;

            then ex y be Element of S st x = ((y,1) -bag ) & y in S;

            hence x in ( Bags NAT );

          end;

          then

          reconsider B as non empty finite Subset of ( Bags NAT ) by A12, A10, TARSKI:def 3;

          

           A13: for x be set holds x in B implies ex y be finite Subset of NAT st y in S & x = ((y,1) -bag )

          proof

            let x be set;

            assume x in B;

            then ex y be Element of S st x = ((y,1) -bag ) & y in S;

            hence thesis;

          end;

          set mw = ( max (B,( InvLexOrder NAT )));

          mw in B by Def4;

          then

          consider y be finite Subset of NAT such that

           A14: y in S and

           A15: mw = ((y,1) -bag ) by A13;

          set IT = the Element of (F " {( support mw)});

          y = ( support mw) by A15, UPROOTS: 8;

          then (F " {( support mw)}) is non empty by A14, FUNCT_1: 72;

          then IT in ( dom F) by FUNCT_1:def 7;

          then IT in ( dom V2G) by RELAT_1: 57;

          then

          reconsider IT as Vertex of G;

          for x be finite Subset of NAT holds x in S implies ((x,1) -bag ) in B;

          then ex S be non empty finite Subset of ( bool NAT ), B be non empty finite Subset of ( Bags NAT ), F be Function st S = ( rng F) & F = (V2G | (VG \ ( dom VLG))) & (for x be finite Subset of NAT holds x in S implies (((x,1) -bag ) in B)) & (for x be set holds x in B implies ex y be finite Subset of NAT st y in S & x = ((y,1) -bag )) & IT = the Element of (F " {( support ( max (B,( InvLexOrder NAT ))))}) & IT is Vertex of G by A13;

          hence thesis;

        end;

      end;

      uniqueness

      proof

        let IT1,IT2 be Vertex of G;

        set VG = ( the_Vertices_of G);

        set V2G = (L `2 );

        set VLG = (L `1 );

        thus ( dom VLG) = VG & IT1 = the Element of VG & IT2 = the Element of VG implies IT1 = IT2;

        assume ( dom VLG) <> VG;

        given S1 be non empty finite Subset of ( bool NAT ), B1 be non empty finite Subset of ( Bags NAT ), F1 be Function such that

         A16: S1 = ( rng F1) and

         A17: F1 = (V2G | (VG \ ( dom VLG))) and

         A18: for x be finite Subset of NAT holds x in S1 implies ((x,1) -bag ) in B1 and

         A19: for x be set holds x in B1 implies ex y be finite Subset of NAT st y in S1 & x = ((y,1) -bag ) and

         A20: IT1 = the Element of (F1 " {( support ( max (B1,( InvLexOrder NAT ))))});

        given S2 be non empty finite Subset of ( bool NAT ), B2 be non empty finite Subset of ( Bags NAT ), F2 be Function such that

         A21: S2 = ( rng F2) and

         A22: F2 = (V2G | (VG \ ( dom VLG))) and

         A23: for x be finite Subset of NAT holds x in S2 implies ((x,1) -bag ) in B2 and

         A24: for x be set holds x in B2 implies ex y be finite Subset of NAT st y in S2 & x = ((y,1) -bag ) and

         A25: IT2 = the Element of (F2 " {( support ( max (B2,( InvLexOrder NAT ))))});

        now

          let x be object;

          assume x in B2;

          then ex y be finite Subset of NAT st y in S2 & x = ((y,1) -bag ) by A24;

          hence x in B1 by A16, A17, A18, A21, A22;

        end;

        then

         A26: B2 c= B1;

        now

          let x be object;

          assume x in B1;

          then ex y be finite Subset of NAT st y in S1 & x = ((y,1) -bag ) by A19;

          hence x in B2 by A16, A17, A21, A22, A23;

        end;

        then B1 c= B2;

        then B1 = B2 by A26, XBOOLE_0:def 10;

        hence IT1 = IT2 by A17, A20, A22, A25;

      end;

      consistency ;

    end

    definition

      let G be _finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, n be Nat;

      :: LEXBFS:def13

      func LexBFS:Update (L,v,n) -> LexBFS:Labeling of G equals [((L `1 ) +* (v .--> ((G .order() ) -' n))), ((L `2 ) .\/ (((G .AdjacentSet {v}) \ ( dom (L `1 ))) --> {((G .order() ) -' n)}))];

      coherence

      proof

        set F = (((G .AdjacentSet {v}) \ ( dom (L `1 ))) --> {((G .order() ) -' n)});

        reconsider nn = ((G .order() ) -' n) as Element of NAT ;

        set L2 = ((L `2 ) .\/ (((G .AdjacentSet {v}) \ ( dom (L `1 ))) --> {((G .order() ) -' n)}));

        set f = (v .--> ((G .order() ) -' n));

        set L1 = ((L `1 ) +* f);

        

         A1: ( dom f) = {v};

        ( rng L1) c= (( rng (L `1 )) \/ ( rng f)) by FUNCT_4: 17;

        then

         A2: ( rng L1) c= NAT by XBOOLE_1: 1;

        ( dom L1) = (( dom (L `1 )) \/ ( dom f)) by FUNCT_4:def 1;

        then ( dom L1) c= ( the_Vertices_of G) by A1, XBOOLE_1: 8;

        then

         A3: L1 in ( PFuncs (( the_Vertices_of G), NAT )) by A2, PARTFUN1:def 3;

         {nn} in ( Fin NAT ) by FINSUB_1:def 5;

        then

         A4: { {nn}} c= ( Fin NAT ) by ZFMISC_1: 31;

        consider f be Function such that

         A5: (L `2 ) = f and

         A6: ( dom f) = ( the_Vertices_of G) and

         A7: ( rng f) c= ( Fin NAT ) by FUNCT_2:def 2;

        ( rng F) c= { {nn}} by FUNCOP_1: 13;

        then

         A8: ( rng F) c= ( Fin NAT ) by A4;

        

         A9: ( dom L2) = (( dom f) \/ ( dom F)) by A5, Def1;

        

         A10: ( rng L2) c= ( Fin NAT )

        proof

          let y be object;

          assume y in ( rng L2);

          then

          consider x be object such that

           A11: x in ( dom L2) and

           A12: y = (L2 . x) by FUNCT_1:def 3;

          

           A13: y = ((f . x) \/ (F . x)) by A5, A11, A12, Def1, A9;

          per cases by A11, A9, XBOOLE_0:def 3;

            suppose that

             A14: x in ( dom f) and

             A15: not x in ( dom F);

            

             A16: (F . x) = {} by A15, FUNCT_1:def 2;

            (f . x) in ( rng f) by A14, FUNCT_1: 3;

            hence thesis by A7, A13, A16;

          end;

            suppose that

             A17: not x in ( dom f) and

             A18: x in ( dom F);

            

             A19: (f . x) = {} by A17, FUNCT_1:def 2;

            (F . x) in ( rng F) by A18, FUNCT_1: 3;

            hence thesis by A8, A13, A19;

          end;

            suppose that

             A20: x in ( dom f) and

             A21: x in ( dom F);

            

             A22: (F . x) in ( rng F) by A21, FUNCT_1: 3;

            (f . x) in ( rng f) by A20, FUNCT_1: 3;

            hence thesis by A7, A8, A13, A22, FINSUB_1:def 1;

          end;

        end;

        ( dom L2) = (( dom f) \/ ( dom F)) by A9;

        then ( dom L2) = ( the_Vertices_of G) by A6, XBOOLE_1: 12;

        then L2 in ( Funcs (( the_Vertices_of G),( Fin NAT ))) by A10, FUNCT_2:def 2;

        hence thesis by A3, ZFMISC_1:def 2;

      end;

    end

    theorem :: LEXBFS:25

    

     Th25: for G be _finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be set, k be Nat st not x in (G .AdjacentSet {v}) holds ((L `2 ) . x) = ((( LexBFS:Update (L,v,k)) `2 ) . x)

    proof

      let G be _finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be set, k be Nat such that

       A1: not x in (G .AdjacentSet {v});

      set F = (((G .AdjacentSet {v}) \ ( dom (L `1 ))) --> {((G .order() ) -' k)});

      

       A2: not x in ( dom F) by A1, XBOOLE_0:def 5;

      then

       A3: (F . x) = {} by FUNCT_1:def 2;

      set L2 = (( LexBFS:Update (L,v,k)) `2 );

      per cases ;

        suppose x in ( dom (L `2 ));

        then x in (( dom (L `2 )) \/ ( dom F)) by XBOOLE_0:def 3;

        

        hence (L2 . x) = (((L `2 ) . x) \/ (F . x)) by Def1

        .= ((L `2 ) . x) by A3;

      end;

        suppose

         A4: not x in ( dom (L `2 ));

        then not x in (( dom (L `2 )) \/ ( dom F)) by A2, XBOOLE_0:def 3;

        then not x in ( dom L2) by Def1;

        

        hence (L2 . x) = {} by FUNCT_1:def 2

        .= ((L `2 ) . x) by A4, FUNCT_1:def 2;

      end;

    end;

    theorem :: LEXBFS:26

    

     Th26: for G be _finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be set, k be Nat st x in ( dom (L `1 )) holds ((( LexBFS:Update (L,v,k)) `2 ) . x) = ((L `2 ) . x)

    proof

      let G be _finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be set, k be Nat such that

       A1: x in ( dom (L `1 ));

      set F = (((G .AdjacentSet {v}) \ ( dom (L `1 ))) --> {((G .order() ) -' k)});

      

       A2: not x in ( dom F) by A1, XBOOLE_0:def 5;

      then

       A3: (F . x) = {} by FUNCT_1:def 2;

      set L2 = (( LexBFS:Update (L,v,k)) `2 );

      per cases ;

        suppose x in ( dom (L `2 ));

        then x in (( dom (L `2 )) \/ ( dom F)) by XBOOLE_0:def 3;

        

        hence (L2 . x) = (((L `2 ) . x) \/ (F . x)) by Def1

        .= ((L `2 ) . x) by A3;

      end;

        suppose

         A4: not x in ( dom (L `2 ));

        then not x in (( dom (L `2 )) \/ ( dom F)) by A2, XBOOLE_0:def 3;

        then not x in ( dom L2) by Def1;

        

        hence (L2 . x) = {} by FUNCT_1:def 2

        .= ((L `2 ) . x) by A4, FUNCT_1:def 2;

      end;

    end;

    theorem :: LEXBFS:27

    

     Th27: for G be _finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be set, k be Nat st x in (G .AdjacentSet {v}) & not x in ( dom (L `1 )) holds ((( LexBFS:Update (L,v,k)) `2 ) . x) = (((L `2 ) . x) \/ {((G .order() ) -' k)})

    proof

      let G be _finite _Graph, L be LexBFS:Labeling of G, v be Vertex of G, x be set, k be Nat such that

       A1: x in (G .AdjacentSet {v}) and

       A2: not x in ( dom (L `1 ));

      

       A3: x in ((G .AdjacentSet {v}) \ ( dom (L `1 ))) by A1, A2, XBOOLE_0:def 5;

      then x in ( dom (((G .AdjacentSet {v}) \ ( dom (L `1 ))) --> {((G .order() ) -' k)}));

      then

       A4: x in (( dom (L `2 )) \/ ( dom (((G .AdjacentSet {v}) \ ( dom (L `1 ))) --> {((G .order() ) -' k)}))) by XBOOLE_0:def 3;

      set L2 = (( LexBFS:Update (L,v,k)) `2 );

      ((((G .AdjacentSet {v}) \ ( dom (L `1 ))) --> {((G .order() ) -' k)}) . x) = {((G .order() ) -' k)} by A3, FUNCOP_1: 7;

      hence thesis by A4, Def1;

    end;

    definition

      let G be _finite _Graph, L be LexBFS:Labeling of G;

      :: LEXBFS:def14

      func LexBFS:Step (L) -> LexBFS:Labeling of G equals

      : Def13: L if (G .order() ) <= ( card ( dom (L `1 )))

      otherwise ( LexBFS:Update (L,( LexBFS:PickUnnumbered L),( card ( dom (L `1 )))));

      coherence ;

      consistency ;

    end

    definition

      let G be _Graph;

      :: LEXBFS:def15

      mode LexBFS:LabelingSeq of G -> ManySortedSet of NAT means

      : Def14: for n be Nat holds (it . n) is LexBFS:Labeling of G;

      existence

      proof

        set L = the LexBFS:Labeling of G;

        deffunc F( object) = L;

        consider f be ManySortedSet of NAT such that

         A1: for i be object st i in NAT holds (f . i) = F(i) from PBOOLE:sch 4;

        take f;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

    end

    definition

      let G be _Graph, S be LexBFS:LabelingSeq of G, n be Nat;

      :: original: .

      redefine

      func S . n -> LexBFS:Labeling of G ;

      coherence by Def14;

    end

    definition

      let G be _Graph, S be LexBFS:LabelingSeq of G;

      :: original: .Result()

      redefine

      func S .Result() -> LexBFS:Labeling of G ;

      coherence by Def14;

    end

    definition

      let G be _finite _Graph, S be LexBFS:LabelingSeq of G;

      :: LEXBFS:def16

      func S ``1 -> preVNumberingSeq of G means

      : Def15: for n be Nat holds (it . n) = ((S . n) `1 );

      existence

      proof

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

        consider f be ManySortedSet of NAT such that

         A1: for i be object st i in NAT holds (f . i) = F(i) from PBOOLE:sch 4;

        now

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          then (f . i) = ((S . i) `1 ) by A1;

          hence (f . i) is PartFunc of ( the_Vertices_of G), NAT ;

        end;

        then

        reconsider f as preVNumberingSeq of G by Def7;

        take f;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be preVNumberingSeq of G such that

         A2: for n be Nat holds (it1 . n) = ((S . n) `1 ) and

         A3: for n be Nat holds (it2 . n) = ((S . n) `1 );

        now

          let i be object;

          assume i in NAT ;

          then

          reconsider i9 = i as Nat;

          

          thus (it1 . i) = ((S . i9) `1 ) by A2

          .= (it2 . i) by A3;

        end;

        hence it1 = it2 by PBOOLE: 3;

      end;

    end

    definition

      let G be _finite _Graph;

      :: LEXBFS:def17

      func LexBFS:CSeq (G) -> LexBFS:LabelingSeq of G means

      : Def16: (it . 0 ) = ( LexBFS:Init G) & for n be Nat holds (it . (n + 1)) = ( LexBFS:Step (it . n));

      existence

      proof

        defpred P[ Nat, set, set] means ($2 is LexBFS:Labeling of G implies ex L be LexBFS:Labeling of G st $2 = L & $3 = ( LexBFS:Step L)) & ( not $2 is LexBFS:Labeling of G implies $3 = $2);

        now

          let n be Nat, x be set;

          now

            per cases ;

              suppose x is LexBFS:Labeling of G;

              then

              reconsider L = x as LexBFS:Labeling of G;

              ( LexBFS:Step L) = ( LexBFS:Step L);

              hence ex y be set st P[n, x, y];

            end;

              suppose not x is LexBFS:Labeling of G;

              hence ex y be set st P[n, x, y];

            end;

          end;

          hence ex y be set st P[n, x, y];

        end;

        then

         A1: for n be Nat holds for x be set holds ex y be set st P[n, x, y];

        consider IT be Function such that

         A2: ( dom IT) = NAT & (IT . 0 ) = ( LexBFS:Init G) & for n be Nat holds P[n, (IT . n), (IT . (n + 1))] from RECDEF_1:sch 1( A1);

        reconsider IT as ManySortedSet of NAT by A2, PARTFUN1:def 2, RELAT_1:def 18;

        defpred P2[ Nat] means (IT . $1) is LexBFS:Labeling of G;

         A3:

        now

          let n be Nat;

          assume

           A4: P2[n];

          ex Gn be LexBFS:Labeling of G st (IT . n) = Gn & (IT . (n + 1)) = ( LexBFS:Step Gn) by A2, A4;

          hence P2[(n + 1)];

        end;

        

         A5: P2[ 0 ] by A2;

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

        then

        reconsider IT as LexBFS:LabelingSeq of G by Def14;

        take IT;

        thus (IT . 0 ) = ( LexBFS:Init G) by A2;

        let n be Nat;

        ex Gn be LexBFS:Labeling of G st (IT . n) = Gn & (IT . (n + 1)) = ( LexBFS:Step Gn) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be LexBFS:LabelingSeq of G such that

         A6: (IT1 . 0 ) = ( LexBFS:Init G) and

         A7: for n be Nat holds (IT1 . (n + 1)) = ( LexBFS:Step (IT1 . n)) and

         A8: (IT2 . 0 ) = ( LexBFS:Init G) and

         A9: for n be Nat holds (IT2 . (n + 1)) = ( LexBFS:Step (IT2 . n));

        defpred P[ Nat] means (IT1 . $1) = (IT2 . $1);

        now

          let n be Nat;

          assume P[n];

          

          then (IT1 . (n + 1)) = ( LexBFS:Step (IT2 . n)) by A7

          .= (IT2 . (n + 1)) by A9;

          hence P[(n + 1)];

        end;

        then

         A10: for n be Nat st P[n] holds P[(n + 1)];

        

         A11: P[ 0 ] by A6, A8;

        for n be Nat holds P[n] from NAT_1:sch 2( A11, A10);

        then for n be object st n in NAT holds (IT1 . n) = (IT2 . n);

        hence IT1 = IT2 by PBOOLE: 3;

      end;

    end

    theorem :: LEXBFS:28

    

     Th28: for G be _finite _Graph holds ( LexBFS:CSeq G) is iterative

    proof

      let G be _finite _Graph;

      set CS = ( LexBFS:CSeq G);

      let k,n be Nat such that

       A1: (CS . k) = (CS . n);

      (CS . (k + 1)) = ( LexBFS:Step (CS . k)) by Def16;

      hence (CS . (k + 1)) = (CS . (n + 1)) by A1, Def16;

    end;

    registration

      let G be _finite _Graph;

      cluster ( LexBFS:CSeq G) -> iterative;

      coherence by Th28;

    end

    definition

      let X,Y be set, f be Function of X, ( Fin Y), x be set;

      :: original: .

      redefine

      func f . x -> finite Subset of Y ;

      coherence

      proof

        

         A1: ( dom f) = X by FUNCT_2:def 1;

        per cases ;

          suppose x in X;

          then (f . x) in ( Fin Y) by FUNCT_2: 5;

          hence thesis by FINSUB_1:def 5;

        end;

          suppose not x in X;

          then (f . x) = {} by A1, FUNCT_1:def 2;

          hence thesis by XBOOLE_1: 2;

        end;

      end;

    end

    theorem :: LEXBFS:29

    

     Th29: for G be _finite _Graph, L be LexBFS:Labeling of G, x be set st not x in ( dom (L `1 )) & ( dom (L `1 )) <> ( the_Vertices_of G) holds ((((L `2 ) . x),1) -bag ) <= (((((L `2 ) . ( LexBFS:PickUnnumbered L)),1) -bag ),( InvLexOrder NAT ))

    proof

      let G be _finite _Graph, L be LexBFS:Labeling of G, x be set such that

       A1: not x in ( dom (L `1 )) and

       A2: ( dom (L `1 )) <> ( the_Vertices_of G);

      set VG = ( the_Vertices_of G);

      set V2G = (L `2 );

      set VLG = (L `1 );

      set w = ( LexBFS:PickUnnumbered L);

      consider S be non empty finite Subset of ( bool NAT ), B be non empty finite Subset of ( Bags NAT ), F be Function such that

       A3: S = ( rng F) and

       A4: F = (V2G | (VG \ ( dom VLG))) and

       A5: for x be finite Subset of NAT holds x in S implies ((x,1) -bag ) in B and

       A6: for x be set holds x in B implies ex y be finite Subset of NAT st y in S & x = ((y,1) -bag ) and

       A7: w = the Element of (F " {( support ( max (B,( InvLexOrder NAT ))))}) by A2, Def11;

      

       A8: ( dom F) = (( dom V2G) /\ (VG \ ( dom VLG))) by A4, RELAT_1: 61;

      set mw = ( max (B,( InvLexOrder NAT )));

      mw in B by Def4;

      then

      consider y be finite Subset of NAT such that

       A9: y in S and

       A10: mw = ((y,1) -bag ) by A6;

      

       A11: y = ( support mw) by A10, UPROOTS: 8;

      then

       A12: (F " {( support mw)}) is non empty by A3, A9, FUNCT_1: 72;

      then w in ( dom F) by A7, FUNCT_1:def 7;

      then

       A13: (V2G . w) = (F . w) by A4, FUNCT_1: 47;

      (F . w) in {( support mw)} by A7, A12, FUNCT_1:def 7;

      then

       A14: (((V2G . w),1) -bag ) = mw by A10, A11, A13, TARSKI:def 1;

      

       A15: ( dom V2G) = ( the_Vertices_of G) by FUNCT_2:def 1;

      per cases ;

        suppose x in ( the_Vertices_of G);

        then x in (VG \ ( dom VLG)) by A1, XBOOLE_0:def 5;

        then

         A16: x in ( dom F) by A15, A8, XBOOLE_0:def 4;

        then

         A17: (F . x) in S by A3, FUNCT_1:def 3;

        (F . x) = (V2G . x) by A4, A16, FUNCT_1: 47;

        then (((V2G . x),1) -bag ) in B by A5, A17;

        hence thesis by A14, Def4;

      end;

        suppose not x in ( the_Vertices_of G);

        then (V2G . x) = {} by A15, FUNCT_1:def 2;

        then (((V2G . x),1) -bag ) = ( EmptyBag NAT ) by UPROOTS: 9;

        hence thesis by TERMORD: 9;

      end;

    end;

    theorem :: LEXBFS:30

    

     Th30: for G be _finite _Graph, L be LexBFS:Labeling of G st ( dom (L `1 )) <> ( the_Vertices_of G) holds not ( LexBFS:PickUnnumbered L) in ( dom (L `1 ))

    proof

      let G be _finite _Graph, L be LexBFS:Labeling of G such that

       A1: ( dom (L `1 )) <> ( the_Vertices_of G);

      set VG = ( the_Vertices_of G);

      set V2G = (L `2 );

      set VLG = (L `1 );

      set w = ( LexBFS:PickUnnumbered L);

      consider S be non empty finite Subset of ( bool NAT ), B be non empty finite Subset of ( Bags NAT ), F be Function such that

       A2: S = ( rng F) and

       A3: F = (V2G | (VG \ ( dom VLG))) and for x be finite Subset of NAT holds x in S implies ((x,1) -bag ) in B and

       A4: for x be set holds x in B implies ex y be finite Subset of NAT st y in S & x = ((y,1) -bag ) and

       A5: w = the Element of (F " {( support ( max (B,( InvLexOrder NAT ))))}) by A1, Def11;

      set mw = ( max (B,( InvLexOrder NAT )));

      mw in B by Def4;

      then

      consider y be finite Subset of NAT such that

       A6: y in S and

       A7: mw = ((y,1) -bag ) by A4;

      y = ( support mw) by A7, UPROOTS: 8;

      then (F " {( support mw)}) is non empty by A2, A6, FUNCT_1: 72;

      then

       A8: w in ( dom F) by A5, FUNCT_1:def 7;

      assume w in ( dom VLG);

      then

       A9: not w in (VG \ ( dom VLG)) by XBOOLE_0:def 5;

      ( dom F) = (( dom V2G) /\ (VG \ ( dom VLG))) by A3, RELAT_1: 61;

      hence contradiction by A8, A9, XBOOLE_0:def 4;

    end;

    theorem :: LEXBFS:31

    

     Th31: for G be _finite _Graph, n be Nat st ( card ( dom ((( LexBFS:CSeq G) . n) `1 ))) < (G .order() ) holds ((( LexBFS:CSeq G) . (n + 1)) `1 ) = (((( LexBFS:CSeq G) . n) `1 ) +* (( LexBFS:PickUnnumbered (( LexBFS:CSeq G) . n)) .--> ((G .order() ) -' ( card ( dom ((( LexBFS:CSeq G) . n) `1 ))))))

    proof

      let G be _finite _Graph, n be Nat;

      set CS = ( LexBFS:CSeq G);

      assume

       A1: ( card ( dom ((CS . n) `1 ))) < (G .order() );

      set CN1 = (CS . (n + 1));

      set CSN = (CS . n);

      set VLN = (CSN `1 );

      set w = ( LexBFS:PickUnnumbered CSN);

      CN1 = ( LexBFS:Step CSN) by Def16;

      then CN1 = ( LexBFS:Update (CSN,w,( card ( dom VLN)))) by A1, Def13;

      hence thesis;

    end;

    theorem :: LEXBFS:32

    

     Th32: for G be _finite _Graph, n be Nat st n <= (G .order() ) holds ( card ( dom ((( LexBFS:CSeq G) . n) `1 ))) = n

    proof

      let G be _finite _Graph, n be Nat such that

       A1: n <= (G .order() );

      set CS = ( LexBFS:CSeq G);

      defpred P[ Nat] means $1 <= (G .order() ) implies ( card ( dom ((CS . $1) `1 ))) = $1;

      

       A2: for k be Nat st k < (G .order() ) & ( card ( dom ((CS . k) `1 ))) = k holds ( card ( dom ((CS . (k + 1)) `1 ))) = (k + 1)

      proof

        let k be Nat such that

         A3: k < (G .order() ) and

         A4: ( card ( dom ((CS . k) `1 ))) = k;

        set CK1 = (CS . (k + 1));

        set CSK = (CS . k);

        set VLK = (CSK `1 );

        set VK1 = (CK1 `1 );

        set w = ( LexBFS:PickUnnumbered CSK);

        set wf = (w .--> ((G .order() ) -' k));

        

         A5: ( dom wf) = {w};

        VK1 = (VLK +* (w .--> ((G .order() ) -' k))) by A3, A4, Th31;

        then ( dom VK1) = (( dom VLK) \/ {w}) by A5, FUNCT_4:def 1;

        hence thesis by A3, A4, Th30, CARD_2: 41;

      end;

      

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

      proof

        let k be Nat such that

         A7: P[k];

        per cases ;

          suppose k < (G .order() );

          hence thesis by A2, A7;

        end;

          suppose k >= (G .order() );

          hence thesis by NAT_1: 13;

        end;

      end;

      (CS . 0 ) = ( LexBFS:Init G) by Def16;

      then

       A8: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A8, A6);

      hence thesis by A1;

    end;

    theorem :: LEXBFS:33

    

     Th33: for G be _finite _Graph, n be Nat st (G .order() ) <= n holds (( LexBFS:CSeq G) . (G .order() )) = (( LexBFS:CSeq G) . n)

    proof

      let G be _finite _Graph, n be Nat;

      assume (G .order() ) <= n;

      then

       A1: ex i be Nat st ((G .order() ) + i) = n by NAT_1: 10;

      set CS = ( LexBFS:CSeq G);

      defpred V[ Nat] means (G .order() ) = ( card ( dom ((CS . ((G .order() ) + $1)) `1 )));

      defpred P[ Nat] means (CS . (G .order() )) = (CS . ((G .order() ) + $1));

      

       A2: for k be Nat st V[k] holds V[(k + 1)]

      proof

        let k be Nat such that

         A3: V[k];

        set CK1 = (CS . (((G .order() ) + k) + 1));

        set CSK = (CS . ((G .order() ) + k));

        CK1 = ( LexBFS:Step CSK) by Def16;

        hence thesis by A3, Def13;

      end;

      

       A4: V[ 0 ] by Th32;

      

       A5: for k be Nat holds V[k] from NAT_1:sch 2( A4, A2);

      

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

      proof

        let k be Nat such that

         A7: P[k];

        set CK1 = (CS . (((G .order() ) + k) + 1));

        set CSK = (CS . ((G .order() ) + k));

        set VLK = (CSK `1 );

        

         A8: CK1 = ( LexBFS:Step CSK) by Def16;

        ( card ( dom VLK)) = (G .order() ) by A5;

        hence thesis by A7, A8, Def13;

      end;

      

       A9: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A9, A6);

      hence thesis by A1;

    end;

    theorem :: LEXBFS:34

    

     Th34: for G be _finite _Graph, m,n be Nat st (G .order() ) <= m & m <= n holds (( LexBFS:CSeq G) . m) = (( LexBFS:CSeq G) . n)

    proof

      let G be _finite _Graph, m,n be Nat such that

       A1: (G .order() ) <= m and

       A2: m <= n;

      (( LexBFS:CSeq G) . m) = (( LexBFS:CSeq G) . (G .order() )) by A1, Th33;

      hence thesis by A1, A2, Th33, XXREAL_0: 2;

    end;

    theorem :: LEXBFS:35

    

     Th35: for G be _finite _Graph holds ( LexBFS:CSeq G) is eventually-constant

    proof

      let G be _finite _Graph;

      take (G .order() );

      let m be Nat;

      assume (G .order() ) <= m;

      hence (( LexBFS:CSeq G) . (G .order() )) = (( LexBFS:CSeq G) . m) by Th33;

    end;

    registration

      let G be _finite _Graph;

      cluster ( LexBFS:CSeq G) -> eventually-constant;

      coherence by Th35;

    end

    theorem :: LEXBFS:36

    

     Th36: for G be _finite _Graph, n be Nat holds ( dom ((( LexBFS:CSeq G) . n) `1 )) = ( the_Vertices_of G) iff (G .order() ) <= n

    proof

      let G be _finite _Graph, n be Nat;

      set CS = ( LexBFS:CSeq G);

      set CSN = (CS . n);

      set VLN = (CSN `1 );

      set CSO = (CS . (G .order() ));

      set VLO = (CSO `1 );

      thus not ( dom VLN) = ( the_Vertices_of G) or not n < (G .order() ) by Th32;

      ( card ( dom VLO)) = ( card ( the_Vertices_of G)) by Th32;

      then

       A1: ( dom VLO) = ( the_Vertices_of G) by CARD_2: 102;

      assume (G .order() ) <= n;

      hence thesis by A1, Th34;

    end;

    theorem :: LEXBFS:37

    

     Th37: for G be _finite _Graph holds (( LexBFS:CSeq G) .Lifespan() ) = (G .order() )

    proof

      let G be _finite _Graph;

      set CS = ( LexBFS:CSeq G);

      

       A1: for n be Nat st (CS . n) = (CS . (n + 1)) holds (G .order() ) <= n

      proof

        let n be Nat such that

         A2: (CS . n) = (CS . (n + 1));

        set w = ( LexBFS:PickUnnumbered (CS . n));

        set VN1 = ((CS . (n + 1)) `1 );

        set VLN = ((CS . n) `1 );

        set j = ( card ( dom VLN));

        set wf = (w .--> ((G .order() ) -' j));

        assume

         A3: n < (G .order() );

        then ( dom VLN) <> ( the_Vertices_of G) by Th36;

        then

         A4: not w in ( dom VLN) by Th30;

        j < (G .order() ) by A3, Th32;

        then

         A5: VN1 = (VLN +* (w .--> ((G .order() ) -' j))) by Th31;

        ( dom wf) = {w};

        then

         A6: ( dom VN1) = (( dom VLN) \/ {w}) by A5, FUNCT_4:def 1;

        w in {w} by TARSKI:def 1;

        hence contradiction by A2, A4, A6, XBOOLE_0:def 3;

      end;

      (G .order() ) <= ((G .order() ) + 1) by NAT_1: 13;

      then (CS . (G .order() )) = (CS . ((G .order() ) + 1)) by Th33;

      hence thesis by A1, GLIB_000:def 56;

    end;

    theorem :: LEXBFS:38

    

     Th38: for G be _finite _Graph holds (( LexBFS:CSeq G) ``1 ) is eventually-constant

    proof

      let G be _finite _Graph;

      set CS = ( LexBFS:CSeq G);

      set S = (( LexBFS:CSeq G) ``1 );

      now

        consider n be Nat such that

         A1: for m be Nat st n <= m holds (CS . n) = (CS . m) by Def6;

        take n;

        let m be Nat such that

         A2: n <= m;

        

        thus (S . n) = ((CS . n) `1 ) by Def15

        .= ((CS . m) `1 ) by A1, A2

        .= (S . m) by Def15;

      end;

      hence thesis;

    end;

    theorem :: LEXBFS:39

    

     Th39: for G be _finite _Graph holds ((( LexBFS:CSeq G) ``1 ) .Lifespan() ) = (( LexBFS:CSeq G) .Lifespan() )

    proof

      let G be _finite _Graph;

      set S = ( LexBFS:CSeq G);

      set VN = (S ``1 );

      set ls = (G .order() );

      

       A1: VN is eventually-constant by Th38;

      

       A2: ((S . (ls + 1)) `1 ) = ((S ``1 ) . (ls + 1)) by Def15;

       A3:

      now

        let n be Nat such that

         A4: (VN . n) = (VN . (n + 1)) and

         A5: ls > n;

        (n + 1) <= ls by A5, NAT_1: 13;

        then

         A6: ( card ( dom ((S . (n + 1)) `1 ))) = (n + 1) by Th32;

        

         A7: ((S . (n + 1)) `1 ) = (VN . (n + 1)) by Def15;

        

         A8: ((S . n) `1 ) = (VN . n) by Def15;

        ( card ( dom ((S . n) `1 ))) = n by A5, Th32;

        hence contradiction by A4, A6, A8, A7;

      end;

      ((S . ls) `1 ) = ((S ``1 ) . ls) by Def15;

      then

       A9: (VN . ls) = (VN . (ls + 1)) by A2, Th33, NAT_1: 11;

      (S .Lifespan() ) = ls by Th37;

      hence thesis by A1, A9, A3, GLIB_000:def 56;

    end;

    registration

      let G be _finite _Graph;

      cluster (( LexBFS:CSeq G) ``1 ) -> vertex-numbering;

      correctness

      proof

        set S = (( LexBFS:CSeq G) ``1 );

        set CS = ( LexBFS:CSeq G);

        

         A1: (S .Lifespan() ) = (CS .Lifespan() ) by Th39;

        

        thus (S . 0 ) = ((CS . 0 ) `1 ) by Def15

        .= (( LexBFS:Init G) `1 ) by Def16

        .= {} ;

        now

          let k,n be Nat such that

           A2: (S . k) = (S . n);

          

           A3: (S . (k + 1)) = ((CS . (k + 1)) `1 ) by Def15;

          

           A4: (S . k) = ((CS . k) `1 ) by Def15;

          

           A5: (S . (n + 1)) = ((CS . (n + 1)) `1 ) by Def15;

          

           A6: (S . n) = ((CS . n) `1 ) by Def15;

          per cases ;

            suppose

             A7: k <= (G .order() ) & n <= (G .order() );

            then ( card ( dom ((CS . n) `1 ))) = n by Th32;

            hence (S . (k + 1)) = (S . (n + 1)) by A2, A4, A6, A7, Th32;

          end;

            suppose

             A8: k <= (G .order() ) & n >= (G .order() );

            then

             A9: (CS . n) = (CS . (G .order() )) by Th33;

            

             A10: ( card ( dom ((CS . (G .order() )) `1 ))) = (G .order() ) by Th32;

            

             A11: (n + 1) >= (G .order() ) by A8, NAT_1: 13;

            ( card ( dom ((CS . k) `1 ))) = k by A8, Th32;

            then (k + 1) >= (G .order() ) by A2, A4, A6, A9, A10, NAT_1: 13;

            

            hence (S . (k + 1)) = ((CS . (G .order() )) `1 ) by A3, Th33

            .= (S . (n + 1)) by A5, A11, Th33;

          end;

            suppose

             A12: k >= (G .order() ) & n <= (G .order() );

            then

             A13: (CS . k) = (CS . (G .order() )) by Th33;

            

             A14: ( card ( dom ((CS . (G .order() )) `1 ))) = (G .order() ) by Th32;

            ( card ( dom ((CS . n) `1 ))) = n by A12, Th32;

            then

             A15: (n + 1) >= (G .order() ) by A2, A4, A6, A13, A14, NAT_1: 13;

            (k + 1) >= (G .order() ) by A12, NAT_1: 13;

            

            hence (S . (k + 1)) = ((CS . (G .order() )) `1 ) by A3, Th33

            .= (S . (n + 1)) by A5, A15, Th33;

          end;

            suppose

             A16: k >= (G .order() ) & n >= (G .order() );

            then

             A17: (n + 1) >= (G .order() ) by NAT_1: 13;

            

             A18: (k + 1) >= (G .order() ) by A16, NAT_1: 13;

            

            thus (S . (k + 1)) = ((CS . (k + 1)) `1 ) by Def15

            .= ((CS . (G .order() )) `1 ) by A18, Th33

            .= ((CS . (n + 1)) `1 ) by A17, Th33

            .= (S . (n + 1)) by Def15;

          end;

        end;

        hence S is iterative;

        S is eventually-constant by Th38;

        hence S is halting;

        

         A19: (CS .Lifespan() ) = (G .order() ) by Th37;

        hence (S .Lifespan() ) = (G .order() ) by Th39;

        let n be Nat such that

         A20: n < (S .Lifespan() );

        

         A21: n < (G .order() ) by A19, A20, Th39;

        take w = ( LexBFS:PickUnnumbered (CS . n));

        

         A22: (S . n) = ((CS . n) `1 ) by Def15;

        

         A23: ( card ( dom ((CS . n) `1 ))) = n by A21, Th32;

        hence not w in ( dom (S . n)) by A21, A22, Th30;

        (S . (n + 1)) = ((CS . (n + 1)) `1 ) by Def15;

        hence thesis by A1, A19, A20, A22, A23, Th31;

      end;

    end

    theorem :: LEXBFS:40

    

     Th40: for G be _finite _Graph holds ((( LexBFS:CSeq G) ``1 ) .Result() ) = ((( LexBFS:CSeq G) .Result() ) `1 )

    proof

      let G be _finite _Graph;

      set S = ( LexBFS:CSeq G);

      

      thus ((S ``1 ) .Result() ) = ((S ``1 ) . (S .Lifespan() )) by Th39

      .= ((S .Result() ) `1 ) by Def15;

    end;

    theorem :: LEXBFS:41

    

     Th41: for G be _finite _Graph, n be Nat st n < (G .order() ) holds ((( LexBFS:CSeq G) ``1 ) .PickedAt n) = ( LexBFS:PickUnnumbered (( LexBFS:CSeq G) . n))

    proof

      let G be _finite _Graph, n be Nat such that

       A1: n < (G .order() );

      set CS = ( LexBFS:CSeq G);

      set CSN = (CS . n);

      set CS1 = (CS . (n + 1));

      set VLN = (CSN `1 );

      set VL1 = (CS1 `1 );

      

       A2: (CS .Lifespan() ) = (G .order() ) by Th37;

      set PU = ( LexBFS:PickUnnumbered CSN);

      set f2 = (PU .--> ((CS .Lifespan() ) -' n));

      

       A3: ( dom f2) = {PU};

      n = ( card ( dom VLN)) by A1, Th32;

      then VL1 = (VLN +* (PU .--> ((CS .Lifespan() ) -' n))) by A1, A2, Th31;

      then

       A4: ( dom VL1) = (( dom VLN) \/ {PU}) by A3, FUNCT_4:def 1;

      

       A5: (CSN `1 ) = ((CS ``1 ) . n) by Def15;

      set PA = ((CS ``1 ) .PickedAt n);

      set f1 = (PA .--> ((CS .Lifespan() ) -' n));

      

       A6: ( dom f1) = {PA};

      

       A7: (CS .Lifespan() ) = ((CS ``1 ) .Lifespan() ) by Th39;

      (CS1 `1 ) = ((CS ``1 ) . (n + 1)) by Def15;

      then VL1 = (VLN +* (PA .--> ((CS .Lifespan() ) -' n))) by A1, A2, A7, A5, Def9;

      then

       A8: ( dom VL1) = (( dom VLN) \/ {PA}) by A6, FUNCT_4:def 1;

      

       A9: not PA in ( dom VLN) by A1, A2, A7, A5, Def9;

      now

        assume PA <> PU;

        then not PA in {PU} by TARSKI:def 1;

        then

         A10: not PA in ( dom VL1) by A9, A4, XBOOLE_0:def 3;

        PA in {PA} by TARSKI:def 1;

        hence contradiction by A8, A10, XBOOLE_0:def 3;

      end;

      hence thesis;

    end;

    theorem :: LEXBFS:42

    

     Th42: for G be _finite _Graph, n be Nat st n < (G .order() ) holds ex w be Vertex of G st w = ( LexBFS:PickUnnumbered (( LexBFS:CSeq G) . n)) & for v be set holds (v in (G .AdjacentSet {w}) & not v in ( dom ((( LexBFS:CSeq G) . n) `1 )) implies (((( LexBFS:CSeq G) . (n + 1)) `2 ) . v) = ((((( LexBFS:CSeq G) . n) `2 ) . v) \/ {((G .order() ) -' n)})) & (( not v in (G .AdjacentSet {w}) or v in ( dom ((( LexBFS:CSeq G) . n) `1 ))) implies (((( LexBFS:CSeq G) . (n + 1)) `2 ) . v) = (((( LexBFS:CSeq G) . n) `2 ) . v))

    proof

      let G be _finite _Graph, n be Nat such that

       A1: n < (G .order() );

      set CS = ( LexBFS:CSeq G);

      set CSN = (CS . n);

      set VLN = (CSN `1 );

      set V2N = (CSN `2 );

      set CN1 = (CS . (n + 1));

      set V21 = (CN1 `2 );

      set w = ( LexBFS:PickUnnumbered CSN);

      take w;

      

       A2: CN1 = ( LexBFS:Step CSN) by Def16;

      ( card ( dom VLN)) = n by A1, Th32;

      then

       A3: CN1 = ( LexBFS:Update (CSN,w,n)) by A1, A2, Def13;

      now

        let v be set;

        assume

         A4: not v in (G .AdjacentSet {w}) or v in ( dom VLN);

        per cases by A4;

          suppose not v in (G .AdjacentSet {w});

          hence (V21 . v) = (V2N . v) by A3, Th25;

        end;

          suppose v in ( dom VLN);

          hence (V21 . v) = (V2N . v) by A3, Th26;

        end;

      end;

      hence thesis by A3, Th27;

    end;

    theorem :: LEXBFS:43

    

     Th43: for G be _finite _Graph, i be Nat, v be set holds (((( LexBFS:CSeq G) . i) `2 ) . v) c= (( Seg (G .order() )) \ ( Seg ((G .order() ) -' i)))

    proof

      let G be _finite _Graph, i be Nat, v be set;

      set CS = ( LexBFS:CSeq G);

      set CSI = (CS . i);

      set V2I = (CSI `2 );

      set CSO = (CS . (G .order() ));

      set V2O = (CSO `2 );

      defpred P[ Nat] means $1 <= (G .order() ) implies (((( LexBFS:CSeq G) . $1) `2 ) . v) c= (( Seg (G .order() )) \ ( Seg ((G .order() ) -' $1)));

      

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

      proof

        let k be Nat such that

         A2: P[k];

        set CK1 = (CS . (k + 1));

        set CSK = (CS . k);

        set V2K = (CSK `2 );

        set VLK = (CSK `1 );

        set V21 = (CK1 `2 );

        per cases ;

          suppose (k + 1) <= (G .order() );

          then

           A3: k < (G .order() ) by NAT_1: 13;

          then

          consider w be Vertex of G such that w = ( LexBFS:PickUnnumbered CSK) and

           A4: for v be set holds (v in (G .AdjacentSet {w}) & not v in ( dom VLK) implies (V21 . v) = ((V2K . v) \/ {((G .order() ) -' k)})) & ( not v in (G .AdjacentSet {w}) or v in ( dom VLK) implies (V21 . v) = (V2K . v)) by Th42;

          per cases ;

            suppose

             A5: v in (G .AdjacentSet {w}) & not v in ( dom VLK);

            

             A6: ((( Seg (G .order() )) \ ( Seg ((G .order() ) -' k))) \/ {((G .order() ) -' k)}) = (( Seg (G .order() )) \ ( Seg ((G .order() ) -' (k + 1)))) by A3, Th5;

            (V21 . v) = ((V2K . v) \/ {((G .order() ) -' k)}) by A4, A5;

            hence thesis by A2, A6, NAT_1: 13, XBOOLE_1: 9;

          end;

            suppose

             A7: not v in (G .AdjacentSet {w}) or v in ( dom VLK);

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

            then

             A8: (( Seg (G .order() )) \ ( Seg ((G .order() ) -' k))) c= (( Seg (G .order() )) \ ( Seg ((G .order() ) -' (k + 1)))) by Th4;

            (V21 . v) = (V2K . v) by A4, A7;

            hence thesis by A2, A8, NAT_1: 13, XBOOLE_1: 1;

          end;

        end;

          suppose (G .order() ) < (k + 1);

          hence thesis;

        end;

      end;

      (CS . 0 ) = ( LexBFS:Init G) by Def16;

      then (((CS . 0 ) `2 ) . v) = {} ;

      then

       A9: P[ 0 ] by XBOOLE_1: 2;

      

       A10: for k be Nat holds P[k] from NAT_1:sch 2( A9, A1);

      per cases ;

        suppose i <= (G .order() );

        hence thesis by A10;

      end;

        suppose

         A11: i > (G .order() );

        then ((G .order() ) - i) < (i - i) by XREAL_1: 9;

        then ((G .order() ) -' i) = 0 by XREAL_0:def 2;

        then

         A12: ((G .order() ) -' (G .order() )) = ((G .order() ) -' i) by XREAL_1: 232;

        V2O = V2I by A11, Th34;

        hence thesis by A10, A12;

      end;

    end;

    theorem :: LEXBFS:44

    

     Th44: for G be _finite _Graph, x be set, i,j be Nat st i <= j holds (((( LexBFS:CSeq G) . i) `2 ) . x) c= (((( LexBFS:CSeq G) . j) `2 ) . x)

    proof

      let G be _finite _Graph, x be set, i,j be Nat;

      assume i <= j;

      then

       A1: ex k be Nat st j = (i + k) by NAT_1: 10;

      set CS = ( LexBFS:CSeq G);

      set CSI = (CS . i), V2I = (CSI `2 );

      defpred P[ Nat] means (V2I . x) c= (((CS . (i + $1)) `2 ) . x);

      

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

      proof

        let k be Nat such that

         A3: P[k];

        set CK1 = (CS . ((i + k) + 1));

        set CSK = (CS . (i + k));

        set V2K = (CSK `2 );

        set VLK = (CSK `1 );

        set V21 = (CK1 `2 );

        per cases ;

          suppose ((i + k) + 1) <= (G .order() );

          then (i + k) < (G .order() ) by NAT_1: 13;

          then

          consider w be Vertex of G such that w = ( LexBFS:PickUnnumbered CSK) and

           A4: for v be set holds (v in (G .AdjacentSet {w}) & not v in ( dom VLK) implies (V21 . v) = ((V2K . v) \/ {((G .order() ) -' (i + k))})) & ( not v in (G .AdjacentSet {w}) or v in ( dom VLK) implies (V21 . v) = (V2K . v)) by Th42;

          per cases ;

            suppose x in (G .AdjacentSet {w}) & not x in ( dom VLK);

            then (V21 . x) = ((V2K . x) \/ {((G .order() ) -' (i + k))}) by A4;

            then (V2K . x) c= (V21 . x) by XBOOLE_1: 7;

            hence thesis by A3, XBOOLE_1: 1;

          end;

            suppose not x in (G .AdjacentSet {w}) or x in ( dom VLK);

            hence thesis by A3, A4;

          end;

        end;

          suppose

           A5: (G .order() ) < ((i + k) + 1);

          

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

          (G .order() ) <= (i + k) by A5, NAT_1: 13;

          hence thesis by A3, A6, Th34;

        end;

      end;

      

       A7: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A7, A2);

      hence thesis by A1;

    end;

    theorem :: LEXBFS:45

    

     Th45: for G be _finite _Graph, m,n be Nat, x,y be set st n < (G .order() ) & n < m & y = ( LexBFS:PickUnnumbered (( LexBFS:CSeq G) . n)) & not x in ( dom ((( LexBFS:CSeq G) . n) `1 )) & x in (G .AdjacentSet {y}) holds ((G .order() ) -' n) in (((( LexBFS:CSeq G) . m) `2 ) . x)

    proof

      let G be _finite _Graph;

      let m,n be Nat, x,y be set such that

       A1: n < (G .order() ) and

       A2: n < m;

      set CS = ( LexBFS:CSeq G);

      set CSM = (CS . m), V2M = (CSM `2 );

      set CN1 = (CS . (n + 1));

      set V21 = (CN1 `2 );

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

      then

       A3: (V21 . x) c= (V2M . x) by Th44;

      

       A4: ((G .order() ) -' n) in {((G .order() ) -' n)} by TARSKI:def 1;

      set CSN = (CS . n), VLN = (CSN `1 ), V2N = (CSN `2 );

      assume that

       A5: y = ( LexBFS:PickUnnumbered CSN) and

       A6: not x in ( dom VLN) and

       A7: x in (G .AdjacentSet {y});

      ex w be Vertex of G st w = ( LexBFS:PickUnnumbered CSN) & for v be set holds (v in (G .AdjacentSet {w}) & not v in ( dom VLN) implies (V21 . v) = ((V2N . v) \/ {((G .order() ) -' n)})) & ( not v in (G .AdjacentSet {w}) or v in ( dom VLN) implies (V21 . v) = (V2N . v)) by A1, Th42;

      then (V21 . x) = ((V2N . x) \/ {((G .order() ) -' n)}) by A5, A6, A7;

      then ((G .order() ) -' n) in (V21 . x) by A4, XBOOLE_0:def 3;

      hence thesis by A3;

    end;

    theorem :: LEXBFS:46

    

     Th46: for G be _finite _Graph, m,n be Nat st m < n holds for x be set st not ((G .order() ) -' m) in (((( LexBFS:CSeq G) . (m + 1)) `2 ) . x) holds not ((G .order() ) -' m) in (((( LexBFS:CSeq G) . n) `2 ) . x)

    proof

      let G be _finite _Graph, m,n be Nat;

      assume m < n;

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

      then

       A1: ex j be Nat st ((m + 1) + j) = n by NAT_1: 10;

      set CS = ( LexBFS:CSeq G);

      set CSM = (CS . (m + 1));

      set V2M = (CSM `2 );

      let x be set such that

       A2: not ((G .order() ) -' m) in (V2M . x);

      defpred P[ Nat] means not ((G .order() ) -' m) in (((( LexBFS:CSeq G) . ((m + 1) + $1)) `2 ) . x);

      

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

      proof

        let k be Nat such that

         A4: P[k];

        set CSK = (CS . ((m + 1) + k));

        set VLK = (CSK `1 ), V2K = (CSK `2 ), CK1 = (CS . (((m + 1) + k) + 1));

        set V21 = (CK1 `2 );

        now

          per cases ;

            suppose

             A5: ((m + 1) + k) < (G .order() );

            then

            consider w be Vertex of G such that w = ( LexBFS:PickUnnumbered CSK) and

             A6: for v be set holds (v in (G .AdjacentSet {w}) & not v in ( dom VLK) implies (V21 . v) = ((V2K . v) \/ {((G .order() ) -' ((m + 1) + k))})) & (( not v in (G .AdjacentSet {w}) or v in ( dom VLK)) implies (V21 . v) = (V2K . v)) by Th42;

            per cases ;

              suppose

               A7: x in (G .AdjacentSet {w}) & not x in ( dom VLK);

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

              then m < ((m + 1) + k) by XREAL_1: 39;

              then ((G .order() ) -' m) > ((G .order() ) -' ((m + 1) + k)) by A5, Th2;

              then

               A8: not ((G .order() ) -' m) in {((G .order() ) -' ((m + 1) + k))} by TARSKI:def 1;

              (V21 . x) = ((V2K . x) \/ {((G .order() ) -' ((m + 1) + k))}) by A6, A7;

              hence not ((G .order() ) -' m) in (V21 . x) by A4, A8, XBOOLE_0:def 3;

            end;

              suppose not x in (G .AdjacentSet {w}) or x in ( dom VLK);

              hence not ((G .order() ) -' m) in (V21 . x) by A4, A6;

            end;

          end;

            suppose

             A9: (G .order() ) <= ((m + 1) + k);

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

            hence not ((G .order() ) -' m) in (V21 . x) by A4, A9, Th34;

          end;

        end;

        hence thesis;

      end;

      

       A10: P[ 0 ] by A2;

      for k be Nat holds P[k] from NAT_1:sch 2( A10, A3);

      hence thesis by A1;

    end;

    theorem :: LEXBFS:47

    

     Th47: for G be _finite _Graph, m,n,k be Nat st k < n & n <= m holds for x be set st not ((G .order() ) -' k) in (((( LexBFS:CSeq G) . n) `2 ) . x) holds not ((G .order() ) -' k) in (((( LexBFS:CSeq G) . m) `2 ) . x)

    proof

      let G be _finite _Graph, m,n,k be Nat such that

       A1: k < n and

       A2: n <= m;

      set CS = ( LexBFS:CSeq G);

      set CSN = (CS . n);

      set V2N = (CSN `2 );

      let x be set such that

       A3: not ((G .order() ) -' k) in (V2N . x);

      set CK1 = (CS . (k + 1)), V21 = (CK1 `2 );

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

      then (V21 . x) c= (V2N . x) by Th44;

      then

       A4: not ((G .order() ) -' k) in (V21 . x) by A3;

      k < m by A1, A2, XXREAL_0: 2;

      hence thesis by A4, Th46;

    end;

    theorem :: LEXBFS:48

    

     Th48: for G be _finite _Graph, m,n be Nat, x be Vertex of G st n in (((( LexBFS:CSeq G) . m) `2 ) . x) holds ex y be Vertex of G st ( LexBFS:PickUnnumbered (( LexBFS:CSeq G) . ((G .order() ) -' n))) = y & not y in ( dom ((( LexBFS:CSeq G) . ((G .order() ) -' n)) `1 )) & x in (G .AdjacentSet {y})

    proof

      let G be _finite _Graph, m,n be Nat;

      set CS = ( LexBFS:CSeq G);

      set CSM = (CS . m);

      set V2M = (CSM `2 );

      set CSN = (CS . ((G .order() ) -' n));

      set VLN = (CSN `1 );

      set V2N = (CSN `2 );

      set on1 = (((G .order() ) -' n) + 1);

      set CN1 = (CS . on1);

      set V21 = (CN1 `2 );

      let x be Vertex of G such that

       A1: n in (V2M . x);

      

       A2: (V2M . x) c= (( Seg (G .order() )) \ ( Seg ((G .order() ) -' m))) by Th43;

      then

       A3: ((G .order() ) -' m) < n by A1, Th3;

      n <= (G .order() ) by A1, A2, Th3;

      then

       A4: ((G .order() ) -' n) = ((G .order() ) - n) by XREAL_1: 233;

      then

       A5: ((G .order() ) -' n) < (G .order() ) by A3, XREAL_1: 44;

      then

       A6: ((G .order() ) -' ((G .order() ) -' n)) = ((G .order() ) - ((G .order() ) - n)) by A4, XREAL_1: 233;

      then

      consider w be Vertex of G such that

       A7: w = ( LexBFS:PickUnnumbered CSN) and

       A8: for v be set holds (v in (G .AdjacentSet {w}) & not v in ( dom VLN) implies (V21 . v) = ((V2N . v) \/ {n})) & ( not v in (G .AdjacentSet {w}) or v in ( dom VLN) implies (V21 . v) = (V2N . v)) by A3, A4, Th42, XREAL_1: 44;

      (V2N . x) c= (( Seg (G .order() )) \ ( Seg ((G .order() ) -' ((G .order() ) -' n)))) by Th43;

      then

       A9: not n in (V2N . x) by A6, Th3;

       A10:

      now

        per cases ;

          suppose m <= (G .order() );

          then ((G .order() ) -' m) = ((G .order() ) - m) by XREAL_1: 233;

          then (((G .order() ) - m) + m) < (n + m) by A3, XREAL_1: 6;

          then ((G .order() ) - n) < ((m + n) - n) by XREAL_1: 9;

          hence on1 <= m by A4, NAT_1: 13;

        end;

          suppose (G .order() ) < m;

          then ((G .order() ) -' n) < m by A5, XXREAL_0: 2;

          hence on1 <= m by NAT_1: 13;

        end;

      end;

      

       A11: ((G .order() ) -' n) < on1 by XREAL_1: 39;

      assume

       A12: not ex y be Vertex of G st ( LexBFS:PickUnnumbered CSN) = y & not y in ( dom VLN) & x in (G .AdjacentSet {y});

      ( dom VLN) <> ( the_Vertices_of G) by A5, Th36;

      then not x in (G .AdjacentSet {w}) by A12, A7, Th30;

      then not n in (V21 . x) by A9, A8;

      hence contradiction by A1, A6, A10, A11, Th47;

    end;

    theorem :: LEXBFS:49

    

     Th49: for G be _finite _Graph holds ( dom ((( LexBFS:CSeq G) .Result() ) `1 )) = ( the_Vertices_of G)

    proof

      let G be _finite _Graph;

      set CS = ( LexBFS:CSeq G);

      set CSO = (CS . (G .order() ));

      (CS .Result() ) = CSO by Th37;

      hence thesis by Th36;

    end;

    ::$Notion-Name

    theorem :: LEXBFS:50

    

     Th50: for G be _finite _Graph holds (((( LexBFS:CSeq G) .Result() ) `1 ) " ) is VertexScheme of G

    proof

      let G be _finite _Graph;

      set CS = ( LexBFS:CSeq G);

      set CSO = (CS . (G .order() ));

      set VLO = (CSO `1 );

      set VL = (CS ``1 );

      

       A1: CSO = (( LexBFS:CSeq G) .Result() ) by Th37;

      

       A2: (CS .Lifespan() ) = (G .order() ) by Th37;

      

       A3: VLO = (VL . (G .order() )) by Def15;

      then

       A4: VLO is one-to-one by Th18;

      ( dom VLO) = ( the_Vertices_of G) by Th36;

      then

       A5: ( rng (VLO " )) = ( the_Vertices_of G) by A4, FUNCT_1: 33;

      (CS .Lifespan() ) = (VL .Lifespan() ) by Th39;

      

      then ( rng (VL . (G .order() ))) = (( Seg (G .order() )) \ ( Seg ((G .order() ) -' (G .order() )))) by A2, Th14

      .= (( Seg (G .order() )) \ ( Seg 0 )) by XREAL_1: 232

      .= ( Seg (G .order() ));

      then ( dom (VLO " )) = ( Seg (G .order() )) by A3, A4, FUNCT_1: 33;

      then (VLO " ) is FinSequence by FINSEQ_1:def 2;

      then (VLO " ) is FinSequence of ( the_Vertices_of G) by A5, FINSEQ_1:def 4;

      hence thesis by A1, A4, A5, CHORD:def 12;

    end;

    theorem :: LEXBFS:51

    

     Th51: for G be _finite _Graph, i,j be Nat, a,b be Vertex of G st a in ( dom ((( LexBFS:CSeq G) . i) `1 )) & b in ( dom ((( LexBFS:CSeq G) . i) `1 )) & (((( LexBFS:CSeq G) . i) `1 ) . a) < (((( LexBFS:CSeq G) . i) `1 ) . b) & j = ((G .order() ) -' (((( LexBFS:CSeq G) . i) `1 ) . b)) holds (((((( LexBFS:CSeq G) . j) `2 ) . a),1) -bag ) <= ((((((( LexBFS:CSeq G) . j) `2 ) . b),1) -bag ),( InvLexOrder NAT ))

    proof

      let G be _finite _Graph;

      let i,j be Nat, a,b be Vertex of G such that

       A1: a in ( dom ((( LexBFS:CSeq G) . i) `1 )) and

       A2: b in ( dom ((( LexBFS:CSeq G) . i) `1 )) and

       A3: (((( LexBFS:CSeq G) . i) `1 ) . a) < (((( LexBFS:CSeq G) . i) `1 ) . b) and

       A4: j = ((G .order() ) -' (((( LexBFS:CSeq G) . i) `1 ) . b));

      set VL = (( LexBFS:CSeq G) ``1 );

      set CSJ = (( LexBFS:CSeq G) . j);

      set VLI = (VL . i), VLJ = (VL . j);

      

       A5: (((( LexBFS:CSeq G) . i) `1 ) . b) = (((( LexBFS:CSeq G) ``1 ) . i) . b) by Def15;

      

       A6: a in ( the_Vertices_of G);

      

       A7: ((( LexBFS:CSeq G) . i) `1 ) = ((( LexBFS:CSeq G) ``1 ) . i) by Def15;

      

       A8: (( LexBFS:CSeq G) .Lifespan() ) = (VL .Lifespan() ) by Th39;

      

       A9: (G .order() ) = (( LexBFS:CSeq G) .Lifespan() ) by Th37;

      then (VLI . b) <= (G .order() ) by A8, Th15;

      then

       A10: ((G .order() ) -' (VLI . b)) = ((G .order() ) - (VLI . b)) by XREAL_1: 233;

      then

       A11: ((G .order() ) -' j) = ((G .order() ) - ((G .order() ) - (VLI . b))) by A4, A5, NAT_D: 35, XREAL_1: 233;

       A12:

      now

        assume a in ( dom (CSJ `1 ));

        then

         A13: a in ( dom VLJ) by Def15;

        then (VLI . b) < (VLJ . a) by A9, A8, A11, Th22;

        hence contradiction by A1, A3, A7, A13, Th19;

      end;

      (VL .PickedAt j) = b by A2, A4, A7, A9, A8, Th20;

      then ( LexBFS:PickUnnumbered CSJ) = b by A3, A4, A5, A10, Th41, XREAL_1: 44;

      hence thesis by A6, A12, Th29;

    end;

    theorem :: LEXBFS:52

    

     Th52: for G be _finite _Graph, i,j be Nat, v be Vertex of G st j in (((( LexBFS:CSeq G) . i) `2 ) . v) holds ex w be Vertex of G st w in ( dom ((( LexBFS:CSeq G) . i) `1 )) & (((( LexBFS:CSeq G) . i) `1 ) . w) = j & v in (G .AdjacentSet {w})

    proof

      let G be _finite _Graph, i,j be Nat;

      let v be Vertex of G;

      set CSI = (( LexBFS:CSeq G) . i);

      set VLI = ((( LexBFS:CSeq G) ``1 ) . i);

      set V2I = (CSI `2 );

      set n = ((G .order() ) -' j);

      set CSN = (( LexBFS:CSeq G) . n);

      set VLN = (CSN `1 );

      

       A1: (G .order() ) = (( LexBFS:CSeq G) .Lifespan() ) by Th37;

      

       A2: (( LexBFS:CSeq G) .Lifespan() ) = ((( LexBFS:CSeq G) ``1 ) .Lifespan() ) by Th39;

      assume

       A3: j in (V2I . v);

      then

      consider w be Vertex of G such that

       A4: ( LexBFS:PickUnnumbered CSN) = w and not w in ( dom VLN) and

       A5: v in (G .AdjacentSet {w}) by Th48;

      

       A6: (V2I . v) c= (( Seg (G .order() )) \ ( Seg ((G .order() ) -' i))) by Th43;

      then

       A7: ((G .order() ) -' i) < j by A3, Th3;

      

       A8: j <= (G .order() ) by A3, A6, Th3;

      then

       A9: ((G .order() ) -' j) = ((G .order() ) - j) by XREAL_1: 233;

      then

       A10: n < (G .order() ) by A7, XREAL_1: 44;

      

       A11: ((G .order() ) - n) = ((G .order() ) - ((G .order() ) - j)) by A8, XREAL_1: 233;

      then ((G .order() ) - i) < ((G .order() ) - n) by A7, XREAL_0:def 2;

      then (((G .order() ) - i) + i) < (((G .order() ) - n) + i) by XREAL_1: 6;

      then ((G .order() ) + n) < ((((G .order() ) + i) - n) + n) by XREAL_1: 6;

      then

       A12: ((n + (G .order() )) - (G .order() )) < ((i + (G .order() )) - (G .order() )) by XREAL_1: 9;

      

       A13: w = ((( LexBFS:CSeq G) ``1 ) .PickedAt n) by A4, A7, A9, Th41, XREAL_1: 44;

      then

       A14: (VLI . w) = ((G .order() ) -' n) by A10, A1, A2, A12, Th21;

      

       A15: (CSI `1 ) = VLI by Def15;

      then w in ( dom (CSI `1 )) by A10, A1, A2, A13, A12, Th21;

      hence thesis by A15, A5, A10, A11, A14, XREAL_1: 233;

    end;

    definition

      let G be _Graph, F be PartFunc of ( the_Vertices_of G), NAT ;

      :: LEXBFS:def18

      attr F is with_property_L3 means for a,b,c be Vertex of G st a in ( dom F) & b in ( dom F) & c in ( dom F) & (F . a) < (F . b) & (F . b) < (F . c) & (a,c) are_adjacent & not (b,c) are_adjacent holds ex d be Vertex of G st d in ( dom F) & (F . c) < (F . d) & (b,d) are_adjacent & not (a,d) are_adjacent & for e be Vertex of G st e <> d & (e,b) are_adjacent & not (e,a) are_adjacent holds (F . e) < (F . d);

    end

    theorem :: LEXBFS:53

    

     Th53: for G be _finite _Graph, n be Nat holds ((( LexBFS:CSeq G) . n) `1 ) is with_property_L3

    proof

      let G be _finite _Graph, i be Nat;

      set CSi = (( LexBFS:CSeq G) . i);

      set VLi = ((( LexBFS:CSeq G) ``1 ) . i);

      

       A1: (CSi `1 ) = VLi by Def15;

      now

        

         A2: (( LexBFS:CSeq G) .Lifespan() ) = ((( LexBFS:CSeq G) ``1 ) .Lifespan() ) by Th39;

        

         A3: (( LexBFS:CSeq G) .Lifespan() ) = (G .order() ) by Th37;

        let a,b,c be Vertex of G such that

         A4: a in ( dom VLi) and

         A5: b in ( dom VLi) and

         A6: c in ( dom VLi) and

         A7: (VLi . a) < (VLi . b) and

         A8: (VLi . b) < (VLi . c) and

         A9: (a,c) are_adjacent and

         A10: not (b,c) are_adjacent ;

        defpred P[ Nat] means ex v be Vertex of G st v in ( dom VLi) & (b,v) are_adjacent & not (a,v) are_adjacent & (VLi . c) < (VLi . v) & (VLi . v) = $1;

        

         A11: (VLi . a) < (VLi . c) by A7, A8, XXREAL_0: 2;

        now

          set kc = ((G .order() ) -' (VLi . c));

          set k = ((G .order() ) -' (VLi . b));

          assume

           A12: for d be Vertex of G st d in ( dom VLi) & (VLi . c) < (VLi . d) & (d,b) are_adjacent holds (d,a) are_adjacent ;

          set VLc = ((( LexBFS:CSeq G) ``1 ) . kc);

          set CSc = (( LexBFS:CSeq G) . kc);

          set VLb = ((( LexBFS:CSeq G) ``1 ) . k);

          set CSb = (( LexBFS:CSeq G) . k);

          reconsider sb = ((CSb `2 ) . b), sa = ((CSb `2 ) . a) as finite Subset of NAT ;

          

           A13: (( Seg (G .order() )) \ ( Seg ((G .order() ) -' k))) c= ( Seg (G .order() )) by XBOOLE_1: 36;

          sb c= (( Seg (G .order() )) \ ( Seg ((G .order() ) -' k))) by Th43;

          then

           A14: sb c= ( Seg (G .order() )) by A13;

          

           A15: (CSc `1 ) = VLc by Def15;

          sa c= (( Seg (G .order() )) \ ( Seg ((G .order() ) -' k))) by Th43;

          then

           A16: sa c= ( Seg (G .order() )) by A13;

          

           A17: c in ( dom VLb) by A5, A6, A8, A3, A2, Th23;

          

           A18: (VLi . c) <= (G .order() ) by A3, A2, Th15;

          then

           A19: ((G .order() ) -' (VLi . c)) = ((G .order() ) - (VLi . c)) by XREAL_1: 233;

          then

           A20: kc < (G .order() ) by A8, XREAL_1: 44;

          then

           A21: ((G .order() ) -' kc) = ((G .order() ) - ((G .order() ) - (VLi . c))) by A19, XREAL_1: 233;

           A22:

          now

            

             A23: ( rng VLc) = (( Seg (G .order() )) \ ( Seg ((G .order() ) -' kc))) by A3, A2, Th14;

            

             A24: (VLi . a) < (VLi . c) by A7, A8, XXREAL_0: 2;

            assume

             A25: a in ( dom VLc);

            then (VLc . a) in ( rng VLc) by FUNCT_1:def 3;

            then (VLi . c) < (VLc . a) by A21, A23, Th3;

            hence contradiction by A4, A25, A24, Th19;

          end;

          ((( LexBFS:CSeq G) ``1 ) .PickedAt kc) = c by A6, A3, A2, Th20;

          then

           A26: c = ( LexBFS:PickUnnumbered CSc) by A8, A19, Th41, XREAL_1: 44;

          

           A27: kc < k by A8, A18, Th2;

          set j = (VLb . c);

          

           A28: (CSb `1 ) = VLb by Def15;

          a in (G .AdjacentSet {c}) by A7, A8, A9, CHORD: 52;

          then (VLi . c) in sa by A15, A20, A27, A26, A21, A22, Th45;

          then

           A29: (VLb . c) in sa by A6, A17, Th19;

          

           A30: not b in (G .AdjacentSet {c}) by A10, CHORD: 52;

           A31:

          now

            assume (VLb . c) in sb;

            then

             A32: ex z be Vertex of G st z in ( dom VLb) & (VLb . z) = (VLb . c) & b in (G .AdjacentSet {z}) by A28, Th52;

            VLb is one-to-one by Th18;

            hence contradiction by A30, A17, A32, FUNCT_1:def 4;

          end;

          then (((sb,1) -bag ) . j) = 0 by UPROOTS: 6;

          then

           A33: (((sb,1) -bag ) . j) < (((sa,1) -bag ) . j) by A29, UPROOTS: 7;

           [((sb,1) -bag ), ((sa,1) -bag )] in ( InvLexOrder NAT )

          proof

            per cases ;

              suppose for k be Ordinal st j in k & k in NAT holds (((sb,1) -bag ) . k) = (((sa,1) -bag ) . k);

              hence thesis by A33, BAGORDER:def 6;

            end;

              suppose

               A34: not for k be Ordinal st j in k & k in NAT holds (((sb,1) -bag ) . k) = (((sa,1) -bag ) . k);

              defpred M[ Nat] means j in $1 & (((sb,1) -bag ) . $1) <> (((sa,1) -bag ) . $1);

              

               A35: for k be Nat st M[k] holds k <= (G .order() )

              proof

                let k be Nat such that

                 A36: M[k];

                

                 A37: (((sa,1) -bag ) . k) = 1 or (((sa,1) -bag ) . k) = 0 by UPROOTS: 6, UPROOTS: 7;

                k in NAT by ORDINAL1:def 12;

                then

                consider ok be Ordinal such that

                 A38: ok = k and j in ok and ok in NAT and

                 A39: (((sb,1) -bag ) . ok) <> (((sa,1) -bag ) . ok) by A36;

                per cases ;

                  suppose not ok in sb;

                  then ok in sa by A38, A39, A37, UPROOTS: 6;

                  hence thesis by A16, A38, FINSEQ_1: 1;

                end;

                  suppose ok in sb;

                  hence thesis by A14, A38, FINSEQ_1: 1;

                end;

              end;

              

               A40: ex k be Nat st M[k] by A34;

              consider mm be Nat such that

               A41: M[mm] and

               A42: for i be Nat st M[i] holds i <= mm from NAT_1:sch 6( A35, A40);

              reconsider mm as Element of NAT by ORDINAL1:def 12;

               A43:

              now

                let k be Ordinal such that

                 A44: mm in k and

                 A45: k in NAT ;

                reconsider kk = k as Element of NAT by A45;

                mm in { y where y be Nat : y < kk } by A44, AXIOMS: 4;

                then

                 A46: ex mmy be Nat st mmy = mm & mmy < kk;

                assume (((sb,1) -bag ) . k) <> (((sa,1) -bag ) . k);

                hence contradiction by A41, A42, A44, A46, ORDINAL1: 10;

              end;

              j in { y where y be Nat : y < mm } by A41, AXIOMS: 4;

              then

               A47: ex jy be Nat st jy = j & jy < mm;

               A48:

              now

                assume

                 A49: (((sb,1) -bag ) . mm) = 1;

                then mm in sb by UPROOTS: 6;

                then

                consider z be Vertex of G such that

                 A50: z in ( dom (CSb `1 )) and

                 A51: ((CSb `1 ) . z) = mm and

                 A52: b in (G .AdjacentSet {z}) by Th52;

                set kc = ((G .order() ) -' (VLi . z));

                

                 A53: (VLi . z) <= (G .order() ) by A3, A2, Th15;

                then

                 A54: ((G .order() ) -' (VLi . z)) = ((G .order() ) - (VLi . z)) by XREAL_1: 233;

                k < i by A5, A3, A2, Th22;

                then

                 A55: (CSb `1 ) c= (CSi `1 ) by A1, A28, Th17;

                then

                 A56: ( dom (CSb `1 )) c= ( dom (CSi `1 )) by RELAT_1: 11;

                then

                 A57: 0 < (VLi . z) by A1, A50, Th15;

                then

                 A58: kc < (G .order() ) by A54, XREAL_1: 44;

                then

                 A59: ((G .order() ) -' kc) = ((G .order() ) - ((G .order() ) - (VLi . z))) by A54, XREAL_1: 233;

                set VLc = ((( LexBFS:CSeq G) ``1 ) . kc);

                set CSc = (( LexBFS:CSeq G) . kc);

                z = ((( LexBFS:CSeq G) ``1 ) .PickedAt kc) by A1, A3, A2, A50, A56, Th20;

                then

                 A60: z = ( LexBFS:PickUnnumbered CSc) by A57, A54, Th41, XREAL_1: 44;

                

                 A61: [z, mm] in (CSb `1 ) by A50, A51, FUNCT_1:def 2;

                then

                 A62: (VLi . z) = mm by A1, A50, A55, A56, FUNCT_1:def 2;

                

                 A63: [c, j] in (CSb `1 ) by A28, A17, FUNCT_1:def 2;

                then

                 A64: (VLi . c) = j by A1, A6, A55, FUNCT_1:def 2;

                then (VLi . b) < (VLi . z) by A8, A47, A62, XXREAL_0: 2;

                then

                 A65: kc < k by A53, Th2;

                

                 A66: (VLi . c) < (VLi . z) by A1, A47, A50, A55, A56, A61, A64, FUNCT_1:def 2;

                 A67:

                now

                  (VLi . a) < (VLi . c) by A7, A8, XXREAL_0: 2;

                  then

                   A68: (VLi . a) < (VLi . z) by A66, XXREAL_0: 2;

                  

                   A69: ( rng VLc) = (( Seg (G .order() )) \ ( Seg ((G .order() ) -' kc))) by A3, A2, Th14;

                  assume

                   A70: a in ( dom VLc);

                  then (VLc . a) in ( rng VLc) by FUNCT_1:def 3;

                  then (VLi . z) < (VLc . a) by A59, A69, Th3;

                  hence contradiction by A4, A70, A68, Th19;

                end;

                

                 A71: (VLi . c) < (VLi . z) by A1, A6, A47, A55, A62, A63, FUNCT_1:def 2;

                (b,z) are_adjacent by A52, CHORD: 52;

                then (z,a) are_adjacent by A1, A12, A47, A50, A56, A62, A64;

                then

                 A72: a in (G .AdjacentSet {z}) by A11, A71, CHORD: 52;

                (CSc `1 ) = VLc by Def15;

                then ((G .order() ) -' kc) in ((CSb `2 ) . a) by A72, A58, A65, A60, A67, Th45;

                hence contradiction by A41, A49, A62, A59, UPROOTS: 7;

              end;

              (((sb,1) -bag ) . mm) = 0 or (((sb,1) -bag ) . mm) = 1 by UPROOTS: 6, UPROOTS: 7;

              hence thesis by A41, A48, A43, BAGORDER:def 6;

            end;

          end;

          then

           A73: ((sb,1) -bag ) <= (((sa,1) -bag ),( InvLexOrder NAT )) by TERMORD:def 2;

          ((sb,1) -bag ) <> ((sa,1) -bag ) by A29, A31, Th6;

          then

           A74: ((sb,1) -bag ) < (((sa,1) -bag ),( InvLexOrder NAT )) by A73, TERMORD:def 3;

          ((sa,1) -bag ) <= (((sb,1) -bag ),( InvLexOrder NAT )) by A1, A4, A5, A7, Th51;

          hence contradiction by A74, TERMORD: 5;

        end;

        then

         A75: ex k be Nat st P[k];

        

         A76: for k be Nat st P[k] holds k <= (G .order() )

        proof

          let k be Nat;

          assume P[k];

          then k in ( rng VLi) by FUNCT_1:def 3;

          then

           A77: k in (( Seg (G .order() )) \ ( Seg ((G .order() ) -' i))) by A3, A2, Th14;

          (( Seg (G .order() )) \ ( Seg ((G .order() ) -' i))) c= ( Seg (G .order() )) by XBOOLE_1: 36;

          hence thesis by A77, FINSEQ_1: 1;

        end;

        ex k be Nat st P[k] & for n be Nat st P[n] holds n <= k from NAT_1:sch 6( A76, A75);

        then

        consider k be Nat such that

         A78: P[k] and

         A79: for n be Nat st P[n] holds n <= k;

        consider v be Vertex of G such that

         A80: v in ( dom VLi) and

         A81: (b,v) are_adjacent and

         A82: not (a,v) are_adjacent and

         A83: (VLi . c) < (VLi . v) and

         A84: (VLi . v) = k by A78;

        for d be Vertex of G st d <> v & (d,b) are_adjacent & not (d,a) are_adjacent holds (VLi . d) < (VLi . v)

        proof

          let d be Vertex of G such that

           A85: d <> v and

           A86: (d,b) are_adjacent and

           A87: not (d,a) are_adjacent ;

          per cases ;

            suppose (VLi . d) <= (VLi . c);

            hence thesis by A83, XXREAL_0: 2;

          end;

            suppose

             A88: (VLi . c) < (VLi . d);

            then

             A89: d in ( dom VLi) by FUNCT_1:def 2;

            VLi is one-to-one by Th18;

            then

             A90: (VLi . d) <> (VLi . v) by A80, A85, A89, FUNCT_1:def 4;

            (VLi . d) <= k by A79, A86, A87, A88, A89;

            hence thesis by A84, A90, XXREAL_0: 1;

          end;

        end;

        hence ex d be Vertex of G st d in ( dom VLi) & (VLi . c) < (VLi . d) & (b,d) are_adjacent & not (a,d) are_adjacent & for e be Vertex of G st e <> d & (e,b) are_adjacent & not (e,a) are_adjacent holds (VLi . e) < (VLi . d) by A80, A81, A82, A83;

      end;

      hence thesis by A1;

    end;

    theorem :: LEXBFS:54

    

     Th54: for G be _finite chordal _Graph, L be PartFunc of ( the_Vertices_of G), NAT st L is with_property_L3 & ( dom L) = ( the_Vertices_of G) holds for V be VertexScheme of G st (V " ) = L holds V is perfect

    proof

      let G be _finite chordal _Graph, L be PartFunc of ( the_Vertices_of G), NAT such that

       A1: L is with_property_L3 and

       A2: ( dom L) = ( the_Vertices_of G);

      let V be VertexScheme of G such that

       A3: (V " ) = L;

      

       A4: V is one-to-one by CHORD:def 12;

      

       A5: for x,y be Vertex of G, i,j be Nat st i in ( dom V) & j in ( dom V) & (V /. i) = x & (V /. j) = y holds i < j iff (L . x) < (L . y)

      proof

        let x,y be Vertex of G;

        let i,j be Nat such that

         A6: i in ( dom V) and

         A7: j in ( dom V) and

         A8: (V /. i) = x and

         A9: (V /. j) = y;

        (V . j) = y by A7, A9, PARTFUN1:def 6;

        then

         A10: (L . y) = j by A3, A4, A7, FUNCT_1: 34;

        

         A11: (V . i) = x by A6, A8, PARTFUN1:def 6;

        hence i < j implies (L . x) < (L . y) by A3, A4, A6, A10, FUNCT_1: 34;

        thus thesis by A3, A4, A6, A11, A10, FUNCT_1: 34;

      end;

      defpred R[ Nat] means ex P be Walk of G, v1,v2,v3,v4 be Vertex of G st P is Path-like & P is open & P is chordless & (P .length() ) = ($1 - 1) & v1 = (P . (( len P) - 2)) & v2 = (P . 3) & v3 = (P .last() ) & v4 = (P .first() ) & (L . v4) > (L . v3) & (L . v3) > (L . v2) & (L . v2) > (L . v1) & (for x be set st x in (P .vertices() ) holds (L . x) <= (L . v4)) & for x be Vertex of G st x <> v4 & (x,v2) are_adjacent & not (x,v1) are_adjacent holds (L . x) < (L . v4);

      

       A12: for k be Nat st 4 <= k & R[k] holds R[(k + 1)]

      proof

        

         A13: ((2 * 0 ) + 1) < ((2 * 1) + 1);

        let kk be Nat such that

         A14: 4 <= kk and

         A15: R[kk];

        reconsider k = kk as non zero Nat by A14;

        consider P be Walk of G, v1,v2,v3,v4 be Vertex of G such that

         A16: P is Path-like and

         A17: P is open and

         A18: P is chordless and

         A19: (P .length() ) = (k - 1) and

         A20: v1 = (P . (( len P) - 2)) and

         A21: v2 = (P . 3) and

         A22: v3 = (P .last() ) and

         A23: v4 = (P .first() ) and

         A24: (L . v4) > (L . v3) and

         A25: (L . v3) > (L . v2) and

         A26: (L . v2) > (L . v1) and

         A27: for x be set st x in (P .vertices() ) holds (L . x) <= (L . v4) and

         A28: for x be Vertex of G st x <> v4 & (x,v2) are_adjacent & not (x,v1) are_adjacent holds (L . x) < (L . v4) by A15;

        

         A29: ( len P) = ((2 * (k - 1)) + 1) by A19, GLIB_001: 112;

        (2 * k) >= (2 * 4) by A14, XREAL_1: 64;

        then

         A30: ((2 * k) - 1) >= (8 - 1) by XREAL_1: 9;

        then 1 <= ( len P) by A29, XXREAL_0: 2;

        then

         A31: ( len P) in ( dom P) by FINSEQ_3: 25;

        now

          

           A32: ((2 * 0 ) + 1) < ( len P) by A29, A30, XXREAL_0: 2;

          let e be object;

          assume e Joins (v4,v3,G);

          then (1 + 2) = ( len P) by A16, A17, A18, A22, A23, A32, CHORD: 92;

          hence contradiction by A14, A29;

        end;

        then

         A33: not (v4,v3) are_adjacent by CHORD:def 3;

        3 < ( len P) by A29, A30, XXREAL_0: 2;

        then ex ez be object st ez Joins ((P . 1),(P . 3),G) by A16, A17, A18, A13, CHORD: 92;

        then (v4,v2) are_adjacent by A21, A23, CHORD:def 3;

        then

        consider v5 be Vertex of G such that v5 in ( dom L) and

         A34: (L . v4) < (L . v5) and

         A35: (v5,v3) are_adjacent and

         A36: not (v5,v2) are_adjacent and

         A37: for x be Vertex of G st x <> v5 & (x,v3) are_adjacent & not (x,v2) are_adjacent holds (L . x) < (L . v5) by A1, A2, A24, A25, A33;

        consider e be object such that

         A38: e Joins ((P .last() ),v5,G) by A22, A35, CHORD:def 3;

        now

          (L . v2) < (L . v4) by A24, A25, XXREAL_0: 2;

          then

           A39: (L . v2) < (L . v5) by A34, XXREAL_0: 2;

          assume (v5,v1) are_adjacent ;

          then

          consider v6 be Vertex of G such that v6 in ( dom L) and

           A40: (L . v5) < (L . v6) and

           A41: (v6,v2) are_adjacent and

           A42: not (v6,v1) are_adjacent and for x be Vertex of G st x <> v6 & (x,v2) are_adjacent & not (x,v1) are_adjacent holds (L . x) < (L . v6) by A1, A2, A26, A36, A39;

          thus contradiction by A28, A34, A40, A41, A42, XXREAL_0: 2;

        end;

        then

         A43: not ex e be object st e Joins ((P . (( len P) - 2)),v5,G) by A20, CHORD:def 3;

        set Qr = (P .addEdge e);

        set Q = (Qr .reverse() );

        

         A44: ( len Q) = ( len Qr) by GLIB_001: 21;

        

         A45: not v5 in (P .vertices() ) by A27, A34;

        then Qr is open by A16, A17, A18, A38, A43, CHORD: 97;

        then

         A46: Q is open by GLIB_001: 120;

        3 <= ( len P) by A29, A30, XXREAL_0: 2;

        then

         A47: 3 in ( dom P) by FINSEQ_3: 25;

        then

         A48: 3 in ( dom Qr) by A38, Lm6;

        v2 = (Qr . 3) by A21, A38, A47, Lm6;

        then

         A49: v2 = (Q . ((( len Q) - 3) + 1)) by A48, A44, GLIB_001: 24;

        v4 = (Qr .first() ) by A23, A38, GLIB_001: 63;

        then

         A50: v4 = (Q .last() ) by GLIB_001: 22;

        

         A51: ( len Qr) = (( len P) + 2) by A38, GLIB_001: 64;

        then

         A52: (( len Qr) - 2) in ( dom Qr) by A38, A31, Lm6;

        v3 = (Qr . (( len Qr) - 2)) by A22, A38, A51, A31, Lm6;

        then

         A53: v3 = (Q . ((( len Q) - (( len Qr) - 2)) + 1)) by A52, A44, GLIB_001: 24;

        v5 = (Qr .last() ) by A38, GLIB_001: 63;

        then

         A54: v5 = (Q .first() ) by GLIB_001: 22;

        Qr is chordless by A16, A17, A18, A38, A45, A43, CHORD: 97;

        then

         A55: Q is chordless by CHORD: 91;

        (Qr .length() ) = ((k - 1) + 1) by A19, A38, Lm4;

        then

         A56: (Q .length() ) = ((k + 1) - 1) by Lm5;

         A57:

        now

          let x be set;

          assume x in (Q .vertices() );

          then x in (Qr .vertices() ) by GLIB_001: 92;

          then

           A58: x in ((P .vertices() ) \/ {v5}) by A38, GLIB_001: 95;

          per cases by A58, XBOOLE_0:def 3;

            suppose x in (P .vertices() );

            then (L . x) <= (L . v4) by A27;

            hence (L . x) <= (L . v5) by A34, XXREAL_0: 2;

          end;

            suppose x in {v5};

            hence (L . x) <= (L . v5) by TARSKI:def 1;

          end;

        end;

        Qr is Path-like by A16, A17, A18, A38, A45, A43, CHORD: 97;

        hence thesis by A24, A25, A34, A37, A46, A55, A56, A44, A49, A53, A50, A54, A57;

      end;

      

       A59: 11 <= (11 + (G .order() )) by NAT_1: 11;

      assume not V is perfect;

      then

      consider k be non zero Nat such that

       A60: k <= ( len V) and

       A61: not for H be inducedSubgraph of G, (V .followSet k) holds for v be Vertex of H st v = (V . k) holds v is simplicial by CHORD:def 13;

      consider HH be inducedSubgraph of G, (V .followSet k), hv be Vertex of HH such that

       A62: hv = (V . k) and

       A63: not hv is simplicial by A61;

      consider ha,hb be Vertex of HH such that

       A64: ha <> hb and hv <> ha and hv <> hb and

       A65: (hv,ha) are_adjacent and

       A66: (hv,hb) are_adjacent and

       A67: not (ha,hb) are_adjacent by A63, CHORD: 69;

      

       A68: hv in ( the_Vertices_of HH);

      

       A69: hb in ( the_Vertices_of HH);

      ha in ( the_Vertices_of HH);

      then

      reconsider v = hv, aa = ha, bb = hb as Vertex of G by A68, A69;

      

       A70: (V .followSet k) is non empty Subset of ( the_Vertices_of G) by A60, CHORD: 107;

      then

       A71: ( the_Vertices_of HH) = (V .followSet k) by GLIB_000:def 37;

      now

        

         A72: (L . aa) <> (L . bb) by A2, A3, A4, A64, FUNCT_1:def 4;

        per cases by A72, XXREAL_0: 1;

          suppose

           A73: (L . aa) < (L . bb);

          take aa, bb;

          thus aa in (V .followSet k) by A71;

          thus (L . aa) < (L . bb) by A73;

          thus (v,aa) are_adjacent by A65, A70, CHORD: 45;

          thus (v,bb) are_adjacent by A66, A70, CHORD: 45;

          thus not (aa,bb) are_adjacent by A67, A70, CHORD: 45;

        end;

          suppose

           A74: (L . aa) > (L . bb);

          take bb, aa;

          thus bb in (V .followSet k) by A71;

          thus (L . aa) > (L . bb) by A74;

          thus (v,bb) are_adjacent by A66, A70, CHORD: 45;

          thus (v,aa) are_adjacent by A65, A70, CHORD: 45;

          thus not (bb,aa) are_adjacent by A67, A70, CHORD: 45;

        end;

      end;

      then

      consider a,bb be Vertex of G such that

       A75: a in (V .followSet k) and

       A76: (L . a) < (L . bb) and

       A77: (v,a) are_adjacent and

       A78: (v,bb) are_adjacent and

       A79: not (a,bb) are_adjacent ;

      defpred Q[ Nat] means $1 in ( dom V) & (L . a) < (L . (V /. $1)) & a <> (V /. $1) & (v,(V /. $1)) are_adjacent & not (a,(V /. $1)) are_adjacent ;

      

       A80: ( rng V) = ( the_Vertices_of G) by CHORD:def 12;

      

       A81: ex k be Nat st Q[k]

      proof

        consider mbb be object such that

         A82: mbb in ( dom V) and

         A83: bb = (V . mbb) by A80, FUNCT_1:def 3;

        reconsider mbb as Element of NAT by A82;

        take mbb;

        thus mbb in ( dom V) by A82;

        thus (L . a) < (L . (V /. mbb)) by A76, A82, A83, PARTFUN1:def 6;

        thus a <> (V /. mbb) by A76, A82, A83, PARTFUN1:def 6;

        thus (v,(V /. mbb)) are_adjacent by A78, A82, A83, PARTFUN1:def 6;

        thus thesis by A79, A82, A83, PARTFUN1:def 6;

      end;

      

       A84: for k be Nat st Q[k] holds k <= ( len V) by FINSEQ_3: 25;

      consider mb be Nat such that

       A85: Q[mb] and for n be Nat st Q[n] holds n <= mb from NAT_1:sch 6( A84, A81);

      reconsider v, a, b = (V /. mb) as Vertex of G;

      consider ma be object such that

       A86: ma in ( dom V) and

       A87: a = (V . ma) by A80, FUNCT_1:def 3;

      reconsider ma as Element of NAT by A86;

      

       A88: a = (V /. ma) by A86, A87, PARTFUN1:def 6;

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

      then

       A89: k in ( dom V) by A60, FINSEQ_3: 25;

       A90:

      now

        assume ma <= k;

        then

         A91: ma < k by A62, A78, A79, A87, XXREAL_0: 1;

        a in ( the_Vertices_of G);

        then

         A92: a in ( rng V) by CHORD:def 12;

        V is one-to-one by CHORD:def 12;

        then (a .. V) >= k by A75, A89, A92, CHORD: 16;

        then (a .. V) > ma by A91, XXREAL_0: 2;

        hence contradiction by A86, A87, FINSEQ_4: 24;

      end;

      

       A93: v = (V /. k) by A62, A89, PARTFUN1:def 6;

      then

       A94: (L . v) < (L . a) by A5, A89, A86, A88, A90;

      

       A95: v <> b by A77, A85;

      

       A96: R[4]

      proof

        

         A97: (L . a) > (L . v) by A5, A89, A93, A86, A88, A90;

        consider c be Vertex of G such that c in ( dom L) and

         A98: (L . b) < (L . c) and

         A99: (c,a) are_adjacent and

         A100: not (c,v) are_adjacent and

         A101: for x be Vertex of G st x <> c & (x,a) are_adjacent & not (x,v) are_adjacent holds (L . x) < (L . c) by A1, A2, A85, A94;

        consider P be Path of G, e1,e2 be object such that

         A102: P is open and

         A103: ( len P) = 5 and

         A104: (P .length() ) = 2 and e1 Joins (b,v,G) and e2 Joins (v,a,G) and (P .edges() ) = {e1, e2} and

         A105: (P .vertices() ) = {b, v, a} and

         A106: (P . 1) = b and

         A107: (P . 3) = v and

         A108: (P . 5) = a by A77, A85, A95, CHORD: 47;

        consider e be object such that

         A109: e Joins ((P .last() ),c,G) by A99, A103, A108, CHORD:def 3;

        set Qr = (P .addEdge e);

        set Q = (Qr .reverse() );

        

         A110: (Qr .last() ) = c by A109, GLIB_001: 63;

        

         A111: ( len Qr) = (5 + 2) by A103, A109, GLIB_001: 64;

        then

         A112: 1 in ( dom Qr) by FINSEQ_3: 25;

        5 in ( dom P) by A103, FINSEQ_3: 25;

        then

         A113: (Qr . 5) = a by A108, A109, GLIB_001: 65;

        5 in ( dom Qr) by A111, FINSEQ_3: 25;

        then

         A114: a = (Q . ((7 - 5) + 1)) by A111, A113, GLIB_001: 24;

        7 in ( dom Qr) by A111, FINSEQ_3: 25;

        then c = (Q . ((7 - 7) + 1)) by A111, A110, GLIB_001: 24;

        then

         A115: c = (Q .first() );

        3 in ( dom P) by A103, FINSEQ_3: 25;

        then

         A116: (Qr . 3) = v by A107, A109, GLIB_001: 65;

        (Qr .length() ) = (2 + 1) by A104, A109, Lm4;

        then

         A117: (Q .length() ) = ((3 + 1) - 1) by Lm5;

        1 in ( dom P) by A103, FINSEQ_3: 25;

        then (Qr . 1) = b by A106, A109, GLIB_001: 65;

        then b = (Q . ((( len Qr) - 1) + 1)) by A112, GLIB_001: 24;

        then

         A118: b = (Q .last() ) by GLIB_001: 21;

        

         A119: ( len Q) = ( len Qr) by GLIB_001: 21;

        

         A120: (P .first() ) = b by A106;

        (P .last() ) = a by A103, A108;

        then

         A121: P is chordless by A85, A103, A120, CHORD: 90;

         A122:

        now

          let x be set such that

           A123: x in (P .vertices() );

          per cases by A105, A123, ENUMSET1:def 1;

            suppose x = b;

            hence (L . x) <= (L . b);

          end;

            suppose x = v;

            hence (L . x) <= (L . b) by A85, A94, XXREAL_0: 2;

          end;

            suppose x = a;

            hence (L . x) <= (L . b) by A85;

          end;

        end;

        then

         A124: not c in (P .vertices() ) by A98;

        

         A125: not ex e be object st e Joins ((P . (( len P) - 2)),c,G) by A100, A103, A107, CHORD:def 3;

        then Qr is open by A102, A121, A109, A124, CHORD: 97;

        then

         A126: Q is open by GLIB_001: 120;

         A127:

        now

          let x be set;

          assume x in (Q .vertices() );

          then x in (Qr .vertices() ) by GLIB_001: 92;

          then

           A128: x in ((P .vertices() ) \/ {c}) by A109, GLIB_001: 95;

          per cases by A128, XBOOLE_0:def 3;

            suppose x in (P .vertices() );

            then (L . x) <= (L . b) by A122;

            hence (L . x) <= (L . c) by A98, XXREAL_0: 2;

          end;

            suppose x in {c};

            hence (L . x) <= (L . c) by TARSKI:def 1;

          end;

        end;

        3 in ( dom Qr) by A111, FINSEQ_3: 25;

        then v = (Q . ((7 - 3) + 1)) by A111, A116, GLIB_001: 24;

        then

         A129: v = (Q . (( len Q) - 2)) by A111, A119;

        Qr is chordless by A102, A121, A109, A124, A125, CHORD: 97;

        then

         A130: Q is chordless by CHORD: 91;

        Qr is Path-like by A102, A121, A109, A124, A125, CHORD: 97;

        hence thesis by A85, A98, A101, A126, A130, A117, A114, A129, A118, A115, A97, A127;

      end;

      for i be Nat st 4 <= i holds R[i] from NAT_1:sch 8( A96, A12);

      then R[((G .order() ) + 11)] by A59, XXREAL_0: 2;

      then

      consider P be Walk of G, v1,v2,v3,v4 be Vertex of G such that

       A131: P is Path-like and P is open and P is chordless and

       A132: (P .length() ) = (((G .order() ) + 11) - 1) and v1 = (P . (( len P) - 2)) and v2 = (P . 3) and v3 = (P .last() ) and v4 = (P .first() ) and (L . v4) > (L . v3) and (L . v3) > (L . v2) and (L . v2) > (L . v1) and for x be Vertex of G st x <> v4 & (x,v2) are_adjacent & not (x,v1) are_adjacent holds (L . x) < (L . v4);

      ( len P) = ((2 * ((G .order() ) + 10)) + 1) by A132, GLIB_001: 112;

      then (((2 * (G .order() )) + 21) + 1) = (2 * ( len (P .vertexSeq() ))) by GLIB_001:def 14;

      then ((G .order() ) + 11) <= ((G .order() ) + 1) by A131, GLIB_001: 154;

      hence contradiction by XREAL_1: 8;

    end;

    theorem :: LEXBFS:55

    for G be _finite chordal _Graph holds (((( LexBFS:CSeq G) .Result() ) `1 ) " ) is perfect VertexScheme of G

    proof

      let G be _finite chordal _Graph;

      set Hh = ((( LexBFS:CSeq G) .Result() ) `1 );

      reconsider V = (Hh " ) as VertexScheme of G by Th50;

      

       A1: ( dom Hh) = ( the_Vertices_of G) by Th49;

      Hh = ((( LexBFS:CSeq G) ``1 ) .Result() ) by Th40;

      then Hh is one-to-one by Th18;

      then

       A2: (V " ) = Hh by FUNCT_1: 43;

      Hh is with_property_L3 by Th53;

      hence thesis by A1, A2, Th54;

    end;

    begin

    definition

      let G be _Graph;

      mode MCS:Labeling of G is Element of [:( PFuncs (( the_Vertices_of G), NAT )), ( Funcs (( the_Vertices_of G), NAT )):];

    end

    definition

      let G be _finite _Graph;

      :: LEXBFS:def19

      func MCS:Init (G) -> MCS:Labeling of G equals [ {} , (( the_Vertices_of G) --> 0 )];

      coherence

      proof

        set f = (( the_Vertices_of G) --> 0 );

        

         A1: ( rng {} ) c= NAT ;

        

         A2: ( rng f) c= NAT ;

        ( dom f) = ( the_Vertices_of G);

        then

         A3: f in ( Funcs (( the_Vertices_of G), NAT )) by A2, FUNCT_2:def 2;

        ( dom {} ) c= ( the_Vertices_of G);

        then {} in ( PFuncs (( the_Vertices_of G), NAT )) by A1, PARTFUN1:def 3;

        hence thesis by A3, ZFMISC_1:def 2;

      end;

    end

    definition

      let G be _finite _Graph, L be MCS:Labeling of G;

      :: LEXBFS:def20

      func MCS:PickUnnumbered (L) -> Vertex of G means

      : Def19: it = the Element of ( the_Vertices_of G) if ( dom (L `1 )) = ( the_Vertices_of G)

      otherwise ex S be finite non empty natural-membered set, F be Function st S = ( rng F) & F = ((L `2 ) | (( the_Vertices_of G) \ ( dom (L `1 )))) & it = the Element of (F " {( max S)});

      existence

      proof

        set VG = ( the_Vertices_of G);

        set V2G = (L `2 );

        set VLG = (L `1 );

        set F = (V2G | (VG \ ( dom VLG)));

        set S = ( rng F);

        per cases ;

          suppose ( dom VLG) = VG;

          hence thesis;

        end;

          suppose

           A1: ( dom VLG) <> VG;

          

           A2: ( dom F) = (( dom V2G) /\ (VG \ ( dom VLG))) by RELAT_1: 61;

          ( dom V2G) = VG by FUNCT_2:def 1;

          then

           A3: ( dom F) = ((VG /\ VG) \ ( dom VLG)) by A2, XBOOLE_1: 49;

          now

            assume ( dom F) = {} ;

            then VG c= ( dom VLG) by A3, XBOOLE_1: 37;

            hence contradiction by A1, XBOOLE_0:def 10;

          end;

          then

          reconsider S as non empty finite natural-membered set by RELAT_1: 42;

          set y = ( max S);

          set IT = the Element of (F " {( max S)});

          y in S by XXREAL_2:def 8;

          then (F " {( max S)}) is non empty by FUNCT_1: 72;

          then IT in ( dom F) by FUNCT_1:def 7;

          then IT in ( dom V2G) by RELAT_1: 57;

          then

          reconsider IT as Vertex of G;

          ex S be finite non empty natural-membered set, F be Function st S = ( rng F) & F = ((L `2 ) | (( the_Vertices_of G) \ ( dom (L `1 )))) & IT = the Element of (F " {( max S)}) & IT is Vertex of G;

          hence thesis;

        end;

      end;

      uniqueness ;

      consistency ;

    end

    definition

      let G be _finite _Graph, L be MCS:Labeling of G, v be set;

      :: LEXBFS:def21

      func MCS:LabelAdjacent (L,v) -> MCS:Labeling of G equals [(L `1 ), ((L `2 ) .incSubset (((G .AdjacentSet {v}) \ ( dom (L `1 ))),1))];

      coherence

      proof

        set V2G = (L `2 );

        set VLG = (L `1 );

        set f = (V2G .incSubset (((G .AdjacentSet {v}) \ ( dom VLG)),1));

        for x be object st x in ( rng f) holds x in NAT by ORDINAL1:def 12;

        then

         A1: ( rng f) c= NAT ;

        ( dom f) = ( dom V2G) by Def3;

        then ( dom f) = ( the_Vertices_of G) by FUNCT_2:def 1;

        then f is Function of ( the_Vertices_of G), NAT by A1, FUNCT_2: 2;

        then f in ( Funcs (( the_Vertices_of G), NAT )) by FUNCT_2: 8;

        hence thesis by ZFMISC_1: 87;

      end;

    end

    definition

      let G be _finite _Graph, L be MCS:Labeling of G, v be Vertex of G, n be Nat;

      :: LEXBFS:def22

      func MCS:Update (L,v,n) -> MCS:Labeling of G means

      : Def21: ex M be MCS:Labeling of G st M = [((L `1 ) +* (v .--> ((G .order() ) -' n))), (L `2 )] & it = ( MCS:LabelAdjacent (M,v));

      existence

      proof

        set k = ((G .order() ) -' n);

        set L1 = ((L `1 ) +* (v .--> k));

        

         A1: ( dom L1) = (( dom (L `1 )) \/ {v}) by Lm1;

        ( rng L1) c= (( rng (L `1 )) \/ ( rng (v .--> k))) by FUNCT_4: 17;

        then ( rng L1) c= NAT by XBOOLE_1: 1;

        then L1 in ( PFuncs (( the_Vertices_of G), NAT )) by A1, PARTFUN1:def 3;

        then

        reconsider M = [L1, (L `2 )] as MCS:Labeling of G by ZFMISC_1: 87;

        ( MCS:LabelAdjacent (M,v)) is MCS:Labeling of G;

        hence thesis;

      end;

      uniqueness ;

    end

    definition

      let G be _finite _Graph, L be MCS:Labeling of G;

      :: LEXBFS:def23

      func MCS:Step (L) -> MCS:Labeling of G equals

      : Def22: L if (G .order() ) <= ( card ( dom (L `1 )))

      otherwise ( MCS:Update (L,( MCS:PickUnnumbered L),( card ( dom (L `1 )))));

      coherence ;

      consistency ;

    end

    definition

      let G be _Graph;

      :: LEXBFS:def24

      mode MCS:LabelingSeq of G -> ManySortedSet of NAT means

      : Def23: for n be Nat holds (it . n) is MCS:Labeling of G;

      existence

      proof

        set L = the MCS:Labeling of G;

        deffunc F( object) = L;

        consider f be ManySortedSet of NAT such that

         A1: for i be object st i in NAT holds (f . i) = F(i) from PBOOLE:sch 4;

        take f;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

    end

    definition

      let G be _Graph, S be MCS:LabelingSeq of G, n be Nat;

      :: original: .

      redefine

      func S . n -> MCS:Labeling of G ;

      coherence by Def23;

    end

    definition

      let G be _Graph, S be MCS:LabelingSeq of G;

      :: original: .Result()

      redefine

      func S .Result() -> MCS:Labeling of G ;

      coherence by Def23;

    end

    definition

      let G be _finite _Graph, S be MCS:LabelingSeq of G;

      :: LEXBFS:def25

      func S ``1 -> preVNumberingSeq of G means

      : Def24: for n be Nat holds (it . n) = ((S . n) `1 );

      existence

      proof

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

        consider f be ManySortedSet of NAT such that

         A1: for i be object st i in NAT holds (f . i) = F(i) from PBOOLE:sch 4;

        now

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          then (f . i) = ((S . i) `1 ) by A1;

          hence (f . i) is PartFunc of ( the_Vertices_of G), NAT ;

        end;

        then

        reconsider f as preVNumberingSeq of G by Def7;

        take f;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let it1,it2 be preVNumberingSeq of G such that

         A2: for n be Nat holds (it1 . n) = ((S . n) `1 ) and

         A3: for n be Nat holds (it2 . n) = ((S . n) `1 );

        now

          let i be object;

          assume i in NAT ;

          then

          reconsider i9 = i as Nat;

          

          thus (it1 . i) = ((S . i9) `1 ) by A2

          .= (it2 . i) by A3;

        end;

        hence it1 = it2 by PBOOLE: 3;

      end;

    end

    definition

      let G be _finite _Graph;

      :: LEXBFS:def26

      func MCS:CSeq (G) -> MCS:LabelingSeq of G means

      : Def25: (it . 0 ) = ( MCS:Init G) & for n be Nat holds (it . (n + 1)) = ( MCS:Step (it . n));

      existence

      proof

        defpred P[ set, set, set] means ($2 is MCS:Labeling of G & $1 is Nat & ex nn be Nat, Gn,Gn1 be MCS:Labeling of G st $1 = nn & $2 = Gn & $3 = Gn1 & Gn1 = ( MCS:Step Gn)) or (( not $2 is MCS:Labeling of G or not $1 is Nat) & $2 = $3);

        now

          let n,x be set;

          now

            per cases ;

              suppose

               A1: x is MCS:Labeling of G & n is Nat;

              then

              reconsider Gn = x as MCS:Labeling of G;

              ex SGn be MCS:Labeling of G st SGn = ( MCS:Step Gn);

              hence ex y be set st P[n, x, y] by A1;

            end;

              suppose not x is MCS:Labeling of G or not n is Nat;

              hence ex y be set st P[n, x, y];

            end;

          end;

          hence ex y be set st P[n, x, y];

        end;

        then

         A2: for n be Nat holds for x be set holds ex y be set st P[n, x, y];

        consider IT be Function such that

         A3: ( dom IT) = NAT & (IT . 0 ) = ( MCS:Init G) & for n be Nat holds P[n, (IT . n), (IT . (n + 1))] from RECDEF_1:sch 1( A2);

        reconsider IT as ManySortedSet of NAT by A3, PARTFUN1:def 2, RELAT_1:def 18;

        defpred P2[ Nat] means (IT . $1) is MCS:Labeling of G;

         A4:

        now

          let n be Nat;

          assume

           A5: P2[n];

          ex nn be Nat, Gn,Gn1 be MCS:Labeling of G st n = nn & (IT . n) = Gn & (IT . (n + 1)) = Gn1 & Gn1 = ( MCS:Step Gn) by A3, A5;

          hence P2[(n + 1)];

        end;

        

         A6: P2[ 0 ] by A3;

        for n be Nat holds P2[n] from NAT_1:sch 2( A6, A4);

        then

        reconsider IT as MCS:LabelingSeq of G by Def23;

        take IT;

        thus (IT . 0 ) = ( MCS:Init G) by A3;

        let n be Nat;

        ex nn be Nat, Gn,Gn1 be MCS:Labeling of G st n = nn & (IT . n) = Gn & (IT . (n + 1)) = Gn1 & Gn1 = ( MCS:Step Gn) by A3;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be MCS:LabelingSeq of G such that

         A7: (IT1 . 0 ) = ( MCS:Init G) and

         A8: for n be Nat holds (IT1 . (n + 1)) = ( MCS:Step (IT1 . n)) and

         A9: (IT2 . 0 ) = ( MCS:Init G) and

         A10: for n be Nat holds (IT2 . (n + 1)) = ( MCS:Step (IT2 . n));

        defpred P[ Nat] means (IT1 . $1) = (IT2 . $1);

        now

          let n be Nat;

          assume P[n];

          

          then (IT1 . (n + 1)) = ( MCS:Step (IT2 . n)) by A8

          .= (IT2 . (n + 1)) by A10;

          hence P[(n + 1)];

        end;

        then

         A11: for n be Nat st P[n] holds P[(n + 1)];

        

         A12: P[ 0 ] by A7, A9;

        for n be Nat holds P[n] from NAT_1:sch 2( A12, A11);

        then for n be object st n in NAT holds (IT1 . n) = (IT2 . n);

        hence IT1 = IT2 by PBOOLE: 3;

      end;

    end

    theorem :: LEXBFS:56

    

     Th56: for G be _finite _Graph holds ( MCS:CSeq G) is iterative

    proof

      let G be _finite _Graph;

      set CS = ( MCS:CSeq G);

      let k,n be Nat;

      (CS . (k + 1)) = ( MCS:Step (CS . k)) by Def25;

      hence thesis by Def25;

    end;

    registration

      let G be _finite _Graph;

      cluster ( MCS:CSeq G) -> iterative;

      coherence by Th56;

    end

    theorem :: LEXBFS:57

    for G be _finite _Graph, v be set holds ((( MCS:Init G) `2 ) . v) = 0 ;

    theorem :: LEXBFS:58

    

     Th58: for G be _finite _Graph, L be MCS:Labeling of G, x be set st not x in ( dom (L `1 )) & ( dom (L `1 )) <> ( the_Vertices_of G) holds ((L `2 ) . x) <= ((L `2 ) . ( MCS:PickUnnumbered L))

    proof

      let G be _finite _Graph, L be MCS:Labeling of G, x be set such that

       A1: not x in ( dom (L `1 )) and

       A2: ( dom (L `1 )) <> ( the_Vertices_of G);

      set VG = ( the_Vertices_of G);

      set V2G = (L `2 );

      set VLG = (L `1 );

      set w = ( MCS:PickUnnumbered L);

      consider S be finite non empty natural-membered set, F be Function such that

       A3: S = ( rng F) and

       A4: F = (V2G | (VG \ ( dom VLG))) and

       A5: w = the Element of (F " {( max S)}) by A2, Def19;

      

       A6: ( dom F) = (( dom V2G) /\ (VG \ ( dom VLG))) by A4, RELAT_1: 61;

      set y = ( max S);

      y in ( rng F) by A3, XXREAL_2:def 8;

      then

       A7: (F " {( max S)}) is non empty by FUNCT_1: 72;

      then w in ( dom F) by A5, FUNCT_1:def 7;

      then

       A8: (V2G . w) = (F . w) by A4, FUNCT_1: 47;

      (F . w) in {( max S)} by A5, A7, FUNCT_1:def 7;

      then

       A9: (V2G . w) = y by A8, TARSKI:def 1;

      

       A10: ( dom (L `2 )) = ( the_Vertices_of G) by FUNCT_2:def 1;

      per cases ;

        suppose x in ( the_Vertices_of G);

        then x in (VG \ ( dom VLG)) by A1, XBOOLE_0:def 5;

        then

         A11: x in ( dom F) by A10, A6, XBOOLE_0:def 4;

        then

         A12: (F . x) in S by A3, FUNCT_1:def 3;

        (F . x) = (V2G . x) by A4, A11, FUNCT_1: 47;

        hence thesis by A9, A12, XXREAL_2:def 8;

      end;

        suppose not x in ( the_Vertices_of G);

        hence thesis by A10, FUNCT_1:def 2;

      end;

    end;

    theorem :: LEXBFS:59

    

     Th59: for G be _finite _Graph, L be MCS:Labeling of G st ( dom (L `1 )) <> ( the_Vertices_of G) holds not ( MCS:PickUnnumbered L) in ( dom (L `1 ))

    proof

      let G be _finite _Graph, L be MCS:Labeling of G such that

       A1: ( dom (L `1 )) <> ( the_Vertices_of G);

      set VG = ( the_Vertices_of G);

      set V2G = (L `2 );

      set VLG = (L `1 );

      set w = ( MCS:PickUnnumbered L);

      consider S be finite non empty natural-membered set, F be Function such that

       A2: S = ( rng F) and

       A3: F = (V2G | (VG \ ( dom VLG))) and

       A4: w = the Element of (F " {( max S)}) by A1, Def19;

      set y = ( max S);

      y in ( rng F) by A2, XXREAL_2:def 8;

      then (F " {( max S)}) is non empty by FUNCT_1: 72;

      then

       A5: w in ( dom F) by A4, FUNCT_1:def 7;

      assume w in ( dom VLG);

      then

       A6: not w in (VG \ ( dom VLG)) by XBOOLE_0:def 5;

      ( dom F) = (( dom V2G) /\ (VG \ ( dom VLG))) by A3, RELAT_1: 61;

      hence contradiction by A5, A6, XBOOLE_0:def 4;

    end;

    theorem :: LEXBFS:60

    

     Th60: for G be _finite _Graph, L be MCS:Labeling of G, v,x be set st not x in (G .AdjacentSet {v}) holds ((L `2 ) . x) = ((( MCS:LabelAdjacent (L,v)) `2 ) . x)

    proof

      let G be _finite _Graph, L be MCS:Labeling of G, v,x be set such that

       A1: not x in (G .AdjacentSet {v});

      set V2G = (L `2 );

      set VLG = (L `1 );

      set GL = ( MCS:LabelAdjacent (L,v));

      set V2 = (GL `2 );

       not x in ((G .AdjacentSet {v}) \ ( dom VLG)) by A1, XBOOLE_0:def 5;

      hence thesis by Def3;

    end;

    theorem :: LEXBFS:61

    

     Th61: for G be _finite _Graph, L be MCS:Labeling of G, v,x be set st x in ( dom (L `1 )) holds ((L `2 ) . x) = ((( MCS:LabelAdjacent (L,v)) `2 ) . x)

    proof

      let G be _finite _Graph, L be MCS:Labeling of G, v,x be set such that

       A1: x in ( dom (L `1 ));

      set V2G = (L `2 );

      set VLG = (L `1 );

      set GL = ( MCS:LabelAdjacent (L,v));

      set V2 = (GL `2 );

       not x in ((G .AdjacentSet {v}) \ ( dom VLG)) by A1, XBOOLE_0:def 5;

      hence thesis by Def3;

    end;

    theorem :: LEXBFS:62

    

     Th62: for G be _finite _Graph, L be MCS:Labeling of G, v,x be set st x in ( dom (L `2 )) & x in (G .AdjacentSet {v}) & not x in ( dom (L `1 )) holds ((( MCS:LabelAdjacent (L,v)) `2 ) . x) = (((L `2 ) . x) + 1)

    proof

      let G be _finite _Graph, L be MCS:Labeling of G, v,x be set such that

       A1: x in ( dom (L `2 )) and

       A2: x in (G .AdjacentSet {v}) and

       A3: not x in ( dom (L `1 ));

      set V2G = (L `2 );

      set VLG = (L `1 );

      set GL = ( MCS:LabelAdjacent (L,v));

      set V2 = (GL `2 );

      x in ((G .AdjacentSet {v}) \ ( dom VLG)) by A2, A3, XBOOLE_0:def 5;

      hence thesis by A1, Def3;

    end;

    theorem :: LEXBFS:63

    for G be _finite _Graph, L be MCS:Labeling of G, v be set st ( dom (L `2 )) = ( the_Vertices_of G) holds ( dom (( MCS:LabelAdjacent (L,v)) `2 )) = ( the_Vertices_of G) by Def3;

    theorem :: LEXBFS:64

    

     Th64: for G be _finite _Graph, n be Nat st ( card ( dom ((( MCS:CSeq G) . n) `1 ))) < (G .order() ) holds ((( MCS:CSeq G) . (n + 1)) `1 ) = (((( MCS:CSeq G) . n) `1 ) +* (( MCS:PickUnnumbered (( MCS:CSeq G) . n)) .--> ((G .order() ) -' ( card ( dom ((( MCS:CSeq G) . n) `1 ))))))

    proof

      let G be _finite _Graph, n be Nat such that

       A1: ( card ( dom ((( MCS:CSeq G) . n) `1 ))) < (G .order() );

      set CN1 = (( MCS:CSeq G) . (n + 1));

      set CSN = (( MCS:CSeq G) . n);

      set VLN = (CSN `1 );

      set w = ( MCS:PickUnnumbered CSN);

      set k = ((G .order() ) -' ( card ( dom VLN)));

      CN1 = ( MCS:Step CSN) by Def25;

      then CN1 = ( MCS:Update (CSN,w,( card ( dom VLN)))) by A1, Def22;

      then

      consider L be MCS:Labeling of G such that

       A2: L = [((CSN `1 ) +* (w .--> k)), (CSN `2 )] and

       A3: CN1 = ( MCS:LabelAdjacent (L,w)) by Def21;

      (CN1 `1 ) = ( [((CSN `1 ) +* (w .--> k)), (CSN `2 )] `1 ) by A3, A2;

      hence thesis;

    end;

    theorem :: LEXBFS:65

    

     Th65: for G be _finite _Graph, n be Nat st n <= (G .order() ) holds ( card ( dom ((( MCS:CSeq G) . n) `1 ))) = n

    proof

      let G be _finite _Graph, n be Nat such that

       A1: n <= (G .order() );

      defpred P[ Nat] means $1 <= (G .order() ) implies ( card ( dom ((( MCS:CSeq G) . $1) `1 ))) = $1;

      

       A2: for k be Element of NAT st k < (G .order() ) & ( card ( dom ((( MCS:CSeq G) . k) `1 ))) = k holds ( card ( dom ((( MCS:CSeq G) . (k + 1)) `1 ))) = (k + 1)

      proof

        let k be Element of NAT such that

         A3: k < (G .order() ) and

         A4: ( card ( dom ((( MCS:CSeq G) . k) `1 ))) = k;

        set CK1 = (( MCS:CSeq G) . (k + 1));

        set CSK = (( MCS:CSeq G) . k);

        set VLK = (CSK `1 );

        set VK1 = (CK1 `1 );

        set w = ( MCS:PickUnnumbered CSK);

        set wf = (w .--> ((G .order() ) -' k));

        

         A5: ( dom wf) = {w};

        VK1 = (VLK +* (w .--> ((G .order() ) -' k))) by A3, A4, Th64;

        then ( dom VK1) = (( dom VLK) \/ {w}) by A5, FUNCT_4:def 1;

        hence thesis by A3, A4, Th59, CARD_2: 41;

      end;

      

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

      proof

        let k be Nat such that

         A7: P[k];

        per cases ;

          suppose k < (G .order() );

          hence thesis by A2, A7;

        end;

          suppose k >= (G .order() );

          hence thesis by NAT_1: 13;

        end;

      end;

      (( MCS:CSeq G) . 0 ) = ( MCS:Init G) by Def25;

      then

       A8: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A8, A6);

      hence thesis by A1;

    end;

    theorem :: LEXBFS:66

    

     Th66: for G be _finite _Graph, n be Nat st (G .order() ) <= n holds (( MCS:CSeq G) . (G .order() )) = (( MCS:CSeq G) . n)

    proof

      let G be _finite _Graph, n be Nat;

      assume (G .order() ) <= n;

      then

       A1: ex i be Nat st ((G .order() ) + i) = n by NAT_1: 10;

      set CS = ( MCS:CSeq G);

      defpred V[ Nat] means (G .order() ) = ( card ( dom ((CS . ((G .order() ) + $1)) `1 )));

      defpred P[ Nat] means (CS . (G .order() )) = (CS . ((G .order() ) + $1));

      

       A2: for k be Nat st V[k] holds V[(k + 1)]

      proof

        let k be Nat such that

         A3: V[k];

        set CK1 = (( MCS:CSeq G) . (((G .order() ) + k) + 1));

        set CSK = (( MCS:CSeq G) . ((G .order() ) + k));

        CK1 = ( MCS:Step CSK) by Def25;

        hence thesis by A3, Def22;

      end;

      

       A4: V[ 0 ] by Th65;

      

       A5: for k be Nat holds V[k] from NAT_1:sch 2( A4, A2);

      

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

      proof

        let k be Nat such that

         A7: P[k];

        set CK1 = (( MCS:CSeq G) . (((G .order() ) + k) + 1));

        set CSK = (( MCS:CSeq G) . ((G .order() ) + k));

        set VLK = (CSK `1 );

        

         A8: CK1 = ( MCS:Step CSK) by Def25;

        ( card ( dom VLK)) = (G .order() ) by A5;

        hence thesis by A7, A8, Def22;

      end;

      

       A9: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A9, A6);

      hence thesis by A1;

    end;

    theorem :: LEXBFS:67

    

     Th67: for G be _finite _Graph, m,n be Nat st (G .order() ) <= m & m <= n holds (( MCS:CSeq G) . m) = (( MCS:CSeq G) . n)

    proof

      let G be _finite _Graph, m,n be Nat such that

       A1: (G .order() ) <= m and

       A2: m <= n;

      (( MCS:CSeq G) . m) = (( MCS:CSeq G) . (G .order() )) by A1, Th66;

      hence thesis by A1, A2, Th66, XXREAL_0: 2;

    end;

    theorem :: LEXBFS:68

    

     Th68: for G be _finite _Graph holds ( MCS:CSeq G) is eventually-constant

    proof

      let G be _finite _Graph;

      take (G .order() );

      let m be Nat;

      assume (G .order() ) <= m;

      hence (( MCS:CSeq G) . (G .order() )) = (( MCS:CSeq G) . m) by Th66;

    end;

    registration

      let G be _finite _Graph;

      cluster ( MCS:CSeq G) -> eventually-constant;

      coherence by Th68;

    end

    theorem :: LEXBFS:69

    

     Th69: for G be _finite _Graph, n be Nat holds ( dom ((( MCS:CSeq G) . n) `1 )) = ( the_Vertices_of G) iff (G .order() ) <= n

    proof

      let G be _finite _Graph, n be Nat;

      set VLN = ((( MCS:CSeq G) . n) `1 );

      set CSO = (( MCS:CSeq G) . (G .order() ));

      set VLO = (CSO `1 );

      thus ( dom VLN) = ( the_Vertices_of G) implies not n < (G .order() ) by Th65;

      ( card ( dom VLO)) = ( card ( the_Vertices_of G)) by Th65;

      then

       A1: ( dom VLO) = ( the_Vertices_of G) by CARD_2: 102;

      assume (G .order() ) <= n;

      hence thesis by A1, Th67;

    end;

    theorem :: LEXBFS:70

    

     Th70: for G be _finite _Graph holds (( MCS:CSeq G) .Lifespan() ) = (G .order() )

    proof

      let G be _finite _Graph;

      set CS = ( MCS:CSeq G);

      

       A1: for n be Nat st (CS . n) = (CS . (n + 1)) holds (G .order() ) <= n

      proof

        let n be Nat such that

         A2: (CS . n) = (CS . (n + 1));

        set w = ( MCS:PickUnnumbered (CS . n));

        set VN1 = ((CS . (n + 1)) `1 );

        set VLN = ((CS . n) `1 );

        set j = ( card ( dom VLN));

        set wf = (w .--> ((G .order() ) -' j));

        assume

         A3: n < (G .order() );

        then ( dom VLN) <> ( the_Vertices_of G) by Th69;

        then

         A4: not w in ( dom VLN) by Th59;

        j < (G .order() ) by A3, Th65;

        then

         A5: VN1 = (VLN +* (w .--> ((G .order() ) -' j))) by Th64;

        ( dom wf) = {w};

        then

         A6: ( dom VN1) = (( dom VLN) \/ {w}) by A5, FUNCT_4:def 1;

        w in {w} by TARSKI:def 1;

        hence contradiction by A2, A4, A6, XBOOLE_0:def 3;

      end;

      (G .order() ) <= ((G .order() ) + 1) by NAT_1: 13;

      then (CS . (G .order() )) = (CS . ((G .order() ) + 1)) by Th66;

      hence thesis by A1, GLIB_000:def 56;

    end;

    theorem :: LEXBFS:71

    

     Th71: for G be _finite _Graph holds (( MCS:CSeq G) ``1 ) is eventually-constant

    proof

      let G be _finite _Graph;

      set CS = ( MCS:CSeq G);

      set S = (CS ``1 );

      now

        consider n be Nat such that

         A1: for m be Nat st n <= m holds (CS . n) = (CS . m) by Def6;

        take n;

        let m be Nat such that

         A2: n <= m;

        

        thus (S . n) = ((CS . n) `1 ) by Def24

        .= ((CS . m) `1 ) by A1, A2

        .= (S . m) by Def24;

      end;

      hence thesis;

    end;

    theorem :: LEXBFS:72

    

     Th72: for G be _finite _Graph holds ((( MCS:CSeq G) ``1 ) .Lifespan() ) = (( MCS:CSeq G) .Lifespan() )

    proof

      let G be _finite _Graph;

      set S = ( MCS:CSeq G);

      set VN = (S ``1 );

      set ls = (G .order() );

      

       A1: VN is eventually-constant by Th71;

      

       A2: ((S . (ls + 1)) `1 ) = ((S ``1 ) . (ls + 1)) by Def24;

       A3:

      now

        let n be Nat such that

         A4: (VN . n) = (VN . (n + 1)) and

         A5: ls > n;

        (n + 1) <= ls by A5, NAT_1: 13;

        then

         A6: ( card ( dom ((S . (n + 1)) `1 ))) = (n + 1) by Th65;

        

         A7: ((S . (n + 1)) `1 ) = (VN . (n + 1)) by Def24;

        

         A8: ((S . n) `1 ) = (VN . n) by Def24;

        ( card ( dom ((S . n) `1 ))) = n by A5, Th65;

        hence contradiction by A4, A6, A8, A7;

      end;

      ((S . ls) `1 ) = ((S ``1 ) . ls) by Def24;

      then

       A9: (VN . ls) = (VN . (ls + 1)) by A2, Th66, NAT_1: 11;

      (S .Lifespan() ) = ls by Th70;

      hence thesis by A1, A9, A3, GLIB_000:def 56;

    end;

    theorem :: LEXBFS:73

    

     Th73: for G be _finite _Graph holds (( MCS:CSeq G) ``1 ) is vertex-numbering

    proof

      let G be _finite _Graph;

      set GS = ( MCS:CSeq G);

      set S = (GS ``1 );

      

       A1: (GS . 0 ) = ( MCS:Init G) by Def25;

      (S . 0 ) = ((GS . 0 ) `1 ) by Def24;

      hence (S . 0 ) = {} by A1;

      now

        let k,n be Nat such that

         A2: (S . k) = (S . n);

        

         A3: (S . (k + 1)) = ((GS . (k + 1)) `1 ) by Def24;

        

         A4: (S . k) = ((GS . k) `1 ) by Def24;

        

         A5: (S . (n + 1)) = ((GS . (n + 1)) `1 ) by Def24;

        

         A6: (S . n) = ((GS . n) `1 ) by Def24;

        per cases ;

          suppose

           A7: k <= (G .order() ) & n <= (G .order() );

          then ( card ( dom ((GS . n) `1 ))) = n by Th65;

          hence (S . (k + 1)) = (S . (n + 1)) by A2, A4, A6, A7, Th65;

        end;

          suppose

           A8: k <= (G .order() ) & n >= (G .order() );

          then

           A9: (GS . n) = (GS . (G .order() )) by Th66;

          

           A10: ( card ( dom ((GS . (G .order() )) `1 ))) = (G .order() ) by Th65;

          

           A11: (n + 1) >= (G .order() ) by A8, NAT_1: 13;

          ( card ( dom ((GS . k) `1 ))) = k by A8, Th65;

          then (k + 1) >= (G .order() ) by A2, A4, A6, A9, A10, NAT_1: 13;

          

          hence (S . (k + 1)) = ((GS . (G .order() )) `1 ) by A3, Th66

          .= (S . (n + 1)) by A5, A11, Th66;

        end;

          suppose

           A12: k >= (G .order() ) & n <= (G .order() );

          then

           A13: (GS . k) = (GS . (G .order() )) by Th66;

          

           A14: ( card ( dom ((GS . (G .order() )) `1 ))) = (G .order() ) by Th65;

          ( card ( dom ((GS . n) `1 ))) = n by A12, Th65;

          then

           A15: (n + 1) >= (G .order() ) by A2, A4, A6, A13, A14, NAT_1: 13;

          (k + 1) >= (G .order() ) by A12, NAT_1: 13;

          

          hence (S . (k + 1)) = ((GS . (G .order() )) `1 ) by A3, Th66

          .= (S . (n + 1)) by A5, A15, Th66;

        end;

          suppose

           A16: k >= (G .order() ) & n >= (G .order() );

          then

           A17: (n + 1) >= (G .order() ) by NAT_1: 13;

          

           A18: (k + 1) >= (G .order() ) by A16, NAT_1: 13;

          

          thus (S . (k + 1)) = ((GS . (k + 1)) `1 ) by Def24

          .= ((GS . (G .order() )) `1 ) by A18, Th66

          .= ((GS . (n + 1)) `1 ) by A17, Th66

          .= (S . (n + 1)) by Def24;

        end;

      end;

      hence S is iterative;

      S is eventually-constant by Th71;

      hence S is halting;

      (GS .Lifespan() ) = (S .Lifespan() ) by Th72;

      hence

       A19: (S .Lifespan() ) = (G .order() ) by Th70;

      let n be Nat such that

       A20: n < (S .Lifespan() );

      take w = ( MCS:PickUnnumbered (GS . n));

      

       A21: ((GS . n) `1 ) = (S . n) by Def24;

      then ( dom (S . n)) <> ( the_Vertices_of G) by A19, A20, Th69;

      hence not w in ( dom (S . n)) by A21, Th59;

      

       A22: ((GS . (n + 1)) `1 ) = (S . (n + 1)) by Def24;

      n = ( card ( dom (S . n))) by A19, A20, A21, Th65;

      hence thesis by A19, A20, A21, A22, Th64;

    end;

    registration

      let G be _finite _Graph;

      cluster (( MCS:CSeq G) ``1 ) -> vertex-numbering;

      coherence by Th73;

    end

    theorem :: LEXBFS:74

    

     Th74: for G be _finite _Graph, n be Nat st n < (G .order() ) holds ((( MCS:CSeq G) ``1 ) .PickedAt n) = ( MCS:PickUnnumbered (( MCS:CSeq G) . n))

    proof

      let G be _finite _Graph, n be Nat such that

       A1: n < (G .order() );

      set GS = ( MCS:CSeq G);

      set CSN = (GS . n);

      set CS1 = (GS . (n + 1));

      set VLN = (CSN `1 );

      set VL1 = (CS1 `1 );

      

       A2: (GS .Lifespan() ) = (G .order() ) by Th70;

      set PU = ( MCS:PickUnnumbered CSN);

      set f2 = (PU .--> ((GS .Lifespan() ) -' n));

      

       A3: ( dom f2) = {PU};

      n = ( card ( dom VLN)) by A1, Th65;

      then VL1 = (VLN +* (PU .--> ((GS .Lifespan() ) -' n))) by A1, A2, Th64;

      then

       A4: ( dom VL1) = (( dom VLN) \/ {PU}) by A3, FUNCT_4:def 1;

      

       A5: ((GS ``1 ) .Lifespan() ) = (GS .Lifespan() ) by Th72;

      set PA = ((GS ``1 ) .PickedAt n);

      set f1 = (PA .--> ((GS .Lifespan() ) -' n));

      

       A6: ( dom f1) = {PA};

      

       A7: VLN = ((GS ``1 ) . n) by Def24;

      VL1 = ((GS ``1 ) . (n + 1)) by Def24;

      then VL1 = (VLN +* (PA .--> ((GS .Lifespan() ) -' n))) by A1, A2, A7, A5, Def9;

      then

       A8: ( dom VL1) = (( dom VLN) \/ {PA}) by A6, FUNCT_4:def 1;

      

       A9: not PA in ( dom VLN) by A1, A2, A7, A5, Def9;

      now

        assume PA <> PU;

        then not PA in {PU} by TARSKI:def 1;

        then

         A10: not PA in ( dom VL1) by A9, A4, XBOOLE_0:def 3;

        PA in {PA} by TARSKI:def 1;

        hence contradiction by A8, A10, XBOOLE_0:def 3;

      end;

      hence thesis;

    end;

    theorem :: LEXBFS:75

    

     Th75: for G be _finite _Graph, n be Nat st n < (G .order() ) holds ex w be Vertex of G st w = ( MCS:PickUnnumbered (( MCS:CSeq G) . n)) & for v be set holds (v in (G .AdjacentSet {w}) & not v in ( dom ((( MCS:CSeq G) . n) `1 )) implies (((( MCS:CSeq G) . (n + 1)) `2 ) . v) = ((((( MCS:CSeq G) . n) `2 ) . v) + 1)) & ( not v in (G .AdjacentSet {w}) or v in ( dom ((( MCS:CSeq G) . n) `1 )) implies (((( MCS:CSeq G) . (n + 1)) `2 ) . v) = (((( MCS:CSeq G) . n) `2 ) . v))

    proof

      let G be _finite _Graph, n be Nat such that

       A1: n < (G .order() );

      set CSN = (( MCS:CSeq G) . n);

      set VLN = (CSN `1 );

      

       A2: n = ( card ( dom VLN)) by A1, Th65;

      set k = ((G .order() ) -' n);

      set w = ( MCS:PickUnnumbered CSN);

      set CN1 = (( MCS:CSeq G) . (n + 1));

      set CSlv = [((CSN `1 ) +* (w .--> k)), (CSN `2 )];

      set CSlv1 = ((CSN `1 ) +* (w .--> k));

      

       A3: ( dom CSlv1) = (( dom (CSN `1 )) \/ {w}) by Lm1;

      ( rng CSlv1) c= (( rng (CSN `1 )) \/ ( rng (w .--> k))) by FUNCT_4: 17;

      then ( rng CSlv1) c= NAT by XBOOLE_1: 1;

      then CSlv1 in ( PFuncs (( the_Vertices_of G), NAT )) by A3, PARTFUN1:def 3;

      then

      reconsider CSlv as MCS:Labeling of G by ZFMISC_1:def 2;

      

       A4: CN1 = ( MCS:Step CSN) by Def25

      .= ( MCS:Update (CSN,w,n)) by A1, A2, Def22

      .= ( MCS:LabelAdjacent (CSlv,w)) by Def21;

      take w;

      set V2v = (CSlv `2 );

      set VLv = (CSlv `1 );

      set V21 = (CN1 `2 );

      set V2N = (CSN `2 );

      

       A5: ( dom VLv) = (( dom (CSN `1 )) \/ {w}) by Lm1;

      then

       A6: ( dom VLN) c= ( dom VLv) by XBOOLE_1: 7;

       A7:

      now

        let v be set;

        assume

         A8: not v in (G .AdjacentSet {w}) or v in ( dom VLN);

        per cases by A8;

          suppose not v in (G .AdjacentSet {w});

          hence (V21 . v) = (V2N . v) by A4, Th60;

        end;

          suppose v in ( dom VLN);

          hence (V21 . v) = (V2N . v) by A4, A6, Th61;

        end;

      end;

      

       A9: ( dom V2N) = ( the_Vertices_of G) by FUNCT_2:def 1;

      now

        let v be set;

        assume that

         A10: v in (G .AdjacentSet {w}) and

         A11: not v in ( dom VLN);

         not v in {w} by A10, CHORD: 49;

        then not v in ( dom VLv) by A5, A11, XBOOLE_0:def 3;

        hence (V21 . v) = ((V2N . v) + 1) by A4, A9, A10, Th62;

      end;

      hence thesis by A7;

    end;

    theorem :: LEXBFS:76

    

     Th76: for G be _finite _Graph, n be Nat, x be set st not x in ( dom ((( MCS:CSeq G) . n) `1 )) holds (((( MCS:CSeq G) . n) `2 ) . x) = ( card ((G .AdjacentSet {x}) /\ ( dom ((( MCS:CSeq G) . n) `1 ))))

    proof

      let G be _finite _Graph, n be Nat;

      set CN = (( MCS:CSeq G) . n);

      set VLN = (CN `1 );

      defpred P[ Nat] means for x be set st not x in ( dom ((( MCS:CSeq G) . $1) `1 )) holds (((( MCS:CSeq G) . $1) `2 ) . x) = ( card ((G .AdjacentSet {x}) /\ ( dom ((( MCS:CSeq G) . $1) `1 ))));

      

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

      proof

        let k be Nat such that

         A2: P[k];

        set CS1 = (( MCS:CSeq G) . (k + 1));

        set CSK = (( MCS:CSeq G) . k);

        set VLK = (CSK `1 );

        set VK2 = (CSK `2 );

        set VL1 = (CS1 `1 );

        set V12 = (CS1 `2 );

        

         A3: k <= (k + 1) by XREAL_1: 38;

        per cases ;

          suppose

           A4: (G .order() ) <= k;

          then

           A5: VK2 = V12 by A3, Th67;

          VLK = VL1 by A3, A4, Th67;

          hence thesis by A2, A5;

        end;

          suppose

           A6: k < (G .order() );

          set VL = (( MCS:CSeq G) ``1 );

          

           A7: (G .order() ) = (( MCS:CSeq G) .Lifespan() ) by Th70;

          

           A8: VLK = (VL . k) by Def24;

          

           A9: (( MCS:CSeq G) .Lifespan() ) = (VL .Lifespan() ) by Th72;

          

           A10: VL1 = (VL . (k + 1)) by Def24;

          consider w be Vertex of G such that

           A11: w = ( MCS:PickUnnumbered CSK) and

           A12: for v be set holds (v in (G .AdjacentSet {w}) & not v in ( dom VLK) implies (V12 . v) = ((VK2 . v) + 1)) & ( not v in (G .AdjacentSet {w}) or v in ( dom VLK) implies (V12 . v) = (VK2 . v)) by A6, Th75;

          w = ((( MCS:CSeq G) ``1 ) .PickedAt k) by A6, A11, Th74;

          then

           A13: ( dom (CS1 `1 )) = (( dom (CSK `1 )) \/ {w}) by A6, A7, A8, A10, A9, Th11;

          now

            let x be set such that

             A14: not x in ( dom VL1);

            

             A15: not x in ( dom VLK) by A13, A14, XBOOLE_0:def 3;

            then

             A16: ( card ((G .AdjacentSet {x}) /\ ( dom VLK))) = (VK2 . x) by A2;

            per cases ;

              suppose

               A17: x in (G .AdjacentSet {w}) & not x in ( dom VLK);

              set GAS = (G .AdjacentSet {x});

              w in GAS by A17, CHORD: 53;

              then

               A18: {w} c= GAS by ZFMISC_1: 31;

              

               A19: (GAS /\ ( dom VL1)) = ((GAS /\ ( dom VLK)) \/ (GAS /\ {w})) by A13, XBOOLE_1: 23

              .= ((GAS /\ ( dom VLK)) \/ {w}) by A18, XBOOLE_1: 28;

              ( dom VLK) <> ( the_Vertices_of G) by A6, Th69;

              then not w in ( dom VLK) by A11, Th59;

              then

               A20: not w in (GAS /\ ( dom VLK)) by XBOOLE_0:def 4;

              (V12 . x) = ((VK2 . x) + 1) by A12, A17;

              hence ( card ((G .AdjacentSet {x}) /\ ( dom VL1))) = (V12 . x) by A16, A20, A19, CARD_2: 41;

            end;

              suppose

               A21: not x in (G .AdjacentSet {w}) or x in ( dom VLK);

              set GAS = (G .AdjacentSet {x});

              

               A22: not w in GAS by A13, A14, A21, CHORD: 53, XBOOLE_0:def 3;

               A23:

              now

                assume (GAS /\ {w}) = {w};

                then w in (GAS /\ {w}) by TARSKI:def 1;

                hence contradiction by A22, XBOOLE_0:def 4;

              end;

              (GAS /\ {w}) c= {w} by XBOOLE_1: 17;

              then (GAS /\ {w}) in ( bool {w});

              then

               A24: (GAS /\ {w}) in { {} , {w}} by ZFMISC_1: 24;

              

               A25: (V12 . x) = (VK2 . x) by A12, A21;

              (GAS /\ ( dom VL1)) = ((GAS /\ ( dom VLK)) \/ (GAS /\ {w})) by A13, XBOOLE_1: 23

              .= ((GAS /\ ( dom VLK)) \/ {} ) by A24, A23, TARSKI:def 2

              .= (GAS /\ ( dom VLK));

              hence ( card ((G .AdjacentSet {x}) /\ ( dom VL1))) = (V12 . x) by A2, A15, A25;

            end;

          end;

          hence thesis;

        end;

      end;

      now

        set C0 = (( MCS:CSeq G) . 0 );

        let x be set;

        set VL0 = (C0 `1 );

        set V20 = (C0 `2 );

        assume not x in ( dom VL0);

        

         A26: C0 = ( MCS:Init G) by Def25;

        ( dom VL0) = {} by A26;

        hence (V20 . x) = ( card ((G .AdjacentSet {x}) /\ ( dom VL0))) by A26;

      end;

      then

       A27: P[ 0 ];

      

       A28: for k be Nat holds P[k] from NAT_1:sch 2( A27, A1);

      let x be set;

      assume not x in ( dom VLN);

      hence thesis by A28;

    end;

    definition

      let G be _Graph, F be PartFunc of ( the_Vertices_of G), NAT ;

      :: LEXBFS:def27

      attr F is with_property_T means for a,b,c be Vertex of G st a in ( dom F) & b in ( dom F) & c in ( dom F) & (F . a) < (F . b) & (F . b) < (F . c) & (a,c) are_adjacent & not (b,c) are_adjacent holds ex d be Vertex of G st d in ( dom F) & (F . b) < (F . d) & (b,d) are_adjacent & not (a,d) are_adjacent ;

    end

    theorem :: LEXBFS:77

    for G be _finite _Graph, n be Nat holds ((( MCS:CSeq G) . n) `1 ) is with_property_T

    proof

      let G be _finite _Graph, n be Nat;

      set CN = (( MCS:CSeq G) . n);

      set VLN = (CN `1 );

      set VL = (( MCS:CSeq G) ``1 );

      now

        

         A1: (( MCS:CSeq G) .Lifespan() ) = (VL .Lifespan() ) by Th72;

        

         A2: VLN = (VL . n) by Def24;

        let a,b,c be Vertex of G such that

         A3: a in ( dom VLN) and

         A4: b in ( dom VLN) and

         A5: c in ( dom VLN) and

         A6: (VLN . a) < (VLN . b) and

         A7: (VLN . b) < (VLN . c) and

         A8: (a,c) are_adjacent and

         A9: not (b,c) are_adjacent ;

        

         A10: (G .order() ) = (( MCS:CSeq G) .Lifespan() ) by Th70;

        now

          set bn = ((G .order() ) -' (VLN . b));

          set CSB = (( MCS:CSeq G) . bn);

          set VLB = (CSB `1 );

          set VL2 = (CSB `2 );

           not c in (G .AdjacentSet {b}) by A9, CHORD: 52;

          then

           A11: not c in ((G .AdjacentSet {b}) /\ ( dom VLB)) by XBOOLE_0:def 4;

          

           A12: b = ((( MCS:CSeq G) ``1 ) .PickedAt bn) by A4, A10, A2, A1, Th20;

          

           A13: c in (G .AdjacentSet {a}) by A6, A7, A8, CHORD: 52;

          

           A14: VLB = (VL . bn) by Def24;

          then not a in ( dom VLB) by A3, A6, A10, A2, A1, Th24;

          then

           A15: (VL2 . a) = ( card ((G .AdjacentSet {a}) /\ ( dom VLB))) by Th76;

          bn < n by A4, A10, A2, A1, Th22;

          then VLB c= VLN by A2, A14, Th17;

          then

           A16: ( dom VLB) c= ( dom VLN) by RELAT_1: 11;

          (VLN . b) <= (G .order() ) by A10, A2, A1, Th15;

          then

           A17: ((G .order() ) -' (VLN . b)) = ((G .order() ) - (VLN . b)) by XREAL_1: 233;

          then (VLN . b) = ((G .order() ) - ((G .order() ) -' (VLN . b)));

          then

           A18: (VLN . b) = ((G .order() ) -' ((G .order() ) -' (VLN . b))) by NAT_D: 35, XREAL_1: 233;

           A19:

          now

            assume

             A20: a in ( dom VLB);

            then (VLN . b) < (VLB . a) by A10, A1, A14, A18, Th22;

            hence contradiction by A3, A6, A2, A14, A20, Th19;

          end;

          

           A21: 1 <= (VLN . b) by A4, A2, Th15;

          then

           A22: bn < (G .order() ) by A17, XREAL_1: 44;

          then

           A23: ( dom VLB) <> ( the_Vertices_of G) by Th69;

          assume

           A24: for d be Vertex of G st d in ( dom VLN) & (VLN . b) < (VLN . d) & (b,d) are_adjacent holds (a,d) are_adjacent ;

          now

            set CSB1 = (( MCS:CSeq G) . (bn + 1));

            set VLB1 = (CSB1 `1 );

            let x be object such that

             A25: x in ((G .AdjacentSet {b}) /\ ( dom VLB));

            reconsider d = x as Vertex of G by A25;

            

             A26: x in ( dom VLB) by A25, XBOOLE_0:def 4;

            x in ( dom VLB) by A25, XBOOLE_0:def 4;

            then

             A27: (VLN . d) = (VLB . d) by A2, A14, A16, Th19;

            

             A28: VLB1 = (VL . (bn + 1)) by Def24;

            then b in ( dom VLB1) by A10, A1, A22, A12, Th11;

            then

             A29: (VLN . b) = (VLB1 . b) by A4, A2, A28, Th19;

            bn < (bn + 1) by XREAL_1: 39;

            then VLB c= VLB1 by A14, A28, Th17;

            then ( dom VLB) c= ( dom VLB1) by RELAT_1: 11;

            then

             A30: (VLB . d) = (VLB1 . d) by A14, A26, A28, Th19;

            (VLB . d) in ( rng VLB) by A26, FUNCT_1:def 3;

            then (VLB . d) in (( Seg (G .order() )) \ ( Seg ((G .order() ) -' bn))) by A10, A1, A14, Th14;

            then ((G .order() ) -' bn) < (VLB1 . d) by A30, Th3;

            then

             A31: (VLN . b) < (VLN . d) by A10, A1, A17, A21, A12, A28, A29, A27, A30, Th12, XREAL_1: 44;

            d in (G .AdjacentSet {b}) by A25, XBOOLE_0:def 4;

            then (b,d) are_adjacent by CHORD: 52;

            then (a,d) are_adjacent by A24, A16, A26, A31;

            then d in (G .AdjacentSet {a}) by A6, A31, CHORD: 52;

            hence x in ((G .AdjacentSet {a}) /\ ( dom VLB)) by A26, XBOOLE_0:def 4;

          end;

          then

           A32: ((G .AdjacentSet {b}) /\ ( dom VLB)) c= ((G .AdjacentSet {a}) /\ ( dom VLB));

          c in ( dom VLB) by A4, A5, A7, A10, A2, A1, A14, Th23;

          then c in ((G .AdjacentSet {a}) /\ ( dom VLB)) by A13, XBOOLE_0:def 4;

          then

           A33: ((G .AdjacentSet {b}) /\ ( dom VLB)) c< ((G .AdjacentSet {a}) /\ ( dom VLB)) by A11, A32, XBOOLE_0:def 8;

          

           A34: b = ( MCS:PickUnnumbered CSB) by A17, A21, A12, Th74, XREAL_1: 44;

          then (VL2 . b) = ( card ((G .AdjacentSet {b}) /\ ( dom VLB))) by A23, Th59, Th76;

          hence contradiction by A23, A34, A19, A15, A33, Th58, TREES_1: 6;

        end;

        hence ex d be Vertex of G st d in ( dom VLN) & (VLN . b) < (VLN . d) & (b,d) are_adjacent & not (a,d) are_adjacent ;

      end;

      hence thesis;

    end;

    theorem :: LEXBFS:78

    for G be _finite _Graph holds ((( LexBFS:CSeq G) .Result() ) `1 ) is with_property_T

    proof

      let G be _finite _Graph;

      set CS = ( LexBFS:CSeq G);

      set L = ((CS .Result() ) `1 );

      

       A1: L is with_property_L3 by Th53;

      now

        let a,b,c be Vertex of G such that

         A2: a in ( dom L) and

         A3: b in ( dom L) and

         A4: c in ( dom L) and

         A5: (L . a) < (L . b) and

         A6: (L . b) < (L . c) and

         A7: (a,c) are_adjacent and

         A8: not (b,c) are_adjacent ;

        consider d be Vertex of G such that

         A9: d in ( dom L) and

         A10: (L . c) < (L . d) and

         A11: (b,d) are_adjacent and

         A12: not (a,d) are_adjacent and for e be Vertex of G st e <> d & (e,b) are_adjacent & not (e,a) are_adjacent holds (L . e) < (L . d) by A1, A2, A3, A4, A5, A6, A7, A8;

        take d;

        thus d in ( dom L) by A9;

        thus (L . b) < (L . d) by A6, A10, XXREAL_0: 2;

        thus (b,d) are_adjacent by A11;

        thus not (a,d) are_adjacent by A12;

      end;

      hence thesis;

    end;

    theorem :: LEXBFS:79

    for G be _finite chordal _Graph, L be PartFunc of ( the_Vertices_of G), NAT st L is with_property_T & ( dom L) = ( the_Vertices_of G) holds for V be VertexScheme of G st (V " ) = L holds V is perfect

    proof

      let G be _finite chordal _Graph, L be PartFunc of ( the_Vertices_of G), NAT such that

       A1: L is with_property_T and

       A2: ( dom L) = ( the_Vertices_of G);

      defpred Q[ Path of G] means ( len $1) >= 5 & $1 is open & $1 is chordless & (L . ($1 .first() )) > (L . ($1 .last() )) & (L . ($1 .last() )) > (L . ($1 . 3)) & ex i be odd Element of NAT st 1 < i & i < ( len $1) & (for j,k be odd Element of NAT st i <= j & j < k & k <= ( len $1) holds (L . ($1 . j)) < (L . ($1 . k))) & (for j,k be odd Element of NAT st 1 <= j & j < k & k <= i holds (L . ($1 . j)) > (L . ($1 . k)));

      let V be VertexScheme of G such that

       A3: (V " ) = L;

      

       A4: V is one-to-one by CHORD:def 12;

      ( len V) = ( card ( the_Vertices_of G)) by CHORD: 104;

      then ( dom V) = ( Seg (G .order() )) by FINSEQ_1:def 3;

      then

       A5: ( rng L) = ( Seg (G .order() )) by A3, A4, FUNCT_1: 33;

       A6:

      now

        defpred M[ Nat] means ex P be Path of G st Q[P] & (L . (P .last() )) = $1;

        

         A7: for k be Nat st M[k] holds k <= (G .order() )

        proof

          let k be Nat;

          assume M[k];

          then

          consider P be Path of G such that Q[P] and

           A8: (L . (P .last() )) = k;

          (L . (P .last() )) in ( Seg (G .order() )) by A2, A5, FUNCT_1:def 3;

          hence thesis by A8, FINSEQ_1: 1;

        end;

        let R be Path of G;

        assume Q[R];

        then

         A9: ex k be Nat st M[k];

        consider k be Nat such that

         A10: M[k] and

         A11: for n be Nat st M[n] holds n <= k from NAT_1:sch 6( A7, A9);

        consider P be Path of G such that

         A12: Q[P] and

         A13: (L . (P .last() )) = k by A10;

        3 <= ( len P) by A12, XXREAL_0: 2;

        then (P . 3) = (P .vertexAt ((2 * 1) + 1)) by GLIB_001:def 8;

        then

        reconsider a = (P . 3) as Vertex of G;

        

         A14: 3 < ( len P) by A12, XXREAL_0: 2;

        reconsider b = (P .last() ) as Vertex of G;

        reconsider c = (P .first() ) as Vertex of G;

         A15:

        now

          ((2 * 0 ) + 1) < ( len P) by A12, XXREAL_0: 2;

          then

           A16: (ex e be object st e Joins ((P . 1),(P . ( len P)),G)) iff (1 + 2) = ( len P) by A12, CHORD: 92;

          let e be object;

          assume e Joins (c,b,G);

          hence contradiction by A12, A16;

        end;

        then

         A17: not (b,c) are_adjacent by CHORD:def 3;

        ((2 * 0 ) + 1) < ((2 * 1) + 1);

        then ex ez be object st ez Joins ((P . 1),(P . 3),G) by A12, A14, CHORD: 92;

        then (c,a) are_adjacent by CHORD:def 3;

        then

        consider d be Vertex of G such that d in ( dom L) and

         A18: (L . b) < (L . d) and

         A19: (b,d) are_adjacent and

         A20: not (a,d) are_adjacent by A1, A2, A12, A17;

        

         A21: (L . d) <> (L . c) by A2, A3, A4, A17, A19, FUNCT_1:def 4;

        consider i be odd Element of NAT such that

         A22: 1 < i and i < ( len P) and

         A23: for j,k be odd Element of NAT st i <= j & j < k & k <= ( len P) holds (L . (P . j)) < (L . (P . k)) and

         A24: for j,k be odd Element of NAT st 1 <= j & j < k & k <= i holds (L . (P . j)) > (L . (P . k)) by A12;

        

         A25: (L . a) < (L . d) by A12, A18, XXREAL_0: 2;

         A26:

        now

          assume d in (P .vertices() );

          then

          consider dn be odd Element of NAT such that

           A27: dn <= ( len P) and

           A28: (P . dn) = d by GLIB_001: 87;

          

           A29: 1 <= dn by CHORD: 2;

          dn <> 1 by A15, A19, A28, CHORD:def 3;

          then ((2 * 0 ) + 1) < dn by A29, XXREAL_0: 1;

          then (1 + 2) <= dn by CHORD: 4;

          then

           A30: ((2 * 1) + 1) < dn by A12, A18, A28, XXREAL_0: 1;

          

           A31: dn < ( len P) by A18, A27, A28, XXREAL_0: 1;

          per cases ;

            suppose i <= dn;

            hence contradiction by A23, A18, A28, A31;

          end;

            suppose dn < i;

            hence contradiction by A24, A25, A28, A30;

          end;

        end;

        defpred Mi[ Nat] means $1 is odd & 3 < $1 & $1 <= ( len P) & ex e be object st e Joins ((P . $1),d,G);

        ex el be object st el Joins ((P .last() ),d,G) by A19, CHORD:def 3;

        then

         A32: ex k be Nat st Mi[k] by A14;

        ex j be Nat st Mi[j] & for n be Nat st Mi[n] holds j <= n from NAT_1:sch 5( A32);

        then

        consider j be Nat such that

         A33: j is odd and

         A34: 3 < j and

         A35: j <= ( len P) and

         A36: ex e be object st e Joins ((P . j),d,G) and

         A37: for i be Nat st Mi[i] holds j <= i;

        reconsider j as odd Element of NAT by A33, ORDINAL1:def 12;

        reconsider C = (P .cut (1,j)) as Path of G;

        consider e be object such that

         A38: e Joins ((P . j),d,G) by A36;

        ((2 * 0 ) + 1) < j by A34, XXREAL_0: 2;

        then

         A39: C is open chordless by A12, A35, CHORD: 93;

        

         A40: ((2 * 0 ) + 1) <= j by CHORD: 2;

        then

         A41: (( len C) + 1) = (j + 1) by A35, GLIB_001: 36;

         A42:

        now

          let n be odd Element of NAT such that

           A43: n <= j;

          1 <= n by CHORD: 2;

          then n in ( dom C) by A41, A43, FINSEQ_3: 25;

          then (C . n) = (P . ((1 + n) - 1)) by A35, A40, GLIB_001: 47;

          hence (C . n) = (P . n);

        end;

        ((2 * 1) + 1) < j by A34;

        then

         A44: (C . 3) = a by A42;

         A45:

        now

          ( len C) > ((2 * 1) + 1) by A34, A41;

          then

           A46: ( len C) >= (3 + 2) by CHORD: 4;

          let f be object such that

           A47: f Joins ((C . (( len C) - 2)),d,G);

          ( len C) <> 5 by A20, A44, A47, CHORD:def 3;

          then ( len C) > 5 by A46, XXREAL_0: 1;

          then

           A48: ((3 + 2) - 2) < (( len C) - 2) by XREAL_1: 9;

          then 0 < (( len C) - (2 * 1));

          then

          reconsider cc = (( len C) - 2) as odd Element of NAT by INT_1: 3;

          

           A49: cc < ( len C) by XREAL_1: 44;

          then

           A50: cc < ( len P) by A35, A41, XXREAL_0: 2;

          f Joins ((P . cc),d,G) by A41, A42, A47, A49;

          hence contradiction by A37, A41, A48, A49, A50;

        end;

        

         A51: e Joins ((C .last() ),d,G) by A35, A38, A40, GLIB_001: 37;

        (C .vertices() ) c= (P .vertices() ) by A35, A40, GLIB_001: 94;

        then

         A52: not d in (C .vertices() ) by A26;

        then

        reconsider D = (C .addEdge e) as Path of G by A51, A39, A45, CHORD: 97;

        reconsider R = (D .reverse() ) as Path of G;

        

         A53: (C .last() ) = (P . j) by A35, A40, GLIB_001: 37;

        then

         A54: ( len D) = (( len C) + 2) by A38, GLIB_001: 64;

         A55:

        now

          per cases ;

            suppose

             A56: i < j;

            now

              per cases by A35, XXREAL_0: 1;

                suppose j = ( len P);

                hence (L . (P . j)) <= (L . b);

              end;

                suppose j < ( len P);

                hence (L . (P . j)) <= (L . b) by A23, A56;

              end;

            end;

            hence (L . (P . j)) < (L . c) by A12, XXREAL_0: 2;

          end;

            suppose

             A57: i >= j;

            1 < ((2 * 1) + 1);

            then (L . (P . j)) < (L . (P . 3)) by A24, A34, A57;

            then (L . (P . j)) < (L . b) by A12, XXREAL_0: 2;

            hence (L . (P . j)) < (L . c) by A12, XXREAL_0: 2;

          end;

        end;

        (C .first() ) = (P .first() ) by A35, A40, GLIB_001: 37;

        then

         A58: (D .first() ) = c by A38, A53, GLIB_001: 63;

        then

         A59: (R .last() ) = c by GLIB_001: 22;

        3 in ( dom C) by A34, A41, FINSEQ_3: 25;

        then

         A60: (D . 3) = a by A38, A53, A44, GLIB_001: 65;

        

         A61: D is chordless by A52, A51, A39, A45, CHORD: 97;

        

         A62: (D .last() ) = d by A38, A53, GLIB_001: 63;

        then

         A63: (R .first() ) = d by GLIB_001: 22;

        

         A64: for n be odd Element of NAT st n <= ( len R) holds (R . n) = (D . ((( len D) - n) + 1)) & ((( len D) - n) + 1) is Element of NAT

        proof

          let n be odd Element of NAT such that

           A65: n <= ( len R);

          1 <= n by CHORD: 2;

          then

           A66: n in ( dom R) by A65, FINSEQ_3: 25;

          hence (R . n) = (D . ((( len D) - n) + 1)) by GLIB_001: 25;

          ((( len D) - n) + 1) in ( dom D) by A66, GLIB_001: 25;

          hence thesis;

        end;

         A67:

        now

          let n be odd Nat such that

           A68: n <= j;

          1 <= n by CHORD: 2;

          then n in ( dom C) by A41, A68, FINSEQ_3: 25;

          hence (C . n) = (D . n) by A51, GLIB_001: 65;

        end;

        

         A69: ex i be odd Element of NAT st 1 < i & i < ( len D) & (for j,k be odd Element of NAT st i <= j & j < k & k <= ( len D) holds (L . (D . j)) < (L . (D . k))) & for j,k be odd Element of NAT st 1 <= j & j < k & k <= i holds (L . (D . j)) > (L . (D . k))

        proof

          per cases ;

            suppose

             A70: j <= i;

             A71:

            now

              1 < ((2 * 1) + 1);

              then

               A72: (L . (P . 3)) > (L . (P . j)) by A24, A34, A70;

              let e,f be odd Element of NAT such that

               A73: j <= e and

               A74: e < f and

               A75: f <= ( len D);

              e < (j + (2 * 1)) by A41, A54, A74, A75, XXREAL_0: 2;

              then e <= ((j + 2) - 2) by CHORD: 3;

              then

               A76: e = j by A73, XXREAL_0: 1;

              then (D . e) = (C . j) by A67;

              then

               A77: (D . e) = (P . j) by A42;

              (( len C) + 2) <= f by A41, A74, A76, CHORD: 4;

              then (D . f) = d by A54, A62, A75, XXREAL_0: 1;

              hence (L . (D . e)) < (L . (D . f)) by A25, A77, A72, XXREAL_0: 2;

            end;

            take j;

            now

              let e,f be odd Element of NAT such that

               A78: 1 <= e and

               A79: e < f and

               A80: f <= j;

              (D . e) = (C . e) by A67, A79, A80, XXREAL_0: 2;

              then

               A81: (D . e) = (P . e) by A42, A79, A80, XXREAL_0: 2;

              (D . f) = (C . f) by A67, A80;

              then

               A82: (D . f) = (P . f) by A42, A80;

              f <= i by A70, A80, XXREAL_0: 2;

              hence (L . (D . e)) > (L . (D . f)) by A24, A78, A79, A81, A82;

            end;

            hence thesis by A34, A41, A54, A71, XREAL_1: 29, XXREAL_0: 2;

          end;

            suppose

             A83: i < j;

            take i;

             A84:

            now

              let e,f be odd Element of NAT such that

               A85: i <= e and

               A86: e < f and

               A87: f <= ( len D);

              e < (j + (2 * 1)) by A41, A54, A86, A87, XXREAL_0: 2;

              then

               A88: e <= ((j + 2) - 2) by CHORD: 3;

              then

               A89: e <= ( len P) by A35, XXREAL_0: 2;

              

               A90: (D . e) = (C . e) by A67, A88;

              then

               A91: (D . e) = (P . e) by A42, A88;

              per cases by A87, XXREAL_0: 1;

                suppose

                 A92: f = ( len D);

                now

                  per cases by A89, XXREAL_0: 1;

                    suppose e = ( len P);

                    hence (L . (D . e)) <= (L . b) by A42, A88, A90;

                  end;

                    suppose e < ( len P);

                    hence (L . (D . e)) <= (L . b) by A23, A85, A91;

                  end;

                end;

                hence (L . (D . e)) < (L . (D . f)) by A18, A62, A92, XXREAL_0: 2;

              end;

                suppose f < ( len D);

                then

                 A93: f <= ((j + 2) - 2) by A41, A54, CHORD: 3;

                then (D . f) = (C . f) by A67;

                then

                 A94: (D . f) = (P . f) by A42, A93;

                f <= ( len P) by A35, A93, XXREAL_0: 2;

                hence (L . (D . e)) < (L . (D . f)) by A23, A85, A86, A91, A94;

              end;

            end;

             A95:

            now

              let e,f be odd Element of NAT such that

               A96: 1 <= e and

               A97: e < f and

               A98: f <= i;

              (D . f) = (C . f) by A67, A83, A98, XXREAL_0: 2;

              then

               A99: (D . f) = (P . f) by A42, A83, A98, XXREAL_0: 2;

              

               A100: e <= i by A97, A98, XXREAL_0: 2;

              then (D . e) = (C . e) by A67, A83, XXREAL_0: 2;

              then (D . e) = (P . e) by A42, A83, A100, XXREAL_0: 2;

              hence (L . (D . e)) > (L . (D . f)) by A24, A96, A97, A98, A99;

            end;

            ( len D) > j by A41, A54, XREAL_1: 29;

            hence thesis by A22, A83, A84, A95, XXREAL_0: 2;

          end;

        end;

        

         A101: ex i be odd Element of NAT st 1 < i & i < ( len R) & (for j,k be odd Element of NAT st i <= j & j < k & k <= ( len R) holds (L . (R . j)) < (L . (R . k))) & for j,k be odd Element of NAT st 1 <= j & j < k & k <= i holds (L . (R . j)) > (L . (R . k))

        proof

          consider i be odd Element of NAT such that

           A102: 1 < i and

           A103: i < ( len D) and

           A104: for j,k be odd Element of NAT st i <= j & j < k & k <= ( len D) holds (L . (D . j)) < (L . (D . k)) and

           A105: for j,k be odd Element of NAT st 1 <= j & j < k & k <= i holds (L . (D . j)) > (L . (D . k)) by A69;

          set ir = ((( len D) - i) + 1);

          (( len D) - 1) > (( len D) - i) by A102, XREAL_1: 15;

          then

           A106: ((( len D) - 1) + 1) > ((( len D) - i) + 1) by XREAL_1: 8;

          then

           A107: ir < ( len R) by GLIB_001: 21;

          

           A108: (( len D) - ( len D)) < (( len D) - i) by A103, XREAL_1: 15;

          then

          reconsider ir as odd Element of NAT by INT_1: 3;

           A109:

          now

            let ja,k be odd Element of NAT such that

             A110: 1 <= ja and

             A111: ja < k and

             A112: k <= ir;

            set jr = ((( len D) - ja) + 1);

            

             A113: k <= ( len R) by A107, A112, XXREAL_0: 2;

            then

             A114: ja <= ( len R) by A111, XXREAL_0: 2;

            then

             A115: (R . ja) = (D . jr) by A64;

            (i + k) <= (((( len D) - i) + 1) + i) by A112, XREAL_1: 7;

            then

             A116: ((i + k) - k) <= ((( len D) + 1) - k) by XREAL_1: 9;

            set kr = ((( len D) - k) + 1);

            

             A117: kr < jr by A111, Lm3;

            reconsider jr as odd Element of NAT by A64, A114;

            reconsider kr as odd Element of NAT by A64, A113;

            (( len D) - ja) <= (( len D) - 1) by A110, XREAL_1: 10;

            then jr <= ((( len D) - 1) + 1) by XREAL_1: 7;

            then (L . (D . kr)) < (L . (D . jr)) by A104, A116, A117;

            hence (L . (R . ja)) > (L . (R . k)) by A64, A113, A115;

          end;

          take ir;

           A118:

          now

            let j,k be odd Element of NAT such that

             A119: ir <= j and

             A120: j < k and

             A121: k <= ( len R);

            set kr = ((( len D) - k) + 1);

            

             A122: (R . k) = (D . kr) by A64, A121;

            set jr = ((( len D) - j) + 1);

            

             A123: j <= ( len R) by A120, A121, XXREAL_0: 2;

            then

             A124: (R . j) = (D . jr) by A64;

            reconsider kr as odd Element of NAT by A64, A121;

            (i + j) >= (((( len D) - i) + 1) + i) by A119, XREAL_1: 7;

            then

             A125: ((i + j) - j) >= ((( len D) + 1) - j) by XREAL_1: 9;

            reconsider jr as odd Element of NAT by A64, A123;

            kr < jr by A120, Lm3;

            hence (L . (R . j)) < (L . (R . k)) by A105, A124, A122, A125, CHORD: 2;

          end;

          ( 0 + 1) < ((( len D) - i) + 1) by A108, XREAL_1: 8;

          hence thesis by A106, A118, A109, GLIB_001: 21;

        end;

        

         A126: ( len D) >= (3 + 2) by A34, A41, A54, XREAL_1: 7;

        then

         A127: ( len R) >= (3 + 2) by GLIB_001: 21;

        then 3 <= ( len R) by XXREAL_0: 2;

        then 3 in ( dom R) by FINSEQ_3: 25;

        then (R . 3) = (D . ((( len D) - 3) + 1)) by GLIB_001: 25;

        then (R . 3) = (C . j) by A41, A54, A67;

        then

         A128: (L . (R .last() )) > (L . (R . 3)) by A42, A59, A55;

        d <> c by A15, A19, CHORD:def 3;

        then

         A129: R is open by A63, A59;

        D is open by A52, A51, A39, A45, CHORD: 97;

        then (L . c) <= (L . d) by A11, A13, A18, A25, A61, A126, A58, A62, A60, A69;

        then

         A130: (L . c) < (L . d) by A21, XXREAL_0: 1;

        R is chordless by A61, CHORD: 91;

        hence contradiction by A11, A12, A13, A130, A63, A59, A129, A127, A128, A101;

      end;

      

       A131: (L " ) = V by A3, A4, FUNCT_1: 43;

      now

        let a,b,c be Vertex of G such that

         A132: b <> c and

         A133: (a,b) are_adjacent and

         A134: (a,c) are_adjacent ;

        let va,vb,vc be Nat such that

         A135: va in ( dom V) and

         A136: vb in ( dom V) and

         A137: vc in ( dom V) and

         A138: (V . va) = a and

         A139: (V . vb) = b and

         A140: (V . vc) = c and

         A141: va < vb and

         A142: va < vc;

        

         A143: (L . a) = va by A3, A4, A135, A138, FUNCT_1: 34;

        

         A144: c = (V . (L . c)) by A2, A3, A4, A131, FUNCT_1: 34;

        

         A145: b = (V . (L . b)) by A2, A3, A4, A131, FUNCT_1: 34;

        assume

         A146: not (b,c) are_adjacent ;

        

         A147: (L . b) = vb by A3, A4, A136, A139, FUNCT_1: 34;

        

         A148: (L . c) = vc by A3, A4, A137, A140, FUNCT_1: 34;

        per cases by A132, A145, A144, XXREAL_0: 1;

          suppose

           A149: (L . b) < (L . c);

          

           A150: ((2 * 1) + 1) is odd;

          consider P be Path of G, e1,e2 be object such that

           A151: P is open and

           A152: ( len P) = 5 and (P .length() ) = 2 and e1 Joins (c,a,G) and e2 Joins (a,b,G) and (P .edges() ) = {e1, e2} and (P .vertices() ) = {c, a, b} and

           A153: (P . 1) = c and

           A154: (P . 3) = a and

           A155: (P . 5) = b by A132, A133, A134, A141, A142, A143, A147, A148, CHORD: 47;

          

           A156: (P .first() ) = c by A153;

           A157:

          now

            let j,k be odd Element of NAT such that 1 <= j and

             A158: j < k and

             A159: k <= 3;

            j < 3 by A158, A159, XXREAL_0: 2;

            then j = 1 by CHORD: 7, XXREAL_0: 2;

            hence (L . (P . j)) > (L . (P . k)) by A142, A143, A148, A153, A154, A158, A159, CHORD: 7, XXREAL_0: 2;

          end;

           A160:

          now

            let j,k be odd Element of NAT such that

             A161: 3 <= j and

             A162: j < k and

             A163: k <= ( len P);

            j < 5 by A152, A162, A163, XXREAL_0: 2;

            then j = 1 or j = 3 or j = 5 by CHORD: 8, XXREAL_0: 2;

            hence (L . (P . j)) < (L . (P . k)) by A141, A142, A143, A147, A148, A152, A153, A154, A155, A161, A162, A163, CHORD: 8, XXREAL_0: 2;

          end;

          (P .last() ) = b by A152, A155;

          then Q[P] by A146, A149, A151, A152, A156, A160, A157, A150, CHORD: 90;

          hence contradiction by A6;

        end;

          suppose

           A164: (L . c) < (L . b);

          

           A165: ((2 * 1) + 1) is odd;

          consider P be Path of G, e1,e2 be object such that

           A166: P is open and

           A167: ( len P) = 5 and (P .length() ) = 2 and e1 Joins (b,a,G) and e2 Joins (a,c,G) and (P .edges() ) = {e1, e2} and (P .vertices() ) = {b, a, c} and

           A168: (P . 1) = b and

           A169: (P . 3) = a and

           A170: (P . 5) = c by A132, A133, A134, A141, A142, A143, A147, A148, CHORD: 47;

          

           A171: (P .first() ) = b by A168;

           A172:

          now

            let j,k be odd Element of NAT such that 1 <= j and

             A173: j < k and

             A174: k <= 3;

            j < 3 by A173, A174, XXREAL_0: 2;

            then j = 1 by CHORD: 7, XXREAL_0: 2;

            hence (L . (P . j)) > (L . (P . k)) by A141, A143, A147, A168, A169, A173, A174, CHORD: 7, XXREAL_0: 2;

          end;

           A175:

          now

            let j,k be odd Element of NAT such that

             A176: 3 <= j and

             A177: j < k and

             A178: k <= ( len P);

            j < 5 by A167, A177, A178, XXREAL_0: 2;

            then j = 1 or j = 3 or j = 5 by CHORD: 8, XXREAL_0: 2;

            hence (L . (P . j)) < (L . (P . k)) by A141, A142, A143, A147, A148, A167, A168, A169, A170, A176, A177, A178, CHORD: 8, XXREAL_0: 2;

          end;

          (P .last() ) = c by A167, A170;

          then Q[P] by A146, A164, A166, A167, A171, A175, A172, A165, CHORD: 90;

          hence contradiction by A6;

        end;

      end;

      hence thesis by CHORD: 109;

    end;